commit c718684963dc92b3611089bd387b372af59c1cea
parent 2c75f58e42b3b3c3919d09ce83b5d38e9e80770f
Author: James Eversole <james@eversole.co>
Date: Fri, 27 Dec 2024 16:30:32 -0600
Include equality testing in basic library
Diffstat:
4 files changed, 56 insertions(+), 67 deletions(-)
diff --git a/sapling.cabal b/sapling.cabal
@@ -1,7 +1,7 @@
cabal-version: 1.12
name: sapling
-version: 0.3.0
+version: 0.4.0
description: A micro-language for exploring Tree Calculus
author: James Eversole
maintainer: james@eversole.co
@@ -34,6 +34,7 @@ executable sapling
other-modules:
Eval
Lexer
+ Library
Parser
REPL
Research
@@ -55,6 +56,7 @@ test-suite sapling-tests
other-modules:
Eval
Lexer
+ Library
Parser
REPL
Research
diff --git a/src/Library.hs b/src/Library.hs
@@ -0,0 +1,43 @@
+module Library where
+
+import Eval
+import Parser
+import Research
+
+import qualified Data.Map as Map
+
+library :: Map.Map String T
+library = evalSapling Map.empty $ parseSapling
+ "false = t\n \
+ \ true = t t\n \
+ \ k = t t\n \
+ \ i = t (t k) t\n \
+ \ s = t (t (k t)) t\n \
+ \ m = s i i\n \
+ \ b = s (k s) k\n \
+ \ c = s (s (k s) (s (k k) s)) (k k)\n \
+ \ iC = (\\a b c : s a (k c) b)\n \
+ \ iD = b (b iC) iC\n \
+ \ iE = b (b iD) iC\n \
+ \ yi = (\\i : b m (c b (i m)))\n \
+ \ y = yi iC\n \
+ \ yC = yi iD\n \
+ \ yD = yi iE\n \
+ \ id = (\\a : a)\n \
+ \ triage = (\\a b c : t (t a b) c)\n \
+ \ pair = t\n \
+ \ matchBool = (\\ot of : triage of (\\z : ot) t)\n \
+ \ matchList = (\\oe oc : triage oe _ oc)\n \
+ \ matchPair = (\\op : triage _ _ op)\n \
+ \ and = matchBool id (\\z : false)\n \
+ \ if = (\\cond then else : t (t else (t t then)) t cond)\n \
+ \ test = triage \"leaf\" (\\z : \"stem\") (\\a b : \"fork\")\n \
+ \ emptyList = matchList true (\\y z : false)\n \
+ \ nonEmptyList = matchList false (\\y z : true)\n \
+ \ head = matchList t (\\hd tl : hd)\n \
+ \ tail = matchList t (\\hd tl : tl)\n \
+ \ listConcat = y (\\self : matchList (\\k : k) (\\h t k : pair h (self t k)))\n \
+ \ listConcat \"foo\" \"bar\"\n \
+ \ lAnd = triage (\\x : false) (\\z x : x) (\\y z x : x)\n \
+ \ lOr = triage (\\x : x) (\\z x : true) (\\y z x : true)\n \
+ \ equal = y (\\self : triage (triage true (\\z : false) (\\y z : false)) (\\ax : triage false (self ax) (\\y z : false)) (\\ax ay : triage false (\\z : false) (\\bx by : lAnd (self ax bx) (self ay by))))"
diff --git a/src/Main.hs b/src/Main.hs
@@ -2,6 +2,7 @@ module Main where
import Eval
import Lexer
+import Library
import Parser
import REPL (repl)
import Research
@@ -14,38 +15,4 @@ main = repl library
runSapling :: String -> String
runSapling s = show $ result (evalSapling Map.empty $ parseSapling s)
-
-library :: Map.Map String T
-library = evalSapling Map.empty $ parseSapling
- "false = t\n \
- \ k = t t\n \
- \ i = t (t k) t\n \
- \ s = t (t (k t)) t\n \
- \ m = s i i\n \
- \ b = s (k s) k\n \
- \ c = s (s (k s) (s (k k) s)) (k k)\n \
- \ iC = (\\a b c : s a (k c) b)\n \
- \ iD = b (b iC) iC\n \
- \ iE = b (b iD) iC\n \
- \ yi = (\\i : b m (c b (i m)))\n \
- \ y = yi iC\n \
- \ yC = yi iD\n \
- \ yD = yi iE \
- \ true = t t\n \
- \ id = (\\a : a)\n \
- \ triage = (\\a b c : t (t a b) c)\n \
- \ pair = t\n \
- \ matchBool = (\\ot of : triage of (\\z : ot) t)\n \
- \ matchList = (\\oe oc : triage oe _ oc)\n \
- \ matchPair = (\\op : triage _ _ op)\n \
- \ and = matchBool id (\\z : false)\n \
- \ if = (\\cond then else : t (t else (t t then)) t cond)\n \
- \ test = triage \"leaf\" (\\z : \"stem\") (\\a b : \"fork\")\n \
- \ emptyList = matchList true (\\y z : false)\n \
- \ nonEmptyList = matchList false (\\y z : true)\n \
- \ head = matchList t (\\hd tl : hd)\n \
- \ tail = matchList t (\\hd tl : tl)\n \
- \ listConcat = y (\\self : matchList (\\k : k) (\\h t k : pair h (self t k)))\n \
- \ listConcat \"foo\" \"bar\""
-
runSaplingEnv env s = show $ result (evalSapling env $ parseSapling s)
diff --git a/test/Spec.hs b/test/Spec.hs
@@ -2,6 +2,7 @@ module Main where
import Eval
import Lexer
+import Library
import Parser
import Research
import Control.Exception (evaluate, try, SomeException)
@@ -227,48 +228,25 @@ evaluationTests = testGroup "Evaluation Tests"
result env @?= Stem Leaf
, testCase "Boolean AND_ TF" $ do
let input = "and (t t) (t)"
- env = evalSapling boolEnv (parseSapling input)
+ env = evalSapling library (parseSapling input)
result env @?= Leaf
, testCase "Boolean AND_ FT" $ do
let input = "and (t) (t t)"
- env = evalSapling boolEnv (parseSapling input)
+ env = evalSapling library (parseSapling input)
result env @?= Leaf
, testCase "Boolean AND_ FF" $ do
let input = "and (t) (t)"
- env = evalSapling boolEnv (parseSapling input)
+ env = evalSapling library (parseSapling input)
result env @?= Leaf
, testCase "Boolean AND_ TT" $ do
let input = "and (t t) (t t)"
- env = evalSapling boolEnv (parseSapling input)
+ env = evalSapling library (parseSapling input)
+ result env @?= Stem Leaf
+ , testCase "Verifying Equality" $ do
+ let input = "equal (t t t) (t t t)"
+ env = evalSapling library (parseSapling input)
result env @?= Stem Leaf
- --, testCase "Verifying Equality" $ do
- -- let input = "equal (t t t) (t t t)"
- -- env = evalSapling boolEnv (parseSapling input)
- -- result env @?= Stem Leaf
]
- where
- boolEnv = evalSapling Map.empty $ parseSapling
- "false = t\n \
- \ true = t t\n \
- \ id = (\\a : a)\n \
- \ triage = (\\a b c : t (t a b) c)\n \
- \ match_bool = (\\ot of : triage of (\\z : ot) t)\n \
- \ and = match_bool id (\\z : false)\n \
- \ if = (\\cond then else : t (t else (t t then)) t cond)\n \
- \ fix = (\\m wait f : wait m (\\x : f (wait m x))) (\\x : x x) (\\a b c : (t (t a) (t t c) b))\n \
- \ equal = fix ((\\self : triage (triage true (\\z : false) (\\z x : false)) (\\ax : triage false (self ax) (\\z x : false)) (\\ax ay : triage false (\\z : false) (\\bx by : and (self ax bx) (self ay by)))))"
-
--- false = t
--- true = t t
--- id = \x x
--- fix = (\m \wait2 \f wait2 m (\x f (wait2 m x))) (\x x x) (\a \b \c t (t a) (t t c) b)
--- triage = \a \b \c t (t a b) c
--- match_bool = \ot \of triage of (\_ ot) t
--- and = match_bool id (\_ false)
--- equal = fix $ \self triage
--- (triage true (\_ false) (\_ \_ false))
--- (\ax triage false (self ax) (\_ \_ false))
--- (\ax \ay triage false (\_ false) (\bx \by and (self ax bx) (self ay by)))
lambdaEvalTests :: TestTree
lambdaEvalTests = testGroup "Lambda Evaluation Tests"
@@ -340,4 +318,3 @@ propertyTests = testGroup "Property Tests"
Left _ -> property True
Right ast -> parseSingle input === ast
]
-
