96a982a · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Add do-rewrite

commit96a982aa2f09e83f3ab137c08e1eb01d95cd0f59 authorbe5invis <belleve@typeof.net> dateSun 4 Jun 2017, 18:53 (9 years ago) parenta859f65

8 files changed+27

compare with master

unifiedsplit

src/Idris/AbsSyntaxTree.hs+7 src/Idris/DSL.hs+2 src/Idris/Elab/Quasiquote.hs+1 src/Idris/Error.hs+1 src/Idris/IBC.hs+7 src/Idris/IdrisDoc.hs+1 src/Idris/Parser/Expr.hs+7 src/Idris/Prover.hs+1

src/Idris/AbsSyntaxTree.hs+7

@@ -1177,6 +1177,7 @@ mapPTermFC f g (PDoBlock dos) = PDoBlock (map mapPDoFC dos)

11771177 DoBindP (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2) (map (\(l,r)-> (mapPTermFC f g l, mapPTermFC f g r)) alts)

11781178 mapPDoFC (DoLet fc n nfc t1 t2) = DoLet (f fc) n (g nfc) (mapPTermFC f g t1) (mapPTermFC f g t2)

11791179 mapPDoFC (DoLetP fc t1 t2) = DoLetP (f fc) (mapPTermFC f g t1) (mapPTermFC f g t2)

1180+ mapPDoFC (DoRewrite fc h) = DoRewrite (f fc) (mapPTermFC f g h)

11801181mapPTermFC f g (PIdiom fc t) = PIdiom (f fc) (mapPTermFC f g t)

11811182mapPTermFC f g (PMetavar fc n) = PMetavar (g fc) n

11821183mapPTermFC f g (PProof tacs) = PProof (map (fmap (mapPTermFC f g)) tacs)

@@ -1301,6 +1302,7 @@ data PDo' t = DoExp FC t

13011302 | DoBindP FC t t [(t,t)]

13021303 | DoLet FC Name FC t t -- ^ second FC is precise name location

13031304 | DoLetP FC t t

1305+ | DoRewrite FC t -- rewrite in do block

13041306 deriving (Eq, Ord, Functor, Data, Generic, Typeable)

13051307{-!

13061308deriving instance Binary PDo'

@@ -1312,6 +1314,7 @@ instance Sized a => Sized (PDo' a) where

13121314 size (DoBindP fc l r alts) = 1 + size fc + size l + size r + size alts

13131315 size (DoLet fc nm nfc l r) = 1 + size fc + size nm + size l + size r

13141316 size (DoLetP fc l r) = 1 + size fc + size l + size r

1317+ size (DoRewrite fc h) = 1 + size fc + size h

13151318

13161319type PDo = PDo' PTerm

13171320

@@ -1407,6 +1410,7 @@ highestFC (PDoBlock lines) =

14071410 getDoFC (DoBindP fc l r alts) = fc

14081411 getDoFC (DoLet fc nm nfc l r) = fc

14091412 getDoFC (DoLetP fc l r) = fc

1413+ getDoFC (DoRewrite fc h) = fc

14101414

14111415highestFC (PIdiom fc _) = Just fc

14121416highestFC (PMetavar fc _) = Just fc

@@ -2081,6 +2085,9 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd

20812085 ppdo bnd (DoLetP _ _ _ : dos) = -- ok because never made by delab

20822086 text "no pretty printer for pattern-matching do binding" :

20832087 ppdo bnd dos

2088+ ppdo bnd (DoRewrite _ _ : dos) = -- ok because never made by delab

2089+ text "no pretty printer for pattern-matching do binding" :

2090+ ppdo bnd dos

20842091 ppdo _ [] = []

20852092 prettySe d p bnd (PCoerced t) = prettySe d p bnd t

20862093 prettySe d p bnd (PElabError s) = pretty s

src/Idris/DSL.hs+2

@@ -109,6 +109,8 @@ expandSugar dsl (PDoBlock ds)

109109 = PLet fc n nfc ty tm (block b rest)

110110 block b (DoLetP fc p tm : rest)

111111 = PCase fc tm [(p, block b rest)]

112+ block b (DoRewrite fc h : rest)

113+ = PRewrite fc Nothing h (block b rest) Nothing

112114 block b (DoExp fc tm : rest)

113115 = PApp fc b

114116 [pexp tm,

src/Idris/Elab/Quasiquote.hs+1

@@ -75,6 +75,7 @@ extractDoUnquotes d (DoLet fc n nfc v b)

7575 (b', ex2) <- extractUnquotes d b

7676 return (DoLet fc n nfc v' b', ex1 ++ ex2)

7777extractDoUnquotes d (DoLetP fc t t') = fail "Pattern-matching lets cannot be quasiquoted"

78+extractDoUnquotes d (DoRewrite fc h) = fail "Rewrites in Do block cannot be quasiquoted"

7879

7980

8081extractUnquotes :: Int -> PTerm -> Elab' aux (PTerm, [(Name, PTerm)])

src/Idris/Error.hs+1

@@ -138,6 +138,7 @@ warnDisamb ist (PDoBlock steps) = mapM_ wStep steps

138138 mapM_ (\(x,y) -> warnDisamb ist x >> warnDisamb ist y) cs

139139 wStep (DoLet _ _ _ x y) = warnDisamb ist x >> warnDisamb ist y

140140 wStep (DoLetP _ x y) = warnDisamb ist x >> warnDisamb ist y

141+ wStep (DoRewrite _ h) = warnDisamb ist h

141142warnDisamb ist (PIdiom _ x) = warnDisamb ist x

142143warnDisamb ist (PMetavar _ _) = return ()

143144warnDisamb ist (PProof tacs) = mapM_ (Foldable.mapM_ (warnDisamb ist)) tacs

src/Idris/IBC.hs+7

@@ -2292,6 +2292,9 @@ instance (Binary t) => Binary (PDo' t) where

22922292 put x1

22932293 put x2

22942294 put x3

2295+ DoRewrite x1 x2 -> do putWord8 3

2296+ put x1

2297+ put x2

22952298 get

22962299 = do i <- getWord8

22972300 case i of

@@ -2318,6 +2321,10 @@ instance (Binary t) => Binary (PDo' t) where

23182321 x2 <- get

23192322 x3 <- get

23202323 return (DoLetP x1 x2 x3)

2324+ 5 -> do

2325+ x1 <- get

2326+ x2 <- get

2327+ return (DoRewrite x1 x2)

23212328 _ -> error "Corrupted binary data for PDo'"

23222329

23232330

src/Idris/IdrisDoc.hs+1

@@ -343,6 +343,7 @@ extractPDo (DoBindP _ p1 p2 ps) = let (ps1, ps2) = unzip ps

343343 in concatMap extract (p1 : p2 : ps')

344344extractPDo (DoLet _ n _ p1 p2) = n : concatMap extract [p1, p2]

345345extractPDo (DoLetP _ p1 p2) = concatMap extract [p1, p2]

346+extractPDo (DoRewrite _ p) = extract p

346347

347348-- | Helper function for extractPTermNames

348349extractPTactic :: PTactic -> [Name]

src/Idris/Parser/Expr.hs+7

@@ -233,6 +233,7 @@ updateSynMatch = update

233233 = DoBindP fc (update ns i) (update ns t)

234234 (map (\(l,r) -> (update ns l, update ns r)) ts)

235235 upd ns (DoLetP fc i t) = DoLetP fc (update ns i) (update ns t)

236+ upd ns (DoRewrite fc h) = DoRewrite fc (update ns h)

236237 update ns (PIdiom fc t) = PIdiom fc $ update ns t

237238 update ns (PMetavar fc n) = uncurry (flip PMetavar) $ updateB ns (n, fc)

238239 update ns (PProof tacs) = PProof $ map (updTactic ns) tacs

@@ -1342,6 +1343,7 @@ doBlock syn

13421343Do ::=

13431344 'let' Name TypeSig'? '=' Expr

13441345 | 'let' Expr' '=' Expr

1346+ | 'rewrite Expr

13451347 | Name '<-' Expr

13461348 | Expr' '<-' Expr

13471349 | Expr

@@ -1366,6 +1368,11 @@ do_ syn

13661368 sc <- expr syn

13671369 highlightP kw AnnKeyword

13681370 return (DoLetP fc i sc))

1371+ <|> try (do kw <- reservedFC "rewrite"

1372+ fc <- getFC

1373+ sc <- expr syn

1374+ highlightP kw AnnKeyword

1375+ return (DoRewrite fc sc))

13691376 <|> try (do (i, ifc) <- name

13701377 symbol "<-"

13711378 fc <- getFC

src/Idris/Prover.hs+1

@@ -349,6 +349,7 @@ elabloop info fn d prompt prf e prev h env

349349 Success (Right cmd') ->

350350 case cmd' of

351351 DoLetP {} -> ifail "Pattern-matching let not supported here"

352+ DoRewrite {} -> ifail "Pattern-matching do-rewrite not supported here"

352353 DoBindP {} -> ifail "Pattern-matching <- not supported here"

353354 DoLet fc i ifc Placeholder expr ->

354355 do (tm, ty) <- elabVal (recinfo proverfc) ERHS (inLets ist env expr)