83ef000 · Idris-dev · git.iko.soy

idris.cabal+3

compare with master

unifiedsplit

@@ -338,6 +338,9 @@ Extra-source-files:

338 test/reg073/run

339 test/reg073/*.lidr

340 test/reg073/expected

341+ test/reg074/run

342+ test/reg074/*.idr

343+ test/reg074/expected

341

344

342

345

343 test/basic001/run

346 test/basic001/run

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

@@ -763,7 +763,7 @@ infer_app infer fun arg str =

763 do a <- getNameFrom (sMN 0 "__argTy")

764 b <- getNameFrom (sMN 0 "__retTy")

765 f <- getNameFrom (sMN 0 "f")

766− s <- getNameFrom (sMN 0 "s")

766+ s <- getNameFrom (sMN 0 "is")

767 claim a RType

768 claim b RType

769 claim f (RBind (sMN 0 "_aX") (Pi Nothing (Var a) RType) (Var b))

@@ -797,7 +797,7 @@ dep_app fun arg str =

797 b <- getNameFrom (sMN 0 "__retTy")

798 fty <- getNameFrom (sMN 0 "__fnTy")

799 f <- getNameFrom (sMN 0 "f")

800− s <- getNameFrom (sMN 0 "s")

800+ s <- getNameFrom (sMN 0 "ds")

801 claim a RType

802 claim fty RType

803 claim f (Var fty)

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

@@ -340,7 +340,7 @@ envAtFocus :: ProofState -> TC Env

340envAtFocus ps

341 | not $ null (holes ps) = do g <- goal (Just (head (holes ps))) (pterm ps)

342 return (premises g)

343− | otherwise = fail "No holes"

343+ | otherwise = fail $ "No holes in " ++ show (getProofTerm (pterm ps))

344

345goalAtFocus :: ProofState -> TC (Binder Type)

346goalAtFocus ps

@@ -1083,7 +1083,8 @@ processTactic t ps

1083 [] -> case t of

1084 Focus _ -> return (ps, "") -- harmless to refocus when done, since

1085 -- '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))

1087 (h:_) -> do ps' <- execStateT (process t h) ps

1088 (h:_) -> do ps' <- execStateT (process t h) ps

1088 let (ns_in, probs')

1089 let (ns_in, probs')

1089 = case solved ps' of

1090 = case solved ps' of

src/Idris/Elab/Term.hs+5−3

@@ -1259,9 +1259,11 @@ elab ist info emode opts fn tm

1259 -- Delay dotted things to the end, then when we elaborate them

1260 -- we can check the result against what was inferred

1261 movelast h

1262− delayElab 10 $ do focus h

1262+ delayElab 10 $ do hs <- get_holes

1263+ when (h `elem` hs) $ do

1264+ focus h

1263− dotterm

1265+ dotterm

1264− elab' ina fc t

1266+ elab' ina fc t

1265 elab' ina fc (PRunElab fc' tm ns) =

1267 elab' ina fc (PRunElab fc' tm ns) =

1266 do attack

1268 do attack

1267 n <- getNameFrom (sMN 0 "tacticScript")

1269 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