Skip to content
Browse files

Use new evaluator in type checker

  • Loading branch information...
1 parent 17cbcef commit 95e09f598310d192330d6b250815ed07f488c54a Edwin Brady committed Jul 12, 2010
Showing with 11 additions and 9 deletions.
  1. +1 −1 Ivor/Datatype.lhs
  2. +4 −3 Ivor/TT.lhs
  3. +6 −5 Ivor/Typecheck.lhs
View
2 Ivor/Datatype.lhs
@@ -81,7 +81,7 @@ the context and an executable elimination rule.
> (er,ev) (cr,cv) Nothing Nothing [] [])
> checkCons gamma t [] = return ([], gamma)
-> checkCons gamma t ((cn,cty):cs) =
+> checkCons gamma t ((cn,cty):cs) = -- trace ("Checking " ++ show (cn, cty)) $
> do (cv,_) <- typecheck gamma cty
> let ccon = G (DCon t (arity gamma cv)) cv defplicit
> let gamma' = extend gamma (cn,ccon)
View
7 Ivor/TT.lhs
@@ -276,7 +276,7 @@
> -> [(Name, ([Int], Int))] -- ^ Functions and static arguments
> -> [Name] -- ^ Frozen names
> -> TTM Context
-> spec ctxt@(Ctxt st) fn statics frozen = trace ("Doing " ++ show fn) $
+> spec ctxt@(Ctxt st) fn statics frozen =
Look up the name, specialise it, then add the new pattern definition to the
context
@@ -318,9 +318,9 @@ context
> v <- raw tm
> let ctxt = defs st
> case (typecheck ctxt v) of
-> (Right (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
+> newdefs <- gInsert n (G (Fun [] v') t defplicit) ctxt
> -- let newdefs = Gam ((n,G (Fun [] v) t):ctxt)
> return $ Ctxt st { defs = newdefs }
> (Left err) -> tt $ ifail err
@@ -473,6 +473,7 @@ do let olddefs = defs st
> Just x' -> case cast y of
> Just y' -> Just $ Const (f x' y')
> Nothing -> Nothing
+> Nothing -> Nothing
> mktt _ = Nothing
> -- | Add a new binary function on constants. Warning: The type you give
View
11 Ivor/Typecheck.lhs
@@ -551,17 +551,18 @@ Insert inferred values into the term
> checkbinder gamma env lvl n (B Lambda t) = do
> (Ind tv,Ind tt) <- tcfixup env lvl t (Just (Ind Star))
-> let ttnf = normaliseEnv env gamma (Ind tt)
-> let (Ind tvnf) = normaliseEnv env gamma (Ind tv)
+> let ttnf = eval_nf_env env gamma (Ind tt)
+> let (Ind tvnf) = eval_nf_env env gamma (Ind tv)
> 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 *"
> checkbinder gamma env lvl n (B Pi t) = do
> (Ind tv,Ind tt) <- tcfixup env lvl t (Just (Ind Star))
-> let (Ind tvnf) = normaliseEnv env gamma (Ind tv)
-> -- let ttnf = normaliseEnv env gamma (Ind tt)
-> checkConvSt env gamma (Ind tt) (Ind Star)
+> let (Ind tvnf) = eval_nf_env env gamma (Ind tv)
+> let ttnf = -- trace ("PI: " ++ show (tv, tvnf, debugTT tv)) $
+> eval_nf_env env gamma (Ind tt)
+> checkConvSt env gamma ttnf (Ind Star)
> return (B Pi tvnf)
case ttnf of

0 comments on commit 95e09f5

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