ivor 0.1.5 → 0.1.8
raw patch · 22 files changed
+848/−371 lines, 22 filesdep +containersdep +haskell98dep −pluginsnew-uploader
Dependencies added: containers, haskell98
Dependencies removed: plugins
Files
- Ivor/Construction.lhs +3/−3
- Ivor/Datatype.lhs +19/−7
- Ivor/Display.lhs +1/−1
- Ivor/Evaluator.lhs +14/−5
- Ivor/Gadgets.lhs +3/−0
- Ivor/ICompile.lhs +1/−1
- Ivor/MakeData.lhs +1/−1
- Ivor/Nobby.lhs +55/−55
- Ivor/PatternDefs.lhs +38/−16
- Ivor/Plugin.lhs +45/−42
- Ivor/Prefix.hs +1/−1
- Ivor/RunTT.lhs +1/−1
- Ivor/Scopecheck.lhs +52/−0
- Ivor/Shell.lhs +5/−4
- Ivor/State.lhs +32/−30
- Ivor/TT.lhs +207/−88
- Ivor/TTCore.lhs +52/−7
- Ivor/Tactics.lhs +33/−12
- Ivor/Typecheck.lhs +169/−58
- Ivor/Unify.lhs +16/−14
- Ivor/ViewTerm.lhs +76/−3
- ivor.cabal +24/−22
Ivor/Construction.lhs view
@@ -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 ++ " ++
Ivor/Datatype.lhs view
@@ -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)
Ivor/Display.lhs view
@@ -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
Ivor/Evaluator.lhs view
@@ -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
Ivor/Gadgets.lhs view
@@ -81,3 +81,6 @@ > catch (do content <- readFile $ d ++ "/" ++ fn > return content) > (\e -> ff' ds fn)++> unJust :: Maybe a -> a+> unJust (Just a) = a
Ivor/ICompile.lhs view
@@ -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)
Ivor/MakeData.lhs view
@@ -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
Ivor/Nobby.lhs view
@@ -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
Ivor/PatternDefs.lhs view
@@ -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)
Ivor/Plugin.lhs view
@@ -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
Ivor/Prefix.hs view
@@ -1,1 +1,1 @@-module Ivor.Prefix where prefix = "/usr/local"+module Ivor.Prefix where prefix = "/Users/edwin"
Ivor/RunTT.lhs view
@@ -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)
+ Ivor/Scopecheck.lhs view
@@ -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"++
Ivor/Shell.lhs view
@@ -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) }
Ivor/State.lhs view
@@ -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"
Ivor/TT.lhs view
@@ -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"
Ivor/TTCore.lhs view
@@ -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<length ctx) then P (ctx!!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)) =
Ivor/Tactics.lhs view
@@ -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))
Ivor/Typecheck.lhs view
@@ -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))
Ivor/Unify.lhs view
@@ -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
Ivor/ViewTerm.lhs view
@@ -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
ivor.cabal view
@@ -1,13 +1,16 @@-Name: ivor-Version: 0.1.5-License: BSD3-License-file: LICENSE-Author: Edwin Brady-Maintainer: Edwin Brady <eb@dcs.st-and.ac.uk>-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 <eb@dcs.st-and.ac.uk>+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