From 43f6d0a76152a78df120ea03e079eb892064987b Mon Sep 17 00:00:00 2001 From: Mario Carneiro Date: Tue, 30 May 2023 15:08:24 -0400 Subject: [PATCH] feat: implement `have this` (part 1) --- src/Init/Notation.lean | 6 ------ src/Init/Tactics.lean | 2 +- src/Lean/Elab/Binders.lean | 5 +++-- src/Lean/Elab/BuiltinNotation.lean | 26 +++++++++++++++++--------- src/Lean/Elab/Deriving/DecEq.lean | 2 +- src/Lean/Elab/Do.lean | 22 ++++++++++++++-------- src/Lean/Elab/LetRec.lean | 2 ++ src/Lean/Elab/MutualDef.lean | 1 + src/Lean/Parser/Term.lean | 8 ++++---- stage0/src/stdlib_flags.h | 2 +- 10 files changed, 44 insertions(+), 32 deletions(-) diff --git a/src/Init/Notation.lean b/src/Init/Notation.lean index 51b49db630..fa83914edb 100644 --- a/src/Init/Notation.lean +++ b/src/Init/Notation.lean @@ -496,12 +496,6 @@ macro_rules else `(%[ $elems,* | List.nil ]) --- Declare `this` as a keyword that unhygienically binds to a scope-less `this` assumption (or other binding). --- The keyword prevents declaring a `this` binding except through metaprogramming, as is done by `have`/`show`. -/-- Special identifier introduced by "anonymous" `have : ...`, `suffices p ...` etc. -/ -macro tk:"this" : term => - return (⟨(Syntax.ident tk.getHeadInfo "this".toSubstring `this [])⟩ : TSyntax `term) - /-- Category for carrying raw syntax trees between macros; any content is printed as is by the pretty printer. The only accepted parser for this category is an antiquotation. diff --git a/src/Init/Tactics.lean b/src/Init/Tactics.lean index 394d0e4894..845a824773 100644 --- a/src/Init/Tactics.lean +++ b/src/Init/Tactics.lean @@ -511,7 +511,7 @@ macro "refine_lift' " e:term : tactic => `(tactic| focus (refine' no_implicit_la /-- Similar to `have`, but using `refine'` -/ macro "have' " d:haveDecl : tactic => `(tactic| refine_lift' have $d:haveDecl; ?_) /-- Similar to `have`, but using `refine'` -/ -macro (priority := high) "have'" x:ident " := " p:term : tactic => `(tactic| have' $x : _ := $p) +macro (priority := high) "have'" x:ident " := " p:term : tactic => `(tactic| have' $x:ident : _ := $p) /-- Similar to `let`, but using `refine'` -/ macro "let' " d:letDecl : tactic => `(tactic| refine_lift' let $d:letDecl; ?_) diff --git a/src/Lean/Elab/Binders.lean b/src/Lean/Elab/Binders.lean index 7db9a88b6d..6ba8fbdb84 100644 --- a/src/Lean/Elab/Binders.lean +++ b/src/Lean/Elab/Binders.lean @@ -689,7 +689,7 @@ structure LetIdDeclView where value : Syntax def mkLetIdDeclView (letIdDecl : Syntax) : LetIdDeclView := - -- `letIdDecl` is of the form `ident >> many bracketedBinder >> optType >> " := " >> termParser + -- `letIdDecl` is of the form `binderIdent >> many bracketedBinder >> optType >> " := " >> termParser let id := letIdDecl[0] let binders := letIdDecl[1].getArgs let optType := letIdDecl[2] @@ -708,6 +708,7 @@ def elabLetDeclCore (stx : Syntax) (expectedType? : Option Expr) (useLetExpr : B let body := stx[3] if letDecl.getKind == ``Lean.Parser.Term.letIdDecl then let { id, binders, type, value } := mkLetIdDeclView letDecl + let id ← if id.isIdent then pure id else mkFreshIdent id (canonical := true) elabLetDeclAux id binders type value body expectedType? useLetExpr elabBodyFirst usedLetOnly else if letDecl.getKind == ``Lean.Parser.Term.letPatDecl then -- node `Lean.Parser.Term.letPatDecl $ try (termParser >> pushNone >> optType >> " := ") >> termParser @@ -717,7 +718,7 @@ def elabLetDeclCore (stx : Syntax) (expectedType? : Option Expr) (useLetExpr : B let optType := letDecl[2] let val := letDecl[4] if pat.getKind == ``Parser.Term.hole then - -- `let _ := ...` should not be treated at a `letIdDecl` + -- `let _ := ...` should not be treated as a `letIdDecl` let id ← mkFreshIdent pat (canonical := true) let type := expandOptType id optType elabLetDeclAux id #[] type val body expectedType? useLetExpr elabBodyFirst usedLetOnly diff --git a/src/Lean/Elab/BuiltinNotation.lean b/src/Lean/Elab/BuiltinNotation.lean index cfe145dc19..e2ff3e907d 100644 --- a/src/Lean/Elab/BuiltinNotation.lean +++ b/src/Lean/Elab/BuiltinNotation.lean @@ -104,17 +104,25 @@ open Meta @[builtin_macro Lean.Parser.Term.have] def expandHave : Macro := fun stx => match stx with - | `(have $x $bs* $[: $type]? := $val; $body) => `(let_fun $x $bs* $[: $type]? := $val; $body) - | `(have%$tk $[: $type]? := $val; $body) => `(have $(mkIdentFrom tk `this (canonical := true)) $[: $type]? := $val; $body) - | `(have $x $bs* $[: $type]? $alts; $body) => `(let_fun $x $bs* $[: $type]? $alts; $body) - | `(have%$tk $[: $type]? $alts:matchAlts; $body) => `(have $(mkIdentFrom tk `this (canonical := true)) $[: $type]? $alts:matchAlts; $body) - | `(have $pattern:term $[: $type]? := $val:term; $body) => `(let_fun $pattern:term $[: $type]? := $val:term ; $body) - | _ => Macro.throwUnsupported + | `(have $hy:hygieneInfo $bs* $[: $type]? := $val; $body) => + `(have $(HygieneInfo.mkIdent hy `this (canonical := true)) $bs* $[: $type]? := $val; $body) + | `(have $hy:hygieneInfo $bs* $[: $type]? $alts; $body) => + `(have $(HygieneInfo.mkIdent hy `this (canonical := true)) $bs* $[: $type]? $alts; $body) + | `(have $x:ident $bs* $[: $type]? := $val; $body) => `(let_fun $x $bs* $[: $type]? := $val; $body) + | `(have $x:ident $bs* $[: $type]? $alts; $body) => `(let_fun $x $bs* $[: $type]? $alts; $body) + | `(have _%$x $bs* $[: $type]? := $val; $body) => `(let_fun _%$x $bs* $[: $type]? := $val; $body) + | `(have _%$x $bs* $[: $type]? $alts; $body) => `(let_fun _%$x $bs* $[: $type]? $alts; $body) + | `(have $pattern:term $[: $type]? := $val; $body) => `(let_fun $pattern:term $[: $type]? := $val; $body) + | _ => Macro.throwUnsupported @[builtin_macro Lean.Parser.Term.suffices] def expandSuffices : Macro - | `(suffices%$tk $[$x :]? $type from $val; $body) => `(have%$tk $[$x]? : $type := $body; $val) - | `(suffices%$tk $[$x :]? $type by%$b $tac:tacticSeq; $body) => `(have%$tk $[$x]? : $type := $body; by%$b $tac) - | _ => Macro.throwUnsupported + | `(suffices%$tk $x:ident : $type from $val; $body) => `(have%$tk $x : $type := $body; $val) + | `(suffices%$tk _%$x : $type from $val; $body) => `(have%$tk _%$x : $type := $body; $val) + | `(suffices%$tk $hy:hygieneInfo $type from $val; $body) => `(have%$tk $hy:hygieneInfo : $type := $body; $val) + | `(suffices%$tk $x:ident : $type by%$b $tac:tacticSeq; $body) => `(have%$tk $x : $type := $body; by%$b $tac) + | `(suffices%$tk _%$x : $type by%$b $tac:tacticSeq; $body) => `(have%$tk _%$x : $type := $body; by%$b $tac) + | `(suffices%$tk $hy:hygieneInfo $type by%$b $tac:tacticSeq; $body) => `(have%$tk $hy:hygieneInfo : $type := $body; by%$b $tac) + | _ => Macro.throwUnsupported open Lean.Parser in private def elabParserMacroAux (prec e : Term) (withAnonymousAntiquot : Bool) : TermElabM Syntax := do diff --git a/src/Lean/Elab/Deriving/DecEq.lean b/src/Lean/Elab/Deriving/DecEq.lean index 9e655ccddf..8a7c66136b 100644 --- a/src/Lean/Elab/Deriving/DecEq.lean +++ b/src/Lean/Elab/Deriving/DecEq.lean @@ -166,7 +166,7 @@ def mkDecEqEnum (declName : Name) : CommandElabM Unit := do fun x y => if h : x.toCtorIdx = y.toCtorIdx then -- We use `rfl` in the following proof because the first script fails for unit-like datatypes due to etaStruct. - isTrue (by first | have aux := congrArg $ofNatIdent h; rw [$auxThmIdent:ident, $auxThmIdent:ident] at aux; assumption | rfl) + isTrue (by first | refine_lift let_fun aux := congrArg $ofNatIdent h; ?_; rw [$auxThmIdent:ident, $auxThmIdent:ident] at aux; assumption | rfl) else isFalse fun h => by subst h; contradiction ) diff --git a/src/Lean/Elab/Do.lean b/src/Lean/Elab/Do.lean index 9160cd89a9..e8cb54516e 100644 --- a/src/Lean/Elab/Do.lean +++ b/src/Lean/Elab/Do.lean @@ -49,7 +49,7 @@ private def letDeclArgHasBinders (letDeclArg : Syntax) : Bool := else if k == ``Parser.Term.letEqnsDecl then true else if k == ``Parser.Term.letIdDecl then - -- letIdLhs := ident >> checkWsBefore "expected space before binders" >> many (ppSpace >> letIdBinder)) >> optType + -- letIdLhs := binderIdent >> checkWsBefore "expected space before binders" >> many (ppSpace >> letIdBinder)) >> optType let binders := letDeclArg[1] binders.getNumArgs > 0 else @@ -584,8 +584,11 @@ def concat (terminal : CodeBlock) (kRef : Syntax) (y? : Option Var) (k : CodeBlo let terminal ← liftMacroM <| convertTerminalActionIntoJmp terminal.code jp xs return { code := attachJP jpDecl terminal, uvars := k.uvars } -def getLetIdDeclVar (letIdDecl : Syntax) : Var := - letIdDecl[0] +def getLetIdDeclVars (letIdDecl : Syntax) : Array Var := + if letIdDecl[0].isIdent then + #[letIdDecl[0]] + else + #[] -- support both regular and syntax match def getPatternVarsEx (pattern : Syntax) : TermElabM (Array Var) := @@ -600,17 +603,20 @@ def getLetPatDeclVars (letPatDecl : Syntax) : TermElabM (Array Var) := do let pattern := letPatDecl[0] getPatternVarsEx pattern -def getLetEqnsDeclVar (letEqnsDecl : Syntax) : Var := - letEqnsDecl[0] +def getLetEqnsDeclVars (letEqnsDecl : Syntax) : Array Var := + if letEqnsDecl[0].isIdent then + #[letEqnsDecl[0]] + else + #[] def getLetDeclVars (letDecl : Syntax) : TermElabM (Array Var) := do let arg := letDecl[0] if arg.getKind == ``Parser.Term.letIdDecl then - return #[getLetIdDeclVar arg] + return getLetIdDeclVars arg else if arg.getKind == ``Parser.Term.letPatDecl then getLetPatDeclVars arg else if arg.getKind == ``Parser.Term.letEqnsDecl then - return #[getLetEqnsDeclVar arg] + return getLetEqnsDeclVars arg else throwError "unexpected kind of let declaration" @@ -672,7 +678,7 @@ def getDoLetArrowVars (doLetArrow : Syntax) : TermElabM (Array Var) := do def getDoReassignVars (doReassign : Syntax) : TermElabM (Array Var) := do let arg := doReassign[0] if arg.getKind == ``Parser.Term.letIdDecl then - return #[getLetIdDeclVar arg] + return getLetIdDeclVars arg else if arg.getKind == ``Parser.Term.letPatDecl then getLetPatDeclVars arg else diff --git a/src/Lean/Elab/LetRec.lean b/src/Lean/Elab/LetRec.lean index 41a5153137..73e49fe7df 100644 --- a/src/Lean/Elab/LetRec.lean +++ b/src/Lean/Elab/LetRec.lean @@ -37,6 +37,8 @@ private def mkLetRecDeclView (letRec : Syntax) : TermElabM LetRecView := do throwErrorAt decl "patterns are not allowed in 'let rec' expressions" else if decl.isOfKind `Lean.Parser.Term.letIdDecl || decl.isOfKind `Lean.Parser.Term.letEqnsDecl then let declId := decl[0] + unless declId.isIdent do + throwErrorAt declId "'let rec' expressions must be named" let shortDeclName := declId.getId let currDeclName? ← getDeclName? let declName := currDeclName?.getD Name.anonymous ++ shortDeclName diff --git a/src/Lean/Elab/MutualDef.lean b/src/Lean/Elab/MutualDef.lean index 522c15719f..e37eb7d206 100644 --- a/src/Lean/Elab/MutualDef.lean +++ b/src/Lean/Elab/MutualDef.lean @@ -210,6 +210,7 @@ private def expandWhereStructInst : Macro have : Coe (TSyntax ``letIdBinder) (TSyntax ``funBinder) := ⟨(⟨·⟩)⟩ val ← if binders.size > 0 then `(fun $binders* => $val) else pure val `(structInstField|$id:ident := $val) + | stx@`(letIdDecl|_ $_* $[: $_]? := $_) => Macro.throwErrorAt stx "'_' is not allowed here" | _ => Macro.throwUnsupported let body ← `({ $structInstFields,* }) match whereDecls? with diff --git a/src/Lean/Parser/Term.lean b/src/Lean/Parser/Term.lean index 5654ed66ca..47d0853c0e 100644 --- a/src/Lean/Parser/Term.lean +++ b/src/Lean/Parser/Term.lean @@ -119,6 +119,7 @@ def optSemicolon (p : Parser) : Parser := "_" @[builtin_term_parser] def syntheticHole := leading_parser "?" >> (ident <|> hole) +def binderIdent : Parser := ident <|> hole /-- A temporary placeholder for a missing proof or value. -/ @[builtin_term_parser] def «sorry» := leading_parser "sorry" @@ -165,7 +166,7 @@ def fromTerm := leading_parser "from " >> termParser def showRhs := fromTerm <|> byTactic' def sufficesDecl := leading_parser - optIdent >> termParser >> ppSpace >> showRhs + (atomic (group (binderIdent >> " : ")) <|> hygieneInfo) >> termParser >> ppSpace >> showRhs @[builtin_term_parser] def «suffices» := leading_parser:leadPrec withPosition ("suffices " >> sufficesDecl) >> optSemicolon termParser @[builtin_term_parser] def «show» := leading_parser:leadPrec "show " >> termParser >> ppSpace >> showRhs @@ -209,7 +210,6 @@ In contrast to regular patterns, `e` may be an arbitrary term of the appropriate -/ @[builtin_term_parser] def inaccessible := leading_parser ".(" >> withoutPosition termParser >> ")" -def binderIdent : Parser := ident <|> hole def binderType (requireType := false) : Parser := if requireType then node nullKind (" : " >> termParser) else optional (" : " >> termParser) def binderTactic := leading_parser @@ -394,7 +394,7 @@ def letIdBinder := binderIdent <|> bracketedBinder /- Remark: we use `checkWsBefore` to ensure `let x[i] := e; b` is not parsed as `let x [i] := e; b` where `[i]` is an `instBinder`. -/ def letIdLhs : Parser := - ident >> notFollowedBy (checkNoWsBefore "" >> "[") + binderIdent >> notFollowedBy (checkNoWsBefore "" >> "[") "space is required before instance '[...]' binders to distinguish them from array updates `let x[i] := e; ...`" >> many (ppSpace >> letIdBinder) >> optType def letIdDecl := leading_parser (withAnonymousAntiquot := false) @@ -467,7 +467,7 @@ It is often used when building macros. withPosition ("let_tmp " >> letDecl) >> optSemicolon termParser /- like `let_fun` but with optional name -/ -def haveIdLhs := optional (ppSpace >> ident >> many (ppSpace >> letIdBinder)) >> optType +def haveIdLhs := ((ppSpace >> binderIdent) <|> hygieneInfo) >> many (ppSpace >> letIdBinder) >> optType def haveIdDecl := leading_parser (withAnonymousAntiquot := false) atomic (haveIdLhs >> " := ") >> termParser def haveEqnsDecl := leading_parser (withAnonymousAntiquot := false) diff --git a/stage0/src/stdlib_flags.h b/stage0/src/stdlib_flags.h index a574103a7f..1b694ba677 100644 --- a/stage0/src/stdlib_flags.h +++ b/stage0/src/stdlib_flags.h @@ -8,7 +8,7 @@ options get_default_options() { // switch to `true` for ABI-breaking changes affecting meta code opts = opts.update({"interpreter", "prefer_native"}, false); // switch to `true` for changing built-in parsers used in quotations - opts = opts.update({"internal", "parseQuotWithCurrentStage"}, false); + opts = opts.update({"internal", "parseQuotWithCurrentStage"}, true); // toggling `parseQuotWithCurrentStage` may also require toggling the following option if macros/syntax // with custom precheck hooks were affected opts = opts.update({"quotPrecheck"}, true);