git.iko.soy/Idris-dev
on master help sign in
Fix elaboration of "with ... proof ..." clauses
56e8355David Raymond Christiansen
idris.cabal+3
compare with master
unifiedsplit
@@ -308,6 +308,9 @@ Extra-source-files:
308 test/reg062/run
308 test/reg062/run
309 test/reg062/*.idr
309 test/reg062/*.idr
310 test/reg062/expected
310 test/reg062/expected
311+ test/reg063/run
312+ test/reg063/*.idr
313+ test/reg063/expected
311
314
312 test/basic001/run
315 test/basic001/run
313 test/basic001/*.idr
316 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)
827 -- so this doesn't lose anything)
827 -- so this doesn't lose anything)
828 case getArgTys cwvaltyN of
828 case getArgTys cwvaltyN of
829 [] -> return ()
829 [] -> return ()
830− (_:_) -> ierror $ At fc (WithFnType cwvalty)
830+ (_:_) -> ierror $ At fc (WithFnType cwvalty)
831
831
832 let pvars = map fst (getPBtys cwvalty)
832 let pvars = map fst (getPBtys cwvalty)
833 -- we need the unelaborated term to get the names it depends on
833 -- 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)
897 (map (pexp . (PRef fc) . fst) bargs_post) ++
897 (map (pexp . (PRef fc) . fst) bargs_post) ++
898 case mpn of
898 case mpn of
899 Nothing -> []
899 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+ ])])
901 logLvl 5 ("New RHS " ++ showTmImpls rhs)
904 logLvl 5 ("New RHS " ++ showTmImpls rhs)
902 ctxt <- getContext -- New context with block added
905 ctxt <- getContext -- New context with block added
903 i <- getIState
906 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