From ddafed330fceb9c133c8610c2a2f2b36069abddd Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Fri, 24 Jun 2022 20:31:38 +0200 Subject: [PATCH] chore: changes to placate coercions --- src/Init/NotationExtra.lean | 2 +- src/Lean/Elab/Deriving/Repr.lean | 2 +- src/Lean/Elab/ElabRules.lean | 6 +++--- src/Lean/Elab/Quotation.lean | 4 ++-- src/Lean/Hygiene.lean | 7 ++++--- src/Lean/PrettyPrinter/Delaborator/Builtins.lean | 2 +- src/Lean/Server/Rpc/Deriving.lean | 2 +- 7 files changed, 13 insertions(+), 12 deletions(-) diff --git a/src/Init/NotationExtra.lean b/src/Init/NotationExtra.lean index 86ae88ec5201..6b4a67bc8070 100644 --- a/src/Init/NotationExtra.lean +++ b/src/Init/NotationExtra.lean @@ -170,7 +170,7 @@ macro_rules macro_rules | `(%[ $[$x],* | $k ]) => if x.size < 8 then - x.foldrM (init := k) fun x k => + x.foldrM (β := TSyntax `term) (init := k) fun x k => `(List.cons $x $k) else let m := x.size / 2 diff --git a/src/Lean/Elab/Deriving/Repr.lean b/src/Lean/Elab/Deriving/Repr.lean index 6483c460a0ec..30394b41907e 100644 --- a/src/Lean/Elab/Deriving/Repr.lean +++ b/src/Lean/Elab/Deriving/Repr.lean @@ -58,7 +58,7 @@ where for _ in [:indVal.numIndices] do patterns := patterns.push (← `(_)) let mut ctorArgs := #[] - let mut rhs := Syntax.mkStrLit (toString ctorInfo.name) + let mut rhs : TSyntax `term := Syntax.mkStrLit (toString ctorInfo.name) rhs ← `(Format.text $rhs) -- add `_` for inductive parameters, they are inaccessible for _ in [:indVal.numParams] do diff --git a/src/Lean/Elab/ElabRules.lean b/src/Lean/Elab/ElabRules.lean index 6f70d3b01d8a..561194dda4a8 100644 --- a/src/Lean/Elab/ElabRules.lean +++ b/src/Lean/Elab/ElabRules.lean @@ -88,9 +88,9 @@ def elabElab : CommandElab let name ← match name? with | some name => pure name.getId | none => liftMacroM <| mkNameFromParserSyntax cat.getId (mkNullNode stxParts) - let pat := mkNode ((← getCurrNamespace) ++ name) patArgs - `($[$doc?:docComment]? $attrKind:attrKind syntax$[:$prec?]? (name := $(← mkIdentFromRef name)) (priority := $(quote prio)) $[$stxParts]* : $cat - $[$doc?:docComment]? elab_rules : $cat $[<= $expectedType?]? | `($pat) => $rhs) >>= elabCommand + let pat := ⟨mkNode ((← getCurrNamespace) ++ name) patArgs⟩ + `($[$doc?:docComment]? $attrKind:attrKind syntax$[:$prec?]? (name := $(← mkIdentFromRef name)) (priority := $(quote prio):num) $[$stxParts]* : $cat + $[$doc?:docComment]? elab_rules : $cat $[<= $expectedType?]? | `($pat) => $rhs) >>= (elabCommand ·) | _ => throwUnsupportedSyntax end Lean.Elab.Command diff --git a/src/Lean/Elab/Quotation.lean b/src/Lean/Elab/Quotation.lean index 88e3afedbbbc..4fbc245122b4 100644 --- a/src/Lean/Elab/Quotation.lean +++ b/src/Lean/Elab/Quotation.lean @@ -47,7 +47,7 @@ private def getSepFromSplice (splice : Syntax) : String := private def getSepStxFromSplice (splice : Syntax) : Syntax := Unhygienic.run do match getSepFromSplice splice with | "" => `(mkNullNode) -- sepByIdent uses the null node for separator-less enumerations - | sep => `(mkAtom $(.mkStrLit sep)) + | sep => `(mkAtom $(Syntax.mkStrLit sep)) partial def mkTuple : Array Syntax → TermElabM Syntax | #[] => `(Unit.unit) @@ -151,7 +151,7 @@ private partial def quoteSyntax : Syntax → TermElabM (TSyntax `term) | $[some $ids:ident],* => $(quote inner) | $[_%$ids],* => Array.empty) | _ => - let arr ← ids[:ids.size-1].foldrM (fun id arr => `(Array.zip $id $arr)) ids.back + let arr ← ids[:ids.size-1].foldrM (fun id arr => `(Array.zip $id:ident $arr)) ids.back `(Array.map (fun $(← mkTuple ids) => $(inner[0])) $arr) let arr ← if k == `sepBy then `(mkSepArray $arr $(getSepStxFromSplice arg)) diff --git a/src/Lean/Hygiene.lean b/src/Lean/Hygiene.lean index 228e7a15dcd7..5b7ff6f28db3 100644 --- a/src/Lean/Hygiene.lean +++ b/src/Lean/Hygiene.lean @@ -95,9 +95,10 @@ def sanitizeName (userName : Name) : StateM NameSanitizerState Name := do private partial def sanitizeSyntaxAux : Syntax → StateM NameSanitizerState Syntax | stx@(Syntax.ident _ _ n _) => do - mkIdentFrom stx <$> match (← get).userName2Sanitized.find? n with - | some n' => pure n' - | none => if n.hasMacroScopes then sanitizeName n else pure n + let n ← match (← get).userName2Sanitized.find? n with + | some n' => pure n' + | none => if n.hasMacroScopes then sanitizeName n else pure n + return mkIdentFrom stx n | Syntax.node info k args => Syntax.node info k <$> args.mapM sanitizeSyntaxAux | stx => pure stx diff --git a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean index d81a74fc1cb4..c8cf6fc4f318 100644 --- a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean +++ b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean @@ -274,7 +274,7 @@ def delabAppImplicit : Delab := do let v := param.defVal.get! if !v.hasLooseBVars && v == arg then pure none else delab else if !param.isRegularExplicit && param.defVal.isNone then - if ← getPPOption getPPAnalysisNamedArg <||> (pure (param.name == `motive) <&&> shouldShowMotive arg opts) then mkNamedArg param.name (← delab) else pure none + if ← getPPOption getPPAnalysisNamedArg <||> (pure (param.name == `motive) <&&> shouldShowMotive arg opts) then some <$> mkNamedArg param.name (← delab) else pure none else delab let argStxs := match argStx? with | none => argStxs diff --git a/src/Lean/Server/Rpc/Deriving.lean b/src/Lean/Server/Rpc/Deriving.lean index 60cf8c27472c..ed0b8a9bf6b7 100644 --- a/src/Lean/Server/Rpc/Deriving.lean +++ b/src/Lean/Server/Rpc/Deriving.lean @@ -229,7 +229,7 @@ private def deriveInductiveInstance (indVal : InductiveVal) (params : Array Expr -- helpers for type name syntax let paramIds ← params.mapM fun p => return mkIdent (← getFVarLocalDecl p).userName let typeId := Syntax.mkApp (← `(@$(mkIdent indVal.name))) paramIds - let packetAppliedId := Syntax.mkApp (mkIdent packetNm) (st.uniqEncArgTypes.map mkIdent) + let packetAppliedId := Syntax.mkApp (mkIdent packetNm) (st.uniqEncArgTypes.map (mkIdent ·)) `(variable $st.binders*