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

feat: modify app representation

Browse source
This commit is contained in:
Leonardo de Moura 2020-01-17 16:49:22 -08:00
parent 749b6b1b7e
commit e4123585b2
2 changed files with 7 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
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) (addMacroScope $val scp) $(quote preresolved))
`(_app_ Syntax.ident none $(quote rawVal) (_app_ addMacroScope $val scp) $(quote preresolved))
-- if antiquotation, insert contents as-is, else recurse
| stx@(Syntax.node k args) =>
if isAntiquot stx then
@ -272,7 +272,7 @@ 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 (Syntax.getArgs discr) == $(quote pats.size))
| 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)
| _, _ => unreachable!
@ -391,8 +391,8 @@ private unsafe partial def toPreterm : Syntax → TermElabM Expr
pure $ lctx.mkLambda #[mkFVar n] e
| `Lean.Parser.Term.app => do
fn ← toPreterm $ args.get! 0;
arg ← toPreterm $ args.get! 1;
pure $ mkApp fn arg
as ← (args.get! 1).getArgs.mapM toPreterm;
pure $ mkAppN fn as
| `Lean.Parser.Term.appCore => do
fn ← toPreterm $ args.get! 1;
as ← (args.get! 2).getArgs.mapM toPreterm;

5
src/Init/Lean/Parser/Term.lean
View file

@ -112,7 +112,7 @@ def bracketedDoSeq := parser! "{" >> doSeq >> "}"
@[builtinTermParser] def uminus := parser! "-" >> termParser 100
def namedArgument := tparser! try ("(" >> ident >> " := ") >> termParser >> ")"
@[builtinTermParser] def app := tparser! pushLeading >> (namedArgument <|> termParser appPrec)
@[builtinTermParser] def app := tparser! pushLeading >> many1 (namedArgument <|> termParser appPrec)
-- Auxiliary notation used for fixing bootstrapping issues
@[builtinTermParser] def appCore := parser! "_app_ " >> termParser appPrec >> many1 (termParser appPrec)
@ -183,7 +183,8 @@ end Parser
open Parser
def mkAppStx (fn : Syntax) (args : Array Syntax) : Syntax :=
args.foldl (fun fn arg => Syntax.node `Lean.Parser.Term.app #[fn, arg]) fn
Syntax.node `Lean.Parser.Term.app #[fn, mkNullNode args]
-- args.foldl (fun fn arg => Syntax.node `Lean.Parser.Term.app #[fn, arg]) fn
def mkHole (ref : Syntax) := mkNode `Lean.Parser.Term.hole #[mkAtomFrom ref "_"]