From 22475b8669ce4691e305dca0207ffc3fcdf2ad57 Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Sat, 25 Jun 2022 11:31:31 +0200 Subject: [PATCH] refactor: introduce common TSyntax abbreviations --- src/Init/Meta.lean | 65 ++++++++++++------- src/Init/NotationExtra.lean | 4 +- src/Lean/Elab/AuxDiscr.lean | 4 +- src/Lean/Elab/Binders.lean | 2 +- src/Lean/Elab/BuiltinNotation.lean | 20 +++--- src/Lean/Elab/Deriving/BEq.lean | 4 +- src/Lean/Elab/Deriving/DecEq.lean | 4 +- src/Lean/Elab/Deriving/FromToJson.lean | 8 +-- src/Lean/Elab/Deriving/Hashable.lean | 4 +- src/Lean/Elab/Deriving/Ord.lean | 6 +- src/Lean/Elab/Deriving/Repr.lean | 10 +-- src/Lean/Elab/Deriving/Util.lean | 8 +-- src/Lean/Elab/Do.lean | 2 +- src/Lean/Elab/ElabRules.lean | 2 +- src/Lean/Elab/MacroArgUtil.lean | 8 +-- src/Lean/Elab/Match.lean | 2 +- src/Lean/Elab/Notation.lean | 6 +- src/Lean/Elab/PatternVar.lean | 8 +-- src/Lean/Elab/Quotation.lean | 14 ++-- src/Lean/Elab/Quotation/Util.lean | 2 +- src/Lean/Elab/Syntax.lean | 8 +-- src/Lean/Elab/Tactic/Match.lean | 2 +- src/Lean/Elab/Tactic/Simp.lean | 2 +- src/Lean/PrettyPrinter.lean | 2 +- src/Lean/PrettyPrinter/Delaborator/Basic.lean | 10 +-- .../PrettyPrinter/Delaborator/Builtins.lean | 10 +-- src/Lean/Server/Rpc/Deriving.lean | 14 ++-- 27 files changed, 124 insertions(+), 107 deletions(-) diff --git a/src/Init/Meta.lean b/src/Init/Meta.lean index 99d8248c68..554089afe1 100644 --- a/src/Init/Meta.lean +++ b/src/Init/Meta.lean @@ -244,6 +244,23 @@ instance monadNameGeneratorLift (m n : Type → Type) [MonadLift m n] [MonadName setNGen := fun ngen => liftM (setNGen ngen : m _) } +namespace Syntax + +abbrev Term := TSyntax `term +abbrev Command := TSyntax `command +protected abbrev Level := TSyntax `level +abbrev Prec := TSyntax `prec +abbrev Prio := TSyntax `prio +abbrev Ident := TSyntax identKind +abbrev StrLit := TSyntax strLitKind +abbrev CharLit := TSyntax charLitKind +abbrev NameLit := TSyntax nameLitKind +abbrev NumLit := TSyntax numLitKind + +end Syntax + +export Syntax (Term Command Prec Prio Ident StrLit CharLit NameLit NumLit) + namespace TSyntax instance : Coe (TSyntax [k]) (TSyntax (k :: ks)) where @@ -252,25 +269,25 @@ instance : Coe (TSyntax [k]) (TSyntax (k :: ks)) where instance [Coe (TSyntax [k]) (TSyntax ks)] : Coe (TSyntax [k]) (TSyntax (k' :: ks)) where coe stx := ⟨stx⟩ -instance : Coe (TSyntax identKind) (TSyntax `term) where +instance : Coe Ident Term where coe s := ⟨s.raw⟩ -instance : CoeDep (TSyntax `term) ⟨Syntax.ident info ss n res⟩ (TSyntax `ident) where +instance : CoeDep Term ⟨Syntax.ident info ss n res⟩ Ident where coe := ⟨Syntax.ident info ss n res⟩ -instance : Coe (TSyntax strLitKind) (TSyntax `term) where +instance : Coe StrLit Term where coe s := ⟨s.raw⟩ -instance : Coe (TSyntax nameLitKind) (TSyntax `term) where +instance : Coe NameLit Term where coe s := ⟨s.raw⟩ -instance : Coe (TSyntax numLitKind) (TSyntax `term) where +instance : Coe NumLit Term where coe s := ⟨s.raw⟩ -instance : Coe (TSyntax charLitKind) (TSyntax `term) where +instance : Coe CharLit Term where coe s := ⟨s.raw⟩ -instance : Coe (TSyntax numLitKind) (TSyntax `prec) where +instance : Coe NumLit Prec where coe s := ⟨s.raw⟩ namespace Compat @@ -430,17 +447,17 @@ partial def expandMacros : Syntax → MacroM Syntax /-- Create an identifier copying the position from `src`. To refer to a specific constant, use `mkCIdentFrom` instead. -/ -def mkIdentFrom (src : Syntax) (val : Name) : TSyntax identKind := +def mkIdentFrom (src : Syntax) (val : Name) : Ident := ⟨Syntax.ident (SourceInfo.fromRef src) (toString val).toSubstring val []⟩ -def mkIdentFromRef [Monad m] [MonadRef m] (val : Name) : m (TSyntax identKind) := do +def mkIdentFromRef [Monad m] [MonadRef m] (val : Name) : m Ident := do return mkIdentFrom (← getRef) val /-- Create an identifier referring to a constant `c` copying the position from `src`. This variant of `mkIdentFrom` makes sure that the identifier cannot accidentally be captured. -/ -def mkCIdentFrom (src : Syntax) (c : Name) : TSyntax identKind := +def mkCIdentFrom (src : Syntax) (c : Name) : Ident := -- Remark: We use the reserved macro scope to make sure there are no accidental collision with our frontend let id := addMacroScope `_internal c reservedMacroScope ⟨Syntax.ident (SourceInfo.fromRef src) (toString id).toSubstring id [(c, [])]⟩ @@ -448,11 +465,11 @@ def mkCIdentFrom (src : Syntax) (c : Name) : TSyntax identKind := def mkCIdentFromRef [Monad m] [MonadRef m] (c : Name) : m Syntax := do return mkCIdentFrom (← getRef) c -def mkCIdent (c : Name) : TSyntax identKind := +def mkCIdent (c : Name) : Ident := mkCIdentFrom Syntax.missing c @[export lean_mk_syntax_ident] -def mkIdent (val : Name) : TSyntax identKind := +def mkIdent (val : Name) : Ident := ⟨Syntax.ident SourceInfo.none (toString val).toSubstring val []⟩ @[inline] def mkNullNode (args : Array Syntax := #[]) : Syntax := @@ -499,27 +516,27 @@ instance : Coe (TSyntaxArray k) (TSepArray k sep) where coe a := ⟨mkSepArray a.raw (mkAtom sep)⟩ /-- Create syntax representing a Lean term application, but avoid degenerate empty applications. -/ -def mkApp (fn : TSyntax `term) : (args : TSyntaxArray `term) → TSyntax `term +def mkApp (fn : Term) : (args : TSyntaxArray `term) → Term | #[] => fn | args => ⟨mkNode `Lean.Parser.Term.app #[fn, mkNullNode args.raw]⟩ -def mkCApp (fn : Name) (args : TSyntaxArray `term) : TSyntax `term := +def mkCApp (fn : Name) (args : TSyntaxArray `term) : Term := mkApp (mkCIdent fn) args def mkLit (kind : SyntaxNodeKind) (val : String) (info := SourceInfo.none) : TSyntax kind := let atom : Syntax := Syntax.atom info val mkNode kind #[atom] -def mkStrLit (val : String) (info := SourceInfo.none) : TSyntax strLitKind := +def mkStrLit (val : String) (info := SourceInfo.none) : StrLit := mkLit strLitKind (String.quote val) info -def mkNumLit (val : String) (info := SourceInfo.none) : TSyntax numLitKind := +def mkNumLit (val : String) (info := SourceInfo.none) : NumLit := mkLit numLitKind val info def mkScientificLit (val : String) (info := SourceInfo.none) : TSyntax scientificLitKind := mkLit scientificLitKind val info -def mkNameLit (val : String) (info := SourceInfo.none) : TSyntax nameLitKind := +def mkNameLit (val : String) (info := SourceInfo.none) : NameLit := mkLit nameLitKind val info /- Recall that we don't have special Syntax constructors for storing numeric and string atoms. @@ -824,7 +841,7 @@ namespace TSyntax def getNat (s : TSyntax numLitKind) : Nat := s.raw.isNatLit?.get! -def getId (s : TSyntax identKind) : Name := +def getId (s : Ident) : Name := s.raw.getId def getString (s : TSyntax strLitKind) : String := @@ -847,7 +864,7 @@ export Quote (quote) instance [Quote α k] [CoeHTCT (TSyntax k) (TSyntax [k'])]: Quote α k' := ⟨fun a => quote (k := k) a⟩ -instance : Quote (TSyntax `term) := ⟨id⟩ +instance : Quote Term := ⟨id⟩ instance : Quote Bool := ⟨fun | true => mkCIdent `Bool.true | false => mkCIdent `Bool.false⟩ instance : Quote String strLitKind := ⟨Syntax.mkStrLit⟩ instance : Quote Nat numLitKind := ⟨fun n => Syntax.mkNumLit <| toString n⟩ @@ -861,7 +878,7 @@ private def getEscapedNameParts? (acc : List String) : Name → Option (List Str getEscapedNameParts? (s::acc) n | Name.num _ _ _ => none -def quoteNameMk : Name → TSyntax `term +def quoteNameMk : Name → Term | Name.anonymous => mkCIdent ``Name.anonymous | Name.str n s _ => Syntax.mkCApp ``Name.mkStr #[quoteNameMk n, quote s] | Name.num n i _ => Syntax.mkCApp ``Name.mkNum #[quoteNameMk n, quote i] @@ -875,7 +892,7 @@ instance [Quote α `term] [Quote β `term] : Quote (α × β) `term where quote | ⟨a, b⟩ => Syntax.mkCApp ``Prod.mk #[quote a, quote b] -private def quoteList [Quote α `term] : List α → TSyntax `term +private def quoteList [Quote α `term] : List α → Term | [] => mkCIdent ``List.nil | (x::xs) => Syntax.mkCApp ``List.cons #[quote x, quoteList xs] @@ -1002,10 +1019,10 @@ instance [Coe (TSyntax k) (TSyntax k')] : Coe (TSyntaxArray k) (TSyntaxArray k') instance : Coe (TSyntaxArray k) (Array Syntax) where coe a := a.raw -instance : Coe (TSyntax identKind) (TSyntax `Lean.Parser.Command.declId) where +instance : Coe Ident (TSyntax `Lean.Parser.Command.declId) where coe id := mkNode _ #[id, mkNullNode #[]] -instance : Coe (Lean.TSyntax `term) (Lean.TSyntax `Lean.Parser.Term.funBinder) where +instance : Coe (Lean.Term) (Lean.TSyntax `Lean.Parser.Term.funBinder) where coe stx := ⟨stx⟩ end Lean.Syntax @@ -1072,7 +1089,7 @@ def expandInterpolatedStrChunks (chunks : Array Syntax) (mkAppend : Syntax → S return result open TSyntax.Compat in -def expandInterpolatedStr (interpStr : TSyntax interpolatedStrKind) (type : TSyntax `term) (toTypeFn : TSyntax `term) : MacroM (TSyntax `term) := do +def expandInterpolatedStr (interpStr : TSyntax interpolatedStrKind) (type : Term) (toTypeFn : Term) : MacroM Term := do let r ← expandInterpolatedStrChunks interpStr.raw.getArgs (fun a b => `($a ++ $b)) (fun a => `($toTypeFn $a)) `(($r : $type)) diff --git a/src/Init/NotationExtra.lean b/src/Init/NotationExtra.lean index 6bdcbcc6b2..6b978e8012 100644 --- a/src/Init/NotationExtra.lean +++ b/src/Init/NotationExtra.lean @@ -71,7 +71,7 @@ macro_rules let mut body ← `($t₁ = $t₂) for (c₁, c₂) in cs₁.zip cs₂ |>.reverse do body ← `($c₁ = $c₂ → $body) - let hint : TSyntax `ident ← `(hint) + let hint : Ident ← `(hint) `(@[$kind:attrKind unificationHint] def $(n.getD hint):ident $bs:bracketedBinder* : Sort _ := $body) end Lean @@ -182,7 +182,7 @@ macro_rules macro_rules | `(%[ $[$x],* | $k ]) => if x.size < 8 then - x.foldrM (β := TSyntax `term) (init := k) fun x k => + x.foldrM (β := Term) (init := k) fun x k => `(List.cons $x $k) else let m := x.size / 2 diff --git a/src/Lean/Elab/AuxDiscr.lean b/src/Lean/Elab/AuxDiscr.lean index e3c692cfb6..c07326fac3 100644 --- a/src/Lean/Elab/AuxDiscr.lean +++ b/src/Lean/Elab/AuxDiscr.lean @@ -10,14 +10,14 @@ namespace Lean Create an auxiliary identifier for storing non-atomic discriminants. This kind of free variable is cleared before elaborating a `match` alternative rhs. -/ -def mkAuxDiscr [Monad m] [MonadQuotation m] : m (TSyntax identKind) := +def mkAuxDiscr [Monad m] [MonadQuotation m] : m Ident := `(_discr) /-- Create an auxiliary identifier for expanding notation such as `fun (a, b) => ...`. This kind of free variable is cleared before elaborating a `match` alternative rhs. -/ -def mkAuxFunDiscr [Monad m] [MonadQuotation m] : m (TSyntax identKind) := +def mkAuxFunDiscr [Monad m] [MonadQuotation m] : m Ident := `(_fun_discr) /-- Return true iff `n` is an auxiliary variable created by `expandNonAtomicDiscrs?` -/ diff --git a/src/Lean/Elab/Binders.lean b/src/Lean/Elab/Binders.lean index a0eaec94f7..98a009eaab 100644 --- a/src/Lean/Elab/Binders.lean +++ b/src/Lean/Elab/Binders.lean @@ -245,7 +245,7 @@ in the literature. -/ Auxiliary functions for converting `id_1 ... id_n` application into `#[id_1, ..., id_m]` It is used at `expandFunBinders`. -/ private partial def getFunBinderIds? (stx : Syntax) : OptionT MacroM (Array Syntax) := - let convertElem (stx : TSyntax `term) : OptionT MacroM Syntax := + let convertElem (stx : Term) : OptionT MacroM Syntax := match stx with | `(_) => do let ident ← mkFreshIdent stx; pure ident | `($id:ident) => return id diff --git a/src/Lean/Elab/BuiltinNotation.lean b/src/Lean/Elab/BuiltinNotation.lean index a2919bd4fb..96717f897a 100644 --- a/src/Lean/Elab/BuiltinNotation.lean +++ b/src/Lean/Elab/BuiltinNotation.lean @@ -95,7 +95,7 @@ are turned into a new anonymous constructor application. For example, | _ => Macro.throwUnsupported open Lean.Parser in -private def elabParserMacroAux (prec e : TSyntax `term) (withAnonymousAntiquot : Bool) : TermElabM Syntax := do +private def elabParserMacroAux (prec e : Term) (withAnonymousAntiquot : Bool) : TermElabM Syntax := do let (some declName) ← getDeclName? | throwError "invalid `leading_parser` macro, it must be used in definitions" match extractMacroScopes declName with @@ -111,7 +111,7 @@ private def elabParserMacroAux (prec e : TSyntax `term) (withAnonymousAntiquot : elabParserMacroAux (prec?.getD (quote Parser.maxPrec)) e (anon?.all (·.raw.isOfKind ``Parser.Term.trueVal)) | _ => throwUnsupportedSyntax -private def elabTParserMacroAux (prec lhsPrec e : TSyntax `term) : TermElabM Syntax := do +private def elabTParserMacroAux (prec lhsPrec e : Term) : TermElabM Syntax := do let declName? ← getDeclName? match declName? with | some declName => let kind := quote declName; ``(Lean.Parser.trailingNode $kind $prec $lhsPrec $e) @@ -168,8 +168,8 @@ interpolated string literal) to stderr. It should only be used for debugging. -/ withMacroExpansion stx stxNew <| elabTerm stxNew expectedType? /-- Return syntax `Prod.mk elems[0] (Prod.mk elems[1] ... (Prod.mk elems[elems.size - 2] elems[elems.size - 1])))` -/ -partial def mkPairs (elems : Array (TSyntax `term)) : MacroM (TSyntax `term) := - let rec loop (i : Nat) (acc : TSyntax `term) := do +partial def mkPairs (elems : Array Term) : MacroM Term := + let rec loop (i : Nat) (acc : Term) := do if i > 0 then let i := i - 1 let elem := elems[i] @@ -192,7 +192,7 @@ private partial def hasCDot : Syntax → Bool Examples: - `· + 1` => `fun _a_1 => _a_1 + 1` - `f · · b` => `fun _a_1 _a_2 => f _a_1 _a_2 b` -/ -partial def expandCDot? (stx : TSyntax `term) : MacroM (Option (TSyntax `term)) := do +partial def expandCDot? (stx : Term) : MacroM (Option Term) := do if hasCDot stx then let (newStx, binders) ← (go stx).run #[] `(fun $binders* => $(⟨newStx⟩)) @@ -204,10 +204,10 @@ where The extra state `Array Syntax` contains the new binder names. If `stx` is a `·`, we create a fresh identifier, store in the extra state, and return it. Otherwise, we just return `stx`. -/ - go : Syntax → StateT (Array (TSyntax identKind)) MacroM Syntax + go : Syntax → StateT (Array Ident) MacroM Syntax | stx@`(($(_))) => pure stx | stx@`(·) => withFreshMacroScope do - let id : TSyntax `ident ← `(a) + let id : Ident ← `(a) modify fun s => s.push id pure id | stx => match stx with @@ -220,7 +220,7 @@ where Helper method for elaborating terms such as `(.+.)` where a constant name is expected. This method is usually used to implement tactics that function names as arguments (e.g., `simp`). -/ -def elabCDotFunctionAlias? (stx : TSyntax `term) : TermElabM (Option Expr) := do +def elabCDotFunctionAlias? (stx : Term) : TermElabM (Option Expr) := do let some stx ← liftMacroM <| expandCDotArg? stx | pure none let stx ← liftMacroM <| expandMacros stx match stx with @@ -236,7 +236,7 @@ def elabCDotFunctionAlias? (stx : TSyntax `term) : TermElabM (Option Expr) := do return none | _ => return none where - expandCDotArg? (stx : TSyntax `term) : MacroM (Option (TSyntax `term)) := + expandCDotArg? (stx : Term) : MacroM (Option Term) := match stx with | `(($e)) => Term.expandCDot? e | _ => Term.expandCDot? stx @@ -286,7 +286,7 @@ private def isSubstCandidate (lhs rhs : Expr) : MetaM Bool := Given an expression `e` that is the elaboration of `stx`, if `e` is a free variable, then return `k stx`. Otherwise, return `(fun x => k x) e` -/ -private def withLocalIdentFor (stx : TSyntax `term) (e : Expr) (k : TSyntax `term → TermElabM Expr) : TermElabM Expr := do +private def withLocalIdentFor (stx : Term) (e : Expr) (k : Term → TermElabM Expr) : TermElabM Expr := do if e.isFVar then k stx else diff --git a/src/Lean/Elab/Deriving/BEq.lean b/src/Lean/Elab/Deriving/BEq.lean index 1ce8a83caa..91d896570f 100644 --- a/src/Lean/Elab/Deriving/BEq.lean +++ b/src/Lean/Elab/Deriving/BEq.lean @@ -14,7 +14,7 @@ open Meta def mkBEqHeader (indVal : InductiveVal) : TermElabM Header := do mkHeader `BEq 2 indVal -def mkMatch (header : Header) (indVal : InductiveVal) (auxFunName : Name) : TermElabM (TSyntax `term) := do +def mkMatch (header : Header) (indVal : InductiveVal) (auxFunName : Name) : TermElabM Term := do let discrs ← mkDiscrs header indVal let alts ← mkAlts `(match $[$discrs],* with $alts:matchAlt*) @@ -68,7 +68,7 @@ where alts := alts.push (← mkElseAlt) return alts -def mkAuxFunction (ctx : Context) (i : Nat) : TermElabM (TSyntax `command) := do +def mkAuxFunction (ctx : Context) (i : Nat) : TermElabM Command := do let auxFunName := ctx.auxFunNames[i] let indVal := ctx.typeInfos[i] let header ← mkBEqHeader indVal diff --git a/src/Lean/Elab/Deriving/DecEq.lean b/src/Lean/Elab/Deriving/DecEq.lean index bcaf9add29..4820dc89d4 100644 --- a/src/Lean/Elab/Deriving/DecEq.lean +++ b/src/Lean/Elab/Deriving/DecEq.lean @@ -15,12 +15,12 @@ open Meta def mkDecEqHeader (indVal : InductiveVal) : TermElabM Header := do mkHeader `DecidableEq 2 indVal -def mkMatch (header : Header) (indVal : InductiveVal) (auxFunName : Name) : TermElabM (TSyntax `term) := do +def mkMatch (header : Header) (indVal : InductiveVal) (auxFunName : Name) : TermElabM Term := do let discrs ← mkDiscrs header indVal let alts ← mkAlts `(match $[$discrs],* with $alts:matchAlt*) where - mkSameCtorRhs : List (TSyntax identKind × TSyntax identKind × Bool × Bool) → TermElabM (TSyntax `term) + mkSameCtorRhs : List (Ident × Ident × Bool × Bool) → TermElabM Term | [] => ``(isTrue rfl) | (a, b, recField, isProof) :: todo => withFreshMacroScope do let rhs ← if isProof then diff --git a/src/Lean/Elab/Deriving/FromToJson.lean b/src/Lean/Elab/Deriving/FromToJson.lean index fb7b2ffa0c..b4f63dcbdd 100644 --- a/src/Lean/Elab/Deriving/FromToJson.lean +++ b/src/Lean/Elab/Deriving/FromToJson.lean @@ -14,7 +14,7 @@ open Lean.Json open Lean.Parser.Term open Lean.Meta -def mkJsonField (n : Name) : Bool × TSyntax `term := +def mkJsonField (n : Name) : Bool × Term := let s := n.toString let s₁ := s.dropRightWhile (· == '?') (s != s₁, Syntax.mkStrLit s₁) @@ -42,7 +42,7 @@ def mkToJsonInstanceHandler (declNames : Array Name) : CommandElabM Bool := do let toJsonFuncId := mkIdent ctx.auxFunNames[0] -- Return syntax to JSONify `id`, either via `ToJson` or recursively -- if `id`'s type is the type we're deriving for. - let mkToJson (id : TSyntax identKind) (type : Expr) : TermElabM (TSyntax `term) := do + let mkToJson (id : Ident) (type : Expr) : TermElabM Term := do if type.isAppOf indVal.name then `($toJsonFuncId:ident $id:ident) else ``(toJson $id:ident) let header ← mkHeader ``ToJson 1 ctx.typeInfos[0] @@ -74,7 +74,7 @@ def mkToJsonInstanceHandler (declNames : Array Name) : CommandElabM Bool := do where mkAlts (indVal : InductiveVal) - (rhs : ConstructorVal → Array (TSyntax identKind × Expr) → Option (Array Name) → TermElabM (TSyntax `term)) : TermElabM (Array (TSyntax ``matchAlt)) := do + (rhs : ConstructorVal → Array (Ident × Expr) → Option (Array Name) → TermElabM Term) : TermElabM (Array (TSyntax ``matchAlt)) := do indVal.ctors.toArray.mapM fun ctor => do let ctorInfo ← getConstInfoCtor ctor forallTelescopeReducing ctorInfo.type fun xs _ => do @@ -145,7 +145,7 @@ def mkFromJsonInstanceHandler (declNames : Array Name) : CommandElabM Bool := do else return false where - mkAlts (indVal : InductiveVal) (fromJsonFuncId : TSyntax identKind) : TermElabM (Array (TSyntax `term)) := do + mkAlts (indVal : InductiveVal) (fromJsonFuncId : Ident) : TermElabM (Array Term) := do let alts ← indVal.ctors.toArray.mapM fun ctor => do let ctorInfo ← getConstInfoCtor ctor diff --git a/src/Lean/Elab/Deriving/Hashable.lean b/src/Lean/Elab/Deriving/Hashable.lean index e59c63842e..94fbe62fc3 100644 --- a/src/Lean/Elab/Deriving/Hashable.lean +++ b/src/Lean/Elab/Deriving/Hashable.lean @@ -15,7 +15,7 @@ open Meta def mkHashableHeader (indVal : InductiveVal) : TermElabM Header := do mkHeader `Hashable 1 indVal -def mkMatch (ctx : Context) (header : Header) (indVal : InductiveVal) : TermElabM (TSyntax `term) := do +def mkMatch (ctx : Context) (header : Header) (indVal : InductiveVal) : TermElabM Term := do let discrs ← mkDiscrs header indVal let alts ← mkAlts `(match $[$discrs],* with $alts:matchAlt*) @@ -54,7 +54,7 @@ where ctorIdx := ctorIdx + 1 return alts -def mkAuxFunction (ctx : Context) (i : Nat) : TermElabM (TSyntax `command) := do +def mkAuxFunction (ctx : Context) (i : Nat) : TermElabM Command := do let auxFunName := ctx.auxFunNames[i] let indVal := ctx.typeInfos[i] let header ← mkHashableHeader indVal diff --git a/src/Lean/Elab/Deriving/Ord.lean b/src/Lean/Elab/Deriving/Ord.lean index e205847705..5e092ea82a 100644 --- a/src/Lean/Elab/Deriving/Ord.lean +++ b/src/Lean/Elab/Deriving/Ord.lean @@ -14,7 +14,7 @@ open Meta def mkOrdHeader (indVal : InductiveVal) : TermElabM Header := do mkHeader `Ord 2 indVal -def mkMatch (header : Header) (indVal : InductiveVal) : TermElabM (TSyntax `term) := do +def mkMatch (header : Header) (indVal : InductiveVal) : TermElabM Term := do let discrs ← mkDiscrs header indVal let alts ← mkAlts `(match $[$discrs],* with $alts:matchAlt*) @@ -32,7 +32,7 @@ where let mut ctorArgs1 := #[] let mut ctorArgs2 := #[] -- construct RHS top-down as continuation over the remaining comparison - let mut rhsCont : TSyntax `term → TermElabM (TSyntax `term) := fun rhs => pure rhs + let mut rhsCont : Term → TermElabM Term := fun rhs => pure rhs -- add `_` for inductive parameters, they are inaccessible for _ in [:indVal.numParams] do ctorArgs1 := ctorArgs1.push (← `(_)) @@ -64,7 +64,7 @@ where alts := alts ++ (alt : Array (TSyntax ``matchAlt)) return alts.pop.pop -def mkAuxFunction (ctx : Context) (i : Nat) : TermElabM (TSyntax `command) := do +def mkAuxFunction (ctx : Context) (i : Nat) : TermElabM Command := do let auxFunName := ctx.auxFunNames[i] let indVal := ctx.typeInfos[i] let header ← mkOrdHeader indVal diff --git a/src/Lean/Elab/Deriving/Repr.lean b/src/Lean/Elab/Deriving/Repr.lean index 837817add5..105f4a82a2 100644 --- a/src/Lean/Elab/Deriving/Repr.lean +++ b/src/Lean/Elab/Deriving/Repr.lean @@ -19,7 +19,7 @@ def mkReprHeader (indVal : InductiveVal) : TermElabM Header := do binders := header.binders.push (← `(bracketedBinder| (prec : Nat))) } -def mkBodyForStruct (header : Header) (indVal : InductiveVal) : TermElabM (TSyntax `term) := do +def mkBodyForStruct (header : Header) (indVal : InductiveVal) : TermElabM Term := do let ctorVal ← getConstInfoCtor indVal.ctors.head! let fieldNames := getStructureFields (← getEnv) indVal.name let numParams := indVal.numParams @@ -43,7 +43,7 @@ def mkBodyForStruct (header : Header) (indVal : InductiveVal) : TermElabM (TSynt fields ← `($fields ++ $fieldNameLit ++ " := " ++ repr ($target.$(mkIdent fieldName):ident)) `(Format.bracket "{ " $fields:term " }") -def mkBodyForInduct (header : Header) (indVal : InductiveVal) (auxFunName : Name) : TermElabM (TSyntax `term) := do +def mkBodyForInduct (header : Header) (indVal : InductiveVal) (auxFunName : Name) : TermElabM Term := do let discrs ← mkDiscrs header indVal let alts ← mkAlts `(match $[$discrs],* with $alts:matchAlt*) @@ -58,7 +58,7 @@ where for _ in [:indVal.numIndices] do patterns := patterns.push (← `(_)) let mut ctorArgs := #[] - let mut rhs : TSyntax `term := Syntax.mkStrLit (toString ctorInfo.name) + let mut rhs : Term := Syntax.mkStrLit (toString ctorInfo.name) rhs ← `(Format.text $rhs) -- add `_` for inductive parameters, they are inaccessible for _ in [:indVal.numParams] do @@ -78,13 +78,13 @@ where alts := alts.push alt return alts -def mkBody (header : Header) (indVal : InductiveVal) (auxFunName : Name) : TermElabM (TSyntax `term) := do +def mkBody (header : Header) (indVal : InductiveVal) (auxFunName : Name) : TermElabM Term := do if isStructure (← getEnv) indVal.name then mkBodyForStruct header indVal else mkBodyForInduct header indVal auxFunName -def mkAuxFunction (ctx : Context) (i : Nat) : TermElabM (TSyntax `command) := do +def mkAuxFunction (ctx : Context) (i : Nat) : TermElabM Command := do let auxFunName := ctx.auxFunNames[i] let indVal := ctx.typeInfos[i] let header ← mkReprHeader indVal diff --git a/src/Lean/Elab/Deriving/Util.lean b/src/Lean/Elab/Deriving/Util.lean index 4c0bc7ea41..745d5acaf5 100644 --- a/src/Lean/Elab/Deriving/Util.lean +++ b/src/Lean/Elab/Deriving/Util.lean @@ -26,7 +26,7 @@ def mkInductArgNames (indVal : InductiveVal) : TermElabM (Array Name) := do pure argNames /-- Return the inductive declaration's type applied to the arguments in `argNames`. -/ -def mkInductiveApp (indVal : InductiveVal) (argNames : Array Name) : TermElabM (TSyntax `term) := +def mkInductiveApp (indVal : InductiveVal) (argNames : Array Name) : TermElabM Term := let f := mkIdent indVal.name let args := argNames.map mkIdent `(@$f $args*) @@ -101,12 +101,12 @@ def mkLocalInstanceLetDecls (ctx : Context) (className : Name) (argNames : Array letDecls := letDecls.push letDecl return letDecls -def mkLet (letDecls : Array (TSyntax ``Parser.Term.letDecl)) (body : TSyntax `term) : TermElabM (TSyntax `term) := +def mkLet (letDecls : Array (TSyntax ``Parser.Term.letDecl)) (body : Term) : TermElabM Term := letDecls.foldrM (init := body) fun letDecl body => `(let $letDecl:letDecl; $body) open TSyntax.Compat in -def mkInstanceCmds (ctx : Context) (className : Name) (typeNames : Array Name) (useAnonCtor := true) : TermElabM (Array (TSyntax `command)) := do +def mkInstanceCmds (ctx : Context) (className : Name) (typeNames : Array Name) (useAnonCtor := true) : TermElabM (Array Command) := do let mut instances := #[] for i in [:ctx.typeInfos.size] do let indVal := ctx.typeInfos[i] @@ -129,7 +129,7 @@ structure Header where binders : Array (TSyntax ``Parser.Term.bracketedBinder) argNames : Array Name targetNames : Array Name - targetType : TSyntax `term + targetType : Term open TSyntax.Compat in def mkHeader (className : Name) (arity : Nat) (indVal : InductiveVal) : TermElabM Header := do diff --git a/src/Lean/Elab/Do.lean b/src/Lean/Elab/Do.lean index 7104ddd2fe..367bac9a98 100644 --- a/src/Lean/Elab/Do.lean +++ b/src/Lean/Elab/Do.lean @@ -123,7 +123,7 @@ private partial def extractBind (expectedType? : Option Expr) : TermElabM Extrac namespace Do -abbrev Var := Syntax -- TODO: should be `TSyntax identKind` +abbrev Var := Syntax -- TODO: should be `Ident` /- A `doMatch` alternative. `vars` is the array of variables declared by `patterns`. -/ structure Alt (σ : Type) where diff --git a/src/Lean/Elab/ElabRules.lean b/src/Lean/Elab/ElabRules.lean index 561194dda4..2661a52960 100644 --- a/src/Lean/Elab/ElabRules.lean +++ b/src/Lean/Elab/ElabRules.lean @@ -17,7 +17,7 @@ def withExpectedType (expectedType? : Option Expr) (x : Expr → TermElabM Expr) | throwError "expected type must be known" x expectedType -def elabElabRulesAux (doc? : Option (TSyntax ``docComment)) (attrKind : TSyntax ``attrKind) (k : SyntaxNodeKind) (cat? expty? : Option (TSyntax `ident)) (alts : Array (TSyntax ``matchAlt)) : CommandElabM Syntax := do +def elabElabRulesAux (doc? : Option (TSyntax ``docComment)) (attrKind : TSyntax ``attrKind) (k : SyntaxNodeKind) (cat? expty? : Option (Ident)) (alts : Array (TSyntax ``matchAlt)) : CommandElabM Syntax := do let alts ← alts.mapM fun (alt : TSyntax ``matchAlt) => match alt with | `(matchAltExpr| | $pats,* => $rhs) => do let pat := pats.elemsAndSeps[0] diff --git a/src/Lean/Elab/MacroArgUtil.lean b/src/Lean/Elab/MacroArgUtil.lean index 32bad015e5..1596aa2b26 100644 --- a/src/Lean/Elab/MacroArgUtil.lean +++ b/src/Lean/Elab/MacroArgUtil.lean @@ -11,9 +11,9 @@ open Lean.Parser.Term hiding macroArg open Lean.Parser.Command /- Convert `macro` arg into a `syntax` command item and a pattern element -/ -partial def expandMacroArg (stx : TSyntax ``macroArg) : CommandElabM (TSyntax `stx × TSyntax `term) := do +partial def expandMacroArg (stx : TSyntax ``macroArg) : CommandElabM (TSyntax `stx × Term) := do let (id?, id, stx) ← match (← liftMacroM <| expandMacros stx) with - | `(macroArg| $id:ident:$stx) => pure (some id, (id : TSyntax `term), stx) + | `(macroArg| $id:ident:$stx) => pure (some id, (id : Term), stx) | `(macroArg| $stx:stx) => pure (none, (← `(x)), stx) | _ => throwUnsupportedSyntax mkSyntaxAndPat id? id stx @@ -40,9 +40,9 @@ where -- otherwise `group` the syntax to enforce arity 1, e.g. for `noWs` | none => return (← `(stx| group($stx)), (← mkAntiquotNode stx id)) pure (stx, pat) - mkSplicePat kind stx id suffix : CommandElabM (TSyntax `term) := + mkSplicePat kind stx id suffix : CommandElabM Term := return ⟨mkNullNode #[mkAntiquotSuffixSpliceNode kind (← mkAntiquotNode stx id) suffix]⟩ - mkAntiquotNode : TSyntax `stx → TSyntax `term → CommandElabM (TSyntax `term) + mkAntiquotNode : TSyntax `stx → Term → CommandElabM Term | `(stx| ($stx)), term => mkAntiquotNode stx term | `(stx| $id:ident$[:$p:prec]?), term => do let kind ← match (← Elab.Term.resolveParserName id) with diff --git a/src/Lean/Elab/Match.lean b/src/Lean/Elab/Match.lean index 02f52438ac..5e3fb8c211 100644 --- a/src/Lean/Elab/Match.lean +++ b/src/Lean/Elab/Match.lean @@ -19,7 +19,7 @@ namespace Lean.Elab.Term open Meta open Lean.Parser.Term -private def expandSimpleMatch (stx : Syntax) (discr : TSyntax `term) (lhsVar : TSyntax identKind) (rhs : TSyntax `term) (expectedType? : Option Expr) : TermElabM Expr := do +private def expandSimpleMatch (stx : Syntax) (discr : Term) (lhsVar : Ident) (rhs : Term) (expectedType? : Option Expr) : TermElabM Expr := do let newStx ← `(let $lhsVar := $discr; $rhs) withMacroExpansion stx newStx <| elabTerm newStx expectedType? diff --git a/src/Lean/Elab/Notation.lean b/src/Lean/Elab/Notation.lean index 824efad405..2bd12f9b4c 100644 --- a/src/Lean/Elab/Notation.lean +++ b/src/Lean/Elab/Notation.lean @@ -71,7 +71,7 @@ partial def hasDuplicateAntiquot (stxs : Array Syntax) : Bool := Id.run do The notation must be of the form `notation ... => c body` where `c` is a declaration in the current scope and `body` any syntax that contains each variable from the LHS at most once. -/ -def mkSimpleDelab (attrKind : TSyntax ``attrKind) (pat qrhs : TSyntax `term) : OptionT MacroM Syntax := do +def mkSimpleDelab (attrKind : TSyntax ``attrKind) (pat qrhs : Term) : OptionT MacroM Syntax := do let (c, args) ← match qrhs with | `($c:ident $args*) => pure (c, args) | `($c:ident) => pure (c, #[]) @@ -105,7 +105,7 @@ private def isLocalAttrKind (attrKind : Syntax) : Bool := | _ => false private def expandNotationAux (ref : Syntax) - (currNamespace : Name) (attrKind : TSyntax ``attrKind) (prec? : Option (TSyntax `prec)) (name? : Option (TSyntax identKind)) (prio? : Option (TSyntax `prio)) (items : Array (TSyntax ``notationItem)) (rhs : TSyntax `term) : MacroM Syntax := do + (currNamespace : Name) (attrKind : TSyntax ``attrKind) (prec? : Option Prec) (name? : Option Ident) (prio? : Option Prio) (items : Array (TSyntax ``notationItem)) (rhs : Term) : MacroM Syntax := do let prio ← evalOptPrio prio? -- build parser let syntaxParts ← items.mapM expandNotationItemIntoSyntaxItem @@ -122,7 +122,7 @@ private def expandNotationAux (ref : Syntax) /- The command `syntax [] ...` adds the current namespace to the syntax node kind. So, we must include current namespace when we create a pattern for the following `macro_rules` commands. -/ let fullName := currNamespace ++ name - let pat : TSyntax `term := ⟨mkNode fullName patArgs⟩ + let pat : Term := ⟨mkNode fullName patArgs⟩ let stxDecl ← `($attrKind:attrKind syntax $[: $prec?]? (name := $(mkIdent name)) (priority := $(quote prio):num) $[$syntaxParts]* : $cat) let macroDecl ← `(macro_rules | `($pat) => ``($qrhs)) let macroDecls ← diff --git a/src/Lean/Elab/PatternVar.lean b/src/Lean/Elab/PatternVar.lean index b75019dcaf..08daafdb4a 100644 --- a/src/Lean/Elab/PatternVar.lean +++ b/src/Lean/Elab/PatternVar.lean @@ -11,7 +11,7 @@ namespace Lean.Elab.Term open Meta -abbrev PatternVar := Syntax -- TODO: should be `TSyntax identKind` +abbrev PatternVar := Syntax -- TODO: should be `Ident` /- Patterns define new local variables. @@ -60,7 +60,7 @@ An application in a pattern can be -/ structure Context where - funId : TSyntax identKind + funId : Ident ctorVal? : Option ConstructorVal -- It is `some`, if constructor application explicit : Bool ellipsis : Bool @@ -68,7 +68,7 @@ structure Context where paramDeclIdx : Nat := 0 namedArgs : Array NamedArg args : List Arg - newArgs : Array (TSyntax `term) := #[] + newArgs : Array Term := #[] deriving Inhabited private def isDone (ctx : Context) : Bool := @@ -109,7 +109,7 @@ private def processVar (idStx : Syntax) : M Syntax := do modify fun s => { s with vars := s.vars.push idStx, found := s.found.insert id } return idStx -private def nameToPattern : Name → TermElabM (TSyntax `term) +private def nameToPattern : Name → TermElabM Term | Name.anonymous => `(Name.anonymous) | Name.str p s _ => do let p ← nameToPattern p; `(Name.str $p $(quote s) _) | Name.num p n _ => do let p ← nameToPattern p; `(Name.num $p $(quote n) _) diff --git a/src/Lean/Elab/Quotation.lean b/src/Lean/Elab/Quotation.lean index 4fbc245122..55a2849d8f 100644 --- a/src/Lean/Elab/Quotation.lean +++ b/src/Lean/Elab/Quotation.lean @@ -70,13 +70,13 @@ def resolveSectionVariable (sectionVars : NameMap Name) (id : Name) : List (Name loop extractionResult.name [] /-- Transform sequence of pushes and appends into acceptable code -/ -def ArrayStxBuilder := Sum (Array (TSyntax `term)) (TSyntax `term) +def ArrayStxBuilder := Sum (Array Term) Term namespace ArrayStxBuilder def empty : ArrayStxBuilder := Sum.inl #[] -def build : ArrayStxBuilder → TSyntax `term +def build : ArrayStxBuilder → Term | Sum.inl elems => quote elems | Sum.inr arr => arr @@ -91,7 +91,7 @@ def append (b : ArrayStxBuilder) (arr : Syntax) (appendName := ``Array.append) : end ArrayStxBuilder -- Elaborate the content of a syntax quotation term -private partial def quoteSyntax : Syntax → TermElabM (TSyntax `term) +private partial def quoteSyntax : Syntax → TermElabM Term | Syntax.ident _ rawVal val preresolved => do if !hygiene.get (← getOptions) then return ← `(Syntax.ident info $(quote rawVal) $(quote val) $(quote preresolved)) @@ -237,7 +237,7 @@ elab_stx_quot Parser.Command.quot /- match -/ -- an "alternative" of patterns plus right-hand side -private abbrev Alt := List (TSyntax `term) × TSyntax `term +private abbrev Alt := List Term × Term /-- In a single match step, we match the first discriminant against the "head" of the first pattern of the first @@ -283,7 +283,7 @@ structure HeadInfo where -- compute compatibility of pattern with given head check onMatch (taken : HeadCheck) : MatchResult -- actually run the specified head check, with the discriminant bound to `discr` - doMatch (yes : (newDiscrs : List (TSyntax `term)) → TermElabM (TSyntax `term)) (no : TermElabM (TSyntax `term)) : TermElabM (TSyntax `term) + doMatch (yes : (newDiscrs : List Term) → TermElabM Term) (no : TermElabM Term) : TermElabM Term /-- Adapt alternatives that do not introduce new discriminants in `doMatch`, but are covered by those that do so. -/ private def noOpMatchAdaptPats : HeadCheck → Alt → Alt @@ -291,7 +291,7 @@ private def noOpMatchAdaptPats : HeadCheck → Alt → Alt | slice p s, (pats, rhs) => (List.replicate (p + 1 + s) (Unhygienic.run `(_)) ++ pats, rhs) | _, alt => alt -private def adaptRhs (fn : TSyntax `term → TermElabM (TSyntax `term)) : Alt → TermElabM Alt +private def adaptRhs (fn : Term → TermElabM Term) : Alt → TermElabM Alt | (pats, rhs) => return (pats, ← fn rhs) private partial def getHeadInfo (alt : Alt) : TermElabM HeadInfo := @@ -492,7 +492,7 @@ private def deduplicate (floatedLetDecls : Array Syntax) : Alt → TermElabM (Ar let rhs' ← `(rhs $vars*) pure (floatedLetDecls.push (← `(letDecl|rhs $vars:ident* := $rhs)), (pats, rhs')) -private partial def compileStxMatch (discrs : List (TSyntax `term)) (alts : List Alt) : TermElabM Syntax := do +private partial def compileStxMatch (discrs : List Term) (alts : List Alt) : TermElabM Syntax := do trace[Elab.match_syntax] "match {discrs} with {alts}" match discrs, alts with | [], ([], rhs)::_ => pure rhs -- nothing left to match diff --git a/src/Lean/Elab/Quotation/Util.lean b/src/Lean/Elab/Quotation/Util.lean index 0fff63b9f6..dd52fa4fe2 100644 --- a/src/Lean/Elab/Quotation/Util.lean +++ b/src/Lean/Elab/Quotation/Util.lean @@ -13,7 +13,7 @@ register_builtin_option hygiene : Bool := { descr := "Annotate identifiers in quotations such that they are resolved relative to the scope at their declaration, not that at their eventual use/expansion, to avoid accidental capturing. Note that quotations/notations already defined are unaffected." } -def getAntiquotationIds (stx : Syntax) : TermElabM (Array (TSyntax identKind)) := do +def getAntiquotationIds (stx : Syntax) : TermElabM (Array Ident) := do let mut ids := #[] for stx in stx.topDown (firstChoiceOnly := true) do if (isAntiquot stx || isTokenAntiquot stx) && !isEscapedAntiquot stx then diff --git a/src/Lean/Elab/Syntax.lean b/src/Lean/Elab/Syntax.lean index 0d89a16cbc..3d5a6acd40 100644 --- a/src/Lean/Elab/Syntax.lean +++ b/src/Lean/Elab/Syntax.lean @@ -17,7 +17,7 @@ def expandOptPrecedence (stx : Syntax) : MacroM (Option Nat) := else return some (← evalPrec stx[0][1]) -private def mkParserSeq (ds : Array (TSyntax `term)) : TermElabM Syntax := do +private def mkParserSeq (ds : Array Term) : TermElabM Syntax := do if ds.size == 0 then throwUnsupportedSyntax else if ds.size == 1 then @@ -83,12 +83,12 @@ open TSyntax.Compat in Given a `stx` of category `syntax`, return a pair `(newStx, lhsPrec?)`, where `newStx` is of category `term`. After elaboration, `newStx` should have type `TrailingParserDescr` if `lhsPrec?.isSome`, and `ParserDescr` otherwise. -/ -partial def toParserDescr (stx : Syntax) (catName : Name) : TermElabM (TSyntax `term × Option Nat) := do +partial def toParserDescr (stx : Syntax) (catName : Name) : TermElabM (Term × Option Nat) := do let env ← getEnv let behavior := Parser.leadingIdentBehavior env catName (process stx { catName := catName, first := true, leftRec := true, behavior := behavior }).run none where - process (stx : Syntax) : ToParserDescrM (TSyntax `term) := withRef stx do + process (stx : Syntax) : ToParserDescrM Term := withRef stx do let kind := stx.getKind if kind == nullKind then processSeq stx @@ -352,7 +352,7 @@ def inferMacroRulesAltKind : TSyntax ``matchAlt → CommandElabM SyntaxNodeKind /-- Infer syntax kind `k` from first pattern, put alternatives of same kind into new `macro/elab_rules (kind := k)` via `mkCmd (some k)`, leave remaining alternatives (via `mkCmd none`) to be recursively expanded. -/ -def expandNoKindMacroRulesAux (alts : Array (TSyntax ``matchAlt)) (cmdName : String) (mkCmd : Option Name → Array (TSyntax ``matchAlt) → CommandElabM (TSyntax `command)) : CommandElabM (TSyntax `command) := do +def expandNoKindMacroRulesAux (alts : Array (TSyntax ``matchAlt)) (cmdName : String) (mkCmd : Option Name → Array (TSyntax ``matchAlt) → CommandElabM Command) : CommandElabM Command := do let mut k ← inferMacroRulesAltKind alts[0] if k.isStr && k.getString! == "antiquot" then k := k.getPrefix diff --git a/src/Lean/Elab/Tactic/Match.lean b/src/Lean/Elab/Tactic/Match.lean index de562adfb2..30ca7a03da 100644 --- a/src/Lean/Elab/Tactic/Match.lean +++ b/src/Lean/Elab/Tactic/Match.lean @@ -13,7 +13,7 @@ open Meta open TSyntax.Compat in open Parser.Tactic in -private def mkAuxiliaryMatchTerm (parentTag : Name) (matchTac : Syntax) : MacroM (TSyntax `term × Array Syntax) := do +private def mkAuxiliaryMatchTerm (parentTag : Name) (matchTac : Syntax) : MacroM (Term × Array Syntax) := do let matchAlts := matchTac[5] let alts := matchAlts[0].getArgs let mut newAlts := #[] diff --git a/src/Lean/Elab/Tactic/Simp.lean b/src/Lean/Elab/Tactic/Simp.lean index 2b6f109f25..830071a0f2 100644 --- a/src/Lean/Elab/Tactic/Simp.lean +++ b/src/Lean/Elab/Tactic/Simp.lean @@ -175,7 +175,7 @@ private def elabSimpArgs (stx : Syntax) (ctx : Simp.Context) (eraseLocal : Bool) throwUnsupportedSyntax return { ctx := { ctx with simpTheorems := thmsArray.set! 0 thms }, starArg } where - resolveSimpIdTheorem? (simpArgTerm : TSyntax `term) : TacticM ResolveSimpIdResult := do + resolveSimpIdTheorem? (simpArgTerm : Term) : TacticM ResolveSimpIdResult := do let resolveExt (n : Name) : TacticM ResolveSimpIdResult := do if let some ext ← getSimpExtension? n then return .ext ext diff --git a/src/Lean/PrettyPrinter.lean b/src/Lean/PrettyPrinter.lean index 09d0920e69..e31f729b8b 100644 --- a/src/Lean/PrettyPrinter.lean +++ b/src/Lean/PrettyPrinter.lean @@ -25,7 +25,7 @@ def ppTerm (stx : Syntax) : CoreM Format := do let stx := (sanitizeSyntax stx).run' { options := opts } parenthesizeTerm stx >>= formatTerm -def ppUsing (e : Expr) (delab : Expr → MetaM (TSyntax `term)) : MetaM Format := do +def ppUsing (e : Expr) (delab : Expr → MetaM Term) : MetaM Format := do let lctx := (← getLCtx).sanitizeNames.run' { options := (← getOptions) } Meta.withLCtx lctx #[] do ppTerm (← delab e) diff --git a/src/Lean/PrettyPrinter/Delaborator/Basic.lean b/src/Lean/PrettyPrinter/Delaborator/Basic.lean index 4147bfb095..8c46b15c46 100644 --- a/src/Lean/PrettyPrinter/Delaborator/Basic.lean +++ b/src/Lean/PrettyPrinter/Delaborator/Basic.lean @@ -61,7 +61,7 @@ structure State where builtin_initialize delabFailureId : InternalExceptionId ← registerInternalExceptionId `delabFailure abbrev DelabM := ReaderT Context (StateRefT State MetaM) -abbrev Delab := DelabM (TSyntax `term) +abbrev Delab := DelabM Term instance : Inhabited (DelabM α) where default := throw default @@ -166,10 +166,10 @@ def withOptionAtCurrPos (k : Name) (v : DataValue) (x : DelabM α) : DelabM α : { ctx with optionsPerPos := ctx.optionsPerPos.insert pos opts' }) x -def annotatePos (pos : Pos) (stx : TSyntax `term) : TSyntax `term := +def annotatePos (pos : Pos) (stx : Term) : Term := ⟨stx.raw.setInfo (SourceInfo.synthetic ⟨pos⟩ ⟨pos⟩)⟩ -def annotateCurPos (stx : TSyntax `term) : Delab := +def annotateCurPos (stx : Term) : Delab := return annotatePos (← getPos) stx def getUnusedName (suggestion : Name) (body : Expr) : DelabM Name := do @@ -274,7 +274,7 @@ end Delaborator open SubExpr (Pos) open Delaborator (OptionsPerPos topDownAnalyze) -def delabCore (e : Expr) (optionsPerPos : OptionsPerPos := {}) (delab := Delaborator.delab) : MetaM (TSyntax `term × Std.RBMap Pos Elab.Info compare) := do +def delabCore (e : Expr) (optionsPerPos : OptionsPerPos := {}) (delab := Delaborator.delab) : MetaM (Term × Std.RBMap Pos Elab.Info compare) := do /- Using `erasePatternAnnotations` here is a bit hackish, but we do it `Expr.mdata` affects the delaborator. TODO: should we fix that? -/ let e ← Meta.erasePatternRefAnnotations e @@ -302,7 +302,7 @@ def delabCore (e : Expr) (optionsPerPos : OptionsPerPos := {}) (delab := Delabor return (stx, infos) /-- "Delaborate" the given term into surface-level syntax using the default and given subterm-specific options. -/ -def delab (e : Expr) (optionsPerPos : OptionsPerPos := {}) : MetaM (TSyntax `term) := do +def delab (e : Expr) (optionsPerPos : OptionsPerPos := {}) : MetaM Term := do let (stx, _) ← delabCore e optionsPerPos return stx diff --git a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean index c8cf6fc4f3..dc7c7e3c58 100644 --- a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean +++ b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean @@ -294,17 +294,17 @@ structure AppMatchState where info : MatcherInfo matcherTy : Expr params : Array Expr := #[] - motive : Option (TSyntax `term × Expr) := none + motive : Option (Term × Expr) := none motiveNamed : Bool := false - discrs : Array (TSyntax `term) := #[] + discrs : Array Term := #[] varNames : Array (Array Name) := #[] - rhss : Array (TSyntax `term) := #[] + rhss : Array Term := #[] -- additional arguments applied to the result of the `match` expression - moreArgs : Array (TSyntax `term) := #[] + moreArgs : Array Term := #[] /-- Extract arguments of motive applications from the matcher type. For the example below: `#[#[`([])], #[`(a::as)]]` -/ -private partial def delabPatterns (st : AppMatchState) : DelabM (Array (Array (TSyntax `term))) := +private partial def delabPatterns (st : AppMatchState) : DelabM (Array (Array Term)) := withReader (fun ctx => { ctx with inPattern := true, optionsPerPos := {} }) do let ty ← instantiateForall st.matcherTy st.params -- need to reduce `let`s that are lifted into the matcher type diff --git a/src/Lean/Server/Rpc/Deriving.lean b/src/Lean/Server/Rpc/Deriving.lean index ed0b8a9bf6..d4173b4d04 100644 --- a/src/Lean/Server/Rpc/Deriving.lean +++ b/src/Lean/Server/Rpc/Deriving.lean @@ -88,7 +88,7 @@ end def isOptField (n : Name) : Bool := n.toString.endsWith "?" -private def deriveStructureInstance (indVal : InductiveVal) (params : Array Expr) : TermElabM (TSyntax `command) := +private def deriveStructureInstance (indVal : InductiveVal) (params : Array Expr) : TermElabM Command := withFields indVal params fun fields => do trace[Elab.Deriving.RpcEncoding] "for structure {indVal.name} with params {params}" -- Postulate that every field have a rpc encoding, storing the encoding type ident @@ -96,9 +96,9 @@ private def deriveStructureInstance (indVal : InductiveVal) (params : Array Expr -- as otherwise typeclass synthesis fails. let mut binders := #[] let mut fieldIds := #[] - let mut fieldEncIds : Array (TSyntax `term) := #[] - let mut uniqFieldEncIds : Array (TSyntax identKind) := #[] - let mut fieldEncIds' : DiscrTree (TSyntax identKind) := {} + let mut fieldEncIds : Array Term := #[] + let mut uniqFieldEncIds : Array Ident := #[] + let mut fieldEncIds' : DiscrTree Ident := {} for (fieldName, fieldTp) in fields do let mut fieldTp := fieldTp if isOptField fieldName then @@ -108,7 +108,7 @@ private def deriveStructureInstance (indVal : InductiveVal) (params : Array Expr -- postulate that the field has an encoding and remember the encoding's binder name fieldIds := fieldIds.push <| mkIdent fieldName - let mut fieldEncId : TSyntax identKind := ⟨Syntax.missing⟩ + let mut fieldEncId : Ident := ⟨Syntax.missing⟩ match (← fieldEncIds'.getMatch fieldTp).back? with | none => fieldEncId ← mkIdent <$> mkFreshUserName fieldName @@ -167,7 +167,7 @@ private structure CtorState where deriving Inhabited private def matchF := Lean.Parser.Term.matchAlt (rhsParser := Lean.Parser.termParser) -private def deriveInductiveInstance (indVal : InductiveVal) (params : Array Expr) : TermElabM (TSyntax `command) := do +private def deriveInductiveInstance (indVal : InductiveVal) (params : Array Expr) : TermElabM Command := do trace[Elab.Deriving.RpcEncoding] "for inductive {indVal.name} with params {params}" -- produce all encoding types and binders for them @@ -214,7 +214,7 @@ private def deriveInductiveInstance (indVal : InductiveVal) (params : Array Expr -- create encoder and decoder match arms let nms ← argVars.mapM fun _ => mkIdent <$> mkFreshBinderName let mkPattern (src : Name) := Syntax.mkApp (mkIdent <| Name.mkStr src ctor.getString!) nms - let mkBody (tgt : Name) (func : Name) : TermElabM (TSyntax `term) := do + let mkBody (tgt : Name) (func : Name) : TermElabM Term := do let items ← nms.mapM fun nm => `(← $(mkIdent func) $nm) let tm := Syntax.mkApp (mkIdent <| Name.mkStr tgt ctor.getString!) items `(return $tm:term)