diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -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. diff --git a/app/Main.hs b/app/Main.hs --- a/app/Main.hs +++ b/app/Main.hs @@ -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 diff --git a/ntha.cabal b/ntha.cabal --- a/ntha.cabal +++ b/ntha.cabal @@ -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 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 diff --git a/src/Ast.hs b/src/Ast.hs deleted file mode 100644 --- a/src/Ast.hs +++ /dev/null @@ -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 diff --git a/src/Eval.hs b/src/Eval.hs deleted file mode 100644 --- a/src/Eval.hs +++ /dev/null @@ -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 diff --git a/src/Infer.hs b/src/Infer.hs deleted file mode 100644 --- a/src/Infer.hs +++ /dev/null @@ -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 diff --git a/src/Lexer.x b/src/Lexer.x deleted file mode 100644 --- a/src/Lexer.x +++ /dev/null @@ -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 -} diff --git a/src/Ntha.hs b/src/Ntha.hs new file mode 100644 --- /dev/null +++ b/src/Ntha.hs @@ -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 diff --git a/src/Ntha/Core/Ast.hs b/src/Ntha/Core/Ast.hs new file mode 100644 --- /dev/null +++ b/src/Ntha/Core/Ast.hs @@ -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 diff --git a/src/Ntha/Core/Prologue.hs b/src/Ntha/Core/Prologue.hs new file mode 100644 --- /dev/null +++ b/src/Ntha/Core/Prologue.hs @@ -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))] diff --git a/src/Ntha/Parser/Lexer.x b/src/Ntha/Parser/Lexer.x new file mode 100644 --- /dev/null +++ b/src/Ntha/Parser/Lexer.x @@ -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 +} diff --git a/src/Ntha/Parser/Parser.y b/src/Ntha/Parser/Parser.y new file mode 100644 --- /dev/null +++ b/src/Ntha/Parser/Parser.y @@ -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 +} diff --git a/src/Ntha/Runtime/Eval.hs b/src/Ntha/Runtime/Eval.hs new file mode 100644 --- /dev/null +++ b/src/Ntha/Runtime/Eval.hs @@ -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 diff --git a/src/Ntha/Runtime/Value.hs b/src/Ntha/Runtime/Value.hs new file mode 100644 --- /dev/null +++ b/src/Ntha/Runtime/Value.hs @@ -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 _) = "" + show (FnApArgs pairs) = "FnApArgs(" ++ stringOfPairs pairs ++ ")" + show (DestrFnApArgs pats val) = "DestrFnApArgs(" ++ intercalate ", " (map show pats) ++ " * " ++ show val ++ ")" + show (TConArgs values tag) = "TConArgs(" ++ stringOfAdt tag values ++ ")" + +instance Eq Value where + VNum int1 == VNum int2 = int1 == int2 + VChar char1 == VChar char2 = char1 == char2 + VBool bool1 == VBool bool2 = bool1 == bool2 + VTuple values1 == VTuple values2 = values1 == values2 + VRecord pairs1 == VRecord pairs2 = pairs1 == pairs2 + VUnit == VUnit = True + Adt tag1 values1 == Adt tag2 values2 = tag1 == tag2 && values1 == values2 + FnApArgs pairs1 == FnApArgs pairs2 = pairs1 == pairs2 + DestrFnApArgs vals1 val1 == DestrFnApArgs vals2 val2 = vals1 == vals2 && val1 == val2 + TConArgs vals1 tag1 == TConArgs vals2 tag2 = vals1 == vals2 && tag1 == tag2 + _ == _ = False + +instance Ord Value where + VNum int1 <= VNum int2 = int1 <= int2 + VChar char1 <= VChar char2 = char1 <= char2 + VBool bool1 <= VBool bool2 = bool1 <= bool2 + VTuple values1 <= VTuple values2 = values1 <= values2 + VRecord pairs1 <= VRecord pairs2 = pairs1 <= pairs2 + VUnit <= VUnit = True + Adt tag1 values1 <= Adt tag2 values2 = tag1 <= tag2 && values1 <= values2 + FnApArgs pairs1 <= FnApArgs pairs2 = pairs1 <= pairs2 + DestrFnApArgs vals1 val1 <= DestrFnApArgs vals2 val2 = vals1 <= vals2 && val1 <= val2 + TConArgs vals1 tag1 <= TConArgs vals2 tag2 = vals1 <= vals2 && tag1 <= tag2 + _ <= _ = False diff --git a/src/Ntha/State.hs b/src/Ntha/State.hs new file mode 100644 --- /dev/null +++ b/src/Ntha/State.hs @@ -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 'α' diff --git a/src/Ntha/Type/Infer.hs b/src/Ntha/Type/Infer.hs new file mode 100644 --- /dev/null +++ b/src/Ntha/Type/Infer.hs @@ -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 diff --git a/src/Ntha/Type/Refined.hs b/src/Ntha/Type/Refined.hs new file mode 100644 --- /dev/null +++ b/src/Ntha/Type/Refined.hs @@ -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 () diff --git a/src/Ntha/Type/Type.hs b/src/Ntha/Type/Type.hs new file mode 100644 --- /dev/null +++ b/src/Ntha/Type/Type.hs @@ -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 diff --git a/src/Ntha/Type/TypeScope.hs b/src/Ntha/Type/TypeScope.hs new file mode 100644 --- /dev/null +++ b/src/Ntha/Type/TypeScope.hs @@ -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 -> " -| " diff --git a/src/Ntha/Z3/Assertion.hs b/src/Ntha/Z3/Assertion.hs new file mode 100644 --- /dev/null +++ b/src/Ntha/Z3/Assertion.hs @@ -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 diff --git a/src/Ntha/Z3/Class.hs b/src/Ntha/Z3/Class.hs new file mode 100644 --- /dev/null +++ b/src/Ntha/Z3/Class.hs @@ -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 diff --git a/src/Ntha/Z3/Context.hs b/src/Ntha/Z3/Context.hs new file mode 100644 --- /dev/null +++ b/src/Ntha/Z3/Context.hs @@ -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) } diff --git a/src/Ntha/Z3/Encoding.hs b/src/Ntha/Z3/Encoding.hs new file mode 100644 --- /dev/null +++ b/src/Ntha/Z3/Encoding.hs @@ -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 diff --git a/src/Ntha/Z3/Logic.hs b/src/Ntha/Z3/Logic.hs new file mode 100644 --- /dev/null +++ b/src/Ntha/Z3/Logic.hs @@ -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) diff --git a/src/Parser.y b/src/Parser.y deleted file mode 100644 --- a/src/Parser.y +++ /dev/null @@ -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 -} diff --git a/src/Prologue.hs b/src/Prologue.hs deleted file mode 100644 --- a/src/Prologue.hs +++ /dev/null @@ -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))] diff --git a/src/Refined.hs b/src/Refined.hs deleted file mode 100644 --- a/src/Refined.hs +++ /dev/null @@ -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 () diff --git a/src/State.hs b/src/State.hs deleted file mode 100644 --- a/src/State.hs +++ /dev/null @@ -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 'α' diff --git a/src/Type.hs b/src/Type.hs deleted file mode 100644 --- a/src/Type.hs +++ /dev/null @@ -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 diff --git a/src/TypeScope.hs b/src/TypeScope.hs deleted file mode 100644 --- a/src/TypeScope.hs +++ /dev/null @@ -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 -> " -| " diff --git a/src/Value.hs b/src/Value.hs deleted file mode 100644 --- a/src/Value.hs +++ /dev/null @@ -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 _) = "" - show (FnApArgs pairs) = "FnApArgs(" ++ stringOfPairs pairs ++ ")" - show (DestrFnApArgs pats val) = "DestrFnApArgs(" ++ intercalate ", " (map show pats) ++ " * " ++ show val ++ ")" - show (TConArgs values tag) = "TConArgs(" ++ stringOfAdt tag values ++ ")" - -instance Eq Value where - VNum int1 == VNum int2 = int1 == int2 - VChar char1 == VChar char2 = char1 == char2 - VBool bool1 == VBool bool2 = bool1 == bool2 - VTuple values1 == VTuple values2 = values1 == values2 - VRecord pairs1 == VRecord pairs2 = pairs1 == pairs2 - VUnit == VUnit = True - Adt tag1 values1 == Adt tag2 values2 = tag1 == tag2 && values1 == values2 - FnApArgs pairs1 == FnApArgs pairs2 = pairs1 == pairs2 - DestrFnApArgs vals1 val1 == DestrFnApArgs vals2 val2 = vals1 == vals2 && val1 == val2 - TConArgs vals1 tag1 == TConArgs vals2 tag2 = vals1 == vals2 && tag1 == tag2 - _ == _ = False - -instance Ord Value where - VNum int1 <= VNum int2 = int1 <= int2 - VChar char1 <= VChar char2 = char1 <= char2 - VBool bool1 <= VBool bool2 = bool1 <= bool2 - VTuple values1 <= VTuple values2 = values1 <= values2 - VRecord pairs1 <= VRecord pairs2 = pairs1 <= pairs2 - VUnit <= VUnit = True - Adt tag1 values1 <= Adt tag2 values2 = tag1 <= tag2 && values1 <= values2 - FnApArgs pairs1 <= FnApArgs pairs2 = pairs1 <= pairs2 - DestrFnApArgs vals1 val1 <= DestrFnApArgs vals2 val2 = vals1 <= vals2 && val1 <= val2 - TConArgs vals1 tag1 <= TConArgs vals2 tag2 = vals1 <= vals2 && tag1 <= tag2 - _ <= _ = False diff --git a/src/Z3/Assertion.hs b/src/Z3/Assertion.hs deleted file mode 100644 --- a/src/Z3/Assertion.hs +++ /dev/null @@ -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 diff --git a/src/Z3/Class.hs b/src/Z3/Class.hs deleted file mode 100644 --- a/src/Z3/Class.hs +++ /dev/null @@ -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 diff --git a/src/Z3/Context.hs b/src/Z3/Context.hs deleted file mode 100644 --- a/src/Z3/Context.hs +++ /dev/null @@ -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) } diff --git a/src/Z3/Encoding.hs b/src/Z3/Encoding.hs deleted file mode 100644 --- a/src/Z3/Encoding.hs +++ /dev/null @@ -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 diff --git a/src/Z3/Logic.hs b/src/Z3/Logic.hs deleted file mode 100644 --- a/src/Z3/Logic.hs +++ /dev/null @@ -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) diff --git a/test/EvalSpec.hs b/test/EvalSpec.hs --- a/test/EvalSpec.hs +++ b/test/EvalSpec.hs @@ -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 diff --git a/test/InferSpec.hs b/test/InferSpec.hs --- a/test/InferSpec.hs +++ b/test/InferSpec.hs @@ -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 diff --git a/test/ParserSpec.hs b/test/ParserSpec.hs --- a/test/ParserSpec.hs +++ b/test/ParserSpec.hs @@ -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