diff --git a/Ivor/Bytecode.lhs b/Ivor/Bytecode.lhs deleted file mode 100644 --- a/Ivor/Bytecode.lhs +++ /dev/null @@ -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 - diff --git a/Ivor/CodegenC.lhs b/Ivor/CodegenC.lhs deleted file mode 100644 --- a/Ivor/CodegenC.lhs +++ /dev/null @@ -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 \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 diff --git a/Ivor/Compiler.lhs b/Ivor/Compiler.lhs deleted file mode 100644 --- a/Ivor/Compiler.lhs +++ /dev/null @@ -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) -> -} diff --git a/Ivor/CtxtTT.lhs b/Ivor/CtxtTT.lhs new file mode 100644 --- /dev/null +++ b/Ivor/CtxtTT.lhs @@ -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 + diff --git a/Ivor/Datatype.lhs b/Ivor/Datatype.lhs --- a/Ivor/Datatype.lhs +++ b/Ivor/Datatype.lhs @@ -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 diff --git a/Ivor/Errors.lhs b/Ivor/Errors.lhs --- a/Ivor/Errors.lhs +++ b/Ivor/Errors.lhs @@ -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 diff --git a/Ivor/EvalTT.lhs b/Ivor/EvalTT.lhs new file mode 100644 --- /dev/null +++ b/Ivor/EvalTT.lhs @@ -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) + + + diff --git a/Ivor/Evaluator.lhs b/Ivor/Evaluator.lhs --- a/Ivor/Evaluator.lhs +++ b/Ivor/Evaluator.lhs @@ -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 diff --git a/Ivor/Grouper.lhs b/Ivor/Grouper.lhs deleted file mode 100644 --- a/Ivor/Grouper.lhs +++ /dev/null @@ -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 - diff --git a/Ivor/ICompile.lhs b/Ivor/ICompile.lhs deleted file mode 100644 --- a/Ivor/ICompile.lhs +++ /dev/null @@ -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) diff --git a/Ivor/Nobby.lhs b/Ivor/Nobby.lhs --- a/Ivor/Nobby.lhs +++ b/Ivor/Nobby.lhs @@ -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)) diff --git a/Ivor/PMComp.lhs b/Ivor/PMComp.lhs new file mode 100644 --- /dev/null +++ b/Ivor/PMComp.lhs @@ -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 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 + diff --git a/Ivor/PatternDefs.lhs b/Ivor/PatternDefs.lhs --- a/Ivor/PatternDefs.lhs +++ b/Ivor/PatternDefs.lhs @@ -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, []) + diff --git a/Ivor/RunTT.lhs b/Ivor/RunTT.lhs deleted file mode 100644 --- a/Ivor/RunTT.lhs +++ /dev/null @@ -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) diff --git a/Ivor/SC.lhs b/Ivor/SC.lhs deleted file mode 100644 --- a/Ivor/SC.lhs +++ /dev/null @@ -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 diff --git a/Ivor/Scopecheck.lhs b/Ivor/Scopecheck.lhs --- a/Ivor/Scopecheck.lhs +++ b/Ivor/Scopecheck.lhs @@ -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) diff --git a/Ivor/State.lhs b/Ivor/State.lhs --- a/Ivor/State.lhs +++ b/Ivor/State.lhs @@ -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) diff --git a/Ivor/TT.lhs b/Ivor/TT.lhs --- a/Ivor/TT.lhs +++ b/Ivor/TT.lhs @@ -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 diff --git a/Ivor/TTCore.lhs b/Ivor/TTCore.lhs --- a/Ivor/TTCore.lhs +++ b/Ivor/TTCore.lhs @@ -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 diff --git a/Ivor/Tactics.lhs b/Ivor/Tactics.lhs --- a/Ivor/Tactics.lhs +++ b/Ivor/Tactics.lhs @@ -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) diff --git a/Ivor/Typecheck.lhs b/Ivor/Typecheck.lhs --- a/Ivor/Typecheck.lhs +++ b/Ivor/Typecheck.lhs @@ -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. diff --git a/Ivor/Unify.lhs b/Ivor/Unify.lhs --- a/Ivor/Unify.lhs +++ b/Ivor/Unify.lhs @@ -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. diff --git a/Ivor/Values.lhs b/Ivor/Values.lhs --- a/Ivor/Values.lhs +++ b/Ivor/Values.lhs @@ -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 _) = "<>" > show (PrimOp _ _) = "<>" -> 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 +> -} diff --git a/Ivor/ViewTerm.lhs b/Ivor/ViewTerm.lhs --- a/Ivor/ViewTerm.lhs +++ b/Ivor/ViewTerm.lhs @@ -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) diff --git a/ivor.cabal b/ivor.cabal --- a/ivor.cabal +++ b/ivor.cabal @@ -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