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

src/Idris/AbsSyntaxTree.hs+7

compare with master

unifiedsplit

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

1303 | DoLetP FC t t

1304 | DoLetP FC t t

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

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

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

1305{-!

1307{-!

1306deriving instance Binary PDo'

1308deriving instance Binary PDo'

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

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

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

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

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

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

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

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

1315

1318

1316type PDo = PDo' PTerm

1319type PDo = PDo' PTerm

1317

1320

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

1407 getDoFC (DoBindP fc l r alts) = fc

1410 getDoFC (DoBindP fc l r alts) = fc

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

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

1409 getDoFC (DoLetP fc l r) = fc

1412 getDoFC (DoLetP fc l r) = fc

1413+ getDoFC (DoRewrite fc h) = fc

1410

1414

1411highestFC (PIdiom fc _) = Just fc

1415highestFC (PIdiom fc _) = Just fc

1412highestFC (PMetavar fc _) = Just fc

1416highestFC (PMetavar fc _) = Just fc

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

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

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

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

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

2083 ppdo bnd dos

2087 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

2084 ppdo _ [] = []

2091 ppdo _ [] = []

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

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

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

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

src/Idris/DSL.hs+2

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

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

110 block b (DoLetP fc p tm : rest)

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

112+ block b (DoRewrite fc h : rest)

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

112 block b (DoExp fc tm : rest)

114 block b (DoExp fc tm : rest)

113 = PApp fc b

115 = PApp fc b

114 [pexp tm,

116 [pexp tm,

src/Idris/Elab/Quasiquote.hs+1

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

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

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

77extractDoUnquotes 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"

78

79

80

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

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

src/Idris/Error.hs+1

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

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

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

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

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

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

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

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

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

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

144warnDisamb 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

2292 put x1

2293 put x2

2294 put x3

2295+ DoRewrite x1 x2 -> do putWord8 3

2296+ put x1

2297+ put x2

2295 get

2298 get

2296 = do i <- getWord8

2299 = do i <- getWord8

2297 case i of

2300 case i of

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

2318 x2 <- get

2321 x2 <- get

2319 x3 <- get

2322 x3 <- get

2320 return (DoLetP x1 x2 x3)

2323 return (DoLetP x1 x2 x3)

2324+ 5 -> do

2325+ x1 <- get

2326+ x2 <- get

2327+ return (DoRewrite x1 x2)

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

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

2322

2329

2323

2330

src/Idris/IdrisDoc.hs+1

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

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

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

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

346+extractPDo (DoRewrite _ p) = extract p

346

347

347-- | Helper function for extractPTermNames

348-- | Helper function for extractPTermNames

348extractPTactic :: PTactic -> [Name]

349extractPTactic :: PTactic -> [Name]

src/Idris/Parser/Expr.hs+7

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

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

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

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

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

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

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

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

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

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

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

1342Do ::=

1343Do ::=

1343 'let' Name TypeSig'? '=' Expr

1344 'let' Name TypeSig'? '=' Expr

1344 | 'let' Expr' '=' Expr

1345 | 'let' Expr' '=' Expr

1346+ | 'rewrite Expr

1345 | Name '<-' Expr

1347 | Name '<-' Expr

1346 | Expr' '<-' Expr

1348 | Expr' '<-' Expr

1347 | Expr

1349 | Expr

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

1366 sc <- expr syn

1368 sc <- expr syn

1367 highlightP kw AnnKeyword

1369 highlightP kw AnnKeyword

1368 return (DoLetP fc i sc))

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

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

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

1370 symbol "<-"

1377 symbol "<-"

1371 fc <- getFC

1378 fc <- getFC

src/Idris/Prover.hs+1

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

349 Success (Right cmd') ->

350 case cmd' of

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

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

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

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

353 DoLet fc i ifc Placeholder expr ->

354 DoLet fc i ifc Placeholder expr ->

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

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