git.iko.soy/Idris-dev
on master help sign in
Fix elaboration of "with ... proof ..." clauses
commit56e83556f19b5c2a7c13860a25076bf212e48407 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateTue 12 May 2015, 13:04 (11 years ago) parent7e8e25b
5 files changed+30−2
compare with master
unifiedsplit
idris.cabal+3 src/Idris/Elab/Clause.hs+5−2 test/reg063/Cmp.idr+19 test/reg063/expected test/reg063/run+3
idris.cabal+3
@@ -308,6 +308,9 @@ Extra-source-files:
308308 test/reg062/run
309309 test/reg062/*.idr
310310 test/reg062/expected
311+ test/reg063/run
312+ test/reg063/*.idr
313+ test/reg063/expected
311314
312315 test/basic001/run
313316 test/basic001/*.idr
src/Idris/Elab/Clause.hs+5−2
@@ -827,7 +827,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)
827827 -- so this doesn't lose anything)
828828 case getArgTys cwvaltyN of
829829 [] -> return ()
830− (_:_) -> ierror $ At fc (WithFnType cwvalty)
830+ (_:_) -> ierror $ At fc (WithFnType cwvalty)
831831
832832 let pvars = map fst (getPBtys cwvalty)
833833 -- we need the unelaborated term to get the names it depends on
@@ -897,7 +897,10 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)
897897 (map (pexp . (PRef fc) . fst) bargs_post) ++
898898 case mpn of
899899 Nothing -> []
900− Just _ -> [pexp (PRef fc eqCon)])
900+ Just _ -> [pexp (PApp NoFC (PRef NoFC eqCon)
901+ [ pimp (sUN "A") Placeholder False
902+ , pimp (sUN "x") Placeholder False
903+ ])])
901904 logLvl 5 ("New RHS " ++ showTmImpls rhs)
902905 ctxt <- getContext -- New context with block added
903906 i <- getIState
test/reg063/Cmp.idrnew file+19
@@ -0,0 +1,19 @@
1+||| Test that explicit proof objects on the with rule work
2+module Cmp
3+
4+
5+data MyCmp : Nat -> Nat -> Type where
6+ IsLT : (d : Nat) -> MyCmp n (S d + n)
7+ IsEQ : MyCmp n n
8+ IsGT : (d : Nat) -> MyCmp (S d + n) n
9+
10+myCmp : (j, k : Nat) -> MyCmp j k
11+myCmp Z Z = IsEQ
12+myCmp Z (S k) = rewrite sym $ plusZeroRightNeutral k in IsLT k
13+myCmp (S j) Z = rewrite sym $ plusZeroRightNeutral j in IsGT j
14+myCmp (S j) (S k) with (myCmp j k) proof p
15+ myCmp (S j) (S (S (plus d j))) | (IsLT d) = rewrite plusSuccRightSucc d j
16+ in let useless = id p in IsLT d
17+ myCmp (S j) (S j) | IsEQ = IsEQ
18+ myCmp (S (S (plus d k))) (S k) | (IsGT d) = rewrite plusSuccRightSucc d k
19+ in IsGT d
test/reg063/expectednew file

No changes to the content.

test/reg063/runnew file+3
@@ -0,0 +1,3 @@
1+#!/usr/bin/env bash
2+idris $@ Cmp.idr --check --nocolour --quiet
3+rm *.ibc