ivor 0.1.12 → 0.1.14
raw patch · 25 files changed
+1314/−1429 lines, 25 files
Files
- Ivor/Bytecode.lhs +0/−166
- Ivor/CodegenC.lhs +0/−161
- Ivor/Compiler.lhs +0/−191
- Ivor/CtxtTT.lhs +108/−0
- Ivor/Datatype.lhs +30/−7
- Ivor/Errors.lhs +2/−0
- Ivor/EvalTT.lhs +72/−0
- Ivor/Evaluator.lhs +354/−110
- Ivor/Grouper.lhs +0/−59
- Ivor/ICompile.lhs +0/−93
- Ivor/Nobby.lhs +8/−4
- Ivor/PMComp.lhs +270/−0
- Ivor/PatternDefs.lhs +56/−14
- Ivor/RunTT.lhs +0/−107
- Ivor/SC.lhs +0/−174
- Ivor/Scopecheck.lhs +1/−1
- Ivor/State.lhs +8/−7
- Ivor/TT.lhs +164/−227
- Ivor/TTCore.lhs +70/−6
- Ivor/Tactics.lhs +44/−44
- Ivor/Typecheck.lhs +36/−30
- Ivor/Unify.lhs +9/−7
- Ivor/Values.lhs +44/−7
- Ivor/ViewTerm.lhs +28/−6
- ivor.cabal +10/−8
− Ivor/Bytecode.lhs
@@ -1,166 +0,0 @@-> module Ivor.Bytecode where--Compilation of supercombinators to bytecode--> import Ivor.SC-> import Ivor.TTCore--> type Arity = Int-> type Tag = Int-> type TmpVar = Int--> type Bytecode = [ByteOp]--> data ByteOp-> = STARTFN SCName Arity -- Needed?-> | DECLARE Int-> | TMP Int-> | RETURN TmpVar-> | CALL TmpVar SCName [TmpVar]-> | CON TmpVar Tag [TmpVar]-> | CLOSURE TmpVar SCName [TmpVar]-> | VAR TmpVar Int-> | GETARG TmpVar Int TmpVar-> | CLOSUREADD TmpVar TmpVar [TmpVar]-> | EVAL Int-> | EVALTMP TmpVar-> | TYPE TmpVar-> | TAILCALL SCName [TmpVar]-> | ALET Int TmpVar-> | CASE Int [Bytecode]-> deriving Show--> data FunInfo-> = FI {-> bytecode :: Bytecode,-> cname :: String,-> ctag :: String,-> farity :: Int,-> ctagid :: Int-> }-> deriving Show--> type ByteDef = [(SCName,FunInfo)]--I wonder how generally useful this is...--> mapInc :: (Int->a->b) -> [a] -> Int -> [b]-> mapInc f [] i = []-> mapInc f (x:xs) i = (f i x):(mapInc f xs (i+1))--> compileAll :: SCs -> SCs -> ByteDef-> compileAll ctxt group = mapInc scomp group ((length ctxt)-(length group))-> where scomp i (n,(a,sc)) = (n,FI (adddecls a (scompile n ctxt sc))-> (mkcname n)-> (mkctag n)-> a-> i)-> mkcname (N n) = "_EVM_"++show n-> mkcname (SN n i) = "_EVMSC_"++show i++"_"++show n-> mkctag (N n) = "FTAG_EVM_"++show n-> mkctag (SN n i) = "FTAG_EVMSC_"++show i++"_"++show n--> scompile :: SCName -> SCs -> SC -> Bytecode-> scompile name scs (SLam args body) =-> (STARTFN name (length args)):(bcomp (length args) 0 body)-> where-> getarity n = case lookup n scs of-> (Just (a,d)) -> a-> Nothing -> error $ "Can't happen (scompile, name "++show n++", " ++ show (map fst scs)++ ")"-> bcomp v t (SCase scr alts) = -> (EVAL scr):-> [CASE scr (map (acomp v t) alts)]-> bcomp v t (SApp (SP n) as) -> | getarity n == length as = -> concat (mapInc (ecomp v) as (t+1))-> ++ [TAILCALL n (mktargs (length as) (t+1))]-> bcomp v t x = (ecomp v t x)++[RETURN t]--> mktargs 0 s = []-> mktargs n s = s:(mktargs (n-1) (s+1))--> acomp v t x = bcomp v t x -- Hmm. Well, maybe alts will get more complex--> ecomp :: Int -> TmpVar -> SCBody -> Bytecode-> ecomp v t (SP n) | getarity n == 0 = [CALL t n []]-> | otherwise = [CLOSURE t n []]-> -- ecomp v (SElim n) | getarity n == 0 = CALL n []-> -- | otherwise = CLOSURE n []-> ecomp v t (SV i) = [VAR t i]-> ecomp v t (SCon tag n as) -> = concat (mapInc (ecomp v) as (t+1))-> ++ [CON t tag (mktargs (length as) (t+1))]--> ecomp v t (SApp f as) = fcomp v t f as-> ecomp v t (SLet val ty b) = -> (ecomp v (t+1) val) ++-> (ALET v (t+1)):-> (ecomp (v+1) (t+2) b)-> ecomp v t (SProj i b) = (ecomp v (t+1) b) ++-> [GETARG t i (t+1)]-> ecomp v t (SPi e ty) = [TYPE t]-> ecomp v t SStar = [TYPE t]-> ecomp v t (SConst c) = error "Can't compile constants yet"-> ecomp v t _ = [TYPE t]--> fcomp v t (SP n) as -> | getarity n == length as-> = concat (mapInc (ecomp v) as (t+1))-> ++ [CALL t n (mktargs (length as) (t+1))]-> | otherwise -> = concat (mapInc (ecomp v) as (t+1))-> ++ [CLOSURE t n (mktargs (length as) (t+1))]--> fcomp v t f as -> = (ecomp v (t+1) f) ++-> concat (mapInc (ecomp v) as (t+2))-> ++ [CLOSUREADD t (t+1) (mktargs (length as) (t+2))]--> -- ccomp Star t = [TYPE t]--Add type declarations to the top of bytecode, for the benefit of C/C--.--> adddecls :: Int -> Bytecode -> Bytecode-> adddecls arity bc = let (tmps,vars) = fd (-1,-1) bc in-> ad (tmps+1) (vars+1) ++ bc-> where ad 0 n | n<=arity = []-> ad 0 n = (DECLARE (n-1)):(ad 0 (n-1))-> ad m n = (TMP (m-1)):(ad (m-1) n)--> fd (t,v) [] = (t,v)-> fd (t,v) (c:cs) = let (t',v') = fd' (t,v) c in-> fd (t',v') cs--> fd' (t,v) (RETURN rt) | rt>t = (rt,v)-> | otherwise = (t,v)-> fd' (t,v) (CALL tv _ _)-> | tv > t = (tv,v)-> | otherwise = (t,v) -> fd' (t,v) (CON tv _ _)-> | tv > t = (tv,v)-> | otherwise = (t,v) -> fd' (t,v) (CLOSURE tv _ _)-> | tv > t = (tv,v)-> | otherwise = (t,v) -> fd' (t,v) (CLOSUREADD tv _ _)-> | tv > t = (tv,v)-> | otherwise = (t,v) -> fd' (t,v) (VAR tv _)-> | tv > t = (tv,v)-> | otherwise = (t,v) -> fd' (t,v) (GETARG tv _ _)-> | tv > t = (tv,v)-> | otherwise = (t,v) -> fd' (t,v) (TYPE tv)-> | tv > t = (tv,v)-> | otherwise = (t,v) -> fd' (t,v) (ALET vv _)-> | vv > v = (t,vv)-> | otherwise = (t,v)-> fd' (t,v) (CASE _ bs) = fdcs (t,v) bs-> fd' ts _ = ts--> fdcs (t,v) [] = (t,v)-> fdcs (t,v) (c:cs) = let (t',v') = fd (t,v) c in-> fdcs (t',v') cs-
− Ivor/CodegenC.lhs
@@ -1,161 +0,0 @@-> module Ivor.CodegenC where--Spit out C. I think this is write-only code...--> import Ivor.Bytecode-> import Ivor.SC--Some useful gadgets--> getTag :: ByteDef -> SCName -> String-> getTag scs n = case lookup n scs of-> Just (FI _ _ tag _ _) -> tag-> Nothing -> error "Can't happen (getTag)"--> getCName :: ByteDef -> SCName -> String-> getCName scs n = case lookup n scs of-> Just (FI _ cname _ _ _) -> cname-> Nothing -> error "Can't happen (getTag)"--Make the module's eval function, which checks the function tag on the-closure it is passed, and runs the appropriate function.--> mkEval :: ByteDef -> String-> mkEval scs = evalHead ++ "\n" ++ concat (map (mke'.snd) scs) ++ evalTail-> where-> evalHead = "VAL eval(VAL x) {" ++-> "\n if (x->ty != FUN) return x;" ++-> "\n else {" ++-> "\n function* f = (function*)(x -> info);" ++-> "\n switch(f->ftag) {"-> evalTail = " }" ++-> "\n }" ++-> "\n return x;" ++-> "\n}\n"--> mke' (FI _ name tag arity _) = " EVALCASE("++tag++","++-> show arity ++ "," ++ name ++ "("-> ++ showargs arity ++ "));\n"-> showargs 0 = ""-> showargs 1 = "FARG(0)"-> showargs n = showargs (n-1) ++ "," ++ "FARG("++show (n-1)++")"--Make the header, including definitions of all the function tags and-function prototypes.--> mkHeaders :: ByteDef -> String-> mkHeaders scs = fileHeader ++ concat (map (mkh'.snd) scs)-> where fileHeader = "#include \"closure.h\"\n"++-> "#include <stdio.h>\n\n"--> mkh' (FI _ name tag arity tagid) =-> "#define "++ tag ++ " " ++ show tagid ++"\n" ++-> "VAL "++ name ++ "(" ++ showargs arity ++");\n"-> showargs 0 = ""-> showargs 1 = "VAL v0"-> showargs n = showargs (n-1) ++ "," ++ "VAL v"++show (n-1)--Output C code for each supercombinator.--> mkCode :: ByteDef -> String-> mkCode scs = concat (map (mhc'.snd) scs)-> where mhc' (FI bc name _ arity _) = -> let code = writeCode scs bc in-> "VAL "++ name ++ "(" ++ showargs arity ++") {\n"-> ++ "\n" ++ code ++ "}\n\n"--> declaretmps 0 = "VAL tmp0;"-> declaretmps n = declaretmps (n-1) ++ "\nVAL tmp" ++ show n ++";"-> showargs 0 = ""-> showargs 1 = "VAL v0"-> showargs n = showargs (n-1) ++ "," ++ "VAL v"++show (n-1)---> writeCode :: ByteDef -> Bytecode -> String-> writeCode scs [] = ""-> writeCode scs (c:cs) = " " ++ wc c ++ "\n" ++ writeCode scs cs-> where wc (STARTFN _ _) = "VAL* args;"-> wc (DECLARE i) = "VAL v"++show i++";"-> wc (TMP i) = "VAL tmp"++show i++";"-> wc (RETURN i) = "return tmp"++show i++";"-> wc (CALL t n vs) = "tmp"++show t++ " = "++ getCName scs n ++-> "(" ++ showargs vs ++ ");"-> wc (CON t tag as) -> | length as == 0 =-> "tmp"++show t++ " = MKCON0("++show tag++");"-> | length as < 2 =-> "tmp"++show t++ " = MKCON"++show (length as)++-> "("++show tag++"," ++ showargs as++");"-> | otherwise = "args = MKARGS(" ++ show (length as) ++ -> ");\n " ++ mkargs as 0 ++ "tmp"++show t++ -> " = MKCONN("++show tag ++",args,"++show (length as)++");"-> wc (CLOSURE t n as) -> | length as == 0 = -> "tmp"++show t++ " = CLOSURE0("++-> getTag scs n++","++show (length as)++");"-> | length as < 6 = -> "tmp"++show t++ " = CLOSURE"++show (length as)++-> "("++getTag scs n++","++show (length as)++","++showargs as++");"-> | otherwise = "args = MKARGS(" ++ show (length as) ++ -> ");\n " ++ mkargs as 0 ++ "tmp"++show t++-> " = CLOSUREN("++getTag scs n ++","++show (length as)++",args,"++ -> show (length as)++");"-> wc (VAR t i) = "tmp"++show t++" = v" ++ show i ++ ";"-> wc (GETARG t i v) = "tmp"++show t++" = GETCONARG(tmp"++show v++","-> ++show i++");"-> wc (CLOSUREADD t tf as) -> | length as < 6 = "tmp"++show t++ " = CLOSUREADD"++-> show (length as)++"(tmp"++show tf++","++-> showargs as++");"-> | otherwise = "args = MKARGS(" ++ show (length as) ++ -> ");\n " ++ mkargs as 0 ++ "tmp"++show t++-> " = CLOSUREADDN(tmp"++ show tf ++",args,"++ -> show (length as)++");"-> wc (EVAL i) = "eval(v" ++ show i ++");"-> wc (EVALTMP i) = "eval(tmp" ++ show i ++");"-> wc (TYPE t) = "tmp"++show t++" = MKTYPE;"-> wc (TAILCALL n vs) = "return "++getCName scs n ++ "(" ++ showargs vs ++ ");"-> wc (ALET i t) = "v"++show i++" = tmp"++show t++";"-> wc (CASE v cs) = "switch(TAG(v"++show v++")) {\n" ++-> cc cs 0 ++ " }"--> cc [] i = " default:\n return NULL;\n"-> cc (c:cs) i = " case "++show i++":\n" ++-> writeCode scs c ++ "\n" ++ cc cs (i+1)--> mkargs [] _ = ""-> mkargs (a:as) i = "args["++show i++"] = tmp"++show a ++ ";"-> ++ "\n " ++ mkargs as (i+1)--> showargs [] = ""-> showargs [x] = "tmp"++show x-> showargs (x:xs) = "tmp"++show x++","++showargs xs-- writeCode bc t [] = ("",t)- writeCode bc tmp (c:cs) = let (code,tmp') = opc tmp c- (code',tmp'') = writeCode bc tmp' cs in- ("\t" ++ code ++ "\n" ++ code', tmp'')- where opc t (STARTFN _ _) = ("VAL* args;",t)- opc t (DECLARE x) = ("VAL v"++show x++";",t)- opc t (RETURN e) = let (code,tmp') = ecomp (t+1) e in- (code ++ "return t"++show t,tmp')- opc t (TAILCALL n es) - = let (code,tmp',ts) = argcode (t+1) es [] "" in- (code ++ "return "++ getCName bc n ++ "(" ++ arglist ts ++ ")",tmp')- opc t (ALET x e) = error "Not done Let yet"- opc t (CASE e es) = ("CASE foo;",t)- ecomp t e = ("expression",t)- | length es < 2 = "MKCON"++show (length es)++"("++show t++","++- argcode es++")"- | otherwise = mkArgList (length es) ++ "MKCONN("++show t++- ",args,"++length es++");"- -- argcode t [] l code = (code,t,l)- argcode t (e:es) as c- = let (ecode,t') = ecomp (t+1) e- code = "tmp"++show t++ " = " ++ ecode ++ ";" in- argcode t' es (t:as) (c++code)- arglist [] = ""- arglist [e] = "tmp"++show e- arglist (e:es) = arglist es ++ "," ++ "tmp"++show e
− Ivor/Compiler.lhs
@@ -1,191 +0,0 @@-> {-# OPTIONS_GHC -fglasgow-exts #-}--> module Ivor.Compiler(compile) where--> import Ivor.RunTT-> import Ivor.State-> import Ivor.Nobby-> import Ivor.Datatype-> import Ivor.TTCore-> import Ivor.ICompile--> import System.IO-> import Control.Monad--> compile :: IState -> String -> IO ()-> compile st froot = fail "Deprecated"---> {- do h <- openFile (froot++".hs") WriteMode-> hPutStr h (header froot)-> compileData (defs st) (datadefs st) st h-> compileGamma (defs st) st h-> hFlush h-> hClose h--FIXME! Only does elim, not case.--> compileData :: Gamma Name -> [(Name,Datatype Name)] -> IState ->-> Handle -> IO ()-> compileData gam [] st h = return ()-> compileData gam ((n,dt):xs) st h =-> do let caseexp = compileSchemes (e_ischemes dt)-> let arity = getArity (e_ischemes dt)-> rn <- rulename-> if (length (datacons dt)>0) then-> hPutStrLn h $ "data TT_" ++ exportName n ++ " = " ++ compileCons (datacons dt)-> else hPutStrLn h $ "data TT_" ++ exportName n ++ " = TT_" ++ exportName n-> let inst = projInstance (datacons dt)-> when ((length (words inst))>0)-> $ hPutStrLn h $ "\ninstance Project TT_"++ exportName n ++-> " where\n" ++ inst-> let rtt = mkRTElim n arity caseexp-> let fn = mkGHC st rn arity rtt-> hPutStrLn h fn-> --putStrLn $ elimInterface n (snd (erule dt))-> --putStrLn $ elimBody n rn (snd (erule dt))-> --hPutStrLn h $ show rtt-> compileData gam xs st h-> where rulename = case lookupval n gam of-> (Just (TCon _ (Elims x _ _))) -> return x-> Nothing -> fail "No such type"--This creation of elim rule interfaces only works for completely simple types!--> elimInterface :: Name -> Indexed Name -> String-> elimInterface n (Ind ty) = "elim_" ++ exportName n ++ " :: " ++ mkET ty-> where mkET (Bind _ (B Pi ty) (Sc sc)) = mkArg ty ++ mkET sc-> mkET _ = "a"-> mkArg ty | Star <- getReturnType ty = "" -- Skip Phi-> | TyCon x _ <- getFun ty-> = "TT_" ++ exportName x ++ " -> "-> | otherwise = "(" ++ mkET ty ++ ") -> "--> elimBody :: Name -> Name -> Indexed Name -> String-> elimBody n rn (Ind ty) = "elim_" ++ exportName n ++ " = " ++ mkLams ty 0 ++-> "(coerce (fn_" ++ exportName rn ++ " " ++ mkET ty 0-> ++ "))::a"-> where-> mkET (Bind _ (B Pi ty) (Sc sc)) n | Star <- getReturnType ty-> = mkArg ty n ++ mkET sc n-> mkET (Bind _ (B Pi ty) (Sc sc)) n = mkArg ty n ++ mkET sc (n+1)-> mkET _ _ = ""-> mkLams (Bind _ (B Pi ty) (Sc sc)) n | Star <- getReturnType ty-> = mkLams sc n-> mkLams (Bind _ (B Pi ty) (Sc sc)) n = "\\x"++show n ++ " -> "-> ++ mkLams sc (n+1)-> mkLams _ _ = ""--> mkArg ty n | Star <- getReturnType ty = "((coerce Type)::val)"-> | otherwise = "((coerce x"++show n++")::val)"--> compileCons :: [(Name,Gval Name)] -> String-> compileCons [] = ""-> compileCons [x] = compileCon x-> compileCons (x:xs) = compileCon x ++ "| " ++ compileCons xs--> compileCon (n,G (DCon _ _) (Ind t) _) =-> foralls numargs ++ "TT_" ++ show n ++ " " ++ showargs numargs-> where numargs = length (getExpected t)-> foralls n | n == 0 = ""-> | otherwise = "forall arg. "-> showargs 0 = ""-> showargs n = "arg " ++ showargs (n-1)--> projInstance :: [(Name,Gval Name)] -> String-> projInstance [] = ""-> projInstance (x:xs) =-> let xp = projAll x in-> if (length (words xp)>0) then xp ++ "\n" ++ projInstance xs-> else projInstance xs--> projAll (n,G (DCon _ _) (Ind t) _) =-> project numargs-> where numargs = length (getExpected t)-> project 0 = "\n"-> project k = " project "++show (k-1)++" (TT_" ++ exportName n ++-> " " ++ showargs numargs++") = ((coerce a" ++ show (k-1)-> ++ ")::val)\n" ++ project (k-1)-> showargs 0 = ""-> showargs n = showargs (n-1) ++ " a" ++ show (n-1)--> compileGamma :: Gamma Name -> IState -> Handle -> IO ()-> compileGamma gam@(Gam g) st h = cg g where-> cg [] = return ()-> cg ((n,G (Fun _ ind) indty _):xs) =-> do -- putStrLn $ "Compiling " ++ show n-> let nind = normalise (Gam []) ind-> let rtt = mkRTFun gam (levelise nind)-> let (Ind ty) = normalise gam indty-> let arity = length (getExpected ty)-> let fn = mkGHC st n arity rtt-> hPutStrLn h fn-> cg xs-> cg (x:xs) = do -- putStrLn $ "Skipping " ++ show x-> cg xs--> mkGHC :: IState -> Name -> Int -> RunTT -> String-> mkGHC st n arity tm = "fn_" ++ exportName n ++ " :: " ++ mkSig arity ++ "\n" ++-> "fn_" ++ exportName n ++ " = " ++ mkBody 0 tm ++ "\n"-> where mkSig 0 = "val"-> mkSig n = "val -> " ++ mkSig (n-1)-> mkBody l (RTVar i) = "v"++show i-> mkBody l (RTFun n) = "fn_" ++ exportName n-> mkBody l (RTCon _ n args) = "(coerce (TT_" ++ exportName n ++ " " ++ showargs l args ++ ")::val)"-> mkBody l (RTElim n t m ms) = "(fn_" ++ exportName n ++ " " ++ showarg l t ++-> " ((coerce Type)::val) " ++ showargs l ms-> mkBody l (RTApp f xs) = "(" ++ showfun l f (length xs) ++ " " ++ showargs l xs ++ ")"-> mkBody l (RTBind (RTLam,_) (sc,_)) = "(\\v"++show l ++" -> " ++ mkBody (l+1) sc ++ ")"-> mkBody l (RTBind (RTLet (v,_),_) (sc,_)) = "(let v"++show l ++" = " ++ "(" ++ mkBody l v ++ ") in (" ++ mkBody (l+1) sc ++ "))"-> mkBody l (RTBind (RTPi,_) (sc,_)) = "((coerce Type)::val)"-> mkBody l RTypeVal = "((coerce Type)::val)"-> mkBody l RTCantHappen = "error \"Impossible\""-> mkBody l (RTProj ty i (v,_)) = "(project " ++ show i ++-> "((coerce " ++ mkBody l v ++")::TT_"++show ty++"))"-> mkBody l (RTCase ty (v,_) xs) = "(case ((coerce "++mkBody l v++")::TT_"++show ty++") of { " ++ doCaseBody l (getCons (datadefs st) ty) xs ++ "})"-> mkBody l (RTConst c) = error "Sorry, can't compile constants yet"-> -- mkBody l x = "[[Not done "++show x++"]]"--> doCaseBody l [] [] = ""-> doCaseBody l ((n,ar):ns) (i:is) = doCase l n ar i ++ " ; " ++ doCaseBody l ns is-> doCase l n ar (i,_) = "TT_"++exportName n++" "++caseargs ar++" -> " ++ mkBody l i-> caseargs 0 = ""-> caseargs n = "_ "++caseargs (n-1)--> showargs l [] = ""-> showargs l (x:xs) = showarg l x ++ " " ++ showargs l xs-> showarg l (x,_) = "((coerce "++mkBody l x++")::val)"-> showfun l (f,_) n = "((coerce "++mkBody l f++")::"++mkty n++")"--> mkty 0 = "val"-> mkty n = "val->"++mkty (n-1)--Given a type name, get all the constructors and their arities--> getCons :: [(Name,Datatype Name)] -> Name -> [(Name,Int)]-> getCons ds n = case lookup n ds of-> Nothing -> []-> Just dt -> map (\ (x,y) -> (x, arity y)) (datacons dt)-> where arity (G _ (Ind ty) _) = length (getExpected ty)--> header mod = "{-# OPTIONS_GHC -fglasgow-exts #-} \n\-> \\n\-> \module " ++ mod ++ " where\n\-> \\n\-> \import GHC.Base\n\-> \\n\-> \coerce :: a -> b\n\-> \coerce = unsafeCoerce#\n\-> \\n\-> \data Type = forall a. Type a\n\-> \data Val = Val\n\-> \\n\-> \class Project x where\n\-> \ project :: forall val. Int -> x -> val\n\n"--> exportName :: Name -> String-> exportName (UN n) = show $ UN (okch n)-> where okch [] = []-> okch ('\'':xs) = "_AP_"++okch xs-> okch (x:xs) = x:(okch xs)-> -}
+ Ivor/CtxtTT.lhs view
@@ -0,0 +1,108 @@+> -- |+> -- Module : Ivor.CtxtTT+> -- Copyright : Edwin Brady+> -- Licence : BSD-style (see LICENSE in the distribution)+> --+> -- Maintainer : eb@dcs.st-and.ac.uk+> -- Stability : experimental+> -- Portability : non-portable+> --+> -- Public interface to ivor contexts.++> module Ivor.CtxtTT where++> import Ivor.TTCore as TTCore+> import Ivor.Errors+> import Ivor.ViewTerm as VTerm+> import Ivor.State+> import Control.Monad.Error(Error,noMsg,strMsg)++> data TTError = CantUnify ViewTerm ViewTerm+> | NotConvertible ViewTerm ViewTerm+> | Message String+> | Unbound ViewTerm ViewTerm ViewTerm ViewTerm [Name]+> | NoSuchVar Name+> | CantInfer Name ViewTerm+> | ErrContext String TTError+> | AmbiguousName [Name]++> type TTM = Either TTError++> ttfail :: String -> TTM a+> ttfail s = Left (Message s)++> tt :: IvorM a -> TTM a+> tt (Left err) = Left (getError err)+> tt (Right v) = Right v++> getError :: IError -> TTError+> getError (ICantUnify l r) = CantUnify (view (Term (l, Ind TTCore.Star))) (view (Term (r, Ind TTCore.Star)))+> getError (INotConvertible l r) = NotConvertible (view (Term (l, Ind TTCore.Star))) (view (Term (r, Ind TTCore.Star)))+> getError (IMessage s) = Message s+> getError (IUnbound clause clty rhs rhsty names) +> = Unbound (view (Term (clause, Ind TTCore.Star)))+> (view (Term (clty, Ind TTCore.Star)))+> (view (Term (rhs, Ind TTCore.Star)))+> (view (Term (rhsty, Ind TTCore.Star)))+> names+> getError (ICantInfer nm tm) = CantInfer nm (view (Term (tm, Ind TTCore.Star)))+> getError (INoSuchVar n) = NoSuchVar n+> getError (IAmbiguousName ns) = AmbiguousName ns+> getError (IContext s e) = ErrContext s (getError e)++> instance Show TTError where+> show (CantUnify t1 t2) = "Can't unify " ++ show t1 ++ " and " ++ show t2+> show (NotConvertible t1 t2) = show t1 ++ " and " ++ show t2 ++ " are not convertible"+> show (Message s) = s+> show (Unbound clause clty rhs rhsty ns) +> = show ns ++ " unbound in clause " ++ show clause ++ " : " ++ show clty ++ +> " = " ++ show rhs+> show (CantInfer n tm) = "Can't infer value for " ++ show n ++ " in " ++ show tm+> show (NoSuchVar n) = "No such name as " ++ show n+> show (AmbiguousName ns) = "Ambiguous name " ++ show ns+> show (ErrContext c err) = c ++ show err++> instance Error TTError where+> noMsg = Message "Ivor Error"+> strMsg s = Message s++> -- | Abstract type representing state of the system.+> newtype Context = Ctxt IState++> -- | Abstract type representing goal or subgoal names.+> data Goal = Goal Name | DefaultGoal+> deriving Eq++> instance Show Goal where+> show (Goal g) = show g+> show (DefaultGoal) = "Default Goal"++> goal :: String -> Goal+> goal g = Goal $ UN g++> defaultGoal :: Goal+> defaultGoal = DefaultGoal++> -- |A tactic is any function which manipulates a term at the given goal+> -- binding. Tactics may fail, hence the monad.+> type Tactic = Goal -> Context -> TTM Context++> -- | Initialise a context, with no data or definitions and an+> -- empty proof state.+> emptyContext :: Context+> emptyContext = Ctxt initstate++> class IsTerm a where+> -- | Typecheck a term+> check :: Context -> a -> TTM Term+> raw :: a -> TTM Raw++> class IsData a where+> -- Add a data type with case and elim rules an elimination rule+> addData :: Context -> a -> TTM Context+> addData ctxt x = addData' True ctxt x+> -- Add a data type without an elimination rule+> addDataNoElim :: Context -> a -> TTM Context+> addDataNoElim ctxt x = addData' False ctxt x+> addData' :: Bool -> Context -> a -> TTM Context+
Ivor/Datatype.lhs view
@@ -9,6 +9,7 @@ > import Ivor.Values > import Debug.Trace+> import List > data Datadecl = Datadecl { > datatycon :: Name,@@ -63,8 +64,8 @@ > (ev, _) <- typecheck gamma'' erty > (cv, _) <- typecheck gamma'' crty > -- let gamma''' = extend gamma'' (er,G (ElimRule dummyRule) ev defplicit)-> ([(_, esch, _)], _, _) <- checkDef gamma'' er erty eschemes False False Nothing-> ([(_, csch, _)], _, _) <- checkDef gamma'' cr crty cschemes False False Nothing+> ([(_, esch, _)], _, _) <- checkDef gamma'' er erty eschemes False False Nothing Nothing+> ([(_, csch, _)], _, _) <- checkDef gamma'' cr crty cschemes False False Nothing Nothing > return (Data (ty,G (TCon (arity gamma kv) erdata) kv defplicit) consv numps > (er,ev) (cr,cv) (Just esch) (Just csch) eschemes cschemes) @@ -81,13 +82,35 @@ > (er,ev) (cr,cv) Nothing Nothing [] []) > checkCons gamma t [] = return ([], gamma)-> checkCons gamma t ((cn,cty):cs) = +> checkCons gamma t ((cn,cty):cs) = -- trace ("Checking " ++ show (cn, cty)) $ > do (cv,_) <- typecheck gamma cty-> let ccon = G (DCon t (arity gamma cv)) cv defplicit+> let ccon = let fpos = forcepos cty in+> G (DCon t (arity gamma cv) (forcepos cty)) cv defplicit > let gamma' = extend gamma (cn,ccon) > (rest,gamma'') <- checkCons gamma' (t+1) cs > return (((cn,ccon):rest), gamma'')+> where forcepos cty = let nms = nub (guardedNames [] cty) in+> map (argpos 0 cty) nms +> argpos i (RBind x _ t) n +> | x == n = i+> | otherwise = argpos (i+1) t n+> guardedNames ns (RBind n _ t) = guardedNames (n:ns) t+> guardedNames ns (RApp f a) = guardedApp ns f [a]+> guardedNames ns (Var n) | n `elem` ns = [n]+> guardedNames ns _ = []++> guardedApp ns (RApp f a) as = guardedApp ns f (a:as)+> guardedApp ns (Var n) as+> | isCon n = concatMap (guardedNames ns) as+> | otherwise = []+> isCon n = case lookupval n gamma of+> Just (DCon t i _) -> True+> Just (TCon _ _) -> True+> _ -> False+++ checkScheme takes a raw iota scheme and returns a scheme with a well-typed RHS (or fails if there is a type error). @@ -109,7 +132,7 @@ > mkPat :: Gamma Name -> Raw -> Pattern Name > mkPat gam (Var n) = mkPatV n (lookupval n gam)-> where mkPatV n (Just (DCon t x)) = PCon t n tyname []+> where mkPatV n (Just (DCon t x _)) = PCon t n tyname [] > mkPatV n (Just (TCon x _)) = PCon 0 n (UN "Type") [] > mkPatV n _ = PVar n > tyname = case (getTyName gam n) of@@ -123,7 +146,7 @@ > pat' (RFileLoc _ _ t, as) = pat' (t, as) > pat' _ = PTerm -> mkPatV n (Just (DCon t x)) as = PCon t n tyname as+> mkPatV n (Just (DCon t x _)) as = PCon t n tyname as > mkPatV n (Just (TCon x _)) as = PCon 0 n (UN "Type") as > mkPatV _ _ _ = PTerm > tyname = case (getTyName gam (getname (getappfun f))) of@@ -185,7 +208,7 @@ > sv' (RFileLoc _ _ t) = sv' t > mkGood x = case (lookupval x gam) of-> (Just (DCon t i)) -> Con t x i+> (Just (DCon t i _)) -> Con t x i > (Just (TCon i _)) -> TyCon x i > (Just (ElimRule _)) -> Elim er > _ -> P x
Ivor/Errors.lhs view
@@ -23,6 +23,8 @@ > ifail = Left +> tacfail str = ifail (IMessage str)+ Generic error checking can go here: Check that all the names are real rather than implicit and inferred
+ Ivor/EvalTT.lhs view
@@ -0,0 +1,72 @@+> -- |+> -- Module : Ivor.TT+> -- Copyright : Edwin Brady+> -- Licence : BSD-style (see LICENSE in the distribution)+> --+> -- Maintainer : eb@dcs.st-and.ac.uk+> -- Stability : experimental+> -- Portability : non-portable+> --+> -- Public interface to evaluator.++> module Ivor.EvalTT where++> import Ivor.Evaluator+> import Ivor.CtxtTT+> import Ivor.Values+> import Ivor.ViewTerm as VTerm+> import Ivor.State+> import Ivor.Nobby+> import Ivor.TTCore+> import qualified Ivor.Tactics as Tactics++> -- |Normalise a term and its type (using old evaluator_+> eval :: Context -> Term -> Term+> eval (Ctxt st) (Term (tm,ty)) = Term (normalise (defs st) tm,+> normalise (defs st) ty)++> -- |Reduce a term and its type to Weak Head Normal Form+> whnf :: Context -> Term -> Term+> whnf (Ctxt st) (Term (tm,ty)) = Term (eval_whnf (defs st) tm,+> eval_whnf (defs st) ty)++> -- |Reduce a term and its type to Normal Form (using new evaluator)+> evalnew :: Context -> Term -> Term+> evalnew (Ctxt st) (Term (tm,ty)) = Term (tidyNames (eval_nf (defs st) tm),+> tidyNames (eval_nf (defs st) ty))++> -- |Reduce a term and its type to Normal Form (using new evaluator, not+> -- reducing given names)+> evalnewWithout :: Context -> Term -> [Name] -> Term+> evalnewWithout (Ctxt st) (Term (tm,ty)) ns +> = Term (tidyNames (eval_nf_without (defs st) tm ns),+> tidyNames (eval_nf_without (defs st) ty ns))++> -- |Reduce a term and its type to Normal Form (using new evaluator, reducing+> -- given names a maximum number of times)+> evalnewLimit :: Context -> Term -> [(Name, Int)] -> Term+> evalnewLimit (Ctxt st) (Term (tm,ty)) ns +> = Term (eval_nf_limit (defs st) tm ns Nothing,+> eval_nf_limit (defs st) ty ns Nothing)++Specialise a pattern matching definition - support for 'spec'++> specialise :: Context -> PMFun Name -> +> [(Name, ([Int], Int))] -> -- functions with static args+> [Name] -> -- frozen names+> (PMFun Name, Context, [Name]) -- also, new names+> specialise ctxt (PMFun ar ps) statics frozen = sp ctxt ps [] []+> where+> sp ctxt [] names acc = (PMFun ar (reverse acc), ctxt, names)+> sp ctxt@(Ctxt st) (p@(Sch args env ret):ps) names acc +> = let ret' = eval_nf_limit (defs st) ret +> (map (\x -> (x,0)) frozen)+> (Just statics) in+> sp ctxt ps names (Sch args env ret' : acc) ++ sp ctxt (p@(PWithClause eq args scr pats):ps) names acc + = let (pats', ctxt', names') = specialise ctxt pats statics frozen in+ sp ctxt' ps names' (p:acc) +++
Ivor/Evaluator.lhs view
@@ -2,7 +2,7 @@ > module Ivor.Evaluator(eval_whnf, eval_nf, eval_nf_env, > eval_nf_without, eval_nf_limit,-> eval_nfEnv, tidyNames) where+> tidyNames) where > import Ivor.TTCore > import Ivor.Gadgets@@ -20,13 +20,15 @@ menv :: [(Name, Binder (TT Name))] } > eval_whnf :: Gamma Name -> Indexed Name -> Indexed Name-> eval_whnf gam (Ind tm) = let res = makePs (evaluate False gam tm Nothing Nothing)+> eval_whnf gam (Ind tm) = let res = makePs (evaluate False gam tm Nothing Nothing Nothing) > in finalise (Ind res) > eval_nf :: Gamma Name -> Indexed Name -> Indexed Name-> eval_nf gam (Ind tm) = let res = makePs (evaluate True gam tm Nothing Nothing)+> eval_nf gam (Ind tm) = let res = makePs (evaluate True gam tm Nothing Nothing Nothing) > in finalise (Ind res) + eval_nf gam (Ind tm) = Ind (evaluate True gam tm Nothing Nothing Nothing)+ > eval_nf_env :: Env Name -> Gamma Name -> Indexed Name -> Indexed Name > eval_nf_env env g t > = eval_nf (addenv env g) t@@ -37,21 +39,31 @@ > eval_nf_without :: Gamma Name -> Indexed Name -> [Name] -> Indexed Name > eval_nf_without gam tm [] = eval_nf gam tm-> eval_nf_without gam (Ind tm) ns = let res = makePs (evaluate True gam tm (Just ns) Nothing)+> eval_nf_without gam (Ind tm) ns = let res = makePs (evaluate True gam tm (Just ns) Nothing Nothing) > in finalise (Ind res) -> eval_nf_limit :: Gamma Name -> Indexed Name -> [(Name, Int)] -> Indexed Name-> eval_nf_limit gam tm [] = eval_nf gam tm-> eval_nf_limit gam (Ind tm) ns -> = let res = makePs (evaluate True gam tm Nothing (Just ns))+> eval_nf_limit :: Gamma Name -> Indexed Name -> [(Name, Int)] -> +> Maybe [(Name, ([Int], Int))] -> Indexed Name+> eval_nf_limit gam tm [] stat = eval_nf gam tm+> eval_nf_limit gam (Ind tm) ns stat +> = -- trace (show (tm, stat)) $+> let res = makePs (evaluate True gam tm Nothing (Just ns) stat) > in finalise (Ind res) -> type Stack = [TT Name] > type SEnv = [(Name, TT Name, TT Name)]+> type StackEntry = (TT Name, SEnv, [(Name, TT Name)])+> type Stack = [StackEntry] -> getEnv i env = (\ (_,_,val) -> val) (env!!i)+> getEnv i env = (\ (_,_,val) -> val) (traceIndex env i "Evaluator fail") > sfst (n,_,_) = n+> senv (_,e,_) = e+> stkpats (_,_,p) = p +> allNames :: Stack -> SEnv -> [(Name, TT Name)] -> [Name]+> allNames stk env pats = map sfst env ++ map fst pats +++> concat (map (map sfst) (map senv stk)) +++> concat (map (map fst) (map stkpats stk))+ Code Stack Env Result [[x{global}]] xs es (lookup x), xs, es@@ -62,89 +74,142 @@ (or leave alone for whnf) [[let x = t in e]] xs es [[e]], xs, (Let x t: es) +> type EvalState = (Maybe [(Name, Int)], +> Maybe [(Name, ([Int], Int))],+> Int)+ > evaluate :: Bool -> -- under binders? 'False' gives WHNF > Gamma Name -> TT Name -> > Maybe [Name] -> -- Names not to reduce > Maybe [(Name, Int)] -> -- Names to reduce a maximum number+> Maybe [(Name, ([Int], Int))] -> -- Names and list of static args > TT Name-> evaluate open gam tm jns maxns = -- trace ("EVALUATING: " ++ debugTT tm) $ -> let res = evalState (eval tm [] [] []) maxns-> in {- trace ("RESULT: " ++ debugTT res) -} +> evaluate open gam tm jns maxns statics = -- trace ("EVALUATING: " ++ debugTT tm) $ +> let res = evalState (eval (True, True) tm [] [] []) (maxns, statics, 0)+> in {- trace ("RESULT: " ++ debugTT res) -} > res > where-> eval :: TT Name -> Stack -> SEnv -> -> [(Name, TT Name)] -> State (Maybe [(Name, Int)]) (TT Name)-> eval tm stk env pats = {- trace (show (tm, stk, env, pats)) $ -} eval' tm stk env pats+> eval :: (Bool, Bool) -> TT Name -> Stack -> SEnv -> +> [(Name, TT Name)] -> State EvalState (TT Name)+> eval nms@(ev,top) tm stk env pats = -- trace (show (tm, stk, env, pats)) $+> {-# SCC "eval" #-} do eval' nms tm stk env pats+> {- if (ev && top && null stk && tm'/=tm)+> then eval nms tm' [] env pats+> else return tm' -}+> -> eval' (P x) xs env pats -> = do mns <- get-> let (use, mns') = usename x jns mns-> put mns'-> case lookup x pats of-> Nothing -> if use then evalP x (lookupval x gam) xs env pats-> else evalP x Nothing xs env pats-> Just val -> eval val xs env (removep x pats)+> eval' (everything, top) (P x) xs env pats +> = {-# SCC "evalptop" #-} do+> (mns, sts, tmp) <- {-# SCC "evalpget" #-} get+> let (use, mns', sts') = {-# SCC "evalpif" #-}+> if (everything || top)+> then {-# SCC "usename" #-} usename x jns mns (sts, (xs, pats))+> else (False, mns, sts)+> {-# SCC "evalPput" #-} put (mns', sts, tmp)+> -- when (not nms) (trace ("Not using " ++ show x) (return ()))+> case {-# SCC "evalPlookup" #-} lookup x pats of+> Nothing -> if use && (everything || top)+> then {-# SCC "evalptop" #-} evalP (everything, top) x (lookupval x gam) xs env pats+> else {-# SCC "evalptop" #-} evalP (everything, top) x Nothing xs env pats+> Just val -> eval (everything, False) val xs env (removep x pats) > where removep n [] = [] > removep n ((x,t):xs) | n==x = removep n xs > | otherwise = (x,t):(removep n xs)-> eval' (V i) xs env pats -> = if (length env>i) -> then eval (getEnv i env) xs env pats-> else unload (V i) xs pats env -- blocked, so unload-> eval' (App f a) xs env pats -> = do a' <- eval a [] env pats-> eval f (a':xs) env pats-> eval' (Bind n (B Lambda ty) (Sc sc)) xs env pats-> = do ty' <- eval ty [] env pats-> evalScope Lambda n ty' sc xs env pats-> eval' (Bind n (B Pi ty) (Sc sc)) xs env pats-> = do ty' <- eval ty [] env pats-> evalScope Pi n ty' sc xs env pats+> eval' nms@(ev,_) (V i) xs env pats +> = {-# SCC "evalVtoplevel" #-}+> if (length env>i) +> then eval nms (getEnv i env) xs env pats+> else unload ev (V i) xs pats env -- blocked, so unload+> eval' nms (App f a) xs env pats +> = do -- a' <- eval a [] env pats+> eval nms f ((a, env, pats):xs) env pats+> eval' nms (Bind n (B Lambda ty) (Sc sc)) xs env pats+> = do ty' <- eval nms ty [] env pats+> {-# SCC "evalscope" #-} evalScope nms Lambda n ty' sc xs env pats+> eval' nms (Bind n (B Pi ty) (Sc sc)) xs env pats+> = do ty' <- eval nms ty [] env pats+> {-# SCC "evalscope" #-} evalScope nms Pi n ty' sc xs env pats > -- unload (Bind n (B Pi ty') (Sc sc)) [] pats env-> eval' (Bind n (B (Let val) ty) (Sc sc)) xs env pats -> = do val' <- eval val [] env pats-> eval sc xs ((n,ty,val'):env) pats-> eval' (Bind n (B bt ty) (Sc sc)) xs env pats-> = do ty' <- eval ty [] env pats-> unload (Bind n (B bt ty') (Sc sc)) [] pats env-> eval' x stk env pats = unload x stk pats env+> eval' nms (Bind n (B (Let val) ty) (Sc sc)) xs env pats +> = do val' <- eval nms val [] env pats+> ty' <- eval nms ty [] env pats+> eval nms sc xs ((n,ty',val'):env) pats+> eval' nms@(ev,_) (Bind n (B bt ty) (Sc sc)) xs env pats+> = do ty' <- eval nms ty [] env pats+> unload ev (Bind n (B bt ty') (Sc sc)) [] pats env+> eval' (ev,_) x stk env pats = unload ev x stk pats env -> evalP n (Just v) xs env pats -> = case v of-> Fun opts (Ind v) -> eval v xs env pats-> PatternDef p _ _ -> pmatch n p xs env pats-> PrimOp _ f -> case f xs of-> Nothing -> unload (P n) xs pats env-> Just v -> eval v [] env pats-> _ -> unload (P n) xs pats env-> evalP n Nothing xs env pats = unload (P n) xs pats env -- blocked, so unload stack+> evalP (ev, top) n (Just v) xs env pats +> = {-# SCC "evalP" #-} case v of+> Fun opts (Ind v) -> eval (ev, False) v xs env pats+> PatternDef p@(PMFun arity _) _ _ pc -> +> do ans <- {-# SCC "pmatchc" #-} pmatchC (ev, top) n pc xs env pats+> -- ans <- pmatch (ev, top) n p xs env pats+> return ans+> PrimOp _ f -> do xs' <- mapM (\(x, xenv, xpats) -> eval (ev, False) x [] xenv xpats) xs+> case f xs' of+> Nothing -> unload ev (P n) xs pats env+> Just v -> eval (ev, False) v [] env pats+> _ -> unload ev (P n) xs pats env+> evalP (ev,top) n Nothing xs env pats = {-# SCC "evalP" #-} unload ev (P n) xs pats env -- blocked, so unload stack -> evalScope b n ty sc (x:xs) env pats = eval sc xs ((n,ty,x):env) pats-> evalScope b n ty sc [] env pats-> | open = do let n' = uniqify' n (map sfst env ++ map fst pats)-> let tmpname = (MN ("E", length env))-> sc' <- eval sc [] ((n',ty,P tmpname):env) pats+> evalScope nms b n ty sc stk@((x,xenv,xpats):xs) env pats +> = do let n' = uniqify' n (allNames stk env pats)+> x' <- eval nms x [] xenv xpats+> eval nms sc xs ((n',ty,x'):env) pats+> evalScope nms@(ev,_) b n ty sc [] env pats+> | open = do let n' = uniqify' n (allNames [] env pats)+> (mns, sts, tmp) <- get+> let tmpname = MN ("E",tmp) -- uniqify' (MN ("E", length env)) (allNames [] env pats) -- (MN ("E", length env))+> put (mns, sts, tmp+1)+> sc' <- eval nms sc [] ((n',ty,P tmpname):env) pats > let newsc = pToV tmpname sc'-> u' <- unload (Bind n' (B b ty) newsc) [] pats env+> u' <- unload ev (Bind n' (B b ty) newsc) [] pats env+> --trace ("SCOPE: " ++ show (sc, newsc, env, debugTT u', debugTT (buildenv env u'))) $ > return $ buildenv env u' > | otherwise -> = do let n' = uniqify' n (map sfst env ++ map fst pats)-> u' <- unload (Bind n' (B Lambda ty) (Sc sc)) [] pats env -- in Whnf+> = do let n' = uniqify' n (allNames [] env pats)+> u' <- unload ev (Bind n' (B Lambda ty) (Sc sc)) [] pats env -- in Whnf > return $ buildenv env u'-> unload x [] pats env -> = return $ foldl (\tm (n,val) -> substName n val (Sc tm)) x pats-> unload x (a:as) pats env = unload (App x a) as pats env+> unload ev x [] pats env +> = {-# SCC "unload" #-} return $ foldl (\tm (n,val) -> substName n val (Sc tm)) x pats+> unload ev x ((a, aenv, apats):as) pats env +> = {-# SCC "unload" #-}+> do a' <- eval (ev, False) a [] aenv apats+> unload ev (App x a') as pats env >-> uniqify' u@(UN n) ns = uniqify (MN (n,0)) ns-> uniqify' n ns = uniqify n ns+> uniqify' u@(UN n) ns = {-# SCC "uniqify'" #-} uniqify (MN (n,0)) ns+> uniqify' n ns = {-# SCC "uniqify'" #-} uniqify n ns -> usename x Nothing Nothing = (True, Nothing)-> usename x _ (Just ys) = case lookup x ys of-> Just 0 -> (False, Just ys)-> Just n -> (True, Just (update x (n-1) ys))-> _ -> (True, Just ys)-> usename x (Just xs) m = (not (elem x xs), m)+> evalStk ev ((a, aenv, apats):as) +> = do a' <- eval (ev, True) a [] aenv apats+> as' <- evalStk ev as+> return (a':as')+> evalStk ev [] = return [] +> evalArgs ev ((n, Left (a, aenv, apats)):as) +> = do a' <- eval (ev, True) a [] aenv apats+> as' <- evalArgs ev as+> return ((n,a'):as')+> evalArgs ev ((n,Right a'):as) +> = do as' <- evalArgs ev as+> return ((n,a'):as')+> evalArgs ev [] = return []++ usename x _ mns (sts, (stk, pats)) + | Just (static, arity) <- lookup x sts + = useDyn x mns static arity stk pats++> usename x Nothing Nothing (sts, _) = (True, Nothing, sts)+> usename x _ (Just ys) (sts, _) +> = case lookup x ys of+> Just 0 -> (False, Just ys, sts)+> Just n -> (True, Just (update x (n-1) ys), sts)+> _ -> (True, Just ys, sts)+> usename x (Just xs) m (sts, _) = (not (elem x xs), m, sts)++ useDyn x mns static arity stk pats =+ > update x v [] = [] > update x v ((k,_):xs) | x == k = ((x,v):xs) > update x v (kv:xs) = kv : update x v xs@@ -154,67 +219,228 @@ > = buildenv xs (subst tm (Sc t)) > -- = buildenv xs (Bind n (B (Let tm) ty) (Sc t)) -> renameRHS pbinds rhs env = rrhs [] [] (nub pbinds) rhs where+> bindRHS [] rhs = rhs+> bindRHS ((x,t):xs) rhs = bindRHS xs $ substName x t (Sc rhs)++> renameRHS pbinds rhs env stk = rrhs [] [] (nub pbinds) rhs where > rrhs namemap pbinds' [] rhs = {-trace ("BEFORE " ++ show (rhs, pbinds, pbinds')) $ -} > (pbinds', substNames namemap rhs) > rrhs namemap pbinds ((n,t):ns) rhs-> = let n' = uniqify' (UN (show n)) (map sfst env ++ map fst pbinds ++ map fst ns) in+> = let n' = uniqify' (UN (show n)) (map sfst env ++ +> map fst pbinds ++ map fst ns ++ +> concat (map (map sfst) (map senv stk)) ++ +> concat (map (map fst) (map stkpats stk))) in > rrhs ((n,P n'):namemap) ((n',t):pbinds) ns rhs -> substNames [] rhs = {-trace ("AFTER " ++ show rhs) $ -} rhs-> substNames ((n,t):ns) rhs = substNames ns (substName n t (Sc rhs))+ substNames [] rhs = {-trace ("AFTER " ++ show rhs) $ -} rhs+ substNames ((n,t):ns) rhs = substNames ns (substName n t (Sc rhs)) -> pmatch n (PMFun i clauses) xs env pats = -> do cm <- matches clauses xs env pats+> pmatch (False, False) n _ xs env pats +> = unload False (P n) xs pats env+> pmatch (ev, top) n (PMFun i clauses) xs env pats = matchtrace (show n) xs $ +> do (mns, statics, tmp) <- get+> let static = fmap (lookup n) statics+> let rcs = reqCons clauses+> {- xs' <- zipWithM (\(x, xenv, xpats) reqcon -> +> do x' <- if reqcon then eval (False, True) x [] xenv pats+> else return x +> return (x', xenv, xpats)) xs rcs -}+> old <- get -- HACK! If it fails, restore old state+> cm <- matches clauses xs env pats > case cm of-> Nothing -> unload (P n) xs pats env+> Nothing -> do put old+> unload ev (P n) xs pats env > Just (rhs, pbinds, stk) -> -> let (pbinds', rhs') = renameRHS pbinds rhs env in-> eval rhs' stk env pbinds'+> do rhsin <- case static of+> -- Just (Just staticargs) -> +> -- do -- mkNewDef n staticargs xs+> -- trace ("STATIC: " ++ show (n, staticargs, (map (\(x,y,z) -> x) xs))) $ return rhs +> _ -> return rhs+> let rhs' = bindRHS pbinds rhsin +> rhstrace (show n) rhs' []+> $ eval (ev, False) rhs' stk env [] +> reqCons [] = repeat False+> reqCons ((Sch pats _ _):ss) = zipWith (||) (reqCons ss) (rc pats)+> rc [] = []+> rc ((PCon _ _ _ _):ps) = True:(rc ps)+> rc ((PConst _):ps) = True:(rc ps)+> rc (_:ps) = False:(rc ps)++Careful with matching against catch all cases. If one clause *might* match,+but doesn't because an argument is not in canonical form, then we're stuck,+so better not look further!+ > matches [] xs env pats = return Nothing-> matches (c:cs) xs env pats -> = do cm <- (match c xs env pats)+> matches (c:cs) xs env pats+> = do cm <- match c xs env pats > case cm of-> Just v -> return $ Just v-> Nothing -> matches cs xs env pats+> (Just v, _) -> return $ Just v+> (Nothing, False) -> matches cs xs env pats+> (Nothing, True) -> return Nothing -- Stuck due to variable -> match :: Scheme Name -> [TT Name] -> SEnv -> +> match :: Scheme Name -> Stack -> SEnv -> > [(Name, TT Name)] ->-> State (Maybe [(Name, Int)]) (Maybe (TT Name, [(Name, TT Name)], Stack))+> State EvalState +> (Maybe (TT Name, [(Name, TT Name)], Stack), Bool) > match (Sch pats _ rhs) xs env patvars -> = matchargs pats xs rhs env patvars []-> matchargs [] xs (Ind rhs) env patvars pv' = return $ Just (rhs, pv', xs)-> matchargs (p:ps) (x:xs) rhs env patvars pv'-> = do x' <- (eval x [] env patvars) -> case matchPat p x' pv' of-> Just patvars' -> matchargs ps xs rhs env patvars patvars'-> Nothing -> return Nothing-> matchargs _ _ _ _ _ _ = return Nothing+> = do r <- matchargs pats xs rhs env patvars []+> return r -> matchPat PTerm x patvars = Just patvars-> matchPat (PVar n) x patvars = Just ((n,x):patvars) -- (filter (\ (x,y) -> x/=n) patvars))-> matchPat (PConst t) (Const t') patvars-> = do tc <- cast t-> if (tc == t') then Just patvars-> else Nothing-> matchPat pc@(PCon t _ _ args) app patvars-> | Just (tag, cargs) <- getConArgs app [] =-> if (tag == t) then matchPats args cargs patvars-> else Nothing-> where matchPats [] [] patvars = Just patvars+> matchargs [] xs (Ind rhs) env patvars pv' +> = return $ (Just (rhs, pv', xs), False)+> matchargs (p:ps) ((x, xenv, xpats):xs) rhs env patvars pv'+> = do old <- get+> x' <- {- trace ("against " ++ show x) $ -} eval (False, True) x [] xenv xpats+> xm <- matchPat p x' xenv xpats pv' old+> case xm of+> (Just patvars', _) -> matchargs ps xs rhs env patvars patvars'++FIXME: We should only get stuck if we have a variable matching against+a pattern (i.e. we've got a potential match) *and* all the rest of the+arguments are matches or potential matches.++If any of the remaining arguments definitely fail to match, we're not+stuck.++> (Nothing, False) -> do put old+> return (Nothing, False)+> (Nothing, True) ->+> do rest <- matchargs ps xs rhs env patvars pv'+> case rest of+> (Nothing, False) -> return (Nothing, False)+> _ -> return (Nothing, True)++ do xnms' <- eval True x [] xenv xpats+ trace ("Fully evalled " ++ show (x,xnms')) $ case matchPat p x' pv' of+ Just patvars' -> matchargs ps xs rhs env patvars patvars'+ Nothing -> return Nothing++> matchargs _ _ _ _ _ _ = return (Nothing, False)++> matchPat PTerm x _ _ patvars old = return $ (Just patvars, False)+> matchPat (PVar n) x _ _ patvars old+> = return $ (Just ((n,x):patvars), False) -- (filter (\ (x,y) -> x/=n) patvars))+> matchPat (PConst t) x xenv xpats patvars old+> = do x' <- eval (True, True) x [] [] []+> case x' of+> Const t' -> case cast t of+> Just tc -> +> if (tc == t') then return $ (Just patvars, False)+> else return (Nothing, False)+> _ -> return (Nothing, False)+> matchPat pc@(PCon t _ _ args) x xenv xpats patvars old+> = do -- old <- get+> x' <- eval (False, True) x [] xenv xpats+> case getConArgs x' [] of+> Just (tag, cargs) ->+> if (tag == t) then matchPats args cargs patvars+> else return (Nothing, False)+> _ -> do put old+> x' <- eval (True, True) x [] xenv xpats+> case getConArgs x' [] of+> Just (tag, cargs) ->+> if (tag == t) then matchPats args cargs patvars+> else return (Nothing, False)++> _ -> return (Nothing, True)+> where matchPats [] [] patvars = return $ (Just patvars, False) > matchPats (a:as) (b:bs) patvars-> = do vs' <- matchPat a b patvars-> matchPats as bs vs'-> matchPats _ _ _ = Nothing-> matchPat _ _ _ = Nothing+> = do vs' <- matchPat a b xenv xpats patvars old+> case vs' of+> (Just pats, _) -> matchPats as bs pats+> x -> return x+> matchPats _ _ _ = return (Nothing, False)+> matchPat _ _ _ _ _ _ = return (Nothing, False) > getConArgs (Con t _ _) args = Just (t, args) > getConArgs (App f a) args = getConArgs f (a:args) > getConArgs _ _ = Nothing +Substitution using compiled matches +> pmatchC top n (args, pc) xs env pats+> | length xs >= length args+> = -- trace (show (n, map (\ (x,_,_) -> x) (take arity xs))) $+> do let stk = take (length args) xs+> let rest = drop (length args) xs+> -- FIXME: make this lazy so interp fact works again!+> -- then lose the annoying extra params+> -- then PE might start working, and put the magic here.+> argvals' <- {-# SCC "evalstk" #-} evalStk True stk+> old <- get+> m <- pmSubst n env (zip args (map Right argvals')) pc -- argvals') pc+> case m of+> Just t -> eval (True,True) t rest env pats+> Nothing -> do put old+> unload True (P n) xs pats env+> | otherwise = unload True (P n) xs pats env++> substArgNames :: [(Name, Either StackEntry (TT Name))] ->+> TT Name -> State EvalState (TT Name)+> substArgNames args e = do stk' <- evalArgs True (filter (occ e) args)+> return $ substNames stk' e++> occ e (n,_) = n `elem` getNames (Sc e)+> right (n, Right x) = (n, x)+> isRight (n, Right _) = True+> isRight (n, Left _) = False++> pmSubst :: Name -> SEnv -> -- Name useful for debugging+> [(Name, Either StackEntry (TT Name))] -> -- function arguments, value+> TSimpleCase Name -> -- compiled match+> State EvalState (Maybe (TT Name))+> pmSubst n env args (TTm rhs) +> = do rhs' <- {-# SCC "pmsubstnames" #-} substArgNames args rhs+> return $ Just rhs'+> pmSubst n env args TErrorCase = return $ Nothing+> pmSubst n env args TImpossible = return $ Nothing+> pmSubst n env args (TSCase scr cases)+> = case scr of+> P n -> do (e' , args') <- alookup [] n args+> pmSubstCases e' cases args'+> e -> do e' <- substArgNames args e+> e' <- eval (True, True) e' [] env []+> pmSubstCases e' cases args+> where alookup acc n ((x,arg@(Left (a, aenv, apats))):args) +> | n == x = do e' <- eval (False, True) a [] aenv apats+> return (e', acc ++ (x, Right e'):args)+> alookup acc n ((x,Right e'):args) +> | n == x = return (e', acc ++ (x, Right e'):args)+> alookup acc n (a:args) = alookup (acc ++ [a]) n args++> pmSubstCases e [] args = return Nothing+> pmSubstCases e (c:cs) args +> = do t <- pmCase e c args+> case t of+> (Just t', _) -> return (Just t')+> (Nothing, False) -> pmSubstCases e cs args+> _ -> return Nothing++Matching will either succeed, fail (but not be stuck), or realise it's stuck++> pmCase e (TDefault rhs) args = do v <- pmSubst n env args rhs+> return (v, False)+> pmCase e (TAlt con t cargs sc) args+> | Just (t', cargs') <- getConArgs e []+> = if (t==t' && length cargs == length cargs')+> then do v <- pmSubst n env +> (args ++ zip cargs (map Right cargs')) sc+> return (v, False)+> else return (Nothing, False)+> | otherwise = return (Nothing, True)+> pmCase (Const e) (TConstAlt c sc) args+> = case cast e of+> Just e' -> if (e'==c) +> then do v <- pmSubst n env args sc+> return (v, False)+> else return (Nothing, False)+> Nothing -> return (Nothing, False)+> pmCase _ _ _ = return (Nothing, True)++> traceIf t s x = if t then (trace s x) else x+ > eval_nfEnv :: Env Name -> Gamma Name -> Indexed Name -> Indexed Name > eval_nfEnv env g t > = eval_nf (addenv env g) t@@ -234,3 +460,21 @@ > = Bind x (B b (tidy' ns t)) (Sc (tidy' (x:ns) tm)) > tidy' ns (App f a) = App (tidy' ns f) (tidy' ns a) > tidy' ns x = x++Various tracing facilities for spying on specific cases++> tracefns = []++> matchtrace n xs =+> if (n `elem` tracefns)+> then trace ("Matching " ++ n ++ " " ++ show (map (\(x,y,z) -> x) xs))+> else id++> rhstrace :: String -> TT Name -> [(Name, TT Name)] -> a -> a+> rhstrace n rhs pbinds =+> if (n `elem` tracefns)+> then trace ("Returned " ++ n ++ " => " ++ show rhs ++ "\n" +++> showb pbinds)+> else id+> where showb [] = ""+> showb (m:xs) = " " ++ show m ++ "\n" ++ showb xs
− Ivor/Grouper.lhs
@@ -1,59 +0,0 @@-> {-# OPTIONS_GHC -fglasgow-exts #-}--> module Ivor.Grouper where--> import Ivor.TTCore-> import Ivor.Nobby-> import Ivor.Constant--TT expressions with lambdas/function arguments grouped, for better lambda-lifting.--> data GroupTT n-> = GP n-> | GV Int-> | GCon Int n [GroupTT n] -- Saturated now-> | GTyCon n Int-> | GElim n-> | GApp (GroupTT n) [GroupTT n]-> | GLam [GroupTT n] Int (GroupTT n) -- Variables and level-> | GLet (GroupTT n) (GroupTT n) (GroupTT n)-> | GPi (GroupTT n) (GroupTT n)-> | GProj Int (GroupTT n)-> | forall c. Constant c => GConst c-> | GStar-> | GCant-> -- deriving Show--> group :: Show n => Levelled n -> GroupTT n-> group (Lev term) = gr 0 term where-> gr l (P n) = GP n-> gr l (V i) = GV i-> gr l c@(Con t n a) = mkApp l c []-> gr l (TyCon n a) = GTyCon n a-> gr l (Elim n) = GElim n-> gr l c@(App f a) = mkApp l c []-> gr l (Bind n (B Lambda t) (Sc sc)) = mkLam (l+1) [gr l t] sc-> gr l (Bind n (B Pi t) (Sc sc)) = GPi (gr l t) (gr (l+1) sc)-> gr l (Bind n (B (Let v) t) (Sc sc)) -> = GLet (gr l v) (gr l t) (gr (l+1) sc)-> gr l (Proj _ i t) = GProj i (gr l t)-> gr l (Const c) = GConst c-> gr l (Label t _) = gr l t-> gr l (Call _ t) = gr l t-> gr l (Return t) = gr l t-> gr l Star = GStar-> gr _ _ = GCant--> mkApp l (App f a) sp = mkApp l f ((gr l a):sp)-> mkApp l (Con t n a) sp | length sp == a = GCon t n sp-> | otherwise = saturate l t n a sp-> mkApp l x sp = GApp (gr l x) sp--> mkLam l xs (Bind n (B Lambda t) (Sc sc)) -> = mkLam (l+1) (xs++[gr l t]) sc-> mkLam l xs sc = GLam xs (l-length xs) (gr l sc)--> saturate lev tag name arity sp -> = error $ "Constructor saturation unimplemented " ++ show term-
− Ivor/ICompile.lhs
@@ -1,93 +0,0 @@-FIXME: I don't believe this is used. Make it go away.--> module Ivor.ICompile where--> import Ivor.TTCore-> import Ivor.Datatype-> import Ivor.Nobby-> import Ivor.Gadgets-> import Ivor.Values--> import Data.List-> import Debug.Trace--Structure of simple case expressions, from which we can build actual code for-elimination rules in whatever form we like, eg for NBE or compiled code.--> data SimpleCase = Case Name Int [SimpleCase] -- case x::ty of xs, x is a local var-> | IReduce (Indexed Name) -- Found a reduction!-> | Impossible -- No well-typed term can get here-> deriving Show--Compile a set of iota schemes to simple case structure.--TMP ASSUMPTION: There is always one argument where all cases are disjoint.-We can make sure this is always the case even for detaggable/collapsible-families, although we should do better later.--> compileSchemes :: [Scheme Name] -> SimpleCase-> compileSchemes [] = Impossible-> compileSchemes ss = icomp ss [0..(length (getPat (ss!!0)))-1]-> where icomp ss es = let pats = transpose (map getPat ss) in-> let (pats',es') = unzip $ orderPatts (zip pats es) in-> let ss' = mangleArgOrder ss (reverse es') in-> let top = map schhead ss'-> rest = map schtail ss' in-> icomp' top rest es'-> schhead (Sch x bs red) = (head x, red)-> schtail (Sch x bs red) = Sch (tail x) bs red-> icomp' x xs (e:es) | allDisjoint (map fst x) = doCase1 e x-> | otherwise = error "Can't find a scrutinee"-> orderPatts = sortBy cmpPat-> cmpPat (p,v) (p',v') = compare (numDisjoint p') (numDisjoint p)--I wish I'd written a comment here when I wrote this...--> mangleArgOrder :: [Scheme Name] -> [Int] -> [Scheme Name]-> mangleArgOrder [] _ = []-> mangleArgOrder (x:xs) es = (ma' x es):(mangleArgOrder xs es)-> where ma' (Sch ps bs ired) es = Sch (reorder ps es) bs ired-> reorder ps xs = foldl (\ih x -> (ps!!x):ih) [] xs--> allDisjoint ps = numDisjoint ps == length ps--> numDisjoint :: [Pattern n] -> Int-> numDisjoint [] = 0-> numDisjoint (x:xs) | x `djWith` xs = 1+(numDisjoint xs)-> | otherwise = numDisjoint xs-> where djWith (PCon _ _ _ _) [] = True-> djWith _ [] = False-> djWith x (y:ys) | dj x y = djWith x ys-> | otherwise = False-> dj (PCon x _ _ _) (PCon y _ _ _) = x /= y-> dj _ _ = False--Case 1: All patterns are disjoint.--> doCase1 :: Int -> [(Pattern Name, Indexed Name)] -> SimpleCase-> doCase1 x ps = Case (ty ps) x (order ps)-> where order ps = insertDefaults-> (sortBy (\ (x,y) (x',y') -> compare x x') ps)-> insertDefaults ps = id' 0 ps-> id' n [] = []-> id' n allps@((PCon i _ _ _,t):ps)-> | n == i = (IReduce t):(id' (n+1) ps)-> | otherwise = Impossible:(id' (n+1) allps)-> ty ((PCon _ _ tyname _, _):xs) = tyname---Make an elimination rule implementation from a simple case expression.--> mkElim :: Name -> (Indexed Name) -> Int -> SimpleCase -> ElimRule-> mkElim ename ty arity cs sp | size sp /= arity = Nothing-> | otherwise = doElim sp cs-> where doElim sp Impossible = Nothing-> doElim sp (Case _ x cs) = let xval = (sp??x) in-> case xval of-> (MR (RCon tag _ _)) -> doElim sp (cs!!tag)-> _ -> Nothing-> doElim sp (IReduce (Ind t))-> = let recrule = mkElim ename ty arity cs-> gam = extend emptyGam (ename,G (ElimRule recrule) ty defplicit)-> red = (nf gam (VG (revlistify sp)) [] False t)-> in (Just red)
Ivor/Nobby.lhs view
@@ -40,18 +40,18 @@ > eval stage gamma (VG g) (V n) > | (length g) <= n = MB (BV n, MR RdInfer) Empty -- error $ "Reference out of context! " ++ show n ++ ", " ++ show (length g) ---> | otherwise = g!!n+> | otherwise = traceIndex g n "Nobby fail" > eval stage gamma g (P n) > = case lookup n patvals of > Just val -> val > Nothing -> evalP (lookupval n gamma) > where evalP (Just Unreducible) = (MB (BP n,pty n) Empty) > evalP (Just Undefined) = (MB (BP n, pty n) Empty)-> evalP (Just (PatternDef p@(PMFun 0 pats) _ _)) =+> evalP (Just (PatternDef p@(PMFun 0 pats) _ _ _)) = > case patmatch gamma g pats [] of > Nothing -> (MB (BPatDef p n, pty n) Empty) > Just v -> v-> evalP (Just (PatternDef p _ _)) = (MB (BPatDef p n, pty n) Empty)+> evalP (Just (PatternDef p _ _ _)) = (MB (BPatDef p n, pty n) Empty) > evalP (Just (Partial (Ind v) _)) = (MB (BP n, pty n) Empty) > evalP (Just (PrimOp f _)) = (MB (BPrimOp f n, pty n) Empty) > evalP (Just (Fun opts (Ind v)))@@ -74,6 +74,7 @@ > where bty = eval stage gamma g ty > eval stage gamma g (Const x) = (MR (RdConst x)) > eval stage gamma g Star = MR RdStar+> eval stage gamma g Erased = MR RdErased > eval stage gamma (VG g) (Bind n (B Lambda ty) (Sc sc)) = > (MR (RdBind n (B Lambda (eval stage gamma (VG g) ty)) > (Kr (\w x -> eval stage gamma (VG (x:(weaken w g))) sc,Wk 0))))@@ -238,6 +239,7 @@ > weakenp i (RdBind n bind sc) = RdBind n (weakenp i bind) (weakenp i sc) > weakenp i (RdConst x) = RdConst x > weakenp i RdStar = RdStar+> weakenp i RdErased = RdErased > weakenp i (RCon t n sp) = RCon t n (fmap (weakenp i) sp) > weakenp i (RTyCon n sp) = RTyCon n (fmap (weakenp i) sp) > weakenp i (RdLabel t c) = RdLabel (weakenp i t) (weakenp i c)@@ -292,6 +294,7 @@ > instance Quote (Ready Kripke) (Ready Scope) where > quote' ns (RdConst x) = RdConst x > quote' ns RdStar = RdStar+> quote' ns RdErased = RdErased > quote' ns (RdBind n b@(B _ ty) sc) > = let n' = mkUnique n ns in > RdBind n' (quote' ns b)@@ -387,6 +390,7 @@ > forget (RdBind n b (Sc sc)) = Bind n (forget b) (Sc (forget sc)) > forget (RdConst x) = (Const x) > forget RdStar = Star+> forget RdErased = Erased > forget (RCon t c sp) = makeApp (Con t c (size sp)) (fmap forget sp) > forget (RTyCon c sp) = makeApp (TyCon c (size sp)) (fmap forget sp) > forget (RdLabel t c) = Label (forget t) (forget c)@@ -487,7 +491,7 @@ > instance Functor Global where > fmap f (Fun opts n) = Fun opts $ fmap f n > fmap f (ElimRule e) = ElimRule e-> fmap f (DCon t i) = DCon t i+> fmap f (DCon t i fc) = DCon t i fc > fmap f (TCon i (Elims en cn cons)) > = TCon i (Elims (f en) (f cn) (fmap f cons))
+ Ivor/PMComp.lhs view
@@ -0,0 +1,270 @@+> {-# OPTIONS_GHC -fglasgow-exts #-}++> module Ivor.PMComp where++Pattern matching compiler, convert to simple case expressions+(This was originally in Idris, and ideally the Idris version would reuse+this. Let's just make it work first...)++> import Ivor.TTCore+> import Ivor.Values++> import Data.Typeable+> import Debug.Trace+> import Control.Monad.State+> import List hiding (partition)++> data CS = CS Int++> pmcomp :: Gamma Name -> +> Name -> TT Name -> PMFun Name -> +> ([Name], TSimpleCase Name)+> pmcomp ctxt n ty (PMFun arity ps)+> = pm' n (map mkPat ps)+> where mkPat (Sch args _ (Ind rv))+> = Clause args rv+> pm' n ps = evalState (doCaseComp ctxt ps) (CS 0)++> data Clause = Clause [Pattern Name] (TT Name)++> isVarPat (Clause ((PVar _):ps) _) = True+> isVarPat (Clause (PTerm:ps) _) = True+> isVarPat _ = False++> isConPat (Clause ((PCon _ _ _ _):ps) _) = True+> isConPat (Clause ((PConst _):ps) _) = True+> isConPat _ = False++> data Partition = Cons [Clause]+> | Vars [Clause]++> partition :: Gamma Name -> [Clause] -> [Partition]+> partition ctxt [] = []+> partition ctxt ms@(m:_)+> | isVarPat m = let (vars, rest) = span isVarPat ms in+> (Vars vars):partition ctxt rest +> | isConPat m = let (cons, rest) = span isConPat ms in+> (Cons cons):(partition ctxt rest)+> partition ctxt x = error "Can't happen PMComp partition"++Make sure the variables bound have proper pattern names (to avoid embarrassing+clashes)++> pnames :: [Name] -> TSimpleCase Name -> TSimpleCase Name+> pnames ns (TSCase tm alts) = TSCase (pnamestm ns tm) (map (pnamesalt ns) alts)+> pnames ns (TTm tm) = TTm (pnamestm ns tm)+> pnames ns x = x++> pnamestm :: [Name] -> TT Name -> TT Name+> pnamestm [] tm = tm+> pnamestm (x:xs) tm = substName x (P (PN x)) (Sc (pnamestm xs tm))++> pnamesalt ns (TAlt c t args sc) +> = TAlt c t (map PN args) (pnames (ns++args) sc)+> pnamesalt ns (TConstAlt c sc) = TConstAlt c (pnames ns sc)+> pnamesalt ns (TDefault sc) = TDefault (pnames ns sc)++> doCaseComp :: Gamma Name ->+> [Clause] -> State CS ([Name], TSimpleCase Name)+> doCaseComp ctxt cs = do vs <- newVars cs+> let (cs', vs') = reOrder cs vs+> sc <- match ctxt (map mkVT vs') cs' TErrorCase+> -- return names in original order (this is the+> -- argument list we're making)+> return (vs, sc)+> where newVars [] = return []+> newVars ((Clause ps _):_)+> = do CS i <- get+> put (CS (i+(length ps)))+> return $ map (\x-> MN ("cvar", x)) [i..(i+(length ps)-1)]+> mkVT x = P x++Reorder variables so that one with most disjoint cases is first.+(Actually, quick hack, just reverse them, since then the dependent things+will at least be looked at last, and we'll be matching on the real arguments+rather than indices.)++> reOrder cs vs = let djs = (reverse.sort.(mapI 0 dj).transpose.allArgs) cs in+> (pickAll (map snd djs) cs, pick (map snd djs) vs)+> pickAll _ [] = []+> pickAll djs ((Clause args rest):cs) +> = (Clause (pick djs args) rest):(pickAll djs cs)+> allArgs [] = []+> allArgs ((Clause args rest):cs) = args:(allArgs cs)++> pick [] _ = []+> pick (i:is) xs = if (i<length xs) then xs!!i : (pick is xs)+> else error ("ARGH! pick " ++ show i)++Count the number of different constructor forms in xs++> dj xs = dj' [] xs+> dj' acc [] = length (nub acc)+> dj' acc (PCon i _ _ p:xs) = dj' (i:acc) xs+> dj' acc (_:xs) = dj' acc xs++> mapI i f [] = []+> mapI i f (x:xs) = (f x, i):(mapI (i+1) f xs)++> match :: Gamma Name -> +> [TT Name] -> -- arguments+> [Clause] -> -- clauses+> TSimpleCase Name -> -- fallthrough (error case)+> State CS (TSimpleCase Name)+> match ctxt [] ((Clause [] ret):_) err +> = return $ TTm ret -- run out of arguments+> match ctxt vs cs err +> = mixture ctxt vs (partition ctxt cs) err++> mixture :: Gamma Name -> +> [TT Name] ->+> [Partition] -> TSimpleCase Name -> State CS (TSimpleCase Name)+> mixture ctxt vs [] err = return err+> mixture ctxt vs ((Cons ms):ps) err +> = do fallthrough <- (mixture ctxt vs ps err)+> conRule ctxt vs ms fallthrough+> mixture ctxt vs ((Vars ms):ps) err +> = do fallthrough <- (mixture ctxt vs ps err)+> varRule ctxt vs ms fallthrough++In the constructor rule:++For each distinct constructor (or constant) create a group of possible+patterns in ConType and Group++> data ConType = CName Name Int -- ordinary named constructor+> | forall c. Constant c => CConst c -- constant pattern++> data Group = ConGroup ConType -- constructor+> -- arguments and rest of alternative for each instance+> [([Pattern Name], Clause)] ++> conRule :: Gamma Name -> [TT Name] ->+> [Clause] -> TSimpleCase Name -> State CS (TSimpleCase Name)+> conRule ctxt (v:vs) cs err = +> do groups <- groupCons cs+> caseGroups ctxt (v:vs) groups err++> caseGroups :: Gamma Name -> [TT Name] ->+> [Group] -> TSimpleCase Name ->+> State CS (TSimpleCase Name)+> caseGroups ctxt (v:vs) gs err+> = do g <- altGroups gs+> return $ TSCase v g+> where altGroups [] = return [TDefault err]+> altGroups ((ConGroup (CName n i) args):cs)+> = do g <- altGroup n i args+> rest <- altGroups cs+> return (g:rest)+> altGroups ((ConGroup (CConst cval) args):cs)+> = do g <- altConstGroup cval args+> rest <- altGroups cs+> return (g:rest)++> altGroup n i gs +> = do (newArgs, nextCs) <- argsToAlt gs+> matchCs <- match ctxt (map P newArgs++vs)+> nextCs err+> return $ TAlt n i newArgs matchCs+> altConstGroup n gs+> = do (_, nextCs) <- argsToAlt gs+> matchCs <- match ctxt vs nextCs err+> return $ TConstAlt n matchCs++Find out how many new arguments we need to generate for the next step+of matching (since we're going to be matching further on the arguments+of each group for the constructor, and we'll need to give them names)++Return the new variables we've added to do case analysis on, and the+new set of clauses to match.++> argsToAlt :: [([Pattern Name], Clause)] -> State CS ([Name], [Clause])+> argsToAlt [] = return ([],[])+> argsToAlt rs@((r,m):_) +> = do newArgs <- getNewVars r+> -- generate new match alternatives, by combining the arguments+> -- matched on the constructor with the rest of the clause+> return (newArgs, addRs rs)+> where getNewVars [] = return []+> getNewVars ((PVar n):ns) = do nsv <- getNewVars ns+> return (n:nsv)+> getNewVars (_:ns) = do v <- getVar+> nsv <- getNewVars ns+> return (v:nsv)+> addRs [] = []+> addRs ((r,(Clause ps res) ):rs)+> = (Clause (r++ps) res):(addRs rs)++> getVar :: State CS Name+> getVar = do (CS var) <- get+> put (CS (var+1))+> return (MN ("pvar", var))++> groupCons :: Monad m => [Clause] -> m [Group]+> groupCons cs = gc [] cs+> where gc acc [] = return acc+> gc acc ((Clause (p:ps) res):cs) = do+> acc' <- addGroup p ps res acc+> gc acc' cs++> addGroup p ps res acc = case p of+> PCon i con _ args -> return $ addg con i args (Clause ps res) acc+> PConst cval -> return $ addConG cval (Clause ps res) acc+> pat -> fail $ show pat ++ " is not a constructor or constant (can't happen)"+ +> addg con i conargs res [] +> = [ConGroup (CName con i) [(conargs, res)]]+> addg con i conargs res (g@(ConGroup (CName n j) cs):gs)+> | i == j = (ConGroup (CName n i) (cs ++ [(conargs, res)])):gs+> | otherwise = g:(addg con i conargs res gs)++> addConG :: Constant c => c -> Clause -> [Group] -> [Group]+> addConG con res [] = [ConGroup (CConst con) [([],res)]]+> addConG con res (g@(ConGroup (CConst n) cs):gs)+> | constEq con n = (ConGroup (CConst n) (cs ++ [([], res)])):gs+> | otherwise = g:(addConG con res gs)++HATEHATEHATE. This completely defeats the point of having generic constants.+However, it seems there is no alternative... pattern matching will only work+for Int, String and Char as a result.++> constEq :: (Constant a, Constant b) => a -> b -> Bool+> constEq x y = ceq_1 (cast x) (cast y)+> || ceq_2 (cast x) (cast y)+> || ceq_3 (cast x) (cast y)+> where ceq_1 :: Maybe Int -> Maybe Int -> Bool+> ceq_1 (Just x) (Just y) = x == y+> ceq_1 _ _ = False+> ceq_2 :: Maybe String -> Maybe String -> Bool+> ceq_2 (Just x) (Just y) = x == y+> ceq_2 _ _ = False+> ceq_3 :: Maybe Char -> Maybe Char -> Bool+> ceq_3 (Just x) (Just y) = x == y+> ceq_3 _ _ = False+++In the variable rule:++case v args of+ p pats -> r1+ ...+ pn patsn -> rn++====>++case args of+ pats -> r1[p/v]+ ...+ patsn -> rn[p/v]++> varRule :: Gamma Name -> [TT Name] ->+> [Clause] -> TSimpleCase Name -> State CS (TSimpleCase Name)+> varRule ctxt (v:vs) alts err = do+> let alts' = map (repVar v) alts+> match ctxt vs alts' err+> where repVar v (Clause ((PVar p):ps) res) +> = let nres = substName p v (Sc res) in+> {- trace (show v ++ " for " ++ dbgshow p ++ " in " ++ show res ++ " gives " ++ show nres) $ -}+> Clause ps nres+> repVar v (Clause (PTerm:ps) res) = Clause ps res+
Ivor/PatternDefs.lhs view
@@ -26,8 +26,9 @@ > Bool -> -- Check for coverage > Bool -> -- Check for well-foundedness > Maybe [(Name, Int)] -> -- Names to specialise+> Maybe [(Name, ([Int], Int))] -> -- Names and static args, when specialising > IvorM ([(Name, PMFun Name, Indexed Name)], [(Name, Indexed Name)], Bool)-> checkDef gam fn tyin pats cover wellfounded spec = do+> checkDef gam fn tyin pats cover wellfounded spec specst = do > --x <- expandCon gam (mkapp (Var (UN "S")) [mkapp (Var (UN "S")) [Var (UN "x")]]) > --x <- expandCon gam (mkapp (Var (UN "vcons")) [RInfer,RInfer,RInfer,mkapp (Var (UN "vnil")) [Var (UN "foo")]]) > clausesIn <- mapM (expandClause gam) pats@@ -39,7 +40,7 @@ > checkNotExists fn gam > gam' <- gInsert fn (G Undefined ty defplicit) gam > clauses' <- validClauses gam' fn ty clauses'-> (pmdefs, newdefs, covers) <- matchClauses gam' fn pats tyin ty cover clauses' spec+> (pmdefs, newdefs, covers) <- matchClauses gam' fn pats tyin ty cover clauses' spec specst > wf <- return True > {- if wellfounded then > do checkWellFounded gam fn [0..arity-1] pmdef@@ -48,7 +49,7 @@ > Nothing -> return False > _ -> return True -} > let total = wf && covers-> return (pmdefs, newdefs, total)+> return (mangleVars pmdefs, newdefs, total) > where checkNotExists n gam = case lookupval n gam of > Just Undefined -> return () > Just _ -> fail $ show n ++ " already defined"@@ -183,8 +184,9 @@ > Bool -> -- Check coverage > [(Indexed Name, Indexed Name)] -> > Maybe [(Name, Int)] ->+> Maybe [(Name, ([Int], Int))] -> > IvorM ([(Name, PMFun Name, Indexed Name)], [(Name, Indexed Name)], Bool)-> matchClauses gam fn pats tyin ty@(Ind ty') cover gen spec = do+> matchClauses gam fn pats tyin ty@(Ind ty') cover gen spec specst = do > let raws = zip (map mkRaw pats) (map getRet pats) > (checkpats, newdefs, aux, covers) <- mytypechecks gam raws [] [] [] True > cv <- if cover then @@ -212,7 +214,7 @@ > do (tm@(Ind tmtt), pty, > rtm@(Ind rtmtt), rty, env, newdefs) <- checkAndBindPair gam clause ret > unified <- unifyenv gam env pty rty-> let gam' = foldl (\g (n,t) -> extend g (n,G Undefined t 0))+> let gam' = foldl (\g (n,t) -> extend g (n,G Undefined t defplicit)) > gam newdefs > let rtmtt' = substNames unified rtmtt > -- checkConvEnv env gam pty rty $ "Pattern error: " ++ show pty ++ " and " ++ show rty ++ " are not convertible " ++ show unify@@ -220,11 +222,13 @@ > let namesbound = getNames (Sc tmtt) > checkAllBound (fileLine ret) namesret namesbound (Ind rtmtt') tmtt rty pty > -- trace (show env) $-> let specrtm = case spec of-> Nothing -> Ind rtmtt'+> -- Actually, let's try specialising elsewhere++> let specrtm = Ind (forced gam' rtmtt') -- case spec of+> {- Nothing -> Ind rtmtt' > Just [] -> eval_nf gam (Ind rtmtt')-> Just ns -> eval_nf_limit gam (Ind rtmtt') ns-> return ((tm, specrtm, env), [], newdefs, True)+> Just ns -> eval_nf_limit gam (Ind rtmtt') ns specst -}+> return ((Ind (forced gam tmtt), specrtm, env), [], newdefs, True) > mytypecheck gam (clause, (RWith addprf scr pats)) i = > do -- Get the type of scrutinee, construct the type of the auxiliary definition > (tm@(Ind clausett), clausety, _, scrty@(Ind stt), env) <- checkAndBindWith gam clause scr fn@@ -248,10 +252,10 @@ > [scr] ++ if addprf then > [RApp (RApp (Var (UN "refl")) RInfer) RInfer] > else [])-> let gam' = insertGam newname (G Undefined newfnTy 0) gam+> let gam' = insertGam newname (G Undefined newfnTy defplicit) gam > newpdef <- mapM (newp tm newargs 1 addprf) (zip newpats pats) > (chk, auxdefs, _, _) <- mytypecheck gam' (clause, (RWRet ret)) i-> (auxdefs', newdefs, covers) <- checkDef gam' newname (forget newfnTy) newpdef False cover spec+> (auxdefs', newdefs, covers) <- checkDef gam' newname (forget newfnTy) newpdef False cover spec specst > return (chk, auxdefs++auxdefs', newdefs, covers) > addLastArg (RBind n (B Pi arg) x) ty scr addprf @@ -311,9 +315,10 @@ > mkpat (App f a) = addPatArg (mkpat f) (mkpat a) > mkpat (Con i nm ar) = mkPatV nm (lookupval nm gam) > mkpat (Const c) = PConst c+> mkpat Erased = PTerm > mkpat _ = PTerm -> mkPatV n (Just (DCon t x)) = PCon t n (tyname n) []+> mkPatV n (Just (DCon t x _)) = PCon t n (tyname n) [] > mkPatV n _ = PVar n > tyname n = case (getTyName gam n) of > Just x -> x@@ -334,7 +339,7 @@ > checkCoverage pats [] = return () > checkCoverage pats (c:cs) > | length (filter (matches c) pats) > 0 = checkCoverage pats cs-> | otherwise = fail $ "Missing clause: " ++ show c+> | otherwise = tacfail $ "Missing clause: " ++ show c > matches p t = getMatches p t /= Nothing @@ -347,7 +352,8 @@ > matches' (P x) (P y) | x == y = return [(y, P x)] > matches' t (P n) = return [(n,t)] > matches' (P nm@(MN ("INFER",_))) t = return []-> matches' x y = if x == y then return [] else fail "With pattern does not match parent"+> matches' (Bind _ _ _) (Bind _ _ _) = return []+> matches' x y = if x == y then return [] else fail $ "With pattern does not match parent" > expandClause :: Gamma Name -> RawScheme -> IvorM [RawScheme]@@ -477,3 +483,39 @@ union (gpp 0 pats) (getPatPos numargs xs) where gpp pos [] = [] gpp pos ((PCon _ _ _ _):xs) = pos:(gpp (pos+1) xs)++Convert human names in pattern definitions to machine names (to avoid+ambiguities when running)++FIXME: This is really just an almighty hack until patterns are represented +better in terms.++> mangleVars :: [(Name, PMFun Name, Indexed Name)] ->+> [(Name, PMFun Name, Indexed Name)]+> mangleVars xs = map (\ (n, pm, ty) -> (n, manglePM pm, ty)) xs++> manglePM :: PMFun Name -> PMFun Name+> manglePM (PMFun a ps) = PMFun a (map mangleScheme ps)++> mangleScheme :: Scheme Name -> Scheme Name+> mangleScheme (Sch ps env (Ind rhs))+> = let (ps', vars) = collectVars ([], []) ps in+> Sch ps' env (Ind (renameRHS vars rhs))+> where renameRHS [] rhs = rhs+> renameRHS (x:xs) rhs +> = renameRHS xs $ substName x (P (newN x)) (Sc rhs)++> newN x = PN x -- MN (x,42)+> -- newN (MN (x, i)) = MN (x, i+42)++> collectVars acc [] = acc+> collectVars (aps, avars) (p:ps) +> = let (p', vars) = collectPat p in+> collectVars (aps++[p'], nub (avars++vars)) ps++> collectPat (PVar n) = (PVar (newN n), [n])+> collectPat (PCon a tag ty ps) =+> let (ps', vars') = collectVars ([],[]) ps in+> (PCon a tag ty ps', vars')+> collectPat x = (x, [])+
− Ivor/RunTT.lhs
@@ -1,107 +0,0 @@-> {-# OPTIONS_GHC -fglasgow-exts #-}--> module Ivor.RunTT where--FIXME: We don't use this. Got to go.--Representation of the run-time language.-Used for spitting out GHC core.--> import Ivor.TTCore-> import Ivor.Gadgets-> import Ivor.ICompile-> import Ivor.Nobby-> import Ivor.Values--When we compile, we need to know the term as well as bits of info about-its type, ie its arity and emptiness.--> type RunValue = (RunTT, TypeInfo)--> data RunTT =-> RTVar Int -- de Bruijn level-> | RTFun Name-> | RTCon Int Name [RunValue] -- Fully applied, Name is for display only-> | RTElim Name RunValue RunValue [RunValue] -- Fully applied, with-> -- target, motive, methods-> | RTApp RunValue [RunValue]-> | RTBind (RTBinder,TypeInfo) RunValue -> | RTCase Name RunValue [RunValue] -- name is type case is on-> | RTProj Name Int RunValue -- name is type we're projecting from-> | forall c. Constant c => RTConst c-> | RTypeVal -- Useless, uninspectable type value-> | RTCantHappen -- Flag on unexecutable code-> -- deriving Show--> data RTBinder = RTLam-> | RTPi-> | RTLet RunValue-> -- deriving Show--> data TypeInfo = TI Int Bool -- Arity, emptiness (whether its the empty type)-> deriving Show--> newtype RunTTs = RGam [(Name,RunTT)]--Make a term in RunTT from a de Bruijn levelled representation--> mkRTFun :: Gamma Name -> Levelled Name -> RunTT-> mkRTFun gam (Lev term) = mkrt 0 term where-> mkrt l (P n) = RTFun n-> mkrt l (V x) = RTVar x-> mkrt l (Con t n 0) = RTCon t n []-> mkrt l c@(Con t n a) = mkApp l c []-> mkrt l (TyCon n x) = RTypeVal-> mkrt l (Elim n) = RTFun n-> mkrt l c@(App f a) = mkApp l c []-> mkrt l (Bind n b (Sc sc)) = RTBind (mkBinder l b) -> ((mkrt (l+1) sc), TI 0 False)-> mkrt l (Proj n i t) = RTProj n i (mkrt l t, TI 0 False)-> mkrt l (Label t _) = mkrt l t-> mkrt l (Call _ t) = mkrt l t-> mkrt l (Return t) = mkrt l t-> mkrt l (Const c) = RTConst c -- error "Sorry, I don't know how to compile constants yet"-> mkrt l (Stage _) = error "Sorry, I can't compile multi-stage programs."-> mkrt l Star = RTypeVal--> mkBinder l (B Lambda t) = (RTLam, TI 0 False)-> mkBinder l (B (Let v) t) = (RTLet (mkrt l v, TI 0 False), TI 0 False)-> mkBinder l (B Pi t) = (RTPi, TI 0 False)--> mkApp l (App f a) sp = mkApp l f ((mkrt l a, TI 0 False):sp)-> mkApp l (Con t n a) sp | length sp == a = RTCon t n sp-> | otherwise = saturate l a (length sp) -> (RTCon t n sp) (RTCon t n sp)-> mkApp l x sp = RTApp (mkrt l x, TI (length sp) False) sp--> saturate lev arity splen acc (RTCon t n sp) -- cached inner constructor-> | splen == arity = acc-> | otherwise = let newcon = RTCon t n (sp++[(RTVar lev, TI 0 False)]) in-> saturate (lev+1) arity (splen+1)-> (RTBind (RTLam, TI 0 False) (newcon, TI 0 False)) -> newcon-> --let c = mkRawApp (Con tag naem arity) sp in- error $ "Saturate " ++ show c-- mkRawApp = forget mr- where mr f [] = f- mr f (x:xs) = mr (App f x) xs---error "Constructor saturation unimplemented"--Make an elimination rule in RunTT from a simple case expression--> mkRTElim :: Name -> Int -> SimpleCase -> RunTT-> mkRTElim ename arity es = fst $ abstract arity (mkrt es)-> where mkrt Impossible = RTCantHappen-> mkrt (IReduce t) = mkRTFun (emptyGam) (mkvarnum t)-> mkrt (Case ty x cs) = RTCase ty (RTVar (arity-x-1), TI 0 False)-> (map mkcase cs)-> mkcase c = (mkrt c, TI 0 False)-> mkvarnum (Ind t) = Lev $ vapp (\ (ctx,i) -> V (arity-i-1)) t--> abstract 0 t = (t, TI 0 False)-> abstract n t = (RTBind (RTLam, TI 0 False) (abstract (n-1) t), TI 0 False)
− Ivor/SC.lhs
@@ -1,174 +0,0 @@-> {-# OPTIONS_GHC -fglasgow-exts #-}--> module Ivor.SC where--Lambda lifter. Two bits:--lift: Takes a TT function definition and returns a set of supercombinators.-elimSC: Takes a simple case expression and returns a supercombinator.--> import Ivor.Grouper-> import Ivor.TTCore-> import Ivor.Nobby-> import Ivor.ICompile-> import Ivor.Constant--> import Debug.Trace--> data SCName = N Name-> | SN Name Int-> deriving Eq--> instance Show SCName where-> show (N n) = show n-> show (SN n i) = "$"++show n ++show i--> type SCs = [(SCName, (Int, SC))]--> data SC = SLam [SCBody] SCBody--> data SCBody-> = SP SCName-> | SV Int-> | SCon Int SCName [SCBody]-> | STyCon SCName Int-> {- | SElim SCName -}-> | SApp SCBody [SCBody]-> | SLet SCBody SCBody SCBody-> | SPi SCBody SCBody-> | SProj Int SCBody-> | forall c. Constant c => SConst c-> | SStar-> | SCase Int [SCBody]-> | SCantHappen-> | SSomeType-> -- deriving Show--Turn a well typed term with de Bruijn levels into a set of supercombinators.-The main supercombinator will have the given name--> lift :: Name -> Levelled Name -> SCs-> lift basename t = collect basename (group (fmap N t))--> collect :: Name -> GroupTT SCName -> [(SCName,(Int,SC))]-> collect basename g = snd $ sc (N basename) [] 0 [] g where-> sc name args next scs (GLam args' lev body)-> = let (next',scs',scargs) = sclist args next scs args'-> (next'',scs'',scb) = scbody (args++scargs) next' scs' body -> newsc = SLam (args++scargs) scb in-> (next'',((name, (length (args++scargs),newsc)):scs''))-> sc name args next scs body-> = let (next',scs',scb) = scbody [] next scs body-> newsc = SLam [] scb in-> (next',((name,(0,newsc)):scs'))--Do the tricky case first. -This is the quick hack version; it ought to-check that previously bound variables are actually used.--> scbody args next scs b@(GLam args' l body) -> = let (next',scs') = sc (SN basename next) args (next+1) scs-> (GLam args' 0 body) in-> (next',scs',mkapp (SP (SN basename next)) (argvals args))-> where mkapp x [] = x-> mkapp x as = SApp x as-> argvals xs = map SV [0..(length xs)-1]--Everything else is pretty much structural...--> scbody args next scs (GP n) = (next, scs, SP n)-> scbody args next scs (GV i) = (next, scs, SV i)-> scbody args next scs (GCon i n as) =-> let (next',scs',scas) = sclist args next scs as in-> (next',scs',SCon i n scas)-> scbody args next scs (GTyCon n i) = (next,scs,STyCon n i)-> scbody args next scs (GElim n) = (next, scs, SP n)-> scbody args next scs (GApp f as) =-> let (next',scs',scf) = scbody args next scs f -> (next'',scs'',scas) = sclist args next' scs' as in-> (next'',scs'',SApp scf scas)-> scbody args next scs (GLet t v sc) =-> let (next',scs',sct) = scbody args next scs t-> (next'',scs'',scv) = scbody args next' scs' v-> (next''',scs''',scsc) = scbody (args++[sct]) next'' scs'' sc in-> (next''',scs''',SLet sct scv scsc)-> scbody args next scs (GPi t sc) =-> let (next',scs',sct) = scbody args next scs t-> (next'',scs'',scsc) = scbody args next' scs' sc in-> (next'',scs'',SPi sct scsc)-> scbody args next scs (GProj i t) =-> let (next',scs',sct) = scbody args next scs t in-> (next',scs',SProj i sct)-> scbody args next scs (GConst c) = (next,scs,SConst c)-> scbody args next scs GStar = (next,scs,SStar)-> scbody _ next scs GCant = (next,scs,SCantHappen)--> sclist args next scs [] = (next,scs,[])-> sclist args next scs (x:xs) -> = let (next',scs',xsc) = scbody args next scs x-> (next'',scs'',xscs) = sclist args next' scs' xs in-> (next'',scs'',xsc:xscs)---Turn a simple case tree into a supercombinator--> elimSC :: Name -> Levelled Name -> SimpleCase -> SC-> elimSC ename (Lev rtype) es = SLam (mkargs rtype) (mksc es)-> where mksc Impossible = SCantHappen-> mksc (IReduce t) = mkreduce (mkvarnum t)-> mksc (Case _ x cs) = SCase (arity-x-1)-> (map mksc cs)-> mkvarnum (Ind t) = vapp (\ (ctx,i) -> V (arity-i-1)) t-> args = mkargs rtype-> arity = length args-- Reductions will have no lambdas, so an easy, boring, structural job.- -> mkreduce (P n) = SP (N n)-> mkreduce (Elim n) = SP (N n)-> mkreduce (V x) = SV x-> mkreduce ap@(App f a) = mkapp ap []-> mkreduce (Proj _ i t) = SProj i (mkreduce t)-> mkreduce (TyCon n i) = STyCon (N n) i-> mkreduce (Con i t a) = SSomeType-> mkreduce x = SSomeType--> mkapp (App f a) sp = mkapp f ((mkreduce a):sp)-> mkapp x sp = SApp (mkreduce x) sp--> mkargs (Bind n (B Pi t) (Sc sc)) = (mkreduce t):(mkargs sc)-> mkargs t = []--Ugly printer--> instance Show SC where-> show = showSC---> showSCs :: SCs -> String-> showSCs [] = ""-> showSCs ((n,(a,sc)):xs) = show n ++ "("++show a++") = " ++ showSC sc ++ "\n" ++ showSCs xs--> showSC (SLam args body) = "\\" ++ showargs 0 args ++ " -> " ++ showBody body-> where showargs i [] = ""-> showargs i (x:xs) = "v" ++ show i ++ ":" ++ showBody x ++ " " ++ showargs (i+1) xs--> showBody (SP n) = show n-> showBody (SV i) = "v"++show i-> showBody (SCon i n bs) = show n ++ "<" ++ showBs bs ++ ">"-> showBody (STyCon n i) = show n-> --showBody (SElim n) = show n-> showBody (SApp f as) = showBody f ++ "(" ++ showBs as ++ ")"-> showBody (SLet t v b) = "let " ++ showBody v ++ ":" ++ showBody t ++ " in "-> ++ showBody b-> showBody (SPi t sc) = "{"++showBody t++"}"++showBody sc-> showBody (SProj i sc) = "("++showBody sc++")!"++show i-> showBody (SConst c) = show c-> showBody (SCantHappen) = "Impossible"-> showBody (SSomeType) = "Unknown"-> showBody (SCase e cs) = "case v" ++ show e ++ " {" ++ showBs cs ++ "}"-> showBody (SStar) = "*"--> showBs [] = ""-> showBs [x] = showBody x-> showBs (x:xs) = showBody x ++ "," ++ showBs xs
Ivor/Scopecheck.lhs view
@@ -17,7 +17,7 @@ > case lookup n env of > Just _ -> P n > Nothing -> case glookup n gam of-> Just ((DCon tag i), _) -> Con tag n i+> Just ((DCon tag i _), _) -> Con tag n i > Just ((TCon i _),_) -> TyCon n i > _ -> P n > sc env (RApp f a) = App (sc env f) (sc env a)
Ivor/State.lhs view
@@ -8,16 +8,12 @@ > import Ivor.Typecheck > import Ivor.Datatype > import Ivor.MakeData-> import Ivor.ICompile-> import Ivor.Grouper-> import Ivor.SC-> import Ivor.Bytecode-> import Ivor.CodegenC > import Ivor.Tactics as Tactics > import Ivor.Display > import Ivor.Unify > import Ivor.Errors > import Ivor.Values+> import Ivor.PMComp > import System.Environment > import Data.List@@ -107,10 +103,15 @@ > ctxt <- addCons xs ctxt > gInsert n gl ctxt > addElim ctxt erule schemes = do-> newdefs <- gInsert (fst erule)-> (G (PatternDef schemes True False) (snd erule) defplicit)+> let rnm = fst erule+> let rty = snd erule+> newdefs <- gInsert rnm+> (G (patternDef ctxt rnm rty schemes True False) rty defplicit) > ctxt > return newdefs++> patternDef gam n (Ind ty) pmf t g = PatternDef pmf t g (pmcomp gam n ty pmf)+ > doMkData :: Bool -> IState -> Datadecl -> IvorM IState > doMkData elim st (Datadecl n ps rawty cs)
Ivor/TT.lhs view
@@ -10,38 +10,34 @@ > -- Public interface for theorem proving gadgets. > module Ivor.TT(-- * System state-> emptyContext, Context,-> Ivor.TT.check,fastCheck,-> checkCtxt,converts,+> fastCheck,checkCtxt,converts, > Ivor.TT.compile,+> module Ivor.CtxtTT, > -- * Exported view of terms-> module VTerm, IsTerm, IsData, -> -- * Errors-> TTError(..), ttfail, getError, TTM,+> module VTerm, > -- * Definitions and Theorems-> addDef,addTypedDef,addData,addDataNoElim,+> addDef,addTypedDef, > addAxiom,declare,declareData, > theorem,interactive, > addPrimitive,addBinOp,addBinFn,addPrimFn,addExternalFn, > addEquality,forgetDef,addGenRec,addImplicit, > -- * Pattern matching definitions > PClause(..), Patterns(..),PattOpt(..),addPatternDef,-> toPattern,+> toPattern, spec, > -- * Manipulating Proof State > proving,numUnsolved,suspend,resume, > save, restore, clearSaved, > proofterm, getGoals, getGoal, uniqueName, -- getActions > allSolved,qed, > -- * Examining the Context-> eval, whnf, evalnew, evalnewWithout, evalnewLimit, evalCtxt, getDef, defined, getPatternDef,+> module Ivor.EvalTT, evalCtxt,+> getDef, defined, getPatternDef, getCompiledPatternDef, > getAllTypes, getAllDefs, getAllPatternDefs, isAuxPattern, getConstructors, > getInductive, getAllInductives, getType, > Rule(..), getElimRule, nameType, getConstructorTag, > getConstructorArity, > Ivor.TT.freeze,Ivor.TT.thaw, > -- * Goals, tactic types-> Goal,goal,defaultGoal,-> Tactic, --Tactics.TacticAction(..), > GoalData, bindings, goalName, goalType, > goalData, subGoals, > -- * Primitive Tactics@@ -100,18 +96,17 @@ > import Ivor.Gadgets > import Ivor.Nobby > import Ivor.Evaluator-> import Ivor.SC-> import Ivor.Bytecode > import Ivor.Datatype > import Ivor.Constant > import Ivor.ViewTerm as VTerm > import Ivor.TermParser > import qualified Ivor.Tactics as Tactics-> import Ivor.Compiler as Compiler-> import Ivor.CodegenC > import Ivor.PatternDefs > import Ivor.Errors > import Ivor.Values+> import Ivor.EvalTT+> import Ivor.CtxtTT+> import Ivor.PMComp > import Data.List > import Debug.Trace@@ -119,61 +114,21 @@ > import Control.Monad(when) > import Control.Monad.Error(Error,noMsg,strMsg) -> -- | Abstract type representing state of the system.-> newtype Context = Ctxt IState--> -- | Abstract type representing goal or subgoal names.-> data Goal = Goal Name | DefaultGoal-> deriving Eq--> instance Show Goal where-> show (Goal g) = show g-> show (DefaultGoal) = "Default Goal"--> goal :: String -> Goal-> goal g = Goal $ UN g--> defaultGoal :: Goal-> defaultGoal = DefaultGoal--> -- |A tactic is any function which manipulates a term at the given goal-> -- binding. Tactics may fail, hence the monad.-> type Tactic = Goal -> Context -> TTM Context--> -- | Initialise a context, with no data or definitions and an-> -- empty proof state.-> emptyContext :: Context-> emptyContext = Ctxt initstate--> class IsTerm a where-> -- | Typecheck a term-> check :: Context -> a -> TTM Term-> raw :: a -> TTM Raw--> class IsData a where-> -- Add a data type with case and elim rules an elimination rule-> addData :: Context -> a -> TTM Context-> addData ctxt x = addData' True ctxt x-> -- Add a data type without an elimination rule-> addDataNoElim :: Context -> a -> TTM Context-> addDataNoElim ctxt x = addData' False ctxt x-> addData' :: Bool -> Context -> a -> TTM Context- > instance IsTerm Term where > check _ tm = return tm > raw tm = return $ forget (view tm) > instance IsTerm ViewTerm where-> check ctxt tm = Ivor.TT.check ctxt (forget tm)+> check ctxt tm = Ivor.CtxtTT.check ctxt (forget tm) > raw tm = return $ forget tm > instance IsTerm String where > check ctxt str = case parseTermString str of-> (Success tm) -> Ivor.TT.check ctxt (forget tm)-> (Failure err) -> fail err+> (Success tm) -> Ivor.CtxtTT.check ctxt (forget tm)+> (Failure err) -> ttfail err > raw str = case parseTermString str of > (Success tm) -> return $ forget tm-> (Failure err) -> fail err+> (Failure err) -> ttfail err > instance IsTerm Raw where > check (Ctxt st) t = do@@ -182,55 +137,6 @@ > (Left err) -> tt $ ifail err > raw t = return t -> data TTError = CantUnify ViewTerm ViewTerm-> | NotConvertible ViewTerm ViewTerm-> | Message String-> | Unbound ViewTerm ViewTerm ViewTerm ViewTerm [Name]-> | NoSuchVar Name-> | CantInfer Name ViewTerm-> | ErrContext String TTError-> | AmbiguousName [Name]--> instance Show TTError where-> show (CantUnify t1 t2) = "Can't unify " ++ show t1 ++ " and " ++ show t2-> show (NotConvertible t1 t2) = show t1 ++ " and " ++ show t2 ++ " are not convertible"-> show (Message s) = s-> show (Unbound clause clty rhs rhsty ns) -> = show ns ++ " unbound in clause " ++ show clause ++ " : " ++ show clty ++ -> " = " ++ show rhs-> show (CantInfer n tm) = "Can't infer value for " ++ show n ++ " in " ++ show tm-> show (NoSuchVar n) = "No such name as " ++ show n-> show (AmbiguousName ns) = "Ambiguous name " ++ show ns-> show (ErrContext c err) = c ++ show err--> instance Error TTError where-> noMsg = Message "Ivor Error"-> strMsg s = Message s--> type TTM = Either TTError--> ttfail :: String -> TTM a-> ttfail s = Left (Message s)--> tt :: IvorM a -> TTM a-> tt (Left err) = Left (getError err)-> tt (Right v) = Right v--> getError :: IError -> TTError-> getError (ICantUnify l r) = CantUnify (view (Term (l, Ind TTCore.Star))) (view (Term (r, Ind TTCore.Star)))-> getError (INotConvertible l r) = NotConvertible (view (Term (l, Ind TTCore.Star))) (view (Term (r, Ind TTCore.Star)))-> getError (IMessage s) = Message s-> getError (IUnbound clause clty rhs rhsty names) -> = Unbound (view (Term (clause, Ind TTCore.Star)))-> (view (Term (clty, Ind TTCore.Star)))-> (view (Term (rhs, Ind TTCore.Star)))-> (view (Term (rhsty, Ind TTCore.Star)))-> names-> getError (ICantInfer nm tm) = CantInfer nm (view (Term (tm, Ind TTCore.Star)))-> getError (INoSuchVar n) = NoSuchVar n-> getError (IAmbiguousName ns) = AmbiguousName ns-> getError (IContext s e) = ErrContext s (getError e)- > -- | Quickly convert a 'ViewTerm' into a real 'Term'. > -- This is dangerous; you must know that typechecking will succeed, > -- and the resulting term won't have a valid type, but you will be@@ -247,7 +153,7 @@ > addData' elim (Ctxt st) str = do > case (parseDataString str) of > Success ind -> addData' elim (Ctxt st) ind-> Failure err -> fail err+> Failure err -> ttfail err > instance IsData Inductive where > addData' elim (Ctxt st) ind = do st' <- tt $ doMkData elim st (datadecl ind)@@ -263,7 +169,7 @@ > checkNotExists n gam = case lookupval n gam of > Just Undefined -> return () > Just (TCon _ NoConstructorsYet) -> return ()-> Just _ -> fail $ show n ++ " already defined"+> Just _ -> ttfail $ show n ++ " already defined" > Nothing -> return () > data PClause = PClause {@@ -303,15 +209,18 @@ > toPat gam _ = Placeholder > matchable gam n > = case lookupval n gam of-> Just (DCon _ _) -> True -- since it's a constructor+> Just (DCon _ _ _) -> True -- since it's a constructor > Nothing -> True -- since it' a variable > _ -> False > + patternDef gam n ty pmf t g = PatternDef pmf t g (pmcomp gam n ty pmf)+ > data PattOpt = Partial -- ^ No need to cover all cases > | GenRec -- ^ No termination checking > | Holey -- ^ Allow metavariables in the definition, which will become theorems which need to be proved. > | Specialise [(Name, Int)] -- ^ Specialise the right hand side+> | SpecStatic [(Name, ([Int], Int))] -- ^ Functions plus static arguments, plus arity, for use when specialising > deriving Eq > -- |Add a new definition to the global state.@@ -328,54 +237,77 @@ > checkNotExists n (defs st) > let ndefs = defs st > inty <- raw ty+> let unused = defplicit > let (Patterns clauses) = pats > (pmdefs, newnames, tot) > <- tt $ checkDef ndefs n inty (map mkRawClause clauses) > (not (elem Ivor.TT.Partial opts)) > (not (elem GenRec opts)) > (getSpec opts)+> (getSpecSt opts) > (ndefs',vnewnames) > <- if (null newnames) then return (ndefs, []) > else do when (not (Holey `elem` opts)) $ -> fail "No metavariables allowed"+> ttfail "No metavariables allowed" > let vnew = map (\ (n,t) -> > (n, view (Term (t,Ind TTCore.Star)))) newnames > let ngam = foldl (\g (n, t) ->-> extend g (n, G Unreducible t 0))+> extend g (n, G Unreducible t unused)) > ndefs newnames > return (ngam, vnew)-> newdefs <- insertAll pmdefs ndefs' tot+> newdefs <- insertAll pmdefs ndefs' tot unused > return (Ctxt st { defs = newdefs }, vnewnames)-> where insertAll [] gam tot = return gam-> insertAll ((nm, def, ty):xs) gam tot = -> do gam' <- gInsert nm (G (PatternDef def tot (gen nm)) ty defplicit) gam-> insertAll xs gam' tot+> where insertAll [] gam tot unused = return gam+> insertAll ((nm, def, ty):xs) gam tot unused = +> do gam' <- gInsert nm (G (patternDef gam nm ty def tot (gen nm)) ty unused) gam+> insertAll xs gam' tot unused > gen nm = nm /= n -- generated if it's not the provided name. > getSpec [] = Nothing > getSpec (Specialise fns:_) = Just fns > getSpec (_:xs) = getSpec xs +> getSpecSt [] = Nothing+> getSpecSt (SpecStatic fns:_) = Just fns+> getSpecSt (_:xs) = getSpecSt xs++> -- |Specialise an existing pattern matching definition+> spec :: Context -> Name+> -> [(Name, ([Int], Int))] -- ^ Functions and static arguments+> -> [Name] -- ^ Frozen names+> -> TTM Context+> spec ctxt@(Ctxt st) fn statics frozen = ++Look up the name, specialise it, then add the new pattern definition to the+context++> do (pats, tot, gen, ty, unused) <- getPatternDefCore ctxt fn+> let (ps', ctxt', names) = trace ("Specialising " ++ show (fn, pats)) $ specialise ctxt pats statics frozen+> let gam = defs st+> let gam' = remove fn gam+> gam' <- gInsert fn (G (patternDef gam' fn ty ps' tot gen) ty unused) gam'+> return $ Ctxt st { defs = gam' }+ > -- |Add a new definition, with its type to the global state. > -- These definitions can be recursive, so use with care. > addTypedDef :: (IsTerm term, IsTerm ty) => > Context -> Name -> term -> ty -> TTM Context > addTypedDef (Ctxt st) n tm ty = do > checkNotExists n (defs st)-> (Term (inty,_)) <- Ivor.TT.check (Ctxt st) ty+> (Term (inty,_)) <- Ivor.CtxtTT.check (Ctxt st) ty > (Ctxt tmpctxt) <- declare (Ctxt st) n ty > let tmp = defs tmpctxt > let ctxt = defs st > term <- raw tm > case (checkAndBind tmp [] term (Just inty)) of-> (Right (v,t@(Ind sc),_)) -> do+> (Right (Ind v,t@(Ind sc),_)) -> do > if (convert (defs st) inty t) > then (do > checkBound (getNames (Sc sc)) t-> newdefs <- gInsert n (G (Fun [Recursive] v) t defplicit) ctxt+> newdefs <- gInsert n (G (Fun [Recursive] (Ind (forced ctxt v))) t defplicit) ctxt > -- = Gam ((n,G (Fun [] v) t):ctxt) > return $ Ctxt st { defs = newdefs })-> else (fail $ "The given type and inferred type do not match, inferred " ++ show t)+> else (ttfail $ "The given type and inferred type do not match, inferred " ++ show t) > (Left err) -> tt $ ifail err @@ -386,9 +318,9 @@ > v <- raw tm > let ctxt = defs st > case (typecheck ctxt v) of-> (Right (v,t@(Ind sc))) -> do+> (Right (Ind v',t@(Ind sc))) -> do > checkBound (getNames (Sc sc)) t-> newdefs <- gInsert n (G (Fun [] v) t defplicit) ctxt+> newdefs <- gInsert n (G (Fun [] (Ind (forced ctxt v'))) t defplicit) ctxt > -- let newdefs = Gam ((n,G (Fun [] v) t):ctxt) > return $ Ctxt st { defs = newdefs } > (Left err) -> tt $ ifail err@@ -396,12 +328,12 @@ > checkBound :: [Name] -> (Indexed Name) -> TTM () > checkBound [] t = return () > checkBound (nm@(MN ("INFER",_)):ns) t-> = fail $ "Can't infer value for " ++ show nm ++ " in " ++ show t+> = ttfail $ "Can't infer value for " ++ show nm ++ " in " ++ show t > checkBound (_:ns) t = checkBound ns t > -- |Forget a definition and all following definitions. > forgetDef :: Context -> Name -> TTM Context-> forgetDef (Ctxt st) n = fail "Not any more..."+> forgetDef (Ctxt st) n = ttfail "Not any more..." do let olddefs = defs st newdefs <- f olddefs n@@ -426,7 +358,6 @@ > (Right (v,t)) -> do > -- let newdefs = Gam ((n,G (Fun [] v) t):ctxt) > newdefs <- gInsert n (G (Fun [] v) t defplicit) ctxt-> let scs = lift n (levelise (normalise (emptyGam) v)) > return $ Ctxt st { defs = newdefs } > (Left err) -> ttfail $ "Can't happen (general): "++ show err @@ -482,7 +413,7 @@ > declareData :: (IsTerm a) => Context -> Name -> a -> TTM Context > declareData ctxt@(Ctxt st) n tm = do > let gamma = defs st-> Term (ty, _) <- Ivor.TT.check ctxt tm+> Term (ty, _) <- Ivor.CtxtTT.check ctxt tm > addUn (TCon (arity gamma ty) NoConstructorsYet) ctxt n tm > -- | Add a new axiom to the global state.@@ -521,7 +452,7 @@ > Context -> Name -> (a->b->c) -> ty -> TTM Context > addBinOp (Ctxt st) n f tyin = do > checkNotExists n (defs st)-> Term (ty, _) <- Ivor.TT.check (Ctxt st) tyin+> Term (ty, _) <- Ivor.CtxtTT.check (Ctxt st) tyin > let fndef = PrimOp mkfun mktt > let Gam ctxt = defs st > -- let newdefs = Gam ((n,(G fndef ty)):ctxt)@@ -541,6 +472,7 @@ > Just x' -> case cast y of > Just y' -> Just $ Const (f x' y') > Nothing -> Nothing+> Nothing -> Nothing > mktt _ = Nothing > -- | Add a new binary function on constants. Warning: The type you give@@ -549,7 +481,7 @@ > Context -> Name -> (a->b->ViewTerm) -> ty -> TTM Context > addBinFn (Ctxt st) n f tyin = do > checkNotExists n (defs st)-> Term (ty, _) <- Ivor.TT.check (Ctxt st) tyin+> Term (ty, _) <- Ivor.CtxtTT.check (Ctxt st) tyin > let fndef = PrimOp mkfun mktt > let Gam ctxt = defs st > -- let newdefs = Gam ((n,(G fndef ty)):ctxt)@@ -559,7 +491,7 @@ > mkfun (Snoc (Snoc Empty (MR (RdConst x))) (MR (RdConst y))) > = case cast x of > Just x' -> case cast y of-> Just y' -> case Ivor.TT.check (Ctxt st) $ f x' y' of+> Just y' -> case Ivor.CtxtTT.check (Ctxt st) $ f x' y' of > Right (Term (Ind v,_)) -> > Just $ nf (emptyGam) (VG []) [] False v > Nothing -> Nothing@@ -569,7 +501,7 @@ > mktt [Const x, Const y] > = case cast x of > Just x' -> case cast y of-> Just y' -> case Ivor.TT.check (Ctxt st) $ f x' y' of+> Just y' -> case Ivor.CtxtTT.check (Ctxt st) $ f x' y' of > Right (Term (Ind v,_)) -> > Just v > Nothing -> Nothing@@ -584,7 +516,7 @@ > Context -> Name -> (a->ViewTerm) -> ty -> TTM Context > addPrimFn (Ctxt st) n f tyin = do > checkNotExists n (defs st)-> Term (ty, _) <- Ivor.TT.check (Ctxt st) tyin+> Term (ty, _) <- Ivor.CtxtTT.check (Ctxt st) tyin > let fndef = PrimOp mkfun mktt > let ctxt = defs st > -- let newdefs = Gam ((n,(G fndef ty)):ctxt)@@ -593,7 +525,7 @@ > where mkfun :: Spine Value -> Maybe Value > mkfun (Snoc Empty (MR (RdConst x))) > = case cast x of-> Just x' -> case Ivor.TT.check (Ctxt st) $ f x' of+> Just x' -> case Ivor.CtxtTT.check (Ctxt st) $ f x' of > Right (Term (Ind v,_)) -> > Just $ nf (emptyGam) (VG []) [] False v > _ -> Nothing@@ -602,7 +534,7 @@ > mktt :: [TT Name] -> Maybe (TT Name) > mktt [Const x] > = case cast x of-> Just x' -> case Ivor.TT.check (Ctxt st) $ f x' of+> Just x' -> case Ivor.CtxtTT.check (Ctxt st) $ f x' of > Right (Term (Ind v,_)) -> > Just v > _ -> Nothing@@ -618,7 +550,7 @@ > -> ty -> TTM Context > addExternalFn (Ctxt st) n arity f tyin = do > checkNotExists n (defs st)-> Term (ty, _) <- Ivor.TT.check (Ctxt st) tyin+> Term (ty, _) <- Ivor.CtxtTT.check (Ctxt st) tyin > let fndef = PrimOp mkfun mktt > let ctxt = defs st > -- let newdefs = Gam ((n,(G fndef ty)):ctxt)@@ -629,7 +561,7 @@ > = if (length xs) /= arity then Nothing > else case runf xs of > Just res ->-> case (Ivor.TT.check (Ctxt st) res) of+> case (Ivor.CtxtTT.check (Ctxt st) res) of > Right (Term (Ind tm, _)) -> > Just $ nf (emptyGam) (VG []) [] False tm > _ -> Nothing@@ -639,7 +571,7 @@ > = if (length xs) /= arity then Nothing > else case f (map viewtt xs) of > Just res ->-> case (Ivor.TT.check (Ctxt st) res) of+> case (Ivor.CtxtTT.check (Ctxt st) res) of > Right (Term (Ind tm, _)) -> > Just tm > _ -> Nothing@@ -683,7 +615,7 @@ > holequeue = [n], > hidden = [] > }-> (Just t) -> fail "Already a proof in progress"+> (Just t) -> ttfail "Already a proof in progress" > -- |Begin a new interactive definition. > -- Actually, just the same as 'theorem' but this version allows you to@@ -702,7 +634,7 @@ > holequeue = [n], > hidden = [] > }-> (Just t) -> fail "Already a proof in progress"+> (Just t) -> ttfail "Already a proof in progress" > -- |Suspend the current proof. Clears the current proof state; use 'resume' > -- to continue the proof.@@ -728,14 +660,14 @@ > Just (Undefined,ty) -> > do let st' = st { defs = remove n (defs st) } > theorem (Ctxt st') n (Term (ty, Ind TTCore.Star))-> _ -> fail "No such suspended proof"+> _ -> ttfail "No such suspended proof" > -- | Freeze a name (i.e., set it so that it does not reduce) > -- Fails if the name does not exist. > freeze :: Context -> Name -> TTM Context > freeze (Ctxt st) n > = case glookup n (defs st) of-> Nothing -> fail $ show n ++ " is not defined"+> Nothing -> ttfail $ show n ++ " is not defined" > _ -> return $ Ctxt st { defs = Ivor.Values.freeze n (defs st) } > -- | Unfreeze a name (i.e., allow it to reduce).@@ -743,7 +675,7 @@ > thaw :: Context -> Name -> TTM Context > thaw (Ctxt st) n > = case glookup n (defs st) of-> Nothing -> fail $ show n ++ " is not defined"+> Nothing -> ttfail $ show n ++ " is not defined" > _ -> return $ Ctxt st { defs = Ivor.Values.thaw n (defs st) } @@ -759,7 +691,7 @@ > -- | Restore a saved state; fails if none have been saved. > restore :: Context -> TTM Context > restore (Ctxt st) = case undoState st of-> Nothing -> fail "No saved state"+> Nothing -> ttfail "No saved state" > (Just st') -> return $ Ctxt st' @@ -776,39 +708,13 @@ return $ Term (tm, ty) Failure err -> fail err -> -- |Normalise a term and its type (using old evaluator_-> eval :: Context -> Term -> Term-> eval (Ctxt st) (Term (tm,ty)) = Term (normalise (defs st) tm,-> normalise (defs st) ty) -> -- |Reduce a term and its type to Weak Head Normal Form-> whnf :: Context -> Term -> Term-> whnf (Ctxt st) (Term (tm,ty)) = Term (eval_whnf (defs st) tm,-> eval_whnf (defs st) ty)--> -- |Reduce a term and its type to Normal Form (using new evaluator)-> evalnew :: Context -> Term -> Term-> evalnew (Ctxt st) (Term (tm,ty)) = Term (tidyNames (eval_nf (defs st) tm),-> tidyNames (eval_nf (defs st) ty))--> -- |Reduce a term and its type to Normal Form (using new evaluator, not-> -- reducing given names)-> evalnewWithout :: Context -> Term -> [Name] -> Term-> evalnewWithout (Ctxt st) (Term (tm,ty)) ns = Term (tidyNames (eval_nf_without (defs st) tm ns),-> tidyNames (eval_nf_without (defs st) ty ns))--> -- |Reduce a term and its type to Normal Form (using new evaluator, reducing-> -- given names a maximum number of times)-> evalnewLimit :: Context -> Term -> [(Name, Int)] -> Term-> evalnewLimit (Ctxt st) (Term (tm,ty)) ns = Term (eval_nf_limit (defs st) tm ns,-> eval_nf_limit (defs st) ty ns)- > -- |Check a term in the context of the given goal > checkCtxt :: (IsTerm a) => Context -> Goal -> a -> TTM Term > checkCtxt (Ctxt st) goal tm = > do rawtm <- raw tm > prf <- case proofstate st of-> Nothing -> fail "No proof in progress"+> Nothing -> ttfail "No proof in progress" > Just x -> return x > let h = case goal of > (Goal x) -> x@@ -816,29 +722,10 @@ > case (Tactics.findhole (defs st) (Just h) prf holeenv) of > (Just env) -> do t <- tt $ Ivor.Typecheck.check (defs st) env rawtm Nothing > return $ Term t-> Nothing -> fail "No such goal"-> where holeenv :: Gamma Name -> Env Name -> Indexed Name -> Env Name-> holeenv gam hs _ = Tactics.ptovenv hs--> -- |Evaluate a term in the context of the given goal-> evalCtxt :: (IsTerm a) => Context -> Goal -> a -> TTM Term-> evalCtxt (Ctxt st) goal tm =-> do rawtm <- raw tm-> prf <- case proofstate st of-> Nothing -> fail "No proof in progress"-> Just x -> return x-> let h = case goal of-> (Goal x) -> x-> DefaultGoal -> head (holequeue st)-> case (Tactics.findhole (defs st) (Just h) prf holeenv) of-> (Just env) -> do (tm, ty) <- tt $ Ivor.Typecheck.check (defs st) env rawtm Nothing-> let tnorm = normaliseEnv env (defs st) tm-> return $ Term (tnorm, ty)-> Nothing -> fail "No such goal"+> Nothing -> ttfail "No such goal" > where holeenv :: Gamma Name -> Env Name -> Indexed Name -> Env Name > holeenv gam hs _ = Tactics.ptovenv hs - > -- |Check whether the conversion relation holds between two terms, in the > -- context of the given goal @@ -848,7 +735,7 @@ > = do atm <- checkCtxt ctxt goal a > btm <- checkCtxt ctxt goal b > prf <- case proofstate st of-> Nothing -> fail "No proof in progress"+> Nothing -> ttfail "No proof in progress" > Just x -> return x > let (Term (av,_)) = atm > let (Term (bv,_)) = btm@@ -859,21 +746,39 @@ > (Just env) -> case checkConvEnv env (defs st) av bv (IMessage "") of > Right _ -> return True > _ -> return False-> Nothing -> fail "No such goal"+> Nothing -> ttfail "No such goal" > where holeenv :: Gamma Name -> Env Name -> Indexed Name -> Env Name > holeenv gam hs _ = Tactics.ptovenv hs +> -- |Evaluate a term in the context of the given goal+> evalCtxt :: (IsTerm a) => Context -> Goal -> a -> TTM Term+> evalCtxt (Ctxt st) goal tm =+> do rawtm <- raw tm+> prf <- case proofstate st of+> Nothing -> ttfail "No proof in progress"+> Just x -> return x+> let h = case goal of+> (Goal x) -> x+> DefaultGoal -> head (holequeue st)+> case (Tactics.findhole (defs st) (Just h) prf holeenv) of+> (Just env) -> do (tm, ty) <- tt $ Ivor.Typecheck.check (defs st) env rawtm Nothing+> let tnorm = eval_nf_env env (defs st) tm+> return $ Term (tnorm, ty)+> Nothing -> ttfail "No such goal"+> where holeenv :: Gamma Name -> Env Name -> Indexed Name -> Env Name+> holeenv gam hs _ = Tactics.ptovenv hs+ > -- |Lookup a definition in the context. > getDef :: Context -> Name -> TTM Term > getDef (Ctxt st) n = case glookup n (defs st) of > Just ((Fun _ tm),ty) -> return $ Term (tm,ty)-> _ -> fail "Not a function name"+> _ -> ttfail "Not a function name" > -- |Get the type of a definition in the context. > getType :: Context -> Name -> TTM Term > getType (Ctxt st) n = case glookup n (defs st) of > Just (_,ty) -> return $ Term (ty,Ind TTCore.Star)-> _ -> fail "Not a defined name"+> _ -> ttfail "Not a defined name" > -- |Check whether a name is defined > defined :: Context -> Name -> Bool@@ -892,7 +797,7 @@ > return (Inductive n [] (getIndices (view (Term (ty, Ind TTCore.Star)))) > (getTyType (view (Term (ty, Ind TTCore.Star)))) > (getConTypes cons))-> _ -> fail "Not an inductive family"+> _ -> ttfail "Not an inductive family" > where getIndices v = getArgTypes v > getTyType v = VTerm.getReturnType v > getConTypes [] = []@@ -904,13 +809,13 @@ > getPatternDef :: Context -> Name -> TTM (ViewTerm, Patterns) > getPatternDef (Ctxt st) n > = case glookup n (defs st) of-> Just ((PatternDef pmf _ _),ty) ->+> Just ((PatternDef pmf _ _ _),ty) -> > return $ (view (Term (ty, Ind TTCore.Star)), > Patterns (map mkPat (getPats pmf))) > Just ((Fun _ ind), ty) -> > return $ (view (Term (ty, Ind TTCore.Star)), > Patterns [mkCAFpat ind])-> _ -> fail "Not a pattern matching definition"+> _ -> ttfail "Not a pattern matching definition" > where getPats (PMFun _ ps) = ps > mkPat (Sch ps bs ret) > = PClause (map viewPat ps) @@ -919,10 +824,42 @@ > (view (Term (ret, (Ind TTCore.Star)))) > mkCAFpat tm = PClause [] [] (view (Term (tm, (Ind TTCore.Star)))) > viewPat (PVar n) = Name Bound n --(name (show n))-> viewPat (PCon t n ty ts) = VTerm.apply (Name Bound (name (show n))) (map viewPat ts)+> viewPat (PCon t n ty ts) = VTerm.apply (Name DataCon (name (show n))) (map viewPat ts) > viewPat (PConst c) = Constant c > viewPat _ = Placeholder +> getPatternDefCore :: Context -> Name -> +> TTM (PMFun Name, Bool, Bool, Indexed Name, Plicity)+> getPatternDefCore (Ctxt st) n+> = case glookupall n (defs st) of+> Just ((PatternDef pmf t g _),ty,plicit) -> +> return (pmf, t, g, ty, plicit)+> Just ((Fun _ ind), ty, plicit) -> +> return (PMFun 0 [Sch [] [] ind], True, False, ty, plicit)+> _ -> ttfail "Not a pattern matching definition"++> -- |Lookup a pattern matching definition in the context. Return the+> -- argument names and compiled simple case tree.+> getCompiledPatternDef :: Context -> Name -> TTM ([Name], SimpleCase)+> getCompiledPatternDef (Ctxt st) n+> = case glookup n (defs st) of+> Just ((PatternDef pmf _ _ (ns, sc)),ty) ->+> Right (ns, mkSC sc)+> Just ((Fun _ (Ind ind)), ty) ->+> return ([], mkSC (TTm ind))+> _ -> ttfail "Not a pattern matching definition"+> where mkSC :: TSimpleCase Name -> SimpleCase+> mkSC (TTm t) = Tm (mkSCtm t)+> mkSC TErrorCase = ErrorCase+> mkSC TImpossible = Impossible+> mkSC (TSCase tm alts) = SCase (mkSCtm tm) (map mkAlt alts)+> mkAlt (TAlt n t args sc) = Alt n t args (mkSC sc)+> mkAlt (TConstAlt c sc) = ConstAlt c (mkSC sc)+> mkAlt (TDefault sc) = Default (mkSC sc)++> mkSCtm t = view (Term (Ind t, dontcare))+> dontcare = Ind (TTCore.Star)+ > -- |Get all the names and types in the context > getAllTypes :: Context -> [(Name,Term)] > getAllTypes (Ctxt st) = let ds = getAList (defs st) in@@ -943,7 +880,7 @@ > -- clause? > isAuxPattern :: Context -> Name -> Bool > isAuxPattern (Ctxt st) n = case glookup n (defs st) of-> Just ((PatternDef pmf _ gen),ty) -> gen+> Just ((PatternDef pmf _ gen _),ty) -> gen > _ -> False @@ -966,31 +903,31 @@ > getConstructors (Ctxt st) n > = case glookup n (defs st) of > Just ((TCon _ (Elims _ _ cs)),ty) -> return cs-> _ -> fail "Not a type constructor"+> _ -> ttfail "Not a type constructor" > -- |Find out what type of variable the given name is > nameType :: Context -> Name -> TTM NameType > nameType (Ctxt st) n > = case glookup n (defs st) of-> Just ((DCon _ _), _) -> return DataCon+> Just ((DCon _ _ _), _) -> return DataCon > Just ((TCon _ _), _) -> return TypeCon > Just _ -> return Bound -- any function-> Nothing -> fail "No such name"+> Nothing -> ttfail "No such name" > -- | Get an integer tag for a constructor. Each constructor has a tag > -- unique within the data type, which could be used by a compiler. > getConstructorTag :: Context -> Name -> TTM Int > getConstructorTag (Ctxt st) n > = case glookup n (defs st) of-> Just ((DCon tag _), _) -> return tag-> _ -> fail "Not a constructor"+> Just ((DCon tag _ _), _) -> return tag+> _ -> ttfail "Not a constructor" > -- | Get the arity of the given constructor. > getConstructorArity :: Context -> Name -> TTM Int > getConstructorArity (Ctxt st) n > = case glookup n (defs st) of-> Just ((DCon _ _), Ind ty) -> return (length (getExpected ty))-> _ -> fail "Not a constructor"+> Just ((DCon _ _ _), Ind ty) -> return (length (getExpected ty))+> _ -> ttfail "Not a constructor" Examine pattern matching elimination rules @@ -1009,7 +946,7 @@ > Ivor.TT.Elim -> erule > elim <- lookupM rule (eliminators st) > return $ Patterns $ map mkRed (fst $ snd elim)-> Nothing -> fail $ (show nm) ++ " is not a type constructor"+> Nothing -> ttfail $ (show nm) ++ " is not a type constructor" > where mkRed (RSch pats (RWRet ret)) = PClause (map viewRaw pats) [] (viewRaw ret) > -- a reduction will only have variables and applications > viewRaw (Var n) = Name Free n@@ -1048,10 +985,10 @@ > -- |Get the current proof term, if we are in the middle of a proof. > proofterm :: Context -> TTM Term > proofterm (Ctxt st) = case proofstate st of-> Nothing -> fail "No proof in progress"+> Nothing -> ttfail "No proof in progress" > Just (Ind (Bind _ (B (Guess v) t) _)) -> > return $ Term (Ind v,Ind t)-> Just t -> fail $ "Proof finished; " ++ show t+> Just t -> ttfail $ "Proof finished; " ++ show t > -- |Get the type and context of the given goal, if it exists > getGoal :: Context -> Goal -> TTM ([(Name,Term)], Term)@@ -1060,11 +997,11 @@ > (Goal x) -> x > DefaultGoal -> head (holequeue st) in > case (proofstate st) of-> Nothing -> fail "No proof in progress"+> Nothing -> ttfail "No proof in progress" > (Just tm) -> > case (Tactics.findhole (defs st) (Just h) tm getHoleTerm) of > Just x -> return x-> Nothing -> fail "No such goal"+> Nothing -> ttfail "No such goal" > getHoleTerm gam hs tm = (getctxt hs, > Term (normaliseEnv hs (emptyGam) (binderType tm), @@ -1091,14 +1028,14 @@ > -- just lambda bindings (False) > -> Goal -> TTM GoalData > goalData (Ctxt st) all goal = case proofstate st of-> Nothing -> fail "No proof in progress"+> Nothing -> ttfail "No proof in progress" > (Just prf) -> > let h = case goal of > (Goal x) -> x > DefaultGoal -> head (holequeue st) in > case (Tactics.findhole (defs st) (Just h) prf holedata) of > (Just x) -> return x-> Nothing -> fail "No such goal"+> Nothing -> ttfail "No such goal" > where holedata :: Gamma Name -> Env Name -> Indexed Name -> GoalData > holedata gam hs tm = hd' (Tactics.ptovenv hs) (finalise tm) -- (normaliseEnv hs (Gam []) (finalise tm)) > hd' hs (Ind (Bind n (B _ tm) _))@@ -1115,7 +1052,7 @@ > -- | Get the names and types of all goals > subGoals :: Context -> TTM [(Name,Term)] > subGoals (Ctxt st) = case proofstate st of-> Nothing -> fail "No proof in progress"+> Nothing -> ttfail "No proof in progress" > (Just prf) -> return $ > map (\ (x,ty) -> (x,Term (ty,Ind TTCore.Star))) > $ Tactics.allholes (defs st) True prf@@ -1124,7 +1061,7 @@ > uniqueName :: Context -> Name -- ^ Suggested name > -> TTM Name -- ^ Unique name based on suggested name > uniqueName (Ctxt st) n = case proofstate st of-> Nothing -> fail "No proof in progress"+> Nothing -> ttfail "No proof in progress" > (Just (Ind prf)) -> return $ uniqify n $ getBoundNames (Sc prf) Tactics@@ -1159,7 +1096,7 @@ > let newdefs = setRec name isrec defs' > return $ Ctxt st { proofstate = Nothing, > defs = newdefs } -- Gam (newdef:olddefs) }-> Nothing -> fail "No proof in progress"+> Nothing -> ttfail "No proof in progress" > where rec nm = case lookupval nm (defs st) of > Nothing -> False > _ -> True@@ -1170,16 +1107,16 @@ > (Ind (Bind x (B (TTCore.Let v) ty) (Sc (P n)))) | n == x = > do let (Ind vnorm) = convNormalise (emptyGam) (finalise (Ind v)) > tt $ verify gam (Ind v)-> return $ (x, G (Fun opts (Ind vnorm)) (finalise (Ind ty)) defplicit)+> return $ (x, G (Fun opts (Ind (forced gam vnorm))) (finalise (Ind ty)) defplicit) > where opts = if freeze then [Frozen] else []-> qedLift _ _ tm = fail $ "Not a complete proof " ++ show tm+> qedLift _ _ tm = ttfail $ "Not a complete proof " ++ show tm > -- | Focus on a different hole, i.e. set the default goal. > focus :: Tactic > focus (Goal n) (Ctxt st) > | n `elem` holequeue st > = attack (Goal n) $ Ctxt st { holequeue = jumpqueue n (holequeue st) }-> | otherwise = fail "No such goal"+> | otherwise = ttfail "No such goal" > focus _ x = return x -- Default goal already first > -- | Hide a premise@@ -1266,7 +1203,7 @@ Convert an internal tactic into a publicly available tactic. > runTac :: Tactics.Tactic -> Tactic-> runTac tac goal (Ctxt st) | null (holequeue st) = fail "No more goals"+> runTac tac goal (Ctxt st) | null (holequeue st) = ttfail "No more goals" > runTac tac goal (Ctxt st) = do > let hole = case goal of > (Goal x) -> x@@ -1306,7 +1243,7 @@ > attack goal (Ctxt st) = do n <- getName > attackWith n goal (Ctxt st) > where getName = do allnames <- case (proofstate st) of-> Nothing -> fail "No proof in progress"+> Nothing -> ttfail "No proof in progress" > Just (Ind tm) -> > return $ binderMap (\n _ _ -> n) tm > return $ uniqify (name "H") ((holequeue st)++allnames)@@ -1531,7 +1468,7 @@ > ctxt <- claim name rtype g ctxt > fill (VTerm.Return (Name Bound name)) g ctxt > where getRType (VTerm.Label _ _ ty) = return ty-> getRType _ = fail "Not a labelled type"+> getRType _ = ttfail "Not a labelled type" > -- | Prepare to return a quoted value > quoteVal :: Tactic@@ -1568,7 +1505,7 @@ > = do gd <- goalData ctxt False g > let ps = bindings gd > tryall ps g ctxt-> where tryall [] g ctxt = fail "No trivial solution found"+> where tryall [] g ctxt = ttfail "No trivial solution found" > tryall ((x,ty):xs) g ctxt > = do ctxt' <- ((refine (Name Free x)) >|> (fill (Name Free x)) > >|> idTac) g ctxt@@ -1614,7 +1551,7 @@ > fill rec g ctxt > where > findRec :: [RecAllowed] -> Raw -> TTM ViewTerm-> findRec [] tm = fail "This recursive call not allowed"+> findRec [] tm = ttfail "This recursive call not allowed" > findRec ((Rec fs nm args hyp):rs) tm = > case mkRec fs nm args hyp tm of > Right x -> return x@@ -1626,7 +1563,7 @@ > if (nm==tmf) then do > ihargs <- getIH fs args vtmas > return $ VTerm.Call nm vtmas (VTerm.apply hyp ihargs)-> else fail "Not this one"+> else ttfail "Not this one" > getfa (RApp f a) args = getfa f (a:args) > getfa (Var x) args = (x,args) > getIH fs [] [] = return []@@ -1638,7 +1575,7 @@ > getIH fs (x:xs) (y:ys) > | tryvareq x y > = getIH fs xs ys -- x not pi bound, but names okay.-> getIH _ _ _ = fail "Not this one" -- Something doesn't match up.+> getIH _ _ _ = ttfail "Not this one" -- Something doesn't match up. > tryvar (Name _ x) = Just x > tryvar _ = Nothing
Ivor/TTCore.lhs view
@@ -46,6 +46,7 @@ > data TT n > = P n > | V Int+> | L Int -- pattern variable > | Con Int n Int -- Tag, name and arity > | TyCon n Int -- Name and arity > | Meta n (TT n) -- Metavariable and its type@@ -59,6 +60,7 @@ > | forall c. Constant c => Const !c > | Star > | Stage (Stage n)+> | Erased -- Forced, so deleted > data Computation n = Comp n [TT n] @@ -104,7 +106,7 @@ > data Pattern n = > PVar n -- Variable-> | PCon Int n n [Pattern n] -- Constructor, with tag and type+> | PCon Int n n [Pattern n] -- Constructor, with tag, name and type > | forall c.(Constant c) => PConst !c > | PMarkCon n [Pattern n] -- Detagged constructor > | PTerm -- Presupposed term (don't care what it is)@@ -138,12 +140,53 @@ > compare (PCon x _ _ _) (PCon y _ _ _) = compare x y > compare _ _ = EQ -- Don't care! +Simple case statements are either a case analysis, just a term. ErrorCase +and Impossible are distinct in that 'Impossible' should be the default +fallthrough when a function is known to be total, and ErrorCase otherwise.++> data TSimpleCase n = TSCase (TT n) [TCaseAlt n]+> | TTm (TT n)+> | TErrorCase+> | TImpossible+> deriving (Show, Eq)++> data TCaseAlt n = TAlt n Int [n] (TSimpleCase n)+> | forall c. Constant c => TConstAlt c (TSimpleCase n)+> | TDefault (TSimpleCase n)++Only the kind of pattern it is matters. Just as well since constants are+a pain...++> instance Ord (TCaseAlt n) where+> compare (TAlt _ t _ _) (TAlt _ u _ _) = compare t u+> compare (TConstAlt c _) (TConstAlt d _) = EQ+> compare (TDefault _) (TDefault _) = EQ+> compare (TAlt _ _ _ _) _ = LT+> compare (TConstAlt _ _) (TAlt _ _ _ _) = GT+> compare (TConstAlt _ _) (TDefault _) = LT+> compare (TDefault _) _ = GT++> instance Eq (TCaseAlt n) where+> (==) (TAlt _ t _ _) (TAlt _ u _ _) = t == u+> (==) (TConstAlt c _) (TConstAlt d _) = True+> (==) (TDefault _) (TDefault _) = True+> (==) (TAlt _ _ _ _) _ = False+> (==) (TConstAlt _ _) (TAlt _ _ _ _) = False+> (==) (TConstAlt _ _) (TDefault _) = False+> (==) (TDefault _) _ = False++> instance Show n => Show (TCaseAlt n) where+> show (TAlt c t ns sc) = "Case " ++ show c ++ " " ++ show ns ++ " " ++ show sc+> show (TConstAlt c sc) = "Constant " ++ show sc+> show (TDefault sc) = "Default " ++ show sc+ UN covers names defined by users, MN covers names invented by the system. This keeps both namespaces separate. > data Name > = UN String > | MN (String,Int)+> | PN Name -- original name, pattern index > deriving (Ord, Eq) > instance Typeable Name where@@ -464,14 +507,14 @@ names and return all the new names we need to define for it to be a complete definition. -> updateMetas :: TT n -> (TT n, [(n, TT n)])+> updateMetas :: Eq n => TT n -> (TT n, [(n, TT n)]) > updateMetas tm = runState (ums tm) [] > where ums (App f a) = do f' <- ums f > a' <- ums a > return (App f' a') > ums (Meta n ty) = do ty' <- ums ty > mvs <- get-> put ((n,ty'):mvs)+> put $ nub ((n,ty'):mvs) > return (P n) > ums (Bind n (B b ty) (Sc sc)) > = do b' <- umsB b@@ -541,6 +584,20 @@ > p' (Stage t) = Stage (sLift p' t) > p' x = x +> substNames :: (Show n, Eq n) => [(n, TT n)] -> TT n -> TT n+> substNames ptms x = p' x where+> p' (P x) | Just tm <- lookup x ptms = tm+> p' (App f' a) = (App (p' f') (p' a))+> p' (Bind n b (Sc sc)) = (Bind n (fmap p' b) (Sc (p' sc)))+> -- | n == p = (Bind n (fmap p' b) (Sc sc))+> -- | otherwise+> p' (Proj n i x) = Proj n i (p' x)+> p' (Label t (Comp n cs)) = Label (p' t) (Comp n (map p' cs))+> p' (Call (Comp n cs) t) = Call (Comp n (map p' cs)) (p' t)+> p' (Return t) = Return (p' t)+> p' (Stage t) = Stage (sLift p' t)+> p' x = x+ Look for a specific term and replace it. Probably hopelessly inefficient. @@ -677,6 +734,8 @@ > (==) (Elim x) (Elim y) = x==y > (==) (App f a) (App f' a') = f==f' && a==a' > (==) (Bind _ b sc) (Bind _ b' sc') = b==b' && sc==sc'+> (==) Erased _ = True+> (==) _ Erased = True Eta equality: @@ -710,6 +769,7 @@ > forget (MN ("INFER",i)) = "y"++show i > forget (MN ("T",i)) = "z"++show i > forget (MN (x,i)) = x ++ "[" ++ show i ++ "]"+> forget (PN x) = forget x > instance Forget Raw String where > forget x = fPrec 10 x where@@ -749,7 +809,7 @@ > fPrec _ (RConst x) = show x > fPrec _ (RStar) = "*" > fPrec _ (RInfer) = "_"-> fPrec _ (RMeta n) = "?"++forget n+> fPrec _ (RMeta n) = "[?"++forget n++"]" > fPrec p (RFileLoc f l t) = fPrec p t > fPrec p (RAnnot s) = "[" ++ s ++ "]" > bracket outer inner str | inner>outer = "("++str++")"@@ -813,6 +873,7 @@ > forgetTT (Stage t) = RStage (forget t) > forgetTT (Const x) = RConst x > forgetTT Star = RStar+> forgetTT Erased = RInfer > instance (Show n) => Forget (TT n) Raw where > forget t = forgetTT (vapp showV t)@@ -854,6 +915,7 @@ > forgetTT (Stage t) = RStage (forget t) > forgetTT (Const x) = RConst x > forgetTT Star = RStar+> forgetTT Erased = RInfer > instance Show n => Forget (Stage n) RStage where > forget (Code x) = RCode (forget x)@@ -915,7 +977,7 @@ > showV (ctx,i) | i < length ctx = P (UN ("{v}"++show i)) > | otherwise = V i > forgetTT (P x) = Var $ UN (show x)-> forgetTT (V i) = RAnnot $ "v" ++ (show i)+> forgetTT (V i) = RAnnot $ "vFail{" ++ (show i) ++ "}" > forgetTT (Con t x i) = Var $ UN (show x) > forgetTT (TyCon x i) = Var $ UN (show x) > forgetTT (Meta x i) = RMeta (UN (show x))@@ -949,7 +1011,8 @@ > forgetTT (Stage (Eval t _)) = RStage (REval (forgetTT t)) > forgetTT (Stage (Escape t _)) = RStage (REscape (forgetTT t)) > forgetTT (Const x) = RConst x-> forgetTT Star = RStar+> forgetTT Erased = RInfer+> forgetTT x = RInfer > pToV :: Eq n => n -> (TT n) -> (Scope (TT n)) > pToV = pToV2 0@@ -979,3 +1042,4 @@ > pToV2 v p (Stage t) = Sc $ Stage (sLift (getSc.(pToV2 v p)) t) > pToV2 v p (Const x) = Sc (Const x) > pToV2 v p Star = Sc Star+> pToV2 v p Erased = Sc Erased
Ivor/Tactics.lhs view
@@ -93,7 +93,7 @@ > holecheck :: Name -> Gamma Name -> Indexed Name -> > Raw -> IvorM (Indexed Name, Indexed Name) > holecheck n gam state raw = case (findhole gam (Just n) state docheck) of-> Nothing -> fail "No such hole binder"+> Nothing -> tacfail "No such hole binder" > (Just x) -> x > where docheck gam env _ = check gam env raw Nothing @@ -126,7 +126,7 @@ > | x == n = do (Ind b',u) <- tactic gam env (Ind b) > return (b',u) - | otherwise = return (b, []) -- fail "No such hole"+ | otherwise = return (b, []) -- tacfail "No such hole" > rt env b@(Bind x (B Lambda ty) _) > | x == n = do (Ind b',u) <- tactic gam env (Ind b)@@ -219,7 +219,7 @@ > = tacret $ Ind (Bind x (B (Guess newtm) ty) sc) > where newtm = Bind h0 (B Hole ty) (Sc (P h0)) > h0 = uniqify h (x:(map fst env))-> attack _ _ _ t = fail $ "Internal error; not an attackable hole: " ++ show t+> attack _ _ _ t = tacfail $ "Internal error; not an attackable hole: " ++ show t Try filling the current goal with a term @@ -253,7 +253,7 @@ > nodups [] = [] > nodups ((x,y):xs) | x `elem` (map fst xs) = nodups xs > | otherwise = (x,y):(nodups xs)-> fill _ _ _ _ = fail "Can't try to fill something which isn't a hole"+> fill _ _ _ _ = tacfail "Can't try to fill something which isn't a hole" Use defaults to fill in arguments which don't appear in the goal (hence aren't solvable by unification). (FIXME: Not yet implemented.)@@ -339,9 +339,9 @@ > else ((x,ty):cl', Ind sc') > | otherwise = ([], tm) -> refine _ _ _ _ _ = fail "Not focused on a hole"+> refine _ _ _ _ _ = tacfail "Not focused on a hole" - trace (show claims) $ fail "Unimplemented"+ trace (show claims) $ tacfail "Unimplemented" > getClaims :: TT Name -> [(Name, TT Name)] > getClaims (Bind n (B Pi ty) (Sc sc)) = (n,ty):(getClaims sc)@@ -375,17 +375,17 @@ > regret :: Tactic > regret _ _ (Ind (Bind x (B (Guess gv) ty) sc)) = > tacret $ Ind (Bind x (B Hole ty) sc)-> regret _ _ _ = fail "Can't regret something you haven't done"+> regret _ _ _ = tacfail "Can't regret something you haven't done" Attempt to solve the current goal with the guess > solve :: Tactic > solve _ _ (Ind (Bind x (B (Guess gv) ty) sc)) > | (pure gv) = tacret (Ind (Bind x (B (Let (finind gv)) ty) sc))-> | otherwise = fail "I see a hole in your solution"+> | otherwise = tacfail "I see a hole in your solution" > where finind t = case (finalise (Ind t)) of > (Ind x) -> x-> solve _ _ _ = fail "Not a guess"+> solve _ _ _ = tacfail "Not a guess" Substitute a let bound variable into a term @@ -394,7 +394,7 @@ > tacret $ {- trace ("Cutting "++show v++" into "++show sc) $ -} > Ind (substName x (makePsEnv (map fst env) v) sc) > where-> cut _ _ _ = fail "Not a let bound term"+> cut _ _ _ = tacfail "Not a let bound term" Normalise the goal @@ -402,8 +402,8 @@ > evalGoal gam env (Ind (Bind x (B Hole ty) sc)) = > do let (Ind nty) = eval_nf_env (ptovenv env) gam (finalise (Ind ty)) > tacret $ Ind (Bind x (B Hole nty) sc)-> evalGoal _ _ (Ind (Bind x _ _)) = fail $ "evalGoal: " ++ show x ++ " Not a hole"-> evalGoal _ _ _ = fail "evalGoal: Can't happen"+> evalGoal _ _ (Ind (Bind x _ _)) = tacfail $ "evalGoal: " ++ show x ++ " Not a hole"+> evalGoal _ _ _ = tacfail "evalGoal: Can't happen" Do beta reductions (i.e., normalise the goal without expanding global names) @@ -411,22 +411,22 @@ > betaReduce gam env (Ind (Bind x (B Hole ty) sc)) = > do let (Ind nty) = normaliseEnv (ptovenv env) (emptyGam) (finalise (Ind ty)) > tacret $ Ind (Bind x (B Hole nty) sc)-> betaReduce _ _ (Ind (Bind x _ _)) = fail $ "betaReduce: " ++ show x ++ " Not a hole"-> betaReduce _ _ _ = fail "betaReduce: Not a binder, can't happen"+> betaReduce _ _ (Ind (Bind x _ _)) = tacfail $ "betaReduce: " ++ show x ++ " Not a hole"+> betaReduce _ _ _ = tacfail "betaReduce: Not a binder, can't happen" Normalise the goal, only expanding the given global name. > reduceWith :: Name ->Tactic > reduceWith fn gam env (Ind (Bind x (B Hole ty) sc)) = > do case glookup fn gam of-> Nothing -> fail $ "Unknown name " ++ show fn+> Nothing -> tacfail $ "Unknown name " ++ show fn > Just (v,t) -> do > let (Ind nty) = normaliseEnv (ptovenv env) > (extend emptyGam (fn, (G v t defplicit))) > (finalise (Ind ty)) > tacret $ Ind (Bind x (B Hole nty) sc)-> reduceWith _ _ _ (Ind (Bind x _ _)) = fail $ "reduceWith: " ++ show x ++ " Not a hole"-> reduceWith _ _ _ _ = fail "reduceWith: Not a binder, can't happen"+> reduceWith _ _ _ (Ind (Bind x _ _)) = tacfail $ "reduceWith: " ++ show x ++ " Not a hole"+> reduceWith _ _ _ _ = tacfail "reduceWith: Not a binder, can't happen" Do case analysis by the given elimination operator @@ -462,7 +462,7 @@ > meths <- getMeths sc > let names = map fst env > return ((mname,(uniqifyBinders names ty)), meths)-> getBits _ = fail "What's my motivation?"+> getBits _ = tacfail "What's my motivation?" > getMeths (Bind meth (B Pi ty) (Sc sc)) = do > rest <- getMeths sc > return ((meth,ty):rest)@@ -474,7 +474,7 @@ > substTerm earg (P marg) (Sc (motiveType xs ty)) > mkGuess [] n = n > mkGuess ((x,_):xs) n = (mkGuess xs (App n (P x)))-> by _ _ _ _ = fail "Not focussed on a hole"+> by _ _ _ _ = tacfail "Not focussed on a hole" Do case analysis on the given term. Work out which elimination rule is needed and the necessary indices, then run the 'by' tactic.@@ -492,7 +492,7 @@ > let indices = getArgs btin > let ty = getFun btin > runCaseTac rec ty (indices++[bvin]) gam env tm-> casetac _ _ _ _ _ = fail "Not focussed on a hole"+> casetac _ _ _ _ _ = tacfail "Not focussed on a hole" > runCaseTac :: Bool -> TT Name -> [TT Name] -> Tactic > runCaseTac rec (TyCon n _) args gam env tm =@@ -501,11 +501,11 @@ > by (mkapp (Var (if rec then erule else crule)) > (map forget args)) gam env tm > (Just (TCon _ NoConstructorsYet)) ->-> fail $ (show n) ++ " is declared but not defined"-> _ -> fail $ (show n) ++ " is not a type constructor"+> tacfail $ (show n) ++ " is declared but not defined"+> _ -> tacfail $ (show n) ++ " is not a type constructor" > runCaseTac _ x indices gam env tm =-> fail $ (show x) ++ " is not a type constructor"+> tacfail $ (show x) ++ " is not a type constructor" elimargs <- Get arguments to elimination operator motiveargs <- Get expected arguments to motive@@ -534,9 +534,9 @@ > tacret $ Ind (Bind x (B Hole renamed) sc) > where doRename n (Bind x b sc) > = return (Bind n b (Sc (substName x (P n) sc)))-> doRename _ _ = fail "Nothing to rename"-> rename _ _ _ (Ind (Bind x _ _)) = fail $ "rename: " ++ show x ++ " Not a hole"-> rename _ _ _ _ = fail "rename: Not a binder, can't happen"+> doRename _ _ = tacfail "Nothing to rename"+> rename _ _ _ (Ind (Bind x _ _)) = tacfail $ "rename: " ++ show x ++ " Not a hole"+> rename _ _ _ _ = tacfail "rename: Not a binder, can't happen" Make sure the binder has a user accessible name @@ -548,11 +548,11 @@ > where doRename (Bind x b sc) > = do let n = uniqify (sensible x) (map fst env) > return (Bind n b (Sc (substName x (P n) sc)))-> doRename _ = fail "Nothing to rename"+> doRename _ = tacfail "Nothing to rename" > sensible n@(MN _) = UN "X" > sensible x = x-> rename_user _ _ (Ind (Bind x _ _)) = fail $ "rename: " ++ show x ++ " Not a hole"-> rename_user _ _ _ = fail "rename: Not a binder, can't happen"+> rename_user _ _ (Ind (Bind x _ _)) = tacfail $ "rename: " ++ show x ++ " Not a hole"+> rename_user _ _ _ = tacfail "rename: Not a binder, can't happen" Introduce a lambda or let @@ -563,8 +563,8 @@ > let ty' = makePsEnv (map fst env) ty > introsty (uniqify (sensible x) (map fst env)) ty' (Sc p) > | otherwise =-> fail $ "Not an introduceable hole. Attack it first."-> intro _ _ _ = fail $ "Can't introduce here."+> tacfail $ "Not an introduceable hole. Attack it first."+> intro _ _ _ = tacfail $ "Can't introduce here." > sensible (MN _) = (UN "X") -- don't use machine names > sensible x = x@@ -573,7 +573,7 @@ > tacret $ Ind (Bind y (B Lambda s) (Sc (Bind x (B Hole t) xscope))) > introsty x (Bind y (B (Let v) s) (Sc t)) xscope = > tacret $ Ind (Bind y (B (Let v) s) (Sc (Bind x (B Hole t) xscope)))-> introsty x b xscope = fail $ "Nothing to introduce from " ++ show b+> introsty x b xscope = tacfail $ "Nothing to introduce from " ++ show b Tidy up a term to remove all holes which are not used. @@ -598,8 +598,8 @@ > checkConvEnv env gam (Ind goalv) (finalise (Ind ty)) > (IMessage "Not equivalent to the Goal") > tacret $ Ind (Bind x (B Hole goalvin) sc)-> equiv _ _ _ (Ind (Bind x _ _)) = fail $ "equiv: " ++ show x ++ " Not a hole"-> equiv _ _ _ _ = fail "equiv: Not a binder, can't happen"+> equiv _ _ _ (Ind (Bind x _ _)) = tacfail $ "equiv: " ++ show x ++ " Not a hole"+> equiv _ _ _ _ = tacfail "equiv: Not a binder, can't happen" > generalise :: Raw -> Tactic > generalise expr gam env (Ind (Bind x (B Hole tyin) sc)) =@@ -616,8 +616,8 @@ > let newty = Bind newname (B Pi exprtin) (Sc newtysc) > let newsc = substName x (App (P x) exprvin) sc > tacret $ Ind (Bind x (B Hole newty) (Sc newsc))-> generalise _ _ _ (Ind (Bind x b sc)) = fail $ "generalise: " ++ show x ++ " Not a hole"-> generalise _ _ _ _ = fail "generalise: Can't happen"+> generalise _ _ _ (Ind (Bind x b sc)) = tacfail $ "generalise: " ++ show x ++ " Not a hole"+> generalise _ _ _ _ = tacfail "generalise: Can't happen" Replace a term in the goal according to the given equality rule, and the given equality type and replacement/symmetry lemmas.@@ -650,10 +650,10 @@ > claimname = mkns x (UN "q") > getTypes (App (App (App (App eq x) _) a) b) = return (x,a,b) > getTypes (App (App (App eq x) a) b) = return (x,a,b)-> getTypes t = fail $ "Rule is not of equality type: " ++ show t+> getTypes t = tacfail $ "Rule is not of equality type: " ++ show t > mkns (UN a) (UN b) = UN (a++"_"++b)-> replace _ _ _ _ _ _ _ (Ind (Bind x b sc)) = fail $ "replace: " ++ show x ++ " Not a hole"-> replace _ _ _ _ _ _ _ _ = fail "replace: Not a binder, can't happen"+> replace _ _ _ _ _ _ _ (Ind (Bind x b sc)) = tacfail $ "replace: " ++ show x ++ " Not a hole"+> replace _ _ _ _ _ _ _ _ = tacfail "replace: Not a binder, can't happen" Create an axiom for the current goal (quantifying over all bound variables in the goal, and [FIXME!] all variables they depend on) and use it to@@ -672,8 +672,8 @@ > getUsedBoundVars ((n,b@(B _ ty)):bs) ns > | n `elem` ns = (n,ty):(getUsedBoundVars bs ns) > | otherwise = getUsedBoundVars bs ns-> axiomatise _ _ _ _ (Ind (Bind x b sc)) = fail $ "axiomatise: " ++ show x ++ " Not a hole"-> axiomatise _ _ _ _ _ = fail "axiomatise: Not a binder, can't happen"+> axiomatise _ _ _ _ (Ind (Bind x b sc)) = tacfail $ "axiomatise: " ++ show x ++ " Not a hole"+> axiomatise _ _ _ _ _ = tacfail "axiomatise: Not a binder, can't happen" Prepare to return a quoted value @@ -689,10 +689,10 @@ > let filltm = Stage (Quote tm) > return (Ind (Bind h (B (Guess filltm) tyin) sc), [AddGoal qv]) > where checkQuoted (Stage (Code t)) = return t-> checkQuoted _ = fail "Not a code type"+> checkQuoted _ = tacfail "Not a code type" > mkns (UN a) (UN b) = UN (a++"_"++b)-> quote _ _ (Ind (Bind x b sc)) = fail $ "quote: " ++ show x ++ " Not a hole"-> quote _ _ _ = fail "quote: Not a binder, can't happen"+> quote _ _ (Ind (Bind x b sc)) = tacfail $ "quote: " ++ show x ++ " Not a hole"+> quote _ _ _ = tacfail "quote: Not a binder, can't happen" > ptovenv [] = [] > ptovenv ((x,b):xs) = (x,fmap finind b):(ptovenv xs)
Ivor/Typecheck.lhs view
@@ -113,7 +113,7 @@ > Indexed Name -> Indexed Name -> > IvorM (Indexed Name, Indexed Name) > doConversion raw gam constraints (Ind tm) (Ind ty) =-> -- trace ("Finishing checking " ++ show tm ++ " with " ++ show (length constraints) ++ " equations\n" ++ showeqn (map (\x -> (True,x)) constraints)) $ +> -- trace ("Finishing checking " ++ show tm ++ " with " ++ show (length constraints) ++ " equations\n" ++ showeqn (map (\x -> (True,x)) constraints)) $ > -- Unify twice; first time collect the substitutions, second > -- time do them. Because we don't know what order we can solve > -- constraints in and they might depend on each other...@@ -138,11 +138,15 @@ > mkSubstQ (s',nms) (ok, (env,Ind x,Ind y,fc)) all > = do -- (s',nms) <- mkSubst xs > let x' = papp s' x-> let (Ind y') = eval_nf gam (Ind (papp s' y))+> let y' = papp s' y+> let (Ind y'') = -- trace ("Unifying with " ++ show x' ++ " and " ++ show (papp s' y) ++ "[" ++ show (x,y) ++ "]") $ +> eval_nf gam (Ind (papp s' y)) > uns <- case unifyenvErr ok gam env (Ind y') (Ind x') of > Right uns -> return uns-> Left err -> {- trace (showeqn all) $ -} -> ifail (errCtxt fc (ICantUnify (Ind y') (Ind x')))+> Left err -> -- trace (showeqn all) $+> case unifyenvErr ok gam env (Ind y'') (Ind x') of+> Right uns -> return uns+> Left err -> ifail (errCtxt fc (ICantUnify (Ind y') (Ind x'))) Failure err -> fail $ err ++"\n" ++ show nms ++"\n" ++ show constraints -- $ -} ++ " Can't convert "++show x'++" and "++show y' ++ "\n" ++ show constraints ++ "\n" ++ show nms @@ -239,20 +243,20 @@ > e <- convertAllEnv gam bs e > e' <- renameB gam realNames (renameBinders e) > (v1, t1) <- doConversion tm1 gam bs v1 t1-> (v1', t1') <- fixupGam gam realNames (v1, t1)+> (v1'@(Ind lhsret), t1') <- fixupGam gam realNames (v1, t1) > (v1''@(Ind vtm),t1'') <- doConversion tm1 gam bs v1' t1' -- (normalise gam t1') > -- Drop names out of e' that don't appear in v1'' as a result of the > -- unification. > let namesbound = getNames (Sc vtm) > let ein = orderEnv (filter (\ (n, ty) -> n `elem` namesbound) e') > ((v2,t2), (_, _, e'', bs',metas,_)) <- {- trace ("Checking " ++ show tm2 ++ " has type " ++ show t1') $ -} lvlcheck 0 inf next gam ein tm2 (Just t1')-> (v2',t2') <- doConversion tm2 gam bs' v2 t2 -- (normalise gam t2) +> (v2'@(Ind rhsret),t2') <- doConversion tm2 gam bs' v2 t2 -- (normalise gam t2) > let retEnv = reverse (ein ++ e'') > if (null metas) -> then return (v1',t1',v2',t2',retEnv, [])+> then return (Ind (forced gam lhsret),t1',Ind (forced gam rhsret),t2',retEnv, []) > else do let (Ind v2tt) = v2' > let (v2'', newdefs) = updateMetas v2tt-> return (v1',t1',Ind v2'',t2',retEnv, map (\ (x,y) -> (x, (normalise gam (Ind y)))) newdefs)+> return (Ind (forced gam lhsret),t1',Ind (forced gam v2''),t2',retEnv, map (\ (x,y) -> (x, (normalise gam (Ind y)))) newdefs) if (null newdefs) then else trace (traceConstraints bs') $ return (v1',t1',Ind v2'',t2',e'', map (\ (x,y) -> (x, Ind y)) newdefs)@@ -312,22 +316,23 @@ Do the typechecking, then unify all the inferred terms. > tcfixupTop env lvl t exp = do-> tm@(_,tmty) <- tc env lvl t exp+> tm@(Ind tmval,tmty) <- tc env lvl t exp > (next, infer, bindings, errs ,mvs, fc) <- get > -- First, insert inferred values into the term-> tm'@(_,tmty) <- fixup errs tm+> tm'@(_, tmty') <- fixup errs tm > -- Then check the resulting type matches the expected type. > if infer then (case exp of > Nothing -> return ()-> Just expty -> checkConvSt env gamma tmty expty )+> Just expty -> checkConvSt env gamma tmty' expty ) > else return () > -- Then fill in any remained inferred values we got by knowing the > -- expected type > (next, infer, bindings, errs, mvs, fc) <- get-> tm <- fixup errs tm+> tm@(Ind tmval, tmty) <- fixup errs tm > -- bindings <- fixupB gamma errs bindings > put (next, infer, bindings, errs, mvs, fc)-> return tm'+> -- return (Ind (forced gamma tmval), tmty)+> return tm > tcfixup env lvl t exp = do > tm@(_,tmty) <- tc env lvl t exp@@ -357,12 +362,12 @@ > where mkTT (Just (i, B _ t)) _ = return (Ind (P n), Ind t) > mkTT Nothing (Just ((Fun _ _),t)) = return (Ind (P n), t) > mkTT Nothing (Just ((Partial _ _),t)) = return (Ind (P n), t)-> mkTT Nothing (Just ((PatternDef _ _ _),t)) = return (Ind (P n), t)+> mkTT Nothing (Just ((PatternDef _ _ _ _),t)) = return (Ind (P n), t) > mkTT Nothing (Just (Unreducible,t)) = return (Ind (P n), t) > mkTT Nothing (Just (Undefined,t)) = return (Ind (P n), t) > mkTT Nothing (Just ((ElimRule _),t)) = return (Ind (Elim n), t) > mkTT Nothing (Just ((PrimOp _ _),t)) = return (Ind (P n), t)-> mkTT Nothing (Just ((DCon tag i),t)) = return (Ind (Con tag n i), t)+> mkTT Nothing (Just ((DCon tag i _),t)) = return (Ind (Con tag n i), t) > mkTT Nothing (Just ((TCon i _),t)) = return (Ind (TyCon n i), t) > mkTT Nothing Nothing = defaultResult @@ -471,7 +476,7 @@ > else bindings > put (next+1, infer, bindings', errs, mvs, fc) > return (Ind (P (inferName next)), Ind exp)-> tc env lvl RInfer Nothing = fail "Can't infer a term for placeholder"+> tc env lvl RInfer Nothing = lift $ tacfail "Can't infer a term for placeholder" If we have a metavariable, we need to record the type of the expression which will solve it. It needs to take the environment as arguments, and return@@ -483,7 +488,7 @@ > -- Abstract it over the environment so that we have everything > -- in scope we need. > tm <- abstractOver (orderEnv env) n exp []-> {-trace (show tm ++ " : " ++ show exp) $ -}+> -- trace (show tm ++ " : " ++ show exp) $ > return (tm,Ind exp) > -- fail $ show (n, exp, bindings, env) ++ " -- Not implemented" > where abstractOver [] mv exp args =@@ -513,7 +518,7 @@ > let ttnf = normaliseEnv env gamma (Ind tt) > case ttnf of > (Ind Star) -> return (Ind (Stage (Code tv)), Ind Star)-> _ -> fail $ "Type of code " ++ show t ++ " must be *"+> _ -> lift $ tacfail $ "Type of code " ++ show t ++ " must be *" > tcStage env lvl (REval t) _ = do > -- when (lvl/=0) $ fail $ "Can't eval at level " ++ show lvl > (Ind tv, Ind tt) <- tc env lvl t Nothing@@ -521,7 +526,7 @@ > case ttnf of > (Ind (Stage (Code tcode))) -> > return (Ind (Stage (Eval tv tt)), Ind tcode)-> _ -> fail $ "Can't eval a non-quoted term (type " ++ show ttnf ++ ")"+> _ -> lift $ tacfail $ "Can't eval a non-quoted term (type " ++ show ttnf ++ ")" > tcStage env lvl (REscape t) _ = do > -- when (lvl==0) $ fail $ "Can't escape at level " ++ show lvl > (Ind tv, Ind tt) <- tc env lvl t Nothing@@ -529,7 +534,7 @@ > case ttnf of > (Ind (Stage (Code tcode))) -> > return (Ind (Stage (Escape tv tt)), Ind tcode)-> _ -> fail "Can't escape a non-quoted term"+> _ -> lift $ tacfail "Can't escape a non-quoted term" > checkComp env lvl (RComp n ts) = do > tsc <- mapM (\ t -> tcfixup env lvl t Nothing) ts@@ -551,17 +556,18 @@ > checkbinder gamma env lvl n (B Lambda t) = do > (Ind tv,Ind tt) <- tcfixup env lvl t (Just (Ind Star))-> let ttnf = normaliseEnv env gamma (Ind tt)-> let (Ind tvnf) = normaliseEnv env gamma (Ind tv)+> let ttnf = eval_nf_env env gamma (Ind tt)+> let (Ind tvnf) = eval_nf_env env gamma (Ind tv) > case ttnf of > (Ind Star) -> return (B Lambda tvnf) > (Ind (P (MN ("INFER",_)))) -> return (B Lambda tvnf)-> _ -> fail $ "The type of the binder " ++ show n ++ " must be *"+> _ -> lift $ tacfail $ "The type of the binder " ++ show n ++ " must be *" > checkbinder gamma env lvl n (B Pi t) = do > (Ind tv,Ind tt) <- tcfixup env lvl t (Just (Ind Star))-> let (Ind tvnf) = normaliseEnv env gamma (Ind tv)-> -- let ttnf = normaliseEnv env gamma (Ind tt)-> checkConvSt env gamma (Ind tt) (Ind Star)+> let (Ind tvnf) = eval_nf_env env gamma (Ind tv)+> let ttnf = -- trace ("PI: " ++ show (tv, tvnf, debugTT tv)) $ +> eval_nf_env env gamma (Ind tt)+> checkConvSt env gamma ttnf (Ind Star) > return (B Pi tvnf) case ttnf of@@ -580,7 +586,7 @@ > lift $ checkConvEnv env gamma (Ind vt) (Ind tv) (INotConvertible (Ind vt) (Ind tv)) > case ttnf of > (Ind Star) -> return (B (Let vv) tv)-> _ -> fail $ "The type of the binder " ++ show n ++ " must be *"+> _ -> lift $ tacfail $ "The type of the binder " ++ show n ++ " must be *" > where dbg (Ind t) = debugTT t > checkbinder gamma env lvl n (B Hole t) = do@@ -588,7 +594,7 @@ > let ttnf = normaliseEnv env gamma (Ind tt) > case ttnf of > (Ind Star) -> return (B Hole tv)-> _ -> fail $ "The type of the binder " ++ show n ++ " must be *"+> _ -> lift $ tacfail $ "The type of the binder " ++ show n ++ " must be *" > checkbinder gamma env lvl n (B (Guess v) t) = do > (Ind tv,Ind tt) <- tcfixup env lvl t Nothing > (Ind vv,Ind vt) <- tcfixup env lvl v Nothing@@ -596,7 +602,7 @@ > lift $ checkConvEnv env gamma (Ind vt) (Ind tv) (INotConvertible (Ind vt) (Ind tv)) > case ttnf of > (Ind Star) -> return (B (Guess vv) tv)-> _ -> fail $ "The type of the binder " ++ show n ++ " must be *"+> _ -> lift $ tacfail $ "The type of the binder " ++ show n ++ " must be *" > checkpatt gamma env lvl n RInfer t = do > (Ind tv,Ind tt) <- tcfixup env lvl t Nothing@@ -613,7 +619,7 @@ > -- show patt ++ " and " ++ show tv ++ " are not convertible" > case ttnf of > (Ind Star) -> return ((B (Pattern patv) tv), bindings++env)-> _ -> fail $ "The type of the binder " ++ show n ++ " must be *"+> _ -> lift $ tacfail $ "The type of the binder " ++ show n ++ " must be *" Check a raw term representing a pattern. Return the pattern, and the extended environment.
Ivor/Unify.lhs view
@@ -38,10 +38,9 @@ > -- Also, there is no point reducing if we don't have to, and not calling > -- the normaliser really speeds things up if we have a lot of easy > -- constraints to solve...-> unifyenvErr i gam env x y = -- trace ("Unifying in " ++ show env) $ -> {- trace (show (x,y) ++ "\n" +++> unifyenvErr i gam env x y = {- trace ("Unifying " ++ (show (x,y) ++ "\n" ++ > show (p (normalise (gam' gam) x)) ++ "\n" ++-> show (p (normalise (gam' gam) x))) $-}+> show (p (normalise (gam' gam) x)))) $ -} > case unifynferr False env (p x) > (p y) of > (Right x) -> return x@@ -129,6 +128,9 @@ > un envl envr (Call c t) (Call c' t') acc = un envl envr t t' acc > un envl envr (Return t) (Return t') acc = un envl envr t t' acc > un envl envr (Stage x) (Stage y) acc = unst envl envr x y acc+> un envl envr (Meta _ _) (Meta _ _) acc = return acc+> un envl envr Erased _ acc = return acc+> un envl envr _ Erased acc = return acc > un envl envr x y acc > | x == y || ignore = return acc > | otherwise = ifail $ ICantUnify (Ind x) (Ind y)@@ -142,7 +144,7 @@ > unbb envl envr (Guess v) (Guess v') acc = un envl envr v v' acc > unbb envl envr x y acc > = if ignore then return acc-> else fail $ "Can't unify binders " ++ show x ++ " and " ++ show y+> else tacfail $ "Can't unify binders " ++ show x ++ " and " ++ show y > unst envl envr (Quote x) (Quote y) acc = un envl envr x y acc > unst envl envr (Code x) (Code y) acc = un envl envr x y acc@@ -186,9 +188,9 @@ > _ -> False -> substNames :: [(Name,TT Name)] -> TT Name -> TT Name-> substNames [] tm = tm-> substNames ((n,t):xs) tm = substNames xs (substName n t (Sc tm))+ substNames :: [(Name,TT Name)] -> TT Name -> TT Name+ substNames [] tm = tm+ substNames ((n,t):xs) tm = substNames xs (substName n t (Sc tm)) Look for a specific term (unifying with a subterm) and replace it.
Ivor/Values.lhs view
@@ -25,10 +25,11 @@ > data Global n > = Fun [FunOptions] (Indexed n) -- User defined function > | Partial (Indexed n) [n] -- Unfinished definition-> | PatternDef (PMFun n) Bool Bool -- Pattern matching definition, totality, generated+> -- Pattern matching definition, totality, generated, compiled+> | PatternDef (PMFun n) Bool Bool ([n], TSimpleCase n) > | ElimRule ElimRule -- Elimination Rule > | PrimOp PrimOp EvPrim -- Primitive function-> | DCon Int Int -- Data Constructor, tag and arity+> | DCon Int Int [Int] -- Data Constructor, tag and arity, forced args > | TCon Int (Elims n) -- Type Constructor and arity, elim rule name > | Unreducible -- Unreducible name > | Undefined -- Declared but undefined name@@ -45,15 +46,15 @@ > show (Fun opts t) = "Fun " ++ show t > show (ElimRule _) = "<<elim rule>>" > show (PrimOp _ _) = "<<primitive operator>>"-> show (DCon x t) = "DCon " ++ show x ++ "," ++show t+> show (DCon x t f) = "DCon " ++ show x ++ "," ++show t ++ "," ++ show f > show (TCon x (Elims e c cons)) = "TCon " ++ show x > show Unreducible = "Unreducible" > show Undefined = "Undefined" -> type Plicity = Int+> type Plicity = [Int] -- unused and implicit argument positions -> defplicit :: Int-> defplicit = 0+> defplicit :: Plicity+> defplicit = [] > data Ord n => Gval n = G (Global n) (Indexed n) Plicity > deriving Show@@ -82,6 +83,10 @@ > glookup :: (Ord n, Eq n) => n -> Gamma n -> Maybe (Global n,Indexed n) > glookup n (Gam xs) = fmap (\x -> (getglob x,gettype x)) (Map.lookup n xs) +> glookupall :: (Ord n, Eq n) => n -> Gamma n -> +> Maybe (Global n,Indexed n, Plicity)+> glookupall n (Gam xs) = fmap (\x -> (getglob x,gettype x,getplicity x)) (Map.lookup n xs)+ Get a type name from the context > getTyName :: Monad m => Gamma Name -> Name -> m Name@@ -98,7 +103,7 @@ > recCon :: Name -> Gamma Name -> Bool > recCon n gam = case glookup n gam of-> (Just (DCon _ t, Ind ty)) ->+> (Just (DCon _ t _, Ind ty)) -> > checkRec (conFamily ty) (map snd (getExpected ty)) > _ -> False > where conFamily t = fname (getFun (getReturnType t))@@ -156,7 +161,13 @@ > return $ Gam (Map.insert nm val xs) > Just _ -> fail $ "Name " ++ show nm ++ " is already defined" +Replace a name in the context with a new pattern matching definitions +> gReplace :: (Monad m, Ord n, Eq n, Show n) => +> n -> Gval n -> Gamma n -> m (Gamma n)+> gReplace nm val gam = do let gam' = remove nm gam+> gInsert nm val gam'+ An ElimRule is a Haskell implementation of the iota reductions of a family. @@ -180,6 +191,7 @@ > | RTyCon Name (Spine (Model s)) > | forall c. Constant c => RdConst c > | RdStar+> | RdErased > | RdLabel (Model s) (MComp s) > | RdCall (MComp s) (Model s) > | RdReturn (Model s)@@ -211,3 +223,28 @@ > type Value = Model Kripke > type Normal = Model Scope++Erase forced arguments from an application++> forced :: Gamma Name -> TT Name -> TT Name+> forced gam x = x++> {-+> forced gam (Bind n b (Sc t)) = Bind n (forcedb b) (Sc (forced gam t))+> where forcedb (B (Let v) ty) = B (Let (forced gam v)) ty+> forcedb b = b+> forced gam ap@(App f a) = force' f [(forced gam a)]+> where force' (App f a) as = force' f ((forced gam a):as)+> force' c@(Con _ n _) as -- put forced args here for efficiency?+> = case lookupval n gam of+> Just (DCon _ _ fs) -> let res = appArgs c (erase fs 0 as)+> in res -- trace (show res) res+> _ -> ap+> force' _ _ = ap++> erase fs i [] = []+> erase fs i (x:xs)+> | i `elem` fs = Erased:(erase fs (i+1) xs)+> | otherwise = x:(erase fs (i+1) xs)+> forced gam x = x+> -}
Ivor/ViewTerm.lhs view
@@ -17,12 +17,15 @@ > -- * Terms > Term(..), ViewTerm(..), Annot(..), apply, > view, viewType, ViewConst, typeof, -> freeIn, namesIn, occursIn, subst, getApp, +> freeIn, namesIn, namesTypesIn, occursIn, +> subst, getApp, > Ivor.ViewTerm.getFnArgs, transform, > getArgTypes, Ivor.ViewTerm.getReturnType, > dbgshow, > -- * Inductive types-> Inductive(..)) +> Inductive(..),+> -- * Compile pattern matches+> SimpleCase(..), CaseAlt(..)) > where > import Ivor.TTCore as TTCore hiding (subst)@@ -54,7 +57,7 @@ > -- is for. > data NameType = Bound | Free | DataCon | TypeCon | ElimOp > | Unknown -- ^ Use for sending to typechecker.-> deriving (Show, Enum)+> deriving (Show, Enum, Eq) > -- | Construct a term representing a variable > mkVar :: String -- ^ Variable name@@ -85,8 +88,21 @@ > data Annot = FileLoc FilePath Int -- ^ source file, line number +> data SimpleCase = SCase ViewTerm [CaseAlt]+> | Tm ViewTerm+> | ErrorCase+> | Impossible+> deriving Show +> data CaseAlt = Alt Name Int [Name] SimpleCase+> | forall c. Constant c => ConstAlt c SimpleCase+> | Default SimpleCase +> instance Show CaseAlt where+> show (Alt n i args sc) = "Alt " ++ show (n,i) ++ " " ++ +> show args ++ " => " ++ show sc+> show (Default sc) = "Default => " ++ show sc+ > instance Eq ViewTerm where > (==) (Name _ x) (Name _ y) = x == y > (==) (Ivor.ViewTerm.App f a) (Ivor.ViewTerm.App f' a') = f == f' && a == a'@@ -213,6 +229,7 @@ > vtaux ctxt (Stage (TTCore.Escape tm _)) > = Ivor.ViewTerm.Escape (vtaux ctxt tm) > vtaux ctxt (Meta n _) = Metavar n+> vtaux ctxt Erased = Placeholder > vtaux _ t = error $ "Can't happen vtaux " ++ debugTT t > -- | Return whether the name occurs free in the term.@@ -241,9 +258,13 @@ > -- | Return the names occurring free in a term > namesIn :: ViewTerm -> [Name]-> namesIn t = nub $ fi [] t where-> fi ns (Ivor.ViewTerm.Name _ x) | x `elem` ns = []-> | otherwise = [x]+> namesIn t = nub $ (map fst (namesTypesIn t))++> -- | Return the names occurring free in a term, and what kind of name they are+> namesTypesIn :: ViewTerm -> [(Name, NameType)]+> namesTypesIn t = nub $ fi [] t where+> fi ns (Ivor.ViewTerm.Name t x) | x `elem` ns = []+> | otherwise = [(x, t)] > fi ns (Ivor.ViewTerm.App f a) = fi ns f ++ fi ns a > fi ns (Ivor.ViewTerm.Lambda x ty sc) = fi (x:ns) sc > fi ns (Forall x ty sc) = fi (x:ns) sc@@ -397,6 +418,7 @@ > case tag of > 0 -> liftM UN get > 1 -> liftM MN get+> n -> error $ "ViewTerm.lhs: Unknown Name tag " ++ show n > instance Binary NameType where > put x = put (fromEnum x)
ivor.cabal view
@@ -1,5 +1,5 @@ Name: ivor-Version: 0.1.12+Version: 0.1.14 Author: Edwin Brady License: BSD3 License-file: LICENSE@@ -69,16 +69,18 @@ -- GHC-options: -Wall Exposed-modules:- Ivor.TT, Ivor.Shell, Ivor.Primitives,+ Ivor.TT, Ivor.CtxtTT, Ivor.EvalTT,+ Ivor.Shell, Ivor.Primitives, Ivor.TermParser, Ivor.ViewTerm, Ivor.Equality, Ivor.Plugin, Ivor.Construction Other-modules: Ivor.Nobby, Ivor.TTCore, Ivor.State, Ivor.Tactics, Ivor.Typecheck, Ivor.Evaluator- Ivor.Gadgets, Ivor.SC, Ivor.Bytecode, Ivor.Values,- Ivor.CodegenC, Ivor.Datatype, Ivor.Display,- Ivor.ICompile, Ivor.MakeData, Ivor.Unify,- Ivor.Grouper, Ivor.ShellParser, Ivor.Constant,- Ivor.RunTT, Ivor.Compiler, Ivor.Errors,+ Ivor.Gadgets, Ivor.Values,+ Ivor.Datatype, Ivor.Display,+ Ivor.MakeData, Ivor.Unify,+ Ivor.ShellParser, Ivor.Constant,+ Ivor.Errors, Ivor.PatternDefs, Ivor.ShellState, Ivor.Scopecheck,- Ivor.Overloading,+ Ivor.Overloading, Ivor.PMComp, Paths_ivor+ghc-prof-options: -auto-all