aa0b315 · Idris-dev · git.iko.soy

src/Idris/AbsSyntaxTree.hs+7

compare with master

unifiedsplit

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

1173 | DoLetP FC t t

1174 | DoLetP FC t t

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

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

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

1175{-!

1177{-!

1176deriving instance Binary PDo'

1178deriving instance Binary PDo'

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

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

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

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

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

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

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

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

1185

1188

1186type PDo = PDo' PTerm

1189type PDo = PDo' PTerm

1187

1190

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

1277 getDoFC (DoBindP fc l r alts) = fc

1280 getDoFC (DoBindP fc l r alts) = fc

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

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

1279 getDoFC (DoLetP fc l r) = fc

1282 getDoFC (DoLetP fc l r) = fc

1283+ getDoFC (DoRewrite fc h) = fc

1280

1284

1281highestFC (PIdiom fc _) = Just fc

1285highestFC (PIdiom fc _) = Just fc

1282highestFC (PMetavar fc _) = Just fc

1286highestFC (PMetavar fc _) = Just fc

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

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

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

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

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

1953 ppdo bnd dos

1957 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

1954 ppdo _ [] = []

1961 ppdo _ [] = []

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

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

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

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

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

48import System.FilePath

49

50ibcVersion :: Word16

51−ibcVersion = 160

51+ibcVersion = 161

52

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

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

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

2293 put x1

2294 put x2

2295 put x3

2296+ DoRewrite x1 x2 -> do putWord8 5

2297+ put x1

2298+ put x2

2296 get

2299 get

2297 = do i <- getWord8

2300 = do i <- getWord8

2298 case i of

2301 case i of

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

2319 x2 <- get

2322 x2 <- get

2320 x3 <- get

2323 x3 <- get

2321 return (DoLetP x1 x2 x3)

2324 return (DoLetP x1 x2 x3)

2325+ 5 -> do

2326+ x1 <- get

2327+ x2 <- get

2328+ return (DoRewrite x1 x2)

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

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

2323

2330

2324

2331

src/Idris/IdrisDoc.hs+1

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

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

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

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

347+extractPDo (DoRewrite _ p) = extract p

347

348

348-- | Helper function for extractPTermNames

349-- | Helper function for extractPTermNames

349extractPTactic :: PTactic -> [Name]

350extractPTactic :: PTactic -> [Name]

src/Idris/Parser/Expr.hs+7

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

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

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

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

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

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

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

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

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

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

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

1343Do ::=

1344Do ::=

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

1345 'let' Name TypeSig'? '=' Expr

1345 | 'let' Expr' '=' Expr

1346 | 'let' Expr' '=' Expr

1347+ | 'rewrite Expr

1346 | Name '<-' Expr

1348 | Name '<-' Expr

1347 | Expr' '<-' Expr

1349 | Expr' '<-' Expr

1348 | Expr

1350 | Expr

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

1367 sc <- expr syn

1369 sc <- expr syn

1368 highlightP kw AnnKeyword

1370 highlightP kw AnnKeyword

1369 return (DoLetP fc i sc))

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

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

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

1371 symbol "<-"

1378 symbol "<-"

1372 fc <- getFC

1379 fc <- getFC

src/Idris/Prover.hs+1

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

350 Success (Right cmd') ->

351 case cmd' of

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

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

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

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

354 DoLet fc i ifc Placeholder expr ->

355 DoLet fc i ifc Placeholder expr ->

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

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