From a78302243c26395199ca2b71f33edebbba0883bf Mon Sep 17 00:00:00 2001 From: Sebastian Ullrich Date: Wed, 15 Jun 2022 15:26:07 +0200 Subject: [PATCH] refactor: strengthen `Syntax` signatures Most notable change: `Quote` is now parameterized by the target kind. Which means that `Name` etc. could actually have different implementations for quoting into `term` and `level`, if that need ever arises. --- src/Init/Meta.lean | 100 ++++++++++-------- src/Lean/Elab/AuxDiscr.lean | 5 +- src/Lean/Elab/Binders.lean | 2 +- src/Lean/Elab/BuiltinCommand.lean | 2 +- src/Lean/Elab/BuiltinNotation.lean | 16 +-- src/Lean/Elab/Command.lean | 4 +- src/Lean/Elab/Deriving/BEq.lean | 8 +- src/Lean/Elab/Deriving/Basic.lean | 6 +- src/Lean/Elab/Deriving/DecEq.lean | 6 +- src/Lean/Elab/Deriving/FromToJson.lean | 10 +- src/Lean/Elab/Deriving/Hashable.lean | 6 +- src/Lean/Elab/Deriving/Ord.lean | 8 +- src/Lean/Elab/Deriving/Repr.lean | 10 +- src/Lean/Elab/Deriving/Util.lean | 14 +-- src/Lean/Elab/ElabRules.lean | 5 +- src/Lean/Elab/MacroArgUtil.lean | 4 +- src/Lean/Elab/MacroRules.lean | 4 +- src/Lean/Elab/Match.lean | 2 +- src/Lean/Elab/Notation.lean | 4 +- src/Lean/Elab/PatternVar.lean | 6 +- src/Lean/Elab/Quotation.lean | 16 +-- src/Lean/Elab/Quotation/Util.lean | 2 +- src/Lean/Elab/Syntax.lean | 10 +- src/Lean/Elab/Tactic/Match.lean | 2 +- src/Lean/Elab/Tactic/Simp.lean | 2 +- src/Lean/Level.lean | 10 +- src/Lean/PrettyPrinter.lean | 2 +- src/Lean/PrettyPrinter/Delaborator/Basic.lean | 14 +-- .../PrettyPrinter/Delaborator/Builtins.lean | 10 +- src/Lean/Server/Rpc/Deriving.lean | 26 ++--- 30 files changed, 162 insertions(+), 154 deletions(-) diff --git a/src/Init/Meta.lean b/src/Init/Meta.lean index 6e09307597..99d8248c68 100644 --- a/src/Init/Meta.lean +++ b/src/Init/Meta.lean @@ -407,8 +407,8 @@ end Syntax | none => x | some ref => withRef ref x -@[inline] def mkNode (k : SyntaxNodeKind) (args : Array Syntax) : Syntax := - Syntax.node SourceInfo.none k args +@[inline] def mkNode (k : SyntaxNodeKind) (args : Array Syntax) : TSyntax k := + ⟨Syntax.node SourceInfo.none k args⟩ /- Syntax objects for a Lean module. -/ structure Module where @@ -430,30 +430,30 @@ 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) : Syntax := - Syntax.ident (SourceInfo.fromRef src) (toString val).toSubstring val [] +def mkIdentFrom (src : Syntax) (val : Name) : TSyntax identKind := + ⟨Syntax.ident (SourceInfo.fromRef src) (toString val).toSubstring val []⟩ -def mkIdentFromRef [Monad m] [MonadRef m] (val : Name) : m Syntax := do +def mkIdentFromRef [Monad m] [MonadRef m] (val : Name) : m (TSyntax identKind) := 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) : Syntax := +def mkCIdentFrom (src : Syntax) (c : Name) : TSyntax identKind := -- 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, [])] + ⟨Syntax.ident (SourceInfo.fromRef src) (toString id).toSubstring id [(c, [])]⟩ def mkCIdentFromRef [Monad m] [MonadRef m] (c : Name) : m Syntax := do return mkCIdentFrom (← getRef) c -def mkCIdent (c : Name) : Syntax := +def mkCIdent (c : Name) : TSyntax identKind := mkCIdentFrom Syntax.missing c @[export lean_mk_syntax_ident] -def mkIdent (val : Name) : Syntax := - Syntax.ident SourceInfo.none (toString val).toSubstring val [] +def mkIdent (val : Name) : TSyntax identKind := + ⟨Syntax.ident SourceInfo.none (toString val).toSubstring val []⟩ @[inline] def mkNullNode (args : Array Syntax := #[]) : Syntax := mkNode nullKind args @@ -499,27 +499,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 : Syntax) : (args : Array Syntax) → Syntax +def mkApp (fn : TSyntax `term) : (args : TSyntaxArray `term) → TSyntax `term | #[] => fn - | args => mkNode `Lean.Parser.Term.app #[fn, mkNullNode args] + | args => ⟨mkNode `Lean.Parser.Term.app #[fn, mkNullNode args.raw]⟩ -def mkCApp (fn : Name) (args : Array Syntax) : Syntax := +def mkCApp (fn : Name) (args : TSyntaxArray `term) : TSyntax `term := mkApp (mkCIdent fn) args -def mkLit (kind : SyntaxNodeKind) (val : String) (info := SourceInfo.none) : Syntax := +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) : Syntax := +def mkStrLit (val : String) (info := SourceInfo.none) : TSyntax strLitKind := mkLit strLitKind (String.quote val) info -def mkNumLit (val : String) (info := SourceInfo.none) : Syntax := +def mkNumLit (val : String) (info := SourceInfo.none) : TSyntax numLitKind := mkLit numLitKind val info -def mkScientificLit (val : String) (info := SourceInfo.none) : Syntax := +def mkScientificLit (val : String) (info := SourceInfo.none) : TSyntax scientificLitKind := mkLit scientificLitKind val info -def mkNameLit (val : String) (info := SourceInfo.none) : Syntax := +def mkNameLit (val : String) (info := SourceInfo.none) : TSyntax nameLitKind := mkLit nameLitKind val info /- Recall that we don't have special Syntax constructors for storing numeric and string atoms. @@ -840,15 +840,17 @@ end Compat end TSyntax /-- Reflect a runtime datum back to surface syntax (best-effort). -/ -class Quote (α : Type) where - quote : α → Syntax +class Quote (α : Type) (k : SyntaxNodeKind := `term) where + quote : α → TSyntax k export Quote (quote) -instance : Quote Syntax := ⟨id⟩ +instance [Quote α k] [CoeHTCT (TSyntax k) (TSyntax [k'])]: Quote α k' := ⟨fun a => quote (k := k) a⟩ + +instance : Quote (TSyntax `term) := ⟨id⟩ instance : Quote Bool := ⟨fun | true => mkCIdent `Bool.true | false => mkCIdent `Bool.false⟩ -instance : Quote String := ⟨Syntax.mkStrLit⟩ -instance : Quote Nat := ⟨fun n => Syntax.mkNumLit <| toString n⟩ +instance : Quote String strLitKind := ⟨Syntax.mkStrLit⟩ +instance : Quote Nat numLitKind := ⟨fun n => Syntax.mkNumLit <| toString n⟩ instance : Quote Substring := ⟨fun s => Syntax.mkCApp `String.toSubstring #[quote s.toString]⟩ -- in contrast to `Name.toString`, we can, and want to be, precise here @@ -859,43 +861,42 @@ private def getEscapedNameParts? (acc : List String) : Name → Option (List Str getEscapedNameParts? (s::acc) n | Name.num _ _ _ => none -private def quoteNameMk : Name → Syntax +def quoteNameMk : Name → TSyntax `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] -instance : Quote Name where +instance : Quote Name `term where quote n := match getEscapedNameParts? [] n with - | some ss => mkNode `Lean.Parser.Term.quotedName #[Syntax.mkNameLit ("`" ++ ".".intercalate ss)] - | none => quoteNameMk n + | some ss => ⟨mkNode `Lean.Parser.Term.quotedName #[Syntax.mkNameLit ("`" ++ ".".intercalate ss)]⟩ + | none => ⟨quoteNameMk n⟩ -instance {α β : Type} [Quote α] [Quote β] : Quote (α × β) where +instance [Quote α `term] [Quote β `term] : Quote (α × β) `term where quote | ⟨a, b⟩ => Syntax.mkCApp ``Prod.mk #[quote a, quote b] -private def quoteList {α : Type} [Quote α] : List α → Syntax +private def quoteList [Quote α `term] : List α → TSyntax `term | [] => mkCIdent ``List.nil | (x::xs) => Syntax.mkCApp ``List.cons #[quote x, quoteList xs] -instance {α : Type} [Quote α] : Quote (List α) where +instance [Quote α `term] : Quote (List α) `term where quote := quoteList -instance {α : Type} [Quote α] : Quote (Array α) where +instance [Quote α `term] : Quote (Array α) `term where quote xs := Syntax.mkCApp ``List.toArray #[quote xs.toList] -private def quoteOption {α : Type} [Quote α] : Option α → Syntax - | none => mkIdent ``none - | (some x) => Syntax.mkCApp ``some #[quote x] +instance Option.hasQuote {α : Type} [Quote α `term] : Quote (Option α) `term where + quote + | none => mkIdent ``none + | (some x) => Syntax.mkCApp ``some #[quote x] -instance Option.hasQuote {α : Type} [Quote α] : Quote (Option α) where - quote := quoteOption /- Evaluator for `prec` DSL -/ def evalPrec (stx : Syntax) : MacroM Nat := Macro.withIncRecDepth stx do let stx ← expandMacros stx match stx with - | `(prec| $num:num) => return num.isNatLit?.getD 0 + | `(prec| $num:num) => return num.getNat | _ => Macro.throwErrorAt stx "unexpected precedence" macro_rules @@ -904,14 +905,14 @@ macro_rules macro_rules | `(prec| $a - $b) => do `(prec| $(quote <| (← evalPrec a) - (← evalPrec b)):num) -macro "eval_prec " p:prec:max : term => return quote (← evalPrec p) +macro "eval_prec " p:prec:max : term => return quote (k := `term) (← evalPrec p) /- Evaluator for `prio` DSL -/ def evalPrio (stx : Syntax) : MacroM Nat := Macro.withIncRecDepth stx do let stx ← expandMacros stx match stx with - | `(prio| $num:num) => return num.isNatLit?.getD 0 + | `(prio| $num:num) => return num.getNat | _ => Macro.throwErrorAt stx "unexpected priority" macro_rules @@ -920,9 +921,9 @@ macro_rules macro_rules | `(prio| $a - $b) => do `(prio| $(quote <| (← evalPrio a) - (← evalPrio b)):num) -macro "eval_prio " p:prio:max : term => return quote (← evalPrio p) +macro "eval_prio " p:prio:max : term => return quote (k := `term) (← evalPrio p) -def evalOptPrio : Option Syntax → MacroM Nat +def evalOptPrio : Option (TSyntax `prio) → MacroM Nat | some prio => evalPrio prio | none => return 1000 -- TODO: FIX back eval_prio default @@ -1049,6 +1050,13 @@ partial def isInterpolatedStrLit? (stx : Syntax) : Option String := | none => none | some val => decodeInterpStrLit val +def getSepArgs (stx : Syntax) : Array Syntax := + stx.getArgs.getSepElems + +end Syntax + +namespace TSyntax + def expandInterpolatedStrChunks (chunks : Array Syntax) (mkAppend : Syntax → Syntax → MacroM Syntax) (mkElem : Syntax → MacroM Syntax) : MacroM Syntax := do let mut i := 0 let mut result := Syntax.missing @@ -1063,14 +1071,12 @@ def expandInterpolatedStrChunks (chunks : Array Syntax) (mkAppend : Syntax → S i := i+1 return result -def expandInterpolatedStr (interpStr : Syntax) (type : Syntax) (toTypeFn : Syntax) : MacroM Syntax := do - let r ← expandInterpolatedStrChunks interpStr.getArgs (fun a b => `($a ++ $b)) (fun a => `($toTypeFn $a)) +open TSyntax.Compat in +def expandInterpolatedStr (interpStr : TSyntax interpolatedStrKind) (type : TSyntax `term) (toTypeFn : TSyntax `term) : MacroM (TSyntax `term) := do + let r ← expandInterpolatedStrChunks interpStr.raw.getArgs (fun a b => `($a ++ $b)) (fun a => `($toTypeFn $a)) `(($r : $type)) -def getSepArgs (stx : Syntax) : Array Syntax := - stx.getArgs.getSepElems - -end Syntax +end TSyntax namespace Meta diff --git a/src/Lean/Elab/AuxDiscr.lean b/src/Lean/Elab/AuxDiscr.lean index 0e9e1051c2..e3c692cfb6 100644 --- a/src/Lean/Elab/AuxDiscr.lean +++ b/src/Lean/Elab/AuxDiscr.lean @@ -5,18 +5,19 @@ Authors: Leonardo de Moura -/ 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 Syntax := +def mkAuxDiscr [Monad m] [MonadQuotation m] : m (TSyntax identKind) := `(_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 Syntax := +def mkAuxFunDiscr [Monad m] [MonadQuotation m] : m (TSyntax identKind) := `(_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 f09d3834bb..8c2c36abae 100644 --- a/src/Lean/Elab/Binders.lean +++ b/src/Lean/Elab/Binders.lean @@ -244,7 +244,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 : Syntax) : OptionT MacroM Syntax := + let convertElem (stx : TSyntax `term) : OptionT MacroM Syntax := match stx with | `(_) => do let ident ← mkFreshIdent stx; pure ident | `($id:ident) => return id diff --git a/src/Lean/Elab/BuiltinCommand.lean b/src/Lean/Elab/BuiltinCommand.lean index acaea509d3..749e7f507e 100644 --- a/src/Lean/Elab/BuiltinCommand.lean +++ b/src/Lean/Elab/BuiltinCommand.lean @@ -172,7 +172,7 @@ private def matchBinderNames (ids : Array Syntax) (binderNames : Array Name) : C variable {α} -- trying to update part of the binder block defined above. ``` -/ -private def replaceBinderAnnotation (binder : Syntax) : CommandElabM Bool := do +private def replaceBinderAnnotation (binder : TSyntax ``Parser.Term.bracketedBinder) : CommandElabM Bool := do if let some (binderNames, explicit) := typelessBinder? binder then let varDecls := (← getScope).varDecls let mut varDeclsNew := #[] diff --git a/src/Lean/Elab/BuiltinNotation.lean b/src/Lean/Elab/BuiltinNotation.lean index dd33fde13e..b795e2813a 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 : Syntax) (e : Syntax) (withAnonymousAntiquot : Bool) : TermElabM Syntax := do +private def elabParserMacroAux (prec e : TSyntax `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 : Syntax) (e : Syntax) (withAnonymousAntiqu elabParserMacroAux (prec?.getD (quote Parser.maxPrec)) e (anon?.all (·.isOfKind ``Parser.Term.trueVal)) | _ => throwUnsupportedSyntax -private def elabTParserMacroAux (prec lhsPrec : Syntax) (e : Syntax) : TermElabM Syntax := do +private def elabTParserMacroAux (prec lhsPrec e : TSyntax `term) : TermElabM Syntax := do let declName? ← getDeclName? match declName? with | some declName => let kind := quote declName; ``(Lean.Parser.trailingNode $kind $prec $lhsPrec $e) @@ -169,8 +169,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 Syntax) : MacroM Syntax := - let rec loop (i : Nat) (acc : Syntax) := do +partial def mkPairs (elems : Array (TSyntax `term)) : MacroM (TSyntax `term) := + let rec loop (i : Nat) (acc : TSyntax `term) := do if i > 0 then let i := i - 1 let elem := elems[i] @@ -193,7 +193,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 : Syntax) : MacroM (Option Syntax) := do +partial def expandCDot? (stx : TSyntax `term) : MacroM (Option (TSyntax `term)) := do if hasCDot stx then let (newStx, binders) ← (go stx).run #[]; `(fun $binders* => $newStx) @@ -221,7 +221,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 : Syntax) : TermElabM (Option Expr) := do +def elabCDotFunctionAlias? (stx : TSyntax `term) : TermElabM (Option Expr) := do let some stx ← liftMacroM <| expandCDotArg? stx | pure none let stx ← liftMacroM <| expandMacros stx match stx with @@ -237,7 +237,7 @@ def elabCDotFunctionAlias? (stx : Syntax) : TermElabM (Option Expr) := do return none | _ => return none where - expandCDotArg? (stx : Syntax) : MacroM (Option Syntax) := + expandCDotArg? (stx : TSyntax `term) : MacroM (Option (TSyntax `term)) := match stx with | `(($e)) => Term.expandCDot? e | _ => Term.expandCDot? stx @@ -287,7 +287,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 : Syntax) (e : Expr) (k : Syntax → TermElabM Expr) : TermElabM Expr := do +private def withLocalIdentFor (stx : TSyntax `term) (e : Expr) (k : TSyntax `term → TermElabM Expr) : TermElabM Expr := do if e.isFVar then k stx else diff --git a/src/Lean/Elab/Command.lean b/src/Lean/Elab/Command.lean index 1befba23f8..65a29672e8 100644 --- a/src/Lean/Elab/Command.lean +++ b/src/Lean/Elab/Command.lean @@ -23,8 +23,8 @@ structure Scope where currNamespace : Name := Name.anonymous openDecls : List OpenDecl := [] levelNames : List Name := [] - /-- section variables as `bracketedBinder`s -/ - varDecls : Array Syntax := #[] + /-- section variables -/ + varDecls : Array (TSyntax ``Parser.Term.bracketedBinder) := #[] /-- Globally unique internal identifiers for the `varDecls` -/ varUIds : Array Name := #[] /-- noncomputable sections automatically add the `noncomputable` modifier to any declaration we cannot generate code for. -/ diff --git a/src/Lean/Elab/Deriving/BEq.lean b/src/Lean/Elab/Deriving/BEq.lean index 56c02dd72c..671b3911d9 100644 --- a/src/Lean/Elab/Deriving/BEq.lean +++ b/src/Lean/Elab/Deriving/BEq.lean @@ -14,12 +14,12 @@ open Meta def mkBEqHeader (indVal : InductiveVal) : TermElabM Header := do mkHeader `BEq 2 indVal -def mkMatch (header : Header) (indVal : InductiveVal) (auxFunName : Name) : TermElabM Syntax := do +def mkMatch (header : Header) (indVal : InductiveVal) (auxFunName : Name) : TermElabM (TSyntax `term) := do let discrs ← mkDiscrs header indVal let alts ← mkAlts `(match $[$discrs],* with $alts:matchAlt*) where - mkElseAlt : TermElabM Syntax := do + mkElseAlt : TermElabM (TSyntax ``matchAltExpr) := do let mut patterns := #[] -- add `_` pattern for indices for _ in [:indVal.numIndices] do @@ -29,7 +29,7 @@ where let altRhs ← `(false) `(matchAltExpr| | $[$patterns:term],* => $altRhs:term) - mkAlts : TermElabM (Array Syntax) := do + mkAlts : TermElabM (Array (TSyntax ``matchAlt)) := do let mut alts := #[] for ctorName in indVal.ctors do let ctorInfo ← getConstInfoCtor ctorName @@ -68,7 +68,7 @@ where alts := alts.push (← mkElseAlt) return alts -def mkAuxFunction (ctx : Context) (i : Nat) : TermElabM Syntax := do +def mkAuxFunction (ctx : Context) (i : Nat) : TermElabM (TSyntax `command) := do let auxFunName := ctx.auxFunNames[i] let indVal := ctx.typeInfos[i] let header ← mkBEqHeader indVal diff --git a/src/Lean/Elab/Deriving/Basic.lean b/src/Lean/Elab/Deriving/Basic.lean index 1522cc074f..4a72b66b28 100644 --- a/src/Lean/Elab/Deriving/Basic.lean +++ b/src/Lean/Elab/Deriving/Basic.lean @@ -9,7 +9,7 @@ import Lean.Elab.MutualDef namespace Lean.Elab open Command -def DerivingHandler := (typeNames : Array Name) → (args? : Option Syntax) → CommandElabM Bool +def DerivingHandler := (typeNames : Array Name) → (args? : Option (TSyntax ``Parser.Term.structInst)) → CommandElabM Bool def DerivingHandlerNoArgs := (typeNames : Array Name) → CommandElabM Bool builtin_initialize derivingHandlersRef : IO.Ref (NameMap DerivingHandler) ← IO.mkRef {} @@ -33,7 +33,7 @@ def registerBuiltinDerivingHandler (className : Name) (handler : DerivingHandler def defaultHandler (className : Name) (typeNames : Array Name) : CommandElabM Unit := do throwError "default handlers have not been implemented yet, class: '{className}' types: {typeNames}" -def applyDerivingHandlers (className : Name) (typeNames : Array Name) (args? : Option Syntax) : CommandElabM Unit := do +def applyDerivingHandlers (className : Name) (typeNames : Array Name) (args? : Option (TSyntax ``Parser.Term.structInst)) : CommandElabM Unit := do match (← derivingHandlersRef.get).find? className with | some handler => unless (← handler typeNames args?) do @@ -62,7 +62,7 @@ private def tryApplyDefHandler (className : Name) (declName : Name) : CommandEla structure DerivingClassView where ref : Syntax className : Name - args? : Option Syntax + args? : Option (TSyntax ``Parser.Term.structInst) def getOptDerivingClasses [Monad m] [MonadEnv m] [MonadResolveName m] [MonadError m] [MonadInfoTree m] (optDeriving : Syntax) : m (Array DerivingClassView) := do match optDeriving with diff --git a/src/Lean/Elab/Deriving/DecEq.lean b/src/Lean/Elab/Deriving/DecEq.lean index 6b232a2da7..af367aa527 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 Syntax := do +def mkMatch (header : Header) (indVal : InductiveVal) (auxFunName : Name) : TermElabM (TSyntax `term) := do let discrs ← mkDiscrs header indVal let alts ← mkAlts `(match $[$discrs],* with $alts:matchAlt*) where - mkSameCtorRhs : List (Syntax × Syntax × Bool × Bool) → TermElabM Syntax + mkSameCtorRhs : List (TSyntax identKind × TSyntax identKind × Bool × Bool) → TermElabM (TSyntax `term) | [] => ``(isTrue rfl) | (a, b, recField, isProof) :: todo => withFreshMacroScope do let rhs ← if isProof then @@ -36,7 +36,7 @@ where else return rhs - mkAlts : TermElabM (Array Syntax) := do + mkAlts : TermElabM (Array (TSyntax ``matchAlt)) := do let mut alts := #[] for ctorName₁ in indVal.ctors do let ctorInfo ← getConstInfoCtor ctorName₁ diff --git a/src/Lean/Elab/Deriving/FromToJson.lean b/src/Lean/Elab/Deriving/FromToJson.lean index 54497424bf..171c121ba5 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 × Syntax := +def mkJsonField (n : Name) : Bool × TSyntax `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 : Syntax) (type : Expr) : TermElabM Syntax := do + let mkToJson (id : TSyntax identKind) (type : Expr) : TermElabM (TSyntax `term) := do if type.isAppOf indVal.name then `($toJsonFuncId:ident $id:ident) else ``(toJson $id:ident) let header ← mkHeader ``ToJson 1 ctx.typeInfos[0] @@ -73,7 +73,7 @@ def mkToJsonInstanceHandler (declNames : Array Name) : CommandElabM Bool := do where mkAlts (indVal : InductiveVal) - (rhs : ConstructorVal → Array (Syntax × Expr) → (Option $ Array Name) → TermElabM Syntax) : TermElabM (Array Syntax) := do + (rhs : ConstructorVal → Array (TSyntax identKind × Expr) → Option (Array Name) → TermElabM (TSyntax `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 : Syntax) : TermElabM (Array Syntax) := do + mkAlts (indVal : InductiveVal) (fromJsonFuncId : TSyntax identKind) : TermElabM (Array (TSyntax `term)) := do let alts ← indVal.ctors.toArray.mapM fun ctor => do let ctorInfo ← getConstInfoCtor ctor @@ -162,7 +162,7 @@ where -- Return syntax to parse `id`, either via `FromJson` or recursively -- if `id`'s type is the type we're deriving for. - let mkFromJson (idx : Nat) (type : Expr) : TermElabM Syntax := + let mkFromJson (idx : Nat) (type : Expr) : TermElabM (TSyntax ``doExpr) := if type.isAppOf indVal.name then `(Lean.Parser.Term.doExpr| $fromJsonFuncId:ident jsons[$(quote idx)]) else `(Lean.Parser.Term.doExpr| fromJson? jsons[$(quote idx)]) let identNames := binders.map Prod.fst diff --git a/src/Lean/Elab/Deriving/Hashable.lean b/src/Lean/Elab/Deriving/Hashable.lean index 0c036e8684..3b24b03f56 100644 --- a/src/Lean/Elab/Deriving/Hashable.lean +++ b/src/Lean/Elab/Deriving/Hashable.lean @@ -15,13 +15,13 @@ open Meta def mkHashableHeader (indVal : InductiveVal) : TermElabM Header := do mkHeader `Hashable 1 indVal -def mkMatch (ctx : Context) (header : Header) (indVal : InductiveVal) : TermElabM Syntax := do +def mkMatch (ctx : Context) (header : Header) (indVal : InductiveVal) : TermElabM (TSyntax `term) := do let discrs ← mkDiscrs header indVal let alts ← mkAlts `(match $[$discrs],* with $alts:matchAlt*) where - mkAlts : TermElabM (Array Syntax) := do + mkAlts : TermElabM (Array (TSyntax ``matchAlt)) := do let mut alts := #[] let mut ctorIdx := 0 let allIndVals := indVal.all.toArray @@ -54,7 +54,7 @@ where ctorIdx := ctorIdx + 1 return alts -def mkAuxFunction (ctx : Context) (i : Nat) : TermElabM Syntax := do +def mkAuxFunction (ctx : Context) (i : Nat) : TermElabM (TSyntax `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 0e398468d9..315d254f57 100644 --- a/src/Lean/Elab/Deriving/Ord.lean +++ b/src/Lean/Elab/Deriving/Ord.lean @@ -14,12 +14,12 @@ open Meta def mkOrdHeader (indVal : InductiveVal) : TermElabM Header := do mkHeader `Ord 2 indVal -def mkMatch (header : Header) (indVal : InductiveVal) : TermElabM Syntax := do +def mkMatch (header : Header) (indVal : InductiveVal) : TermElabM (TSyntax `term) := do let discrs ← mkDiscrs header indVal let alts ← mkAlts `(match $[$discrs],* with $alts:matchAlt*) where - mkAlts : TermElabM (Array Syntax) := do + mkAlts : TermElabM (Array (TSyntax ``matchAlt)) := do let mut alts := #[] for ctorName in indVal.ctors do let ctorInfo ← getConstInfoCtor ctorName @@ -32,7 +32,7 @@ where let mut ctorArgs1 := #[] let mut ctorArgs2 := #[] -- construct RHS top-down as continuation over the remaining comparison - let mut rhsCont : Syntax → TermElabM Syntax := fun rhs => pure rhs + let mut rhsCont : TSyntax `term → TermElabM (TSyntax `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 return alts.pop.pop -def mkAuxFunction (ctx : Context) (i : Nat) : TermElabM Syntax := do +def mkAuxFunction (ctx : Context) (i : Nat) : TermElabM (TSyntax `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 f57ad1ea30..94dcb76c46 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 (← `(explicitBinderF| (prec : Nat))) } -def mkBodyForStruct (header : Header) (indVal : InductiveVal) : TermElabM Syntax := do +def mkBodyForStruct (header : Header) (indVal : InductiveVal) : TermElabM (TSyntax `term) := do let ctorVal ← getConstInfoCtor indVal.ctors.head! let fieldNames := getStructureFields (← getEnv) indVal.name let numParams := indVal.numParams @@ -43,12 +43,12 @@ def mkBodyForStruct (header : Header) (indVal : InductiveVal) : TermElabM Syntax fields ← `($fields ++ $fieldNameLit ++ " := " ++ repr ($target.$(mkIdent fieldName):ident)) `(Format.bracket "{ " $fields:term " }") -def mkBodyForInduct (header : Header) (indVal : InductiveVal) (auxFunName : Name) : TermElabM Syntax := do +def mkBodyForInduct (header : Header) (indVal : InductiveVal) (auxFunName : Name) : TermElabM (TSyntax `term) := do let discrs ← mkDiscrs header indVal let alts ← mkAlts `(match $[$discrs],* with $alts:matchAlt*) where - mkAlts : TermElabM (Array Syntax) := do + mkAlts : TermElabM (Array (TSyntax ``matchAlt)) := do let mut alts := #[] for ctorName in indVal.ctors do let ctorInfo ← getConstInfoCtor ctorName @@ -78,13 +78,13 @@ where alts := alts.push alt return alts -def mkBody (header : Header) (indVal : InductiveVal) (auxFunName : Name) : TermElabM Syntax := do +def mkBody (header : Header) (indVal : InductiveVal) (auxFunName : Name) : TermElabM (TSyntax `term) := do if isStructure (← getEnv) indVal.name then mkBodyForStruct header indVal else mkBodyForInduct header indVal auxFunName -def mkAuxFunction (ctx : Context) (i : Nat) : TermElabM Syntax := do +def mkAuxFunction (ctx : Context) (i : Nat) : TermElabM (TSyntax `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 d37d312e8d..c1fa845b34 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 Syntax := +def mkInductiveApp (indVal : InductiveVal) (argNames : Array Name) : TermElabM (TSyntax `term) := let f := mkIdent indVal.name let args := argNames.map mkIdent `(@$f $args*) @@ -82,7 +82,7 @@ def mkContext (fnPrefix : String) (typeName : Name) : TermElabM Context := do usePartial := usePartial } -def mkLocalInstanceLetDecls (ctx : Context) (className : Name) (argNames : Array Name) : TermElabM (Array Syntax) := do +def mkLocalInstanceLetDecls (ctx : Context) (className : Name) (argNames : Array Name) : TermElabM (Array (TSyntax ``Parser.Term.letDecl)) := do let mut letDecls := #[] for i in [:ctx.typeInfos.size] do let indVal := ctx.typeInfos[i] @@ -100,7 +100,7 @@ def mkLocalInstanceLetDecls (ctx : Context) (className : Name) (argNames : Array letDecls := letDecls.push letDecl return letDecls -def mkLet (letDecls : Array Syntax) (body : Syntax) : TermElabM Syntax := +def mkLet (letDecls : Array (TSyntax ``Parser.Term.letDecl)) (body : TSyntax `term) : TermElabM (TSyntax `term) := letDecls.foldrM (init := body) fun letDecl body => `(let $letDecl:letDecl; $body) @@ -120,14 +120,14 @@ def mkInstanceCmds (ctx : Context) (className : Name) (typeNames : Array Name) ( instances := instances.push instCmd return instances -def mkDiscr (varName : Name) : TermElabM Syntax := +def mkDiscr (varName : Name) : TermElabM (TSyntax ``Parser.Term.matchDiscr) := `(Parser.Term.matchDiscr| $(mkIdent varName):term) structure Header where - binders : Array Syntax + binders : Array (TSyntax ``Parser.Term.bracketedBinder) argNames : Array Name targetNames : Array Name - targetType : Syntax + targetType : TSyntax `term def mkHeader (className : Name) (arity : Nat) (indVal : InductiveVal) : TermElabM Header := do let argNames ← mkInductArgNames indVal @@ -145,7 +145,7 @@ def mkHeader (className : Name) (arity : Nat) (indVal : InductiveVal) : TermElab targetType := targetType } -def mkDiscrs (header : Header) (indVal : InductiveVal) : TermElabM (Array Syntax) := do +def mkDiscrs (header : Header) (indVal : InductiveVal) : TermElabM (Array (TSyntax ``Parser.Term.matchDiscr)) := do let mut discrs := #[] -- add indices for argName in header.argNames[indVal.numParams:] do diff --git a/src/Lean/Elab/ElabRules.lean b/src/Lean/Elab/ElabRules.lean index 07062ac698..e7fd47d426 100644 --- a/src/Lean/Elab/ElabRules.lean +++ b/src/Lean/Elab/ElabRules.lean @@ -9,6 +9,7 @@ import Lean.Elab.AuxDef namespace Lean.Elab.Command open Lean.Syntax open Lean.Parser.Term hiding macroArg +open Lean.Parser.Command def withExpectedType (expectedType? : Option Expr) (x : Expr → TermElabM Expr) : TermElabM Expr := do Term.tryPostponeIfNoneOrMVar expectedType? @@ -16,8 +17,8 @@ def withExpectedType (expectedType? : Option Expr) (x : Expr → TermElabM Expr) | throwError "expected type must be known" x expectedType -def elabElabRulesAux (doc? : Option Syntax) (attrKind : Syntax) (k : SyntaxNodeKind) (cat? expty? : Option Syntax) (alts : Array Syntax) : CommandElabM Syntax := do - let alts ← alts.mapM fun alt => match alt with +def elabElabRulesAux (doc? : Option (TSyntax ``docComment)) (attrKind : TSyntax ``attrKind) (k : SyntaxNodeKind) (cat? expty? : Option (TSyntax `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] if !pat.isQuot then diff --git a/src/Lean/Elab/MacroArgUtil.lean b/src/Lean/Elab/MacroArgUtil.lean index b8aae5dfa0..76c37e5d74 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 : Syntax) : CommandElabM (Syntax × Syntax) := do +partial def expandMacroArg (stx : TSyntax ``macroArg) : CommandElabM (TSyntax `stx × TSyntax `term) := do let (id?, id, stx) ← match (← liftMacroM <| expandMacros stx) with - | `(macroArg| $id:ident:$stx) => pure (some id, id, stx) + | `(macroArg| $id:ident:$stx) => pure (some id, (id : TSyntax `term), stx) | `(macroArg| $stx:stx) => pure (none, (← `(x)), stx) | _ => throwUnsupportedSyntax mkSyntaxAndPat id? id stx diff --git a/src/Lean/Elab/MacroRules.lean b/src/Lean/Elab/MacroRules.lean index a6f047deba..8478fc7fb4 100644 --- a/src/Lean/Elab/MacroRules.lean +++ b/src/Lean/Elab/MacroRules.lean @@ -15,8 +15,8 @@ open Lean.Parser.Command Remark: `k` is the user provided kind with the current namespace included. Recall that syntax node kinds contain the current namespace. -/ -def elabMacroRulesAux (doc? : Option Syntax) (attrKind tk : Syntax) (k : SyntaxNodeKind) (alts : Array Syntax) : CommandElabM Syntax := do - let alts ← alts.mapM fun alt => match alt with +def elabMacroRulesAux (doc? : Option (TSyntax ``docComment)) (attrKind : TSyntax ``attrKind) (tk : Syntax) (k : SyntaxNodeKind) (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] if !pat.isQuot then diff --git a/src/Lean/Elab/Match.lean b/src/Lean/Elab/Match.lean index 579cca517c..65031a1bd0 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 discr lhsVar rhs : Syntax) (expectedType? : Option Expr) : TermElabM Expr := do +private def expandSimpleMatch (stx : Syntax) (discr : TSyntax `term) (lhsVar : TSyntax identKind) (rhs : TSyntax `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 c4c517427f..5f03ddde91 100644 --- a/src/Lean/Elab/Notation.lean +++ b/src/Lean/Elab/Notation.lean @@ -75,7 +75,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 : Syntax) (pat qrhs : Syntax) : OptionT MacroM Syntax := do +def mkSimpleDelab (attrKind : TSyntax ``attrKind) (pat qrhs : TSyntax `term) : OptionT MacroM Syntax := do match qrhs with | `($c:ident $args*) => let [(c, [])] ← Macro.resolveGlobalName c.getId | failure @@ -113,7 +113,7 @@ private def isLocalAttrKind (attrKind : Syntax) : Bool := | _ => false private def expandNotationAux (ref : Syntax) - (currNamespace : Name) (attrKind : Syntax) (prec? : Option Syntax) (name? : Option Syntax) (prio? : Option Syntax) (items : Array Syntax) (rhs : Syntax) : MacroM Syntax := do + (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 let prio ← evalOptPrio prio? -- build parser let syntaxParts ← items.mapM expandNotationItemIntoSyntaxItem diff --git a/src/Lean/Elab/PatternVar.lean b/src/Lean/Elab/PatternVar.lean index a5e399037e..8fe6c6d5d5 100644 --- a/src/Lean/Elab/PatternVar.lean +++ b/src/Lean/Elab/PatternVar.lean @@ -60,7 +60,7 @@ An application in a pattern can be -/ structure Context where - funId : Syntax + funId : TSyntax identKind 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 Syntax := #[] + newArgs : Array (TSyntax `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 Syntax +private def nameToPattern : Name → TermElabM (TSyntax `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 d6994d609c..9538c54a5a 100644 --- a/src/Lean/Elab/Quotation.lean +++ b/src/Lean/Elab/Quotation.lean @@ -69,13 +69,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 Syntax) Syntax +def ArrayStxBuilder := Sum (Array (TSyntax `term)) (TSyntax `term) namespace ArrayStxBuilder def empty : ArrayStxBuilder := Sum.inl #[] -def build : ArrayStxBuilder → Syntax +def build : ArrayStxBuilder → TSyntax `term | Sum.inl elems => quote elems | Sum.inr arr => arr @@ -90,8 +90,8 @@ 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 Syntax - | Syntax.ident _ rawVal val preresolved => do +private partial def quoteSyntax : Syntax → TermElabM (TSyntax `term) + | Syntax.ident _ rawVal val preresolved => do if !hygiene.get (← getOptions) then return ← `(Syntax.ident info $(quote rawVal) $(quote val) $(quote preresolved)) -- Add global scopes at compilation time (now), add macro scope at runtime (in the quotation). @@ -234,7 +234,7 @@ elab_stx_quot Parser.Command.quot /- match -/ -- an "alternative" of patterns plus right-hand side -private abbrev Alt := List Syntax × Syntax +private abbrev Alt := List (TSyntax `term) × TSyntax `term /-- In a single match step, we match the first discriminant against the "head" of the first pattern of the first @@ -280,7 +280,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 Syntax) → TermElabM Syntax) (no : TermElabM Syntax) : TermElabM Syntax + doMatch (yes : (newDiscrs : List (TSyntax `term)) → TermElabM (TSyntax `term)) (no : TermElabM (TSyntax `term)) : TermElabM (TSyntax `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 @@ -288,7 +288,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 : Syntax → TermElabM Syntax) : Alt → TermElabM Alt +private def adaptRhs (fn : TSyntax `term → TermElabM (TSyntax `term)) : Alt → TermElabM Alt | (pats, rhs) => return (pats, ← fn rhs) private partial def getHeadInfo (alt : Alt) : TermElabM HeadInfo := @@ -489,7 +489,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 Syntax) (alts : List Alt) : TermElabM Syntax := do +private partial def compileStxMatch (discrs : List (TSyntax `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 d9870e416b..bfc485a64d 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 Syntax) := do +def getAntiquotationIds (stx : Syntax) : TermElabM (Array (TSyntax identKind)) := 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 13cedcb80c..3e8db79ab0 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 Syntax) : TermElabM Syntax := do +private def mkParserSeq (ds : Array (TSyntax `term)) : TermElabM Syntax := do if ds.size == 0 then throwUnsupportedSyntax else if ds.size == 1 then @@ -82,12 +82,12 @@ def resolveParserName [Monad m] [MonadInfoTree m] [MonadResolveName m] [MonadEnv 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 (Syntax × Option Nat) := do +partial def toParserDescr (stx : Syntax) (catName : Name) : TermElabM (TSyntax `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 Syntax := withRef stx do + process (stx : Syntax) : ToParserDescrM (TSyntax `term) := withRef stx do let kind := stx.getKind if kind == nullKind then processSeq stx @@ -340,7 +340,7 @@ def resolveSyntaxKind (k : Name) : CommandElabM Name := do def checkRuleKind (given expected : SyntaxNodeKind) : Bool := given == expected || given == expected ++ `antiquot -def inferMacroRulesAltKind : Syntax → CommandElabM SyntaxNodeKind +def inferMacroRulesAltKind : TSyntax ``matchAlt → CommandElabM SyntaxNodeKind | `(matchAltExpr| | $pat:term => $_) => do if !pat.isQuot then throwUnsupportedSyntax @@ -351,7 +351,7 @@ def inferMacroRulesAltKind : Syntax → 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 Syntax) (cmdName : String) (mkCmd : Option Name → Array Syntax → CommandElabM Syntax) : CommandElabM Syntax := do +def expandNoKindMacroRulesAux (alts : Array (TSyntax ``matchAlt)) (cmdName : String) (mkCmd : Option Name → Array (TSyntax ``matchAlt) → CommandElabM (TSyntax `command)) : CommandElabM (TSyntax `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 d724c8d71e..6e903d467a 100644 --- a/src/Lean/Elab/Tactic/Match.lean +++ b/src/Lean/Elab/Tactic/Match.lean @@ -12,7 +12,7 @@ namespace Lean.Elab.Tactic open Meta open Parser.Tactic in -private def mkAuxiliaryMatchTerm (parentTag : Name) (matchTac : Syntax) : MacroM (Syntax × Array Syntax) := do +private def mkAuxiliaryMatchTerm (parentTag : Name) (matchTac : Syntax) : MacroM (TSyntax `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 a4b3299e42..4d2e084171 100644 --- a/src/Lean/Elab/Tactic/Simp.lean +++ b/src/Lean/Elab/Tactic/Simp.lean @@ -174,7 +174,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 : Syntax) : TacticM ResolveSimpIdResult := do + resolveSimpIdTheorem? (simpArgTerm : TSyntax `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/Level.lean b/src/Lean/Level.lean index 4ec9e052d2..eeea31779f 100644 --- a/src/Lean/Level.lean +++ b/src/Lean/Level.lean @@ -447,8 +447,8 @@ mutual | Result.imaxNode fs, r => parenIfFalse (Format.group <| "imax" ++ formatLst fs) r end -protected partial def Result.quote (r : Result) (prec : Nat) : Syntax := - let addParen (s : Syntax) := +protected partial def Result.quote (r : Result) (prec : Nat) : TSyntax `level := + let addParen (s : TSyntax `level) := if prec > 0 then Unhygienic.run `(level| ( $s )) else s match r with | Result.leaf n => Unhygienic.run `(level| $(mkIdent n):ident) @@ -469,11 +469,11 @@ instance : ToFormat Level where instance : ToString Level where toString u := Format.pretty (Level.format u) -protected def quote (u : Level) (prec : Nat := 0) : Syntax := +protected def quote (u : Level) (prec : Nat := 0) : TSyntax `level := (PP.toResult u).quote prec -instance : Quote Level where - quote u := Level.quote u +instance : Quote Level `level where + quote := Level.quote end Level diff --git a/src/Lean/PrettyPrinter.lean b/src/Lean/PrettyPrinter.lean index 77bb2eade3..09d0920e69 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 Syntax) : MetaM Format := do +def ppUsing (e : Expr) (delab : Expr → MetaM (TSyntax `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 b2ee14cabb..4147bfb095 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 Syntax +abbrev Delab := DelabM (TSyntax `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 : Syntax) : Syntax := - stx.setInfo (SourceInfo.synthetic ⟨pos⟩ ⟨pos⟩) +def annotatePos (pos : Pos) (stx : TSyntax `term) : TSyntax `term := + ⟨stx.raw.setInfo (SourceInfo.synthetic ⟨pos⟩ ⟨pos⟩)⟩ -def annotateCurPos (stx : Syntax) : Delab := +def annotateCurPos (stx : TSyntax `term) : Delab := return annotatePos (← getPos) stx def getUnusedName (suggestion : Name) (body : Expr) : DelabM Name := do @@ -248,7 +248,7 @@ partial def delab : Delab := do else return ← ``(_) let k ← getExprKind - let stx ← delabFor k <|> (liftM $ show MetaM Syntax from throwError "don't know how to delaborate '{k}'") + let stx ← delabFor k <|> (liftM $ show MetaM _ from throwError "don't know how to delaborate '{k}'") if ← getPPOption getPPAnalyzeTypeAscriptions <&&> getPPOption getPPAnalysisNeedsType <&&> pure !e.isMData then let typeStx ← withType delab `(($stx:term : $typeStx:term)) >>= annotateCurPos @@ -274,7 +274,7 @@ end Delaborator open SubExpr (Pos) open Delaborator (OptionsPerPos topDownAnalyze) -def delabCore (e : Expr) (optionsPerPos : OptionsPerPos := {}) (delab := Delaborator.delab) : MetaM (Syntax × Std.RBMap Pos Elab.Info compare) := do +def delabCore (e : Expr) (optionsPerPos : OptionsPerPos := {}) (delab := Delaborator.delab) : MetaM (TSyntax `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 Syntax := do +def delab (e : Expr) (optionsPerPos : OptionsPerPos := {}) : MetaM (TSyntax `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 dcec957fbb..a32cef01f0 100644 --- a/src/Lean/PrettyPrinter/Delaborator/Builtins.lean +++ b/src/Lean/PrettyPrinter/Delaborator/Builtins.lean @@ -293,17 +293,17 @@ structure AppMatchState where info : MatcherInfo matcherTy : Expr params : Array Expr := #[] - motive : Option (Syntax × Expr) := none + motive : Option (TSyntax `term × Expr) := none motiveNamed : Bool := false - discrs : Array Syntax := #[] + discrs : Array (TSyntax `term) := #[] varNames : Array (Array Name) := #[] - rhss : Array Syntax := #[] + rhss : Array (TSyntax `term) := #[] -- additional arguments applied to the result of the `match` expression - moreArgs : Array Syntax := #[] + moreArgs : Array (TSyntax `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 Syntax)) := +private partial def delabPatterns (st : AppMatchState) : DelabM (Array (Array (TSyntax `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 e0e4af003c..78d829f136 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 Syntax := +private def deriveStructureInstance (indVal : InductiveVal) (params : Array Expr) : TermElabM (TSyntax `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 Syntax := #[] - let mut uniqFieldEncIds : Array Syntax := #[] - let mut fieldEncIds' : DiscrTree Syntax := {} + let mut fieldEncIds : Array (TSyntax `term) := #[] + let mut uniqFieldEncIds : Array (TSyntax identKind) := #[] + let mut fieldEncIds' : DiscrTree (TSyntax identKind) := {} 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 := Syntax.missing + let mut fieldEncId : TSyntax identKind := ⟨Syntax.missing⟩ match (← fieldEncIds'.getMatch fieldTp).back? with | none => fieldEncId ← mkIdent <$> mkFreshUserName fieldName @@ -157,17 +157,17 @@ private structure CtorState where encArgTypes : DiscrTree Name := {} uniqEncArgTypes : Array Name := #[] -- binders for `encArgTypes` as well as the relevant `RpcEncoding`s - binders : Array Syntax := #[] + binders : Array (TSyntax ``Parser.Term.bracketedBinder) := #[] -- the syntax of each constructor in the packet - ctors : Array Syntax := #[] + ctors : Array (TSyntax ``Parser.Command.ctor) := #[] -- syntax of each arm of the `rpcEncode` pattern-match - encodes : Array Syntax := #[] + encodes : Array (TSyntax ``Parser.Term.matchAlt) := #[] -- syntax of each arm of the `rpcDecode` pattern-match - decodes : Array Syntax := #[] + decodes : Array (TSyntax ``Parser.Term.matchAlt) := #[] deriving Inhabited private def matchF := Lean.Parser.Term.matchAlt (rhsParser := Lean.Parser.termParser) -private def deriveInductiveInstance (indVal : InductiveVal) (params : Array Expr) : TermElabM Syntax := do +private def deriveInductiveInstance (indVal : InductiveVal) (params : Array Expr) : TermElabM (TSyntax `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 Syntax := do + let mkBody (tgt : Name) (func : Name) : TermElabM (TSyntax `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) @@ -284,7 +284,7 @@ private def deriveInstance (typeName : Name) : CommandElabM Bool := do elabCommand cmd return true -private unsafe def dispatchDeriveInstanceUnsafe (declNames : Array Name) (args? : Option Syntax) : CommandElabM Bool := do +private unsafe def dispatchDeriveInstanceUnsafe (declNames : Array Name) (args? : Option (TSyntax ``Parser.Term.structInst)) : CommandElabM Bool := do if declNames.size ≠ 1 then return false let args ← @@ -301,7 +301,7 @@ private unsafe def dispatchDeriveInstanceUnsafe (declNames : Array Name) (args? deriveInstance declNames[0] @[implementedBy dispatchDeriveInstanceUnsafe] -private opaque dispatchDeriveInstance (declNames : Array Name) (args? : Option Syntax) : CommandElabM Bool +private opaque dispatchDeriveInstance (declNames : Array Name) (args? : Option (TSyntax ``Parser.Term.structInst)) : CommandElabM Bool builtin_initialize Elab.registerBuiltinDerivingHandlerWithArgs ``RpcEncoding dispatchDeriveInstance