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

git.iko.soy/Idris-dev

on master help sign in

Allow syntax rules at the declaration level

0655d3dEdwin Brady11 years ago

CHANGELOG+1

compare with master

unifiedsplit

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

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

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

31 them in a declaration context and many bug fixes.

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

33New in 0.9.18:

34New in 0.9.18:

34--------------

35--------------

idris.cabal+3

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

659 test/syntax001/run

660 test/syntax001/*.idr

661 test/syntax001/expected

662+ test/syntax002/run

663+ test/syntax002/*.idr

664+ test/syntax002/expected

662

665

663 test/tactics001/run

666 test/tactics001/run

664 test/tactics001/*.idr

667 test/tactics001/*.idr

src/Idris/AbsSyntaxTree.hs+5

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

1246!-}

1247

1248data Syntax = Rule [SSymbol] PTerm SynContext

1249+ | DeclRule [SSymbol] [PDecl]

1249 deriving Show

1250 deriving Show

1250

1251

1251syntaxNames :: Syntax -> [Name]

1252syntaxNames :: Syntax -> [Name]

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

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

1253 where ename (Keyword n) = Just n

1254 where ename (Keyword n) = Just n

1254 ename _ = Nothing

1255 ename _ = Nothing

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

1257+ where ename (Keyword n) = Just n

1258+ ename _ = Nothing

1255

1259

1256syntaxSymbols :: Syntax -> [SSymbol]

1260syntaxSymbols :: Syntax -> [SSymbol]

1257syntaxSymbols (Rule ss _ _) = ss

1261syntaxSymbols (Rule ss _ _) = ss

1262+syntaxSymbols (DeclRule ss _) = ss

1258{-!

1263{-!

1259deriving instance Binary Syntax

1264deriving instance Binary Syntax

1260deriving instance NFData Syntax

1265deriving instance NFData Syntax

src/Idris/DeepSeq.hs+1

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

369

370instance NFData Syntax where

371 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` ()

372

373

373instance NFData SSymbol where

374instance NFData SSymbol where

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

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

src/Idris/IBC.hs+17−6

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

40import Codec.Archive.Zip

42ibcVersion :: Word16

43−ibcVersion = 117

43+ibcVersion = 118

45data IBCFile = IBCFile { ver :: Word16,

46 sourcefile :: FilePath,

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

2174

2175instance Binary Syntax where

2176 put (Rule x1 x2 x3)

2177+ = do putWord8 0

2177− = do put x1

2178+ put x1

2178 put x2

2179 put x2

2179 put x3

2180 put x3

2181+ put (DeclRule x1 x2)

2182+ = do putWord8 1

2183+ put x1

2184+ put x2

2180 get

2185 get

2186+ = do i <- getWord8

2187+ case i of

2181− = do x1 <- get

2188+ 0 -> do x1 <- get

2182− x2 <- get

2189+ x2 <- get

2183− x3 <- get

2190+ x3 <- get

2184− return (Rule x1 x2 x3)

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"

2185

2196

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

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

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

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

128 isValid (Rule _ _ AnySyntax) = True

129 isValid (Rule _ _ PatternSyntax) = inPattern syn

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

131+ isValid (DeclRule _ _) = False

131

132

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

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

134+ deriving Show

133

135

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

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

135extension syn ns rules =

137extension syn ns rules =

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

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

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

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

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

142 -- nondeterministic.

144 -- nondeterministic.

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

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

144 where

146 where

145 ruleGroup [] [] = True

147 ruleGroup [] [] = True

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

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

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

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

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

160 highlightP fc AnnKeyword

162 highlightP fc AnnKeyword

161 return Nothing

163 return Nothing

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

164+

163− dropn n [] = []

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

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

166−

167 flatten :: PTerm -> PTerm -- flatten application

165 flatten :: PTerm -> PTerm -- flatten application

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

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

169 flatten t = t

167 flatten t = t

170

168

169+updateSynMatch = update

170+ where

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

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

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

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

251

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

253 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+

254

260

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

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

256@

262@

src/Idris/Parser.hs+137−2

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

184@

185-}

186decl :: SyntaxInfo -> IdrisParser [PDecl]

187+decl syn = try (externalDecl syn)

188+ <|> internalDecl syn

189+ <?> "declaration"

190+

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

192+internalDecl syn

187−decl syn = do fc <- getFC

193+ = do fc <- getFC

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

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

189 let continue = case maxline syn of

195 let continue = case maxline syn of

190 Nothing -> True

196 Nothing -> True

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

235 <|> runElabDecl syn

241 <|> runElabDecl syn

236 <?> "declaration"

242 <?> "declaration"

237

243

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+

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

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

239

363

240@

364@

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

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

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

304 terminator

428 terminator

305 return (Rule (mkSimple syms) tm sty)

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

306 where

441 where

307 isExpr (Expr _) = True

442 isExpr (Expr _) = True

308 isExpr _ = False

443 isExpr _ = False

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

317 mkSimple es

452 mkSimple es

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

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

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

454 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

321 where ts = dropWhile isSpace . dropWhileEnd isSpace $ s

456 where ts = dropWhile isSpace . dropWhileEnd isSpace $ s

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

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

323 mkSimple' [] = []

458 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+