Permalink
Browse files

Is there any more fail fail?

  • Loading branch information...
1 parent 5a77f8c commit c91de6057814eee2c4bbcaca58c44ac5c4360411 Edwin Brady committed Apr 4, 2011
Showing with 38 additions and 12 deletions.
  1. +4 −1 Ivor/Evaluator.lhs
  2. +17 −0 Ivor/PMComp.lhs
  3. +7 −1 Ivor/TTCore.lhs
  4. +9 −9 Ivor/Typecheck.lhs
  5. +1 −1 Ivor/Unify.lhs
View
@@ -2,7 +2,7 @@
> module Ivor.Evaluator(eval_whnf, eval_nf, eval_nf_env,
> eval_nf_without, eval_nf_limit,
-> eval_nfEnv, tidyNames) where
+> tidyNames) where
> import Ivor.TTCore
> import Ivor.Gadgets
@@ -27,6 +27,8 @@
> eval_nf gam (Ind tm) = let res = makePs (evaluate True gam tm Nothing Nothing Nothing)
> in finalise (Ind res)
+ eval_nf gam (Ind tm) = Ind (evaluate True gam tm Nothing Nothing Nothing)
+
> eval_nf_env :: Env Name -> Gamma Name -> Indexed Name -> Indexed Name
> eval_nf_env env g t
> = eval_nf (addenv env g) t
@@ -163,6 +165,7 @@ Code Stack Env Result
> sc' <- eval nms sc [] ((n',ty,P tmpname):env) pats
> let newsc = pToV tmpname sc'
> u' <- unload ev (Bind n' (B b ty) newsc) [] pats env
+> --trace ("SCOPE: " ++ show (sc, newsc, env, debugTT u', debugTT (buildenv env u'))) $
> return $ buildenv env u'
> | otherwise
> = do let n' = uniqify' n (allNames [] env pats)
View
@@ -47,6 +47,23 @@ this. Let's just make it work first...)
> (Cons cons):(partition ctxt rest)
> partition ctxt x = error "Can't happen PMComp partition"
+Make sure the variables bound have proper pattern names (to avoid embarrassing
+clashes)
+
+> pnames :: [Name] -> TSimpleCase Name -> TSimpleCase Name
+> pnames ns (TSCase tm alts) = TSCase (pnamestm ns tm) (map (pnamesalt ns) alts)
+> pnames ns (TTm tm) = TTm (pnamestm ns tm)
+> pnames ns x = x
+
+> pnamestm :: [Name] -> TT Name -> TT Name
+> pnamestm [] tm = tm
+> pnamestm (x:xs) tm = substName x (P (PN x)) (Sc (pnamestm xs tm))
+
+> pnamesalt ns (TAlt c t args sc)
+> = TAlt c t (map PN args) (pnames (ns++args) sc)
+> pnamesalt ns (TConstAlt c sc) = TConstAlt c (pnames ns sc)
+> pnamesalt ns (TDefault sc) = TDefault (pnames ns sc)
+
> doCaseComp :: Gamma Name ->
> [Clause] -> State CS ([Name], TSimpleCase Name)
> doCaseComp ctxt cs = do vs <- newVars cs
View
@@ -148,7 +148,7 @@ fallthrough when a function is known to be total, and ErrorCase otherwise.
> | TTm (TT n)
> | TErrorCase
> | TImpossible
-> deriving Eq
+> deriving (Show, Eq)
> data TCaseAlt n = TAlt n Int [n] (TSimpleCase n)
> | forall c. Constant c => TConstAlt c (TSimpleCase n)
@@ -175,6 +175,11 @@ a pain...
> (==) (TConstAlt _ _) (TDefault _) = False
> (==) (TDefault _) _ = False
+> instance Show n => Show (TCaseAlt n) where
+> show (TAlt c t ns sc) = "Case " ++ show c ++ " " ++ show ns ++ " " ++ show sc
+> show (TConstAlt c sc) = "Constant " ++ show sc
+> show (TDefault sc) = "Default " ++ show sc
+
UN covers names defined by users, MN covers names invented by the system.
This keeps both namespaces separate.
@@ -1007,6 +1012,7 @@ Some handy gadgets for Raw terms
> forgetTT (Stage (Escape t _)) = RStage (REscape (forgetTT t))
> forgetTT (Const x) = RConst x
> forgetTT Erased = RInfer
+> forgetTT x = RInfer
> pToV :: Eq n => n -> (TT n) -> (Scope (TT n))
> pToV = pToV2 0
View
@@ -476,7 +476,7 @@ and we don't convert names to de Bruijn indices
> else bindings
> put (next+1, infer, bindings', errs, mvs, fc)
> return (Ind (P (inferName next)), Ind exp)
-> tc env lvl RInfer Nothing = fail "Can't infer a term for placeholder"
+> tc env lvl RInfer Nothing = lift $ tacfail "Can't infer a term for placeholder"
If we have a metavariable, we need to record the type of the expression which
will solve it. It needs to take the environment as arguments, and return
@@ -518,23 +518,23 @@ fail $ "Don't know the expected type of " ++ show n
> let ttnf = normaliseEnv env gamma (Ind tt)
> case ttnf of
> (Ind Star) -> return (Ind (Stage (Code tv)), Ind Star)
-> _ -> fail $ "Type of code " ++ show t ++ " must be *"
+> _ -> lift $ tacfail $ "Type of code " ++ show t ++ " must be *"
> tcStage env lvl (REval t) _ = do
> -- when (lvl/=0) $ fail $ "Can't eval at level " ++ show lvl
> (Ind tv, Ind tt) <- tc env lvl t Nothing
> let ttnf = normaliseEnv env gamma (Ind tt)
> case ttnf of
> (Ind (Stage (Code tcode))) ->
> return (Ind (Stage (Eval tv tt)), Ind tcode)
-> _ -> fail $ "Can't eval a non-quoted term (type " ++ show ttnf ++ ")"
+> _ -> lift $ tacfail $ "Can't eval a non-quoted term (type " ++ show ttnf ++ ")"
> tcStage env lvl (REscape t) _ = do
> -- when (lvl==0) $ fail $ "Can't escape at level " ++ show lvl
> (Ind tv, Ind tt) <- tc env lvl t Nothing
> let ttnf = normaliseEnv env gamma (Ind tt)
> case ttnf of
> (Ind (Stage (Code tcode))) ->
> return (Ind (Stage (Escape tv tt)), Ind tcode)
-> _ -> fail "Can't escape a non-quoted term"
+> _ -> lift $ tacfail "Can't escape a non-quoted term"
> checkComp env lvl (RComp n ts) = do
> tsc <- mapM (\ t -> tcfixup env lvl t Nothing) ts
@@ -561,7 +561,7 @@ Insert inferred values into the term
> case ttnf of
> (Ind Star) -> return (B Lambda tvnf)
> (Ind (P (MN ("INFER",_)))) -> return (B Lambda tvnf)
-> _ -> fail $ "The type of the binder " ++ show n ++ " must be *"
+> _ -> lift $ tacfail $ "The type of the binder " ++ show n ++ " must be *"
> checkbinder gamma env lvl n (B Pi t) = do
> (Ind tv,Ind tt) <- tcfixup env lvl t (Just (Ind Star))
> let (Ind tvnf) = eval_nf_env env gamma (Ind tv)
@@ -586,23 +586,23 @@ Insert inferred values into the term
> lift $ checkConvEnv env gamma (Ind vt) (Ind tv) (INotConvertible (Ind vt) (Ind tv))
> case ttnf of
> (Ind Star) -> return (B (Let vv) tv)
-> _ -> fail $ "The type of the binder " ++ show n ++ " must be *"
+> _ -> lift $ tacfail $ "The type of the binder " ++ show n ++ " must be *"
> where dbg (Ind t) = debugTT t
> checkbinder gamma env lvl n (B Hole t) = do
> (Ind tv,Ind tt) <- tcfixup env lvl t Nothing
> let ttnf = normaliseEnv env gamma (Ind tt)
> case ttnf of
> (Ind Star) -> return (B Hole tv)
-> _ -> fail $ "The type of the binder " ++ show n ++ " must be *"
+> _ -> lift $ tacfail $ "The type of the binder " ++ show n ++ " must be *"
> checkbinder gamma env lvl n (B (Guess v) t) = do
> (Ind tv,Ind tt) <- tcfixup env lvl t Nothing
> (Ind vv,Ind vt) <- tcfixup env lvl v Nothing
> let ttnf = normaliseEnv env gamma (Ind tt)
> lift $ checkConvEnv env gamma (Ind vt) (Ind tv) (INotConvertible (Ind vt) (Ind tv))
> case ttnf of
> (Ind Star) -> return (B (Guess vv) tv)
-> _ -> fail $ "The type of the binder " ++ show n ++ " must be *"
+> _ -> lift $ tacfail $ "The type of the binder " ++ show n ++ " must be *"
> checkpatt gamma env lvl n RInfer t = do
> (Ind tv,Ind tt) <- tcfixup env lvl t Nothing
@@ -619,7 +619,7 @@ Insert inferred values into the term
> -- show patt ++ " and " ++ show tv ++ " are not convertible"
> case ttnf of
> (Ind Star) -> return ((B (Pattern patv) tv), bindings++env)
-> _ -> fail $ "The type of the binder " ++ show n ++ " must be *"
+> _ -> lift $ tacfail $ "The type of the binder " ++ show n ++ " must be *"
Check a raw term representing a pattern. Return the pattern, and the
extended environment.
View
@@ -144,7 +144,7 @@ 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 binders " ++ show x ++ " and " ++ show y
+> else tacfail $ "Can't unify binders " ++ show x ++ " and " ++ show y
> unst envl envr (Quote x) (Quote y) acc = un envl envr x y acc
> unst envl envr (Code x) (Code y) acc = un envl envr x y acc

0 comments on commit c91de60

Please sign in to comment.