Include equality testing in basic library
This commit is contained in:
parent
e835caabbc
commit
c820eda816
@ -1,7 +1,7 @@
|
|||||||
cabal-version: 1.12
|
cabal-version: 1.12
|
||||||
|
|
||||||
name: sapling
|
name: sapling
|
||||||
version: 0.3.0
|
version: 0.4.0
|
||||||
description: A micro-language for exploring Tree Calculus
|
description: A micro-language for exploring Tree Calculus
|
||||||
author: James Eversole
|
author: James Eversole
|
||||||
maintainer: james@eversole.co
|
maintainer: james@eversole.co
|
||||||
@ -34,6 +34,7 @@ executable sapling
|
|||||||
other-modules:
|
other-modules:
|
||||||
Eval
|
Eval
|
||||||
Lexer
|
Lexer
|
||||||
|
Library
|
||||||
Parser
|
Parser
|
||||||
REPL
|
REPL
|
||||||
Research
|
Research
|
||||||
@ -55,6 +56,7 @@ test-suite sapling-tests
|
|||||||
other-modules:
|
other-modules:
|
||||||
Eval
|
Eval
|
||||||
Lexer
|
Lexer
|
||||||
|
Library
|
||||||
Parser
|
Parser
|
||||||
REPL
|
REPL
|
||||||
Research
|
Research
|
||||||
|
43
src/Library.hs
Normal file
43
src/Library.hs
Normal file
@ -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))))"
|
35
src/Main.hs
35
src/Main.hs
@ -2,6 +2,7 @@ module Main where
|
|||||||
|
|
||||||
import Eval
|
import Eval
|
||||||
import Lexer
|
import Lexer
|
||||||
|
import Library
|
||||||
import Parser
|
import Parser
|
||||||
import REPL (repl)
|
import REPL (repl)
|
||||||
import Research
|
import Research
|
||||||
@ -14,38 +15,4 @@ main = repl library
|
|||||||
|
|
||||||
runSapling :: String -> String
|
runSapling :: String -> String
|
||||||
runSapling s = show $ result (evalSapling Map.empty $ parseSapling s)
|
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)
|
runSaplingEnv env s = show $ result (evalSapling env $ parseSapling s)
|
||||||
|
41
test/Spec.hs
41
test/Spec.hs
@ -2,6 +2,7 @@ module Main where
|
|||||||
|
|
||||||
import Eval
|
import Eval
|
||||||
import Lexer
|
import Lexer
|
||||||
|
import Library
|
||||||
import Parser
|
import Parser
|
||||||
import Research
|
import Research
|
||||||
import Control.Exception (evaluate, try, SomeException)
|
import Control.Exception (evaluate, try, SomeException)
|
||||||
@ -227,48 +228,25 @@ evaluationTests = testGroup "Evaluation Tests"
|
|||||||
result env @?= Stem Leaf
|
result env @?= Stem Leaf
|
||||||
, testCase "Boolean AND_ TF" $ do
|
, testCase "Boolean AND_ TF" $ do
|
||||||
let input = "and (t t) (t)"
|
let input = "and (t t) (t)"
|
||||||
env = evalSapling boolEnv (parseSapling input)
|
env = evalSapling library (parseSapling input)
|
||||||
result env @?= Leaf
|
result env @?= Leaf
|
||||||
, testCase "Boolean AND_ FT" $ do
|
, testCase "Boolean AND_ FT" $ do
|
||||||
let input = "and (t) (t t)"
|
let input = "and (t) (t t)"
|
||||||
env = evalSapling boolEnv (parseSapling input)
|
env = evalSapling library (parseSapling input)
|
||||||
result env @?= Leaf
|
result env @?= Leaf
|
||||||
, testCase "Boolean AND_ FF" $ do
|
, testCase "Boolean AND_ FF" $ do
|
||||||
let input = "and (t) (t)"
|
let input = "and (t) (t)"
|
||||||
env = evalSapling boolEnv (parseSapling input)
|
env = evalSapling library (parseSapling input)
|
||||||
result env @?= Leaf
|
result env @?= Leaf
|
||||||
, testCase "Boolean AND_ TT" $ do
|
, testCase "Boolean AND_ TT" $ do
|
||||||
let input = "and (t t) (t t)"
|
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
|
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 :: TestTree
|
||||||
lambdaEvalTests = testGroup "Lambda Evaluation Tests"
|
lambdaEvalTests = testGroup "Lambda Evaluation Tests"
|
||||||
@ -340,4 +318,3 @@ propertyTests = testGroup "Property Tests"
|
|||||||
Left _ -> property True
|
Left _ -> property True
|
||||||
Right ast -> parseSingle input === ast
|
Right ast -> parseSingle input === ast
|
||||||
]
|
]
|
||||||
|
|
||||||
|
Loading…
x
Reference in New Issue
Block a user