3629548 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Fix implicits under rewrite

They were being erased in the wrong place

commit362954819561ddfdc26632ca714176578a603a9e authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSat 25 Mar 2017, 20:18 (10 years ago) parent4a10e27

3 files changed+18−4

unifiedsplit

src/Idris/Elab/Rewrite.hs+3−3

@@ -76,9 +76,9 @@ elabRewrite elab ist fc substfn_in rule sc_in newg

7676 when (g == pred_tt) $ lift $ tfail (NoRewriting l r g)

7777 let pred = PLam fc rname fc Placeholder

7878 (delab ist pred_tt)

79− let rewrite = stripImpls $

80− addImplBound ist (map fstEnv env) (PApp fc (PRef fc [] substfn)

81− [pexp pred, pexp rule, pexp sc])

79+ let rewrite = addImplBound ist (map fstEnv env) (PApp fc (PRef fc [] substfn)

80+ [pexp (stripImpls pred),

81+ pexp (stripImpls rule), pexp sc])

8282-- trace ("LHS: " ++ show l ++ "\n" ++

8383-- "RHS: " ++ show r ++ "\n" ++

8484-- "REWRITE: " ++ show rewrite ++ "\n" ++

test/regression001/reg006.idrnew file+14

@@ -0,0 +1,14 @@

1+module Parity

3+data Parity : Nat -> Type where

4+ Even : Parity (n + n)

5+ Odd : Parity (S (plus n n))

7+parity : (n:Nat) -> Parity n

8+parity Z = Even {n = Z}

9+parity (S Z) = Odd {n = Z}

10+parity (S (S k)) with (parity k)

11+ parity (S (S (j + j))) | Even

12+ = rewrite plusSuccRightSucc j j in (Even {n = S j})

13+ parity (S (S (S (plus j j)))) | Odd

14+ = rewrite plusSuccRightSucc j j in (Odd {n = S j})

test/regression001/run+1−1

@@ -1,7 +1,7 @@

11#!/usr/bin/env bash

22${IDRIS:-idris} $@ --check \

33 reg001.idr reg002.idr reg003.idr reg004.lidr reg005.idr \

4− reg036.idr reg037.idr reg038.idr reg046.idr \

4+ reg006.idr reg036.idr reg037.idr reg038.idr reg046.idr \

55 reg047a.idr reg053.idr reg057.idr reg058.idr reg058a.idr \

66 reg059.idr reg060.idr reg061.idr reg062.idr reg063.idr \

77 reg064.idr reg065.idr reg066.idr reg071.idr reg074.idr \