db5973b · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Added rewrite ... in ... construct

rewrite prf in v rewrites the goal type using prf. It is equivalent to applying replace, without the need to provide a predicate. It works by applying the rewrite tactic with prf before elaborating v.

commitdb5973bd5a7885d48c547e32744a004553421448 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateMon 18 Mar 2013, 21:53 (14 years ago) parent93819ed

9 files changed+70−3

compare with master

unifiedsplit

src/Core/CoreParser.hs+1−1 src/Core/TT.hs+2 src/Idris/AbsSyntax.hs+15 src/Idris/AbsSyntaxTree.hs+13 src/Idris/Delaborate.hs+1 src/Idris/ElabTerm.hs+17 src/Idris/IBC.hs+8 src/Idris/Parser.hs+9 test/reg012/reg012.lidr+4−2

src/Core/CoreParser.hs+1−1

@@ -31,7 +31,7 @@ idrisDef = haskellDef {

3131 = ["let", "in", "data", "codata", "record", "Type",

3232 "do", "dsl", "import", "impossible",

3333 "case", "of", "total", "partial", "mutual",

34− "infix", "infixl", "infixr",

34+ "infix", "infixl", "infixr", "rewrite",

3535 "where", "with", "syntax", "proof", "postulate",

3636 "using", "namespace", "class", "instance",

3737 "public", "private", "abstract", "implicit",

src/Core/TT.hs+2

@@ -69,6 +69,7 @@ data Err = Msg String

6969 | NonCollapsiblePostulate Name

7070 | AlreadyDefined Name

7171 | ProofSearchFail Err

72+ | NoRewriting Term

7273 | At FC Err

7374 deriving Eq

7475

@@ -82,6 +83,7 @@ instance Sized Err where

8283 size (NoTypeDecl name) = size name

8384 size (NotInjective l c r) = size l + size c + size r

8485 size (CantResolve trm) = size trm

86+ size (NoRewriting trm) = size trm

8587 size (CantResolveAlts _) = 1

8688 size (IncompleteTerm trm) = size trm

8789 size UniverseError = 1

src/Idris/AbsSyntax.hs+15

@@ -497,6 +497,7 @@ expandParams dec ps ns infs tm = en tm

497497 PLet n' (en ty) (en v) (en (shadow n n' s))

498498 | otherwise = PLet n (en ty) (en v) (en s)

499499 en (PEq f l r) = PEq f (en l) (en r)

500+ en (PRewrite f l r) = PRewrite f (en l) (en r)

500501 en (PTyped l r) = PTyped (en l) (en r)

501502 en (PPair f l r) = PPair f (en l) (en r)

502503 en (PDPair f l t r) = PDPair f (en l) (en t) (en r)

@@ -632,6 +633,7 @@ getPriority i tm = 1 -- pri tm

632633 pri (PFalse _) = 0

633634 pri (PRefl _ _) = 1

634635 pri (PEq _ l r) = max 1 (max (pri l) (pri r))

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

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

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

637639 pri (PTyped l r) = pri l

@@ -742,6 +744,10 @@ implicitise syn ignore ist tm

742744 = do (decls, ns) <- get

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

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

747+ imps top env (PRewrite _ l r)

748+ = do (decls, ns) <- get

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

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

745751 imps top env (PTyped l r)

746752 = imps top env l

747753 imps top env (PPair _ l r)

@@ -801,6 +807,9 @@ addImpl' inpat env infns ist ptm = ai (zip env (repeat Nothing)) ptm

801807 ai env (PEq fc l r) = let l' = ai env l

802808 r' = ai env r in

803809 PEq fc l' r'

810+ ai env (PRewrite fc l r) = let l' = ai env l

811+ r' = ai env r in

812+ PRewrite fc l' r'

804813 ai env (PTyped l r) = let l' = ai env l

805814 r' = ai env r in

806815 PTyped l' r'

@@ -1056,6 +1065,10 @@ matchClause' names i x y = checkRpts $ match (fullApp x) (fullApp y) where

10561065 match (PEq _ l r) (PEq _ l' r') = do ml <- match' l l'

10571066 mr <- match' r r'

10581067 return (ml ++ mr)

1068+ match (PRewrite _ l r) (PRewrite _ l' r')

1069+ = do ml <- match' l l'

1070+ mr <- match' r r'

1071+ return (ml ++ mr)

10591072 match (PTyped l r) (PTyped l' r') = do ml <- match l l'

10601073 mr <- match r r'

10611074 return (ml ++ mr)

@@ -1137,6 +1150,7 @@ substMatchShadow n shs tm t = sm shs t where

11371150 sm xs (PApp f x as) = PApp f (sm xs x) (map (fmap (sm xs)) as)

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

11391152 sm xs (PEq f x y) = PEq f (sm xs x) (sm xs y)

1153+ sm xs (PRewrite f x y) = PRewrite f (sm xs x) (sm xs y)

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

11411155 sm xs (PPair f x y) = PPair f (sm xs x) (sm xs y)

11421156 sm xs (PDPair f x t y) = PDPair f (sm xs x) (sm xs t) (sm xs y)

@@ -1152,6 +1166,7 @@ shadow n n' t = sm t where

11521166 sm (PApp f x as) = PApp f (sm x) (map (fmap sm) as)

11531167 sm (PCase f x as) = PCase f (sm x) (map (pmap sm) as)

11541168 sm (PEq f x y) = PEq f (sm x) (sm y)

1169+ sm (PRewrite f x y) = PRewrite f (sm x) (sm y)

11551170 sm (PTyped x y) = PTyped (sm x) (sm y)

11561171 sm (PPair f x y) = PPair f (sm x) (sm y)

11571172 sm (PDPair f x t y) = PDPair f (sm x) (sm t) (sm y)

src/Idris/AbsSyntaxTree.hs+13

@@ -442,6 +442,7 @@ data PTerm = PQuote Raw

442442 | PRefl FC PTerm

443443 | PResolveTC FC

444444 | PEq FC PTerm PTerm

445+ | PRewrite FC PTerm PTerm

445446 | PPair FC PTerm PTerm

446447 | PDPair FC PTerm PTerm PTerm

447448 | PAlternative Bool [PTerm] -- True if only one may work

@@ -468,6 +469,7 @@ mapPT f t = f (mpt t) where

468469 mpt (PLam n t s) = PLam n (mapPT f t) (mapPT f s)

469470 mpt (PPi p n t s) = PPi p n (mapPT f t) (mapPT f s)

470471 mpt (PLet n ty v s) = PLet n (mapPT f ty) (mapPT f v) (mapPT f s)

472+ mpt (PRewrite fc t s) = PRewrite fc (mapPT f t) (mapPT f s)

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

472474 mpt (PCase fc c os) = PCase fc (mapPT f c) (map (pmap (mapPT f)) os)

473475 mpt (PEq fc l r) = PEq fc (mapPT f l) (mapPT f r)

@@ -878,6 +880,12 @@ prettyImp impl = prettySe 10

878880 prettySe 10 l <+> text "=" $$ nest nestingSize (prettySe 10 r)

879881 else

880882 prettySe 10 l <+> text "=" <+> prettySe 10 r

883+ prettySe p (PRewrite _ l r) =

884+ bracket p 2 $

885+ if size r > breakingSize then

886+ text "rewrite" <+> prettySe 10 l <+> text "in" $$ nest nestingSize (prettySe 10 r)

887+ else

888+ text "rewrite" <+> prettySe 10 l <+> text "in" <+> prettySe 10 r

881889 prettySe p (PTyped l r) =

882890 lparen <> prettySe 10 l <+> colon <+> prettySe 10 r <> rparen

883891 prettySe p (PPair _ l r) =

@@ -985,6 +993,7 @@ showImp impl tm = se 10 tm where

985993 se p (PTrue _) = "()"

986994 se p (PFalse _) = "_|_"

987995 se p (PEq _ l r) = bracket p 2 $ se 10 l ++ " = " ++ se 10 r

996+ se p (PRewrite _ l r) = bracket p 2 $ "rewrite " ++ se 10 l ++ " in " ++ se 10 r

988997 se p (PTyped l r) = "(" ++ se 10 l ++ " : " ++ se 10 r ++ ")"

989998 se p (PPair _ l r) = "(" ++ se 10 l ++ ", " ++ se 10 r ++ ")"

990999 se p (PDPair _ l t r) = "(" ++ se 10 l ++ " ** " ++ se 10 r ++ ")"

@@ -1030,6 +1039,7 @@ instance Sized PTerm where

10301039 size (PRefl fc _) = 1

10311040 size (PResolveTC fc) = 1

10321041 size (PEq fc left right) = 1 + size left + size right

1042+ size (PRewrite fc left right) = 1 + size left + size right

10331043 size (PPair fc left right) = 1 + size left + size right

10341044 size (PDPair fs left ty right) = 1 + size left + size ty + size right

10351045 size (PAlternative a alts) = 1 + size alts

@@ -1062,6 +1072,7 @@ allNamesIn tm = nub $ ni [] tm

10621072 ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc

10631073 ni env (PHidden tm) = ni env tm

10641074 ni env (PEq _ l r) = ni env l ++ ni env r

1075+ ni env (PRewrite _ l r) = ni env l ++ ni env r

10651076 ni env (PTyped l r) = ni env l ++ ni env r

10661077 ni env (PPair _ l r) = ni env l ++ ni env r

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

@@ -1084,6 +1095,7 @@ namesIn uvars ist tm = nub $ ni [] tm

10841095 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc

10851096 ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc

10861097 ni env (PEq _ l r) = ni env l ++ ni env r

1098+ ni env (PRewrite _ l r) = ni env l ++ ni env r

10871099 ni env (PTyped l r) = ni env l ++ ni env r

10881100 ni env (PPair _ l r) = ni env l ++ ni env r

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

@@ -1107,6 +1119,7 @@ usedNamesIn vars ist tm = nub $ ni [] tm

11071119 ni env (PLam n ty sc) = ni env ty ++ ni (n:env) sc

11081120 ni env (PPi _ n ty sc) = ni env ty ++ ni (n:env) sc

11091121 ni env (PEq _ l r) = ni env l ++ ni env r

1122+ ni env (PRewrite _ l r) = ni env l ++ ni env r

11101123 ni env (PTyped l r) = ni env l ++ ni env r

11111124 ni env (PPair _ l r) = ni env l ++ ni env r

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

src/Idris/Delaborate.hs+1

@@ -109,6 +109,7 @@ pshow i (NonCollapsiblePostulate n)

109109 = "The return type of postulate " ++ show n ++ " is not collapsible"

110110pshow i (AlreadyDefined n) = show n ++ " is already defined"

111111pshow i (ProofSearchFail e) = pshow i e

112+pshow i (NoRewriting tm) = "rewrite did not change type " ++ show (delab i tm)

112113pshow i (At f e) = show f ++ ":" ++ pshow i e

113114

114115showSc i [] = ""

src/Idris/ElabTerm.hs+17

@@ -407,6 +407,23 @@ elab ist info pattern tcgen fn tm

407407 | not pattern = do mapM_ (runTac False ist) ts

408408 | otherwise = elab' ina Placeholder

409409 elab' ina (PElabError e) = fail (pshow ist e)

410+ elab' ina (PRewrite fc r sc)

411+ = do attack

412+ tyn <- unique_hole (MN 0 "rty")

413+ claim tyn RType

414+ valn <- unique_hole (MN 0 "rval")

415+ claim valn (Var tyn)

416+ letn <- unique_hole (MN 0 "rewrite_rule")

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

418+ focus valn

419+ elab' ina r

420+ compute

421+ g <- goal

422+ rewrite (Var letn)

423+ g' <- goal

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

425+ elab' ina sc

426+ solve

410427 elab' ina@(_, a) c@(PCase fc scr opts)

411428 = do attack

412429 tyn <- unique_hole (MN 0 "scty")

src/Idris/IBC.hs+8

@@ -1257,6 +1257,10 @@ instance Binary PTerm where

12571257 PInferRef x1 x2 -> do putWord8 29

12581258 put x1

12591259 put x2

1260+ PRewrite x1 x2 x3 -> do putWord8 30

1261+ put x1

1262+ put x2

1263+ put x3

12601264 get

12611265 = do i <- getWord8

12621266 case i of

@@ -1341,6 +1345,10 @@ instance Binary PTerm where

13411345 29 -> do x1 <- get

13421346 x2 <- get

13431347 return (PInferRef x1 x2)

1348+ 30 -> do x1 <- get

1349+ x2 <- get

1350+ x3 <- get

1351+ return (PRewrite x1 x2 x3)

13441352 _ -> error "Corrupted binary data for PTerm"

13451353

13461354instance (Binary t) => Binary (PTactic' t) where

src/Idris/Parser.hs+9

@@ -606,6 +606,7 @@ pNoExtExpr syn =

606606 <|> try (pSimpleExpr syn)

607607 <|> pLambda syn

608608 <|> pLet syn

609+ <|> pRewriteTerm syn

609610 <|> pPi syn

610611 <|> pDoBlock syn

611612 <|> pComprehension syn

@@ -936,6 +937,14 @@ pLambda syn = do lchar '\\'

936937 (PCase fc (PRef fc (MN i "lamp"))

937938 [(x, pmList xs sc)])

938939

940+pRewriteTerm syn =

941+ do reserved "rewrite"

942+ fc <- pfc

943+ prf <- pExpr syn

944+ reserved "in"; sc <- pExpr syn

945+ return (PRewrite fc

946+ (PApp fc (PRef fc (UN "sym")) [pexp prf]) sc)

947+

939948pLet syn = try (do reserved "let"; n <- pName;

940949 ty <- option Placeholder (do lchar ':'; pExpr' syn)

941950 lchar '='

test/reg012/reg012.lidr+4−2

@@ -28,5 +28,7 @@

2828> (ab : (alpha, beta)) ->

2929> modifyFun f ab (fst ab) = snd ab

3030> modifyFunLemma f (a,b) =

31−> replace {P = \ z => boolElim (a == a) b (f a) = boolElim z b (f a)}

32−> (soTrue (reflexive_eqeq a)) refl

31+> rewrite soTrue (reflexive_eqeq a) in refl

32+

33+ replace {P = \ z => boolElim (a == a) b (f a) = boolElim z b (f a)}

34+ (soTrue (reflexive_eqeq a)) refl