b92f7ac · Idris-dev · git.iko.soy

idris.cabal+4

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

663663 test/proof010/run

664664 test/proof010/*.idr

665665 test/proof010/expected

666+ test/proof011/run

667+ test/proof011/*.idr

668+ test/proof011/expected

666669

667670 test/proofsearch001/run

668671 test/proofsearch001/*.idr

@@ -906,6 +909,7 @@ Library

906909 , Idris.Elab.Value

907910 , Idris.Elab.Term

908911 , Idris.Elab.Quasiquote

912+ , Idris.Elab.Rewrite

909913

910914 , Idris.REPL.Browse

911915

libs/prelude/Builtins.idr+9−3

@@ -87,13 +87,19 @@ infix 5 ~=~

8787(~=~) x y = (x = y)

8888

8989||| Perform substitution in a term according to some equality.

90−|||

91−||| This is used by the `rewrite` tactic and term.

9290replace : {a:_} -> {x:_} -> {y:_} -> {P : a -> Type} -> x = y -> P x -> P y

9391replace Refl prf = prf

9492

93+||| Perform substitution in a term according to some equality.

94+|||

95+||| Like `replace`, but with an explicit predicate, and applying the rewrite

96+||| in the other direction, which puts it in a form usable by the `rewrite`

97+||| tactic and term.

98+rewrite__impl : (P : a -> Type) -> x = y -> P y -> P x

99+rewrite__impl P Refl prf = prf

100+

95101||| Symmetry of propositional equality

96−sym : {left:a} -> {right:a} -> left = right -> right = left

102+sym : {left:a} -> {right:b} -> left = right -> right = left

97103sym Refl = Refl

98104

99105||| Transitivity of propositional equality

src/Idris/AbsSyntax.hs+9−9

@@ -1134,7 +1134,7 @@ expandParams dec ps ns infs tm = en 0 tm

11341134 | n `elem` (map fst ps ++ ns) && t /= Placeholder

11351135 = let n' = mkShadow n in

11361136 PDPair f hls p (PRef f' fcs n') (en 0 t) (en 0 (shadow n n' r))

1137− en 0 (PRewrite f l r g) = PRewrite f (en 0 l) (en 0 r) (fmap (en 0) g)

1137+ en 0 (PRewrite f by l r g) = PRewrite f by (en 0 l) (en 0 r) (fmap (en 0) g)

11381138 en 0 (PTyped l r) = PTyped (en 0 l) (en 0 r)

11391139 en 0 (PPair f hls p l r) = PPair f hls p (en 0 l) (en 0 r)

11401140 en 0 (PDPair f hls p l t r) = PDPair f hls p (en 0 l) (en 0 t) (en 0 r)

@@ -1307,7 +1307,7 @@ getPriority i tm = 1 -- pri tm

13071307 [] -> 0 -- must be locally bound, if it's not an error...

13081308 pri (PPi _ _ _ x y) = max 5 (max (pri x) (pri y))

13091309 pri (PTrue _ _) = 0

1310− pri (PRewrite _ l r _) = max 1 (max (pri l) (pri r))

1310+ pri (PRewrite _ _ l r _) = max 1 (max (pri l) (pri r))

13111311 pri (PApp _ f as) = max 1 (max (pri f) (foldr (max . pri . getTm) 0 as))

13121312 pri (PAppBind _ f as) = max 1 (max (pri f) (foldr (max . pri . getTm) 0 as))

13131313 pri (PCase _ f as) = max 1 (max (pri f) (foldr (max . pri . snd) 0 as))

@@ -1628,7 +1628,7 @@ implicitise auto syn ignore ist tm = -- trace ("INCOMING " ++ showImp True tm) $

16281628 put (PTacImplicit 10 l n scr Placeholder : decls,

16291629 nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))

16301630 imps True (n:env) sc

1631− imps top env (PRewrite _ l r _)

1631+ imps top env (PRewrite _ _ l r _)

16321632 = do (decls, ns) <- get

16331633 let isn = namesIn uvars ist l ++ namesIn uvars ist r

16341634 put (decls, nub (ns ++ (isn `dropAll` (env ++ map fst (getImps decls)))))

@@ -1704,11 +1704,11 @@ addImpl' inpat env infns imp_meths ist ptm

17041704 | not (f `elem` map fst env) = handleErr $ aiFn topname inpat inpat qq imp_meths ist fc f fc ds []

17051705 ai inpat qq env ds (PHidden (PRef fc hl f))

17061706 | not (f `elem` map fst env) = PHidden (handleErr $ aiFn topname inpat False qq imp_meths ist fc f fc ds [])

1707− ai inpat qq env ds (PRewrite fc l r g)

1707+ ai inpat qq env ds (PRewrite fc by l r g)

17081708 = let l' = ai inpat qq env ds l

17091709 r' = ai inpat qq env ds r

17101710 g' = fmap (ai inpat qq env ds) g in

1711− PRewrite fc l' r' g'

1711+ PRewrite fc by l' r' g'

17121712 ai inpat qq env ds (PTyped l r)

17131713 = let l' = ai inpat qq env ds l

17141714 r' = ai inpat qq env ds r in

@@ -2127,7 +2127,7 @@ matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where

21272127 | not names && (not (isConName n (tt_ctxt i) ||

21282128 isFnName n (tt_ctxt i)) || tm == Placeholder)

21292129 = return [(n, tm)]

2130− match (PRewrite _ l r _) (PRewrite _ l' r' _)

2130+ match (PRewrite _ by l r _) (PRewrite _ by' l' r' _) | by == by'

21312131 = do ml <- match' l l'

21322132 mr <- match' r r'

21332133 return (ml ++ mr)

@@ -2222,8 +2222,8 @@ substMatchShadow n shs tm t = sm shs t where

22222222 sm xs (PApp f x as) = fullApp $ PApp f (sm xs x) (map (fmap (sm xs)) as)

22232223 sm xs (PCase f x as) = PCase f (sm xs x) (map (pmap (sm xs)) as)

22242224 sm xs (PIfThenElse fc c t f) = PIfThenElse fc (sm xs c) (sm xs t) (sm xs f)

2225− sm xs (PRewrite f x y tm) = PRewrite f (sm xs x) (sm xs y)

2226− (fmap (sm xs) tm)

2225+ sm xs (PRewrite f by x y tm) = PRewrite f by (sm xs x) (sm xs y)

2226+ (fmap (sm xs) tm)

22272227 sm xs (PTyped x y) = PTyped (sm xs x) (sm xs y)

22282228 sm xs (PPair f hls p x y) = PPair f hls p (sm xs x) (sm xs y)

22292229 sm xs (PDPair f hls p x t y) = PDPair f hls p (sm xs x) (sm xs t) (sm xs y)

@@ -2251,7 +2251,7 @@ shadow n n' t = sm 0 t where

22512251 sm 0 (PAppBind f x as) = PAppBind f (sm 0 x) (map (fmap (sm 0)) as)

22522252 sm 0 (PCase f x as) = PCase f (sm 0 x) (map (pmap (sm 0)) as)

22532253 sm 0 (PIfThenElse fc c t f) = PIfThenElse fc (sm 0 c) (sm 0 t) (sm 0 f)

2254− sm 0 (PRewrite f x y tm) = PRewrite f (sm 0 x) (sm 0 y) (fmap (sm 0) tm)

2254+ sm 0 (PRewrite f by x y tm) = PRewrite f by (sm 0 x) (sm 0 y) (fmap (sm 0) tm)

22552255 sm 0 (PTyped x y) = PTyped (sm 0 x) (sm 0 y)

22562256 sm 0 (PPair f hls p x y) = PPair f hls p (sm 0 x) (sm 0 y)

22572257 sm 0 (PDPair f hls p x t y) = PDPair f hls p (sm 0 x) (sm 0 t) (sm 0 y)

src/Idris/AbsSyntaxTree.hs+19−12

@@ -1024,7 +1024,9 @@ data PTerm = PQuote Raw -- ^ Inclusion of a core term into the high-level langua

10241024 | PCase FC PTerm [(PTerm, PTerm)] -- ^ A case expression. Args are source location, scrutinee, and a list of pattern/RHS pairs

10251025 | PTrue FC PunInfo -- ^ Unit type..?

10261026 | PResolveTC FC -- ^ Solve this dictionary by type class resolution

1027− | PRewrite FC PTerm PTerm (Maybe PTerm) -- ^ "rewrite" syntax, with optional result type

1027+ | PRewrite FC (Maybe Name) PTerm PTerm (Maybe PTerm)

1028+ -- ^ "rewrite" syntax, with optional rewriting function

1029+ -- and optional result type

10281030 | PPair FC [FC] PunInfo PTerm PTerm -- ^ A pair (a, b) and whether it's a product type or a pair (solved by elaboration). The list of FCs is its punctuation.

10291031 | PDPair FC [FC] PunInfo PTerm PTerm PTerm -- ^ A dependent pair (tm : a ** b) and whether it's a sigma type or a pair that inhabits one (solved by elaboration). The [FC] is its punctuation.

10301032 | PAs FC Name PTerm -- ^ @-pattern, valid LHS only

@@ -1080,7 +1082,7 @@ mapPTermFC f g (PIfThenElse fc t1 t2 t3) = PIfThenElse (f fc) (mapPTermFC f

10801082mapPTermFC f g (PCase fc t cases) = PCase (f fc) (mapPTermFC f g t) (map (\(l,r) -> (mapPTermFC f g l, mapPTermFC f g r)) cases)

10811083mapPTermFC f g (PTrue fc info) = PTrue (f fc) info

10821084mapPTermFC f g (PResolveTC fc) = PResolveTC (f fc)

1083−mapPTermFC f g (PRewrite fc t1 t2 t3) = PRewrite (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2) (fmap (mapPTermFC f g) t3)

1085+mapPTermFC f g (PRewrite fc by t1 t2 t3) = PRewrite (f fc) by (mapPTermFC f g t1) (mapPTermFC f g t2) (fmap (mapPTermFC f g) t3)

10841086mapPTermFC f g (PPair fc hls info t1 t2) = PPair (f fc) (map g hls) info (mapPTermFC f g t1) (mapPTermFC f g t2)

10851087mapPTermFC f g (PDPair fc hls info t1 t2 t3) = PDPair (f fc) (map g hls) info (mapPTermFC f g t1) (mapPTermFC f g t2) (mapPTermFC f g t3)

10861088mapPTermFC f g (PAs fc n t) = PAs (f fc) n (mapPTermFC f g t)

@@ -1125,7 +1127,7 @@ mapPT f t = f (mpt t) where

11251127 mpt (PLam fc n nfc t s) = PLam fc n nfc (mapPT f t) (mapPT f s)

11261128 mpt (PPi p n nfc t s) = PPi p n nfc (mapPT f t) (mapPT f s)

11271129 mpt (PLet fc n nfc ty v s) = PLet fc n nfc (mapPT f ty) (mapPT f v) (mapPT f s)

1128− mpt (PRewrite fc t s g) = PRewrite fc (mapPT f t) (mapPT f s) (fmap (mapPT f) g)

1130+ mpt (PRewrite fc by t s g) = PRewrite fc by (mapPT f t) (mapPT f s) (fmap (mapPT f) g)

11291131 mpt (PApp fc t as) = PApp fc (mapPT f t) (map (fmap (mapPT f)) as)

11301132 mpt (PWithApp fc t a) = PWithApp fc (mapPT f t) (mapPT f a)

11311133 mpt (PAppBind fc t as) = PAppBind fc (mapPT f t) (map (fmap (mapPT f)) as)

@@ -1302,7 +1304,7 @@ highestFC (PCase fc _ _) = Just fc

13021304highestFC (PIfThenElse fc _ _ _) = Just fc

13031305highestFC (PTrue fc _) = Just fc

13041306highestFC (PResolveTC fc) = Just fc

1305−highestFC (PRewrite fc _ _ _) = Just fc

1307+highestFC (PRewrite fc _ _ _ _) = Just fc

13061308highestFC (PPair fc _ _ _ _) = Just fc

13071309highestFC (PDPair fc _ _ _ _ _) = Just fc

13081310highestFC (PAs fc _ _) = Just fc

@@ -1882,9 +1884,14 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd

18821884 prettySe d p bnd (PTrue _ IsType) = annName unitTy $ text "()"

18831885 prettySe d p bnd (PTrue _ IsTerm) = annName unitCon $ text "()"

18841886 prettySe d p bnd (PTrue _ TypeOrTerm) = text "()"

1885− prettySe d p bnd (PRewrite _ l r _) =

1887+ prettySe d p bnd (PRewrite _ by l r _) =

18861888 depth d . bracket p startPrec $

1887− text "rewrite" <+> prettySe (decD d) (startPrec + 1) bnd l <+> text "in" <+> prettySe (decD d) startPrec bnd r

1889+ text "rewrite" <+> prettySe (decD d) (startPrec + 1) bnd l

1890+ <+> (case by of

1891+ Nothing -> empty

1892+ Just fn -> text "using" <+>

1893+ prettyName True (ppopt_impl ppo) bnd fn) <+>

1894+ text "in" <+> prettySe (decD d) startPrec bnd r

18881895 prettySe d p bnd (PTyped l r) =

18891896 lparen <> prettySe (decD d) startPrec bnd l <+> colon <+> prettySe (decD d) startPrec bnd r <> rparen

18901897 prettySe d p bnd pair@(PPair _ _ pun _ _) -- flatten tuples to the right, like parser

@@ -2247,7 +2254,7 @@ instance Sized PTerm where

22472254 size (PIfThenElse fc c t f) = 1 + sum (map size [c, t, f])

22482255 size (PTrue fc _) = 1

22492256 size (PResolveTC fc) = 1

2250− size (PRewrite fc left right _) = 1 + size left + size right

2257+ size (PRewrite fc by left right _) = 1 + size left + size right

22512258 size (PPair fc _ _ left right) = 1 + size left + size right

22522259 size (PDPair fs _ _ left ty right) = 1 + size left + size ty + size right

22532260 size (PAlternative _ a alts) = 1 + size alts

@@ -2288,7 +2295,7 @@ allNamesIn tm = nub $ ni 0 [] tm

22882295 ni 0 env (PPi p n _ ty sc) = niTacImp 0 env p ++ ni 0 env ty ++ ni 0 (n:env) sc

22892296 ni 0 env (PLet _ n _ ty val sc) = ni 0 env ty ++ ni 0 env val ++ ni 0 (n:env) sc

22902297 ni 0 env (PHidden tm) = ni 0 env tm

2291− ni 0 env (PRewrite _ l r _) = ni 0 env l ++ ni 0 env r

2298+ ni 0 env (PRewrite _ _ l r _) = ni 0 env l ++ ni 0 env r

22922299 ni 0 env (PTyped l r) = ni 0 env l ++ ni 0 env r

22932300 ni 0 env (PPair _ _ _ l r) = ni 0 env l ++ ni 0 env r

22942301 ni 0 env (PDPair _ _ _ (PRef _ _ n) Placeholder r) = n : ni 0 env r

@@ -2319,7 +2326,7 @@ boundNamesIn tm = S.toList (ni 0 S.empty tm)

23192326 ni 0 set (PLam fc n _ ty sc) = S.insert n $ ni 0 (ni 0 set ty) sc

23202327 ni 0 set (PLet fc n nfc ty val sc) = S.insert n $ ni 0 (ni 0 (ni 0 set ty) val) sc

23212328 ni 0 set (PPi p n _ ty sc) = niTacImp 0 (S.insert n $ ni 0 (ni 0 set ty) sc) p

2322− ni 0 set (PRewrite _ l r _) = ni 0 (ni 0 set l) r

2329+ ni 0 set (PRewrite _ _ l r _) = ni 0 (ni 0 set l) r

23232330 ni 0 set (PTyped l r) = ni 0 (ni 0 set l) r

23242331 ni 0 set (PPair _ _ _ l r) = ni 0 (ni 0 set l) r

23252332 ni 0 set (PDPair _ _ _ (PRef _ _ n) t r) = ni 0 (ni 0 set t) r

@@ -2395,7 +2402,7 @@ implicitNamesIn uvars ist tm

23952402 ni 0 env (PIfThenElse _ c t f) = mapM_ (ni 0 env) [c, t, f]

23962403 ni 0 env (PLam fc n _ ty sc) = do ni 0 env ty; ni 0 (n:env) sc

23972404 ni 0 env (PPi p n _ ty sc) = do ni 0 env ty; ni 0 (n:env) sc

2398− ni 0 env (PRewrite _ l r _) = do ni 0 env l; ni 0 env r

2405+ ni 0 env (PRewrite _ _ l r _) = do ni 0 env l; ni 0 env r

23992406 ni 0 env (PTyped l r) = do ni 0 env l; ni 0 env r

24002407 ni 0 env (PPair _ _ _ l r) = do ni 0 env l; ni 0 env r

24012408 ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = do ni 0 env t; ni 0 (n:env) r

@@ -2432,7 +2439,7 @@ namesIn uvars ist tm = nub $ ni 0 [] tm

24322439 ni 0 env (PIfThenElse _ c t f) = concatMap (ni 0 env) [c, t, f]

24332440 ni 0 env (PLam fc n nfc ty sc) = ni 0 env ty ++ ni 0 (n:env) sc

24342441 ni 0 env (PPi p n _ ty sc) = niTacImp 0 env p ++ ni 0 env ty ++ ni 0 (n:env) sc

2435− ni 0 env (PRewrite _ l r _) = ni 0 env l ++ ni 0 env r

2442+ ni 0 env (PRewrite _ _ l r _) = ni 0 env l ++ ni 0 env r

24362443 ni 0 env (PTyped l r) = ni 0 env l ++ ni 0 env r

24372444 ni 0 env (PPair _ _ _ l r) = ni 0 env l ++ ni 0 env r

24382445 ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = ni 0 env t ++ ni 0 (n:env) r

@@ -2467,7 +2474,7 @@ usedNamesIn vars ist tm = nub $ ni 0 [] tm

24672474 ni 0 env (PIfThenElse _ c t f) = concatMap (ni 0 env) [c, t, f]

24682475 ni 0 env (PLam fc n _ ty sc) = ni 0 env ty ++ ni 0 (n:env) sc

24692476 ni 0 env (PPi p n _ ty sc) = niTacImp 0 env p ++ ni 0 env ty ++ ni 0 (n:env) sc

2470− ni 0 env (PRewrite _ l r _) = ni 0 env l ++ ni 0 env r

2477+ ni 0 env (PRewrite _ _ l r _) = ni 0 env l ++ ni 0 env r

24712478 ni 0 env (PTyped l r) = ni 0 env l ++ ni 0 env r

24722479 ni 0 env (PPair _ _ _ l r) = ni 0 env l ++ ni 0 env r

24732480 ni 0 env (PDPair _ _ _ (PRef _ _ n) t r) = ni 0 env t ++ ni 0 (n:env) r

src/Idris/DSL.hs+2−2

@@ -88,8 +88,8 @@ expandSugar dsl (PNoImplicits t) = PNoImplicits (expandSugar dsl t)

8888expandSugar dsl (PUnifyLog t) = PUnifyLog (expandSugar dsl t)

8989expandSugar dsl (PDisamb ns t) = PDisamb ns (expandSugar dsl t)

9090expandSugar dsl (PReturn fc) = dsl_return dsl

91−expandSugar dsl (PRewrite fc r t ty)

92− = PRewrite fc r (expandSugar dsl t) ty

91+expandSugar dsl (PRewrite fc by r t ty)

92+ = PRewrite fc by r (expandSugar dsl t) ty

9393expandSugar dsl (PGoal fc r n sc)

9494 = PGoal fc (expandSugar dsl r) n (expandSugar dsl sc)

9595expandSugar dsl (PDoBlock ds)

src/Idris/DeepSeq.hs+2−2

@@ -536,8 +536,8 @@ instance NFData PTerm where

536536 rnf (PIfThenElse x1 x2 x3 x4) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

537537 rnf (PTrue x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

538538 rnf (PResolveTC x1) = rnf x1 `seq` ()

539− rnf (PRewrite x1 x2 x3 x4)

540− = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` ()

539+ rnf (PRewrite x1 x2 x3 x4 x5)

540+ = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()

541541 rnf (PPair x1 x2 x3 x4 x5) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` x5 `seq` ()

542542 rnf (PDPair x1 x2 x3 x4 x5 x6)

543543 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` x6 `seq` ()

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

@@ -109,13 +109,13 @@ extractUnquotes n (PIfThenElse fc c t f)

109109 (t', ex2) <- extractUnquotes n t

110110 (f', ex3) <- extractUnquotes n f

111111 return (PIfThenElse fc c' t' f', ex1 ++ ex2 ++ ex3)

112−extractUnquotes n (PRewrite fc x y z)

112+extractUnquotes n (PRewrite fc by x y z)

113113 = do (x', ex1) <- extractUnquotes n x

114114 (y', ex2) <- extractUnquotes n y

115115 case z of

116116 Just zz -> do (z', ex3) <- extractUnquotes n zz

117− return (PRewrite fc x' y' (Just z'), ex1 ++ ex2 ++ ex3)

118− Nothing -> return (PRewrite fc x' y' Nothing, ex1 ++ ex2)

117+ return (PRewrite fc by x' y' (Just z'), ex1 ++ ex2 ++ ex3)

118+ Nothing -> return (PRewrite fc by x' y' Nothing, ex1 ++ ex2)

119119extractUnquotes n (PPair fc hls info l r)

120120 = do (l', ex1) <- extractUnquotes n l

121121 (r', ex2) <- extractUnquotes n r

src/Idris/Elab/Rewrite.hsnew file+133

@@ -0,0 +1,133 @@

1+{-# LANGUAGE PatternGuards, ViewPatterns #-}

2+{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

3+module Idris.Elab.Rewrite(elabRewrite) where

4+

5+import Idris.AbsSyntax

6+import Idris.AbsSyntaxTree

7+import Idris.Delaborate

8+import Idris.Error

9+import Idris.Core.TT

10+import Idris.Core.Elaborate

11+import Idris.Core.Evaluate

12+

13+import Control.Monad

14+import Control.Monad.State.Strict

15+import Data.List

16+

17+import Debug.Trace

18+

19+elabRewrite :: (PTerm -> ElabD ()) -> IState ->

20+ FC -> Maybe Name -> PTerm -> PTerm -> Maybe PTerm -> ElabD ()

21+-- Old version, no rewrite rule given

22+{-

23+elabRewrite elab ist fc Nothing rule sc newg

24+ = do attack

25+ tyn <- getNameFrom (sMN 0 "rty")

26+ claim tyn RType

27+ valn <- getNameFrom (sMN 0 "rval")

28+ claim valn (Var tyn)

29+ letn <- getNameFrom (sMN 0 "_rewrite_rule")

30+ letbind letn (Var tyn) (Var valn)

31+ focus valn

32+ elab rule

33+ compute

34+ g <- goal

35+ rewrite (Var letn)

36+ g' <- goal

37+ when (g == g') $ lift $ tfail (NoRewriting g)

38+ case newg of

39+ Nothing -> elab sc

40+ Just t -> doEquiv elab fc t sc

41+ solve

42+ -}

43+elabRewrite elab ist fc Nothing rule sc newg

44+ = elabRewrite elab ist fc (Just (sUN "rewrite__impl")) rule sc newg

45+elabRewrite elab ist fc (Just substfn_in) rule sc newg

46+ = do substfn <- case lookupTyName substfn_in (tt_ctxt ist) of

47+ [(n, t)] -> return n

48+ [] -> lift . tfail . NoSuchVariable $ substfn_in

49+ more -> lift . tfail . CantResolveAlts $ map fst more

50+ attack

51+ tyn <- getNameFrom (sMN 0 "rty")

52+ claim tyn RType

53+ valn <- getNameFrom (sMN 0 "rval")

54+ claim valn (Var tyn)

55+ letn <- getNameFrom (sMN 0 "_rewrite_rule")

56+ letbind letn (Var tyn) (Var valn)

57+ focus valn

58+ elab rule

59+ compute

60+ g <- goal

61+ (tmv, rule_in) <- get_type_val (Var letn)

62+ env <- get_env

63+ let ttrule = normalise (tt_ctxt ist) env rule_in

64+ rname <- unique_hole (sMN 0 "replaced")

65+ case unApply ttrule of

66+ (P _ (UN q) _, [lt, rt, l, r]) | q == txt "=" ->

67+ do let pred_tt = mkP (P Bound rname rt) l r g

68+ when (g == pred_tt) $ lift $ tfail (NoRewriting g)

69+ let pred = PLam fc rname fc Placeholder

70+ (delab ist pred_tt)

71+ let rewrite = stripImpls $

72+ addImplBound ist (map fst env) (PApp fc (PRef fc [] substfn)

73+ [pexp pred, pexp rule, pexp sc])

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

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

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

77+-- "GOAL: " ++ show (delab ist g)) $

78+ elab rewrite

79+ solve

80+ _ -> lift $ tfail (NotEquality tmv ttrule)

81+ where

82+ mkP :: TT Name -> -- Left term, top level

83+ TT Name -> TT Name -> TT Name -> TT Name

84+ mkP lt l r ty | l == ty = lt

85+ mkP lt l r (App s f a)

86+ = let f' = if (r /= f) then mkP lt l r f else f

87+ a' = if (r /= a) then mkP lt l r a else a in

88+ App s f' a'

89+ mkP lt l r (Bind n b sc)

90+ = let b' = mkPB b

91+ sc' = if (r /= sc) then mkP lt l r sc else sc in

92+ Bind n b' sc'

93+ where mkPB (Let t v) = let t' = if (r /= t) then mkP lt l r t else t

94+ v' = if (r /= v) then mkP lt l r v else v in

95+ Let t' v'

96+ mkPB b = let ty = binderTy b

97+ ty' = if (r /= ty) then mkP lt l r ty else ty in

98+ b { binderTy = ty' }

99+ mkP lt l r x = x

100+

101+ -- If we're rewriting a dependent type, the rewrite type the rewrite

102+ -- may break the indices.

103+ -- So, for any function argument which can be determined by looking

104+ -- at the indices (i.e. any constructor guarded elsewhere in the type)

105+ -- replace it with a _. e.g. (++) a n m xs ys becomes (++) _ _ _ xs ys

106+ -- because a,n, and m are constructor guarded later in the type of ++

107+

108+ -- FIXME: Currently this is an approximation which just strips

109+ -- implicits. This is perfectly fine for most cases, but not as

110+ -- general as it should be.

111+ stripImpls tm = mapPT phApps tm

112+

113+ phApps (PApp fc f args) = PApp fc f (map removeImp args)

114+ where removeImp tm@(PImp{}) = tm { getTm = Placeholder }

115+ removeImp t = t

116+ phApps tm = tm

117+

118+doEquiv elab fc t sc

119+ = do attack

120+ tyn <- getNameFrom (sMN 0 "ety")

121+ claim tyn RType

122+ valn <- getNameFrom (sMN 0 "eqval")

123+ claim valn (Var tyn)

124+ letn <- getNameFrom (sMN 0 "equiv_val")

125+ letbind letn (Var tyn) (Var valn)

126+ focus tyn

127+ elab t

128+ focus valn

129+ elab sc

130+ elab (PRef fc [] letn)

131+ solve

132+

133+

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

@@ -22,6 +22,7 @@ import Idris.Coverage (buildSCG, checkDeclTotality, checkPositive, genClauses, r

2222import Idris.ErrReverse (errReverse)

2323import Idris.Elab.Quasiquote (extractUnquotes)

2424import Idris.Elab.Utils

25+import Idris.Elab.Rewrite

2526import Idris.Reflection

2627import qualified Util.Pretty as U

2728

@@ -995,39 +996,8 @@ elab ist info emode opts fn tm

995996 | not pattern = do mapM_ (runTac False ist fc fn) ts

996997 | otherwise = elab' ina fc Placeholder

997998 elab' ina fc (PElabError e) = lift $ tfail e

998− elab' ina _ (PRewrite fc r sc newg)

999− = do attack

1000− tyn <- getNameFrom (sMN 0 "rty")

1001− claim tyn RType

1002− valn <- getNameFrom (sMN 0 "rval")

1003− claim valn (Var tyn)

1004− letn <- getNameFrom (sMN 0 "_rewrite_rule")

1005− letbind letn (Var tyn) (Var valn)

1006− focus valn

1007− elab' ina (Just fc) r

1008− compute

1009− g <- goal

1010− rewrite (Var letn)

1011− g' <- goal

1012− when (g == g') $ lift $ tfail (NoRewriting g)

1013− case newg of

1014− Nothing -> elab' ina (Just fc) sc

1015− Just t -> doEquiv t sc

1016− solve

1017− where doEquiv t sc =

1018− do attack

1019− tyn <- getNameFrom (sMN 0 "ety")

1020− claim tyn RType

1021− valn <- getNameFrom (sMN 0 "eqval")

1022− claim valn (Var tyn)

1023− letn <- getNameFrom (sMN 0 "equiv_val")

1024− letbind letn (Var tyn) (Var valn)

1025− focus tyn

1026− elab' ina (Just fc) t

1027− focus valn

1028− elab' ina (Just fc) sc

1029− elab' ina (Just fc) (PRef fc [] letn)

1030− solve

999+ elab' ina _ (PRewrite fc substfn rule sc newg)

1000+ = elabRewrite (elab' ina (Just fc)) ist fc substfn rule sc newg

10311001 elab' ina _ c@(PCase fc scr opts)

10321002 = do attack

10331003

src/Idris/Error.hs+2−2

@@ -106,8 +106,8 @@ warnDisamb ist (PCase _ tm cases) = warnDisamb ist tm >>

106106warnDisamb ist (PIfThenElse _ c t f) = mapM_ (warnDisamb ist) [c, t, f]

107107warnDisamb ist (PTrue _ _) = return ()

108108warnDisamb ist (PResolveTC _) = return ()

109−warnDisamb ist (PRewrite _ x y z) = warnDisamb ist x >> warnDisamb ist y >>

110− Foldable.mapM_ (warnDisamb ist) z

109+warnDisamb ist (PRewrite _ _ x y z) = warnDisamb ist x >> warnDisamb ist y >>

110+ Foldable.mapM_ (warnDisamb ist) z

111111warnDisamb ist (PPair _ _ _ x y) = warnDisamb ist x >> warnDisamb ist y

112112warnDisamb ist (PDPair _ _ _ x y z) = warnDisamb ist x >> warnDisamb ist y >> warnDisamb ist z

113113warnDisamb ist (PAlternative _ _ tms) = mapM_ (warnDisamb ist) tms

src/Idris/IBC.hs+9−7

@@ -40,7 +40,7 @@ import System.Directory

4040import Codec.Archive.Zip

4141

4242ibcVersion :: Word16

43−ibcVersion = 136

43+ibcVersion = 137

4444

4545-- When IBC is being loaded - we'll load different things (and omit different

4646-- structures/definitions) depending on which phase we're in

@@ -1732,11 +1732,12 @@ instance Binary PTerm where

17321732 put x2

17331733 PResolveTC x1 -> do putWord8 15

17341734 put x1

1735− PRewrite x1 x2 x3 x4 -> do putWord8 17

1736− put x1

1737− put x2

1738− put x3

1739− put x4

1735+ PRewrite x1 x2 x3 x4 x5 -> do putWord8 17

1736+ put x1

1737+ put x2

1738+ put x3

1739+ put x4

1740+ put x5

17401741 PPair x1 x2 x3 x4 x5 -> do putWord8 18

17411742 put x1

17421743 put x2

@@ -1887,7 +1888,8 @@ instance Binary PTerm where

18871888 x2 <- get

18881889 x3 <- get

18891890 x4 <- get

1890− return (PRewrite x1 x2 x3 x4)

1891+ x5 <- get

1892+ return (PRewrite x1 x2 x3 x4 x5)

18911893 18 -> do x1 <- get

18921894 x2 <- get

18931895 x3 <- get

src/Idris/IdrisDoc.hs+2−2

@@ -304,9 +304,9 @@ extractPTermNames (PMatchApp _ n) = [n]

304304extractPTermNames (PCase _ p ps) = let (ps1, ps2) = unzip ps

305305 in concatMap extract (p:(ps1 ++ ps2))

306306extractPTermNames (PIfThenElse _ c t f) = concatMap extract [c, t, f]

307−extractPTermNames (PRewrite _ a b m) | Just c <- m =

307+extractPTermNames (PRewrite _ _ a b m) | Just c <- m =

308308 concatMap extract [a, b, c]

309−extractPTermNames (PRewrite _ a b _) = concatMap extract [a, b]

309+extractPTermNames (PRewrite _ _ a b _) = concatMap extract [a, b]

310310extractPTermNames (PPair _ _ _ p1 p2) = concatMap extract [p1, p2]

311311extractPTermNames (PDPair _ _ _ a b c) = concatMap extract [a, b, c]

312312extractPTermNames (PAlternative _ _ l) = concatMap extract l

src/Idris/Parser/Expr.hs+6−5

@@ -200,8 +200,8 @@ updateSynMatch = update

200200 = PIfThenElse fc (update ns c) (update ns t) (update ns f)

201201 update ns (PCase fc c opts)

202202 = PCase fc (update ns c) (map (pmap (update ns)) opts)

203− update ns (PRewrite fc eq tm mty)

204− = PRewrite fc (update ns eq) (update ns tm) (fmap (update ns) mty)

203+ update ns (PRewrite fc by eq tm mty)

204+ = PRewrite fc by (update ns eq) (update ns tm) (fmap (update ns) mty)

205205 update ns (PPair fc hls p l r) = PPair fc hls p (update ns l) (update ns r)

206206 update ns (PDPair fc hls p l t r)

207207 = PDPair fc hls p (update ns l) (update ns t) (update ns r)

@@ -949,12 +949,13 @@ rewriteTerm syn = do kw <- reservedFC "rewrite"

949949 fc <- getFC

950950 prf <- expr syn

951951 giving <- optional (do symbol "==>"; expr' syn)

952+ using <- optional (do reserved "using"

953+ (n, _) <- name

954+ return n)

952955 kw' <- reservedFC "in"; sc <- expr syn

953956 highlightP kw AnnKeyword

954957 highlightP kw' AnnKeyword

955− return (PRewrite fc

956− (PApp fc (PRef fc [] (sUN "sym")) [pexp prf]) sc

957− giving)

958+ return (PRewrite fc using prf sc giving)

958959 <?> "term rewrite expression"

959960

960961{- |Parses a let binding

test/primitives006/run+1−1

@@ -3,4 +3,4 @@ ${CC:-cc} -c -O2 -o array.o array.c $(${IDRIS:-idris} --include)

33${IDRIS:-idris} $@ -o load-test load-test.idr --nocolour --warnreach

44./load-test

55rm -f load-test *.o *.ibc

6−find -name \*.ibc -delete

6+rm -f Data/*.ibc

test/proof011/expectednew file+6

@@ -0,0 +1,6 @@

1+proof011.idr:19:9:

2+When checking right hand side of vassoc' with expected type

3+ (x :: xs) ++ ys ++ zs = ((x :: xs) ++ ys) ++ zs

4+

5+rewrite did not change type x :: xs ++ ys ++ zs =

6+ x :: (xs ++ ys) ++ zs

test/proof011/proof011.idrnew file+21

@@ -0,0 +1,21 @@

1+import Data.Vect

2+

3+vreplace : {xs : Vect n a} -> {ys : Vect m a} ->

4+ (P : {len : Nat} -> Vect len a -> Type) ->

5+ xs = ys -> P ys -> P xs

6+vreplace P Refl prop = prop

7+

8+total

9+vassoc : (xs : Vect n a) -> (ys : Vect m a) -> (zs : Vect p a) ->

10+ xs ++ (ys ++ zs) = (xs ++ ys) ++ zs

11+vassoc [] ys zs = Refl

12+vassoc (x :: xs) ys zs

13+ = rewrite vassoc xs ys zs using vreplace in

14+ Refl

15+total

16+vassoc' : (xs : Vect n a) -> (ys : Vect m a) -> (zs : Vect p a) ->

17+ xs ++ (ys ++ zs) = (xs ++ ys) ++ zs

18+vassoc' [] ys zs = Refl

19+vassoc' (x :: xs) ys zs

20+ = rewrite vassoc xs ys xs using vreplace in

21+ Refl

test/proof011/runnew file+3

@@ -0,0 +1,3 @@

1+#!/usr/bin/env bash

2+${IDRIS:-idris} $@ proof011.idr --nocolour --check

3+rm -f *.ibc