aa0b315 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge pull request #3847 from be5invis/be5invis-do-rewrite

Add do-rewrite construction

commitaa0b315625ba6d765282f9367bc02cf0f5db75e0 authorNiklas Larsson <metaniklas@gmail.com> dateWed 26 Jul 2017, 16:08 (9 years ago) parentcc45cdd 0e3922b

8 files changed+28−1

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+8−1 src/Idris/IdrisDoc.hs+1 src/Idris/Parser/Expr.hs+7 src/Idris/Prover.hs+1

src/Idris/AbsSyntaxTree.hs+7

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

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

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

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

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

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

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

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

@@ -1171,6 +1172,7 @@ data PDo' t = DoExp FC t

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

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

11731174 | DoLetP FC t t

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

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

11751177{-!

11761178deriving instance Binary PDo'

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

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

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

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

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

11851188

11861189type PDo = PDo' PTerm

11871190

@@ -1277,6 +1280,7 @@ highestFC (PDoBlock lines) =

12771280 getDoFC (DoBindP fc l r alts) = fc

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

12791282 getDoFC (DoLetP fc l r) = fc

1283+ getDoFC (DoRewrite fc h) = fc

12801284

12811285highestFC (PIdiom fc _) = Just fc

12821286highestFC (PMetavar fc _) = Just fc

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

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

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

19531957 ppdo bnd dos

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

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

1960+ ppdo bnd dos

19541961 ppdo _ [] = []

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

19561963 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+8−1

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

4848import System.FilePath

4949

5050ibcVersion :: Word16

51−ibcVersion = 160

51+ibcVersion = 161

5252

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

5454-- different structures/definitions) depending on which phase we're in.

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

22932293 put x1

22942294 put x2

22952295 put x3

2296+ DoRewrite x1 x2 -> do putWord8 5

2297+ put x1

2298+ put x2

22962299 get

22972300 = do i <- getWord8

22982301 case i of

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

23192322 x2 <- get

23202323 x3 <- get

23212324 return (DoLetP x1 x2 x3)

2325+ 5 -> do

2326+ x1 <- get

2327+ x2 <- get

2328+ return (DoRewrite x1 x2)

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

23232330

23242331

src/Idris/IdrisDoc.hs+1

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

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

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

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

347+extractPDo (DoRewrite _ p) = extract p

347348

348349-- | Helper function for extractPTermNames

349350extractPTactic :: PTactic -> [Name]

src/Idris/Parser/Expr.hs+7

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

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

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

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

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

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

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

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

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

13431344Do ::=

13441345 'let' Name TypeSig'? '=' Expr

13451346 | 'let' Expr' '=' Expr

1347+ | 'rewrite Expr

13461348 | Name '<-' Expr

13471349 | Expr' '<-' Expr

13481350 | Expr

@@ -1367,6 +1369,11 @@ do_ syn

13671369 sc <- expr syn

13681370 highlightP kw AnnKeyword

13691371 return (DoLetP fc i sc))

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

1373+ fc <- getFC

1374+ sc <- expr syn

1375+ highlightP kw AnnKeyword

1376+ return (DoRewrite fc sc))

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

13711378 symbol "<-"

13721379 fc <- getFC

src/Idris/Prover.hs+1

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

350350 Success (Right cmd') ->

351351 case cmd' of

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

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

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

354355 DoLet fc i ifc Placeholder expr ->

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