d10c1e9 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Can't assume explicit names in updateSolved

Fixes #1242

commitd10c1e9421d1195d333b191e1fa93c7d41a657d2 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateMon 26 May 2014, 17:08 (12 years ago) parent45c8eca

2 files changed+8−5

unifiedsplit

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

@@ -789,8 +789,9 @@ updateSolved' [] x = x

789789updateSolved' xs (Bind n (Hole ty) t)

790790 | Just v <- lookup n xs

791791 = case xs of

792− [_] -> psubst n v t

793− _ -> psubst n v (updateSolved' xs t)

792+ [_] -> substV v $ psubst n v t -- some may be Vs! Can't assume

793+ -- explicit names

794+ _ -> substV v $ psubst n v (updateSolved' xs t)

794795updateSolved' xs (Bind n b t)

795796 | otherwise = Bind n (fmap (updateSolved' xs) b) (updateSolved' xs t)

796797updateSolved' xs (App f a)

@@ -838,7 +839,7 @@ updateProblems ctxt ns ps inj holes = up ns ps where

838839 y' = updateSolved ns y

839840 err' = updateError ns err

840841 env' = updateEnv ns env in

841−-- trace ("Updating " ++ show (x',y')) $

842+-- trace ("Updating " ++ show (x',y')) $

842843 case unify ctxt env' x' y' inj holes while of

843844 OK (v, []) -> -- trace ("Added " ++ show v ++ " from " ++ show (x', y')) $

844845 up (ns ++ v) ps

src/Idris/ElabTerm.hs+4−2

@@ -70,11 +70,13 @@ build ist info pattern opts fn tm

7070 when (not pattern) $

7171 traceWhen u ("Remaining problems:\n" ++ show probs) $

7272 do unify_all; matchProblems True; unifyProblems

73+

7374 probs <- get_probs

7475 case probs of

7576 [] -> return ()

76− ((_,_,_,e,_,_):es) -> if inf then return ()

77− else lift (Error e)

77+ ((_,_,_,e,_,_):es) -> traceWhen u ("Final problems:\n" ++ show probs) $

78+ if inf then return ()

79+ else lift (Error e)

7880 is <- getAux

7981 tt <- get_term

8082 let (tm, ds) = runState (collectDeferred (Just fn) tt) []