max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: remove auxiliary _app_

Browse source
This commit is contained in:
Leonardo de Moura 2020-01-17 17:39:44 -08:00
parent eda70a5567
commit 47fb604e78
1 changed files with 15 additions and 15 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

30
src/Init/Lean/Elab/Quotation.lean
View file

@ -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