0655d3d · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Allow syntax rules at the declaration level

decl syntax [lhs] = decl1 decl2 ... The lhs has the same form as expression syntax rules, except that any names bounds in braces {n} are replaced in top level name bindings as well as explicit lambda/pi/let bindings. This is mostly intended to be used in conjection with top level %runElab declarations, but probably has wider use.

commit0655d3d96db96ef55968276761817e0e70a2875a authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSat 22 Aug 2015, 16:58 (11 years ago) parentb693b81

10 files changed+204−14

compare with master

unifiedsplit

CHANGELOG+1 idris.cabal+3 src/Idris/AbsSyntaxTree.hs+5 src/Idris/DeepSeq.hs+1 src/Idris/IBC.hs+17−6 src/Idris/ParseExpr.hs+12−6 src/Idris/Parser.hs+137−2 test/syntax002/expected+2 test/syntax002/run+4 test/syntax002/syntax002.idr+22

CHANGELOG+1

@@ -29,6 +29,7 @@ New in 0.9.19:

2929* Moved System.Interactive, along with getArgs to the Prelude.

3030* Major improvements to reflected elaboration scripts, including the ability to run

3131 them in a declaration context and many bug fixes.

32+* "decl syntax" rules to allow syntax extensions at the declaration level

3233

3334New in 0.9.18:

3435--------------

idris.cabal+3

@@ -659,6 +659,9 @@ Extra-source-files:

659659 test/syntax001/run

660660 test/syntax001/*.idr

661661 test/syntax001/expected

662+ test/syntax002/run

663+ test/syntax002/*.idr

664+ test/syntax002/expected

662665

663666 test/tactics001/run

664667 test/tactics001/*.idr

src/Idris/AbsSyntaxTree.hs+5

@@ -1246,15 +1246,20 @@ deriving instance NFData SynContext

12461246!-}

12471247

12481248data Syntax = Rule [SSymbol] PTerm SynContext

1249+ | DeclRule [SSymbol] [PDecl]

12491250 deriving Show

12501251

12511252syntaxNames :: Syntax -> [Name]

12521253syntaxNames (Rule syms _ _) = mapMaybe ename syms

12531254 where ename (Keyword n) = Just n

12541255 ename _ = Nothing

1256+syntaxNames (DeclRule syms _) = mapMaybe ename syms

1257+ where ename (Keyword n) = Just n

1258+ ename _ = Nothing

12551259

12561260syntaxSymbols :: Syntax -> [SSymbol]

12571261syntaxSymbols (Rule ss _ _) = ss

1262+syntaxSymbols (DeclRule ss _) = ss

12581263{-!

12591264deriving instance Binary Syntax

12601265deriving instance NFData Syntax

src/Idris/DeepSeq.hs+1

@@ -369,6 +369,7 @@ instance NFData SynContext where

369369

370370instance NFData Syntax where

371371 rnf (Rule x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

372+ rnf (DeclRule x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

372373

373374instance NFData SSymbol where

374375 rnf (Keyword x1) = rnf x1 `seq` ()

src/Idris/IBC.hs+17−6

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

4040import Codec.Archive.Zip

4141

4242ibcVersion :: Word16

43−ibcVersion = 117

43+ibcVersion = 118

4444

4545data IBCFile = IBCFile { ver :: Word16,

4646 sourcefile :: FilePath,

@@ -2174,14 +2174,25 @@ instance Binary SynContext where

21742174

21752175instance Binary Syntax where

21762176 put (Rule x1 x2 x3)

2177− = do put x1

2177+ = do putWord8 0

2178+ put x1

21782179 put x2

21792180 put x3

2181+ put (DeclRule x1 x2)

2182+ = do putWord8 1

2183+ put x1

2184+ put x2

21802185 get

2181− = do x1 <- get

2182− x2 <- get

2183− x3 <- get

2184− return (Rule x1 x2 x3)

2186+ = do i <- getWord8

2187+ case i of

2188+ 0 -> do x1 <- get

2189+ x2 <- get

2190+ x3 <- get

2191+ return (Rule x1 x2 x3)

2192+ 1 -> do x1 <- get

2193+ x2 <- get

2194+ return (DeclRule x1 x2)

2195+ _ -> error "Corrupted binary data for Syntax"

21852196

21862197instance (Binary t) => Binary (DSL' t) where

21872198 put (DSL x1 x2 x3 x4 x5 x6 x7 x8 x9 x10)

src/Idris/ParseExpr.hs+12−6

@@ -128,8 +128,10 @@ extensions syn rules = extension syn [] (filter isValid rules)

128128 isValid (Rule _ _ AnySyntax) = True

129129 isValid (Rule _ _ PatternSyntax) = inPattern syn

130130 isValid (Rule _ _ TermSyntax) = not (inPattern syn)

131+ isValid (DeclRule _ _) = False

131132

132133data SynMatch = SynTm PTerm | SynBind FC Name -- ^ the FC is for highlighting information

134+ deriving Show

133135

134136extension :: SyntaxInfo -> [Maybe (Name, SynMatch)] -> [Syntax] -> IdrisParser PTerm

135137extension syn ns rules =

@@ -140,7 +142,7 @@ extension syn ns rules =

140142 extension syn (n : ns) [Rule ss t ctx | (Rule (_:ss) t ctx) <- rs]

141143 -- If we have more than one Rule in this bucket, our grammar is

142144 -- nondeterministic.

143− Rule [] ptm _ -> return (flatten (update (mapMaybe id ns) ptm))

145+ Rule [] ptm _ -> return (flatten (updateSynMatch (mapMaybe id ns) ptm))

144146 where

145147 ruleGroup [] [] = True

146148 ruleGroup (s1:_) (s2:_) = s1 == s2

@@ -159,15 +161,13 @@ extension syn ns rules =

159161 extensionSymbol (Symbol s) = do fc <- symbolFC s

160162 highlightP fc AnnKeyword

161163 return Nothing

162− dropn :: Name -> [(Name, a)] -> [(Name, a)]

163− dropn n [] = []

164− dropn n ((x,t) : xs) | n == x = xs

165− | otherwise = (x,t):dropn n xs

166−

164+

167165 flatten :: PTerm -> PTerm -- flatten application

168166 flatten (PApp fc (PApp _ f as) bs) = flatten (PApp fc f (as ++ bs))

169167 flatten t = t

170168

169+updateSynMatch = update

170+ where

171171 updateB :: [(Name, SynMatch)] -> (Name, FC) -> (Name, FC)

172172 updateB ns (n, fc) = case lookup n ns of

173173 Just (SynBind tfc t) -> (t, tfc)

@@ -251,6 +251,12 @@ extension syn ns rules =

251251

252252 updTacImp ns (TacImp o st scr) = TacImp o st (update ns scr)

253253 updTacImp _ x = x

254+

255+ dropn :: Name -> [(Name, a)] -> [(Name, a)]

256+ dropn n [] = []

257+ dropn n ((x,t) : xs) | n == x = xs

258+ | otherwise = (x,t):dropn n xs

259+

254260

255261{- | Parses a (normal) built-in expression

256262@

src/Idris/Parser.hs+137−2

@@ -184,7 +184,13 @@ Decl ::=

184184@

185185-}

186186decl :: SyntaxInfo -> IdrisParser [PDecl]

187−decl syn = do fc <- getFC

187+decl syn = try (externalDecl syn)

188+ <|> internalDecl syn

189+ <?> "declaration"

190+

191+internalDecl :: SyntaxInfo -> IdrisParser [PDecl]

192+internalDecl syn

193+ = do fc <- getFC

188194 -- if we're after maxline, stop here

189195 let continue = case maxline syn of

190196 Nothing -> True

@@ -235,6 +241,124 @@ decl' syn = fixity

235241 <|> runElabDecl syn

236242 <?> "declaration"

237243

244+externalDecl :: SyntaxInfo -> IdrisParser [PDecl]

245+externalDecl syn = do i <- get

246+ notEndBlock

247+ FC fn start _ <- getFC

248+ decls <- declExtensions syn (syntaxRulesList $ syntax_rules i)

249+ FC _ _ end <- getFC

250+ let outerFC = FC fn start end

251+ return decls

252+

253+declExtensions :: SyntaxInfo -> [Syntax] -> IdrisParser [PDecl]

254+declExtensions syn rules = declExtension syn [] (filter isDeclRule rules)

255+ <?> "user-defined declaration"

256+ where

257+ isDeclRule (DeclRule _ _) = True

258+ isDeclRule _ = False

259+

260+declExtension :: SyntaxInfo -> [Maybe (Name, SynMatch)] -> [Syntax]

261+ -> IdrisParser [PDecl]

262+declExtension syn ns rules =

263+ choice $ flip map (groupBy (ruleGroup `on` syntaxSymbols) rules) $ \rs ->

264+ case head rs of -- can never be []

265+ DeclRule (symb:_) _ -> try $ do

266+ n <- extSymbol symb

267+ declExtension syn (n : ns) [DeclRule ss t | (DeclRule (_:ss) t) <- rs]

268+ -- If we have more than one Rule in this bucket, our grammar is

269+ -- nondeterministic.

270+ DeclRule [] dec -> let r = map (update (mapMaybe id ns)) dec in

271+ return r

272+

273+ where

274+ update :: [(Name, SynMatch)] -> PDecl -> PDecl

275+ update ns = updateNs ns . fmap (updateRefs ns) . fmap (updateSynMatch ns)

276+

277+ updateRefs ns = mapPT newref

278+ where

279+ newref (PRef fc fcs n) = PRef fc fcs (updateB ns n)

280+ newref t = t

281+

282+ -- Below is a lot of tedious boilerplate which updates any top level

283+ -- names in the declaration. It will only change names which are bound in

284+ -- the declaration (including method names in classes and field names in

285+ -- record declarations, not including pattern variables)

286+ updateB :: [(Name, SynMatch)] -> Name -> Name

287+ updateB ns (NS n mods) = NS (updateB ns n) mods

288+ updateB ns n = case lookup n ns of

289+ Just (SynBind tfc t) -> t

290+ _ -> n

291+

292+ updateNs :: [(Name, SynMatch)] -> PDecl -> PDecl

293+ updateNs ns (PTy doc argdoc s fc o n fc' t)

294+ = PTy doc argdoc s fc o (updateB ns n) fc' t

295+ updateNs ns (PClauses fc o n cs)

296+ = PClauses fc o (updateB ns n) (map (updateClause ns) cs)

297+ updateNs ns (PCAF fc n t) = PCAF fc (updateB ns n) t

298+ updateNs ns (PData ds cds s fc o dat)

299+ = PData ds cds s fc o (updateData ns dat)

300+ updateNs ns (PParams fc ps ds) = PParams fc ps (map (updateNs ns) ds)

301+ updateNs ns (PNamespace s fc ds) = PNamespace s fc (map (updateNs ns) ds)

302+ updateNs ns (PRecord doc syn fc o n fc' ps pdocs fields cname cdoc s)

303+ = PRecord doc syn fc o (updateB ns n) fc' ps pdocs

304+ (map (updateField ns) fields)

305+ (updateRecCon ns cname)

306+ cdoc

307+ s

308+ updateNs ns (PClass docs s fc cs cn fc' ps pdocs pdets ds cname cdocs)

309+ = PClass docs s fc cs (updateB ns cn) fc' ps pdocs pdets

310+ (map (updateNs ns) ds)

311+ (updateRecCon ns cname)

312+ cdocs

313+ updateNs ns (PInstance docs pdocs s fc cs cn fc' ps ity ni ds)

314+ = PInstance docs pdocs s fc cs (updateB ns cn) fc'

315+ ps ity (fmap (updateB ns) ni)

316+ (map (updateNs ns) ds)

317+ updateNs ns (PMutual fc ds) = PMutual fc (map (updateNs ns) ds)

318+ updateNs ns (PProvider docs s fc fc' pw n)

319+ = PProvider docs s fc fc' pw (updateB ns n)

320+ updateNs ns d = d

321+

322+ updateRecCon ns Nothing = Nothing

323+ updateRecCon ns (Just (n, fc)) = Just (updateB ns n, fc)

324+

325+ updateField ns (m, p, t, doc) = (updateRecCon ns m, p, t, doc)

326+

327+ updateClause ns (PClause fc n t ts t' ds)

328+ = PClause fc (updateB ns n) t ts t' (map (update ns) ds)

329+ updateClause ns (PWith fc n t ts t' m ds)

330+ = PWith fc (updateB ns n) t ts t' m (map (update ns) ds)

331+ updateClause ns (PClauseR fc ts t ds)

332+ = PClauseR fc ts t (map (update ns) ds)

333+ updateClause ns (PWithR fc ts t m ds)

334+ = PWithR fc ts t m (map (update ns) ds)

335+

336+ updateData ns (PDatadecl n fc t cs)

337+ = PDatadecl (updateB ns n) fc t (map (updateCon ns) cs)

338+ updateData ns (PLaterdecl n fc t)

339+ = PLaterdecl (updateB ns n) fc t

340+

341+ updateCon ns (cd, ads, cn, fc, ty, fc', fns)

342+ = (cd, ads, updateB ns cn, fc, ty, fc', fns)

343+

344+ ruleGroup [] [] = True

345+ ruleGroup (s1:_) (s2:_) = s1 == s2

346+ ruleGroup _ _ = False

347+

348+ extSymbol :: SSymbol -> IdrisParser (Maybe (Name, SynMatch))

349+ extSymbol (Keyword n) = do fc <- reservedFC (show n)

350+ highlightP fc AnnKeyword

351+ return Nothing

352+ extSymbol (Expr n) = do tm <- expr syn

353+ return $ Just (n, SynTm tm)

354+ extSymbol (SimpleExpr n) = do tm <- simpleExpr syn

355+ return $ Just (n, SynTm tm)

356+ extSymbol (Binding n) = do (b, fc) <- name

357+ return $ Just (n, SynBind fc b)

358+ extSymbol (Symbol s) = do fc <- symbolFC s

359+ highlightP fc AnnKeyword

360+ return Nothing

361+

238362{- | Parses a syntax extension declaration (and adds the rule to parser state)

239363

240364@

@@ -303,6 +427,17 @@ syntaxRule syn

303427 tm <- typeExpr (allowImp syn) >>= uniquifyBinders [n | Binding n <- syms]

304428 terminator

305429 return (Rule (mkSimple syms) tm sty)

430+ <|> do reservedHL "decl"; reservedHL "syntax"

431+ syms <- some syntaxSym

432+ when (all isExpr syms) $ unexpected "missing keywords in syntax rule"

433+ let ns = mapMaybe getName syms

434+ when (length ns /= length (nub ns))

435+ $ unexpected "repeated variable in syntax rule"

436+ lchar '='

437+ openBlock

438+ dec <- some (decl syn)

439+ closeBlock

440+ return (DeclRule (mkSimple syms) (concat dec))

306441 where

307442 isExpr (Expr _) = True

308443 isExpr _ = False

@@ -317,7 +452,7 @@ syntaxRule syn

317452 mkSimple es

318453 -- Can't parse a full expression followed by operator like characters due to ambiguity

319454 mkSimple' (Expr e : Symbol s : es)

320− | takeWhile (`elem` opChars) ts /= "" && ts `notElem` invalidOperators = SimpleExpr e : Symbol s : mkSimple' es

455+ | takeWhile (`elem` opChars) ts /= "" = SimpleExpr e : Symbol s : mkSimple' es

321456 where ts = dropWhile isSpace . dropWhileEnd isSpace $ s

322457 mkSimple' (e : es) = e : mkSimple' es

323458 mkSimple' [] = []

test/syntax002/expectednew file+2

@@ -0,0 +1,2 @@

1+Nothing

2+7

test/syntax002/runnew file+4

@@ -0,0 +1,4 @@

1+#!/usr/bin/env bash

2+idris $@ syntax002.idr -o syntax002

3+./syntax002

4+rm -f syntax002 *.ibc

test/syntax002/syntax002.idrnew file+22

@@ -0,0 +1,22 @@

2+decl syntax fun {n} ":" [ty] "=" [def]

3+ = n : ty

4+ n = def

6+decl syntax newtype {tname} "=" {conname} [tysyn]

7+ = data tname = conname tysyn

9+decl syntax EmptyShow {n} =

10+ instance Show n where

11+ show x = "Nothing"

12+

13+fun add : (Int -> Int -> Int) = \x, y => x + y

14+

15+newtype Foo = MkFoo Int

16+

17+EmptyShow Foo

18+

19+main : IO ()

20+main = do printLn (MkFoo 42)

21+ printLn (add 3 4)

22+