Skip to content
Browse files

Changed internal errors from String to IError

Ignore-this: 3559f070d67c06b258cde572c911e867

darcs-hash:20090715153049-228f4-9aaabe19ec23aa60f1445fb18c5acd244944ccc9.gz
  • Loading branch information...
1 parent 2f36338 commit d5b3720c3df9d65e40e5f5cf5d6c5c8cf10160b2 eb committed Jul 15, 2009
Showing with 149 additions and 161 deletions.
  1. +4 −4 Ivor/Datatype.lhs
  2. +2 −1 Ivor/Errors.lhs
  3. +15 −15 Ivor/PatternDefs.lhs
  4. +6 −5 Ivor/State.lhs
  5. +31 −28 Ivor/TT.lhs
  6. +16 −17 Ivor/Tactics.lhs
  7. +53 −60 Ivor/Typecheck.lhs
  8. +22 −31 Ivor/Unify.lhs
View
8 Ivor/Datatype.lhs
@@ -5,6 +5,7 @@
> import Ivor.Typecheck
> import Ivor.Nobby
> import Ivor.PatternDefs
+> import Ivor.Errors
> import Debug.Trace
@@ -52,7 +53,7 @@ checkType checks a raw data type, with its elimination rule and iota
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)
@@ -66,7 +67,7 @@ the context and an executable elimination rule.
> 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,8 +97,7 @@ foo p0 p1 ... pn = t
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 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
View
3 Ivor/Errors.lhs
@@ -6,8 +6,9 @@
> import Control.Monad.Error
> data IError = ICantUnify (Indexed Name) (Indexed Name)
+> | INotConvertible (Indexed Name) (Indexed Name)
> | IMessage String
-> deriving Show
+> deriving (Show, Eq)
> instance Error IError where
> noMsg = IMessage "Ivor Error"
View
30 Ivor/PatternDefs.lhs
@@ -7,6 +7,7 @@
> import Ivor.Nobby
> import Ivor.Typecheck
> import Ivor.Unify
+> import Ivor.Errors
> import Debug.Trace
> import Data.List
@@ -19,10 +20,10 @@ 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 ([(Name, 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")]])
@@ -67,11 +68,10 @@ of which arguments are well-founded
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 ()
@@ -175,18 +175,18 @@ names bound in patterns) then type check the right hand side.
Each clause may generate auxiliary definitions, so return all definitons created.
-> matchClauses :: Monad m => Gamma Name -> Name -> [PMRaw] -> Raw -> Indexed Name ->
+> matchClauses :: Gamma Name -> Name -> [PMRaw] -> Raw -> Indexed Name ->
> Bool -> -- Check coverage
> [(Indexed Name, Indexed Name)] ->
-> m ([(Name, PMFun Name, Indexed Name)], [(Name, Indexed Name)], Bool)
+> 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, 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
> let pmdef = map (mkScheme gam) checkpats
> let arity = length (getExpected ty')
@@ -305,7 +305,7 @@ cases in the second argument. Each of the necessary cases in 'covering'
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
@@ -325,24 +325,24 @@ fails, reporting which case isn't matched, if patterns don't cover.
> 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
> where checkValid gam acc [] = return acc
> 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
@@ -374,7 +374,7 @@ Return true if the given pattern clause is the most specific in a list
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
View
11 Ivor/State.lhs
@@ -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 @@ compiled terms, etc.
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 @@ Take a data type definition and add constructors and elim rule to the context.
> 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 @@ Take a data type definition and add constructors and elim rule to the context.
> 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 @@ Take a data type definition and add constructors and elim rule to the context.
> 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 @@ And an argument to the current proof (after any dependencies)
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
View
59 Ivor/TT.lhs
@@ -179,15 +179,17 @@
> 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
> 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
> instance Error TTError where
@@ -196,15 +198,16 @@
> type TTM = Either TTError
-> ttfail :: TTError -> TTM a
-> ttfail = Left
+> 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
> -- | Quickly convert a 'ViewTerm' into a real 'Term'.
@@ -226,7 +229,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) =
@@ -302,7 +305,7 @@
> inty <- raw ty
> let (Patterns clauses) = pats
> (pmdefs, newnames, tot)
-> <- checkDef ndefs n inty (map mkRawClause clauses)
+> <- tt $ checkDef ndefs n inty (map mkRawClause clauses)
> (not (elem Ivor.TT.Partial opts))
> (not (elem GenRec opts))
> (ndefs',vnewnames)
@@ -334,15 +337,15 @@
> 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
> newdefs <- gInsert n (G (Fun [Recursive] v) t defplicit) ctxt
> -- = Gam ((n,G (Fun [] v) t):ctxt)
> return $ Ctxt st { defs = newdefs })
> else (fail $ "The given type and inferred type do not match, inferred " ++ show t)
-> (Failure err) -> fail err
+> (Left err) -> tt $ ifail err
> -- |Add a new definition to the global state.
@@ -352,12 +355,12 @@
> 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 :: [Name] -> (Indexed Name) -> TTM ()
> checkBound [] t = return ()
@@ -389,12 +392,12 @@ do let olddefs = defs st
> 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 :: Context -> Name -- ^ Name to give equality type
@@ -409,7 +412,7 @@ do let olddefs = defs st
> 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)
@@ -460,12 +463,12 @@ do let olddefs = defs st
> 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
@@ -639,7 +642,7 @@ intuitive)
> 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
@@ -658,7 +661,7 @@ intuitive)
> 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
@@ -673,8 +676,8 @@ intuitive)
> -- 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
@@ -685,7 +688,7 @@ intuitive)
> 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) }
@@ -767,7 +770,7 @@ Give a parseable but ugly representation of a term.
> (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
@@ -784,7 +787,7 @@ Give a parseable but ugly representation of a term.
> (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"
@@ -809,8 +812,8 @@ Give a parseable but ugly representation of a term.
> (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
@@ -1110,7 +1113,7 @@ Tactics
> 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
@@ -1213,7 +1216,7 @@ Convert an internal tactic into a publicly available tactic.
> (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
@@ -1418,7 +1421,7 @@ FIXME: Choose a sensible name here
> 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
View
33 Ivor/Tactics.lhs
@@ -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 @@ new axiom to the context.
> | 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 @@ no guesses attached (False).
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 @@ the term. Oh well.]
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 @@ FIXME: Why not use a state monad for the unified variables in rt?
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 @@ Try to run a tactic, do nothing silently if it fails.
> 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 @@ Add a new claim to the current state
> 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 @@ Try filling the current goal with a term
> 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 @@ Replace a goal with an equivalent (convertible) goal.
> 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"
View
113 Ivor/Typecheck.lhs
@@ -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 @@ syntactic.
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 @@ so....
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))
@@ -86,7 +85,7 @@ type.
> 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)],
+> [(Env Name, Indexed Name, Indexed Name, IError)],
> -- Metavariables we've introduce to define later
> [Name])
@@ -95,11 +94,10 @@ type.
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,IError)] ->
> 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
@@ -125,8 +123,8 @@ constraints and applying it to the term and type.
> let (Ind y') = normalise gam (Ind (papp s' y))
> uns <-
> case unifyenvErr ok gam env (Ind x') (Ind y') of
-> Success x' -> return x'
-> Failure err -> fail err
+> Right x' -> return x'
+> Left err -> ifail 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,16 +140,16 @@ constraints and applying it to the term and type.
> 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'' <- 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), (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')
@@ -160,8 +158,8 @@ constraints and applying it to the term and type.
Check a pattern and an intermediate computation together
-> checkAndBindWith :: Monad m => Gamma Name -> Raw -> Raw -> Name ->
-> m (Indexed Name, Indexed Name, Indexed Name, Indexed Name, Env Name)
+> 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,
@@ -195,8 +193,8 @@ 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
@@ -226,7 +224,7 @@ Return a list of the functions we need to define to complete the definition.
> 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))
@@ -266,10 +264,10 @@ if (all (\e -> envLT x e) (y:ys))
> 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, [], [], [])
> where
@@ -285,8 +283,8 @@ Do the typechecking, then unify all the inferred terms.
> 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)
+> $ IMessage ("Expected type and inferred type do not match: "
+> ++ show expty ++ " and " ++ show tmty))
> else return ()
> -- Then fill in any remained inferred values we got by knowing the
> -- expected type
@@ -312,13 +310,13 @@ generate, the stage we're at, and a list of conversion errors (which
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 $ (IMessage "Type error")
> return (rv,rt)
> where mkTT (Just (i, B _ t)) _ = return (Ind (P n), Ind t)
@@ -357,21 +355,21 @@ typechecker...
> 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) $ IMessage ("Type error in application of " ++ show fv ++ " : " ++ show a ++ " : " ++ show at ++ ", expected type "++show sty ++ " " ++ show tmty)
> return (Ind (App fv av), tmty)
> (_, (Ind (Bind _ (B Pi s) (Sc t)))) -> do
> (Ind av,Ind at) <- tcfixup env lvl a (Just (Ind s))
-> 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) $ IMessage ("Type error: " ++ show a ++ " : " ++ show at ++ ", expected type "++show s) -- ++" "++show env
> 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)))
> _ -> fail $ "Cannot apply a non function type " ++ show ft ++ " to " ++ show a
> 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 (IMessage "Type error")
> 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)
Pattern bindings are a special case since they may bind several names,
@@ -416,7 +414,7 @@ and we don't convert names to de Bruijn indices
> (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
+> IMessage ("Type error: " ++ show tt ++", expected type " ++ show lt)
> 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
@@ -498,7 +496,7 @@ Insert inferred values into the term
> 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...
@@ -531,10 +529,8 @@ Insert inferred values into the term
> (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 *"
@@ -550,8 +546,7 @@ Insert inferred values into the term
> (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 *"
@@ -619,8 +614,8 @@ extended environment.
> 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')
@@ -654,18 +649,16 @@ extended environment.
> 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"
+> IMessage "The scope of a Pi binding must be a type"
> let lt = Star
> let lv = Bind n (B Pi t) scv
> return (Ind lv,Ind lt)
@@ -677,26 +670,26 @@ extended environment.
> 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
@@ -733,11 +726,11 @@ extended environment.
> 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 ()
View
53 Ivor/Unify.lhs
@@ -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 @@ Unify on named terms, but normalise using de Bruijn indices.
> 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 @@ Make the local environment something that Nobby knows about. Very hacky...
> = 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 @@ Collect names which do unify, and ignore errors
> 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 @@ Collect names which do unify, and ignore errors
> 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,16 +118,15 @@ Collect names which do unify, and ignore errors
> 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 unifer 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
> unst envl envr (Eval x _) (Eval y _) acc = un envl envr x y acc
> 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 @@ Collect names which do unify, and ignore errors
> | (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 @@ TMP HACK! ;)
> 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

0 comments on commit d5b3720

Please sign in to comment.
Something went wrong with that request. Please try again.