ntha 0.1.1 → 0.1.3
raw patch · 39 files changed
+2302/−2275 lines, 39 files
Files
- README.md +1/−1
- app/Main.hs +14/−9
- ntha.cabal +18/−17
- src/Ast.hs +0/−168
- src/Eval.hs +0/−228
- src/Infer.hs +0/−266
- src/Lexer.x +0/−110
- src/Ntha.hs +21/−0
- src/Ntha/Core/Ast.hs +168/−0
- src/Ntha/Core/Prologue.hs +82/−0
- src/Ntha/Parser/Lexer.x +110/−0
- src/Ntha/Parser/Parser.y +310/−0
- src/Ntha/Runtime/Eval.hs +228/−0
- src/Ntha/Runtime/Value.hs +151/−0
- src/Ntha/State.hs +38/−0
- src/Ntha/Type/Infer.hs +266/−0
- src/Ntha/Type/Refined.hs +139/−0
- src/Ntha/Type/Type.hs +287/−0
- src/Ntha/Type/TypeScope.hs +39/−0
- src/Ntha/Z3/Assertion.hs +63/−0
- src/Ntha/Z3/Class.hs +223/−0
- src/Ntha/Z3/Context.hs +61/−0
- src/Ntha/Z3/Encoding.hs +52/−0
- src/Ntha/Z3/Logic.hs +18/−0
- src/Parser.y +0/−310
- src/Prologue.hs +0/−82
- src/Refined.hs +0/−139
- src/State.hs +0/−38
- src/Type.hs +0/−287
- src/TypeScope.hs +0/−39
- src/Value.hs +0/−151
- src/Z3/Assertion.hs +0/−63
- src/Z3/Class.hs +0/−223
- src/Z3/Context.hs +0/−61
- src/Z3/Encoding.hs +0/−52
- src/Z3/Logic.hs +0/−18
- test/EvalSpec.hs +5/−5
- test/InferSpec.hs +5/−5
- test/ParserSpec.hs +3/−3
README.md view
@@ -22,7 +22,7 @@ * 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)).+* 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)), based on [z3-encoding](https://github.com/izgzhen/z3-encoding/tree/1d794c10db716ac9308e49bf4f5a115e14212f31) * Module system (still in early stage, lack of namespace control). * Support pattern matching on function parameters. * Lambdas and curried function by default.
app/Main.hs view
@@ -1,15 +1,20 @@ 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 Ntha(+ Expr(..),+ Type(..),+ ValueScope(..),+ Value(..),+ TypeScope(..),+ EPath,+ isImport,+ eval,+ analyze,+ checker,+ parseExpr,+ assumptions,+ builtins) import Control.Lens import Control.Monad (foldM) import Control.Monad.Trans
ntha.cabal view
@@ -1,5 +1,5 @@ name: ntha-version: 0.1.1+version: 0.1.3 synopsis: A tiny statically typed functional programming language. description: Check out <https://github.com/zjhmale/Ntha#readme the readme> for documentation. homepage: https://github.com/zjhmale/ntha@@ -21,22 +21,23 @@ library hs-source-dirs: src- exposed-modules: Ast- , Type- , TypeScope- , Value- , State- , Infer- , Eval- , Refined- , Prologue- , Lexer- , Parser- , Z3.Assertion- , Z3.Class- , Z3.Context- , Z3.Encoding- , Z3.Logic+ exposed-modules: Ntha.Core.Ast+ , Ntha.Core.Prologue+ , Ntha.Runtime.Eval+ , Ntha.Runtime.Value+ , Ntha.Type.Type+ , Ntha.Type.TypeScope+ , Ntha.Type.Refined+ , Ntha.Type.Infer+ , Ntha.State+ , Ntha.Parser.Lexer+ , Ntha.Parser.Parser+ , Ntha.Z3.Assertion+ , Ntha.Z3.Class+ , Ntha.Z3.Context+ , Ntha.Z3.Encoding+ , Ntha.Z3.Logic+ , Ntha build-depends: base >= 4.7 && < 5 , containers , pretty
− src/Ast.hs
@@ -1,168 +0,0 @@-module Ast where--import Type-import Data.Maybe (fromMaybe)-import Data.List (intercalate)-import qualified Data.Map as M-import qualified Text.PrettyPrint as PP--type EName = String -- variable name-type EPath = String-type EField = String-type EIndent = Int-type TypeVariable = Type -- just for documentation--data Expr = EVar EName- | EAccessor Expr EField- | ENum Int- | EStr String- | EChar Char- | EBool Bool- | EList [Expr]- | ETuple [Expr]- | ERecord (M.Map EField Expr)- | EUnit- | ELambda [Named] (Maybe Type) [Expr]- | EApp Expr Expr- | EIf Expr [Expr] [Expr]- | EPatternMatching Expr [Case]- | ELetBinding Pattern Expr [Expr]- | EDestructLetBinding Pattern [Pattern] [Expr]- | EDataDecl EName Type [TypeVariable] [TypeConstructor]- | ETypeSig EName Type -- explicit type annotation- | EImport EPath- | EProgram [Expr]- deriving (Eq, Ord)--isImport :: Expr -> Bool-isImport expr = case expr of- EImport _ -> True- _ -> False---- for do block desuger to bind-data Bind = Bind EName Expr- | Return Expr- | Single Expr---- for cond desuger to if-data Clause = Clause Expr Expr- | Else Expr--data TypeConstructor = TypeConstructor EName [Type]- deriving (Eq, Ord)--data Named = Named EName (Maybe Type)- deriving (Eq, Ord)--data Pattern = WildcardPattern- | IdPattern EName- | NumPattern Int- | BoolPattern Bool- | CharPattern Char- | TuplePattern [Pattern]- | TConPattern EName [Pattern]- deriving (Eq, Ord)--data Case = Case Pattern [Expr]- deriving (Eq, Ord)---- temp structure for parser-data EVConArg = EVCAVar EName- | EVCAOper EName [EName]- | EVCAList EVConArg- | EVCATuple [EVConArg]- deriving (Show, Eq, Ord)--data EVConstructor = EVConstructor EName [EVConArg]- deriving (Show, Eq, Ord)--substName :: M.Map EName EName -> Expr -> Expr-substName subrule (EVar name) = EVar $ fromMaybe name $ M.lookup name subrule-substName subrule (EAccessor expr field) = EAccessor (substName subrule expr) field-substName subrule (EList exprs) = EList $ map (substName subrule) exprs-substName subrule (ETuple exprs) = ETuple $ map (substName subrule) exprs-substName subrule (ERecord pairs) = ERecord $ M.map (substName subrule) pairs-substName subrule (ELambda nameds t exprs) = ELambda newNames t newExprs- where- newNames = map (\(Named name t') -> Named (fromMaybe name $ M.lookup name subrule) t') nameds- newExprs = map (substName subrule) exprs-substName subrule (EApp fn arg) = EApp (substName subrule fn) (substName subrule arg)-substName subrule (EIf cond thenInstrs elseInstrs) = EIf newCond newThenInstrs newElseInstrs- where- newCond = substName subrule cond- newThenInstrs = map (substName subrule) thenInstrs- newElseInstrs = map (substName subrule) elseInstrs-substName subrule (EPatternMatching expr cases) = EPatternMatching newExpr newCases- where- newCases = map (\(Case pat exprs) -> Case pat (map (substName subrule) exprs)) cases- newExpr = substName subrule expr-substName subrule (ELetBinding pat expr exprs) = ELetBinding pat (substName subrule expr) $ map (substName subrule) exprs-substName _ e = e--tab :: EIndent -> String-tab i = intercalate "" $ take i $ repeat "\t"--stringOfNamed :: Named -> String-stringOfNamed (Named name t) = name ++ case t of- Just t' -> ":" ++ show t'- Nothing -> ""--stringofNameds :: [Named] -> String-stringofNameds = unwords . (map stringOfNamed)--stringOfExpr :: Expr -> String-stringOfExpr e = case e of- EApp fn arg -> "<" ++ show fn ++ ">(" ++ show arg ++ ")"- ELambda params annoT body -> "λ" ++ stringofNameds params ++ (case annoT of- Just annoT' -> " : " ++ show annoT'- Nothing -> "") ++ " = \n" ++ intercalate "" (map (\instr -> "\t" ++ show instr ++ "\n") body)- EIf cond thenInstrs elseInstrs -> "if " ++ show cond ++ " then \n" ++ stringOfInstrs thenInstrs ++ "else \n" ++ stringOfInstrs elseInstrs where- stringOfInstrs instrs = intercalate "" $ map (\instr -> "\t" ++ show instr ++ "\n") instrs- EProgram instrs -> intercalate "" $ map (\instr -> show instr ++ "\n") instrs- _ -> reprOfExpr 0 e--stringOfCase :: EIndent -> Case -> String-stringOfCase i (Case pat outcomes) = "\n" ++ tab i ++ show pat ++ " ⇒ " ++ show outcomes--stringOfCases :: EIndent -> [Case] -> String-stringOfCases i cases = intercalate "" (map (stringOfCase i) cases)--reprOfExpr :: EIndent -> Expr -> String-reprOfExpr i e = case e of- EVar n -> tab i ++ n- EAccessor e' f -> tab i ++ reprOfExpr 0 e' ++ "." ++ f- ENum v -> tab i ++ show v- EStr v -> tab i ++ v- EChar v -> tab i ++ [v]- EBool v -> tab i ++ show v- EUnit -> tab i ++ "()"- EList es -> tab i ++ show es- ETuple es -> "(" ++ intercalate "," (map (reprOfExpr 0) es) ++ ")"- ERecord pairs -> "{" ++ intercalate "," (M.elems $ M.mapWithKey (\f v -> f ++ ": " ++ reprOfExpr 0 v) pairs) ++ "}"- EApp _ _ -> tab i ++ show e- ELambda params annoT body -> tab i ++ "λ" ++ stringofNameds params ++ (case annoT of- Just annoT' -> " : " ++ show annoT'- Nothing -> "") ++ " = \n" ++ intercalate "" (map (\instr -> "\t" ++ reprOfExpr (i + 1) instr ++ "\n") body)- EIf cond thenInstrs elseInstrs -> tab i ++ "if " ++ show cond ++ " then \n" ++ stringOfInstrs thenInstrs ++ tab i ++ "else \n" ++ stringOfInstrs elseInstrs where- stringOfInstrs instrs = intercalate "" $ map (\instr -> "\t" ++ reprOfExpr (i + 1) instr ++ "\n") instrs- EPatternMatching input cases -> tab i ++ "match " ++ show input ++ stringOfCases i cases- EDataDecl name _ tvars tcons -> tab i ++ "data " ++ name ++ " " ++ unwords (map show tvars) ++ " = " ++ intercalate " | " (map (\(TypeConstructor name' types) -> name' ++ case types of- [] -> ""- _ -> " " ++ unwords (map show types)) tcons)- EDestructLetBinding main args instrs -> tab i ++ "let " ++ show main ++ " " ++ unwords (map show args) ++ " = \n" ++ intercalate "" (map (\instr -> reprOfExpr (i + 1) instr ++ "\n") instrs)- ELetBinding main def body -> tab i ++ "let " ++ show main ++ " " ++ show def ++ " in " ++ intercalate "\n" (map show body)- ETypeSig name t -> tab i ++ "(" ++ name ++ " : " ++ show t ++ ")"- EImport path -> "import " ++ path- EProgram instrs -> intercalate "" $ map (\instr -> reprOfExpr i instr ++ "\n") instrs--instance Show Expr where- showsPrec _ x = shows $ PP.text $ stringOfExpr x--instance Show Pattern where- show WildcardPattern = "_"- show (NumPattern val) = "pint→" ++ show val- show (BoolPattern val) = "pbool→" ++ show val- show (CharPattern val) = "pchar→" ++ show val- show (IdPattern name) = "'" ++ name ++ "'"- show (TuplePattern pattens) = "(" ++ intercalate "," (map show pattens) ++ ")"- show (TConPattern name pattens) = name ++ " " ++ show pattens
− src/Eval.hs
@@ -1,228 +0,0 @@-module Eval where--import Ast-import Value-import Data.Maybe (fromMaybe)-import Prelude hiding (lookup)-import qualified Data.Map as M-import qualified Data.Set as S--type Exclude = S.Set EName--evalFn :: Value -> Value -> ValueScope -> Value-evalFn (Fn f) arg scope = f arg scope-evalFn _ _ _ = VUnit--chainingFn :: EName -> Value -> Value-chainingFn argName next = Fn (\oarg _ -> Fn (\arg scope -> let margs = case oarg of- FnApArgs pairs -> let v = fromMaybe VUnit $ M.lookup "***" pairs- in FnApArgs $ M.insert "***" arg $ M.insert argName v pairs- _ -> FnApArgs $ M.fromList [(argName, oarg), ("***", arg)]- in evalFn next margs scope))--chaininLastFn :: EName -> [Expr] -> Value-chaininLastFn argName body = Fn (\arg scope -> let scope' = case arg of- FnApArgs pairs -> foldl (\env (k, v) -> insert k v env)- scope- (M.toList $ M.insert argName (fromMaybe VUnit $ M.lookup "***" pairs) pairs)- _ -> insert argName arg scope- in snd $ foldl (\(env, val) instr -> val `seq` eval instr env) (scope', VUnit) body)--destrChainingFn :: Pattern -> Value -> Value-destrChainingFn pat next = Fn (\oarg _ -> Fn (\arg scope -> let margs = case oarg of- DestrFnApArgs args freeVal -> DestrFnApArgs (args ++ [PatVal pat freeVal]) arg- _ -> DestrFnApArgs [PatVal pat oarg] arg- in evalFn next margs scope))--destrChaininLastFn :: Pattern -> [Expr] -> Value-destrChaininLastFn pat body = Fn (\arg scope -> let scope' = case arg of- DestrFnApArgs args freeVal -> let s = foldl (\env (PatVal pat' val) -> define pat' val env)- scope args- in define pat freeVal s- _ -> define pat arg scope- in snd $ foldl (\(env, val) instr -> val `seq` eval instr env) (scope', VUnit) body)--tConChainingFn :: Tag -> Value -> Value-tConChainingFn tag next = Fn (\oarg _ -> Fn (\arg scope -> let targs = case oarg of- TConArgs args tag' -> TConArgs (args ++ [arg]) tag'- _ -> TConArgs [oarg, arg] tag- in evalFn next targs scope))--tConChaininLastFn :: Tag -> Value-tConChaininLastFn tag = Fn (\arg _ -> let args = case arg of- TConArgs args' _ -> args'- VUnit -> []- _ -> [arg]- in Adt tag args)--excludePatternBoundNames :: Pattern -> Exclude -> Exclude-excludePatternBoundNames pat excluded = case pat of- IdPattern name -> S.insert name excluded- TuplePattern pats -> foldl (\exc p -> excludePatternBoundNames p exc) excluded pats- TConPattern _ pats -> foldl (\exc p -> excludePatternBoundNames p exc) excluded pats- _ -> excluded--visit :: Expr -> ValueScope -> ValueEnv -> Exclude -> (ValueScope, ValueEnv, Exclude)-visit expr scope capturedEnv excluded = case expr of- EList values -> foldl (\(s, c, e) value -> visit value s c e)- (scope, capturedEnv, excluded) values- EIf cond thenInstrs elseInstrs -> (sco'', env'', exc'') where- (sco, env, exc) = visit cond scope capturedEnv excluded- (sco', env', exc') = foldl (\(s, c, e) value -> visit value s c e)- (sco, env, exc) thenInstrs- (sco'', env'', exc'') = foldl (\(s, c, e) value -> visit value s c e)- (sco', env', exc') elseInstrs- EVar name -> if name `notElem` excluded- then let (scope', val) = eval expr scope- in (scope', M.insert name val capturedEnv, excluded)- else (scope, capturedEnv, excluded)- EApp fn arg -> let (s, c, e) = visit fn scope capturedEnv excluded- in visit arg s c e- EDestructLetBinding main _ _ -> (scope, capturedEnv, excludePatternBoundNames main excluded)- EPatternMatching input cases -> let (scope', capturedEnv', excluded') = visit input scope capturedEnv excluded- in foldl (\(s, c, e) (Case pat outcomes) -> let e' = excludePatternBoundNames pat e- in let (s', c', _) = foldl (\(sco, env, exc) instr -> visit instr sco env exc)- (s, c, e') outcomes- in (s', c', e))- (scope', capturedEnv', excluded') cases- _ -> (scope, capturedEnv, excluded)--envCapturingFnWrapper :: Value -> Expr -> ValueScope -> Value-envCapturingFnWrapper fn expr scope = case expr of- (ELambda params _ instrs) -> mkFn capturedEnv where- excluded = foldl (\exc (Named name _) -> S.insert name exc) S.empty params- capturedEnv = mkCapturedEnv excluded instrs- (EDestructLetBinding (IdPattern name) args instrs) -> mkFn capturedEnv where- excluded = foldl (\exc pat -> excludePatternBoundNames pat exc) (S.singleton name) args- capturedEnv = mkCapturedEnv excluded instrs- _ -> VUnit- where- mkCapturedEnv excluded instrs = let (_, capturedEnv, _) = foldl (\(s, c, e) instr -> visit instr s c e)- (scope, M.empty, excluded) instrs- in capturedEnv- mkFn capturedEnv = Fn (\arg scope' -> let scope'' = foldl (\env (k, v) -> insert k v env)- scope' $ M.toList capturedEnv- in evalFn fn arg scope'')---- to predicate if a value is match specific pattern-match :: Value -> Pattern -> ValueScope -> (ValueScope, Bool)-match input pattern scope = case pattern of- WildcardPattern -> (scope, True)- IdPattern name -> (insert name input scope, True)- NumPattern val -> (scope, input == (VNum val))- BoolPattern val -> (scope, input == (VBool val))- CharPattern val -> (scope, input == (VChar val))- TuplePattern pats -> case input of- VTuple items -> if length items /= length pats- then (scope, False)- else isAllMatch items pats- _ -> (scope, False)- TConPattern name pats -> case input of- Adt tag args -> if name == tag && length pats == length args- then isAllMatch args pats- else (scope, False)- _ -> (scope, False)- where- isAllMatch items pats = let (scope', isMatchs) = foldl (\(env, matchs) (item, pat) -> let (env', isMatch) = match item pat env- in (env', matchs ++ [isMatch]))- (scope, []) $ zip items pats- in (scope', all id isMatchs)--define :: Pattern -> Value -> ValueScope -> ValueScope-define pattern val scope = case pattern of- IdPattern name -> insert name val scope- TuplePattern pats -> case val of- VTuple items -> defineVals pats items- _ -> error $ "Invalid value " ++ show val ++ " for pattern " ++ show pattern- -- maybe should check pattern name and length of pats and args just like the match function above- TConPattern _ pats -> case val of- Adt _ args -> defineVals pats args- _ -> error $ "Invalid value " ++ show val ++ " for pattern " ++ show pattern- _ -> scope- where- defineVals pats items = foldl (\env (pat, item) -> define pat item env)- scope $ zip pats items--eval :: Expr -> ValueScope -> (ValueScope, Value)-eval expr scope = case expr of- ENum v -> (scope, VNum v)- EBool v -> (scope, VBool v)- EChar v -> (scope, VChar v)- EStr v -> (scope, makeList $ map VChar v)- EUnit -> (scope, VUnit)- EVar name -> case lookup name scope of- Just val -> (scope, val)- Nothing -> error $ "Unknown identifier " ++ show expr- EAccessor obj field -> case eval obj scope of- (_, VRecord pairs) -> case M.lookup field pairs of- Just val -> (scope, val)- Nothing -> error $ "No field " ++ field ++ "in "++ show obj- _ -> error $ "Not a record " ++ show obj- ETuple values -> (scope, VTuple $ map (\v -> snd (eval v scope)) values)- EList values -> (scope, makeList $ map (\v -> snd (eval v scope)) values)- ERecord pairs -> (scope, VRecord $ M.map (\v -> snd (eval v scope)) pairs)- ELambda params _ instrs -> let fnV = case reverse params of- (Named name _):xs -> fnChain where- lastFn = chaininLastFn name instrs- fnChain = foldl (\fn (Named n _) -> chainingFn n fn) lastFn xs- _ -> VUnit- in (scope, envCapturingFnWrapper fnV expr scope)- EApp fn arg -> case fnV of- Fn f -> let (_, argV) = eval arg scope'- in (scope, f argV scope')- Adt _ _ -> case eval arg scope' of- (_, VUnit) -> (scope, fnV)- _ -> error $ "Error while evaluating " ++ show expr ++ ": " ++ show fnV ++ " constructor doesn't take arguments"- _ -> error $ "Error while evaluating " ++ show expr ++ ": " ++ show fnV ++ " is not a function"- where- scope' = child scope- (_, fnV) = eval fn scope'- EIf cond thenInstrs elseInstrs -> let (_, condV) = eval cond scope- in case condV of- VBool v -> if v- then (scope, evalInstrs thenInstrs)- else (scope, evalInstrs elseInstrs)- where- evalInstrs instrs = let scope' = child scope- in snd $ foldl (\(env, val) instr -> val `seq` eval instr env) (scope', VUnit) instrs- _ -> error $ "Error while evaluating " ++ show expr ++ ": the condition is not a boolean"- EPatternMatching input cases -> findPattern inputV cases- where (_, inputV) = eval input scope- findPattern :: Value -> [Case] -> (ValueScope, Value)- findPattern val [] = error $ "Match exception: " ++ show input ++ " = " ++ show val ++ " didn't match any case of " ++ show expr- findPattern val ((Case pat instrs):cs) = let (scope', isMatch) = match val pat $ child scope- in if isMatch- then (scope, snd $ foldl (\(env, val') instr -> val' `seq` eval instr env) (scope', VUnit) instrs)- else findPattern val cs- ELetBinding name def body -> let (scope', _) = eval (EDestructLetBinding name [] [def]) scope- in (scope, snd $ foldl (\(env, val) instr -> val `seq` eval instr env) (scope', VUnit) body)- EDestructLetBinding main args instrs -> if length args == 0- -- define variable- then let (_, val) = foldl (\(env, val') instr -> val' `seq` eval instr env) (child scope, VUnit) instrs- in (define main val scope, val)- -- define function- else case main of- IdPattern name -> let fnV = case reverse args of- pat:pats -> fnChain where- lastFn = destrChaininLastFn pat instrs- fnChain = foldl (\fn p -> destrChainingFn p fn) lastFn pats- _ -> VUnit- in let fn = envCapturingFnWrapper fnV expr scope- in (insert name fn scope, fn)- _ -> error $ "Function name can only be a name, whereas a pattern " ++ show main ++ " was provided in " ++ show expr- EDataDecl _ _ _ typeConstructors -> let scope' = foldl makeChain scope typeConstructors- in (scope', VUnit)- where- makeChain env (TypeConstructor name types) = let fnV = case reverse types of- _:ts -> fnChain where- lastFn = tConChaininLastFn name- fnChain = foldl (\fn _ -> tConChainingFn name fn)- lastFn ts- _ -> VUnit- in if fnV == VUnit- then insert name (Adt name []) env- else insert name fnV env- ETypeSig _ _ -> (scope, VUnit)- EProgram instrs -> foldl (\(env, val) instr -> val `seq` eval instr env)- (child scope, VUnit) instrs- _ -> error $ "not support eval expr: " ++ show expr
− src/Infer.hs
@@ -1,266 +0,0 @@-module Infer where--import Ast-import Type-import TypeScope-import State-import Data.IORef-import Control.Monad (when, zipWithM_, foldM, forM_)-import Control.Monad.Loops (anyM)-import qualified Data.Map as M-import qualified Data.Set as S-import Prelude hiding (lookup)--type NonGeneric = (S.Set Type)--occursInType :: Type -> Type -> Infer Bool-occursInType v t = do- tP <- prune t- case tP of- TOper _ ts -> occursIn v ts- v' -> return $ v == v'--occursIn :: Type -> [Type] -> Infer Bool-occursIn t = anyM (occursInType t)--isGeneric :: Type -> NonGeneric -> Infer Bool-isGeneric t nonGeneric = not <$> (occursIn t $ S.toList nonGeneric)--fresh :: Type -> NonGeneric -> Infer Type-fresh t nonGeneric = do- mappings <- newIORef M.empty -- A mapping of TypeVariables to TypeVariables- let freshrec ty = prune ty >>= (\tyP -> case tyP of- TVar _ _ _ -> do- isG <- isGeneric tyP nonGeneric- if isG- then do- m <- readIORef mappings- case M.lookup tyP m of- Just tVar -> return tVar- Nothing -> do- newVar <- makeVariable- modifyIORef mappings $ M.insert tyP newVar- return newVar- else return tyP- TOper name types -> do- newTypes <- mapM freshrec types- return $ TOper name newTypes- TCon name types dataType -> do- newTypes <- mapM freshrec types- newDataType <- freshrec dataType- return $ TCon name newTypes newDataType- TRecord valueTypes -> do- newValueTypes <- foldM (\acc (k, v) -> do- fv <- freshrec v- return $ M.insert k fv acc)- M.empty $ M.toList valueTypes- return $ TRecord newValueTypes- _ -> return tyP)- freshrec t--getType :: TName -> TypeScope -> NonGeneric -> Infer Type-getType name scope nonGeneric = case lookup name scope of- Just var -> fresh var nonGeneric- Nothing -> error $ "Undefined symbol " ++ name--adjustType :: Type -> Type-adjustType t = case t of- TCon _ types dataType -> functionT types dataType- _ -> t--unify :: Type -> Type -> Infer ()-unify t1 t2 = do- t1P <- prune t1- t2P <- prune t2- let t1PA = adjustType t1P- let t2PA = adjustType t2P- case (t1PA, t2PA) of- (a@(TVar _ inst _), b) -> when (a /= b) $ do- isOccurs <- occursInType a b- when isOccurs $ error "Recusive unification"- writeIORef inst $ Just b- (a@(TOper _ _), b@(TVar _ _ _)) -> unify b a- (a@(TOper name1 types1), b@(TOper name2 types2)) -> if name1 /= name2 || (length types1) /= (length types2)- then error $ "Type mismatch " ++ show a ++ " ≠ " ++ show b- else zipWithM_ unify types1 types2- (a@(TRecord types1), b@(TRecord types2)) -> mapM_ (\(k, t2') -> do- case M.lookup k types1 of- Just t1' -> unify t2' t1'- Nothing -> error $ "Cannot unify, no field " ++ k ++ " " ++ show a ++ ", " ++ show b)- $ M.toList types2- _ -> error $ "Can not unify " ++ show t1 ++ ", " ++ show t2--visitPattern :: Pattern -> TypeScope -> NonGeneric -> Infer (TypeScope, NonGeneric, Type)-visitPattern pattern scope nonGeneric = case pattern of- WildcardPattern -> do- resT <- makeVariable- return (scope, nonGeneric, resT)- IdPattern name -> do- resT <- makeVariable- return (insert name resT scope, S.insert resT nonGeneric, resT)- NumPattern _ -> return (scope, nonGeneric, intT)- BoolPattern _ -> return (scope, nonGeneric, boolT)- CharPattern _ -> return (scope, nonGeneric, charT)- TuplePattern items -> do- (itemTypes, newScope, newNonGeneric) <- foldM (\(types, env, nonGen) item -> do- (newEnv, newNonGen, itemT) <- visitPattern item env nonGen- return (types ++ [itemT], newEnv, newNonGen))- ([], scope, nonGeneric) items- return (newScope, newNonGeneric, productT itemTypes)- TConPattern name patterns -> do- (patTypes, newScope, newNonGeneric) <- foldM (\(types, env, nonGen) pat -> do- (newEnv, newNonGen, patT) <- visitPattern pat env nonGen- return (types ++ [patT], newEnv, newNonGen))- ([], scope, nonGeneric) patterns- case lookup name newScope of- Nothing -> error $ "Unknow type constructor " ++ name- Just tconT -> case tconT of- TCon _ _ _ -> do- (TCon _ types dataType) <- fresh tconT newNonGeneric- if (length patterns) /= (length types)- then error $ "Bad arity: case " ++ show pattern ++ " provided " ++ (show . length) patterns ++ " arguments whereas " ++ name ++ " takes " ++ (show . length) types- else do- zipWithM_ unify patTypes types- return (newScope, newNonGeneric, dataType)- _ -> error $ "Invalid type constructor " ++ name--definePattern :: Pattern -> Type -> TypeScope -> Infer TypeScope-definePattern pattern t scope = do- tP <- prune t- case pattern of- IdPattern name -> return $ insert name tP scope- TuplePattern items -> case tP of- TOper _ types -> do- newScope <- foldM (\env (pat, patT) -> do- newEnv <- definePattern pat patT env- return newEnv)- scope $ zip items types- return newScope- _ -> error $ "Invalid type " ++ show tP ++ " for pattern " ++ show pattern- TConPattern _ patterns -> case tP of- -- t is always functionT for now so a little non-sense for this case.- TCon _ types _ -> do- newScope <- foldM (\env (pat, patT) -> do- newEnv <- definePattern pat patT env- return newEnv)- scope $ zip patterns types- return newScope- TOper _ types -> do- newScope <- foldM (\env (pat, patT) -> do- newEnv <- definePattern pat patT env- return newEnv)- scope $ zip patterns types- return newScope- _ -> error $ "Invalid type " ++ show tP ++ " for pattern " ++ show pattern- _ -> return scope--analyze :: Expr -> TypeScope -> NonGeneric -> Infer (TypeScope, Type)-analyze expr scope nonGeneric = case expr of- ENum _ -> return (scope, intT)- EBool _ -> return (scope, boolT)- EChar _ -> return (scope, charT)- EStr _ -> return (scope, strT)- EUnit -> return (scope, unitT)- EList exprs -> do- valueT <- makeVariable- -- type checking procedure, since types of elems in a list should be the same.- forM_ exprs (\e -> do- (_, eT) <- analyze e scope nonGeneric- unify valueT eT)- return (scope, listT valueT)- ETuple exprs -> do- types <- foldM (\types expr' -> do- (_, ty) <- analyze expr' scope nonGeneric- return $ types ++ [ty])- [] exprs- return (scope, productT types)- ERecord pairs -> do- valueTypes <- foldM (\vts (k, v) -> do- (_, t) <- analyze v scope nonGeneric- return $ M.insert k t vts)- M.empty $ M.toList pairs- return (scope, TRecord valueTypes)- EVar name -> (scope,) <$> getType name scope nonGeneric- EApp fn arg -> do- (_, fnT) <- analyze fn scope nonGeneric- (_, argT) <- analyze arg scope nonGeneric- rtnT <- makeVariable- unify (functionT [argT] rtnT) fnT- return (scope, rtnT)- ELambda params annoT instructions -> do- let newScope = child scope- (paramTypes, newScope', newNonGeneric) <- foldM (\(types', env', nonGeneric') (Named name t) ->- case t of- Just t' -> return (types' ++ [t'], insert name t' env', S.insert t' nonGeneric')- Nothing -> do- t' <- makeVariable- return (types' ++ [t'], insert name t' env', S.insert t' nonGeneric'))- ([], newScope, nonGeneric) params- rtnT <- foldM (\_ instr -> snd <$> analyze instr newScope' newNonGeneric) unitT instructions- case annoT of- Just annoT' -> unify rtnT annoT' -- type propagation from return type to param type- Nothing -> return ()- -- use fresh just to make sure sequence of lambda abstractions with same type var name could work well e.g.- -- ((λ(x: α) : α → x) 3)- -- ((λ(x: α) : α → x) true)- (scope,) <$> fresh (functionT paramTypes rtnT) nonGeneric- EAccessor obj field -> do- (_, objT) <- analyze obj scope nonGeneric- fieldT <- makeVariable- let desiredT = TRecord $ M.fromList [(field, fieldT)]- unify objT desiredT- return (scope, fieldT)- EIf cond thenInstructions elseInstructions -> do- (_, condT) <- analyze cond scope nonGeneric- unify condT boolT- (newScope, thenT) <- foldM (\(env, _) instr -> analyze instr env nonGeneric)- (scope, unitT) thenInstructions- (newScope', elseT) <- foldM (\(env, _) instr -> analyze instr env nonGeneric)- (newScope, unitT) elseInstructions- unify thenT elseT- return (newScope', thenT)- ELetBinding main def body -> do- (scope', _) <- analyze (EDestructLetBinding main [] [def]) scope nonGeneric- foldM (\(env, _) instr -> analyze instr env nonGeneric) (scope', unitT) body- EDestructLetBinding main args instructions -> do- let name = case main of- IdPattern n -> n ++ "-sig"- _ -> ""- let typeSig = lookup name scope- let newScope = child scope- (newScope', newNonGeneric, letTV) <- visitPattern main newScope nonGeneric- let newNonGeneric' = S.insert letTV newNonGeneric- (argTypes, newScope'', newNonGeneric'') <- foldM (\(types, env, nonGen) arg -> do- (newEnv, newNonGen, argT) <- visitPattern arg env nonGen- return (types ++ [argT], newEnv, newNonGen))- ([], newScope', newNonGeneric') args- rtnT <- foldM (\_ instr -> snd <$> analyze instr newScope'' newNonGeneric'') unitT instructions- let letT = functionT argTypes rtnT- newScope''' <- definePattern main letT newScope''- case typeSig of- Just (TSig ta) -> do- let ta' = extractType ta- unify ta' letT- _ -> return ()- return (newScope''', letT)- EDataDecl _ t _ tconstructors -> do- let newScope = foldl (\env (TypeConstructor conName conTypes) ->- insert conName (TCon conName conTypes t) env)- scope tconstructors- return (newScope, t)- EPatternMatching input cases -> do- (_, inputT) <- analyze input scope nonGeneric- resT <- makeVariable- resT' <- foldM (\rt (Case pat outcomes) -> do- let newScope = child scope- (newScope', newNonGeneric, patT) <- visitPattern pat newScope nonGeneric- unify patT inputT- (_, caseT) <- foldM (\(env, _) outcome -> analyze outcome env newNonGeneric)- (newScope', unitT) outcomes- unify caseT rt- return rt)- resT cases- return (scope, resT')- ETypeSig name t -> return (insert (name ++ "-sig") (TSig t) scope, unitT)- EProgram instructions -> foldM (\(env, _) instr -> analyze instr env nonGeneric) (scope, unitT) instructions- _ -> error $ "not support infer expr: " ++ show expr
− src/Lexer.x
@@ -1,110 +0,0 @@-{-module Lexer where-import Ast (EName)-import Data.Char (toUpper)-}--%wrapper "basic"--$upper = [A-Z]-$lower = [a-z]-$greek = [α-ω]-$digit = [0-9]-$operator = [\+\-\*\/\%\=\>\<\∧\∨\¬\?\'\~\!\.]-$chars = [$lower $upper $digit $operator $greek]-$eol = [\n]--tokens :-- $eol ;- $white+ ;- ";;".* ; --comments- -- TODO support multiline comments- "data" { \_ -> DATA }- "match" { \_ -> MATCH }- "begin" { \_ -> BEGIN }- "type" { \_ -> TYPE }- "if" { \_ -> IF }- "cond" { \_ -> COND }- "else" { \_ -> ELSE }- "monad" { \_ -> MONAD }- "do" { \_ -> DO }- "return" { \_ -> RETURN }- "ƒ" | "fun" { \_ -> DEFUN }- "λ" | "lambda" { \_ -> LAMBDA }- "⇒" | "=>" | "→" | "->" { \_ -> RARROW }- "⇐" | "<=" | "←" | "<-" { \_ -> LARROW }- "[" { \_ -> LBRACKET }- "]" { \_ -> RBRACKET }- "(" { \_ -> LPAREN }- ")" { \_ -> RPAREN }- "{" { \_ -> LBRACE }- "}" { \_ -> RBRACE }- "_" { \_ -> WILDCARD }- "." { \_ -> DOT }- ":" $chars+ { \s -> KEYWORD (tail s) }- ":" { \_ -> COLON }- "∷" | "::" { \_ -> DOUBLECOLON }- "|" { \_ -> BAR }- "let" { \_ -> LET }- "Z" { \_ -> NUMBERT }- "B" { \_ -> BOOLT }- "C" { \_ -> CHART }- "S" { \_ -> STRT }- "×" { \_ -> PRODUCT }- "import" { \_ -> IMPORT }- "true" | "false" { \s -> BOOLEAN (read ([toUpper (s!!0)] ++ tail s)) }- $upper $chars* { \s -> CON s }- $lower $chars* { \s -> VAR s }- $greek { \s -> TVAR (s!!0) }- \"[^\"]*\" { \s -> STRING ((tail . init) s) }- '[^'\"]{1}' { \s -> CHAR ((head . tail . init) s) }- $operator | "≠" | "≤" | "≥" { \s -> OPERATOR s }- $digit+ { \s -> NUMBER (read s) }- "-" $digit+ { \s -> NUMBER (read s) }--{-data Token = DATA- | MATCH- | BEGIN- | TYPE- | DEFUN- | LAMBDA- | MONAD- | DO- | RETURN- | IF- | COND- | ELSE- | RARROW- | LARROW- | LBRACKET- | RBRACKET- | LPAREN- | RPAREN- | LBRACE- | RBRACE- | WILDCARD- | DOT- | COLON- | DOUBLECOLON- | BAR- | VAR EName- | TVAR Char- | CON EName -- constructor names or uppercase symbols- | LET- | NUMBERT- | BOOLT- | CHART- | STRT- | PRODUCT- | IMPORT- | KEYWORD String- | OPERATOR String- | BOOLEAN Bool- | NUMBER Int- | STRING String- | CHAR Char- deriving(Eq, Show)--scanTokens = alexScanTokens-}
+ src/Ntha.hs view
@@ -0,0 +1,21 @@+module Ntha+ ( module Ntha.Core.Ast+ , module Ntha.Runtime.Value+ , module Ntha.Type.Type+ , module Ntha.Type.TypeScope+ , module Ntha.Type.Refined+ , module Ntha.Runtime.Eval+ , module Ntha.Type.Infer+ , module Ntha.Core.Prologue+ , module Ntha.Parser.Parser+ ) where++import Ntha.Core.Ast+import Ntha.Runtime.Value(ValueScope(..), Value(..))+import Ntha.Type.Type+import Ntha.Type.TypeScope+import Ntha.Type.Refined+import Ntha.Runtime.Eval+import Ntha.Type.Infer+import Ntha.Core.Prologue+import Ntha.Parser.Parser
+ src/Ntha/Core/Ast.hs view
@@ -0,0 +1,168 @@+module Ntha.Core.Ast where++import Ntha.Type.Type+import Data.Maybe (fromMaybe)+import Data.List (intercalate)+import qualified Data.Map as M+import qualified Text.PrettyPrint as PP++type EName = String -- variable name+type EPath = String+type EField = String+type EIndent = Int+type TypeVariable = Type -- just for documentation++data Expr = EVar EName+ | EAccessor Expr EField+ | ENum Int+ | EStr String+ | EChar Char+ | EBool Bool+ | EList [Expr]+ | ETuple [Expr]+ | ERecord (M.Map EField Expr)+ | EUnit+ | ELambda [Named] (Maybe Type) [Expr]+ | EApp Expr Expr+ | EIf Expr [Expr] [Expr]+ | EPatternMatching Expr [Case]+ | ELetBinding Pattern Expr [Expr]+ | EDestructLetBinding Pattern [Pattern] [Expr]+ | EDataDecl EName Type [TypeVariable] [TypeConstructor]+ | ETypeSig EName Type -- explicit type annotation+ | EImport EPath+ | EProgram [Expr]+ deriving (Eq, Ord)++isImport :: Expr -> Bool+isImport expr = case expr of+ EImport _ -> True+ _ -> False++-- for do block desuger to bind+data Bind = Bind EName Expr+ | Return Expr+ | Single Expr++-- for cond desuger to if+data Clause = Clause Expr Expr+ | Else Expr++data TypeConstructor = TypeConstructor EName [Type]+ deriving (Eq, Ord)++data Named = Named EName (Maybe Type)+ deriving (Eq, Ord)++data Pattern = WildcardPattern+ | IdPattern EName+ | NumPattern Int+ | BoolPattern Bool+ | CharPattern Char+ | TuplePattern [Pattern]+ | TConPattern EName [Pattern]+ deriving (Eq, Ord)++data Case = Case Pattern [Expr]+ deriving (Eq, Ord)++-- temp structure for parser+data EVConArg = EVCAVar EName+ | EVCAOper EName [EName]+ | EVCAList EVConArg+ | EVCATuple [EVConArg]+ deriving (Show, Eq, Ord)++data EVConstructor = EVConstructor EName [EVConArg]+ deriving (Show, Eq, Ord)++substName :: M.Map EName EName -> Expr -> Expr+substName subrule (EVar name) = EVar $ fromMaybe name $ M.lookup name subrule+substName subrule (EAccessor expr field) = EAccessor (substName subrule expr) field+substName subrule (EList exprs) = EList $ map (substName subrule) exprs+substName subrule (ETuple exprs) = ETuple $ map (substName subrule) exprs+substName subrule (ERecord pairs) = ERecord $ M.map (substName subrule) pairs+substName subrule (ELambda nameds t exprs) = ELambda newNames t newExprs+ where+ newNames = map (\(Named name t') -> Named (fromMaybe name $ M.lookup name subrule) t') nameds+ newExprs = map (substName subrule) exprs+substName subrule (EApp fn arg) = EApp (substName subrule fn) (substName subrule arg)+substName subrule (EIf cond thenInstrs elseInstrs) = EIf newCond newThenInstrs newElseInstrs+ where+ newCond = substName subrule cond+ newThenInstrs = map (substName subrule) thenInstrs+ newElseInstrs = map (substName subrule) elseInstrs+substName subrule (EPatternMatching expr cases) = EPatternMatching newExpr newCases+ where+ newCases = map (\(Case pat exprs) -> Case pat (map (substName subrule) exprs)) cases+ newExpr = substName subrule expr+substName subrule (ELetBinding pat expr exprs) = ELetBinding pat (substName subrule expr) $ map (substName subrule) exprs+substName _ e = e++tab :: EIndent -> String+tab i = intercalate "" $ take i $ repeat "\t"++stringOfNamed :: Named -> String+stringOfNamed (Named name t) = name ++ case t of+ Just t' -> ":" ++ show t'+ Nothing -> ""++stringofNameds :: [Named] -> String+stringofNameds = unwords . (map stringOfNamed)++stringOfExpr :: Expr -> String+stringOfExpr e = case e of+ EApp fn arg -> "<" ++ show fn ++ ">(" ++ show arg ++ ")"+ ELambda params annoT body -> "λ" ++ stringofNameds params ++ (case annoT of+ Just annoT' -> " : " ++ show annoT'+ Nothing -> "") ++ " = \n" ++ intercalate "" (map (\instr -> "\t" ++ show instr ++ "\n") body)+ EIf cond thenInstrs elseInstrs -> "if " ++ show cond ++ " then \n" ++ stringOfInstrs thenInstrs ++ "else \n" ++ stringOfInstrs elseInstrs where+ stringOfInstrs instrs = intercalate "" $ map (\instr -> "\t" ++ show instr ++ "\n") instrs+ EProgram instrs -> intercalate "" $ map (\instr -> show instr ++ "\n") instrs+ _ -> reprOfExpr 0 e++stringOfCase :: EIndent -> Case -> String+stringOfCase i (Case pat outcomes) = "\n" ++ tab i ++ show pat ++ " ⇒ " ++ show outcomes++stringOfCases :: EIndent -> [Case] -> String+stringOfCases i cases = intercalate "" (map (stringOfCase i) cases)++reprOfExpr :: EIndent -> Expr -> String+reprOfExpr i e = case e of+ EVar n -> tab i ++ n+ EAccessor e' f -> tab i ++ reprOfExpr 0 e' ++ "." ++ f+ ENum v -> tab i ++ show v+ EStr v -> tab i ++ v+ EChar v -> tab i ++ [v]+ EBool v -> tab i ++ show v+ EUnit -> tab i ++ "()"+ EList es -> tab i ++ show es+ ETuple es -> "(" ++ intercalate "," (map (reprOfExpr 0) es) ++ ")"+ ERecord pairs -> "{" ++ intercalate "," (M.elems $ M.mapWithKey (\f v -> f ++ ": " ++ reprOfExpr 0 v) pairs) ++ "}"+ EApp _ _ -> tab i ++ show e+ ELambda params annoT body -> tab i ++ "λ" ++ stringofNameds params ++ (case annoT of+ Just annoT' -> " : " ++ show annoT'+ Nothing -> "") ++ " = \n" ++ intercalate "" (map (\instr -> "\t" ++ reprOfExpr (i + 1) instr ++ "\n") body)+ EIf cond thenInstrs elseInstrs -> tab i ++ "if " ++ show cond ++ " then \n" ++ stringOfInstrs thenInstrs ++ tab i ++ "else \n" ++ stringOfInstrs elseInstrs where+ stringOfInstrs instrs = intercalate "" $ map (\instr -> "\t" ++ reprOfExpr (i + 1) instr ++ "\n") instrs+ EPatternMatching input cases -> tab i ++ "match " ++ show input ++ stringOfCases i cases+ EDataDecl name _ tvars tcons -> tab i ++ "data " ++ name ++ " " ++ unwords (map show tvars) ++ " = " ++ intercalate " | " (map (\(TypeConstructor name' types) -> name' ++ case types of+ [] -> ""+ _ -> " " ++ unwords (map show types)) tcons)+ EDestructLetBinding main args instrs -> tab i ++ "let " ++ show main ++ " " ++ unwords (map show args) ++ " = \n" ++ intercalate "" (map (\instr -> reprOfExpr (i + 1) instr ++ "\n") instrs)+ ELetBinding main def body -> tab i ++ "let " ++ show main ++ " " ++ show def ++ " in " ++ intercalate "\n" (map show body)+ ETypeSig name t -> tab i ++ "(" ++ name ++ " : " ++ show t ++ ")"+ EImport path -> "import " ++ path+ EProgram instrs -> intercalate "" $ map (\instr -> reprOfExpr i instr ++ "\n") instrs++instance Show Expr where+ showsPrec _ x = shows $ PP.text $ stringOfExpr x++instance Show Pattern where+ show WildcardPattern = "_"+ show (NumPattern val) = "pint→" ++ show val+ show (BoolPattern val) = "pbool→" ++ show val+ show (CharPattern val) = "pchar→" ++ show val+ show (IdPattern name) = "'" ++ name ++ "'"+ show (TuplePattern pattens) = "(" ++ intercalate "," (map show pattens) ++ ")"+ show (TConPattern name pattens) = name ++ " " ++ show pattens
+ src/Ntha/Core/Prologue.hs view
@@ -0,0 +1,82 @@+module Ntha.Core.Prologue where++import Ntha.State+import Ntha.Core.Ast+import Ntha.Runtime.Value+import Ntha.Type.Type+import Ntha.Type.TypeScope+import Debug.Trace+import qualified Data.Map as M++mkTCon :: TypeConstructor -> Expr -> Type+mkTCon (TypeConstructor name types) (EDataDecl _ t _ _) = TCon name types t+mkTCon _ _ = error "not support"++assumptions :: Infer TypeScope+assumptions = do+ tvarA <- makeVariable+ tvarB <- makeVariable+ let name = "List"+ let vars = [tvarA]+ let dataType = TOper name vars+ let consConstructor = TypeConstructor "Cons" [tvarA, TOper "List" [tvarA]]+ let nilConstructor = TypeConstructor "Nil" []+ let listData = EDataDecl "List" dataType vars [consConstructor, nilConstructor]+ return $ TypeScope Nothing $ M.fromList [("+", functionT [intT, intT] intT),+ ("-", functionT [intT, intT] intT),+ ("*", functionT [intT, intT] intT),+ ("/", functionT [intT, intT] intT),+ ("%", functionT [intT, intT] intT),+ ("=", functionT [tvarB, tvarB] boolT),+ ("≠", functionT [tvarB, tvarB] boolT),+ ("<", functionT [intT, intT] boolT),+ (">", functionT [intT, intT] boolT),+ ("≤", functionT [intT, intT] boolT),+ ("≥", functionT [intT, intT] boolT),+ ("∧", functionT [boolT, boolT] boolT),+ ("∨", functionT [boolT, boolT] boolT),+ ("¬", functionT [boolT] boolT),+ ("int2str", functionT [intT] strT),+ ("bool2str", functionT [boolT] strT),+ ("asserteq", functionT [tvarB, tvarB] unitT),+ ("print", functionT [strT] unitT),+ ("error", functionT [strT] tvarB),+ ("reverse", functionT [listT tvarB] (listT tvarB)),+ ("list?", functionT [tvarB] boolT),+ ("string?", functionT [tvarB] boolT),+ ("Cons", mkTCon consConstructor listData),+ ("Nil", mkTCon nilConstructor listData),+ ("inc", functionT [intT] intT),+ ("dec", functionT [intT] intT)]++builtins :: ValueScope+builtins = ValueScope Nothing $ M.fromList [("+", binFn (\(VNum a) (VNum b) -> (VNum $ a + b))),+ ("-", binFn (\(VNum a) (VNum b) -> (VNum $ a - b))),+ ("*", binFn (\(VNum a) (VNum b) -> (VNum $ a * b))),+ ("/", binFn (\(VNum a) (VNum b) -> (VNum $ a `div` b))),+ ("%", binFn (\(VNum a) (VNum b) -> (VNum $ a `mod` b))),+ ("=", binFn (\a b -> VBool $ a == b)),+ ("≠", binFn (\a b -> VBool $ a /= b)),+ ("<", binFn (\a b -> VBool $ a < b)),+ (">", binFn (\a b -> VBool $ a > b)),+ ("≤", binFn (\a b -> VBool $ a <= b)),+ ("≥", binFn (\a b -> VBool $ a >= b)),+ ("∧", binFn (\(VBool a) (VBool b) -> VBool $ a && b)),+ ("∨", binFn (\(VBool a) (VBool b) -> VBool $ a || b)),+ ("¬", Fn (\(VBool b) _ -> VBool $ not b)),+ ("int2str", Fn (\(VNum n) _ -> strV $ show n)),+ ("bool2str", Fn (\(VBool b) _ -> strV $ show b)),+ ("asserteq", binFn (\a b -> if a == b+ then VUnit+ else error $ show a ++ " and " ++ show b ++ " not equal.")),+ ("print", Fn (\v _ -> trace (desugerStrV v) VUnit)),+ ("error", Fn (\v _ -> error $ desugerStrV v)),+ ("reverse", Fn (\v _ -> reverseList v)),+ ("list?", Fn (\v _ -> case v of+ Adt "Cons" _ -> VBool True+ _ -> VBool False)),+ ("string?", Fn (\v _ -> VBool $ isString v)),+ ("Cons", binFn (\a b -> cons a b)),+ ("Nil", nil),+ ("inc", Fn (\(VNum n) _ -> VNum $ n + 1)),+ ("dec", Fn (\(VNum n) _ -> VNum $ n - 1))]
+ src/Ntha/Parser/Lexer.x view
@@ -0,0 +1,110 @@+{+module Ntha.Parser.Lexer where+import Ntha.Core.Ast (EName)+import Data.Char (toUpper)+}++%wrapper "basic"++$upper = [A-Z]+$lower = [a-z]+$greek = [α-ω]+$digit = [0-9]+$operator = [\+\-\*\/\%\=\>\<\∧\∨\¬\?\'\~\!\.]+$chars = [$lower $upper $digit $operator $greek]+$eol = [\n]++tokens :-+ $eol ;+ $white+ ;+ ";;".* ; --comments+ -- TODO support multiline comments+ "data" { \_ -> DATA }+ "match" { \_ -> MATCH }+ "begin" { \_ -> BEGIN }+ "type" { \_ -> TYPE }+ "if" { \_ -> IF }+ "cond" { \_ -> COND }+ "else" { \_ -> ELSE }+ "monad" { \_ -> MONAD }+ "do" { \_ -> DO }+ "return" { \_ -> RETURN }+ "ƒ" | "fun" { \_ -> DEFUN }+ "λ" | "lambda" { \_ -> LAMBDA }+ "⇒" | "=>" | "→" | "->" { \_ -> RARROW }+ "⇐" | "<=" | "←" | "<-" { \_ -> LARROW }+ "[" { \_ -> LBRACKET }+ "]" { \_ -> RBRACKET }+ "(" { \_ -> LPAREN }+ ")" { \_ -> RPAREN }+ "{" { \_ -> LBRACE }+ "}" { \_ -> RBRACE }+ "_" { \_ -> WILDCARD }+ "." { \_ -> DOT }+ ":" $chars+ { \s -> KEYWORD (tail s) }+ ":" { \_ -> COLON }+ "∷" | "::" { \_ -> DOUBLECOLON }+ "|" { \_ -> BAR }+ "let" { \_ -> LET }+ "Z" { \_ -> NUMBERT }+ "B" { \_ -> BOOLT }+ "C" { \_ -> CHART }+ "S" { \_ -> STRT }+ "×" { \_ -> PRODUCT }+ "import" { \_ -> IMPORT }+ "true" | "false" { \s -> BOOLEAN (read ([toUpper (s!!0)] ++ tail s)) }+ $upper $chars* { \s -> CON s }+ $lower $chars* { \s -> VAR s }+ $greek { \s -> TVAR (s!!0) }+ \"[^\"]*\" { \s -> STRING ((tail . init) s) }+ '[^'\"]{1}' { \s -> CHAR ((head . tail . init) s) }+ $operator | "≠" | "≤" | "≥" { \s -> OPERATOR s }+ $digit+ { \s -> NUMBER (read s) }+ "-" $digit+ { \s -> NUMBER (read s) }++{+data Token = DATA+ | MATCH+ | BEGIN+ | TYPE+ | DEFUN+ | LAMBDA+ | MONAD+ | DO+ | RETURN+ | IF+ | COND+ | ELSE+ | RARROW+ | LARROW+ | LBRACKET+ | RBRACKET+ | LPAREN+ | RPAREN+ | LBRACE+ | RBRACE+ | WILDCARD+ | DOT+ | COLON+ | DOUBLECOLON+ | BAR+ | VAR EName+ | TVAR Char+ | CON EName -- constructor names or uppercase symbols+ | LET+ | NUMBERT+ | BOOLT+ | CHART+ | STRT+ | PRODUCT+ | IMPORT+ | KEYWORD String+ | OPERATOR String+ | BOOLEAN Bool+ | NUMBER Int+ | STRING String+ | CHAR Char+ deriving(Eq, Show)++scanTokens = alexScanTokens+}
+ src/Ntha/Parser/Parser.y view
@@ -0,0 +1,310 @@+{+module Ntha.Parser.Parser where++import Ntha.State+import Ntha.Core.Ast+import Ntha.Type.Type+import Ntha.Type.Refined (convertProg')+import Ntha.Parser.Lexer+import Control.Monad+import Data.List+import Data.IORef+import Data.Maybe (fromMaybe, fromJust)+import qualified Data.Map as M+import System.IO.Unsafe (unsafePerformIO)+}++%name expr+%tokentype { Token }+%error { parseError }++%token+ data { DATA }+ match { MATCH }+ begin { BEGIN }+ type { TYPE }+ defun { DEFUN }+ lambda { LAMBDA }+ monad { MONAD }+ do { DO }+ return { RETURN }+ if { IF }+ cond { COND }+ else { ELSE }+ rarrow { RARROW }+ larrow { LARROW }+ con { CON $$ }+ '[' { LBRACKET }+ ']' { RBRACKET }+ '(' { LPAREN }+ ')' { RPAREN }+ '{' { LBRACE }+ '}' { RBRACE }+ '_' { WILDCARD }+ '.' { DOT }+ ':' { COLON }+ '::' { DOUBLECOLON }+ '|' { BAR }+ let { LET }+ import { IMPORT }+ TNumber { NUMBERT }+ TBool { BOOLT }+ TChar { CHART }+ TString { STRT }+ product { PRODUCT }+ keyword { KEYWORD $$ }+ VAR { VAR $$ }+ TVAR { TVAR $$ }+ OPERATOR { OPERATOR $$ }+ number { NUMBER $$ }+ boolean { BOOLEAN $$ }+ string { STRING $$ }+ char { CHAR $$ }++%%++Program : Exprs { EProgram $1 }++Exprs : Expr { [$1] }+ | Expr Exprs { $1 : $2 }++Expr : '(' defun VAR '[' Args ']' FormsPlus ')' { EDestructLetBinding (IdPattern $3) $5 $7 }+ | '(' data con SimpleArgs VConstructors ')' { unsafePerformIO $ do+ (env, vars) <- foldM (\(env, vars) arg -> do+ var <- makeVariable+ return (M.insert arg var env, vars ++ [var]))+ (M.empty, []) $4+ let dataType = TOper $3 vars+ let constructors' = map (\(EVConstructor cname cargs) -> let cargs' = map getType+ cargs+ where readEnv scope n = fromMaybe unitT $ M.lookup n scope+ getType arg = case arg of+ EVCAVar aname -> readEnv env aname+ EVCAOper aname operArgs -> TOper aname $ map (readEnv env) operArgs+ EVCAList arg' -> listT (getType arg')+ EVCATuple args -> productT (map getType args)+ in TypeConstructor cname cargs')+ $5+ return $ EDataDecl $3 dataType vars constructors' }+ | '(' let Pattern FormsPlus ')' { EDestructLetBinding $3 [] $4 }+ | '(' type con VConArg ')' { unsafePerformIO $ do+ $4 `seq` modifyIORef aliasMap $ M.insert $3 $4+ return EUnit }+ | '(' monad con Form ')' { unsafePerformIO $ do+ $4 `seq` modifyIORef monadMap $ M.insert $3 $4+ return $ EDestructLetBinding (IdPattern $3) [] [$4] }+ | '(' VAR ':' Type ')' { ETypeSig $2 $4 }+ | '(' import VAR ')' { EImport (getPathStr $3) }+ | Form { $1 }++-- TODO should support arg parameter such as (Maybe N umber)+SimpleArgs : {- empty -} { [] }+ | VAR SimpleArgs { $1 : $2 }++VConArg : VAR { EVCAVar $1 }+ | con { unsafePerformIO $ do+ alias <- readIORef aliasMap+ case M.lookup $1 alias of+ Just vconarg -> return vconarg+ Nothing -> if $1 == "String"+ then return $ EVCAList (EVCAOper "Char" []) -- special case for String pattern+ else return $ EVCAOper $1 [] }+ | '(' con SimpleArgs ')' { EVCAOper $2 $3 }+ -- TODO more specs here+ | '[' VConArg ']' { EVCAList $2 }+ | '(' TupleVConArgs ')' { EVCATuple $2 }++TupleVConArgs : VConArg '.' VConArg { [$1, $3] }+ | TupleVConArgs '.' VConArg { $1 ++ [$3] }++VConArgs : VConArg { [$1] }+ | VConArg VConArgs { $1 : $2 }++VConstructor : con { EVConstructor $1 [] }+ | '(' con VConArgs ')' { EVConstructor $2 $3 }+ | '(' VConArg keyword VConArg ')' { EVConstructor $3 [$2, $4] }++VConstructors : VConstructor { [$1] }+ | VConstructor VConstructors { $1 : $2 }++Args : {- empty -} { [] }+ | Pattern Args { $1 : $2 }++Nameds : {- empty -} { [] }+ | VAR Nameds { (Named $1 Nothing) : $2 }+ | '(' VAR ':' Type ')' Nameds { (Named $2 (Just $4)) : $6 }++binding : Pattern Form { ELetBinding $1 $2 [] }++bindings : binding { [$1] }+ | binding bindings { $1 : $2 }++bind : Form { Single $1 }+ | '(' return Form ')' { Return $3 }+ | '(' VAR larrow Form ')' { Bind $2 $4 }++binds : bind { [$1] }+ | bind binds { $1 : $2 }++Clause : '(' else rarrow Form ')' { Else $4 }+ | '(' Form rarrow Form ')' { Clause $2 $4 }++Clauses : Clause { [$1] }+ | Clause Clauses { $1 : $2 }++Form : '(' match Form Cases ')' { EPatternMatching $3 $4 }+ | '(' lambda Nameds rarrow FormsPlus ')' { ELambda $3 Nothing $5 }+ | '(' lambda Nameds ':' AtomType rarrow FormsPlus ')' { ELambda $3 (Just $5) $7 }+ | '(' let '[' bindings ']' FormsPlus ')' { head $ foldr (\(ELetBinding pat def _) body -> [ELetBinding pat def body]) $6 $4 }+ | '(' if Form Form Form ')' { EIf $3 [$4] [$5] }+ | '(' cond Clauses ')' { case last $3 of+ Else alt -> foldr (\(Clause cond consequent) alternative -> EIf cond [consequent] [alternative])+ alt (init $3)+ _ -> error "last clause in cond should be an else" }+ -- do block desuger to nested >>= and return, inspired by http://www.haskellforall.com/2014/10/how-to-desugar-haskell-code.html+ | '(' do con binds ')' { unsafePerformIO $ do+ monads <- readIORef monadMap+ return $ case M.lookup $3 monads of+ Just (ERecord pairs) -> case M.lookup "return" pairs of+ Just rtn -> case M.lookup ">>=" pairs of+ Just bind -> foldr (\b next -> case next of+ EUnit -> case b of+ Bind n e -> error "illegal do expression"+ Return e -> EApp newRtn e+ Single e -> e+ _ -> case b of+ Bind n e -> EApp (EApp newBind e) (ELambda [Named n Nothing] Nothing [next])+ Return e -> EApp newRtn e+ Single e -> e)+ EUnit $4+ where+ newBind = aliasArgName bind+ newRtn = aliasArgName rtn+ Nothing -> error $ "bind function is not defined for " ++ $3 ++ " monad"+ Nothing -> error $ "return function is not defined for " ++ $3 ++ " monad"+ _ -> error $ $3 ++ " monad is not defined" }+ | '(' ListForms ')' { $2 }+ | '(' TupleFroms ')' { ETuple $2 }+ | '(' Form FormsPlus ')' { foldl (\oper param -> (EApp oper param)) $2 $3 }+ | '(' Form keyword Form ')' { foldl (\oper param -> (EApp oper param)) (EVar $3) [$2, $4] }+ | '(' OPERATOR FormsPlus ')' { case $3 of+ a:[] -> EApp (EVar $2) a+ a:b:[] -> EApp (EApp (EVar $2) a) b+ a:b:xs -> foldl (\oper param -> (EApp (EApp (EVar $2) oper) param)) (EApp (EApp (EVar $2) a) b) xs }+ | '[' FormsStar ']' { EList $2 }+ | '{' RecordForms '}' { ERecord $2 }+ | '(' keyword Form ')' { EAccessor $3 $2 }+ | '(' begin Exprs ')' { EProgram $3 }+ | Atom { $1 }++RecordForms : keyword Form { M.singleton $1 $2 }+ | RecordForms keyword Form { M.insert $2 $3 $1 }++ListForms : Form '::' Form { EApp (EApp (EVar "Cons") $1) $3 }+ | Form '::' ListForms { EApp (EApp (EVar "Cons") $1) $3 }++TupleFroms : Form '.' Form { [$1, $3] }+ | TupleFroms '.' Form { $1 ++ [$3] }++FormsPlus : Form { [$1] }+ | Form FormsPlus { $1 : $2 }++FormsStar : {- empty -} { [] }+ | Form FormsStar { $1 : $2 }++Pattern : '_' { WildcardPattern }+ | VAR { IdPattern $1 }+ | number { NumPattern $1 }+ | boolean { BoolPattern $1 }+ | char { CharPattern $1 }+ | string { foldr (\p t -> TConPattern "Cons" [p, t]) (TConPattern "Nil" []) (map CharPattern $1) }+ | con { TConPattern $1 [] }+ | '(' con Args ')' { TConPattern $2 $3 }+ -- e.g. (t1 :~> t2)+ | '(' Pattern keyword Pattern ')' { TConPattern $3 [$2, $4] }+ | '(' TuplePatterns ')' { TuplePattern $2 }+ | '[' ']' { TConPattern "Nil" [] }+ | '[' Patterns ']' { foldr (\p t -> TConPattern "Cons" [p, t]) (TConPattern "Nil" []) $2 }+ | ListPatterns { $1 }+ | '(' ListDestructPats ')' { $2 }++Patterns : Pattern { [$1] }+ | Pattern Patterns { $1 : $2 }++TuplePatterns : Pattern '.' Pattern { [$1, $3] }+ | TuplePatterns '.' Pattern { $1 ++ [$3] }++ListPatterns : Pattern '::' Pattern { TConPattern "Cons" [$1, $3] }+ | Pattern '::' ListPatterns { TConPattern "Cons" [$1, $3] }++ListDestructPats : Pattern '::' Pattern { TConPattern "Cons" [$1, TConPattern "Cons" [$3, TConPattern "Nil" []]] }+ | Pattern '::' ListDestructPats { TConPattern "Cons" [$1, $3] }++Case : '(' Pattern rarrow FormsPlus ')' { Case $2 $4 }++Cases : Case { [$1] }+ | Case Cases { $1 : $2 }++Atom : boolean { EBool $1 }+ | number { ENum $1 }+ | string { EStr $1 }+ | char { EChar $1 }+ | VAR { EVar $1 }+ | OPERATOR { EVar $1 }+ | con { EVar $1 }++-- parsing type++Type : AtomType { $1 }+ | AtomType rarrow Type { arrowT $1 $3 }++-- TODO support type alias in type signature+AtomType : TVAR { fromJust $ M.lookup $1 tvarMap }+ | TNumber { intT }+ | TBool { boolT }+ | TChar { charT }+ | TString { strT }+ | con Types { TOper $1 $2 }+ | '[' Type ']' { listT $2 }+ | '(' TupleTypes ')' { productT $2 }+ | '(' Type ')' { $2 }+ | RefinedType { $1 }++RefinedType : '(' VAR ':' Type '|' Form ')' { TRefined $2 $4 (convertProg' $6) }++Types : {- empty -} { [] }+ | Type Types { $1 : $2 }++TupleTypes : Type product Type { [$1, $3] }+ | TupleTypes product Type { $1 ++ [$3] }++{+aliasMap :: IORef (M.Map String EVConArg)+aliasMap = createState M.empty++monadMap :: IORef (M.Map String Expr)+monadMap = createState M.empty++aliasArgName :: Expr -> Expr+aliasArgName expr@(ELambda nameds t exprs) = substName subrule expr+ where+ subrule = M.fromList $ foldl (\rule (Named name _) -> rule ++ [(name, name ++ "__monadarg__")]) [] nameds++tvarMap :: M.Map Char Type+tvarMap = unsafePerformIO $ do+ foldM (\m greek -> do+ tvar <- makeVariable+ return $ M.insert greek tvar m)+ M.empty ['α'..'ω']++getPathStr :: EPath -> EPath+getPathStr s = (map f s) ++ ".ntha"+ where f '.' = '/'+ f c = c++parseError :: [Token] -> a+parseError _ = error "Parse error"++parseExpr :: String -> Expr+parseExpr = expr . scanTokens+}
+ src/Ntha/Runtime/Eval.hs view
@@ -0,0 +1,228 @@+module Ntha.Runtime.Eval where++import Ntha.Core.Ast+import Ntha.Runtime.Value+import Data.Maybe (fromMaybe)+import Prelude hiding (lookup)+import qualified Data.Map as M+import qualified Data.Set as S++type Exclude = S.Set EName++evalFn :: Value -> Value -> ValueScope -> Value+evalFn (Fn f) arg scope = f arg scope+evalFn _ _ _ = VUnit++chainingFn :: EName -> Value -> Value+chainingFn argName next = Fn (\oarg _ -> Fn (\arg scope -> let margs = case oarg of+ FnApArgs pairs -> let v = fromMaybe VUnit $ M.lookup "***" pairs+ in FnApArgs $ M.insert "***" arg $ M.insert argName v pairs+ _ -> FnApArgs $ M.fromList [(argName, oarg), ("***", arg)]+ in evalFn next margs scope))++chaininLastFn :: EName -> [Expr] -> Value+chaininLastFn argName body = Fn (\arg scope -> let scope' = case arg of+ FnApArgs pairs -> foldl (\env (k, v) -> insert k v env)+ scope+ (M.toList $ M.insert argName (fromMaybe VUnit $ M.lookup "***" pairs) pairs)+ _ -> insert argName arg scope+ in snd $ foldl (\(env, val) instr -> val `seq` eval instr env) (scope', VUnit) body)++destrChainingFn :: Pattern -> Value -> Value+destrChainingFn pat next = Fn (\oarg _ -> Fn (\arg scope -> let margs = case oarg of+ DestrFnApArgs args freeVal -> DestrFnApArgs (args ++ [PatVal pat freeVal]) arg+ _ -> DestrFnApArgs [PatVal pat oarg] arg+ in evalFn next margs scope))++destrChaininLastFn :: Pattern -> [Expr] -> Value+destrChaininLastFn pat body = Fn (\arg scope -> let scope' = case arg of+ DestrFnApArgs args freeVal -> let s = foldl (\env (PatVal pat' val) -> define pat' val env)+ scope args+ in define pat freeVal s+ _ -> define pat arg scope+ in snd $ foldl (\(env, val) instr -> val `seq` eval instr env) (scope', VUnit) body)++tConChainingFn :: Tag -> Value -> Value+tConChainingFn tag next = Fn (\oarg _ -> Fn (\arg scope -> let targs = case oarg of+ TConArgs args tag' -> TConArgs (args ++ [arg]) tag'+ _ -> TConArgs [oarg, arg] tag+ in evalFn next targs scope))++tConChaininLastFn :: Tag -> Value+tConChaininLastFn tag = Fn (\arg _ -> let args = case arg of+ TConArgs args' _ -> args'+ VUnit -> []+ _ -> [arg]+ in Adt tag args)++excludePatternBoundNames :: Pattern -> Exclude -> Exclude+excludePatternBoundNames pat excluded = case pat of+ IdPattern name -> S.insert name excluded+ TuplePattern pats -> foldl (\exc p -> excludePatternBoundNames p exc) excluded pats+ TConPattern _ pats -> foldl (\exc p -> excludePatternBoundNames p exc) excluded pats+ _ -> excluded++visit :: Expr -> ValueScope -> ValueEnv -> Exclude -> (ValueScope, ValueEnv, Exclude)+visit expr scope capturedEnv excluded = case expr of+ EList values -> foldl (\(s, c, e) value -> visit value s c e)+ (scope, capturedEnv, excluded) values+ EIf cond thenInstrs elseInstrs -> (sco'', env'', exc'') where+ (sco, env, exc) = visit cond scope capturedEnv excluded+ (sco', env', exc') = foldl (\(s, c, e) value -> visit value s c e)+ (sco, env, exc) thenInstrs+ (sco'', env'', exc'') = foldl (\(s, c, e) value -> visit value s c e)+ (sco', env', exc') elseInstrs+ EVar name -> if name `notElem` excluded+ then let (scope', val) = eval expr scope+ in (scope', M.insert name val capturedEnv, excluded)+ else (scope, capturedEnv, excluded)+ EApp fn arg -> let (s, c, e) = visit fn scope capturedEnv excluded+ in visit arg s c e+ EDestructLetBinding main _ _ -> (scope, capturedEnv, excludePatternBoundNames main excluded)+ EPatternMatching input cases -> let (scope', capturedEnv', excluded') = visit input scope capturedEnv excluded+ in foldl (\(s, c, e) (Case pat outcomes) -> let e' = excludePatternBoundNames pat e+ in let (s', c', _) = foldl (\(sco, env, exc) instr -> visit instr sco env exc)+ (s, c, e') outcomes+ in (s', c', e))+ (scope', capturedEnv', excluded') cases+ _ -> (scope, capturedEnv, excluded)++envCapturingFnWrapper :: Value -> Expr -> ValueScope -> Value+envCapturingFnWrapper fn expr scope = case expr of+ (ELambda params _ instrs) -> mkFn capturedEnv where+ excluded = foldl (\exc (Named name _) -> S.insert name exc) S.empty params+ capturedEnv = mkCapturedEnv excluded instrs+ (EDestructLetBinding (IdPattern name) args instrs) -> mkFn capturedEnv where+ excluded = foldl (\exc pat -> excludePatternBoundNames pat exc) (S.singleton name) args+ capturedEnv = mkCapturedEnv excluded instrs+ _ -> VUnit+ where+ mkCapturedEnv excluded instrs = let (_, capturedEnv, _) = foldl (\(s, c, e) instr -> visit instr s c e)+ (scope, M.empty, excluded) instrs+ in capturedEnv+ mkFn capturedEnv = Fn (\arg scope' -> let scope'' = foldl (\env (k, v) -> insert k v env)+ scope' $ M.toList capturedEnv+ in evalFn fn arg scope'')++-- to predicate if a value is match specific pattern+match :: Value -> Pattern -> ValueScope -> (ValueScope, Bool)+match input pattern scope = case pattern of+ WildcardPattern -> (scope, True)+ IdPattern name -> (insert name input scope, True)+ NumPattern val -> (scope, input == (VNum val))+ BoolPattern val -> (scope, input == (VBool val))+ CharPattern val -> (scope, input == (VChar val))+ TuplePattern pats -> case input of+ VTuple items -> if length items /= length pats+ then (scope, False)+ else isAllMatch items pats+ _ -> (scope, False)+ TConPattern name pats -> case input of+ Adt tag args -> if name == tag && length pats == length args+ then isAllMatch args pats+ else (scope, False)+ _ -> (scope, False)+ where+ isAllMatch items pats = let (scope', isMatchs) = foldl (\(env, matchs) (item, pat) -> let (env', isMatch) = match item pat env+ in (env', matchs ++ [isMatch]))+ (scope, []) $ zip items pats+ in (scope', all id isMatchs)++define :: Pattern -> Value -> ValueScope -> ValueScope+define pattern val scope = case pattern of+ IdPattern name -> insert name val scope+ TuplePattern pats -> case val of+ VTuple items -> defineVals pats items+ _ -> error $ "Invalid value " ++ show val ++ " for pattern " ++ show pattern+ -- maybe should check pattern name and length of pats and args just like the match function above+ TConPattern _ pats -> case val of+ Adt _ args -> defineVals pats args+ _ -> error $ "Invalid value " ++ show val ++ " for pattern " ++ show pattern+ _ -> scope+ where+ defineVals pats items = foldl (\env (pat, item) -> define pat item env)+ scope $ zip pats items++eval :: Expr -> ValueScope -> (ValueScope, Value)+eval expr scope = case expr of+ ENum v -> (scope, VNum v)+ EBool v -> (scope, VBool v)+ EChar v -> (scope, VChar v)+ EStr v -> (scope, makeList $ map VChar v)+ EUnit -> (scope, VUnit)+ EVar name -> case lookup name scope of+ Just val -> (scope, val)+ Nothing -> error $ "Unknown identifier " ++ show expr+ EAccessor obj field -> case eval obj scope of+ (_, VRecord pairs) -> case M.lookup field pairs of+ Just val -> (scope, val)+ Nothing -> error $ "No field " ++ field ++ "in "++ show obj+ _ -> error $ "Not a record " ++ show obj+ ETuple values -> (scope, VTuple $ map (\v -> snd (eval v scope)) values)+ EList values -> (scope, makeList $ map (\v -> snd (eval v scope)) values)+ ERecord pairs -> (scope, VRecord $ M.map (\v -> snd (eval v scope)) pairs)+ ELambda params _ instrs -> let fnV = case reverse params of+ (Named name _):xs -> fnChain where+ lastFn = chaininLastFn name instrs+ fnChain = foldl (\fn (Named n _) -> chainingFn n fn) lastFn xs+ _ -> VUnit+ in (scope, envCapturingFnWrapper fnV expr scope)+ EApp fn arg -> case fnV of+ Fn f -> let (_, argV) = eval arg scope'+ in (scope, f argV scope')+ Adt _ _ -> case eval arg scope' of+ (_, VUnit) -> (scope, fnV)+ _ -> error $ "Error while evaluating " ++ show expr ++ ": " ++ show fnV ++ " constructor doesn't take arguments"+ _ -> error $ "Error while evaluating " ++ show expr ++ ": " ++ show fnV ++ " is not a function"+ where+ scope' = child scope+ (_, fnV) = eval fn scope'+ EIf cond thenInstrs elseInstrs -> let (_, condV) = eval cond scope+ in case condV of+ VBool v -> if v+ then (scope, evalInstrs thenInstrs)+ else (scope, evalInstrs elseInstrs)+ where+ evalInstrs instrs = let scope' = child scope+ in snd $ foldl (\(env, val) instr -> val `seq` eval instr env) (scope', VUnit) instrs+ _ -> error $ "Error while evaluating " ++ show expr ++ ": the condition is not a boolean"+ EPatternMatching input cases -> findPattern inputV cases+ where (_, inputV) = eval input scope+ findPattern :: Value -> [Case] -> (ValueScope, Value)+ findPattern val [] = error $ "Match exception: " ++ show input ++ " = " ++ show val ++ " didn't match any case of " ++ show expr+ findPattern val ((Case pat instrs):cs) = let (scope', isMatch) = match val pat $ child scope+ in if isMatch+ then (scope, snd $ foldl (\(env, val') instr -> val' `seq` eval instr env) (scope', VUnit) instrs)+ else findPattern val cs+ ELetBinding name def body -> let (scope', _) = eval (EDestructLetBinding name [] [def]) scope+ in (scope, snd $ foldl (\(env, val) instr -> val `seq` eval instr env) (scope', VUnit) body)+ EDestructLetBinding main args instrs -> if length args == 0+ -- define variable+ then let (_, val) = foldl (\(env, val') instr -> val' `seq` eval instr env) (child scope, VUnit) instrs+ in (define main val scope, val)+ -- define function+ else case main of+ IdPattern name -> let fnV = case reverse args of+ pat:pats -> fnChain where+ lastFn = destrChaininLastFn pat instrs+ fnChain = foldl (\fn p -> destrChainingFn p fn) lastFn pats+ _ -> VUnit+ in let fn = envCapturingFnWrapper fnV expr scope+ in (insert name fn scope, fn)+ _ -> error $ "Function name can only be a name, whereas a pattern " ++ show main ++ " was provided in " ++ show expr+ EDataDecl _ _ _ typeConstructors -> let scope' = foldl makeChain scope typeConstructors+ in (scope', VUnit)+ where+ makeChain env (TypeConstructor name types) = let fnV = case reverse types of+ _:ts -> fnChain where+ lastFn = tConChaininLastFn name+ fnChain = foldl (\fn _ -> tConChainingFn name fn)+ lastFn ts+ _ -> VUnit+ in if fnV == VUnit+ then insert name (Adt name []) env+ else insert name fnV env+ ETypeSig _ _ -> (scope, VUnit)+ EProgram instrs -> foldl (\(env, val) instr -> val `seq` eval instr env)+ (child scope, VUnit) instrs+ _ -> error $ "not support eval expr: " ++ show expr
+ src/Ntha/Runtime/Value.hs view
@@ -0,0 +1,151 @@+module Ntha.Runtime.Value where++import Ntha.Core.Ast+import Data.List (intercalate)+import Prelude hiding (lookup)+import qualified Data.Map as M++type ValueEnv = M.Map EName Value+type ParentScope = ValueScope++data ValueScope = ValueScope (Maybe ParentScope) ValueEnv++createEmptyScope :: ValueScope+createEmptyScope = ValueScope Nothing M.empty++createScopeWithParent :: ParentScope -> ValueScope+createScopeWithParent parent = ValueScope (Just parent) M.empty++createScope :: ParentScope -> ValueEnv -> ValueScope+createScope parent env = ValueScope (Just parent) env++insert :: EName -> Value -> ValueScope -> ValueScope+insert name t (ValueScope parent env) = ValueScope parent (M.insert name t env)++lookup :: EName -> ValueScope -> Maybe Value+lookup name (ValueScope parent env) = case M.lookup name env of+ Just t -> Just t+ Nothing -> case parent of+ Just p -> lookup name p+ Nothing -> Nothing++-- create a child type scope of current parent type scope+-- just to mock immutable scope, will remove later+child :: ParentScope -> ValueScope+child = createScopeWithParent++instance Show ValueScope where+ show (ValueScope parent env) = (show . M.toList) env ++ case parent of+ Just p -> " -> " ++ show p+ Nothing -> " -| "++type Tag = String+type FreeVal = Value++data Value = VNum Int+ | VChar Char+ | VBool Bool+ | VTuple [Value]+ | VRecord (M.Map EField Value)+ | VUnit+ | Adt Tag [Value]+ | Fn (Value -> ValueScope -> Value) -- or closure+ | FnApArgs (M.Map String Value)+ | DestrFnApArgs [PatVal] FreeVal+ | TConArgs [Value] Tag++data PatVal = PatVal Pattern Value+ deriving (Eq, Show, Ord)++nil :: Value+nil = Adt "Nil" []++cons :: Value -> Value -> Value+cons h t = Adt "Cons" [h, t]++makeList :: [Value] -> Value+makeList res = case res of+ [] -> nil+ x:xs -> cons x $ makeList xs++getElements :: Value -> [Value]+getElements l = case l of+ Adt "Cons" [h, t] -> h : (getElements t)+ _ -> []++reverseList :: Value -> Value+reverseList l = makeList . reverse . getElements $ l++strV :: String -> Value+strV s = makeList $ map (VChar) s++desugerStrV :: Value -> String+desugerStrV (Adt _ values) = case values of+ [] -> ""+ _ -> intercalate "" (map desugerStrV values)+desugerStrV v = show v++-- binary operator+binFn :: (Value -> Value -> Value) -> Value+binFn f = Fn (\arg1 _ -> Fn (\arg2 _ -> f arg1 arg2))++isString :: Value -> Bool+isString v = case v of+ Adt "Cons" [h, _] -> case h of+ VChar _ -> True+ _ -> False+ _ -> False++stringOfAdt :: Tag -> [Value] -> String+stringOfAdt tag values = case tag of+ "Cons" -> case (head values) of+ VChar _ -> "\"" ++ intercalate "" (map show (getElements (Adt tag values))) ++ "\""+ _ -> "[" ++ intercalate ", " (map (\v -> case v of+ Adt "Nil" [] -> "[]"+ _ -> show v) (getElements (Adt tag values))) ++ "]"+ "Nil" -> "[]"+ _ -> tag ++ case values of+ []-> ""+ _ -> " " ++ intercalate " | " (map show values)++stringOfPairs :: M.Map String Value -> String+stringOfPairs pairs = "{" ++ intercalate "," (M.elems $ M.mapWithKey (\f v -> f ++ " : " ++ show v) pairs) ++ "}"++instance Show Value where+ show (VNum i) = show i+ show (VChar c) = [c]+ show (VBool b) = show b+ show (VTuple values) = "(" ++ intercalate "," (map show values) ++ ")"+ show (VRecord pairs) = stringOfPairs pairs+ show VUnit = "⊥"+ show (Adt tag values) = stringOfAdt tag values+ show (Fn _) = "<fun>"+ show (FnApArgs pairs) = "FnApArgs(" ++ stringOfPairs pairs ++ ")"+ show (DestrFnApArgs pats val) = "DestrFnApArgs(" ++ intercalate ", " (map show pats) ++ " * " ++ show val ++ ")"+ show (TConArgs values tag) = "TConArgs(" ++ stringOfAdt tag values ++ ")"++instance Eq Value where+ VNum int1 == VNum int2 = int1 == int2+ VChar char1 == VChar char2 = char1 == char2+ VBool bool1 == VBool bool2 = bool1 == bool2+ VTuple values1 == VTuple values2 = values1 == values2+ VRecord pairs1 == VRecord pairs2 = pairs1 == pairs2+ VUnit == VUnit = True+ Adt tag1 values1 == Adt tag2 values2 = tag1 == tag2 && values1 == values2+ FnApArgs pairs1 == FnApArgs pairs2 = pairs1 == pairs2+ DestrFnApArgs vals1 val1 == DestrFnApArgs vals2 val2 = vals1 == vals2 && val1 == val2+ TConArgs vals1 tag1 == TConArgs vals2 tag2 = vals1 == vals2 && tag1 == tag2+ _ == _ = False++instance Ord Value where+ VNum int1 <= VNum int2 = int1 <= int2+ VChar char1 <= VChar char2 = char1 <= char2+ VBool bool1 <= VBool bool2 = bool1 <= bool2+ VTuple values1 <= VTuple values2 = values1 <= values2+ VRecord pairs1 <= VRecord pairs2 = pairs1 <= pairs2+ VUnit <= VUnit = True+ Adt tag1 values1 <= Adt tag2 values2 = tag1 <= tag2 && values1 <= values2+ FnApArgs pairs1 <= FnApArgs pairs2 = pairs1 <= pairs2+ DestrFnApArgs vals1 val1 <= DestrFnApArgs vals2 val2 = vals1 <= vals2 && val1 <= val2+ TConArgs vals1 tag1 <= TConArgs vals2 tag2 = vals1 <= vals2 && tag1 <= tag2+ _ <= _ = False
+ src/Ntha/State.hs view
@@ -0,0 +1,38 @@+module Ntha.State where++import Data.IORef+import System.IO.Unsafe (unsafePerformIO)++createState :: a -> IORef a+createState = unsafePerformIO . newIORef++readState :: IORef a -> a+readState = unsafePerformIO . readIORef++type Infer a = IO a++currentId :: IORef Int+currentId = createState 0++nextId :: Infer Int+nextId = do+ v <- readIORef currentId+ writeIORef currentId (v + 1)+ return v++resetId :: Infer ()+resetId = writeIORef currentId 0++currentUniqueName :: IORef Char+currentUniqueName = createState 'α'++nextUniqueName :: Infer String+nextUniqueName = do+ char <- readIORef currentUniqueName+ if char == 'ω'+ then resetUniqueName+ else writeIORef currentUniqueName $ succ char+ return [char]++resetUniqueName :: Infer ()+resetUniqueName = writeIORef currentUniqueName 'α'
+ src/Ntha/Type/Infer.hs view
@@ -0,0 +1,266 @@+module Ntha.Type.Infer where++import Ntha.State+import Ntha.Core.Ast+import Ntha.Type.Type+import Ntha.Type.TypeScope+import Data.IORef+import Control.Monad (when, zipWithM_, foldM, forM_)+import Control.Monad.Loops (anyM)+import qualified Data.Map as M+import qualified Data.Set as S+import Prelude hiding (lookup)++type NonGeneric = (S.Set Type)++occursInType :: Type -> Type -> Infer Bool+occursInType v t = do+ tP <- prune t+ case tP of+ TOper _ ts -> occursIn v ts+ v' -> return $ v == v'++occursIn :: Type -> [Type] -> Infer Bool+occursIn t = anyM (occursInType t)++isGeneric :: Type -> NonGeneric -> Infer Bool+isGeneric t nonGeneric = not <$> (occursIn t $ S.toList nonGeneric)++fresh :: Type -> NonGeneric -> Infer Type+fresh t nonGeneric = do+ mappings <- newIORef M.empty -- A mapping of TypeVariables to TypeVariables+ let freshrec ty = prune ty >>= (\tyP -> case tyP of+ TVar _ _ _ -> do+ isG <- isGeneric tyP nonGeneric+ if isG+ then do+ m <- readIORef mappings+ case M.lookup tyP m of+ Just tVar -> return tVar+ Nothing -> do+ newVar <- makeVariable+ modifyIORef mappings $ M.insert tyP newVar+ return newVar+ else return tyP+ TOper name types -> do+ newTypes <- mapM freshrec types+ return $ TOper name newTypes+ TCon name types dataType -> do+ newTypes <- mapM freshrec types+ newDataType <- freshrec dataType+ return $ TCon name newTypes newDataType+ TRecord valueTypes -> do+ newValueTypes <- foldM (\acc (k, v) -> do+ fv <- freshrec v+ return $ M.insert k fv acc)+ M.empty $ M.toList valueTypes+ return $ TRecord newValueTypes+ _ -> return tyP)+ freshrec t++getType :: TName -> TypeScope -> NonGeneric -> Infer Type+getType name scope nonGeneric = case lookup name scope of+ Just var -> fresh var nonGeneric+ Nothing -> error $ "Undefined symbol " ++ name++adjustType :: Type -> Type+adjustType t = case t of+ TCon _ types dataType -> functionT types dataType+ _ -> t++unify :: Type -> Type -> Infer ()+unify t1 t2 = do+ t1P <- prune t1+ t2P <- prune t2+ let t1PA = adjustType t1P+ let t2PA = adjustType t2P+ case (t1PA, t2PA) of+ (a@(TVar _ inst _), b) -> when (a /= b) $ do+ isOccurs <- occursInType a b+ when isOccurs $ error "Recusive unification"+ writeIORef inst $ Just b+ (a@(TOper _ _), b@(TVar _ _ _)) -> unify b a+ (a@(TOper name1 types1), b@(TOper name2 types2)) -> if name1 /= name2 || (length types1) /= (length types2)+ then error $ "Type mismatch " ++ show a ++ " ≠ " ++ show b+ else zipWithM_ unify types1 types2+ (a@(TRecord types1), b@(TRecord types2)) -> mapM_ (\(k, t2') -> do+ case M.lookup k types1 of+ Just t1' -> unify t2' t1'+ Nothing -> error $ "Cannot unify, no field " ++ k ++ " " ++ show a ++ ", " ++ show b)+ $ M.toList types2+ _ -> error $ "Can not unify " ++ show t1 ++ ", " ++ show t2++visitPattern :: Pattern -> TypeScope -> NonGeneric -> Infer (TypeScope, NonGeneric, Type)+visitPattern pattern scope nonGeneric = case pattern of+ WildcardPattern -> do+ resT <- makeVariable+ return (scope, nonGeneric, resT)+ IdPattern name -> do+ resT <- makeVariable+ return (insert name resT scope, S.insert resT nonGeneric, resT)+ NumPattern _ -> return (scope, nonGeneric, intT)+ BoolPattern _ -> return (scope, nonGeneric, boolT)+ CharPattern _ -> return (scope, nonGeneric, charT)+ TuplePattern items -> do+ (itemTypes, newScope, newNonGeneric) <- foldM (\(types, env, nonGen) item -> do+ (newEnv, newNonGen, itemT) <- visitPattern item env nonGen+ return (types ++ [itemT], newEnv, newNonGen))+ ([], scope, nonGeneric) items+ return (newScope, newNonGeneric, productT itemTypes)+ TConPattern name patterns -> do+ (patTypes, newScope, newNonGeneric) <- foldM (\(types, env, nonGen) pat -> do+ (newEnv, newNonGen, patT) <- visitPattern pat env nonGen+ return (types ++ [patT], newEnv, newNonGen))+ ([], scope, nonGeneric) patterns+ case lookup name newScope of+ Nothing -> error $ "Unknow type constructor " ++ name+ Just tconT -> case tconT of+ TCon _ _ _ -> do+ (TCon _ types dataType) <- fresh tconT newNonGeneric+ if (length patterns) /= (length types)+ then error $ "Bad arity: case " ++ show pattern ++ " provided " ++ (show . length) patterns ++ " arguments whereas " ++ name ++ " takes " ++ (show . length) types+ else do+ zipWithM_ unify patTypes types+ return (newScope, newNonGeneric, dataType)+ _ -> error $ "Invalid type constructor " ++ name++definePattern :: Pattern -> Type -> TypeScope -> Infer TypeScope+definePattern pattern t scope = do+ tP <- prune t+ case pattern of+ IdPattern name -> return $ insert name tP scope+ TuplePattern items -> case tP of+ TOper _ types -> do+ newScope <- foldM (\env (pat, patT) -> do+ newEnv <- definePattern pat patT env+ return newEnv)+ scope $ zip items types+ return newScope+ _ -> error $ "Invalid type " ++ show tP ++ " for pattern " ++ show pattern+ TConPattern _ patterns -> case tP of+ -- t is always functionT for now so a little non-sense for this case.+ TCon _ types _ -> do+ newScope <- foldM (\env (pat, patT) -> do+ newEnv <- definePattern pat patT env+ return newEnv)+ scope $ zip patterns types+ return newScope+ TOper _ types -> do+ newScope <- foldM (\env (pat, patT) -> do+ newEnv <- definePattern pat patT env+ return newEnv)+ scope $ zip patterns types+ return newScope+ _ -> error $ "Invalid type " ++ show tP ++ " for pattern " ++ show pattern+ _ -> return scope++analyze :: Expr -> TypeScope -> NonGeneric -> Infer (TypeScope, Type)+analyze expr scope nonGeneric = case expr of+ ENum _ -> return (scope, intT)+ EBool _ -> return (scope, boolT)+ EChar _ -> return (scope, charT)+ EStr _ -> return (scope, strT)+ EUnit -> return (scope, unitT)+ EList exprs -> do+ valueT <- makeVariable+ -- type checking procedure, since types of elems in a list should be the same.+ forM_ exprs (\e -> do+ (_, eT) <- analyze e scope nonGeneric+ unify valueT eT)+ return (scope, listT valueT)+ ETuple exprs -> do+ types <- foldM (\types expr' -> do+ (_, ty) <- analyze expr' scope nonGeneric+ return $ types ++ [ty])+ [] exprs+ return (scope, productT types)+ ERecord pairs -> do+ valueTypes <- foldM (\vts (k, v) -> do+ (_, t) <- analyze v scope nonGeneric+ return $ M.insert k t vts)+ M.empty $ M.toList pairs+ return (scope, TRecord valueTypes)+ EVar name -> (scope,) <$> getType name scope nonGeneric+ EApp fn arg -> do+ (_, fnT) <- analyze fn scope nonGeneric+ (_, argT) <- analyze arg scope nonGeneric+ rtnT <- makeVariable+ unify (functionT [argT] rtnT) fnT+ return (scope, rtnT)+ ELambda params annoT instructions -> do+ let newScope = child scope+ (paramTypes, newScope', newNonGeneric) <- foldM (\(types', env', nonGeneric') (Named name t) ->+ case t of+ Just t' -> return (types' ++ [t'], insert name t' env', S.insert t' nonGeneric')+ Nothing -> do+ t' <- makeVariable+ return (types' ++ [t'], insert name t' env', S.insert t' nonGeneric'))+ ([], newScope, nonGeneric) params+ rtnT <- foldM (\_ instr -> snd <$> analyze instr newScope' newNonGeneric) unitT instructions+ case annoT of+ Just annoT' -> unify rtnT annoT' -- type propagation from return type to param type+ Nothing -> return ()+ -- use fresh just to make sure sequence of lambda abstractions with same type var name could work well e.g.+ -- ((λ(x: α) : α → x) 3)+ -- ((λ(x: α) : α → x) true)+ (scope,) <$> fresh (functionT paramTypes rtnT) nonGeneric+ EAccessor obj field -> do+ (_, objT) <- analyze obj scope nonGeneric+ fieldT <- makeVariable+ let desiredT = TRecord $ M.fromList [(field, fieldT)]+ unify objT desiredT+ return (scope, fieldT)+ EIf cond thenInstructions elseInstructions -> do+ (_, condT) <- analyze cond scope nonGeneric+ unify condT boolT+ (newScope, thenT) <- foldM (\(env, _) instr -> analyze instr env nonGeneric)+ (scope, unitT) thenInstructions+ (newScope', elseT) <- foldM (\(env, _) instr -> analyze instr env nonGeneric)+ (newScope, unitT) elseInstructions+ unify thenT elseT+ return (newScope', thenT)+ ELetBinding main def body -> do+ (scope', _) <- analyze (EDestructLetBinding main [] [def]) scope nonGeneric+ foldM (\(env, _) instr -> analyze instr env nonGeneric) (scope', unitT) body+ EDestructLetBinding main args instructions -> do+ let name = case main of+ IdPattern n -> n ++ "-sig"+ _ -> ""+ let typeSig = lookup name scope+ let newScope = child scope+ (newScope', newNonGeneric, letTV) <- visitPattern main newScope nonGeneric+ let newNonGeneric' = S.insert letTV newNonGeneric+ (argTypes, newScope'', newNonGeneric'') <- foldM (\(types, env, nonGen) arg -> do+ (newEnv, newNonGen, argT) <- visitPattern arg env nonGen+ return (types ++ [argT], newEnv, newNonGen))+ ([], newScope', newNonGeneric') args+ rtnT <- foldM (\_ instr -> snd <$> analyze instr newScope'' newNonGeneric'') unitT instructions+ let letT = functionT argTypes rtnT+ newScope''' <- definePattern main letT newScope''+ case typeSig of+ Just (TSig ta) -> do+ let ta' = extractType ta+ unify ta' letT+ _ -> return ()+ return (newScope''', letT)+ EDataDecl _ t _ tconstructors -> do+ let newScope = foldl (\env (TypeConstructor conName conTypes) ->+ insert conName (TCon conName conTypes t) env)+ scope tconstructors+ return (newScope, t)+ EPatternMatching input cases -> do+ (_, inputT) <- analyze input scope nonGeneric+ resT <- makeVariable+ resT' <- foldM (\rt (Case pat outcomes) -> do+ let newScope = child scope+ (newScope', newNonGeneric, patT) <- visitPattern pat newScope nonGeneric+ unify patT inputT+ (_, caseT) <- foldM (\(env, _) outcome -> analyze outcome env newNonGeneric)+ (newScope', unitT) outcomes+ unify caseT rt+ return rt)+ resT cases+ return (scope, resT')+ ETypeSig name t -> return (insert (name ++ "-sig") (TSig t) scope, unitT)+ EProgram instructions -> foldM (\(env, _) instr -> analyze instr env nonGeneric) (scope, unitT) instructions+ _ -> error $ "not support infer expr: " ++ show expr
+ src/Ntha/Type/Refined.hs view
@@ -0,0 +1,139 @@+module Ntha.Type.Refined where++import Ntha.Core.Ast+import Ntha.Type.Type+import Ntha.Type.TypeScope+import Ntha.Z3.Class+import Ntha.Z3.Logic+import Ntha.Z3.Context+import Ntha.Z3.Assertion+import Z3.Monad+import Prelude hiding (lookup)+import Control.Monad (mapM_)+import Control.Monad.IO.Class (liftIO)++genPred :: Term -> Z3Pred+genPred term = case term of+ TmLT t1 t2 -> PAssert $ Less t1 t2+ TmGT t1 t2 -> PAssert $ Greater t1 t2+ TmLE t1 t2 -> PAssert $ LessE t1 t2+ TmGE t1 t2 -> PAssert $ GreaterE t1 t2+ TmEqual t1 t2 -> PAssert $ Equal t1 t2+ TmAnd t1 t2 -> PConj (genPred t1) (genPred t2)+ TmOr t1 t2 -> PDisj (genPred t1) (genPred t2)+ TmNot t -> PNeg (genPred t)+ _ -> error $ "not support term: " ++ show term++replaceRtnTerm :: String -> Term -> Term -> Term+replaceRtnTerm rtnName rtnTerm predTerm = case predTerm of+ TmVar n -> if n == rtnName then rtnTerm else predTerm+ TmNum _ -> predTerm+ TmLT t1 t2 -> TmLT (replaceRtnTerm' t1) (replaceRtnTerm' t2)+ TmGT t1 t2 -> TmGT (replaceRtnTerm' t1) (replaceRtnTerm' t2)+ TmLE t1 t2 -> TmLE (replaceRtnTerm' t1) (replaceRtnTerm' t2)+ TmGE t1 t2 -> TmGE (replaceRtnTerm' t1) (replaceRtnTerm' t2)+ TmSub t1 t2 -> TmSub (replaceRtnTerm' t1) (replaceRtnTerm' t2)+ TmAdd t1 t2 -> TmAdd (replaceRtnTerm' t1) (replaceRtnTerm' t2)+ TmMul t1 t2 -> TmMul (replaceRtnTerm' t1) (replaceRtnTerm' t2)+ TmDiv t1 t2 -> TmDiv (replaceRtnTerm' t1) (replaceRtnTerm' t2)+ TmEqual t1 t2 -> TmEqual (replaceRtnTerm' t1) (replaceRtnTerm' t2)+ TmAnd t1 t2 -> TmAnd (replaceRtnTerm' t1) (replaceRtnTerm' t2)+ TmOr t1 t2 -> TmOr (replaceRtnTerm' t1) (replaceRtnTerm' t2)+ TmNot t -> TmNot (replaceRtnTerm' t)+ TmIf t1 t2 t3 -> TmIf (replaceRtnTerm' t1) (replaceRtnTerm' t2) (replaceRtnTerm' t3)+ where replaceRtnTerm' = replaceRtnTerm rtnName rtnTerm++genRtnPred :: String -> Term -> Term -> Z3Pred+-- use neg to find counterexamples+genRtnPred rtnName rtnTerm = PNeg . genPred . (replaceRtnTerm rtnName rtnTerm)++convertProg' :: Expr -> Term+convertProg' expr = case expr of+ ENum n -> TmNum n+ EVar name -> TmVar name+ EApp fn arg -> case fn of+ EApp (EVar op) arg' -> opConstruct argTerm' argTerm+ where argTerm' = convertProg' arg'+ argTerm = convertProg' arg+ opConstruct = case op of+ "+" -> TmAdd+ "-" -> TmSub+ "*" -> TmMul+ "/" -> TmDiv+ "<" -> TmLT+ ">" -> TmGT+ "≤" -> TmLE+ "≥" -> TmGE+ "=" -> TmEqual+ "∧" -> TmAnd+ "∨" -> TmOr+ _ -> error $ "not support op: " ++ op+ EVar op -> case op of+ "¬" -> let argTerm = convertProg' arg+ in TmNot argTerm+ _ -> error $ "not support op: " ++ op+ _ -> error $ "not support fn: " ++ show fn+ EIf cond (thenInstruction:[]) (elseInstruction:[]) -> TmIf condTerm thenTerm elseTerm+ where condTerm = convertProg' cond+ thenTerm = convertProg' thenInstruction+ elseTerm = convertProg' elseInstruction+ _ -> error $ "not support expr: " ++ show expr++convertProg :: Expr -> TypeScope -> IO Z3Pred+convertProg expr scope = case expr of+ -- only support exists and exists2 for now+ EDestructLetBinding main args (instruction:[]) -> do+ let name = case main of+ IdPattern n -> n ++ "-sig"+ _ -> ""+ let typeSig = lookup name scope+ let argNames = map (\pat -> case pat of+ IdPattern n -> n+ _ -> show pat)+ args+ case typeSig of+ Just (TSig ta) -> do+ let terms = extractTerm ta+ let predNames = getPredNames ta+ case predNames of+ -- (¬ ⊥) always satisfied+ [] -> return PFalse+ _ -> case (argNames, terms) of+ ([n], [rtnTerm']) -> return $ PExists n RTInt $ genRtnPred' rtnTerm'+ ([n1, n2], [rtnTerm']) -> return $ PExists2 n1 n2 RTInt $ genRtnPred' rtnTerm'+ ([n], [argTerm, rtnTerm']) -> return $ PExists n RTInt $ PConj (genPred argTerm) $ genRtnPred' rtnTerm'+ ([n1, n2], [argTerm1, argTerm2, rtnTerm']) -> return $ PExists2 n1 n2 RTInt $ PConj (PConj (genPred argTerm1) $ genPred argTerm2) $ genRtnPred' rtnTerm'+ _ -> error $ "not support args: " ++ show argNames ++ " and terms: " ++ show terms+ where rtnName = last predNames+ rtnTerm = convertProg' instruction+ genRtnPred' :: Term -> Z3Pred+ genRtnPred' = genRtnPred rtnName rtnTerm+ -- (¬ ⊥) always satisfied+ _ -> return PFalse+ EProgram (instruction:_) -> convertProg instruction scope+ _ -> error $ "not support expr: " ++ show expr++checkPre :: Z3Pred -> Z3SMT () (Result, Maybe Model)+checkPre pre = local $ do+ ast <- encode pre+ local (assert ast >> getModel)++checker :: Expr -> TypeScope -> IO ()+checker expr scope = case expr of+ EDestructLetBinding _ _ _ -> do+ progPred <- convertProg expr scope+ -- trade off+ let adts = [("", [("", [("", RTInt)])])]+ ret <- runSMT adts () $ do+ (r, _mm) <- checkPre progPred+ case r of+ Unsat -> do+ core <- getUnsatCore+ liftIO $ sequence_ (map print core)+ return r+ other -> return other+ if ret == Right Unsat+ then return ()+ else error "refined type check failed"+ EProgram instructions -> mapM_ (\instr -> checker instr scope) instructions+ _ -> return ()
+ src/Ntha/Type/Type.hs view
@@ -0,0 +1,287 @@+module Ntha.Type.Type where++import Ntha.State+import Ntha.Z3.Class+import Ntha.Z3.Logic+import Ntha.Z3.Assertion+import Z3.Monad+import Data.IORef+import Data.List (intercalate)+import Data.Maybe (fromMaybe)+import Control.Monad (foldM, liftM)+import qualified Data.Map as M+import qualified Data.Set as S+import qualified Text.PrettyPrint as PP+import System.IO.Unsafe (unsafePerformIO)++type Id = Int+type TName = String+type TField = String+type Types = [Type]+type TInstance = Maybe Type+type Z3Pred = Pred Term RType Assertion++data Type = TVar Id (IORef TInstance) TName -- type variable+ | TOper TName Types -- type operator+ | TRecord (M.Map TField Type)+ | TCon TName Types Type+ | TSig Type+ | TRefined String Type Term++-- extract normal type from refined type for type inference+extractType :: Type -> Type+extractType t = case t of+ -- just support arrow type for now+ TOper "→" args -> TOper "→" (map extractType args)+ TRefined _ t' _ -> t'+ _ -> t++extractTerm :: Type -> [Term]+extractTerm t = case t of+ TOper "→" args -> args >>= extractTerm+ TRefined _ _ tm -> [tm]+ _ -> []++getPredNames :: Type -> [String]+getPredNames t = case t of+ TOper "→" args -> args >>= getPredNames+ TRefined n _ _ -> [n]+ _ -> []++intT :: Type+intT = TOper "Number" []++boolT :: Type+boolT = TOper "Boolean" []++charT :: Type+charT = TOper "Char" []++listT :: Type -> Type -- list type is not polymorphism+listT t = TOper "List" [t]++productT :: Types -> Type -- tuple type, product type is a name from Algebraic Data type+productT ts = TOper "*" ts++arrowT :: Type -> Type -> Type -- function type with single param+arrowT fromType toType = TOper "→" $ [fromType, toType]++functionT :: Types -> Type -> Type+functionT paramsT rtnT = foldr (\paramT resT -> arrowT paramT resT) rtnT paramsT++strT :: Type+strT = listT charT++unitT :: Type+unitT = TOper "()" []++prune :: Type -> Infer Type+prune t = case t of+ TVar _ inst _ -> do+ instV <- readIORef inst+ case instV of+ Just inst' -> do+ newInstance <- prune inst'+ writeIORef inst $ Just newInstance+ return newInstance+ Nothing -> return t+ _ -> return t++stringOfType :: M.Map TName TName -> Type -> Infer String+stringOfType subrule (TVar _ inst name) = do+ instV <- readIORef inst+ case instV of+ Just inst' -> stringOfType subrule inst'+ Nothing -> return $ fromMaybe "α" $ M.lookup name subrule+stringOfType subrule (TOper name args) = case name of+ "*" -> do+ argsStr <- (intercalate " * ") <$> mapM (stringOfType subrule) args+ return $ "(" ++ argsStr ++ ")"+ "List" -> do+ argStr <- stringOfType subrule $ args!!0+ return $ "[" ++ argStr ++ "]"+ "→" -> do+ argT <- prune $ args!!0+ rtnT <- prune $ args!!1+ argStr <- stringOfType subrule argT+ rtnStr <- stringOfType subrule rtnT+ let adjust t s = case t of+ TOper "→" _ -> "(" ++ s ++ ")"+ _ -> s+ let argStr' = adjust argT argStr+ let rtnStr' = adjust rtnT rtnStr+ return $ argStr' ++ " → " ++ rtnStr'+ _ -> if (length args) == 0+ then return name+ else do+ argsStr <- unwords <$> mapM (stringOfType subrule) args+ return $ "(" ++ name ++ " " ++ argsStr ++ ")"+stringOfType subrule (TRecord pairs) = do+ pairsStr <- (intercalate ", ") <$> (mapM (\(k, v) -> ((k ++ ": ") ++) <$> stringOfType subrule v) $ M.toList pairs)+ return $ "{" ++ pairsStr ++ "}"+stringOfType subrule (TCon name types dataType) = do+ dataTypeStr <- stringOfType subrule dataType+ case types of+ [] -> return dataTypeStr+ _ -> do+ typesStr <- (intercalate ", ") <$> mapM (stringOfType subrule) types+ return $ "(" ++ name ++ " " ++ typesStr ++ " ⇒ " ++ dataTypeStr ++ ")"+stringOfType subrule (TSig t) = liftM ("typesig: " ++) $ stringOfType subrule t+stringOfType subrule (TRefined _ t _) = liftM ("refined: " ++) $ stringOfType subrule t++getFreeVars :: Type -> Infer (S.Set TName)+getFreeVars (TVar _ inst name) = do+ instV <- readIORef inst+ case instV of+ Just inst' -> getFreeVars inst'+ Nothing -> return $ S.singleton name+getFreeVars (TOper _ args) = foldM (\acc arg -> do+ freeVars <- getFreeVars arg+ return $ S.union freeVars acc)+ S.empty args+getFreeVars (TRecord pairs) = foldM (\acc (_, v) -> do+ freeVars <- getFreeVars v+ return $ S.union freeVars acc)+ S.empty $ M.toList pairs+getFreeVars (TCon _ types dataType) = foldM (\acc t -> do+ freeVars <- getFreeVars t+ return $ S.union freeVars acc)+ S.empty $ types ++ [dataType]+getFreeVars (TSig t) = getFreeVars t+getFreeVars (TRefined _ t _) = getFreeVars t++normalize :: Type -> Infer String+normalize t = do+ freeVars <- getFreeVars t+ let subrule = M.map (\c -> [c]) $ M.fromList $ zip (S.toList freeVars) ['α'..'ω']+ stringOfType subrule t++instance Show Type where+ showsPrec _ x = shows $ PP.text $ unsafePerformIO $ normalize x++instance Eq Type where+ TVar id1 inst1 vname1 == TVar id2 inst2 vname2 = id1 == id2 && instV1 == instV2 && vname1 == vname2 where+ instV1 = readState inst1+ instV2 = readState inst2+ TOper name1 args1 == TOper name2 args2 = name1 == name2 && args1 == args2+ TRecord pairs1 == TRecord pairs2 = pairs1 == pairs2+ TCon name1 types1 dataType1 == TCon name2 types2 dataType2 = name1 == name2 && types1 == types2 && dataType1 == dataType2+ TSig t1 == TSig t2 = t1 == t2+ TRefined x1 t1 tm1 == TRefined x2 t2 tm2 = x1 == x2 && t1 == t2 && tm1 == tm2+ _ == _ = False++instance Ord Type where+ TVar id1 inst1 vname1 <= TVar id2 inst2 vname2 = id1 <= id2 && instV1 <= instV2 && vname1 <= vname2 where+ instV1 = readState inst1+ instV2 = readState inst2+ TOper name1 args1 <= TOper name2 args2 = name1 <= name2 && args1 <= args2+ TRecord pairs1 <= TRecord pairs2 = pairs1 <= pairs2+ TCon name1 types1 dataType1 <= TCon name2 types2 dataType2 = name1 <= name2 && types1 <= types2 && dataType1 <= dataType2+ TSig t1 <= TSig t2 = t1 <= t2+ TRefined x1 t1 tm1 <= TRefined x2 t2 tm2 = x1 <= x2 && t1 <= t2 && tm1 <= tm2+ _ <= _ = False++makeVariable :: Infer Type+makeVariable = do+ i <- nextId+ name <- nextUniqueName+ instRef <- newIORef Nothing+ return $ TVar i instRef name++-- for refined type++data Term = TmVar String+ | TmNum Int+ | TmLT Term Term+ | TmGT Term Term+ | TmLE Term Term+ | TmGE Term Term+ | TmSub Term Term+ | TmAdd Term Term+ | TmMul Term Term+ | TmDiv Term Term+ | TmEqual Term Term+ | TmAnd Term Term+ | TmOr Term Term+ | TmNot Term+ | TmIf Term Term Term++deriving instance Eq Term+deriving instance Ord Term+deriving instance Show Term++-- currently just support integer+data RType = RTInt++deriving instance Eq RType+deriving instance Ord RType++instance Z3Encoded Term where+ encode (TmVar x) = do+ ctx <- getQualifierCtx+ case M.lookup x ctx of+ Just (idx, _) -> return idx+ Nothing -> smtError $ "Can't find variable " ++ x+ encode (TmNum n) = mkIntSort >>= mkInt n+ encode (TmLT t1 t2) = encode (Less t1 t2)+ encode (TmGT t1 t2) = encode (Greater t1 t2)+ encode (TmLE t1 t2) = encode (LessE t1 t2)+ encode (TmGE t1 t2) = encode (GreaterE t1 t2)+ encode (TmAdd t1 t2) = do+ a1 <- encode t1+ a2 <- encode t2+ mkAdd [a1, a2]+ encode (TmSub t1 t2) = do+ a1 <- encode t1+ a2 <- encode t2+ mkSub [a1, a2]+ encode (TmMul t1 t2) = do+ a1 <- encode t1+ a2 <- encode t2+ mkMul [a1, a2]+ encode (TmDiv t1 t2) = do+ a1 <- encode t1+ a2 <- encode t2+ mkDiv a1 a2+ encode (TmEqual t1 t2) = do+ a1 <- encode t1+ a2 <- encode t2+ mkEq a1 a2+ encode (TmAnd t1 t2) = do+ a1 <- encode t1+ a2 <- encode t2+ mkAnd [a1, a2]+ encode (TmOr t1 t2) = do+ a1 <- encode t1+ a2 <- encode t2+ mkOr [a1, a2]+ encode (TmNot t) = encode t >>= mkNot+ encode (TmIf p c a) = do+ a1 <- encode p+ a2 <- encode c+ a3 <- encode a+ mkIte a1 a2 a3++instance Z3Sorted Term where+ sort (TmVar x) = do+ ctx <- getQualifierCtx+ case M.lookup x ctx of+ Just (_, s) -> return s+ Nothing -> smtError $ "Can't find variable " ++ x+ sort (TmNum _) = mkIntSort+ sort (TmLT _ _) = mkBoolSort+ sort (TmGT _ _) = mkBoolSort+ sort (TmLE _ _) = mkBoolSort+ sort (TmGE _ _) = mkBoolSort+ sort (TmAdd _ _) = mkIntSort+ sort (TmSub _ _) = mkIntSort+ sort (TmMul _ _) = mkIntSort+ sort (TmDiv _ _) = mkIntSort+ sort (TmEqual _ _) = mkBoolSort+ sort (TmAnd _ _) = mkBoolSort+ sort (TmOr _ _) = mkBoolSort+ sort (TmNot _) = mkBoolSort+ sort (TmIf _ c _) = sort c++instance Z3Sorted RType where+ sort RTInt = mkIntSort
+ src/Ntha/Type/TypeScope.hs view
@@ -0,0 +1,39 @@+module Ntha.Type.TypeScope where++import Ntha.Core.Ast+import Ntha.Type.Type+import Prelude hiding (lookup)+import qualified Data.Map as M++type TypeEnv = M.Map EName Type+type ParentScope = TypeScope++data TypeScope = TypeScope (Maybe ParentScope) TypeEnv++createEmptyScope :: TypeScope+createEmptyScope = TypeScope Nothing M.empty++createScopeWithParent :: ParentScope -> TypeScope+createScopeWithParent parent = TypeScope (Just parent) M.empty++createScope :: ParentScope -> TypeEnv -> TypeScope+createScope parent env = TypeScope (Just parent) env++insert :: EName -> Type -> TypeScope -> TypeScope+insert name t (TypeScope parent env) = TypeScope parent (M.insert name t env)++lookup :: EName -> TypeScope -> Maybe Type+lookup name (TypeScope parent env) = case M.lookup name env of+ Just t -> Just t+ Nothing -> case parent of+ Just p -> lookup name p+ Nothing -> Nothing++-- create a child type scope of current parent type scope+child :: ParentScope -> TypeScope+child = createScopeWithParent++instance Show TypeScope where+ show (TypeScope parent env) = (show . M.toList) env ++ case parent of+ Just p -> " -> " ++ show p+ Nothing -> " -| "
+ src/Ntha/Z3/Assertion.hs view
@@ -0,0 +1,63 @@+-- |+-- Assertions provided by libraries *for convenience*+-- It is not hard-coded into Z3.Logic.Pred+--++module Ntha.Z3.Assertion (Assertion(..)) where++import Ntha.Z3.Class+import Ntha.Z3.Encoding()+import Z3.Monad++import qualified Data.Map as M+import qualified Data.Set as S++data Assertion where+ -- | k is mapped to v in (m :: M.Map k v)+ -- XXX: m should be any "term", too strong now+ InMap :: forall k v. (Z3Sorted k, Z3Encoded k, Z3Sorted v, Z3Reserved v) => k -> v -> M.Map k v -> Assertion+ -- | v is in s+ -- XXX: s should be any "term", too strong now+ InSet :: forall v. (Z3Encoded v, Z3Sorted v) => v -> S.Set v -> Assertion+ -- | All below are binary relationships+ -- XXX: Should make sure v1 ~ v2, too weak now+ Equal :: forall v1 v2. (Z3Encoded v1, Z3Encoded v2, Eq v1, Eq v2) => v1 -> v2 -> Assertion+ LessE :: forall v1 v2. (Z3Encoded v1, Z3Encoded v2, Eq v1, Eq v2) => v1 -> v2 -> Assertion+ GreaterE :: forall v1 v2. (Z3Encoded v1, Z3Encoded v2, Eq v1, Eq v2) => v1 -> v2 -> Assertion+ Less :: forall v1 v2. (Z3Encoded v1, Z3Encoded v2, Eq v1, Eq v2) => v1 -> v2 -> Assertion+ Greater :: forall v1 v2. (Z3Encoded v1, Z3Encoded v2, Eq v1, Eq v2) => v1 -> v2 -> Assertion++instance Z3Encoded Assertion where+ encode (InMap k v m) = do+ kTm <- encode k+ vTm <- encode v+ mTm <- encode m+ lhs <- mkSelect mTm kTm+ mkEq lhs vTm+ encode (InSet e s) = do+ eTm <- encode e+ sTm <- encode s+ lhs <- mkSelect sTm eTm+ -- XXX: magic number+ one <- (mkIntSort >>= mkInt 1)+ mkEq one lhs+ encode (Equal t1 t2) = do+ a1 <- encode t1+ a2 <- encode t2+ mkEq a1 a2+ encode (LessE t1 t2) = do+ a1 <- encode t1+ a2 <- encode t2+ mkLe a1 a2+ encode (GreaterE t1 t2) = do+ a1 <- encode t1+ a2 <- encode t2+ mkGe a1 a2+ encode (Less t1 t2) = do+ a1 <- encode t1+ a2 <- encode t2+ mkLt a1 a2+ encode (Greater t1 t2) = do+ a1 <- encode t1+ a2 <- encode t2+ mkGt a1 a2
+ src/Ntha/Z3/Class.hs view
@@ -0,0 +1,223 @@+-- |+-- Type classes and built-in implementation for primitive Haskell types+-- ++module Ntha.Z3.Class (+ -- ** Types whose values are encodable to Z3 internal AST+ Z3Encoded(..),+ -- ** Types representable as Z3 Sort+ -- XXX: Unsound now+ -- XXX: Too flexible, can be used to encode Type ADT+ Z3Sorted(..),+ -- ** Type proxy helper, used with Z3Sorted+ Z3Sort(..),+ -- ** Types with reserved value for Z3 encoding use+ -- XXX: Magic value for built-in types+ Z3Reserved(..),+ -- ** Monad which can be instantiated into a concrete context+ SMT(..)+) where++import Ntha.Z3.Logic+import Z3.Monad++import Control.Monad.Except++import qualified Data.Map as M+import qualified Data.Set as S++data Z3Sort a = Z3Sort++class Z3Encoded a where+ encode :: SMT m e => a -> m e AST++-- | XXX: Unsound+class Z3Sorted a where+ -- | Map a value to Sort, the value should be a type-level thing+ sort :: SMT m e => a -> m e Sort+ sort _ = sortPhantom (Z3Sort :: Z3Sort a)++ -- | Map a Haskell type to Sort+ sortPhantom :: SMT m e => Z3Sort a -> m e Sort+ sortPhantom _ = smtError "sort error"++class Z3Encoded a => Z3Reserved a where+ def :: a++class (MonadError String (m e), MonadZ3 (m e)) => SMT m e where+ -- | Globally unique id+ genFreshId :: m e Int++ -- | Given data type declarations, extra field, and the SMT monad, return the fallible result in IO monad+ runSMT :: Z3Sorted ty => [(String, [(String, [(String, ty)])])] -> e -> m e a -> IO (Either String a)++ -- | Binding a variable String name to two things: an de Brujin idx as Z3 AST generated by mkBound and binder's Sort+ bindQualified :: String -> AST -> Sort -> m e ()++ -- | Get the above AST+ -- FIXME: The context management need extra -- we need to make sure that old binding wouldn't be destoryed+ -- XXX: We shouldn't expose a Map here. A fallible query interface is better+ getQualifierCtx :: m e (M.Map String (AST, Sort))++ -- | Get the preprocessed datatype context, a map from ADT's type name to its Z3 Sort+ -- XXX: We shouldn't expose a Map here. A fallible query interface is better+ getDataTypeCtx :: m e (M.Map String Sort)++ -- | Get extra+ getExtra :: m e e++ -- | Set extra+ modifyExtra :: (e -> e) -> m e ()++ -- | User don't have to import throwError+ smtError :: String -> m e a+ smtError = throwError++instance Z3Reserved Int where+ def = -1 -- XXX: Magic number++instance Z3Sorted Int where+ sortPhantom _ = mkIntSort++instance Z3Encoded Int where+ encode i = mkIntSort >>= mkInt i++instance Z3Reserved Double where+ def = -1.0 -- XXX: Magic number++instance Z3Sorted Double where+ sortPhantom _ = mkRealSort++instance Z3Encoded Double where+ encode = mkRealNum++instance Z3Reserved Bool where+ def = False -- XXX: Magic number++instance Z3Sorted Bool where+ sortPhantom _ = mkBoolSort++instance Z3Encoded Bool where+ encode = mkBool++-- The basic idea:+-- For each (k, v), assert in Z3 that if we select k from array we will get+-- the same value v+-- HACK: to set a default value for rest fields (or else we always get the last asserted value+-- as default, which is certainly not complying to finite map's definition), thus the+-- user should guarantee that he/she will never never think this value as a vaid one,+-- if not, he/she might get "a valid value mapped to a invalid key" semantics+instance (Z3Sorted k, Z3Encoded k, Z3Sorted v, Z3Reserved v) => Z3Encoded (M.Map k v) where+ encode m = do+ fid <- genFreshId+ arrSort <- sort m+ arr <- mkFreshConst ("map" ++ "_" ++ show fid) arrSort+ mapM_ (\(k, v) -> do+ kast <- encode k+ vast <- encode v+ sel <- mkSelect arr kast+ mkEq sel vast >>= assert) (M.toList m)+ arrValueDef <- mkArrayDefault arr+ vdef <- encode (def :: v)+ mkEq arrValueDef vdef >>= assert+ return arr++instance (Z3Sorted k, Z3Sorted v) => Z3Sorted (M.Map k v) where+ sortPhantom _ = do+ sk <- sortPhantom (Z3Sort :: Z3Sort k)+ sv <- sortPhantom (Z3Sort :: Z3Sort v)+ mkArraySort sk sv++-- Basic idea:+-- Set v =def= Map v {0, 1}+-- Thank god, this is much more sound+instance (Z3Sorted v, Z3Encoded v) => Z3Encoded (S.Set v) where+ encode s = do+ setSort <- sort s+ fid <- genFreshId+ arr <- mkFreshConst ("set" ++ "_" ++ show fid) setSort+ mapM_ (\e -> do+ ast <- encode e+ sel <- mkSelect arr ast+ one <- (mkIntSort >>= mkInt 1)+ mkEq sel one >>= assert) (S.toList s)+ arrValueDef <- mkArrayDefault arr+ zero <- (mkIntSort >>= mkInt 0)+ mkEq zero arrValueDef >>= assert+ return arr++instance Z3Sorted v => Z3Sorted (S.Set v) where+ sortPhantom _ = do+ sortElem <- sortPhantom (Z3Sort :: Z3Sort v)+ intSort <- mkIntSort+ mkArraySort sortElem intSort++instance (Z3Sorted t, Z3Sorted ty, Z3Encoded a) => Z3Encoded (Pred t ty a) where+ encode PTrue = mkTrue+ encode PFalse = mkFalse+ encode (PConj p1 p2) = do+ a1 <- encode p1+ a2 <- encode p2+ mkAnd [a1, a2]++ encode (PDisj p1 p2) = do+ a1 <- encode p1+ a2 <- encode p2+ mkOr [a1, a2]++ encode (PXor p1 p2) = do+ a1 <- encode p1+ a2 <- encode p2+ mkXor a1 a2++ encode (PNeg p) = encode p >>= mkNot++ encode (PForAll x ty p) = do+ sym <- mkStringSymbol x+ xsort <- sort ty+ -- "0" is de brujin idx for current binder+ -- it is passed to Z3 which returns an intenal (idx :: AST)+ -- This (idx :: AST) will be used to replace the variable+ -- in the abstraction body when encountered, thus it is stored+ -- in context by bindQualified we provide+ -- XXX: we should save and restore qualifier context here+ idx <- mkBound 0 xsort+ local $ do+ bindQualified x idx xsort+ body <- encode p+ -- The first [] is [Pattern], which is not really useful here+ mkForall [] [sym] [xsort] body++ encode (PExists x ty p) = do+ sym <- mkStringSymbol x+ xsort <- sort ty+ idx <- mkBound 0 xsort+ local $ do+ bindQualified x idx xsort+ a <- encode p+ mkExists [] [sym] [xsort] a++ -- HACK+ encode (PExists2 x y ty p) = do+ sym1 <- mkStringSymbol x+ sym2 <- mkStringSymbol y+ xsort <- sort ty+ idx1 <- mkBound 0 xsort+ idx2 <- mkBound 1 xsort+ local $ do+ bindQualified x idx1 xsort+ bindQualified y idx2 xsort+ a <- encode p+ mkExists [] [sym1, sym2] [xsort, xsort] a++ encode (PImpli p1 p2) = do+ a1 <- encode p1+ a2 <- encode p2+ mkImplies a1 a2++ encode (PIff p1 p2) = do+ a1 <- encode p1+ a2 <- encode p2+ mkIff a1 a2++ encode (PAssert a) = encode a
+ src/Ntha/Z3/Context.hs view
@@ -0,0 +1,61 @@+{-# LANGUAGE GeneralizedNewtypeDeriving #-}++-- | A concrete context implement SMT provided *for convenience*++module Ntha.Z3.Context (Z3SMT) where++import Ntha.Z3.Class+import Ntha.Z3.Encoding+import Z3.Monad++import Control.Monad.State+import Control.Monad.Except+import qualified Data.Map as M++data SMTContext e = SMTContext {+ -- | Bind local variables introduced by qualifiers to de brujin index in Z3+ _qualifierContext :: M.Map String (AST, Sort),+ -- | From type name to Z3 sort+ _datatypeCtx :: M.Map String Sort,+ -- | Counter used to generate globally unique ID+ _counter :: Int,+ -- | Extra field reserved for extension+ _extra :: e+} deriving (Show, Eq)++newtype Z3SMT e a = Z3SMT { unZ3SMT :: ExceptT String (StateT (SMTContext e) Z3) a }+ deriving (Monad, Applicative, Functor, MonadState (SMTContext e), MonadIO, MonadError String)++instance MonadZ3 (Z3SMT e) where+ getSolver = Z3SMT (lift (lift getSolver))+ getContext = Z3SMT (lift (lift getContext))++instance SMT Z3SMT e where+ genFreshId = do+ i <- _counter <$> get+ modify (\ctx -> ctx { _counter = i + 1 })+ return i++ runSMT datatypes e smt = evalZ3With Nothing opts m+ where+ smt' = do+ sorts <- mapM encodeDataType datatypes+ let datatypeCtx = M.fromList (zip (map fst datatypes) sorts)+ modify $ \ctx -> ctx { _datatypeCtx = datatypeCtx }+ smt++ -- XXX: not sure what does this option mean+ opts = opt "MODEL" True+ m = evalStateT (runExceptT (unZ3SMT smt'))+ (SMTContext M.empty M.empty 0 e)++ bindQualified x idx s = modify $ \ctx ->+ ctx { _qualifierContext = M.insert x (idx, s) (_qualifierContext ctx) }++ getQualifierCtx = _qualifierContext <$> get++ getDataTypeCtx = _datatypeCtx <$> get++ getExtra = _extra <$> get++ modifyExtra f = modify $ \ctx -> ctx { _extra = f (_extra ctx) }
+ src/Ntha/Z3/Encoding.hs view
@@ -0,0 +1,52 @@+-- |+-- Prviding some Z3 encoding for certain language constructs+-- Require a Class.SMT context to work++module Ntha.Z3.Encoding (+ -- ** Heterogenous list, a hack to encode different "term" into a list+ -- Used to encode function argument list+ HeteroList(..),+ -- ** encode function application+ encodeApp,+ -- ** encode datatype definition+ encodeDataType+) where++import Ntha.Z3.Class+import Z3.Monad hiding (mkMap, App)++data HeteroList where+ Cons :: forall a. (Z3Sorted a, Z3Encoded a) => a -> HeteroList -> HeteroList+ Nil :: HeteroList++instance Eq HeteroList where+ Nil == Nil = True+ Cons _ h1 == Cons _ h2 = h1 == h2+ _ == _ = False++mapH :: (forall a. (Z3Sorted a, Z3Encoded a) => a -> b) -> HeteroList -> [b]+mapH _ Nil = []+mapH f (Cons a l) = f a : mapH f l++encodeApp :: SMT m e => String -> HeteroList -> Sort -> m e AST+encodeApp fname args retSort = do+ paramSorts <- sequence $ mapH sort args+ sym <- mkStringSymbol fname+ decl <- mkFuncDecl sym paramSorts retSort+ argASTs <- sequence $ mapH encode args+ mkApp decl argASTs++encodeDataType :: SMT m e => Z3Sorted ty => (String, [(String, [(String, ty)])]) -> m e Sort+encodeDataType (tyName, alts) = do+ constrs <- mapM (\(consName, fields) -> do+ consSym <- mkStringSymbol consName+ -- recognizer. e.g. is_None None = True, is_None (Some _) = False+ recogSym <- mkStringSymbol ("is_" ++ consName)+ flds <- flip mapM fields $ \(fldName, fldTy) -> do+ symFld <- mkStringSymbol fldName+ s <- sort fldTy+ return (symFld, Just s, -1) -- XXX: non-rec+ mkConstructor consSym recogSym flds+ ) alts+ sym <- mkStringSymbol tyName+ mkDatatype sym constrs
+ src/Ntha/Z3/Logic.hs view
@@ -0,0 +1,18 @@+-- | Predicates++module Ntha.Z3.Logic (Pred(..)) where++data Pred t ty a where+ PTrue :: Pred t ty a+ PFalse :: Pred t ty a+ PConj :: Pred t ty a -> Pred t ty a -> Pred t ty a+ PDisj :: Pred t ty a -> Pred t ty a -> Pred t ty a+ PXor :: Pred t ty a -> Pred t ty a -> Pred t ty a+ PNeg :: Pred t ty a -> Pred t ty a+ PForAll :: String -> ty -> Pred t ty a -> Pred t ty a+ PExists :: String -> ty -> Pred t ty a -> Pred t ty a+ PExists2 :: String -> String -> ty -> Pred t ty a -> Pred t ty a+ PImpli :: Pred t ty a -> Pred t ty a -> Pred t ty a+ PIff :: Pred t ty a -> Pred t ty a -> Pred t ty a+ PAssert :: a -> Pred t ty a+ deriving (Show)
− src/Parser.y
@@ -1,310 +0,0 @@-{-module Parser where--import Ast-import Type-import Refined (convertProg')-import Lexer-import State-import Control.Monad-import Data.List-import Data.IORef-import Data.Maybe (fromMaybe, fromJust)-import qualified Data.Map as M-import System.IO.Unsafe (unsafePerformIO)-}--%name expr-%tokentype { Token }-%error { parseError }--%token- data { DATA }- match { MATCH }- begin { BEGIN }- type { TYPE }- defun { DEFUN }- lambda { LAMBDA }- monad { MONAD }- do { DO }- return { RETURN }- if { IF }- cond { COND }- else { ELSE }- rarrow { RARROW }- larrow { LARROW }- con { CON $$ }- '[' { LBRACKET }- ']' { RBRACKET }- '(' { LPAREN }- ')' { RPAREN }- '{' { LBRACE }- '}' { RBRACE }- '_' { WILDCARD }- '.' { DOT }- ':' { COLON }- '::' { DOUBLECOLON }- '|' { BAR }- let { LET }- import { IMPORT }- TNumber { NUMBERT }- TBool { BOOLT }- TChar { CHART }- TString { STRT }- product { PRODUCT }- keyword { KEYWORD $$ }- VAR { VAR $$ }- TVAR { TVAR $$ }- OPERATOR { OPERATOR $$ }- number { NUMBER $$ }- boolean { BOOLEAN $$ }- string { STRING $$ }- char { CHAR $$ }--%%--Program : Exprs { EProgram $1 }--Exprs : Expr { [$1] }- | Expr Exprs { $1 : $2 }--Expr : '(' defun VAR '[' Args ']' FormsPlus ')' { EDestructLetBinding (IdPattern $3) $5 $7 }- | '(' data con SimpleArgs VConstructors ')' { unsafePerformIO $ do- (env, vars) <- foldM (\(env, vars) arg -> do- var <- makeVariable- return (M.insert arg var env, vars ++ [var]))- (M.empty, []) $4- let dataType = TOper $3 vars- let constructors' = map (\(EVConstructor cname cargs) -> let cargs' = map getType- cargs- where readEnv scope n = fromMaybe unitT $ M.lookup n scope- getType arg = case arg of- EVCAVar aname -> readEnv env aname- EVCAOper aname operArgs -> TOper aname $ map (readEnv env) operArgs- EVCAList arg' -> listT (getType arg')- EVCATuple args -> productT (map getType args)- in TypeConstructor cname cargs')- $5- return $ EDataDecl $3 dataType vars constructors' }- | '(' let Pattern FormsPlus ')' { EDestructLetBinding $3 [] $4 }- | '(' type con VConArg ')' { unsafePerformIO $ do- $4 `seq` modifyIORef aliasMap $ M.insert $3 $4- return EUnit }- | '(' monad con Form ')' { unsafePerformIO $ do- $4 `seq` modifyIORef monadMap $ M.insert $3 $4- return $ EDestructLetBinding (IdPattern $3) [] [$4] }- | '(' VAR ':' Type ')' { ETypeSig $2 $4 }- | '(' import VAR ')' { EImport (getPathStr $3) }- | Form { $1 }---- TODO should support arg parameter such as (Maybe N umber)-SimpleArgs : {- empty -} { [] }- | VAR SimpleArgs { $1 : $2 }--VConArg : VAR { EVCAVar $1 }- | con { unsafePerformIO $ do- alias <- readIORef aliasMap- case M.lookup $1 alias of- Just vconarg -> return vconarg- Nothing -> if $1 == "String"- then return $ EVCAList (EVCAOper "Char" []) -- special case for String pattern- else return $ EVCAOper $1 [] }- | '(' con SimpleArgs ')' { EVCAOper $2 $3 }- -- TODO more specs here- | '[' VConArg ']' { EVCAList $2 }- | '(' TupleVConArgs ')' { EVCATuple $2 }--TupleVConArgs : VConArg '.' VConArg { [$1, $3] }- | TupleVConArgs '.' VConArg { $1 ++ [$3] }--VConArgs : VConArg { [$1] }- | VConArg VConArgs { $1 : $2 }--VConstructor : con { EVConstructor $1 [] }- | '(' con VConArgs ')' { EVConstructor $2 $3 }- | '(' VConArg keyword VConArg ')' { EVConstructor $3 [$2, $4] }--VConstructors : VConstructor { [$1] }- | VConstructor VConstructors { $1 : $2 }--Args : {- empty -} { [] }- | Pattern Args { $1 : $2 }--Nameds : {- empty -} { [] }- | VAR Nameds { (Named $1 Nothing) : $2 }- | '(' VAR ':' Type ')' Nameds { (Named $2 (Just $4)) : $6 }--binding : Pattern Form { ELetBinding $1 $2 [] }--bindings : binding { [$1] }- | binding bindings { $1 : $2 }--bind : Form { Single $1 }- | '(' return Form ')' { Return $3 }- | '(' VAR larrow Form ')' { Bind $2 $4 }--binds : bind { [$1] }- | bind binds { $1 : $2 }--Clause : '(' else rarrow Form ')' { Else $4 }- | '(' Form rarrow Form ')' { Clause $2 $4 }--Clauses : Clause { [$1] }- | Clause Clauses { $1 : $2 }--Form : '(' match Form Cases ')' { EPatternMatching $3 $4 }- | '(' lambda Nameds rarrow FormsPlus ')' { ELambda $3 Nothing $5 }- | '(' lambda Nameds ':' AtomType rarrow FormsPlus ')' { ELambda $3 (Just $5) $7 }- | '(' let '[' bindings ']' FormsPlus ')' { head $ foldr (\(ELetBinding pat def _) body -> [ELetBinding pat def body]) $6 $4 }- | '(' if Form Form Form ')' { EIf $3 [$4] [$5] }- | '(' cond Clauses ')' { case last $3 of- Else alt -> foldr (\(Clause cond consequent) alternative -> EIf cond [consequent] [alternative])- alt (init $3)- _ -> error "last clause in cond should be an else" }- -- do block desuger to nested >>= and return, inspired by http://www.haskellforall.com/2014/10/how-to-desugar-haskell-code.html- | '(' do con binds ')' { unsafePerformIO $ do- monads <- readIORef monadMap- return $ case M.lookup $3 monads of- Just (ERecord pairs) -> case M.lookup "return" pairs of- Just rtn -> case M.lookup ">>=" pairs of- Just bind -> foldr (\b next -> case next of- EUnit -> case b of- Bind n e -> error "illegal do expression"- Return e -> EApp newRtn e- Single e -> e- _ -> case b of- Bind n e -> EApp (EApp newBind e) (ELambda [Named n Nothing] Nothing [next])- Return e -> EApp newRtn e- Single e -> e)- EUnit $4- where- newBind = aliasArgName bind- newRtn = aliasArgName rtn- Nothing -> error $ "bind function is not defined for " ++ $3 ++ " monad"- Nothing -> error $ "return function is not defined for " ++ $3 ++ " monad"- _ -> error $ $3 ++ " monad is not defined" }- | '(' ListForms ')' { $2 }- | '(' TupleFroms ')' { ETuple $2 }- | '(' Form FormsPlus ')' { foldl (\oper param -> (EApp oper param)) $2 $3 }- | '(' Form keyword Form ')' { foldl (\oper param -> (EApp oper param)) (EVar $3) [$2, $4] }- | '(' OPERATOR FormsPlus ')' { case $3 of- a:[] -> EApp (EVar $2) a- a:b:[] -> EApp (EApp (EVar $2) a) b- a:b:xs -> foldl (\oper param -> (EApp (EApp (EVar $2) oper) param)) (EApp (EApp (EVar $2) a) b) xs }- | '[' FormsStar ']' { EList $2 }- | '{' RecordForms '}' { ERecord $2 }- | '(' keyword Form ')' { EAccessor $3 $2 }- | '(' begin Exprs ')' { EProgram $3 }- | Atom { $1 }--RecordForms : keyword Form { M.singleton $1 $2 }- | RecordForms keyword Form { M.insert $2 $3 $1 }--ListForms : Form '::' Form { EApp (EApp (EVar "Cons") $1) $3 }- | Form '::' ListForms { EApp (EApp (EVar "Cons") $1) $3 }--TupleFroms : Form '.' Form { [$1, $3] }- | TupleFroms '.' Form { $1 ++ [$3] }--FormsPlus : Form { [$1] }- | Form FormsPlus { $1 : $2 }--FormsStar : {- empty -} { [] }- | Form FormsStar { $1 : $2 }--Pattern : '_' { WildcardPattern }- | VAR { IdPattern $1 }- | number { NumPattern $1 }- | boolean { BoolPattern $1 }- | char { CharPattern $1 }- | string { foldr (\p t -> TConPattern "Cons" [p, t]) (TConPattern "Nil" []) (map CharPattern $1) }- | con { TConPattern $1 [] }- | '(' con Args ')' { TConPattern $2 $3 }- -- e.g. (t1 :~> t2)- | '(' Pattern keyword Pattern ')' { TConPattern $3 [$2, $4] }- | '(' TuplePatterns ')' { TuplePattern $2 }- | '[' ']' { TConPattern "Nil" [] }- | '[' Patterns ']' { foldr (\p t -> TConPattern "Cons" [p, t]) (TConPattern "Nil" []) $2 }- | ListPatterns { $1 }- | '(' ListDestructPats ')' { $2 }--Patterns : Pattern { [$1] }- | Pattern Patterns { $1 : $2 }--TuplePatterns : Pattern '.' Pattern { [$1, $3] }- | TuplePatterns '.' Pattern { $1 ++ [$3] }--ListPatterns : Pattern '::' Pattern { TConPattern "Cons" [$1, $3] }- | Pattern '::' ListPatterns { TConPattern "Cons" [$1, $3] }--ListDestructPats : Pattern '::' Pattern { TConPattern "Cons" [$1, TConPattern "Cons" [$3, TConPattern "Nil" []]] }- | Pattern '::' ListDestructPats { TConPattern "Cons" [$1, $3] }--Case : '(' Pattern rarrow FormsPlus ')' { Case $2 $4 }--Cases : Case { [$1] }- | Case Cases { $1 : $2 }--Atom : boolean { EBool $1 }- | number { ENum $1 }- | string { EStr $1 }- | char { EChar $1 }- | VAR { EVar $1 }- | OPERATOR { EVar $1 }- | con { EVar $1 }---- parsing type--Type : AtomType { $1 }- | AtomType rarrow Type { arrowT $1 $3 }---- TODO support type alias in type signature-AtomType : TVAR { fromJust $ M.lookup $1 tvarMap }- | TNumber { intT }- | TBool { boolT }- | TChar { charT }- | TString { strT }- | con Types { TOper $1 $2 }- | '[' Type ']' { listT $2 }- | '(' TupleTypes ')' { productT $2 }- | '(' Type ')' { $2 }- | RefinedType { $1 }--RefinedType : '(' VAR ':' Type '|' Form ')' { TRefined $2 $4 (convertProg' $6) }--Types : {- empty -} { [] }- | Type Types { $1 : $2 }--TupleTypes : Type product Type { [$1, $3] }- | TupleTypes product Type { $1 ++ [$3] }--{-aliasMap :: IORef (M.Map String EVConArg)-aliasMap = createState M.empty--monadMap :: IORef (M.Map String Expr)-monadMap = createState M.empty--aliasArgName :: Expr -> Expr-aliasArgName expr@(ELambda nameds t exprs) = substName subrule expr- where- subrule = M.fromList $ foldl (\rule (Named name _) -> rule ++ [(name, name ++ "__monadarg__")]) [] nameds--tvarMap :: M.Map Char Type-tvarMap = unsafePerformIO $ do- foldM (\m greek -> do- tvar <- makeVariable- return $ M.insert greek tvar m)- M.empty ['α'..'ω']--getPathStr :: EPath -> EPath-getPathStr s = (map f s) ++ ".ntha"- where f '.' = '/'- f c = c--parseError :: [Token] -> a-parseError _ = error "Parse error"--parseExpr :: String -> Expr-parseExpr = expr . scanTokens-}
− src/Prologue.hs
@@ -1,82 +0,0 @@-module Prologue where--import Ast-import Type-import Value-import State-import TypeScope-import Debug.Trace-import qualified Data.Map as M--mkTCon :: TypeConstructor -> Expr -> Type-mkTCon (TypeConstructor name types) (EDataDecl _ t _ _) = TCon name types t-mkTCon _ _ = error "not support"--assumptions :: Infer TypeScope-assumptions = do- tvarA <- makeVariable- tvarB <- makeVariable- let name = "List"- let vars = [tvarA]- let dataType = TOper name vars- let consConstructor = TypeConstructor "Cons" [tvarA, TOper "List" [tvarA]]- let nilConstructor = TypeConstructor "Nil" []- let listData = EDataDecl "List" dataType vars [consConstructor, nilConstructor]- return $ TypeScope Nothing $ M.fromList [("+", functionT [intT, intT] intT),- ("-", functionT [intT, intT] intT),- ("*", functionT [intT, intT] intT),- ("/", functionT [intT, intT] intT),- ("%", functionT [intT, intT] intT),- ("=", functionT [tvarB, tvarB] boolT),- ("≠", functionT [tvarB, tvarB] boolT),- ("<", functionT [intT, intT] boolT),- (">", functionT [intT, intT] boolT),- ("≤", functionT [intT, intT] boolT),- ("≥", functionT [intT, intT] boolT),- ("∧", functionT [boolT, boolT] boolT),- ("∨", functionT [boolT, boolT] boolT),- ("¬", functionT [boolT] boolT),- ("int2str", functionT [intT] strT),- ("bool2str", functionT [boolT] strT),- ("asserteq", functionT [tvarB, tvarB] unitT),- ("print", functionT [strT] unitT),- ("error", functionT [strT] tvarB),- ("reverse", functionT [listT tvarB] (listT tvarB)),- ("list?", functionT [tvarB] boolT),- ("string?", functionT [tvarB] boolT),- ("Cons", mkTCon consConstructor listData),- ("Nil", mkTCon nilConstructor listData),- ("inc", functionT [intT] intT),- ("dec", functionT [intT] intT)]--builtins :: ValueScope-builtins = ValueScope Nothing $ M.fromList [("+", binFn (\(VNum a) (VNum b) -> (VNum $ a + b))),- ("-", binFn (\(VNum a) (VNum b) -> (VNum $ a - b))),- ("*", binFn (\(VNum a) (VNum b) -> (VNum $ a * b))),- ("/", binFn (\(VNum a) (VNum b) -> (VNum $ a `div` b))),- ("%", binFn (\(VNum a) (VNum b) -> (VNum $ a `mod` b))),- ("=", binFn (\a b -> VBool $ a == b)),- ("≠", binFn (\a b -> VBool $ a /= b)),- ("<", binFn (\a b -> VBool $ a < b)),- (">", binFn (\a b -> VBool $ a > b)),- ("≤", binFn (\a b -> VBool $ a <= b)),- ("≥", binFn (\a b -> VBool $ a >= b)),- ("∧", binFn (\(VBool a) (VBool b) -> VBool $ a && b)),- ("∨", binFn (\(VBool a) (VBool b) -> VBool $ a || b)),- ("¬", Fn (\(VBool b) _ -> VBool $ not b)),- ("int2str", Fn (\(VNum n) _ -> strV $ show n)),- ("bool2str", Fn (\(VBool b) _ -> strV $ show b)),- ("asserteq", binFn (\a b -> if a == b- then VUnit- else error $ show a ++ " and " ++ show b ++ " not equal.")),- ("print", Fn (\v _ -> trace (desugerStrV v) VUnit)),- ("error", Fn (\v _ -> error $ desugerStrV v)),- ("reverse", Fn (\v _ -> reverseList v)),- ("list?", Fn (\v _ -> case v of- Adt "Cons" _ -> VBool True- _ -> VBool False)),- ("string?", Fn (\v _ -> VBool $ isString v)),- ("Cons", binFn (\a b -> cons a b)),- ("Nil", nil),- ("inc", Fn (\(VNum n) _ -> VNum $ n + 1)),- ("dec", Fn (\(VNum n) _ -> VNum $ n - 1))]
− src/Refined.hs
@@ -1,139 +0,0 @@-module Refined where--import Ast-import Type-import TypeScope-import Z3.Class-import Z3.Logic-import Z3.Context-import Z3.Assertion-import Z3.Monad-import Prelude hiding (lookup)-import Control.Monad (mapM_)-import Control.Monad.IO.Class (liftIO)--genPred :: Term -> Z3Pred-genPred term = case term of- TmLT t1 t2 -> PAssert $ Less t1 t2- TmGT t1 t2 -> PAssert $ Greater t1 t2- TmLE t1 t2 -> PAssert $ LessE t1 t2- TmGE t1 t2 -> PAssert $ GreaterE t1 t2- TmEqual t1 t2 -> PAssert $ Equal t1 t2- TmAnd t1 t2 -> PConj (genPred t1) (genPred t2)- TmOr t1 t2 -> PDisj (genPred t1) (genPred t2)- TmNot t -> PNeg (genPred t)- _ -> error $ "not support term: " ++ show term--replaceRtnTerm :: String -> Term -> Term -> Term-replaceRtnTerm rtnName rtnTerm predTerm = case predTerm of- TmVar n -> if n == rtnName then rtnTerm else predTerm- TmNum _ -> predTerm- TmLT t1 t2 -> TmLT (replaceRtnTerm' t1) (replaceRtnTerm' t2)- TmGT t1 t2 -> TmGT (replaceRtnTerm' t1) (replaceRtnTerm' t2)- TmLE t1 t2 -> TmLE (replaceRtnTerm' t1) (replaceRtnTerm' t2)- TmGE t1 t2 -> TmGE (replaceRtnTerm' t1) (replaceRtnTerm' t2)- TmSub t1 t2 -> TmSub (replaceRtnTerm' t1) (replaceRtnTerm' t2)- TmAdd t1 t2 -> TmAdd (replaceRtnTerm' t1) (replaceRtnTerm' t2)- TmMul t1 t2 -> TmMul (replaceRtnTerm' t1) (replaceRtnTerm' t2)- TmDiv t1 t2 -> TmDiv (replaceRtnTerm' t1) (replaceRtnTerm' t2)- TmEqual t1 t2 -> TmEqual (replaceRtnTerm' t1) (replaceRtnTerm' t2)- TmAnd t1 t2 -> TmAnd (replaceRtnTerm' t1) (replaceRtnTerm' t2)- TmOr t1 t2 -> TmOr (replaceRtnTerm' t1) (replaceRtnTerm' t2)- TmNot t -> TmNot (replaceRtnTerm' t)- TmIf t1 t2 t3 -> TmIf (replaceRtnTerm' t1) (replaceRtnTerm' t2) (replaceRtnTerm' t3)- where replaceRtnTerm' = replaceRtnTerm rtnName rtnTerm--genRtnPred :: String -> Term -> Term -> Z3Pred--- use neg to find counterexamples-genRtnPred rtnName rtnTerm = PNeg . genPred . (replaceRtnTerm rtnName rtnTerm)--convertProg' :: Expr -> Term-convertProg' expr = case expr of- ENum n -> TmNum n- EVar name -> TmVar name- EApp fn arg -> case fn of- EApp (EVar op) arg' -> opConstruct argTerm' argTerm- where argTerm' = convertProg' arg'- argTerm = convertProg' arg- opConstruct = case op of- "+" -> TmAdd- "-" -> TmSub- "*" -> TmMul- "/" -> TmDiv- "<" -> TmLT- ">" -> TmGT- "≤" -> TmLE- "≥" -> TmGE- "=" -> TmEqual- "∧" -> TmAnd- "∨" -> TmOr- _ -> error $ "not support op: " ++ op- EVar op -> case op of- "¬" -> let argTerm = convertProg' arg- in TmNot argTerm- _ -> error $ "not support op: " ++ op- _ -> error $ "not support fn: " ++ show fn- EIf cond (thenInstruction:[]) (elseInstruction:[]) -> TmIf condTerm thenTerm elseTerm- where condTerm = convertProg' cond- thenTerm = convertProg' thenInstruction- elseTerm = convertProg' elseInstruction- _ -> error $ "not support expr: " ++ show expr--convertProg :: Expr -> TypeScope -> IO Z3Pred-convertProg expr scope = case expr of- -- only support exists and exists2 for now- EDestructLetBinding main args (instruction:[]) -> do- let name = case main of- IdPattern n -> n ++ "-sig"- _ -> ""- let typeSig = lookup name scope- let argNames = map (\pat -> case pat of- IdPattern n -> n- _ -> show pat)- args- case typeSig of- Just (TSig ta) -> do- let terms = extractTerm ta- let predNames = getPredNames ta- case predNames of- -- (¬ ⊥) always satisfied- [] -> return PFalse- _ -> case (argNames, terms) of- ([n], [rtnTerm']) -> return $ PExists n RTInt $ genRtnPred' rtnTerm'- ([n1, n2], [rtnTerm']) -> return $ PExists2 n1 n2 RTInt $ genRtnPred' rtnTerm'- ([n], [argTerm, rtnTerm']) -> return $ PExists n RTInt $ PConj (genPred argTerm) $ genRtnPred' rtnTerm'- ([n1, n2], [argTerm1, argTerm2, rtnTerm']) -> return $ PExists2 n1 n2 RTInt $ PConj (PConj (genPred argTerm1) $ genPred argTerm2) $ genRtnPred' rtnTerm'- _ -> error $ "not support args: " ++ show argNames ++ " and terms: " ++ show terms- where rtnName = last predNames- rtnTerm = convertProg' instruction- genRtnPred' :: Term -> Z3Pred- genRtnPred' = genRtnPred rtnName rtnTerm- -- (¬ ⊥) always satisfied- _ -> return PFalse- EProgram (instruction:_) -> convertProg instruction scope- _ -> error $ "not support expr: " ++ show expr--checkPre :: Z3Pred -> Z3SMT () (Result, Maybe Model)-checkPre pre = local $ do- ast <- encode pre- local (assert ast >> getModel)--checker :: Expr -> TypeScope -> IO ()-checker expr scope = case expr of- EDestructLetBinding _ _ _ -> do- progPred <- convertProg expr scope- -- trade off- let adts = [("", [("", [("", RTInt)])])]- ret <- runSMT adts () $ do- (r, _mm) <- checkPre progPred- case r of- Unsat -> do- core <- getUnsatCore- liftIO $ sequence_ (map print core)- return r- other -> return other- if ret == Right Unsat- then return ()- else error "refined type check failed"- EProgram instructions -> mapM_ (\instr -> checker instr scope) instructions- _ -> return ()
− src/State.hs
@@ -1,38 +0,0 @@-module State where--import Data.IORef-import System.IO.Unsafe (unsafePerformIO)--createState :: a -> IORef a-createState = unsafePerformIO . newIORef--readState :: IORef a -> a-readState = unsafePerformIO . readIORef--type Infer a = IO a--currentId :: IORef Int-currentId = createState 0--nextId :: Infer Int-nextId = do- v <- readIORef currentId- writeIORef currentId (v + 1)- return v--resetId :: Infer ()-resetId = writeIORef currentId 0--currentUniqueName :: IORef Char-currentUniqueName = createState 'α'--nextUniqueName :: Infer String-nextUniqueName = do- char <- readIORef currentUniqueName- if char == 'ω'- then resetUniqueName- else writeIORef currentUniqueName $ succ char- return [char]--resetUniqueName :: Infer ()-resetUniqueName = writeIORef currentUniqueName 'α'
− src/Type.hs
@@ -1,287 +0,0 @@-module Type where--import State-import Data.IORef-import Data.List (intercalate)-import Control.Monad (foldM, liftM)-import Data.Maybe (fromMaybe)-import Z3.Class-import Z3.Logic-import Z3.Assertion-import Z3.Monad-import qualified Data.Map as M-import qualified Data.Set as S-import qualified Text.PrettyPrint as PP-import System.IO.Unsafe (unsafePerformIO)--type Id = Int-type TName = String-type TField = String-type Types = [Type]-type TInstance = Maybe Type-type Z3Pred = Pred Term RType Assertion--data Type = TVar Id (IORef TInstance) TName -- type variable- | TOper TName Types -- type operator- | TRecord (M.Map TField Type)- | TCon TName Types Type- | TSig Type- | TRefined String Type Term---- extract normal type from refined type for type inference-extractType :: Type -> Type-extractType t = case t of- -- just support arrow type for now- TOper "→" args -> TOper "→" (map extractType args)- TRefined _ t' _ -> t'- _ -> t--extractTerm :: Type -> [Term]-extractTerm t = case t of- TOper "→" args -> args >>= extractTerm- TRefined _ _ tm -> [tm]- _ -> []--getPredNames :: Type -> [String]-getPredNames t = case t of- TOper "→" args -> args >>= getPredNames- TRefined n _ _ -> [n]- _ -> []--intT :: Type-intT = TOper "Number" []--boolT :: Type-boolT = TOper "Boolean" []--charT :: Type-charT = TOper "Char" []--listT :: Type -> Type -- list type is not polymorphism-listT t = TOper "List" [t]--productT :: Types -> Type -- tuple type, product type is a name from Algebraic Data type-productT ts = TOper "*" ts--arrowT :: Type -> Type -> Type -- function type with single param-arrowT fromType toType = TOper "→" $ [fromType, toType]--functionT :: Types -> Type -> Type-functionT paramsT rtnT = foldr (\paramT resT -> arrowT paramT resT) rtnT paramsT--strT :: Type-strT = listT charT--unitT :: Type-unitT = TOper "()" []--prune :: Type -> Infer Type-prune t = case t of- TVar _ inst _ -> do- instV <- readIORef inst- case instV of- Just inst' -> do- newInstance <- prune inst'- writeIORef inst $ Just newInstance- return newInstance- Nothing -> return t- _ -> return t--stringOfType :: M.Map TName TName -> Type -> Infer String-stringOfType subrule (TVar _ inst name) = do- instV <- readIORef inst- case instV of- Just inst' -> stringOfType subrule inst'- Nothing -> return $ fromMaybe "α" $ M.lookup name subrule-stringOfType subrule (TOper name args) = case name of- "*" -> do- argsStr <- (intercalate " * ") <$> mapM (stringOfType subrule) args- return $ "(" ++ argsStr ++ ")"- "List" -> do- argStr <- stringOfType subrule $ args!!0- return $ "[" ++ argStr ++ "]"- "→" -> do- argT <- prune $ args!!0- rtnT <- prune $ args!!1- argStr <- stringOfType subrule argT- rtnStr <- stringOfType subrule rtnT- let adjust t s = case t of- TOper "→" _ -> "(" ++ s ++ ")"- _ -> s- let argStr' = adjust argT argStr- let rtnStr' = adjust rtnT rtnStr- return $ argStr' ++ " → " ++ rtnStr'- _ -> if (length args) == 0- then return name- else do- argsStr <- unwords <$> mapM (stringOfType subrule) args- return $ "(" ++ name ++ " " ++ argsStr ++ ")"-stringOfType subrule (TRecord pairs) = do- pairsStr <- (intercalate ", ") <$> (mapM (\(k, v) -> ((k ++ ": ") ++) <$> stringOfType subrule v) $ M.toList pairs)- return $ "{" ++ pairsStr ++ "}"-stringOfType subrule (TCon name types dataType) = do- dataTypeStr <- stringOfType subrule dataType- case types of- [] -> return dataTypeStr- _ -> do- typesStr <- (intercalate ", ") <$> mapM (stringOfType subrule) types- return $ "(" ++ name ++ " " ++ typesStr ++ " ⇒ " ++ dataTypeStr ++ ")"-stringOfType subrule (TSig t) = liftM ("typesig: " ++) $ stringOfType subrule t-stringOfType subrule (TRefined _ t _) = liftM ("refined: " ++) $ stringOfType subrule t--getFreeVars :: Type -> Infer (S.Set TName)-getFreeVars (TVar _ inst name) = do- instV <- readIORef inst- case instV of- Just inst' -> getFreeVars inst'- Nothing -> return $ S.singleton name-getFreeVars (TOper _ args) = foldM (\acc arg -> do- freeVars <- getFreeVars arg- return $ S.union freeVars acc)- S.empty args-getFreeVars (TRecord pairs) = foldM (\acc (_, v) -> do- freeVars <- getFreeVars v- return $ S.union freeVars acc)- S.empty $ M.toList pairs-getFreeVars (TCon _ types dataType) = foldM (\acc t -> do- freeVars <- getFreeVars t- return $ S.union freeVars acc)- S.empty $ types ++ [dataType]-getFreeVars (TSig t) = getFreeVars t-getFreeVars (TRefined _ t _) = getFreeVars t--normalize :: Type -> Infer String-normalize t = do- freeVars <- getFreeVars t- let subrule = M.map (\c -> [c]) $ M.fromList $ zip (S.toList freeVars) ['α'..'ω']- stringOfType subrule t--instance Show Type where- showsPrec _ x = shows $ PP.text $ unsafePerformIO $ normalize x--instance Eq Type where- TVar id1 inst1 vname1 == TVar id2 inst2 vname2 = id1 == id2 && instV1 == instV2 && vname1 == vname2 where- instV1 = readState inst1- instV2 = readState inst2- TOper name1 args1 == TOper name2 args2 = name1 == name2 && args1 == args2- TRecord pairs1 == TRecord pairs2 = pairs1 == pairs2- TCon name1 types1 dataType1 == TCon name2 types2 dataType2 = name1 == name2 && types1 == types2 && dataType1 == dataType2- TSig t1 == TSig t2 = t1 == t2- TRefined x1 t1 tm1 == TRefined x2 t2 tm2 = x1 == x2 && t1 == t2 && tm1 == tm2- _ == _ = False--instance Ord Type where- TVar id1 inst1 vname1 <= TVar id2 inst2 vname2 = id1 <= id2 && instV1 <= instV2 && vname1 <= vname2 where- instV1 = readState inst1- instV2 = readState inst2- TOper name1 args1 <= TOper name2 args2 = name1 <= name2 && args1 <= args2- TRecord pairs1 <= TRecord pairs2 = pairs1 <= pairs2- TCon name1 types1 dataType1 <= TCon name2 types2 dataType2 = name1 <= name2 && types1 <= types2 && dataType1 <= dataType2- TSig t1 <= TSig t2 = t1 <= t2- TRefined x1 t1 tm1 <= TRefined x2 t2 tm2 = x1 <= x2 && t1 <= t2 && tm1 <= tm2- _ <= _ = False--makeVariable :: Infer Type-makeVariable = do- i <- nextId- name <- nextUniqueName- instRef <- newIORef Nothing- return $ TVar i instRef name---- for refined type--data Term = TmVar String- | TmNum Int- | TmLT Term Term- | TmGT Term Term- | TmLE Term Term- | TmGE Term Term- | TmSub Term Term- | TmAdd Term Term- | TmMul Term Term- | TmDiv Term Term- | TmEqual Term Term- | TmAnd Term Term- | TmOr Term Term- | TmNot Term- | TmIf Term Term Term--deriving instance Eq Term-deriving instance Ord Term-deriving instance Show Term---- currently just support integer-data RType = RTInt--deriving instance Eq RType-deriving instance Ord RType--instance Z3Encoded Term where- encode (TmVar x) = do- ctx <- getQualifierCtx- case M.lookup x ctx of- Just (idx, _) -> return idx- Nothing -> smtError $ "Can't find variable " ++ x- encode (TmNum n) = mkIntSort >>= mkInt n- encode (TmLT t1 t2) = encode (Less t1 t2)- encode (TmGT t1 t2) = encode (Greater t1 t2)- encode (TmLE t1 t2) = encode (LessE t1 t2)- encode (TmGE t1 t2) = encode (GreaterE t1 t2)- encode (TmAdd t1 t2) = do- a1 <- encode t1- a2 <- encode t2- mkAdd [a1, a2]- encode (TmSub t1 t2) = do- a1 <- encode t1- a2 <- encode t2- mkSub [a1, a2]- encode (TmMul t1 t2) = do- a1 <- encode t1- a2 <- encode t2- mkMul [a1, a2]- encode (TmDiv t1 t2) = do- a1 <- encode t1- a2 <- encode t2- mkDiv a1 a2- encode (TmEqual t1 t2) = do- a1 <- encode t1- a2 <- encode t2- mkEq a1 a2- encode (TmAnd t1 t2) = do- a1 <- encode t1- a2 <- encode t2- mkAnd [a1, a2]- encode (TmOr t1 t2) = do- a1 <- encode t1- a2 <- encode t2- mkOr [a1, a2]- encode (TmNot t) = encode t >>= mkNot- encode (TmIf p c a) = do- a1 <- encode p- a2 <- encode c- a3 <- encode a- mkIte a1 a2 a3--instance Z3Sorted Term where- sort (TmVar x) = do- ctx <- getQualifierCtx- case M.lookup x ctx of- Just (_, s) -> return s- Nothing -> smtError $ "Can't find variable " ++ x- sort (TmNum _) = mkIntSort- sort (TmLT _ _) = mkBoolSort- sort (TmGT _ _) = mkBoolSort- sort (TmLE _ _) = mkBoolSort- sort (TmGE _ _) = mkBoolSort- sort (TmAdd _ _) = mkIntSort- sort (TmSub _ _) = mkIntSort- sort (TmMul _ _) = mkIntSort- sort (TmDiv _ _) = mkIntSort- sort (TmEqual _ _) = mkBoolSort- sort (TmAnd _ _) = mkBoolSort- sort (TmOr _ _) = mkBoolSort- sort (TmNot _) = mkBoolSort- sort (TmIf _ c _) = sort c--instance Z3Sorted RType where- sort RTInt = mkIntSort
− src/TypeScope.hs
@@ -1,39 +0,0 @@-module TypeScope where--import Ast-import Type-import Prelude hiding (lookup)-import qualified Data.Map as M--type TypeEnv = M.Map EName Type-type ParentScope = TypeScope--data TypeScope = TypeScope (Maybe ParentScope) TypeEnv--createEmptyScope :: TypeScope-createEmptyScope = TypeScope Nothing M.empty--createScopeWithParent :: ParentScope -> TypeScope-createScopeWithParent parent = TypeScope (Just parent) M.empty--createScope :: ParentScope -> TypeEnv -> TypeScope-createScope parent env = TypeScope (Just parent) env--insert :: EName -> Type -> TypeScope -> TypeScope-insert name t (TypeScope parent env) = TypeScope parent (M.insert name t env)--lookup :: EName -> TypeScope -> Maybe Type-lookup name (TypeScope parent env) = case M.lookup name env of- Just t -> Just t- Nothing -> case parent of- Just p -> lookup name p- Nothing -> Nothing---- create a child type scope of current parent type scope-child :: ParentScope -> TypeScope-child = createScopeWithParent--instance Show TypeScope where- show (TypeScope parent env) = (show . M.toList) env ++ case parent of- Just p -> " -> " ++ show p- Nothing -> " -| "
− src/Value.hs
@@ -1,151 +0,0 @@-module Value where--import Ast-import Data.List (intercalate)-import Prelude hiding (lookup)-import qualified Data.Map as M--type ValueEnv = M.Map EName Value-type ParentScope = ValueScope--data ValueScope = ValueScope (Maybe ParentScope) ValueEnv--createEmptyScope :: ValueScope-createEmptyScope = ValueScope Nothing M.empty--createScopeWithParent :: ParentScope -> ValueScope-createScopeWithParent parent = ValueScope (Just parent) M.empty--createScope :: ParentScope -> ValueEnv -> ValueScope-createScope parent env = ValueScope (Just parent) env--insert :: EName -> Value -> ValueScope -> ValueScope-insert name t (ValueScope parent env) = ValueScope parent (M.insert name t env)--lookup :: EName -> ValueScope -> Maybe Value-lookup name (ValueScope parent env) = case M.lookup name env of- Just t -> Just t- Nothing -> case parent of- Just p -> lookup name p- Nothing -> Nothing---- create a child type scope of current parent type scope--- just to mock immutable scope, will remove later-child :: ParentScope -> ValueScope-child = createScopeWithParent--instance Show ValueScope where- show (ValueScope parent env) = (show . M.toList) env ++ case parent of- Just p -> " -> " ++ show p- Nothing -> " -| "--type Tag = String-type FreeVal = Value--data Value = VNum Int- | VChar Char- | VBool Bool- | VTuple [Value]- | VRecord (M.Map EField Value)- | VUnit- | Adt Tag [Value]- | Fn (Value -> ValueScope -> Value) -- or closure- | FnApArgs (M.Map String Value)- | DestrFnApArgs [PatVal] FreeVal- | TConArgs [Value] Tag--data PatVal = PatVal Pattern Value- deriving (Eq, Show, Ord)--nil :: Value-nil = Adt "Nil" []--cons :: Value -> Value -> Value-cons h t = Adt "Cons" [h, t]--makeList :: [Value] -> Value-makeList res = case res of- [] -> nil- x:xs -> cons x $ makeList xs--getElements :: Value -> [Value]-getElements l = case l of- Adt "Cons" [h, t] -> h : (getElements t)- _ -> []--reverseList :: Value -> Value-reverseList l = makeList . reverse . getElements $ l--strV :: String -> Value-strV s = makeList $ map (VChar) s--desugerStrV :: Value -> String-desugerStrV (Adt _ values) = case values of- [] -> ""- _ -> intercalate "" (map desugerStrV values)-desugerStrV v = show v---- binary operator-binFn :: (Value -> Value -> Value) -> Value-binFn f = Fn (\arg1 _ -> Fn (\arg2 _ -> f arg1 arg2))--isString :: Value -> Bool-isString v = case v of- Adt "Cons" [h, _] -> case h of- VChar _ -> True- _ -> False- _ -> False--stringOfAdt :: Tag -> [Value] -> String-stringOfAdt tag values = case tag of- "Cons" -> case (head values) of- VChar _ -> "\"" ++ intercalate "" (map show (getElements (Adt tag values))) ++ "\""- _ -> "[" ++ intercalate ", " (map (\v -> case v of- Adt "Nil" [] -> "[]"- _ -> show v) (getElements (Adt tag values))) ++ "]"- "Nil" -> "[]"- _ -> tag ++ case values of- []-> ""- _ -> " " ++ intercalate " | " (map show values)--stringOfPairs :: M.Map String Value -> String-stringOfPairs pairs = "{" ++ intercalate "," (M.elems $ M.mapWithKey (\f v -> f ++ " : " ++ show v) pairs) ++ "}"--instance Show Value where- show (VNum i) = show i- show (VChar c) = [c]- show (VBool b) = show b- show (VTuple values) = "(" ++ intercalate "," (map show values) ++ ")"- show (VRecord pairs) = stringOfPairs pairs- show VUnit = "⊥"- show (Adt tag values) = stringOfAdt tag values- show (Fn _) = "<fun>"- show (FnApArgs pairs) = "FnApArgs(" ++ stringOfPairs pairs ++ ")"- show (DestrFnApArgs pats val) = "DestrFnApArgs(" ++ intercalate ", " (map show pats) ++ " * " ++ show val ++ ")"- show (TConArgs values tag) = "TConArgs(" ++ stringOfAdt tag values ++ ")"--instance Eq Value where- VNum int1 == VNum int2 = int1 == int2- VChar char1 == VChar char2 = char1 == char2- VBool bool1 == VBool bool2 = bool1 == bool2- VTuple values1 == VTuple values2 = values1 == values2- VRecord pairs1 == VRecord pairs2 = pairs1 == pairs2- VUnit == VUnit = True- Adt tag1 values1 == Adt tag2 values2 = tag1 == tag2 && values1 == values2- FnApArgs pairs1 == FnApArgs pairs2 = pairs1 == pairs2- DestrFnApArgs vals1 val1 == DestrFnApArgs vals2 val2 = vals1 == vals2 && val1 == val2- TConArgs vals1 tag1 == TConArgs vals2 tag2 = vals1 == vals2 && tag1 == tag2- _ == _ = False--instance Ord Value where- VNum int1 <= VNum int2 = int1 <= int2- VChar char1 <= VChar char2 = char1 <= char2- VBool bool1 <= VBool bool2 = bool1 <= bool2- VTuple values1 <= VTuple values2 = values1 <= values2- VRecord pairs1 <= VRecord pairs2 = pairs1 <= pairs2- VUnit <= VUnit = True- Adt tag1 values1 <= Adt tag2 values2 = tag1 <= tag2 && values1 <= values2- FnApArgs pairs1 <= FnApArgs pairs2 = pairs1 <= pairs2- DestrFnApArgs vals1 val1 <= DestrFnApArgs vals2 val2 = vals1 <= vals2 && val1 <= val2- TConArgs vals1 tag1 <= TConArgs vals2 tag2 = vals1 <= vals2 && tag1 <= tag2- _ <= _ = False
− src/Z3/Assertion.hs
@@ -1,63 +0,0 @@--- |--- Assertions provided by libraries *for convenience*--- It is not hard-coded into Z3.Logic.Pred-----module Z3.Assertion (Assertion(..)) where--import Z3.Class-import Z3.Encoding()-import Z3.Monad--import qualified Data.Map as M-import qualified Data.Set as S--data Assertion where- -- | k is mapped to v in (m :: M.Map k v)- -- XXX: m should be any "term", too strong now- InMap :: forall k v. (Z3Sorted k, Z3Encoded k, Z3Sorted v, Z3Reserved v) => k -> v -> M.Map k v -> Assertion- -- | v is in s- -- XXX: s should be any "term", too strong now- InSet :: forall v. (Z3Encoded v, Z3Sorted v) => v -> S.Set v -> Assertion- -- | All below are binary relationships- -- XXX: Should make sure v1 ~ v2, too weak now- Equal :: forall v1 v2. (Z3Encoded v1, Z3Encoded v2, Eq v1, Eq v2) => v1 -> v2 -> Assertion- LessE :: forall v1 v2. (Z3Encoded v1, Z3Encoded v2, Eq v1, Eq v2) => v1 -> v2 -> Assertion- GreaterE :: forall v1 v2. (Z3Encoded v1, Z3Encoded v2, Eq v1, Eq v2) => v1 -> v2 -> Assertion- Less :: forall v1 v2. (Z3Encoded v1, Z3Encoded v2, Eq v1, Eq v2) => v1 -> v2 -> Assertion- Greater :: forall v1 v2. (Z3Encoded v1, Z3Encoded v2, Eq v1, Eq v2) => v1 -> v2 -> Assertion--instance Z3Encoded Assertion where- encode (InMap k v m) = do- kTm <- encode k- vTm <- encode v- mTm <- encode m- lhs <- mkSelect mTm kTm- mkEq lhs vTm- encode (InSet e s) = do- eTm <- encode e- sTm <- encode s- lhs <- mkSelect sTm eTm- -- XXX: magic number- one <- (mkIntSort >>= mkInt 1)- mkEq one lhs- encode (Equal t1 t2) = do- a1 <- encode t1- a2 <- encode t2- mkEq a1 a2- encode (LessE t1 t2) = do- a1 <- encode t1- a2 <- encode t2- mkLe a1 a2- encode (GreaterE t1 t2) = do- a1 <- encode t1- a2 <- encode t2- mkGe a1 a2- encode (Less t1 t2) = do- a1 <- encode t1- a2 <- encode t2- mkLt a1 a2- encode (Greater t1 t2) = do- a1 <- encode t1- a2 <- encode t2- mkGt a1 a2
− src/Z3/Class.hs
@@ -1,223 +0,0 @@--- |--- Type classes and built-in implementation for primitive Haskell types--- --module Z3.Class (- -- ** Types whose values are encodable to Z3 internal AST- Z3Encoded(..),- -- ** Types representable as Z3 Sort- -- XXX: Unsound now- -- XXX: Too flexible, can be used to encode Type ADT- Z3Sorted(..),- -- ** Type proxy helper, used with Z3Sorted- Z3Sort(..),- -- ** Types with reserved value for Z3 encoding use- -- XXX: Magic value for built-in types- Z3Reserved(..),- -- ** Monad which can be instantiated into a concrete context- SMT(..)-) where--import Z3.Monad-import Z3.Logic--import Control.Monad.Except--import qualified Data.Map as M-import qualified Data.Set as S--data Z3Sort a = Z3Sort--class Z3Encoded a where- encode :: SMT m e => a -> m e AST---- | XXX: Unsound-class Z3Sorted a where- -- | Map a value to Sort, the value should be a type-level thing- sort :: SMT m e => a -> m e Sort- sort _ = sortPhantom (Z3Sort :: Z3Sort a)-- -- | Map a Haskell type to Sort- sortPhantom :: SMT m e => Z3Sort a -> m e Sort- sortPhantom _ = smtError "sort error"--class Z3Encoded a => Z3Reserved a where- def :: a--class (MonadError String (m e), MonadZ3 (m e)) => SMT m e where- -- | Globally unique id- genFreshId :: m e Int-- -- | Given data type declarations, extra field, and the SMT monad, return the fallible result in IO monad- runSMT :: Z3Sorted ty => [(String, [(String, [(String, ty)])])] -> e -> m e a -> IO (Either String a)-- -- | Binding a variable String name to two things: an de Brujin idx as Z3 AST generated by mkBound and binder's Sort- bindQualified :: String -> AST -> Sort -> m e ()-- -- | Get the above AST- -- FIXME: The context management need extra -- we need to make sure that old binding wouldn't be destoryed- -- XXX: We shouldn't expose a Map here. A fallible query interface is better- getQualifierCtx :: m e (M.Map String (AST, Sort))-- -- | Get the preprocessed datatype context, a map from ADT's type name to its Z3 Sort- -- XXX: We shouldn't expose a Map here. A fallible query interface is better- getDataTypeCtx :: m e (M.Map String Sort)-- -- | Get extra- getExtra :: m e e-- -- | Set extra- modifyExtra :: (e -> e) -> m e ()-- -- | User don't have to import throwError- smtError :: String -> m e a- smtError = throwError--instance Z3Reserved Int where- def = -1 -- XXX: Magic number--instance Z3Sorted Int where- sortPhantom _ = mkIntSort--instance Z3Encoded Int where- encode i = mkIntSort >>= mkInt i--instance Z3Reserved Double where- def = -1.0 -- XXX: Magic number--instance Z3Sorted Double where- sortPhantom _ = mkRealSort--instance Z3Encoded Double where- encode = mkRealNum--instance Z3Reserved Bool where- def = False -- XXX: Magic number--instance Z3Sorted Bool where- sortPhantom _ = mkBoolSort--instance Z3Encoded Bool where- encode = mkBool---- The basic idea:--- For each (k, v), assert in Z3 that if we select k from array we will get--- the same value v--- HACK: to set a default value for rest fields (or else we always get the last asserted value--- as default, which is certainly not complying to finite map's definition), thus the--- user should guarantee that he/she will never never think this value as a vaid one,--- if not, he/she might get "a valid value mapped to a invalid key" semantics-instance (Z3Sorted k, Z3Encoded k, Z3Sorted v, Z3Reserved v) => Z3Encoded (M.Map k v) where- encode m = do- fid <- genFreshId- arrSort <- sort m- arr <- mkFreshConst ("map" ++ "_" ++ show fid) arrSort- mapM_ (\(k, v) -> do- kast <- encode k- vast <- encode v- sel <- mkSelect arr kast- mkEq sel vast >>= assert) (M.toList m)- arrValueDef <- mkArrayDefault arr- vdef <- encode (def :: v)- mkEq arrValueDef vdef >>= assert- return arr--instance (Z3Sorted k, Z3Sorted v) => Z3Sorted (M.Map k v) where- sortPhantom _ = do- sk <- sortPhantom (Z3Sort :: Z3Sort k)- sv <- sortPhantom (Z3Sort :: Z3Sort v)- mkArraySort sk sv---- Basic idea:--- Set v =def= Map v {0, 1}--- Thank god, this is much more sound-instance (Z3Sorted v, Z3Encoded v) => Z3Encoded (S.Set v) where- encode s = do- setSort <- sort s- fid <- genFreshId- arr <- mkFreshConst ("set" ++ "_" ++ show fid) setSort- mapM_ (\e -> do- ast <- encode e- sel <- mkSelect arr ast- one <- (mkIntSort >>= mkInt 1)- mkEq sel one >>= assert) (S.toList s)- arrValueDef <- mkArrayDefault arr- zero <- (mkIntSort >>= mkInt 0)- mkEq zero arrValueDef >>= assert- return arr--instance Z3Sorted v => Z3Sorted (S.Set v) where- sortPhantom _ = do- sortElem <- sortPhantom (Z3Sort :: Z3Sort v)- intSort <- mkIntSort- mkArraySort sortElem intSort--instance (Z3Sorted t, Z3Sorted ty, Z3Encoded a) => Z3Encoded (Pred t ty a) where- encode PTrue = mkTrue- encode PFalse = mkFalse- encode (PConj p1 p2) = do- a1 <- encode p1- a2 <- encode p2- mkAnd [a1, a2]-- encode (PDisj p1 p2) = do- a1 <- encode p1- a2 <- encode p2- mkOr [a1, a2]-- encode (PXor p1 p2) = do- a1 <- encode p1- a2 <- encode p2- mkXor a1 a2-- encode (PNeg p) = encode p >>= mkNot-- encode (PForAll x ty p) = do- sym <- mkStringSymbol x- xsort <- sort ty- -- "0" is de brujin idx for current binder- -- it is passed to Z3 which returns an intenal (idx :: AST)- -- This (idx :: AST) will be used to replace the variable- -- in the abstraction body when encountered, thus it is stored- -- in context by bindQualified we provide- -- XXX: we should save and restore qualifier context here- idx <- mkBound 0 xsort- local $ do- bindQualified x idx xsort- body <- encode p- -- The first [] is [Pattern], which is not really useful here- mkForall [] [sym] [xsort] body-- encode (PExists x ty p) = do- sym <- mkStringSymbol x- xsort <- sort ty- idx <- mkBound 0 xsort- local $ do- bindQualified x idx xsort- a <- encode p- mkExists [] [sym] [xsort] a-- -- HACK- encode (PExists2 x y ty p) = do- sym1 <- mkStringSymbol x- sym2 <- mkStringSymbol y- xsort <- sort ty- idx1 <- mkBound 0 xsort- idx2 <- mkBound 1 xsort- local $ do- bindQualified x idx1 xsort- bindQualified y idx2 xsort- a <- encode p- mkExists [] [sym1, sym2] [xsort, xsort] a-- encode (PImpli p1 p2) = do- a1 <- encode p1- a2 <- encode p2- mkImplies a1 a2-- encode (PIff p1 p2) = do- a1 <- encode p1- a2 <- encode p2- mkIff a1 a2-- encode (PAssert a) = encode a
− src/Z3/Context.hs
@@ -1,61 +0,0 @@-{-# LANGUAGE GeneralizedNewtypeDeriving #-}---- | A concrete context implement SMT provided *for convenience*--module Z3.Context (Z3SMT) where--import Z3.Monad-import Z3.Class-import Z3.Encoding--import Control.Monad.State-import Control.Monad.Except-import qualified Data.Map as M--data SMTContext e = SMTContext {- -- | Bind local variables introduced by qualifiers to de brujin index in Z3- _qualifierContext :: M.Map String (AST, Sort),- -- | From type name to Z3 sort- _datatypeCtx :: M.Map String Sort,- -- | Counter used to generate globally unique ID- _counter :: Int,- -- | Extra field reserved for extension- _extra :: e-} deriving (Show, Eq)--newtype Z3SMT e a = Z3SMT { unZ3SMT :: ExceptT String (StateT (SMTContext e) Z3) a }- deriving (Monad, Applicative, Functor, MonadState (SMTContext e), MonadIO, MonadError String)--instance MonadZ3 (Z3SMT e) where- getSolver = Z3SMT (lift (lift getSolver))- getContext = Z3SMT (lift (lift getContext))--instance SMT Z3SMT e where- genFreshId = do- i <- _counter <$> get- modify (\ctx -> ctx { _counter = i + 1 })- return i-- runSMT datatypes e smt = evalZ3With Nothing opts m- where- smt' = do- sorts <- mapM encodeDataType datatypes- let datatypeCtx = M.fromList (zip (map fst datatypes) sorts)- modify $ \ctx -> ctx { _datatypeCtx = datatypeCtx }- smt-- -- XXX: not sure what does this option mean- opts = opt "MODEL" True- m = evalStateT (runExceptT (unZ3SMT smt'))- (SMTContext M.empty M.empty 0 e)-- bindQualified x idx s = modify $ \ctx ->- ctx { _qualifierContext = M.insert x (idx, s) (_qualifierContext ctx) }-- getQualifierCtx = _qualifierContext <$> get-- getDataTypeCtx = _datatypeCtx <$> get-- getExtra = _extra <$> get-- modifyExtra f = modify $ \ctx -> ctx { _extra = f (_extra ctx) }
− src/Z3/Encoding.hs
@@ -1,52 +0,0 @@--- |--- Prviding some Z3 encoding for certain language constructs--- Require a Class.SMT context to work--module Z3.Encoding (- -- ** Heterogenous list, a hack to encode different "term" into a list- -- Used to encode function argument list- HeteroList(..),- -- ** encode function application- encodeApp,- -- ** encode datatype definition- encodeDataType-) where--import Z3.Class-import Z3.Monad hiding (mkMap, App)--data HeteroList where- Cons :: forall a. (Z3Sorted a, Z3Encoded a) => a -> HeteroList -> HeteroList- Nil :: HeteroList--instance Eq HeteroList where- Nil == Nil = True- Cons _ h1 == Cons _ h2 = h1 == h2- _ == _ = False--mapH :: (forall a. (Z3Sorted a, Z3Encoded a) => a -> b) -> HeteroList -> [b]-mapH _ Nil = []-mapH f (Cons a l) = f a : mapH f l--encodeApp :: SMT m e => String -> HeteroList -> Sort -> m e AST-encodeApp fname args retSort = do- paramSorts <- sequence $ mapH sort args- sym <- mkStringSymbol fname- decl <- mkFuncDecl sym paramSorts retSort- argASTs <- sequence $ mapH encode args- mkApp decl argASTs--encodeDataType :: SMT m e => Z3Sorted ty => (String, [(String, [(String, ty)])]) -> m e Sort-encodeDataType (tyName, alts) = do- constrs <- mapM (\(consName, fields) -> do- consSym <- mkStringSymbol consName- -- recognizer. e.g. is_None None = True, is_None (Some _) = False- recogSym <- mkStringSymbol ("is_" ++ consName)- flds <- flip mapM fields $ \(fldName, fldTy) -> do- symFld <- mkStringSymbol fldName- s <- sort fldTy- return (symFld, Just s, -1) -- XXX: non-rec- mkConstructor consSym recogSym flds- ) alts- sym <- mkStringSymbol tyName- mkDatatype sym constrs
− src/Z3/Logic.hs
@@ -1,18 +0,0 @@--- | Predicates--module Z3.Logic (Pred(..)) where--data Pred t ty a where- PTrue :: Pred t ty a- PFalse :: Pred t ty a- PConj :: Pred t ty a -> Pred t ty a -> Pred t ty a- PDisj :: Pred t ty a -> Pred t ty a -> Pred t ty a- PXor :: Pred t ty a -> Pred t ty a -> Pred t ty a- PNeg :: Pred t ty a -> Pred t ty a- PForAll :: String -> ty -> Pred t ty a -> Pred t ty a- PExists :: String -> ty -> Pred t ty a -> Pred t ty a- PExists2 :: String -> String -> ty -> Pred t ty a -> Pred t ty a- PImpli :: Pred t ty a -> Pred t ty a -> Pred t ty a- PIff :: Pred t ty a -> Pred t ty a -> Pred t ty a- PAssert :: a -> Pred t ty a- deriving (Show)
test/EvalSpec.hs view
@@ -1,10 +1,10 @@ module EvalSpec where -import Ast-import Type-import Value-import Eval-import Prologue+import Ntha.Core.Ast+import Ntha.Runtime.Value+import Ntha.Type.Type+import Ntha.Runtime.Eval+import Ntha.Core.Prologue import qualified Data.Map as M import qualified Text.PrettyPrint as PP import Test.Hspec
test/InferSpec.hs view
@@ -1,11 +1,11 @@ module InferSpec where -import Ast-import Type-import Infer-import State (resetId, resetUniqueName)+import Ntha.Core.Ast+import Ntha.Type.Type+import Ntha.Type.Infer+import Ntha.Core.Prologue+import Ntha.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
test/ParserSpec.hs view
@@ -1,8 +1,8 @@ module ParserSpec where -import Ast-import Type-import Parser+import Ntha.Core.Ast+import Ntha.Type.Type+import Ntha.Parser.Parser import qualified Data.Map as M import qualified Text.PrettyPrint as PP import Test.Hspec