c90d4b4 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Parsing for quasiquotes

commitc90d4b4165b57316bd01fa44f602c3bf8c182663 authorDavid Raymond Christiansen <david@davidchristiansen.dk> dateMon 23 Jun 2014, 16:11 (12 years ago) parent18c33c5

4 files changed+43−8

compare with master

unifiedsplit

src/Idris/AbsSyntaxTree.hs+8−3 src/Idris/DeepSeq.hs+4−3 src/Idris/IBC.hs+2−2 src/Idris/ParseExpr.hs+29

src/Idris/AbsSyntaxTree.hs+8−3

@@ -704,6 +704,8 @@ data PTerm = PQuote Raw

704704 | PDisamb [[T.Text]] PTerm -- ^ Preferences for explicit namespaces

705705 | PUnifyLog PTerm -- ^ dump a trace of unifications when building term

706706 | PNoImplicits PTerm -- ^ never run implicit converions on the term

707+ | PQuasiquote PTerm -- ^ `(Term)

708+ | PUnquote PTerm -- ^ ,Term

707709 deriving Eq

708710

709711

@@ -971,14 +973,15 @@ data SyntaxInfo = Syn { using :: [Using],

971973 implicitAllowed :: Bool,

972974 maxline :: Maybe Int,

973975 mut_nesting :: Int,

974− dsl_info :: DSL }

976+ dsl_info :: DSL,

977+ syn_in_quasiquote :: Bool }

975978 deriving Show

976979{-!

977980deriving instance NFData SyntaxInfo

978981deriving instance Binary SyntaxInfo

979982!-}

980983

981−defaultSyntax = Syn [] [] [] [] id False False Nothing 0 initDSL

984+defaultSyntax = Syn [] [] [] [] id False False Nothing 0 initDSL False

982985

983986expandNS :: SyntaxInfo -> Name -> Name

984987expandNS syn n@(NS _ _) = n

@@ -1353,8 +1356,10 @@ pprintPTerm ppo bnd docArgs infixes = prettySe 10 bnd

13531356 prettySe p bnd (PDoBlock _) = text "do block pretty not implemented"

13541357 prettySe p bnd (PCoerced t) = prettySe p bnd t

13551358 prettySe p bnd (PElabError s) = pretty s

1359+ prettySe p bnd (PQuasiquote t) = text "`(" <> prettySe p bnd t <> text ")"

1360+ prettySe p bnd (PUnquote t) = text "~" <> prettySe p bnd t

13561361

1357− prettySe p bnd _ = text "test"

1362+ prettySe p bnd _ = text "missing pretty-printer for term"

13581363

13591364 prettyArgS bnd (PImp _ _ _ n tm) = prettyArgSi bnd (n, tm)

13601365 prettyArgS bnd (PExp _ _ _ tm) = prettyArgSe bnd tm

src/Idris/DeepSeq.hs+4−3

@@ -320,13 +320,14 @@ instance NFData Using where

320320 rnf (UImplicit x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

321321 rnf (UConstraint x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

322322

323−

324323instance NFData SyntaxInfo where

325− rnf (Syn x1 x2 x3 x4 x5 x6 x7 x8 x9 x10)

324+ rnf (Syn x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11)

326325 = rnf x1 `seq`

327326 rnf x2 `seq`

328327 rnf x3 `seq`

329− rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` rnf x9 `seq` rnf x10 `seq` ()

328+ rnf x4 `seq`

329+ rnf x5 `seq`

330+ rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` rnf x9 `seq` rnf x10 `seq` rnf x11 `seq` ()

330331

331332

332333

src/Idris/IBC.hs+2−2

@@ -1239,7 +1239,7 @@ instance Binary Using where

12391239 1 -> do x1 <- get; x2 <- get; return (UConstraint x1 x2)

12401240

12411241instance Binary SyntaxInfo where

1242− put (Syn x1 x2 x3 x4 _ x5 x6 _ _ x7)

1242+ put (Syn x1 x2 x3 x4 _ x5 x6 _ _ x7 _)

12431243 = do put x1

12441244 put x2

12451245 put x3

@@ -1255,7 +1255,7 @@ instance Binary SyntaxInfo where

12551255 x5 <- get

12561256 x6 <- get

12571257 x7 <- get

1258− return (Syn x1 x2 x3 x4 id x5 x6 Nothing 0 x7)

1258+ return (Syn x1 x2 x3 x4 id x5 x6 Nothing 0 x7 False)

12591259

12601260instance (Binary t) => Binary (PClause' t) where

12611261 put x

src/Idris/ParseExpr.hs+29

@@ -289,6 +289,8 @@ SimpleExpr ::=

289289 | Constant

290290 | Type

291291 | '_|_'

292+ | Quasiquote

293+ | Unquote

292294 | '_'

293295 ;

294296@

@@ -326,6 +328,8 @@ simpleExpr syn =

326328 <|> do symbol "_|_"

327329 fc <- getFC

328330 return (PFalse fc)

331+ <|> quasiquote syn

332+ <|> unquote syn

329333 <|> do lchar '_'; return Placeholder

330334 <?> "expression"

331335

@@ -587,6 +591,31 @@ constraintArg syn = do symbol "@{"

587591 return (pconst e)

588592 <?> "constraint argument"

589593

594+{-| Parses a quasiquote expression (for building reflected terms using the elaborator)

595+

596+> Quasiquote ::= '`(' Expr ')'

597+

598+-}

599+quasiquote :: SyntaxInfo -> IdrisParser PTerm

600+quasiquote syn = do guard (not (syn_in_quasiquote syn))

601+ symbol "`("

602+ e <- expr syn { syn_in_quasiquote = True }

603+ symbol ")"

604+ return $ PQuasiquote e

605+ <?> "quasiquotation"

606+

607+{-| Parses an unquoting inside a quasiquotation (for building reflected terms using the elaborator)

608+

609+> Unquote ::= ',' Expr

610+

611+-}

612+unquote :: SyntaxInfo -> IdrisParser PTerm

613+unquote syn = do guard (syn_in_quasiquote syn)

614+ symbol "~"

615+ e <- simpleExpr syn { syn_in_quasiquote = False }

616+ return $ PUnquote e

617+ <?> "unquotation"

618+

590619

591620{-| Parses a record field setter expression

592621@