From b708407b7bb4132a74b5b796dea482e022f2129d Mon Sep 17 00:00:00 2001 From: Leonardo de Moura Date: Sat, 25 Jan 2020 15:34:24 -0800 Subject: [PATCH] chore: implement `Quotation.lean` using `let_core`, disable `let` syntax --- src/Init/Lean/Elab/BuiltinNotation.lean | 2 ++ src/Init/Lean/Elab/Quotation.lean | 27 ++++++++++++++++++------- src/Init/Lean/Elab/TermBinders.lean | 2 ++ 3 files changed, 24 insertions(+), 7 deletions(-) diff --git a/src/Init/Lean/Elab/BuiltinNotation.lean b/src/Init/Lean/Elab/BuiltinNotation.lean index 5261baae9f..7f2a86379f 100644 --- a/src/Init/Lean/Elab/BuiltinNotation.lean +++ b/src/Init/Lean/Elab/BuiltinNotation.lean @@ -77,6 +77,7 @@ adaptExpander $ fun stx => match_syntax stx with | `(have $x : $type := $val; $body) => `((fun ($x:ident : $type) => $body) $val) | _ => throwUnsupportedSyntax +/- @[termElab «where»] def elabWhere : TermElab := adaptExpander $ fun stx => match_syntax stx with | `($body where $decls*) => do @@ -85,6 +86,7 @@ adaptExpander $ fun stx => match_syntax stx with (fun decl body => `(let $decl; $body)) body | _ => throwUnsupportedSyntax +-/ @[termElab «parser!»] def elabParserMacro : TermElab := adaptExpander $ fun stx => match_syntax stx with diff --git a/src/Init/Lean/Elab/Quotation.lean b/src/Init/Lean/Elab/Quotation.lean index a456126299..aa357adb21 100644 --- a/src/Init/Lean/Elab/Quotation.lean +++ b/src/Init/Lean/Elab/Quotation.lean @@ -194,7 +194,7 @@ private def getHeadInfo (alt : Alt) : HeadInfo := let pat := alt.fst.head!; let unconditional (rhsFn) := { HeadInfo . rhsFn := rhsFn }; -- variable pattern -if pat.isOfKind `Lean.Parser.Term.id then unconditional $ fun rhs => `(let $pat:id := discr; $rhs) +if pat.isOfKind `Lean.Parser.Term.id then unconditional $ fun rhs => `(let_core $pat := discr; $rhs) -- wildcard pattern else if pat.isOfKind `Lean.Parser.Term.hole then unconditional pure -- quotation pattern @@ -222,13 +222,13 @@ else if pat.isOfKind `Lean.Parser.Term.stxQuot then | anti => anti; -- Splices should only appear inside a nullKind node, see next case 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:id := discr; $rhs) } + else if anti.isOfKind `Lean.Parser.Term.id then { kind := kind, rhsFn := fun rhs => `(let_core $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:term := Syntax.getArgs discr; $rhs) + unconditional $ fun rhs => `(let_core $anti := Syntax.getArgs discr; $rhs) -- TODO: support for more complex antiquotation splices else -- not an antiquotation: match head shape @@ -269,14 +269,14 @@ private partial def compileStxMatch (ref : Syntax) : List Syntax → List Alt yes ← withFreshMacroScope $ compileStxMatch (newDiscrs ++ discrs) yesAlts; some kind ← pure info.kind -- unconditional match step - | `(let discr := $discr; $yes); + | `(let_core discr := $discr; $yes); -- conditional match step 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 => `(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) + `(let_core discr := $discr; if coe $cond then $yes else $no) | _, _ => unreachable! private partial def getPatternVarsAux : Syntax → List Syntax @@ -314,13 +314,13 @@ private def letBindRhss (cont : List Alt → TermElabM Syntax) : List Alt → Li 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) + `(let_core rhs := fun _ => $rhs; $stx) | _ => do -- rhs ← `(fun $vars* => $rhs) let rhs := Syntax.node `Lean.Parser.Term.fun #[mkAtom "fun", Syntax.node `null vars.toArray, mkAtom "=>", rhs]; rhs' ← `(rhs); stx ← withFreshMacroScope $ letBindRhss alts ((pats, rhs')::altsRev'); - `(let rhs := $rhs; $stx) + `(let_core rhs := $rhs; $stx) def match_syntax.expand (stx : Syntax) : TermElabM Syntax := do let discr := stx.getArg 1; @@ -391,6 +391,19 @@ private unsafe partial def toPreterm : Syntax → TermElabM Expr adaptReader (fun (ctx : Context) => { lctx := lctx, .. ctx }) $ do e ← toPreterm $ args.get! 3; pure $ lctx.mkLambda #[mkFVar n] e + | `Lean.Parser.Term.let_core => + -- parser! "let_core " >> termParser >> ":=" >> termParser >> "; " >> termParser + match (args.get! 1).isSimpleTermId? true with + | some n => do + let n := n.getId; + let val := args.get! 3; + val ← toPreterm val; + lctx ← getLCtx; + let lctx := lctx.mkLetDecl n n exprPlaceholder val; + adaptReader (fun (ctx : Context) => { lctx := lctx, .. ctx }) $ do + e ← toPreterm $ args.get! 5; + pure $ lctx.mkLambda #[mkFVar n] e + | none => throwError stx $ "stxQuot: unsupported let_core" | `Lean.Parser.Term.app => do fn ← toPreterm $ args.get! 0; as ← (args.get! 1).getArgs.mapM toPreterm; diff --git a/src/Init/Lean/Elab/TermBinders.lean b/src/Init/Lean/Elab/TermBinders.lean index 37f0b9e699..c9a7072cc7 100644 --- a/src/Init/Lean/Elab/TermBinders.lean +++ b/src/Init/Lean/Elab/TermBinders.lean @@ -311,6 +311,7 @@ throwError decl "not implemented yet" def elabLetPatDecl (ref : Syntax) (decl body : Syntax) (expectedType? : Option Expr) : TermElabM Expr := throwError decl "not implemented yet" +/- @[builtinTermElab «let»] def elabLet : TermElab := fun stx expectedType? => match_syntax stx with | `(let $id:id := $decl; $body) => do @@ -332,6 +333,7 @@ fun stx expectedType? => match_syntax stx with elabLetPatDecl ref decl body expectedType? else throwError ref "unknown let-declaration kind" +-/ @[init] private def regTraceClasses : IO Unit := do registerTraceClass `Elab.let;