c15d4cb · Idris-dev · git.iko.soy

src/Idris/Core/Evaluate.hs+4−3

compare with master

unifiedsplit

@@ -520,12 +520,13 @@ wknV i (VBind red n b sc) = do b' <- fmapMB (wknV i) b

520wknV i (VApp f a) = liftM2 VApp (wknV i f) (wknV i a)

521wknV i t = return t

522

523−convEq' ctxt x y = evalStateT (convEq ctxt x y) (0, [])

523+convEq' ctxt hs x y = evalStateT (convEq ctxt hs x y) (0, [])

524

525−convEq :: Context -> TT Name -> TT Name -> StateT UCs (TC' Err) Bool

525+convEq :: Context -> [Name] -> TT Name -> TT Name -> StateT UCs (TC' Err) Bool

526−convEq ctxt = ceq [] where

526+convEq ctxt holes = ceq [] where

527 ceq :: [(Name, Name)] -> TT Name -> TT Name -> StateT UCs (TC' Err) Bool

528 ceq ps (P xt x _) (P yt y _)

529+ | x `elem` holes || y `elem` holes = return True

529 | x == y || (x, y) `elem` ps || (y,x) `elem` ps = return True

530 | x == y || (x, y) `elem` ps || (y,x) `elem` ps = return True

530 | otherwise = sameDefs ps x y

531 | otherwise = sameDefs ps x y

531 ceq ps x (Bind n (Lam t) (App y (V 0))) = ceq ps x y

532 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

16-- indexed with 'finalise'

17

18convertsC :: Context -> Env -> Term -> Term -> StateT UCs TC ()

19−convertsC ctxt env x y

19+convertsC ctxt env x y =

20+ do let hs = map fst (filter isHole env)

20− = do c1 <- convEq ctxt x y

21+ c1 <- convEq ctxt hs x y

21 if c1 then return ()

22 if c1 then return ()

22 else

23 else

23− do c2 <- convEq ctxt (finalise (normalise ctxt env x))

24+ do c2 <- convEq ctxt hs (finalise (normalise ctxt env x))

24 (finalise (normalise ctxt env y))

25 (finalise (normalise ctxt env y))

25 if c2 then return ()

26 if c2 then return ()

26 else lift $ tfail (CantConvert

27 else lift $ tfail (CantConvert

@@ -29,15 +30,19 @@ convertsC ctxt env x y

29

30

30converts :: Context -> Env -> Term -> Term -> TC ()

31converts :: Context -> Env -> Term -> Term -> TC ()

31converts ctxt env x y

32converts ctxt env x y

33+ = let hs = map fst (filter isHole env) in

32− = case convEq' ctxt x y of

34+ case convEq' ctxt hs x y of

33 OK True -> return ()

35 OK True -> return ()

34− _ -> case convEq' ctxt (finalise (normalise ctxt env x))

36+ _ -> case convEq' ctxt hs (finalise (normalise ctxt env x))

35− (finalise (normalise ctxt env y)) of

37+ (finalise (normalise ctxt env y)) of

36 OK True -> return ()

38 OK True -> return ()

37 _ -> tfail (CantConvert

39 _ -> tfail (CantConvert

38 (finalise (normalise ctxt env x))

40 (finalise (normalise ctxt env x))

39 (finalise (normalise ctxt env y)) (errEnv env))

41 (finalise (normalise ctxt env y)) (errEnv env))

40

42

43+isHole (n, Hole _) = True

44+isHole _ = False

45+

41errEnv = map (\(x, b) -> (x, binderTy b))

46errEnv = map (\(x, b) -> (x, binderTy b))

42

47

43isType :: Context -> Env -> Term -> TC ()

48isType :: Context -> Env -> Term -> TC ()

src/Idris/Core/Unify.hs+2−2

@@ -79,7 +79,7 @@ match_unify ctxt env topx topy inj holes =

79 ha <- un names ax ay

80 combine names hf ha

81 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 []

83 | otherwise = do UI s f <- get

84 let r = recoverable x y

85 let err = CantUnify r

@@ -356,7 +356,7 @@ unify ctxt env topx topy inj holes =

356 sameBinder (Pi _) (Pi _) = True

357 sameBinder _ _ = False

358 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 []

360 | otherwise = do UI s f <- get

361 let r = recoverable x y

362 let err = CantUnify r

src/Idris/ErrReverse.hs+1−1

@@ -65,7 +65,7 @@ errReverse ist t = rewrite 5 (elideLambdas t)

65

66 elideLambdas (App f a) = App (elideLambdas f) (elideLambdas a)

67 elideLambdas (Bind n (Lam t) sc)

68− | size sc > 100 = P Ref (sUN "...") Erased

68+ | size sc > 200 = P Ref (sUN "...") Erased

69 elideLambdas (Bind n b sc)

70 = Bind n (fmap elideLambdas b) (elideLambdas sc)

71 elideLambdas t = t