ntha 0.1.0 → 0.1.1
raw patch · 10 files changed
+640/−11 lines, 10 filesdep −z3-encodingdep ~mtldep ~z3
Dependencies removed: z3-encoding
Dependency ranges changed: mtl, z3
Files
- README.md +5/−0
- app/Main.hs +1/−1
- examples/misc.ntha +195/−0
- ntha.cabal +16/−4
- src/Z3/Assertion.hs +63/−0
- src/Z3/Class.hs +223/−0
- src/Z3/Context.hs +61/−0
- src/Z3/Encoding.hs +52/−0
- src/Z3/Logic.hs +18/−0
- test/EvalSpec.hs +6/−6
README.md view
@@ -8,6 +8,11 @@ a tiny statically typed functional programming language. +## Installation++* brew install z3+* cabal install ntha+ ## Features * Global type inference with optional type annotations.
app/Main.hs view
@@ -37,7 +37,7 @@ EProgram instructions -> do let imports = filter isImport instructions let continueAst = EProgram $ filter (not . isImport) instructions- importEnv <- foldM (\env (EImport path) -> loadFile env path) env imports+ importEnv <- foldM (\ev (EImport path) -> loadFile ev path) env imports return (importEnv, continueAst) _ -> return (env, expr)
+ examples/misc.ntha view
@@ -0,0 +1,195 @@+;; recursive function++(ƒ penultimate [xs]+ (match xs+ ([] ⇒ 0)+ ([_] ⇒ 0)+ ([a _] ⇒ a)+ (_ :: t ⇒ (penultimate t))))++(fib : Z → Z)+(ƒ fib [x]+ (match x+ (0 ⇒ 0)+ (1 ⇒ 1)+ (_ ⇒ (+ (fib (- x 1)) (fib (- x 2))))))++(asserteq (fib 5) 5)+(print (int2str (fib 5)))++(ƒ fibc [x]+ (cond+ ((= x 0) ⇒ 0)+ ((= x 1) ⇒ 1)+ (else ⇒ (+ (fibc (- x 1)) (fibc (- x 2))))))++(asserteq (fibc 5) 5)+(print (int2str (fibc 5)))++(ƒ fact [n]+ (if (≤ n 1)+ 1+ (* n (fact (- n 1)))))++(let f5 (fact 5))++(asserteq f5 120)+(print (int2str f5))++(ƒ fact-wrap [n]+ (let [fact (λ n → (if (≤ n 1)+ 1+ (* n (fact (- n 1)))))]+ (fact n)))++(let f5 (fact-wrap 5))+(print (int2str f5))++(ƒ factc [n]+ (cond+ ((≤ n 1) → 1)+ (else → (* n (factc (- n 1))))))++(let fc5 (factc 5))++(asserteq fc5 120)+(print (int2str fc5))++;; record data type++(let profile {:name "ntha" :age 3})++(asserteq (:name profile) "ntha")+(print (:name profile))++;; destructuring++(let (a . b) (4 . "d"))++(let d ((4 . true) . ("test" . 'c' . a)))++(let ((_ . bool) . (_ . _ . _)) d)++(asserteq bool true)+(print (bool2str bool))++;; algebraic data type and pattern matching++(data Tree a Empty-Tree (Leaf a) (Node (Tree a) a (Tree a)))++(let t (Node (Leaf 5) 4 (Leaf 3)))++(depth : (Tree α) → Z)+(ƒ depth+ [t]+ (match t+ (Empty-Tree => 0)+ ((Leaf _) => 1)+ ((Node l _ r) => (inc (max (depth l) (depth r))))))++(asserteq (depth t) 2)++(print (int2str (depth t)))++(asserteq (depth (Leaf 3)) 1)++(print (int2str (depth (Leaf 3))))++(asserteq (depth Empty-Tree) 0)++(print (int2str (depth Empty-Tree)))++;; lambda and high-order function++(let l [1 2])++(ƒ double [x] (* 2 x))++(let ll1 (map double l))++(asserteq ll1 [2 4])++(let ll2 (map (λ x => (* 2 x)) l))++(asserteq ll2 [2 4])++(let l2 [[1 2 3] [4 5 6]])++(asserteq (map len l2) [3 3])++;; curried function++(ƒ add [x y] (+ x y))++(let inc (add 1))++(let three (inc 2))++(asserteq three 3)++(print (int2str three))++;; lexical scope++(let a 3)++(let f (λ x → (* a x)))++(let a 5)++(asserteq (f 5) 15)++(print (int2str (f 5)))++;; monad++(let m (do Maybe+ (a <- (Just 3))+ (b <- (Just (+ a 3)))+ (return (* b 3))))++(asserteq m (Just 18))++(begin+ (let name "ntha")+ (print name)+ (print "language"))++;; negative number++(asserteq (+ -1 2) 1)++;; letrec https://github.com/zjhmale/Ntha/issues/1++(let [ev? (λ n →+ (match (λ n → (if (zero? n) false (ev? (dec n))))+ (od? → (if (zero? n) true (od? (dec n))))))+ od? (λ n →+ (match (λ n → (if (zero? n) true (od? (dec n))))+ (ev? → (if (zero? n) false (ev? (dec n))))))]+ (begin (print (bool2str (ev? 11)))+ (print (bool2str (ev? 12)))+ (print (bool2str (od? 11)))+ (print (bool2str (od? 12)))))++(id : α → α)+(ƒ id [a] a)++(asserteq (id 3) 3)+(asserteq (id true) true)++(asserteq ((λ(x: α) : α → x) 3) 3)+(asserteq ((λ(x: α) : α → x) true) true)++(let id' (λ(x: α) : α → x))+(asserteq (id' 3) 3)+(asserteq (id' true) true)++(foo : (x : Z | (> x 5)) → (z : Z | (> z 0)))+(ƒ foo [x] (- x 5))++(add : (x : Z | (≥ x 3)) → (y : Z | (≥ y 3)) → (z : Z | (≥ z 6)))+(ƒ add [x y] (+ x y))++(max : Z → Z → (z : Z | (∧ (≥ z x) (≥ z y))))+(ƒ max [x y] (if (≤ x y) y x))
ntha.cabal view
@@ -1,5 +1,5 @@ name: ntha-version: 0.1.0+version: 0.1.1 synopsis: A tiny statically typed functional programming language. description: Check out <https://github.com/zjhmale/Ntha#readme the readme> for documentation. homepage: https://github.com/zjhmale/ntha@@ -17,7 +17,7 @@ README.md data-files: lib/std.ntha-+ examples/misc.ntha library hs-source-dirs: src@@ -32,17 +32,29 @@ , Prologue , Lexer , Parser+ , Z3.Assertion+ , Z3.Class+ , Z3.Context+ , Z3.Encoding+ , Z3.Logic build-depends: base >= 4.7 && < 5 , containers , pretty , monad-loops , array- , z3 >=4.4.1- , z3-encoding+ , z3 >= 4.1.0+ , mtl >= 2.2 && < 2.3+ --, z3-encoding build-tools: happy , alex default-extensions: TupleSections , StandaloneDeriving+ , FlexibleInstances+ , FlexibleContexts+ , ScopedTypeVariables+ , MultiParamTypeClasses+ , RankNTypes+ , GADTs default-language: Haskell2010 ghc-options: -Wall
+ src/Z3/Assertion.hs view
@@ -0,0 +1,63 @@+-- |+-- Assertions provided by libraries *for convenience*+-- It is not hard-coded into Z3.Logic.Pred+--++module Z3.Assertion (Assertion(..)) where++import Z3.Class+import Z3.Encoding()+import Z3.Monad++import qualified Data.Map as M+import qualified Data.Set as S++data Assertion where+ -- | k is mapped to v in (m :: M.Map k v)+ -- XXX: m should be any "term", too strong now+ InMap :: forall k v. (Z3Sorted k, Z3Encoded k, Z3Sorted v, Z3Reserved v) => k -> v -> M.Map k v -> Assertion+ -- | v is in s+ -- XXX: s should be any "term", too strong now+ InSet :: forall v. (Z3Encoded v, Z3Sorted v) => v -> S.Set v -> Assertion+ -- | All below are binary relationships+ -- XXX: Should make sure v1 ~ v2, too weak now+ Equal :: forall v1 v2. (Z3Encoded v1, Z3Encoded v2, Eq v1, Eq v2) => v1 -> v2 -> Assertion+ LessE :: forall v1 v2. (Z3Encoded v1, Z3Encoded v2, Eq v1, Eq v2) => v1 -> v2 -> Assertion+ GreaterE :: forall v1 v2. (Z3Encoded v1, Z3Encoded v2, Eq v1, Eq v2) => v1 -> v2 -> Assertion+ Less :: forall v1 v2. (Z3Encoded v1, Z3Encoded v2, Eq v1, Eq v2) => v1 -> v2 -> Assertion+ Greater :: forall v1 v2. (Z3Encoded v1, Z3Encoded v2, Eq v1, Eq v2) => v1 -> v2 -> Assertion++instance Z3Encoded Assertion where+ encode (InMap k v m) = do+ kTm <- encode k+ vTm <- encode v+ mTm <- encode m+ lhs <- mkSelect mTm kTm+ mkEq lhs vTm+ encode (InSet e s) = do+ eTm <- encode e+ sTm <- encode s+ lhs <- mkSelect sTm eTm+ -- XXX: magic number+ one <- (mkIntSort >>= mkInt 1)+ mkEq one lhs+ encode (Equal t1 t2) = do+ a1 <- encode t1+ a2 <- encode t2+ mkEq a1 a2+ encode (LessE t1 t2) = do+ a1 <- encode t1+ a2 <- encode t2+ mkLe a1 a2+ encode (GreaterE t1 t2) = do+ a1 <- encode t1+ a2 <- encode t2+ mkGe a1 a2+ encode (Less t1 t2) = do+ a1 <- encode t1+ a2 <- encode t2+ mkLt a1 a2+ encode (Greater t1 t2) = do+ a1 <- encode t1+ a2 <- encode t2+ mkGt a1 a2
+ src/Z3/Class.hs view
@@ -0,0 +1,223 @@+-- |+-- Type classes and built-in implementation for primitive Haskell types+-- ++module Z3.Class (+ -- ** Types whose values are encodable to Z3 internal AST+ Z3Encoded(..),+ -- ** Types representable as Z3 Sort+ -- XXX: Unsound now+ -- XXX: Too flexible, can be used to encode Type ADT+ Z3Sorted(..),+ -- ** Type proxy helper, used with Z3Sorted+ Z3Sort(..),+ -- ** Types with reserved value for Z3 encoding use+ -- XXX: Magic value for built-in types+ Z3Reserved(..),+ -- ** Monad which can be instantiated into a concrete context+ SMT(..)+) where++import Z3.Monad+import Z3.Logic++import Control.Monad.Except++import qualified Data.Map as M+import qualified Data.Set as S++data Z3Sort a = Z3Sort++class Z3Encoded a where+ encode :: SMT m e => a -> m e AST++-- | XXX: Unsound+class Z3Sorted a where+ -- | Map a value to Sort, the value should be a type-level thing+ sort :: SMT m e => a -> m e Sort+ sort _ = sortPhantom (Z3Sort :: Z3Sort a)++ -- | Map a Haskell type to Sort+ sortPhantom :: SMT m e => Z3Sort a -> m e Sort+ sortPhantom _ = smtError "sort error"++class Z3Encoded a => Z3Reserved a where+ def :: a++class (MonadError String (m e), MonadZ3 (m e)) => SMT m e where+ -- | Globally unique id+ genFreshId :: m e Int++ -- | Given data type declarations, extra field, and the SMT monad, return the fallible result in IO monad+ runSMT :: Z3Sorted ty => [(String, [(String, [(String, ty)])])] -> e -> m e a -> IO (Either String a)++ -- | Binding a variable String name to two things: an de Brujin idx as Z3 AST generated by mkBound and binder's Sort+ bindQualified :: String -> AST -> Sort -> m e ()++ -- | Get the above AST+ -- FIXME: The context management need extra -- we need to make sure that old binding wouldn't be destoryed+ -- XXX: We shouldn't expose a Map here. A fallible query interface is better+ getQualifierCtx :: m e (M.Map String (AST, Sort))++ -- | Get the preprocessed datatype context, a map from ADT's type name to its Z3 Sort+ -- XXX: We shouldn't expose a Map here. A fallible query interface is better+ getDataTypeCtx :: m e (M.Map String Sort)++ -- | Get extra+ getExtra :: m e e++ -- | Set extra+ modifyExtra :: (e -> e) -> m e ()++ -- | User don't have to import throwError+ smtError :: String -> m e a+ smtError = throwError++instance Z3Reserved Int where+ def = -1 -- XXX: Magic number++instance Z3Sorted Int where+ sortPhantom _ = mkIntSort++instance Z3Encoded Int where+ encode i = mkIntSort >>= mkInt i++instance Z3Reserved Double where+ def = -1.0 -- XXX: Magic number++instance Z3Sorted Double where+ sortPhantom _ = mkRealSort++instance Z3Encoded Double where+ encode = mkRealNum++instance Z3Reserved Bool where+ def = False -- XXX: Magic number++instance Z3Sorted Bool where+ sortPhantom _ = mkBoolSort++instance Z3Encoded Bool where+ encode = mkBool++-- The basic idea:+-- For each (k, v), assert in Z3 that if we select k from array we will get+-- the same value v+-- HACK: to set a default value for rest fields (or else we always get the last asserted value+-- as default, which is certainly not complying to finite map's definition), thus the+-- user should guarantee that he/she will never never think this value as a vaid one,+-- if not, he/she might get "a valid value mapped to a invalid key" semantics+instance (Z3Sorted k, Z3Encoded k, Z3Sorted v, Z3Reserved v) => Z3Encoded (M.Map k v) where+ encode m = do+ fid <- genFreshId+ arrSort <- sort m+ arr <- mkFreshConst ("map" ++ "_" ++ show fid) arrSort+ mapM_ (\(k, v) -> do+ kast <- encode k+ vast <- encode v+ sel <- mkSelect arr kast+ mkEq sel vast >>= assert) (M.toList m)+ arrValueDef <- mkArrayDefault arr+ vdef <- encode (def :: v)+ mkEq arrValueDef vdef >>= assert+ return arr++instance (Z3Sorted k, Z3Sorted v) => Z3Sorted (M.Map k v) where+ sortPhantom _ = do+ sk <- sortPhantom (Z3Sort :: Z3Sort k)+ sv <- sortPhantom (Z3Sort :: Z3Sort v)+ mkArraySort sk sv++-- Basic idea:+-- Set v =def= Map v {0, 1}+-- Thank god, this is much more sound+instance (Z3Sorted v, Z3Encoded v) => Z3Encoded (S.Set v) where+ encode s = do+ setSort <- sort s+ fid <- genFreshId+ arr <- mkFreshConst ("set" ++ "_" ++ show fid) setSort+ mapM_ (\e -> do+ ast <- encode e+ sel <- mkSelect arr ast+ one <- (mkIntSort >>= mkInt 1)+ mkEq sel one >>= assert) (S.toList s)+ arrValueDef <- mkArrayDefault arr+ zero <- (mkIntSort >>= mkInt 0)+ mkEq zero arrValueDef >>= assert+ return arr++instance Z3Sorted v => Z3Sorted (S.Set v) where+ sortPhantom _ = do+ sortElem <- sortPhantom (Z3Sort :: Z3Sort v)+ intSort <- mkIntSort+ mkArraySort sortElem intSort++instance (Z3Sorted t, Z3Sorted ty, Z3Encoded a) => Z3Encoded (Pred t ty a) where+ encode PTrue = mkTrue+ encode PFalse = mkFalse+ encode (PConj p1 p2) = do+ a1 <- encode p1+ a2 <- encode p2+ mkAnd [a1, a2]++ encode (PDisj p1 p2) = do+ a1 <- encode p1+ a2 <- encode p2+ mkOr [a1, a2]++ encode (PXor p1 p2) = do+ a1 <- encode p1+ a2 <- encode p2+ mkXor a1 a2++ encode (PNeg p) = encode p >>= mkNot++ encode (PForAll x ty p) = do+ sym <- mkStringSymbol x+ xsort <- sort ty+ -- "0" is de brujin idx for current binder+ -- it is passed to Z3 which returns an intenal (idx :: AST)+ -- This (idx :: AST) will be used to replace the variable+ -- in the abstraction body when encountered, thus it is stored+ -- in context by bindQualified we provide+ -- XXX: we should save and restore qualifier context here+ idx <- mkBound 0 xsort+ local $ do+ bindQualified x idx xsort+ body <- encode p+ -- The first [] is [Pattern], which is not really useful here+ mkForall [] [sym] [xsort] body++ encode (PExists x ty p) = do+ sym <- mkStringSymbol x+ xsort <- sort ty+ idx <- mkBound 0 xsort+ local $ do+ bindQualified x idx xsort+ a <- encode p+ mkExists [] [sym] [xsort] a++ -- HACK+ encode (PExists2 x y ty p) = do+ sym1 <- mkStringSymbol x+ sym2 <- mkStringSymbol y+ xsort <- sort ty+ idx1 <- mkBound 0 xsort+ idx2 <- mkBound 1 xsort+ local $ do+ bindQualified x idx1 xsort+ bindQualified y idx2 xsort+ a <- encode p+ mkExists [] [sym1, sym2] [xsort, xsort] a++ encode (PImpli p1 p2) = do+ a1 <- encode p1+ a2 <- encode p2+ mkImplies a1 a2++ encode (PIff p1 p2) = do+ a1 <- encode p1+ a2 <- encode p2+ mkIff a1 a2++ encode (PAssert a) = encode a
+ src/Z3/Context.hs view
@@ -0,0 +1,61 @@+{-# LANGUAGE GeneralizedNewtypeDeriving #-}++-- | A concrete context implement SMT provided *for convenience*++module Z3.Context (Z3SMT) where++import Z3.Monad+import Z3.Class+import Z3.Encoding++import Control.Monad.State+import Control.Monad.Except+import qualified Data.Map as M++data SMTContext e = SMTContext {+ -- | Bind local variables introduced by qualifiers to de brujin index in Z3+ _qualifierContext :: M.Map String (AST, Sort),+ -- | From type name to Z3 sort+ _datatypeCtx :: M.Map String Sort,+ -- | Counter used to generate globally unique ID+ _counter :: Int,+ -- | Extra field reserved for extension+ _extra :: e+} deriving (Show, Eq)++newtype Z3SMT e a = Z3SMT { unZ3SMT :: ExceptT String (StateT (SMTContext e) Z3) a }+ deriving (Monad, Applicative, Functor, MonadState (SMTContext e), MonadIO, MonadError String)++instance MonadZ3 (Z3SMT e) where+ getSolver = Z3SMT (lift (lift getSolver))+ getContext = Z3SMT (lift (lift getContext))++instance SMT Z3SMT e where+ genFreshId = do+ i <- _counter <$> get+ modify (\ctx -> ctx { _counter = i + 1 })+ return i++ runSMT datatypes e smt = evalZ3With Nothing opts m+ where+ smt' = do+ sorts <- mapM encodeDataType datatypes+ let datatypeCtx = M.fromList (zip (map fst datatypes) sorts)+ modify $ \ctx -> ctx { _datatypeCtx = datatypeCtx }+ smt++ -- XXX: not sure what does this option mean+ opts = opt "MODEL" True+ m = evalStateT (runExceptT (unZ3SMT smt'))+ (SMTContext M.empty M.empty 0 e)++ bindQualified x idx s = modify $ \ctx ->+ ctx { _qualifierContext = M.insert x (idx, s) (_qualifierContext ctx) }++ getQualifierCtx = _qualifierContext <$> get++ getDataTypeCtx = _datatypeCtx <$> get++ getExtra = _extra <$> get++ modifyExtra f = modify $ \ctx -> ctx { _extra = f (_extra ctx) }
+ src/Z3/Encoding.hs view
@@ -0,0 +1,52 @@+-- |+-- Prviding some Z3 encoding for certain language constructs+-- Require a Class.SMT context to work++module Z3.Encoding (+ -- ** Heterogenous list, a hack to encode different "term" into a list+ -- Used to encode function argument list+ HeteroList(..),+ -- ** encode function application+ encodeApp,+ -- ** encode datatype definition+ encodeDataType+) where++import Z3.Class+import Z3.Monad hiding (mkMap, App)++data HeteroList where+ Cons :: forall a. (Z3Sorted a, Z3Encoded a) => a -> HeteroList -> HeteroList+ Nil :: HeteroList++instance Eq HeteroList where+ Nil == Nil = True+ Cons _ h1 == Cons _ h2 = h1 == h2+ _ == _ = False++mapH :: (forall a. (Z3Sorted a, Z3Encoded a) => a -> b) -> HeteroList -> [b]+mapH _ Nil = []+mapH f (Cons a l) = f a : mapH f l++encodeApp :: SMT m e => String -> HeteroList -> Sort -> m e AST+encodeApp fname args retSort = do+ paramSorts <- sequence $ mapH sort args+ sym <- mkStringSymbol fname+ decl <- mkFuncDecl sym paramSorts retSort+ argASTs <- sequence $ mapH encode args+ mkApp decl argASTs++encodeDataType :: SMT m e => Z3Sorted ty => (String, [(String, [(String, ty)])]) -> m e Sort+encodeDataType (tyName, alts) = do+ constrs <- mapM (\(consName, fields) -> do+ consSym <- mkStringSymbol consName+ -- recognizer. e.g. is_None None = True, is_None (Some _) = False+ recogSym <- mkStringSymbol ("is_" ++ consName)+ flds <- flip mapM fields $ \(fldName, fldTy) -> do+ symFld <- mkStringSymbol fldName+ s <- sort fldTy+ return (symFld, Just s, -1) -- XXX: non-rec+ mkConstructor consSym recogSym flds+ ) alts+ sym <- mkStringSymbol tyName+ mkDatatype sym constrs
+ src/Z3/Logic.hs view
@@ -0,0 +1,18 @@+-- | Predicates++module Z3.Logic (Pred(..)) where++data Pred t ty a where+ PTrue :: Pred t ty a+ PFalse :: Pred t ty a+ PConj :: Pred t ty a -> Pred t ty a -> Pred t ty a+ PDisj :: Pred t ty a -> Pred t ty a -> Pred t ty a+ PXor :: Pred t ty a -> Pred t ty a -> Pred t ty a+ PNeg :: Pred t ty a -> Pred t ty a+ PForAll :: String -> ty -> Pred t ty a -> Pred t ty a+ PExists :: String -> ty -> Pred t ty a -> Pred t ty a+ PExists2 :: String -> String -> ty -> Pred t ty a -> Pred t ty a+ PImpli :: Pred t ty a -> Pred t ty a -> Pred t ty a+ PIff :: Pred t ty a -> Pred t ty a -> Pred t ty a+ PAssert :: a -> Pred t ty a+ deriving (Show)
test/EvalSpec.hs view
@@ -11,12 +11,12 @@ runEvalSpecCases :: [(Expr, Maybe Value)] -> IO () runEvalSpecCases exprExpects = do- let (_, vals, expects) = foldl (\(env, vals, expects) (expr, expect) → let (env', val) = eval expr env+ let (_, vals', expects') = foldl (\(env, vals, expects) (expr, expect) → let (env', val) = eval expr env in case expect of Just e -> (env', vals ++ [val], expects ++ [e]) Nothing -> (env', vals, expects)) (builtins, [], []) exprExpects- (map (PP.text . show) vals) `shouldBe` map (PP.text . show) expects+ (map (PP.text . show) vals') `shouldBe` map (PP.text . show) expects' spec :: Spec spec = describe "evaluation test" $ do@@ -104,7 +104,7 @@ let res0 = EDestructLetBinding (IdPattern "res0") [] [EApp (EApp (EVar "g") $ ENum 3) $ ENum 3] let f = EDestructLetBinding (IdPattern "f") [] [ELambda [Named "x" (Just intT), Named "y" (Just intT), Named "z" (Just intT)] (Just intT) [EApp (EApp (EVar "+") (EApp (EApp (EVar "+") $ EVar "x") $ EVar "y")) $ EVar "z"]] let res1 = EDestructLetBinding (IdPattern "res1") [] [EApp (EApp (EApp (EVar "f") $ ENum 8) $ ENum 2) $ ENum 3]- let id = EDestructLetBinding (IdPattern "id") [] [ELambda [Named "x" Nothing] Nothing [EVar "x"]]+ let idfn = EDestructLetBinding (IdPattern "id") [] [ELambda [Named "x" Nothing] Nothing [EVar "x"]] let res2 = EDestructLetBinding (IdPattern "res2") [] [EApp (EVar "id") $ ENum 3] let res3 = EDestructLetBinding (IdPattern "res3") [] [EApp (EVar "id") $ EBool True] let idpair = ELetBinding (IdPattern "id") (ELambda [Named "x" Nothing] Nothing [EVar "x"]) [(ETuple [EApp (EVar "id") (ENum 3), EApp (EVar "id") (EBool True)])]@@ -117,7 +117,7 @@ (res0, Just $ VNum 6), (f, Nothing), (res1, Just $ VNum 13),- (id, Nothing),+ (idfn, Nothing), (res2, Just $ VNum 3), (res3, Just $ VBool True), (idpair, Just $ VTuple [VNum 3, VBool True]),@@ -138,7 +138,7 @@ Case (TConPattern "Cons" [IdPattern "x", TConPattern "Cons" [IdPattern "y", IdPattern "t"]]) [EApp (EVar "penultimate") (EVar "t")]]]] let res7 = EDestructLetBinding (IdPattern "res7") [] [EApp (EVar "penultimate") (EList [ENum 1, ENum 2, ENum 3])] let res8 = EDestructLetBinding (IdPattern "res7") [] [EApp (EVar "penultimate") (EList [ENum 1, ENum 2, ENum 3, ENum 4])]- let map = EDestructLetBinding (IdPattern "map") [IdPattern "f", IdPattern "l"] [EPatternMatching (EVar "l") [Case (TConPattern "Cons" [IdPattern "h", IdPattern "t"]) [EApp (EApp (EVar "Cons") $ EApp (EVar "f") $ EVar "h") $ EApp (EApp (EVar "map") $ EVar "f") $ EVar "t"],Case (TConPattern "Nil" []) [EVar "Nil"]]]+ let mapfn = EDestructLetBinding (IdPattern "map") [IdPattern "f", IdPattern "l"] [EPatternMatching (EVar "l") [Case (TConPattern "Cons" [IdPattern "h", IdPattern "t"]) [EApp (EApp (EVar "Cons") $ EApp (EVar "f") $ EVar "h") $ EApp (EApp (EVar "map") $ EVar "f") $ EVar "t"],Case (TConPattern "Nil" []) [EVar "Nil"]]] let map2 = EDestructLetBinding (IdPattern "map2") [IdPattern "f", IdPattern "xs"] [EPatternMatching (EVar "xs") [Case (TConPattern "Nil" []) [EList []],Case (TConPattern "Cons" [IdPattern "h", IdPattern "t"]) [EApp (EApp (EVar "Cons") $ EApp (EVar "f") $ EVar "h") $ EApp (EApp (EVar "map2") $ EVar "f") $ EVar "t"]]] let l = EDestructLetBinding (IdPattern "l") [] [EList [ENum 1, ENum 2, ENum 3]] let l3 = EDestructLetBinding (IdPattern "l3") [] [EApp (EApp (EVar "map") $ ELambda [Named "x" Nothing] Nothing [EApp (EApp (EVar "=") $ EApp (EApp (EVar "%") $ EVar "x") $ ENum 2) $ ENum 0]) $ EVar "l"]@@ -169,7 +169,7 @@ (penultimate, Nothing), (res7, Just $ VNum 0), (res8, Just $ VNum 3),- (map, Nothing),+ (mapfn, Nothing), (map2, Nothing), (l, Just $ cons (VNum 1) (cons (VNum 2) (cons (VNum 3) nil))), (l3, Just $ cons (VBool False) (cons (VBool True) (cons (VBool False) nil))),