From 25f764daadbef2228dd375917506ce5a772a19ea Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Tue, 18 Feb 2020 17:41:30 +0100 Subject: [PATCH] feat: antiquotation escapes --- src/Init/Lean/Elab/Quotation.lean | 61 ++++++++++++++++++------------- src/Init/Lean/Elab/Syntax.lean | 6 +-- src/Init/Lean/Parser/Parser.lean | 10 ++++- src/Init/LeanInit.lean | 4 -- tests/lean/run/bigop.lean | 6 +-- 5 files changed, 48 insertions(+), 39 deletions(-) diff --git a/src/Init/Lean/Elab/Quotation.lean b/src/Init/Lean/Elab/Quotation.lean index 7a2baf8c4f..926d47e8a2 100644 --- a/src/Init/Lean/Elab/Quotation.lean +++ b/src/Init/Lean/Elab/Quotation.lean @@ -69,24 +69,33 @@ def isAntiquot : Syntax → Bool | Syntax.node (Name.str _ "antiquot" _) _ => true | _ => false +-- Antiquotations can be escaped as in `$$x`, which is useful for nesting macros. +def isEscapedAntiquot (stx : Syntax) : Bool := +!(stx.getArg 1).getArgs.isEmpty + +def unescapeAntiquot (stx : Syntax) : Syntax := +if isAntiquot stx then + stx.setArg 1 $ mkNullNode (stx.getArg 1).getArgs.pop +else stx + +def getAntiquotTerm (stx : Syntax) : Syntax := +stx.getArg 2 + def antiquotKind? : Syntax → Option SyntaxNodeKind | Syntax.node (Name.str k "antiquot" _) args => -- we treat all antiquotations where the kind was left implicit (`$e`) the same (see `elimAntiquotChoices`) - if (args.get! 2).isNone then some Name.anonymous + if (args.get! 3).isNone then some Name.anonymous else some k | _ => none -def getAntiquotTerm (stx : Syntax) : Syntax := -stx.getArg 1 - -- `$e*` is an antiquotation "splice" matching an arbitrary number of syntax nodes def isAntiquotSplice (stx : Syntax) : Bool := -isAntiquot stx && (stx.getArg 4).getOptional?.isSome +isAntiquot stx && (stx.getArg 5).getOptional?.isSome -- If any item of a `many` node is an antiquotation splice, its result should -- be substituted into the `many` node's children def isAntiquotSplicePat (stx : Syntax) : Bool := -stx.isOfKind nullKind && stx.getArgs.any isAntiquotSplice +stx.isOfKind nullKind && stx.getArgs.any (fun arg => isAntiquotSplice arg && !isEscapedAntiquot arg) /-- A term like `($e) is actually ambiguous: the antiquotation could be of kind `term`, or `ident`, or ... . But it shouldn't really matter because antiquotations without @@ -110,14 +119,16 @@ private partial def quoteSyntax : Syntax → TermElabM Syntax -- `scp` is bound in stxQuot.expand `(Syntax.ident none $(quote rawVal) (addMacroScope mainModule $val scp) $(quote preresolved)) -- if antiquotation, insert contents as-is, else recurse -| stx@(Syntax.node k args) => - if isAntiquot stx then +| stx@(Syntax.node k _) => + if isAntiquot stx && !isEscapedAntiquot stx then -- splices must occur in a `many` node if isAntiquotSplice stx then throwError stx "unexpected antiquotation splice" else pure $ getAntiquotTerm stx else do empty ← `(Array.empty); - args ← args.foldlM (fun args arg => + -- if escaped antiquotation, decrement by one escape level + let stx := unescapeAntiquot stx; + args ← stx.getArgs.foldlM (fun args arg => if k == nullKind && isAntiquotSplice arg then -- antiquotation splice pattern: inject args array `(Array.append $args $(getAntiquotTerm arg)) @@ -201,9 +212,9 @@ else if pat.isOfKind `Lean.Parser.Term.stxQuot then if quoted.isAtom then -- We assume that atoms are uniquely determined by the node kind and never have to be checked unconditional pure - else match antiquotKind? quoted with - -- quotation is a single antiquotation - | some k => + else if isAntiquot quoted && !isEscapedAntiquot quoted then + -- quotation contains a single antiquotation + let k := antiquotKind? quoted; -- Antiquotation kinds like `$id:id` influence the parser, but also need to be considered by -- match_syntax (but not by quotation terms). For example, `($id:id) and `($e) are not -- distinguishable without checking the kind of the node to be captured. Note that some @@ -214,7 +225,7 @@ else if pat.isOfKind `Lean.Parser.Term.stxQuot then -- let id := stx; ... -- else -- let e := stx; ... - let kind := if k == Name.anonymous then none else some k; + let kind := if k == Name.anonymous then none else k; let anti := match_syntax getAntiquotTerm quoted with | `(($e)) => e | anti => anti; @@ -222,16 +233,16 @@ else if pat.isOfKind `Lean.Parser.Term.stxQuot then if isAntiquotSplice quoted then unconditional $ fun _ => throwError quoted "unexpected antiquotation splice" else if anti.isOfKind `Lean.Parser.Term.id then { kind := kind, rhsFn := fun rhs => `(let $anti := discr; $rhs) } else unconditional $ fun _ => throwError anti ("match_syntax: antiquotation must be variable " ++ toString anti) - | _ => - if isAntiquotSplicePat quoted && quoted.getArgs.size == 1 then - -- quotation is a single antiquotation splice => bind args array - let anti := getAntiquotTerm (quoted.getArg 0); - unconditional $ fun rhs => `(let $anti := Syntax.getArgs discr; $rhs) - -- TODO: support for more complex antiquotation splices - else - -- not an antiquotation: match head shape - let argPats := quoted.getArgs.map $ fun arg => Syntax.node `Lean.Parser.Term.stxQuot #[mkAtom "`(", arg, mkAtom ")"]; - { kind := quoted.getKind, argPats := argPats } + else if isAntiquotSplicePat quoted && quoted.getArgs.size == 1 then + -- quotation is a single antiquotation splice => bind args array + let anti := getAntiquotTerm (quoted.getArg 0); + unconditional $ fun rhs => `(let $anti := Syntax.getArgs discr; $rhs) + -- TODO: support for more complex antiquotation splices + else + -- not an antiquotation or escaped antiquotation: match head shape + let quoted := unescapeAntiquot quoted; + let argPats := quoted.getArgs.map $ fun arg => Syntax.node `Lean.Parser.Term.stxQuot #[mkAtom "`(", arg, mkAtom ")"]; + { kind := quoted.getKind, argPats := argPats } else unconditional $ fun _ => throwError pat ("match_syntax: unexpected pattern kind " ++ toString pat) @@ -279,8 +290,8 @@ private partial def compileStxMatch (ref : Syntax) : List Syntax → List Alt private partial def getPatternVarsAux : Syntax → List Syntax | stx@(Syntax.node k args) => - if isAntiquot stx then - let anti := args.get! 1; + if isAntiquot stx && !isEscapedAntiquot stx then + let anti := getAntiquotTerm stx; let anti := match_syntax anti with | `(($e)) => e | _ => anti; diff --git a/src/Init/Lean/Elab/Syntax.lean b/src/Init/Lean/Elab/Syntax.lean index fca3382b3c..c27f826301 100644 --- a/src/Init/Lean/Elab/Syntax.lean +++ b/src/Init/Lean/Elab/Syntax.lean @@ -259,7 +259,7 @@ private partial def antiquote (vars : Array Syntax) : Syntax → Syntax | stx => match_syntax stx with | `($id:ident) => if (vars.findIdx? (fun var => var.getId == id.getId)).isSome then - Syntax.node `antiquot #[mkAtom "$", Unhygienic.run `($id:ident), mkNullNode, mkNullNode] + Syntax.node `antiquot #[mkAtom "$", mkNullNode, Unhygienic.run `($id:ident), mkNullNode, mkNullNode] else stx | _ => match stx with @@ -290,7 +290,7 @@ def expandNotationItemIntoPattern (stx : Syntax) : MacroM Syntax := let k := stx.getKind; if k == `Lean.Parser.Command.identPrec then let item := stx.getArg 0; - pure $ mkNode `antiquot #[mkAtom "$", mkTermIdFromIdent item, mkNullNode, mkNullNode] + pure $ mkNode `antiquot #[mkAtom "$", mkNullNode, mkTermIdFromIdent item, mkNullNode, mkNullNode] else if k == `Lean.Parser.Command.quotedSymbolPrec then pure $ (stx.getArg 0).getArg 1 else if k == `Lean.Parser.Command.strLitPrec then @@ -346,7 +346,7 @@ def expandMacroArgIntoPattern (stx : Syntax) : MacroM Syntax := let k := stx.getKind; if k == `Lean.Parser.Command.macroArgSimple then let item := stx.getArg 0; - pure $ mkNode `antiquot #[mkAtom "$", mkTermIdFromIdent item, mkNullNode, mkNullNode] + pure $ mkNode `antiquot #[mkAtom "$", mkNullNode, mkTermIdFromIdent item, mkNullNode, mkNullNode] else if k == `Lean.Parser.Command.strLitPrec then strLitPrecToPattern stx else diff --git a/src/Init/Lean/Parser/Parser.lean b/src/Init/Lean/Parser/Parser.lean index 2ac5464b61..238239345f 100644 --- a/src/Init/Lean/Parser/Parser.lean +++ b/src/Init/Lean/Parser/Parser.lean @@ -1432,7 +1432,8 @@ private def antiquotExpr : Parser := antiquotId <|> antiquotNestedExpr Define parser for `$e` (if anonymous == true) and `$e:name`. Both forms can also be used with an appended `*` to turn them into an antiquotation "splice". If `kind` is given, it will additionally be checked - when evaluating `match_syntax`. -/ + when evaluating `match_syntax`. Antiquotations can be escaped as in `$$e`, which + produces the syntax tree for `$e`. -/ def mkAntiquot (name : String) (kind : Option SyntaxNodeKind) (anonymous := true) : Parser := let kind := (kind.getD Name.anonymous) ++ `antiquot; let nameP := checkNoWsBefore ("no space before ':" ++ name ++ "'") >> symbolAux ":" >> nonReservedSymbol name; @@ -1440,7 +1441,12 @@ let nameP := checkNoWsBefore ("no space before ':" ++ name ++ "'") >> symbolAux -- antiquotation kind via `noImmediateColon` let nameP := if anonymous then nameP <|> noImmediateColon >> pushNone >> pushNone else nameP; -- antiquotations are not part of the "standard" syntax, so hide "expected '$'" on error -node kind $ try $ setExpected [] dollarSymbol >> checkNoWsBefore "no space before" >> antiquotExpr >> nameP >> optional (checkNoWsBefore "" >> "*") +node kind $ try $ + setExpected [] dollarSymbol >> + many (checkNoWsBefore "" >> dollarSymbol) >> + checkNoWsBefore "no space before spliced term" >> antiquotExpr >> + nameP >> + optional (checkNoWsBefore "" >> "*") def tryAnti (c : ParserContext) (s : ParserState) : Bool := let (s, stx?) := peekToken c s; diff --git a/src/Init/LeanInit.lean b/src/Init/LeanInit.lean index 6e03a2aab0..f0a6866ef2 100644 --- a/src/Init/LeanInit.lean +++ b/src/Init/LeanInit.lean @@ -697,10 +697,6 @@ match stx.isStrLit? with | none => stx | some val => Syntax.atom stx.getHeadInfo val -/-- Given `var` a `Term.id`, created the antiquotation syntax representing `$:` -/ -def termIdToAntiquot (var : Syntax) (catName : String) : Syntax := -Syntax.node `Lean.Parser.antiquot #[mkAtomFrom var "$", var, mkAtomFrom var ":", mkAtomFrom var catName, mkNullNode] - def isAtom : Syntax → Bool | atom _ _ => true | _ => false diff --git a/tests/lean/run/bigop.lean b/tests/lean/run/bigop.lean index 3605262a0a..49e1515dc8 100644 --- a/tests/lean/run/bigop.lean +++ b/tests/lean/run/bigop.lean @@ -105,11 +105,7 @@ macro_rules `(Σ $idx:index => $F:term) => `(Prod ($idx:index) $F) syntax "def_bigop" str term:max term:max : command macro_rules | `(def_bigop $head:strLit $op $unit) => - -- We have to use `$(mkAntiquotStx idx "index"):index` instead of `$idx:index` because it occurs inside of a nested quasiquotation. - -- We have to use write `(HasBind.bind `(idx) (fund idx => ...))` to make sure `idx` contains the same macro scopes of the `idx` occurring - -- on the left-hand-side of the macro command. - HasBind.bind `(idx) (fun idx => HasBind.bind `(F) (fun F => - `(macro $head:strLit "(" idx:index ")" F:term : term => `(_big [$op, $unit] ($(idx.termIdToAntiquot "index"):index) $(F.termIdToAntiquot "term"))))) + `(macro $head:strLit "(" idx:index ")" F:term : term => `(_big [$op, $unit] ($$idx:index) $$F)) def_bigop "SUM" Nat.add 0 #check SUM (i <- [0, 1, 2]) i+1