forked from GitHub/gf-core
hopefully complete and correct typechecker in PGF
This commit is contained in:
krasimir
@@ -32,6 +32,7 @@ import GF.Command.TreeOperations ---- temporary place for typecheck and compute
|
||||
import GF.Data.Operations
|
||||
import GF.Text.Coding
|
||||
|
||||
import Data.List
|
||||
import Data.Maybe
|
||||
import qualified Data.Map as Map
|
||||
import System.Cmd
|
||||
@@ -283,7 +284,7 @@ allCommands cod env@(pgf, mos) = Map.fromList [
|
||||
_ | isOpt "changes" opts -> changesMsg
|
||||
_ | isOpt "coding" opts -> codingMsg
|
||||
_ | isOpt "license" opts -> licenseMsg
|
||||
[t] -> let co = getCommandOp (showExpr t) in
|
||||
[t] -> let co = getCommandOp (showExpr [] t) in
|
||||
case lookCommand co (allCommands cod env) of ---- new map ??!!
|
||||
Just info -> commandHelp True (co,info)
|
||||
_ -> "command not found"
|
||||
@@ -615,23 +616,29 @@ allCommands cod env@(pgf, mos) = Map.fromList [
|
||||
],
|
||||
exec = \opts arg -> do
|
||||
case arg of
|
||||
[EVar id] -> case Map.lookup id (funs (abstract pgf)) of
|
||||
[EFun id] -> case Map.lookup id (funs (abstract pgf)) of
|
||||
Just (ty,_,eqs) -> return $ fromString $
|
||||
render (text "fun" <+> text (prCId id) <+> colon <+> ppType 0 ty $$
|
||||
render (text "fun" <+> text (prCId id) <+> colon <+> ppType 0 [] ty $$
|
||||
if null eqs
|
||||
then empty
|
||||
else text "def" <+> vcat [text (prCId id) <+> hsep (map (ppPatt 9) patts) <+> char '=' <+> ppExpr 0 res | Equ patts res <- eqs])
|
||||
else text "def" <+> vcat [let (scope,ds) = mapAccumL (ppPatt 9) [] patts
|
||||
in text (prCId id) <+> hsep ds <+> char '=' <+> ppExpr 0 scope res | Equ patts res <- eqs])
|
||||
Nothing -> case Map.lookup id (cats (abstract pgf)) of
|
||||
Just hyps -> do return $ fromString $
|
||||
render (text "cat" <+> text (prCId id) <+> hsep (map ppHypo hyps) $$
|
||||
render (text "cat" <+> text (prCId id) <+> hsep (snd (mapAccumL ppHypo [] hyps)) $$
|
||||
if null (functionsToCat pgf id)
|
||||
then empty
|
||||
else space $$
|
||||
text "fun" <+> vcat [text (prCId fid) <+> colon <+> ppType 0 ty
|
||||
text "fun" <+> vcat [text (prCId fid) <+> colon <+> ppType 0 [] ty
|
||||
| (fid,ty) <- functionsToCat pgf id])
|
||||
Nothing -> do putStrLn "unknown identifier"
|
||||
return void
|
||||
_ -> do putStrLn "a single identifier is expected from the command"
|
||||
[e] -> case inferExpr pgf e of
|
||||
Left tcErr -> error $ render (ppTcError tcErr)
|
||||
Right (e,ty) -> do putStrLn ("Expression: "++showExpr [] e)
|
||||
putStrLn ("Type: "++showType [] ty)
|
||||
return void
|
||||
_ -> do putStrLn "a single identifier or expression is expected from the command"
|
||||
return void
|
||||
})
|
||||
]
|
||||
@@ -689,7 +696,9 @@ allCommands cod env@(pgf, mos) = Map.fromList [
|
||||
optType opts =
|
||||
let str = valStrOpts "cat" (prCId $ lookStartCat pgf) opts
|
||||
in case readType str of
|
||||
Just ty -> ty
|
||||
Just ty -> case checkType pgf ty of
|
||||
Left tcErr -> error $ render (ppTcError tcErr)
|
||||
Right ty -> ty
|
||||
Nothing -> error ("Can't parse '"++str++"' as type")
|
||||
optComm opts = valStrOpts "command" "" opts
|
||||
optViewFormat opts = valStrOpts "format" "png" opts
|
||||
@@ -710,10 +719,10 @@ allCommands cod env@(pgf, mos) = Map.fromList [
|
||||
|
||||
returnFromExprs es = return $ case es of
|
||||
[] -> ([], "no trees found")
|
||||
_ -> (es,unlines (map showExpr es))
|
||||
_ -> (es,unlines (map (showExpr []) es))
|
||||
|
||||
prGrammar opts
|
||||
| isOpt "cats" opts = return $ fromString $ unwords $ map showType $ categories pgf
|
||||
| isOpt "cats" opts = return $ fromString $ unwords $ map (showType []) $ categories pgf
|
||||
| isOpt "fullform" opts = return $ fromString $ concatMap (prFullFormLexicon . morpho) $ optLangs opts
|
||||
| isOpt "missing" opts = return $ fromString $ unlines $ [unwords (prCId la:":": map prCId cs) |
|
||||
la <- optLangs opts, let cs = missingLins pgf la]
|
||||
@@ -739,7 +748,7 @@ allCommands cod env@(pgf, mos) = Map.fromList [
|
||||
|
||||
showAsString t = case t of
|
||||
ELit (LStr s) -> s
|
||||
_ -> "\n" ++ showExpr t --- newline needed in other cases than the first
|
||||
_ -> "\n" ++ showExpr [] t --- newline needed in other cases than the first
|
||||
|
||||
stringOpOptions = sort $ [
|
||||
("bind","bind tokens separated by Prelude.BIND, i.e. &+"),
|
||||
|
||||
@@ -12,14 +12,13 @@ import GF.Command.Abstract
|
||||
import GF.Command.Parse
|
||||
import PGF
|
||||
import PGF.Data
|
||||
import PGF.Macros
|
||||
import PGF.Morphology
|
||||
import GF.System.Signal
|
||||
import GF.Infra.UseIO
|
||||
import GF.Infra.Option
|
||||
|
||||
import GF.Data.ErrM ----
|
||||
|
||||
import Text.PrettyPrint
|
||||
import Control.Monad.Error
|
||||
import qualified Data.Map as Map
|
||||
|
||||
data CommandEnv = CommandEnv {
|
||||
@@ -43,12 +42,6 @@ interpretCommandLine enc env line =
|
||||
case readCommandLine line of
|
||||
Just [] -> return ()
|
||||
Just pipes -> mapM_ (interpretPipe enc env) pipes
|
||||
{-
|
||||
Just pipes -> do res <- runInterruptibly (mapM_ (interpretPipe enc env) pipes)
|
||||
case res of
|
||||
Left ex -> putStrLnFlush $ enc (show ex)
|
||||
Right x -> return x
|
||||
-}
|
||||
Nothing -> putStrLnFlush "command not parsed"
|
||||
|
||||
interpretPipe enc env cs = do
|
||||
@@ -60,12 +53,15 @@ interpretPipe enc env cs = do
|
||||
intercs (trees,_) (c:cs) = do
|
||||
treess2 <- interc trees c
|
||||
intercs treess2 cs
|
||||
interc es comm@(Command co _ arg) = case co of
|
||||
interc es comm@(Command co opts arg) = case co of
|
||||
'%':f -> case Map.lookup f (commandmacros env) of
|
||||
Just css -> do
|
||||
mapM_ (interpretPipe enc env) (appLine (getCommandArg env arg es) css)
|
||||
return ([],[]) ---- return ?
|
||||
_ -> do
|
||||
Just css ->
|
||||
case getCommandTrees env arg es of
|
||||
Right es -> do mapM_ (interpretPipe enc env) (appLine es css)
|
||||
return ([],[])
|
||||
Left msg -> do putStrLn ('\n':msg)
|
||||
return ([],[])
|
||||
Nothing -> do
|
||||
putStrLn $ "command macro " ++ co ++ " not interpreted"
|
||||
return ([],[])
|
||||
_ -> interpret enc env es comm
|
||||
@@ -82,43 +78,53 @@ appCommand xs c@(Command i os arg) = case arg of
|
||||
EApp e1 e2 -> EApp (app e1) (app e2)
|
||||
ELit l -> ELit l
|
||||
EMeta i -> xs !! i
|
||||
EVar x -> EVar x
|
||||
EFun x -> EFun x
|
||||
|
||||
-- return the trees to be sent in pipe, and the output possibly printed
|
||||
interpret :: (String -> String) -> CommandEnv -> [Expr] -> Command -> IO CommandOutput
|
||||
interpret enc env trees0 comm = case lookCommand co comms of
|
||||
Just info -> do
|
||||
checkOpts info
|
||||
tss@(_,s) <- exec info opts trees
|
||||
optTrace $ enc s
|
||||
return tss
|
||||
_ -> do
|
||||
putStrLn $ "command " ++ co ++ " not interpreted"
|
||||
return ([],[])
|
||||
where
|
||||
optTrace = if isOpt "tr" opts then putStrLn else const (return ())
|
||||
(co,opts,trees) = getCommand env comm trees0
|
||||
comms = commands env
|
||||
checkOpts info =
|
||||
case
|
||||
[o | OOpt o <- opts, notElem o ("tr" : map fst (options info))] ++
|
||||
[o | OFlag o _ <- opts, notElem o (map fst (flags info))]
|
||||
of
|
||||
[] -> return ()
|
||||
[o] -> putStrLn $ "option not interpreted: " ++ o
|
||||
os -> putStrLn $ "options not interpreted: " ++ unwords os
|
||||
interpret enc env trees comm =
|
||||
case getCommand env trees comm of
|
||||
Left msg -> do putStrLn ('\n':msg)
|
||||
return ([],[])
|
||||
Right (info,opts,trees) -> do tss@(_,s) <- exec info opts trees
|
||||
if isOpt "tr" opts
|
||||
then putStrLn (enc s)
|
||||
else return ()
|
||||
return tss
|
||||
|
||||
-- analyse command parse tree to a uniform datastructure, normalizing comm name
|
||||
--- the env is needed for macro lookup
|
||||
getCommand :: CommandEnv -> Command -> [Expr] -> (String,[Option],[Expr])
|
||||
getCommand env co@(Command c opts arg) ts =
|
||||
(getCommandOp c,opts,getCommandArg env arg ts)
|
||||
getCommand :: CommandEnv -> [Expr] -> Command -> Either String (CommandInfo,[Option],[Expr])
|
||||
getCommand env es co@(Command c opts arg) = do
|
||||
info <- getCommandInfo env c
|
||||
checkOpts info opts
|
||||
es <- getCommandTrees env arg es
|
||||
return (info,opts,es)
|
||||
|
||||
getCommandArg :: CommandEnv -> Argument -> [Expr] -> [Expr]
|
||||
getCommandArg env a ts = case a of
|
||||
AMacro m -> case Map.lookup m (expmacros env) of
|
||||
Just t -> [t]
|
||||
_ -> []
|
||||
AExpr t -> [t] -- ignore piped
|
||||
ANoArg -> ts -- use piped
|
||||
getCommandInfo :: CommandEnv -> String -> Either String CommandInfo
|
||||
getCommandInfo env cmd =
|
||||
case lookCommand (getCommandOp cmd) (commands env) of
|
||||
Just info -> return info
|
||||
Nothing -> fail $ "command " ++ cmd ++ " not interpreted"
|
||||
|
||||
checkOpts :: CommandInfo -> [Option] -> Either String ()
|
||||
checkOpts info opts =
|
||||
case
|
||||
[o | OOpt o <- opts, notElem o ("tr" : map fst (options info))] ++
|
||||
[o | OFlag o _ <- opts, notElem o (map fst (flags info))]
|
||||
of
|
||||
[] -> return ()
|
||||
[o] -> fail $ "option not interpreted: " ++ o
|
||||
os -> fail $ "options not interpreted: " ++ unwords os
|
||||
|
||||
getCommandTrees :: CommandEnv -> Argument -> [Expr] -> Either String [Expr]
|
||||
getCommandTrees env a es =
|
||||
case a of
|
||||
AMacro m -> case Map.lookup m (expmacros env) of
|
||||
Just e -> return [e]
|
||||
_ -> return []
|
||||
AExpr e -> case inferExpr (multigrammar env) e of
|
||||
Left tcErr -> fail $ render (ppTcError tcErr)
|
||||
Right (e,ty) -> return [e] -- ignore piped
|
||||
ANoArg -> return es -- use piped
|
||||
|
||||
|
||||
@@ -20,9 +20,7 @@ allTreeOps pgf = [
|
||||
("paraphrase",("paraphrase by using semantic definitions (def)",
|
||||
map tree2expr . nub . concatMap (paraphrase pgf . expr2tree))),
|
||||
("smallest",("sort trees from smallest to largest, in number of nodes",
|
||||
smallest)),
|
||||
("typecheck",("type check and solve metavariables; reject if incorrect",
|
||||
concatMap (typecheck pgf)))
|
||||
smallest))
|
||||
]
|
||||
|
||||
smallest :: [Expr] -> [Expr]
|
||||
@@ -31,35 +29,3 @@ smallest = sortBy (\t u -> compare (size t) (size u)) where
|
||||
EAbs _ e -> size e + 1
|
||||
EApp e1 e2 -> size e1 + size e2 + 1
|
||||
_ -> 1
|
||||
|
||||
{-
|
||||
toTree :: G.Term -> Tree
|
||||
toTree t = case M.termForm t of
|
||||
Ok (xx,f,aa) -> Abs xx (Fun f (map toTree aa))
|
||||
|
||||
fromTree :: Tree -> G.Term
|
||||
fromTree t = case t of
|
||||
Abs xx b -> M.mkAbs xx (fromTree b)
|
||||
Var x -> M.vr x
|
||||
Fun f ts -> M.mkApp f (map fromTree ts)
|
||||
-}
|
||||
|
||||
{-
|
||||
data Tree =
|
||||
Abs [CId] Tree -- ^ lambda abstraction. The list of variables is non-empty
|
||||
| Var CId -- ^ variable
|
||||
| Fun CId [Tree] -- ^ function application
|
||||
| Lit Literal -- ^ literal
|
||||
| Meta Int -- ^ meta variable
|
||||
|
||||
data Literal =
|
||||
LStr String -- ^ string constant
|
||||
| LInt Integer -- ^ integer constant
|
||||
| LFlt Double -- ^ floating point constant
|
||||
|
||||
mkType :: A.Type -> C.Type
|
||||
mkType t = case GM.typeForm t of
|
||||
Ok (hyps,(_,cat),args) -> C.DTyp (mkContext hyps) (i2i cat) (map mkExp args)
|
||||
|
||||
mkExp :: A.Term -> C.Expr
|
||||
-}
|
||||
|
||||
@@ -68,7 +68,7 @@ plAbstract (name, Abstr aflags funs cats _catfuns) =
|
||||
plCat :: (CId, [Hypo]) -> String
|
||||
plCat (cat, hypos) = plFact "cat" (plTypeWithHypos typ)
|
||||
where ((_,subst), hypos') = alphaConvert emptyEnv hypos
|
||||
args = reverse [EVar x | (_,x) <- subst]
|
||||
args = reverse [EFun x | (_,x) <- subst]
|
||||
typ = DTyp hypos' cat args
|
||||
|
||||
plFun :: (CId, (Type, Int, [Equation])) -> String
|
||||
@@ -119,7 +119,7 @@ instance PLPrint Hypo where
|
||||
plp (HypV var typ) = plOper ":" (plp var) (plp typ)
|
||||
|
||||
instance PLPrint Expr where
|
||||
plp (EVar x) = plp x
|
||||
plp (EFun x) = plp x
|
||||
plp (EAbs x e) = plOper "^" (plp x) (plp e)
|
||||
plp (EApp e e') = plOper " * " (plp e) (plp e')
|
||||
plp (ELit lit) = plp lit
|
||||
@@ -279,7 +279,7 @@ instance AlphaConvert Expr where
|
||||
alphaConvert env (EApp e1 e2) = (env'', EApp e1' e2')
|
||||
where (env', e1') = alphaConvert env e1
|
||||
(env'', e2') = alphaConvert env' e2
|
||||
alphaConvert env expr@(EVar i) = (env, maybe expr EVar (lookup i (snd env)))
|
||||
alphaConvert env expr@(EFun i) = (env, maybe expr EFun (lookup i (snd env)))
|
||||
alphaConvert env expr = (env, expr)
|
||||
|
||||
-- pattern variables are not alpha converted
|
||||
|
||||
@@ -70,17 +70,17 @@ canon2gfcc opts pars cgr@(M.MGrammar ((a,abm):cms)) =
|
||||
gflags = Map.empty
|
||||
aflags = Map.fromList [(mkCId f,x) | (f,x) <- optionsPGF (M.flags abm)]
|
||||
|
||||
mkDef (Just eqs) = [C.Equ (map mkPatt ps) (mkExp e) | (ps,e) <- eqs]
|
||||
mkDef (Just eqs) = [C.Equ ps' (mkExp scope' e) | (ps,e) <- eqs, let (scope',ps') = mapAccumL mkPatt [] ps]
|
||||
mkDef Nothing = []
|
||||
|
||||
mkArrity (Just a) = a
|
||||
mkArrity Nothing = 0
|
||||
|
||||
-- concretes
|
||||
lfuns = [(f', (mkType ty, mkArrity ma, mkDef pty)) |
|
||||
lfuns = [(f', (mkType [] ty, mkArrity ma, mkDef pty)) |
|
||||
(f,AbsFun (Just ty) ma pty) <- tree2list (M.jments abm), let f' = i2i f]
|
||||
funs = Map.fromAscList lfuns
|
||||
lcats = [(i2i c, mkContext cont) |
|
||||
lcats = [(i2i c, snd (mkContext [] cont)) |
|
||||
(c,AbsCat (Just cont) _) <- tree2list (M.jments abm)]
|
||||
cats = Map.fromAscList lcats
|
||||
catfuns = Map.fromList
|
||||
@@ -118,36 +118,45 @@ canon2gfcc opts pars cgr@(M.MGrammar ((a,abm):cms)) =
|
||||
i2i :: Ident -> CId
|
||||
i2i = CId . ident2bs
|
||||
|
||||
mkType :: A.Type -> C.Type
|
||||
mkType t = case GM.typeForm t of
|
||||
Ok (hyps,(_,cat),args) -> C.DTyp (mkContext hyps) (i2i cat) (map mkExp args)
|
||||
mkType :: [Ident] -> A.Type -> C.Type
|
||||
mkType scope t =
|
||||
case GM.typeForm t of
|
||||
Ok (hyps,(_,cat),args) -> let (scope',hyps') = mkContext scope hyps
|
||||
in C.DTyp hyps' (i2i cat) (map (mkExp scope') args)
|
||||
|
||||
mkExp :: A.Term -> C.Expr
|
||||
mkExp t = case GM.termForm t of
|
||||
Ok (xs,c,args) -> mkAbs xs (mkApp c (map mkExp args))
|
||||
mkExp :: [Ident] -> A.Term -> C.Expr
|
||||
mkExp scope t = case GM.termForm t of
|
||||
Ok (xs,c,args) -> mkAbs xs (mkApp (reverse xs++scope) c (map (mkExp scope) args))
|
||||
where
|
||||
mkAbs xs t = foldr (C.EAbs . i2i) t xs
|
||||
mkApp c args = case c of
|
||||
Q _ c -> foldl C.EApp (C.EVar (i2i c)) args
|
||||
QC _ c -> foldl C.EApp (C.EVar (i2i c)) args
|
||||
Vr x -> C.EVar (i2i x)
|
||||
mkApp scope c args = case c of
|
||||
Q _ c -> foldl C.EApp (C.EFun (i2i c)) args
|
||||
QC _ c -> foldl C.EApp (C.EFun (i2i c)) args
|
||||
Vr x -> case lookup x (zip scope [0..]) of
|
||||
Just i -> foldl C.EApp (C.EVar i) args
|
||||
Nothing -> foldl C.EApp (C.EMeta 0) args
|
||||
EInt i -> C.ELit (C.LInt i)
|
||||
EFloat f -> C.ELit (C.LFlt f)
|
||||
K s -> C.ELit (C.LStr s)
|
||||
Meta (MetaSymb i) -> C.EMeta i
|
||||
_ -> C.EMeta 0
|
||||
|
||||
mkPatt p = case p of
|
||||
A.PP _ c ps -> C.PApp (i2i c) (map mkPatt ps)
|
||||
A.PV x -> C.PVar (i2i x)
|
||||
A.PW -> C.PWild
|
||||
A.PInt i -> C.PLit (C.LInt i)
|
||||
A.PFloat f -> C.PLit (C.LFlt f)
|
||||
A.PString s -> C.PLit (C.LStr s)
|
||||
mkPatt scope p =
|
||||
case p of
|
||||
A.PP _ c ps -> let (scope',ps') = mapAccumL mkPatt scope ps
|
||||
in (scope',C.PApp (i2i c) ps')
|
||||
A.PV x -> (x:scope,C.PVar (i2i x))
|
||||
A.PW -> ( scope,C.PWild)
|
||||
A.PInt i -> ( scope,C.PLit (C.LInt i))
|
||||
A.PFloat f -> ( scope,C.PLit (C.LFlt f))
|
||||
A.PString s -> ( scope,C.PLit (C.LStr s))
|
||||
|
||||
|
||||
mkContext :: A.Context -> [C.Hypo]
|
||||
mkContext hyps = [(if x == identW then C.Hyp else C.HypV (i2i x)) (mkType ty) | (x,ty) <- hyps]
|
||||
mkContext :: [Ident] -> A.Context -> ([Ident],[C.Hypo])
|
||||
mkContext scope hyps = mapAccumL (\scope (x,ty) -> let ty' = mkType scope ty
|
||||
in if x == identW
|
||||
then ( scope,C.Hyp ty')
|
||||
else (x:scope,C.HypV (i2i x) ty')) scope hyps
|
||||
|
||||
mkTerm :: Term -> C.Term
|
||||
mkTerm tr = case tr of
|
||||
|
||||
11
src/PGF.hs
11
src/PGF.hs
@@ -9,7 +9,7 @@
|
||||
-- load and interpret grammars compiled in Portable Grammar Format (PGF).
|
||||
-- The PGF format is produced as a final output from the GF compiler.
|
||||
-- The API is meant to be used for embedding GF grammars in Haskell
|
||||
-- programs.
|
||||
-- programs
|
||||
-------------------------------------------------
|
||||
|
||||
module PGF(
|
||||
@@ -51,7 +51,11 @@ module PGF(
|
||||
parse, canParse, parseAllLang, parseAll,
|
||||
|
||||
-- ** Evaluation
|
||||
tree2expr, expr2tree, PGF.compute, paraphrase, typecheck,
|
||||
tree2expr, expr2tree, PGF.compute, paraphrase,
|
||||
|
||||
-- ** Type Checking
|
||||
checkType, checkExpr, inferExpr,
|
||||
ppTcError, TcError(..),
|
||||
|
||||
-- ** Word Completion (Incremental Parsing)
|
||||
complete,
|
||||
@@ -80,6 +84,7 @@ import GF.Data.Utilities (replace)
|
||||
|
||||
import Data.Char
|
||||
import qualified Data.Map as Map
|
||||
import qualified Data.IntMap as IntMap
|
||||
import Data.Maybe
|
||||
import Data.Binary
|
||||
import System.Random (newStdGen)
|
||||
@@ -307,4 +312,4 @@ complete pgf from typ input =
|
||||
|
||||
-- | Converts an expression to normal form
|
||||
compute :: PGF -> Expr -> Expr
|
||||
compute pgf = PGF.Data.normalForm (funs (abstract pgf))
|
||||
compute pgf = PGF.Data.normalForm (funs (abstract pgf)) 0 []
|
||||
|
||||
@@ -104,20 +104,24 @@ instance Binary Term where
|
||||
instance Binary Expr where
|
||||
put (EAbs x exp) = putWord8 0 >> put (x,exp)
|
||||
put (EApp e1 e2) = putWord8 1 >> put (e1,e2)
|
||||
put (EVar x) = putWord8 2 >> put x
|
||||
put (ELit (LStr s)) = putWord8 3 >> put s
|
||||
put (ELit (LFlt d)) = putWord8 4 >> put d
|
||||
put (ELit (LInt i)) = putWord8 5 >> put i
|
||||
put (EMeta i) = putWord8 6 >> put i
|
||||
put (ELit (LStr s)) = putWord8 2 >> put s
|
||||
put (ELit (LFlt d)) = putWord8 3 >> put d
|
||||
put (ELit (LInt i)) = putWord8 4 >> put i
|
||||
put (EMeta i) = putWord8 5 >> put i
|
||||
put (EFun f) = putWord8 6 >> put f
|
||||
put (EVar i) = putWord8 7 >> put i
|
||||
put (ETyped e ty) = putWord8 8 >> put (e,ty)
|
||||
get = do tag <- getWord8
|
||||
case tag of
|
||||
0 -> liftM2 EAbs get get
|
||||
1 -> liftM2 EApp get get
|
||||
2 -> liftM EVar get
|
||||
3 -> liftM (ELit . LStr) get
|
||||
4 -> liftM (ELit . LFlt) get
|
||||
5 -> liftM (ELit . LInt) get
|
||||
6 -> liftM EMeta get
|
||||
2 -> liftM (ELit . LStr) get
|
||||
3 -> liftM (ELit . LFlt) get
|
||||
4 -> liftM (ELit . LInt) get
|
||||
5 -> liftM EMeta get
|
||||
6 -> liftM EFun get
|
||||
7 -> liftM EVar get
|
||||
8 -> liftM2 ETyped get get
|
||||
_ -> decodingError
|
||||
|
||||
instance Binary Patt where
|
||||
|
||||
261
src/PGF/Expr.hs
261
src/PGF/Expr.hs
@@ -7,12 +7,12 @@ module PGF.Expr(Tree(..), Literal(..),
|
||||
tree2expr, expr2tree, normalForm,
|
||||
|
||||
-- needed in the typechecker
|
||||
Value(..), Env, eval, apply, eqValue,
|
||||
Value(..), Env, Funs, eval, apply,
|
||||
|
||||
MetaId,
|
||||
|
||||
-- helpers
|
||||
pStr,pFactor,
|
||||
pStr,pFactor,freshName,ppMeta
|
||||
) where
|
||||
|
||||
import PGF.CId
|
||||
@@ -20,16 +20,17 @@ import PGF.Type
|
||||
|
||||
import Data.Char
|
||||
import Data.Maybe
|
||||
import Data.List as List
|
||||
import Data.Map as Map hiding (showTree)
|
||||
import Control.Monad
|
||||
import qualified Text.PrettyPrint as PP
|
||||
import qualified Text.ParserCombinators.ReadP as RP
|
||||
import qualified Data.Map as Map
|
||||
|
||||
data Literal =
|
||||
LStr String -- ^ string constant
|
||||
| LInt Integer -- ^ integer constant
|
||||
| LFlt Double -- ^ floating point constant
|
||||
deriving (Eq,Ord)
|
||||
deriving (Eq,Ord,Show)
|
||||
|
||||
type MetaId = Int
|
||||
|
||||
@@ -52,9 +53,10 @@ data Expr =
|
||||
| EApp Expr Expr -- ^ application
|
||||
| ELit Literal -- ^ literal
|
||||
| EMeta {-# UNPACK #-} !MetaId -- ^ meta variable
|
||||
| EVar CId -- ^ variable or function reference
|
||||
| EPi CId Expr Expr -- ^ dependent function type
|
||||
deriving (Eq,Ord)
|
||||
| EFun CId -- ^ function or data constructor
|
||||
| EVar {-# UNPACK #-} !Int -- ^ variable with de Bruijn index
|
||||
| ETyped Expr Type
|
||||
deriving (Eq,Ord,Show)
|
||||
|
||||
-- | The pattern is used to define equations in the abstract syntax of the grammar.
|
||||
data Patt =
|
||||
@@ -94,12 +96,12 @@ readExpr s = case [x | (x,cs) <- RP.readP_to_S pExpr s, all isSpace cs] of
|
||||
[x] -> Just x
|
||||
_ -> Nothing
|
||||
|
||||
-- | renders expression as 'String'
|
||||
showExpr :: Expr -> String
|
||||
showExpr = PP.render . ppExpr 0
|
||||
|
||||
instance Show Expr where
|
||||
showsPrec i x = showString (PP.render (ppExpr i x))
|
||||
-- | renders expression as 'String'. The list
|
||||
-- of identifiers is the list of all free variables
|
||||
-- in the expression in order reverse to the order
|
||||
-- of binding.
|
||||
showExpr :: [CId] -> Expr -> String
|
||||
showExpr vars = PP.render . ppExpr 0 vars
|
||||
|
||||
instance Read Expr where
|
||||
readsPrec _ = RP.readP_to_S pExpr
|
||||
@@ -124,24 +126,31 @@ pTree isNested = RP.skipSpaces >> (pParen RP.<++ pAbs RP.<++ pApp RP.<++ fmap Li
|
||||
return (Fun f ts)
|
||||
|
||||
pExpr :: RP.ReadP Expr
|
||||
pExpr = RP.skipSpaces >> (pAbs RP.<++ pTerm)
|
||||
pExpr = pExpr0 >>= optTyped
|
||||
where
|
||||
pExpr0 = RP.skipSpaces >> (pAbs RP.<++ pTerm)
|
||||
|
||||
pTerm = fmap (foldl1 EApp) (RP.sepBy1 pFactor RP.skipSpaces)
|
||||
|
||||
pAbs = do xs <- RP.between (RP.char '\\') (RP.skipSpaces >> RP.string "->") (RP.sepBy1 (RP.skipSpaces >> pCId) (RP.skipSpaces >> RP.char ','))
|
||||
e <- pExpr
|
||||
e <- pExpr0
|
||||
return (foldr EAbs e xs)
|
||||
|
||||
pFactor = fmap EVar pCId
|
||||
optTyped e = do RP.skipSpaces
|
||||
RP.char ':'
|
||||
RP.skipSpaces
|
||||
ty <- pType
|
||||
return (ETyped e ty)
|
||||
RP.<++
|
||||
return e
|
||||
|
||||
pFactor = fmap EFun pCId
|
||||
RP.<++ fmap ELit pLit
|
||||
RP.<++ fmap EMeta pMeta
|
||||
RP.<++ RP.between (RP.char '(') (RP.char ')') pExpr
|
||||
|
||||
pMeta = do RP.char '?'
|
||||
cs <- RP.look
|
||||
case cs of
|
||||
(c:_) | isDigit c -> fmap read (RP.munch1 isDigit)
|
||||
_ -> return 0
|
||||
return 0
|
||||
|
||||
pLit :: RP.ReadP Literal
|
||||
pLit = pNum RP.<++ liftM LStr pStr
|
||||
@@ -161,35 +170,37 @@ pStr = RP.char '"' >> (RP.manyTill (pEsc RP.<++ RP.get) (RP.char '"'))
|
||||
-----------------------------------------------------
|
||||
|
||||
ppTree d (Abs xs t) = ppParens (d > 0) (PP.char '\\' PP.<>
|
||||
PP.hsep (PP.punctuate PP.comma (map (PP.text . prCId) xs)) PP.<+>
|
||||
PP.hsep (PP.punctuate PP.comma (List.map (PP.text . prCId) xs)) PP.<+>
|
||||
PP.text "->" PP.<+>
|
||||
ppTree 0 t)
|
||||
ppTree d (Fun f []) = PP.text (prCId f)
|
||||
ppTree d (Fun f ts) = ppParens (d > 0) (PP.text (prCId f) PP.<+> PP.hsep (map (ppTree 1) ts))
|
||||
ppTree d (Fun f ts) = ppParens (d > 0) (PP.text (prCId f) PP.<+> PP.hsep (List.map (ppTree 1) ts))
|
||||
ppTree d (Lit l) = ppLit l
|
||||
ppTree d (Meta n) = ppMeta n
|
||||
ppTree d (Var id) = PP.text (prCId id)
|
||||
|
||||
|
||||
ppExpr :: Int -> Expr -> PP.Doc
|
||||
ppExpr d (EAbs x e) = let (xs,e1) = getVars (EAbs x e)
|
||||
in ppParens (d > 0) (PP.char '\\' PP.<>
|
||||
PP.hsep (PP.punctuate PP.comma (map (PP.text . prCId) xs)) PP.<+>
|
||||
PP.text "->" PP.<+>
|
||||
ppExpr 0 e1)
|
||||
where
|
||||
getVars (EAbs x e) = let (xs,e1) = getVars e in (x:xs,e1)
|
||||
getVars e = ([],e)
|
||||
ppExpr d (EApp e1 e2) = ppParens (d > 1) ((ppExpr 1 e1) PP.<+> (ppExpr 2 e2))
|
||||
ppExpr d (ELit l) = ppLit l
|
||||
ppExpr d (EMeta n) = ppMeta n
|
||||
ppExpr d (EVar f) = PP.text (prCId f)
|
||||
ppExpr d (EPi x e1 e2)= PP.parens (PP.text (prCId x) PP.<+> PP.colon PP.<+> ppExpr 0 e1) PP.<+> PP.text "->" PP.<+> ppExpr 0 e2
|
||||
ppExpr :: Int -> [CId] -> Expr -> PP.Doc
|
||||
ppExpr d scope (EAbs x e) = let (xs,e1) = getVars [x] e
|
||||
in ppParens (d > 1) (PP.char '\\' PP.<>
|
||||
PP.hsep (PP.punctuate PP.comma (List.map (PP.text . prCId) (reverse xs))) PP.<+>
|
||||
PP.text "->" PP.<+>
|
||||
ppExpr 1 (xs++scope) e1)
|
||||
where
|
||||
getVars xs (EAbs x e) = getVars (freshName x xs:xs) e
|
||||
getVars xs e = (xs,e)
|
||||
ppExpr d scope (EApp e1 e2) = ppParens (d > 3) ((ppExpr 3 scope e1) PP.<+> (ppExpr 4 scope e2))
|
||||
ppExpr d scope (ELit l) = ppLit l
|
||||
ppExpr d scope (EMeta n) = ppMeta n
|
||||
ppExpr d scope (EFun f) = PP.text (prCId f)
|
||||
ppExpr d scope (EVar i) = PP.text (prCId (scope !! i))
|
||||
ppExpr d scope (ETyped e ty)= ppParens (d > 0) (ppExpr 0 scope e PP.<+> PP.colon PP.<+> ppType 0 scope ty)
|
||||
|
||||
ppPatt d (PApp f ps) = ppParens (d > 1) (PP.text (prCId f) PP.<+> PP.hsep (map (ppPatt 2) ps))
|
||||
ppPatt d (PLit l) = ppLit l
|
||||
ppPatt d (PVar f) = PP.text (prCId f)
|
||||
ppPatt d PWild = PP.char '_'
|
||||
ppPatt d scope (PApp f ps) = let (scope',ds) = mapAccumL (ppPatt 2) scope ps
|
||||
in (scope',ppParens (not (List.null ps) && d > 1) (PP.text (prCId f) PP.<+> PP.hsep ds))
|
||||
ppPatt d scope (PLit l) = (scope,ppLit l)
|
||||
ppPatt d scope (PVar f) = (scope,PP.text (prCId f))
|
||||
ppPatt d scope PWild = (scope,PP.char '_')
|
||||
|
||||
ppLit (LStr s) = PP.text (show s)
|
||||
ppLit (LInt n) = PP.integer n
|
||||
@@ -203,6 +214,12 @@ ppMeta n
|
||||
ppParens True = PP.parens
|
||||
ppParens False = id
|
||||
|
||||
freshName :: CId -> [CId] -> CId
|
||||
freshName x xs = loop 1 x
|
||||
where
|
||||
loop i y
|
||||
| elem y xs = loop (i+1) (mkCId (show x++"'"++show i))
|
||||
| otherwise = y
|
||||
|
||||
-----------------------------------------------------
|
||||
-- Conversion Expr <-> Tree
|
||||
@@ -211,33 +228,38 @@ ppParens False = id
|
||||
-- | Converts a tree to expression. The conversion
|
||||
-- is always total, every tree is a valid expression.
|
||||
tree2expr :: Tree -> Expr
|
||||
tree2expr (Fun x ts) = foldl EApp (EVar x) (map tree2expr ts)
|
||||
tree2expr (Lit l) = ELit l
|
||||
tree2expr (Meta n) = EMeta n
|
||||
tree2expr (Abs xs t) = foldr EAbs (tree2expr t) xs
|
||||
tree2expr (Var x) = EVar x
|
||||
tree2expr = tree2expr []
|
||||
where
|
||||
tree2expr ys (Fun x ts) = foldl EApp (EFun x) (List.map (tree2expr ys) ts)
|
||||
tree2expr ys (Lit l) = ELit l
|
||||
tree2expr ys (Meta n) = EMeta n
|
||||
tree2expr ys (Abs xs t) = foldr EAbs (tree2expr (reverse xs++ys) t) xs
|
||||
tree2expr ys (Var x) = case List.lookup x (zip ys [0..]) of
|
||||
Just i -> EVar i
|
||||
Nothing -> error "unknown variable"
|
||||
|
||||
-- | Converts an expression to tree. The conversion is only partial.
|
||||
-- Variables and meta variables of function type and beta redexes are not allowed.
|
||||
expr2tree :: Expr -> Tree
|
||||
expr2tree e = abs [] [] e
|
||||
where
|
||||
abs ys xs (EAbs x e) = abs ys (x:xs) e
|
||||
abs ys xs e = case xs of
|
||||
[] -> app ys [] e
|
||||
xs -> Abs (reverse xs) (app (xs++ys) [] e)
|
||||
abs ys xs (EAbs x e) = abs ys (x:xs) e
|
||||
abs ys xs (ETyped e _) = abs ys xs e
|
||||
abs ys xs e = case xs of
|
||||
[] -> app ys [] e
|
||||
xs -> Abs (reverse xs) (app (xs++ys) [] e)
|
||||
|
||||
app xs as (EApp e1 e2) = app xs ((abs xs [] e2) : as) e1
|
||||
app xs as (EApp e1 e2) = app xs ((abs xs [] e2) : as) e1
|
||||
app xs as (ELit l)
|
||||
| null as = Lit l
|
||||
| otherwise = error "literal of function type encountered"
|
||||
| List.null as = Lit l
|
||||
| otherwise = error "literal of function type encountered"
|
||||
app xs as (EMeta n)
|
||||
| null as = Meta n
|
||||
| otherwise = error "meta variables of function type are not allowed in trees"
|
||||
app xs as (EAbs x e) = error "beta redexes are not allowed in trees"
|
||||
app xs as (EVar x)
|
||||
| x `elem` xs = Var x
|
||||
| otherwise = Fun x as
|
||||
| List.null as = Meta n
|
||||
| otherwise = error "meta variables of function type are not allowed in trees"
|
||||
app xs as (EAbs x e) = error "beta redexes are not allowed in trees"
|
||||
app xs as (EVar i) = Var (xs !! i)
|
||||
app xs as (EFun f) = Fun f as
|
||||
app xs as (ETyped e _) = app xs as e
|
||||
|
||||
|
||||
-----------------------------------------------------
|
||||
@@ -245,109 +267,84 @@ expr2tree e = abs [] [] e
|
||||
-----------------------------------------------------
|
||||
|
||||
-- | Compute an expression to normal form
|
||||
normalForm :: Funs -> Expr -> Expr
|
||||
normalForm funs e = value2expr 0 (eval funs Map.empty e)
|
||||
normalForm :: Funs -> Int -> Env -> Expr -> Expr
|
||||
normalForm funs k env e = value2expr k (eval funs env e)
|
||||
where
|
||||
value2expr i (VApp f vs) = foldl EApp (EVar f) (map (value2expr i) vs)
|
||||
value2expr i (VGen j vs) = foldl EApp (EVar (var j)) (map (value2expr i) vs)
|
||||
value2expr i (VMeta j vs) = foldl EApp (EMeta j) (map (value2expr i) vs)
|
||||
value2expr i (VSusp j vs k) = value2expr i (k (VGen j vs))
|
||||
value2expr i (VApp f vs) = foldl EApp (EFun f) (List.map (value2expr i) vs)
|
||||
value2expr i (VGen j vs) = foldl EApp (EVar (i-j-1)) (List.map (value2expr i) vs)
|
||||
value2expr i (VMeta j env vs) = foldl EApp (EMeta j) (List.map (value2expr i) vs)
|
||||
value2expr i (VSusp j env vs k) = value2expr i (k (VGen j vs))
|
||||
value2expr i (VLit l) = ELit l
|
||||
value2expr i (VClosure env (EAbs x e)) = EAbs (var i) (value2expr (i+1) (eval funs (Map.insert x (VGen i []) env) e))
|
||||
|
||||
var i = mkCId ('v':show i)
|
||||
|
||||
ret [] t = t
|
||||
ret xs t = Abs (reverse xs) t
|
||||
value2expr i (VClosure env (EAbs x e)) = EAbs x (value2expr (i+1) (eval funs ((VGen i []):env) e))
|
||||
|
||||
data Value
|
||||
= VApp CId [Value]
|
||||
| VLit Literal
|
||||
| VMeta {-# UNPACK #-} !MetaId [Value]
|
||||
| VGen {-# UNPACK #-} !MetaId [Value]
|
||||
| VSusp {-# UNPACK #-} !MetaId [Value] (Value -> Value)
|
||||
| VMeta {-# UNPACK #-} !MetaId Env [Value]
|
||||
| VSusp {-# UNPACK #-} !MetaId Env [Value] (Value -> Value)
|
||||
| VGen {-# UNPACK #-} !Int [Value]
|
||||
| VClosure Env Expr
|
||||
|
||||
type Funs = Map.Map CId (Type,Int,[Equation]) -- type and def of a fun
|
||||
type Env = Map.Map CId Value
|
||||
type Env = [Value]
|
||||
|
||||
eval :: Funs -> Env -> Expr -> Value
|
||||
eval funs env (EVar x) = case Map.lookup x env of
|
||||
Just v -> v
|
||||
Nothing -> case Map.lookup x funs of
|
||||
Just (_,a,eqs) -> if a == 0
|
||||
then case eqs of
|
||||
Equ [] e : _ -> eval funs Map.empty e
|
||||
_ -> VApp x []
|
||||
else VApp x []
|
||||
Nothing -> error ("unknown variable "++prCId x)
|
||||
eval funs env (EVar i) = env !! i
|
||||
eval funs env (EFun f) = case Map.lookup f funs of
|
||||
Just (_,a,eqs) -> if a == 0
|
||||
then case eqs of
|
||||
Equ [] e : _ -> eval funs [] e
|
||||
_ -> VApp f []
|
||||
else VApp f []
|
||||
Nothing -> error ("unknown function "++prCId f)
|
||||
eval funs env (EApp e1 e2) = apply funs env e1 [eval funs env e2]
|
||||
eval funs env (EAbs x e) = VClosure env (EAbs x e)
|
||||
eval funs env (EMeta k) = VMeta k []
|
||||
eval funs env (EMeta i) = VMeta i env []
|
||||
eval funs env (ELit l) = VLit l
|
||||
eval funs env (EPi x e1 e2)= VClosure env (EPi x e1 e2)
|
||||
eval funs env (ETyped e _) = eval funs env e
|
||||
|
||||
apply :: Funs -> Env -> Expr -> [Value] -> Value
|
||||
apply funs env e [] = eval funs env e
|
||||
apply funs env (EVar x) vs = case Map.lookup x env of
|
||||
Just v -> applyValue funs env v vs
|
||||
Nothing -> case Map.lookup x funs of
|
||||
Just (_,a,eqs) -> if a <= length vs
|
||||
then let (as,vs') = splitAt a vs
|
||||
in match funs x eqs as vs'
|
||||
else VApp x vs
|
||||
Nothing -> error ("unknown variable "++prCId x)
|
||||
apply funs env (EVar i) vs = applyValue funs (env !! i) vs
|
||||
apply funs env (EFun f) vs = case Map.lookup f funs of
|
||||
Just (_,a,eqs) -> if a <= length vs
|
||||
then let (as,vs') = splitAt a vs
|
||||
in match funs f eqs as vs'
|
||||
else VApp f vs
|
||||
Nothing -> error ("unknown function "++prCId f)
|
||||
apply funs env (EApp e1 e2) vs = apply funs env e1 (eval funs env e2 : vs)
|
||||
apply funs env (EAbs x e) (v:vs) = apply funs (Map.insert x v env) e vs
|
||||
apply funs env (EMeta k) vs = VMeta k vs
|
||||
apply funs env (EAbs x e) (v:vs) = apply funs (v:env) e vs
|
||||
apply funs env (EMeta i) vs = VMeta i env vs
|
||||
apply funs env (ELit l) vs = error "literal of function type"
|
||||
apply funs env (ETyped e _) vs = apply funs env e vs
|
||||
|
||||
applyValue funs env (VApp f vs0) vs = apply funs env (EVar f) (vs0++vs)
|
||||
applyValue funs env (VLit _) vs = error "literal of function type"
|
||||
applyValue funs env (VMeta i vs0) vs = VMeta i (vs0++vs)
|
||||
applyValue funs env (VGen i vs0) vs = VGen i (vs0++vs)
|
||||
applyValue funs env (VSusp i vs0 k) vs = VSusp i vs0 (\v -> applyValue funs env (k v) vs)
|
||||
applyValue funs _ (VClosure env (EAbs x e)) (v:vs) = apply funs (Map.insert x v env) e vs
|
||||
applyValue funs v [] = v
|
||||
applyValue funs (VApp f vs0) vs = apply funs [] (EFun f) (vs0++vs)
|
||||
applyValue funs (VLit _) vs = error "literal of function type"
|
||||
applyValue funs (VMeta i env vs0) vs = VMeta i env (vs0++vs)
|
||||
applyValue funs (VGen i vs0) vs = VGen i (vs0++vs)
|
||||
applyValue funs (VSusp i env vs0 k) vs = VSusp i env vs0 (\v -> applyValue funs (k v) vs)
|
||||
applyValue funs (VClosure env (EAbs x e)) (v:vs) = apply funs (v:env) e vs
|
||||
|
||||
-----------------------------------------------------
|
||||
-- Pattern matching
|
||||
-----------------------------------------------------
|
||||
|
||||
match :: Funs -> CId -> [Equation] -> [Value] -> [Value] -> Value
|
||||
match funs f eqs as0 vs0 =
|
||||
match sig f eqs as0 vs0 =
|
||||
case eqs of
|
||||
[] -> VApp f (as0++vs0)
|
||||
(Equ ps res):eqs -> tryMatches eqs ps as0 res Map.empty
|
||||
(Equ ps res):eqs -> tryMatches eqs ps as0 res []
|
||||
where
|
||||
tryMatches eqs [] [] res env = apply funs env res vs0
|
||||
tryMatches eqs [] [] res env = apply sig env res vs0
|
||||
tryMatches eqs (p:ps) (a:as) res env = tryMatch p a env
|
||||
where
|
||||
tryMatch (PVar x ) (v ) env = tryMatches eqs ps as res (Map.insert x v env)
|
||||
tryMatch (PWild ) (_ ) env = tryMatches eqs ps as res env
|
||||
tryMatch (p ) (VMeta i vs ) env = VSusp i vs (\v -> tryMatch p v env)
|
||||
tryMatch (p ) (VGen i vs ) env = VApp f (as0++vs0)
|
||||
tryMatch (p ) (VSusp i vs k) env = VSusp i vs (\v -> tryMatch p (k v) env)
|
||||
tryMatch (PApp f1 ps1) (VApp f2 vs2 ) env | f1 == f2 = tryMatches eqs (ps1++ps) (vs2++as) res env
|
||||
tryMatch (PLit l1 ) (VLit l2 ) env | l1 == l2 = tryMatches eqs ps as res env
|
||||
tryMatch _ _ env = match funs f eqs as0 vs0
|
||||
|
||||
|
||||
-----------------------------------------------------
|
||||
-- Equality checking
|
||||
-----------------------------------------------------
|
||||
|
||||
eqValue :: Funs -> Int -> Value -> Value -> [(Value,Value)]
|
||||
eqValue funs k v1 v2 =
|
||||
case (whnf v1,whnf v2) of
|
||||
(VApp f1 vs1, VApp f2 vs2) | f1 == f2 -> concat (zipWith (eqValue funs k) vs1 vs2)
|
||||
(VLit l1, VLit l2 ) | l1 == l2 -> []
|
||||
(VMeta i vs1, VMeta j vs2) | i == j -> concat (zipWith (eqValue funs k) vs1 vs2)
|
||||
(VGen i vs1, VGen j vs2) | i == j -> concat (zipWith (eqValue funs k) vs1 vs2)
|
||||
(VClosure env1 (EAbs x1 e1), VClosure env2 (EAbs x2 e2)) ->
|
||||
let v = VGen k []
|
||||
in eqValue funs (k+1) (VClosure (Map.insert x1 v env1) e1) (VClosure (Map.insert x2 v env2) e2)
|
||||
_ -> [(v1,v2)]
|
||||
where
|
||||
whnf (VClosure env e) = eval funs env e -- should be removed when the typechecker is improved
|
||||
whnf v = v
|
||||
tryMatch (PVar x ) (v ) env = tryMatches eqs ps as res (v:env)
|
||||
tryMatch (PWild ) (_ ) env = tryMatches eqs ps as res env
|
||||
tryMatch (p ) (VMeta i envi vs ) env = VSusp i envi vs (\v -> tryMatch p v env)
|
||||
tryMatch (p ) (VGen i vs ) env = VApp f (as0++vs0)
|
||||
tryMatch (p ) (VSusp i envi vs k) env = VSusp i envi vs (\v -> tryMatch p (k v) env)
|
||||
tryMatch (PApp f1 ps1) (VApp f2 vs2 ) env | f1 == f2 = tryMatches eqs (ps1++ps) (vs2++as) res env
|
||||
tryMatch (PLit l1 ) (VLit l2 ) env | l1 == l2 = tryMatches eqs ps as res env
|
||||
tryMatch _ _ env = match sig f eqs as0 vs0
|
||||
|
||||
|
||||
@@ -1,13 +1,17 @@
|
||||
module PGF.Expr where
|
||||
|
||||
import PGF.CId
|
||||
import qualified Text.PrettyPrint as PP
|
||||
import qualified Text.ParserCombinators.ReadP as RP
|
||||
|
||||
data Expr
|
||||
|
||||
instance Eq Expr
|
||||
instance Ord Expr
|
||||
instance Eq Expr
|
||||
instance Ord Expr
|
||||
instance Show Expr
|
||||
|
||||
pFactor :: RP.ReadP Expr
|
||||
|
||||
ppExpr :: Int -> Expr -> PP.Doc
|
||||
ppExpr :: Int -> [CId] -> Expr -> PP.Doc
|
||||
|
||||
freshName :: CId -> [CId] -> CId
|
||||
@@ -5,22 +5,22 @@ module PGF.Type ( Type(..), Hypo(..),
|
||||
import PGF.CId
|
||||
import {-# SOURCE #-} PGF.Expr
|
||||
import Data.Char
|
||||
import Data.List
|
||||
import qualified Text.PrettyPrint as PP
|
||||
import qualified Text.ParserCombinators.ReadP as RP
|
||||
import Control.Monad
|
||||
import Debug.Trace
|
||||
|
||||
-- | To read a type from a 'String', use 'read' or 'readType'.
|
||||
data Type =
|
||||
DTyp [Hypo] CId [Expr]
|
||||
deriving (Eq,Ord)
|
||||
deriving (Eq,Ord,Show)
|
||||
|
||||
-- | 'Hypo' represents a hypothesis in a type i.e. in the type A -> B, A is the hypothesis
|
||||
data Hypo =
|
||||
Hyp Type -- ^ hypothesis without bound variable like in A -> B
|
||||
| HypV CId Type -- ^ hypothesis with bound variable like in (x : A) -> B x
|
||||
| HypI CId Type -- ^ hypothesis with bound implicit variable like in {x : A} -> B x
|
||||
deriving (Eq,Ord)
|
||||
deriving (Eq,Ord,Show)
|
||||
|
||||
-- | Reads a 'Type' from a 'String'.
|
||||
readType :: String -> Maybe Type
|
||||
@@ -28,15 +28,12 @@ readType s = case [x | (x,cs) <- RP.readP_to_S pType s, all isSpace cs] of
|
||||
[x] -> Just x
|
||||
_ -> Nothing
|
||||
|
||||
instance Show Type where
|
||||
showsPrec i x = showString (PP.render (ppType i x))
|
||||
|
||||
instance Read Type where
|
||||
readsPrec _ = RP.readP_to_S pType
|
||||
|
||||
-- | renders type as 'String'
|
||||
showType :: Type -> String
|
||||
showType = PP.render . ppType 0
|
||||
-- | renders type as 'String'. The list
|
||||
-- of identifiers is the list of all free variables
|
||||
-- in the expression in order reverse to the order
|
||||
-- of binding.
|
||||
showType :: [CId] -> Type -> String
|
||||
showType vars = PP.render . ppType 0 vars
|
||||
|
||||
pType :: RP.ReadP Type
|
||||
pType = do
|
||||
@@ -72,17 +69,19 @@ pType = do
|
||||
args <- RP.sepBy pFactor RP.skipSpaces
|
||||
return (cat, args)
|
||||
|
||||
ppType :: Int -> Type -> PP.Doc
|
||||
ppType d (DTyp ctxt cat args)
|
||||
| null ctxt = ppRes cat args
|
||||
| otherwise = ppParens (d > 0) (foldr ppCtxt (ppRes cat args) ctxt)
|
||||
ppType :: Int -> [CId] -> Type -> PP.Doc
|
||||
ppType d scope (DTyp hyps cat args)
|
||||
| null hyps = ppRes scope cat args
|
||||
| otherwise = let (scope',hdocs) = mapAccumL ppHypo scope hyps
|
||||
in ppParens (d > 0) (foldr (\hdoc doc -> hdoc PP.<+> PP.text "->" PP.<+> doc) (ppRes scope' cat args) hdocs)
|
||||
where
|
||||
ppCtxt hyp doc = ppHypo hyp PP.<+> PP.text "->" PP.<+> doc
|
||||
ppRes cat es = PP.text (prCId cat) PP.<+> PP.hsep (map (ppExpr 2) es)
|
||||
ppRes scope cat es = PP.text (prCId cat) PP.<+> PP.hsep (map (ppExpr 4 scope) es)
|
||||
|
||||
ppHypo (Hyp typ) = ppType 1 typ
|
||||
ppHypo (HypV x typ) = PP.parens (PP.text (prCId x) PP.<+> PP.char ':' PP.<+> ppType 0 typ)
|
||||
ppHypo (HypI x typ) = PP.braces (PP.text (prCId x) PP.<+> PP.char ':' PP.<+> ppType 0 typ)
|
||||
ppHypo scope (Hyp typ) = ( scope,ppType 1 scope typ)
|
||||
ppHypo scope (HypV x typ) = let y = freshName x scope
|
||||
in (y:scope,PP.parens (PP.text (prCId y) PP.<+> PP.char ':' PP.<+> ppType 0 scope typ))
|
||||
ppHypo scope (HypI x typ) = let y = freshName x scope
|
||||
in (y:scope,PP.braces (PP.text (prCId y) PP.<+> PP.char ':' PP.<+> ppType 0 scope typ))
|
||||
|
||||
ppParens :: Bool -> PP.Doc -> PP.Doc
|
||||
ppParens True = PP.parens
|
||||
|
||||
@@ -1,201 +1,463 @@
|
||||
----------------------------------------------------------------------
|
||||
-- |
|
||||
-- Module : TypeCheck
|
||||
-- Maintainer : AR
|
||||
-- Module : PGF.TypeCheck
|
||||
-- Maintainer : Krasimir Angelov
|
||||
-- Stability : (stable)
|
||||
-- Portability : (portable)
|
||||
--
|
||||
-- type checking in abstract syntax with dependent types.
|
||||
-- Type checking in abstract syntax with dependent types.
|
||||
-- The type checker also performs renaming and checking for unknown
|
||||
-- functions. The variable references are replaced by de Bruijn indices.
|
||||
--
|
||||
-- modified from src GF TC
|
||||
-----------------------------------------------------------------------------
|
||||
|
||||
module PGF.TypeCheck (
|
||||
typecheck
|
||||
) where
|
||||
module PGF.TypeCheck (checkType, checkExpr, inferExpr,
|
||||
|
||||
ppTcError, TcError(..)
|
||||
) where
|
||||
|
||||
import PGF.Data
|
||||
import PGF.Macros (lookDef,isData)
|
||||
import PGF.Expr
|
||||
import PGF.Macros (typeOfHypo)
|
||||
import PGF.CId
|
||||
|
||||
import GF.Data.ErrM
|
||||
import qualified Data.Map as Map
|
||||
import Control.Monad (liftM2,foldM)
|
||||
import Data.List (partition,sort,groupBy)
|
||||
import Data.Map as Map
|
||||
import Data.IntMap as IntMap
|
||||
import Data.Maybe as Maybe
|
||||
import Data.List as List
|
||||
import Control.Monad
|
||||
import Text.PrettyPrint
|
||||
|
||||
import Debug.Trace
|
||||
-----------------------------------------------------
|
||||
-- The Scope
|
||||
-----------------------------------------------------
|
||||
|
||||
typecheck :: PGF -> Expr -> [Expr]
|
||||
typecheck pgf e = case inferExpr pgf (newMetas e) of
|
||||
Ok e -> [e]
|
||||
Bad s -> trace s []
|
||||
data TType = TTyp Env Type
|
||||
newtype Scope = Scope [(CId,TType)]
|
||||
|
||||
inferExpr :: PGF -> Expr -> Err Expr
|
||||
inferExpr pgf e = case infer pgf emptyTCEnv e of
|
||||
Ok (e,_,cs) -> let (ms,cs2) = splitConstraints pgf cs in case cs2 of
|
||||
[] -> trace (prConstraints cs ++"\n"++ show ms) $ Ok (metaSubst ms e)
|
||||
_ -> Bad ("Error in tree " ++ showExpr e ++ " :\n " ++ prConstraints cs2)
|
||||
Bad s -> Bad s
|
||||
emptyScope = Scope []
|
||||
|
||||
infer :: PGF -> TCEnv -> Expr -> Err (Expr, Value, [(Value,Value)])
|
||||
infer pgf tenv@(k,rho,gamma) e = case e of
|
||||
EVar x -> do
|
||||
ty <- lookupEVar pgf tenv x
|
||||
return (e,ty,[])
|
||||
addScopedVar :: CId -> TType -> Scope -> Scope
|
||||
addScopedVar x tty (Scope gamma) = Scope ((x,tty):gamma)
|
||||
|
||||
-- EInt i -> return (AInt i, valAbsInt, [])
|
||||
-- EFloat i -> return (AFloat i, valAbsFloat, [])
|
||||
-- K i -> return (AStr i, valAbsString, [])
|
||||
-- | returns the type and the De Bruijn index of a local variable
|
||||
lookupVar :: CId -> Scope -> Maybe (Int,TType)
|
||||
lookupVar x (Scope gamma) = listToMaybe [(i,tty) | ((y,tty),i) <- zip gamma [0..], x == y]
|
||||
|
||||
EApp f t -> do
|
||||
(f',typ,csf) <- infer pgf tenv f
|
||||
case typ of
|
||||
VClosure env (EPi x a b) -> do
|
||||
(a',csa) <- checkExp pgf tenv t (VClosure env a)
|
||||
let b' = eval (getFunEnv (abstract pgf)) (eins x (VClosure rho t) env) b
|
||||
return $ (EApp f' a', b', csf ++ csa)
|
||||
_ -> Bad ("function type expected for function " ++ show f)
|
||||
_ -> Bad ("cannot infer type of expression" ++ show e)
|
||||
-- | returns the type and the name of a local variable
|
||||
getVar :: Int -> Scope -> (CId,TType)
|
||||
getVar i (Scope gamma) = gamma !! i
|
||||
|
||||
scopeEnv :: Scope -> Env
|
||||
scopeEnv (Scope gamma) = let n = length gamma
|
||||
in [VGen (n-i-1) [] | i <- [0..n-1]]
|
||||
|
||||
checkExp :: PGF -> TCEnv -> Expr -> Value -> Err (Expr, [(Value,Value)])
|
||||
checkExp pgf tenv@(k,rho,gamma) e typ = do
|
||||
let v = VGen k []
|
||||
case e of
|
||||
EMeta m -> return $ (e,[])
|
||||
EAbs x t -> case typ of
|
||||
VClosure env (EPi y a b) -> do
|
||||
let a' = eval (getFunEnv (abstract pgf)) env a
|
||||
(t',cs) <- checkExp pgf (k+1,eins x v rho, eins x a' gamma) t
|
||||
(VClosure (eins y v env) b)
|
||||
return (EAbs x t', cs)
|
||||
_ -> Bad ("function type expected for " ++ show e)
|
||||
_ -> checkInferExp pgf tenv e typ
|
||||
scopeVars :: Scope -> [CId]
|
||||
scopeVars (Scope gamma) = List.map fst gamma
|
||||
|
||||
getFunEnv abs = Map.union (funs abs) (Map.map (\hypos -> (DTyp hypos cidType [],0,[])) (cats abs))
|
||||
scopeSize :: Scope -> Int
|
||||
scopeSize (Scope gamma) = length gamma
|
||||
|
||||
-----------------------------------------------------
|
||||
-- The Monad
|
||||
-----------------------------------------------------
|
||||
|
||||
type MetaStore = IntMap MetaValue
|
||||
data MetaValue
|
||||
= MUnbound Scope [Expr -> TcM ()]
|
||||
| MBound Expr
|
||||
| MGuarded Expr [Expr -> TcM ()] {-# UNPACK #-} !Int -- the Int is the number of constraints that have to be solved
|
||||
-- to unlock this meta variable
|
||||
|
||||
newtype TcM a = TcM {unTcM :: Abstr -> MetaId -> MetaStore -> TcResult a}
|
||||
data TcResult a
|
||||
= Ok {-# UNPACK #-} !MetaId MetaStore a
|
||||
| Fail TcError
|
||||
|
||||
instance Monad TcM where
|
||||
return x = TcM (\abstr metaid ms -> Ok metaid ms x)
|
||||
f >>= g = TcM (\abstr metaid ms -> case unTcM f abstr metaid ms of
|
||||
Ok metaid ms x -> unTcM (g x) abstr metaid ms
|
||||
Fail e -> Fail e)
|
||||
|
||||
instance Functor TcM where
|
||||
fmap f x = TcM (\abstr metaid ms -> case unTcM x abstr metaid ms of
|
||||
Ok metaid ms x -> Ok metaid ms (f x)
|
||||
Fail e -> Fail e)
|
||||
|
||||
lookupCatHyps :: CId -> TcM [Hypo]
|
||||
lookupCatHyps cat = TcM (\abstr metaid ms -> case Map.lookup cat (cats abstr) of
|
||||
Just hyps -> Ok metaid ms hyps
|
||||
Nothing -> Fail (UnknownCat cat))
|
||||
|
||||
lookupFunType :: CId -> TcM TType
|
||||
lookupFunType fun = TcM (\abstr metaid ms -> case Map.lookup fun (funs abstr) of
|
||||
Just (ty,_,_) -> Ok metaid ms (TTyp [] ty)
|
||||
Nothing -> Fail (UnknownFun fun))
|
||||
|
||||
newMeta :: Scope -> TcM MetaId
|
||||
newMeta scope = TcM (\abstr metaid ms -> Ok (metaid+1) (IntMap.insert metaid (MUnbound scope []) ms) metaid)
|
||||
|
||||
newGuardedMeta :: Scope -> Expr -> TcM MetaId
|
||||
newGuardedMeta scope e = getFuns >>= \funs -> TcM (\abstr metaid ms -> Ok (metaid+1) (IntMap.insert metaid (MGuarded e [] 0) ms) metaid)
|
||||
|
||||
getMeta :: MetaId -> TcM MetaValue
|
||||
getMeta i = TcM (\abstr metaid ms -> Ok metaid ms $! case IntMap.lookup i ms of
|
||||
Just mv -> mv)
|
||||
setMeta :: MetaId -> MetaValue -> TcM ()
|
||||
setMeta i mv = TcM (\abstr metaid ms -> Ok metaid (IntMap.insert i mv ms) ())
|
||||
|
||||
tcError :: TcError -> TcM a
|
||||
tcError e = TcM (\abstr metaid ms -> Fail e)
|
||||
|
||||
getFuns :: TcM Funs
|
||||
getFuns = TcM (\abstr metaid ms -> Ok metaid ms (funs abstr))
|
||||
|
||||
addConstraint :: MetaId -> MetaId -> Env -> [Value] -> (Value -> TcM ()) -> TcM ()
|
||||
addConstraint i j env vs c = do
|
||||
funs <- getFuns
|
||||
mv <- getMeta j
|
||||
case mv of
|
||||
MUnbound scope cs -> addRef >> setMeta j (MUnbound scope ((\e -> release >> c (apply funs env e vs)) : cs))
|
||||
MBound e -> c (apply funs env e vs)
|
||||
MGuarded e cs x | x == 0 -> c (apply funs env e vs)
|
||||
| otherwise -> addRef >> setMeta j (MGuarded e ((\e -> release >> c (apply funs env e vs)) : cs) x)
|
||||
where
|
||||
cidType = mkCId "Type"
|
||||
addRef = TcM (\abstr metaid ms -> case IntMap.lookup i ms of
|
||||
Just (MGuarded e cs x) -> Ok metaid (IntMap.insert i (MGuarded e cs (x+1)) ms) ())
|
||||
|
||||
checkInferExp :: PGF -> TCEnv -> Expr -> Value -> Err (Expr, [(Value,Value)])
|
||||
checkInferExp pgf tenv@(k,_,_) e typ = do
|
||||
(e',w,cs1) <- infer pgf tenv e
|
||||
let cs2 = eqValue (getFunEnv (abstract pgf)) k w typ
|
||||
return (e',cs1 ++ cs2)
|
||||
|
||||
lookupEVar :: PGF -> TCEnv -> CId -> Err Value
|
||||
lookupEVar pgf (_,g,_) x = case Map.lookup x g of
|
||||
Just v -> return v
|
||||
_ -> maybe (Bad "var not found") (return . VClosure eempty . type2expr . (\(a,b,c) -> a)) $
|
||||
Map.lookup x (funs (abstract pgf))
|
||||
release = TcM (\abstr metaid ms -> case IntMap.lookup i ms of
|
||||
Just (MGuarded e cs x) -> if x == 1
|
||||
then unTcM (sequence_ [c e | c <- cs]) abstr metaid (IntMap.insert i (MGuarded e [] 0) ms)
|
||||
else Ok metaid (IntMap.insert i (MGuarded e cs (x-1)) ms) ())
|
||||
|
||||
type2expr :: Type -> Expr
|
||||
type2expr (DTyp hyps cat es) =
|
||||
foldr (uncurry EPi) (foldl EApp (EVar cat) es) [toPair h | h <- hyps]
|
||||
-----------------------------------------------------
|
||||
-- Type errors
|
||||
-----------------------------------------------------
|
||||
|
||||
data TcError
|
||||
= UnknownCat CId
|
||||
| UnknownFun CId
|
||||
| WrongCatArgs Scope Type CId Int Int
|
||||
| TypeMismatch Scope Expr Type Type
|
||||
| NotFunType Scope Expr Type
|
||||
| CannotInferType Scope Expr
|
||||
| UnresolvedMetaVars Scope Expr [MetaId]
|
||||
|
||||
ppTcError :: TcError -> Doc
|
||||
ppTcError (UnknownCat cat) = text "Category" <+> text (prCId cat) <+> text "is not in scope"
|
||||
ppTcError (UnknownFun fun) = text "Function" <+> text (prCId fun) <+> text "is not in scope"
|
||||
ppTcError (WrongCatArgs scope ty cat m n) =
|
||||
text "Category" <+> text (prCId cat) <+> text "should have" <+> int m <+> text "argument(s), but has been given" <+> int n $$
|
||||
text "In the type:" <+> ppType 0 (scopeVars scope) ty
|
||||
ppTcError (TypeMismatch scope e ty1 ty2) = text "Couldn't match expected type" <+> ppType 0 (scopeVars scope) ty1 $$
|
||||
text " against inferred type" <+> ppType 0 (scopeVars scope) ty2 $$
|
||||
text "In the expression:" <+> ppExpr 0 (scopeVars scope) e
|
||||
ppTcError (NotFunType scope e ty) = text "A function type is expected for the expression" <+> ppExpr 0 (scopeVars scope) e <+> text "instead of type" <+> ppType 0 (scopeVars scope) ty
|
||||
ppTcError (CannotInferType scope e) = text "Cannot infer the type of expression" <+> ppExpr 0 (scopeVars scope) e
|
||||
ppTcError (UnresolvedMetaVars scope e xs) = text "Meta variable(s)" <+> fsep (List.map ppMeta xs) <+> text "should be resolved" $$
|
||||
text "in the expression:" <+> ppExpr 0 (scopeVars scope) e
|
||||
|
||||
-----------------------------------------------------
|
||||
-- checkType
|
||||
-----------------------------------------------------
|
||||
|
||||
checkType :: PGF -> Type -> Either TcError Type
|
||||
checkType pgf ty =
|
||||
case unTcM (tcType emptyScope ty >>= refineType) (abstract pgf) 0 IntMap.empty of
|
||||
Ok _ ms ty -> Right ty
|
||||
Fail err -> Left err
|
||||
|
||||
tcType :: Scope -> Type -> TcM Type
|
||||
tcType scope ty@(DTyp hyps cat es) = do
|
||||
(scope,hyps) <- tcHypos scope hyps
|
||||
c_hyps <- lookupCatHyps cat
|
||||
let m = length es
|
||||
n = length c_hyps
|
||||
if m == n
|
||||
then do (delta,es) <- tcHypoExprs scope [] (zip es c_hyps)
|
||||
return (DTyp hyps cat es)
|
||||
else tcError (WrongCatArgs scope ty cat n m)
|
||||
|
||||
tcHypos :: Scope -> [Hypo] -> TcM (Scope,[Hypo])
|
||||
tcHypos scope [] = return (scope,[])
|
||||
tcHypos scope (h:hs) = do
|
||||
(scope,h ) <- tcHypo scope h
|
||||
(scope,hs) <- tcHypos scope hs
|
||||
return (scope,h:hs)
|
||||
|
||||
tcHypo :: Scope -> Hypo -> TcM (Scope,Hypo)
|
||||
tcHypo scope (Hyp ty) = do
|
||||
ty <- tcType scope ty
|
||||
return (scope,Hyp ty)
|
||||
tcHypo scope (HypV x ty) = do
|
||||
ty <- tcType scope ty
|
||||
return (addScopedVar x (TTyp (scopeEnv scope) ty) scope,HypV x ty)
|
||||
|
||||
tcHypoExprs :: Scope -> Env -> [(Expr,Hypo)] -> TcM (Env,[Expr])
|
||||
tcHypoExprs scope delta [] = return (delta,[])
|
||||
tcHypoExprs scope delta ((e,h):xs) = do
|
||||
(delta,e ) <- tcHypoExpr scope delta e h
|
||||
(delta,es) <- tcHypoExprs scope delta xs
|
||||
return (delta,e:es)
|
||||
|
||||
tcHypoExpr :: Scope -> Env -> Expr -> Hypo -> TcM (Env,Expr)
|
||||
tcHypoExpr scope delta e (Hyp ty) = do
|
||||
e <- tcExpr scope e (TTyp delta ty)
|
||||
return (delta,e)
|
||||
tcHypoExpr scope delta e (HypV x ty) = do
|
||||
e <- tcExpr scope e (TTyp delta ty)
|
||||
funs <- getFuns
|
||||
return (eval funs (scopeEnv scope) e:delta,e)
|
||||
|
||||
|
||||
-----------------------------------------------------
|
||||
-- checkExpr
|
||||
-----------------------------------------------------
|
||||
|
||||
checkExpr :: PGF -> Expr -> Type -> Either TcError Expr
|
||||
checkExpr pgf e ty =
|
||||
case unTcM (do e <- tcExpr emptyScope e (TTyp [] ty)
|
||||
e <- refineExpr e
|
||||
checkResolvedMetaStore emptyScope e
|
||||
return e) (abstract pgf) 0 IntMap.empty of
|
||||
Ok _ ms e -> Right e
|
||||
Fail err -> Left err
|
||||
|
||||
tcExpr :: Scope -> Expr -> TType -> TcM Expr
|
||||
tcExpr scope e0@(EAbs x e) tty =
|
||||
case tty of
|
||||
TTyp delta (DTyp (h:hs) c es) -> do e <- case h of
|
||||
Hyp ty -> tcExpr (addScopedVar x (TTyp delta ty) scope)
|
||||
e (TTyp delta (DTyp hs c es))
|
||||
HypV y ty -> tcExpr (addScopedVar x (TTyp delta ty) scope)
|
||||
e (TTyp ((VGen (scopeSize scope) []):delta) (DTyp hs c es))
|
||||
return (EAbs x e)
|
||||
_ -> do ty <- evalType (scopeSize scope) tty
|
||||
tcError (NotFunType scope e0 ty)
|
||||
tcExpr scope (EMeta _) tty = do
|
||||
i <- newMeta scope
|
||||
return (EMeta i)
|
||||
tcExpr scope e0 tty = do
|
||||
(e0,tty0) <- infExpr scope e0
|
||||
i <- newGuardedMeta scope e0
|
||||
eqType scope (scopeSize scope) i tty tty0
|
||||
return (EMeta i)
|
||||
|
||||
|
||||
-----------------------------------------------------
|
||||
-- inferExpr
|
||||
-----------------------------------------------------
|
||||
|
||||
inferExpr :: PGF -> Expr -> Either TcError (Expr,Type)
|
||||
inferExpr pgf e =
|
||||
case unTcM (do (e,tty) <- infExpr emptyScope e
|
||||
e <- refineExpr e
|
||||
checkResolvedMetaStore emptyScope e
|
||||
ty <- evalType 0 tty
|
||||
return (e,ty)) (abstract pgf) 1 IntMap.empty of
|
||||
Ok _ ms (e,ty) -> Right (e,ty)
|
||||
Fail err -> Left err
|
||||
|
||||
infExpr :: Scope -> Expr -> TcM (Expr,TType)
|
||||
infExpr scope e0@(EApp e1 e2) = do
|
||||
(e1,tty1) <- infExpr scope e1
|
||||
case tty1 of
|
||||
(TTyp delta1 (DTyp (h:hs) c es)) -> do (delta1,e2) <- tcHypoExpr scope delta1 e2 h
|
||||
return (EApp e1 e2,TTyp delta1 (DTyp hs c es))
|
||||
_ -> do ty1 <- evalType (scopeSize scope) tty1
|
||||
tcError (NotFunType scope e1 ty1)
|
||||
infExpr scope e0@(EFun x) = do
|
||||
case lookupVar x scope of
|
||||
Just (i,tty) -> return (EVar i,tty)
|
||||
Nothing -> do tty <- lookupFunType x
|
||||
return (e0,tty)
|
||||
infExpr scope e0@(EVar i) = do
|
||||
return (e0,snd (getVar i scope))
|
||||
infExpr scope e0@(ELit l) = do
|
||||
let cat = case l of
|
||||
LStr _ -> mkCId "String"
|
||||
LInt _ -> mkCId "Int"
|
||||
LFlt _ -> mkCId "Float"
|
||||
return (e0,TTyp [] (DTyp [] cat []))
|
||||
infExpr scope (ETyped e ty) = do
|
||||
ty <- tcType scope ty
|
||||
e <- tcExpr scope e (TTyp (scopeEnv scope) ty)
|
||||
return (ETyped e ty,TTyp (scopeEnv scope) ty)
|
||||
infExpr scope e = tcError (CannotInferType scope e)
|
||||
|
||||
-----------------------------------------------------
|
||||
-- eqType
|
||||
-----------------------------------------------------
|
||||
|
||||
eqType :: Scope -> Int -> MetaId -> TType -> TType -> TcM ()
|
||||
eqType scope k i0 tty1@(TTyp delta1 ty1@(DTyp hyps1 cat1 es1)) tty2@(TTyp delta2 ty2@(DTyp hyps2 cat2 es2))
|
||||
| cat1 == cat2 = do (k,delta1,delta2) <- eqHyps k delta1 hyps1 delta2 hyps2
|
||||
sequence_ [eqExpr k delta1 e1 delta2 e2 | (e1,e2) <- zip es1 es2]
|
||||
| otherwise = raiseTypeMatchError
|
||||
where
|
||||
toPair (Hyp t) = (wildCId, type2expr t)
|
||||
toPair (HypV x t) = (x, type2expr t)
|
||||
raiseTypeMatchError = do ty1 <- evalType k tty1
|
||||
ty2 <- evalType k tty2
|
||||
e <- refineExpr (EMeta i0)
|
||||
tcError (TypeMismatch scope e ty1 ty2)
|
||||
|
||||
type TCEnv = (Int,Env,Env)
|
||||
eqHyps :: Int -> Env -> [Hypo] -> Env -> [Hypo] -> TcM (Int,Env,Env)
|
||||
eqHyps k delta1 [] delta2 [] =
|
||||
return (k,delta1,delta2)
|
||||
eqHyps k delta1 (Hyp ty1 : h1s) delta2 (Hyp ty2 : h2s) = do
|
||||
eqType scope k i0 (TTyp delta1 ty1) (TTyp delta2 ty2)
|
||||
(k,delta1,delta2) <- eqHyps k delta1 h1s delta2 h2s
|
||||
return (k,delta1,delta2)
|
||||
eqHyps k delta1 (HypV x ty1 : h1s) delta2 (HypV y ty2 : h2s) = do
|
||||
eqType scope k i0 (TTyp delta1 ty1) (TTyp delta2 ty2)
|
||||
(k,delta1,delta2) <- eqHyps (k+1) ((VGen k []):delta1) h1s ((VGen k []):delta2) h2s
|
||||
return (k,delta1,delta2)
|
||||
eqHyps k delta1 h1s delta2 h2s = raiseTypeMatchError
|
||||
|
||||
eempty = Map.empty
|
||||
eins = Map.insert
|
||||
eqExpr :: Int -> Env -> Expr -> Env -> Expr -> TcM ()
|
||||
eqExpr k env1 e1 env2 e2 = do
|
||||
funs <- getFuns
|
||||
eqValue k (eval funs env1 e1) (eval funs env2 e2)
|
||||
|
||||
emptyTCEnv :: TCEnv
|
||||
emptyTCEnv = (0,eempty,eempty)
|
||||
eqValue :: Int -> Value -> Value -> TcM ()
|
||||
eqValue k v1 v2 = do
|
||||
v1 <- deRef v1
|
||||
v2 <- deRef v2
|
||||
eqValue' k v1 v2
|
||||
|
||||
deRef v@(VMeta i env vs) = do
|
||||
mv <- getMeta i
|
||||
funs <- getFuns
|
||||
case mv of
|
||||
MBound e -> deRef (apply funs env e vs)
|
||||
MGuarded e _ x | x == 0 -> deRef (apply funs env e vs)
|
||||
| otherwise -> return v
|
||||
MUnbound _ _ -> return v
|
||||
deRef v = return v
|
||||
|
||||
eqValue' k (VSusp i env vs1 c) v2 = addConstraint i0 i env vs1 (\v1 -> eqValue k (c v1) v2)
|
||||
eqValue' k v1 (VSusp i env vs2 c) = addConstraint i0 i env vs2 (\v2 -> eqValue k v1 (c v2))
|
||||
eqValue' k (VMeta i env1 vs1) (VMeta j env2 vs2) | i == j = zipWithM_ (eqValue k) vs1 vs2
|
||||
eqValue' k (VMeta i env1 vs1) v2 = do (MUnbound scopei cs) <- getMeta i
|
||||
e2 <- mkLam i scopei env1 vs1 v2
|
||||
sequence_ [c e2 | c <- cs]
|
||||
setMeta i (MBound e2)
|
||||
eqValue' k v1 (VMeta i env2 vs2) = do (MUnbound scopei cs) <- getMeta i
|
||||
e1 <- mkLam i scopei env2 vs2 v1
|
||||
sequence_ [c e1 | c <- cs]
|
||||
setMeta i (MBound e1)
|
||||
eqValue' k (VApp f1 vs1) (VApp f2 vs2) | f1 == f2 = zipWithM_ (eqValue k) vs1 vs2
|
||||
eqValue' k (VLit l1) (VLit l2 ) | l1 == l2 = return ()
|
||||
eqValue' k (VGen i vs1) (VGen j vs2) | i == j = zipWithM_ (eqValue k) vs1 vs2
|
||||
eqValue' k (VClosure env1 (EAbs x1 e1)) (VClosure env2 (EAbs x2 e2)) = let v = VGen k []
|
||||
in eqExpr (k+1) (v:env1) e1 (v:env2) e2
|
||||
eqValue' k v1 v2 = raiseTypeMatchError
|
||||
|
||||
mkLam i scope env vs0 v = do
|
||||
let k = scopeSize scope
|
||||
vs = reverse (take k env) ++ vs0
|
||||
xs = nub [i | VGen i [] <- vs]
|
||||
if length vs == length xs
|
||||
then return ()
|
||||
else raiseTypeMatchError
|
||||
v <- occurCheck i k xs v
|
||||
funs <- getFuns
|
||||
return (addLam vs0 (value2expr funs (length xs) v))
|
||||
where
|
||||
addLam [] e = e
|
||||
addLam (v:vs) e = EAbs var (addLam vs e)
|
||||
|
||||
var = mkCId "v"
|
||||
|
||||
occurCheck i0 k xs (VApp f vs) = do vs <- mapM (occurCheck i0 k xs) vs
|
||||
return (VApp f vs)
|
||||
occurCheck i0 k xs (VLit l) = return (VLit l)
|
||||
occurCheck i0 k xs (VMeta i env vs) = do if i == i0
|
||||
then raiseTypeMatchError
|
||||
else return ()
|
||||
mv <- getMeta i
|
||||
funs <- getFuns
|
||||
case mv of
|
||||
MBound e -> occurCheck i0 k xs (apply funs env e vs)
|
||||
MGuarded e _ _ -> occurCheck i0 k xs (apply funs env e vs)
|
||||
MUnbound scopei _ | scopeSize scopei > k -> raiseTypeMatchError
|
||||
| otherwise -> do vs <- mapM (occurCheck i0 k xs) vs
|
||||
return (VMeta i env vs)
|
||||
occurCheck i0 k xs (VSusp i env vs cnt) = do addConstraint i0 i env vs (\v -> occurCheck i0 k xs (cnt v) >> return ())
|
||||
return (VSusp i env vs cnt)
|
||||
occurCheck i0 k xs (VGen i vs) = case List.findIndex (==i) xs of
|
||||
Just i -> do vs <- mapM (occurCheck i0 k xs) vs
|
||||
return (VGen i vs)
|
||||
Nothing -> raiseTypeMatchError
|
||||
occurCheck i0 k xs (VClosure env e) = do env <- mapM (occurCheck i0 k xs) env
|
||||
return (VClosure env e)
|
||||
|
||||
|
||||
-- this is not given in Expr
|
||||
prValue = showExpr . value2expr
|
||||
-----------------------------------------------------------
|
||||
-- check for meta variables that still have to be resolved
|
||||
-----------------------------------------------------------
|
||||
|
||||
value2expr v = case v of
|
||||
VApp f vs -> foldl EApp (EVar f) (map value2expr vs)
|
||||
VMeta i vs -> foldl EApp (EMeta i) (map value2expr vs)
|
||||
VClosure g e -> e ----
|
||||
VLit l -> ELit l
|
||||
checkResolvedMetaStore :: Scope -> Expr -> TcM ()
|
||||
checkResolvedMetaStore scope e = TcM (\abstr metaid ms ->
|
||||
let xs = [i | (i,mv) <- IntMap.toList ms, not (isResolved mv)]
|
||||
in if List.null xs
|
||||
then Ok metaid ms ()
|
||||
else Fail (UnresolvedMetaVars scope e xs))
|
||||
where
|
||||
isResolved (MUnbound _ []) = True
|
||||
isResolved (MGuarded _ _ _) = True
|
||||
isResolved (MBound _) = True
|
||||
isResolved _ = False
|
||||
|
||||
prConstraints :: [(Value,Value)] -> String
|
||||
prConstraints cs = unwords
|
||||
["(" ++ prValue v ++ " <> " ++ prValue w ++ ")" | (v,w) <- cs]
|
||||
-----------------------------------------------------
|
||||
-- evalType
|
||||
-----------------------------------------------------
|
||||
|
||||
-- work more on this: unification, compute,...
|
||||
|
||||
{-
|
||||
splitConstraints :: PGF -> [(Value,Value)] -> ([(Int,Expr)],[(Value,Value)])
|
||||
splitConstraints pgf = mkSplit . partition isSubst . regroup . map reorder . map reduce where
|
||||
reorder (v,w) = case w of
|
||||
VMeta _ _ -> (w,v)
|
||||
_ -> (v,w)
|
||||
|
||||
reduce (v,w) = (whnf v,whnf w)
|
||||
|
||||
whnf (VClosure env e) = eval (getFunEnv (abstract pgf)) env e -- should be removed when the typechecker is improved
|
||||
whnf v = v
|
||||
|
||||
regroup = groupBy (\x y -> fst x == fst y) . sort
|
||||
|
||||
isSubst cs@((v,u):_) = case v of
|
||||
VMeta _ _ -> all ((==u) . snd) cs
|
||||
_ -> False
|
||||
mkSplit (ms,cs) = ([(i,value2expr v) | (VMeta i _,v):_ <- ms], concat cs)
|
||||
-}
|
||||
|
||||
splitConstraints :: PGF -> [(Value,Value)] -> ([(Int,Expr)],[(Value,Value)])
|
||||
splitConstraints pgf = mkSplit . unifyAll [] . map reduce where
|
||||
reduce (v,w) = (whnf v,whnf w)
|
||||
|
||||
whnf (VClosure env e) = eval (getFunEnv (abstract pgf)) env e -- should be removed when the typechecker is improved
|
||||
whnf v = v
|
||||
mkSplit (ms,cs) = ([(i,value2expr v) | (i,v) <- ms], cs)
|
||||
|
||||
unifyAll g [] = (g, [])
|
||||
unifyAll g ((a@(s, t)) : l) =
|
||||
let (g1, c) = unifyAll g l
|
||||
in case unify s t g1 of
|
||||
Just g2 -> (g2, c)
|
||||
_ -> (g1, a : c)
|
||||
|
||||
unify e1 e2 g = case (e1, e2) of
|
||||
(VMeta s _, t) -> do
|
||||
let tg = substMetas g t
|
||||
let sg = maybe e1 id (lookup s g)
|
||||
if null (eqValue (funs (abstract pgf)) 0 sg e1) then extend s tg g else unify sg tg g
|
||||
(t, VMeta _ _) -> unify e2 e1 g
|
||||
(VApp c as, VApp d bs) | c == d ->
|
||||
foldM (\ h (a,b) -> unify a b h) g (zip as bs)
|
||||
_ -> Nothing
|
||||
|
||||
extend s t g = case t of
|
||||
VMeta u _ | u == s -> return g
|
||||
_ | occCheck s t -> Nothing
|
||||
_ -> return ((s, t) : g)
|
||||
|
||||
substMetas subst trm = case trm of
|
||||
VMeta s _ -> maybe trm id (lookup s subst)
|
||||
VApp c vs -> VApp c (map (substMetas subst) vs)
|
||||
_ -> trm
|
||||
|
||||
occCheck s u = case u of
|
||||
VMeta t _ -> s == t
|
||||
VApp c as -> any (occCheck s) as
|
||||
_ -> False
|
||||
evalType :: Int -> TType -> TcM Type
|
||||
evalType k (TTyp delta ty) = do funs <- getFuns
|
||||
refineType (evalTy funs k delta ty)
|
||||
where
|
||||
evalTy sig k delta (DTyp hyps cat es) =
|
||||
let ((k1,delta1),hyps1) = mapAccumL (evalHypo sig) (k,delta) hyps
|
||||
in DTyp hyps1 cat (List.map (normalForm sig k1 delta1) es)
|
||||
|
||||
evalHypo sig (k,delta) (Hyp ty) = ((k, delta),Hyp (evalTy sig k delta ty))
|
||||
evalHypo sig (k,delta) (HypV x ty) = ((k+1,(VGen k []):delta),HypV x (evalTy sig k delta ty))
|
||||
evalHypo sig (k,delta) (HypI x ty) = ((k+1,(VGen k []):delta),HypI x (evalTy sig k delta ty))
|
||||
|
||||
|
||||
metaSubst :: [(Int,Expr)] -> Expr -> Expr
|
||||
metaSubst vs exp = case exp of
|
||||
EApp u v -> EApp (subst u) (subst v)
|
||||
EMeta i -> maybe exp id $ lookup i vs
|
||||
EPi x a b -> EPi x (subst a) (subst b)
|
||||
EAbs x b -> EAbs x (subst b)
|
||||
_ -> exp
|
||||
where
|
||||
subst = metaSubst vs
|
||||
-----------------------------------------------------
|
||||
-- refinement
|
||||
-----------------------------------------------------
|
||||
|
||||
--- use composOp and state monad...
|
||||
newMetas :: Expr -> Expr
|
||||
newMetas = fst . metas 0 where
|
||||
metas i exp = case exp of
|
||||
EAbs x e -> let (f,j) = metas i e in (EAbs x f, j)
|
||||
EApp f a -> let (g,j) = metas i f ; (b,k) = metas j a in (EApp g b,k)
|
||||
EMeta _ -> (EMeta i, i+1)
|
||||
_ -> (exp,i)
|
||||
refineExpr :: Expr -> TcM Expr
|
||||
refineExpr e = TcM (\abstr metaid ms -> Ok metaid ms (refineExpr_ ms e))
|
||||
|
||||
refineExpr_ ms e = refine e
|
||||
where
|
||||
refine (EAbs x e) = EAbs x (refine e)
|
||||
refine (EApp e1 e2) = EApp (refine e1) (refine e2)
|
||||
refine (ELit l) = ELit l
|
||||
refine (EMeta i) = case IntMap.lookup i ms of
|
||||
Just (MBound e ) -> refine e
|
||||
Just (MGuarded e _ _) -> refine e
|
||||
_ -> EMeta i
|
||||
refine (EFun f) = EFun f
|
||||
refine (EVar i) = EVar i
|
||||
refine (ETyped e ty) = ETyped (refine e) (refineType_ ms ty)
|
||||
|
||||
refineType :: Type -> TcM Type
|
||||
refineType ty = TcM (\abstr metaid ms -> Ok metaid ms (refineType_ ms ty))
|
||||
|
||||
refineType_ ms (DTyp hyps cat es) = DTyp (List.map (refineHypo_ ms) hyps) cat (List.map (refineExpr_ ms) es)
|
||||
|
||||
refineHypo_ ms (Hyp ty) = Hyp (refineType_ ms ty)
|
||||
refineHypo_ ms (HypV x ty) = HypV x (refineType_ ms ty)
|
||||
refineHypo_ ms (HypI x ty) = HypI x (refineType_ ms ty)
|
||||
|
||||
value2expr sig i (VApp f vs) = foldl EApp (EFun f) (List.map (value2expr sig i) vs)
|
||||
value2expr sig i (VGen j vs) = foldl EApp (EVar (i-j-1)) (List.map (value2expr sig i) vs)
|
||||
value2expr sig i (VMeta j env vs) = foldl EApp (EMeta j) (List.map (value2expr sig i) vs)
|
||||
value2expr sig i (VSusp j env vs k) = value2expr sig i (k (VGen j vs))
|
||||
value2expr sig i (VLit l) = ELit l
|
||||
value2expr sig i (VClosure env (EAbs x e)) = EAbs x (value2expr sig (i+1) (eval sig ((VGen i []):env) e))
|
||||
|
||||
@@ -14,7 +14,7 @@ def g0 = g2 ;
|
||||
fun g3 : Int -> (Int -> Int) ;
|
||||
def g3 3 = g ;
|
||||
|
||||
fun const : Int -> Int -> Int ;
|
||||
fun const : Float -> String -> Float ;
|
||||
def const x _ = x ;
|
||||
|
||||
cat Nat ;
|
||||
|
||||
@@ -1,34 +1,30 @@
|
||||
i testsuite/runtime/eval/Test.gf
|
||||
|
||||
pt -compute \x -> x 1
|
||||
pt -compute ? 1
|
||||
pt -compute (\x -> x 1) ?
|
||||
pt -compute unknown_var
|
||||
pt -compute unknown_var 1
|
||||
pt -compute 1 2
|
||||
pt -compute \x -> x 1 : (Int->Int)->Int
|
||||
pt -compute (? : Int -> Int) 1
|
||||
pt -compute (\x -> x 1 : (Int->Int)->Int) ?
|
||||
pt -compute f 1 2
|
||||
pt -compute \x -> x
|
||||
pt -compute ?666
|
||||
pt -compute \x -> x : Nat -> Nat
|
||||
pt -compute ? : String
|
||||
pt -compute f
|
||||
pt -compute (\x -> x 2) (f 1)
|
||||
pt -compute (\x -> x 2) 1
|
||||
pt -compute (\x -> x 2 : (Int->Int)->Int) (f 1)
|
||||
pt -compute g 1
|
||||
pt -compute g 0
|
||||
pt -compute \x -> g x
|
||||
pt -compute \x -> g x : Int -> Int
|
||||
pt -compute g ?
|
||||
pt -compute (\x -> x 5) (g2 1)
|
||||
pt -compute (\x -> x 3) (\x -> x)
|
||||
pt -compute (\x -> x 5 : (Int->Int)->Int) (g2 1)
|
||||
pt -compute (\x -> x 3 : (Int->Int)->Int) (\x -> x)
|
||||
pt -compute g0
|
||||
pt -compute (\x -> x 3.2) (\x -> f x)
|
||||
pt -compute g0 2.3
|
||||
pt -compute g0 ((\x -> f x) 0) 1
|
||||
pt -compute (\x -> x 32 : (Int -> Int -> Int) -> Int -> Int) (\x -> f x : Int -> Int -> Int)
|
||||
pt -compute g0 23
|
||||
pt -compute const 3.14 "pi"
|
||||
pt -compute dec (succ (succ zero))
|
||||
pt -compute dec (succ ?)
|
||||
pt -compute \x -> dec x
|
||||
pt -compute \x -> dec x : Nat -> Nat
|
||||
pt -compute dec ?
|
||||
pt -compute (\f -> f 0) (g3 ?)
|
||||
pt -compute (\f -> f 0 : (Int -> Int) -> Int) (g3 ?)
|
||||
pt -compute g (g2 ? 0)
|
||||
pt -compute plus (succ zero) (succ zero)
|
||||
pt -compute dec2 0 (succ zero)
|
||||
pt -compute dec2 0 err
|
||||
pt -compute plus err (succ zero)
|
||||
@@ -1,30 +1,26 @@
|
||||
\v0 -> v0 1
|
||||
\x -> x 1
|
||||
|
||||
|
||||
|
||||
|
||||
? 1
|
||||
?1 1
|
||||
|
||||
|
||||
|
||||
? 1
|
||||
|
||||
|
||||
|
||||
?3 1
|
||||
|
||||
|
||||
|
||||
|
||||
f 1 2
|
||||
|
||||
|
||||
|
||||
|
||||
\x -> x
|
||||
|
||||
|
||||
|
||||
|
||||
?1
|
||||
|
||||
?666
|
||||
|
||||
|
||||
f
|
||||
|
||||
@@ -32,29 +28,29 @@ g ?
|
||||
|
||||
f 1 2
|
||||
|
||||
f 1 2
|
||||
|
||||
|
||||
|
||||
|
||||
literal of function type
|
||||
2
|
||||
|
||||
|
||||
|
||||
g 0
|
||||
|
||||
g 0
|
||||
|
||||
|
||||
|
||||
\x -> g x
|
||||
|
||||
\v0 -> g v0
|
||||
|
||||
|
||||
|
||||
g ?1
|
||||
|
||||
g ?
|
||||
|
||||
|
||||
5
|
||||
|
||||
|
||||
|
||||
3
|
||||
|
||||
|
||||
|
||||
|
||||
@@ -1,10 +1,10 @@
|
||||
\v0 -> v0
|
||||
\x -> x
|
||||
|
||||
|
||||
|
||||
1
|
||||
1
|
||||
|
||||
|
||||
|
||||
|
||||
\x -> x
|
||||
|
||||
|
||||
37
testsuite/runtime/typecheck/Test.gf
Normal file
37
testsuite/runtime/typecheck/Test.gf
Normal file
@@ -0,0 +1,37 @@
|
||||
abstract Test = {
|
||||
|
||||
cat Nat ;
|
||||
data zero : Nat ;
|
||||
succ : Nat -> Nat ;
|
||||
|
||||
fun plus : Nat -> Nat -> Nat ;
|
||||
def plus zero n = n ;
|
||||
plus (succ m) n = plus m (succ n) ;
|
||||
|
||||
cat Vector Nat ;
|
||||
fun vector : (n : Nat) -> Vector n ;
|
||||
|
||||
fun append : (m,n : Nat) -> Vector m -> Vector n -> Vector (plus m n) ;
|
||||
fun diff : (m,n : Nat) -> Vector (plus m n) -> Vector m -> Vector n ;
|
||||
|
||||
cat Morph (Nat -> Nat) ;
|
||||
fun mkMorph : (f : Nat -> Nat) -> Morph f ;
|
||||
fun mkMorph2 : (f : Nat -> Nat) -> Vector (f zero) -> Morph f ;
|
||||
fun idMorph : Morph (\x -> x) -> Nat ;
|
||||
|
||||
fun f0 : (n : Nat) -> ((m : Nat) -> Vector n) -> Int ;
|
||||
fun f1 : (n : Nat -> Nat) -> ((m : Nat) -> Vector (n m)) -> Int ;
|
||||
|
||||
fun cmpVector : (n : Nat) -> Vector n -> Vector n -> Int ;
|
||||
|
||||
fun g : ((n : Nat) -> Vector n) -> Int ;
|
||||
|
||||
cat U (n,m : Nat) ;
|
||||
fun u0 : (n : Nat) -> U n n ;
|
||||
fun u1 : (n : Nat) -> U n (succ n) ;
|
||||
fun h : (n : Nat) -> U n n -> Int ;
|
||||
|
||||
-- fun u2 : (n : Nat) -> U (plus n zero) zero ;
|
||||
-- fun h2 : (f : Nat -> Nat) -> ((n : Nat) -> U (f n) (f zero)) -> Int ;
|
||||
|
||||
}
|
||||
30
testsuite/runtime/typecheck/typecheck.gfs
Normal file
30
testsuite/runtime/typecheck/typecheck.gfs
Normal file
@@ -0,0 +1,30 @@
|
||||
i testsuite/runtime/typecheck/Test.gf
|
||||
|
||||
ai succ "0"
|
||||
ai succ : Int 0
|
||||
ai 1 2
|
||||
ai (\x -> x 2 : (Int->Int)->Int) 1
|
||||
ai unknown_fun
|
||||
ai 0 : unknown_cat
|
||||
ai \x -> x
|
||||
ai \x -> x : Int
|
||||
ai append (succ (succ zero)) (succ zero) (vector (succ (succ zero))) (vector (succ zero))
|
||||
ai \m,n -> vector (plus m n) : (m,n : Nat) -> Vector (plus m n)
|
||||
ai mkMorph (\x -> succ zero)
|
||||
ai idMorph (mkMorph (\x -> x))
|
||||
ai idMorph (mkMorph (\x -> succ zero))
|
||||
ai append zero (succ zero) : Vector zero -> Vector (succ zero) -> Vector (succ zero)
|
||||
ai \n,v1,n,v2 -> append ? ? v1 v2 : (n : Nat) -> Vector n -> (m : Nat) -> Vector m -> Vector (plus n m)
|
||||
ai \n -> (\v1,v2 -> eqVector n v1 v2 : Vector ? -> Vector ? -> EQ) (vector ?) : (n : Nat) -> Vector n -> EQ
|
||||
ai (\v1,v2 -> cmpVector ? v1 v2 : Vector ? -> Vector ? -> Int) (vector ?)
|
||||
ai f0 ? vector
|
||||
ai f1 ? vector
|
||||
ai f1 ? (\x -> vector (succ x))
|
||||
ai mkMorph (\x -> cmpVector ? (vector x) (vector (succ x)))
|
||||
ai g (\n -> vector (succ n))
|
||||
ai h ? (u0 ?)
|
||||
ai h ? (u1 ?)
|
||||
ai cmpVector (succ (succ zero)) (vector (succ (succ zero))) (append ? (succ zero) (vector ?) (vector (succ zero)))
|
||||
ai diff ? (succ (succ zero)) (vector (succ (succ (succ (succ (succ zero)))))) (vector (succ (succ (succ zero))))
|
||||
ai diff ? (succ (succ zero)) (vector (succ (succ (succ (succ zero))))) (vector (succ (succ (succ zero))))
|
||||
ai idMorph (mkMorph2 (\x -> ?) (vector zero))
|
||||
102
testsuite/runtime/typecheck/typecheck.gfs.gold
Normal file
102
testsuite/runtime/typecheck/typecheck.gfs.gold
Normal file
@@ -0,0 +1,102 @@
|
||||
|
||||
|
||||
Couldn't match expected type Nat
|
||||
|
||||
against inferred type String
|
||||
|
||||
In the expression: "0"
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
Category Int should have 0 argument(s), but has been given 1
|
||||
|
||||
In the type: Int 0
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
A function type is expected for the expression 1 instead of type Int
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
Couldn't match expected type Int -> Int
|
||||
|
||||
against inferred type Int
|
||||
|
||||
In the expression: 1
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
Function unknown_fun is not in scope
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
Category unknown_cat is not in scope
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
Cannot infer the type of expression \x -> x
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
A function type is expected for the expression \x -> x instead of type Int
|
||||
|
||||
|
||||
|
||||
Expression: append (succ (succ zero)) (succ zero) (vector (succ (succ zero))) (vector (succ zero))
|
||||
|
||||
Type: Vector (plus (succ (succ zero)) (succ zero))
|
||||
|
||||
|
||||
|
||||
Expression: \m, n -> vector (plus m n) : (m : Nat) -> (n : Nat) -> Vector (plus m n)
|
||||
|
||||
Type: (m : Nat) -> (n : Nat) -> Vector (plus m n)
|
||||
|
||||
|
||||
|
||||
Expression: mkMorph (\x -> succ zero)
|
||||
|
||||
Type: Morph (\x -> succ zero)
|
||||
|
||||
|
||||
|
||||
Expression: idMorph (mkMorph (\x -> x))
|
||||
|
||||
Type: Nat
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
Couldn't match expected type Morph (\x -> x)
|
||||
|
||||
against inferred type Morph (\x -> succ zero)
|
||||
|
||||
In the expression: mkMorph (\x -> succ zero)
|
||||
|
||||
|
||||
|
||||
Expression: append zero (succ zero) : Vector zero -> Vector (succ zero) -> Vector (succ zero)
|
||||
|
||||
Type: Vector zero -> Vector (succ zero) -> Vector (succ zero)
|
||||
|
||||
|
||||
|
||||
Expression: \n, v1, n'1, v2 -> append n n'1 v1 v2 : (n : Nat) -> Vector n -> (m : Nat) -> Vector m -> Vector (plus n m)
|
||||
|
||||
Type: (n : Nat) -> Vector n -> (m : Nat) -> Vector m -> Vector (plus n m)
|
||||
|
||||
Reference in New Issue
Block a user