git.iko.soy/Idris-dev
on master help sign in
Check delayed holes are still holes

They may be solved by unification. Fixes #2737

commit83ef000ab25f2f2db450dcaa8e7914fa4256fcde authorEdwin Brady <ecb10@st-andrews.ac.uk> dateTue 31 May 2016, 14:46 (10 years ago) parentef0ce29
7 files changed+37−7
compare with master
unifiedsplit
idris.cabal+3 src/Idris/Core/Elaborate.hs+2−2 src/Idris/Core/ProofState.hs+3−2 src/Idris/Elab/Term.hs+5−3 test/reg074/expected test/reg074/reg074.idr+21 test/reg074/run+3
idris.cabal+3
@@ -338,6 +338,9 @@ Extra-source-files:
338338 test/reg073/run
339339 test/reg073/*.lidr
340340 test/reg073/expected
341+ test/reg074/run
342+ test/reg074/*.idr
343+ test/reg074/expected
341344
342345
343346 test/basic001/run
src/Idris/Core/Elaborate.hs+2−2
@@ -763,7 +763,7 @@ infer_app infer fun arg str =
763763 do a <- getNameFrom (sMN 0 "__argTy")
764764 b <- getNameFrom (sMN 0 "__retTy")
765765 f <- getNameFrom (sMN 0 "f")
766− s <- getNameFrom (sMN 0 "s")
766+ s <- getNameFrom (sMN 0 "is")
767767 claim a RType
768768 claim b RType
769769 claim f (RBind (sMN 0 "_aX") (Pi Nothing (Var a) RType) (Var b))
@@ -797,7 +797,7 @@ dep_app fun arg str =
797797 b <- getNameFrom (sMN 0 "__retTy")
798798 fty <- getNameFrom (sMN 0 "__fnTy")
799799 f <- getNameFrom (sMN 0 "f")
800− s <- getNameFrom (sMN 0 "s")
800+ s <- getNameFrom (sMN 0 "ds")
801801 claim a RType
802802 claim fty RType
803803 claim f (Var fty)
src/Idris/Core/ProofState.hs+3−2
@@ -340,7 +340,7 @@ envAtFocus :: ProofState -> TC Env
340340envAtFocus ps
341341 | not $ null (holes ps) = do g <- goal (Just (head (holes ps))) (pterm ps)
342342 return (premises g)
343− | otherwise = fail "No holes"
343+ | otherwise = fail $ "No holes in " ++ show (getProofTerm (pterm ps))
344344
345345goalAtFocus :: ProofState -> TC (Binder Type)
346346goalAtFocus ps
@@ -1083,7 +1083,8 @@ processTactic t ps
10831083 [] -> case t of
10841084 Focus _ -> return (ps, "") -- harmless to refocus when done, since
10851085 -- 'focus' doesn't fail
1086− _ -> fail $ "Nothing to fill in."
1086+ _ -> fail $ "Proof done, nothing to run tactic on: " ++ show t ++
1087+ "\n" ++ show (getProofTerm (pterm ps))
10871088 (h:_) -> do ps' <- execStateT (process t h) ps
10881089 let (ns_in, probs')
10891090 = case solved ps' of
src/Idris/Elab/Term.hs+5−3
@@ -1259,9 +1259,11 @@ elab ist info emode opts fn tm
12591259 -- Delay dotted things to the end, then when we elaborate them
12601260 -- we can check the result against what was inferred
12611261 movelast h
1262− delayElab 10 $ do focus h
1263− dotterm
1264− elab' ina fc t
1262+ delayElab 10 $ do hs <- get_holes
1263+ when (h `elem` hs) $ do
1264+ focus h
1265+ dotterm
1266+ elab' ina fc t
12651267 elab' ina fc (PRunElab fc' tm ns) =
12661268 do attack
12671269 n <- getNameFrom (sMN 0 "tacticScript")
test/reg074/expectednew file

No changes to the content.

test/reg074/reg074.idrnew file+21
@@ -0,0 +1,21 @@
1+%default total
2+
3+binary_relation : (a : Type) -> Type
4+binary_relation a = (x, y : a) -> Type
5+
6+reflexive : (a : Type) -> (r : binary_relation a) -> Type
7+reflexive a r = (x : a) -> r x x
8+
9+symmetric : (a : Type) -> (r : binary_relation a) -> Type
10+symmetric a r = (x, y : a) -> r x y -> r y x
11+
12+data Equal : (a : Type) -> binary_relation a where
13+ Same : (a : Type) -> (x : a) -> Equal a x x
14+
15+Equal_reflexive : (a : Type) -> reflexive a (Equal a)
16+Equal_reflexive a x = Same a x
17+
18+Equal_symmetric : (a : Type) -> symmetric a (Equal a)
19+-- Equal_symmetric : (a : Type) -> (x, y : a) -> Equal a x y -> Equal a y x
20+Equal_symmetric a x x (Same a x) = Same a x
21+
test/reg074/runnew file+3
@@ -0,0 +1,3 @@
1+#!/usr/bin/env bash
2+${IDRIS:-idris} $@ reg074.idr --check
3+rm -f *.ibc