ivor 0.1.8 → 0.1.9

raw patch · 17 files changed

+645/−374 lines, 17 filesdep ~basePVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependency ranges changed: base

API changes (from Hackage documentation)

Files

• Ivor/Datatype.lhs +11/−7
• Ivor/Errors.lhs +22/−0
• Ivor/MakeData.lhs +6/−4
• Ivor/PatternDefs.lhs +108/−43
• Ivor/Primitives.lhs +2/−2
• Ivor/Shell.lhs +11/−11
• Ivor/ShellParser.lhs +14/−3
• Ivor/ShellState.lhs +1/−1
• Ivor/State.lhs +6/−5
• Ivor/TT.lhs +194/−135
• Ivor/TTCore.lhs +74/−8
• Ivor/Tactics.lhs +16/−17
• Ivor/Typecheck.lhs +137/−102
• Ivor/Unify.lhs +22/−31
• Ivor/ViewTerm.lhs +17/−1
• emacs/ivor-mode.el +1/−1
• ivor.cabal +3/−3

@@ -5,6 +5,7 @@ > import Ivor.Typecheck > import Ivor.Nobby > import Ivor.PatternDefs+> import Ivor.Errors  > import Debug.Trace @@ -52,7 +53,7 @@ schemes, and returns a DataType, ready for compilation to entries in the context and an executable elimination rule. -> checkType :: Monad m => Gamma Name -> RawDatatype -> m (Datatype Name)+> checkType :: Gamma Name -> RawDatatype -> IvorM (Datatype Name) > checkType 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)@@ -61,12 +62,12 @@ >	 (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) (Just esch) (Just csch) eschemes cschemes) -> checkTypeNoElim :: Monad m => Gamma Name -> RawDatatype -> m (Datatype Name)+> checkTypeNoElim :: Gamma Name -> RawDatatype -> IvorM (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)@@ -96,9 +97,8 @@ we get V 0 = pn ... V n = p0 then pattern variables are retrieved by projection with Proj in typechecked t. -> checkScheme :: Monad m =>->	          Gamma Name -> Name -> RawScheme -> m (Scheme Name)-> checkScheme gamma n (RSch pats ret) = +> checkScheme :: Gamma Name -> Name -> RawScheme -> IvorM (Scheme Name)+> checkScheme gamma n (RSch pats (RWRet ret)) =  >     do let ps = map (mkPat gamma) pats >	 let rhsvars = getPatVars gamma ps >        let rhs = substVars gamma n rhsvars ret@@ -116,8 +116,10 @@ > mkPat gam (RApp f a) = pat' (unwind f a) >   where unwind (RApp f s) a = let (f',as) = unwind f s in >				    (f',(mkPat gam a):as)+>         unwind (RFileLoc _ _ t) a = unwind t a >	  unwind t a = (t, [mkPat gam a]) >         pat' (Var n, as) = mkPatV n (lookupval n gam) (reverse as)+>         pat' (RFileLoc _ _ t, as) = pat' (t, as) >         pat' _ = PTerm  >         mkPatV n (Just (DCon t x)) as = PCon t n tyname as@@ -126,6 +128,7 @@ >         tyname = case (getTyName gam (getname (getappfun f))) of >                    Just x -> x >         getname (Var n) = n+>         getname (RFileLoc _ _ t) = getname t > mkPat gam _ {-(RBind _ _ _)-} = PTerm > {- > TODO: If a datatype has a placeholder in its indices, the value should@@ -178,6 +181,7 @@ >			    (Just i) -> i >	   sv' (RApp f a) = App (sv' f) (sv' a) >          sv' (RConst c) = Const c+>          sv' (RFileLoc _ _ t) = sv' t  >          mkGood x = case (lookupval x gam) of >	       (Just (DCon t i)) -> Con t x i

@@ -0,0 +1,22 @@+> {-# OPTIONS_GHC -fglasgow-exts #-}++> module Ivor.Errors where++> import Ivor.TTCore+> import Control.Monad.Error++> data IError = ICantUnify (Indexed Name) (Indexed Name)+>             | INotConvertible (Indexed Name) (Indexed Name)+>             | IMessage String+>             | IUnbound (Indexed Name) (Indexed Name) (Indexed Name) (Indexed Name) [Name]+>             | INoSuchVar Name+>             | IContext String IError+>   deriving (Show, Eq)++> instance Error IError where+>     noMsg = IMessage "Ivor Error"+>     strMsg s = IMessage s++> type IvorM = Either IError++> ifail = Left

@@ -29,8 +29,7 @@ >         cischemes = mkSchemes False name (ruleName name "Case")  >                               params datacons motiveName methNames >         tycontype = mkCon params contype in->         return $ -- (trace (show eischemes)) $  ->          RData (name,tycontype) datacons (length params)+>         return $ RData (name,tycontype) datacons (length params) >                    (ruleName name "Elim", ecasetype) -- elim rule >                    (ruleName name "Case", ccasetype) -- case rule >                    eischemes -- elim rule iota schemes@@ -49,8 +48,8 @@ >              = (mkScheme rec n ername ps c cty motive mns m):(mks cs ms mns)  > mkScheme rec n ername ps c cty motive mns meth ->     = RSch (mkIArgs ps c cty motive mns) ->            (mkIRet rec n ername meth motive mns ps cty)+>     = RSch (mkIArgs ps c cty motive mns)+>            (RWRet (mkIRet rec n ername meth motive mns ps cty))  > mkIArgs ps c cty motive mns = getappargs (getrettype cty) ++ >                               [mkapp (Var c) (map Var (getargnames cty))] ++@@ -62,6 +61,7 @@ >            | isrec ty tyname && rec  >                = (Var n):(mkRecApp ername ty n motive mns):(mkArgs sc) >            | otherwise = (Var n):(mkArgs sc)+>         mkArgs (RFileLoc f l t) = mkArgs t >         mkArgs _ = [] >         mkRecApp en ty n motive mns =  >             mkapp (Var en) $ (getappargs ty)++(map Var (n:motive:mns))@@ -91,6 +91,7 @@  > bindIndices (RBind n (B Pi ty) sc) rest  >     = (RBind n (B Pi ty) (bindIndices sc rest))+> bindIndices (RFileLoc f l t) rest = bindIndices t rest > bindIndices sc rest = rest  > bindTarget x n ps ty rest @@ -111,6 +112,7 @@ >            | isrec argtype tyname && rec >                = (RBind a (B Pi argtype) (mkrec a argtype sc)) >            | otherwise = (RBind a (B Pi argtype) (methtype sc))+>        methtype (RFileLoc _ _ t) = methtype t >        methtype sc = mkapp (Var p) $ (getindices sc)++ >              [mkapp (Var n) (map Var ((map fst ps)++(getargnames ty)))] >        mkrec a argtype sc = (RBind (ih a) (B Pi (rectype a argtype p)) 

@@ -7,6 +7,7 @@ > import Ivor.Nobby > import Ivor.Typecheck > import Ivor.Unify+> import Ivor.Errors  > import Debug.Trace > import Data.List@@ -14,14 +15,15 @@  Use the iota schemes from Datatype to represent pattern matching definitions. -Return the definition and its type, as well as any other names which need+Return the definition, and auxiliary definitions,+and their types, 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] -> +> checkDef :: Gamma Name -> Name -> Raw -> [PMRaw] ->  >             Bool -> -- Check for coverage >             Bool -> -- Check for well-foundedness->             m (PMFun Name, Indexed Name, [(Name, Indexed Name)], Bool)+>             IvorM ([(Name, 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")]])@@ -33,15 +35,16 @@ >   checkNotExists fn gam >   gam' <- gInsert fn (G Undefined ty defplicit) gam >   clauses' <- validClauses gam' fn ty clauses'->   (pmdef, newdefs, covers) <- matchClauses gam' fn pats tyin cover clauses'->   wf <- if wellfounded then+>   (pmdefs, newdefs, covers) <- matchClauses gam' fn pats tyin ty cover clauses'+>   wf <- return True +>         {- 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+>                   _ -> return True -} >   let total = wf && covers->   return (PMFun arity pmdef, ty, newdefs, total)+>   return (pmdefs, newdefs, total) >     where checkNotExists n gam = case lookupval n gam of >                                 Just Undefined -> return () >                                 Just _ -> fail $ show n ++ " already defined"@@ -65,11 +68,10 @@ 2) Alternatively, a definition is well founded if in every recursive call there are no increasing arguments and at least one decreasing argument. -> checkWellFounded :: Monad m =>->                     Gamma Name ->+> checkWellFounded :: Gamma Name -> >                     Name -> -- recursive function name >                     [Int] -> -- set of well founded args->                     [PMDef Name] -> m ()+>                     [PMDef Name] -> IvorM () > checkWellFounded gam fn args cs = case cwf1 fn args cs of >                                     Failure err -> cwf2 fn cs err >                                     Success v -> return ()@@ -171,20 +173,24 @@ Match up the inferred arguments to the names (so getting the types of the names bound in patterns) then type check the right hand side. -> matchClauses :: Monad m => Gamma Name -> Name -> [PMRaw] -> Raw ->+Each clause may generate auxiliary definitions, so return all definitons created.++> matchClauses :: Gamma Name -> Name -> [PMRaw] -> Raw -> Indexed Name ->  >                 Bool -> -- Check coverage >                 [(Indexed Name, Indexed Name)] -> ->                 m ([PMDef Name], [(Name, Indexed Name)], Bool)-> matchClauses gam fn pats tyin cover gen = do+>                 IvorM ([(Name, PMFun Name, Indexed Name)], [(Name, Indexed Name)], Bool)+> matchClauses gam fn pats tyin ty@(Ind ty') cover gen = do >    let raws = zip (map mkRaw pats) (map getRet pats)->    (checkpats, newdefs) <- mytypechecks gam raws [] []+>    (checkpats, newdefs, aux, covers) <- mytypechecks gam raws [] [] [] True >    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+>                 Left err -> return False >                 _ -> return True->    return $ (map (mkScheme gam) checkpats, newdefs, cv)+>    let pmdef = map (mkScheme gam) checkpats+>    let arity = length (getExpected ty')+>    return $ ((fn, PMFun arity pmdef, ty) : aux , newdefs, cv && covers)      where mkRaw (RSch pats r) = mkPBind pats tyin r           mkPBind [] _ r = r@@ -193,14 +199,13 @@  >   where mkRaw (RSch pats r) = mkapp (Var fn) pats >         getRet (RSch pats r) = r->         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) = +>         mytypechecks gam [] acc defs auxdefs cov = return (reverse acc, auxdefs, defs, cov)+>         mytypechecks gam (c:cs) acc defs auxdefs cov =+>             do ((cl, cr, _), newdefs, aux', covd) <- mytypecheck gam c (length cs)+>                mytypechecks gam cs ((cl,cr):acc) (defs++newdefs) (auxdefs++aux') (cov && covd)+>         mytypecheck gam (clause, (RWRet ret)) i =  >             do (tm@(Ind tmtt), pty,->                 rtm@(Ind rtmtt), rty, env, newdefs) <-->                   checkAndBindPair gam clause ret+>                 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@@ -208,17 +213,73 @@ >                -- checkConvEnv env gam pty rty $ "Pattern error: " ++ show pty ++ " and " ++ show rty ++ " are not convertible " ++ show unify >                let namesret = filter (notGlobal gam') $ getNames (Sc rtmtt') >                let namesbound = getNames (Sc tmtt)->                checkAllBound namesret namesbound (Ind rtmtt') tmtt->                return (tm, Ind rtmtt', newdefs)+>                checkAllBound (fileLine ret) namesret namesbound (Ind rtmtt') tmtt rty pty+>                -- trace (show (unified, rtmtt, tm, rtmtt')) $ +>                return ((tm, Ind rtmtt', newdefs), [], newdefs, True)+>         mytypecheck gam (clause, (RWith scr pats)) i =+>             do -- Get the type of scrutinee, construct the type of the auxiliary definition+>                (tm@(Ind clausett), clausety, _, scrty@(Ind stt), env) <- checkAndBindWith gam clause scr fn+>                let args = getRawArgs clause+>                let restTyin = addLastArg tyin (forget scrty)+>                margs <- getMatches tm tm+>                let margNames = nub (map fst margs)+>                let newargs = filter (\ (x,ty) -> x `elem` margNames) env+>                newpats <- mapM (getNewPat tm 1) pats+>                let newfntyin = mkNewTy (newargs ++ [(UN "__scr", B Pi stt)]) clausety+>                (newfnTy, _) <- check gam env (forget newfntyin) (Just (Ind Star))+>                -- Make a name for the new function, clauses in 'pats' need the new name,+>                -- and form a definition of type restTy+>                let newname = mkNewName fn i+>                -- TODO: All pats have to match against args ++ [_]+>                -- Final clause returns newname applied to args++scrutinee+>                let ret = rawApp (Var newname) ((map Var (map fst newargs)) ++ [scr])+>                let gam' = insertGam newname (G Undefined newfnTy 0) gam+>                newpdef <- mapM (newp tm newargs 1) (zip newpats pats)+>                (chk, auxdefs, _, _) <- mytypecheck gam' (clause, (RWRet ret)) i+>                (auxdefs', newdefs, covers) <- checkDef gam' newname (forget newfnTy) newpdef False cover+>                return (chk, auxdefs++auxdefs', newdefs, covers)++>         addLastArg (RBind n (B Pi arg) x) ty = RBind n (B Pi arg) (addLastArg x ty)+>         addLastArg x ty = RBind (UN "X") (B Pi ty) x+>         rawApp f [] = f+>         rawApp f (a:as) = rawApp (RApp f a) as++>         mkNewName (UN n) i = UN ("W__"++ n ++ "__" ++ show i) -- MN (n, i)+>         mkNewName (MN (n,j)) i = MN (n, (j + i + 255))++>         mkNewTy [] (Ind t) = t+>         mkNewTy ((x,b):ts) t = Bind x b (Sc (mkNewTy ts t))++>         getNewPat proto i (RSch args ret) = do+>             let pargs = rawApp (Var fn) (take (length args - i) args)+>             (argv, argt, _) <- checkAndBind gam [] pargs Nothing+>             getMatches argv proto++>         newp proto newargs i (newps, RSch args ret) = do+>             ret' <- newpRet ret+>             return $ RSch ((getAuxPats (map fst newargs) newps)++(lastn i args)) ret'+>                 where newpRet (RWith v schs) = +>                          do newpats <- mapM (getNewPat proto (i+1)) schs+>                             newpdef <- mapM (newp proto newargs (i+1)) (zip newpats schs)+>                             return (RWith v newpdef)+>                       newpRet r = return r++>         lastn i xs = reverse $ take i (reverse xs)++>         getAuxPats [] n = []+>         getAuxPats (x:xs) n = case lookup x n of+>                                 (Just t) -> (forget t):(getAuxPats xs n)+ >         notGlobal gam n = case lookupval n gam of >                               Nothing -> True >                               _ -> False->         checkAllBound r b rhs clause = do+>         checkAllBound fl r b rhs clause rhsTy clauseTy = do >              let unbound = filter (\y -> not (elem y b)) r >              if (length unbound == 0) >                 then return ()->                 else fail $ "Unbound names in clause for " ++ show clause ++ ":\n" ++ show rhs ++ "\n"->                             ++ show unbound ++ "\n"+>                 else ifail $ addContext fl (IUnbound (Ind clause) clauseTy rhs rhsTy unbound)+>         addContext Nothing err = err+>         addContext (Just (f,l)) err = IContext (f ++ ":" ++ show l ++ ":") err  > mkScheme :: Gamma Name -> (Indexed Name, Indexed Name) -> PMDef Name > mkScheme gam (Ind pat, ret) = Sch (map mkpat (getPatArgs pat)) ret@@ -245,31 +306,35 @@ must match one of 'pats'. fails, reporting which case isn't matched, if patterns don't cover. -> checkCoverage :: Monad m => [Indexed Name] -> [Indexed Name] -> m ()+> checkCoverage :: [Indexed Name] -> [Indexed Name] -> IvorM () > checkCoverage pats [] = return () > checkCoverage pats (c:cs) >     | length (filter (matches c) pats) > 0 = checkCoverage pats cs >     | otherwise = fail $ "Missing clause: " ++ show c -> matches (Ind p) (Ind t) = matches' p t-> matches' (App f a) (App f' a') = matches' f f' && matches' a a'-> matches' (Con _ x _) (Con _ y _) | x == y = True-> matches' (TyCon x _) (TyCon y _) | x == y = True-> matches' (P x) (P y) | x == y = True-> matches' (P (MN ("INFER",_))) _ = True-> matches' _ (P _) = True-> matches' x y = x == y+> matches p t = getMatches p t /= Nothing +> getMatches (Ind p) (Ind t) = matches' p t+> matches' (App f a) (App f' a') = do fm <- matches' f f'+>                                     am <- matches' a a'+>                                     return $ (fm ++ am)+> matches' (Con _ x _) (Con _ y _) | x == y = return []+> matches' (TyCon x _) (TyCon y _) | x == y = return []+> matches' (P x) (P y) | x == y = return [(y, P x)]+> matches' t (P n) = return [(n,t)]+> matches' (P nm@(MN ("INFER",_))) t = return []+> matches' x y = if x == y then return [] else fail "With pattern does not match parent" -> expandClause :: Monad m => Gamma Name -> RawScheme -> m [RawScheme]++> expandClause :: Gamma Name -> RawScheme -> IvorM [RawScheme] > expandClause gam (RSch ps ret) = do >   expanded <- mapM (expandCon gam) ps >   return $ map (\p -> RSch p ret) (combine expanded)  Remove the clauses which can't possibly be type correct. -> validClauses :: Monad m => Gamma Name -> Name -> Indexed Name ->->                 [RawScheme] -> m [(Indexed Name, Indexed Name)]+> validClauses :: Gamma Name -> Name -> Indexed Name ->+>                 [RawScheme] -> IvorM [(Indexed Name, Indexed Name)] > validClauses gam fn ty cs = do >     -- add fn:ty to the context as an axiom >     checkValid gam [] cs@@ -277,8 +342,8 @@ >        checkValid gam acc ((RSch c r):cs) >           = do let app = mkapp (Var fn) c >                case typecheck gam app of->                  Nothing -> checkValid gam acc cs->                  Just (v,t) -> checkValid gam ((v,t):acc) cs+>                  Right (v,t) -> checkValid gam ((v,t):acc) cs+>                  _ -> checkValid gam acc cs   Return true if the given pattern clause is the most specific in a list@@ -310,7 +375,7 @@ Given a raw term, recursively expand all of its arguments which are in constructor form -> expandCon :: Monad m => Gamma Name -> Raw -> m [Raw]+> expandCon :: Gamma Name -> Raw -> IvorM [Raw] > expandCon gam r = do >     let f = getappfun r >     let as = getappargs r

@@ -58,7 +58,7 @@ > -- | Add primitive types for Int, Float and String, and some > -- primitive operations [add,sub,mult,div][int,float] and concat. -> addPrimitives :: Monad m => Context -> m Context+> addPrimitives :: Context -> TTM Context > addPrimitives c = do c <- addPrimitive c (name "Int") >                      c <- addPrimitive c (name "Float") >                      c <- addPrimitive c (name "String")@@ -127,7 +127,7 @@ > parseInt = lexeme $ fmap read (many1 digit)  > -- | Parse a term including primitives-> parsePrimTerm :: Monad m => String -> m ViewTerm+> parsePrimTerm :: String -> TTM ViewTerm > parsePrimTerm str >     = case parse (do t <- pTerm (Just parsePrimitives) ; eof ; return t)  >                  "(input)" str of

@@ -50,9 +50,8 @@ > newShell ctxt = Shell Nothing "> " False ctxt "" [] [] [] Nothing []  > -- | Update the context in a shell-> updateShell :: Monad m =>->                (Context -> m Context) -- ^ Function to update context->                -> ShellState -> m ShellState+> updateShell :: (Context -> TTM Context) -- ^ Function to update context+>                -> ShellState -> TTM ShellState > updateShell fctxt (Shell r p f c resp tacs coms imp ext path) >     = do ctxt <- fctxt c >          return (Shell r p f ctxt resp tacs coms imp ext path)@@ -96,7 +95,7 @@  output st = hPutStr (outputstream st)  outputLn st x = output st (x++"\n") -> runCommand :: (Monad m) => Command -> ShellState -> m ShellState+> runCommand :: Command -> ShellState -> TTM ShellState > runCommand (Def nm tm) st = do let (_, tm') = addImplicit (context st) tm >                                ctxt <- addDef (context st) (name nm) tm' >                                return st { context = ctxt }@@ -148,9 +147,9 @@ >                       return (respondLn st (show (whnf (context st) tm))) > runCommand (Print n) st = do >     case (getDef (context st) (name n)) of->       Just tm -> return (respondLn st (show (view tm)))+>       Right tm -> return (respondLn st (show (view tm))) >       _ -> case (getPatternDef (context st) (name n)) of->             Just (_,pats) -> return (respondLn st (printPats pats))+>             Right (_,pats) -> return (respondLn st (printPats pats)) >             _ -> do tm <- check (context st) n >                     case view tm of >                         (Name TypeCon _) -> return (respondLn st "Type constructor")@@ -297,9 +296,10 @@ >     (resp, ctxt) <- fn arg (context st) >     let st' = st { context = ctxt, response = resp } >     return st'-> process x st = processInput x st+> process x st = do let (Right r) = processInput x st+>                   return r -> processInput :: Monad m => Result Input -> ShellState -> m ShellState+> processInput :: Result Input -> ShellState -> TTM ShellState > processInput (Failure err) st = return $ respondLn st err > processInput (Success (Command cmd)) st = runCommand cmd st > processInput (Success (Tactic goal tac)) st@@ -324,7 +324,7 @@ >  where >   ctxt = context st >   showGoalState :: Goal -> String->   showGoalState g = let (Just gd) = goalData ctxt True g+>   showGoalState g = let (Right gd) = goalData ctxt True g >                         env = bindings gd >                         ty = goalType gd >                         nm = goalName gd in@@ -365,7 +365,7 @@ >        return st  > -- | Send a command directly to a shell-> sendCommand :: Monad m => String -> ShellState -> m ShellState+> sendCommand :: String -> ShellState -> TTM ShellState > sendCommand str st = processInput >                        (parseInput (extensions st) >                                    (gettacs (usertactics st))@@ -383,7 +383,7 @@ >                                    (map fst (usercommands st)) str) $ >                          clearResponse st -> gettacs :: [(String, String -> Goal -> Context -> IO Context)] -> [String]+> gettacs :: [(String, String -> Goal -> Context -> TTM Context)] -> [String] > gettacs = map fst  > -- | Get the install prefix of the library

@@ -126,9 +126,20 @@ >     = do name <- identifier; >          when (name /= nm) $ fail $ show nm ++ " & " ++ show name ++ " do not match" >          args <- many (pNoApp ext)->          lchar '=' ;->          ret <- pTerm ext->          return $ PClause args ret+>          try (pclauseret args ext) <|> pclausewith nm args ext++> pclauseret :: [ViewTerm] -> Maybe (Parser ViewTerm) -> Parser PClause+> pclauseret args ext = do lchar '='+>                          ret <- pTerm ext+>                          return $ PClause args ret++> pclausewith :: String -> [ViewTerm] -> Maybe (Parser ViewTerm) -> Parser PClause+> pclausewith nm args ext = do lchar '|'+>                              scr <- pTerm ext+>                              lchar '{'+>                              pats <- ppatterns nm ext+>                              lchar '}'+>                              return $ PWithClause args scr pats  > ppatterns :: String -> Maybe (Parser ViewTerm) -> Parser Patterns > ppatterns name ext

@@ -23,7 +23,7 @@ >                          context :: !Context, >                          -- | Get reply from last shell command >                          response :: String,->                          usertactics :: forall m.Monad m => [(String, String -> Goal -> Context -> m Context)],+>                          usertactics :: [(String, String -> Goal -> Context -> TTM Context)], >                          usercommands :: [(String, String -> Context -> IO (String, Context))], >                          imported :: [String], >                          extensions :: Maybe (Parser ViewTerm),

@@ -16,6 +16,7 @@ > import Ivor.Tactics as Tactics > import Ivor.Display > import Ivor.Unify+> import Ivor.Errors  > import System.Environment > import Data.List@@ -72,7 +73,7 @@  Take a data type definition and add constructors and elim rule to the context. -> doData :: Monad m => Bool -> IState -> Name -> RawDatatype -> m IState+> doData :: Bool -> IState -> Name -> RawDatatype -> IvorM IState > doData elim st n r = do >            let ctxt = defs st >            dt <- if elim then checkType (defs st) r -- Make iota schemes@@ -110,7 +111,7 @@ >                               ctxt >            return newdefs -> doMkData :: Monad m => Bool -> IState -> Datadecl -> m IState+> doMkData :: Bool -> IState -> Datadecl -> IvorM IState > doMkData elim st (Datadecl n ps rawty cs)  >     = do (gty,_) <- checkIndices (defs st) ps [] rawty >          let ty = forget (normalise (defs st) gty)@@ -129,7 +130,7 @@ >        stripps 0 t = t >        stripps n (RBind _ _ sc) = stripps (n-1) sc -> suspendProof :: Monad m => IState -> m IState+> suspendProof :: IState -> IvorM IState > suspendProof st = do case proofstate st of >                        (Just prf) -> do >                          let olddefs = defs st@@ -144,7 +145,7 @@ >               return $ (x, G (Partial (Ind v) q) (finalise (Ind ty)) defplicit) > suspendFrom _ _ _ = fail "Not a suspendable proof" -> resumeProof :: Monad m => IState -> Name -> m IState+> resumeProof :: IState -> Name -> IvorM IState > resumeProof st n = case (proofstate st) of >      Nothing -> >          case glookup n (defs st) of@@ -170,7 +171,7 @@ e.g. adding z:C x to foo : (x:A)(y:B)Z = [x:A][y:B]H  becomes foo : (x:A)(z:C x)(y:B) = [x:A][z:C x][y:B]H. -> addArg :: Monad m => IState -> Name -> TT Name -> m IState+> addArg :: IState -> Name -> TT Name -> IvorM IState > addArg st n ty = >     case proofstate st of >         Just (Ind (Bind n (B (Guess v) t) sc)) -> do

@@ -17,7 +17,9 @@ >               checkCtxt,converts, >               Ivor.TT.compile, >               -- * Exported view of terms->               module VTerm, IsTerm, IsData,+>               module VTerm, IsTerm, IsData, +>               -- * Errors+>               TTError(..), ttfail, getError, TTM, >               -- * Definitions and Theorems >               addDef,addTypedDef,addData,addDataNoElim, >               addAxiom,declare,declareData,@@ -110,11 +112,13 @@ > import Ivor.Compiler as Compiler > import Ivor.CodegenC > import Ivor.PatternDefs+> import Ivor.Errors  > import Data.List > import Debug.Trace > import Data.Typeable > import Control.Monad(when)+> import Control.Monad.Error(Error,noMsg,strMsg)  > -- | Abstract type representing state of the system. > newtype Context = Ctxt IState@@ -135,7 +139,7 @@  > -- |A tactic is any function which manipulates a term at the given goal > -- binding. Tactics may fail, hence the monad.-> type Tactic = forall m.Monad m => Goal -> Context -> m Context+> type Tactic = Goal -> Context -> TTM Context  > -- | Initialise a context, with no data or definitions and an > -- empty proof state.@@ -144,17 +148,17 @@  > class IsTerm a where >     -- | Typecheck a term->     check :: Monad m => Context -> a -> m Term->     raw :: Monad m => a -> m Raw+>     check :: Context -> a -> TTM Term+>     raw :: a -> TTM Raw  > class IsData a where >     -- Add a data type with case and elim rules an elimination rule->     addData :: Monad m => Context -> a -> m Context+>     addData :: Context -> a -> TTM Context >     addData ctxt x = addData' True ctxt x >     -- Add a data type without an elimination rule->     addDataNoElim :: Monad m => Context -> a -> m Context+>     addDataNoElim :: Context -> a -> TTM Context >     addDataNoElim ctxt x = addData' False ctxt x->     addData' :: Monad m => Bool -> Context -> a -> m Context+>     addData' :: Bool -> Context -> a -> TTM Context  > instance IsTerm Term where >     check _ tm = return tm@@ -175,10 +179,53 @@ > instance IsTerm Raw where >     check (Ctxt st) t = do >        case (typecheck (defs st) t) of->           (Success (t, ty)) -> return $ Term (t,ty)->           (Failure err) -> fail err+>           (Right (t, ty)) -> return $ Term (t,ty)+>           (Left err) -> tt $ ifail err >     raw t = return t +> data TTError = CantUnify ViewTerm ViewTerm+>              | NotConvertible ViewTerm ViewTerm+>              | Message String+>              | Unbound ViewTerm ViewTerm ViewTerm ViewTerm [Name]+>              | NoSuchVar Name+>              | ErrContext String TTError++> instance Show TTError where+>     show (CantUnify t1 t2) = "Can't unify " ++ show t1 ++ " and " ++ show t2+>     show (NotConvertible t1 t2) = show t1 ++ " and " ++ show t2 ++ " are not convertible"+>     show (Message s) = s+>     show (Unbound clause clty rhs rhsty ns) +>        = show ns ++ " unbound in clause " ++ show clause ++ " : " ++ show clty ++ +>                     " = " ++ show rhs+>     show (NoSuchVar n) = "No such name as " ++ show n+>     show (ErrContext c err) = c ++ show err++> instance Error TTError where+>     noMsg = Message "Ivor Error"+>     strMsg s = Message s++> type TTM = Either TTError++> ttfail :: String -> TTM a+> ttfail s = Left (Message s)++> tt :: IvorM a -> TTM a+> tt (Left err) = Left (getError err)+> tt (Right v) = Right v++> getError :: IError -> TTError+> getError (ICantUnify l r) = CantUnify (view (Term (l, Ind TTCore.Star))) (view (Term (r, Ind TTCore.Star)))+> getError (INotConvertible l r) = NotConvertible (view (Term (l, Ind TTCore.Star))) (view (Term (r, Ind TTCore.Star)))+> getError (IMessage s) = Message s+> getError (IUnbound clause clty rhs rhsty names) +>              = Unbound (view (Term (clause, Ind TTCore.Star)))+>                        (view (Term (clty, Ind TTCore.Star)))+>                        (view (Term (rhs, Ind TTCore.Star)))+>                        (view (Term (rhsty, Ind TTCore.Star)))+>                        names+> getError (INoSuchVar n) = NoSuchVar n+> getError (IContext s e) = ErrContext s (getError e)+ > -- | Quickly convert a 'ViewTerm' into a real 'Term'. > -- This is dangerous; you must know that typechecking will succeed, > -- and the resulting term won't have a valid type, but you will be@@ -198,7 +245,7 @@ >             Failure err -> fail err  > instance IsData Inductive where->     addData' elim (Ctxt st) ind = do st' <- doMkData elim st (datadecl ind)+>     addData' elim (Ctxt st) ind = do st' <- tt $ doMkData elim st (datadecl ind) >                                      return (Ctxt st') >       where >         datadecl (Inductive n ps inds cty cons) =@@ -218,6 +265,11 @@ >                         arguments :: [ViewTerm], >                         returnval :: ViewTerm >                        }+>              | PWithClause {+>                         arguments :: [ViewTerm],+>                         scrutinee :: ViewTerm,+>                         patterns :: Patterns+>                            } >    deriving Show  > data Patterns = Patterns [PClause]@@ -225,8 +277,9 @@  > mkRawClause :: PClause -> RawScheme > mkRawClause (PClause args ret) =->     RSch (map forget args) (forget ret)-+>     RSch (map forget args) (RWRet (forget ret))+> mkRawClause (PWithClause args scr (Patterns rest)) = +>     RSch (map forget args) (RWith (forget scr) (map mkRawClause rest))  > -- ^ Convert a term to matchable pattern form; i.e. the only names allowed > -- are variables and constructors. Any arbitrary function application is@@ -239,6 +292,7 @@ >     toPat gam (VTerm.App f a) = case toPat gam f of >                                   Placeholder -> Placeholder >                                   apptm -> VTerm.App f (toPat gam a)+>     toPat gam (Annotation _ a) = toPat gam a >     toPat gam _ = Placeholder >     matchable gam n >        = case lookupval n gam of@@ -257,18 +311,18 @@ > -- 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) =>+> addPatternDef :: (IsTerm ty) => >                Context -> Name -> ty -- ^ Type >                  -> Patterns -- ^ Definition >                -> [PattOpt] -- ^ Options to set which definitions will be accepted->                -> m (Context, [(Name, ViewTerm)])+>                -> TTM (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, newnames, tot) ->                <- checkDef ndefs n inty (map mkRawClause clauses)+>         (pmdefs, newnames, tot) +>               <- tt $ checkDef ndefs n inty (map mkRawClause clauses) >                            (not (elem Ivor.TT.Partial opts)) >                            (not (elem GenRec opts)) >         (ndefs',vnewnames) @@ -281,13 +335,17 @@ >                                                  extend g (n, G Unreducible t 0)) >                                               ndefs newnames >                              return (ngam, vnew)->         newdefs <- gInsert n (G (PatternDef pmdef tot) fty defplicit) ndefs'+>         newdefs <- insertAll pmdefs ndefs' tot >         return (Ctxt st { defs = newdefs }, vnewnames)+>   where insertAll [] gam tot = return gam+>         insertAll ((nm, def, ty):xs) gam tot = +>             do gam' <- gInsert nm (G (PatternDef def tot) ty defplicit) gam+>                insertAll xs gam' tot  > -- |Add a new definition, with its type to the global state. > -- These definitions can be recursive, so use with care.-> addTypedDef :: (IsTerm term, IsTerm ty, Monad m) =>->                Context -> Name -> term -> ty -> m Context+> addTypedDef :: (IsTerm term, IsTerm ty) =>+>                Context -> Name -> term -> ty -> TTM Context > addTypedDef (Ctxt st) n tm ty = do >         checkNotExists n (defs st) >         (Term (inty,_)) <- Ivor.TT.check (Ctxt st) ty@@ -296,7 +354,7 @@ >         let ctxt = defs st >         term <- raw tm >         case (checkAndBind tmp [] term (Just inty)) of->              (Success (v,t@(Ind sc),_)) -> do+>              (Right (v,t@(Ind sc),_)) -> do >                 if (convert (defs st) inty t) >                     then (do >                       checkBound (getNames (Sc sc)) t@@ -304,31 +362,31 @@ >                               -- = Gam ((n,G (Fun [] v) t):ctxt) >                       return $ Ctxt st { defs = newdefs }) >                     else (fail $ "The given type and inferred type do not match, inferred " ++ show t)->              (Failure err) -> fail err+>              (Left err) -> tt $ ifail err   > -- |Add a new definition to the global state.-> addDef :: (IsTerm a, Monad m) => Context -> Name -> a -> m Context+> addDef :: (IsTerm a) => Context -> Name -> a -> TTM Context > addDef (Ctxt st) n tm = do >         checkNotExists n (defs st) >         v <- raw tm >         let ctxt = defs st >         case (typecheck ctxt v) of->             (Success (v,t@(Ind sc))) -> do+>             (Right (v,t@(Ind sc))) -> do >                 checkBound (getNames (Sc sc)) t >                 newdefs <- gInsert n (G (Fun [] v) t defplicit) ctxt >                 -- let newdefs = Gam ((n,G (Fun [] v) t):ctxt) >                 return $ Ctxt st { defs = newdefs }->             (Failure err) -> fail err+>             (Left err) -> tt $ ifail err -> checkBound :: Monad m => [Name] -> (Indexed Name) -> m ()+> checkBound :: [Name] -> (Indexed Name) -> TTM () > checkBound [] t = return () > checkBound (nm@(MN ("INFER",_)):ns) t >                = fail $ "Can't infer value for " ++ show nm ++ " in " ++ show t > checkBound (_:ns) t = checkBound ns t  > -- |Forget a definition and all following definitions.-> forgetDef :: Monad m => Context -> Name -> m Context+> forgetDef :: Context -> Name -> TTM Context > forgetDef (Ctxt st) n = fail "Not any more..."  do let olddefs = defs st@@ -340,8 +398,8 @@  > -- |Add the general recursion elimination rule, thus making all further > -- definitions untrustworthy :).-> addGenRec :: Monad m => Context -> Name -- ^ Name to give recursion rule->                      -> m Context+> addGenRec :: Context -> Name -- ^ Name to give recursion rule+>                      -> TTM Context > addGenRec (Ctxt st) n >     = do checkNotExists n (defs st) >          (Ctxt tmpctxt) <- addAxiom (Ctxt st) n@@ -351,17 +409,17 @@ >          general <- raw $ "[P:*][meth_general:(p:P)P](meth_general (" ++  >                            show n ++ " P meth_general))" >          case (typecheck tmp general) of->              (Success (v,t)) -> do+>              (Right (v,t)) -> do >                 -- let newdefs = Gam ((n,G (Fun [] v) t):ctxt) >                 newdefs <- gInsert n (G (Fun [] v) t defplicit) ctxt >                 let scs = lift n (levelise (normalise (emptyGam) v)) >                 return $ Ctxt st { defs = newdefs }->              (Failure err) -> fail $ "Can't happen (general): "++err+>              (Left err) -> ttfail $ "Can't happen (general): "++ show err  > -- | Add the heterogenous (\"John Major\") equality rule and its reduction-> addEquality :: Monad m => Context -> Name -- ^ Name to give equality type+> addEquality :: Context -> Name -- ^ Name to give equality type >             -> Name -- ^ Name to give constructor->             -> m Context+>             -> TTM Context > addEquality ctxt@(Ctxt st) ty con = do >     checkNotExists ty (defs st) >     checkNotExists con (defs st)@@ -371,7 +429,7 @@ >     rcrule <- eqElimType (show ty) (show con) "Case" >     rischeme <- eqElimSch (show con) >     let rdata = (RData rtycon [rdatacon] 2 rerule rcrule [rischeme] [rischeme])->     st <- doData True st ty rdata+>     st <- tt $ doData True st ty rdata >     return $ Ctxt st  > -- eqElim : (A:*)(a:A)(b:A)(q:JMEq A A a a)@@ -400,21 +458,21 @@ >                     mrefl <- raw "meth_refl" >                     arg <- raw $ refl ++ " A a" >                     ret <- raw "meth_refl"->                     return $ RSch [aty,a,b,arg,phi,mrefl] ret+>                     return $ RSch [aty,a,b,arg,phi,mrefl] (RWRet ret)  > -- | Declare a name which is to be defined later-> declare :: (IsTerm a, Monad m) => Context -> Name -> a -> m Context+> declare :: (IsTerm a) => Context -> Name -> a -> TTM Context > declare ctxt n tm = addUn Undefined ctxt n tm  > -- | Declare a type constructor which is to be defined later-> declareData :: (IsTerm a, Monad m) => Context -> Name -> a -> m Context+> declareData :: (IsTerm a) => Context -> Name -> a -> TTM Context > declareData ctxt@(Ctxt st) n tm = do >   let gamma = defs st >   Term (ty, _) <- Ivor.TT.check ctxt tm >   addUn (TCon (arity gamma ty) NoConstructorsYet) ctxt n tm  > -- | Add a new axiom to the global state.-> addAxiom :: (IsTerm a, Monad m) => Context -> Name -> a -> m Context+> addAxiom :: (IsTerm a) => Context -> Name -> a -> TTM Context > addAxiom ctxt n tm = addUn Unreducible ctxt n tm  > addUn und (Ctxt st) n tm = do@@ -422,18 +480,18 @@ >        t <- raw tm >        let Gam ctxt = defs st >        case (typecheck (defs st) t) of->           (Success (t, ty)) ->->              do checkConv (defs st) ty (Ind TTCore.Star) "Not a type"+>           (Right (t, ty)) ->+>              do tt $ checkConv (defs st) ty (Ind TTCore.Star) (IMessage "Not a type") >                 -- let newdefs = Gam ((n, (G und (finalise t))):ctxt) >                 newdefs <- gInsert n (G und (finalise t) defplicit) (Gam ctxt) >                 return $ Ctxt st { defs = newdefs }->           (Failure err) -> fail err+>           (Left err) -> tt $ ifail err  > -- | Add a new primitive type. This should be done in assocation with > -- creating an instance of 'ViewConst' for the type, and creating appropriate > -- primitive functions.-> addPrimitive :: Monad m => Context -> Name -- ^ Type name->                 -> m Context+> addPrimitive :: Context -> Name -- ^ Type name+>                 -> TTM Context > addPrimitive (Ctxt st) n = do >        checkNotExists n (defs st) >        let Gam ctxt = defs st@@ -444,8 +502,8 @@  > -- | Add a new binary operator on constants. Warning: The type you give > -- is not checked!-> addBinOp :: (ViewConst a, ViewConst b, ViewConst c, IsTerm ty, Monad m) =>->             Context -> Name -> (a->b->c) -> ty -> m Context+> addBinOp :: (ViewConst a, ViewConst b, ViewConst c, IsTerm ty) =>+>             Context -> Name -> (a->b->c) -> ty -> TTM Context > addBinOp (Ctxt st) n f tyin = do >        checkNotExists n (defs st) >        Term (ty, _) <- Ivor.TT.check (Ctxt st) tyin@@ -472,8 +530,8 @@  > -- | Add a new binary function on constants. Warning: The type you give > -- is not checked!-> addBinFn :: (ViewConst a, ViewConst b, IsTerm ty, Monad m) =>->             Context -> Name -> (a->b->ViewTerm) -> ty -> m Context+> addBinFn :: (ViewConst a, ViewConst b, IsTerm ty) =>+>             Context -> Name -> (a->b->ViewTerm) -> ty -> TTM Context > addBinFn (Ctxt st) n f tyin = do >        checkNotExists n (defs st) >        Term (ty, _) <- Ivor.TT.check (Ctxt st) tyin@@ -487,7 +545,7 @@ >              = case cast x of >                   Just x' -> case cast y of >                      Just y' -> case Ivor.TT.check (Ctxt st) $ f x' y' of->                          Just (Term (Ind v,_)) ->+>                          Right (Term (Ind v,_)) -> >                              Just $ nf (emptyGam) (VG []) [] False v >                      Nothing -> Nothing >                   Nothing -> Nothing@@ -497,7 +555,7 @@ >              = case cast x of >                   Just x' -> case cast y of >                      Just y' -> case Ivor.TT.check (Ctxt st) $ f x' y' of->                          Just (Term (Ind v,_)) ->+>                          Right (Term (Ind v,_)) -> >                              Just v >                      Nothing -> Nothing >                   Nothing -> Nothing@@ -507,8 +565,8 @@ > -- | Add a new primitive function on constants, usually used for converting > -- to some form which can be examined in the type theory itself. > -- Warning: The type you give is not checked!-> addPrimFn :: (ViewConst a, IsTerm ty, Monad m) =>->             Context -> Name -> (a->ViewTerm) -> ty -> m Context+> addPrimFn :: (ViewConst a, IsTerm ty) =>+>             Context -> Name -> (a->ViewTerm) -> ty -> TTM Context > addPrimFn (Ctxt st) n f tyin = do >        checkNotExists n (defs st) >        Term (ty, _) <- Ivor.TT.check (Ctxt st) tyin@@ -521,28 +579,28 @@ >          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,_)) ->+>                                  Right (Term (Ind v,_)) -> >                                      Just $ nf (emptyGam) (VG []) [] False v->                                  Nothing -> Nothing+>                                  _ -> Nothing >                   Nothing -> Nothing >          mkfun _ = Nothing >          mktt :: [TT Name] -> Maybe (TT Name) >          mktt [Const x] >               = case cast x of >                   Just x' -> case Ivor.TT.check (Ctxt st) $ f x' of->                                  Just (Term (Ind v,_)) ->+>                                  Right (Term (Ind v,_)) -> >                                      Just v->                                  Nothing -> Nothing+>                                  _ -> Nothing >                   Nothing -> Nothing >          mktt _ = Nothing  > -- | Add a new externally defined function. > -- Warning: The type you give is not checked!-> addExternalFn :: (IsTerm ty, Monad m) =>+> addExternalFn :: (IsTerm ty) => >                  Context -> Name -> Int -- ^ arity >                  -> ([ViewTerm] -> Maybe ViewTerm) -- ^ The function, which must >                     -- accept a list of the right length given by arity.->                  -> ty -> m Context+>                  -> ty -> TTM Context > addExternalFn (Ctxt st) n arity f tyin = do >        checkNotExists n (defs st) >        Term (ty, _) <- Ivor.TT.check (Ctxt st) tyin@@ -557,9 +615,9 @@ >               else case runf xs of >                      Just res -> >                          case (Ivor.TT.check (Ctxt st) res) of->                             Nothing -> Nothing->                             Just (Term (Ind tm, _)) ->+>                             Right (Term (Ind tm, _)) -> >                                 Just $ nf (emptyGam) (VG []) [] False tm+>                             _ -> Nothing >                      Nothing -> Nothing >          mktt :: [TT Name] -> Maybe (TT Name) >          mktt xs@@ -567,9 +625,9 @@ >               else case f (map viewtt xs) of >                      Just res -> >                          case (Ivor.TT.check (Ctxt st) res) of->                             Nothing -> Nothing->                             Just (Term (Ind tm, _)) ->+>                             Right (Term (Ind tm, _)) -> >                                 Just tm+>                             _ -> Nothing >                      Nothing -> Nothing  Using 'Star' here is a bit of a hack; I don't want to export vt from@@ -597,11 +655,11 @@ >                                           (Forall n Placeholder tm)  > -- |Begin a new proof.-> theorem :: (IsTerm a, Monad m) => Context -> Name -> a -> m Context+> theorem :: (IsTerm a) => Context -> Name -> a -> TTM Context > theorem (Ctxt st) n tm = do >        checkNotExists n (defs st) >        rawtm <- raw tm->        (tv,tt) <- tcClaim (defs st) rawtm+>        (tv,tt) <- tt $ tcClaim (defs st) rawtm >        case (proofstate st) of >            Nothing -> do >                       let thm = Tactics.theorem n tv@@ -615,12 +673,12 @@ > -- |Begin a new interactive definition. > -- Actually, just the same as 'theorem' but this version allows you to > -- make recursive calls, which should of course be done with care.-> interactive :: (IsTerm a, Monad m) => Context -> Name -> a -> m Context+> interactive :: (IsTerm a) => Context -> Name -> a -> TTM Context > interactive (Ctxt st) n tm = do >        checkNotExists n (defs st) >        (Ctxt st') <- declare (Ctxt st) n tm >        rawtm <- raw tm->        (tv,tt) <- tcClaim (defs st) rawtm+>        (tv,tt) <- tt $ tcClaim (defs st) rawtm >        case (proofstate st) of >            Nothing -> do >                       let thm = Tactics.theorem n tv@@ -635,19 +693,19 @@ > -- to continue the proof. > suspend :: Context -> Context > suspend (Ctxt st) = case (suspendProof st) of->                        (Just st') -> Ctxt st'->                        Nothing -> Ctxt st+>                        (Right st') -> Ctxt st'+>                        _ -> Ctxt st  > -- |Resume an unfinished proof, suspending the current one if necessary. > -- Fails if there is no such name. Can also be used to begin a > -- proof of an identifier previously claimed as an axiom. > -- Remember that you will need to 'attack' the goal if you are resuming an > -- axiom.-> resume :: Monad m => Context -> Name -> m Context+> resume :: Context -> Name -> TTM Context > resume ctxt@(Ctxt st) n = >     case glookup n (defs st) of >         Just ((Ivor.Nobby.Partial _ _),_) -> do let (Ctxt st) = suspend ctxt->                                                 st' <- resumeProof st n+>                                                 st' <- tt$ resumeProof st n >                                                 return (Ctxt st') >         Just (Unreducible,ty) -> >             do let st' = st { defs = remove n (defs st) }@@ -659,7 +717,7 @@  > -- | Freeze a name (i.e., set it so that it does not reduce) > -- Fails if the name does not exist.-> freeze :: Monad m => Context -> Name -> m Context+> freeze :: Context -> Name -> TTM Context > freeze (Ctxt st) n >      = case glookup n (defs st) of >           Nothing -> fail $ show n ++ " is not defined"@@ -667,7 +725,7 @@  > -- | Unfreeze a name (i.e., allow it to reduce). > -- Fails if the name does not exist.-> thaw :: Monad m => Context -> Name -> m Context+> thaw :: Context -> Name -> TTM Context > thaw (Ctxt st) n >      = case glookup n (defs st) of >           Nothing -> fail $ show n ++ " is not defined"@@ -684,7 +742,7 @@ > clearSaved (Ctxt st) = Ctxt st { undoState = Nothing }  > -- | Restore a saved state; fails if none have been saved.-> restore :: Monad m => Context -> m Context+> restore :: Context -> TTM Context > restore (Ctxt st) = case undoState st of >                        Nothing -> fail "No saved state" >                        (Just st') -> return $ Ctxt st'@@ -719,7 +777,7 @@ >                                          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 :: (IsTerm a) => Context -> Goal -> a -> TTM Term > checkCtxt (Ctxt st) goal tm = >     do rawtm <- raw tm >        prf <- case proofstate st of@@ -729,14 +787,14 @@ >                (Goal x) -> x >                DefaultGoal -> head (holequeue st) >        case (Tactics.findhole (defs st) (Just h) prf holeenv) of->          (Just env) -> do t <- Ivor.Typecheck.check (defs st) env rawtm Nothing+>          (Just env) -> do t <- tt $ Ivor.Typecheck.check (defs st) env rawtm Nothing >                           return $ Term t >          Nothing -> fail "No such goal" >  where holeenv :: Gamma Name -> Env Name -> Indexed Name -> Env Name >        holeenv gam hs _ = Tactics.ptovenv hs  > -- |Evaluate a term in the context of the given goal-> evalCtxt :: (IsTerm a, Monad m) => Context -> Goal -> a -> m Term+> evalCtxt :: (IsTerm a) => Context -> Goal -> a -> TTM Term > evalCtxt (Ctxt st) goal tm = >     do rawtm <- raw tm >        prf <- case proofstate st of@@ -746,7 +804,7 @@ >                (Goal x) -> x >                DefaultGoal -> head (holequeue st) >        case (Tactics.findhole (defs st) (Just h) prf holeenv) of->          (Just env) -> do (tm, ty) <- Ivor.Typecheck.check (defs st) env rawtm Nothing+>          (Just env) -> do (tm, ty) <- tt $ Ivor.Typecheck.check (defs st) env rawtm Nothing >                           let tnorm = normaliseEnv env (defs st) tm >                           return $ Term (tnorm, ty) >          Nothing -> fail "No such goal"@@ -757,8 +815,8 @@ > -- |Check whether the conversion relation holds between two terms, in the > -- context of the given goal -> converts :: (Monad m, IsTerm a, IsTerm b) =>->             Context -> Goal -> a -> b -> m Bool+> converts :: (IsTerm a, IsTerm b) =>+>             Context -> Goal -> a -> b -> TTM Bool > converts ctxt@(Ctxt st) goal a b >     = do atm <- checkCtxt ctxt goal a >          btm <- checkCtxt ctxt goal b@@ -771,21 +829,21 @@ >                (Goal x) -> x >                DefaultGoal -> head (holequeue st) >          case (Tactics.findhole (defs st) (Just h) prf holeenv) of->                (Just env) -> case checkConvEnv env (defs st) av bv "" of->                     Just _ -> return True+>                (Just env) -> case checkConvEnv env (defs st) av bv (IMessage "") of+>                     Right _ -> return True >                     _ -> return False >                Nothing -> fail "No such goal" >  where holeenv :: Gamma Name -> Env Name -> Indexed Name -> Env Name >        holeenv gam hs _ = Tactics.ptovenv hs  > -- |Lookup a definition in the context.-> getDef :: Monad m => Context -> Name -> m Term+> getDef :: Context -> Name -> TTM Term > getDef (Ctxt st) n = case glookup n (defs st) of >                         Just ((Fun _ tm),ty) -> return $ Term (tm,ty) >                         _ -> fail "Not a function name"  > -- |Get the type of a definition in the context.-> getType :: Monad m => Context -> Name -> m Term+> getType :: Context -> Name -> TTM Term > getType (Ctxt st) n = case glookup n (defs st) of >                         Just (_,ty) -> return $ Term (ty,Ind TTCore.Star) >                         _ -> fail "Not a defined name"@@ -799,7 +857,7 @@ > -- | 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 :: Context -> Name -> TTM Inductive > getInductive (Ctxt st) n  >     = case glookup n (defs st) of >         Just (TCon _ (Elims _ _ cons), ty) ->@@ -812,11 +870,11 @@ >         getTyType v = VTerm.getReturnType v >         getConTypes [] = [] >         getConTypes (c:cs) = case getType (Ctxt st) c of->                                Just ty -> (c,view ty):(getConTypes cs)+>                                Right 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 :: Context -> Name -> TTM (ViewTerm, Patterns) > getPatternDef (Ctxt st) n >     = case glookup n (defs st) of >           Just ((PatternDef pmf _),ty) ->@@ -847,7 +905,7 @@ >        = getPD (map fst (getAllTypes ctxt)) >   where getPD [] = [] >         getPD (x:xs) = case (getPatternDef ctxt x) of->                          Just d -> (x,d):(getPD xs)+>                          Right d -> (x,d):(getPD xs) >                          _ -> getPD xs  > -- |Get all the inductive type definitions in the context.@@ -856,22 +914,23 @@ >        = getI (map fst (getAllTypes ctxt)) >   where getI [] = [] >         getI (x:xs) = case (getInductive ctxt x) of->                          Just d -> (x,d):(getI xs)+>                          Right 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+>                       map (\ x -> (x, unRight (getDef ctxt x))) names+>   where unRight (Right r) = r  > -- |Get the names of all of the constructors of an inductive family-> getConstructors :: Monad m => Context -> Name -> m [Name]+> getConstructors :: Context -> Name -> TTM [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 :: Context -> Name -> TTM NameType > nameType (Ctxt st) n  >     = case glookup n (defs st) of >         Just ((DCon _ _), _) -> return DataCon@@ -881,14 +940,14 @@  > -- | 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 :: Context -> Name -> TTM 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 :: Context -> Name -> TTM Int > getConstructorArity (Ctxt st) n >    = case glookup n (defs st) of >        Just ((DCon _ _), Ind ty) -> return (length (getExpected ty))@@ -900,9 +959,9 @@ > data Rule = Case | Elim  > -- | Get the pattern matching elimination rule for a type-> getElimRule :: Monad m => Context -> Name -- ^ Type+> getElimRule :: Context -> Name -- ^ Type >                  -> Rule -- ^ Which rule to get patterns for (case or elim)->                  -> m Patterns+>                  -> TTM Patterns > getElimRule (Ctxt st) nm r = >     case (lookupval nm (defs st)) of >       Just (TCon _ (Elims erule crule cons)) ->@@ -912,7 +971,7 @@ >             elim <- lookupM rule (eliminators st) >             return $ Patterns $ map mkRed (fst $ snd elim) >       Nothing -> fail $ (show nm) ++ " is not a type constructor"->  where mkRed (RSch pats ret) = PClause (map viewRaw pats) (viewRaw ret)+>  where mkRed (RSch pats (RWRet ret)) = PClause (map viewRaw pats) (viewRaw ret) >         -- a reduction will only have variables and applications >        viewRaw (Var n) = Name Free n >        viewRaw (RApp f a) = VTerm.App (viewRaw f) (viewRaw a)@@ -948,7 +1007,7 @@ >                        _ -> True  > -- |Get the current proof term, if we are in the middle of a proof.-> proofterm :: Monad m => Context -> m Term+> proofterm :: Context -> TTM Term > proofterm (Ctxt st) = case proofstate st of >                         Nothing -> fail "No proof in progress" >                         Just (Ind (Bind _ (B (Guess v) t) _)) ->@@ -956,7 +1015,7 @@ >                         Just t -> fail $ "Proof finished; " ++ show t  > -- |Get the type and context of the given goal, if it exists-> getGoal :: Monad m => Context -> Goal -> m ([(Name,Term)], Term)+> getGoal :: Context -> Goal -> TTM ([(Name,Term)], Term) > getGoal (Ctxt st) goal = >     let h = case goal of >                   (Goal x) -> x@@ -989,9 +1048,9 @@   > -- |Get information about a subgoal.-> goalData :: Monad m => Context -> Bool -- ^ Get all bindings (True), or+> goalData :: Context -> Bool -- ^ Get all bindings (True), or >                                        -- just lambda bindings (False)->          -> Goal -> m GoalData+>          -> Goal -> TTM GoalData > goalData (Ctxt st) all goal = case proofstate st of >         Nothing -> fail "No proof in progress" >         (Just prf) ->@@ -1015,7 +1074,7 @@ >        getbs (_:xs) = getbs xs  > -- | Get the names and types of all goals-> subGoals :: Monad m => Context -> m [(Name,Term)]+> subGoals :: Context -> TTM [(Name,Term)] > subGoals (Ctxt st) = case proofstate st of >         Nothing -> fail "No proof in progress" >         (Just prf) -> return $@@ -1023,8 +1082,8 @@ >                         $ Tactics.allholes (defs st) True prf  > -- | Create a name unique in the proof state-> uniqueName :: Monad m => Context -> Name -- ^ Suggested name->            -> m Name -- ^ Unique name based on suggested name+> uniqueName :: Context -> Name -- ^ Suggested name+>            -> TTM Name -- ^ Unique name based on suggested name > uniqueName (Ctxt st) n = case proofstate st of >         Nothing -> fail "No proof in progress" >         (Just (Ind prf)) -> return $ uniqify n $ getBoundNames (Sc prf)@@ -1049,7 +1108,7 @@   > -- |Lift a finished proof into the context-> qed :: Monad m => Context -> m Context+> qed :: Context -> TTM Context > qed (Ctxt st) >     = do case proofstate st of >            Just prf -> do@@ -1066,12 +1125,12 @@ >                   Nothing -> False >                   _ -> True -> qedLift :: Monad m => Gamma Name -> Bool -> Indexed Name ->->                       m (Name, Gval Name)+> qedLift :: Gamma Name -> Bool -> Indexed Name ->+>                       TTM (Name, Gval Name) > qedLift gam freeze >             (Ind (Bind x (B (TTCore.Let v) ty) (Sc (P n)))) | n == x = >     do let (Ind vnorm) = convNormalise (emptyGam) (finalise (Ind v))->        verify gam (Ind v)+>        tt $ verify gam (Ind v) >        return $ (x, G (Fun opts (Ind vnorm)) (finalise (Ind ty)) defplicit) >   where opts = if freeze then [Frozen] else [] > qedLift _ _ tm = fail $ "Not a complete proof " ++ show tm@@ -1140,8 +1199,8 @@  > -- | Apply a sequence of tactics to the default goal. Read the type > -- as ['Tactic'] -> 'Tactic'-> tacs :: Monad m => [Goal -> Context -> m Context] ->->         Goal -> Context -> m Context+> tacs :: [Goal -> Context -> TTM Context] ->+>         Goal -> Context -> TTM Context > tacs [] = idTac > tacs (t:ts) = \g ctxt -> do ctxt <- t g ctxt >                             tacs ts DefaultGoal ctxt@@ -1157,8 +1216,8 @@ >     -> Tactic > try tac success failure goal ctxt = >     case tac goal ctxt of->         Just ctxt' -> success goal ctxt'->         Nothing -> failure goal ctxt+>         Right ctxt' -> success goal ctxt'+>         _ -> failure goal ctxt  > -- | Tries the left tactic, if that fails try the right one. Shorthand for > -- 'try' x 'idTac' y.@@ -1174,7 +1233,7 @@ >                     (Goal x) -> x >                     DefaultGoal -> head (holequeue st) >     let (Just prf) = proofstate st->     (prf', act) <- Tactics.runtactic (defs st) hole prf tac+>     (prf', act) <- tt $ Tactics.runtactic (defs st) hole prf tac >     let st' = addgoals act st >     return $ Ctxt st' { proofstate = Just prf', >                         --holequeue = jumpqueue hole@@ -1233,17 +1292,17 @@ > -- already have a guess attached after refinement, but the guess will not > -- be solved (via 'solve'). > basicRefine :: IsTerm a => a -> Tactic-> basicRefine tm = do rawtm <- raw tm->                     runTac (Tactics.refine rawtm [])+> basicRefine tm ctxt goal = do rawtm <- raw tm+>                               runTac (Tactics.refine rawtm []) ctxt goal  > -- | Solve a goal by applying a function with some arguments filled in. > -- See 'refine' for details. > refineWith :: IsTerm a => a -> [a] -> Tactic > refineWith tm args = (refineWith' tm args >=> trySolve) >+> keepSolving -> refineWith' tm args = do rawtm <- raw tm->                          rawargs <- mapM raw args->                          runTac (Tactics.refine rawtm rawargs)+> refineWith' tm args c g = do rawtm <- raw tm+>                              rawargs <- mapM raw args+>                              runTac (Tactics.refine rawtm rawargs) c g  > -- | Finalise a goal's solution. > solve :: Tactic@@ -1270,8 +1329,8 @@ >    where trySolve [] ctxt = return ctxt >          trySolve (x:xs) ctxt >              = case solve x ctxt of->                   Just ctxt' -> trySolve xs ctxt'->                   Nothing -> trySolve xs ctxt+>                   Right ctxt' -> trySolve xs ctxt'+>                   _ -> trySolve xs ctxt  -- > keepSolving goal ctxt -- >   | not (null (getGoals ctxt)) =@@ -1284,8 +1343,8 @@ > fill :: IsTerm a => a -> Tactic > fill guess = fill' guess >+> keepSolving -> fill' guess = do rawguess <- raw guess->                  runTac (Tactics.fill rawguess)+> fill' guess c g = do rawguess <- raw guess+>                      runTac (Tactics.fill rawguess) c g  > -- | Remove a solution from a goal. > abandon :: Tactic@@ -1343,15 +1402,15 @@ > -- | Check that the goal is definitionally equal to the given term, > -- and rewrite the goal accordingly. > equiv :: IsTerm a => a -> Tactic-> equiv ty = do rawty <- raw ty->               runTac (Tactics.equiv rawty)+> equiv ty c g = do rawty <- raw ty+>                   runTac (Tactics.equiv rawty) c g  > -- | Abstract over the given term in the goal. > generalise :: IsTerm a => a -> Tactic > generalise tm = generalise' tm >-> attack -> generalise' tm = do rawtm <- raw tm->                     runTac (Tactics.generalise rawtm)+> generalise' tm c g = do rawtm <- raw tm+>                         runTac (Tactics.generalise rawtm) c g  > -- | Abstract over the given term in the goal, and also all variables > -- appearing in the goal whose types depend on it.@@ -1379,7 +1438,7 @@ > addArg n ty g ctxt@(Ctxt st) >     = do rawty <- raw ty >          Term (Ind tm, _) <- checkCtxt ctxt g rawty->          st' <- Ivor.State.addArg st n tm+>          st' <- tt $ Ivor.State.addArg st n tm >          return $ Ctxt st'  > -- | Replace a term in the goal according to an equality premise. Any@@ -1396,12 +1455,12 @@ >         -> Bool -- ^ apply premise backwards (i.e. apply symmetry) >         -> Tactic > replace eq repl sym tm flip = replace' eq repl sym tm flip >+> attack-> replace' eq repl sym tm flip =+> replace' eq repl sym tm flip c g = >     do rawtm <- raw tm >        raweq <- raw eq >        rawrepl <- raw repl >        rawsym <- raw sym->        runTac (Tactics.replace raweq rawrepl rawsym rawtm flip)+>        runTac (Tactics.replace raweq rawrepl rawsym rawtm flip) c g  > -- | Add an axiom to the global context which would solve the goal, > -- and apply it.@@ -1444,24 +1503,24 @@ >        -> Tactic > by rule = (by' rule >=> attack) >+> keepSolving -> by' rule = do rawrule <- raw rule->               runTac (Tactics.by rawrule)+> by' rule c g = do rawrule <- raw rule+>                   runTac (Tactics.by rawrule) c g  > -- | Apply the appropriate induction rule to the term. > induction :: IsTerm a => a -- ^ target of the elimination >                -> Tactic > induction tm = (induction' tm >=> attack) >+> keepSolving -> induction' tm = do rawtm <- raw tm->                    runTac (Tactics.casetac True rawtm)+> induction' tm c g = do rawtm <- raw tm+>                        runTac (Tactics.casetac True rawtm) c g  > -- | Apply the appropriate case analysis rule to the term. > -- Like 'induction', but no induction hypotheses generated. > cases :: IsTerm a => a -- ^ target of the case analysis >                -> Tactic > cases tm = (cases' tm >=> attack) >+> keepSolving-> cases' tm = do rawtm <- raw tm->                runTac (Tactics.casetac False rawtm)+> cases' tm c g = do rawtm <- raw tm+>                    runTac (Tactics.casetac False rawtm) c g  > -- | Find a trivial solution to the goal by searching through the context > -- for a premise which solves it immediately by refinement@@ -1489,7 +1548,7 @@ >                       } >   deriving Show -> allowedrec :: Monad m => Goal -> Context -> m [RecAllowed]+> allowedrec :: Goal -> Context -> TTM [RecAllowed] > allowedrec g ctxt = do >     gd <- goalData ctxt False g >     return $ findRec $ bindings gd@@ -1515,11 +1574,11 @@ >                     rec <- {- trace (show allowed) $ -} findRec allowed tm >                     fill rec g ctxt >   where->     findRec :: Monad m => [RecAllowed] -> Raw -> m ViewTerm+>     findRec :: [RecAllowed] -> Raw -> TTM ViewTerm >     findRec [] tm = fail "This recursive call not allowed" >     findRec ((Rec fs nm args hyp):rs) tm = >         case mkRec fs nm args hyp tm of->            Just x -> return x+>            Right x -> return x >            _ -> findRec rs tm >     mkRec fs nm args hyp tm = do >          let (tmf,tmas) = getfa tm []

@@ -1,4 +1,4 @@-> {-# OPTIONS_GHC -fglasgow-exts #-}+> {-# OPTIONS_GHC -fglasgow-exts -XIncoherentInstances #-}  > module Ivor.TTCore where @@ -26,6 +26,7 @@ >     | RCall RComputation Raw >     | RReturn Raw >     | RAnnot String -- Debugging hack+>     | RFileLoc FilePath Int Raw -- For more helpful type error messages >     | RStage RStage  > data RComputation = RComp Name [Raw]@@ -143,19 +144,21 @@ >     | MN (String,Int) >   deriving (Ord, Eq) +> instance Typeable Name where+>     typeOf n = mkTyConApp (mkTyCon "Name") []+ Data declarations and pattern matching - data RawWith = RWith [Raw] -              | RWPatt [Raw]-              | RWNone-   deriving Show+> data RawWith = RWith Raw [RawScheme] -- match with an extra arg, add new schemes+>              | RWRet Raw+>   deriving Show   data With = With [Indexed n]            | WPatt [Pattern n]            | WNone    deriving Show -> data RawScheme = RSch [Raw] {- RawWith -} Raw+> data RawScheme = RSch [Raw] RawWith >   deriving Show  > data Scheme n = Sch [Pattern n] {- With -} (Indexed n)@@ -309,6 +312,12 @@ >                            --if (i<length ctx) then P (ctx!!i) >                              --           else V i) t' +> makePsUniq :: TT Name -> TT Name+> makePsUniq 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" ++ debugTT t))) t'@@ -565,6 +574,11 @@ > getArgs (App f a) = getArgs f ++ [a] > getArgs _ = [] +> getRawArgs :: Raw -> [Raw]+> getRawArgs (RApp f a) = getRawArgs f ++ [a]+> getRawArgs (RFileLoc f l t) = getRawArgs t+> getRawArgs _ = []+ Get the function being applied in an application  > getFun :: TT Name -> TT Name@@ -649,6 +663,7 @@ >     (==) (RStage t) (RStage t') = t == t' >     (==) RInfer RInfer = True >     (==) (RMeta x) (RMeta x') = x == x'+>     (==) (RFileLoc f l t) (RFileLoc _ _ t') = t == t' >     (==) _ _ = False  > instance Eq n => Eq (TT n) where@@ -726,7 +741,7 @@ >       fPrec _ (RStar) = "*" >       fPrec _ (RInfer) = "_" >       fPrec _ (RMeta n) = "?"++forget n->       fPrec _ (RAnnot t) = t+>       fPrec p (RFileLoc f l t) = fPrec p t >       bracket outer inner str | inner>outer = "("++str++")" >                               | otherwise = str @@ -746,11 +761,54 @@ > instance Show n => Forget (Levelled n) Raw where >     forget (Lev t) = forget t -> instance Show n => Forget (TT n) Raw where+> instance (Show Name) => Forget (TT Name) Raw where >     forget t = forgetTT (vapp showV t) >      where >        showV (ctx,i) | i < length ctx = P (ctx!!i) >	               | otherwise = V i+>        forgetTT (P x) = case (cast x) of+>                           Just (MN ("INFER",i)) -> RInfer+>                           _ -> Var $ UN (show x)+>        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)) =+>                    (RBind (UN (show n)) (B Lambda (forget t)) (forget sc))+>        forgetTT (Bind n (B Pi t) (Sc sc)) =+>                    (RBind (UN (show n)) (B Pi (forget t)) (forget sc))+>        forgetTT (Bind n (B MatchAny t) (Sc sc)) =+>                    (RBind (UN (show n)) (B MatchAny (forget t)) (forget sc))+>        forgetTT (Bind n (B (Let v) t) (Sc sc)) =+>                    (RBind (UN (show n)) (B (Let (forget v)) (forget t))+>                      (forget sc))+>        forgetTT (Bind n (B Hole t) (Sc sc)) =+>                    (RBind (UN (show n)) (B Hole (forget t)) (forget sc))+>        forgetTT (Bind n (B (Guess v) t) (Sc sc)) =+>                    (RBind (UN (show n)) (B (Guess (forget v)) (forget t))+>                      (forget sc))+>        forgetTT (Bind n (B (Pattern v) t) (Sc sc)) =+>                    (RBind (UN (show n)) (B (Pattern (forget v)) (forget t))+>                      (forget sc))+>        forgetTT (Proj n i t) = RAnnot $ (show t)++"!"++(show i)++":"++show n+>        forgetTT (Label t (Comp n cs)) = RLabel (forgetTT t)+>                                          (RComp (UN $ show n)+>                                             (map forgetTT cs))+>        forgetTT (Call (Comp n cs) t) = RCall (RComp (UN $ show n)+>                                               (map forgetTT cs))+>                                                 (forgetTT t)+>        forgetTT (Return t) = RReturn (forgetTT t)+>        forgetTT (Stage t) = RStage (forget t)+>        forgetTT (Const x) = RConst x+>        forgetTT Star = RStar++> instance (Show n) => Forget (TT n) Raw where+>     forget t = forgetTT (vapp showV t)+>      where+>        showV (ctx,i) | i < length ctx = P (ctx!!i)+>	               | otherwise = V i >        forgetTT (P x) = Var $ UN (show x) >        forgetTT (V i) = RAnnot $ "v" ++ (show i) >        forgetTT (Con t x i) = Var $ UN (show x)@@ -802,15 +860,19 @@ > mkapp f (x:xs) = mkapp (RApp f x) xs  > getargnames (RBind n _ sc) = n:(getargnames sc)+> getargnames (RFileLoc _ _ t) = getargnames t > getargnames _ = []  > getappargs (RApp f a) = getappargs f ++ [a]+> getappargs (RFileLoc _ _ t) = getappargs t > getappargs _ = []  > getappfun (RApp f a) = getappfun f+> getappfun (RFileLoc _ _ t) = getappfun t > getappfun x = x  > getrettype (RBind n (B Pi _) sc) = getrettype sc+> getrettype (RFileLoc _ _ t) = getrettype t > getrettype x = x  > nameOccurs x (Var n) | x == n = True@@ -823,6 +885,7 @@ > nameOccurs x (RCall comp r)  = nameOccurs x r || occComp x comp > nameOccurs x (RReturn r) = nameOccurs x r > nameOccurs x (RStage s) = occStage x s+> nameOccurs x (RFileLoc f l t) = nameOccurs x t > nameOccurs x _ = False  > occComp x (RComp _ rs) = or $ map (nameOccurs x) rs@@ -833,6 +896,9 @@ > occStage x (REval r) = nameOccurs x r > occStage x (REscape r) = nameOccurs x r +> fileLine (RFileLoc f l t) = Just (f,l)+> fileLine (RBind n b sc) = fileLine sc+> fileLine _ = Nothing  > debugTT t = show (forgetTT (vapp showV t)) >      where

@@ -7,6 +7,7 @@ > import Ivor.Nobby > import Ivor.Gadgets > import Ivor.Unify+> import Ivor.Errors  > import Data.List > import Data.Maybe@@ -27,10 +28,8 @@ >                   | HideGoal Name >    deriving (Show,Eq) -> type Tactic = Monad m => Gamma Name ->->                          Env Name ->->                          Indexed Name ->->                          m (Indexed Name, [TacticAction])+> type Tactic = Gamma Name -> Env Name ->+>               Indexed Name -> IvorM (Indexed Name, [TacticAction])  > type HoleFn a = Gamma Name -> Env Name -> Indexed Name -> a @@ -91,8 +90,8 @@  Typecheck a term in the context of the given hole -> holecheck :: Monad m => Name -> Gamma Name -> Indexed Name ->->              Raw -> m (Indexed Name, Indexed Name)+> holecheck :: Name -> Gamma Name -> Indexed Name ->+>              Raw -> IvorM (Indexed Name, Indexed Name) > holecheck n gam state raw = case (findhole gam (Just n) state docheck) of >                                Nothing -> fail "No such hole binder" >                                (Just x) -> x@@ -108,12 +107,12 @@  FIXME: Why not use a state monad for the unified variables in rt? -> runtactic :: Monad m => Gamma Name -> Name ->->              Indexed Name -> Tactic -> m (Indexed Name, [TacticAction])+> runtactic :: Gamma Name -> Name ->+>              Indexed Name -> Tactic -> IvorM (Indexed Name, [TacticAction]) > runtactic gam n t tac = runtacticEnv gam [] n t tac -> runtacticEnv :: Monad m => Gamma Name -> Env Name -> Name ->->                 Indexed Name -> Tactic -> m (Indexed Name, [TacticAction])+> runtacticEnv :: Gamma Name -> Env Name -> Name ->+>                 Indexed Name -> Tactic -> IvorM (Indexed Name, [TacticAction]) > runtacticEnv gam env n (Ind s) tactic = >     do (tm, actions) <- (rt env s) >        return ((Ind (substNames (mapMaybe mkUnify actions) tm)), actions)@@ -164,7 +163,7 @@  Tactics by default don't need to return the other holes they solved. -> tacret :: Monad m => Indexed Name -> m (Indexed Name, [TacticAction])+> tacret :: Indexed Name -> IvorM (Indexed Name, [TacticAction]) > tacret x = return (x,[])  Sequence two tactics@@ -179,8 +178,8 @@ > attempt :: Tactic -> Tactic > attempt tac gam env tm = >     case tac gam env tm of->        Just (tm',act) -> return (tm',act)->        Nothing -> tacret tm+>        Right (tm',act) -> return (tm',act)+>        _ -> tacret tm  Create a new theorem ?x:S. x @@ -198,7 +197,7 @@ > claim :: Name -> Raw -> Tactic -- ?Name:Type. > claim x s gam env (Ind t) = >     do (Ind sv, st) <- check gam (ptovenv env) s Nothing->        checkConv gam st (Ind Star) "Type of claim must be *"+>        checkConv gam st (Ind Star) (IMessage "Type of claim must be *") >        return $ (Ind (Bind x (B Hole (makePsEnv (map fst env) sv)) (Sc t)), >                      [NextGoal x]) @@ -238,8 +237,8 @@ >        let fty = finalise (Ind ty) >        others <- -- trace ("unifying "++show gt++" and "++show ty') $ >                  case unifyenv (emptyGam) (ptovenv env) fgt fty' of->                     Nothing -> unifyenv gam (ptovenv env) fgt fty->                     (Just x) -> return x+>                     Left _ -> unifyenv gam (ptovenv env) fgt fty+>                     (Right x) -> return x >        -- let newgt = substNames others gt >        -- let newgv = substNames others gv >        let newgv = gv@@ -583,7 +582,7 @@ >     do (Ind goalv,Ind goalt) <- check gam (ptovenv env) goal Nothing >        let goalvin = makePsEnv (map fst env) goalv >        checkConvEnv env gam (Ind goalv) (finalise (Ind ty))->                         "Not equivalent to the Goal"+>                         (IMessage "Not equivalent to the Goal") >        tacret $ Ind (Bind x (B Hole goalvin) sc) > equiv _ _ _ (Ind (Bind x _ _)) = fail $ "equiv: " ++ show x ++ " Not a hole" > equiv _ _ _ _ = fail "equiv: Not a binder, can't happen"

@@ -1,7 +1,7 @@ > {-# OPTIONS_GHC -fglasgow-exts #-}  > module Ivor.Typecheck(typecheck, tcClaim,->                       check, checkAndBind, checkAndBindPair,+>                       check, checkAndBind, checkAndBindWith, checkAndBindPair, >                       convert, >                       checkConv, checkConvEnv, pToV, pToV2, >                       verify, Gamma) where@@ -11,6 +11,7 @@ > import Ivor.Nobby > import Ivor.Unify > import Ivor.Constant+> import Ivor.Errors  > import Control.Monad.State > import Data.List@@ -31,16 +32,14 @@   convert g x y = trace ((show (normalise g x)) ++ " & " ++ (show (normalise g y))) $ (normalise g x)==(normalise g y) -> checkConv :: Monad m => Gamma Name -> Indexed Name -> Indexed Name -> ->              String -> m ()+> checkConv :: Gamma Name -> Indexed Name -> Indexed Name -> IError -> IvorM () > checkConv g x y err = if convert g x y then return ()->	                 else fail err+>	                 else ifail err -> checkConvEnv :: Monad m => Env Name -> Gamma Name -> ->                 Indexed Name -> Indexed Name -> ->              String -> m ()+> checkConvEnv :: Env Name -> Gamma Name -> Indexed Name -> Indexed Name -> +>                 IError -> IvorM () > checkConvEnv env g x y err = if convertEnv env g x y then return ()->                              else fail err+>                              else ifail err   *****@@ -60,18 +59,18 @@ Top level typechecking function - takes a context and a raw term, returning a pair of a term and its type -> typecheck :: Monad m => Gamma Name -> Raw -> m (Indexed Name,Indexed Name)+> typecheck :: Gamma Name -> Raw -> IvorM (Indexed Name,Indexed Name) > typecheck gamma term = do t <- check gamma [] term Nothing >			    return t -> typecheckAndBind :: Monad m => Gamma Name -> Raw -> ->                     m (Indexed Name,Indexed Name, Env Name)+> typecheckAndBind :: Gamma Name -> Raw -> +>                     IvorM (Indexed Name,Indexed Name, Env Name) > typecheckAndBind gamma term = checkAndBind gamma [] term Nothing  Check a term, and return well typed terms with explicit names (i.e. no de Bruijn indices) -> tcClaim :: Monad m => Gamma Name -> Raw -> m (Indexed Name,Indexed Name)+> tcClaim :: Gamma Name -> Raw -> IvorM (Indexed Name,Indexed Name) > tcClaim gamma term = do (Ind t, Ind v) <- check gamma [] term Nothing >			    {-trace (show t) $-} >                         return (Ind (makePs t), Ind (makePs v))@@ -85,30 +84,39 @@ >      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->      -- also a string explaining where the constraint came from->      [(Env Name, Indexed Name, Indexed Name, String)],+>      -- also the context of where the constraint came from+>      [(Env Name, Indexed Name, Indexed Name, Maybe FileContext)], >      -- Metavariables we've introduce to define later->      [Name])+>      [Name],+>      Maybe FileContext)  > type Level = Int +> data FileContext = FC FilePath Int+>   deriving Eq++> errCtxt :: Maybe FileContext -> IError -> IError+> errCtxt (Just (FC f l)) err = IContext (f ++ ":" ++ show l ++ ":") err+> errCtxt _ err = err++> errCtxtCS :: CheckState -> IError -> IError+> errCtxtCS (_,_,_,_,_,fc) err = errCtxt fc err+ Finishes up type checking by making a substitution from all the conversion constraints and applying it to the term and type. -> doConversion :: Monad m =>->                 Raw -> Gamma Name ->->                 [(Env Name, Indexed Name, Indexed Name,String)] ->+> doConversion :: Raw -> Gamma Name ->+>                 [(Env Name, Indexed Name, Indexed Name,Maybe FileContext)] -> >                 Indexed Name -> Indexed Name -> ->                m (Indexed Name, Indexed Name)+>                 IvorM (Indexed Name, Indexed Name) > doConversion raw gam constraints (Ind tm) (Ind ty) = >     -- trace ("Finishing checking " ++ show tm ++ " with " ++ show (length constraints) ++ " equations") $  >           -- 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 let cs = nub constraints->          (subst, nms) <- {-# SCC "name" #-}->                          mkSubst $ (map (\x -> (True,x)) cs)->                                    ++ (map (\x -> (False,x)) (reverse cs))+>          (subst, nms) <- mkSubst $ (map (\x -> (True,x)) cs) +++>                                    (map (\x -> (False,x)) (reverse cs)) >          let tm' = papp subst tm >          let ty' = papp subst ty >          return (Ind tm',Ind ty')@@ -119,14 +127,14 @@ >             = do acc' <- mkSubstQ acc q >                  mkSubst' acc' xs >->          mkSubstQ (s',nms) (ok, (env,Ind x,Ind y,msg))+>          mkSubstQ (s',nms) (ok, (env,Ind x,Ind y,fc)) >             = do -- (s',nms) <- mkSubst xs >                  let x' = papp s' x >                  let (Ind y') = normalise gam (Ind (papp s' y))->                  uns <- {-# SCC "substUnify" #-}+>                  uns <-  >                         case unifyenvErr ok gam env (Ind x') (Ind y') of->                           Success x' -> return x'->                           Failure err -> fail err+>                           Right x' -> return x'+>                           Left err -> ifail (errCtxt fc err)                           Failure err -> fail $ err ++"\n" ++ show nms ++"\n" ++ show constraints -- $ -} ++ " Can't convert "++show x'++" and "++show y' ++ "\n" ++ show constraints ++ "\n" ++ show nms @@ -142,50 +150,83 @@ >          delta n ty n' | n == n' = ty >                        | otherwise = P n' -> check :: Monad m => Gamma Name -> Env Name -> Raw -> Maybe (Indexed Name) -> ->          m (Indexed Name, Indexed Name)+> check :: Gamma Name -> Env Name -> Raw -> Maybe (Indexed Name) -> +>          IvorM (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'' -> checkAndBind :: Monad m => Gamma Name -> Env Name -> Raw -> +> checkAndBind :: Gamma Name -> Env Name -> Raw ->  >                 Maybe (Indexed Name) -> ->                 m (Indexed Name, Indexed Name, Env Name)+>                 IvorM (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',ty') <- doConversion tm gam convs v t->    return (v',ty',e)+>    ((v,t), (next,inf,e,convs,_,_)) <- lvlcheck 0 True 0 gam env tm mty+>    (v'@(Ind vtm),t') <- doConversion tm gam convs v t -- (normalise gam t1') +>    return (v',t',e)  +Check a pattern and an intermediate computation together++> checkAndBindWith :: Gamma Name -> Raw -> Raw -> Name ->+>                     IvorM (Indexed Name, Indexed Name, Indexed Name, Indexed Name, Env Name)+> checkAndBindWith gam tm1 tm2 root = do+>    ((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' <- renameB gam realNames (renameBinders e)+>    (v1', t1') <- fixupGam gam realNames (v1, t1)+>    (v1''@(Ind vtm),t1'') <- doConversion tm1 gam bs v1' t1' -- (normalise gam t1') +>    -- Drop names out of e' that don't appear in v1'' as a result of the+>    -- unification.+>    let namesbound = getNames (Sc vtm)+>    let ein = orderEnv (filter (\ (n, ty) -> n `elem` namesbound) e')+>    ((v2,t2), (_, _, e'', bs',metas,_)) <- lvlcheck 0 inf next gam ein tm2 Nothing+>    (v2',t2') <- doConversion tm2 gam bs' v2 t2 -- (normalise gam t2) +>    let retEnv = reverse (ein ++ e'')+>    if (null metas) +>       then return (v1',t1',v2',t2',retEnv)+>       else fail "Can't have metavariables here"++>  where mkNames 0 = []+>        mkNames n+>           = ([],Ind (P (MN ("INFER",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+ 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, +> checkAndBindPair :: Gamma Name -> Raw -> Raw -> +>                     IvorM (Indexed Name, Indexed 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' <- renameB gam realNames (renameBinders e) >    (v1', t1') <- fixupGam gam realNames (v1, t1)->    (v1''@(Ind vtm),t1'') <- {-# SCC "convert1" #-}doConversion tm1 gam bs v1' t1' -- (normalise gam t1') +>    (v1''@(Ind vtm),t1'') <- doConversion tm1 gam bs v1' t1' -- (normalise gam t1')  >    -- Drop names out of e' that don't appear in v1'' as a result of the >    -- unification. >    let namesbound = getNames (Sc vtm) >    let ein = orderEnv (filter (\ (n, ty) -> n `elem` namesbound) e')->    ((v2,t2), (_, _, e'', bs',metas)) <- {- trace ("Checking " ++ show tm2 ++ " has type " ++ show t1') $ -} {-# SCC "pairLvlCheck" #-} lvlcheck 0 inf next gam ein tm2 (Just t1')->    (v2',t2') <- {-# SCC "convert2" #-} doConversion tm2 gam bs' v2 t2 -- (normalise gam t2) +>    ((v2,t2), (_, _, e'', bs',metas,_)) <- {- trace ("Checking " ++ show tm2 ++ " has type " ++ show t1') $ -} lvlcheck 0 inf next gam ein tm2 (Just t1')+>    (v2',t2') <- doConversion tm2 gam bs' v2 t2 -- (normalise gam t2) +>    let retEnv = reverse (ein ++ e'') >    if (null metas) ->       then return (v1',t1',v2',t2',e'', [])+>       then return (v1',t1',v2',t2',retEnv, []) >       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)+>               return (v1',t1',Ind v2'',t2',retEnv, map (\ (x,y) -> (x, (normalise gam (Ind y)))) newdefs)                 if (null newdefs) then                    else trace (traceConstraints bs') $ return (v1',t1',Ind v2'',t2',e'', map (\ (x,y) -> (x, Ind y)) newdefs)@@ -193,7 +234,7 @@ >  where mkNames 0 = [] >        mkNames n >           = ([],Ind (P (MN ("INFER",n-1))), ->                 Ind (P (MN ("T",n-1))), "renaming"):(mkNames (n-1))+>                 Ind (P (MN ("T",n-1))), IMessage "renaming"):(mkNames (n-1)) >        renameBinders [] = [] >        renameBinders (((MN ("INFER",n)),b):bs)  >                         = ((MN ("T",n),b):(renameBinders bs))@@ -233,34 +274,32 @@  > inferName n = (MN ("INFER", n)) -> lvlcheck :: Monad m => Level -> Bool -> Int -> +> lvlcheck :: Level -> Bool -> Int ->  >             Gamma Name -> Env Name -> Raw ->  >             Maybe (Indexed Name) -> ->             m ((Indexed Name, Indexed Name), CheckState)+>             IvorM ((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, [], [], [], Nothing)  >  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 ,mvs) <- get+>     (next, infer, bindings, errs ,mvs, fc) <- get >     -- First, insert inferred values into the term >     tm'@(_,tmty) <- fixup errs tm >     -- Then check the resulting type matches the expected type. >     if infer then (case exp of >              Nothing -> return ()->              Just expty -> checkConvSt env gamma expty tmty ->                               $ "Expected type and inferred type do not match: " ->                               ++ show expty ++ " and " ++ show tmty)+>              Just expty -> checkConvSt env gamma expty tmty ) >       else return () >     -- Then fill in any remained inferred values we got by knowing the >     -- expected type->     (next, infer, bindings, errs, mvs) <- get+>     (next, infer, bindings, errs, mvs, fc) <- get >     tm <- fixup errs tm >     -- bindings <- fixupB gamma errs bindings->     put (next, infer, bindings, errs, mvs)+>     put (next, infer, bindings, errs, mvs, fc) >     return tm'  >  tcfixup env lvl t exp = do@@ -268,10 +307,10 @@ >     -- case exp of >     --   Nothing -> return () >     --   Just expt -> checkConvSt env gamma expt tmty "Type error"->     (next, infer, bindings, errs, mvs) <- get+>     (next, infer, bindings, errs, mvs, fc) <- get >     tm' <- fixup errs tm >     bindings <- (fixupB gamma errs) $! bindings->     put (next, infer, bindings, errs, mvs)+>     put (next, infer, bindings, errs, mvs, fc) >     return tm'  tc has state threaded through -- state is a tuple of the next name to@@ -279,13 +318,13 @@ will later be unified).  Needs an explicit type to help out ghc's typechecker... ->  tc :: Monad m => Env Name -> Level -> Raw -> Maybe (Indexed Name) ->->                   StateT CheckState m (Indexed Name, Indexed Name)+>  tc :: Env Name -> Level -> Raw -> Maybe (Indexed Name) ->+>        StateT CheckState IvorM (Indexed Name, Indexed Name) >  tc env lvl (Var n) exp = do >        (rv, rt) <- mkTT (lookupi n env 0) (glookup n gamma) >        case exp of >           Nothing -> return (rv,rt)->           Just expt -> do checkConvSt env gamma rt expt $ "Type error"+>           Just expt -> do checkConvSt env gamma rt expt >                           return (rv,rt)  >    where mkTT (Just (i, B _ t)) _ = return (Ind (P n), Ind t)@@ -305,13 +344,13 @@ >          lookupi x (_:xs) i = lookupi x xs (i+1)  >          defaultResult = do->              (next, infer, bindings, errs, mvs) <- get+>              (next, infer, bindings, errs, mvs, fc) <- 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, mvs)+>                        Nothing -> lift $ ifail (errCtxt fc (INoSuchVar n))+>                        Just (Ind t) -> do put (next, infer, (n, B Pi t):bindings, errs, mvs, fc) >                                           return (Ind (P n), Ind t)->                 else fail $ "No such name as " ++ show n+>                 else lift $ ifail (errCtxt fc (INoSuchVar n))  >  tc env lvl (RApp f a) exp = do >     (Ind fv, Ind ft) <- tcfixup env lvl f Nothing@@ -324,11 +363,11 @@ >          let sty = (normaliseEnv env emptyGam (Ind s)) >          let tt = (Bind (MN ("x",0)) (B (Let av) at) (Sc t)) >          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+>          checkConvSt env gamma (Ind at) (Ind s) >          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))->          checkConvSt env gamma (Ind at) (Ind s) $ "Type error: " ++ show a ++ " : " ++ show at ++ ", expected type "++show s -- ++" "++show env+>          checkConvSt env gamma (Ind at) (Ind s) >          let tt = (Bind (MN ("x",0)) (B (Let av) at) (Sc t)) >          let tt' = (normaliseEnv env gamma (Ind tt)) >          return (Ind (App fv av), (normaliseEnv env gamma (Ind tt)))@@ -336,10 +375,14 @@ >     return (rv,rt) >     case exp of >        Nothing -> return (rv,rt)->        Just expt -> do checkConvSt env gamma rt expt $ "Type error"+>        Just expt -> do checkConvSt env gamma rt expt >                        return (rv,rt)->  tc env lvl (RConst x) _ = tcConst x+>  tc env lvl (RConst x) _ = lift $ tcConst x >  tc env lvl RStar _ = return (Ind Star, Ind Star)+>  tc env lvl (RFileLoc f l t) exp = +>     do (next, infer, bindings, errs, mvs, fc) <- get+>        put (next, infer, bindings, errs, mvs, Just (FC f l))+>        tc env lvl t exp  Pattern bindings are a special case since they may bind several names, and we don't convert names to de Bruijn indices@@ -382,8 +425,7 @@ >     case expnf of >       (Ind (Label lt comp)) -> do >          (Ind tv, Ind tt) <- tcfixup env lvl t (Just (Ind lt))->          checkConvSt env gamma (Ind lt) (Ind tt) $ ->             "Type error: " ++ show tt ++", expected type " ++ show lt+>          checkConvSt env gamma (Ind lt) (Ind tt) >          return (Ind (Return tv), Ind (Label tt comp)) >       _ -> fail $ "return " ++ show t++ " should give a label, got " ++ show expnf >  tc env lvl (RReturn t) Nothing = fail $ "Need to know the type to return for "++show t@@ -391,11 +433,11 @@ >          (Ind sv, Ind st) <- tcStage env lvl s exp >          return (Ind sv, Ind st) >  tc env lvl RInfer (Just (Ind exp)) = do ->                       (next, infer, bindings, errs, mvs) <- get+>                       (next, infer, bindings, errs, mvs, fc) <- get >                       let bindings' = if infer  >                                        then (inferName next, B Pi exp):bindings >                                        else bindings->                       put (next+1, infer, bindings', errs, mvs)+>                       put (next+1, infer, bindings', errs, mvs, fc) >                       return (Ind (P (inferName next)), Ind exp) >  tc env lvl RInfer Nothing = fail "Can't infer a term for placeholder" @@ -404,8 +446,8 @@ the expected type.  >  tc env lvl (RMeta n) (Just (Ind exp)) ->     = do (next, infer, bindings, errs, mvs) <- get->          put (next, infer, bindings, errs, n:mvs)+>     = do (next, infer, bindings, errs, mvs, fc) <- get+>          put (next, infer, bindings, errs, n:mvs, fc) >          -- Abstract it over the environment so that we have everything >          -- in scope we need. >          tm <- abstractOver (orderEnv env) n exp []@@ -422,8 +464,8 @@  >  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)+>     = do (next, infer, bindings, errs, mvs, fc) <- get+>          put (next+1, infer, bindings, errs, mvs, fc) >          -- let guessty = Bind (MN ("X", 0)) (B Pi (P (inferName next))) >          --                 (Sc (P (inferName (next+1)))) >          let guessty = (P (inferName next))@@ -465,7 +507,7 @@  >  fixup e tm = fixupGam gamma e tm ->  tcConst :: (Monad m, Constant c) => c -> m (Indexed Name, Indexed Name)+>  tcConst :: (Constant c) => c -> IvorM (Indexed Name, Indexed Name) >  tcConst c = return (Ind (Const c), Ind (constType c))   tcConst Star = return (Ind (Const Star), Ind (Const Star)) --- *:* is a bit dodgy...@@ -498,10 +540,7 @@ >     (Ind tv,Ind tt) <- tcfixup env lvl t (Just (Ind Star)) >     (Ind vv,Ind vt) <- tcfixup env lvl v (Just (Ind tv)) >     let ttnf = normaliseEnv env gamma (Ind tt)->     checkConvEnv env gamma (Ind vt) (Ind tv) $ ->        show vt ++ " and " ++ show tv ++ " are not convertible\n" ++ ->             dbg (normaliseEnv env gamma (Ind vt)) ++ "\n" ++->             dbg (normaliseEnv env gamma (Ind tv)) ++ "\n"+>     lift $ checkConvEnv env gamma (Ind vt) (Ind tv) (INotConvertible (Ind vt) (Ind tv)) >     case ttnf of >       (Ind Star) -> return (B (Let vv) tv) >       _ -> fail $ "The type of the binder " ++ show n ++ " must be *"@@ -517,8 +556,7 @@ >     (Ind tv,Ind tt) <- tcfixup env lvl t Nothing >     (Ind vv,Ind vt) <- tcfixup env lvl v Nothing >     let ttnf = normaliseEnv env gamma (Ind tt)->     checkConvEnv env gamma (Ind vt) (Ind tv) $ ->        show vt ++ " and " ++ show tv ++ " are not convertible"+>     lift $ checkConvEnv env gamma (Ind vt) (Ind tv) (INotConvertible (Ind vt) (Ind tv)) >     case ttnf of >       (Ind Star) -> return (B (Guess vv) tv) >       _ -> fail $ "The type of the binder " ++ show n ++ " must be *"@@ -528,11 +566,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, mvs) <- get->     put (next, True, bindings, err, mvs)+>     (next, infer, bindings, err, mvs, fc) <- get+>     put (next, True, bindings, err, mvs, fc) >     (Ind patv,Ind patt) <- tcfixup (bindings++env) lvl pat Nothing->     (next, _ ,bindings, err, mvs) <- get->     put (next, infer, bindings, err, mvs)+>     (next, _ ,bindings, err, mvs, fc) <- get+>     put (next, infer, bindings, err, mvs, fc) >     let ttnf = normaliseEnv env gamma (Ind tt) >     --checkConvEnv env gamma (Ind patt) (Ind tv) $  >     --   show patt ++ " and " ++ show tv ++ " are not convertible"@@ -578,16 +616,16 @@ -- > checkPatt gam env acc RInfer ty = return (combinepats acc PTerm, env) -- > checkPatt gam env _ _ _ = fail "Invalid pattern" -> checkConvSt env g x y msg->                 = do (next, infer, bindings, err, mvs) <- get->                      put (next, infer, bindings, (env,x,y,msg):err, mvs)+> checkConvSt env g x y+>                 = do (next, infer, bindings, err, mvs, fc) <- get+>                      put (next, infer, bindings, (env,x,y,fc):err, mvs, fc) >                      return ()  > fixupGam gamma [] tm = return tm > 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++")"+>                 Right x' -> return x'+>                 Left err -> return [] -- fail err -- $ "Can't convert "++show x++" and "++show y ++ " ("++show err++")" >      let tm' = fixupNames gamma uns tm >      let ty' = fixupNames gamma uns ty >      fixupGam gamma xs (Ind tm', Ind ty')@@ -621,18 +659,15 @@ > 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]) - discharge :: Monad m =>-              Gamma Name -> Name -> Binder (TT Name) -> -	       (Scope (TT Name)) -> (Scope (TT Name)) ->-	       m (Indexed Name, Indexed Name)-+> discharge :: Gamma Name -> Name -> Binder (TT Name) -> +>	       (Scope (TT Name)) -> (Scope (TT Name)) ->+>	       StateT CheckState IvorM (Indexed Name, Indexed Name) > discharge gamma n (B Lambda t) scv sct = do >    let lt = Bind n (B Pi t) sct >    let lv = Bind n (B Lambda t) scv >    return (Ind lv,Ind lt) > discharge gamma n (B Pi t) scv (Sc sct) = do->    checkConvSt [] gamma (Ind Star) (Ind sct) $ ->       "The scope of a Pi binding must be a type"+>    checkConvSt [] gamma (Ind Star) (Ind sct) >    let lt = Star >    let lv = Bind n (B Pi t) scv >    return (Ind lv,Ind lt)@@ -644,26 +679,26 @@ >    let lt = sct -- already checked sct and t are convertible >    let lv = Bind n (B Hole t) scv >    -- A hole can't appear in the type of its scope, however.->    checkNotHoley 0 sct+>    lift $ checkNotHoley 0 sct >    return (Ind lv,Ind lt) > discharge gamma n (B (Guess v) t) scv (Sc sct) = do >    let lt = sct -- already checked sct and t are convertible >    let lv = Bind n (B (Guess v) t) scv >    -- A hole can't appear in the type of its scope, however.->    checkNotHoley 0 sct+>    lift $ checkNotHoley 0 sct >    return (Ind lv,Ind lt) > discharge gamma n (B (Pattern v) t) scv (Sc sct) = do >    let lt = sct -- already checked sct and t are convertible >    let lv = Bind n (B (Pattern v) t) scv >    -- A hole can't appear in the type of its scope, however.->    checkNotHoley 0 sct+>    lift $ checkNotHoley 0 sct >    return (Ind lv,Ind lt) > discharge gamma n (B MatchAny t) scv (Sc sct) = do >    let lt = sct >    let lv = Bind n (B MatchAny t) scv >    return (Ind lv,Ind lt) -> checkNotHoley :: Monad m => Int -> TT n -> m ()+> checkNotHoley :: Int -> TT n -> IvorM () > checkNotHoley i (V v) | v == i = fail "You can't put a hole where a hole don't belong." > checkNotHoley i (App f a) = do checkNotHoley i f >                                checkNotHoley i a@@ -700,11 +735,11 @@ > pToV2 v p (Const x) = Sc (Const x) > pToV2 v p Star = Sc Star -> checkR g t = (typecheck g t):: (Result (Indexed Name, Indexed Name)) + checkR g t = (typecheck g t):: (Result (Indexed Name, Indexed Name))   If we're paranoid - recheck a supposedly well-typed term. Might want to do this after finishing a proof. -> verify :: Monad m => Gamma Name -> Indexed Name -> m ()+> verify :: Gamma Name -> Indexed Name -> IvorM () > verify gam tm = do (_,_) <- typecheck gam (forget tm) >                    return ()

@@ -4,6 +4,7 @@  > import Ivor.Nobby > import Ivor.TTCore+> import Ivor.Errors  > import Data.List @@ -16,24 +17,20 @@ Unify on named terms, but normalise using de Bruijn indices. (I hope this doesn't get too confusing...) -> unify :: Monad m =>->          Gamma Name -> Indexed Name -> Indexed Name -> m Unified+> unify :: Gamma Name -> Indexed Name -> Indexed Name -> IvorM Unified > unify gam x y = unifyenv gam [] (finalise x) (finalise y) -> unifyenv :: Monad m =>->             Gamma Name -> Env Name ->->             Indexed Name -> Indexed Name -> m Unified+> unifyenv :: Gamma Name -> Env Name ->+>             Indexed Name -> Indexed Name -> IvorM Unified > unifyenv = unifyenvErr False -> unifyenvCollect :: Monad m =>->                    Gamma Name -> Env Name ->->                    Indexed Name -> Indexed Name -> m Unified+> unifyenvCollect :: Gamma Name -> Env Name ->+>                    Indexed Name -> Indexed Name -> IvorM Unified > unifyenvCollect = unifyenvErr True -> unifyenvErr :: Monad m =>->                Bool -> -- Ignore errors+> unifyenvErr :: Bool -> -- Ignore errors >                Gamma Name -> Env Name ->->                Indexed Name -> Indexed Name -> m Unified+>                Indexed Name -> Indexed Name -> IvorM Unified > -- For the sake of readability of the results, first attempt to unify > -- without reducing, and reduce if that doesn't work. > -- Also, there is no point reducing if we don't have to, and not calling@@ -45,9 +42,9 @@ >                                    show (p (normalise (gam' gam) x))) $-} >     case unifynferr i env (p x) >                           (p y) of->           (Just x) -> return x->           Nothing -> unifynferr i env (p (normalise (gam' gam) x))->                                       (p (normalise (gam' gam) y))+>           (Right x) -> return x+>           _ -> 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) @@ -58,21 +55,18 @@ >     = insertGam n (G (Fun [] (Ind v)) (Ind ty) defplicit) (envToGamHACK xs) > envToGamHACK (_:xs) = envToGamHACK xs -> unifynf :: Monad m =>->            Env Name -> Indexed Name -> Indexed Name -> m Unified+> unifynf :: Env Name -> Indexed Name -> Indexed Name -> IvorM Unified > unifynf = unifynferr True  Collect names which do unify, and ignore errors -> unifyCollect :: Monad m =>->            Env Name -> Indexed Name -> Indexed Name -> m Unified+> unifyCollect :: Env Name -> Indexed Name -> Indexed Name -> IvorM Unified > unifyCollect = unifynferr False  > sentinel = [(MN ("HACK!!",0), P (MN ("HACK!!",0)))] -> unifynferr :: Monad m =>->               Bool -> -- Ignore errors->               Env Name -> Indexed Name -> Indexed Name -> m Unified+> unifynferr :: Bool -> -- Ignore errors+>               Env Name -> Indexed Name -> Indexed Name -> IvorM Unified > unifynferr ignore env topx@(Ind x) topy@(Ind y) >                = do acc <- un env env x y [] >                     if ignore then return () else checkAcc acc@@ -96,7 +90,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+>                               else ifail $ ICantUnify (Ind x) (Ind y) >             where funify (P x) (P y) >                       | x==y = True >                       | otherwise = hole envl x || hole envl y@@ -113,8 +107,7 @@ >          un envl envr (Stage x) (Stage y) acc = unst envl envr x y acc >          un envl envr x y acc >                     | x == y || ignore = return acc->                     | otherwise = fail $ "Can't unify " ++ show x ++->                                          " and " ++ show y ++ " in " ++ show (topx,topy)+>                     | otherwise = ifail $ ICantUnify (Ind x) (Ind y) >          unb envl envr (B b ty) (B b' ty') acc = >              do acc' <- unbb envl envr b b' acc >                 un envl envr ty ty' acc'@@ -125,7 +118,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+>                        else fail $ "Can't unify binders " ++ show x ++ " and " ++ show y  >          unst envl envr (Quote x) (Quote y) acc = un envl envr x y acc >          unst envl envr (Code x) (Code y) acc = un envl envr x y acc@@ -133,8 +126,7 @@ >          unst envl envr (Escape x _) (Escape y _) acc = un envl envr x y acc >          unst envl envr x y acc = >                   if ignore then return acc->                       else fail $ "Can't unify " ++ show (Stage x) ++->                                " and " ++ show (Stage y)+>                       else ifail $ ICantUnify (Ind (Stage x)) (Ind (Stage y))  >          hole env x | (Just (B Hole ty)) <- lookup x env = True >                     | otherwise = isInferred x@@ -146,8 +138,7 @@ >              | (Just tm') <- lookup n xs >                  = if (ueq tm tm')  -- Take account of names! == no good. >                       then checkAcc xs->                       else fail $ "Can't unify " ++ show tm ++->                                   " and " ++ show tm'+>                       else ifail $ ICantUnify (Ind tm) (Ind tm') >              | otherwise = checkAcc xs  >          loc x xs = loc' 0 x xs@@ -160,14 +151,14 @@  >          ueq :: TT Name -> TT Name -> Bool >          ueq x y = case unifyenv emptyGam [] (Ind x) (Ind y) of->                   Just _ -> True+>                   Right _ -> True >                   _ -> False  Grr!  > ueq :: Gamma Name -> TT Name -> TT Name -> Bool > ueq gam x y = case unifyenv gam [] (Ind x) (Ind y) of->                   Just _ -> True+>                   Right _ -> True >                   _ -> False  

@@ -15,7 +15,7 @@ > module Ivor.ViewTerm(-- * Variable names >                        Name,name,displayName,NameType(..),mkVar, >                        -- * Terms->                        Term(..), ViewTerm(..), apply,+>                        Term(..), ViewTerm(..), Annot(..), apply, >                        view, viewType, ViewConst, typeof,  >                        freeIn, namesIn, occursIn, subst, getApp,  >                        Ivor.ViewTerm.getFnArgs,@@ -75,8 +75,12 @@ >     | Eval { evalterm :: ViewTerm } -- ^ Staging annotation >     | Escape { escapedterm :: ViewTerm } -- ^ Staging annotation >     | Placeholder+>     | Annotation { annotation :: Annot,+>                    term :: ViewTerm } -- ^ additional annotations >     | Metavar { var :: Name } +> data Annot = FileLoc FilePath Int -- ^ source file, line number+ > instance Eq ViewTerm where >     (==) (Name _ x) (Name _ y) = x == y >     (==) (Ivor.ViewTerm.App f a) (Ivor.ViewTerm.App f' a') = f == f' && a == a'@@ -97,6 +101,7 @@ >     (==) (Ivor.ViewTerm.Code t) (Ivor.ViewTerm.Code t') = t==t' >     (==) (Ivor.ViewTerm.Eval t) (Ivor.ViewTerm.Eval t') = t==t' >     (==) (Ivor.ViewTerm.Escape t) (Ivor.ViewTerm.Escape t') = t==t'+>     (==) (Annotation _ t) (Annotation _ t') = t == t' >     (==) _ _ = False  > -- | Haskell types which can be used as constants@@ -139,6 +144,7 @@ >     forget (Ivor.ViewTerm.Code t) = RStage (RCode (forget t)) >     forget (Ivor.ViewTerm.Eval t) = RStage (REval (forget t)) >     forget (Ivor.ViewTerm.Escape t) = RStage (REscape (forget t))+>     forget (Annotation (FileLoc f l) t) = RFileLoc f l (forget t) >     forget x = Var (var x)  > instance Show ViewTerm where@@ -220,6 +226,7 @@ >    fi n (Ivor.ViewTerm.Code t) = fi n t >    fi n (Ivor.ViewTerm.Eval t) = fi n t >    fi n (Ivor.ViewTerm.Escape t) = fi n t+>    fi n (Annotation _ t) = fi n t >    fi n _ = False  > -- | Return the names occurring free in a term@@ -238,6 +245,7 @@ >    fi ns (Ivor.ViewTerm.Code t) = fi ns t >    fi ns (Ivor.ViewTerm.Eval t) = fi ns t >    fi ns (Ivor.ViewTerm.Escape t) = fi ns t+>    fi ns (Annotation _ t) = fi ns t >    fi ns _ = []  > -- | Return whether a subterm occurs in a (first order) term.@@ -253,27 +261,32 @@ >    fi n (Ivor.ViewTerm.Code t) = fi n t >    fi n (Ivor.ViewTerm.Eval t) = fi n t >    fi n (Ivor.ViewTerm.Escape t) = fi n t+>    fi n (Annotation _ t) = fi n t >    fi n x = n == x  > -- | Get the function from an application. If no application, returns the > -- entire term. > getApp :: ViewTerm -> ViewTerm > getApp (Ivor.ViewTerm.App f a) = getApp f+> getApp (Annotation _ t) = getApp t > 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 (Annotation _ t) = getFnArgs t > 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 (Annotation _ t) = getArgTypes t > 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 (Annotation _ t) = Ivor.ViewTerm.getReturnType t > getReturnType x = x  > dbgshow (UN n) = "UN " ++ show n@@ -289,6 +302,8 @@ >   m' (Ivor.ViewTerm.App f a) (Ivor.ViewTerm.App f' a') acc  >       = do acc' <- m' f f' acc >            m' a a' acc'+>   m' (Annotation _ t) t' acc = m' t t' acc+>   m' t (Annotation _ t') acc = m' t t' acc >   m' x y acc | x == y = return acc >              | otherwise = fail $"Mismatch " ++ show x ++ " and " ++ show y @@ -328,5 +343,6 @@ >           = Ivor.ViewTerm.Eval (subst n v r) > subst n v (Ivor.ViewTerm.Escape r)  >           = Ivor.ViewTerm.Escape (subst n v r)+> subst n v (Annotation a t) = Annotation a (subst n v t) > subst n v t = t 

@@ -211,4 +211,4 @@              (comint-send-input))))   (goto-char (point-min))) -(provide 'ivor)+(provide 'ivor-mode)

@@ -1,5 +1,5 @@ Name:		ivor-Version:	0.1.8+Version:	0.1.9 Author:		Edwin Brady License:	BSD3 License-file:	LICENSE@@ -58,7 +58,7 @@   -Build-depends:  base, parsec, mtl, directory+Build-depends:  base >=3 && <5, parsec, mtl, directory Build-type:     Simple  Extensions:     MultiParamTypeClasses, FunctionalDependencies,@@ -76,5 +76,5 @@ 		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.RunTT, Ivor.Compiler, Ivor.Prefix, Ivor.Errors, 		Ivor.PatternDefs,  Ivor.ShellState, Ivor.Scopecheck