7fc4865 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Allow 'rewrite ... in' to assert the resulting type

"rewrite f ==> t in x" means that after applying the rewrite f, the required type of x must be t. This is primarily for readability of proofs built by successive rewritings.

commit7fc48656f3101daeef08a2d4a8a59c3ef78b7f04 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateTue 9 Jul 2013, 12:17 (13 years ago) parent3448469

6 files changed+66−26

compare with master

unifiedsplit

lib/Language/Reflection.idr+2 src/Idris/AbsSyntax.hs+11−9 src/Idris/AbsSyntaxTree.hs+13−9 src/Idris/ElabTerm.hs+18−2 src/Idris/IBC.hs+17−5 src/Idris/Parser.hs+5−1

lib/Language/Reflection.idr+2

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

11module Language.Reflection

3+import Prelude.Vect

35%access public

57data TTName = UN String

src/Idris/AbsSyntax.hs+11−9

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

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

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

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

601− en (PRewrite f l r) = PRewrite f (en l) (en r)

601+ en (PRewrite f l r g) = PRewrite f (en l) (en r) (fmap en g)

602602 en (PTyped l r) = PTyped (en l) (en r)

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

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

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

735735 pri (PFalse _) = 0

736736 pri (PRefl _ _) = 1

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

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

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

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

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

741741 pri (PTyped l r) = pri l

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

892892 = do (decls, ns) <- get

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

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

895− imps top env (PRewrite _ l r)

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

896896 = do (decls, ns) <- get

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

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

@@ -956,9 +956,10 @@ addImpl' inpat env infns ist ptm = ai (zip env (repeat Nothing)) ptm

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

957957 r' = ai env r in

958958 PEq fc l' r'

959− ai env (PRewrite fc l r) = let l' = ai env l

960− r' = ai env r in

961− PRewrite fc l' r'

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

960+ r' = ai env r

961+ g' = fmap (ai env) g in

962+ PRewrite fc l' r' g'

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

963964 r' = ai env r in

964965 PTyped l' r'

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

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

12211222 mr <- match' r r'

12221223 return (ml ++ mr)

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

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

12241225 = do ml <- match' l l'

12251226 mr <- match' r r'

12261227 return (ml ++ mr)

@@ -1307,7 +1308,8 @@ substMatchShadow n shs tm t = sm shs t where

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

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

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

1310− sm xs (PRewrite f x y) = PRewrite f (sm xs x) (sm xs y)

1311+ sm xs (PRewrite f x y tm) = PRewrite f (sm xs x) (sm xs y)

1312+ (fmap (sm xs) tm)

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

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

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

@@ -1324,7 +1326,7 @@ shadow n n' t = sm t where

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

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

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

1327− sm (PRewrite f x y) = PRewrite f (sm x) (sm y)

1329+ sm (PRewrite f x y tm) = PRewrite f (sm x) (sm y) (fmap sm tm)

13281330 sm (PTyped x y) = PTyped (sm x) (sm y)

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

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

src/Idris/AbsSyntaxTree.hs+13−9

@@ -375,7 +375,10 @@ data PDecl' t

375375 | PMutual FC [PDecl' t] -- ^ Mutual block

376376 | PDirective (Idris ()) -- ^ Compiler directive. The parser inserts the corresponding action in the Idris monad.

377377 | PProvider SyntaxInfo FC Name t t -- ^ Type provider. The first t is the type, the second is the term

378− deriving Functor

378+ | PReflection FC Name -- type to reflect to

379+ t -- type of variables

380+ [PClause' t] -- ^ Pattern clauses

381+ deriving Functor

379382{-!

380383deriving instance Binary PDecl'

381384!-}

@@ -511,7 +514,7 @@ data PTerm = PQuote Raw

511514 | PRefl FC PTerm

512515 | PResolveTC FC

513516 | PEq FC PTerm PTerm

514− | PRewrite FC PTerm PTerm

517+ | PRewrite FC PTerm PTerm (Maybe PTerm)

515518 | PPair FC PTerm PTerm

516519 | PDPair FC PTerm PTerm PTerm

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

@@ -539,7 +542,8 @@ mapPT f t = f (mpt t) where

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

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

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

542− mpt (PRewrite fc t s) = PRewrite fc (mapPT f t) (mapPT f s)

545+ mpt (PRewrite fc t s g) = PRewrite fc (mapPT f t) (mapPT f s)

546+ (fmap (mapPT f) g)

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

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

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

@@ -965,7 +969,7 @@ prettyImp impl = prettySe 10

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

966970 else

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

968− prettySe p (PRewrite _ l r) =

972+ prettySe p (PRewrite _ l r _) =

969973 bracket p 2 $

970974 if size r > breakingSize then

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

@@ -1082,7 +1086,7 @@ showImp impl tm = se 10 tm where

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

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

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

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

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

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

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

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

@@ -1160,7 +1164,7 @@ instance Sized PTerm where

11601164 size (PRefl fc _) = 1

11611165 size (PResolveTC fc) = 1

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

1163− size (PRewrite fc left right) = 1 + size left + size right

1167+ size (PRewrite fc left right _) = 1 + size left + size right

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

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

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

@@ -1194,7 +1198,7 @@ allNamesIn tm = nub $ ni [] tm

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

11951199 ni env (PHidden tm) = ni env tm

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

1197− ni env (PRewrite _ l r) = ni env l ++ ni env r

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

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

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

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

@@ -1218,7 +1222,7 @@ namesIn uvars ist tm = nub $ ni [] tm

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

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

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

1221− ni env (PRewrite _ l r) = ni env l ++ ni env r

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

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

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

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

@@ -1243,7 +1247,7 @@ usedNamesIn vars ist tm = nub $ ni [] tm

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

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

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

1246− ni env (PRewrite _ l r) = ni env l ++ ni env r

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

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

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

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

src/Idris/ElabTerm.hs+18−2

@@ -420,7 +420,7 @@ elab ist info pattern tcgen fn tm

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

421421 | otherwise = elab' ina Placeholder

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

423− elab' ina (PRewrite fc r sc)

423+ elab' ina (PRewrite fc r sc newg)

424424 = do attack

425425 tyn <- unique_hole (MN 0 "rty")

426426 claim tyn RType

@@ -435,8 +435,24 @@ elab ist info pattern tcgen fn tm

435435 rewrite (Var letn)

436436 g' <- goal

437437 when (g == g') $ lift $ tfail (NoRewriting g)

438− elab' ina sc

438+ case newg of

439+ Nothing -> elab' ina sc

440+ Just t -> doEquiv t sc

439441 solve

442+ where doEquiv t sc =

443+ do attack

444+ tyn <- unique_hole (MN 0 "ety")

445+ claim tyn RType

446+ valn <- unique_hole (MN 0 "eqval")

447+ claim valn (Var tyn)

448+ letn <- unique_hole (MN 0 "equiv_val")

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

450+ focus tyn

451+ elab' ina t

452+ focus valn

453+ elab' ina sc

454+ elab' ina (PRef fc letn)

455+ solve

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

441457 = do attack

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

src/Idris/IBC.hs+17−5

@@ -1037,6 +1037,11 @@ instance (Binary t) => Binary (PDecl' t) where

10371037 put x4

10381038 put x5

10391039 put x6

1040+ PReflection x1 x2 x3 x4 -> do putWord8 13

1041+ put x1

1042+ put x2

1043+ put x3

1044+ put x4

10401045 get

10411046 = do i <- getWord8

10421047 case i of

@@ -1112,6 +1117,11 @@ instance (Binary t) => Binary (PDecl' t) where

11121117 x5 <- get

11131118 x6 <- get

11141119 return (PPostulate x1 x2 x3 x4 x5 x6)

1120+ 13 -> do x1 <- get

1121+ x2 <- get

1122+ x3 <- get

1123+ x4 <- get

1124+ return (PReflection x1 x2 x3 x4)

11151125 _ -> error "Corrupted binary data for PDecl'"

11161126

11171127instance Binary Using where

@@ -1306,10 +1316,11 @@ instance Binary PTerm where

13061316 PInferRef x1 x2 -> do putWord8 29

13071317 put x1

13081318 put x2

1309− PRewrite x1 x2 x3 -> do putWord8 30

1310− put x1

1311− put x2

1312− put x3

1319+ PRewrite x1 x2 x3 x4 -> do putWord8 30

1320+ put x1

1321+ put x2

1322+ put x3

1323+ put x4

13131324 get

13141325 = do i <- getWord8

13151326 case i of

@@ -1397,7 +1408,8 @@ instance Binary PTerm where

13971408 30 -> do x1 <- get

13981409 x2 <- get

13991410 x3 <- get

1400− return (PRewrite x1 x2 x3)

1411+ x4 <- get

1412+ return (PRewrite x1 x2 x3 x4)

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

14021414

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

src/Idris/Parser.hs+5−1

@@ -974,9 +974,13 @@ pRewriteTerm syn =

974974 do reserved "rewrite"

975975 fc <- pfc

976976 prf <- pExpr syn

977+ giving <- option Nothing

978+ (do symbol "==>"; tm <- pExpr' syn

979+ return (Just tm))

977980 reserved "in"; sc <- pExpr syn

978981 return (PRewrite fc

979− (PApp fc (PRef fc (UN "sym")) [pexp prf]) sc)

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

983+ giving)

980984

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

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