c90d4b4 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Parsing for quasiquotes

c90d4b4David Raymond Christiansen12 years ago

src/Idris/AbsSyntaxTree.hs+8−3

compare with master

unifiedsplit

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

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

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

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

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

708+ | PUnquote PTerm -- ^ ,Term

707 deriving Eq

709 deriving Eq

708

710

709

711

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

971 implicitAllowed :: Bool,

973 implicitAllowed :: Bool,

972 maxline :: Maybe Int,

974 maxline :: Maybe Int,

973 mut_nesting :: Int,

975 mut_nesting :: Int,

974− dsl_info :: DSL }

976+ dsl_info :: DSL,

977+ syn_in_quasiquote :: Bool }

975 deriving Show

978 deriving Show

976{-!

979{-!

977deriving instance NFData SyntaxInfo

980deriving instance NFData SyntaxInfo

978deriving instance Binary SyntaxInfo

981deriving instance Binary SyntaxInfo

979!-}

982!-}

980

983

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

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

982

985

983expandNS :: SyntaxInfo -> Name -> Name

986expandNS :: SyntaxInfo -> Name -> Name

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

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

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

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

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

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

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

1355 prettySe p bnd (PElabError s) = pretty s

1358 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

1356

1361

1357− prettySe p bnd _ = text "test"

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

1358

1363

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

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

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

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

src/Idris/DeepSeq.hs+4−3

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

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

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

322

323−

324instance NFData SyntaxInfo where

323instance 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)

326 = rnf x1 `seq`

325 = rnf x1 `seq`

327 rnf x2 `seq`

326 rnf x2 `seq`

328 rnf x3 `seq`

327 rnf x3 `seq`

328+ rnf x4 `seq`

329+ rnf x5 `seq`

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

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

330

331

332

333

src/Idris/IBC.hs+2−2

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

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

1240

1241instance Binary SyntaxInfo where

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

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

1243 = do put x1

1244 put x2

1245 put x3

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

1255 x5 <- get

1256 x6 <- get

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

1259

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

1261 put x

src/Idris/ParseExpr.hs+29

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

289 | Constant

290 | Type

291 | '_|_'

292+ | Quasiquote

293+ | Unquote

292 | '_'

294 | '_'

293 ;

295 ;

294@

296@

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

326 <|> do symbol "_|_"

328 <|> do symbol "_|_"

327 fc <- getFC

329 fc <- getFC

328 return (PFalse fc)

330 return (PFalse fc)

331+ <|> quasiquote syn

332+ <|> unquote syn

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

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

330 <?> "expression"

334 <?> "expression"

331

335

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

587 return (pconst e)

591 return (pconst e)

588 <?> "constraint argument"

592 <?> "constraint argument"

589

593

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+

590

619

591{-| Parses a record field setter expression

620{-| Parses a record field setter expression

592@

621@