refactor: introduce common TSyntax abbreviations
This commit is contained in:
Sebastian Ullrich
parent
db42874be4
commit
22475b8669
27 changed files with 124 additions and 107 deletions
|
|
@ -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))
|
||||
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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?` -/
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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]
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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?
|
||||
|
||||
|
|
|
|||
|
|
@ -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 [<kind>] ...` 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 ←
|
||||
|
|
|
|||
|
|
@ -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) _)
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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 := #[]
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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)
|
||||
|
|
|
|||
Loading…
Add table
Reference in a new issue