git.iko.soy/Idris-dev
on master help sign in
Evaluator bug fix

Weakening out of scope variables should not happen (we had a flawed assumption about where the evaluator might be called from...)

commitecfb2935c1e7c33af21497e8d48180f95a69a196 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateFri 21 Feb 2014, 17:57 (13 years ago) parent0fa9239
10 files changed+119−8
compare with master
unifiedsplit
idris.cabal+4 src/Idris/Core/Evaluate.hs+3−3 src/Idris/Core/ProofState.hs+7−3 src/Idris/Core/Unify.hs+2−2 src/Idris/ElabTerm.hs+2 test/reg035/expected+4 test/reg035/reg035.idr+15 test/reg035/reg035a.lidr+66 test/reg035/reg035b.idr+11 test/reg035/run+5
idris.cabal+4
@@ -214,6 +214,10 @@ Extra-source-files:
214214 test/reg034/run
215215 test/reg034/*.idr
216216 test/reg034/expected
217+ test/reg035/run
218+ test/reg035/*.idr
219+ test/reg035/*.lidr
220+ test/reg035/expected
217221
218222 test/basic001/run
219223 test/basic001/*.idr
src/Idris/Core/Evaluate.hs+3−3
@@ -309,7 +309,7 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where
309309 apply ntimes stk top env (VBind True n (Lam t) sc) (a:as)
310310 = do a' <- sc a
311311 app <- apply ntimes stk top env a' as
312− wknV (-1) app
312+ wknV 1 app
313313 apply ntimes_in stk top env f@(VP Ref n ty) args
314314 | not top && hnf = case args of
315315 [] -> return f
@@ -513,10 +513,10 @@ instance Quote Value where
513513 quote i (VTmp x) = return $ V (i - x - 1)
514514
515515wknV :: Int -> Value -> Eval Value
516−wknV i (VV x) = return $ VV (x + i)
516+wknV i (VV x) | x >= i = return $ VV (x - 1)
517517wknV i (VBind red n b sc) = do b' <- fmapMB (wknV i) b
518518 return $ VBind red n b' (\x -> do x' <- sc x
519− wknV i x')
519+ wknV (i + 1) x')
520520wknV i (VApp f a) = liftM2 VApp (wknV i f) (wknV i a)
521521wknV i t = return t
522522
src/Idris/Core/ProofState.hs+7−3
@@ -796,10 +796,12 @@ updateProblems ctxt ns ps inj holes = up ns ps where
796796 y' = updateSolved ns y
797797 err' = updateError ns err
798798 env' = updateEnv ns env in
799− case unify ctxt env' x' y' inj holes of
799+-- trace ("Updating " ++ show (x',y')) $
800+ case unify ctxt env' x' y' inj holes of
800801 OK (v, []) -> -- trace ("Added " ++ show v ++ " from " ++ show (x', y')) $
801802 up (ns ++ v) ps
802− _ -> let (ns', ps') = up ns ps in
803+ e -> -- trace ("Failed " ++ show e) $
804+ let (ns', ps') = up ns ps in
803805 (ns', (x',y',env',err', um) : ps')
804806
805807-- attempt to solve remaining problems with match_unify
@@ -873,7 +875,9 @@ processTactic t ps
873875 (h:_) -> do ps' <- execStateT (process t h) ps
874876 let (ns', probs')
875877 = case solved ps' of
876− Just s -> updateProblems (context ps')
878+ Just s -> traceWhen (unifylog ps')
879+ ("SOLVED " ++ show s) $
880+ updateProblems (context ps')
877881 [s] (problems ps')
878882 (injective ps')
879883 (holes ps')
src/Idris/Core/Unify.hs+2−2
@@ -137,7 +137,7 @@ match_unify ctxt env topx topy inj holes =
137137 let v = highV (-1) tm in
138138 if v >= length ns
139139 then lift $ tfail (Msg "SCOPE ERROR")
140− else return [(x, bind (highV (-1) tm) ns tm)]
140+ else return [(x, bind v ns tm)]
141141 where inst [] tm = tm
142142 inst ((n, _) : ns) tm = inst ns (substV (P Bound n Erased) tm)
143143
@@ -506,7 +506,7 @@ unify ctxt env topx topy inj holes =
506506 let v = highV (-1) tm in
507507 if v >= length ns
508508 then lift $ tfail (Msg "SCOPE ERROR")
509− else return [(x, bind (highV (-1) tm) ns tm)]
509+ else return [(x, bind v ns tm)]
510510 where inst [] tm = tm
511511 inst (((n, _), _) : ns) tm = inst ns (substV (P Bound n Erased) tm)
512512
src/Idris/ElabTerm.hs+2
@@ -71,6 +71,8 @@ build ist info pattern opts fn tm
7171 resolveTC 7 g fn ist) ivs
7272 tm <- get_term
7373 ctxt <- get_context
74+ probs <- get_probs
75+
7476 when (not pattern) $ do matchProblems True; unifyProblems
7577 probs <- get_probs
7678 case probs of
test/reg035/expectednew file+4
@@ -0,0 +1,4 @@
1+reg035b.idr:7:6:Can't convert
2+ Additive -> Nat
3+with
4+ Fin 0
test/reg035/reg035.idrnew file+15
@@ -0,0 +1,15 @@
1+elimId : (a : Type) ->
2+ (a1 : a) ->
3+ (a2 : a) ->
4+ (m : (x : a) -> (y : a) -> x = y -> Type) ->
5+ (f : (x : a) -> m x x refl) ->
6+ (id : a1 = a2) ->
7+ m a1 a2 id
8+elimId _ x _ _ f refl = f x
9+
10+tran : (a : Type) -> (b : a) -> (c : a) -> (d : a) ->
11+ (e : b = c) -> (f : c = d) -> b = d
12+tran = \ a : Type , b : a , c : a , d : a , e : b = c =>
13+ (elimId a b c (\ f : a , g : a , h : f = g =>
14+ (i : a) -> (j : g = i) -> f = i)
15+ (\ f : a , g : a , h : f = g => h) e d)
test/reg035/reg035a.lidrnew file+66
@@ -0,0 +1,66 @@
1+> module Set
2+
3+> %default total
4+
5+> postulate soAndIntro : (p : alpha -> Bool) ->
6+> (q : beta -> Bool) ->
7+> (a : alpha) ->
8+> (b : beta) ->
9+> so (p a) ->
10+> so (q b) ->
11+> so (p a && q b)
12+
13+> hasNoDuplicates : (Eq alpha) => List alpha -> Bool
14+> hasNoDuplicates as = as == nub as
15+
16+> %assert_total
17+> setEq : (Eq alpha) => List alpha -> List alpha -> Bool
18+> setEq Nil Nil = True
19+> setEq Nil (y :: ys) = False
20+> setEq (x :: xs) Nil = False
21+> setEq {alpha} (x :: xs) (y :: ys) =
22+> (x == y && setEq xs ys)
23+> ||
24+> (elem x ys && elem y xs &&
25+> setEq (filter (/= y) xs) (filter (/= x) ys)
26+> )
27+
28+> data Set : Type -> Type where
29+> setify : (as : List a) -> Set a
30+
31+> instance (Eq a) => Eq (Set a) where
32+> (==) (setify as) (setify bs) = setEq as bs
33+
34+> postulate reflexive_Set_eqeq : (Eq a) =>
35+> (as : Set a) ->
36+> so (as == as)
37+
38+> unwrap : Set a -> List a
39+> unwrap (setify as) = as
40+
41+> union : Set (Set a) -> Set a
42+> union (setify ss) = setify (concat (map unwrap ss))
43+
44+> listify : (Eq a) => Set a -> List a
45+> listify = nub . unwrap
46+
47+> arePairwiseDisjoint : (Eq a) => Set (Set a) -> Bool
48+> arePairwiseDisjoint (setify ss) =
49+> hasNoDuplicates (concat (map listify ss))
50+
51+> isPartition : (Eq a) => Set (Set a) -> Set a -> Bool
52+> isPartition ass as = arePairwiseDisjoint ass && union ass == as
53+
54+> partitionLemma0 : (Eq alpha) =>
55+> (ass : Set (Set alpha)) ->
56+> so (arePairwiseDisjoint ass) ->
57+> so (ass `isPartition` union ass)
58+> partitionLemma0 ass asspd = (soAndIntro (\ xss => arePairwiseDisjoint xss)
59+> (\ xs => union ass == xs)
60+> ass
61+> (union ass)
62+> asspd
63+> uasseqas) where
64+> uasseqas : so (union ass == union ass)
65+> uasseqas = reflexive_Set_eqeq (union ass)
66+
test/reg035/reg035b.idrnew file+11
@@ -0,0 +1,11 @@
1+import Data.Vect
2+
3+total
4+finZEmpty : Fin Z -> a
5+
6+fins : (n : Nat) -> (xs : Vect n (Fin n) ** ((x : Fin n) -> Elem x xs))
7+fins Z = ([] ** (finZEmpty {a=_}))
8+
9+-- f : (a : Nat) -> a = S a -> _|_
10+-- f a = believe_me
11+
test/reg035/runnew file+5
@@ -0,0 +1,5 @@
1+#!/usr/bin/env bash
2+idris --check reg035.idr
3+idris --check reg035a.lidr
4+idris --check reg035b.idr
5+rm -f *.ibc