diff --git a/Ivor/Construction.lhs b/Ivor/Construction.lhs --- a/Ivor/Construction.lhs +++ b/Ivor/Construction.lhs @@ -79,7 +79,7 @@ > -- | Try to solve a goal @A@ by evaluating a term of type @Maybe A@. If the -> -- answer is @just a@, fill in the goal with the proof term @a@. +> -- answer is @Just a@, fill in the goal with the proof term @a@. > isItJust :: IsTerm a => a -> Tactic > isItJust tm g ctxt = do > gd <- goalData ctxt False g @@ -90,9 +90,9 @@ > case ty of > (App (Name _ m) a) | m == (name "Maybe") > -> do case prf of -> (App (Name _ n) _) | n == (name "nothing") +> (App (Name _ n) _) | n == (name "Nothing") > -> fail "No solution found" -> (App (App (Name _ j) _) p) | j == (name "just") +> (App (App (Name _ j) _) p) | j == (name "Just") > -> fill p g ctxt > tm -> fail $ "Evaluated to " ++ show tm > _ -> fail $ "Type of decision procedure must be ++ " ++ diff --git a/Ivor/Datatype.lhs b/Ivor/Datatype.lhs --- a/Ivor/Datatype.lhs +++ b/Ivor/Datatype.lhs @@ -34,8 +34,8 @@ > num_params :: Int, > erule :: (n, Indexed n), > crule :: (n, Indexed n), -> e_ischemes :: PMFun Name, -> c_ischemes :: PMFun Name, +> e_ischemes :: Maybe (PMFun Name), +> c_ischemes :: Maybe (PMFun Name), > e_rawschemes :: [RawScheme], > c_rawschemes :: [RawScheme] > } @@ -61,13 +61,25 @@ > (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 -> (csch, _) <- checkDef gamma'' cr crty cschemes False False +> (esch, _, _, _) <- checkDef gamma'' er erty eschemes False False +> (csch, _, _, _) <- checkDef gamma'' cr crty cschemes False False > return (Data (ty,G (TCon (arity gamma kv) erdata) kv defplicit) consv numps -> (er,ev) (cr,cv) esch csch eschemes cschemes) +> (er,ev) (cr,cv) (Just esch) (Just csch) eschemes cschemes) -> where checkCons gamma t [] = return ([], gamma) -> checkCons gamma t ((cn,cty):cs) = +> checkTypeNoElim :: Monad m => Gamma Name -> RawDatatype -> m (Datatype Name) +> checkTypeNoElim gamma (RData (ty,kind) cons numps (er,erty) (cr,crty) eschemes cschemes) = +> do (kv, _) <- typecheck gamma kind +> let erdata = Elims er cr (map fst cons) +> let gamma' = extend gamma (ty,G (TCon (arity gamma kv) erdata) kv defplicit) +> (consv,gamma'') <- checkCons gamma' 0 cons +> (ev, _) <- typecheck gamma'' erty +> (cv, _) <- typecheck gamma'' crty +> -- let gamma''' = extend gamma'' (er,G (ElimRule dummyRule) ev defplicit) +> return (Data (ty,G (TCon (arity gamma kv) erdata) kv defplicit) consv numps +> (er,ev) (cr,cv) Nothing Nothing [] []) + +> checkCons gamma t [] = return ([], gamma) +> checkCons gamma t ((cn,cty):cs) = > do (cv,_) <- typecheck gamma cty > let ccon = G (DCon t (arity gamma cv)) cv defplicit > let gamma' = extend gamma (cn,ccon) diff --git a/Ivor/Display.lhs b/Ivor/Display.lhs --- a/Ivor/Display.lhs +++ b/Ivor/Display.lhs @@ -18,7 +18,7 @@ > displayHole :: [Name] -> Gamma Name -> Env Name -> Indexed Name -> String > displayHole hidden gam hs tm = dh hs ++ > "\n=======================================\n" ++ -> show (normaliseEnv hs (Gam []) tm) ++ "\n" +> show (normaliseEnv hs emptyGam tm) ++ "\n" > where dh [] = "" > dh ((n,B _ ty):xs) > | n `elem` hidden = dh xs diff --git a/Ivor/Evaluator.lhs b/Ivor/Evaluator.lhs --- a/Ivor/Evaluator.lhs +++ b/Ivor/Evaluator.lhs @@ -1,11 +1,12 @@ > {-# OPTIONS_GHC -fglasgow-exts #-} -> module Ivor.Evaluator(eval_whnf) where +> module Ivor.Evaluator(eval_whnf, eval_nf) where > import Ivor.TTCore > import Ivor.Gadgets > import Ivor.Constant > import Ivor.Nobby +> import Ivor.Typecheck > import Debug.Trace > import Data.Typeable @@ -18,10 +19,15 @@ > eval_whnf gam (Ind tm) = let res = makePs (evaluate False gam tm) > in finalise (Ind res) +> eval_nf :: Gamma Name -> Indexed Name -> Indexed Name +> eval_nf gam (Ind tm) = let res = makePs (evaluate True gam tm) +> in finalise (Ind res) + > type Stack = [TT Name] > type SEnv = [(Name, TT Name, TT Name)] > getEnv i env = (\ (_,_,val) -> val) (env!!i) +> sfst (n,_,_) = n Code Stack Env Result @@ -62,7 +68,7 @@ > 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 +> 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 @@ -71,9 +77,12 @@ > evalScope n ty sc (x:xs) env pats = eval sc xs ((n,ty,x):env) pats > evalScope n ty sc [] env pats -> | open = error "Normalising not implemented" -> | otherwise -> = buildenv env $ unload (Bind n (B Lambda ty) (Sc sc)) [] pats env -- in Whnf +> | open = let n' = uniqify n (map sfst env) +> newsc = pToV n' (eval sc [] ((n',ty,P n'):env) pats) in +> buildenv env $ unload (Bind n' (B Lambda ty) newsc) +> [] pats env +> | otherwise +> = buildenv env $ unload (Bind n (B Lambda ty) (Sc sc)) [] pats env -- in Whnf > unload x [] pats env > = foldl (\tm (n,val) -> substName n val (Sc tm)) x pats > unload x (a:as) pats env = unload (App x a) as pats env diff --git a/Ivor/Gadgets.lhs b/Ivor/Gadgets.lhs --- a/Ivor/Gadgets.lhs +++ b/Ivor/Gadgets.lhs @@ -81,3 +81,6 @@ > catch (do content <- readFile $ d ++ "/" ++ fn > return content) > (\e -> ff' ds fn) + +> unJust :: Maybe a -> a +> unJust (Just a) = a diff --git a/Ivor/ICompile.lhs b/Ivor/ICompile.lhs --- a/Ivor/ICompile.lhs +++ b/Ivor/ICompile.lhs @@ -85,6 +85,6 @@ > _ -> Nothing > doElim sp (IReduce (Ind t)) > = let recrule = mkElim ename ty arity cs -> gam = Gam ((ename,G (ElimRule recrule) ty defplicit):[]) +> gam = extend emptyGam (ename,G (ElimRule recrule) ty defplicit) > red = (nf gam (VG (revlistify sp)) [] False t) > in (Just red) diff --git a/Ivor/MakeData.lhs b/Ivor/MakeData.lhs --- a/Ivor/MakeData.lhs +++ b/Ivor/MakeData.lhs @@ -29,7 +29,7 @@ > cischemes = mkSchemes False name (ruleName name "Case") > params datacons motiveName methNames > tycontype = mkCon params contype in -> return $ --(trace (show ischemes)) $ +> return $ -- (trace (show eischemes)) $ > RData (name,tycontype) datacons (length params) > (ruleName name "Elim", ecasetype) -- elim rule > (ruleName name "Case", ccasetype) -- case rule diff --git a/Ivor/Nobby.lhs b/Ivor/Nobby.lhs --- a/Ivor/Nobby.lhs +++ b/Ivor/Nobby.lhs @@ -9,6 +9,7 @@ > import Data.List > import Control.Monad > import Data.Typeable +> import qualified Data.Map as Map > import Debug.Trace @@ -23,7 +24,7 @@ > data Global n > = Fun [FunOptions] (Indexed n) -- User defined function > | Partial (Indexed n) [n] -- Unfinished definition -> | PatternDef (PMFun n) -- Pattern matching definition +> | PatternDef (PMFun n) Bool -- Pattern matching definition, totality > | ElimRule ElimRule -- Elimination Rule > | PrimOp PrimOp EvPrim -- Primitive function > | DCon Int Int -- Data Constructor, tag and arity @@ -36,7 +37,7 @@ > constructors :: [n] } > | NoConstructorsYet -> data FunOptions = Frozen | Recursive +> data FunOptions = Frozen | Recursive | Total > deriving Eq > instance Show n => Show (Global n) where @@ -52,29 +53,33 @@ > defplicit = 0 -> data Gval n = G (Global n) (Indexed n) Plicity +> data Ord n => Gval n = G (Global n) (Indexed n) Plicity > deriving Show > getglob (G v t p) = v > gettype (G v t p) = t > getplicity (G v t p) = p -> newtype Gamma n = Gam [(n,Gval n)] +> newtype Ord n => Gamma n = Gam (Map.Map n (Gval n)) > deriving Show -> extend (Gam x) (n,v) = Gam ((n,v):x) +> extend (Gam x) (n,v) = Gam (Map.insert n v x) -> emptyGam = Gam [] +> emptyGam :: Ord n => Gamma n +> emptyGam = Gam Map.empty -> lookupval :: Eq n => n -> Gamma n -> Maybe (Global n) -> lookupval n (Gam xs) = fmap getglob (lookup n xs) +> getAList :: Ord n => Gamma n -> [(n,(Gval n))] +> getAList (Gam n) = Map.toAscList n -> lookuptype :: Eq n => n -> Gamma n -> Maybe (Indexed n) -> lookuptype n (Gam xs) = fmap gettype (lookup n xs) +> lookupval :: (Ord n, Eq n) => n -> Gamma n -> Maybe (Global n) +> lookupval n (Gam xs) = fmap getglob (Map.lookup n xs) -> glookup :: Eq n => n -> Gamma n -> Maybe (Global n,Indexed n) -> glookup n (Gam xs) = fmap (\x -> (getglob x,gettype x)) (lookup n xs) +> lookuptype :: (Ord n, Eq n) => n -> Gamma n -> Maybe (Indexed n) +> lookuptype n (Gam xs) = fmap gettype (Map.lookup n xs) +> 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) + Get a type name from the context > getTyName :: Monad m => Gamma Name -> Name -> m Name @@ -100,62 +105,54 @@ > checkRec n [] = False > checkRec n (x:xs) = nameOccurs n (forget x) || checkRec n xs -> insertGam :: n -> Gval n -> Gamma n -> Gamma n -> insertGam nm val (Gam gam) = Gam $ (nm,val):gam +> insertGam :: Ord n => n -> Gval n -> Gamma n -> Gamma n +> insertGam nm val (Gam gam) = Gam $ Map.insert nm val gam -> concatGam :: Gamma n -> Gamma n -> Gamma n -> concatGam (Gam x) (Gam y) = Gam (x++y) +> concatGam :: Ord n => Gamma n -> Gamma n -> Gamma n +> concatGam (Gam x) (Gam y) = Gam (Map.union x y) -> setFrozen :: Eq n => n -> Bool -> Gamma n -> Gamma n -> setFrozen n freeze (Gam xs) = Gam $ sf xs where -> sf [] = [] -> sf ((p,G (Fun opts v) ty plicit):xs) -> | n == p = (p,G (Fun (doFreeze freeze opts) v) ty plicit):xs -> sf (x:xs) = x:(sf xs) +> setFrozen :: (Ord n, Eq n) => n -> Bool -> Gamma n -> Gamma n +> setFrozen n freeze (Gam xs) = Gam $ Map.mapWithKey sf xs where +> sf p (G (Fun opts v) ty plicit) +> | n == p = (G (Fun (doFreeze freeze opts) v) ty plicit) +> sf _ x = x > doFreeze True opts = nub (Frozen:opts) > doFreeze False opts = opts \\ [Frozen] -> setRec :: Eq n => n -> Bool -> Gamma n -> Gamma n -> setRec n frec (Gam xs) = Gam $ sf xs where -> sf [] = [] -> sf ((p,G (Fun opts v) ty plicit):xs) -> | n == p = (p,G (Fun (doFrec frec opts) v) ty plicit):xs -> sf (x:xs) = x:(sf xs) +> setRec :: (Ord n, Eq n) => n -> Bool -> Gamma n -> Gamma n +> setRec n frec (Gam xs) = Gam $ Map.mapWithKey sf xs where +> sf p (G (Fun opts v) ty plicit) +> | n == p = (G (Fun (doFrec frec opts) v) ty plicit) +> sf _ x = x > doFrec True opts = nub (Recursive:opts) > doFrec False opts = opts \\ [Recursive] -> freeze :: Eq n => n -> Gamma n -> Gamma n +> freeze :: (Ord n, Eq n) => n -> Gamma n -> Gamma n > freeze n gam = setFrozen n True gam -> thaw :: Eq n => n -> Gamma n -> Gamma n +> thaw :: (Ord n, Eq n) => n -> Gamma n -> Gamma n > thaw n gam = setFrozen n False gam Remove a name from the middle of the context - should only be valid if it's a partial definition or an axiom which is about to be replaced. -> remove :: Eq n => n -> Gamma n -> Gamma n -> remove n (Gam xs) = Gam $ rm n xs where -> rm n [] = [] -> rm n (d@(p,_):xs) | n==p = xs -> | otherwise = d:(rm n xs) +> remove :: (Ord n, Eq n) => n -> Gamma n -> Gamma n +> remove n (Gam xs) = Gam $ Map.delete n xs Insert a name into the context. If the name is already there, this is an error *unless* the old definition was 'Undefined', in which case the name is replaced. -> gInsert :: (Monad m, Eq n, Show n) => n -> Gval n -> Gamma n -> m (Gamma n) -> gInsert nm val (Gam xs) = do xs' <- ins nm val xs [] -> return $ Gam xs' -> where ins n val [] acc = return $ (n,val):(reverse acc) +> gInsert :: (Monad m, Ord n, Eq n, Show n) => +> n -> Gval n -> Gamma n -> m (Gamma n) +> gInsert nm val (Gam xs) = case Map.lookup nm xs of > -- FIXME: Check ty against val -> ins n val (d@(p,G Undefined ty _):xs) acc -> | n == p = return $ (n,val):(reverse acc) ++ xs -> ins n val (d@(p,G (TCon _ NoConstructorsYet) ty _):xs) acc -> | n == p = return $ (n,val):(reverse acc) ++ xs -> ins n val (d@(p,_):xs) acc -> | n == p = fail $ "Name " ++ show p ++ " is already defined" -> | otherwise = ins n val xs (d:acc) +> Nothing -> return $ Gam (Map.insert nm val xs) +> Just (G Undefined ty _) -> return $ Gam (Map.insert nm val xs) +> Just (G (TCon _ NoConstructorsYet) ty _) -> +> return $ Gam (Map.insert nm val xs) +> Just _ -> fail $ "Name " ++ show nm ++ " is already defined" An ElimRule is a Haskell implementation of the iota reductions of a family. @@ -243,11 +240,11 @@ > 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))) @@ -306,7 +303,7 @@ > -- This is again a bit of a hack, just evaluating without any definitions > -- but it is a nice cheap way of seeing what we'd have to generate code > -- for at run-time. -> else MR (RdQuote (eval (stage+1) (Gam []) g t)) +> else MR (RdQuote (eval (stage+1) (Gam Map.empty) g t)) > -- else let cd = (forget ((quote (eval (Gam []) g t)::Normal))) in > -- MR (RdQuote cd) > -- MR (RdQuote (substV g t)) --(splice t)) -- broken @@ -376,6 +373,7 @@ > = do newvals <- pmatch pat val vals > newvals <- checkdups newvals > pm gam g ps vs ret newvals +> pm _ _ _ _ _ _ = Nothing > checkdups v = Just v @@ -622,7 +620,7 @@ > = normalise (addenv env g) t > where addenv [] g = g > addenv ((n,B (Let v) ty):xs) (Gam g) -> = addenv xs (Gam ((n,G (Fun [] (Ind v)) (Ind ty) defplicit):g)) +> = addenv xs (Gam (Map.insert n (G (Fun [] (Ind v)) (Ind ty) defplicit) g)) > addenv (_:xs) g = addenv xs g > convNormaliseEnv :: Env Name -> Gamma Name -> Indexed Name -> Indexed Name @@ -630,7 +628,7 @@ > = convNormalise (addenv env g) t > where addenv [] g = g > addenv ((n,B (Let v) ty):xs) (Gam g) -> = addenv xs (Gam ((n,G (Fun [] (Ind v)) (Ind ty) defplicit):g)) +> = addenv xs (Gam (Map.insert n (G (Fun [] (Ind v)) (Ind ty) defplicit) g)) > addenv (_:xs) g = addenv xs g = Ind (forget (quote (nf g (VG (valenv env [])) t)::Normal)) @@ -665,11 +663,13 @@ ====================== Functors for contexts =============================== -> instance Functor Gamma where -> fmap f (Gam xs) = Gam (fmap (\ (x,y) -> (f x,fmap f y)) xs) + instance Functor Gamma where + fmap f (Gam xs) = let xsList = Map.toAscList xs + mList = fmap (\ (x,y) -> (f x,fmap f y)) xsList in + Gam (Map.fromAscList mList) -> instance Functor Gval where -> fmap f (G g i p) = G (fmap f g) (fmap f i) p + instance Functor Gval where + fmap f (G g i p) = G (fmap f g) (fmap f i) p > instance Functor Global where > fmap f (Fun opts n) = Fun opts $ fmap f n diff --git a/Ivor/PatternDefs.lhs b/Ivor/PatternDefs.lhs --- a/Ivor/PatternDefs.lhs +++ b/Ivor/PatternDefs.lhs @@ -14,10 +14,14 @@ Use the iota schemes from Datatype to represent pattern matching definitions. -> checkDef :: Monad m => Gamma Name -> Name -> Raw -> [PMRaw] -> +Return the definition and its type, as well as any other names which need +to be defined to complete the definition. +Also return whether the function is definitely total. + +> checkDef :: Monad m => Gamma Name -> Name -> Raw -> [PMRaw] -> > Bool -> -- Check for coverage > Bool -> -- Check for well-foundedness -> m (PMFun Name, Indexed Name) +> m (PMFun Name, Indexed Name, [(Name, Indexed Name)], Bool) > checkDef gam fn tyin pats cover wellfounded = 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")]]) @@ -29,9 +33,15 @@ > checkNotExists fn gam > gam' <- gInsert fn (G Undefined ty defplicit) gam > clauses' <- validClauses gam' fn ty clauses' -> pmdef <- matchClauses gam' fn pats tyin cover clauses' -> when wellfounded $ checkWellFounded gam fn [0..arity-1] pmdef -> return (PMFun arity pmdef, ty) +> (pmdef, newdefs, covers) <- matchClauses gam' fn pats tyin cover clauses' +> wf <- if wellfounded then +> do checkWellFounded gam fn [0..arity-1] pmdef +> return True +> else case checkWellFounded gam fn [0..arity-1] pmdef of +> Nothing -> return False +> _ -> return True +> let total = wf && covers +> return (PMFun arity pmdef, ty, newdefs, total) > where checkNotExists n gam = case lookupval n gam of > Just Undefined -> return () > Just _ -> fail $ show n ++ " already defined" @@ -163,12 +173,18 @@ > matchClauses :: Monad m => Gamma Name -> Name -> [PMRaw] -> Raw -> > Bool -> -- Check coverage -> [(Indexed Name, Indexed Name)] -> m [PMDef Name] +> [(Indexed Name, Indexed Name)] -> +> m ([PMDef Name], [(Name, Indexed Name)], Bool) > matchClauses gam fn pats tyin cover gen = do > let raws = zip (map mkRaw pats) (map getRet pats) -> checkpats <- mapM (mytypecheck gam) raws -> when cover $ checkCoverage (map fst checkpats) (map fst gen) -> return $ map (mkScheme gam) checkpats +> (checkpats, newdefs) <- mytypechecks gam raws [] [] +> cv <- if cover then +> do checkCoverage (map fst checkpats) (map fst gen) +> return True +> else case checkCoverage (map fst checkpats) (map fst gen) of +> Nothing -> return False +> _ -> return True +> return $ (map (mkScheme gam) checkpats, newdefs, cv) where mkRaw (RSch pats r) = mkPBind pats tyin r mkPBind [] _ r = r @@ -177,20 +193,26 @@ > where mkRaw (RSch pats r) = mkapp (Var fn) pats > getRet (RSch pats r) = r -> mytypecheck gam (clause, ret) = +> mytypechecks gam [] acc defs = return (reverse acc, defs) +> mytypechecks gam (c:cs) acc defs +> = do (cl, cr, newdefs) <- mytypecheck gam c +> mytypechecks gam cs ((cl,cr):acc) (defs++newdefs) +> mytypecheck gam (clause, ret) = > do (tm@(Ind tmtt), pty, -> rtm@(Ind rtmtt), rty, env) <- +> 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)) +> gam newdefs > let rtmtt' = substNames unified rtmtt > -- checkConvEnv env gam pty rty $ "Pattern error: " ++ show pty ++ " and " ++ show rty ++ " are not convertible " ++ show unify -> let namesret = filter notGlobal $ getNames (Sc rtmtt') +> let namesret = filter (notGlobal gam') $ getNames (Sc rtmtt') > let namesbound = getNames (Sc tmtt) > checkAllBound namesret namesbound (Ind rtmtt') tmtt -> return (tm, Ind rtmtt') -> notGlobal n = case lookupval n gam of -> Nothing -> True -> _ -> False +> return (tm, Ind rtmtt', newdefs) +> notGlobal gam n = case lookupval n gam of +> Nothing -> True +> _ -> False > checkAllBound r b rhs clause = do > let unbound = filter (\y -> not (elem y b)) r > if (length unbound == 0) diff --git a/Ivor/Plugin.lhs b/Ivor/Plugin.lhs --- a/Ivor/Plugin.lhs +++ b/Ivor/Plugin.lhs @@ -16,7 +16,7 @@ > import Ivor.TT > import Ivor.ShellState -> import System.Plugins as Plugins +> -- import System.Plugins as Plugins > import Text.ParserCombinators.Parsec > -- | Load the given plugin file (which should be a full path to a .o or @@ -37,46 +37,49 @@ > Maybe (Parser ViewTerm), > Maybe (ShellState -> IO ShellState), > Maybe (IO [(String, String -> Context -> IO (String, Context))])) -> load fn ctxt = do -> objIn <- compilePlugin fn -> obj <- case objIn of -> Left errs -> fail errs -> Right ok -> return ok -> contextMod <- Plugins.load_ obj [] "plugin_context" -> -- mv <- Plugins.load fn [] ["/Users/edwin/.ghc/i386-darwin-6.6.1/package.conf"] "initialise" -> (mod, contextFn) <- case contextMod of -> LoadFailure msg -> fail $ "Plugin loading failed: " ++ -> show msg -> LoadSuccess mod v -> return (mod, v) -> parserMod <- Plugins.reload mod "plugin_parser" -> parserules <- case parserMod of -> LoadFailure msg -> return Nothing -> LoadSuccess _ v -> return $ Just v -> cmdMod <- Plugins.reload mod "plugin_commands" -> cmds <- case cmdMod of -> LoadFailure msg -> return Nothing -> LoadSuccess _ v -> return $ Just v -> shellMod <- Plugins.reload mod "plugin_shell" -> shellfn <- case shellMod of -> LoadFailure msg -> return Nothing -> LoadSuccess _ v -> return $ Just v -> ctxt' <- case contextFn ctxt of -> Just x -> return x -> Nothing -> fail "Error in running plugin_context" -> return $ (ctxt', parserules, shellfn, cmds) -Make a .o from a .hs, so that we can load Haskell source as well as object -files +> load fn ctxt = fail "Currently disabled" -> compilePlugin :: FilePath -> IO (Either String FilePath) -> compilePlugin hs -> | isExt ".hs" hs || isExt ".lhs" hs = -> do status <- makeAll hs [] -> case status of -> MakeSuccess c out -> return $ Right out -> MakeFailure errs -> return $ Left (concat (map (++"\n") errs)) -> | isExt ".o" hs = return $ Right hs -> | elem '.' hs = return (Left $ "unrecognised file type " ++ hs) -> | otherwise = compilePlugin (hs++".o") -> where isExt ext fn = case span (/='.') fn of -> (file, e) -> ext == e +-- > load fn ctxt = do +-- > objIn <- compilePlugin fn +-- > obj <- case objIn of +-- > Left errs -> fail errs +-- > Right ok -> return ok +-- > contextMod <- Plugins.load_ obj [] "plugin_context" +-- > -- mv <- Plugins.load fn [] ["/Users/edwin/.ghc/i386-darwin-6.6.1/package.conf"] "initialise" +-- > (mod, contextFn) <- case contextMod of +-- > LoadFailure msg -> fail $ "Plugin loading failed: " ++ +-- > show msg +-- > LoadSuccess mod v -> return (mod, v) +-- > parserMod <- Plugins.reload mod "plugin_parser" +-- > parserules <- case parserMod of +-- > LoadFailure msg -> return Nothing +-- > LoadSuccess _ v -> return $ Just v +-- > cmdMod <- Plugins.reload mod "plugin_commands" +-- > cmds <- case cmdMod of +-- > LoadFailure msg -> return Nothing +-- > LoadSuccess _ v -> return $ Just v +-- > shellMod <- Plugins.reload mod "plugin_shell" +-- > shellfn <- case shellMod of +-- > LoadFailure msg -> return Nothing +-- > LoadSuccess _ v -> return $ Just v +-- > ctxt' <- case contextFn ctxt of +-- > Just x -> return x +-- > Nothing -> fail "Error in running plugin_context" +-- > return $ (ctxt', parserules, shellfn, cmds) + +-- Make a .o from a .hs, so that we can load Haskell source as well as object +-- files + +-- > compilePlugin :: FilePath -> IO (Either String FilePath) +-- > compilePlugin hs +-- > | isExt ".hs" hs || isExt ".lhs" hs = +-- > do status <- makeAll hs [] +-- > case status of +-- > MakeSuccess c out -> return $ Right out +-- > MakeFailure errs -> return $ Left (concat (map (++"\n") errs)) +-- > | isExt ".o" hs = return $ Right hs +-- > | elem '.' hs = return (Left $ "unrecognised file type " ++ hs) +-- > | otherwise = compilePlugin (hs++".o") +-- > where isExt ext fn = case span (/='.') fn of +-- > (file, e) -> ext == e diff --git a/Ivor/Prefix.hs b/Ivor/Prefix.hs --- a/Ivor/Prefix.hs +++ b/Ivor/Prefix.hs @@ -1,1 +1,1 @@ -module Ivor.Prefix where prefix = "/usr/local" +module Ivor.Prefix where prefix = "/Users/edwin" diff --git a/Ivor/RunTT.lhs b/Ivor/RunTT.lhs --- a/Ivor/RunTT.lhs +++ b/Ivor/RunTT.lhs @@ -94,7 +94,7 @@ > mkRTElim :: Name -> Int -> SimpleCase -> RunTT > mkRTElim ename arity es = fst $ abstract arity (mkrt es) > where mkrt Impossible = RTCantHappen -> mkrt (IReduce t) = mkRTFun (Gam []) (mkvarnum t) +> 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) diff --git a/Ivor/Scopecheck.lhs b/Ivor/Scopecheck.lhs new file mode 100644 --- /dev/null +++ b/Ivor/Scopecheck.lhs @@ -0,0 +1,52 @@ +> {-# OPTIONS_GHC -fglasgow-exts #-} + +> module Ivor.Scopecheck(scopeCheck) where + +> import Ivor.TTCore +> import Ivor.Nobby +> import Ivor.Typecheck + +Typechecking on terms we assume to be okay - in other words, just convert +bound names to a de Bruijn index. + +> scopeCheck :: Gamma Name -> Env Name -> Raw -> TT Name +> scopeCheck gam = sc where +> sc :: Env Name -> Raw -> TT Name +> sc env (Var n) = +> case lookup n env of +> Just _ -> P n +> Nothing -> case glookup n gam of +> 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) +> sc env (RConst c) = Const c +> sc env (RBind n b scope) = +> let b' = scBinder env b +> sc' = sc ((n,b'):env) scope in +> Bind n b' (pToV n sc') +> sc env RStar = Star +> sc env RInfer = error "Can't fastcheck a term with placeholders" +> sc env t = error $ "Can't fastcheck " ++ show t + +> scBinder :: Env Name -> Binder Raw -> Binder (TT Name) +> scBinder env (B (Let v) t) +> = let v' = sc env v +> t' = sc env t in +> B (Let v') t' +> scBinder env (B Lambda t) +> = let t' = sc env t in +> B Lambda t' +> scBinder env (B Pi t) +> = let t' = sc env t in +> B Pi t' +> scBinder env (B (Guess v) t) +> = error "Can't fastcheck a term with guesses" +> scBinder env (B (Pattern v) t) +> = error "Can't fastcheck a term with patterns" +> scBinder env (B MatchAny t) +> = error "Can't fastcheck a term with patterns" +> scBinder env (B Hole t) +> = error "Can't fastcheck a term with holes" + + diff --git a/Ivor/Shell.lhs b/Ivor/Shell.lhs --- a/Ivor/Shell.lhs +++ b/Ivor/Shell.lhs @@ -104,8 +104,9 @@ > ctxt <- addTypedDef (context st) (name nm) tm ty > return st { context = ctxt } > runCommand (PatternDef nm ty pats opts) st = do -> ctxt <- addPatternDef (context st) (name nm) ty pats opts -> return st { context = ctxt } +> (ctxt, new) <- addPatternDef (context st) (name nm) ty pats (Holey:opts) +> let st' = respondLn st $ ("Need to define: " ++ show new) +> return st' { context = ctxt } > runCommand (Data dat) st = do ctxt <- addData (context st) dat > return st { context = ctxt } > runCommand (Axiom nm tm) st = do ctxt <- addAxiom (context st) (name nm) tm @@ -149,7 +150,7 @@ > case (getDef (context st) (name n)) of > Just tm -> return (respondLn st (show (view tm))) > _ -> case (getPatternDef (context st) (name n)) of -> Just pats -> return (respondLn st (printPats pats)) +> Just (_,pats) -> return (respondLn st (printPats pats)) > _ -> do tm <- check (context st) n > case view tm of > (Name TypeCon _) -> return (respondLn st "Type constructor") @@ -174,7 +175,7 @@ > runCommand (Focus n) st = do ctxt <- focus (goal n) (context st) > return st { context = ctxt } > runCommand (Dump n) st = do -> let ds = getAllDefs (context st) +> let ds = getAllTypes (context st) > return (respondLn st (dumpAll n ds)) > runCommand (ReplData eq repl sym) st > = return st { repldata = Just (eq, repl, sym) } diff --git a/Ivor/State.lhs b/Ivor/State.lhs --- a/Ivor/State.lhs +++ b/Ivor/State.lhs @@ -33,10 +33,6 @@ > -- (with type) > eliminators :: [(Name, (Indexed Name, > ([RawScheme], PMFun Name)))], -> -- Supercombinators for each definition -> runtt :: SCs, -> -- Bytecode for each definitions -> bcdefs :: ByteDef, > -- List of holes to be solved in proof state > holequeue :: ![Name], > -- Premises we're not interested in, so don't show @@ -53,7 +49,7 @@ > undoState :: !(Maybe IState) > } -> initstate = ISt (Gam []) [] [] [] [] [] [] Nothing [] mknames "" Nothing +> initstate = ISt (emptyGam) [] [] [] [] Nothing [] mknames "" Nothing > where mknames = [MN ("myName",x) | x <- [1..]] > respond :: IState -> String -> IState @@ -76,48 +72,54 @@ Take a data type definition and add constructors and elim rule to the context. -> doData :: Monad m => IState -> Name -> RawDatatype -> m IState -> doData st n r = do +> doData :: Monad m => Bool -> IState -> Name -> RawDatatype -> m IState +> doData elim st n r = do > let ctxt = defs st -> let runtts = runtt st -> let bcs = bcdefs st -> dt <- checkType (defs st) r -- Make iota schemes +> dt <- if elim then checkType (defs st) r -- Make iota schemes +> else checkTypeNoElim (defs st) r > ctxt <- gInsert (fst (tycon dt)) (snd (tycon dt)) ctxt > -- let ctxt' = (tycon dt):ctxt > ctxt <- addCons (datacons dt) ctxt -> (ctxt, newruntts, newbc) <- -> addElim ctxt runtts bcs (erule dt) (e_ischemes dt) -> (newdefs, newruntts, newbc) <- -> addElim ctxt newruntts newbc (crule dt) (c_ischemes dt) -> let newelims = (fst (erule dt), (snd (erule dt), -> (e_rawschemes dt, e_ischemes dt))): +> case e_ischemes dt of +> Just eischemes -> +> -- We've done elim rules +> do let (Just cischemes) = c_ischemes dt +> ctxt <- +> addElim ctxt (erule dt) eischemes +> newdefs <- +> addElim ctxt (crule dt) cischemes +> let newelims = (fst (erule dt), (snd (erule dt), +> (e_rawschemes dt, eischemes))): > (fst (crule dt), (snd (crule dt), -> (c_rawschemes dt, c_ischemes dt))): +> (c_rawschemes dt, cischemes))): > eliminators st -> let newdatadefs = (n,dt):(datadefs st) -> return $ st { defs = newdefs, datadefs = newdatadefs, -> eliminators = newelims, -> bcdefs = newbc, runtt = newruntts } +> let newdatadefs = (n,dt):(datadefs st) +> return $ st { defs = newdefs, datadefs = newdatadefs, +> eliminators = newelims +> } +> Nothing -> -- no elim rules +> return $ st { defs = ctxt, +> datadefs = (n,dt):(datadefs st) } > where addCons [] ctxt = return ctxt > addCons ((n,gl):xs) ctxt = do > ctxt <- addCons xs ctxt > gInsert n gl ctxt -> addElim ctxt runtts bcdefs erule schemes = do +> addElim ctxt erule schemes = do > newdefs <- gInsert (fst erule) -> (G (PatternDef schemes) (snd erule) defplicit) +> (G (PatternDef schemes True) (snd erule) defplicit) > ctxt -> return (newdefs, runtts, bcdefs) +> return newdefs -> doMkData :: Monad m => IState -> Datadecl -> m IState -> doMkData st (Datadecl n ps rawty cs) +> doMkData :: Monad m => Bool -> IState -> Datadecl -> m IState +> doMkData elim st (Datadecl n ps rawty cs) > = do (gty,_) <- checkIndices (defs st) ps [] rawty > let ty = forget (normalise (defs st) gty) > -- TMP HACK: Do it twice, to fill in _ placeholders. > rd1 <- mkRawData n ps ty cs -> dt1 <- checkType (defs st) rd1 +> dt1 <- checkTypeNoElim (defs st) rd1 > let csfilled = map (forgetcon (length ps)) (datacons dt1) > rd <- mkRawData n ps ty csfilled -> doData st n rd +> doData elim st n rd > where checkIndices gam [] env rawty = check gam env rawty Nothing > checkIndices gam ((n,nrawty):xs) env rawty = do > (Ind nty,_) <- check gam env nrawty Nothing @@ -130,10 +132,10 @@ > suspendProof :: Monad m => IState -> m IState > suspendProof st = do case proofstate st of > (Just prf) -> do -> let (Gam olddefs) = defs st +> let olddefs = defs st > newdef <- suspendFrom (defs st) prf (holequeue st) > return $ st { proofstate = Nothing, -> defs = Gam (newdef:olddefs), +> defs = extend olddefs newdef, > holequeue = [] > } > _ -> fail "No proof in progress" diff --git a/Ivor/TT.lhs b/Ivor/TT.lhs --- a/Ivor/TT.lhs +++ b/Ivor/TT.lhs @@ -13,27 +13,31 @@ > module Ivor.TT(-- * System state > emptyContext, Context, -> Ivor.TT.check, +> Ivor.TT.check,fastCheck, > checkCtxt,converts, > Ivor.TT.compile, > -- * Exported view of terms > module VTerm, IsTerm, IsData, > -- * Definitions and Theorems -> addDef,addTypedDef,addData,addAxiom,declare,declareData, +> addDef,addTypedDef,addData,addDataNoElim, +> addAxiom,declare,declareData, > theorem,interactive, > addPrimitive,addBinOp,addBinFn,addPrimFn,addExternalFn, > addEquality,forgetDef,addGenRec,addImplicit, > -- * Pattern matching definitions > PClause(..), Patterns(..),PattOpt(..),addPatternDef, +> toPattern, > -- * Manipulating Proof State > proving,numUnsolved,suspend,resume, > save, restore, clearSaved, > proofterm, getGoals, getGoal, uniqueName, -- getActions > allSolved,qed, > -- * Examining the Context -> eval, whnf, evalCtxt, getDef, defined, getPatternDef, -> getAllDefs, getConstructors, -> Rule(..), getElimRule, +> eval, whnf, evalnew, evalCtxt, getDef, defined, getPatternDef, +> getAllTypes, getAllDefs, getAllPatternDefs, getConstructors, +> getInductive, getAllInductives, getType, +> Rule(..), getElimRule, nameType, getConstructorTag, +> getConstructorArity, > Ivor.TT.freeze,Ivor.TT.thaw, > -- * Goals, tactic types > Goal,goal,defaultGoal, @@ -92,6 +96,7 @@ > import Ivor.TTCore as TTCore > import Ivor.State > import Ivor.Typecheck +> import Ivor.Scopecheck > import Ivor.Gadgets > import Ivor.Nobby > import Ivor.Evaluator @@ -109,6 +114,7 @@ > import Data.List > import Debug.Trace > import Data.Typeable +> import Control.Monad(when) > -- | Abstract type representing state of the system. > newtype Context = Ctxt IState @@ -142,7 +148,13 @@ > raw :: Monad m => a -> m Raw > class IsData a where +> -- Add a data type with case and elim rules an elimination rule > addData :: Monad m => Context -> a -> m Context +> addData ctxt x = addData' True ctxt x +> -- Add a data type without an elimination rule +> addDataNoElim :: Monad m => Context -> a -> m Context +> addDataNoElim ctxt x = addData' False ctxt x +> addData' :: Monad m => Bool -> Context -> a -> m Context > instance IsTerm Term where > check _ tm = return tm @@ -167,17 +179,27 @@ > (Failure err) -> fail err > raw t = return t +> -- | 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 +> -- able to run it. This is useful if you simply want to do a substitution +> -- into a 'ViewTerm'. + +> fastCheck :: Context -> ViewTerm -> Term +> fastCheck (Ctxt st) vt = Term (Ind (scopeCheck (defs st) [] (forget vt)), +> (Ind TTCore.Star)) + > -- | Parse and typecheck a data declaration, of the form > -- "x:Type = c1:Type | ... | cn:Type" > instance IsData String where -> addData (Ctxt st) str = do +> addData' elim (Ctxt st) str = do > case (parseDataString str) of -> Success ind -> addData (Ctxt st) ind +> Success ind -> addData' elim (Ctxt st) ind > Failure err -> fail err > instance IsData Inductive where -> addData (Ctxt st) ind = do st' <- doMkData st (datadecl ind) -> return (Ctxt st') +> addData' elim (Ctxt st) ind = do st' <- doMkData elim st (datadecl ind) +> return (Ctxt st') > where > datadecl (Inductive n ps inds cty cons) = > Datadecl n (map (\ (n,ty) -> (n, forget ty)) ps) @@ -205,27 +227,62 @@ > mkRawClause (PClause args ret) = > RSch (map forget args) (forget ret) + +> -- ^ Convert a term to matchable pattern form; i.e. the only names allowed +> -- are variables and constructors. Any arbitrary function application is +> -- removed. + +> toPattern :: Context -> ViewTerm -> ViewTerm +> toPattern (Ctxt ctxt) tm = toPat (defs ctxt) tm where +> toPat gam c@(Name _ n) | matchable gam n = c +> | otherwise = Placeholder +> toPat gam (VTerm.App f a) = case toPat gam f of +> Placeholder -> Placeholder +> apptm -> VTerm.App f (toPat gam a) +> toPat gam _ = Placeholder +> matchable gam n +> = case lookupval n gam of +> Just (DCon _ _) -> True -- since it's a constructor +> Nothing -> True -- since it' a variable +> _ -> False +> + > 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. > deriving Eq > -- |Add a new definition to the global state. > -- By default, these definitions must cover all cases and be well-founded, -> -- but can be optionally partial or general recursive +> -- but can be optionally partial or general recursive. +> -- Returns the new context, and a list of names which need to be defined +> -- to complete the definition. > addPatternDef :: (IsTerm ty, Monad m) => > Context -> Name -> ty -- ^ Type > -> Patterns -- ^ Definition > -> [PattOpt] -- ^ Options to set which definitions will be accepted -> -> m Context +> -> m (Context, [(Name, ViewTerm)]) > addPatternDef (Ctxt st) n ty pats opts = do > checkNotExists n (defs st) +> let ndefs = defs st > inty <- raw ty > let (Patterns clauses) = pats -> (pmdef, fty) <- checkDef (defs st) n inty (map mkRawClause clauses) +> (pmdef, fty, newnames, tot) +> <- checkDef ndefs n inty (map mkRawClause clauses) > (not (elem Ivor.TT.Partial opts)) > (not (elem GenRec opts)) -> newdefs <- gInsert n (G (PatternDef pmdef) fty defplicit) (defs st) -> return $ Ctxt st { defs = newdefs } +> (ndefs',vnewnames) +> <- if (null newnames) then return (ndefs, []) +> else do when (not (Holey `elem` opts)) $ +> fail "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)) +> ndefs newnames +> return (ngam, vnew) +> newdefs <- gInsert n (G (PatternDef pmdef tot) fty defplicit) ndefs' +> return (Ctxt st { defs = newdefs }, vnewnames) > -- |Add a new definition, with its type to the global state. > -- These definitions can be recursive, so use with care. @@ -235,22 +292,17 @@ > checkNotExists n (defs st) > (Term (inty,_)) <- Ivor.TT.check (Ctxt st) ty > (Ctxt tmpctxt) <- declare (Ctxt st) n ty -> let Gam tmp = defs tmpctxt -> let Gam ctxt = defs st -> let runtts = runtt st +> let tmp = defs tmpctxt +> let ctxt = defs st > term <- raw tm -> case (checkAndBind (Gam tmp) [] term (Just inty)) of +> case (checkAndBind tmp [] term (Just inty)) of > (Success (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) (Gam ctxt) +> newdefs <- gInsert n (G (Fun [Recursive] v) t defplicit) ctxt > -- = Gam ((n,G (Fun [] v) t):ctxt) -> let scs = lift n (levelise (normalise (Gam []) v)) -> let bc = compileAll (runtts++scs) scs -> let newbc = bc++(bcdefs st) -> return $ Ctxt st { defs = newdefs, bcdefs = newbc, -> runtt = (runtts++scs) }) +> return $ Ctxt st { defs = newdefs }) > else (fail $ "The given type and inferred type do not match, inferred " ++ show t) > (Failure err) -> fail err @@ -260,18 +312,13 @@ > addDef (Ctxt st) n tm = do > checkNotExists n (defs st) > v <- raw tm -> let Gam ctxt = defs st -> let runtts = runtt st -> case (typecheck (Gam ctxt) v) of +> let ctxt = defs st +> case (typecheck ctxt v) of > (Success (v,t@(Ind sc))) -> do > checkBound (getNames (Sc sc)) t -> newdefs <- gInsert n (G (Fun [] v) t defplicit) (Gam ctxt) +> newdefs <- gInsert n (G (Fun [] v) t defplicit) ctxt > -- let newdefs = Gam ((n,G (Fun [] v) t):ctxt) -> let scs = lift n (levelise (normalise (Gam []) v)) -> let bc = compileAll (runtts++scs) scs -> let newbc = bc++(bcdefs st) -> return $ Ctxt st { defs = newdefs, bcdefs = newbc, -> runtt = (runtts++scs) } +> return $ Ctxt st { defs = newdefs } > (Failure err) -> fail err > checkBound :: Monad m => [Name] -> (Indexed Name) -> m () @@ -282,13 +329,15 @@ > -- |Forget a definition and all following definitions. > forgetDef :: Monad m => Context -> Name -> m Context -> forgetDef (Ctxt st) n = do let (Gam olddefs) = defs st -> newdefs <- f olddefs n -> return $ Ctxt st { defs = Gam newdefs } -> where f [] n = fail "No such name" -> f (def@(x,_):xs) n | x == n = return xs -> | otherwise = f xs n +> forgetDef (Ctxt st) n = fail "Not any more..." +do let olddefs = defs st + newdefs <- f olddefs n + return $ Ctxt st { defs = newdefs + where f [] n = fail "No such name" + f (def@(x,_):xs) n | x == n = return xs + | otherwise = f xs n + > -- |Add the general recursion elimination rule, thus making all further > -- definitions untrustworthy :). > addGenRec :: Monad m => Context -> Name -- ^ Name to give recursion rule @@ -297,20 +346,16 @@ > = do checkNotExists n (defs st) > (Ctxt tmpctxt) <- addAxiom (Ctxt st) n > "(P:*)(meth_general:(p:P)P)P" -> let Gam tmp = defs tmpctxt -> let Gam ctxt = defs st -> let runtts = runtt st -> general <- raw $ "[P:*][meth_general:(p:P)P](meth_general (" ++ +> let tmp = defs tmpctxt +> let ctxt = defs st +> general <- raw $ "[P:*][meth_general:(p:P)P](meth_general (" ++ > show n ++ " P meth_general))" -> case (typecheck (Gam tmp) general) of +> case (typecheck tmp general) of > (Success (v,t)) -> do > -- let newdefs = Gam ((n,G (Fun [] v) t):ctxt) -> newdefs <- gInsert n (G (Fun [] v) t defplicit) (Gam ctxt) -> let scs = lift n (levelise (normalise (Gam []) v)) -> let bc = compileAll (runtts++scs) scs -> let newbc = bc++(bcdefs st) -> return $ Ctxt st { defs = newdefs, bcdefs = newbc, -> runtt = (runtts++scs) } +> newdefs <- gInsert n (G (Fun [] v) t defplicit) ctxt +> let scs = lift n (levelise (normalise (emptyGam) v)) +> return $ Ctxt st { defs = newdefs } > (Failure err) -> fail $ "Can't happen (general): "++err > -- | Add the heterogenous (\"John Major\") equality rule and its reduction @@ -326,7 +371,7 @@ > rcrule <- eqElimType (show ty) (show con) "Case" > rischeme <- eqElimSch (show con) > let rdata = (RData rtycon [rdatacon] 2 rerule rcrule [rischeme] [rischeme]) -> st <- doData st ty rdata +> st <- doData True st ty rdata > return $ Ctxt st > -- eqElim : (A:*)(a:A)(b:A)(q:JMEq A A a a) @@ -443,7 +488,7 @@ > Just x' -> case cast y of > Just y' -> case Ivor.TT.check (Ctxt st) $ f x' y' of > Just (Term (Ind v,_)) -> -> Just $ nf (Gam []) (VG []) [] False v +> Just $ nf (emptyGam) (VG []) [] False v > Nothing -> Nothing > Nothing -> Nothing > mkfun _ = Nothing @@ -468,16 +513,16 @@ > checkNotExists n (defs st) > Term (ty, _) <- Ivor.TT.check (Ctxt st) tyin > let fndef = PrimOp mkfun mktt -> let Gam ctxt = defs st +> let ctxt = defs st > -- let newdefs = Gam ((n,(G fndef ty)):ctxt) -> newdefs <- gInsert n (G fndef ty defplicit) (Gam ctxt) +> newdefs <- gInsert n (G fndef ty defplicit) ctxt > return $ Ctxt st { defs = newdefs } > 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 (Term (Ind v,_)) -> -> Just $ nf (Gam []) (VG []) [] False v +> Just $ nf (emptyGam) (VG []) [] False v > Nothing -> Nothing > Nothing -> Nothing > mkfun _ = Nothing @@ -502,9 +547,9 @@ > checkNotExists n (defs st) > Term (ty, _) <- Ivor.TT.check (Ctxt st) tyin > let fndef = PrimOp mkfun mktt -> let Gam ctxt = defs st +> let ctxt = defs st > -- let newdefs = Gam ((n,(G fndef ty)):ctxt) -> newdefs <- gInsert n (G fndef ty defplicit) (Gam ctxt) +> newdefs <- gInsert n (G fndef ty defplicit) ctxt > return $ Ctxt st { defs = newdefs } > where mkfun :: Spine Value -> Maybe Value > mkfun sx | xs <- listify sx @@ -514,7 +559,7 @@ > case (Ivor.TT.check (Ctxt st) res) of > Nothing -> Nothing > Just (Term (Ind tm, _)) -> -> Just $ nf (Gam []) (VG []) [] False tm +> Just $ nf (emptyGam) (VG []) [] False tm > Nothing -> Nothing > mktt :: [TT Name] -> Maybe (TT Name) > mktt xs @@ -607,6 +652,9 @@ > Just (Unreducible,ty) -> > do let st' = st { defs = remove n (defs st) } > theorem (Ctxt st') n (Term (ty, Ind TTCore.Star)) +> 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" > -- | Freeze a name (i.e., set it so that it does not reduce) @@ -655,7 +703,7 @@ return $ Term (tm, ty) Failure err -> fail err -> -- |Normalise a term and its type +> -- |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) @@ -665,6 +713,11 @@ > 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 (eval_nf (defs st) tm, +> eval_nf (defs st) ty) + > -- |Check a term in the context of the given goal > checkCtxt :: (IsTerm a, Monad m) => Context -> Goal -> a -> m Term > checkCtxt (Ctxt st) goal tm = @@ -731,40 +784,116 @@ > Just ((Fun _ tm),ty) -> return $ Term (tm,ty) > _ -> fail "Not a function name" +> -- |Get the type of a definition in the context. +> getType :: Monad m => Context -> Name -> m Term +> getType (Ctxt st) n = case glookup n (defs st) of +> Just (_,ty) -> return $ Term (ty,Ind TTCore.Star) +> _ -> fail "Not a defined name" + > -- |Check whether a name is defined > defined :: Context -> Name -> Bool > defined (Ctxt st) n = case glookup n (defs st) of > Just _ -> True > _ -> False -> -- |Lookup a pattern matching definition in the context. -> getPatternDef :: Monad m => Context -> Name -> m Patterns +> -- | Return the data type with the given name. Note that this knows nothing +> -- about the difference between parameters and indices; that information +> -- is discarded after the elimination rule is constructed. +> getInductive :: Monad m => Context -> Name -> m Inductive +> getInductive (Ctxt st) n +> = case glookup n (defs st) of +> Just (TCon _ (Elims _ _ cons), ty) -> +> -- reconstruct the 'Inductive' from types of ty and cons +> return (Inductive n [] (getIndices (view (Term (ty, Ind TTCore.Star)))) +> (getTyType (view (Term (ty, Ind TTCore.Star)))) +> (getConTypes cons)) +> _ -> fail "Not an inductive family" +> where getIndices v = getArgTypes v +> getTyType v = VTerm.getReturnType v +> getConTypes [] = [] +> getConTypes (c:cs) = case getType (Ctxt st) c of +> Just ty -> (c,view ty):(getConTypes cs) + +> -- |Lookup a pattern matching definition in the context. Return the +> -- type and the pattern definition. +> getPatternDef :: Monad m => Context -> Name -> m (ViewTerm, Patterns) > getPatternDef (Ctxt st) n > = case glookup n (defs st) of -> Just ((PatternDef pmf),ty) -> -> return $ Patterns (map mkPat (getPats pmf)) -> Nothing -> fail "Not a pattern matching definition" +> 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" > where getPats (PMFun _ ps) = ps > mkPat (Sch ps ret) = PClause (map viewPat ps) (view (Term (ret, (Ind TTCore.Star)))) -> -> viewPat (PVar n) = Name Bound (name (show n)) +> 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 (PConst c) = Constant c > viewPat _ = Placeholder > -- |Get all the names and types in the context -> getAllDefs :: Context -> [(Name,Term)] -> getAllDefs (Ctxt st) = let (Gam ds) = defs st in -> reverse (map info ds) -- input order! +> getAllTypes :: Context -> [(Name,Term)] +> getAllTypes (Ctxt st) = let ds = getAList (defs st) in +> reverse (map info ds) -- input order! > where info (n,G _ ty _) = (n, Term (ty, Ind TTCore.Star)) -> -- | Get the names of all of the constructors of an inductive family +> -- |Get all the pattern matching definitions in the context. +> -- Also returns CAFs (i.e. 0 argument functions) +> getAllPatternDefs :: Context -> [(Name,(ViewTerm, Patterns))] +> getAllPatternDefs ctxt +> = getPD (map fst (getAllTypes ctxt)) +> where getPD [] = [] +> getPD (x:xs) = case (getPatternDef ctxt x) of +> Just d -> (x,d):(getPD xs) +> _ -> getPD xs + +> -- |Get all the inductive type definitions in the context. +> getAllInductives :: Context -> [(Name,Inductive)] +> getAllInductives ctxt +> = getI (map fst (getAllTypes ctxt)) +> where getI [] = [] +> getI (x:xs) = case (getInductive ctxt x) of +> Just d -> (x,d):(getI xs) +> _ -> getI xs + +> getAllDefs :: Context -> [(Name, Term)] +> getAllDefs ctxt = let names = map fst (getAllTypes ctxt) in +> map (\ x -> (x, unJust (getDef ctxt x))) names + +> -- |Get the names of all of the constructors of an inductive family > getConstructors :: Monad m => Context -> Name -> m [Name] > getConstructors (Ctxt st) n > = case glookup n (defs st) of > Just ((TCon _ (Elims _ _ cs)),ty) -> return cs > _ -> fail "Not a type constructor" +> -- |Find out what type of variable the given name is +> nameType :: Monad m => Context -> Name -> m NameType +> nameType (Ctxt st) n +> = case glookup n (defs st) of +> Just ((DCon _ _), _) -> return DataCon +> Just ((TCon _ _), _) -> return TypeCon +> Just _ -> return Bound -- any function +> Nothing -> fail "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 :: Monad m => Context -> Name -> m Int +> getConstructorTag (Ctxt st) n +> = case glookup n (defs st) of +> Just ((DCon tag _), _) -> return tag +> _ -> fail "Not a constructor" + +> -- | Get the arity of the given constructor. +> getConstructorArity :: Monad m => Context -> Name -> m Int +> getConstructorArity (Ctxt st) n +> = case glookup n (defs st) of +> Just ((DCon _ _), Ind ty) -> return (length (getExpected ty)) +> _ -> fail "Not a constructor" + Examine pattern matching elimination rules > -- | Types of elimination rule @@ -839,8 +968,8 @@ > Just x -> return x > Nothing -> fail "No such goal" -> getHoleTerm gam hs tm = (getctxt hs, -> Term (normaliseEnv hs (Gam []) (binderType tm), +> getHoleTerm gam hs tm = (getctxt hs, +> Term (normaliseEnv hs (emptyGam) (binderType tm), > Ind TTCore.Star)) > where getctxt [] = [] > getctxt ((n,B _ ty):xs) = (n,Term (Ind ty,Ind TTCore.Star)): @@ -928,15 +1057,9 @@ > qedLift (defs st) False prf > let isrec = rec name > let (Gam olddefs) = remove name (defs st) -> let runtts = runtt st -> let scs = lift name (levelise (normalise (Gam []) ind)) -> let bc = compileAll (runtts++scs) scs -> let newbc = bc++(bcdefs st) > defs' <- gInsert name val (defs st) > let newdefs = setRec name isrec defs' -> return $ Ctxt st { proofstate = Nothing, -> bcdefs = newbc, -> runtt = runtts ++ scs, +> return $ Ctxt st { proofstate = Nothing, > defs = newdefs } -- Gam (newdef:olddefs) } > Nothing -> fail "No proof in progress" > where rec nm = case lookupval nm (defs st) of @@ -947,7 +1070,7 @@ > m (Name, Gval Name) > qedLift gam freeze > (Ind (Bind x (B (TTCore.Let v) ty) (Sc (P n)))) | n == x = -> do let (Ind vnorm) = convNormalise (Gam []) (finalise (Ind v)) +> do let (Ind vnorm) = convNormalise (emptyGam) (finalise (Ind v)) > verify gam (Ind v) > return $ (x, G (Fun opts (Ind vnorm)) (finalise (Ind ty)) defplicit) > where opts = if freeze then [Frozen] else [] @@ -1064,9 +1187,9 @@ > addgoals ((Tactics.NextGoal n):xs) st > = addgoals xs (st { holequeue = nub (second n (holequeue st)) }) > addgoals ((Tactics.AddAxiom n ty):xs) st -> = let Gam ctxt = defs st in +> = let ctxt = defs st in > addgoals xs (st -> { defs = Gam ((n,G Unreducible (finalise (Ind ty)) defplicit):ctxt) }) +> { defs = extend ctxt (n,G Unreducible (finalise (Ind ty)) defplicit) }) > addgoals ((Tactics.HideGoal n):xs) st > = addgoals xs (st { hidden = nub (n:(hidden st)) }) > addgoals (_:xs) st = addgoals xs st @@ -1186,7 +1309,7 @@ > -- | Introduce an assumption (i.e. a lambda binding) > intro :: Tactic -> intro = runTac (Tactics.intro) +> intro = (runTac Tactics.rename_user) >-> (runTac (Tactics.intro)) > -- | Introduce an assumption (i.e. a lambda binding) > introName :: Name -- ^ Name for the assumption @@ -1432,10 +1555,6 @@ > -> String -- ^ root of filenames to generate > -> IO () > compile (Ctxt st) froot -> = do let hd = mkHeaders (bcdefs st) -> let ev = mkEval (bcdefs st) -> let cd = mkCode (bcdefs st) -> Compiler.compile st froot -> -- writeFile (froot++".c") $ hd ++ ev ++ cd +> = fail "No compiler at the minute" diff --git a/Ivor/TTCore.lhs b/Ivor/TTCore.lhs --- a/Ivor/TTCore.lhs +++ b/Ivor/TTCore.lhs @@ -45,6 +45,7 @@ > | V Int > | Con Int n Int -- Tag, name and arity > | TyCon n Int -- Name and arity +> | Meta n (TT n) -- Metavariable and its type > | Elim n > | App (TT n) (TT n) > | Bind n (Binder (TT n)) (Scope (TT n)) @@ -140,14 +141,24 @@ > data Name > = UN String > | MN (String,Int) -> deriving Eq +> deriving (Ord, Eq) Data declarations and pattern matching -> data RawScheme = RSch [Raw] Raw + data RawWith = RWith [Raw] + | RWPatt [Raw] + | RWNone + deriving Show + + data With = With [Indexed n] + | WPatt [Pattern n] + | WNone + deriving Show + +> data RawScheme = RSch [Raw] {- RawWith -} Raw > deriving Show -> data Scheme n = Sch [Pattern n] (Indexed n) +> data Scheme n = Sch [Pattern n] {- With -} (Indexed n) > deriving Show > type PMRaw = RawScheme @@ -188,6 +199,7 @@ > fmap f (V i) = V i > fmap f (Con t x i) = Con t (f x) i > fmap f (TyCon x i) = TyCon (f x) i +> fmap f (Meta x t) = Meta (f x) (fmap f t) > fmap f (Elim x) = Elim (f x) > fmap f (App tf a) = App (fmap f tf) (fmap f a) > fmap f (Bind n b sc) = Bind (f n) (fmap (fmap f) b) (fmap (fmap f) sc) @@ -274,6 +286,7 @@ > where > v' (P n) = f n > v' (V i) = V i +> v' (Meta n t) = Meta n (v' t) > v' (App f' a) = (App (v' f') (v' a)) > v' (Bind n b (Sc sc)) = (Bind n (fmap (v') b) > (Sc (v' sc))) @@ -291,12 +304,14 @@ > makePs :: TT Name -> TT Name > makePs t = let t' = evalState (uniqifyAllState t) [] in -> vapp (\ (ctx,i) -> P (traceIndex ctx i "makePsEnv")) t' +> vapp (\ (ctx,i) -> P (traceIndex ctx i ("makePs " ++ +> debugTT t))) t' > --if (i -- else V i) t' > makePsEnv env t = let t' = evalState (uniqifyAllState t) env in -> vapp (\ (ctx,i) -> P (traceIndex ctx i "makePsEnv")) t' +> vapp (\ (ctx,i) -> P (traceIndex ctx i +> ("makePsEnv" ++ debugTT t))) t' > uniqifyAllState :: TT Name -> State [Name] (TT Name) @@ -434,14 +449,41 @@ > vinc (V n) = V (n+1) -- So that we weakenv it correctly > vinc x = x +Traverse a term looking for metavariables. Replace them with concrete +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 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) +> return (P n) +> ums (Bind n (B b ty) (Sc sc)) +> = do b' <- umsB b +> ty' <- ums ty +> sc' <- ums sc +> return (Bind n (B b' ty') (Sc sc')) +> ums x = return x +> umsB (Let v) = do v' <- ums v +> return (Let v') +> umsB (Guess v) = do v' <- ums v +> return (Guess v') +> umsB (Pattern v) = do v' <- ums v +> return (Pattern v') +> umsB x = return x + Return all the names used in a scope -> getNames :: Eq n => Scope (TT n) -> [n] +> getNames :: (Show n, Eq n) => Scope (TT n) -> [n] > getNames (Sc x) = nub $ p' x where > p' (P x) = [x] > p' (App f' a) = (p' f')++(p' a) > p' (Bind n b (Sc sc)) -> | scnames <- p' sc = (scnames \\ [n]) ++ pb' b +> | scnames <- p' sc = ((nub scnames) \\ [n]) ++ pb' b > p' (Proj _ i x) = p' x > p' (Label t (Comp n cs)) = p' t ++ concat (map p' cs) > p' (Call (Comp n cs) t) = concat (map p' cs) ++ p' t @@ -614,6 +656,7 @@ > (==) (V i) (V j) = i==j > (==) (Con t x i) (Con t' y j) = x==y > (==) (TyCon x i) (TyCon y j) = x==y +> (==) (Meta x t) (Meta y t') = x==y && t==t' > (==) (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' @@ -712,6 +755,7 @@ > forgetTT (V i) = RAnnot $ "v" ++ (show i) > forgetTT (Con t x i) = Var $ UN (show x) > forgetTT (TyCon x i) = Var $ UN (show x) +> forgetTT (Meta n i) = RMeta (UN (show n ++ " : " ++ show i)) > forgetTT (Elim x) = Var $ UN (show x) > forgetTT (App f a) = RApp (forgetTT f) (forgetTT a) > forgetTT (Bind n (B Lambda t) (Sc sc)) = @@ -798,6 +842,7 @@ > forgetTT (V i) = RAnnot $ "v" ++ (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)) > forgetTT (Elim x) = Var $ UN (show x) > forgetTT (App f a) = RApp (forgetTT f) (forgetTT a) > forgetTT (Bind n (B Lambda t) (Sc sc)) = diff --git a/Ivor/Tactics.lhs b/Ivor/Tactics.lhs --- a/Ivor/Tactics.lhs +++ b/Ivor/Tactics.lhs @@ -231,13 +231,13 @@ > checkAndBind gam (ptovenv env) guess (Just (Ind tyin)) > let gv = makePsEnv (map fst env) gvin > let gt = makePsEnv (map fst env) gtin -> let (Ind ty') = normaliseEnv (ptovenv env) (Gam []) (Ind tyin) +> let (Ind ty') = normaliseEnv (ptovenv env) (emptyGam) (Ind tyin) > let (Ind ty) = normaliseEnv (ptovenv env) gam (Ind tyin) > let fgt = finalise (Ind gt) > let fty' = finalise (Ind ty') > let fty = finalise (Ind ty) > others <- -- trace ("unifying "++show gt++" and "++show ty') $ -> case unifyenv (Gam []) (ptovenv env) fgt fty' of +> case unifyenv (emptyGam) (ptovenv env) fgt fty' of > Nothing -> unifyenv gam (ptovenv env) fgt fty > (Just x) -> return x > -- let newgt = substNames others gt @@ -397,7 +397,7 @@ > betaReduce :: Tactic > betaReduce gam env (Ind (Bind x (B Hole ty) sc)) = -> do let (Ind nty) = normaliseEnv (ptovenv env) (Gam []) (finalise (Ind ty)) +> 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" @@ -409,8 +409,8 @@ > do case glookup fn gam of > Nothing -> fail $ "Unknown name " ++ show fn > Just (v,t) -> do -> let (Ind nty) = normaliseEnv (ptovenv env) -> (Gam [(fn,G v t defplicit)]) +> 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" @@ -515,7 +515,9 @@ > rename :: Name -> Tactic > rename n gam env (Ind (Bind x (B Hole rnin) sc)) -> = do renamed <- doRename n rnin +> -- better make sure we haven't used it already +> = do let n' = uniqify n (map fst env) +> renamed <- doRename n' rnin > 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))) @@ -523,18 +525,37 @@ > rename _ _ _ (Ind (Bind x _ _)) = fail $ "rename: " ++ show x ++ " Not a hole" > rename _ _ _ _ = fail "rename: Not a binder, can't happen" +Make sure the binder has a user accessible name + +> rename_user :: Tactic +> rename_user gam env (Ind (Bind x (B Hole rnin) sc)) +> -- better make sure we haven't used it already +> = do renamed <- doRename rnin +> tacret $ Ind (Bind x (B Hole renamed) sc) +> 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" +> 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" + Introduce a lambda or let > intro :: Tactic > intro gam env intm@(Ind (Bind x (B Hole tyin) (Sc p))) > | p == (P x) = -> do let (Ind ty) = normaliseEnv (ptovenv env) (Gam []) (finalise (Ind tyin)) +> do let (Ind ty) = normaliseEnv (ptovenv env) (emptyGam) (finalise (Ind tyin)) > let ty' = makePsEnv (map fst env) ty -> introsty (uniqify x (map fst env)) ty' (Sc p) +> 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." +> sensible (MN _) = (UN "X") -- don't use machine names +> sensible x = x + > introsty x (Bind y (B Pi s) (Sc t)) xscope = > 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 = @@ -570,7 +591,7 @@ > generalise :: Raw -> Tactic > generalise expr gam env (Ind (Bind x (B Hole tyin) sc)) = > do (nv, nt) <- check gam (ptovenv env) expr Nothing -> let (Ind ntyin) = normaliseEnv (ptovenv env) (Gam []) (finalise (Ind tyin)) +> let (Ind ntyin) = normaliseEnv (ptovenv env) (emptyGam) (finalise (Ind tyin)) > let (Ind exprv) = normaliseEnv (ptovenv env) gam nv > let (Ind exprt) = normaliseEnv (ptovenv env) gam nt > let ty = makePsEnv (map fst env) ntyin @@ -616,7 +637,7 @@ > 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 _ = fail "Rule is not of equality type" +> getTypes t = fail $ "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" @@ -627,7 +648,7 @@ > axiomatise :: Name -> [Name] -> Tactic > axiomatise n helpers gam env tm@(Ind (Bind x (B Hole tyin) sc)) = -> do let (Ind ty') = normaliseEnv (ptovenv env) (Gam []) (finalise (Ind tyin)) +> do let (Ind ty') = normaliseEnv (ptovenv env) (emptyGam) (finalise (Ind tyin)) > let ty = makePsEnv (map fst env) ty' > let fvs = reverse $ getUsedBoundVars env ((getNames (Sc ty))++helpers) > let axiom = bind Pi fvs (Sc ty) @@ -645,7 +666,7 @@ > quote :: Tactic > quote gam env tm@(Ind (Bind h (B Hole tyin) sc)) = -> do let (Ind ty') = normaliseEnv (ptovenv env) (Gam []) (finalise (Ind tyin)) +> do let (Ind ty') = normaliseEnv (ptovenv env) (emptyGam) (finalise (Ind tyin)) > ty <- checkQuoted ty' > let qv = uniqify (mkns h (UN "qv")) $ > (map fst env) ++ (getBoundNames (Sc ty)) diff --git a/Ivor/Typecheck.lhs b/Ivor/Typecheck.lhs --- a/Ivor/Typecheck.lhs +++ b/Ivor/Typecheck.lhs @@ -13,6 +13,7 @@ > import Ivor.Constant > import Control.Monad.State +> import Data.List > import Debug.Trace Conversion in the presence of staging is a bit more than simply syntactic @@ -84,7 +85,10 @@ > Bool, -- Inferring types of names (if true) > Env Name, -- Extra bindings, if above is true > -- conversion constraints; remember the environment at the time we tried -> [(Env Name, Indexed Name, Indexed Name)]) +> -- also a string explaining where the constraint came from +> [(Env Name, Indexed Name, Indexed Name, String)], +> -- Metavariables we've introduce to define later +> [Name]) > type Level = Int @@ -93,30 +97,38 @@ > doConversion :: Monad m => > Raw -> Gamma Name -> -> [(Env Name, Indexed Name, Indexed Name)] -> +> [(Env Name, Indexed Name, Indexed Name,String)] -> > Indexed Name -> Indexed Name -> > m (Indexed Name, Indexed Name) > doConversion raw gam constraints (Ind tm) (Ind ty) = -> -- trace ("Finishing checking " ++ show tm) $ -- ++ " with " ++ show constraints) $ +> -- trace ("Finishing checking " ++ show tm ++ " with " ++ show (length constraints) ++ " equations") $ > -- 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... -> do (subst, nms) <- mkSubst $ (map (\x -> (False,x)) constraints) ++ -> (map (\x -> (True,x)) ((reverse constraints)++constraints)) +> do let cs = nub constraints +> (subst, nms) <- {-# SCC "name" #-} +> mkSubst $ (map (\x -> (True,x)) cs) +> ++ (map (\x -> (False,x)) (reverse cs)) > let tm' = papp subst tm > let ty' = papp subst ty -> return {- $ trace (show nms ++ "\n" ++ show (tm',ty')) -} (Ind tm',Ind ty') +> return (Ind tm',Ind ty') -> where mkSubst [] = return (P, []) -> mkSubst ((ok, (env,Ind x,Ind y)):xs) -> = do (s',nms) <- mkSubst xs +> where mkSubst xs = mkSubst' (P,[]) xs +> mkSubst' acc [] = return acc +> mkSubst' acc (q:xs) +> = do acc' <- mkSubstQ acc q +> mkSubst' acc' xs +> +> mkSubstQ (s',nms) (ok, (env,Ind x,Ind y,msg)) +> = do -- (s',nms) <- mkSubst xs > let x' = papp s' x > let (Ind y') = normalise gam (Ind (papp s' y)) -> uns <- case unifyenvErr ok gam env (Ind x') (Ind y') of -> Success x' -> return x' -> Failure err -> fail err +> uns <- {-# SCC "substUnify" #-} +> case unifyenvErr ok gam env (Ind x') (Ind y') of +> Success x' -> return x' +> Failure err -> fail err -{- trace ("XXX: " ++ err ++ show (x',y')) $ return [] -} fail $ err {- ++"\n" ++ show nms ++"\n" ++ show constraints -- $ -} ++ " Can't convert "++show x'++" and "++show y' ++ "\n" ++ show constraints ++ "\n" ++ show nms + Failure err -> fail $ err ++"\n" ++ show nms ++"\n" ++ show constraints -- $ -} ++ " Can't convert "++show x'++" and "++show y' ++ "\n" ++ show constraints ++ "\n" ++ show nms > extend s' nms uns @@ -133,7 +145,7 @@ > check :: Monad m => Gamma Name -> Env Name -> Raw -> Maybe (Indexed Name) -> > m (Indexed Name, Indexed Name) > check gam env tm mty = do -> ((tm', ty'), (_,_,_,convs)) <- lvlcheck 0 False 0 gam env tm mty +> ((tm', ty'), (_,_,_,convs,_)) <- lvlcheck 0 False 0 gam env tm mty > tm'' <- doConversion tm gam convs tm' ty' > return tm'' @@ -141,7 +153,7 @@ > Maybe (Indexed Name) -> > m (Indexed Name, Indexed Name, Env Name) > checkAndBind gam env tm mty = do -> ((v,t), (_,_,e,convs)) <- lvlcheck 0 True 0 gam env tm mty +> ((v,t), (_,_,e,convs,_)) <- lvlcheck 0 True 0 gam env tm mty > (v',ty') <- doConversion tm gam convs v t > return (v',ty',e) @@ -149,39 +161,91 @@ Check two things together, with the same environment and variable inference, and with the same expected type. We need this for checking pattern clauses... +Return a list of the functions we need to define to complete the definition. > checkAndBindPair :: Monad m => Gamma Name -> Raw -> Raw -> > m (Indexed Name, Indexed Name, -> Indexed Name, Indexed Name, Env Name) +> Indexed Name, Indexed Name, Env Name, +> [(Name, Indexed Name)]) > checkAndBindPair gam tm1 tm2 = do -> ((v1,t1), (next, inf, e, bs)) <- lvlcheck 0 True 0 gam [] tm1 Nothing +> ((v1,t1), (next, inf, e, bs,_)) <- lvlcheck 0 True 0 gam [] tm1 Nothing > -- rename all the 'inferred' things to another generated name, > -- so that they actually get properly checked on the rhs > let realNames = mkNames next -> e' <- fixupB gam realNames e +> e' <- renameB gam realNames (renameBinders e) > (v1', t1') <- fixupGam gam realNames (v1, t1) -> (v1'',t1'') <- doConversion tm1 gam bs v1 (normalise gam t1) -> ((v2,t2), (_, _, e'', bs')) <- {- trace ("Checking " ++ show tm2 ++ " has type " ++ show t1') $ -} lvlcheck 0 inf next gam e' tm2 (Just t1') -> (v2',t2') <- doConversion tm2 gam bs' v2 (normalise gam t2) -> return (v1',t1',v2',t2',e'') +> (v1''@(Ind vtm),t1'') <- {-# SCC "convert1" #-}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') $ -} {-# SCC "pairLvlCheck" #-} lvlcheck 0 inf next gam ein tm2 (Just t1') +> (v2',t2') <- {-# SCC "convert2" #-} doConversion tm2 gam bs' v2 t2 -- (normalise gam t2) +> if (null metas) +> then return (v1',t1',v2',t2',e'', []) +> else do let (Ind v2tt) = v2' +> let (v2'', newdefs) = updateMetas v2tt +> return (v1',t1',Ind v2'',t2',e'', 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) + > where mkNames 0 = [] > mkNames n > = ([],Ind (P (MN ("INFER",n-1))), -> Ind (P (MN ("T",n-1)))):(mkNames (n-1)) +> Ind (P (MN ("T",n-1))), "renaming"):(mkNames (n-1)) +> renameBinders [] = [] +> renameBinders (((MN ("INFER",n)),b):bs) +> = ((MN ("T",n),b):(renameBinders bs)) +> renameBinders (b:bs) = b:renameBinders bs +We need to order environments so that names used later are bound first. +*sigh*. This is turning into an almighty hack... I'm not convinced an +ordinary sort will do all the comparisons we need. Still, it's O(n^3) but +n is unlikely ever to be very big. Let's rethink this if it proves a +bottleneck. + +> orderEnv [] = [] +> orderEnv (x:xs) = insertEnv x (orderEnv xs) +> insertEnv x [] = [x] + +Insert here if the name at x does not appear later in any type. + +> insertEnv x (y:ys) = if (appearsIn x (y:ys)) +> then y:(insertEnv x ys) +> else x:y:ys + +if (all (\e -> envLT x e) (y:ys)) + then y:(insertEnv x ys) + else x:y:ys + +> where +> appearsIn (n,_) env = any (n_in n) env +> n_in n (n2, B _ t) = n `elem` (getNames (Sc t)) + + envLT (n1,B _ t1) (n2,B _ t2) + | n2 `elem` (getNames (Sc t1)) = False + | otherwise = True -- not (n1 `elem` (getNames (Sc t2))) + + +> traceConstraints [] = "" +> traceConstraints ((_,x,y,_):xs) = show (x,y) ++ "\n" ++ traceConstraints xs + +> inferName n = (MN ("INFER", n)) + > lvlcheck :: Monad m => Level -> Bool -> Int -> > Gamma Name -> Env Name -> Raw -> > Maybe (Indexed Name) -> > m ((Indexed Name, Indexed Name), CheckState) > lvlcheck lvl infer next gamma env tm exp -> = do runStateT (tcfixupTop env lvl tm exp) (next, infer, [], []) +> = do runStateT (tcfixupTop env lvl tm exp) (next, infer, [], [], []) > where Do the typechecking, then unify all the inferred terms. > tcfixupTop env lvl t exp = do > tm@(_,tmty) <- tc env lvl t exp -> (next, infer, bindings, errs) <- get +> (next, infer, bindings, errs ,mvs) <- get > -- First, insert inferred values into the term > tm'@(_,tmty) <- fixup errs tm > -- Then check the resulting type matches the expected type. @@ -193,10 +257,10 @@ > else return () > -- Then fill in any remained inferred values we got by knowing the > -- expected type -> (next, infer, bindings, errs) <- get +> (next, infer, bindings, errs, mvs) <- get > tm <- fixup errs tm -> bindings <- fixupB gamma errs bindings -> put (next, infer, bindings, errs) +> -- bindings <- fixupB gamma errs bindings +> put (next, infer, bindings, errs, mvs) > return tm' > tcfixup env lvl t exp = do @@ -204,10 +268,10 @@ > -- case exp of > -- Nothing -> return () > -- Just expt -> checkConvSt env gamma expt tmty "Type error" -> (next, infer, bindings, errs) <- get +> (next, infer, bindings, errs, mvs) <- get > tm' <- fixup errs tm -> bindings <- fixupB gamma errs bindings -> put (next, infer, bindings, errs) +> bindings <- (fixupB gamma errs) $! bindings +> put (next, infer, bindings, errs, mvs) > return tm' tc has state threaded through -- state is a tuple of the next name to @@ -227,7 +291,7 @@ > 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) @@ -241,25 +305,26 @@ > lookupi x (_:xs) i = lookupi x xs (i+1) > defaultResult = do -> (next, infer, bindings, errs) <- get +> (next, infer, bindings, errs, mvs) <- get > if infer > then case exp of > Nothing -> fail $ "No such name as " ++ show n -> Just (Ind t) -> do put (next, infer, (n, B Pi t):bindings, errs) +> Just (Ind t) -> do put (next, infer, (n, B Pi t):bindings, errs, mvs) > return (Ind (P n), Ind t) > else fail $ "No such name as " ++ show n > tc env lvl (RApp f a) exp = do > (Ind fv, Ind ft) <- tcfixup env lvl f Nothing -> let fnfng = normaliseEnv env (Gam []) (Ind ft) +> let fnfng = normaliseEnv env emptyGam (Ind ft) > let fnf = normaliseEnv env gamma (Ind ft) > (rv, rt) <- > case (fnfng,fnf) of > ((Ind (Bind _ (B Pi s) (Sc t))),_) -> do > (Ind av,Ind at) <- tcfixup env lvl a (Just (Ind s)) -> checkConvSt env gamma (Ind at) (Ind s) $ "Type error: " ++ show a ++ " : " ++ show at ++ ", expected type "++show s -- ++" "++show env +> let sty = (normaliseEnv env emptyGam (Ind s)) > let tt = (Bind (MN ("x",0)) (B (Let av) at) (Sc t)) -> let tmty = (normaliseEnv env (Gam []) (Ind tt)) +> let tmty = (normaliseEnv env emptyGam (Ind tt)) +> checkConvSt env gamma (Ind at) (Ind s) $ "Type error in application of " ++ show fv ++ " : " ++ show a ++ " : " ++ show at ++ ", expected type "++show sty ++ " " ++ show tmty > return (Ind (App fv av), tmty) > (_, (Ind (Bind _ (B Pi s) (Sc t)))) -> do > (Ind av,Ind at) <- tcfixup env lvl a (Just (Ind s)) @@ -295,7 +360,7 @@ > (Just (Ind (Bind sn sb (Sc st)))) -> Just $ > normaliseEnv ((sn,sb):env) gamma (Ind st) > _ -> fail (show exp) -> (Ind scv, Ind sct) <- tcfixup ((n,gb):env) lvl sc scexp +> (Ind scv, Ind sct) <- tcfixup ((n,gb):env) lvl sc Nothing -- scexp > --discharge gamma n gb (Sc scv) (Sc sct) > discharge gamma n gb (pToV n scv) (pToV n sct) > tc env lvl l@(RLabel t comp) _ = do @@ -325,20 +390,47 @@ > tc env lvl (RStage s) exp = do > (Ind sv, Ind st) <- tcStage env lvl s exp > return (Ind sv, Ind st) -> tc env lvl RInfer (Just exp) = do -> (next, infer, bindings, errs) <- get -> put (next+1, infer, bindings, errs) -> return (Ind (P (MN ("INFER",next))), exp) +> tc env lvl RInfer (Just (Ind exp)) = do +> (next, infer, bindings, errs, mvs) <- get +> let bindings' = if infer +> then (inferName next, B Pi exp):bindings +> else bindings +> put (next+1, infer, bindings', errs, mvs) +> return (Ind (P (inferName next)), Ind exp) > tc env lvl RInfer Nothing = fail "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 the expected type. -> tc env lvl (RMeta n) (Just exp) = do (next, infer, bindings, errs) <- get -> fail $ show (n, exp, bindings, env) ++ " -- Not implemented" -> tc env lvl (RMeta n) Nothing = fail $ "Don't know the expected type of " ++ show n +> tc env lvl (RMeta n) (Just (Ind exp)) +> = do (next, infer, bindings, errs, mvs) <- get +> put (next, infer, bindings, errs, n:mvs) +> -- 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) $ -} +> return (tm,Ind exp) +> -- fail $ show (n, exp, bindings, env) ++ " -- Not implemented" +> where abstractOver [] mv exp args = +> return (Ind (appArgs (Meta mv exp) args)) +> abstractOver ((n,B _ t):ns) mv exp args = +> abstractOver ns mv (Bind n (B Pi t) (pToV n exp)) ((P n):args) + mkn (UN n) = MN (n,0) + mkn (MN (n,x)) = MN (n,x+1) + +> tc env lvl (RMeta n) Nothing +> -- just invent a name for it and see what inference gives us +> = do (next, infer, bindings, errs, mvs) <- get +> put (next+1, infer, bindings, errs, mvs) +> -- let guessty = Bind (MN ("X", 0)) (B Pi (P (inferName next))) +> -- (Sc (P (inferName (next+1)))) +> let guessty = (P (inferName next)) +> tc env lvl (RMeta n) (Just (Ind guessty)) + +fail $ "Don't know the expected type of " ++ show n + > tcStage env lvl (RQuote t) _ = do > (Ind tv, Ind tt) <- tc env (lvl+1) t Nothing > return (Ind (Stage (Quote tv)), Ind (Stage (Code tt))) @@ -436,11 +528,11 @@ > return ((B MatchAny tv), env) > checkpatt gamma env lvl n pat t = do > (Ind tv,Ind tt) <- tcfixup env lvl t Nothing -> (next, infer, bindings, err) <- get -> put (next, True, bindings, err) +> (next, infer, bindings, err, mvs) <- get +> put (next, True, bindings, err, mvs) > (Ind patv,Ind patt) <- tcfixup (bindings++env) lvl pat Nothing -> (next, _ ,bindings, err) <- get -> put (next, infer, bindings, err) +> (next, _ ,bindings, err, mvs) <- get +> put (next, infer, bindings, err, mvs) > let ttnf = normaliseEnv env gamma (Ind tt) > --checkConvEnv env gamma (Ind patt) (Ind tv) $ > -- show patt ++ " and " ++ show tv ++ " are not convertible" @@ -486,12 +578,13 @@ -- > checkPatt gam env acc RInfer ty = return (combinepats acc PTerm, env) -- > checkPatt gam env _ _ _ = fail "Invalid pattern" -> checkConvSt env g x y err = do (next, infer, bindings, err) <- get -> put (next, infer, bindings, (env,x,y):err) -> return () +> checkConvSt env g x y msg +> = do (next, infer, bindings, err, mvs) <- get +> put (next, infer, bindings, (env,x,y,msg):err, mvs) +> return () > fixupGam gamma [] tm = return tm -> fixupGam gamma ((env,x,y):xs) (Ind tm, Ind ty) = do +> fixupGam gamma ((env,x,y,_):xs) (Ind tm, Ind ty) = do > uns <- case unifyenv gamma env y x of > Success x' -> return x' > Failure err -> return [] -- fail err -- $ "Can't convert "++show x++" and "++show y ++ " ("++show err++")" @@ -502,12 +595,28 @@ > fixupNames gam [] tm = tm > fixupNames gam ((x,ty):xs) tm = fixupNames gam xs $ substName x ty (Sc tm) -> fixupB gam xs [] = return [] -> fixupB gam xs ((n, (B b t)):bs) = do -> bs' <- fixupB gam xs bs -> (Ind t', _) <- fixupGam gam xs (Ind t, Ind Star) -> return ((n,(B b t')):bs') +> fixupB gam xs bs = fixupB' gam xs bs [] +> fixupB' gam xs [] acc = return acc +> fixupB' gam xs ((n, (B b t)):bs) acc = +> -- if t is already fully explicit, don't bother +> if (allExplicit (getNames (Sc t))) then fixupB' gam xs bs ((n,(B b t)):acc) +> else do (Ind t', _) <- fixupGam gam xs (Ind t, Ind Star) +> fixupB' gam xs bs ((n,(B b t')):acc) +> where allExplicit [] = True +> allExplicit ((MN ("INFER",_)):_) = False +> allExplicit (_:xs) = allExplicit xs + +> renameB gam xs [] = return [] +> renameB gam xs ((n, (B b t)):bs) = do +> bs' <- renameB gam xs bs +> let t' = renameGam xs t +> return ((n,(B b t')):bs') +> where renameGam [] tm = tm +> renameGam ((env,Ind (P x),Ind (P y),_):xs) tm = +> let tm' = fixupNames gam [(x, P y)] tm in +> renameGam xs tm' + > combinepats Nothing x = x > combinepats (Just (PVar n)) x = error "can't apply things to a variable" > combinepats (Just (PCon tag n ty args)) x = PCon tag n ty (args++[x]) @@ -570,6 +679,8 @@ > pToV2 v p (V w) = Sc (V w) > pToV2 v p (Con t n i) = Sc (Con t n i) > pToV2 v p (TyCon n i) = Sc (TyCon n i) +> pToV2 v p (Meta n t) = Sc (Meta n (getSc (pToV2 v p t))) +> where getSc (Sc a) = a > pToV2 v p (Elim n) = Sc (Elim n) > pToV2 v p (Bind n b (Sc sc)) = Sc (Bind n (fmap (getSc.(pToV2 v p)) b) > (pToV2 (v+1) p sc)) diff --git a/Ivor/Unify.lhs b/Ivor/Unify.lhs --- a/Ivor/Unify.lhs +++ b/Ivor/Unify.lhs @@ -35,15 +35,18 @@ > Gamma Name -> Env Name -> > Indexed Name -> Indexed Name -> m Unified > -- For the sake of readability of the results, first attempt to unify -> -- without reducing global names, and reduce if that doesn't work. -> -- (Actually, I'm not sure this helps. Probably just slows things down.) -> unifyenvErr i gam env x y = {- trace (show (x,y) ++ "\n" ++ +> -- without reducing, and reduce if that doesn't work. +> -- 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" ++ > show (p (normalise (gam' gam) x)) ++ "\n" ++ > show (p (normalise (gam' gam) x))) $-} -> {-case unifynferr i env (p (normalise emptyGam x)) -> (p (normalise emptyGam y)) of +> case unifynferr i env (p x) +> (p y) of > (Just x) -> return x -> Nothing -> -} unifynferr i env (p (normalise (gam' gam) x)) +> Nothing -> unifynferr i env (p (normalise (gam' gam) x)) > (p (normalise (gam' gam) y)) > where p (Ind t) = Ind (makePs t) > gam' g = concatGam g (envToGamHACK env) @@ -70,7 +73,7 @@ > unifynferr :: Monad m => > Bool -> -- Ignore errors > Env Name -> Indexed Name -> Indexed Name -> m Unified -> unifynferr ignore env (Ind x) (Ind y) +> unifynferr ignore env topx@(Ind x) topy@(Ind y) > = do acc <- un env env x y [] > if ignore then return () else checkAcc acc > return (acc \\ sentinel) @@ -78,7 +81,6 @@ > | x == y = return acc > | loc x envl == loc y envr && loc x envl >=0 > = return acc -> -- | ignore = trace (show (x,y)) $ return sentinel -- broken, forget acc, but move on > un envl envr (P x) t acc | hole envl x = return ((x,t):acc) > un envl envr t (P x) acc | hole envl x = return ((x,t):acc) > un envl envr (Bind x b@(B Hole ty) (Sc sc)) t acc @@ -94,7 +96,7 @@ > do acc' <- un envl envr f f' acc > un envl envr s s' acc' > | otherwise = if ignore then return acc -> else fail $ "Can't unify "++show x++" and "++show y -- ++ " 5" +> else fail $ "Can't unify "++show x++" and "++show y > where funify (P x) (P y) > | x==y = True > | otherwise = hole envl x || hole envl y @@ -112,7 +114,7 @@ > un envl envr x y acc > | x == y || ignore = return acc > | otherwise = fail $ "Can't unify " ++ show x ++ -> " and " ++ show y -- ++ " 1" +> " and " ++ show y ++ " in " ++ show (topx,topy) > unb envl envr (B b ty) (B b' ty') acc = > do acc' <- unbb envl envr b b' acc > un envl envr ty ty' acc' @@ -123,7 +125,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 "++show x++" and "++show y -- ++ " 2" +> else fail $ "Can't unify "++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 @@ -132,7 +134,7 @@ > unst envl envr x y acc = > if ignore then return acc > else fail $ "Can't unify " ++ show (Stage x) ++ -> " and " ++ show (Stage y) -- ++ " 3" +> " and " ++ show (Stage y) > hole env x | (Just (B Hole ty)) <- lookup x env = True > | otherwise = isInferred x @@ -145,7 +147,7 @@ > = if (ueq tm tm') -- Take account of names! == no good. > then checkAcc xs > else fail $ "Can't unify " ++ show tm ++ -> " and " ++ show tm' -- ++ " 4" +> " and " ++ show tm' > | otherwise = checkAcc xs > loc x xs = loc' 0 x xs @@ -157,7 +159,7 @@ TMP HACK! ;) > ueq :: TT Name -> TT Name -> Bool -> ueq x y = case unifyenv (Gam []) [] (Ind x) (Ind y) of +> ueq x y = case unifyenv emptyGam [] (Ind x) (Ind y) of > Just _ -> True > _ -> False 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(..), apply, > view, viewType, ViewConst, typeof, -> freeIn, namesIn, occursIn, getApp, +> freeIn, namesIn, occursIn, subst, getApp, +> Ivor.ViewTerm.getFnArgs, +> getArgTypes, Ivor.ViewTerm.getReturnType, +> dbgshow, > -- * Inductive types > Inductive(..)) > where -> import Ivor.TTCore as TTCore +> import Ivor.TTCore as TTCore hiding (subst) > import Ivor.Gadgets > import Ivor.State > import Ivor.Typecheck @@ -48,6 +51,7 @@ > -- is for. > data NameType = Bound | Free | DataCon | TypeCon | ElimOp > | Unknown -- ^ Use for sending to typechecker. +> deriving Show > -- | Construct a term representing a variable > mkVar :: String -- ^ Variable name @@ -193,7 +197,7 @@ > = Ivor.ViewTerm.Eval (vtaux ctxt tm) > vtaux ctxt (Stage (TTCore.Escape tm _)) > = Ivor.ViewTerm.Escape (vtaux ctxt tm) -> vtaux _ _ = error "Can't happen vtaux" +> vtaux _ t = error $ "Can't happen vtaux " ++ debugTT t > -- | Return whether the name occurs free in the term. > freeIn :: Name -> ViewTerm -> Bool @@ -256,4 +260,73 @@ > getApp :: ViewTerm -> ViewTerm > getApp (Ivor.ViewTerm.App f a) = getApp f > getApp x = x + +> -- | Get the arguments from a function application. +> getFnArgs :: ViewTerm -> [ViewTerm] +> getFnArgs (Ivor.ViewTerm.App f a) = Ivor.ViewTerm.getFnArgs f ++ [a] +> getFnArgs x = [] + +> -- | Get the argument names and types from a function type +> getArgTypes :: ViewTerm -> [(Name, ViewTerm)] +> getArgTypes (Ivor.ViewTerm.Forall n ty sc) = (n,ty):(getArgTypes sc) +> getArgTypes x = [] + +> -- | Get the return type from a function type +> getReturnType :: ViewTerm -> ViewTerm +> getReturnType (Ivor.ViewTerm.Forall n ty sc) = Ivor.ViewTerm.getReturnType sc +> getReturnType x = x + +> dbgshow (UN n) = "UN " ++ show n +> dbgshow (MN (n,i)) = "MN [" ++ show n ++ "," ++ show i ++ "]" + +> -- | Match the second argument against the first, returning a list of +> -- the names in the first paired with their matches in the second. Returns +> -- Nothing if there is a match failure. There is no searching under binders. +> match :: ViewTerm -> ViewTerm -> Maybe [(Name, ViewTerm)] +> match t1 t2 = do acc <- m' t1 t2 [] +> checkDups acc [] where +> m' (Name _ n) t acc = return ((n,t):acc) +> m' (Ivor.ViewTerm.App f a) (Ivor.ViewTerm.App f' a') acc +> = do acc' <- m' f f' acc +> m' a a' acc' +> m' x y acc | x == y = return acc +> | otherwise = fail $"Mismatch " ++ show x ++ " and " ++ show y + +> checkDups [] acc = return acc +> checkDups ((x,t):xs) acc +> = case lookup x xs of +> Just t' -> if t == t' then checkDups xs acc +> else fail $ "Mismatch on " ++ show x +> Nothing -> checkDups xs ((x,t):acc) + +> -- |Substitute a name n with a value v in a term f +> subst :: Name -> ViewTerm -> ViewTerm -> ViewTerm +> subst n v nm@(Name _ p) | p == n = v +> | otherwise = nm +> subst n v (Ivor.ViewTerm.App f a) +> = Ivor.ViewTerm.App (subst n v f) (subst n v a) +> subst n v (Ivor.ViewTerm.Lambda nn ty sc) +> = Ivor.ViewTerm.Lambda nn (subst n v ty) $ +> if (n==nn) then sc else subst n v sc +> subst n v (Forall nn ty sc) +> = Forall nn (subst n v ty) $ +> if (n==nn) then sc else subst n v sc +> subst n v (Ivor.ViewTerm.Let nn ty vv sc) +> = Ivor.ViewTerm.Let nn (subst n v ty) (subst n v vv) $ +> if (n==nn) then sc else subst n v sc +> subst n v (Ivor.ViewTerm.Label fn args ty) +> = Ivor.ViewTerm.Label fn (map (subst n v) args) (subst n v ty) +> subst n v (Ivor.ViewTerm.Call fn args ty) +> = Ivor.ViewTerm.Call fn (map (subst n v) args) (subst n v ty) +> subst n v (Ivor.ViewTerm.Return r) +> = Ivor.ViewTerm.Return (subst n v r) +> subst n v (Ivor.ViewTerm.Quote r) +> = Ivor.ViewTerm.Quote (subst n v r) +> subst n v (Ivor.ViewTerm.Code r) +> = Ivor.ViewTerm.Code (subst n v r) +> subst n v (Ivor.ViewTerm.Eval r) +> = Ivor.ViewTerm.Eval (subst n v r) +> subst n v (Ivor.ViewTerm.Escape r) +> = Ivor.ViewTerm.Escape (subst n v r) +> subst n v t = t diff --git a/ivor.cabal b/ivor.cabal --- a/ivor.cabal +++ b/ivor.cabal @@ -1,13 +1,16 @@ -Name: ivor -Version: 0.1.5 -License: BSD3 -License-file: LICENSE -Author: Edwin Brady -Maintainer: Edwin Brady -Homepage: http://www.dcs.st-and.ac.uk/~eb/Ivor/ - +Name: ivor +Version: 0.1.8 +Author: Edwin Brady +License: BSD3 +License-file: LICENSE +Author: Edwin Brady +Maintainer: Edwin Brady +Homepage: http://www.dcs.st-and.ac.uk/~eb/Ivor/ Stability: experimental -Category: Theorem provers +Build-depends: base, haskell98, parsec, mtl, directory, containers +Extensions: MultiParamTypeClasses, FunctionalDependencies, + ExistentialQuantification, OverlappingInstances +Category: Theorem provers, Dependent Types Synopsis: Theorem proving library based on dependent type theory Description: Ivor is a type theory based theorem prover, with a Haskell API, designed for easy extending and embedding @@ -55,7 +58,7 @@ -Build-depends: base, parsec, mtl, plugins, directory +Build-depends: base, parsec, mtl, directory Build-type: Simple Extensions: MultiParamTypeClasses, FunctionalDependencies, @@ -64,15 +67,14 @@ -- GHC-options: -Wall Exposed-modules: - Ivor.TT, 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.CodegenC, Ivor.Datatype, Ivor.Display, - Ivor.ICompile, Ivor.MakeData, Ivor.Unify, - Ivor.Grouper, Ivor.ShellParser, Ivor.Constant, - Ivor.RunTT, Ivor.Compiler, Ivor.Prefix, - Ivor.PatternDefs, Ivor.ShellState - + Ivor.TT, 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.CodegenC, Ivor.Datatype, Ivor.Display, + Ivor.ICompile, Ivor.MakeData, Ivor.Unify, + Ivor.Grouper, Ivor.ShellParser, Ivor.Constant, + Ivor.RunTT, Ivor.Compiler, Ivor.Prefix, + Ivor.PatternDefs, Ivor.ShellState, Ivor.Scopecheck