From 47fb604e786726431c6ca65468acdf706c7573e5 Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Fri, 17 Jan 2020 17:39:44 -0800 Subject: [PATCH] chore: remove auxiliary `_app_` --- src/Init/Lean/Elab/Quotation.lean | 30 +++++++++++++++--------------- 1 file changed, 15 insertions(+), 15 deletions(-) diff --git a/src/Init/Lean/Elab/Quotation.lean b/src/Init/Lean/Elab/Quotation.lean index 01e116d28b..a4776b3177 100644 --- a/src/Init/Lean/Elab/Quotation.lean +++ b/src/Init/Lean/Elab/Quotation.lean @@ -106,7 +106,7 @@ private partial def quoteSyntax : Syntax → TermElabM Syntax let preresolved := resolveGlobalName env currNamespace openDecls val ++ preresolved; let val := quote val; -- `scp` is bound in stxQuot.expand - `(_app_ Syntax.ident none $(quote rawVal) (_app_ addMacroScope $val scp) $(quote preresolved)) + `(Syntax.ident none $(quote rawVal) (addMacroScope $val scp) $(quote preresolved)) -- if antiquotation, insert contents as-is, else recurse | stx@(Syntax.node k args) => if isAntiquot stx then @@ -119,13 +119,13 @@ private partial def quoteSyntax : Syntax → TermElabM Syntax if k == nullKind && isAntiquotSplice arg then -- antiquotation splice pattern: inject args array let arg := arg.getArg 1; - `(_app_ Array.append $args $arg) + `(Array.append $args $arg) else do arg ← quoteSyntax arg; - `(_app_ Array.push $args $arg)) empty; - `(_app_ Syntax.node $(quote k) $args) + `(Array.push $args $arg)) empty; + `(Syntax.node $(quote k) $args) | Syntax.atom info val => - `(_app_ Syntax.atom none $(quote val)) + `(Syntax.atom none $(quote val)) | Syntax.missing => unreachable! def stxQuot.expand (stx : Syntax) : TermElabM Syntax := do @@ -137,7 +137,7 @@ let quoted := stx.getArg 1; including it literally in a syntax quotation. -/ -- TODO: simplify to `(do scp ← getCurrMacroScope; pure $(quoteSyntax quoted)) stx ← quoteSyntax (elimAntiquotChoices quoted); -`(_app_ bind getCurrMacroScope (fun scp => _app_ pure $stx)) +`(bind getCurrMacroScope (fun scp => pure $stx)) /- NOTE: It may seem like the newly introduced binding `scp` may accidentally capture identifiers in an antiquotation introduced by `quoteSyntax`. However, note that the syntax quotation above enjoys the same hygiene guarantees as @@ -226,7 +226,7 @@ else if pat.isOfKind `Lean.Parser.Term.stxQuot then if isAntiquotSplicePat quoted && quoted.getArgs.size == 1 then -- quotation is a single antiquotation splice => bind args array let anti := (quoted.getArg 0).getArg 1; - unconditional $ fun rhs => `(let $anti:term := _app_ Syntax.getArgs discr; $rhs) + unconditional $ fun rhs => `(let $anti:term := Syntax.getArgs discr; $rhs) -- TODO: support for more complex antiquotation splices else -- not an antiquotation: match head shape @@ -258,7 +258,7 @@ private partial def compileStxMatch (ref : Syntax) : List Syntax → List Alt let (info, alt) := alts.tail!.foldl (fun (min : HeadInfo × Alt) (alt : HeadInfo × Alt) => if min.1.generalizes alt.1 then alt else min) alts.head!; -- introduce pattern matches on the discriminant's children if there are any nested patterns newDiscrs ← match info.argPats with - | some pats => (List.range pats.size).mapM $ fun i => `(_app_ Syntax.getArg discr $(quote i)) + | some pats => (List.range pats.size).mapM $ fun i => `(Syntax.getArg discr $(quote i)) | none => pure []; -- collect matching alternatives and explode them let yesAlts := alts.filter $ fun (alt : HeadInfo × Alt) => alt.1.generalizes info; @@ -272,9 +272,9 @@ private partial def compileStxMatch (ref : Syntax) : List Syntax → List Alt let noAlts := (alts.filter $ fun (alt : HeadInfo × Alt) => !info.generalizes alt.1).map Prod.snd; no ← withFreshMacroScope $ compileStxMatch (discr::discrs) noAlts; cond ← match info.argPats with - | some pats => `(_app_ Syntax.isOfKind discr $(quote kind) && _app_ Array.size (_app_ Syntax.getArgs discr) == $(quote pats.size)) - | none => `(_app_ Syntax.isOfKind discr $(quote kind)); - `(let discr := $discr; if _app_ coe $cond then $yes else $no) + | some pats => `(Syntax.isOfKind discr $(quote kind) && Array.size (Syntax.getArgs discr) == $(quote pats.size)) + | none => `(Syntax.isOfKind discr $(quote kind)); + `(let discr := $discr; if coe $cond then $yes else $no) | _, _ => unreachable! private partial def getPatternVarsAux : Syntax → TermElabM (List Syntax) @@ -309,7 +309,7 @@ private def letBindRhss (cont : List Alt → TermElabM Syntax) : List Alt → Li -- no antiquotations => introduce Unit parameter to preserve evaluation order | [] => do -- NOTE: references binding below - rhs' ← `(_app_ rhs ()); + rhs' ← `(rhs ()); -- NOTE: new macro scope so that introduced bindings do not collide stx ← withFreshMacroScope $ letBindRhss alts ((pats, rhs')::altsRev'); `(let rhs := fun _ => $rhs; $stx) @@ -401,17 +401,17 @@ private unsafe partial def toPreterm : Syntax → TermElabM Expr let con := args.get! 2; let yes := args.get! 4; let no := args.get! 6; - toPreterm $ Unhygienic.run `(_app_ ite $con $yes $no) + toPreterm $ Unhygienic.run `(ite $con $yes $no) | `Lean.Parser.Term.paren => let inner := (args.get! 1).getArgs; if inner.size == 0 then pure $ Lean.mkConst `Unit.unit else toPreterm $ inner.get! 0 | `Lean.Parser.Term.band => let lhs := args.get! 0; let rhs := args.get! 2; - toPreterm $ Unhygienic.run `(_app_ and $lhs $rhs) + toPreterm $ Unhygienic.run `(and $lhs $rhs) | `Lean.Parser.Term.beq => let lhs := args.get! 0; let rhs := args.get! 2; - toPreterm $ Unhygienic.run `(_app_ HasBeq.beq $lhs $rhs) + toPreterm $ Unhygienic.run `(HasBeq.beq $lhs $rhs) | `Lean.Parser.Term.str => pure $ mkStrLit $ (stx.getArg 0).isStrLit?.getD "" | `Lean.Parser.Term.num => pure $ mkNatLit $ (stx.getArg 0).isNatLit?.getD 0 | `expr => pure $ unsafeCast $ stx.getArg 0 -- HACK: see below