git.iko.soy/Idris-dev
on master help sign in
Conversion checking tweak

Slightly more liberal if there are holes in the terms being checked, so that we don't fail too early.

commitc15d4cb410db22c5edf832dc610f10279c84862c authorEdwin Brady <ecb10@st-andrews.ac.uk> dateThu 27 Feb 2014, 11:09 (13 years ago) parent2f9c617
4 files changed+18−12
compare with master
unifiedsplit
src/Idris/Core/Evaluate.hs+4−3 src/Idris/Core/Typecheck.hs+11−6 src/Idris/Core/Unify.hs+2−2 src/Idris/ErrReverse.hs+1−1
src/Idris/Core/Evaluate.hs+4−3
@@ -520,12 +520,13 @@ wknV i (VBind red n b sc) = do b' <- fmapMB (wknV i) b
520520wknV i (VApp f a) = liftM2 VApp (wknV i f) (wknV i a)
521521wknV i t = return t
522522
523−convEq' ctxt x y = evalStateT (convEq ctxt x y) (0, [])
523+convEq' ctxt hs x y = evalStateT (convEq ctxt hs x y) (0, [])
524524
525−convEq :: Context -> TT Name -> TT Name -> StateT UCs (TC' Err) Bool
526−convEq ctxt = ceq [] where
525+convEq :: Context -> [Name] -> TT Name -> TT Name -> StateT UCs (TC' Err) Bool
526+convEq ctxt holes = ceq [] where
527527 ceq :: [(Name, Name)] -> TT Name -> TT Name -> StateT UCs (TC' Err) Bool
528528 ceq ps (P xt x _) (P yt y _)
529+ | x `elem` holes || y `elem` holes = return True
529530 | x == y || (x, y) `elem` ps || (y,x) `elem` ps = return True
530531 | otherwise = sameDefs ps x y
531532 ceq ps x (Bind n (Lam t) (App y (V 0))) = ceq ps x y
src/Idris/Core/Typecheck.hs+11−6
@@ -16,11 +16,12 @@ import Idris.Core.Evaluate
1616-- indexed with 'finalise'
1717
1818convertsC :: Context -> Env -> Term -> Term -> StateT UCs TC ()
19−convertsC ctxt env x y
20− = do c1 <- convEq ctxt x y
19+convertsC ctxt env x y =
20+ do let hs = map fst (filter isHole env)
21+ c1 <- convEq ctxt hs x y
2122 if c1 then return ()
2223 else
23− do c2 <- convEq ctxt (finalise (normalise ctxt env x))
24+ do c2 <- convEq ctxt hs (finalise (normalise ctxt env x))
2425 (finalise (normalise ctxt env y))
2526 if c2 then return ()
2627 else lift $ tfail (CantConvert
@@ -29,15 +30,19 @@ convertsC ctxt env x y
2930
3031converts :: Context -> Env -> Term -> Term -> TC ()
3132converts ctxt env x y
32− = case convEq' ctxt x y of
33+ = let hs = map fst (filter isHole env) in
34+ case convEq' ctxt hs x y of
3335 OK True -> return ()
34− _ -> case convEq' ctxt (finalise (normalise ctxt env x))
35− (finalise (normalise ctxt env y)) of
36+ _ -> case convEq' ctxt hs (finalise (normalise ctxt env x))
37+ (finalise (normalise ctxt env y)) of
3638 OK True -> return ()
3739 _ -> tfail (CantConvert
3840 (finalise (normalise ctxt env x))
3941 (finalise (normalise ctxt env y)) (errEnv env))
4042
43+isHole (n, Hole _) = True
44+isHole _ = False
45+
4146errEnv = map (\(x, b) -> (x, binderTy b))
4247
4348isType :: Context -> Env -> Term -> TC ()
src/Idris/Core/Unify.hs+2−2
@@ -79,7 +79,7 @@ match_unify ctxt env topx topy inj holes =
7979 ha <- un names ax ay
8080 combine names hf ha
8181 un names x y
82− | OK True <- convEq' ctxt x y = do sc 1; return []
82+ | OK True <- convEq' ctxt holes x y = do sc 1; return []
8383 | otherwise = do UI s f <- get
8484 let r = recoverable x y
8585 let err = CantUnify r
@@ -356,7 +356,7 @@ unify ctxt env topx topy inj holes =
356356 sameBinder (Pi _) (Pi _) = True
357357 sameBinder _ _ = False
358358 un' fn bnames x y
359− | OK True <- convEq' ctxt x y = do sc 1; return []
359+ | OK True <- convEq' ctxt holes x y = do sc 1; return []
360360 | otherwise = do UI s f <- get
361361 let r = recoverable x y
362362 let err = CantUnify r
src/Idris/ErrReverse.hs+1−1
@@ -65,7 +65,7 @@ errReverse ist t = rewrite 5 (elideLambdas t)
6565
6666 elideLambdas (App f a) = App (elideLambdas f) (elideLambdas a)
6767 elideLambdas (Bind n (Lam t) sc)
68− | size sc > 100 = P Ref (sUN "...") Erased
68+ | size sc > 200 = P Ref (sUN "...") Erased
6969 elideLambdas (Bind n b sc)
7070 = Bind n (fmap elideLambdas b) (elideLambdas sc)
7171 elideLambdas t = t