ntha (empty) → 0.1.0
raw patch · 21 files changed
+3047/−0 lines, 21 filesdep +arraydep +basedep +containerssetup-changed
Dependencies added: array, base, containers, haskeline, hspec, lens, monad-loops, mtl, ntha, pretty, z3, z3-encoding
Files
- LICENSE +30/−0
- README.md +147/−0
- Setup.hs +2/−0
- app/Main.hs +98/−0
- lib/std.ntha +179/−0
- ntha.cabal +80/−0
- src/Ast.hs +168/−0
- src/Eval.hs +228/−0
- src/Infer.hs +266/−0
- src/Lexer.x +110/−0
- src/Parser.y +310/−0
- src/Prologue.hs +82/−0
- src/Refined.hs +139/−0
- src/State.hs +38/−0
- src/Type.hs +287/−0
- src/TypeScope.hs +39/−0
- src/Value.hs +151/−0
- test/EvalSpec.hs +264/−0
- test/InferSpec.hs +268/−0
- test/ParserSpec.hs +160/−0
- test/Spec.hs +1/−0
+ LICENSE view
@@ -0,0 +1,30 @@+Copyright (c) 2016 zjhmale++All rights reserved.++Redistribution and use in source and binary forms, with or without+modification, are permitted provided that the following conditions are met:++ * Redistributions of source code must retain the above copyright+ notice, this list of conditions and the following disclaimer.++ * Redistributions in binary form must reproduce the above+ copyright notice, this list of conditions and the following+ disclaimer in the documentation and/or other materials provided+ with the distribution.++ * Neither the name of Author name here nor the names of other+ contributors may be used to endorse or promote products derived+ from this software without specific prior written permission.++THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS+"AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT+LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR+A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT+OWNER OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,+SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT+LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,+DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY+THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT+(INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE+OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
+ README.md view
@@ -0,0 +1,147 @@+# Ntha Programming Language++[](https://travis-ci.org/zjhmale/Ntha)+[](https://github.com/zjhmale)+[](https://en.wikipedia.org/wiki/Haskell_(programming_language))+[](https://hackage.haskell.org/package/ntha)+[](https://hackage.haskell.org/package/ntha)++a tiny statically typed functional programming language.++## Features++* Global type inference with optional type annotations.+* Lisp flavored syntax with Haskell like semantic inside.+* Support basic types: Integer, Character, String, Boolean, Tuple, List and Record.+* Support unicode keywords.+* Support destructuring.+* ADTs and pattern matching.+* Haskell like type signature for type checking.+* Refined types (still in early stage, just support basic arithmetic operations and propositinal logic, [here is some examples](https://github.com/zjhmale/Ntha/blob/master/examples/misc.ntha#L188-L195)).+* Module system (still in early stage, lack of namespace control).+* Support pattern matching on function parameters.+* Lambdas and curried function by default.+* Global and Local let binding.+* Recursive functions.+* If-then-else / Cond control flow.+* Type alias.+* Do notation.+* Begin block.++## Future Works++* Atoms (need to handle mutable state in evaluation procedure, reference to the [implementation of Clea Programming Language](https://github.com/zjhmale/Clea/blob/master/src/Prologue.hs#L191-211)).+* error propagation (try / catch).+* Lazyness.+* JIT backend.+* Type-classes (desuger to Records).+* Rank-N types ([a naive implementation of First-Class Polymorphism](https://github.com/zjhmale/HMF/tree/master/src/FCP)).+* λπ+* Fully type checked lisp like macros (comply with the internal design of Template Haskell).+* TCO.++## Screenshot++++## Example++```Clojure+(type Name String)+(type Env [(Name . Expr)])++(data Op Add Sub Mul Div Less Iff)++(data Expr+ (Num Number)+ (Bool Boolean)+ (Var Name)+ (If Expr Expr Expr)+ (Let [Char] Expr Expr)+ (LetRec Name Expr Expr)+ (Lambda Name Expr)+ (Closure Expr Env)+ (App Expr Expr)+ (Binop Op (Expr . Expr)))++(let op-map {:add ++ :sub -+ :mul *+ :div /+ :less <+ :iff =})++(arith-eval : (α → (β → Z)) → ((α × β) → (Maybe Expr)))+(ƒ arith-eval [fn (v1 . v2)]+ (Just (Num (fn v1 v2))))++(logic-eval : (α → (β → B)) → ((α × β) → (Maybe Expr)))+(ƒ logic-eval [fn (v1 . v2)]+ (Just (Bool (fn v1 v2))))++(let eval-op+ (λ op v1 v2 ⇒+ (match (v1 . v2)+ (((Just (Num v1)) . (Just (Num v2))) ⇒+ (match op+ (Add ⇒ (arith-eval (:add op-map) (v1 . v2)))+ (Sub ⇒ (arith-eval (:sub op-map) (v1 . v2)))+ (Mul ⇒ (arith-eval (:mul op-map) (v1 . v2)))+ (Div ⇒ (arith-eval (:div op-map) (v1 . v2)))+ (Less ⇒ (logic-eval (:less op-map) (v1 . v2)))+ (Iff ⇒ (logic-eval (:iff op-map) (v1 . v2)))))+ (_ ⇒ Nothing))))++(eval : [(S × Expr)] → (Expr → (Maybe Expr)))+(ƒ eval [env expr]+ (match expr+ ((Num _) ⇒ (Just expr))+ ((Bool _) → (Just expr))+ ((Var x) ⇒ (do Maybe+ (val ← (lookup x env))+ (return val)))+ ((If condition consequent alternative) →+ (match (eval env condition)+ ((Just (Bool true)) → (eval env consequent))+ ((Just (Bool false)) → (eval env alternative))+ (_ → (error "condition should be evaluated to a boolean value"))))+ ((Lambda _ _) → (Just (Closure expr env)))+ ((App fn arg) → (let [fnv (eval env fn)]+ (match fnv+ ((Just (Closure (Lambda x e) innerenv)) →+ (do Maybe+ (argv ← (eval env arg))+ (eval ((x . argv) :: innerenv) e)))+ (_ → (error "should apply arg to a function")))))+ ((Let x e1 in-e2) ⇒ (do Maybe+ (v ← (eval env e1))+ (eval ((x . v) :: env) in-e2)))+ ;; use fix point combinator to approach "Turing-complete"+ ((LetRec x e1 in-e2) → (eval env (Let "Y" (Lambda "h" (App (Lambda "f" (App (Var "f") (Var "f")))+ (Lambda "f" (App (Var "h")+ (Lambda "n" (App (App (Var "f") (Var "f"))+ (Var "n")))))))+ (Let x (App (Var "Y") (Lambda x e1))+ in-e2))))+ ((Binop op (e1 . e2)) => (let [v1 (eval env e1)+ v2 (eval env e2)]+ (eval-op op v1 v2)))))++(begin+ (print "start")+ (let result (match (eval [] (LetRec "fact" (Lambda "n" (If (Binop Less ((Var "n") . (Num 2)))+ (Num 1)+ (Binop Mul ((Var "n") . (App (Var "fact")+ (Binop Sub ((Var "n") . (Num 1))))))))+ (App (Var "fact") (Num 5))))+ ((Just (Num num)) ⇒ (print (int2str num)))+ (Nothing ⇒ (error "oops"))))+ (print result)+ (print "finish"))+```++## License++Copyright © 2016 zjhmale++Distributed under the [](https://en.wikipedia.org/wiki/BSD_licenses)
+ Setup.hs view
@@ -0,0 +1,2 @@+import Distribution.Simple+main = defaultMain
+ app/Main.hs view
@@ -0,0 +1,98 @@+module Main where++import Paths_ntha+import Ast (Expr(..), EPath, isImport)+import Type (Type(..))+import Eval (eval)+import Infer (analyze)+import Refined (checker)+import Parser (parseExpr)+import Value (ValueScope(..), Value(..))+import TypeScope (TypeScope(..))+import Prologue (assumptions, builtins)+import Control.Lens+import Control.Monad (foldM)+import Control.Monad.Trans+import System.Environment+import System.Console.Haskeline+import Data.List (intercalate)+import qualified Data.Map as M+import qualified Data.Set as S+import qualified Control.Exception as E++type Env = (TypeScope, ValueScope)++emptyEnv :: (TypeScope, ValueScope)+emptyEnv = (TypeScope Nothing M.empty, ValueScope Nothing M.empty)++loadFile :: Env -> EPath -> IO Env+loadFile env path = do+ file <- getDataFileName path+ fileContent <- readFile file+ (env', _, _) <- process' env $ parseExpr fileContent+ return env'++loadImport :: Env -> Expr -> IO (Env, Expr)+loadImport env expr = case expr of+ 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+ return (importEnv, continueAst)+ _ -> return (env, expr)++loadLib :: IO Env+loadLib = do+ assumps <- assumptions+ loadFile (assumps, builtins) "lib/std.ntha"++process' :: Env -> Expr -> IO (Env, Value, Type)+process' env expr = do+ ((importAssumps, importBuiltins), ast) <- loadImport env expr+ (assumps', t) <- analyze ast importAssumps S.empty+ checker ast assumps'+ let (builtins', v) = eval ast importBuiltins+ return ((assumps', builtins'), v, t)++process :: Env -> String -> IO Env+process env@(assumps, prevBuiltins) expr =+ E.catch (do+ (env', v, t) <- process' env $ parseExpr expr+ putStrLn $ show v ++ " : " ++ show t+ return env')+ (\(E.ErrorCall e) -> do+ putStrLn e+ return (assumps, prevBuiltins))++loop :: Env -> InputT IO Env+loop env = do+ minput <- getInputLine "λ> "+ case minput of+ Nothing -> do+ outputStrLn "Goodbye."+ return emptyEnv+ Just input -> (liftIO $ process env input) >>= (\env' -> loop env')++prologueMessage :: String+prologueMessage = intercalate "\n"+ [" _ __ __ __",+ " / | / / / /_ / /_ ____ _",+ " / |/ / / __/ / __ \\ / __ `/",+ " / /| / / /_ / / / // /_/ /",+ " /_/ |_/ \\__/ /_/ /_/ \\__,_/",+ ""+ ]++main :: IO Env+main = do+ env <- loadLib+ args <- getArgs+ case (args ^? element 0) of+ Just arg -> if arg == "repl"+ then repl env+ else do+ file <- readFile arg+ process env file+ Nothing -> repl env+ where repl ev = do putStrLn prologueMessage+ runInputT defaultSettings (loop ev)
+ lib/std.ntha view
@@ -0,0 +1,179 @@+(data Maybe a (Just a) Nothing)++(monad Maybe {:return (λ x → (Just x))+ :>>= (λ x f → (match x+ ((Just v) → (f v))+ (Nothing → Nothing)))})++(ƒ len [l]+ (match l+ ([] ⇒ 0)+ (_ :: t ⇒ (+ 1 (len t)))))++(ƒ map [f xs]+ (match xs+ ([] ⇒ [])+ (h :: t ⇒ ((f h) :: (map f t)))))++(ƒ fold [f s xs]+ (match xs+ ([] ⇒ s)+ (h :: t ⇒ (fold f (f s h) t))))++(ƒ filter [f xs]+ (match xs+ ([] ⇒ [])+ (h :: t ⇒ (if (f h)+ (h :: (filter f t))+ (filter f t)))))++(ƒ range [x y]+ (let [rec-range (λ x y res ⇒ (if (> x y)+ res+ (rec-range x (- y 1) (y :: res))))]+ (rec-range x y [])))++(ƒ lookup [name pairs]+ (match pairs+ ([] ⇒ Nothing)+ ((k . v) :: t ⇒ (if (= name k)+ (Just v)+ (lookup name t)))))++(ƒ lookup! [default name pairs]+ (match pairs+ ([] ⇒ default)+ ((k . v) :: t ⇒ (if (= name k)+ v+ (lookup! default name t)))))++(ƒ exists?+ [e l]+ (match l+ ([] → false)+ (h :: t → (if (= h e)+ true+ (exists? e t)))))++(asserteq (exists? 3 [3 2 1]) true)+(asserteq (exists? 33 [3 2 1]) false)++(ƒ diff-list+ [l1 l2]+ (match l1+ ([] → [])+ (h :: t → (if (exists? h l2)+ (diff-list t l2)+ (h :: (diff-list t l2))))))++(asserteq (diff-list [3 2 1] [2 1]) [3])++(ƒ exists-map?+ [e m]+ (match (lookup e m)+ (Nothing → false)+ (_ → true)))++(ƒ diff-map+ [m l]+ (match m+ ([] → [])+ ((k . v) :: t → (if (exists? k l)+ (diff-map t l)+ ((k . v) :: (diff-map t l))))))++(asserteq (diff-map [(1 . 2) (2 . 3)] [1]) [(2 . 3)])+(asserteq (diff-map [(1 . 2) (2 . 3) (3 . 3)] [1 2]) [(3 . 3)])++(ƒ union-map+ [m1 m2]+ (match m2+ ([] → m1)+ ((k . v) :: t → (if (exists-map? k m1)+ (union-map m1 t)+ ((k . v) :: (union-map m1 t))))))++(asserteq (union-map [(1 . 1) (3 . 3)] [(1 . 3) (3 . 1) (2 . 2)]) [(2 . 2) (1 . 1) (3 . 3)])++(ƒ map-map+ [f m]+ (match m+ ([] → [])+ ((k . v) :: t → ((k . (f v)) :: (map-map f t)))))++(asserteq (map-map (λ x → (+ x 1)) [(1 . 1) (2 . 2)]) [(1 . 2) (2 . 3)])++(ƒ nub+ [l]+ (match l+ ([] → [])+ (h :: t → (if (exists? h t)+ (nub t)+ (h :: (nub t))))))++(asserteq (nub [1 2 3]) [1 2 3])+(asserteq (nub [1 1 1 2 2 3]) [1 2 3])++(ƒ conj [e l]+ (reverse (e :: (reverse l))))++(ƒ concat [l1 l2]+ (match l2+ ([] → l1)+ (h :: t → (concat (conj h l1) t))))++(asserteq (concat [1 2 3] [4 5 6]) [1 2 3 4 5 6])+(asserteq (concat "123" "456") "123456")++(ƒ flatten [l]+ (match l+ ([] → [])+ (h :: t → (concat h (flatten t)))))++(asserteq (flatten [[1] [2] [3]]) [1 2 3])++(ƒ empty? [l]+ (match l+ ([] → true)+ (_ → false)))++(asserteq (empty? []) true)+(asserteq (empty? [3]) false)++(ƒ head [l]+ (match l+ ([] → (error "empty list"))+ (h :: _ → h)))++(asserteq (head [1 2 3]) 1)++(ƒ tail [l]+ (match l+ ([] → [])+ (_ :: t → t)))++(asserteq (tail [1 2 3]) [2 3])++(ƒ take [n l]+ (if (> n 0)+ ((head l) :: (take (- n 1) (tail l)))+ []))++(asserteq (take 3 [1 2 3 4 5 6]) [1 2 3])+(asserteq (take 2 "_.x") "_.")++(ƒ max [a b] (if (≥ a b) a b))++(ƒ zero? [n] (= n 0))++(ƒ fst+ [tuple]+ (match tuple+ ((v . _) → v)+ (_ → (error "need apply a tuple value"))))++(ƒ snd+ [tuple]+ (match tuple+ ((_ . v) → v)+ (_ → (error "need apply a tuple value"))))
+ ntha.cabal view
@@ -0,0 +1,80 @@+name: ntha+version: 0.1.0+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+license: BSD3+license-file: LICENSE+author: zjhmale+maintainer: zjhmale@gmail.com+copyright: 2016 zjhmale+category: Compiler+ , Language+build-type: Simple+-- extra-source-files:+cabal-version: >=1.10+extra-source-files:+ README.md+data-files:+ lib/std.ntha+++library+ hs-source-dirs: src+ exposed-modules: Ast+ , Type+ , TypeScope+ , Value+ , State+ , Infer+ , Eval+ , Refined+ , Prologue+ , Lexer+ , Parser+ build-depends: base >= 4.7 && < 5+ , containers+ , pretty+ , monad-loops+ , array+ , z3 >=4.4.1+ , z3-encoding+ build-tools: happy+ , alex+ default-extensions: TupleSections+ , StandaloneDeriving+ default-language: Haskell2010+ ghc-options: -Wall++executable ntha+ hs-source-dirs: app+ main-is: Main.hs+ other-modules: Paths_ntha+ ghc-options: -threaded -rtsopts -with-rtsopts=-N -Wall+ build-depends: base+ , ntha+ , containers+ , lens+ , haskeline+ , mtl+ default-language: Haskell2010++test-suite ntha-test+ type: exitcode-stdio-1.0+ other-modules: EvalSpec+ , InferSpec+ , ParserSpec+ hs-source-dirs: test+ main-is: Spec.hs+ build-depends: base+ , ntha+ , hspec >= 1.3+ , containers+ , pretty+ default-extensions: UnicodeSyntax+ ghc-options: -threaded -rtsopts -with-rtsopts=-N -Wall+ default-language: Haskell2010++source-repository head+ type: git+ location: https://github.com/zjhmale/ntha
+ src/Ast.hs view
@@ -0,0 +1,168 @@+module Ast where++import Type+import Data.Maybe (fromMaybe)+import Data.List (intercalate)+import qualified Data.Map as M+import qualified Text.PrettyPrint as PP++type EName = String -- variable name+type EPath = String+type EField = String+type EIndent = Int+type TypeVariable = Type -- just for documentation++data Expr = EVar EName+ | EAccessor Expr EField+ | ENum Int+ | EStr String+ | EChar Char+ | EBool Bool+ | EList [Expr]+ | ETuple [Expr]+ | ERecord (M.Map EField Expr)+ | EUnit+ | ELambda [Named] (Maybe Type) [Expr]+ | EApp Expr Expr+ | EIf Expr [Expr] [Expr]+ | EPatternMatching Expr [Case]+ | ELetBinding Pattern Expr [Expr]+ | EDestructLetBinding Pattern [Pattern] [Expr]+ | EDataDecl EName Type [TypeVariable] [TypeConstructor]+ | ETypeSig EName Type -- explicit type annotation+ | EImport EPath+ | EProgram [Expr]+ deriving (Eq, Ord)++isImport :: Expr -> Bool+isImport expr = case expr of+ EImport _ -> True+ _ -> False++-- for do block desuger to bind+data Bind = Bind EName Expr+ | Return Expr+ | Single Expr++-- for cond desuger to if+data Clause = Clause Expr Expr+ | Else Expr++data TypeConstructor = TypeConstructor EName [Type]+ deriving (Eq, Ord)++data Named = Named EName (Maybe Type)+ deriving (Eq, Ord)++data Pattern = WildcardPattern+ | IdPattern EName+ | NumPattern Int+ | BoolPattern Bool+ | CharPattern Char+ | TuplePattern [Pattern]+ | TConPattern EName [Pattern]+ deriving (Eq, Ord)++data Case = Case Pattern [Expr]+ deriving (Eq, Ord)++-- temp structure for parser+data EVConArg = EVCAVar EName+ | EVCAOper EName [EName]+ | EVCAList EVConArg+ | EVCATuple [EVConArg]+ deriving (Show, Eq, Ord)++data EVConstructor = EVConstructor EName [EVConArg]+ deriving (Show, Eq, Ord)++substName :: M.Map EName EName -> Expr -> Expr+substName subrule (EVar name) = EVar $ fromMaybe name $ M.lookup name subrule+substName subrule (EAccessor expr field) = EAccessor (substName subrule expr) field+substName subrule (EList exprs) = EList $ map (substName subrule) exprs+substName subrule (ETuple exprs) = ETuple $ map (substName subrule) exprs+substName subrule (ERecord pairs) = ERecord $ M.map (substName subrule) pairs+substName subrule (ELambda nameds t exprs) = ELambda newNames t newExprs+ where+ newNames = map (\(Named name t') -> Named (fromMaybe name $ M.lookup name subrule) t') nameds+ newExprs = map (substName subrule) exprs+substName subrule (EApp fn arg) = EApp (substName subrule fn) (substName subrule arg)+substName subrule (EIf cond thenInstrs elseInstrs) = EIf newCond newThenInstrs newElseInstrs+ where+ newCond = substName subrule cond+ newThenInstrs = map (substName subrule) thenInstrs+ newElseInstrs = map (substName subrule) elseInstrs+substName subrule (EPatternMatching expr cases) = EPatternMatching newExpr newCases+ where+ newCases = map (\(Case pat exprs) -> Case pat (map (substName subrule) exprs)) cases+ newExpr = substName subrule expr+substName subrule (ELetBinding pat expr exprs) = ELetBinding pat (substName subrule expr) $ map (substName subrule) exprs+substName _ e = e++tab :: EIndent -> String+tab i = intercalate "" $ take i $ repeat "\t"++stringOfNamed :: Named -> String+stringOfNamed (Named name t) = name ++ case t of+ Just t' -> ":" ++ show t'+ Nothing -> ""++stringofNameds :: [Named] -> String+stringofNameds = unwords . (map stringOfNamed)++stringOfExpr :: Expr -> String+stringOfExpr e = case e of+ EApp fn arg -> "<" ++ show fn ++ ">(" ++ show arg ++ ")"+ ELambda params annoT body -> "λ" ++ stringofNameds params ++ (case annoT of+ Just annoT' -> " : " ++ show annoT'+ Nothing -> "") ++ " = \n" ++ intercalate "" (map (\instr -> "\t" ++ show instr ++ "\n") body)+ EIf cond thenInstrs elseInstrs -> "if " ++ show cond ++ " then \n" ++ stringOfInstrs thenInstrs ++ "else \n" ++ stringOfInstrs elseInstrs where+ stringOfInstrs instrs = intercalate "" $ map (\instr -> "\t" ++ show instr ++ "\n") instrs+ EProgram instrs -> intercalate "" $ map (\instr -> show instr ++ "\n") instrs+ _ -> reprOfExpr 0 e++stringOfCase :: EIndent -> Case -> String+stringOfCase i (Case pat outcomes) = "\n" ++ tab i ++ show pat ++ " ⇒ " ++ show outcomes++stringOfCases :: EIndent -> [Case] -> String+stringOfCases i cases = intercalate "" (map (stringOfCase i) cases)++reprOfExpr :: EIndent -> Expr -> String+reprOfExpr i e = case e of+ EVar n -> tab i ++ n+ EAccessor e' f -> tab i ++ reprOfExpr 0 e' ++ "." ++ f+ ENum v -> tab i ++ show v+ EStr v -> tab i ++ v+ EChar v -> tab i ++ [v]+ EBool v -> tab i ++ show v+ EUnit -> tab i ++ "()"+ EList es -> tab i ++ show es+ ETuple es -> "(" ++ intercalate "," (map (reprOfExpr 0) es) ++ ")"+ ERecord pairs -> "{" ++ intercalate "," (M.elems $ M.mapWithKey (\f v -> f ++ ": " ++ reprOfExpr 0 v) pairs) ++ "}"+ EApp _ _ -> tab i ++ show e+ ELambda params annoT body -> tab i ++ "λ" ++ stringofNameds params ++ (case annoT of+ Just annoT' -> " : " ++ show annoT'+ Nothing -> "") ++ " = \n" ++ intercalate "" (map (\instr -> "\t" ++ reprOfExpr (i + 1) instr ++ "\n") body)+ EIf cond thenInstrs elseInstrs -> tab i ++ "if " ++ show cond ++ " then \n" ++ stringOfInstrs thenInstrs ++ tab i ++ "else \n" ++ stringOfInstrs elseInstrs where+ stringOfInstrs instrs = intercalate "" $ map (\instr -> "\t" ++ reprOfExpr (i + 1) instr ++ "\n") instrs+ EPatternMatching input cases -> tab i ++ "match " ++ show input ++ stringOfCases i cases+ EDataDecl name _ tvars tcons -> tab i ++ "data " ++ name ++ " " ++ unwords (map show tvars) ++ " = " ++ intercalate " | " (map (\(TypeConstructor name' types) -> name' ++ case types of+ [] -> ""+ _ -> " " ++ unwords (map show types)) tcons)+ EDestructLetBinding main args instrs -> tab i ++ "let " ++ show main ++ " " ++ unwords (map show args) ++ " = \n" ++ intercalate "" (map (\instr -> reprOfExpr (i + 1) instr ++ "\n") instrs)+ ELetBinding main def body -> tab i ++ "let " ++ show main ++ " " ++ show def ++ " in " ++ intercalate "\n" (map show body)+ ETypeSig name t -> tab i ++ "(" ++ name ++ " : " ++ show t ++ ")"+ EImport path -> "import " ++ path+ EProgram instrs -> intercalate "" $ map (\instr -> reprOfExpr i instr ++ "\n") instrs++instance Show Expr where+ showsPrec _ x = shows $ PP.text $ stringOfExpr x++instance Show Pattern where+ show WildcardPattern = "_"+ show (NumPattern val) = "pint→" ++ show val+ show (BoolPattern val) = "pbool→" ++ show val+ show (CharPattern val) = "pchar→" ++ show val+ show (IdPattern name) = "'" ++ name ++ "'"+ show (TuplePattern pattens) = "(" ++ intercalate "," (map show pattens) ++ ")"+ show (TConPattern name pattens) = name ++ " " ++ show pattens
+ src/Eval.hs view
@@ -0,0 +1,228 @@+module Eval where++import Ast+import Value+import Data.Maybe (fromMaybe)+import Prelude hiding (lookup)+import qualified Data.Map as M+import qualified Data.Set as S++type Exclude = S.Set EName++evalFn :: Value -> Value -> ValueScope -> Value+evalFn (Fn f) arg scope = f arg scope+evalFn _ _ _ = VUnit++chainingFn :: EName -> Value -> Value+chainingFn argName next = Fn (\oarg _ -> Fn (\arg scope -> let margs = case oarg of+ FnApArgs pairs -> let v = fromMaybe VUnit $ M.lookup "***" pairs+ in FnApArgs $ M.insert "***" arg $ M.insert argName v pairs+ _ -> FnApArgs $ M.fromList [(argName, oarg), ("***", arg)]+ in evalFn next margs scope))++chaininLastFn :: EName -> [Expr] -> Value+chaininLastFn argName body = Fn (\arg scope -> let scope' = case arg of+ FnApArgs pairs -> foldl (\env (k, v) -> insert k v env)+ scope+ (M.toList $ M.insert argName (fromMaybe VUnit $ M.lookup "***" pairs) pairs)+ _ -> insert argName arg scope+ in snd $ foldl (\(env, val) instr -> val `seq` eval instr env) (scope', VUnit) body)++destrChainingFn :: Pattern -> Value -> Value+destrChainingFn pat next = Fn (\oarg _ -> Fn (\arg scope -> let margs = case oarg of+ DestrFnApArgs args freeVal -> DestrFnApArgs (args ++ [PatVal pat freeVal]) arg+ _ -> DestrFnApArgs [PatVal pat oarg] arg+ in evalFn next margs scope))++destrChaininLastFn :: Pattern -> [Expr] -> Value+destrChaininLastFn pat body = Fn (\arg scope -> let scope' = case arg of+ DestrFnApArgs args freeVal -> let s = foldl (\env (PatVal pat' val) -> define pat' val env)+ scope args+ in define pat freeVal s+ _ -> define pat arg scope+ in snd $ foldl (\(env, val) instr -> val `seq` eval instr env) (scope', VUnit) body)++tConChainingFn :: Tag -> Value -> Value+tConChainingFn tag next = Fn (\oarg _ -> Fn (\arg scope -> let targs = case oarg of+ TConArgs args tag' -> TConArgs (args ++ [arg]) tag'+ _ -> TConArgs [oarg, arg] tag+ in evalFn next targs scope))++tConChaininLastFn :: Tag -> Value+tConChaininLastFn tag = Fn (\arg _ -> let args = case arg of+ TConArgs args' _ -> args'+ VUnit -> []+ _ -> [arg]+ in Adt tag args)++excludePatternBoundNames :: Pattern -> Exclude -> Exclude+excludePatternBoundNames pat excluded = case pat of+ IdPattern name -> S.insert name excluded+ TuplePattern pats -> foldl (\exc p -> excludePatternBoundNames p exc) excluded pats+ TConPattern _ pats -> foldl (\exc p -> excludePatternBoundNames p exc) excluded pats+ _ -> excluded++visit :: Expr -> ValueScope -> ValueEnv -> Exclude -> (ValueScope, ValueEnv, Exclude)+visit expr scope capturedEnv excluded = case expr of+ EList values -> foldl (\(s, c, e) value -> visit value s c e)+ (scope, capturedEnv, excluded) values+ EIf cond thenInstrs elseInstrs -> (sco'', env'', exc'') where+ (sco, env, exc) = visit cond scope capturedEnv excluded+ (sco', env', exc') = foldl (\(s, c, e) value -> visit value s c e)+ (sco, env, exc) thenInstrs+ (sco'', env'', exc'') = foldl (\(s, c, e) value -> visit value s c e)+ (sco', env', exc') elseInstrs+ EVar name -> if name `notElem` excluded+ then let (scope', val) = eval expr scope+ in (scope', M.insert name val capturedEnv, excluded)+ else (scope, capturedEnv, excluded)+ EApp fn arg -> let (s, c, e) = visit fn scope capturedEnv excluded+ in visit arg s c e+ EDestructLetBinding main _ _ -> (scope, capturedEnv, excludePatternBoundNames main excluded)+ EPatternMatching input cases -> let (scope', capturedEnv', excluded') = visit input scope capturedEnv excluded+ in foldl (\(s, c, e) (Case pat outcomes) -> let e' = excludePatternBoundNames pat e+ in let (s', c', _) = foldl (\(sco, env, exc) instr -> visit instr sco env exc)+ (s, c, e') outcomes+ in (s', c', e))+ (scope', capturedEnv', excluded') cases+ _ -> (scope, capturedEnv, excluded)++envCapturingFnWrapper :: Value -> Expr -> ValueScope -> Value+envCapturingFnWrapper fn expr scope = case expr of+ (ELambda params _ instrs) -> mkFn capturedEnv where+ excluded = foldl (\exc (Named name _) -> S.insert name exc) S.empty params+ capturedEnv = mkCapturedEnv excluded instrs+ (EDestructLetBinding (IdPattern name) args instrs) -> mkFn capturedEnv where+ excluded = foldl (\exc pat -> excludePatternBoundNames pat exc) (S.singleton name) args+ capturedEnv = mkCapturedEnv excluded instrs+ _ -> VUnit+ where+ mkCapturedEnv excluded instrs = let (_, capturedEnv, _) = foldl (\(s, c, e) instr -> visit instr s c e)+ (scope, M.empty, excluded) instrs+ in capturedEnv+ mkFn capturedEnv = Fn (\arg scope' -> let scope'' = foldl (\env (k, v) -> insert k v env)+ scope' $ M.toList capturedEnv+ in evalFn fn arg scope'')++-- to predicate if a value is match specific pattern+match :: Value -> Pattern -> ValueScope -> (ValueScope, Bool)+match input pattern scope = case pattern of+ WildcardPattern -> (scope, True)+ IdPattern name -> (insert name input scope, True)+ NumPattern val -> (scope, input == (VNum val))+ BoolPattern val -> (scope, input == (VBool val))+ CharPattern val -> (scope, input == (VChar val))+ TuplePattern pats -> case input of+ VTuple items -> if length items /= length pats+ then (scope, False)+ else isAllMatch items pats+ _ -> (scope, False)+ TConPattern name pats -> case input of+ Adt tag args -> if name == tag && length pats == length args+ then isAllMatch args pats+ else (scope, False)+ _ -> (scope, False)+ where+ isAllMatch items pats = let (scope', isMatchs) = foldl (\(env, matchs) (item, pat) -> let (env', isMatch) = match item pat env+ in (env', matchs ++ [isMatch]))+ (scope, []) $ zip items pats+ in (scope', all id isMatchs)++define :: Pattern -> Value -> ValueScope -> ValueScope+define pattern val scope = case pattern of+ IdPattern name -> insert name val scope+ TuplePattern pats -> case val of+ VTuple items -> defineVals pats items+ _ -> error $ "Invalid value " ++ show val ++ " for pattern " ++ show pattern+ -- maybe should check pattern name and length of pats and args just like the match function above+ TConPattern _ pats -> case val of+ Adt _ args -> defineVals pats args+ _ -> error $ "Invalid value " ++ show val ++ " for pattern " ++ show pattern+ _ -> scope+ where+ defineVals pats items = foldl (\env (pat, item) -> define pat item env)+ scope $ zip pats items++eval :: Expr -> ValueScope -> (ValueScope, Value)+eval expr scope = case expr of+ ENum v -> (scope, VNum v)+ EBool v -> (scope, VBool v)+ EChar v -> (scope, VChar v)+ EStr v -> (scope, makeList $ map VChar v)+ EUnit -> (scope, VUnit)+ EVar name -> case lookup name scope of+ Just val -> (scope, val)+ Nothing -> error $ "Unknown identifier " ++ show expr+ EAccessor obj field -> case eval obj scope of+ (_, VRecord pairs) -> case M.lookup field pairs of+ Just val -> (scope, val)+ Nothing -> error $ "No field " ++ field ++ "in "++ show obj+ _ -> error $ "Not a record " ++ show obj+ ETuple values -> (scope, VTuple $ map (\v -> snd (eval v scope)) values)+ EList values -> (scope, makeList $ map (\v -> snd (eval v scope)) values)+ ERecord pairs -> (scope, VRecord $ M.map (\v -> snd (eval v scope)) pairs)+ ELambda params _ instrs -> let fnV = case reverse params of+ (Named name _):xs -> fnChain where+ lastFn = chaininLastFn name instrs+ fnChain = foldl (\fn (Named n _) -> chainingFn n fn) lastFn xs+ _ -> VUnit+ in (scope, envCapturingFnWrapper fnV expr scope)+ EApp fn arg -> case fnV of+ Fn f -> let (_, argV) = eval arg scope'+ in (scope, f argV scope')+ Adt _ _ -> case eval arg scope' of+ (_, VUnit) -> (scope, fnV)+ _ -> error $ "Error while evaluating " ++ show expr ++ ": " ++ show fnV ++ " constructor doesn't take arguments"+ _ -> error $ "Error while evaluating " ++ show expr ++ ": " ++ show fnV ++ " is not a function"+ where+ scope' = child scope+ (_, fnV) = eval fn scope'+ EIf cond thenInstrs elseInstrs -> let (_, condV) = eval cond scope+ in case condV of+ VBool v -> if v+ then (scope, evalInstrs thenInstrs)+ else (scope, evalInstrs elseInstrs)+ where+ evalInstrs instrs = let scope' = child scope+ in snd $ foldl (\(env, val) instr -> val `seq` eval instr env) (scope', VUnit) instrs+ _ -> error $ "Error while evaluating " ++ show expr ++ ": the condition is not a boolean"+ EPatternMatching input cases -> findPattern inputV cases+ where (_, inputV) = eval input scope+ findPattern :: Value -> [Case] -> (ValueScope, Value)+ findPattern val [] = error $ "Match exception: " ++ show input ++ " = " ++ show val ++ " didn't match any case of " ++ show expr+ findPattern val ((Case pat instrs):cs) = let (scope', isMatch) = match val pat $ child scope+ in if isMatch+ then (scope, snd $ foldl (\(env, val') instr -> val' `seq` eval instr env) (scope', VUnit) instrs)+ else findPattern val cs+ ELetBinding name def body -> let (scope', _) = eval (EDestructLetBinding name [] [def]) scope+ in (scope, snd $ foldl (\(env, val) instr -> val `seq` eval instr env) (scope', VUnit) body)+ EDestructLetBinding main args instrs -> if length args == 0+ -- define variable+ then let (_, val) = foldl (\(env, val') instr -> val' `seq` eval instr env) (child scope, VUnit) instrs+ in (define main val scope, val)+ -- define function+ else case main of+ IdPattern name -> let fnV = case reverse args of+ pat:pats -> fnChain where+ lastFn = destrChaininLastFn pat instrs+ fnChain = foldl (\fn p -> destrChainingFn p fn) lastFn pats+ _ -> VUnit+ in let fn = envCapturingFnWrapper fnV expr scope+ in (insert name fn scope, fn)+ _ -> error $ "Function name can only be a name, whereas a pattern " ++ show main ++ " was provided in " ++ show expr+ EDataDecl _ _ _ typeConstructors -> let scope' = foldl makeChain scope typeConstructors+ in (scope', VUnit)+ where+ makeChain env (TypeConstructor name types) = let fnV = case reverse types of+ _:ts -> fnChain where+ lastFn = tConChaininLastFn name+ fnChain = foldl (\fn _ -> tConChainingFn name fn)+ lastFn ts+ _ -> VUnit+ in if fnV == VUnit+ then insert name (Adt name []) env+ else insert name fnV env+ ETypeSig _ _ -> (scope, VUnit)+ EProgram instrs -> foldl (\(env, val) instr -> val `seq` eval instr env)+ (child scope, VUnit) instrs+ _ -> error $ "not support eval expr: " ++ show expr
+ src/Infer.hs view
@@ -0,0 +1,266 @@+module Infer where++import Ast+import Type+import TypeScope+import State+import Data.IORef+import Control.Monad (when, zipWithM_, foldM, forM_)+import Control.Monad.Loops (anyM)+import qualified Data.Map as M+import qualified Data.Set as S+import Prelude hiding (lookup)++type NonGeneric = (S.Set Type)++occursInType :: Type -> Type -> Infer Bool+occursInType v t = do+ tP <- prune t+ case tP of+ TOper _ ts -> occursIn v ts+ v' -> return $ v == v'++occursIn :: Type -> [Type] -> Infer Bool+occursIn t = anyM (occursInType t)++isGeneric :: Type -> NonGeneric -> Infer Bool+isGeneric t nonGeneric = not <$> (occursIn t $ S.toList nonGeneric)++fresh :: Type -> NonGeneric -> Infer Type+fresh t nonGeneric = do+ mappings <- newIORef M.empty -- A mapping of TypeVariables to TypeVariables+ let freshrec ty = prune ty >>= (\tyP -> case tyP of+ TVar _ _ _ -> do+ isG <- isGeneric tyP nonGeneric+ if isG+ then do+ m <- readIORef mappings+ case M.lookup tyP m of+ Just tVar -> return tVar+ Nothing -> do+ newVar <- makeVariable+ modifyIORef mappings $ M.insert tyP newVar+ return newVar+ else return tyP+ TOper name types -> do+ newTypes <- mapM freshrec types+ return $ TOper name newTypes+ TCon name types dataType -> do+ newTypes <- mapM freshrec types+ newDataType <- freshrec dataType+ return $ TCon name newTypes newDataType+ TRecord valueTypes -> do+ newValueTypes <- foldM (\acc (k, v) -> do+ fv <- freshrec v+ return $ M.insert k fv acc)+ M.empty $ M.toList valueTypes+ return $ TRecord newValueTypes+ _ -> return tyP)+ freshrec t++getType :: TName -> TypeScope -> NonGeneric -> Infer Type+getType name scope nonGeneric = case lookup name scope of+ Just var -> fresh var nonGeneric+ Nothing -> error $ "Undefined symbol " ++ name++adjustType :: Type -> Type+adjustType t = case t of+ TCon _ types dataType -> functionT types dataType+ _ -> t++unify :: Type -> Type -> Infer ()+unify t1 t2 = do+ t1P <- prune t1+ t2P <- prune t2+ let t1PA = adjustType t1P+ let t2PA = adjustType t2P+ case (t1PA, t2PA) of+ (a@(TVar _ inst _), b) -> when (a /= b) $ do+ isOccurs <- occursInType a b+ when isOccurs $ error "Recusive unification"+ writeIORef inst $ Just b+ (a@(TOper _ _), b@(TVar _ _ _)) -> unify b a+ (a@(TOper name1 types1), b@(TOper name2 types2)) -> if name1 /= name2 || (length types1) /= (length types2)+ then error $ "Type mismatch " ++ show a ++ " ≠ " ++ show b+ else zipWithM_ unify types1 types2+ (a@(TRecord types1), b@(TRecord types2)) -> mapM_ (\(k, t2') -> do+ case M.lookup k types1 of+ Just t1' -> unify t2' t1'+ Nothing -> error $ "Cannot unify, no field " ++ k ++ " " ++ show a ++ ", " ++ show b)+ $ M.toList types2+ _ -> error $ "Can not unify " ++ show t1 ++ ", " ++ show t2++visitPattern :: Pattern -> TypeScope -> NonGeneric -> Infer (TypeScope, NonGeneric, Type)+visitPattern pattern scope nonGeneric = case pattern of+ WildcardPattern -> do+ resT <- makeVariable+ return (scope, nonGeneric, resT)+ IdPattern name -> do+ resT <- makeVariable+ return (insert name resT scope, S.insert resT nonGeneric, resT)+ NumPattern _ -> return (scope, nonGeneric, intT)+ BoolPattern _ -> return (scope, nonGeneric, boolT)+ CharPattern _ -> return (scope, nonGeneric, charT)+ TuplePattern items -> do+ (itemTypes, newScope, newNonGeneric) <- foldM (\(types, env, nonGen) item -> do+ (newEnv, newNonGen, itemT) <- visitPattern item env nonGen+ return (types ++ [itemT], newEnv, newNonGen))+ ([], scope, nonGeneric) items+ return (newScope, newNonGeneric, productT itemTypes)+ TConPattern name patterns -> do+ (patTypes, newScope, newNonGeneric) <- foldM (\(types, env, nonGen) pat -> do+ (newEnv, newNonGen, patT) <- visitPattern pat env nonGen+ return (types ++ [patT], newEnv, newNonGen))+ ([], scope, nonGeneric) patterns+ case lookup name newScope of+ Nothing -> error $ "Unknow type constructor " ++ name+ Just tconT -> case tconT of+ TCon _ _ _ -> do+ (TCon _ types dataType) <- fresh tconT newNonGeneric+ if (length patterns) /= (length types)+ then error $ "Bad arity: case " ++ show pattern ++ " provided " ++ (show . length) patterns ++ " arguments whereas " ++ name ++ " takes " ++ (show . length) types+ else do+ zipWithM_ unify patTypes types+ return (newScope, newNonGeneric, dataType)+ _ -> error $ "Invalid type constructor " ++ name++definePattern :: Pattern -> Type -> TypeScope -> Infer TypeScope+definePattern pattern t scope = do+ tP <- prune t+ case pattern of+ IdPattern name -> return $ insert name tP scope+ TuplePattern items -> case tP of+ TOper _ types -> do+ newScope <- foldM (\env (pat, patT) -> do+ newEnv <- definePattern pat patT env+ return newEnv)+ scope $ zip items types+ return newScope+ _ -> error $ "Invalid type " ++ show tP ++ " for pattern " ++ show pattern+ TConPattern _ patterns -> case tP of+ -- t is always functionT for now so a little non-sense for this case.+ TCon _ types _ -> do+ newScope <- foldM (\env (pat, patT) -> do+ newEnv <- definePattern pat patT env+ return newEnv)+ scope $ zip patterns types+ return newScope+ TOper _ types -> do+ newScope <- foldM (\env (pat, patT) -> do+ newEnv <- definePattern pat patT env+ return newEnv)+ scope $ zip patterns types+ return newScope+ _ -> error $ "Invalid type " ++ show tP ++ " for pattern " ++ show pattern+ _ -> return scope++analyze :: Expr -> TypeScope -> NonGeneric -> Infer (TypeScope, Type)+analyze expr scope nonGeneric = case expr of+ ENum _ -> return (scope, intT)+ EBool _ -> return (scope, boolT)+ EChar _ -> return (scope, charT)+ EStr _ -> return (scope, strT)+ EUnit -> return (scope, unitT)+ EList exprs -> do+ valueT <- makeVariable+ -- type checking procedure, since types of elems in a list should be the same.+ forM_ exprs (\e -> do+ (_, eT) <- analyze e scope nonGeneric+ unify valueT eT)+ return (scope, listT valueT)+ ETuple exprs -> do+ types <- foldM (\types expr' -> do+ (_, ty) <- analyze expr' scope nonGeneric+ return $ types ++ [ty])+ [] exprs+ return (scope, productT types)+ ERecord pairs -> do+ valueTypes <- foldM (\vts (k, v) -> do+ (_, t) <- analyze v scope nonGeneric+ return $ M.insert k t vts)+ M.empty $ M.toList pairs+ return (scope, TRecord valueTypes)+ EVar name -> (scope,) <$> getType name scope nonGeneric+ EApp fn arg -> do+ (_, fnT) <- analyze fn scope nonGeneric+ (_, argT) <- analyze arg scope nonGeneric+ rtnT <- makeVariable+ unify (functionT [argT] rtnT) fnT+ return (scope, rtnT)+ ELambda params annoT instructions -> do+ let newScope = child scope+ (paramTypes, newScope', newNonGeneric) <- foldM (\(types', env', nonGeneric') (Named name t) ->+ case t of+ Just t' -> return (types' ++ [t'], insert name t' env', S.insert t' nonGeneric')+ Nothing -> do+ t' <- makeVariable+ return (types' ++ [t'], insert name t' env', S.insert t' nonGeneric'))+ ([], newScope, nonGeneric) params+ rtnT <- foldM (\_ instr -> snd <$> analyze instr newScope' newNonGeneric) unitT instructions+ case annoT of+ Just annoT' -> unify rtnT annoT' -- type propagation from return type to param type+ Nothing -> return ()+ -- use fresh just to make sure sequence of lambda abstractions with same type var name could work well e.g.+ -- ((λ(x: α) : α → x) 3)+ -- ((λ(x: α) : α → x) true)+ (scope,) <$> fresh (functionT paramTypes rtnT) nonGeneric+ EAccessor obj field -> do+ (_, objT) <- analyze obj scope nonGeneric+ fieldT <- makeVariable+ let desiredT = TRecord $ M.fromList [(field, fieldT)]+ unify objT desiredT+ return (scope, fieldT)+ EIf cond thenInstructions elseInstructions -> do+ (_, condT) <- analyze cond scope nonGeneric+ unify condT boolT+ (newScope, thenT) <- foldM (\(env, _) instr -> analyze instr env nonGeneric)+ (scope, unitT) thenInstructions+ (newScope', elseT) <- foldM (\(env, _) instr -> analyze instr env nonGeneric)+ (newScope, unitT) elseInstructions+ unify thenT elseT+ return (newScope', thenT)+ ELetBinding main def body -> do+ (scope', _) <- analyze (EDestructLetBinding main [] [def]) scope nonGeneric+ foldM (\(env, _) instr -> analyze instr env nonGeneric) (scope', unitT) body+ EDestructLetBinding main args instructions -> do+ let name = case main of+ IdPattern n -> n ++ "-sig"+ _ -> ""+ let typeSig = lookup name scope+ let newScope = child scope+ (newScope', newNonGeneric, letTV) <- visitPattern main newScope nonGeneric+ let newNonGeneric' = S.insert letTV newNonGeneric+ (argTypes, newScope'', newNonGeneric'') <- foldM (\(types, env, nonGen) arg -> do+ (newEnv, newNonGen, argT) <- visitPattern arg env nonGen+ return (types ++ [argT], newEnv, newNonGen))+ ([], newScope', newNonGeneric') args+ rtnT <- foldM (\_ instr -> snd <$> analyze instr newScope'' newNonGeneric'') unitT instructions+ let letT = functionT argTypes rtnT+ newScope''' <- definePattern main letT newScope''+ case typeSig of+ Just (TSig ta) -> do+ let ta' = extractType ta+ unify ta' letT+ _ -> return ()+ return (newScope''', letT)+ EDataDecl _ t _ tconstructors -> do+ let newScope = foldl (\env (TypeConstructor conName conTypes) ->+ insert conName (TCon conName conTypes t) env)+ scope tconstructors+ return (newScope, t)+ EPatternMatching input cases -> do+ (_, inputT) <- analyze input scope nonGeneric+ resT <- makeVariable+ resT' <- foldM (\rt (Case pat outcomes) -> do+ let newScope = child scope+ (newScope', newNonGeneric, patT) <- visitPattern pat newScope nonGeneric+ unify patT inputT+ (_, caseT) <- foldM (\(env, _) outcome -> analyze outcome env newNonGeneric)+ (newScope', unitT) outcomes+ unify caseT rt+ return rt)+ resT cases+ return (scope, resT')+ ETypeSig name t -> return (insert (name ++ "-sig") (TSig t) scope, unitT)+ EProgram instructions -> foldM (\(env, _) instr -> analyze instr env nonGeneric) (scope, unitT) instructions+ _ -> error $ "not support infer expr: " ++ show expr
+ src/Lexer.x view
@@ -0,0 +1,110 @@+{+module Lexer where+import Ast (EName)+import Data.Char (toUpper)+}++%wrapper "basic"++$upper = [A-Z]+$lower = [a-z]+$greek = [α-ω]+$digit = [0-9]+$operator = [\+\-\*\/\%\=\>\<\∧\∨\¬\?\'\~\!\.]+$chars = [$lower $upper $digit $operator $greek]+$eol = [\n]++tokens :-+ $eol ;+ $white+ ;+ ";;".* ; --comments+ -- TODO support multiline comments+ "data" { \_ -> DATA }+ "match" { \_ -> MATCH }+ "begin" { \_ -> BEGIN }+ "type" { \_ -> TYPE }+ "if" { \_ -> IF }+ "cond" { \_ -> COND }+ "else" { \_ -> ELSE }+ "monad" { \_ -> MONAD }+ "do" { \_ -> DO }+ "return" { \_ -> RETURN }+ "ƒ" | "fun" { \_ -> DEFUN }+ "λ" | "lambda" { \_ -> LAMBDA }+ "⇒" | "=>" | "→" | "->" { \_ -> RARROW }+ "⇐" | "<=" | "←" | "<-" { \_ -> LARROW }+ "[" { \_ -> LBRACKET }+ "]" { \_ -> RBRACKET }+ "(" { \_ -> LPAREN }+ ")" { \_ -> RPAREN }+ "{" { \_ -> LBRACE }+ "}" { \_ -> RBRACE }+ "_" { \_ -> WILDCARD }+ "." { \_ -> DOT }+ ":" $chars+ { \s -> KEYWORD (tail s) }+ ":" { \_ -> COLON }+ "∷" | "::" { \_ -> DOUBLECOLON }+ "|" { \_ -> BAR }+ "let" { \_ -> LET }+ "Z" { \_ -> NUMBERT }+ "B" { \_ -> BOOLT }+ "C" { \_ -> CHART }+ "S" { \_ -> STRT }+ "×" { \_ -> PRODUCT }+ "import" { \_ -> IMPORT }+ "true" | "false" { \s -> BOOLEAN (read ([toUpper (s!!0)] ++ tail s)) }+ $upper $chars* { \s -> CON s }+ $lower $chars* { \s -> VAR s }+ $greek { \s -> TVAR (s!!0) }+ \"[^\"]*\" { \s -> STRING ((tail . init) s) }+ '[^'\"]{1}' { \s -> CHAR ((head . tail . init) s) }+ $operator | "≠" | "≤" | "≥" { \s -> OPERATOR s }+ $digit+ { \s -> NUMBER (read s) }+ "-" $digit+ { \s -> NUMBER (read s) }++{+data Token = DATA+ | MATCH+ | BEGIN+ | TYPE+ | DEFUN+ | LAMBDA+ | MONAD+ | DO+ | RETURN+ | IF+ | COND+ | ELSE+ | RARROW+ | LARROW+ | LBRACKET+ | RBRACKET+ | LPAREN+ | RPAREN+ | LBRACE+ | RBRACE+ | WILDCARD+ | DOT+ | COLON+ | DOUBLECOLON+ | BAR+ | VAR EName+ | TVAR Char+ | CON EName -- constructor names or uppercase symbols+ | LET+ | NUMBERT+ | BOOLT+ | CHART+ | STRT+ | PRODUCT+ | IMPORT+ | KEYWORD String+ | OPERATOR String+ | BOOLEAN Bool+ | NUMBER Int+ | STRING String+ | CHAR Char+ deriving(Eq, Show)++scanTokens = alexScanTokens+}
+ src/Parser.y view
@@ -0,0 +1,310 @@+{+module Parser where++import Ast+import Type+import Refined (convertProg')+import Lexer+import State+import Control.Monad+import Data.List+import Data.IORef+import Data.Maybe (fromMaybe, fromJust)+import qualified Data.Map as M+import System.IO.Unsafe (unsafePerformIO)+}++%name expr+%tokentype { Token }+%error { parseError }++%token+ data { DATA }+ match { MATCH }+ begin { BEGIN }+ type { TYPE }+ defun { DEFUN }+ lambda { LAMBDA }+ monad { MONAD }+ do { DO }+ return { RETURN }+ if { IF }+ cond { COND }+ else { ELSE }+ rarrow { RARROW }+ larrow { LARROW }+ con { CON $$ }+ '[' { LBRACKET }+ ']' { RBRACKET }+ '(' { LPAREN }+ ')' { RPAREN }+ '{' { LBRACE }+ '}' { RBRACE }+ '_' { WILDCARD }+ '.' { DOT }+ ':' { COLON }+ '::' { DOUBLECOLON }+ '|' { BAR }+ let { LET }+ import { IMPORT }+ TNumber { NUMBERT }+ TBool { BOOLT }+ TChar { CHART }+ TString { STRT }+ product { PRODUCT }+ keyword { KEYWORD $$ }+ VAR { VAR $$ }+ TVAR { TVAR $$ }+ OPERATOR { OPERATOR $$ }+ number { NUMBER $$ }+ boolean { BOOLEAN $$ }+ string { STRING $$ }+ char { CHAR $$ }++%%++Program : Exprs { EProgram $1 }++Exprs : Expr { [$1] }+ | Expr Exprs { $1 : $2 }++Expr : '(' defun VAR '[' Args ']' FormsPlus ')' { EDestructLetBinding (IdPattern $3) $5 $7 }+ | '(' data con SimpleArgs VConstructors ')' { unsafePerformIO $ do+ (env, vars) <- foldM (\(env, vars) arg -> do+ var <- makeVariable+ return (M.insert arg var env, vars ++ [var]))+ (M.empty, []) $4+ let dataType = TOper $3 vars+ let constructors' = map (\(EVConstructor cname cargs) -> let cargs' = map getType+ cargs+ where readEnv scope n = fromMaybe unitT $ M.lookup n scope+ getType arg = case arg of+ EVCAVar aname -> readEnv env aname+ EVCAOper aname operArgs -> TOper aname $ map (readEnv env) operArgs+ EVCAList arg' -> listT (getType arg')+ EVCATuple args -> productT (map getType args)+ in TypeConstructor cname cargs')+ $5+ return $ EDataDecl $3 dataType vars constructors' }+ | '(' let Pattern FormsPlus ')' { EDestructLetBinding $3 [] $4 }+ | '(' type con VConArg ')' { unsafePerformIO $ do+ $4 `seq` modifyIORef aliasMap $ M.insert $3 $4+ return EUnit }+ | '(' monad con Form ')' { unsafePerformIO $ do+ $4 `seq` modifyIORef monadMap $ M.insert $3 $4+ return $ EDestructLetBinding (IdPattern $3) [] [$4] }+ | '(' VAR ':' Type ')' { ETypeSig $2 $4 }+ | '(' import VAR ')' { EImport (getPathStr $3) }+ | Form { $1 }++-- TODO should support arg parameter such as (Maybe N umber)+SimpleArgs : {- empty -} { [] }+ | VAR SimpleArgs { $1 : $2 }++VConArg : VAR { EVCAVar $1 }+ | con { unsafePerformIO $ do+ alias <- readIORef aliasMap+ case M.lookup $1 alias of+ Just vconarg -> return vconarg+ Nothing -> if $1 == "String"+ then return $ EVCAList (EVCAOper "Char" []) -- special case for String pattern+ else return $ EVCAOper $1 [] }+ | '(' con SimpleArgs ')' { EVCAOper $2 $3 }+ -- TODO more specs here+ | '[' VConArg ']' { EVCAList $2 }+ | '(' TupleVConArgs ')' { EVCATuple $2 }++TupleVConArgs : VConArg '.' VConArg { [$1, $3] }+ | TupleVConArgs '.' VConArg { $1 ++ [$3] }++VConArgs : VConArg { [$1] }+ | VConArg VConArgs { $1 : $2 }++VConstructor : con { EVConstructor $1 [] }+ | '(' con VConArgs ')' { EVConstructor $2 $3 }+ | '(' VConArg keyword VConArg ')' { EVConstructor $3 [$2, $4] }++VConstructors : VConstructor { [$1] }+ | VConstructor VConstructors { $1 : $2 }++Args : {- empty -} { [] }+ | Pattern Args { $1 : $2 }++Nameds : {- empty -} { [] }+ | VAR Nameds { (Named $1 Nothing) : $2 }+ | '(' VAR ':' Type ')' Nameds { (Named $2 (Just $4)) : $6 }++binding : Pattern Form { ELetBinding $1 $2 [] }++bindings : binding { [$1] }+ | binding bindings { $1 : $2 }++bind : Form { Single $1 }+ | '(' return Form ')' { Return $3 }+ | '(' VAR larrow Form ')' { Bind $2 $4 }++binds : bind { [$1] }+ | bind binds { $1 : $2 }++Clause : '(' else rarrow Form ')' { Else $4 }+ | '(' Form rarrow Form ')' { Clause $2 $4 }++Clauses : Clause { [$1] }+ | Clause Clauses { $1 : $2 }++Form : '(' match Form Cases ')' { EPatternMatching $3 $4 }+ | '(' lambda Nameds rarrow FormsPlus ')' { ELambda $3 Nothing $5 }+ | '(' lambda Nameds ':' AtomType rarrow FormsPlus ')' { ELambda $3 (Just $5) $7 }+ | '(' let '[' bindings ']' FormsPlus ')' { head $ foldr (\(ELetBinding pat def _) body -> [ELetBinding pat def body]) $6 $4 }+ | '(' if Form Form Form ')' { EIf $3 [$4] [$5] }+ | '(' cond Clauses ')' { case last $3 of+ Else alt -> foldr (\(Clause cond consequent) alternative -> EIf cond [consequent] [alternative])+ alt (init $3)+ _ -> error "last clause in cond should be an else" }+ -- do block desuger to nested >>= and return, inspired by http://www.haskellforall.com/2014/10/how-to-desugar-haskell-code.html+ | '(' do con binds ')' { unsafePerformIO $ do+ monads <- readIORef monadMap+ return $ case M.lookup $3 monads of+ Just (ERecord pairs) -> case M.lookup "return" pairs of+ Just rtn -> case M.lookup ">>=" pairs of+ Just bind -> foldr (\b next -> case next of+ EUnit -> case b of+ Bind n e -> error "illegal do expression"+ Return e -> EApp newRtn e+ Single e -> e+ _ -> case b of+ Bind n e -> EApp (EApp newBind e) (ELambda [Named n Nothing] Nothing [next])+ Return e -> EApp newRtn e+ Single e -> e)+ EUnit $4+ where+ newBind = aliasArgName bind+ newRtn = aliasArgName rtn+ Nothing -> error $ "bind function is not defined for " ++ $3 ++ " monad"+ Nothing -> error $ "return function is not defined for " ++ $3 ++ " monad"+ _ -> error $ $3 ++ " monad is not defined" }+ | '(' ListForms ')' { $2 }+ | '(' TupleFroms ')' { ETuple $2 }+ | '(' Form FormsPlus ')' { foldl (\oper param -> (EApp oper param)) $2 $3 }+ | '(' Form keyword Form ')' { foldl (\oper param -> (EApp oper param)) (EVar $3) [$2, $4] }+ | '(' OPERATOR FormsPlus ')' { case $3 of+ a:[] -> EApp (EVar $2) a+ a:b:[] -> EApp (EApp (EVar $2) a) b+ a:b:xs -> foldl (\oper param -> (EApp (EApp (EVar $2) oper) param)) (EApp (EApp (EVar $2) a) b) xs }+ | '[' FormsStar ']' { EList $2 }+ | '{' RecordForms '}' { ERecord $2 }+ | '(' keyword Form ')' { EAccessor $3 $2 }+ | '(' begin Exprs ')' { EProgram $3 }+ | Atom { $1 }++RecordForms : keyword Form { M.singleton $1 $2 }+ | RecordForms keyword Form { M.insert $2 $3 $1 }++ListForms : Form '::' Form { EApp (EApp (EVar "Cons") $1) $3 }+ | Form '::' ListForms { EApp (EApp (EVar "Cons") $1) $3 }++TupleFroms : Form '.' Form { [$1, $3] }+ | TupleFroms '.' Form { $1 ++ [$3] }++FormsPlus : Form { [$1] }+ | Form FormsPlus { $1 : $2 }++FormsStar : {- empty -} { [] }+ | Form FormsStar { $1 : $2 }++Pattern : '_' { WildcardPattern }+ | VAR { IdPattern $1 }+ | number { NumPattern $1 }+ | boolean { BoolPattern $1 }+ | char { CharPattern $1 }+ | string { foldr (\p t -> TConPattern "Cons" [p, t]) (TConPattern "Nil" []) (map CharPattern $1) }+ | con { TConPattern $1 [] }+ | '(' con Args ')' { TConPattern $2 $3 }+ -- e.g. (t1 :~> t2)+ | '(' Pattern keyword Pattern ')' { TConPattern $3 [$2, $4] }+ | '(' TuplePatterns ')' { TuplePattern $2 }+ | '[' ']' { TConPattern "Nil" [] }+ | '[' Patterns ']' { foldr (\p t -> TConPattern "Cons" [p, t]) (TConPattern "Nil" []) $2 }+ | ListPatterns { $1 }+ | '(' ListDestructPats ')' { $2 }++Patterns : Pattern { [$1] }+ | Pattern Patterns { $1 : $2 }++TuplePatterns : Pattern '.' Pattern { [$1, $3] }+ | TuplePatterns '.' Pattern { $1 ++ [$3] }++ListPatterns : Pattern '::' Pattern { TConPattern "Cons" [$1, $3] }+ | Pattern '::' ListPatterns { TConPattern "Cons" [$1, $3] }++ListDestructPats : Pattern '::' Pattern { TConPattern "Cons" [$1, TConPattern "Cons" [$3, TConPattern "Nil" []]] }+ | Pattern '::' ListDestructPats { TConPattern "Cons" [$1, $3] }++Case : '(' Pattern rarrow FormsPlus ')' { Case $2 $4 }++Cases : Case { [$1] }+ | Case Cases { $1 : $2 }++Atom : boolean { EBool $1 }+ | number { ENum $1 }+ | string { EStr $1 }+ | char { EChar $1 }+ | VAR { EVar $1 }+ | OPERATOR { EVar $1 }+ | con { EVar $1 }++-- parsing type++Type : AtomType { $1 }+ | AtomType rarrow Type { arrowT $1 $3 }++-- TODO support type alias in type signature+AtomType : TVAR { fromJust $ M.lookup $1 tvarMap }+ | TNumber { intT }+ | TBool { boolT }+ | TChar { charT }+ | TString { strT }+ | con Types { TOper $1 $2 }+ | '[' Type ']' { listT $2 }+ | '(' TupleTypes ')' { productT $2 }+ | '(' Type ')' { $2 }+ | RefinedType { $1 }++RefinedType : '(' VAR ':' Type '|' Form ')' { TRefined $2 $4 (convertProg' $6) }++Types : {- empty -} { [] }+ | Type Types { $1 : $2 }++TupleTypes : Type product Type { [$1, $3] }+ | TupleTypes product Type { $1 ++ [$3] }++{+aliasMap :: IORef (M.Map String EVConArg)+aliasMap = createState M.empty++monadMap :: IORef (M.Map String Expr)+monadMap = createState M.empty++aliasArgName :: Expr -> Expr+aliasArgName expr@(ELambda nameds t exprs) = substName subrule expr+ where+ subrule = M.fromList $ foldl (\rule (Named name _) -> rule ++ [(name, name ++ "__monadarg__")]) [] nameds++tvarMap :: M.Map Char Type+tvarMap = unsafePerformIO $ do+ foldM (\m greek -> do+ tvar <- makeVariable+ return $ M.insert greek tvar m)+ M.empty ['α'..'ω']++getPathStr :: EPath -> EPath+getPathStr s = (map f s) ++ ".ntha"+ where f '.' = '/'+ f c = c++parseError :: [Token] -> a+parseError _ = error "Parse error"++parseExpr :: String -> Expr+parseExpr = expr . scanTokens+}
+ src/Prologue.hs view
@@ -0,0 +1,82 @@+module Prologue where++import Ast+import Type+import Value+import State+import TypeScope+import Debug.Trace+import qualified Data.Map as M++mkTCon :: TypeConstructor -> Expr -> Type+mkTCon (TypeConstructor name types) (EDataDecl _ t _ _) = TCon name types t+mkTCon _ _ = error "not support"++assumptions :: Infer TypeScope+assumptions = do+ tvarA <- makeVariable+ tvarB <- makeVariable+ let name = "List"+ let vars = [tvarA]+ let dataType = TOper name vars+ let consConstructor = TypeConstructor "Cons" [tvarA, TOper "List" [tvarA]]+ let nilConstructor = TypeConstructor "Nil" []+ let listData = EDataDecl "List" dataType vars [consConstructor, nilConstructor]+ return $ TypeScope Nothing $ M.fromList [("+", functionT [intT, intT] intT),+ ("-", functionT [intT, intT] intT),+ ("*", functionT [intT, intT] intT),+ ("/", functionT [intT, intT] intT),+ ("%", functionT [intT, intT] intT),+ ("=", functionT [tvarB, tvarB] boolT),+ ("≠", functionT [tvarB, tvarB] boolT),+ ("<", functionT [intT, intT] boolT),+ (">", functionT [intT, intT] boolT),+ ("≤", functionT [intT, intT] boolT),+ ("≥", functionT [intT, intT] boolT),+ ("∧", functionT [boolT, boolT] boolT),+ ("∨", functionT [boolT, boolT] boolT),+ ("¬", functionT [boolT] boolT),+ ("int2str", functionT [intT] strT),+ ("bool2str", functionT [boolT] strT),+ ("asserteq", functionT [tvarB, tvarB] unitT),+ ("print", functionT [strT] unitT),+ ("error", functionT [strT] tvarB),+ ("reverse", functionT [listT tvarB] (listT tvarB)),+ ("list?", functionT [tvarB] boolT),+ ("string?", functionT [tvarB] boolT),+ ("Cons", mkTCon consConstructor listData),+ ("Nil", mkTCon nilConstructor listData),+ ("inc", functionT [intT] intT),+ ("dec", functionT [intT] intT)]++builtins :: ValueScope+builtins = ValueScope Nothing $ M.fromList [("+", binFn (\(VNum a) (VNum b) -> (VNum $ a + b))),+ ("-", binFn (\(VNum a) (VNum b) -> (VNum $ a - b))),+ ("*", binFn (\(VNum a) (VNum b) -> (VNum $ a * b))),+ ("/", binFn (\(VNum a) (VNum b) -> (VNum $ a `div` b))),+ ("%", binFn (\(VNum a) (VNum b) -> (VNum $ a `mod` b))),+ ("=", binFn (\a b -> VBool $ a == b)),+ ("≠", binFn (\a b -> VBool $ a /= b)),+ ("<", binFn (\a b -> VBool $ a < b)),+ (">", binFn (\a b -> VBool $ a > b)),+ ("≤", binFn (\a b -> VBool $ a <= b)),+ ("≥", binFn (\a b -> VBool $ a >= b)),+ ("∧", binFn (\(VBool a) (VBool b) -> VBool $ a && b)),+ ("∨", binFn (\(VBool a) (VBool b) -> VBool $ a || b)),+ ("¬", Fn (\(VBool b) _ -> VBool $ not b)),+ ("int2str", Fn (\(VNum n) _ -> strV $ show n)),+ ("bool2str", Fn (\(VBool b) _ -> strV $ show b)),+ ("asserteq", binFn (\a b -> if a == b+ then VUnit+ else error $ show a ++ " and " ++ show b ++ " not equal.")),+ ("print", Fn (\v _ -> trace (desugerStrV v) VUnit)),+ ("error", Fn (\v _ -> error $ desugerStrV v)),+ ("reverse", Fn (\v _ -> reverseList v)),+ ("list?", Fn (\v _ -> case v of+ Adt "Cons" _ -> VBool True+ _ -> VBool False)),+ ("string?", Fn (\v _ -> VBool $ isString v)),+ ("Cons", binFn (\a b -> cons a b)),+ ("Nil", nil),+ ("inc", Fn (\(VNum n) _ -> VNum $ n + 1)),+ ("dec", Fn (\(VNum n) _ -> VNum $ n - 1))]
+ src/Refined.hs view
@@ -0,0 +1,139 @@+module Refined where++import Ast+import Type+import TypeScope+import Z3.Class+import Z3.Logic+import Z3.Context+import Z3.Assertion+import Z3.Monad+import Prelude hiding (lookup)+import Control.Monad (mapM_)+import Control.Monad.IO.Class (liftIO)++genPred :: Term -> Z3Pred+genPred term = case term of+ TmLT t1 t2 -> PAssert $ Less t1 t2+ TmGT t1 t2 -> PAssert $ Greater t1 t2+ TmLE t1 t2 -> PAssert $ LessE t1 t2+ TmGE t1 t2 -> PAssert $ GreaterE t1 t2+ TmEqual t1 t2 -> PAssert $ Equal t1 t2+ TmAnd t1 t2 -> PConj (genPred t1) (genPred t2)+ TmOr t1 t2 -> PDisj (genPred t1) (genPred t2)+ TmNot t -> PNeg (genPred t)+ _ -> error $ "not support term: " ++ show term++replaceRtnTerm :: String -> Term -> Term -> Term+replaceRtnTerm rtnName rtnTerm predTerm = case predTerm of+ TmVar n -> if n == rtnName then rtnTerm else predTerm+ TmNum _ -> predTerm+ TmLT t1 t2 -> TmLT (replaceRtnTerm' t1) (replaceRtnTerm' t2)+ TmGT t1 t2 -> TmGT (replaceRtnTerm' t1) (replaceRtnTerm' t2)+ TmLE t1 t2 -> TmLE (replaceRtnTerm' t1) (replaceRtnTerm' t2)+ TmGE t1 t2 -> TmGE (replaceRtnTerm' t1) (replaceRtnTerm' t2)+ TmSub t1 t2 -> TmSub (replaceRtnTerm' t1) (replaceRtnTerm' t2)+ TmAdd t1 t2 -> TmAdd (replaceRtnTerm' t1) (replaceRtnTerm' t2)+ TmMul t1 t2 -> TmMul (replaceRtnTerm' t1) (replaceRtnTerm' t2)+ TmDiv t1 t2 -> TmDiv (replaceRtnTerm' t1) (replaceRtnTerm' t2)+ TmEqual t1 t2 -> TmEqual (replaceRtnTerm' t1) (replaceRtnTerm' t2)+ TmAnd t1 t2 -> TmAnd (replaceRtnTerm' t1) (replaceRtnTerm' t2)+ TmOr t1 t2 -> TmOr (replaceRtnTerm' t1) (replaceRtnTerm' t2)+ TmNot t -> TmNot (replaceRtnTerm' t)+ TmIf t1 t2 t3 -> TmIf (replaceRtnTerm' t1) (replaceRtnTerm' t2) (replaceRtnTerm' t3)+ where replaceRtnTerm' = replaceRtnTerm rtnName rtnTerm++genRtnPred :: String -> Term -> Term -> Z3Pred+-- use neg to find counterexamples+genRtnPred rtnName rtnTerm = PNeg . genPred . (replaceRtnTerm rtnName rtnTerm)++convertProg' :: Expr -> Term+convertProg' expr = case expr of+ ENum n -> TmNum n+ EVar name -> TmVar name+ EApp fn arg -> case fn of+ EApp (EVar op) arg' -> opConstruct argTerm' argTerm+ where argTerm' = convertProg' arg'+ argTerm = convertProg' arg+ opConstruct = case op of+ "+" -> TmAdd+ "-" -> TmSub+ "*" -> TmMul+ "/" -> TmDiv+ "<" -> TmLT+ ">" -> TmGT+ "≤" -> TmLE+ "≥" -> TmGE+ "=" -> TmEqual+ "∧" -> TmAnd+ "∨" -> TmOr+ _ -> error $ "not support op: " ++ op+ EVar op -> case op of+ "¬" -> let argTerm = convertProg' arg+ in TmNot argTerm+ _ -> error $ "not support op: " ++ op+ _ -> error $ "not support fn: " ++ show fn+ EIf cond (thenInstruction:[]) (elseInstruction:[]) -> TmIf condTerm thenTerm elseTerm+ where condTerm = convertProg' cond+ thenTerm = convertProg' thenInstruction+ elseTerm = convertProg' elseInstruction+ _ -> error $ "not support expr: " ++ show expr++convertProg :: Expr -> TypeScope -> IO Z3Pred+convertProg expr scope = case expr of+ -- only support exists and exists2 for now+ EDestructLetBinding main args (instruction:[]) -> do+ let name = case main of+ IdPattern n -> n ++ "-sig"+ _ -> ""+ let typeSig = lookup name scope+ let argNames = map (\pat -> case pat of+ IdPattern n -> n+ _ -> show pat)+ args+ case typeSig of+ Just (TSig ta) -> do+ let terms = extractTerm ta+ let predNames = getPredNames ta+ case predNames of+ -- (¬ ⊥) always satisfied+ [] -> return PFalse+ _ -> case (argNames, terms) of+ ([n], [rtnTerm']) -> return $ PExists n RTInt $ genRtnPred' rtnTerm'+ ([n1, n2], [rtnTerm']) -> return $ PExists2 n1 n2 RTInt $ genRtnPred' rtnTerm'+ ([n], [argTerm, rtnTerm']) -> return $ PExists n RTInt $ PConj (genPred argTerm) $ genRtnPred' rtnTerm'+ ([n1, n2], [argTerm1, argTerm2, rtnTerm']) -> return $ PExists2 n1 n2 RTInt $ PConj (PConj (genPred argTerm1) $ genPred argTerm2) $ genRtnPred' rtnTerm'+ _ -> error $ "not support args: " ++ show argNames ++ " and terms: " ++ show terms+ where rtnName = last predNames+ rtnTerm = convertProg' instruction+ genRtnPred' :: Term -> Z3Pred+ genRtnPred' = genRtnPred rtnName rtnTerm+ -- (¬ ⊥) always satisfied+ _ -> return PFalse+ EProgram (instruction:_) -> convertProg instruction scope+ _ -> error $ "not support expr: " ++ show expr++checkPre :: Z3Pred -> Z3SMT () (Result, Maybe Model)+checkPre pre = local $ do+ ast <- encode pre+ local (assert ast >> getModel)++checker :: Expr -> TypeScope -> IO ()+checker expr scope = case expr of+ EDestructLetBinding _ _ _ -> do+ progPred <- convertProg expr scope+ -- trade off+ let adts = [("", [("", [("", RTInt)])])]+ ret <- runSMT adts () $ do+ (r, _mm) <- checkPre progPred+ case r of+ Unsat -> do+ core <- getUnsatCore+ liftIO $ sequence_ (map print core)+ return r+ other -> return other+ if ret == Right Unsat+ then return ()+ else error "refined type check failed"+ EProgram instructions -> mapM_ (\instr -> checker instr scope) instructions+ _ -> return ()
+ src/State.hs view
@@ -0,0 +1,38 @@+module State where++import Data.IORef+import System.IO.Unsafe (unsafePerformIO)++createState :: a -> IORef a+createState = unsafePerformIO . newIORef++readState :: IORef a -> a+readState = unsafePerformIO . readIORef++type Infer a = IO a++currentId :: IORef Int+currentId = createState 0++nextId :: Infer Int+nextId = do+ v <- readIORef currentId+ writeIORef currentId (v + 1)+ return v++resetId :: Infer ()+resetId = writeIORef currentId 0++currentUniqueName :: IORef Char+currentUniqueName = createState 'α'++nextUniqueName :: Infer String+nextUniqueName = do+ char <- readIORef currentUniqueName+ if char == 'ω'+ then resetUniqueName+ else writeIORef currentUniqueName $ succ char+ return [char]++resetUniqueName :: Infer ()+resetUniqueName = writeIORef currentUniqueName 'α'
+ src/Type.hs view
@@ -0,0 +1,287 @@+module Type where++import State+import Data.IORef+import Data.List (intercalate)+import Control.Monad (foldM, liftM)+import Data.Maybe (fromMaybe)+import Z3.Class+import Z3.Logic+import Z3.Assertion+import Z3.Monad+import qualified Data.Map as M+import qualified Data.Set as S+import qualified Text.PrettyPrint as PP+import System.IO.Unsafe (unsafePerformIO)++type Id = Int+type TName = String+type TField = String+type Types = [Type]+type TInstance = Maybe Type+type Z3Pred = Pred Term RType Assertion++data Type = TVar Id (IORef TInstance) TName -- type variable+ | TOper TName Types -- type operator+ | TRecord (M.Map TField Type)+ | TCon TName Types Type+ | TSig Type+ | TRefined String Type Term++-- extract normal type from refined type for type inference+extractType :: Type -> Type+extractType t = case t of+ -- just support arrow type for now+ TOper "→" args -> TOper "→" (map extractType args)+ TRefined _ t' _ -> t'+ _ -> t++extractTerm :: Type -> [Term]+extractTerm t = case t of+ TOper "→" args -> args >>= extractTerm+ TRefined _ _ tm -> [tm]+ _ -> []++getPredNames :: Type -> [String]+getPredNames t = case t of+ TOper "→" args -> args >>= getPredNames+ TRefined n _ _ -> [n]+ _ -> []++intT :: Type+intT = TOper "Number" []++boolT :: Type+boolT = TOper "Boolean" []++charT :: Type+charT = TOper "Char" []++listT :: Type -> Type -- list type is not polymorphism+listT t = TOper "List" [t]++productT :: Types -> Type -- tuple type, product type is a name from Algebraic Data type+productT ts = TOper "*" ts++arrowT :: Type -> Type -> Type -- function type with single param+arrowT fromType toType = TOper "→" $ [fromType, toType]++functionT :: Types -> Type -> Type+functionT paramsT rtnT = foldr (\paramT resT -> arrowT paramT resT) rtnT paramsT++strT :: Type+strT = listT charT++unitT :: Type+unitT = TOper "()" []++prune :: Type -> Infer Type+prune t = case t of+ TVar _ inst _ -> do+ instV <- readIORef inst+ case instV of+ Just inst' -> do+ newInstance <- prune inst'+ writeIORef inst $ Just newInstance+ return newInstance+ Nothing -> return t+ _ -> return t++stringOfType :: M.Map TName TName -> Type -> Infer String+stringOfType subrule (TVar _ inst name) = do+ instV <- readIORef inst+ case instV of+ Just inst' -> stringOfType subrule inst'+ Nothing -> return $ fromMaybe "α" $ M.lookup name subrule+stringOfType subrule (TOper name args) = case name of+ "*" -> do+ argsStr <- (intercalate " * ") <$> mapM (stringOfType subrule) args+ return $ "(" ++ argsStr ++ ")"+ "List" -> do+ argStr <- stringOfType subrule $ args!!0+ return $ "[" ++ argStr ++ "]"+ "→" -> do+ argT <- prune $ args!!0+ rtnT <- prune $ args!!1+ argStr <- stringOfType subrule argT+ rtnStr <- stringOfType subrule rtnT+ let adjust t s = case t of+ TOper "→" _ -> "(" ++ s ++ ")"+ _ -> s+ let argStr' = adjust argT argStr+ let rtnStr' = adjust rtnT rtnStr+ return $ argStr' ++ " → " ++ rtnStr'+ _ -> if (length args) == 0+ then return name+ else do+ argsStr <- unwords <$> mapM (stringOfType subrule) args+ return $ "(" ++ name ++ " " ++ argsStr ++ ")"+stringOfType subrule (TRecord pairs) = do+ pairsStr <- (intercalate ", ") <$> (mapM (\(k, v) -> ((k ++ ": ") ++) <$> stringOfType subrule v) $ M.toList pairs)+ return $ "{" ++ pairsStr ++ "}"+stringOfType subrule (TCon name types dataType) = do+ dataTypeStr <- stringOfType subrule dataType+ case types of+ [] -> return dataTypeStr+ _ -> do+ typesStr <- (intercalate ", ") <$> mapM (stringOfType subrule) types+ return $ "(" ++ name ++ " " ++ typesStr ++ " ⇒ " ++ dataTypeStr ++ ")"+stringOfType subrule (TSig t) = liftM ("typesig: " ++) $ stringOfType subrule t+stringOfType subrule (TRefined _ t _) = liftM ("refined: " ++) $ stringOfType subrule t++getFreeVars :: Type -> Infer (S.Set TName)+getFreeVars (TVar _ inst name) = do+ instV <- readIORef inst+ case instV of+ Just inst' -> getFreeVars inst'+ Nothing -> return $ S.singleton name+getFreeVars (TOper _ args) = foldM (\acc arg -> do+ freeVars <- getFreeVars arg+ return $ S.union freeVars acc)+ S.empty args+getFreeVars (TRecord pairs) = foldM (\acc (_, v) -> do+ freeVars <- getFreeVars v+ return $ S.union freeVars acc)+ S.empty $ M.toList pairs+getFreeVars (TCon _ types dataType) = foldM (\acc t -> do+ freeVars <- getFreeVars t+ return $ S.union freeVars acc)+ S.empty $ types ++ [dataType]+getFreeVars (TSig t) = getFreeVars t+getFreeVars (TRefined _ t _) = getFreeVars t++normalize :: Type -> Infer String+normalize t = do+ freeVars <- getFreeVars t+ let subrule = M.map (\c -> [c]) $ M.fromList $ zip (S.toList freeVars) ['α'..'ω']+ stringOfType subrule t++instance Show Type where+ showsPrec _ x = shows $ PP.text $ unsafePerformIO $ normalize x++instance Eq Type where+ TVar id1 inst1 vname1 == TVar id2 inst2 vname2 = id1 == id2 && instV1 == instV2 && vname1 == vname2 where+ instV1 = readState inst1+ instV2 = readState inst2+ TOper name1 args1 == TOper name2 args2 = name1 == name2 && args1 == args2+ TRecord pairs1 == TRecord pairs2 = pairs1 == pairs2+ TCon name1 types1 dataType1 == TCon name2 types2 dataType2 = name1 == name2 && types1 == types2 && dataType1 == dataType2+ TSig t1 == TSig t2 = t1 == t2+ TRefined x1 t1 tm1 == TRefined x2 t2 tm2 = x1 == x2 && t1 == t2 && tm1 == tm2+ _ == _ = False++instance Ord Type where+ TVar id1 inst1 vname1 <= TVar id2 inst2 vname2 = id1 <= id2 && instV1 <= instV2 && vname1 <= vname2 where+ instV1 = readState inst1+ instV2 = readState inst2+ TOper name1 args1 <= TOper name2 args2 = name1 <= name2 && args1 <= args2+ TRecord pairs1 <= TRecord pairs2 = pairs1 <= pairs2+ TCon name1 types1 dataType1 <= TCon name2 types2 dataType2 = name1 <= name2 && types1 <= types2 && dataType1 <= dataType2+ TSig t1 <= TSig t2 = t1 <= t2+ TRefined x1 t1 tm1 <= TRefined x2 t2 tm2 = x1 <= x2 && t1 <= t2 && tm1 <= tm2+ _ <= _ = False++makeVariable :: Infer Type+makeVariable = do+ i <- nextId+ name <- nextUniqueName+ instRef <- newIORef Nothing+ return $ TVar i instRef name++-- for refined type++data Term = TmVar String+ | TmNum Int+ | TmLT Term Term+ | TmGT Term Term+ | TmLE Term Term+ | TmGE Term Term+ | TmSub Term Term+ | TmAdd Term Term+ | TmMul Term Term+ | TmDiv Term Term+ | TmEqual Term Term+ | TmAnd Term Term+ | TmOr Term Term+ | TmNot Term+ | TmIf Term Term Term++deriving instance Eq Term+deriving instance Ord Term+deriving instance Show Term++-- currently just support integer+data RType = RTInt++deriving instance Eq RType+deriving instance Ord RType++instance Z3Encoded Term where+ encode (TmVar x) = do+ ctx <- getQualifierCtx+ case M.lookup x ctx of+ Just (idx, _) -> return idx+ Nothing -> smtError $ "Can't find variable " ++ x+ encode (TmNum n) = mkIntSort >>= mkInt n+ encode (TmLT t1 t2) = encode (Less t1 t2)+ encode (TmGT t1 t2) = encode (Greater t1 t2)+ encode (TmLE t1 t2) = encode (LessE t1 t2)+ encode (TmGE t1 t2) = encode (GreaterE t1 t2)+ encode (TmAdd t1 t2) = do+ a1 <- encode t1+ a2 <- encode t2+ mkAdd [a1, a2]+ encode (TmSub t1 t2) = do+ a1 <- encode t1+ a2 <- encode t2+ mkSub [a1, a2]+ encode (TmMul t1 t2) = do+ a1 <- encode t1+ a2 <- encode t2+ mkMul [a1, a2]+ encode (TmDiv t1 t2) = do+ a1 <- encode t1+ a2 <- encode t2+ mkDiv a1 a2+ encode (TmEqual t1 t2) = do+ a1 <- encode t1+ a2 <- encode t2+ mkEq a1 a2+ encode (TmAnd t1 t2) = do+ a1 <- encode t1+ a2 <- encode t2+ mkAnd [a1, a2]+ encode (TmOr t1 t2) = do+ a1 <- encode t1+ a2 <- encode t2+ mkOr [a1, a2]+ encode (TmNot t) = encode t >>= mkNot+ encode (TmIf p c a) = do+ a1 <- encode p+ a2 <- encode c+ a3 <- encode a+ mkIte a1 a2 a3++instance Z3Sorted Term where+ sort (TmVar x) = do+ ctx <- getQualifierCtx+ case M.lookup x ctx of+ Just (_, s) -> return s+ Nothing -> smtError $ "Can't find variable " ++ x+ sort (TmNum _) = mkIntSort+ sort (TmLT _ _) = mkBoolSort+ sort (TmGT _ _) = mkBoolSort+ sort (TmLE _ _) = mkBoolSort+ sort (TmGE _ _) = mkBoolSort+ sort (TmAdd _ _) = mkIntSort+ sort (TmSub _ _) = mkIntSort+ sort (TmMul _ _) = mkIntSort+ sort (TmDiv _ _) = mkIntSort+ sort (TmEqual _ _) = mkBoolSort+ sort (TmAnd _ _) = mkBoolSort+ sort (TmOr _ _) = mkBoolSort+ sort (TmNot _) = mkBoolSort+ sort (TmIf _ c _) = sort c++instance Z3Sorted RType where+ sort RTInt = mkIntSort
+ src/TypeScope.hs view
@@ -0,0 +1,39 @@+module TypeScope where++import Ast+import Type+import Prelude hiding (lookup)+import qualified Data.Map as M++type TypeEnv = M.Map EName Type+type ParentScope = TypeScope++data TypeScope = TypeScope (Maybe ParentScope) TypeEnv++createEmptyScope :: TypeScope+createEmptyScope = TypeScope Nothing M.empty++createScopeWithParent :: ParentScope -> TypeScope+createScopeWithParent parent = TypeScope (Just parent) M.empty++createScope :: ParentScope -> TypeEnv -> TypeScope+createScope parent env = TypeScope (Just parent) env++insert :: EName -> Type -> TypeScope -> TypeScope+insert name t (TypeScope parent env) = TypeScope parent (M.insert name t env)++lookup :: EName -> TypeScope -> Maybe Type+lookup name (TypeScope parent env) = case M.lookup name env of+ Just t -> Just t+ Nothing -> case parent of+ Just p -> lookup name p+ Nothing -> Nothing++-- create a child type scope of current parent type scope+child :: ParentScope -> TypeScope+child = createScopeWithParent++instance Show TypeScope where+ show (TypeScope parent env) = (show . M.toList) env ++ case parent of+ Just p -> " -> " ++ show p+ Nothing -> " -| "
+ src/Value.hs view
@@ -0,0 +1,151 @@+module Value where++import Ast+import Data.List (intercalate)+import Prelude hiding (lookup)+import qualified Data.Map as M++type ValueEnv = M.Map EName Value+type ParentScope = ValueScope++data ValueScope = ValueScope (Maybe ParentScope) ValueEnv++createEmptyScope :: ValueScope+createEmptyScope = ValueScope Nothing M.empty++createScopeWithParent :: ParentScope -> ValueScope+createScopeWithParent parent = ValueScope (Just parent) M.empty++createScope :: ParentScope -> ValueEnv -> ValueScope+createScope parent env = ValueScope (Just parent) env++insert :: EName -> Value -> ValueScope -> ValueScope+insert name t (ValueScope parent env) = ValueScope parent (M.insert name t env)++lookup :: EName -> ValueScope -> Maybe Value+lookup name (ValueScope parent env) = case M.lookup name env of+ Just t -> Just t+ Nothing -> case parent of+ Just p -> lookup name p+ Nothing -> Nothing++-- create a child type scope of current parent type scope+-- just to mock immutable scope, will remove later+child :: ParentScope -> ValueScope+child = createScopeWithParent++instance Show ValueScope where+ show (ValueScope parent env) = (show . M.toList) env ++ case parent of+ Just p -> " -> " ++ show p+ Nothing -> " -| "++type Tag = String+type FreeVal = Value++data Value = VNum Int+ | VChar Char+ | VBool Bool+ | VTuple [Value]+ | VRecord (M.Map EField Value)+ | VUnit+ | Adt Tag [Value]+ | Fn (Value -> ValueScope -> Value) -- or closure+ | FnApArgs (M.Map String Value)+ | DestrFnApArgs [PatVal] FreeVal+ | TConArgs [Value] Tag++data PatVal = PatVal Pattern Value+ deriving (Eq, Show, Ord)++nil :: Value+nil = Adt "Nil" []++cons :: Value -> Value -> Value+cons h t = Adt "Cons" [h, t]++makeList :: [Value] -> Value+makeList res = case res of+ [] -> nil+ x:xs -> cons x $ makeList xs++getElements :: Value -> [Value]+getElements l = case l of+ Adt "Cons" [h, t] -> h : (getElements t)+ _ -> []++reverseList :: Value -> Value+reverseList l = makeList . reverse . getElements $ l++strV :: String -> Value+strV s = makeList $ map (VChar) s++desugerStrV :: Value -> String+desugerStrV (Adt _ values) = case values of+ [] -> ""+ _ -> intercalate "" (map desugerStrV values)+desugerStrV v = show v++-- binary operator+binFn :: (Value -> Value -> Value) -> Value+binFn f = Fn (\arg1 _ -> Fn (\arg2 _ -> f arg1 arg2))++isString :: Value -> Bool+isString v = case v of+ Adt "Cons" [h, _] -> case h of+ VChar _ -> True+ _ -> False+ _ -> False++stringOfAdt :: Tag -> [Value] -> String+stringOfAdt tag values = case tag of+ "Cons" -> case (head values) of+ VChar _ -> "\"" ++ intercalate "" (map show (getElements (Adt tag values))) ++ "\""+ _ -> "[" ++ intercalate ", " (map (\v -> case v of+ Adt "Nil" [] -> "[]"+ _ -> show v) (getElements (Adt tag values))) ++ "]"+ "Nil" -> "[]"+ _ -> tag ++ case values of+ []-> ""+ _ -> " " ++ intercalate " | " (map show values)++stringOfPairs :: M.Map String Value -> String+stringOfPairs pairs = "{" ++ intercalate "," (M.elems $ M.mapWithKey (\f v -> f ++ " : " ++ show v) pairs) ++ "}"++instance Show Value where+ show (VNum i) = show i+ show (VChar c) = [c]+ show (VBool b) = show b+ show (VTuple values) = "(" ++ intercalate "," (map show values) ++ ")"+ show (VRecord pairs) = stringOfPairs pairs+ show VUnit = "⊥"+ show (Adt tag values) = stringOfAdt tag values+ show (Fn _) = "<fun>"+ show (FnApArgs pairs) = "FnApArgs(" ++ stringOfPairs pairs ++ ")"+ show (DestrFnApArgs pats val) = "DestrFnApArgs(" ++ intercalate ", " (map show pats) ++ " * " ++ show val ++ ")"+ show (TConArgs values tag) = "TConArgs(" ++ stringOfAdt tag values ++ ")"++instance Eq Value where+ VNum int1 == VNum int2 = int1 == int2+ VChar char1 == VChar char2 = char1 == char2+ VBool bool1 == VBool bool2 = bool1 == bool2+ VTuple values1 == VTuple values2 = values1 == values2+ VRecord pairs1 == VRecord pairs2 = pairs1 == pairs2+ VUnit == VUnit = True+ Adt tag1 values1 == Adt tag2 values2 = tag1 == tag2 && values1 == values2+ FnApArgs pairs1 == FnApArgs pairs2 = pairs1 == pairs2+ DestrFnApArgs vals1 val1 == DestrFnApArgs vals2 val2 = vals1 == vals2 && val1 == val2+ TConArgs vals1 tag1 == TConArgs vals2 tag2 = vals1 == vals2 && tag1 == tag2+ _ == _ = False++instance Ord Value where+ VNum int1 <= VNum int2 = int1 <= int2+ VChar char1 <= VChar char2 = char1 <= char2+ VBool bool1 <= VBool bool2 = bool1 <= bool2+ VTuple values1 <= VTuple values2 = values1 <= values2+ VRecord pairs1 <= VRecord pairs2 = pairs1 <= pairs2+ VUnit <= VUnit = True+ Adt tag1 values1 <= Adt tag2 values2 = tag1 <= tag2 && values1 <= values2+ FnApArgs pairs1 <= FnApArgs pairs2 = pairs1 <= pairs2+ DestrFnApArgs vals1 val1 <= DestrFnApArgs vals2 val2 = vals1 <= vals2 && val1 <= val2+ TConArgs vals1 tag1 <= TConArgs vals2 tag2 = vals1 <= vals2 && tag1 <= tag2+ _ <= _ = False
+ test/EvalSpec.hs view
@@ -0,0 +1,264 @@+module EvalSpec where++import Ast+import Type+import Value+import Eval+import Prologue+import qualified Data.Map as M+import qualified Text.PrettyPrint as PP+import Test.Hspec++runEvalSpecCases :: [(Expr, Maybe Value)] -> IO ()+runEvalSpecCases exprExpects = do+ 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++spec :: Spec+spec = describe "evaluation test" $ do+ it "should get value of ADT and pattern match expressions part1" $ do+ tvarA <- makeVariable+ let name = "List"+ let vars = [tvarA]+ let dataType = TOper name vars+ let consConstructor = TypeConstructor "Cons" [tvarA, TOper "List" [tvarA]]+ let nilConstructor = TypeConstructor "Nil" []+ let listData = EDataDecl "List" dataType vars [consConstructor, nilConstructor]+ (PP.text . show $ listData) `shouldBe` PP.text "data List α = Cons α [α] | Nil"+ let xs = EDestructLetBinding (IdPattern "xs") [] [(EVar "Nil")]+ let ys = EDestructLetBinding (IdPattern "ys") [] [EApp (EApp (EVar "Cons") $ ENum 5) $ EVar "Nil"]+ let len = EDestructLetBinding (IdPattern "len") [IdPattern "l"] [EPatternMatching (EVar "l") [Case (TConPattern "Nil" []) [ENum 0], Case (TConPattern "Cons" [IdPattern "h", IdPattern "t"]) [EApp (EApp (EVar "+") $ ENum 1) $ EApp (EVar "len") $ EVar "t"]]]+ let xy = EDestructLetBinding (IdPattern "xy") [] [ETuple [EApp (EVar "len") (EVar "xs"), EApp (EVar "len") (EVar"ys")]]+ let zs = EDestructLetBinding (IdPattern "zs") [] [EApp (EApp (EVar "Cons") $ ENum 5) $ EApp (EApp (EVar "Cons") $ ENum 4) $ EApp (EApp (EVar "Cons") $ ENum 3) $ EVar "Nil"]+ let z = EDestructLetBinding (IdPattern "z") [] [EApp (EVar "len") $ EVar "zs"]+ runEvalSpecCases [(listData, Just VUnit),+ (xs, Just $ Adt "Nil" []),+ (ys, Just $ Adt "Cons" [VNum 5, Adt "Nil" []]),+ (len, Nothing),+ (xy, Just $ VTuple [VNum 0, VNum 1]),+ (zs, Just $ Adt "Cons" [VNum 5, Adt "Cons" [VNum 4, Adt "Cons" [VNum 3, Adt "Nil" []]]]),+ (z, Just $ VNum 3)]+ it "should get value of ADT and pattern match expressions part2" $ do+ tvarB <- makeVariable+ let name2 = "Tree"+ let vars2 = [tvarB]+ let dataType2 = TOper name2 vars2+ let nullConstructor = TypeConstructor "Null" []+ let leafConstructor = TypeConstructor "Leaf" [tvarB]+ let nodeConstructor = TypeConstructor "Node" [dataType2, tvarB, dataType2]+ let treeData = EDataDecl name2 dataType2 vars2 [nullConstructor, leafConstructor, nodeConstructor]+ let t = EDestructLetBinding (IdPattern "t") [] [EApp (EApp (EApp (EVar "Node") $ EApp (EVar "Leaf") $ ENum 5) $ ENum 4) $ EApp (EVar "Leaf") $ ENum 3]+ runEvalSpecCases [(treeData, Just VUnit),+ (t, Just $ Adt "Node" [Adt "Leaf" [VNum 5], VNum 4, Adt "Leaf" [VNum 3]])]+ it "should get value of ADT and pattern match expressions part3" $ do+ let name3 = "Ast"+ let dataType3 = TOper name3 []+ let numConstructor = TypeConstructor "Num" [intT]+ let addConstructor = TypeConstructor "Add" [dataType3, dataType3]+ let subConstructor = TypeConstructor "Sub" [dataType3, dataType3]+ let mulConstructor = TypeConstructor "Mul" [dataType3, dataType3]+ let divConstructor = TypeConstructor "Div" [dataType3, dataType3]+ let astData = EDataDecl name3 dataType3 [] [numConstructor, addConstructor, subConstructor, mulConstructor, divConstructor]+ let evalfn = EDestructLetBinding (IdPattern "eval") [IdPattern "n"] [EPatternMatching (EVar "n") [Case (TConPattern "Num" [IdPattern "a"]) [EVar "a"],Case (TConPattern "Add" [IdPattern "a", IdPattern "b"]) [EApp (EApp (EVar "+") $ EApp (EVar "eval") $ EVar "a") $ EApp (EVar "eval") $ EVar "b"],Case (TConPattern "Sub" [IdPattern "a", IdPattern "b"]) [EApp (EApp (EVar "-") $ EApp (EVar "eval") $ EVar "a") $ EApp (EVar "eval") $ EVar "b"],Case (TConPattern "Mul" [IdPattern "a", IdPattern "b"]) [EApp (EApp (EVar "*") $ EApp (EVar "eval") $ EVar "a") $ EApp (EVar "eval") $ EVar "b"],Case (TConPattern "Div" [IdPattern "a", IdPattern "b"]) [EApp (EApp (EVar "/") $ EApp (EVar "eval") $ EVar "a") $ EApp (EVar "eval") $ EVar "b"]]]+ let sym = EDestructLetBinding (IdPattern "sym") [] [EApp (EApp (EVar "Mul") (EApp (EApp (EVar "Add") $ EApp (EVar "Num") $ ENum 4) $ EApp (EVar "Num") $ ENum 3)) (EApp (EApp (EVar "Sub") $ EApp (EVar "Num") $ ENum 4) $ EApp (EVar "Num") $ ENum 1)]+ let result = EDestructLetBinding (IdPattern "result") [] [EApp (EVar "eval") $ EVar "sym"]+ runEvalSpecCases [(astData, Just VUnit),+ (evalfn, Nothing),+ (sym, Just $ Adt "Mul" [Adt "Add" [Adt "Num" [VNum 4], Adt "Num" [VNum 3]], Adt "Sub" [Adt "Num" [VNum 4], Adt "Num" [VNum 1]]]),+ (result, Just $ VNum 21)]+ it "should get value of ADT and pattern match expressions part4" $ do+ let name4 = "Oper"+ let dataType4 = TOper name4 []+ let addOperConstructor = TypeConstructor "Add" []+ let subOperConstructor = TypeConstructor "Sub" []+ let operData = EDataDecl name4 dataType4 [] [addOperConstructor, subOperConstructor]+ let name5 = "Expr"+ let dataType5 = TOper name5 []+ let numExprConstructor = TypeConstructor "Num" [intT]+ let appExprConstructor = TypeConstructor "App" [dataType4, dataType5, dataType5]+ let exprData = EDataDecl name5 dataType5 [] [numExprConstructor, appExprConstructor]+ let a = EDestructLetBinding (IdPattern "a") [] [EApp (EApp (EApp (EVar "App") $ EVar "Add") $ EApp (EVar "Num") $ ENum 5) $ EApp (EVar "Num") $ ENum 6]+ let eval1 = EDestructLetBinding (IdPattern "eval1") [IdPattern "e"] [EPatternMatching (EVar "e") [Case (TConPattern "Num" [IdPattern "n"]) [EVar "n"],Case (TConPattern "App" [IdPattern "o", IdPattern "e1", IdPattern "e2"]) [EPatternMatching (EVar "o") [Case (TConPattern "Add" []) [EApp (EApp (EVar "+") $ EApp (EVar "eval1") $ EVar "e1") $ EApp (EVar "eval1") $ EVar "e2"],Case (TConPattern "Sub" []) [EApp (EApp (EVar "-") $ EApp (EVar "eval1") $ EVar "e1") $ EApp (EVar "eval1") $ EVar "e2"]]]]]+ let eval2 = EDestructLetBinding (IdPattern "eval2") [IdPattern "e"] [EPatternMatching (EVar "e") [Case (TConPattern "Num" [IdPattern "n"]) [EVar "n"],Case (TConPattern "App" [TConPattern "Add" [], IdPattern "e1", IdPattern "e2"]) [EApp (EApp (EVar "+") $ EApp (EVar "eval2") $ EVar "e1") $ EApp (EVar "eval2") $ EVar "e2"],Case (TConPattern "App" [TConPattern "Sub" [], IdPattern "e1", IdPattern "e2"]) [EApp (EApp (EVar "-") $ EApp (EVar "eval2") $ EVar "e1") $ EApp (EVar "eval2") $ EVar "e2"]]]+ let result1 = EDestructLetBinding (IdPattern "result1") [] [EApp (EVar "eval1") $ EVar "a"]+ let result2 = EDestructLetBinding (IdPattern "result2") [] [EApp (EVar "eval2") $ EVar "a"]+ let simplify = EDestructLetBinding (IdPattern "simplify") [IdPattern "e"] [EPatternMatching (EVar "e") [Case (TConPattern "App" [TConPattern "Add" [], TConPattern "Num" [IdPattern "n"], IdPattern "e2"]) [EIf (EApp (EApp (EVar "=") $ EVar "n") $ ENum 0) [EVar "e2"] [EVar "e"]]]]+ let b = EDestructLetBinding (IdPattern "b") [] [EApp (EApp (EApp (EVar "App") $ EVar "Add") $ EApp (EVar "Num") $ ENum 0) $ EApp (EVar "Num") $ ENum 6]+ let c = EDestructLetBinding (IdPattern "c") [] [EApp (EVar "simplify") $ EVar "b"]+ runEvalSpecCases [(operData, Just VUnit),+ (exprData, Just VUnit),+ (a, Just $ Adt "App" [Adt "Add" [], Adt "Num" [VNum 5], Adt "Num" [VNum 6]]),+ (eval1, Nothing),+ (eval2, Nothing),+ (result1, Just $ VNum 11),+ (result2, Just $ VNum 11),+ (simplify, Nothing),+ (b, Just $ Adt "App" [Adt "Add"[], Adt "Num" [VNum 0], Adt "Num" [VNum 6]]),+ (c, Just $ Adt "Num" [VNum 6])]+ it "should get value of lambda expressions even with type annotations" $ do+ let g = EDestructLetBinding (IdPattern "g") [] [ELambda [Named "x" Nothing, Named "y" Nothing] Nothing [EApp (EApp (EVar "+") $ EVar "x") $ EVar "y"]]+ 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 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)])]+ let idpair2 = ELetBinding (IdPattern "id") (ELambda [Named "x" Nothing] Nothing [EVar "x"]) [ELetBinding (IdPattern "a") (ENum 3) [ELetBinding (IdPattern "b") (EApp (EApp (EVar "+") $ EVar "a") $ ENum 3) [(ETuple [EApp (EVar "id") (EVar "a"), EApp (EVar "id") (EVar "b")])]]]+ let f1 = EDestructLetBinding (IdPattern "f1") [] [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 f2 = EDestructLetBinding (IdPattern "f2") [] [ELambda [Named "x" Nothing, Named "y" Nothing, Named "z" Nothing] Nothing [EApp (EApp (EVar "+") (EApp (EApp (EVar "+") $ EVar "x") $ EVar "y")) $ EVar "z"]]+ let f1res = EDestructLetBinding (IdPattern "f1res") [] [EApp (EApp (EApp (EVar "f1") $ ENum 8) $ ENum 2) $ ENum 3]+ let f2res = EDestructLetBinding (IdPattern "f2res") [] [EApp (EApp (EApp (EVar "f2") $ ENum 8) $ ENum 2) $ ENum 3]+ runEvalSpecCases [(g, Nothing),+ (res0, Just $ VNum 6),+ (f, Nothing),+ (res1, Just $ VNum 13),+ (id, Nothing),+ (res2, Just $ VNum 3),+ (res3, Just $ VBool True),+ (idpair, Just $ VTuple [VNum 3, VBool True]),+ (idpair2, Just $ VTuple [VNum 3, VNum 6]),+ (f1, Nothing),+ (f2, Nothing),+ (f1res, Just $ VNum 13),+ (f2res, Just $ VNum 13)]+ it "should get value of function definition, application and pattern match" $ do+ let fib = EDestructLetBinding (IdPattern "fib") [IdPattern "x"] [EPatternMatching (EVar "x") [Case (NumPattern 0) [ENum 0], Case (NumPattern 1) [ENum 1], Case WildcardPattern [EApp (EApp (EVar "+") (EApp (EVar "fib") $ EApp (EApp (EVar "-") $ EVar "x") $ ENum 1)) $ EApp (EVar "fib") $ EApp (EApp (EVar "-") $ EVar "x") $ ENum 2]]]+ let fib0 = EApp (EVar "fib") $ ENum 0+ let fib1 = EApp (EVar "fib") $ ENum 1+ let fib5 = EApp (EVar "fib") $ ENum 5+ let fib6 = EApp (EVar "fib") $ ENum 6+ let penultimate = EProgram [EDestructLetBinding (IdPattern "penultimate") [IdPattern "xs"] [EPatternMatching (EVar "xs") [Case (TConPattern "Nil" []) [ENum 0],+ Case (TConPattern "Cons" [WildcardPattern, TConPattern "Nil" []]) [ENum 0],+ Case (TConPattern "Cons" [IdPattern "a", TConPattern "Cons" [WildcardPattern, TConPattern "Nil" []]]) [EVar "a"],+ 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 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"]+ let l6 = EDestructLetBinding (IdPattern "l6") [] [EApp (EApp (EVar "map2") $ ELambda [Named "x" Nothing] Nothing [EApp (EApp (EVar "=") $ EApp (EApp (EVar "%") $ EVar "x") $ ENum 2) $ ENum 0]) $ EVar "l"]+ let k = EDestructLetBinding (IdPattern "k") [IdPattern "x", IdPattern "y"] [EPatternMatching (ETuple [EVar "x", EVar "y"]) [Case (TuplePattern [NumPattern 0, NumPattern 0]) [ENum 0], Case WildcardPattern [ENum 1]]]+ let fact = EDestructLetBinding (IdPattern "fact") [IdPattern "n"] [EIf (EApp (EApp (EVar "≤") $ EVar "n") $ ENum 1) [ENum 1] [EApp (EApp (EVar "*") $ EVar "n") (EApp (EVar "fact") $ EApp (EApp (EVar "-") $ EVar "n") $ ENum 1)]]+ let f5 = EDestructLetBinding (IdPattern "f5") [] [EApp (EVar "fact") $ ENum 5]+ let comp = EDestructLetBinding (IdPattern "comp") [IdPattern "f", IdPattern "g", IdPattern "x"] [EApp (EVar "f") (EApp (EVar "g") (EVar "x"))]+ let fix = EDestructLetBinding (IdPattern "fix") [] [EApp (EApp (EVar "comp") $ EVar "inc") (EVar "dec")]+ let incdec = EDestructLetBinding (IdPattern "incdec") [] [EApp (EVar "fix") (ENum 5)]+ let len = EDestructLetBinding (IdPattern "len") [IdPattern "xs"] [EPatternMatching (EVar "xs") [Case (TConPattern "Nil" []) [ENum 0],Case (TConPattern "Cons" [WildcardPattern, IdPattern "t"]) [EApp (EApp (EVar "+") $ ENum 1) (EApp (EVar "len") $ EVar "t")]]]+ let lenl = EApp (EVar "len") $ EVar "l"+ let append = EDestructLetBinding (IdPattern "append") [IdPattern "x", IdPattern "xs"] [EApp (EApp (EVar "Cons") $ EVar "x") $ EVar "xs"]+ let l2 = EDestructLetBinding (IdPattern "l2") [] [EApp (EApp (EVar "append") $ ENum 0) $ EVar "l"]+ let patmat0 = EDestructLetBinding (IdPattern "patmat0") [] [EPatternMatching (ETuple [EStr "a", ENum 3]) [Case (IdPattern "a") [ETuple [EStr "ok", EVar "a"]]]]+ let patmat1 = EDestructLetBinding (IdPattern "patmat1") [] [EPatternMatching (ETuple [EStr "a", ENum 3]) [Case (TuplePattern [IdPattern "a", IdPattern "b"]) [ETuple [EStr "ok", EVar "a", EVar "b"]]]]+ let patmat2 = EDestructLetBinding (IdPattern "patmat2") [] [EPatternMatching (ETuple [EStr "a", ENum 3]) [Case (TuplePattern [IdPattern "a", WildcardPattern]) [ETuple [EStr "ok", EVar "a"]]]]+ let patmat3 = EDestructLetBinding (IdPattern "patmat3") [] [EPatternMatching (EChar 'a') [Case (CharPattern 'a') [EBool True], Case WildcardPattern [EBool False]]]+ let patmat4 = EDestructLetBinding (IdPattern "patmat4") [] [EPatternMatching (EBool True) [Case (BoolPattern True) [EBool True], Case WildcardPattern [EBool False]]]+ let patmat5 = EDestructLetBinding (IdPattern "patmat5") [] [EPatternMatching (ENum 1) [Case (NumPattern 1) [EBool True], Case WildcardPattern [EBool False]]]+ let patmat6 = EDestructLetBinding (IdPattern "patmat6") [] [EPatternMatching (EStr "abc") [Case (TConPattern "Cons" [CharPattern 'a', (TConPattern "Cons" [CharPattern 'b', (TConPattern "Cons" [CharPattern 'c', TConPattern "Nil" []])])]) [EBool True], Case WildcardPattern [EBool False]]]+ let patmat7 = EDestructLetBinding (IdPattern "patmat7") [] [EPatternMatching (EStr "acb") [Case (TConPattern "Cons" [CharPattern 'a', (TConPattern "Cons" [CharPattern 'b', (TConPattern "Cons" [CharPattern 'c', TConPattern "Nil" []])])]) [EBool True], Case WildcardPattern [EBool False]]]+ runEvalSpecCases [(fib, Nothing),+ (fib0, Just $ VNum 0),+ (fib1, Just $ VNum 1),+ (fib5, Just $ VNum 5),+ (fib6, Just $ VNum 8),+ (penultimate, Nothing),+ (res7, Just $ VNum 0),+ (res8, Just $ VNum 3),+ (map, 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))),+ (l6, Just $ cons (VBool False) (cons (VBool True) (cons (VBool False) nil))),+ (k, Nothing),+ (fact, Nothing),+ (f5, Just $ VNum 120),+ (comp, Nothing),+ (fix, Nothing),+ (incdec, Just $ VNum 5),+ (len, Nothing),+ (lenl, Just $ VNum 3),+ (append, Nothing),+ (l2, Just $ cons (VNum 0) (cons (VNum 1) (cons (VNum 2) (cons (VNum 3) nil)))),+ (patmat0, Just $ VTuple [cons (VChar 'o') (cons (VChar 'k') nil), VTuple [cons (VChar 'a') nil, VNum 3]]),+ (patmat1, Just $ VTuple [cons (VChar 'o') (cons (VChar 'k') nil), cons (VChar 'a') nil, VNum 3]),+ (patmat2, Just $ VTuple [cons (VChar 'o') (cons (VChar 'k') nil), cons (VChar 'a') nil]),+ (patmat3, Just $ VBool True),+ (patmat4, Just $ VBool True),+ (patmat5, Just $ VBool True),+ (patmat6, Just $ VBool True),+ (patmat7, Just $ VBool False)]+ it "should get value of basic syntax element" $ do+ let xb = EDestructLetBinding (IdPattern "x") [] [EBool True]+ let d = EDestructLetBinding (IdPattern "d") [] [ETuple [ETuple [ENum 4, EBool True], ETuple [EStr "test", EChar 'c', ENum 45]]]+ let intsum = EApp (EApp (EVar "+") (EApp (EApp (EVar "+") (EApp (EApp (EVar "+") (EApp (EApp (EVar "+") $ ENum 1) $ ENum 2)) $ ENum 3)) $ ENum 4)) $ ENum 5+ let l = EDestructLetBinding (IdPattern "y") [] [EList [ENum 1, ENum 2, ENum 3]]+ let l2 = EDestructLetBinding (IdPattern "z") [] [EList []]+ let a = EDestructLetBinding (IdPattern "a") [] [EChar 'a']+ let s = EDestructLetBinding (IdPattern "s") [] [EStr "str"]+ let l3 = EDestructLetBinding (IdPattern "l") [] [EApp (EApp (EVar "Cons") $ ENum 1) $ EApp (EApp (EVar "Cons") $ ENum 2) $ EApp (EApp (EVar "Cons") $ ENum 3) $ EVar "Nil"]+ let profile = EDestructLetBinding (IdPattern "profile") [] [ERecord (M.fromList [("name", EStr "ntha"), ("age", ENum 12)])]+ let name = EAccessor (EVar "profile") "name"+ let equal = (EApp (EApp (EVar "=") $ ENum 3) $ ENum 3)+ let notequal = (EApp (EApp (EVar "≠") $ EBool True) $ EBool False)+ runEvalSpecCases [(xb, Just $ VBool True),+ (d, Just $ VTuple [VTuple [VNum 4, VBool True], VTuple [cons (VChar 't') (cons (VChar 'e') (cons (VChar 's') (cons (VChar 't') nil))), VChar 'c', VNum 45]]),+ (intsum, Just $ VNum 15),+ (l, Just $ cons (VNum 1) (cons (VNum 2) (cons (VNum 3) nil))),+ (l2, Just $ nil),+ (a, Just $ VChar 'a'),+ (s, Just $ cons (VChar 's') (cons (VChar 't') (cons (VChar 'r') nil))),+ (l3, Just $ cons (VNum 1) (cons (VNum 2) (cons (VNum 3) nil))),+ (profile, Just $ VRecord (M.fromList [("name", cons (VChar 'n') (cons (VChar 't') (cons (VChar 'h') (cons (VChar 'a') nil)))), ("age", VNum 12)])),+ (name, Just $ cons (VChar 'n') (cons (VChar 't') (cons (VChar 'h') (cons (VChar 'a') nil)))),+ (equal, Just $ VBool True),+ (notequal, Just $ VBool True)]+ it "should get value of destructuring" $ do+ let abpair = EDestructLetBinding (TuplePattern [IdPattern "a", IdPattern "b"]) [] [ETuple [ENum 3, EStr "d"]]+ let d = EDestructLetBinding (IdPattern "d") [] [ETuple [ETuple [ENum 3, EBool True], ETuple [EStr "test", EChar 'c', EVar "a"]]]+ let bool = EDestructLetBinding (TuplePattern [TuplePattern [WildcardPattern, IdPattern "bool"], TuplePattern [WildcardPattern, WildcardPattern, WildcardPattern]]) [] [EVar "d"]+ let boolv = EVar "bool"+ let abctuple = ELetBinding (TuplePattern [IdPattern "a", IdPattern "b", IdPattern "c"]) (ETuple [ENum 1, ENum 2, ENum 3]) [(EApp (EApp (EVar "+") (EApp (EApp (EVar "+") $ EVar "a") $ EVar "b")) $ EVar "c")]+ let abclist = EDestructLetBinding (TConPattern "Cons" [IdPattern "a", TConPattern "Cons" [IdPattern "b", TConPattern "Cons" [IdPattern "c", TConPattern "Nil" []]]]) [] [EList [ENum 1, ENum 2, ENum 3]]+ let a = EVar "a"+ let b = EVar "b"+ let c = EVar "c"+ let abclist2 = ELetBinding (TConPattern "Cons" [IdPattern "a", TConPattern "Cons" [IdPattern "b", TConPattern "Cons" [IdPattern "c", TConPattern "Nil" []]]]) (EList [ENum 1, ENum 2, ENum 3]) [(EApp (EApp (EVar "+") (EApp (EApp (EVar "+") $ EVar "a") $ EVar "b")) $ EVar "c")]+ let abctuplefn = EDestructLetBinding (IdPattern "f1") [(TuplePattern [IdPattern "a", IdPattern "b", IdPattern "c"])] [(EApp (EApp (EVar "+") (EApp (EApp (EVar "+") $ EVar "a") $ EVar "b")) $ EVar "c")]+ let abclistfn = EDestructLetBinding (IdPattern "f2") [(TConPattern "Cons" [IdPattern "a", TConPattern "Cons" [IdPattern "b", TConPattern "Cons" [IdPattern "c", TConPattern "Nil" []]]])] [(EApp (EApp (EVar "+") (EApp (EApp (EVar "+") $ EVar "a") $ EVar "b")) $ EVar "c")]+ let res1 = EApp (EVar "f1") $ ETuple [EVar "a", EVar "b", EVar "c"]+ let res2 = EApp (EVar "f2") $ EList [EVar "a", EVar "b", EVar "c"]+ tvarA <- makeVariable+ let name = "Maybe"+ let vars = [tvarA]+ let dataType = TOper name vars+ let justConstructor = TypeConstructor "Just" [tvarA]+ let nothingConstructor = TypeConstructor "Nothing" []+ let maybeData = EDataDecl name dataType vars [justConstructor, nothingConstructor]+ let f = EDestructLetBinding (IdPattern "f3") [(TConPattern "Just" [IdPattern "a"])] [(EApp (EApp (EVar "+") $ EVar "a") $ ENum 1)]+ let res3 = EApp (EVar "f3") $ EApp (EVar "Just") $ ENum 2+ let just = EDestructLetBinding (TConPattern "Just" [IdPattern "k"]) [] [EApp (EVar "Just") $ ENum 3]+ let k = EVar "k"+ runEvalSpecCases [(abpair, Just $ VTuple [VNum 3, makeList [VChar 'd']]),+ (d, Just $ VTuple [VTuple [VNum 3, VBool True], VTuple [makeList [VChar 't', VChar 'e', VChar 's', VChar 't'], VChar 'c', VNum 3]]),+ (bool, Just $ VTuple [VTuple [VNum 3, VBool True], VTuple [makeList [VChar 't', VChar 'e', VChar 's', VChar 't'], VChar 'c', VNum 3]]),+ (boolv, Just $ VBool True),+ (abctuple, Just $ VNum 6),+ (abclist, Just $ makeList [VNum 1, VNum 2, VNum 3]),+ (a, Just $ VNum 1),+ (b, Just $ VNum 2),+ (c, Just $ VNum 3),+ (abclist2, Just $ VNum 6),+ (abctuplefn, Nothing),+ (abclistfn, Nothing),+ (res1, Just $ VNum 6),+ (res2, Just $ VNum 6),+ (maybeData, Just VUnit),+ (f, Nothing),+ (res3, Just $ VNum 3),+ (just, Just $ Adt "Just" [VNum 3]),+ (k, Just $ VNum 3)]
+ test/InferSpec.hs view
@@ -0,0 +1,268 @@+module InferSpec where++import Ast+import Type+import Infer+import State (resetId, resetUniqueName)+import Control.Monad (foldM)+import Prologue+import qualified Data.Map as M+import qualified Text.PrettyPrint as PP+import qualified Data.Set as S+import Test.Hspec++runInferSpecCases :: [(Expr, String)] -> IO ()+runInferSpecCases exprExpectPairs = do+ assumps <- assumptions+ (_, types, expects) <- foldM (\(env, types, expects) (expr, expect) -> do+ (env', ty) <- analyze expr env S.empty+ return (env', types ++ [ty], expects ++ [expect]))+ (assumps, [], []) exprExpectPairs+ resetId+ resetUniqueName+ (map (PP.text . show) types) `shouldBe` map PP.text expects++failInferSpecCase :: Expr -> String -> IO ()+failInferSpecCase expr errorMsg = do+ assumps <- assumptions+ analyze expr assumps S.empty `shouldThrow` errorCall errorMsg+ resetId+ resetUniqueName++spec :: Spec+spec = describe "inference test" $ do+ it "should infer type of ADT and pattern match expressions part1" $ do+ resetId+ resetUniqueName+ tvarA <- makeVariable+ let name = "List"+ let vars = [tvarA]+ let dataType = TOper name vars+ let consConstructor = TypeConstructor "Cons" [tvarA, TOper "List" [tvarA]]+ let nilConstructor = TypeConstructor "Nil" []+ let listData = EDataDecl "List" dataType vars [consConstructor, nilConstructor]+ (PP.text . show $ listData) `shouldBe` PP.text "data List α = Cons α [α] | Nil"+ let xs = EDestructLetBinding (IdPattern "xs") [] [(EVar "Nil")]+ let ys = EDestructLetBinding (IdPattern "ys") [] [EApp (EApp (EVar "Cons") $ ENum 5) $ EVar "Nil"]+ let len = EDestructLetBinding (IdPattern "len") [IdPattern "l"] [EPatternMatching (EVar "l") [Case (TConPattern "Nil" []) [ENum 0], Case (TConPattern "Cons" [IdPattern "h", IdPattern "t"]) [EApp (EApp (EVar "+") $ ENum 1) $ EApp (EVar "len") $ EVar "t"]]]+ let xy = EDestructLetBinding (IdPattern "xy") [] [ETuple [EApp (EVar "len") (EVar "xs"), EApp (EVar "len") (EVar"ys")]]+ let zs = EDestructLetBinding (IdPattern "zs") [] [EApp (EApp (EVar "Cons") $ ENum 5) $ EApp (EApp (EVar "Cons") $ ENum 4) $ EApp (EApp (EVar "Cons") $ ENum 3) $ EVar "Nil"]+ let z = EDestructLetBinding (IdPattern "z") [] [EApp (EVar "len") $ EVar "zs"]+ runInferSpecCases [(listData, "[α]"),+ (xs, "[α]"),+ (ys, "[Number]"),+ (len, "[α] → Number"),+ (xy, "(Number * Number)"),+ (zs, "[Number]"),+ (z, "Number")]+ it "should infer type of ADT and pattern match expressions part2" $ do+ tvarB <- makeVariable+ let name2 = "Tree"+ let vars2 = [tvarB]+ let dataType2 = TOper name2 vars2+ let nullConstructor = TypeConstructor "Null" []+ let leafConstructor = TypeConstructor "Leaf" [tvarB]+ let nodeConstructor = TypeConstructor "Node" [dataType2, tvarB, dataType2]+ let treeData = EDataDecl name2 dataType2 vars2 [nullConstructor, leafConstructor, nodeConstructor]+ let t = EApp (EApp (EApp (EVar "Node") $ EApp (EVar "Leaf") $ ENum 5) $ ENum 4) $ EApp (EVar "Leaf") $ ENum 3+ runInferSpecCases [(treeData, "(Tree α)"),+ (t, "(Tree Number)")]+ it "should infer type of ADT and pattern match expressions part3" $ do+ let name3 = "Ast"+ let dataType3 = TOper name3 []+ let numConstructor = TypeConstructor "Num" [intT]+ let addConstructor = TypeConstructor "Add" [dataType3, dataType3]+ let subConstructor = TypeConstructor "Sub" [dataType3, dataType3]+ let mulConstructor = TypeConstructor "Mul" [dataType3, dataType3]+ let divConstructor = TypeConstructor "Div" [dataType3, dataType3]+ let astData = EDataDecl name3 dataType3 [] [numConstructor, addConstructor, subConstructor, mulConstructor, divConstructor]+ let eval = EDestructLetBinding (IdPattern "eval") [IdPattern "n"] [EPatternMatching (EVar "n") [Case (TConPattern "Num" [IdPattern "a"]) [EVar "a"],Case (TConPattern "Add" [IdPattern "a", IdPattern "b"]) [EApp (EApp (EVar "+") $ EApp (EVar "eval") $ EVar "a") $ EApp (EVar "eval") $ EVar "b"],Case (TConPattern "Sub" [IdPattern "a", IdPattern "b"]) [EApp (EApp (EVar "-") $ EApp (EVar "eval") $ EVar "a") $ EApp (EVar "eval") $ EVar "b"],Case (TConPattern "Mul" [IdPattern "a", IdPattern "b"]) [EApp (EApp (EVar "*") $ EApp (EVar "eval") $ EVar "a") $ EApp (EVar "eval") $ EVar "b"],Case (TConPattern "Div" [IdPattern "a", IdPattern "b"]) [EApp (EApp (EVar "/") $ EApp (EVar "eval") $ EVar "a") $ EApp (EVar "eval") $ EVar "b"]]]+ let sym = EDestructLetBinding (IdPattern "sym") [] [EApp (EApp (EVar "Mul") (EApp (EApp (EVar "Add") $ EApp (EVar "Num") $ ENum 4) $ EApp (EVar "Num") $ ENum 3)) (EApp (EApp (EVar "Sub") $ EApp (EVar "Num") $ ENum 4) $ EApp (EVar "Num") $ ENum 1)]+ let result = EDestructLetBinding (IdPattern "result") [] [EApp (EVar "eval") $ EVar "sym"]+ runInferSpecCases [(astData, "Ast"),+ (eval, "Ast → Number"),+ (sym, "Ast"),+ (result, "Number")]+ it "should infer type of ADT and pattern match expressions part4" $ do+ let name4 = "Oper"+ let dataType4 = TOper name4 []+ let addOperConstructor = TypeConstructor "Add" []+ let subOperConstructor = TypeConstructor "Sub" []+ let operData = EDataDecl name4 dataType4 [] [addOperConstructor, subOperConstructor]+ let name5 = "Expr"+ let dataType5 = TOper name5 []+ let numExprConstructor = TypeConstructor "Num" [intT]+ let appExprConstructor = TypeConstructor "App" [dataType4, dataType5, dataType5]+ let exprData = EDataDecl name5 dataType5 [] [numExprConstructor, appExprConstructor]+ let a = EDestructLetBinding (IdPattern "a") [] [EApp (EApp (EApp (EVar "App") $ EVar "Add") $ EApp (EVar "Num") $ ENum 5) $ EApp (EVar "Num") $ ENum 6]+ let eval1 = EDestructLetBinding (IdPattern "eval1") [IdPattern "e"] [EPatternMatching (EVar "e") [Case (TConPattern "Num" [IdPattern "n"]) [EVar "n"],Case (TConPattern "App" [IdPattern "o", IdPattern "e1", IdPattern "e2"]) [EPatternMatching (EVar "o") [Case (TConPattern "Add" []) [EApp (EApp (EVar "+") $ EApp (EVar "eval1") $ EVar "e1") $ EApp (EVar "eval1") $ EVar "e2"],Case (TConPattern "Sub" []) [EApp (EApp (EVar "-") $ EApp (EVar "eval1") $ EVar "e1") $ EApp (EVar "eval1") $ EVar "e2"]]]]]+ let eval2 = EDestructLetBinding (IdPattern "eval2") [IdPattern "e"] [EPatternMatching (EVar "e") [Case (TConPattern "Num" [IdPattern "n"]) [EVar "n"],Case (TConPattern "App" [TConPattern "Add" [], IdPattern "e1", IdPattern "e2"]) [EApp (EApp (EVar "+") $ EApp (EVar "eval2") $ EVar "e1") $ EApp (EVar "eval2") $ EVar "e2"],Case (TConPattern "App" [TConPattern "Sub" [], IdPattern "e1", IdPattern "e2"]) [EApp (EApp (EVar "-") $ EApp (EVar "eval2") $ EVar "e1") $ EApp (EVar "eval2") $ EVar "e2"]]]+ let res1 = EDestructLetBinding (IdPattern "res1") [] [EApp (EVar "eval1") $ EVar "a"]+ let res2 = EDestructLetBinding (IdPattern "res2") [] [EApp (EVar "eval2") $ EVar "a"]+ let simplify = EDestructLetBinding (IdPattern "simplify") [IdPattern "e"] [EPatternMatching (EVar "e") [Case (TConPattern "App" [TConPattern "Add" [], TConPattern "Num" [IdPattern "n"], IdPattern "e2"]) [EIf (EApp (EApp (EVar "=") $ EVar "n") $ ENum 0) [EVar "e2"] [EVar "e"]]]]+ let a2 = EDestructLetBinding (IdPattern "a2") [] [EApp (EApp (EApp (EVar "App") $ EVar "Add") $ EApp (EVar "Num") $ ENum 0) $ EApp (EVar "Num") $ ENum 6]+ let b = EDestructLetBinding (IdPattern "b") [] [EApp (EVar "simplify") $ EVar "a2"]+ runInferSpecCases [(operData, "Oper"),+ (exprData, "Expr"),+ (a, "Expr"),+ (eval1, "Expr → Number"),+ (eval2, "Expr → Number"),+ (res1, "Number"),+ (res2, "Number"),+ (simplify, "Expr → Expr"),+ (a2, "Expr"),+ (b, "Expr")]+ it "should infer type of lambda expressions even with type annotations" $ do+ let g = EDestructLetBinding (IdPattern "g") [] [ELambda [Named "x" Nothing, Named "y" Nothing] Nothing [EApp (EApp (EVar "+") $ EVar "x") $ EVar "y"]]+ 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 ff = EDestructLetBinding (IdPattern "ff") [] [ELambda [Named "x" (Just intT), Named "y" (Just boolT), 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 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 polymorphism here!!!+ let idpair = ELetBinding (IdPattern "id") (ELambda [Named "x" Nothing] Nothing [EVar "x"]) [(ETuple [EApp (EVar "id") (ENum 3), EApp (EVar "id") (EBool True)])]+ let idpair2 = ELetBinding (IdPattern "id") (ELambda [Named "x" Nothing] Nothing [EVar "x"]) [ELetBinding (IdPattern "a") (ENum 3) [ELetBinding (IdPattern "b") (EApp (EApp (EVar "+") $ EVar "a") $ ENum 3) [(ETuple [EApp (EVar "id") (EVar "a"), EApp (EVar "id") (EVar "b")])]]]+ let f1 = EDestructLetBinding (IdPattern "f1") [] [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 f2 = EDestructLetBinding (IdPattern "f2") [] [ELambda [Named "x" Nothing, Named "y" Nothing, Named "z" Nothing] Nothing [EApp (EApp (EVar "+") (EApp (EApp (EVar "+") $ EVar "x") $ EVar "y")) $ EVar "z"]]+ let f1res = EDestructLetBinding (IdPattern "f1res") [] [EApp (EApp (EApp (EVar "f1") $ ENum 8) $ ENum 2) $ ENum 3]+ let f2res = EDestructLetBinding (IdPattern "f2res") [] [EApp (EApp (EApp (EVar "f2") $ ENum 8) $ ENum 2) $ ENum 3]+ runInferSpecCases [(g, "Number → (Number → Number)"),+ (res0, "Number"),+ (f, "Number → (Number → (Number → Number))"),+ (res1, "Number"),+ (idfn, "α → α"),+ (res2, "Number"),+ (res3, "Boolean"),+ (idpair, "(Number * Boolean)"),+ (idpair2, "(Number * Number)"),+ (f1, "Number → (Number → (Number → Number))"),+ (f2, "Number → (Number → (Number → Number))"),+ (f1res, "Number"),+ (f2res, "Number")]+ failInferSpecCase ff "Type mismatch Boolean ≠ Number"+ it "should infer type of function definition, application and pattern match" $ do+ let fib = EDestructLetBinding (IdPattern "fib") [IdPattern "x"] [EPatternMatching (EVar "x") [Case (NumPattern 0) [ENum 0], Case (NumPattern 1) [ENum 1], Case WildcardPattern [EApp (EApp (EVar "+") $ EApp (EApp (EVar "-") $ EVar "x") $ ENum 1) $ EApp (EApp (EVar "-") $ EVar "x") $ ENum 2]]]+ let fib0 = EApp (EVar "fib") $ ENum 0+ let penultimate = EProgram [EDestructLetBinding (IdPattern "penultimate") [IdPattern "xs"] [EPatternMatching (EVar "xs") [Case (TConPattern "Nil" []) [ENum 0],+ Case (TConPattern "Cons" [WildcardPattern, TConPattern "Nil" []]) [ENum 0],+ Case (TConPattern "Cons" [IdPattern "a", TConPattern "Cons" [WildcardPattern, TConPattern "Nil" []]]) [EVar "a"],+ Case (TConPattern "Cons" [IdPattern "x", TConPattern "Cons" [IdPattern "y", IdPattern "t"]]) [EApp (EVar "penultimate") (EVar "t")]]]]+ let res4 = EDestructLetBinding (IdPattern "res4") [] [EApp (EVar "penultimate") (EList [ENum 1, ENum 2, ENum 3])]+ let map1 = 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"]+ let k = EDestructLetBinding (IdPattern "k") [IdPattern "x", IdPattern "y"] [EPatternMatching (ETuple [EVar "x", EVar "y"]) [Case (TuplePattern [NumPattern 0, NumPattern 0]) [ENum 0], Case WildcardPattern [ENum 1]]]+ let fact = EDestructLetBinding (IdPattern "fact") [IdPattern "n"] [EIf (EApp (EApp (EVar "≤") $ EVar "n") $ ENum 1) [ENum 1] [EApp (EApp (EVar "*") $ EVar "n") (EApp (EVar "fact") $ EApp (EApp (EVar "-") $ EVar "n") $ ENum 1)]]+ let f5 = EDestructLetBinding (IdPattern "f5") [] [EApp (EVar "fact") $ ENum 5]+ let comp = EDestructLetBinding (IdPattern "comp") [IdPattern "f", IdPattern "g", IdPattern "x"] [EApp (EVar "f") (EApp (EVar "g") (EVar "x"))]+ let fix = EDestructLetBinding (IdPattern "fix") [] [EApp (EApp (EVar "comp") $ EVar "inc") (EVar "dec")]+ let incdec = EDestructLetBinding (IdPattern "incdec") [] [EApp (EVar "fix") (ENum 5)]+ let len = EDestructLetBinding (IdPattern "len") [IdPattern "xs"] [EPatternMatching (EVar "xs") [Case (TConPattern "Nil" []) [ENum 0],Case (TConPattern "Cons" [WildcardPattern, IdPattern "t"]) [EApp (EApp (EVar "+") $ ENum 1) (EApp (EVar "len") $ EVar "t")]]]+ let lenl = EApp (EVar "len") $ EVar "l"+ let append = EDestructLetBinding (IdPattern "append") [IdPattern "x", IdPattern "xs"] [EApp (EApp (EVar "Cons") $ EVar "x") $ EVar "xs"]+ let l2 = EDestructLetBinding (IdPattern "l2") [] [EApp (EApp (EVar "append") $ ENum 0) $ EVar "l"]+ let patmat0 = EDestructLetBinding (IdPattern "patmat0") [] [EPatternMatching (ETuple [EStr "a", ENum 3]) [Case (IdPattern "a") [ETuple [EStr "ok", EVar "a"]]]]+ let patmat1 = EDestructLetBinding (IdPattern "patmat1") [] [EPatternMatching (ETuple [EStr "a", ENum 3]) [Case (TuplePattern [IdPattern "a", IdPattern "b"]) [ETuple [EStr "ok", EVar "a", EVar "b"]]]]+ let patmat2 = EDestructLetBinding (IdPattern "patmat2") [] [EPatternMatching (ETuple [EStr "a", ENum 3]) [Case (TuplePattern [IdPattern "a", WildcardPattern]) [ETuple [EStr "ok", EVar "a"]]]]+ let patmat3 = EDestructLetBinding (IdPattern "patmat3") [] [EPatternMatching (EChar 'a') [Case (CharPattern 'a') [EBool True], Case WildcardPattern [EBool False]]]+ let patmat4 = EDestructLetBinding (IdPattern "patmat4") [] [EPatternMatching (EBool True) [Case (BoolPattern True) [EBool True], Case WildcardPattern [EBool False]]]+ let patmat5 = EDestructLetBinding (IdPattern "patmat5") [] [EPatternMatching (ENum 1) [Case (NumPattern 1) [EBool True], Case WildcardPattern [EBool False]]]+ let patmat6 = EDestructLetBinding (IdPattern "patmat6") [] [EPatternMatching (EStr "abc") [Case (TConPattern "Cons" [CharPattern 'a', (TConPattern "Cons" [CharPattern 'b', (TConPattern "Cons" [CharPattern 'c', TConPattern "Nil" []])])]) [EBool True], Case WildcardPattern [EBool False]]]+ runInferSpecCases [(fib, "Number → Number"),+ (fib0, "Number"),+ (penultimate, "[Number] → Number"),+ (res4, "Number"),+ (map1, "(α → β) → ([α] → [β])"),+ (map2, "(α → β) → ([α] → [β])"),+ (l, "[Number]"),+ (l3, "[Boolean]"),+ (k, "Number → (Number → Number)"),+ (fact, "Number → Number"),+ (f5, "Number"),+ (comp, "(β → γ) → ((α → β) → (α → γ))"),+ (fix, "Number → Number"),+ (incdec, "Number"),+ (len, "[α] → Number"),+ (lenl, "Number"),+ (append, "α → ([α] → [α])"),+ (l2, "[Number]"),+ (patmat0, "([Char] * ([Char] * Number))"),+ (patmat1, "([Char] * [Char] * Number)"),+ (patmat2, "([Char] * [Char])"),+ (patmat3, "Boolean"),+ (patmat4, "Boolean"),+ (patmat5, "Boolean"),+ (patmat6, "Boolean")]+ it "should infer type of basic syntax element" $ do+ let xb = EDestructLetBinding (IdPattern "x") [] [EBool True]+ let d = EDestructLetBinding (IdPattern "d") [] [ETuple [ETuple [ENum 4, EBool True], ETuple [EStr "test", EChar 'c', ENum 45]]]+ let intsum = EApp (EApp (EVar "+") (EApp (EApp (EVar "+") (EApp (EApp (EVar "+") (EApp (EApp (EVar "+") $ ENum 1) $ ENum 2)) $ ENum 3)) $ ENum 4)) $ ENum 5+ let l = EDestructLetBinding (IdPattern "y") [] [EList [ENum 1, ENum 2, ENum 3]]+ let l2 = EDestructLetBinding (IdPattern "z") [] [EList []]+ let a = EDestructLetBinding (IdPattern "a") [] [EChar 'a']+ let s = EDestructLetBinding (IdPattern "s") [] [EStr "qdsfsdf"]+ let l3 = EDestructLetBinding (IdPattern "l") [] [EApp (EApp (EVar "Cons") $ ENum 1) $ EApp (EApp (EVar "Cons") $ ENum 2) $ EApp (EApp (EVar "Cons") $ ENum 3) $ EVar "Nil"]+ let profile = EDestructLetBinding (IdPattern "profile") [] [ERecord (M.fromList [("name", EStr "ntha"), ("age", ENum 12)])]+ let name = EAccessor (EVar "profile") "name"+ let equal = (EApp (EApp (EVar "=") $ ENum 3) $ ENum 3)+ let notequal = (EApp (EApp (EVar "≠") $ EBool True) $ EBool False)+ runInferSpecCases [(xb, "Boolean"),+ (d, "((Number * Boolean) * ([Char] * Char * Number))"),+ (intsum, "Number"),+ (l, "[Number]"),+ (l2, "[α]"),+ (a, "Char"),+ (s, "[Char]"),+ (l3, "[Number]"),+ (profile, "{age: Number, name: [Char]}"),+ (name, "[Char]"),+ (equal, "Boolean"),+ (notequal, "Boolean")]+ it "should infer type of destructuring" $ do+ let abpair = EDestructLetBinding (TuplePattern [IdPattern "a", IdPattern "b"]) [] [ETuple [ENum 3, EStr "d"]]+ let d = EDestructLetBinding (IdPattern "d") [] [ETuple [ETuple [ENum 3, EBool True], ETuple [EStr "test", EChar 'c', EVar "a"]]]+ let bool = EDestructLetBinding (TuplePattern [TuplePattern [WildcardPattern, IdPattern "bool"], TuplePattern [WildcardPattern, WildcardPattern, WildcardPattern]]) [] [EVar "d"]+ let boolv = EVar "bool"+ let abctuple = ELetBinding (TuplePattern [IdPattern "a", IdPattern "b", IdPattern "c"]) (ETuple [ENum 1, ENum 2, ENum 3]) [(EApp (EApp (EVar "+") (EApp (EApp (EVar "+") $ EVar "a") $ EVar "b")) $ EVar "c")]+ let abclist = EDestructLetBinding (TConPattern "Cons" [IdPattern "a", TConPattern "Cons" [IdPattern "b", TConPattern "Cons" [IdPattern "c", TConPattern "Nil" []]]]) [] [EList [ENum 1, ENum 2, ENum 3]]+ let a = EVar "a"+ let b = EVar "b"+ let c = EVar "c"+ let abclist2 = ELetBinding (TConPattern "Cons" [IdPattern "a", TConPattern "Cons" [IdPattern "b", TConPattern "Cons" [IdPattern "c", TConPattern "Nil" []]]]) (EList [ENum 1, ENum 2, ENum 3]) [(EApp (EApp (EVar "+") (EApp (EApp (EVar "+") $ EVar "a") $ EVar "b")) $ EVar "c")]+ let abctuplefn = EDestructLetBinding (IdPattern "f1") [(TuplePattern [IdPattern "a", IdPattern "b", IdPattern "c"])] [(EApp (EApp (EVar "+") (EApp (EApp (EVar "+") $ EVar "a") $ EVar "b")) $ EVar "c")]+ let abclistfn = EDestructLetBinding (IdPattern "f2") [(TConPattern "Cons" [IdPattern "a", TConPattern "Cons" [IdPattern "b", TConPattern "Cons" [IdPattern "c", TConPattern "Nil" []]]])] [(EApp (EApp (EVar "+") (EApp (EApp (EVar "+") $ EVar "a") $ EVar "b")) $ EVar "c")]+ let res1 = EApp (EVar "f1") $ ETuple [EVar "a", EVar "b", EVar "c"]+ let res2 = EApp (EVar "f2") $ EList [EVar "a", EVar "b", EVar "c"]+ tvarA <- makeVariable+ let name = "Maybe"+ let vars = [tvarA]+ let dataType = TOper name vars+ let justConstructor = TypeConstructor "Just" [tvarA]+ let nothingConstructor = TypeConstructor "Nothing" []+ let maybeData = EDataDecl name dataType vars [justConstructor, nothingConstructor]+ let f = EDestructLetBinding (IdPattern "f3") [(TConPattern "Just" [IdPattern "a"])] [(EApp (EApp (EVar "+") $ EVar "a") $ ENum 1)]+ let res3 = EApp (EVar "f3") $ EApp (EVar "Just") $ ENum 2+ let just = EDestructLetBinding (TConPattern "Just" [IdPattern "k"]) [] [EApp (EVar "Just") $ ENum 3]+ let k = EVar "k"+ runInferSpecCases [(abpair, "(Number * [Char])"),+ (d, "((Number * Boolean) * ([Char] * Char * Number))"),+ (bool, "((Number * Boolean) * ([Char] * Char * Number))"),+ (boolv, "Boolean"),+ (abctuple, "Number"),+ (a, "Number"),+ (b, "Number"),+ (c, "Number"),+ (abclist, "[Number]"),+ (abclist2, "Number"),+ (abctuplefn, "(Number * Number * Number) → Number"),+ (abclistfn, "[Number] → Number"),+ (res1, "Number"),+ (res2, "Number"),+ (maybeData, "(Maybe α)"),+ (f, "(Maybe Number) → Number"),+ (res3, "Number"),+ (just, "(Maybe Number)"),+ (k, "Number")]
+ test/ParserSpec.hs view
@@ -0,0 +1,160 @@+module ParserSpec where++import Ast+import Type+import Parser+import qualified Data.Map as M+import qualified Text.PrettyPrint as PP+import Test.Hspec++spec :: Spec+spec = do+ describe "parser test" $ do+ it "should parse ADT and pattern match expressions part1" $ do+ tvarA <- makeVariable+ let name = "List"+ let vars = [tvarA]+ let dataType = TOper name vars+ let consConstructor = TypeConstructor "Cons" [tvarA, dataType]+ let nilConstructor = TypeConstructor "Nil" []+ let listData = EDataDecl name dataType vars [consConstructor, nilConstructor]+ ((PP.text . show) (parseExpr "(data List a (Cons a (List a)) Nil)")) `shouldBe` ((PP.text . show) (EProgram [listData]))+ parseExpr "(let xs Nil)" `shouldBe` EProgram [EDestructLetBinding (IdPattern "xs") [] [(EVar "Nil")]]+ parseExpr "(let ys (Cons 5 Nil))" `shouldBe` EProgram [EDestructLetBinding (IdPattern "ys") [] [EApp (EApp (EVar "Cons") $ ENum 5) $ EVar "Nil"]]+ parseExpr "(ƒ len [l] (match l (Nil ⇒ 0) ((Cons h t) ⇒ (+ 1 (len t)))))" `shouldBe` EProgram [EDestructLetBinding (IdPattern "len") [IdPattern "l"] [EPatternMatching (EVar "l") [Case (TConPattern "Nil" []) [ENum 0],+ Case (TConPattern "Cons" [IdPattern "h", IdPattern "t"]) [EApp (EApp (EVar "+") $ ENum 1) $ EApp (EVar "len") $ EVar "t"]]]]+ parseExpr "(let xy ((len xs) . (len ys)))" `shouldBe` EProgram [EDestructLetBinding (IdPattern "xy") [] [ETuple [EApp (EVar "len") (EVar "xs"), EApp (EVar "len") (EVar"ys")]]]+ parseExpr "(let zs (Cons 5 (Cons 4 (Cons 3 Nil))))" `shouldBe` EProgram [EDestructLetBinding (IdPattern "zs") [] [EApp (EApp (EVar "Cons") $ ENum 5) $ EApp (EApp (EVar "Cons") $ ENum 4) $ EApp (EApp (EVar "Cons") $ ENum 3) $ EVar "Nil"]]+ parseExpr "(let z (len zs))" `shouldBe` EProgram [EDestructLetBinding (IdPattern "z") [] [EApp (EVar "len") $ EVar "zs"]]+ it "should parse ADT and pattern match expressions part2" $ do+ tvarB <- makeVariable+ let name2 = "Tree"+ let vars2 = [tvarB]+ let dataType2 = TOper name2 vars2+ let nullConstructor = TypeConstructor "Null" []+ let leafConstructor = TypeConstructor "Leaf" [tvarB]+ let nodeConstructor = TypeConstructor "Node" [dataType2, tvarB, dataType2]+ let treeData = EDataDecl name2 dataType2 vars2 [nullConstructor, leafConstructor, nodeConstructor]+ ((PP.text . show) (parseExpr "(data Tree a Null (Leaf a) (Node (Tree a) a (Tree a)))")) `shouldBe` ((PP.text . show) (EProgram [treeData]))+ parseExpr "(let t (Node (Leaf 5) 4 (Leaf 3)))" `shouldBe` EProgram [EDestructLetBinding (IdPattern "t") [] [EApp (EApp (EApp (EVar "Node") $ EApp (EVar "Leaf") $ ENum 5) $ ENum 4) $ EApp (EVar "Leaf") $ ENum 3]]+ it "should parse ADT and pattern match expressions part3" $ do+ let name3 = "Ast"+ let dataType3 = TOper name3 []+ let numConstructor = TypeConstructor "Num" [intT]+ let addConstructor = TypeConstructor "Add" [dataType3, dataType3]+ let subConstructor = TypeConstructor "Sub" [dataType3, dataType3]+ let mulConstructor = TypeConstructor "Mul" [dataType3, dataType3]+ let divConstructor = TypeConstructor "Div" [dataType3, dataType3]+ let astData = EDataDecl name3 dataType3 [] [numConstructor, addConstructor, subConstructor, mulConstructor, divConstructor]+ parseExpr "(data Ast (Num Number) (Add Ast Ast) (Sub Ast Ast) (Mul Ast Ast) (Div Ast Ast))" `shouldBe` EProgram [astData]+ parseExpr "(ƒ eval [n] (match n ((Num a) => a) ((Add a b) => (+ (eval a) (eval b))) ((Sub a b) => (- (eval a) (eval b))) ((Mul a b) => (* (eval a) (eval b))) ((Div a b) => (/ (eval a) (eval b)))))" `shouldBe` EProgram [EDestructLetBinding (IdPattern "eval") [IdPattern "n"] [EPatternMatching (EVar "n") [Case (TConPattern "Num" [IdPattern "a"]) [EVar "a"],+ Case (TConPattern "Add" [IdPattern "a", IdPattern "b"]) [EApp (EApp (EVar "+") $ EApp (EVar "eval") $ EVar "a") $ EApp (EVar "eval") $ EVar "b"],+ Case (TConPattern "Sub" [IdPattern "a", IdPattern "b"]) [EApp (EApp (EVar "-") $ EApp (EVar "eval") $ EVar "a") $ EApp (EVar "eval") $ EVar "b"],+ Case (TConPattern "Mul" [IdPattern "a", IdPattern "b"]) [EApp (EApp (EVar "*") $ EApp (EVar "eval") $ EVar "a") $ EApp (EVar "eval") $ EVar "b"],+ Case (TConPattern "Div" [IdPattern "a", IdPattern "b"]) [EApp (EApp (EVar "/") $ EApp (EVar "eval") $ EVar "a") $ EApp (EVar "eval") $ EVar "b"]]]]+ parseExpr "(let sym (Mul (Add (Num 4) (Num 3)) (Sub (Num 4) (Num 1))))" `shouldBe` EProgram [EDestructLetBinding (IdPattern "sym") [] [EApp (EApp (EVar "Mul") (EApp (EApp (EVar "Add") $ EApp (EVar "Num") $ ENum 4) $ EApp (EVar "Num") $ ENum 3)) (EApp (EApp (EVar "Sub") $ EApp (EVar "Num") $ ENum 4) $ EApp (EVar "Num") $ ENum 1)]]+ parseExpr "(let result (eval sym))" `shouldBe` EProgram [EDestructLetBinding (IdPattern "result") [] [EApp (EVar "eval") $ EVar "sym"]]+ it "should parse ADT and pattern match expressions part4" $ do+ let name4 = "Oper"+ let dataType4 = TOper name4 []+ let addOperConstructor = TypeConstructor "Add" []+ let subOperConstructor = TypeConstructor "Sub" []+ let operData = EDataDecl name4 dataType4 [] [addOperConstructor, subOperConstructor]+ parseExpr "(data Oper Add Sub)" `shouldBe` EProgram [operData]+ let name5 = "Expr"+ let dataType5 = TOper name5 []+ let numExprConstructor = TypeConstructor "Num" [intT]+ let appExprConstructor = TypeConstructor "App" [dataType4, dataType5, dataType5]+ let exprData = EDataDecl name5 dataType5 [] [numExprConstructor, appExprConstructor]+ parseExpr "(data Expr (Num Number) (App Oper Expr Expr))" `shouldBe` EProgram [exprData]+ parseExpr "(let a (App Add (Num 5) (Num 6)))" `shouldBe` EProgram [EDestructLetBinding (IdPattern "a") [] [EApp (EApp (EApp (EVar "App") $ EVar "Add") $ EApp (EVar "Num") $ ENum 5) $ EApp (EVar "Num") $ ENum 6]]+ parseExpr "(ƒ eval [e] (match e ((Num n) => n) ((App o e1 e2) => (match o (Add => (+ (eval e1) (eval e2))) (Sub => (- (eval e1) (eval e2)))))))" `shouldBe` EProgram [EDestructLetBinding (IdPattern "eval") [IdPattern "e"] [EPatternMatching (EVar "e") [Case (TConPattern "Num" [IdPattern "n"]) [EVar "n"],+ Case (TConPattern "App" [IdPattern "o", IdPattern "e1", IdPattern "e2"]) [EPatternMatching (EVar "o") [Case (TConPattern "Add" []) [EApp (EApp (EVar "+") $ EApp (EVar "eval") $ EVar "e1") $ EApp (EVar "eval") $ EVar "e2"],+ Case (TConPattern "Sub" []) [EApp (EApp (EVar "-") $ EApp (EVar "eval") $ EVar "e1") $ EApp (EVar "eval") $ EVar "e2"]]]]]]+ parseExpr "(ƒ eval [e] (match e ((Num n) => n) ((App Add e1 e2) => (+ (eval e1) (eval e2))) ((App Sub e1 e2) => (- (eval e1) (eval e2)))))" `shouldBe` EProgram [EDestructLetBinding (IdPattern "eval") [IdPattern "e"] [EPatternMatching (EVar "e") [Case (TConPattern "Num" [IdPattern "n"]) [EVar "n"],+ Case (TConPattern "App" [TConPattern "Add" [], IdPattern "e1", IdPattern "e2"]) [EApp (EApp (EVar "+") $ EApp (EVar "eval") $ EVar "e1") $ EApp (EVar "eval") $ EVar "e2"],+ Case (TConPattern "App" [TConPattern "Sub" [], IdPattern "e1", IdPattern "e2"]) [EApp (EApp (EVar "-") $ EApp (EVar "eval") $ EVar "e1") $ EApp (EVar "eval") $ EVar "e2"]]]]+ parseExpr "(let av (eval a))" `shouldBe` EProgram [EDestructLetBinding (IdPattern "av") [] [EApp (EVar "eval") $ EVar "a"]]+ parseExpr "(ƒ simplify [e] (match e ((App Add (Num n) e2) => (if (= n 0) e2 e))))" `shouldBe` EProgram [EDestructLetBinding (IdPattern "simplify") [IdPattern "e"] [EPatternMatching (EVar "e") [Case (TConPattern "App" [TConPattern "Add" [], TConPattern "Num" [IdPattern "n"], IdPattern "e2"]) [EIf (EApp (EApp (EVar "=") $ EVar "n") $ ENum 0) [EVar "e2"] [EVar "e"]]]]]+ parseExpr "(let a (App Add (Num 0) (Num 6)))" `shouldBe` EProgram [EDestructLetBinding (IdPattern "a") [] [EApp (EApp (EApp (EVar "App") $ EVar "Add") $ EApp (EVar "Num") $ ENum 0) $ EApp (EVar "Num") $ ENum 6]]+ parseExpr "(let b (simplify a))" `shouldBe` EProgram [EDestructLetBinding (IdPattern "b") [] [EApp (EVar "simplify") $ EVar "a"]]+ it "should parse lambda expressions even with type annotations" $ do+ parseExpr "(let g (λx y ⇒ (+ x y)))" `shouldBe` EProgram [EDestructLetBinding (IdPattern "g") [] [ELambda [Named "x" Nothing, Named "y" Nothing] Nothing [EApp (EApp (EVar "+") $ EVar "x") $ EVar "y"]]]+ parseExpr "(let res0 (g 3 3))" `shouldBe` EProgram [EDestructLetBinding (IdPattern "res0") [] [EApp (EApp (EVar "g") $ ENum 3) $ ENum 3]]+ parseExpr "(let id (λx ⇒ x))" `shouldBe` EProgram [EDestructLetBinding (IdPattern "id") [] [ELambda [Named "x" Nothing] Nothing [EVar "x"]]]+ parseExpr "(let res2 (id 3))" `shouldBe` EProgram [EDestructLetBinding (IdPattern "res2") [] [EApp (EVar "id") $ ENum 3]]+ parseExpr "(let res3 (id true))" `shouldBe` EProgram [EDestructLetBinding (IdPattern "res3") [] [EApp (EVar "id") $ EBool True]]+ parseExpr "(let [id (λx ⇒ x)] ((id 3) . (id true)))" `shouldBe` EProgram [ELetBinding (IdPattern "id") (ELambda [Named "x" Nothing] Nothing [EVar "x"]) [(ETuple [EApp (EVar "id") (ENum 3), EApp (EVar "id") (EBool True)])]]+ parseExpr "(let [id (λx ⇒ x) a 3 b (+ a 3)] ((id a) . (id b)))" `shouldBe` EProgram [ELetBinding (IdPattern "id") (ELambda [Named "x" Nothing] Nothing [EVar "x"]) [ELetBinding (IdPattern "a") (ENum 3) [ELetBinding (IdPattern "b") (EApp (EApp (EVar "+") $ EVar "a") $ ENum 3) [(ETuple [EApp (EVar "id") (EVar "a"), EApp (EVar "id") (EVar "b")])]]]]+ parseExpr "(let f (λ(x: Number) (y: Number) (z: Number) : Number => (+ x y z)))" `shouldBe` EProgram [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"]]]+ parseExpr "(let f (λx y z => (+ x y z)))" `shouldBe` EProgram [EDestructLetBinding (IdPattern "f") [] [ELambda [Named "x" Nothing, Named "y" Nothing, Named "z" Nothing] Nothing [EApp (EApp (EVar "+") (EApp (EApp (EVar "+") $ EVar "x") $ EVar "y")) $ EVar "z"]]]+ parseExpr "(let res (f 8 2 3))" `shouldBe` EProgram [EDestructLetBinding (IdPattern "res") [] [EApp (EApp (EApp (EVar "f") $ ENum 8) $ ENum 2) $ ENum 3]]+ it "should parse function definition, application and pattern match" $ do+ parseExpr "(ƒ fib [x]\n (match x\n (0 => 0)\n (1 => 1)\n (_ => (+ (fib (- x 1)) (fib (- x 2))))))" `shouldBe` EProgram [EDestructLetBinding (IdPattern "fib") [IdPattern "x"] [EPatternMatching (EVar "x") [Case (NumPattern 0) [ENum 0],+ Case (NumPattern 1) [ENum 1],+ Case WildcardPattern [EApp (EApp (EVar "+") (EApp (EVar "fib") $ EApp (EApp (EVar "-") $ EVar "x") $ ENum 1)) $ EApp (EVar "fib") $ EApp (EApp (EVar "-") $ EVar "x") $ ENum 2]]]]+ parseExpr "(ƒ penultimate [xs]\n (match xs\n ([] => 0)\n ([_] => 0)\n ([a _] => a)\n (x :: y :: t => (penultimate t))))" `shouldBe` EProgram [EDestructLetBinding (IdPattern "penultimate") [IdPattern "xs"] [EPatternMatching (EVar "xs") [Case (TConPattern "Nil" []) [ENum 0],+ Case (TConPattern "Cons" [WildcardPattern, TConPattern "Nil" []]) [ENum 0],+ Case (TConPattern "Cons" [IdPattern "a", TConPattern "Cons" [WildcardPattern, TConPattern "Nil" []]]) [EVar "a"],+ Case (TConPattern "Cons" [IdPattern "x", TConPattern "Cons" [IdPattern "y", IdPattern "t"]]) [EApp (EVar "penultimate") (EVar "t")]]]]+ parseExpr "(let res4 (penultimate [1 2 3]))" `shouldBe` EProgram [EDestructLetBinding (IdPattern "res4") [] [EApp (EVar "penultimate") (EList [ENum 1, ENum 2, ENum 3])]]+ parseExpr "(let x (penultimate [[\"g\"] [\"c\"]]))" `shouldBe` EProgram [EDestructLetBinding (IdPattern "x") [] [EApp (EVar "penultimate") (EList [EList [EStr "g"], EList [EStr "c"]])]]+ parseExpr "(ƒ map [f l] (match l ((Cons h t) => (Cons (f h) (map f t))) (Nil => Nil)))" `shouldBe` EProgram [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"]]]]+ parseExpr "(ƒ map [f xs] (match xs ([] ⇒ []) (h :: t ⇒ ((f h) :: (map f t)))))" `shouldBe` EProgram [EDestructLetBinding (IdPattern "map") [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 "map") $ EVar "f") $ EVar "t"]]]]+ parseExpr "(let l3 (map (λx => (= (% x 2) 0)) l))" `shouldBe` EProgram [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"]]+ parseExpr "(ƒ k [x y] (match (x . y) ((0 . 0) => 0) (_ => 1)))" `shouldBe` EProgram [EDestructLetBinding (IdPattern "k") [IdPattern "x", IdPattern "y"] [EPatternMatching (ETuple [EVar "x", EVar "y"]) [Case (TuplePattern [NumPattern 0, NumPattern 0]) [ENum 0], Case WildcardPattern [ENum 1]]]]+ parseExpr "(ƒ fact [n] (if (≤ n 1) 1 (* n (fact (- n 1)))))" `shouldBe` EProgram [EDestructLetBinding (IdPattern "fact") [IdPattern "n"] [EIf (EApp (EApp (EVar "≤") $ EVar "n") $ ENum 1) [ENum 1] [EApp (EApp (EVar "*") $ EVar "n") (EApp (EVar "fact") $ EApp (EApp (EVar "-") $ EVar "n") $ ENum 1)]]]+ parseExpr "(let f5 (fact 5))" `shouldBe` EProgram [EDestructLetBinding (IdPattern "f5") [] [EApp (EVar "fact") $ ENum 5]]+ parseExpr "(ƒ comp [f g x] (f (g x)))" `shouldBe` EProgram [EDestructLetBinding (IdPattern "comp") [IdPattern "f", IdPattern "g", IdPattern "x"] [EApp (EVar "f") (EApp (EVar "g") (EVar "x"))]]+ parseExpr "(let fix (comp inc dec))" `shouldBe` EProgram [EDestructLetBinding (IdPattern "fix") [] [EApp (EApp (EVar "comp") $ EVar "inc") (EVar "dec")]]+ parseExpr "(let incdec (fix 5))" `shouldBe` EProgram [EDestructLetBinding (IdPattern "incdec") [] [EApp (EVar "fix") (ENum 5)]]+ parseExpr "(ƒ len2 [xs] (match xs ([] => 0) (_ :: t => (+ 1 (len2 t)))))" `shouldBe` EProgram [EDestructLetBinding (IdPattern "len2") [IdPattern "xs"] [EPatternMatching (EVar "xs") [Case (TConPattern "Nil" []) [ENum 0],+ Case (TConPattern "Cons" [WildcardPattern, IdPattern "t"]) [EApp (EApp (EVar "+") $ ENum 1) (EApp (EVar "len2") $ EVar "t")]]]]+ parseExpr "(len2 y)" `shouldBe` EProgram [EApp (EVar "len2") $ EVar "y"]+ parseExpr "(ƒ append [x xs] (x :: xs))" `shouldBe` EProgram [EDestructLetBinding (IdPattern "append") [IdPattern "x", IdPattern "xs"] [EApp (EApp (EVar "Cons") $ EVar "x") $ EVar "xs"]]+ parseExpr "(let l2 (append 0 l))" `shouldBe` EProgram [EDestructLetBinding (IdPattern "l2") [] [EApp (EApp (EVar "append") $ ENum 0) $ EVar "l"]]+ parseExpr "(let patmat0 (match (\"a\" . 3) (a => (\"ok\" . a))))" `shouldBe` EProgram [EDestructLetBinding (IdPattern "patmat0") [] [EPatternMatching (ETuple [EStr "a", ENum 3]) [Case (IdPattern "a") [ETuple [EStr "ok", EVar "a"]]]]]+ parseExpr "(let patmat1 (match (\"a\" . 3) ((a . b) => (\"ok\" . a . b))))" `shouldBe` EProgram [EDestructLetBinding (IdPattern "patmat1") [] [EPatternMatching (ETuple [EStr "a", ENum 3]) [Case (TuplePattern [IdPattern "a", IdPattern "b"]) [ETuple [EStr "ok", EVar "a", EVar "b"]]]]]+ parseExpr "(let patmat2 (match (\"a\" . 3) ((a . _) => (\"ok\" . a))))" `shouldBe` EProgram [EDestructLetBinding (IdPattern "patmat2") [] [EPatternMatching (ETuple [EStr "a", ENum 3]) [Case (TuplePattern [IdPattern "a", WildcardPattern]) [ETuple [EStr "ok", EVar "a"]]]]]+ parseExpr "(let patmat3 (match 'a' ('a' => true) (_ => false)))" `shouldBe` EProgram [EDestructLetBinding (IdPattern "patmat3") [] [EPatternMatching (EChar 'a') [Case (CharPattern 'a') [EBool True], Case WildcardPattern [EBool False]]]]+ parseExpr "(let patmat4 (match true (true => true) (_ => false)))" `shouldBe` EProgram [EDestructLetBinding (IdPattern "patmat4") [] [EPatternMatching (EBool True) [Case (BoolPattern True) [EBool True], Case WildcardPattern [EBool False]]]]+ parseExpr "(let patmat5 (match 1 (1 => true) (_ => false)))" `shouldBe` EProgram [EDestructLetBinding (IdPattern "patmat5") [] [EPatternMatching (ENum 1) [Case (NumPattern 1) [EBool True], Case WildcardPattern [EBool False]]]]+ parseExpr "(let patmat6 (match \"abc\" (\"abc\" => true) (_ => false)))" `shouldBe` EProgram [EDestructLetBinding (IdPattern "patmat6") [] [EPatternMatching (EStr "abc") [Case (TConPattern "Cons" [CharPattern 'a', (TConPattern "Cons" [CharPattern 'b', (TConPattern "Cons" [CharPattern 'c', TConPattern "Nil" []])])]) [EBool True], Case WildcardPattern [EBool False]]]]+ it "should parse basic syntax element" $ do+ parseExpr "(let x true)" `shouldBe` EProgram [EDestructLetBinding (IdPattern "x") [] [EBool True]]+ parseExpr "(let d ((4 . true) . (\"test\" . 'c' . 45)))" `shouldBe` EProgram [EDestructLetBinding (IdPattern "d") [] [ETuple [ETuple [ENum 4, EBool True], ETuple [EStr "test", EChar 'c', ENum 45]]]]+ parseExpr "(+ 1 2 3 4 5)" `shouldBe` EProgram [EApp (EApp (EVar "+") (EApp (EApp (EVar "+") (EApp (EApp (EVar "+") (EApp (EApp (EVar "+") $ ENum 1) $ ENum 2)) $ ENum 3)) $ ENum 4)) $ ENum 5]+ parseExpr "(let y [1 2 3])" `shouldBe` EProgram [EDestructLetBinding (IdPattern "y") [] [EList [ENum 1, ENum 2, ENum 3]]]+ parseExpr "(let z [])" `shouldBe` EProgram [EDestructLetBinding (IdPattern "z") [] [EList []]]+ parseExpr "(let a 'a')" `shouldBe` EProgram [EDestructLetBinding (IdPattern "a") [] [EChar 'a']]+ parseExpr "(let s \"qdsfsdf\")" `shouldBe` EProgram [EDestructLetBinding (IdPattern "s") [] [EStr "qdsfsdf"]]+ parseExpr "(let l (1 :: 2 :: 3 :: Nil))" `shouldBe` EProgram [EDestructLetBinding (IdPattern "l") [] [EApp (EApp (EVar "Cons") $ ENum 1) $ EApp (EApp (EVar "Cons") $ ENum 2) $ EApp (EApp (EVar "Cons") $ ENum 3) $ EVar "Nil"]]+ parseExpr "(let profile {:name \"ntha\" :age 12})" `shouldBe` EProgram [EDestructLetBinding (IdPattern "profile") [] [ERecord (M.fromList [("name", EStr "ntha"), ("age", ENum 12)])]]+ parseExpr "(:name profile)" `shouldBe` EProgram [EAccessor (EVar "profile") "name"]+ it "should parse cond expression" $ do+ parseExpr "(ƒ fact [n] (cond ((≤ n 1) → 1) (else → (* n (fact (- n 1))))))" `shouldBe` parseExpr "(ƒ fact [n] (if (≤ n 1) 1 (* n (fact (- n 1)))))"+ parseExpr "(ƒ fib [x] (cond ((= x 0) ⇒ 0) ((= x 1) ⇒ 1) (else ⇒ (+ (fib (- x 1)) (fib (- x 2))))))" `shouldBe` parseExpr "(ƒ fib [x] (if (= x 0) 0 (if (= x 1) 1 (+ (fib (- x 1)) (fib (- x 2))))))"+ it "should parse destructuring" $ do+ parseExpr "(let (a . b) (3 . \"d\"))" `shouldBe` EProgram [EDestructLetBinding (TuplePattern [IdPattern "a", IdPattern "b"]) [] [ETuple [ENum 3, EStr "d"]]]+ parseExpr "(let d ((3 . true) . (\"test\" . 'c' . a)))" `shouldBe` EProgram [EDestructLetBinding (IdPattern "d") [] [ETuple [ETuple [ENum 3, EBool True], ETuple [EStr "test", EChar 'c', EVar "a"]]]]+ parseExpr "(let ((_ . bool) . (_ . _ . _)) d)" `shouldBe` EProgram [EDestructLetBinding (TuplePattern [TuplePattern [WildcardPattern, IdPattern "bool"], TuplePattern [WildcardPattern, WildcardPattern, WildcardPattern]]) [] [EVar "d"]]+ parseExpr "(let [(a . b . c) (1 . 2 . 3)] (+ a b c))" `shouldBe` EProgram [ELetBinding (TuplePattern [IdPattern "a", IdPattern "b", IdPattern "c"]) (ETuple [ENum 1, ENum 2, ENum 3]) [(EApp (EApp (EVar "+") (EApp (EApp (EVar "+") $ EVar "a") $ EVar "b")) $ EVar "c")]]+ parseExpr "(let (a :: b :: c) [1 2 3])" `shouldBe` EProgram [EDestructLetBinding (TConPattern "Cons" [IdPattern "a", TConPattern "Cons" [IdPattern "b", TConPattern "Cons" [IdPattern "c", TConPattern "Nil" []]]]) [] [EList [ENum 1, ENum 2, ENum 3]]]+ parseExpr "(let [(a :: b :: c) [1 2 3]] (+ a b c))" `shouldBe` EProgram [ELetBinding (TConPattern "Cons" [IdPattern "a", TConPattern "Cons" [IdPattern "b", TConPattern "Cons" [IdPattern "c", TConPattern "Nil" []]]]) (EList [ENum 1, ENum 2, ENum 3]) [(EApp (EApp (EVar "+") (EApp (EApp (EVar "+") $ EVar "a") $ EVar "b")) $ EVar "c")]]+ parseExpr "(ƒ f [(a . b . c)] (+ a b c))" `shouldBe` EProgram [EDestructLetBinding (IdPattern "f") [(TuplePattern [IdPattern "a", IdPattern "b", IdPattern "c"])] [(EApp (EApp (EVar "+") (EApp (EApp (EVar "+") $ EVar "a") $ EVar "b")) $ EVar "c")]]+ parseExpr "(ƒ f [(a :: b :: c)] (+ a b c))" `shouldBe` EProgram [EDestructLetBinding (IdPattern "f") [(TConPattern "Cons" [IdPattern "a", TConPattern "Cons" [IdPattern "b", TConPattern "Cons" [IdPattern "c", TConPattern "Nil" []]]])] [(EApp (EApp (EVar "+") (EApp (EApp (EVar "+") $ EVar "a") $ EVar "b")) $ EVar "c")]]+ parseExpr "(f (a . b . c))" `shouldBe` EProgram [EApp (EVar "f") $ ETuple [EVar "a", EVar "b", EVar "c"]]+ parseExpr "(f [a b c])" `shouldBe` EProgram [EApp (EVar "f") $ EList [EVar "a", EVar "b", EVar "c"]]+ tvarA <- makeVariable+ let name = "Maybe"+ let vars = [tvarA]+ let dataType = TOper name vars+ let justConstructor = TypeConstructor "Just" [tvarA]+ let nothingConstructor = TypeConstructor "Nothing" []+ let maybeData = EDataDecl name dataType vars [justConstructor, nothingConstructor]+ ((PP.text . show) (parseExpr "(data Maybe a (Just a) Nothing)")) `shouldBe` ((PP.text . show) (EProgram [maybeData]))+ parseExpr "(ƒ f [(Just a)] (+ a 1))" `shouldBe` EProgram [EDestructLetBinding (IdPattern "f") [(TConPattern "Just" [IdPattern "a"])] [(EApp (EApp (EVar "+") $ EVar "a") $ ENum 1)]]+ parseExpr "(f (Just 2))" `shouldBe` EProgram [EApp (EVar "f") $ EApp (EVar "Just") $ ENum 2]+ parseExpr "(let (Just k) (Just 3))" `shouldBe` EProgram [EDestructLetBinding (TConPattern "Just" [IdPattern "k"]) [] [EApp (EVar "Just") $ ENum 3]]
+ test/Spec.hs view
@@ -0,0 +1,1 @@+{-# OPTIONS_GHC -F -pgmF hspec-discover #-}