Add optimization cases for triage and composition
This commit is contained in:
parent
00cdeca280
commit
6713b05872
11
lib/base.tri
11
lib/base.tri
@ -7,17 +7,14 @@ s = t (t (k t)) t
|
|||||||
m = s i i
|
m = s i i
|
||||||
b = s (k s) k
|
b = s (k s) k
|
||||||
c = s (s (k s) (s (k k) s)) (k k)
|
c = s (s (k s) (s (k k) s)) (k k)
|
||||||
iC = (\a b c : s a (k c) b)
|
|
||||||
iD = b (b iC) iC
|
|
||||||
iE = b (b iD) iC
|
|
||||||
yi = (\i : b m (c b (i m)))
|
|
||||||
y = yi iC
|
|
||||||
yC = yi iD
|
|
||||||
yD = yi iE
|
|
||||||
id = (\a : a)
|
id = (\a : a)
|
||||||
pair = t
|
pair = t
|
||||||
if = (\cond then else : t (t else (t t then)) t cond)
|
if = (\cond then else : t (t else (t t then)) t cond)
|
||||||
|
|
||||||
|
y = ((\mut wait fun : wait mut (\x : fun (wait mut x)))
|
||||||
|
(\x : x x)
|
||||||
|
(\a0 a1 a2 : t (t a0) (t t a2) a1))
|
||||||
|
|
||||||
triage = (\leaf stem fork : t (t leaf stem) fork)
|
triage = (\leaf stem fork : t (t leaf stem) fork)
|
||||||
test = triage "Leaf" (\_ : "Stem") (\_ _ : "Fork")
|
test = triage "Leaf" (\_ : "Stem") (\_ _ : "Fork")
|
||||||
|
|
||||||
|
16
src/Eval.hs
16
src/Eval.hs
@ -59,8 +59,21 @@ evalAST env term
|
|||||||
elimLambda :: TricuAST -> TricuAST
|
elimLambda :: TricuAST -> TricuAST
|
||||||
elimLambda = go
|
elimLambda = go
|
||||||
where
|
where
|
||||||
|
-- η-reduction
|
||||||
go (SLambda [v] (SApp f (SVar x)))
|
go (SLambda [v] (SApp f (SVar x)))
|
||||||
| v == x && not (isFree v f) = elimLambda f
|
| v == x && not (isFree v f) = elimLambda f
|
||||||
|
-- Triage optimization
|
||||||
|
go (SLambda [a] (SLambda [b] (SLambda [c] body)))
|
||||||
|
| body == triageBody = _TRIAGE
|
||||||
|
where
|
||||||
|
triageBody =
|
||||||
|
(SApp (SApp TLeaf (SApp (SApp TLeaf (SVar a)) (SVar b))) (SVar c))
|
||||||
|
-- Compose optimization
|
||||||
|
go (SLambda [f] (SLambda [g] (SLambda [x] body)))
|
||||||
|
| body == composeBody = _COMPOSE
|
||||||
|
where
|
||||||
|
composeBody = SApp (SVar f) (SApp (SVar g) (SVar x))
|
||||||
|
-- General elimination
|
||||||
go (SLambda (v:vs) body)
|
go (SLambda (v:vs) body)
|
||||||
| null vs = toSKI v (elimLambda body)
|
| null vs = toSKI v (elimLambda body)
|
||||||
| otherwise = elimLambda (SLambda [v] (SLambda vs body))
|
| otherwise = elimLambda (SLambda [v] (SLambda vs body))
|
||||||
@ -75,10 +88,13 @@ elimLambda = go
|
|||||||
| otherwise = SApp (SApp _S (toSKI x n)) (toSKI x u)
|
| otherwise = SApp (SApp _S (toSKI x n)) (toSKI x u)
|
||||||
toSKI x t
|
toSKI x t
|
||||||
| not (isFree x t) = SApp _K t
|
| not (isFree x t) = SApp _K t
|
||||||
|
| otherwise = errorWithoutStackTrace "Unhandled toSKI conversion"
|
||||||
|
|
||||||
_S = parseSingle "t (t (t t t)) t"
|
_S = parseSingle "t (t (t t t)) t"
|
||||||
_K = parseSingle "t t"
|
_K = parseSingle "t t"
|
||||||
_I = parseSingle "t (t (t t)) t"
|
_I = parseSingle "t (t (t t)) t"
|
||||||
|
_TRIAGE = parseSingle "t (t (t t (t (t (t t t))))) t"
|
||||||
|
_COMPOSE = parseSingle "t (t (t t (t (t (t t t)) t))) (t t)"
|
||||||
|
|
||||||
isFree x = Set.member x . freeVars
|
isFree x = Set.member x . freeVars
|
||||||
freeVars (SVar v ) = Set.singleton v
|
freeVars (SVar v ) = Set.singleton v
|
||||||
|
@ -497,7 +497,6 @@ fileEval = testGroup "File evaluation tests"
|
|||||||
decodeResult (result res) @?= "\"String test!\""
|
decodeResult (result res) @?= "\"String test!\""
|
||||||
]
|
]
|
||||||
|
|
||||||
|
|
||||||
demos :: TestTree
|
demos :: TestTree
|
||||||
demos = testGroup "Test provided demo functionality"
|
demos = testGroup "Test provided demo functionality"
|
||||||
[ testCase "Structural equality demo" $ do
|
[ testCase "Structural equality demo" $ do
|
||||||
@ -511,7 +510,7 @@ demos = testGroup "Test provided demo functionality"
|
|||||||
, testCase "Determining the size of functions" $ do
|
, testCase "Determining the size of functions" $ do
|
||||||
library <- liftIO $ evaluateFile "./lib/base.tri"
|
library <- liftIO $ evaluateFile "./lib/base.tri"
|
||||||
res <- liftIO $ evaluateFileWithContext library "./demos/size.tri"
|
res <- liftIO $ evaluateFileWithContext library "./demos/size.tri"
|
||||||
decodeResult (result res) @?= "2071"
|
decodeResult (result res) @?= "454"
|
||||||
, testCase "Level Order Traversal demo" $ do
|
, testCase "Level Order Traversal demo" $ do
|
||||||
library <- liftIO $ evaluateFile "./lib/base.tri"
|
library <- liftIO $ evaluateFile "./lib/base.tri"
|
||||||
res <- liftIO $ evaluateFileWithContext library "./demos/levelOrderTraversal.tri"
|
res <- liftIO $ evaluateFileWithContext library "./demos/levelOrderTraversal.tri"
|
||||||
|
Loading…
x
Reference in New Issue
Block a user