diff --git a/LICENSE b/LICENSE new file mode 100644 --- /dev/null +++ b/LICENSE @@ -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. diff --git a/README.md b/README.md new file mode 100644 --- /dev/null +++ b/README.md @@ -0,0 +1,147 @@ +# Ntha Programming Language + +[![Build Status](https://travis-ci.org/zjhmale/Ntha.svg?branch=master)](https://travis-ci.org/zjhmale/Ntha) +[![zjhmale](https://img.shields.io/badge/author-%40zjhmale-blue.svg)](https://github.com/zjhmale) +[![Haskell](https://img.shields.io/badge/language-haskell-red.svg)](https://en.wikipedia.org/wiki/Haskell_(programming_language)) +[![Hackage](https://img.shields.io/hackage/v/ntha.svg)](https://hackage.haskell.org/package/ntha) +[![Hackage-Deps](https://img.shields.io/hackage-deps/v/idrigen.svg)](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 + +![cleantha](http://i.imgur.com/i1BrztC.gif) + +## 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 [![license BSD](https://img.shields.io/badge/license-BSD-orange.svg)](https://en.wikipedia.org/wiki/BSD_licenses) diff --git a/Setup.hs b/Setup.hs new file mode 100644 --- /dev/null +++ b/Setup.hs @@ -0,0 +1,2 @@ +import Distribution.Simple +main = defaultMain diff --git a/app/Main.hs b/app/Main.hs new file mode 100644 --- /dev/null +++ b/app/Main.hs @@ -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) diff --git a/lib/std.ntha b/lib/std.ntha new file mode 100644 --- /dev/null +++ b/lib/std.ntha @@ -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")))) diff --git a/ntha.cabal b/ntha.cabal new file mode 100644 --- /dev/null +++ b/ntha.cabal @@ -0,0 +1,80 @@ +name: ntha +version: 0.1.0 +synopsis: A tiny statically typed functional programming language. +description: Check out 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 diff --git a/src/Ast.hs b/src/Ast.hs new file mode 100644 --- /dev/null +++ b/src/Ast.hs @@ -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 diff --git a/src/Eval.hs b/src/Eval.hs new file mode 100644 --- /dev/null +++ b/src/Eval.hs @@ -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 diff --git a/src/Infer.hs b/src/Infer.hs new file mode 100644 --- /dev/null +++ b/src/Infer.hs @@ -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 diff --git a/src/Lexer.x b/src/Lexer.x new file mode 100644 --- /dev/null +++ b/src/Lexer.x @@ -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 +} diff --git a/src/Parser.y b/src/Parser.y new file mode 100644 --- /dev/null +++ b/src/Parser.y @@ -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 +} diff --git a/src/Prologue.hs b/src/Prologue.hs new file mode 100644 --- /dev/null +++ b/src/Prologue.hs @@ -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))] diff --git a/src/Refined.hs b/src/Refined.hs new file mode 100644 --- /dev/null +++ b/src/Refined.hs @@ -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 () diff --git a/src/State.hs b/src/State.hs new file mode 100644 --- /dev/null +++ b/src/State.hs @@ -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 'α' diff --git a/src/Type.hs b/src/Type.hs new file mode 100644 --- /dev/null +++ b/src/Type.hs @@ -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 diff --git a/src/TypeScope.hs b/src/TypeScope.hs new file mode 100644 --- /dev/null +++ b/src/TypeScope.hs @@ -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 -> " -| " diff --git a/src/Value.hs b/src/Value.hs new file mode 100644 --- /dev/null +++ b/src/Value.hs @@ -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 _) = "" + 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 diff --git a/test/EvalSpec.hs b/test/EvalSpec.hs new file mode 100644 --- /dev/null +++ b/test/EvalSpec.hs @@ -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)] diff --git a/test/InferSpec.hs b/test/InferSpec.hs new file mode 100644 --- /dev/null +++ b/test/InferSpec.hs @@ -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")] diff --git a/test/ParserSpec.hs b/test/ParserSpec.hs new file mode 100644 --- /dev/null +++ b/test/ParserSpec.hs @@ -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]] diff --git a/test/Spec.hs b/test/Spec.hs new file mode 100644 --- /dev/null +++ b/test/Spec.hs @@ -0,0 +1,1 @@ +{-# OPTIONS_GHC -F -pgmF hspec-discover #-}