Permalink
Browse files

Fix expected type when checking binders - it's only legitimate for let

Also some elaboriation of internal error messages.

darcs-hash:20080709014007-228f4-30a733e18b523e96e589fc79c6a0cc3b845a40df.gz
  • Loading branch information...
1 parent 92e54c5 commit a0edbb163ecae6a4217e721a9915dc38895a41db eb committed Jul 9, 2008
Showing with 8 additions and 5 deletions.
  1. +4 −2 Ivor/TTCore.lhs
  2. +1 −1 Ivor/Tactics.lhs
  3. +1 −1 Ivor/Typecheck.lhs
  4. +2 −1 Ivor/Unify.lhs
View
6 Ivor/TTCore.lhs
@@ -304,12 +304,14 @@ we get a duff term when we go back to the indexed version.
> makePs :: TT Name -> TT Name
> makePs t = let t' = evalState (uniqifyAllState t) [] in
-> vapp (\ (ctx,i) -> P (traceIndex ctx i "makePsEnv")) t'
+> vapp (\ (ctx,i) -> P (traceIndex ctx i ("makePs " ++
+> debugTT t))) t'
> --if (i<length ctx) then P (ctx!!i)
> -- else V i) t'
> makePsEnv env t = let t' = evalState (uniqifyAllState t) env in
-> vapp (\ (ctx,i) -> P (traceIndex ctx i "makePsEnv")) t'
+> vapp (\ (ctx,i) -> P (traceIndex ctx i
+> ("makePsEnv" ++ debugTT t))) t'
> uniqifyAllState :: TT Name -> State [Name] (TT Name)
View
2 Ivor/Tactics.lhs
@@ -637,7 +637,7 @@ Boolean flag (flip) is True if symmetry should be applied first.
> claimname = mkns x (UN "q")
> getTypes (App (App (App (App eq x) _) a) b) = return (x,a,b)
> getTypes (App (App (App eq x) a) b) = return (x,a,b)
-> getTypes _ = fail "Rule is not of equality type"
+> getTypes t = fail $ "Rule is not of equality type: " ++ show t
> mkns (UN a) (UN b) = UN (a++"_"++b)
> replace _ _ _ _ _ _ _ (Ind (Bind x b sc)) = fail $ "replace: " ++ show x ++ " Not a hole"
> replace _ _ _ _ _ _ _ _ = fail "replace: Not a binder, can't happen"
View
2 Ivor/Typecheck.lhs
@@ -360,7 +360,7 @@ and we don't convert names to de Bruijn indices
> (Just (Ind (Bind sn sb (Sc st)))) -> Just $
> normaliseEnv ((sn,sb):env) gamma (Ind st)
> _ -> fail (show exp)
-> (Ind scv, Ind sct) <- tcfixup ((n,gb):env) lvl sc scexp
+> (Ind scv, Ind sct) <- tcfixup ((n,gb):env) lvl sc Nothing -- scexp
> --discharge gamma n gb (Sc scv) (Sc sct)
> discharge gamma n gb (pToV n scv) (pToV n sct)
> tc env lvl l@(RLabel t comp) _ = do
View
3 Ivor/Unify.lhs
@@ -39,7 +39,8 @@ Unify on named terms, but normalise using de Bruijn indices.
> -- Also, there is no point reducing if we don't have to, and not calling
> -- the normaliser really speeds things up if we have a lot of easy
> -- constraints to solve...
-> unifyenvErr i gam env x y = {- trace (show (x,y) ++ "\n" ++
+> unifyenvErr i gam env x y = -- trace ("Unifying in " ++ show env) $
+> {- trace (show (x,y) ++ "\n" ++
> show (p (normalise (gam' gam) x)) ++ "\n" ++
> show (p (normalise (gam' gam) x))) $-}
> case unifynferr i env (p x)

0 comments on commit a0edbb1

Please sign in to comment.