db5973b · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Added rewrite ... in ... construct

db5973bEdwin Brady14 years ago

src/Core/CoreParser.hs+1−1

compare with master

unifiedsplit

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

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

32 "do", "dsl", "import", "impossible",

33 "case", "of", "total", "partial", "mutual",

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

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

35 "where", "with", "syntax", "proof", "postulate",

36 "using", "namespace", "class", "instance",

37 "public", "private", "abstract", "implicit",

src/Core/TT.hs+2

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

69 | NonCollapsiblePostulate Name

70 | AlreadyDefined Name

71 | ProofSearchFail Err

72+ | NoRewriting Term

72 | At FC Err

73 | At FC Err

73 deriving Eq

74 deriving Eq

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

82 size (NoTypeDecl name) = size name

83 size (NoTypeDecl name) = size name

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

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

84 size (CantResolve trm) = size trm

85 size (CantResolve trm) = size trm

86+ size (NoRewriting trm) = size trm

85 size (CantResolveAlts _) = 1

87 size (CantResolveAlts _) = 1

86 size (IncompleteTerm trm) = size trm

88 size (IncompleteTerm trm) = size trm

87 size UniverseError = 1

89 size UniverseError = 1

src/Idris/AbsSyntax.hs+15

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

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

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

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

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

500 en (PTyped l r) = PTyped (en l) (en r)

501 en (PTyped l r) = PTyped (en l) (en r)

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

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

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

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

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

632 pri (PFalse _) = 0

633 pri (PFalse _) = 0

633 pri (PRefl _ _) = 1

634 pri (PRefl _ _) = 1

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

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

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

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

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

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

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

637 pri (PTyped l r) = pri l

639 pri (PTyped l r) = pri l

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

742 = do (decls, ns) <- get

744 = do (decls, ns) <- get

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

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

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

746 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)))))

745 imps top env (PTyped l r)

751 imps top env (PTyped l r)

746 = imps top env l

752 = imps top env l

747 imps top env (PPair _ l r)

753 imps top env (PPair _ l r)

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

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

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

802 r' = ai env r in

808 r' = ai env r in

803 PEq fc l' r'

809 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'

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

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

805 r' = ai env r in

814 r' = ai env r in

806 PTyped l' r'

815 PTyped l' r'

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

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

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

1057 mr <- match' r r'

1066 mr <- match' r r'

1058 return (ml ++ mr)

1067 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)

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

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

1060 mr <- match r r'

1073 mr <- match r r'

1061 return (ml ++ mr)

1074 return (ml ++ mr)

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

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

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

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

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

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

1152 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)

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

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

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

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

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

1156 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

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

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

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

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

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

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

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

1155 sm (PTyped x y) = PTyped (sm x) (sm y)

1170 sm (PTyped x y) = PTyped (sm x) (sm y)

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

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

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

1172 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

442 | PRefl FC PTerm

443 | PResolveTC FC

444 | PEq FC PTerm PTerm

445+ | PRewrite FC PTerm PTerm

445 | PPair FC PTerm PTerm

446 | PPair FC PTerm PTerm

446 | PDPair FC PTerm PTerm PTerm

447 | PDPair FC PTerm PTerm PTerm

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

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

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

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

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

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

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

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

471 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)

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

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

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

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

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

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

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

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

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

879 else

881 else

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

882 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

881 prettySe p (PTyped l r) =

889 prettySe p (PTyped l r) =

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

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

883 prettySe p (PPair _ l r) =

891 prettySe p (PPair _ l r) =

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

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

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

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

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

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

995 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

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

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

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

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

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

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

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

1030 size (PRefl fc _) = 1

1039 size (PRefl fc _) = 1

1031 size (PResolveTC fc) = 1

1040 size (PResolveTC fc) = 1

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

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

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

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

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

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

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

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

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

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

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

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

1063 ni env (PHidden tm) = ni env tm

1073 ni env (PHidden tm) = ni env tm

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

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

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

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

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

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

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

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

1078 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

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

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

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

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

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

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

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

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

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

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

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

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

1101 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

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

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

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

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

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

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

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

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

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

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

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

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

1125 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)

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

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

111pshow i (ProofSearchFail e) = pshow i e

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

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

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

113

114

114showSc i [] = ""

115showSc i [] = ""

src/Idris/ElabTerm.hs+17

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

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

408 | otherwise = elab' ina Placeholder

409 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

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

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

411 = do attack

428 = do attack

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

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

src/Idris/IBC.hs+8

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

1257 PInferRef x1 x2 -> do putWord8 29

1258 put x1

1259 put x2

1260+ PRewrite x1 x2 x3 -> do putWord8 30

1261+ put x1

1262+ put x2

1263+ put x3

1260 get

1264 get

1261 = do i <- getWord8

1265 = do i <- getWord8

1262 case i of

1266 case i of

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

1341 29 -> do x1 <- get

1345 29 -> do x1 <- get

1342 x2 <- get

1346 x2 <- get

1343 return (PInferRef x1 x2)

1347 return (PInferRef x1 x2)

1348+ 30 -> do x1 <- get

1349+ x2 <- get

1350+ x3 <- get

1351+ return (PRewrite x1 x2 x3)

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

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

1345

1353

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

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

src/Idris/Parser.hs+9

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

606 <|> try (pSimpleExpr syn)

607 <|> pLambda syn

608 <|> pLet syn

609+ <|> pRewriteTerm syn

609 <|> pPi syn

610 <|> pPi syn

610 <|> pDoBlock syn

611 <|> pDoBlock syn

611 <|> pComprehension syn

612 <|> pComprehension syn

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

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

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

937 [(x, pmList xs sc)])

938 [(x, pmList xs sc)])

938

939

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+

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

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

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

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

941 lchar '='

950 lchar '='

test/reg012/reg012.lidr+4−2

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

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

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

30> modifyFunLemma f (a,b) =

31+> rewrite soTrue (reflexive_eqeq a) in refl

32+

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

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

32−> (soTrue (reflexive_eqeq a)) refl

34+ (soTrue (reflexive_eqeq a)) refl