From 6713b05872f60c65c7c27700588f44e2edbd4e6b Mon Sep 17 00:00:00 2001 From: James Eversole Date: Sat, 25 Jan 2025 15:12:28 -0600 Subject: [PATCH] Add optimization cases for triage and composition --- lib/base.tri | 11 ++++------- src/Eval.hs | 22 +++++++++++++++++++--- test/Spec.hs | 3 +-- 3 files changed, 24 insertions(+), 12 deletions(-) diff --git a/lib/base.tri b/lib/base.tri index 0208f42..b3e27ae 100644 --- a/lib/base.tri +++ b/lib/base.tri @@ -7,17 +7,14 @@ s = t (t (k t)) t m = s i i b = s (k s) 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) pair = t 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) test = triage "Leaf" (\_ : "Stem") (\_ _ : "Fork") diff --git a/src/Eval.hs b/src/Eval.hs index dcfda2a..2664739 100644 --- a/src/Eval.hs +++ b/src/Eval.hs @@ -59,8 +59,21 @@ evalAST env term elimLambda :: TricuAST -> TricuAST elimLambda = go where + -- η-reduction go (SLambda [v] (SApp f (SVar x))) | 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) | null vs = toSKI v (elimLambda body) | otherwise = elimLambda (SLambda [v] (SLambda vs body)) @@ -75,10 +88,13 @@ elimLambda = go | otherwise = SApp (SApp _S (toSKI x n)) (toSKI x u) toSKI x t | not (isFree x t) = SApp _K t + | otherwise = errorWithoutStackTrace "Unhandled toSKI conversion" - _S = parseSingle "t (t (t t t)) t" - _K = parseSingle "t t" - _I = parseSingle "t (t (t t)) t" + _S = parseSingle "t (t (t t t)) t" + _K = parseSingle "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 freeVars (SVar v ) = Set.singleton v diff --git a/test/Spec.hs b/test/Spec.hs index 71ec7f5..c8ea93a 100644 --- a/test/Spec.hs +++ b/test/Spec.hs @@ -497,7 +497,6 @@ fileEval = testGroup "File evaluation tests" decodeResult (result res) @?= "\"String test!\"" ] - demos :: TestTree demos = testGroup "Test provided demo functionality" [ testCase "Structural equality demo" $ do @@ -511,7 +510,7 @@ demos = testGroup "Test provided demo functionality" , testCase "Determining the size of functions" $ do library <- liftIO $ evaluateFile "./lib/base.tri" res <- liftIO $ evaluateFileWithContext library "./demos/size.tri" - decodeResult (result res) @?= "2071" + decodeResult (result res) @?= "454" , testCase "Level Order Traversal demo" $ do library <- liftIO $ evaluateFile "./lib/base.tri" res <- liftIO $ evaluateFileWithContext library "./demos/levelOrderTraversal.tri"