max/lean4-htt
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions 2

chore: update stage0

Browse source
This commit is contained in:
Gabriel Ebner 2022-07-11 21:41:26 +02:00 • committed by Leonardo de Moura
parent a8cab84735
commit 7e380bf236
454 changed files with 76147 additions and 117093 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

81
stage0/src/Init/Meta.lean generated
View file

@ -99,16 +99,16 @@ namespace Name
def getRoot : Name → Name
| anonymous => anonymous
| n@(str anonymous _ _) => n
| n@(num anonymous _ _) => n
| str n _ _ => getRoot n
| num n _ _ => getRoot n
| n@(str anonymous _) => n
| n@(num anonymous _) => n
| str n _ => getRoot n
| num n _ => getRoot n
@[export lean_is_inaccessible_user_name]
def isInaccessibleUserName : Name → Bool
| Name.str _ s _ => s.contains '✝' || s == "_inaccessible"
| Name.num p _ _ => isInaccessibleUserName p
| _ => false
| Name.str _ s => s.contains '✝' || s == "_inaccessible"
| Name.num p _ => isInaccessibleUserName p
| _ => false
def escapePart (s : String) : Option String :=
if s.length > 0 && isIdFirst (s.get 0) && (s.toSubstring.drop 1).all isIdRest then s
@ -118,11 +118,11 @@ def escapePart (s : String) : Option String :=
-- NOTE: does not roundtrip even with `escape = true` if name is anonymous or contains numeric part or `idEndEscape`
variable (sep : String) (escape : Bool)
def toStringWithSep : Name → String
| anonymous => "[anonymous]"
| str anonymous s _ => maybeEscape s
| num anonymous v _ => toString v
| str n s _ => toStringWithSep n ++ sep ++ maybeEscape s
| num n v _ => toStringWithSep n ++ sep ++ Nat.repr v
| anonymous => "[anonymous]"
| str anonymous s => maybeEscape s
| num anonymous v => toString v
| str n s => toStringWithSep n ++ sep ++ maybeEscape s
| num n v => toStringWithSep n ++ sep ++ Nat.repr v
where
maybeEscape s := if escape then escapePart s |>.getD s else s
@ -131,7 +131,7 @@ protected def toString (n : Name) (escape := true) : String :=
toStringWithSep "." (escape && !n.isInaccessibleUserName && !n.hasMacroScopes && !maybePseudoSyntax) n
where
maybePseudoSyntax :=
if let Name.str _ s _ := n.getRoot then
if let .str _ s := n.getRoot then
-- could be pseudo-syntax for loose bvar or universe mvar, output as is
"#".isPrefixOf s || "?".isPrefixOf s
else
@ -148,8 +148,8 @@ private def hasNum : Name → Bool
protected def reprPrec (n : Name) (prec : Nat) : Std.Format :=
match n with
| anonymous => Std.Format.text "Lean.Name.anonymous"
| num p i _ => Repr.addAppParen ("Lean.Name.mkNum " ++ Name.reprPrec p max_prec ++ " " ++ repr i) prec
| str p s _ =>
| num p i => Repr.addAppParen ("Lean.Name.mkNum " ++ Name.reprPrec p max_prec ++ " " ++ repr i) prec
| str p s =>
if p.hasNum then
Repr.addAppParen ("Lean.Name.mkStr " ++ Name.reprPrec p max_prec ++ " " ++ repr s) prec
else
@ -161,23 +161,23 @@ instance : Repr Name where
deriving instance Repr for Syntax
def capitalize : Name → Name
| Name.str p s _ => Name.mkStr p s.capitalize
| n => n
| .str p s => .str p s.capitalize
| n => n
def replacePrefix : Name → Name → Name → Name
| anonymous, anonymous, newP => newP
| anonymous, _, _ => anonymous
| n@(str p s _), queryP, newP => if n == queryP then newP else Name.mkStr (p.replacePrefix queryP newP) s
| n@(num p s _), queryP, newP => if n == queryP then newP else Name.mkNum (p.replacePrefix queryP newP) s
| anonymous, anonymous, newP => newP
| anonymous, _, _ => anonymous
| n@(str p s), queryP, newP => if n == queryP then newP else Name.mkStr (p.replacePrefix queryP newP) s
| n@(num p s), queryP, newP => if n == queryP then newP else Name.mkNum (p.replacePrefix queryP newP) s
/--
`eraseSuffix? n s` return `n'` if `n` is of the form `n == n' ++ s`.
-/
def eraseSuffix? : Name → Name → Option Name
| n, anonymous => some n
| str p s _, str p' s' _ => if s == s' then eraseSuffix? p p' else none
| num p s _, num p' s' _ => if s == s' then eraseSuffix? p p' else none
| _, _ => none
| n, anonymous => some n
| str p s, str p' s' => if s == s' then eraseSuffix? p p' else none
| num p s, num p' s' => if s == s' then eraseSuffix? p p' else none
| _, _ => none
/-- Remove macros scopes, apply `f`, and put them back -/
@[inline] def modifyBase (n : Name) (f : Name → Name) : Name :=
@ -190,21 +190,32 @@ def eraseSuffix? : Name → Name → Option Name
@[export lean_name_append_after]
def appendAfter (n : Name) (suffix : String) : Name :=
n.modifyBase fun
| str p s _ => Name.mkStr p (s ++ suffix)
| n => Name.mkStr n suffix
| str p s => Name.mkStr p (s ++ suffix)
| n => Name.mkStr n suffix
@[export lean_name_append_index_after]
def appendIndexAfter (n : Name) (idx : Nat) : Name :=
n.modifyBase fun
| str p s _ => Name.mkStr p (s ++ "_" ++ toString idx)
| n => Name.mkStr n ("_" ++ toString idx)
| str p s => Name.mkStr p (s ++ "_" ++ toString idx)
| n => Name.mkStr n ("_" ++ toString idx)
@[export lean_name_append_before]
def appendBefore (n : Name) (pre : String) : Name :=
n.modifyBase fun
| anonymous => Name.mkStr anonymous pre
| str p s _ => Name.mkStr p (pre ++ s)
| num p n _ => Name.mkNum (Name.mkStr p pre) n
| str p s => Name.mkStr p (pre ++ s)
| num p n => Name.mkNum (Name.mkStr p pre) n
protected theorem beq_iff_eq {m n : Name} : m == n ↔ m = n := by
show m.beq n ↔ _
induction m generalizing n <;> cases n <;> simp_all [Name.beq, And.comm]
instance : LawfulBEq Name where
eq_of_beq := Name.beq_iff_eq.1
rfl := Name.beq_iff_eq.2 rfl
instance : DecidableEq Name :=
fun a b => if h : a == b then .isTrue (by simp_all) else .isFalse (by simp_all)
end Name
@ -920,15 +931,15 @@ instance : Quote Substring := ⟨fun s => Syntax.mkCApp `String.toSubstring #[qu
-- in contrast to `Name.toString`, we can, and want to be, precise here
private def getEscapedNameParts? (acc : List String) : Name → Option (List String)
| Name.anonymous => if acc.isEmpty then none else some acc
| Name.str n s _ => do
| Name.str n s => do
let s ← Name.escapePart s
getEscapedNameParts? (s::acc) n
| Name.num _ _ _ => none
| Name.num _ _ => none
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]
| 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 `term where
quote n := match getEscapedNameParts? [] n with

72
stage0/src/Init/Prelude.lean generated
View file

@ -1747,47 +1747,47 @@ namespace Lean
/- Hierarchical names -/
inductive Name where
| anonymous : Name
| str : Name → String → UInt64 → Name
| num : Name → Nat → UInt64 → Name
| str : Name → String → Name
| num : Name → Nat → Name
with
@[computedField] hash : Name → UInt64
| .anonymous => .ofNatCore 1723 (by decide)
| .str p s => mixHash p.hash s.hash
| .num p v => mixHash p.hash (dite (LT.lt v UInt64.size) (fun h => UInt64.ofNatCore v h) (fun _ => UInt64.ofNatCore 17 (by decide)))
instance : Inhabited Name where
default := Name.anonymous
protected def Name.hash : Name → UInt64
| Name.anonymous => UInt64.ofNatCore 1723 (by decide)
| Name.str _ _ h => h
| Name.num _ _ h => h
instance : Hashable Name where
hash := Name.hash
namespace Name
@[export lean_name_mk_string]
def mkStr (p : Name) (s : String) : Name :=
Name.str p s (mixHash (hash p) (hash s))
abbrev mkStr (p : Name) (s : String) : Name :=
Name.str p s
@[export lean_name_mk_numeral]
def mkNum (p : Name) (v : Nat) : Name :=
Name.num p v (mixHash (hash p) (dite (LT.lt v UInt64.size) (fun h => UInt64.ofNatCore v h) (fun _ => UInt64.ofNatCore 17 (by decide))))
abbrev mkNum (p : Name) (v : Nat) : Name :=
Name.num p v
def mkSimple (s : String) : Name :=
abbrev mkSimple (s : String) : Name :=
mkStr Name.anonymous s
@[extern "lean_name_eq"]
protected def beq : (@& Name) → (@& Name) → Bool
| anonymous, anonymous => true
| str p₁ s₁ _, str p₂ s₂ _ => and (BEq.beq s₁ s₂) (Name.beq p₁ p₂)
| num p₁ n₁ _, num p₂ n₂ _ => and (BEq.beq n₁ n₂) (Name.beq p₁ p₂)
| _, _ => false
| anonymous, anonymous => true
| str p₁ s₁, str p₂ s₂ => and (BEq.beq s₁ s₂) (Name.beq p₁ p₂)
| num p₁ n₁, num p₂ n₂ => and (BEq.beq n₁ n₂) (Name.beq p₁ p₂)
| _, _ => false
instance : BEq Name where
beq := Name.beq
protected def append : Name → Name → Name
| n, anonymous => n
| n, str p s _ => Name.mkStr (Name.append n p) s
| n, num p d _ => Name.mkNum (Name.append n p) d
| n, str p s => Name.mkStr (Name.append n p) s
| n, num p d => Name.mkNum (Name.append n p) d
instance : Append Name where
append := Name.append
@ -2143,16 +2143,16 @@ The delimiter `_hyg` is used just to improve the `hasMacroScopes` performance.
-/
def Name.hasMacroScopes : Name → Bool
| str _ s _ => beq s "_hyg"
| num p _ _ => hasMacroScopes p
| _ => false
| str _ s => beq s "_hyg"
| num p _ => hasMacroScopes p
| _ => false
private def eraseMacroScopesAux : Name → Name
| Name.str p s _ => match beq s "_@" with
| .str p s => match beq s "_@" with
| true => p
| false => eraseMacroScopesAux p
| Name.num p _ _ => eraseMacroScopesAux p
| Name.anonymous => Name.anonymous
| .num p _ => eraseMacroScopesAux p
| .anonymous => Name.anonymous
@[export lean_erase_macro_scopes]
def Name.eraseMacroScopes (n : Name) : Name :=
@ -2161,8 +2161,8 @@ def Name.eraseMacroScopes (n : Name) : Name :=
| false => n
private def simpMacroScopesAux : Name → Name
| Name.num p i _ => Name.mkNum (simpMacroScopesAux p) i
| n => eraseMacroScopesAux n
| .num p i => Name.mkNum (simpMacroScopesAux p) i
| n => eraseMacroScopesAux n
/- Helper function we use to create binder names that do not need to be unique. -/
@[export lean_simp_macro_scopes]
@ -2188,30 +2188,30 @@ def MacroScopesView.review (view : MacroScopesView) : Name :=
view.scopes.foldl Name.mkNum base
private def assembleParts : List Name → Name → Name
| List.nil, acc => acc
| List.cons (Name.str _ s _) ps, acc => assembleParts ps (Name.mkStr acc s)
| List.cons (Name.num _ n _) ps, acc => assembleParts ps (Name.mkNum acc n)
| _, _ => panic "Error: unreachable @ assembleParts"
| .nil, acc => acc
| .cons (.str _ s) ps, acc => assembleParts ps (Name.mkStr acc s)
| .cons (.num _ n) ps, acc => assembleParts ps (Name.mkNum acc n)
| _, _ => panic "Error: unreachable @ assembleParts"
private def extractImported (scps : List MacroScope) (mainModule : Name) : Name → List Name → MacroScopesView
| n@(Name.str p str _), parts =>
| n@(Name.str p str), parts =>
match beq str "_@" with
| true => { name := p, mainModule := mainModule, imported := assembleParts parts Name.anonymous, scopes := scps }
| false => extractImported scps mainModule p (List.cons n parts)
| n@(Name.num p _ _), parts => extractImported scps mainModule p (List.cons n parts)
| n@(Name.num p _), parts => extractImported scps mainModule p (List.cons n parts)
| _, _ => panic "Error: unreachable @ extractImported"
private def extractMainModule (scps : List MacroScope) : Name → List Name → MacroScopesView
| n@(Name.str p str _), parts =>
| n@(Name.str p str), parts =>
match beq str "_@" with
| true => { name := p, mainModule := assembleParts parts Name.anonymous, imported := Name.anonymous, scopes := scps }
| false => extractMainModule scps p (List.cons n parts)
| n@(Name.num _ _ _), acc => extractImported scps (assembleParts acc Name.anonymous) n List.nil
| n@(Name.num _ _), acc => extractImported scps (assembleParts acc Name.anonymous) n List.nil
| _, _ => panic "Error: unreachable @ extractMainModule"
private def extractMacroScopesAux : Name → List MacroScope → MacroScopesView
| Name.num p scp _, acc => extractMacroScopesAux p (List.cons scp acc)
| Name.str p _ _, acc => extractMainModule acc p List.nil -- str must be "_hyg"
| Name.num p scp, acc => extractMacroScopesAux p (List.cons scp acc)
| Name.str p _ , acc => extractMainModule acc p List.nil -- str must be "_hyg"
| _, _ => panic "Error: unreachable @ extractMacroScopesAux"
/--

8
stage0/src/Init/SizeOf.lean generated
View file

@ -66,17 +66,17 @@ namespace Lean
an opaque function for computing the hashcode field. -/
protected noncomputable def Name.sizeOf : Name → Nat
| anonymous => 1
| str p s _ => 1 + Name.sizeOf p + sizeOf s
| num p n _ => 1 + Name.sizeOf p + sizeOf n
| str p s => 1 + Name.sizeOf p + sizeOf s
| num p n => 1 + Name.sizeOf p + sizeOf n
noncomputable instance : SizeOf Name where
sizeOf n := n.sizeOf
@[simp] theorem Name.anonymous.sizeOf_spec : sizeOf anonymous = 1 :=
rfl
@[simp] theorem Name.str.sizeOf_spec (p : Name) (s : String) (h : UInt64) : sizeOf (str p s h) = 1 + sizeOf p + sizeOf s :=
@[simp] theorem Name.str.sizeOf_spec (p : Name) (s : String) : sizeOf (str p s) = 1 + sizeOf p + sizeOf s :=
rfl
@[simp] theorem Name.num.sizeOf_spec (p : Name) (n : Nat) (h : UInt64) : sizeOf (num p n h) = 1 + sizeOf p + sizeOf n :=
@[simp] theorem Name.num.sizeOf_spec (p : Name) (n : Nat) : sizeOf (num p n) = 1 + sizeOf p + sizeOf n :=
rfl
deriving instance SizeOf for Syntax

2
stage0/src/Lean/Attributes.lean generated
View file

@ -323,7 +323,7 @@ unsafe def mkAttributeImplOfConstantUnsafe (env : Environment) (opts : Options)
| none => throw ("unknow constant '" ++ toString declName ++ "'")
| some info =>
match info.type with
| Expr.const `Lean.AttributeImpl _ _ => env.evalConst AttributeImpl opts declName
| Expr.const `Lean.AttributeImpl _ => env.evalConst AttributeImpl opts declName
| _ => throw ("unexpected attribute implementation type at '" ++ toString declName ++ "' (`AttributeImpl` expected")
@[implementedBy mkAttributeImplOfConstantUnsafe]

2
stage0/src/Lean/AuxRecursor.lean generated
View file

@ -35,7 +35,7 @@ def isAuxRecursor (env : Environment) (declName : Name) : Bool :=
def isAuxRecursorWithSuffix (env : Environment) (declName : Name) (suffix : Name) : Bool :=
match declName with
| Name.str _ s _ => s == suffix && isAuxRecursor env declName
| .str _ s => s == suffix && isAuxRecursor env declName
| _ => false
def isCasesOnRecursor (env : Environment) (declName : Name) : Bool :=

2
stage0/src/Lean/Class.lean generated
View file

@ -94,7 +94,7 @@ private def consumeNLambdas : Nat → Expr → Option Expr
partial def getClassName (env : Environment) : Expr → Option Name
| Expr.forallE _ _ b _ => getClassName env b
| e => do
let Expr.const c _ _ ← pure e.getAppFn | none
let Expr.const c _ ← pure e.getAppFn | none
let info ← env.find? c
match info.value? with
| some val => do

20
stage0/src/Lean/Compiler/ConstFolding.lean generated
View file

@ -40,14 +40,14 @@ def getInfoFromFn (fn : Name) : List NumScalarTypeInfo → Option NumScalarTypeI
else getInfoFromFn fn infos
def getInfoFromVal : Expr → Option NumScalarTypeInfo
| Expr.app (Expr.const fn _ _) _ _ => getInfoFromFn fn numScalarTypes
| _ => none
| Expr.app (Expr.const fn _) _ => getInfoFromFn fn numScalarTypes
| _ => none
@[export lean_get_num_lit]
def getNumLit : Expr → Option Nat
| Expr.lit (Literal.natVal n) _ => some n
| Expr.app (Expr.const fn _ _) a _ => if isOfNat fn then getNumLit a else none
| _ => none
| Expr.lit (Literal.natVal n) => some n
| Expr.app (Expr.const fn _) a => if isOfNat fn then getNumLit a else none
| _ => none
def mkUIntLit (info : NumScalarTypeInfo) (n : Nat) : Expr :=
mkApp (mkConst info.ofNatFn) (mkRawNatLit (n%info.size))
@ -148,9 +148,9 @@ def natFoldFns : List (Name × BinFoldFn) :=
]
def getBoolLit : Expr → Option Bool
| Expr.const ``Bool.true _ _ => some true
| Expr.const ``Bool.false _ _ => some false
| _ => none
| Expr.const ``Bool.true _ => some true
| Expr.const ``Bool.false _ => some false
| _ => none
def foldStrictAnd (_ : Bool) (a₁ a₂ : Expr) : Option Expr :=
let v₁ := getBoolLit a₁
@ -211,7 +211,7 @@ def findUnFoldFn (fn : Name) : Option UnFoldFn :=
@[export lean_fold_bin_op]
def foldBinOp (beforeErasure : Bool) (f : Expr) (a : Expr) (b : Expr) : Option Expr := do
match f with
| Expr.const fn _ _ =>
| Expr.const fn _ =>
let foldFn ← findBinFoldFn fn
foldFn beforeErasure a b
| _ =>
@ -220,7 +220,7 @@ def foldBinOp (beforeErasure : Bool) (f : Expr) (a : Expr) (b : Expr) : Option E
@[export lean_fold_un_op]
def foldUnOp (beforeErasure : Bool) (f : Expr) (a : Expr) : Option Expr := do
match f with
| Expr.const fn _ _ =>
| Expr.const fn _ =>
let foldFn ← findUnFoldFn fn
foldFn beforeErasure a
| _ => failure

6
stage0/src/Lean/Compiler/ExportAttr.lean generated
View file

@ -12,9 +12,9 @@ private def isValidCppId (id : String) : Bool :=
first.isAlpha && (id.toSubstring.drop 1).all (fun c => c.isAlpha || c.isDigit || c == '_')
private def isValidCppName : Name → Bool
| Name.str Name.anonymous s _ => isValidCppId s
| Name.str p s _ => isValidCppId s && isValidCppName p
| _ => false
| .str .anonymous s => isValidCppId s
| .str p s => isValidCppId s && isValidCppName p
| _ => false
builtin_initialize exportAttr : ParametricAttribute Name ←
registerParametricAttribute {

5
stage0/src/Lean/Compiler/IR/Boxing.lean generated
View file

@ -32,9 +32,8 @@ open Std (AssocList)
def mkBoxedName (n : Name) : Name :=
Name.mkStr n "_boxed"
def isBoxedName : Name → Bool
| Name.str _ "_boxed" _ => true
| _ => false
def isBoxedName (name : Name) : Bool :=
name matches .str _ "_boxed"
abbrev N := StateM Nat

12
stage0/src/Lean/Compiler/IR/EmitC.lean generated
View file

@ -72,9 +72,9 @@ def toCName (n : Name) : M String := do
let env ← getEnv;
-- TODO: we should support simple export names only
match getExportNameFor env n with
| some (Name.str Name.anonymous s _) => pure s
| some _ => throwInvalidExportName n
| none => if n == `main then pure leanMainFn else pure n.mangle
| some (.str .anonymous s) => pure s
| some _ => throwInvalidExportName n
| none => if n == `main then pure leanMainFn else pure n.mangle
def emitCName (n : Name) : M Unit :=
toCName n >>= emit
@ -83,9 +83,9 @@ def toCInitName (n : Name) : M String := do
let env ← getEnv;
-- TODO: we should support simple export names only
match getExportNameFor env n with
| some (Name.str Name.anonymous s _) => return "_init_" ++ s
| some _ => throwInvalidExportName n
| none => pure ("_init_" ++ n.mangle)
| some (.str .anonymous s) => return "_init_" ++ s
| some _ => throwInvalidExportName n
| none => pure ("_init_" ++ n.mangle)
def emitCInitName (n : Name) : M Unit :=
toCInitName n >>= emit

8
stage0/src/Lean/Compiler/InitAttr.lean generated
View file

@ -9,12 +9,12 @@ import Lean.Attributes
namespace Lean
private def getIOTypeArg : Expr → Option Expr
| Expr.app (Expr.const `IO _ _) arg _ => some arg
| _ => none
| Expr.app (Expr.const `IO _) arg => some arg
| _ => none
private def isUnitType : Expr → Bool
| Expr.const `Unit _ _ => true
| _ => false
| Expr.const `Unit _ => true
| _ => false
private def isIOUnit (type : Expr) : Bool :=
match getIOTypeArg type with

4
stage0/src/Lean/Compiler/NameMangling.lean generated
View file

@ -48,12 +48,12 @@ namespace Lean
private def Name.mangleAux : Name → String
| Name.anonymous => ""
| Name.str p s _ =>
| Name.str p s =>
let m := String.mangle s
match p with
| Name.anonymous => m
| p => mangleAux p ++ "_" ++ m
| Name.num p n _ => mangleAux p ++ "_" ++ toString n ++ "_"
| Name.num p n => mangleAux p ++ "_" ++ toString n ++ "_"
@[export lean_name_mangle]
def Name.mangle (n : Name) (pre : String := "l_") : String :=

16
stage0/src/Lean/Compiler/Util.lean generated
View file

@ -39,13 +39,13 @@ instance : AndThen Visitor where
| {found := true, result := true} => {found := true, result := x != y}
def visit (x : FVarId) : Expr → Visitor
| Expr.fvar y _ => visitFVar y x
| Expr.app f a _ => visit x a >> visit x f
| Expr.fvar y => visitFVar y x
| Expr.app f a => visit x a >> visit x f
| Expr.lam _ d b _ => visit x d >> visit x b
| Expr.forallE _ d b _ => visit x d >> visit x b
| Expr.letE _ t v b _ => visit x t >> visit x v >> visit x b
| Expr.mdata _ e _ => visit x e
| Expr.proj _ _ e _ => visit x e
| Expr.mdata _ e => visit x e
| Expr.proj _ _ e => visit x e
| _ => skip
end atMostOnce
@ -65,9 +65,9 @@ def mkEagerLambdaLiftingName (n : Name) (idx : Nat) : Name :=
@[export lean_is_eager_lambda_lifting_name]
def isEagerLambdaLiftingName : Name → Bool
| Name.str p s _ => "_elambda".isPrefixOf s || isEagerLambdaLiftingName p
| Name.num p _ _ => isEagerLambdaLiftingName p
| _ => false
| .str p s => "_elambda".isPrefixOf s || isEagerLambdaLiftingName p
| .num p _ => isEagerLambdaLiftingName p
| _ => false
/-- Return the name of new definitions in the a given declaration.
Here we consider only declarations we generate code for.
@ -97,7 +97,7 @@ def mkUnsafeRecName (declName : Name) : Name :=
/-- Return `some _` if the given name was created using `mkUnsafeRecName` -/
@[export lean_is_unsafe_rec_name]
def isUnsafeRecName? : Name → Option Name
| Name.str n "_unsafe_rec" _ => some n
| .str n "_unsafe_rec" => some n
| _ => none
end Compiler

78
stage0/src/Lean/Data/Name.lean generated
View file

@ -18,58 +18,58 @@ namespace Name
def getPrefix : Name → Name
| anonymous => anonymous
| str p _ _ => p
| num p _ _ => p
| str p _ => p
| num p _ => p
def getString! : Name → String
| str _ s _ => s
| _ => unreachable!
| str _ s => s
| _ => unreachable!
def getNumParts : Name → Nat
| anonymous => 0
| str p _ _ => getNumParts p + 1
| num p _ _ => getNumParts p + 1
| str p _ => getNumParts p + 1
| num p _ => getNumParts p + 1
def updatePrefix : Name → Name → Name
| anonymous, _ => anonymous
| str _ s _, newP => Name.mkStr newP s
| num _ s _, newP => Name.mkNum newP s
| str _ s, newP => Name.mkStr newP s
| num _ s, newP => Name.mkNum newP s
def components' : Name → List Name
| anonymous => []
| str n s _ => Name.mkStr anonymous s :: components' n
| num n v _ => Name.mkNum anonymous v :: components' n
| str n s => Name.mkStr anonymous s :: components' n
| num n v => Name.mkNum anonymous v :: components' n
def components (n : Name) : List Name :=
n.components'.reverse
def eqStr : Name → String → Bool
| str anonymous s _, s' => s == s'
| str anonymous s, s' => s == s'
| _, _ => false
def isPrefixOf : Name → Name → Bool
| p, anonymous => p == anonymous
| p, n@(num p' _ _) => p == n || isPrefixOf p p'
| p, n@(str p' _ _) => p == n || isPrefixOf p p'
| p, anonymous => p == anonymous
| p, n@(num p' _) => p == n || isPrefixOf p p'
| p, n@(str p' _) => p == n || isPrefixOf p p'
def isSuffixOf : Name → Name → Bool
| anonymous, _ => true
| str p₁ s₁ _, str p₂ s₂ _ => s₁ == s₂ && isSuffixOf p₁ p₂
| num p₁ n₁ _, num p₂ n₂ _ => n₁ == n₂ && isSuffixOf p₁ p₂
| _, _ => false
| anonymous, _ => true
| str p₁ s₁, str p₂ s₂ => s₁ == s₂ && isSuffixOf p₁ p₂
| num p₁ n₁, num p₂ n₂ => n₁ == n₂ && isSuffixOf p₁ p₂
| _, _ => false
def cmp : Name → Name → Ordering
| anonymous, anonymous => Ordering.eq
| anonymous, _ => Ordering.lt
| _, anonymous => Ordering.gt
| num p₁ i₁ _, num p₂ i₂ _ =>
| anonymous, anonymous => Ordering.eq
| anonymous, _ => Ordering.lt
| _, anonymous => Ordering.gt
| num p₁ i₁, num p₂ i₂ =>
match cmp p₁ p₂ with
| Ordering.eq => compare i₁ i₂
| ord => ord
| num _ _ _, str _ _ _ => Ordering.lt
| str _ _ _, num _ _ _ => Ordering.gt
| str p₁ n₁ _, str p₂ n₂ _ =>
| num _ _, str _ _ => Ordering.lt
| str _ _, num _ _ => Ordering.gt
| str p₁ n₁, str p₂ n₂ =>
match cmp p₁ p₂ with
| Ordering.eq => compare n₁ n₂
| ord => ord
@ -78,16 +78,16 @@ def lt (x y : Name) : Bool :=
cmp x y == Ordering.lt
def quickCmpAux : Name → Name → Ordering
| anonymous, anonymous => Ordering.eq
| anonymous, _ => Ordering.lt
| _, anonymous => Ordering.gt
| num n v _, num n' v' _ =>
| anonymous, anonymous => Ordering.eq
| anonymous, _ => Ordering.lt
| _, anonymous => Ordering.gt
| num n v, num n' v' =>
match compare v v' with
| Ordering.eq => n.quickCmpAux n'
| ord => ord
| num _ _ _, str _ _ _ => Ordering.lt
| str _ _ _, num _ _ _ => Ordering.gt
| str n s _, str n' s' _ =>
| num _ _, str _ _ => Ordering.lt
| str _ _, num _ _ => Ordering.gt
| str n s, str n' s' =>
match compare s s' with
| Ordering.eq => n.quickCmpAux n'
| ord => ord
@ -110,15 +110,15 @@ def quickLt (n₁ n₂ : Name) : Bool :=
/- The frontend does not allow user declarations to start with `_` in any of its parts.
We use name parts starting with `_` internally to create auxiliary names (e.g., `_private`). -/
def isInternal : Name → Bool
| str p s _ => s.get 0 == '_' || isInternal p
| num p _ _ => isInternal p
| _ => false
| str p s => s.get 0 == '_' || isInternal p
| num p _ => isInternal p
| _ => false
def isAtomic : Name → Bool
| anonymous => true
| str anonymous _ _ => true
| num anonymous _ _ => true
| _ => false
| anonymous => true
| str anonymous _ => true
| num anonymous _ => true
| _ => false
def isAnonymous : Name → Bool
| anonymous => true

4
stage0/src/Lean/Data/NameTrie.lean generated
View file

@ -34,8 +34,8 @@ private def toKey (n : Name) : List NamePart :=
loop n []
where
loop
| Name.str p s _, parts => loop p (NamePart.str s :: parts)
| Name.num p n _, parts => loop p (NamePart.num n :: parts)
| Name.str p s, parts => loop p (NamePart.str s :: parts)
| Name.num p n, parts => loop p (NamePart.num n :: parts)
| Name.anonymous, parts => parts
def NameTrie.insert (t : NameTrie β) (n : Name) (b : β) : NameTrie β :=

22
stage0/src/Lean/Elab/App.lean generated
View file

@ -249,11 +249,11 @@ private def fTypeHasOptAutoParams : M Bool := do
See `propagateExpectedType`.
Remark: `(explicit : Bool) == true` when `@` modifier is used. -/
private partial def getForallBody (explicit : Bool) : Nat → List NamedArg → Expr → Option Expr
| i, namedArgs, type@(Expr.forallE n d b c) =>
| i, namedArgs, type@(Expr.forallE n d b bi) =>
match namedArgs.find? fun (namedArg : NamedArg) => namedArg.name == n with
| some _ => getForallBody explicit i (eraseNamedArgCore namedArgs n) b
| none =>
if !explicit && !c.binderInfo.isExplicit then
if !explicit && !bi.isExplicit then
getForallBody explicit i namedArgs b
else if i > 0 then
getForallBody explicit (i-1) namedArgs b
@ -462,21 +462,21 @@ where
isResultType (type : Expr) (i : Nat) : Bool :=
match type with
| .forallE _ _ b _ => isResultType b (i + 1)
| .bvar idx _ => idx == i
| .bvar idx => idx == i
| _ => false
/- (quick filter) Return true if `type` constains a binder `[C ...]` where `C` is a class containing outparams. -/
hasLocalInstaceWithOutParams (type : Expr) : CoreM Bool := do
let .forallE _ d b c := type | return false
if c.binderInfo.isInstImplicit then
let .forallE _ d b bi := type | return false
if bi.isInstImplicit then
if let .const declName .. := d.getAppFn then
if hasOutParams (← getEnv) declName then
return true
hasLocalInstaceWithOutParams b
isOutParamOfLocalInstance (x : Expr) (type : Expr) : MetaM Bool := do
let .forallE _ d b c := type | return false
if c.binderInfo.isInstImplicit then
let .forallE _ d b bi := type | return false
if bi.isInstImplicit then
if let .const declName .. := d.getAppFn then
if hasOutParams (← getEnv) declName then
let cType ← inferType d.getAppFn
@ -538,7 +538,7 @@ mutual
let argType ← getArgExpectedType
match (← read).explicit, argType.getOptParamDefault?, argType.getAutoParamTactic? with
| false, some defVal, _ => addNewArg argName defVal; main
| false, _, some (Expr.const tacticDecl _ _) =>
| false, _, some (Expr.const tacticDecl _) =>
let env ← getEnv
let opts ← getOptions
match evalSyntaxConstant env opts tacticDecl with
@ -773,12 +773,12 @@ private def resolveLValAux (e : Expr) (eType : Expr) (lval : LVal) : TermElabM L
private partial def consumeImplicits (stx : Syntax) (e eType : Expr) (hasArgs : Bool) : TermElabM (Expr × Expr) := do
let eType ← whnfCore eType
match eType with
| .forallE _ d b c =>
if c.binderInfo.isImplicit || (hasArgs && c.binderInfo.isStrictImplicit) then
| .forallE _ d b bi =>
if bi.isImplicit || (hasArgs && bi.isStrictImplicit) then
let mvar ← mkFreshExprMVar d
registerMVarErrorHoleInfo mvar.mvarId! stx
consumeImplicits stx (mkApp e mvar) (b.instantiate1 mvar) hasArgs
else if c.binderInfo.isInstImplicit then
else if bi.isInstImplicit then
let mvar ← mkInstMVar d
let r := mkApp e mvar
registerMVarErrorImplicitArgInfo mvar.mvarId! stx r

2
stage0/src/Lean/Elab/Attributes.lean generated
View file

@ -49,7 +49,7 @@ def elabAttr [Monad m] [MonadEnv m] [MonadResolveName m] [MonadError m] [MonadMa
let attrName ← if attr.getKind == ``Parser.Attr.simple then
pure attr[0].getId.eraseMacroScopes
else match attr.getKind with
| Name.str _ s _ => pure <| Name.mkSimple s
| .str _ s => pure <| Name.mkSimple s
| _ => throwErrorAt attr "unknown attribute"
unless isAttribute (← getEnv) attrName do
throwError "unknown attribute [{attrName}]"

4
stage0/src/Lean/Elab/AutoBound.lean generated
View file

@ -39,12 +39,12 @@ Therefore, we do consider identifier with macro scopes anymore.
def isValidAutoBoundImplicitName (n : Name) (relaxed : Bool) : Bool :=
match n with
| Name.str Name.anonymous s _ => s.length > 0 && (relaxed || ((isGreek s.front || s.front.isLower) && isValidAutoBoundSuffix s))
| .str .anonymous s => s.length > 0 && (relaxed || ((isGreek s.front || s.front.isLower) && isValidAutoBoundSuffix s))
| _ => false
def isValidAutoBoundLevelName (n : Name) (relaxed : Bool) : Bool :=
match n with
| Name.str Name.anonymous s _ => s.length > 0 && (relaxed || (s.front.isLower && isValidAutoBoundSuffix s))
| .str .anonymous s => s.length > 0 && (relaxed || (s.front.isLower && isValidAutoBoundSuffix s))
| _ => false
end Lean.Elab

10
stage0/src/Lean/Elab/BuiltinCommand.lean generated
View file

@ -30,8 +30,8 @@ private def addScope (isNewNamespace : Bool) (isNoncomputable : Bool) (header :
activateScoped newNamespace
private def addScopes (isNewNamespace : Bool) (isNoncomputable : Bool) : Name → CommandElabM Unit
| Name.anonymous => pure ()
| Name.str p header _ => do
| .anonymous => pure ()
| .str p header => do
addScopes isNewNamespace isNoncomputable p
let currNamespace ← getCurrNamespace
addScope isNewNamespace isNoncomputable header (if isNewNamespace then Name.mkStr currNamespace header else currNamespace)
@ -55,9 +55,9 @@ private def checkAnonymousScope : List Scope → Bool
| _ => false
private def checkEndHeader : Name → List Scope → Bool
| Name.anonymous, _ => true
| Name.str p s _, { header := h, .. } :: scopes => h == s && checkEndHeader p scopes
| _, _ => false
| .anonymous, _ => true
| .str p s, { header := h, .. } :: scopes => h == s && checkEndHeader p scopes
| _, _ => false
@[builtinCommandElab «namespace»] def elabNamespace : CommandElab := fun stx =>
match stx with

2
stage0/src/Lean/Elab/BuiltinNotation.lean generated
View file

@ -99,7 +99,7 @@ private def elabParserMacroAux (prec e : Term) (withAnonymousAntiquot : Bool) :
let (some declName) ← getDeclName?
| throwError "invalid `leading_parser` macro, it must be used in definitions"
match extractMacroScopes declName with
| { name := Name.str _ s _, .. } =>
| { name := .str _ s, .. } =>
let kind := quote declName
let s := quote s
``(withAntiquot (mkAntiquot $s $kind $(quote withAnonymousAntiquot)) (leadingNode $kind $prec $e))

4
stage0/src/Lean/Elab/DeclModifiers.lean generated
View file

@ -171,7 +171,7 @@ def mkDeclName (currNamespace : Name) (modifiers : Modifiers) (shortName : Name)
throwError "atomic identifier expected '{shortName}'"
let declName := if isRootName then { view with name := name.replacePrefix `_root_ Name.anonymous }.review else currNamespace ++ shortName
if isRootName then
let .str p s _ := name | throwError "invalid declaration name '{name}'"
let .str p s := name | throwError "invalid declaration name '{name}'"
shortName := Name.mkSimple s
currNamespace := p.replacePrefix `_root_ Name.anonymous
checkIfShadowingStructureField declName
@ -179,7 +179,7 @@ def mkDeclName (currNamespace : Name) (modifiers : Modifiers) (shortName : Name)
match modifiers.visibility with
| Visibility.protected =>
match currNamespace with
| Name.str _ s _ => pure (declName, Name.mkSimple s ++ shortName)
| .str _ s => pure (declName, Name.mkSimple s ++ shortName)
| _ => throwError "protected declarations must be in a namespace"
| _ => pure (declName, shortName)

8
stage0/src/Lean/Elab/DeclUtil.lean generated
View file

@ -19,9 +19,9 @@ def forallTelescopeCompatibleAux {α} (k : Array Expr → Expr → Expr → Meta
throwError "parameter name mismatch '{n₁}', expected '{n₂}'"
unless (← isDefEq d₁ d₂) do
throwError "parameter '{n₁}' {← mkHasTypeButIsExpectedMsg d₁ d₂}"
unless c₁.binderInfo == c₂.binderInfo do
unless c₁ == c₂ do
throwError "binder annotation mismatch at parameter '{n₁}'"
withLocalDecl n₁ c₁.binderInfo d₁ fun x =>
withLocalDecl n₁ c₁ d₁ fun x =>
let type₁ := b₁.instantiate1 x
let type₂ := b₂.instantiate1 x
forallTelescopeCompatibleAux k i type₁ type₂ (xs.push x)
@ -58,8 +58,8 @@ def mkFreshInstanceName (env : Environment) (nextIdx : Nat) : Name :=
def isFreshInstanceName (name : Name) : Bool :=
match name with
| Name.str _ s _ => "_instance".isPrefixOf s
| _ => false
| .str _ s => "_instance".isPrefixOf s
| _ => false
/--
Sort the given list of `usedParams` using the following order:

10
stage0/src/Lean/Elab/Declaration.lean generated
View file

@ -17,12 +17,12 @@ open TSyntax.Compat
private def ensureValidNamespace (name : Name) : MacroM Unit := do
match name with
| Name.str p s _ =>
| .str p s =>
if s == "_root_" then
Macro.throwError s!"invalid namespace '{name}', '_root_' is a reserved namespace"
ensureValidNamespace p
| Name.num _ .. => Macro.throwError s!"invalid namespace '{name}', it must not contain numeric parts"
| Name.anonymous => return ()
| .num .. => Macro.throwError s!"invalid namespace '{name}', it must not contain numeric parts"
| .anonymous => return ()
/-- Auxiliary function for `expandDeclNamespace?` -/
private def expandDeclIdNamespace? (declId : Syntax) : MacroM (Option (Name × Syntax)) := do
@ -32,8 +32,8 @@ private def expandDeclIdNamespace? (declId : Syntax) : MacroM (Option (Name × S
return none
let scpView := extractMacroScopes id
match scpView.name with
| Name.str Name.anonymous _ _ => return none
| Name.str pre s _ =>
| .str .anonymous _ => return none
| .str pre s =>
ensureValidNamespace pre
let nameNew := { scpView with name := Name.mkSimple s }.review
-- preserve "original" info, if any, so that hover etc. on the namespaced

2
stage0/src/Lean/Elab/DefView.lean generated
View file

@ -91,7 +91,7 @@ def mkInstanceName (binders : Array Syntax) (type : Syntax) : CommandElabM Name
else if e.isSort then ref.modify (· ++ "Sort")
else if e.isConst then
match e.constName!.eraseMacroScopes with
| Name.str _ str _ =>
| .str _ str =>
if str.front.isLower then
ref.modify (· ++ str.capitalize)
else

2
stage0/src/Lean/Elab/Deriving/Inhabited.lean generated
View file

@ -49,7 +49,7 @@ where
else
let visit {ω} : StateRefT IndexSet (ST ω) Unit :=
e.forEach fun
| Expr.fvar fvarId _ =>
| Expr.fvar fvarId =>
match localInst2Index.find? fvarId with
| some idx => modify (·.insert idx)
| none => pure ()

4
stage0/src/Lean/Elab/Deriving/Util.lean generated
View file

@ -73,8 +73,8 @@ def mkContext (fnPrefix : String) (typeName : Name) : TermElabM Context := do
let mut auxFunNames := #[]
for typeName in indVal.all do
match typeName.eraseMacroScopes with
| Name.str _ t _ => auxFunNames := auxFunNames.push (← mkFreshUserName <| Name.mkSimple <| fnPrefix ++ t)
| _ => auxFunNames := auxFunNames.push (← mkFreshUserName `instFn)
| .str _ t => auxFunNames := auxFunNames.push (← mkFreshUserName <| Name.mkSimple <| fnPrefix ++ t)
| _ => auxFunNames := auxFunNames.push (← mkFreshUserName `instFn)
trace[Elab.Deriving.beq] "{auxFunNames}"
let usePartial := indVal.isNested || typeInfos.size > 1
return {

2
stage0/src/Lean/Elab/Do.lean generated
View file

@ -100,7 +100,7 @@ private def mkUnknownMonadResult : MetaM ExtractMonadResult := do
private partial def extractBind (expectedType? : Option Expr) : TermElabM ExtractMonadResult := do
let some expectedType := expectedType? | mkUnknownMonadResult
let extractStep? (type : Expr) : MetaM (Option ExtractMonadResult) := do
let .app m returnType _ := type | return none
let .app m returnType := type | return none
try
let bindInstType ← mkAppM ``Bind #[m]
discard <| Meta.synthInstance bindInstType

2
stage0/src/Lean/Elab/Extra.lean generated
View file

@ -171,7 +171,7 @@ private def isUnknow : Expr → Bool
| Expr.mvar .. => true
| Expr.app f .. => isUnknow f
| Expr.letE _ _ _ b _ => isUnknow b
| Expr.mdata _ b _ => isUnknow b
| Expr.mdata _ b => isUnknow b
| _ => false
private def analyze (t : Tree) (expectedType? : Option Expr) : TermElabM AnalyzeResult := do

30
stage0/src/Lean/Elab/Inductive.lean generated
View file

@ -204,7 +204,7 @@ where
go (type : Expr) (acc : Array Name) : Array Name :=
match type with
| .forallE n _ b _ => go b (acc.push n)
| .mdata _ b _ => go b acc
| .mdata _ b => go b acc
| _ => acc
/--
@ -217,11 +217,11 @@ where
go (type : Expr) (i : Nat) : Expr :=
if i < newNames.size then
match type with
| .forallE n d b data =>
| .forallE n d b bi =>
if n.hasMacroScopes then
mkForall newNames[i]! data.binderInfo d (go b (i+1))
mkForall newNames[i]! bi d (go b (i+1))
else
mkForall n data.binderInfo d (go b (i+1))
mkForall n bi d (go b (i+1))
| _ => type
else
type
@ -386,8 +386,8 @@ private def getResultingUniverse : List InductiveType → TermElabM Level
| indType :: _ => forallTelescopeReducing indType.type fun _ r => do
let r ← whnfD r
match r with
| Expr.sort u _ => return u
| _ => throwError "unexpected inductive type resulting type{indentExpr r}"
| Expr.sort u => return u
| _ => throwError "unexpected inductive type resulting type{indentExpr r}"
/--
Return `some ?m` if `u` is of the form `?m + k`.
@ -397,7 +397,7 @@ def shouldInferResultUniverse (u : Level) : TermElabM (Option MVarId) := do
let u ← instantiateLevelMVars u
if u.hasMVar then
match u.getLevelOffset with
| Level.mvar mvarId _ => return some mvarId
| Level.mvar mvarId => return some mvarId
| _ =>
throwError "cannot infer resulting universe level of inductive datatype, given level contains metavariables {mkSort u}, provide universe explicitly"
else
@ -447,11 +447,11 @@ def accLevel (u : Level) (r : Level) (rOffset : Nat) : OptionT (StateT (Array Le
where
go (u : Level) (rOffset : Nat) : OptionT (StateT (Array Level) Id) Unit := do
match u, rOffset with
| .max u v _, rOffset => go u rOffset; go v rOffset
| .imax u v _, rOffset => go u rOffset; go v rOffset
| .zero _, _ => return ()
| .succ u _, rOffset+1 => go u rOffset
| u, rOffset =>
| .max u v, rOffset => go u rOffset; go v rOffset
| .imax u v, rOffset => go u rOffset; go v rOffset
| .zero, _ => return ()
| .succ u, rOffset+1 => go u rOffset
| u, rOffset =>
if rOffset == 0 && u == r then
return ()
else if r.occurs u then
@ -546,8 +546,8 @@ private def checkResultingUniverses (views : Array InductiveView) (numParams : N
let v := (← instantiateLevelMVars (← getLevel type)).normalize
let rec check (v' : Level) (u' : Level) : TermElabM Unit :=
match v', u' with
| .succ v' _, .succ u' _ => check v' u'
| .mvar id _, .param .. =>
| .succ v', .succ u' => check v' u'
| .mvar id, .param .. =>
/- Special case:
The constructor parameter `v` is at unverse level `?v+k` and
the resulting inductive universe level is `u'+k`, where `u'` is a parameter (or zero).
@ -563,7 +563,7 @@ private def checkResultingUniverses (views : Array InductiveView) (numParams : N
-----------------------------------------------------------
-/
assignLevelMVar id u'
| .mvar id _, .zero _ => assignLevelMVar id u' -- TODO: merge with previous case
| .mvar id, .zero => assignLevelMVar id u' -- TODO: merge with previous case
| _, _ =>
unless u.geq v do
let mut msg := m!"invalid universe level in constructor '{ctor.name}', parameter"

30
stage0/src/Lean/Elab/Match.lean generated
View file

@ -26,8 +26,8 @@ private def expandSimpleMatch (stx : Syntax) (discr : Term) (lhsVar : Ident) (rh
private def mkUserNameFor (e : Expr) : TermElabM Name := do
match e with
/- Remark: we use `mkFreshUserName` to make sure we don't add a variable to the local context that can be resolved to `e`. -/
| Expr.fvar fvarId _ => mkFreshUserName ((← getLocalDecl fvarId).userName)
| _ => mkFreshBinderName
| Expr.fvar fvarId => mkFreshUserName ((← getLocalDecl fvarId).userName)
| _ => mkFreshBinderName
/--
@ -59,7 +59,7 @@ def isAtomicDiscr? (discr : Syntax) : TermElabM (Option Expr) := do
private def elabAtomicDiscr (discr : Syntax) : TermElabM Expr := do
let term := discr[1]
match (← isAtomicDiscr? term) with
| some e@(Expr.fvar fvarId _) =>
| some e@(Expr.fvar fvarId) =>
let localDecl ← getLocalDecl fvarId
if !isAuxDiscrName localDecl.userName then
addTermInfo discr e -- it is not an auxiliary local created by `expandNonAtomicDiscrs?`
@ -536,7 +536,7 @@ where
processInaccessible (e : Expr) : M Expr := do
let e' ← erasePatternRefAnnotations e
match e' with
| Expr.fvar _ _ =>
| Expr.fvar _ =>
if (← isExplicitPatternVar e') then
processVar e
else
@ -582,8 +582,8 @@ private partial def toPattern (e : Expr) : MetaM Pattern := do
if let some e := Match.isNamedPattern? e then
let p ← toPattern <| e.getArg! 2
match e.getArg! 1, e.getArg! 3 with
| Expr.fvar x _, Expr.fvar h _ => return Pattern.as x p h
| _, _ => throwError "unexpected occurrence of auxiliary declaration 'namedPattern'"
| Expr.fvar x, Expr.fvar h => return Pattern.as x p h
| _, _ => throwError "unexpected occurrence of auxiliary declaration 'namedPattern'"
else if isMatchValue e then
return Pattern.val e
else if e.isFVar then
@ -615,13 +615,13 @@ private partial def topSort (patternVars : Array Expr) : TermElabM (Array Expr)
where
visit (e : Expr) : TopSortM Unit := do
match e with
| Expr.proj _ _ e _ => visit e
| Expr.proj _ _ e => visit e
| Expr.forallE _ d b _ => visit d; visit b
| Expr.lam _ d b _ => visit d; visit b
| Expr.letE _ t v b _ => visit t; visit v; visit b
| Expr.app f a _ => visit f; visit a
| Expr.mdata _ b _ => visit b
| Expr.mvar mvarId _ =>
| Expr.app f a => visit f; visit a
| Expr.mdata _ b => visit b
| Expr.mvar mvarId =>
let v ← instantiateMVars e
if !v.isMVar then
visit v
@ -631,7 +631,7 @@ where
let mvarDecl ← getMVarDecl mvarId
visit mvarDecl.type
modify fun s => { s with result := s.result.push e }
| Expr.fvar fvarId _ =>
| Expr.fvar fvarId =>
if patternVars.contains e then
unless (← get).visitedFVars.contains fvarId do
modify fun s => { s with visitedFVars := s.visitedFVars.insert fvarId }
@ -652,9 +652,9 @@ where
| .forallE n d b _ => withLocalDecl n b.binderInfo (← go d) fun x => do mkForallFVars #[x] (← go (b.instantiate1 x))
| .lam n d b _ => withLocalDecl n b.binderInfo (← go d) fun x => do mkLambdaFVars #[x] (← go (b.instantiate1 x))
| .letE n t v b .. => withLetDecl n (← go t) (← go v) fun x => do mkLetFVars #[x] (← go (b.instantiate1 x))
| .app f a _ => return mkApp (← go f) (← go a)
| .proj _ _ b _ => return p.updateProj! (← go b)
| .mdata k b _ =>
| .app f a => return mkApp (← go f) (← go a)
| .proj _ _ b => return p.updateProj! (← go b)
| .mdata k b =>
if inaccessible? p |>.isSome then
return mkMData k (← withReader (fun _ => false) (go b))
else if let some (stx, p) := patternWithRef? p then
@ -1229,7 +1229,7 @@ private def isPatternVar (stx : Syntax) : TermElabM Bool := do
match (← resolveId? stx "pattern") with
| none => return isAtomicIdent stx
| some f => match f with
| Expr.const fName _ _ =>
| Expr.const fName _ =>
match (← getEnv).find? fName with
| some (ConstantInfo.ctorInfo _) => return false
| some _ => return !hasMatchPatternAttribute (← getEnv) fName

22
stage0/src/Lean/Elab/MutualDef.lean generated
View file

@ -248,10 +248,10 @@ private def instantiateMVarsAtLetRecToLift (toLift : LetRecToLift) : TermElabM L
private def typeHasRecFun (type : Expr) (funFVars : Array Expr) (letRecsToLift : List LetRecToLift) : Option FVarId :=
let occ? := type.find? fun e => match e with
| Expr.fvar fvarId _ => funFVars.contains e || letRecsToLift.any fun toLift => toLift.fvarId == fvarId
| Expr.fvar fvarId => funFVars.contains e || letRecsToLift.any fun toLift => toLift.fvarId == fvarId
| _ => false
match occ? with
| some (Expr.fvar fvarId _) => some fvarId
| some (Expr.fvar fvarId) => some fvarId
| _ => none
private def getFunName (fvarId : FVarId) (letRecsToLift : List LetRecToLift) : TermElabM Name := do
@ -565,7 +565,7 @@ def insertReplacementForLetRecs (r : Replacement) (letRecClosures : List LetRecC
def Replacement.apply (r : Replacement) (e : Expr) : Expr :=
e.replace fun e => match e with
| Expr.fvar fvarId _ => match r.find? fvarId with
| Expr.fvar fvarId => match r.find? fvarId with
| some c => some c
| _ => none
| _ => none
@ -740,9 +740,9 @@ partial def checkForHiddenUnivLevels (allUserLevelNames : List Name) (preDefs :
-- Otherwise, we try to produce an error message containing the expression with the offending universe
let rec visitLevel (u : Level) : ReaderT Expr TermElabM Unit := do
match u with
| .succ u _ => visitLevel u
| .imax u v _ | .max u v _ => visitLevel u; visitLevel v
| .param n _ =>
| .succ u => visitLevel u
| .imax u v | .max u v => visitLevel u; visitLevel v
| .param n =>
unless sTypes.visitedLevel.contains u || allUserLevelNames.contains n do
let parent ← withOptions (fun o => pp.universes.set o true) do addMessageContext m!"{indentExpr (← read)}"
let body ← withOptions (fun o => pp.letVarTypes.setIfNotSet (pp.funBinderTypes.setIfNotSet o true) true) do addMessageContext m!"{indentExpr preDef.value}"
@ -751,13 +751,13 @@ partial def checkForHiddenUnivLevels (allUserLevelNames : List Name) (preDefs :
let rec visit (e : Expr) : ReaderT Expr (MonadCacheT ExprStructEq Unit TermElabM) Unit := do
checkCache { val := e : ExprStructEq } fun _ => do
match e with
| .forallE n d b c | .lam n d b c => visit d e; withLocalDecl n c.binderInfo d fun x => visit (b.instantiate1 x) e
| .forallE n d b c | .lam n d b c => visit d e; withLocalDecl n c d fun x => visit (b.instantiate1 x) e
| .letE n t v b _ => visit t e; visit v e; withLetDecl n t v fun x => visit (b.instantiate1 x) e
| .app .. => e.withApp fun f args => do visit f e; args.forM fun arg => visit arg e
| .mdata _ b _ => visit b e
| .proj _ _ b _ => visit b e
| .sort u _ => visitLevel u (← read)
| .const _ us _ => us.forM (visitLevel · (← read))
| .mdata _ b => visit b e
| .proj _ _ b => visit b e
| .sort u => visitLevel u (← read)
| .const _ us => us.forM (visitLevel · (← read))
| _ => pure ()
visit preDef.value preDef.value |>.run {}
for preDef in preDefs do

4
stage0/src/Lean/Elab/PatternVar.lean generated
View file

@ -236,7 +236,7 @@ where
match (← resolveId? stx "pattern") with
| none => processVar stx
| some f => match f with
| Expr.const fName _ _ =>
| Expr.const fName _ =>
match (← getEnv).find? fName with
| some (ConstantInfo.ctorInfo _) => processCtor stx
| some _ =>
@ -296,7 +296,7 @@ where
| `($fId:ident) => pure (fId, false)
| `(@$fId:ident) => pure (fId, true)
| _ => throwError "identifier expected"
let some (Expr.const fName _ _) ← resolveId? fId "pattern" (withInfo := true) | throwCtorExpected
let some (Expr.const fName _) ← resolveId? fId "pattern" (withInfo := true) | throwCtorExpected
let fInfo ← getConstInfo fName
let paramDecls ← forallTelescopeReducing fInfo.type fun xs _ => xs.mapM fun x => do
let d ← getFVarLocalDecl x

4
stage0/src/Lean/Elab/PreDefinition/Basic.lean generated
View file

@ -55,7 +55,7 @@ def fixLevelParams (preDefs : Array PreDefinition) (scopeLevelNames allUserLevel
let us := levelParams.map mkLevelParam
let fixExpr (e : Expr) : Expr :=
e.replace fun c => match c with
| Expr.const declName _ _ => if preDefs.any fun preDef => preDef.declName == declName then some $ Lean.mkConst declName us else none
| Expr.const declName _ => if preDefs.any fun preDef => preDef.declName == declName then some $ Lean.mkConst declName us else none
| _ => none
return preDefs.map fun preDef =>
{ preDef with
@ -173,7 +173,7 @@ def addAndCompilePartialRec (preDefs : Array PreDefinition) : TermElabM Unit :=
{ preDef with
declName := Compiler.mkUnsafeRecName preDef.declName
value := preDef.value.replace fun e => match e with
| Expr.const declName us _ =>
| Expr.const declName us =>
if preDefs.any fun preDef => preDef.declName == declName then
some <| mkConst (Compiler.mkUnsafeRecName declName) us
else

10
stage0/src/Lean/Elab/PreDefinition/Eqns.lean generated
View file

@ -20,7 +20,7 @@ structure EqnInfoCore where
partial def expand : Expr → Expr
| Expr.letE _ _ v b _ => expand (b.instantiate1 v)
| Expr.mdata _ b _ => expand b
| Expr.mdata _ b => expand b
| e => e
def expandRHS? (mvarId : MVarId) : MetaM (Option MVarId) := do
@ -115,7 +115,7 @@ def simpEqnType (eqnType : Expr) : MetaM Expr := do
for y in ys.reverse do
trace[Elab.definition] ">> simpEqnType: {← inferType y}, {type}"
if proofVars.contains y.fvarId! then
let some (_, Expr.fvar fvarId _, rhs) ← matchEq? (← inferType y) | throwError "unexpected hypothesis in altenative{indentExpr eqnType}"
let some (_, Expr.fvar fvarId, rhs) ← matchEq? (← inferType y) | throwError "unexpected hypothesis in altenative{indentExpr eqnType}"
eliminated := eliminated.insert fvarId
type := type.replaceFVarId fvarId rhs
else if eliminated.contains y.fvarId! then
@ -250,10 +250,10 @@ def removeUnusedEqnHypotheses (declType declValue : Expr) : CoreM (Expr × Expr)
where
go (type value : Expr) (xs : Array Expr) (lctx : LocalContext) : CoreM (Expr × Expr) := do
match value with
| .lam n d b i =>
| .lam n d b bi =>
let d := d.instantiateRev xs
let fvarId ← mkFreshFVarId
go (type.bindingBody!) b (xs.push (mkFVar fvarId)) (lctx.mkLocalDecl fvarId n d i.binderInfo)
go (type.bindingBody!) b (xs.push (mkFVar fvarId)) (lctx.mkLocalDecl fvarId n d bi)
| _ =>
let type := type.instantiateRev xs
let value := value.instantiateRev xs
@ -286,7 +286,7 @@ private partial def whnfAux (e : Expr) : MetaM Expr := do
let e ← whnfI e -- Must reduce instances too, otherwise it will not be able to reduce `(Nat.rec ... ... (OfNat.ofNat 0))`
let f := e.getAppFn
match f with
| Expr.proj _ _ s _ => return mkAppN (f.updateProj! (← whnfAux s)) e.getAppArgs
| Expr.proj _ _ s => return mkAppN (f.updateProj! (← whnfAux s)) e.getAppArgs
| _ => return e
/-- Apply `whnfR` to lhs, return `none` if `lhs` was not modified -/

2
stage0/src/Lean/Elab/PreDefinition/Main.lean generated
View file

@ -33,7 +33,7 @@ private def addAndCompilePartial (preDefs : Array PreDefinition) (useSorry := fa
private def isNonRecursive (preDef : PreDefinition) : Bool :=
Option.isNone $ preDef.value.find? fun
| Expr.const declName _ _ => preDef.declName == declName
| Expr.const declName _ => preDef.declName == declName
| _ => false
private def partitionPreDefs (preDefs : Array PreDefinition) : Array (Array PreDefinition) :=

16
stage0/src/Lean/Elab/PreDefinition/Structural/BRecOn.lean generated
View file

@ -21,11 +21,11 @@ private partial def toBelowAux (C : Expr) (belowDict : Expr) (arg : Expr) (F : E
let belowDict ← whnf belowDict
trace[Elab.definition.structural] "belowDict: {belowDict}, arg: {arg}"
match belowDict with
| Expr.app (Expr.app (Expr.const `PProd _ _) d1 _) d2 _ =>
| .app (.app (.const `PProd _) d1) d2 =>
(do toBelowAux C d1 arg (← mkAppM `PProd.fst #[F]))
<|>
(do toBelowAux C d2 arg (← mkAppM `PProd.snd #[F]))
| Expr.app (Expr.app (Expr.const `And _ _) d1 _) d2 _ =>
| .app (.app (.const `And _) d1) d2 =>
(do toBelowAux C d1 arg (← mkAppM `And.left #[F]))
<|>
(do toBelowAux C d2 arg (← mkAppM `And.right #[F]))
@ -37,7 +37,7 @@ private partial def toBelowAux (C : Expr) (belowDict : Expr) (arg : Expr) (F : E
let argTailArgs := argArgs.extract (n - xs.size) n
let belowDict := belowDict.replaceFVars xs argTailArgs
match belowDict with
| Expr.app belowDictFun belowDictArg _ =>
| .app belowDictFun belowDictArg =>
unless belowDictFun.getAppFn == C do throwToBelowFailed
unless ← isDefEq belowDictArg arg do throwToBelowFailed
pure (mkAppN F argTailArgs)
@ -105,21 +105,21 @@ private partial def replaceRecApps (recFnName : Name) (recArgInfo : RecArgInfo)
return e
match e with
| Expr.lam n d b c =>
withLocalDecl n c.binderInfo (← loop below d) fun x => do
withLocalDecl n c (← loop below d) fun x => do
mkLambdaFVars #[x] (← loop below (b.instantiate1 x))
| Expr.forallE n d b c =>
withLocalDecl n c.binderInfo (← loop below d) fun x => do
withLocalDecl n c (← loop below d) fun x => do
mkForallFVars #[x] (← loop below (b.instantiate1 x))
| Expr.letE n type val body _ =>
withLetDecl n (← loop below type) (← loop below val) fun x => do
mkLetFVars #[x] (← loop below (body.instantiate1 x)) (usedLetOnly := false)
| Expr.mdata d b _ =>
| Expr.mdata d b =>
if let some _ := getRecAppSyntax? e then
loop below b
else
return mkMData d (← loop below b)
| Expr.proj n i e _ => return mkProj n i (← loop below e)
| Expr.app _ _ _ =>
| Expr.proj n i e => return mkProj n i (← loop below e)
| Expr.app _ _ =>
let processApp (e : Expr) : StateRefT (HasConstCache recFnName) M Expr :=
e.withApp fun f args => do
if f.isConstOf recFnName then

10
stage0/src/Lean/Elab/PreDefinition/Structural/IndPred.lean generated
View file

@ -15,17 +15,17 @@ private partial def replaceIndPredRecApps (recFnName : Name) (recArgInfo : RecAr
let rec loop (e : Expr) : M Expr := do
match e with
| Expr.lam n d b c =>
withLocalDecl n c.binderInfo (← loop d) fun x => do
withLocalDecl n c (← loop d) fun x => do
mkLambdaFVars #[x] (← loop (b.instantiate1 x))
| Expr.forallE n d b c =>
withLocalDecl n c.binderInfo (← loop d) fun x => do
withLocalDecl n c (← loop d) fun x => do
mkForallFVars #[x] (← loop (b.instantiate1 x))
| Expr.letE n type val body _ =>
withLetDecl n (← loop type) (← loop val) fun x => do
mkLetFVars #[x] (← loop (body.instantiate1 x))
| Expr.mdata d e _ => return mkMData d (← loop e)
| Expr.proj n i e _ => return mkProj n i (← loop e)
| Expr.app _ _ _ =>
| Expr.mdata d e => return mkMData d (← loop e)
| Expr.proj n i e => return mkProj n i (← loop e)
| Expr.app _ _ =>
let processApp (e : Expr) : M Expr := do
e.withApp fun f args => do
if f.isConstOf recFnName then

4
stage0/src/Lean/Elab/PreDefinition/Structural/SmartUnfolding.lean generated
View file

@ -32,8 +32,8 @@ where
| Expr.forallE .. => forallTelescope e fun xs b => do mkForallFVars xs (← visit b)
| Expr.letE n type val body _ =>
withLetDecl n type (← visit val) fun x => do mkLetFVars #[x] (← visit (body.instantiate1 x))
| Expr.mdata d b _ => return mkMData d (← visit b)
| Expr.proj n i s _ => return mkProj n i (← visit s)
| Expr.mdata d b => return mkMData d (← visit b)
| Expr.proj n i s => return mkProj n i (← visit s)
| Expr.app .. =>
let processApp (e : Expr) : MetaM Expr :=
e.withApp fun f args =>

8
stage0/src/Lean/Elab/PreDefinition/WF/Fix.lean generated
View file

@ -63,20 +63,20 @@ where
return e
match e with
| Expr.lam n d b c =>
withLocalDecl n c.binderInfo (← loop F d) fun x => do
withLocalDecl n c (← loop F d) fun x => do
mkLambdaFVars #[x] (← loop F (b.instantiate1 x))
| Expr.forallE n d b c =>
withLocalDecl n c.binderInfo (← loop F d) fun x => do
withLocalDecl n c (← loop F d) fun x => do
mkForallFVars #[x] (← loop F (b.instantiate1 x))
| Expr.letE n type val body _ =>
withLetDecl n (← loop F type) (← loop F val) fun x => do
mkLetFVars #[x] (← loop F (body.instantiate1 x)) (usedLetOnly := false)
| Expr.mdata d b _ =>
| Expr.mdata d b =>
if let some stx := getRecAppSyntax? e then
withRef stx <| loop F b
else
return mkMData d (← loop F b)
| Expr.proj n i e _ => return mkProj n i (← loop F e)
| Expr.proj n i e => return mkProj n i (← loop F e)
| Expr.const .. => if e.isConstOf recFnName then processRec F e else return e
| Expr.app .. =>
match (← matchMatcherApp? e) with

6
stage0/src/Lean/Elab/PreDefinition/WF/PackDomain.lean generated
View file

@ -131,16 +131,16 @@ where
checkCache { val := e : ExprStructEq } fun _ => Meta.withIncRecDepth do
match e with
| Expr.lam n d b c =>
withLocalDecl n c.binderInfo (← visit d) fun x => do
withLocalDecl n c (← visit d) fun x => do
mkLambdaFVars (usedLetOnly := false) #[x] (← visit (b.instantiate1 x))
| Expr.forallE n d b c =>
withLocalDecl n c.binderInfo (← visit d) fun x => do
withLocalDecl n c (← visit d) fun x => do
mkForallFVars (usedLetOnly := false) #[x] (← visit (b.instantiate1 x))
| Expr.letE n t v b _ =>
withLetDecl n (← visit t) (← visit v) fun x => do
mkLambdaFVars (usedLetOnly := false) #[x] (← visit (b.instantiate1 x))
| Expr.proj n i s .. => return mkProj n i (← visit s)
| Expr.mdata d b _ => return mkMData d (← visit b)
| Expr.mdata d b => return mkMData d (← visit b)
| Expr.app .. => visitApp e
| Expr.const .. => visitApp e
| e => return e,

4
stage0/src/Lean/Elab/Quotation.lean generated
View file

@ -60,7 +60,7 @@ def resolveSectionVariable (sectionVars : NameMap Name) (id : Name) : List (Name
-- decode macro scopes from name before recursion
let extractionResult := extractMacroScopes id
let rec loop : Name → List String → List (Name × List String)
| id@(Name.str p s _), projs =>
| id@(.str p s), projs =>
-- NOTE: we assume that macro scopes always belong to the projected constant, not the projections
let id := { extractionResult with name := id }.review
match sectionVars.find? id with
@ -179,7 +179,7 @@ def getQuotKind (stx : Syntax) : TermElabM SyntaxNodeKind := do
| ``Parser.Term.attr.quot => pure `attr
| ``Parser.Term.prio.quot => pure `prio
| ``Parser.Term.doElem.quot => pure `doElem
| Name.str kind "quot" _ => return kind
| .str kind "quot" => return kind
| ``dynamicQuot =>
match (← resolveGlobalConst stx[1]) with
| [parser] => pure parser

2
stage0/src/Lean/Elab/RecAppSyntax.lean generated
View file

@ -21,7 +21,7 @@ def mkRecAppWithSyntax (e : Expr) (stx : Syntax) : Expr :=
-/
def getRecAppSyntax? (e : Expr) : Option Syntax :=
match e with
| Expr.mdata d _ _ =>
| Expr.mdata d _ =>
match d.find recAppKey with
| some (DataValue.ofSyntax stx) => some stx
| _ => none

22
stage0/src/Lean/Elab/StructInst.lean generated
View file

@ -209,7 +209,7 @@ private def getStructName (expectedType? : Option Expr) (sourceView : Source) :
| some expectedType =>
let expectedType ← whnf expectedType
match expectedType.getAppFn with
| Expr.const constName _ _ =>
| Expr.const constName _ =>
unless isStructure (← getEnv) constName do
throwError "invalid \{...} notation, structure type expected{indentExpr expectedType}"
return constName
@ -425,8 +425,8 @@ private def expandParentFields (s : Struct) : TermElabM Struct := do
else match getPathToBaseStructure? env baseStructName s.structName with
| some path =>
let path := path.map fun funName => match funName with
| .str _ s _ => .fieldName ref (Name.mkSimple s)
| _ => unreachable!
| .str _ s => .fieldName ref (Name.mkSimple s)
| _ => unreachable!
return { field with lhs := path ++ field.lhs }
| _ => throwErrorAt ref "failed to access field '{fieldName}' in parent structure"
| _ => return field
@ -559,7 +559,7 @@ private def mkCtorHeaderAux : Nat → Expr → Expr → Array MVarId → Array (
| n+1, type, ctorFn, instMVars, params => do
match (← whnfForall type) with
| .forallE paramName d b c =>
match c.binderInfo with
match c with
| .instImplicit =>
let a ← mkFreshExprMVar d .synthetic
mkCtorHeaderAux n (b.instantiate1 a) (mkApp ctorFn a) (instMVars.push a.mvarId!) (params.push (paramName, a))
@ -705,8 +705,8 @@ partial def findDefaultMissing? [Monad m] [MonadMCtx m] (struct : Struct) : m (O
| _ => match field.expr? with
| none => unreachable!
| some expr => match defaultMissing? expr with
| some (.mvar mvarId _) => return if (← isExprMVarAssigned mvarId) then none else some field
| _ => return none
| some (.mvar mvarId) => return if (← isExprMVarAssigned mvarId) then none else some field
| _ => return none
def getFieldName (field : Field Struct) : Name :=
match field.lhs with
@ -727,7 +727,7 @@ def getFieldValue? (struct : Struct) (fieldName : Name) : Option Expr :=
partial def mkDefaultValueAux? (struct : Struct) : Expr → TermElabM (Option Expr)
| .lam n d b c => withRef struct.ref do
if c.binderInfo.isExplicit then
if c.isExplicit then
let fieldName := n
match getFieldValue? struct fieldName with
| none => return none
@ -764,7 +764,7 @@ partial def reduce (structNames : Array Name) (e : Expr) : MetaM Expr := do
| .lam .. => lambdaLetTelescope e fun xs b => do mkLambdaFVars xs (← reduce structNames b)
| .forallE .. => forallTelescope e fun xs b => do mkForallFVars xs (← reduce structNames b)
| .letE .. => lambdaLetTelescope e fun xs b => do mkLetFVars xs (← reduce structNames b)
| .proj _ i b _ =>
| .proj _ i b =>
match (← Meta.project? b i) with
| some r => reduce structNames r
| none => return e.updateProj! (← reduce structNames b)
@ -780,13 +780,13 @@ partial def reduce (structNames : Array Name) (e : Expr) : MetaM Expr := do
else
let args ← e.getAppArgs.mapM (reduce structNames)
return mkAppN f' args
| .mdata _ b _ =>
| .mdata _ b =>
let b ← reduce structNames b
if (defaultMissing? e).isSome && !b.isMVar then
return b
else
return e.updateMData! b
| .mvar mvarId _ =>
| .mvar mvarId =>
match (← getExprMVarAssignment? mvarId) with
| some val => if val.isMVar then pure val else reduce structNames val
| none => return e
@ -828,7 +828,7 @@ partial def step (struct : Struct) : M Unit :=
| none => unreachable!
| some expr =>
match defaultMissing? expr with
| some (.mvar mvarId _) =>
| some (.mvar mvarId) =>
unless (← isExprMVarAssigned mvarId) do
let ctx ← read
if (← withRef field.ref <| tryToSynthesizeDefault ctx.structs ctx.allStructNames ctx.maxDistance (getFieldName field) mvarId) then

14
stage0/src/Lean/Elab/Structure.lean generated
View file

@ -373,7 +373,7 @@ where
go? (e : Expr) : TermElabM (Option Expr) := do
match e with
| Expr.lam n d b c =>
if c.binderInfo.isExplicit then
if c.isExplicit then
match fieldMap.find? n with
| none => failed
| some val =>
@ -446,7 +446,7 @@ where
mkCompositeField (parentType : Expr) (fieldMap : FieldMap) : TermElabM Expr := do
let env ← getEnv
let Expr.const parentStructName us _ ← pure parentType.getAppFn | unreachable!
let Expr.const parentStructName us ← pure parentType.getAppFn | unreachable!
let parentCtor := getStructureCtor env parentStructName
let mut result := mkAppN (mkConst parentCtor.name us) parentType.getAppArgs
for fieldName in getStructureFields env parentStructName do
@ -570,8 +570,8 @@ where
private def getResultUniverse (type : Expr) : TermElabM Level := do
let type ← whnf type
match type with
| Expr.sort u _ => pure u
| _ => throwError "unexpected structure resulting type"
| Expr.sort u => pure u
| _ => throwError "unexpected structure resulting type"
private def collectUsed (params : Array Expr) (fieldInfos : Array StructFieldInfo) : StateRefT CollectFVars.State MetaM Unit := do
params.forM fun p => do
@ -642,7 +642,7 @@ private def updateResultingUniverse (fieldInfos : Array StructFieldInfo) (type :
let rOffset : Nat := r.getOffset
let r : Level := r.getLevelOffset
match r with
| Level.mvar mvarId _ =>
| Level.mvar mvarId =>
let us ← collectUniversesFromFields r rOffset fieldInfos
let rNew := mkResultUniverse us rOffset
assignLevelMVar mvarId rNew
@ -746,13 +746,13 @@ private partial def mkCoercionToCopiedParent (levelParams : List Name) (params :
let structName := view.declName
let sourceFieldNames := getStructureFieldsFlattened env structName
let structType := mkAppN (Lean.mkConst structName (levelParams.map mkLevelParam)) params
let Expr.const parentStructName _ _ ← pure parentType.getAppFn | unreachable!
let Expr.const parentStructName _ ← pure parentType.getAppFn | unreachable!
let binfo := if view.isClass && isClass env parentStructName then BinderInfo.instImplicit else BinderInfo.default
withLocalDecl `self binfo structType fun source => do
let declType ← instantiateMVars (← mkForallFVars params (← mkForallFVars #[source] parentType))
let declType := declType.inferImplicit params.size true
let rec copyFields (parentType : Expr) : MetaM Expr := do
let Expr.const parentStructName us _ ← pure parentType.getAppFn | unreachable!
let Expr.const parentStructName us ← pure parentType.getAppFn | unreachable!
let parentCtor := getStructureCtor env parentStructName
let mut result := mkAppN (mkConst parentCtor.name us) parentType.getAppArgs
for fieldName in getStructureFields env parentStructName do

14
stage0/src/Lean/Elab/Syntax.lean generated
View file

@ -80,11 +80,11 @@ def resolveParserName [Monad m] [MonadInfoTree m] [MonadResolveName m] [MonadEnv
| none => none
| some info =>
match info.type with
| Expr.const ``Lean.Parser.TrailingParser _ _ => (c, false)
| Expr.const ``Lean.Parser.Parser _ _ => (c, false)
| Expr.const ``Lean.ParserDescr _ _ => (c, true)
| Expr.const ``Lean.TrailingParserDescr _ _ => (c, true)
| _ => none
| Expr.const ``Lean.Parser.TrailingParser _ => (c, false)
| Expr.const ``Lean.Parser.Parser _ => (c, false)
| Expr.const ``Lean.ParserDescr _ => (c, true)
| Expr.const ``Lean.TrailingParserDescr _ => (c, true)
| _ => none
catch _ => return []
open TSyntax.Compat in
@ -240,7 +240,7 @@ open Lean.Parser.Term hiding macroArg
open Lean.Parser.Command
private def declareSyntaxCatQuotParser (catName : Name) : CommandElabM Unit := do
if let Name.str _ suffix _ := catName then
if let .str _ suffix := catName then
let quotSymbol := "`(" ++ suffix ++ "|"
let name := catName ++ `quot
let cmd ← `(
@ -297,7 +297,7 @@ where
appendCatName (str : String) :=
match catName with
| Name.str _ s _ => s ++ str
| .str _ s => s ++ str
| _ => str
/- We assume a new syntax can be treated as an atom when it starts and ends with a token.

6
stage0/src/Lean/Elab/Tactic/ElabTerm.lean generated
View file

@ -191,8 +191,8 @@ def getFVarId (id : Syntax) : TacticM FVarId := withRef id do
let e ← withMainContext do
elabTermForApply id (mayPostpone := false)
match e with
| Expr.fvar fvarId _ => return fvarId
| _ => throwError "unexpected term '{e}'; expected single reference to variable"
| Expr.fvar fvarId => return fvarId
| _ => throwError "unexpected term '{e}'; expected single reference to variable"
def getFVarIds (ids : Array Syntax) : TacticM (Array FVarId) := do
withMainContext do ids.mapM getFVarId
@ -224,7 +224,7 @@ def elabAsFVar (stx : Syntax) (userName? : Option Name := none) : TacticM FVarId
withMainContext do
let e ← elabTerm stx none
match e with
| Expr.fvar fvarId _ => pure fvarId
| Expr.fvar fvarId => pure fvarId
| _ =>
let type ← inferType e
let intro (userName : Name) (preserveBinderNames : Bool) : TacticM FVarId := do

2
stage0/src/Lean/Elab/Tactic/Induction.lean generated
View file

@ -130,7 +130,7 @@ partial def mkElimApp (elimInfo : ElimInfo) (targets : Array Expr) (tag : Name)
let target ← withAssignableSyntheticOpaque <| Term.ensureHasType expectedType target
modify fun s => { s with targetPos := s.targetPos + 1 }
addNewArg target
else match c.binderInfo with
else match c with
| BinderInfo.implicit =>
let arg ← mkFreshExprMVar (← getArgExpectedType)
addNewArg arg

24
stage0/src/Lean/Elab/Term.lean generated
View file

@ -490,7 +490,7 @@ def getMVarErrorInfo? (mvarId : MVarId) : TermElabM (Option MVarErrorInfo) := do
def registerCustomErrorIfMVar (e : Expr) (ref : Syntax) (msgData : MessageData) : TermElabM Unit :=
match e.getAppFn with
| Expr.mvar mvarId _ => registerMVarErrorCustomInfo mvarId ref msgData
| Expr.mvar mvarId => registerMVarErrorCustomInfo mvarId ref msgData
| _ => pure ()
/-
@ -673,9 +673,9 @@ partial def visit (e : Expr) : M Unit := do
| Expr.forallE _ d b _ => visit d; visit b
| Expr.lam _ d b _ => visit d; visit b
| Expr.letE _ t v b _ => visit t; visit v; visit b
| Expr.app f a _ => visit f; visit a
| Expr.mdata _ b _ => visit b
| Expr.proj _ _ b _ => visit b
| Expr.app f a => visit f; visit a
| Expr.mdata _ b => visit b
| Expr.proj _ _ b => visit b
| Expr.fvar fvarId .. =>
match (← getLocalDecl fvarId) with
| LocalDecl.cdecl .. => return ()
@ -771,7 +771,7 @@ def synthesizeCoeInstMVarCore (instMVar : MVarId) : TermElabM Bool := do
-/
def tryCoeThunk? (expectedType : Expr) (eType : Expr) (e : Expr) : TermElabM (Option Expr) := do
match expectedType with
| Expr.app (Expr.const ``Thunk u _) arg _ =>
| Expr.app (Expr.const ``Thunk u) arg =>
if (← isDefEq eType arg) then
return some (mkApp2 (mkConst ``Thunk.mk u) arg (mkSimpleThunk e))
else
@ -819,8 +819,8 @@ private def tryCoe (errorMsgHeader? : Option String) (expectedType : Expr) (eTyp
def isTypeApp? (type : Expr) : TermElabM (Option (Expr × Expr)) := do
let type ← withReducible <| whnf type
match type with
| Expr.app m α _ => return some ((← instantiateMVars m), (← instantiateMVars α))
| _ => return none
| Expr.app m α => return some ((← instantiateMVars m), (← instantiateMVars α))
| _ => return none
/-- Helper method used to implement auto-lift and coercions -/
private def synthesizeInst (type : Expr) : TermElabM Expr := do
@ -1092,7 +1092,7 @@ partial def removeSaveInfoAnnotation (e : Expr) : Expr :=
-/
def isTacticOrPostponedHole? (e : Expr) : TermElabM (Option MVarId) := do
match e with
| Expr.mvar mvarId _ =>
| Expr.mvar mvarId =>
match (← getSyntheticMVarDecl? mvarId) with
| some { kind := SyntheticMVarKind.tactic .., .. } => return mvarId
| some { kind := SyntheticMVarKind.postponed .., .. } => return mvarId
@ -1262,7 +1262,7 @@ private def useImplicitLambda? (stx : Syntax) (expectedType? : Option Expr) : Te
let expectedType ← whnfForall expectedType
match expectedType with
| Expr.forallE _ _ _ c =>
if c.binderInfo.isImplicit || c.binderInfo.isInstImplicit then
if c.isImplicit || c.isInstImplicit then
return some expectedType
else
return none
@ -1299,11 +1299,11 @@ private partial def elabImplicitLambda (stx : Syntax) (catchExPostpone : Bool) (
where
loop
| type@(Expr.forallE n d b c), fvars =>
if c.binderInfo.isExplicit then
if c.isExplicit then
elabImplicitLambdaAux stx catchExPostpone type fvars
else withFreshMacroScope do
let n ← MonadQuotation.addMacroScope n
withLocalDecl n c.binderInfo d fun fvar => do
withLocalDecl n c d fun fvar => do
let type ← whnfForall (b.instantiate1 fvar)
loop type (fvars.push fvar)
| type, fvars =>
@ -1650,7 +1650,7 @@ def resolveLocalName (n : Name) : TermElabM (Option (Expr × List String)) := do
match findLocalDecl? givenNameView (skipAuxDecl := not projs.isEmpty) with
| some decl => some (decl.toExpr, projs)
| none => match n with
| .str pre s _ => loop pre (s::projs)
| .str pre s => loop pre (s::projs)
| _ => none
return loop view.name []

4
stage0/src/Lean/Elab/Util.lean generated
View file

@ -75,8 +75,8 @@ def checkSyntaxNodeKind [Monad m] [MonadEnv m] [MonadError m] (k : Name) : m Nam
else throwError "failed"
def checkSyntaxNodeKindAtNamespaces [Monad m] [MonadEnv m] [MonadError m] (k : Name) : Name → m Name
| n@(Name.str p _ _) => checkSyntaxNodeKind (n ++ k) <|> checkSyntaxNodeKindAtNamespaces k p
| Name.anonymous => checkSyntaxNodeKind k
| n@(.str p _) => checkSyntaxNodeKind (n ++ k) <|> checkSyntaxNodeKindAtNamespaces k p
| .anonymous => checkSyntaxNodeKind k
| _ => throwError "failed"
def checkSyntaxNodeKindAtCurrentNamespaces (k : Name) : AttrM Name := do

14
stage0/src/Lean/Environment.lean generated
View file

@ -695,13 +695,13 @@ def getNamespaceSet (env : Environment) : NameSSet :=
namespacesExt.getState env
private def isNamespaceName : Name → Bool
| Name.str Name.anonymous _ _ => true
| Name.str p _ _ => isNamespaceName p
| _ => false
| .str .anonymous _ => true
| .str p _ => isNamespaceName p
| _ => false
private def registerNamePrefixes : Environment → Name → Environment
| env, Name.str p _ _ => if isNamespaceName p then registerNamePrefixes (registerNamespace env p) p else env
| env, _ => env
| env, .str p _ => if isNamespaceName p then registerNamePrefixes (registerNamespace env p) p else env
| env, _ => env
@[export lean_environment_add]
def add (env : Environment) (cinfo : ConstantInfo) : Environment :=
@ -744,14 +744,14 @@ unsafe def evalConstCheck (α) (env : Environment) (opts : Options) (typeName :
| none => throw ("unknown constant '" ++ toString constName ++ "'")
| some info =>
match info.type with
| Expr.const c _ _ =>
| Expr.const c _ =>
if c != typeName then throwUnexpectedType typeName constName
else env.evalConst α opts constName
| _ => throwUnexpectedType typeName constName
def hasUnsafe (env : Environment) (e : Expr) : Bool :=
let c? := e.find? fun e => match e with
| Expr.const c _ _ =>
| Expr.const c _ =>
match env.find? c with
| some cinfo => cinfo.isUnsafe
| none => false

337
stage0/src/Lean/Expr.lean generated
View file

@ -236,37 +236,69 @@ instance : Inhabited (FVarIdMap α) where
/- We use the `E` suffix (short for `Expr`) to avoid collision with keywords.
We considered using «...», but it is too inconvenient to use. -/
inductive Expr where
| bvar : Nat → Data → Expr -- bound variables
| fvar : FVarId → Data → Expr -- free variables
| mvar : MVarId → Data → Expr -- meta variables
| sort : Level → Data → Expr -- Sort
| const : Name → List Level → Data → Expr -- constants
| app : Expr → Expr → Data → Expr -- application
| lam : Name → Expr → Expr → Data → Expr -- lambda abstraction
| forallE : Name → Expr → Expr → Data → Expr -- (dependent) arrow
| letE : Name → Expr → Expr → Expr → Data → Expr -- let expressions
| lit : Literal → Data → Expr -- literals
| mdata : MData → Expr → Data → Expr -- metadata
| proj : Name → Nat → Expr → Data → Expr -- projection
deriving Inhabited, Repr
| bvar : Nat → Expr -- bound variables
| fvar : FVarId → Expr -- free variables
| mvar : MVarId → Expr -- meta variables
| sort : Level → Expr -- Sort
| const : Name → List Level → Expr -- constants
| app : Expr → Expr → Expr -- application
| lam : Name → Expr → Expr → BinderInfo → Expr -- lambda abstraction
| forallE : Name → Expr → Expr → BinderInfo → Expr -- (dependent) arrow
| letE : Name → Expr → Expr → Expr → Bool → Expr -- let expressions
| lit : Literal → Expr -- literals
| mdata : MData → Expr → Expr -- metadata
| proj : Name → Nat → Expr → Expr -- projection
with
@[computedField, extern c inline "lean_ctor_get_uint64(#1, lean_ctor_num_objs(#1)*sizeof(void*))"]
data : @& Expr → Data
| .const n lvls => mkData (mixHash 5 <| mixHash (hash n) (hash lvls)) 0 0 false false (lvls.any Level.hasMVar) (lvls.any Level.hasParam)
| .bvar idx => mkData (mixHash 7 <| hash idx) (idx+1)
| .sort lvl => mkData (mixHash 11 <| hash lvl) 0 0 false false lvl.hasMVar lvl.hasParam
| .fvar fvarId => mkData (mixHash 13 <| hash fvarId) 0 0 true
| .mvar fvarId => mkData (mixHash 17 <| hash fvarId) 0 0 false true
| .mdata _m e =>
let d := e.data.approxDepth.toUInt32+1
mkData (mixHash d.toUInt64 <| e.data.hash) e.data.looseBVarRange.toNat d e.data.hasFVar e.data.hasExprMVar e.data.hasLevelMVar e.data.hasLevelParam
| .proj s i e =>
let d := e.data.approxDepth.toUInt32+1
mkData (mixHash d.toUInt64 <| mixHash (hash s) <| mixHash (hash i) e.data.hash)
e.data.looseBVarRange.toNat d e.data.hasFVar e.data.hasExprMVar e.data.hasLevelMVar e.data.hasLevelParam
| .app f a => mkAppData f.data a.data
| .lam _x t b bi =>
let d := (max t.data.approxDepth.toUInt32 b.data.approxDepth.toUInt32) + 1
mkDataForBinder (mixHash d.toUInt64 <| mixHash t.data.hash b.data.hash)
(max t.data.looseBVarRange.toNat (b.data.looseBVarRange.toNat - 1))
d
(t.data.hasFVar || b.data.hasFVar)
(t.data.hasExprMVar || b.data.hasExprMVar)
(t.data.hasLevelMVar || b.data.hasLevelMVar)
(t.data.hasLevelParam || b.data.hasLevelParam)
bi
| .forallE _x t b bi =>
let d := (max t.data.approxDepth.toUInt32 b.data.approxDepth.toUInt32) + 1
mkDataForBinder (mixHash d.toUInt64 <| mixHash t.data.hash b.data.hash)
(max t.data.looseBVarRange.toNat (b.data.looseBVarRange.toNat - 1))
d
(t.data.hasFVar || b.data.hasFVar)
(t.data.hasExprMVar || b.data.hasExprMVar)
(t.data.hasLevelMVar || b.data.hasLevelMVar)
(t.data.hasLevelParam || b.data.hasLevelParam)
bi
| .letE _x t v b nonDep =>
let d := (max (max t.data.approxDepth.toUInt32 v.data.approxDepth.toUInt32) b.data.approxDepth.toUInt32) + 1
mkDataForLet (mixHash d.toUInt64 <| mixHash t.data.hash <| mixHash v.data.hash b.data.hash)
(max (max t.data.looseBVarRange.toNat v.data.looseBVarRange.toNat) (b.data.looseBVarRange.toNat - 1))
d
(t.data.hasFVar || v.data.hasFVar || b.data.hasFVar)
(t.data.hasExprMVar || v.data.hasExprMVar || b.data.hasExprMVar)
(t.data.hasLevelMVar || v.data.hasLevelMVar || b.data.hasLevelMVar)
(t.data.hasLevelParam || v.data.hasLevelParam || b.data.hasLevelParam)
nonDep
| .lit l => mkData (mixHash 3 (hash l))
deriving Inhabited, Repr
namespace Expr
@[extern c inline "lean_ctor_get_uint64(#1, lean_ctor_num_objs(#1)*sizeof(void*))"]
def data : (@& Expr) → Data
| bvar _ d => d
| fvar _ d => d
| mvar _ d => d
| sort _ d => d
| const _ _ d => d
| app _ _ d => d
| lam _ _ _ d => d
| forallE _ _ _ d => d
| letE _ _ _ _ d => d
| lit _ d => d
| mdata _ _ d => d
| proj _ _ _ d => d
def ctorName : Expr → String
| bvar .. => "bvar"
| fvar .. => "fvar"
@ -329,7 +361,7 @@ def binderInfo (e : Expr) : BinderInfo :=
end Expr
def mkConst (n : Name) (lvls : List Level := []) : Expr :=
Expr.const n lvls <| mkData (mixHash 5 <| mixHash (hash n) (hash lvls)) 0 0 false false (lvls.any Level.hasMVar) (lvls.any Level.hasParam)
Expr.const n lvls
def Literal.type : Literal → Expr
| Literal.natVal _ => mkConst `Nat
@ -339,52 +371,31 @@ def Literal.type : Literal → Expr
def Literal.typeEx : Literal → Expr := Literal.type
def mkBVar (idx : Nat) : Expr :=
Expr.bvar idx <| mkData (mixHash 7 <| hash idx) (idx+1)
Expr.bvar idx
def mkSort (lvl : Level) : Expr :=
Expr.sort lvl <| mkData (mixHash 11 <| hash lvl) 0 0 false false lvl.hasMVar lvl.hasParam
Expr.sort lvl
def mkFVar (fvarId : FVarId) : Expr :=
Expr.fvar fvarId <| mkData (mixHash 13 <| hash fvarId) 0 0 true
Expr.fvar fvarId
def mkMVar (fvarId : MVarId) : Expr :=
Expr.mvar fvarId <| mkData (mixHash 17 <| hash fvarId) 0 0 false true
Expr.mvar fvarId
def mkMData (m : MData) (e : Expr) : Expr :=
let d := e.approxDepth+1
Expr.mdata m e <| mkData (mixHash d.toUInt64 <| hash e) e.looseBVarRange d e.hasFVar e.hasExprMVar e.hasLevelMVar e.hasLevelParam
Expr.mdata m e
def mkProj (s : Name) (i : Nat) (e : Expr) : Expr :=
let d := e.approxDepth+1
Expr.proj s i e <| mkData (mixHash d.toUInt64 <| mixHash (hash s) <| mixHash (hash i) (hash e))
e.looseBVarRange d e.hasFVar e.hasExprMVar e.hasLevelMVar e.hasLevelParam
Expr.proj s i e
def mkApp (f a : Expr) : Expr :=
Expr.app f a (mkAppData f.data a.data)
Expr.app f a
def mkLambda (x : Name) (bi : BinderInfo) (t : Expr) (b : Expr) : Expr :=
let d := (max t.approxDepth b.approxDepth) + 1
-- let x := x.eraseMacroScopes
Expr.lam x t b <| mkDataForBinder (mixHash d.toUInt64 <| mixHash (hash t) (hash b))
(max t.looseBVarRange (b.looseBVarRange - 1))
d
(t.hasFVar || b.hasFVar)
(t.hasExprMVar || b.hasExprMVar)
(t.hasLevelMVar || b.hasLevelMVar)
(t.hasLevelParam || b.hasLevelParam)
bi
Expr.lam x t b bi
def mkForall (x : Name) (bi : BinderInfo) (t : Expr) (b : Expr) : Expr :=
let d := (max t.approxDepth b.approxDepth) + 1
-- let x := x.eraseMacroScopes
Expr.forallE x t b <| mkDataForBinder (mixHash d.toUInt64 <| mixHash (hash t) (hash b))
(max t.looseBVarRange (b.looseBVarRange - 1))
d
(t.hasFVar || b.hasFVar)
(t.hasExprMVar || b.hasExprMVar)
(t.hasLevelMVar || b.hasLevelMVar)
(t.hasLevelParam || b.hasLevelParam)
bi
Expr.forallE x t b bi
/-- Return `Unit -> type`. Do not confuse with `Thunk type` -/
def mkSimpleThunkType (type : Expr) : Expr :=
@ -395,16 +406,7 @@ def mkSimpleThunk (type : Expr) : Expr :=
mkLambda `_ BinderInfo.default (Lean.mkConst `Unit) type
def mkLet (x : Name) (t : Expr) (v : Expr) (b : Expr) (nonDep : Bool := false) : Expr :=
let d := (max (max t.approxDepth v.approxDepth) b.approxDepth) + 1
-- let x := x.eraseMacroScopes
Expr.letE x t v b <| mkDataForLet (mixHash d.toUInt64 <| mixHash (hash t) <| mixHash (hash v) (hash b))
(max (max t.looseBVarRange v.looseBVarRange) (b.looseBVarRange - 1))
d
(t.hasFVar || v.hasFVar || b.hasFVar)
(t.hasExprMVar || v.hasExprMVar || b.hasExprMVar)
(t.hasLevelMVar || v.hasLevelMVar || b.hasLevelMVar)
(t.hasLevelParam || v.hasLevelParam || b.hasLevelParam)
nonDep
Expr.letE x t v b nonDep
def mkAppB (f a b : Expr) := mkApp (mkApp f a) b
def mkApp2 (f a b : Expr) := mkAppB f a b
@ -418,7 +420,7 @@ def mkApp9 (f a b c d e₁ e₂ e₃ e₄ e₅ : Expr) := mkApp5 (mkApp4 f a b c
def mkApp10 (f a b c d e₁ e₂ e₃ e₄ e₅ e₆ : Expr) := mkApp6 (mkApp4 f a b c d) e₁ e₂ e₃ e₄ e₅ e₆
def mkLit (l : Literal) : Expr :=
Expr.lit l <| mkData (mixHash 3 (hash l))
Expr.lit l
def mkRawNatLit (n : Nat) : Expr :=
mkLit (Literal.natVal n)
@ -490,11 +492,11 @@ def isSort : Expr → Bool
| _ => false
def isType : Expr → Bool
| sort (Level.succ ..) _ => true
| sort (Level.succ ..) => true
| _ => false
def isProp : Expr → Bool
| sort (Level.zero ..) _ => true
| sort (Level.zero ..) => true
| _ => false
def isBVar : Expr → Bool
@ -558,20 +560,20 @@ def getForallBody : Expr → Expr
function applications `f a₁ .. aₙ`, return `f`.
Otherwise return the input expression. -/
def getAppFn : Expr → Expr
| app f _ _ => getAppFn f
| app f _ => getAppFn f
| e => e
def getAppNumArgsAux : Expr → Nat → Nat
| app f _ _, n => getAppNumArgsAux f (n+1)
| _, n => n
| app f _, n => getAppNumArgsAux f (n+1)
| _, n => n
/-- Counts the number `n` of arguments for an expression `f a₁ .. aₙ`. -/
def getAppNumArgs (e : Expr) : Nat :=
getAppNumArgsAux e 0
private def getAppArgsAux : Expr → Array Expr → Nat → Array Expr
| app f a _, as, i => getAppArgsAux f (as.set! i a) (i-1)
| _, as, _ => as
| app f a, as, i => getAppArgsAux f (as.set! i a) (i-1)
| _, as, _ => as
/-- Given `f a₁ a₂ ... aₙ`, returns `#[a₁, ..., aₙ]` -/
@[inline] def getAppArgs (e : Expr) : Array Expr :=
@ -580,16 +582,16 @@ private def getAppArgsAux : Expr → Array Expr → Nat → Array Expr
getAppArgsAux e (mkArray nargs dummy) (nargs-1)
private def getAppRevArgsAux : Expr → Array Expr → Array Expr
| app f a _, as => getAppRevArgsAux f (as.push a)
| _, as => as
| app f a, as => getAppRevArgsAux f (as.push a)
| _, as => as
/-- Same as `getAppArgs` but reverse the output array. -/
@[inline] def getAppRevArgs (e : Expr) : Array Expr :=
getAppRevArgsAux e (Array.mkEmpty e.getAppNumArgs)
@[specialize] def withAppAux (k : Expr → Array Expr → α) : Expr → Array Expr → Nat → α
| app f a _, as, i => withAppAux k f (as.set! i a) (i-1)
| f, as, _ => k f as
| app f a, as, i => withAppAux k f (as.set! i a) (i-1)
| f, as, _ => k f as
/-- Given `e = f a₁ a₂ ... aₙ`, returns `k f #[a₁, ..., aₙ]`. -/
@[inline] def withApp (e : Expr) (k : Expr → Array Expr → α) : α :=
@ -604,22 +606,22 @@ def traverseApp {M} [Monad M]
e.withApp fun fn args => mkAppN <$> f fn <*> args.mapM f
@[specialize] private def withAppRevAux (k : Expr → Array Expr → α) : Expr → Array Expr → α
| app f a _, as => withAppRevAux k f (as.push a)
| f, as => k f as
| app f a, as => withAppRevAux k f (as.push a)
| f, as => k f as
/-- Same as `withApp` but with arguments reversed. -/
@[inline] def withAppRev (e : Expr) (k : Expr → Array Expr → α) : α :=
withAppRevAux k e (Array.mkEmpty e.getAppNumArgs)
def getRevArgD : Expr → Nat → Expr → Expr
| app _ a _, 0, _ => a
| app f _ _, i+1, v => getRevArgD f i v
| _, _, v => v
| app _ a, 0, _ => a
| app f _, i+1, v => getRevArgD f i v
| _, _, v => v
def getRevArg! : Expr → Nat → Expr
| app _ a _, 0 => a
| app f _ _, i+1 => getRevArg! f i
| _, _ => panic! "invalid index"
| app _ a, 0 => a
| app f _, i+1 => getRevArg! f i
| _, _ => panic! "invalid index"
/-- Given `f a₀ a₁ ... aₙ`, returns the `i`th argument or panics if out of bounds. -/
@[inline] def getArg! (e : Expr) (i : Nat) (n := e.getAppNumArgs) : Expr :=
@ -632,87 +634,87 @@ def getRevArg! : Expr → Nat → Expr
/-- Given `f a₀ a₁ ... aₙ`, returns true if `f` is a constant with name `n`. -/
def isAppOf (e : Expr) (n : Name) : Bool :=
match e.getAppFn with
| const c _ _ => c == n
| const c _ => c == n
| _ => false
/-- Given `f a₁ ... aᵢ`, returns true if `f` is a constant
with name `n` and has the correct number of arguments. -/
def isAppOfArity : Expr → Name → Nat → Bool
| const c _ _, n, 0 => c == n
| app f _ _, n, a+1 => isAppOfArity f n a
| _, _, _ => false
| const c _, n, 0 => c == n
| app f _, n, a+1 => isAppOfArity f n a
| _, _, _ => false
/-- Similar to `isAppOfArity` but skips `Expr.mdata`. -/
def isAppOfArity' : Expr → Name → Nat → Bool
| mdata _ b _ , n, a => isAppOfArity' b n a
| const c _ _, n, 0 => c == n
| app f _ _, n, a+1 => isAppOfArity' f n a
| _, _, _ => false
| mdata _ b , n, a => isAppOfArity' b n a
| const c _, n, 0 => c == n
| app f _, n, a+1 => isAppOfArity' f n a
| _, _, _ => false
def appFn! : Expr → Expr
| app f _ _ => f
| _ => panic! "application expected"
| app f _ => f
| _ => panic! "application expected"
def appArg! : Expr → Expr
| app _ a _ => a
| _ => panic! "application expected"
| app _ a => a
| _ => panic! "application expected"
def appFn!' : Expr → Expr
| mdata _ b _ => appFn!' b
| app f _ _ => f
| _ => panic! "application expected"
| mdata _ b => appFn!' b
| app f _ => f
| _ => panic! "application expected"
def appArg!' : Expr → Expr
| mdata _ b _ => appArg!' b
| app _ a _ => a
| _ => panic! "application expected"
| mdata _ b => appArg!' b
| app _ a => a
| _ => panic! "application expected"
def sortLevel! : Expr → Level
| sort u .. => u
| _ => panic! "sort expected"
| sort u => u
| _ => panic! "sort expected"
def litValue! : Expr → Literal
| lit v .. => v
| _ => panic! "literal expected"
| lit v => v
| _ => panic! "literal expected"
def isNatLit : Expr → Bool
| lit (Literal.natVal _) _ => true
| _ => false
| lit (Literal.natVal _) => true
| _ => false
def natLit? : Expr → Option Nat
| lit (Literal.natVal v) _ => v
| _ => none
| lit (Literal.natVal v) => v
| _ => none
def isStringLit : Expr → Bool
| lit (Literal.strVal _) _ => true
| _ => false
| lit (Literal.strVal _) => true
| _ => false
def isCharLit (e : Expr) : Bool :=
e.isAppOfArity ``Char.ofNat 1 && e.appArg!.isNatLit
def constName! : Expr → Name
| const n _ _ => n
| _ => panic! "constant expected"
| const n _ => n
| _ => panic! "constant expected"
def constName? : Expr → Option Name
| const n _ _ => some n
| _ => none
| const n _ => some n
| _ => none
def constLevels! : Expr → List Level
| const _ ls _ => ls
| _ => panic! "constant expected"
| const _ ls => ls
| _ => panic! "constant expected"
def bvarIdx! : Expr → Nat
| bvar idx _ => idx
| _ => panic! "bvar expected"
| bvar idx => idx
| _ => panic! "bvar expected"
def fvarId! : Expr → FVarId
| fvar n _ => n
| _ => panic! "fvar expected"
| fvar n => n
| _ => panic! "fvar expected"
def mvarId! : Expr → MVarId
| mvar n _ => n
| _ => panic! "mvar expected"
| mvar n => n
| _ => panic! "mvar expected"
def bindingName! : Expr → Name
| forallE n _ _ _ => n
@ -730,9 +732,9 @@ def bindingBody! : Expr → Expr
| _ => panic! "binding expected"
def bindingInfo! : Expr → BinderInfo
| forallE _ _ _ c => c.binderInfo
| lam _ _ _ c => c.binderInfo
| _ => panic! "binding expected"
| forallE _ _ _ bi => bi
| lam _ _ _ bi => bi
| _ => panic! "binding expected"
def letName! : Expr → Name
| letE n .. => n
@ -751,20 +753,20 @@ def letBody! : Expr → Expr
| _ => panic! "let expression expected"
def consumeMData : Expr → Expr
| mdata _ e _ => consumeMData e
| e => e
| mdata _ e => consumeMData e
| e => e
def mdataExpr! : Expr → Expr
| mdata _ e _ => e
| _ => panic! "mdata expression expected"
| mdata _ e => e
| _ => panic! "mdata expression expected"
def projExpr! : Expr → Expr
| proj _ _ e _ => e
| _ => panic! "proj expression expected"
| proj _ _ e => e
| _ => panic! "proj expression expected"
def projIdx! : Expr → Nat
| proj _ i _ _ => i
| _ => panic! "proj expression expected"
| proj _ i _ => i
| _ => panic! "proj expression expected"
def hasLooseBVars (e : Expr) : Bool :=
e.looseBVarRange > 0
@ -780,8 +782,9 @@ opaque hasLooseBVar (e : @& Expr) (bvarIdx : @& Nat) : Bool
/-- Return true if `e` contains the loose bound variable `bvarIdx` in an explicit parameter, or in the range if `tryRange == true`. -/
def hasLooseBVarInExplicitDomain : Expr → Nat → Bool → Bool
| Expr.forallE _ d b c, bvarIdx, tryRange => (c.binderInfo.isExplicit && hasLooseBVar d bvarIdx) || hasLooseBVarInExplicitDomain b (bvarIdx+1) tryRange
| e, bvarIdx, tryRange => tryRange && hasLooseBVar e bvarIdx
| Expr.forallE _ d b bi, bvarIdx, tryRange =>
(bi.isExplicit && hasLooseBVar d bvarIdx) || hasLooseBVarInExplicitDomain b (bvarIdx+1) tryRange
| e, bvarIdx, tryRange => tryRange && hasLooseBVar e bvarIdx
/--
Lower the loose bound variables `>= s` in `e` by `d`.
@ -806,9 +809,9 @@ opaque liftLooseBVars (e : @& Expr) (s d : @& Nat) : Expr
When the `{}` annotation is used in these commands, we set `considerRange == false`.
-/
def inferImplicit : Expr → Nat → Bool → Expr
| Expr.forallE n d b c, i+1, considerRange =>
| Expr.forallE n d b bi, i+1, considerRange =>
let b := inferImplicit b i considerRange
let newInfo := if c.binderInfo.isExplicit && hasLooseBVarInExplicitDomain b 0 considerRange then BinderInfo.implicit else c.binderInfo
let newInfo := if bi.isExplicit && hasLooseBVarInExplicitDomain b 0 considerRange then BinderInfo.implicit else bi
mkForall n newInfo d b
| e, 0, _ => e
| e, _, _ => e
@ -953,7 +956,7 @@ partial def betaRev (f : Expr) (revArgs : Array Expr) (useZeta := false) (preser
else
let n := sz - i
mkAppRevRange (e.instantiateRange n sz revArgs) 0 n revArgs
| Expr.mdata k b _=>
| Expr.mdata k b =>
if preserveMData then
let n := sz - i
mkMData k (mkAppRevRange (b.instantiateRange n sz revArgs) 0 n revArgs)
@ -972,7 +975,7 @@ def beta (f : Expr) (args : Array Expr) : Expr :=
def isHeadBetaTargetFn (useZeta : Bool) : Expr → Bool
| Expr.lam .. => true
| Expr.letE _ _ _ b _ => useZeta && isHeadBetaTargetFn useZeta b
| Expr.mdata _ b _ => isHeadBetaTargetFn useZeta b
| Expr.mdata _ b => isHeadBetaTargetFn useZeta b
| _ => false
/-- `(fun x => e) a` ==> `e[x/a]`. -/
@ -984,9 +987,9 @@ def isHeadBetaTarget (e : Expr) (useZeta := false) : Bool :=
e.getAppFn.isHeadBetaTargetFn useZeta
private def etaExpandedBody : Expr → Nat → Nat → Option Expr
| app f (bvar j _) _, n+1, i => if j == i then etaExpandedBody f n (i+1) else none
| _, _+1, _ => none
| f, 0, _ => if f.hasLooseBVars then none else some f
| app f (bvar j), n+1, i => if j == i then etaExpandedBody f n (i+1) else none
| _, _+1, _ => none
| f, 0, _ => if f.hasLooseBVars then none else some f
private def etaExpandedAux : Expr → Nat → Option Expr
| lam _ _ b _, n => etaExpandedAux b (n+1)
@ -1048,11 +1051,11 @@ partial def consumeMDataAndTypeAnnotations (e : Expr) : Expr :=
match e with
| Expr.forallE _ d b _ => visit d || visit b
| Expr.lam _ d b _ => visit d || visit b
| Expr.mdata _ e _ => visit e
| Expr.mdata _ e => visit e
| Expr.letE _ t v b _ => visit t || visit v || visit b
| Expr.app f a _ => visit f || visit a
| Expr.proj _ _ e _ => visit e
| Expr.fvar fvarId _ => p fvarId
| Expr.app f a => visit f || visit a
| Expr.proj _ _ e => visit e
| Expr.fvar fvarId => p fvarId
| _ => false
visit e
@ -1128,8 +1131,8 @@ def updateForall (e : Expr) (newBinfo : BinderInfo) (newDomain : Expr) (newBody
@[inline] def updateForallE! (e : Expr) (newDomain : Expr) (newBody : Expr) : Expr :=
match h : e with
| forallE _ _ _ c => updateForall e c.binderInfo newDomain newBody (h ▸ rfl)
| _ => panic! "forall expected"
| forallE _ _ _ c => updateForall e c newDomain newBody (h ▸ rfl)
| _ => panic! "forall expected"
@[extern "lean_expr_update_lambda"]
def updateLambda (e : Expr) (newBinfo : BinderInfo) (newDomain : Expr) (newBody : Expr) (h : e.isLambda) : Expr :=
@ -1142,7 +1145,7 @@ def updateLambda (e : Expr) (newBinfo : BinderInfo) (newDomain : Expr) (newBody
@[inline] def updateLambdaE! (e : Expr) (newDomain : Expr) (newBody : Expr) : Expr :=
match h : e with
| lam _ _ _ c => updateLambda e c.binderInfo newDomain newBody (h ▸ rfl)
| lam _ _ _ c => updateLambda e c newDomain newBody (h ▸ rfl)
| _ => panic! "lambda expected"
@[extern "lean_expr_update_let"]
@ -1155,15 +1158,15 @@ def updateLet (e : Expr) (newType : Expr) (newVal : Expr) (newBody : Expr) (h :
| _ => panic! "let expression expected"
def updateFn : Expr → Expr → Expr
| e@(app f a _), g => e.updateApp! (updateFn f g) a
| _, g => g
| e@(app f a), g => e.updateApp! (updateFn f g) a
| _, g => g
partial def eta (e : Expr) : Expr :=
match e with
| Expr.lam _ d b _ =>
let b' := b.eta
match b' with
| Expr.app f (Expr.bvar 0 _) _ =>
| .app f (.bvar 0) =>
if !f.hasLooseBVar 0 then
f.lowerLooseBVars 1 1
else
@ -1180,11 +1183,11 @@ partial def eta (e : Expr) : Expr :=
| lam _ d b _ => e.updateLambdaE! (visit d) (visit b)
| forallE _ d b _ => e.updateForallE! (visit d) (visit b)
| letE _ t v b _ => e.updateLet! (visit t) (visit v) (visit b)
| app f a _ => e.updateApp! (visit f) (visit a)
| proj _ _ s _ => e.updateProj! (visit s)
| mdata _ b _ => e.updateMData! (visit b)
| const _ us _ => e.updateConst! (us.map (fun u => u.instantiateParams s))
| sort u _ => e.updateSort! (u.instantiateParams s)
| app f a => e.updateApp! (visit f) (visit a)
| proj _ _ s => e.updateProj! (visit s)
| mdata _ b => e.updateMData! (visit b)
| const _ us => e.updateConst! (us.map (fun u => u.instantiateParams s))
| sort u => e.updateSort! (u.instantiateParams s)
| e => e
visit e
@ -1246,8 +1249,8 @@ def mkAnnotation (kind : Name) (e : Expr) : Expr :=
def annotation? (kind : Name) (e : Expr) : Option Expr :=
match e with
| Expr.mdata d b _ => if d.size == 1 && d.getBool kind false then some b else none
| _ => none
| .mdata d b => if d.size == 1 && d.getBool kind false then some b else none
| _ => none
def mkLetFunAnnotation (e : Expr) : Expr :=
mkAnnotation `let_fun e
@ -1278,7 +1281,7 @@ private def patternRefAnnotationKey := `_patWithRef
-/
def patternWithRef? (p : Expr) : Option (Syntax × Expr) :=
match p with
| Expr.mdata d _ _ =>
| Expr.mdata d _ =>
match d.find patternRefAnnotationKey with
| some (DataValue.ofSyntax stx) => some (stx, p.mdataExpr!)
| _ => none

40
stage0/src/Lean/HeadIndex.lean generated
View file

@ -37,15 +37,15 @@ end HeadIndex
namespace Expr
def head : Expr → Expr
| app f _ _ => head f
| app f _ => head f
| letE _ _ _ b _ => head b
| mdata _ e _ => head e
| mdata _ e => head e
| e => e
private def headNumArgsAux : Expr → Nat → Nat
| app f _ _, n => headNumArgsAux f (n + 1)
| app f _, n => headNumArgsAux f (n + 1)
| letE _ _ _ b _, n => headNumArgsAux b n
| mdata _ e _, n => headNumArgsAux e n
| mdata _ e, n => headNumArgsAux e n
| _, n => n
def headNumArgs (e : Expr) : Nat :=
@ -60,17 +60,17 @@ def headNumArgs (e : Expr) : Nat :=
```
-/
private def toHeadIndexQuick? : Expr → Option HeadIndex
| mvar mvarId _ => HeadIndex.mvar mvarId
| fvar fvarId _ => HeadIndex.fvar fvarId
| const constName _ _ => HeadIndex.const constName
| proj structName idx _ _ => HeadIndex.proj structName idx
| sort _ _ => HeadIndex.sort
| mvar mvarId => HeadIndex.mvar mvarId
| fvar fvarId => HeadIndex.fvar fvarId
| const constName _ => HeadIndex.const constName
| proj structName idx _ => HeadIndex.proj structName idx
| sort _ => HeadIndex.sort
| lam _ _ _ _ => HeadIndex.lam
| forallE _ _ _ _ => HeadIndex.forallE
| lit v _ => HeadIndex.lit v
| app f _ _ => toHeadIndexQuick? f
| lit v => HeadIndex.lit v
| app f _ => toHeadIndexQuick? f
| letE _ _ _ b _ => toHeadIndexQuick? b
| mdata _ e _ => toHeadIndexQuick? e
| mdata _ e => toHeadIndexQuick? e
| _ => none
/-
@ -80,17 +80,17 @@ private def toHeadIndexQuick? : Expr → Option HeadIndex
since `toHeadIndexQuick?` succeeds most of the time.
-/
private partial def toHeadIndexSlow : Expr → HeadIndex
| mvar mvarId _ => HeadIndex.mvar mvarId
| fvar fvarId _ => HeadIndex.fvar fvarId
| const constName _ _ => HeadIndex.const constName
| proj structName idx _ _ => HeadIndex.proj structName idx
| sort _ _ => HeadIndex.sort
| mvar mvarId => HeadIndex.mvar mvarId
| fvar fvarId => HeadIndex.fvar fvarId
| const constName _ => HeadIndex.const constName
| proj structName idx _ => HeadIndex.proj structName idx
| sort _ => HeadIndex.sort
| lam _ _ _ _ => HeadIndex.lam
| forallE _ _ _ _ => HeadIndex.forallE
| lit v _ => HeadIndex.lit v
| app f _ _ => toHeadIndexSlow f
| lit v => HeadIndex.lit v
| app f _ => toHeadIndexSlow f
| letE _ _ v b _ => toHeadIndexSlow (b.instantiate1 v)
| mdata _ e _ => toHeadIndexSlow e
| mdata _ e => toHeadIndexSlow e
| _ => panic! "unexpected expression kind"
def toHeadIndex (e : Expr) : HeadIndex :=

6
stage0/src/Lean/Hygiene.lean generated
View file

@ -51,11 +51,11 @@ private def mkInaccessibleUserNameAux (unicode : Bool) (name : Name) (idx : Nat)
name ++ Name.mkNum "_inaccessible" idx
private def mkInaccessibleUserName (unicode : Bool) : Name → Name
| Name.num p@(Name.str _ _ _) idx _ =>
| .num p@(.str ..) idx =>
mkInaccessibleUserNameAux unicode p idx
| Name.num Name.anonymous idx _ =>
| .num .anonymous idx =>
mkInaccessibleUserNameAux unicode Name.anonymous idx
| Name.num p idx _ =>
| .num p idx =>
if unicode then
(mkInaccessibleUserName unicode p).appendAfter ("⁻" ++ idx.toSuperscriptString)
else

2
stage0/src/Lean/KeyedDeclsAttribute.lean generated
View file

@ -120,7 +120,7 @@ protected unsafe def init {γ} (df : Def γ) (attrDeclName : Name) : IO (KeyedDe
let key ← df.evalKey true stx
let decl ← getConstInfo declName
match decl.type with
| Expr.const c _ _ =>
| Expr.const c _ =>
if c != df.valueTypeName then throwError "unexpected type at '{declName}', '{df.valueTypeName}' expected"
else
/- builtin_initialize @addBuiltin $(mkConst valueTypeName) $(mkConst attrDeclName) $(key) $(declName) $(mkConst declName) -/

175
stage0/src/Lean/Level.lean generated
View file

@ -83,24 +83,27 @@ instance : Inhabited (MVarIdMap α) where
default := {}
inductive Level where
| zero : Data → Level
| succ : Level → Data → Level
| max : Level → Level → Data → Level
| imax : Level → Level → Data → Level
| param : Name → Data → Level
| mvar : MVarId → Data → Level
deriving Inhabited, Repr
| zero : Level
| succ : Level → Level
| max : Level → Level → Level
| imax : Level → Level → Level
| param : Name → Level
| mvar : MVarId → Level
with
@[computedField] data : Level → Data
| .zero => mkData 2221 0 false false
| .mvar mvarId => mkData (mixHash 2237 <| hash mvarId) 0 true false
| .param name => mkData (mixHash 2239 <| hash name) 0 false true
| .succ u => mkData (mixHash 2243 <| u.data.hash) (u.data.depth.toNat + 1) u.data.hasMVar u.data.hasParam
| .max u v => mkData (mixHash 2251 <| mixHash (u.data.hash) (v.data.hash)) (Nat.max u.data.depth.toNat v.data.depth.toNat + 1)
(u.data.hasMVar || v.data.hasMVar) (u.data.hasParam || v.data.hasParam)
| .imax u v => mkData (mixHash 2267 <| mixHash (u.data.hash) (v.data.hash)) (Nat.max u.data.depth.toNat v.data.depth.toNat + 1)
(u.data.hasMVar || v.data.hasMVar) (u.data.hasParam || v.data.hasParam)
deriving Inhabited, Repr
namespace Level
@[inline] def data : Level → Data
| zero d => d
| mvar _ d => d
| param _ d => d
| succ _ d => d
| max _ _ d => d
| imax _ _ d => d
protected def hash (u : Level) : UInt64 :=
u.data.hash
@ -123,26 +126,22 @@ def hasParam (u : Level) : Bool :=
end Level
def levelZero :=
Level.zero <| mkData 2221 0 false false
Level.zero
def mkLevelMVar (mvarId : MVarId) :=
Level.mvar mvarId <| mkData (mixHash 2237 <| hash mvarId) 0 true false
Level.mvar mvarId
def mkLevelParam (name : Name) :=
Level.param name <| mkData (mixHash 2239 <| hash name) 0 false true
Level.param name
def mkLevelSucc (u : Level) :=
Level.succ u <| mkData (mixHash 2243 <| hash u) (u.depth + 1) u.hasMVar u.hasParam
Level.succ u
def mkLevelMax (u v : Level) :=
Level.max u v <| mkData (mixHash 2251 <| mixHash (hash u) (hash v)) (Nat.max u.depth v.depth + 1)
(u.hasMVar || v.hasMVar)
(u.hasParam || v.hasParam)
Level.max u v
def mkLevelIMax (u v : Level) :=
Level.imax u v <| mkData (mixHash 2267 <| mixHash (hash u) (hash v)) (Nat.max u.depth v.depth + 1)
(u.hasMVar || v.hasMVar)
(u.hasParam || v.hasParam)
Level.imax u v
def levelOne := mkLevelSucc levelZero
@ -156,7 +155,7 @@ def levelOne := mkLevelSucc levelZero
namespace Level
def isZero : Level → Bool
| zero _ => true
| zero => true
| _ => false
def isSucc : Level → Bool
@ -185,18 +184,18 @@ def isMVar : Level → Bool
| _ => false
def mvarId! : Level → MVarId
| mvar mvarId _ => mvarId
| _ => panic! "metavariable expected"
| mvar mvarId => mvarId
| _ => panic! "metavariable expected"
/-- If result is true, then forall assignments `A` which assigns all parameters and metavariables occuring
in `l`, `l[A] != zero` -/
def isNeverZero : Level → Bool
| zero _ => false
| zero => false
| param .. => false
| mvar .. => false
| succ .. => true
| max l₁ l₂ _ => isNeverZero l₁ || isNeverZero l₂
| imax _ l₂ _ => isNeverZero l₂
| max l₁ l₂ => isNeverZero l₁ || isNeverZero l₂
| imax _ l₂ => isNeverZero l₂
def ofNat : Nat → Level
| 0 => levelZero
@ -210,24 +209,24 @@ def addOffset (u : Level) (n : Nat) : Level :=
u.addOffsetAux n
def isExplicit : Level → Bool
| zero _ => true
| succ u _ => !u.hasMVar && !u.hasParam && isExplicit u
| zero => true
| succ u => !u.hasMVar && !u.hasParam && isExplicit u
| _ => false
def getOffsetAux : Level → Nat → Nat
| succ u _, r => getOffsetAux u (r+1)
| succ u , r => getOffsetAux u (r+1)
| _, r => r
def getOffset (lvl : Level) : Nat :=
getOffsetAux lvl 0
def getLevelOffset : Level → Level
| succ u _ => getLevelOffset u
| succ u => getLevelOffset u
| u => u
def toNat (lvl : Level) : Option Nat :=
match lvl.getLevelOffset with
| zero _ => lvl.getOffset
| zero => lvl.getOffset
| _ => none
@[extern "lean_level_eq"]
@ -237,9 +236,9 @@ instance : BEq Level := ⟨Level.beq⟩
/-- `occurs u l` return `true` iff `u` occurs in `l`. -/
def occurs : Level → Level → Bool
| u, v@(succ v₁ _) => u == v || occurs u v₁
| u, v@(max v₁ v₂ _) => u == v || occurs u v₁ || occurs u v₂
| u, v@(imax v₁ v₂ _) => u == v || occurs u v₁ || occurs u v₂
| u, v@(succ v₁ ) => u == v || occurs u v₁
| u, v@(max v₁ v₂ ) => u == v || occurs u v₁ || occurs u v₂
| u, v@(imax v₁ v₂ ) => u == v || occurs u v₁ || occurs u v₂
| u, v => u == v
def ctorToNat : Level → Nat
@ -252,24 +251,24 @@ def ctorToNat : Level → Nat
/- TODO: use well founded recursion. -/
partial def normLtAux : Level → Nat → Level → Nat → Bool
| succ l₁ _, k₁, l₂, k₂ => normLtAux l₁ (k₁+1) l₂ k₂
| l₁, k₁, succ l₂ _, k₂ => normLtAux l₁ k₁ l₂ (k₂+1)
| l₁@(max l₁₁ l₁₂ _), k₁, l₂@(max l₂₁ l₂₂ _), k₂ =>
| succ l₁, k₁, l₂, k₂ => normLtAux l₁ (k₁+1) l₂ k₂
| l₁, k₁, succ l₂, k₂ => normLtAux l₁ k₁ l₂ (k₂+1)
| l₁@(max l₁₁ l₁₂), k₁, l₂@(max l₂₁ l₂₂), k₂ =>
if l₁ == l₂ then k₁ < k₂
else if l₁₁ != l₂₁ then normLtAux l₁₁ 0 l₂₁ 0
else normLtAux l₁₂ 0 l₂₂ 0
| l₁@(imax l₁₁ l₁₂ _), k₁, l₂@(imax l₂₁ l₂₂ _), k₂ =>
| l₁@(imax l₁₁ l₁₂), k₁, l₂@(imax l₂₁ l₂₂), k₂ =>
if l₁ == l₂ then k₁ < k₂
else if l₁₁ != l₂₁ then normLtAux l₁₁ 0 l₂₁ 0
else normLtAux l₁₂ 0 l₂₂ 0
| param n₁ _, k₁, param n₂ _, k₂ => if n₁ == n₂ then k₁ < k₂ else Name.lt n₁ n₂ -- use `Name.lt` because it is lexicographical
| param n₁, k₁, param n₂, k₂ => if n₁ == n₂ then k₁ < k₂ else Name.lt n₁ n₂ -- use `Name.lt` because it is lexicographical
/-
We also use `Name.lt` in the following case to make sure universe parameters in a declaration
are not affected by shifted indices. We used to use `Name.quickLt` which is not stable over shifted indices (the hashcodes change),
and changes to the elaborator could affect the universe parameters and break code that relies on an explicit order.
Example: test `tests/lean/343.lean`.
-/
| mvar n₁ _, k₁, mvar n₂ _, k₂ => if n₁ == n₂ then k₁ < k₂ else Name.lt n₁.name n₂.name
| mvar n₁, k₁, mvar n₂, k₂ => if n₁ == n₂ then k₁ < k₂ else Name.lt n₁.name n₂.name
| l₁, k₁, l₂, k₂ => if l₁ == l₂ then k₁ < k₂ else ctorToNat l₁ < ctorToNat l₂
/--
@ -281,21 +280,21 @@ def normLt (l₁ l₂ : Level) : Bool :=
normLtAux l₁ 0 l₂ 0
private def isAlreadyNormalizedCheap : Level → Bool
| zero _ => true
| param _ _ => true
| mvar _ _ => true
| succ u _ => isAlreadyNormalizedCheap u
| _ => false
| zero => true
| param _ => true
| mvar _ => true
| succ u => isAlreadyNormalizedCheap u
| _ => false
/- Auxiliary function used at `normalize` -/
private def mkIMaxAux : Level → Level → Level
| _, u@(zero _) => u
| zero _, u => u
| u₁, u₂ => if u₁ == u₂ then u₁ else mkLevelIMax u₁ u₂
| _, zero => zero
| zero, u => u
| u₁, u₂ => if u₁ == u₂ then u₁ else mkLevelIMax u₁ u₂
/- Auxiliary function used at `normalize` -/
@[specialize] private partial def getMaxArgsAux (normalize : Level → Level) : Level → Bool → Array Level → Array Level
| max l₁ l₂ _, alreadyNormalized, lvls => getMaxArgsAux normalize l₂ alreadyNormalized (getMaxArgsAux normalize l₁ alreadyNormalized lvls)
| max l₁ l₂, alreadyNormalized, lvls => getMaxArgsAux normalize l₂ alreadyNormalized (getMaxArgsAux normalize l₁ alreadyNormalized lvls)
| l, false, lvls => getMaxArgsAux normalize (normalize l) true lvls
| l, true, lvls => lvls.push l
@ -360,7 +359,7 @@ partial def normalize (l : Level) : Level :=
let k := l.getOffset
let u := l.getLevelOffset
match u with
| max l₁ l₂ _ =>
| max l₁ l₂ =>
let lvls := getMaxArgsAux normalize l₁ false #[]
let lvls := getMaxArgsAux normalize l₂ false lvls
let lvls := lvls.qsort normLt
@ -370,7 +369,7 @@ partial def normalize (l : Level) : Level :=
let prev := lvl₁.getLevelOffset
let prevK := lvl₁.getOffset
mkMaxAux lvls k (i+1) prev prevK levelZero
| imax l₁ l₂ _ =>
| imax l₁ l₂ =>
if l₂.isNeverZero then addOffset (normalize (mkLevelMax l₁ l₂)) k
else
let l₁ := normalize l₁
@ -385,14 +384,14 @@ def isEquiv (u v : Level) : Bool :=
/-- Reduce (if possible) universe level by 1 -/
def dec : Level → Option Level
| zero _ => none
| param _ _ => none
| mvar _ _ => none
| succ l _ => l
| max l₁ l₂ _ => return mkLevelMax (← dec l₁) (← dec l₂)
| zero => none
| param _ => none
| mvar _ => none
| succ l => l
| max l₁ l₂ => return mkLevelMax (← dec l₁) (← dec l₂)
/- Remark: `mkLevelMax` in the following line is not a typo.
If `dec l₂` succeeds, then `imax l₁ l₂` is equivalent to `max l₁ l₂`. -/
| imax l₁ l₂ _ => return mkLevelMax (← dec l₁) (← dec l₂)
| imax l₁ l₂ => return mkLevelMax (← dec l₁) (← dec l₂)
/- Level to Format/Syntax -/
@ -418,12 +417,12 @@ def Result.imax : Result → Result → Result
| f₁, f₂ => Result.imaxNode [f₁, f₂]
def toResult : Level → Result
| zero _ => Result.num 0
| succ l _ => Result.succ (toResult l)
| max l₁ l₂ _ => Result.max (toResult l₁) (toResult l₂)
| imax l₁ l₂ _ => Result.imax (toResult l₁) (toResult l₂)
| param n _ => Result.leaf n
| mvar n _ =>
| zero => Result.num 0
| succ l => Result.succ (toResult l)
| max l₁ l₂ => Result.max (toResult l₁) (toResult l₂)
| imax l₁ l₂ => Result.imax (toResult l₁) (toResult l₂)
| param n => Result.leaf n
| mvar n =>
let n := n.name.replacePrefix `_uniq (Name.mkSimple "?u");
Result.leaf n
@ -481,7 +480,7 @@ end Level
let subsumes (u v : Level) : Bool :=
if v.isExplicit && u.getOffset ≥ v.getOffset then true
else match u with
| Level.max u₁ u₂ _ => v == u₁ || v == u₂
| Level.max u₁ u₂ => v == u₁ || v == u₂
| _ => false
if u == v then u
else if u.isZero then v
@ -564,11 +563,11 @@ def mkNaryMax : List Level → Level
/- Level to Format -/
@[specialize] def instantiateParams (s : Name → Option Level) : Level → Level
| u@(zero _) => u
| u@(succ v _) => if u.hasParam then u.updateSucc! (instantiateParams s v) else u
| u@(max v₁ v₂ _) => if u.hasParam then u.updateMax! (instantiateParams s v₁) (instantiateParams s v₂) else u
| u@(imax v₁ v₂ _) => if u.hasParam then u.updateIMax! (instantiateParams s v₁) (instantiateParams s v₂) else u
| u@(param n _) => match s n with
| u@(zero) => u
| u@(succ v) => if u.hasParam then u.updateSucc! (instantiateParams s v) else u
| u@(max v₁ v₂) => if u.hasParam then u.updateMax! (instantiateParams s v₁) (instantiateParams s v₂) else u
| u@(imax v₁ v₂) => if u.hasParam then u.updateIMax! (instantiateParams s v₁) (instantiateParams s v₂) else u
| u@(param n) => match s n with
| some u' => u'
| none => u
| u => u
@ -579,12 +578,12 @@ where
go (u v : Level) : Bool :=
u == v ||
match u, v with
| _, zero _ => true
| u, max v₁ v₂ _ => go u v₁ && go u v₂
| max u₁ u₂ _, v => go u₁ v || go u₂ v
| u, imax v₁ v₂ _ => go u v₁ && go u v₂
| imax _ u₂ _, v => go u₂ v
| succ u _, succ v _ => go u v
| _, zero => true
| u, max v₁ v₂ => go u v₁ && go u v₂
| max u₁ u₂, v => go u₁ v || go u₂ v
| u, imax v₁ v₂ => go u v₁ && go u v₂
| imax _ u₂, v => go u₂ v
| succ u, succ v => go u v
| _, _ =>
let v' := v.getLevelOffset
(u.getLevelOffset == v' || v'.isZero)
@ -603,20 +602,20 @@ abbrev PLevelSet := PersistentLevelSet
def Level.collectMVars (u : Level) (s : MVarIdSet := {}) : MVarIdSet :=
match u with
| succ v _ => collectMVars v s
| max u v _ => collectMVars u (collectMVars v s)
| imax u v _ => collectMVars u (collectMVars v s)
| mvar n _ => s.insert n
| _ => s
| succ v => collectMVars v s
| max u v => collectMVars u (collectMVars v s)
| imax u v => collectMVars u (collectMVars v s)
| mvar n => s.insert n
| _ => s
def Level.find? (u : Level) (p : Level → Bool) : Option Level :=
let rec visit (u : Level) : Option Level :=
if p u then
return u
else match u with
| succ v _ => visit v
| max u v _ => visit u <|> visit v
| imax u v _ => visit u <|> visit v
| succ v => visit v
| max u v => visit u <|> visit v
| imax u v => visit u <|> visit v
| _ => failure
visit u

4
stage0/src/Lean/Linter/Basic.lean generated
View file

@ -70,8 +70,8 @@ def unusedVariables : Linter := fun stx => do
let tacticFVarUses : HashSet FVarId ←
tacticMVarAssignments.foldM (init := .empty) fun uses _ expr => do
let (_, s) ← StateT.run (s := uses) <| expr.forEach fun
| .fvar id _ => modify (·.insert id)
| _ => pure ()
| .fvar id => modify (·.insert id)
| _ => pure ()
return s
-- determine unused variables

2
stage0/src/Lean/Message.lean generated
View file

@ -130,7 +130,7 @@ partial def formatAux : NamingContext → Option MessageDataContext → MessageD
| nCtx, ctx, tagged t d =>
/- Messages starting a trace context have their tags postfixed with `_traceCtx` so that
we can detect them later. Here, we do so in order to print the trace context class. -/
if let Name.str cls "_traceCtx" _ := t then do
if let .str cls "_traceCtx" := t then do
let d₁ ← formatAux nCtx ctx d
return f!"[{cls}] {d₁}"
else

30
stage0/src/Lean/Meta/AbstractMVars.lean generated
View file

@ -47,12 +47,12 @@ private partial def abstractLevelMVars (u : Level) : M Level := do
return u
else
match u with
| Level.zero _ => return u
| Level.param _ _ => return u
| Level.succ v _ => return u.updateSucc! (← abstractLevelMVars v)
| Level.max v w _ => return u.updateMax! (← abstractLevelMVars v) (← abstractLevelMVars w)
| Level.imax v w _ => return u.updateIMax! (← abstractLevelMVars v) (← abstractLevelMVars w)
| Level.mvar mvarId _ =>
| Level.zero => return u
| Level.param _ => return u
| Level.succ v => return u.updateSucc! (← abstractLevelMVars v)
| Level.max v w => return u.updateMax! (← abstractLevelMVars v) (← abstractLevelMVars w)
| Level.imax v w => return u.updateIMax! (← abstractLevelMVars v) (← abstractLevelMVars w)
| Level.mvar mvarId =>
let s ← get
let depth := s.mctx.getLevelDepth mvarId;
if depth != s.mctx.depth then
@ -71,18 +71,18 @@ partial def abstractExprMVars (e : Expr) : M Expr := do
return e
else
match e with
| e@(Expr.lit _ _) => return e
| e@(Expr.bvar _ _) => return e
| e@(Expr.fvar _ _) => return e
| e@(Expr.sort u _) => return e.updateSort! (← abstractLevelMVars u)
| e@(Expr.const _ us _) => return e.updateConst! (← us.mapM abstractLevelMVars)
| e@(Expr.proj _ _ s _) => return e.updateProj! (← abstractExprMVars s)
| e@(Expr.app f a _) => return e.updateApp! (← abstractExprMVars f) (← abstractExprMVars a)
| e@(Expr.mdata _ b _) => return e.updateMData! (← abstractExprMVars b)
| e@(Expr.lit _) => return e
| e@(Expr.bvar _) => return e
| e@(Expr.fvar _) => return e
| e@(Expr.sort u) => return e.updateSort! (← abstractLevelMVars u)
| e@(Expr.const _ us) => return e.updateConst! (← us.mapM abstractLevelMVars)
| e@(Expr.proj _ _ s) => return e.updateProj! (← abstractExprMVars s)
| e@(Expr.app f a) => return e.updateApp! (← abstractExprMVars f) (← abstractExprMVars a)
| e@(Expr.mdata _ b) => return e.updateMData! (← abstractExprMVars b)
| e@(Expr.lam _ d b _) => return e.updateLambdaE! (← abstractExprMVars d) (← abstractExprMVars b)
| e@(Expr.forallE _ d b _) => return e.updateForallE! (← abstractExprMVars d) (← abstractExprMVars b)
| e@(Expr.letE _ t v b _) => return e.updateLet! (← abstractExprMVars t) (← abstractExprMVars v) (← abstractExprMVars b)
| e@(Expr.mvar mvarId _) =>
| e@(Expr.mvar mvarId) =>
let decl := (← getMCtx).getDecl mvarId
if decl.depth != (← getMCtx).depth then
return e

6
stage0/src/Lean/Meta/AbstractNestedProofs.lean generated
View file

@ -57,9 +57,9 @@ partial def visit (e : Expr) : M Expr := do
| Expr.lam _ _ _ _ => lambdaLetTelescope e fun xs b => visitBinders xs do mkLambdaFVars xs (← visit b) (usedLetOnly := false)
| Expr.letE _ _ _ _ _ => lambdaLetTelescope e fun xs b => visitBinders xs do mkLambdaFVars xs (← visit b) (usedLetOnly := false)
| Expr.forallE _ _ _ _ => forallTelescope e fun xs b => visitBinders xs do mkForallFVars xs (← visit b)
| Expr.mdata _ b _ => return e.updateMData! (← visit b)
| Expr.proj _ _ b _ => return e.updateProj! (← visit b)
| Expr.app _ _ _ => e.withApp fun f args => return mkAppN f (← args.mapM visit)
| Expr.mdata _ b => return e.updateMData! (← visit b)
| Expr.proj _ _ b => return e.updateProj! (← visit b)
| Expr.app _ _ => e.withApp fun f args => return mkAppN f (← args.mapM visit)
| _ => pure e
end AbstractNestedProofs

14
stage0/src/Lean/Meta/AppBuilder.lean generated
View file

@ -205,9 +205,9 @@ private partial def mkAppMArgs (f : Expr) (fType : Expr) (xs : Array Expr) : Met
if i >= xs.size then
mkAppMFinal `mkAppM f args instMVars
else match type with
| Expr.forallE n d b c =>
| Expr.forallE n d b bi =>
let d := d.instantiateRevRange j args.size args
match c.binderInfo with
match bi with
| BinderInfo.implicit =>
let mvar ← mkFreshExprMVar d MetavarKind.natural n
loop b i j (args.push mvar) instMVars
@ -265,12 +265,12 @@ def mkAppM' (f : Expr) (xs : Array Expr) : MetaM Expr := do
return r
private partial def mkAppOptMAux (f : Expr) (xs : Array (Option Expr)) : Nat → Array Expr → Nat → Array MVarId → Expr → MetaM Expr
| i, args, j, instMVars, Expr.forallE n d b c => do
| i, args, j, instMVars, Expr.forallE n d b bi => do
let d := d.instantiateRevRange j args.size args
if h : i < xs.size then
match xs.get ⟨i, h⟩ with
| none =>
match c.binderInfo with
match bi with
| BinderInfo.instImplicit => do
let mvar ← mkFreshExprMVar d MetavarKind.synthetic n
mkAppOptMAux f xs (i+1) (args.push mvar) j (instMVars.push mvar.mvarId!) b
@ -332,7 +332,7 @@ def mkEqNDRec (motive h1 h2 : Expr) : MetaM Expr := do
let u2 ← getLevel α
let motiveType ← infer motive
match motiveType with
| Expr.forallE _ _ (Expr.sort u1 _) _ =>
| Expr.forallE _ _ (Expr.sort u1) _ =>
return mkAppN (mkConst ``Eq.ndrec [u1, u2]) #[α, a, motive, h1, b, h2]
| _ => throwAppBuilderException ``Eq.ndrec ("invalid motive" ++ indentExpr motive)
@ -347,7 +347,7 @@ def mkEqRec (motive h1 h2 : Expr) : MetaM Expr := do
let u2 ← getLevel α
let motiveType ← infer motive
match motiveType with
| Expr.forallE _ _ (Expr.forallE _ _ (Expr.sort u1 _) _) _ =>
| Expr.forallE _ _ (Expr.forallE _ _ (Expr.sort u1) _) _ =>
return mkAppN (mkConst ``Eq.rec [u1, u2]) #[α, a, motive, h1, b, h2]
| _ =>
throwAppBuilderException ``Eq.rec ("invalid motive" ++ indentExpr motive)
@ -379,7 +379,7 @@ partial def mkProjection (s : Expr) (fieldName : Name) : MetaM Expr := do
let type ← inferType s
let type ← whnf type
match type.getAppFn with
| Expr.const structName us _ =>
| Expr.const structName us =>
let env ← getEnv
unless isStructure env structName do
throwAppBuilderException `mkProjection ("structure expected" ++ hasTypeMsg s type)

38
stage0/src/Lean/Meta/Basic.lean generated
View file

@ -690,13 +690,13 @@ private partial def isClassQuick? : Expr → MetaM (LOption Name)
| Expr.letE .. => pure LOption.undef
| Expr.proj .. => pure LOption.undef
| Expr.forallE _ _ b _ => isClassQuick? b
| Expr.mdata _ e _ => isClassQuick? e
| Expr.const n _ _ => isClassQuickConst? n
| Expr.mvar mvarId _ => do
| Expr.mdata _ e => isClassQuick? e
| Expr.const n _ => isClassQuickConst? n
| Expr.mvar mvarId => do
match (← getExprMVarAssignment? mvarId) with
| some val => isClassQuick? val
| none => pure LOption.none
| Expr.app f _ _ =>
| Expr.app f _ =>
match f.getAppFn with
| Expr.const n .. => isClassQuickConst? n
| Expr.lam .. => pure LOption.undef
@ -798,11 +798,11 @@ mutual
(k : Array Expr → Expr → MetaM α) : MetaM α := do
let rec process (lctx : LocalContext) (fvars : Array Expr) (j : Nat) (type : Expr) : MetaM α := do
match type with
| Expr.forallE n d b c =>
| Expr.forallE n d b bi =>
if fvarsSizeLtMaxFVars fvars maxFVars? then
let d := d.instantiateRevRange j fvars.size fvars
let fvarId ← mkFreshFVarId
let lctx := lctx.mkLocalDecl fvarId n d c.binderInfo
let lctx := lctx.mkLocalDecl fvarId n d bi
let fvar := mkFVar fvarId
let fvars := fvars.push fvar
process lctx fvars j b
@ -840,13 +840,13 @@ mutual
forallTelescopeReducingAux type none fun _ type => do
let env ← getEnv
match type.getAppFn with
| Expr.const c _ _ => do
| Expr.const c _ => do
if isClass env c then
return some c
else
-- make sure abbreviations are unfolded
match (← whnf type).getAppFn with
| Expr.const c _ _ => return if isClass env c then some c else none
| Expr.const c _ => return if isClass env c then some c else none
| _ => return none
| _ => return none
@ -910,10 +910,10 @@ private partial def lambdaTelescopeImp (e : Expr) (consumeLet : Bool) (k : Array
where
process (consumeLet : Bool) (lctx : LocalContext) (fvars : Array Expr) (j : Nat) (e : Expr) : MetaM α := do
match consumeLet, e with
| _, Expr.lam n d b c =>
| _, Expr.lam n d b bi =>
let d := d.instantiateRevRange j fvars.size fvars
let fvarId ← mkFreshFVarId
let lctx := lctx.mkLocalDecl fvarId n d c.binderInfo
let lctx := lctx.mkLocalDecl fvarId n d bi
let fvar := mkFVar fvarId
process consumeLet lctx (fvars.push fvar) j b
| true, Expr.letE n t v b _ => do
@ -958,12 +958,12 @@ where
return (mvars, bis, type)
else
match type with
| Expr.forallE n d b c =>
| Expr.forallE n d b bi =>
let d := d.instantiateRevRange j mvars.size mvars
let k := if c.binderInfo.isInstImplicit then MetavarKind.synthetic else kind
let k := if bi.isInstImplicit then MetavarKind.synthetic else kind
let mvar ← mkFreshExprMVar d k n
let mvars := mvars.push mvar
let bis := bis.push c.binderInfo
let bis := bis.push bi
process mvars bis j b
| _ =>
let type := type.instantiateRevRange j mvars.size mvars;
@ -1008,11 +1008,11 @@ where
finalize ()
else
match type with
| Expr.lam _ d b c =>
| Expr.lam _ d b bi =>
let d := d.instantiateRevRange j mvars.size mvars
let mvar ← mkFreshExprMVar d
let mvars := mvars.push mvar
let bis := bis.push c.binderInfo
let bis := bis.push bi
process mvars bis j b
| _ => finalize ()
@ -1348,9 +1348,9 @@ def getResetPostponed : MetaM (PersistentArray PostponedEntry) := do
/-- Annotate any constant and sort in `e` that satisfies `p` with `pp.universes true` -/
private def exposeRelevantUniverses (e : Expr) (p : Level → Bool) : Expr :=
e.replace fun
| Expr.const _ us _ => if us.any p then some (e.setPPUniverses true) else none
| Expr.sort u _ => if p u then some (e.setPPUniverses true) else none
| _ => none
| Expr.const _ us => if us.any p then some (e.setPPUniverses true) else none
| Expr.sort u => if p u then some (e.setPPUniverses true) else none
| _ => none
private def mkLeveErrorMessageCore (header : String) (entry : PostponedEntry) : MetaM MessageData := do
match entry.ctx? with
@ -1360,7 +1360,7 @@ private def mkLeveErrorMessageCore (header : String) (entry : PostponedEntry) :
withLCtx ctx.lctx ctx.localInstances do
let s := entry.lhs.collectMVars entry.rhs.collectMVars
/- `p u` is true if it contains a universe metavariable in `s` -/
let p (u : Level) := u.any fun | Level.mvar m _ => s.contains m | _ => false
let p (u : Level) := u.any fun | Level.mvar m => s.contains m | _ => false
let lhs := exposeRelevantUniverses (← instantiateMVars ctx.lhs) p
let rhs := exposeRelevantUniverses (← instantiateMVars ctx.rhs) p
try

2
stage0/src/Lean/Meta/CasesOn.lean generated
View file

@ -24,7 +24,7 @@ structure CasesOnApp where
/-- Return `some c` if `e` is a `casesOn` application. -/
def toCasesOnApp? (e : Expr) : MetaM (Option CasesOnApp) := do
let f := e.getAppFn
let .const declName us _ := f | return none
let .const declName us := f | return none
unless isCasesOnRecursor (← getEnv) declName do return none
let indName := declName.getPrefix
let .inductInfo info ← getConstInfo indName | return none

10
stage0/src/Lean/Meta/Check.lean generated
View file

@ -32,7 +32,7 @@ private def getFunctionDomain (f : Expr) : MetaM (Expr × BinderInfo) := do
let fType ← inferType f
let fType ← whnfD fType
match fType with
| Expr.forallE _ d _ c => return (d, c.binderInfo)
| Expr.forallE _ d _ c => return (d, c)
| _ => throwFunctionExpected f
/-
@ -152,10 +152,10 @@ where
| .forallE .. => checkForall e
| .lam .. => checkLambdaLet e
| .letE .. => checkLambdaLet e
| .const c lvls _ => checkConstant c lvls
| .app f a _ => check f; check a; checkApp f a
| .mdata _ e _ => check e
| .proj _ _ e _ => check e
| .const c lvls => checkConstant c lvls
| .app f a => check f; check a; checkApp f a
| .mdata _ e => check e
| .proj _ _ e => check e
| _ => return ()
checkLambdaLet (e : Expr) : MonadCacheT ExprStructEq Unit MetaM Unit :=

22
stage0/src/Lean/Meta/Closure.lean generated
View file

@ -152,12 +152,12 @@ def mkNewLevelParam (u : Level) : ClosureM Level := do
pure $ mkLevelParam p
partial def collectLevelAux : Level → ClosureM Level
| u@(Level.succ v _) => return u.updateSucc! (← visitLevel collectLevelAux v)
| u@(Level.max v w _) => return u.updateMax! (← visitLevel collectLevelAux v) (← visitLevel collectLevelAux w)
| u@(Level.imax v w _) => return u.updateIMax! (← visitLevel collectLevelAux v) (← visitLevel collectLevelAux w)
| u@(Level.succ v) => return u.updateSucc! (← visitLevel collectLevelAux v)
| u@(Level.max v w) => return u.updateMax! (← visitLevel collectLevelAux v) (← visitLevel collectLevelAux w)
| u@(Level.imax v w) => return u.updateIMax! (← visitLevel collectLevelAux v) (← visitLevel collectLevelAux w)
| u@(Level.mvar ..) => mkNewLevelParam u
| u@(Level.param ..) => mkNewLevelParam u
| u@(Level.zero _) => pure u
| u@(Level.zero) => pure u
def collectLevel (u : Level) : ClosureM Level := do
-- u ← instantiateLevelMVars u
@ -188,15 +188,15 @@ def pushToProcess (elem : ToProcessElement) : ClosureM Unit :=
partial def collectExprAux (e : Expr) : ClosureM Expr := do
let collect (e : Expr) := visitExpr collectExprAux e
match e with
| Expr.proj _ _ s _ => return e.updateProj! (← collect s)
| Expr.proj _ _ s => return e.updateProj! (← collect s)
| Expr.forallE _ d b _ => return e.updateForallE! (← collect d) (← collect b)
| Expr.lam _ d b _ => return e.updateLambdaE! (← collect d) (← collect b)
| Expr.letE _ t v b _ => return e.updateLet! (← collect t) (← collect v) (← collect b)
| Expr.app f a _ => return e.updateApp! (← collect f) (← collect a)
| Expr.mdata _ b _ => return e.updateMData! (← collect b)
| Expr.sort u _ => return e.updateSort! (← collectLevel u)
| Expr.const _ us _ => return e.updateConst! (← us.mapM collectLevel)
| Expr.mvar mvarId _ =>
| Expr.app f a => return e.updateApp! (← collect f) (← collect a)
| Expr.mdata _ b => return e.updateMData! (← collect b)
| Expr.sort u => return e.updateSort! (← collectLevel u)
| Expr.const _ us => return e.updateConst! (← us.mapM collectLevel)
| Expr.mvar mvarId =>
let mvarDecl ← getMVarDecl mvarId
let type ← preprocess mvarDecl.type
let type ← collect type
@ -207,7 +207,7 @@ partial def collectExprAux (e : Expr) : ClosureM Expr := do
exprMVarArgs := s.exprMVarArgs.push e
}
return mkFVar newFVarId
| Expr.fvar fvarId _ =>
| Expr.fvar fvarId =>
match (← read).zeta, (← getLocalDecl fvarId).value? with
| true, some value => collect (← preprocess value)
| _, _ =>

14
stage0/src/Lean/Meta/DecLevel.lean generated
View file

@ -16,9 +16,9 @@ structure DecLevelContext where
canAssignMVars : Bool := true
private partial def decAux? : Level → ReaderT DecLevelContext MetaM (Option Level)
| Level.zero _ => return none
| Level.param _ _ => return none
| Level.mvar mvarId _ => do
| Level.zero => return none
| Level.param _ => return none
| Level.mvar mvarId => do
match (← getLevelMVarAssignment? mvarId) with
| some u => decAux? u
| none =>
@ -29,7 +29,7 @@ private partial def decAux? : Level → ReaderT DecLevelContext MetaM (Option Le
trace[Meta.isLevelDefEq.step] "decAux?, {mkLevelMVar mvarId} := {mkLevelSucc u}"
assignLevelMVar mvarId (mkLevelSucc u)
return u
| Level.succ u _ => return u
| Level.succ u => return u
| u =>
let processMax (u v : Level) : ReaderT DecLevelContext MetaM (Option Level) := do
/- Remark: this code uses the fact that `max (u+1) (v+1) = (max u v)+1`.
@ -45,10 +45,10 @@ private partial def decAux? : Level → ReaderT DecLevelContext MetaM (Option Le
| none => return none
| some v => return mkLevelMax' u v
match u with
| Level.max u v _ => processMax u v
| Level.max u v => processMax u v
/- Remark: If `decAux? v` returns `some ...`, then `imax u v` is equivalent to `max u v`. -/
| Level.imax u v _ => processMax u v
| _ => unreachable!
| Level.imax u v => processMax u v
| _ => unreachable!
def decLevel? (u : Level) : MetaM (Option Level) := do
let mctx ← getMCtx

18
stage0/src/Lean/Meta/DiscrTree.lean generated
View file

@ -159,7 +159,7 @@ private def ignoreArg (a : Expr) (i : Nat) (infos : Array ParamInfo) : MetaM Boo
isProof a
private partial def pushArgsAux (infos : Array ParamInfo) : Nat → Expr → Array Expr → MetaM (Array Expr)
| i, Expr.app f a _, todo => do
| i, Expr.app f a, todo => do
if (← ignoreArg a i infos) then
pushArgsAux infos (i-1) f (todo.push tmpStar)
else
@ -280,8 +280,8 @@ private def pushArgs (root : Bool) (todo : Array Expr) (e : Expr) : MetaM (Key
let todo ← pushArgsAux info.paramInfo (nargs-1) e todo
return (k, todo)
match fn with
| Expr.lit v _ => return (Key.lit v, todo)
| Expr.const c _ _ =>
| Expr.lit v => return (Key.lit v, todo)
| Expr.const c _ =>
unless root do
if (← shouldAddAsStar c e) then
return (Key.star, todo)
@ -289,10 +289,10 @@ private def pushArgs (root : Bool) (todo : Array Expr) (e : Expr) : MetaM (Key
push (Key.const c nargs) nargs
| Expr.proj s i a .. =>
return (Key.proj s i, todo.push a)
| Expr.fvar fvarId _ =>
| Expr.fvar fvarId =>
let nargs := e.getAppNumArgs
push (Key.fvar fvarId nargs) nargs
| Expr.mvar mvarId _ =>
| Expr.mvar mvarId =>
if mvarId == tmpMVarId then
-- We use `tmp to mark implicit arguments and proofs
return (Key.star, todo)
@ -368,8 +368,8 @@ def insert [BEq α] (d : DiscrTree α) (e : Expr) (v : α) : MetaM (DiscrTree α
private def getKeyArgs (e : Expr) (isMatch root : Bool) : MetaM (Key × Array Expr) := do
let e ← whnfDT e root
match e.getAppFn with
| Expr.lit v _ => return (Key.lit v, #[])
| Expr.const c _ _ =>
| Expr.lit v => return (Key.lit v, #[])
| Expr.const c _ =>
if (← getConfig).isDefEqStuckEx && e.hasExprMVar then
if (← isReducible c) then
/- `e` is a term `c ...` s.t. `c` is reducible and `e` has metavariables, but it was not unfolded.
@ -400,10 +400,10 @@ private def getKeyArgs (e : Expr) (isMatch root : Bool) : MetaM (Key × Array Ex
Meta.throwIsDefEqStuck
let nargs := e.getAppNumArgs
return (Key.const c nargs, e.getAppRevArgs)
| Expr.fvar fvarId _ =>
| Expr.fvar fvarId =>
let nargs := e.getAppNumArgs
return (Key.fvar fvarId nargs, e.getAppRevArgs)
| Expr.mvar mvarId _ =>
| Expr.mvar mvarId =>
if isMatch then
return (Key.other, #[])
else do

64
stage0/src/Lean/Meta/ExprDefEq.lean generated
View file

@ -78,7 +78,7 @@ private def isDefEqEta (a b : Expr) : MetaM Bool := do
let bType ← whnfD bType
match bType with
| Expr.forallE n d _ c =>
let b' := mkLambda n c.binderInfo d (mkApp b (mkBVar 0))
let b' := mkLambda n c d (mkApp b (mkBVar 0))
checkpointDefEq <| Meta.isExprDefEqAux a b'
| _ => pure false
else
@ -124,7 +124,7 @@ def isDefEqStringLit (s t : Expr) : MetaM LBool := do
Remark: `n` may be 0. -/
def isEtaUnassignedMVar (e : Expr) : MetaM Bool := do
match e.etaExpanded? with
| some (Expr.mvar mvarId _) =>
| some (Expr.mvar mvarId) =>
if (← isReadOnlyOrSyntheticOpaqueExprMVar mvarId) then
pure false
else if (← isExprMVarAssigned mvarId) then
@ -356,10 +356,10 @@ where
| Expr.forallE _ d b _ => visit d; visit b
| Expr.lam _ d b _ => visit d; visit b
| Expr.letE _ t v b _ => visit t; visit v; visit b
| Expr.app f a _ => visit f; visit a
| Expr.mdata _ b _ => visit b
| Expr.proj _ _ b _ => visit b
| Expr.fvar fvarId _ =>
| Expr.app f a => visit f; visit a
| Expr.mdata _ b => visit b
| Expr.proj _ _ b => visit b
| Expr.fvar fvarId =>
let localDecl ← getLocalDecl fvarId
if localDecl.isLet && localDecl.index > (← read) then
modify fun s => s.insert localDecl.fvarId
@ -752,8 +752,8 @@ mutual
partial def check (e : Expr) : CheckAssignmentM Expr := do
match e with
| Expr.mdata _ b _ => return e.updateMData! (← visit check b)
| Expr.proj _ _ s _ => return e.updateProj! (← visit check s)
| Expr.mdata _ b => return e.updateMData! (← visit check b)
| Expr.proj _ _ s => return e.updateProj! (← visit check s)
| Expr.lam _ d b _ => return e.updateLambdaE! (← visit check d) (← visit check b)
| Expr.forallE _ d b _ => return e.updateForallE! (← visit check d) (← visit check b)
| Expr.letE _ t v b _ => return e.updateLet! (← visit check t) (← visit check v) (← visit check b)
@ -789,9 +789,9 @@ partial def check
if !e.hasExprMVar && !e.hasFVar then
true
else match e with
| Expr.mdata _ b _ => visit b
| Expr.proj _ _ s _ => visit s
| Expr.app f a _ => visit f && visit a
| Expr.mdata _ b => visit b
| Expr.proj _ _ s => visit s
| Expr.app f a => visit f && visit a
| Expr.lam _ d b _ => visit d && visit b
| Expr.forallE _ d b _ => visit d && visit b
| Expr.letE _ t v b _ => visit t && visit v && visit b
@ -806,7 +806,7 @@ partial def check
| _ =>
if fvars.any fun x => x.fvarId! == fvarId then true
else false -- We could throw an exception here, but we would have to use ExceptM. So, we let CheckAssignment.check do it
| Expr.mvar mvarId' _ =>
| Expr.mvar mvarId' =>
match mctx.getExprAssignmentCore? mvarId' with
| some _ => false -- use CheckAssignment.check to instantiate
| none =>
@ -851,7 +851,7 @@ def checkAssignment (mvarId : MVarId) (fvars : Array Expr) (v : Expr) : MetaM (O
private def processAssignmentFOApproxAux (mvar : Expr) (args : Array Expr) (v : Expr) : MetaM Bool :=
match v with
| Expr.app f a _ =>
| Expr.app f a =>
if args.isEmpty then
pure false
else
@ -891,8 +891,8 @@ private partial def processAssignmentFOApprox (mvar : Expr) (args : Array Expr)
loop v
private partial def simpAssignmentArgAux : Expr → MetaM Expr
| Expr.mdata _ e _ => simpAssignmentArgAux e
| e@(Expr.fvar fvarId _) => do
| Expr.mdata _ e => simpAssignmentArgAux e
| e@(Expr.fvar fvarId) => do
let decl ← getLocalDecl fvarId
match decl.value? with
| some value => simpAssignmentArgAux value
@ -992,7 +992,7 @@ private partial def processAssignment (mvarApp : Expr) (v : Expr) : MetaM Bool :
let arg ← simpAssignmentArg arg
let args := args.set ⟨i, h⟩ arg
match arg with
| Expr.fvar fvarId _ =>
| Expr.fvar fvarId =>
if args[0:i].any fun prevArg => prevArg == arg then
useFOApprox args
else if mvarDecl.lctx.contains fvarId && !cfg.quasiPatternApprox then
@ -1048,7 +1048,7 @@ private def processAssignment' (mvarApp : Expr) (v : Expr) : MetaM Bool := do
private def isDeltaCandidate? (t : Expr) : MetaM (Option ConstantInfo) := do
match t.getAppFn with
| Expr.const c _ _ =>
| Expr.const c _ =>
match (← getConst? c) with
| r@(some info) => if info.hasValue then return r else return none
| _ => return none
@ -1133,8 +1133,8 @@ private abbrev unfold (e : Expr) (failK : MetaM α) (successK : Expr → MetaM
/-- Auxiliary method for isDefEqDelta -/
private def unfoldBothDefEq (fn : Name) (t s : Expr) : MetaM LBool := do
match t, s with
| Expr.const _ ls₁ _, Expr.const _ ls₂ _ => isListLevelDefEq ls₁ ls₂
| Expr.app _ _ _, Expr.app _ _ _ =>
| Expr.const _ ls₁, Expr.const _ ls₂ => isListLevelDefEq ls₁ ls₂
| Expr.app _ _, Expr.app _ _ =>
if (← tryHeuristic t s) then
pure LBool.true
else
@ -1145,8 +1145,8 @@ private def unfoldBothDefEq (fn : Name) (t s : Expr) : MetaM LBool := do
private def sameHeadSymbol (t s : Expr) : Bool :=
match t.getAppFn, s.getAppFn with
| Expr.const c₁ _ _, Expr.const c₂ _ _ => c₁ == c₂
| _, _ => false
| Expr.const c₁ _, Expr.const c₂ _ => c₁ == c₂
| _, _ => false
/--
- If headSymbol (unfold t) == headSymbol s, then unfold t
@ -1262,8 +1262,8 @@ private def isDefEqDelta (t s : Expr) : MetaM LBool := do
unfoldNonProjFnDefEq tInfo sInfo t s
private def isAssigned : Expr → MetaM Bool
| Expr.mvar mvarId _ => isExprMVarAssigned mvarId
| _ => pure false
| Expr.mvar mvarId => isExprMVarAssigned mvarId
| _ => pure false
private def expandDelayedAssigned? (t : Expr) : MetaM (Option Expr) := do
let tFn := t.getAppFn
@ -1295,7 +1295,7 @@ private def expandDelayedAssigned? (t : Expr) : MetaM (Option Expr) := do
return some (mkAppRange (mkMVar mvarIdPending) fvars.size tArgs.size tArgs)
private def isSynthetic : Expr → MetaM Bool
| Expr.mvar mvarId _ => do
| Expr.mvar mvarId => do
let mvarDecl ← getMVarDecl mvarId
match mvarDecl.kind with
| MetavarKind.synthetic => pure true
@ -1304,8 +1304,8 @@ private def isSynthetic : Expr → MetaM Bool
| _ => pure false
private def isAssignable : Expr → MetaM Bool
| Expr.mvar mvarId _ => do let b ← isReadOnlyOrSyntheticOpaqueExprMVar mvarId; pure (!b)
| _ => pure false
| Expr.mvar mvarId => do let b ← isReadOnlyOrSyntheticOpaqueExprMVar mvarId; pure (!b)
| _ => pure false
private def etaEq (t s : Expr) : Bool :=
match t.etaExpanded? with
@ -1391,13 +1391,13 @@ private partial def isDefEqQuick (t s : Expr) : MetaM LBool :=
let t := consumeLet t
let s := consumeLet s
match t, s with
| Expr.lit l₁ _, Expr.lit l₂ _ => return (l₁ == l₂).toLBool
| Expr.sort u _, Expr.sort v _ => toLBoolM <| isLevelDefEqAux u v
| Expr.lit l₁, Expr.lit l₂ => return (l₁ == l₂).toLBool
| Expr.sort u, Expr.sort v => toLBoolM <| isLevelDefEqAux u v
| Expr.lam .., Expr.lam .. => if t == s then pure LBool.true else toLBoolM <| isDefEqBinding t s
| Expr.forallE .., Expr.forallE .. => if t == s then pure LBool.true else toLBoolM <| isDefEqBinding t s
-- | Expr.mdata _ t _, s => isDefEqQuick t s
-- | t, Expr.mdata _ s _ => isDefEqQuick t s
| Expr.fvar fvarId₁ _, Expr.fvar fvarId₂ _ => do
| Expr.fvar fvarId₁, Expr.fvar fvarId₂ => do
if (← isLetFVar fvarId₁ <||> isLetFVar fvarId₂) then
pure LBool.undef
else if fvarId₁ == fvarId₂ then
@ -1572,9 +1572,9 @@ private def isDefEqOnFailure (t s : Expr) : MetaM Bool := do
tryUnificationHints t s <||> tryUnificationHints s t
private def isDefEqProj : Expr → Expr → MetaM Bool
| Expr.proj _ i t _, Expr.proj _ j s _ => pure (i == j) <&&> Meta.isExprDefEqAux t s
| Expr.proj structName 0 s _, v => isDefEqSingleton structName s v
| v, Expr.proj structName 0 s _ => isDefEqSingleton structName s v
| Expr.proj _ i t, Expr.proj _ j s => pure (i == j) <&&> Meta.isExprDefEqAux t s
| Expr.proj structName 0 s, v => isDefEqSingleton structName s v
| v, Expr.proj structName 0 s => isDefEqSingleton structName s v
| _, _ => pure false
where
/- If `structName` is a structure with a single field and `(?m ...).1 =?= v`, then solve contraint as `?m ... =?= ⟨v⟩` -/

32
stage0/src/Lean/Meta/ExprLens.lean generated
View file

@ -28,17 +28,17 @@ Mdata is ignored. An index of 3 is interpreted as the type of the expression. An
See also `Lean.Meta.transform`, `Lean.Meta.traverseChildren`. -/
private def lensCoord (g : Expr → M Expr) : Nat → Expr → M Expr
| 0, e@(Expr.app f a _) => return e.updateApp! (← g f) a
| 1, e@(Expr.app f a _) => return e.updateApp! f (← g a)
| 0, e@(Expr.app f a) => return e.updateApp! (← g f) a
| 1, e@(Expr.app f a) => return e.updateApp! f (← g a)
| 0, e@(Expr.lam _ y b _) => return e.updateLambdaE! (← g y) b
| 1, (Expr.lam n y b c) => withLocalDecl n c.binderInfo y fun x => do mkLambdaFVars #[x] <|← g <| b.instantiateRev #[x]
| 1, (Expr.lam n y b c) => withLocalDecl n c y fun x => do mkLambdaFVars #[x] <|← g <| b.instantiateRev #[x]
| 0, e@(Expr.forallE _ y b _) => return e.updateForallE! (← g y) b
| 1, (Expr.forallE n y b c) => withLocalDecl n c.binderInfo y fun x => do mkForallFVars #[x] <|← g <| b.instantiateRev #[x]
| 1, (Expr.forallE n y b c) => withLocalDecl n c y fun x => do mkForallFVars #[x] <|← g <| b.instantiateRev #[x]
| 0, e@(Expr.letE _ y a b _) => return e.updateLet! (← g y) a b
| 1, e@(Expr.letE _ y a b _) => return e.updateLet! y (← g a) b
| 2, (Expr.letE n y a b _) => withLetDecl n y a fun x => do mkLetFVars #[x] <|← g <| b.instantiateRev #[x]
| 0, e@(Expr.proj _ _ b _) => e.updateProj! <$> g b
| n, e@(Expr.mdata _ a _) => e.updateMData! <$> lensCoord g n a
| 0, e@(Expr.proj _ _ b) => e.updateProj! <$> g b
| n, e@(Expr.mdata _ a) => e.updateMData! <$> lensCoord g n a
| 3, _ => throwError "Lensing on types is not supported"
| c, e => throwError "Invalid coordinate {c} for {e}"
@ -57,17 +57,17 @@ The subexpression value passed to `k` is not instantiated with respect to the
array of free variables. -/
private def viewCoordAux (k : Array Expr → Expr → M α) (fvars: Array Expr) : Nat → Expr → M α
| 3, _ => throwError "Internal: Types should be handled by viewAux"
| 0, (Expr.app f _ _) => k fvars f
| 1, (Expr.app _ a _) => k fvars a
| 0, (Expr.app f _) => k fvars f
| 1, (Expr.app _ a) => k fvars a
| 0, (Expr.lam _ y _ _) => k fvars y
| 1, (Expr.lam n y b c) => withLocalDecl n c.binderInfo (y.instantiateRev fvars) fun x => k (fvars.push x) b
| 1, (Expr.lam n y b c) => withLocalDecl n c (y.instantiateRev fvars) fun x => k (fvars.push x) b
| 0, (Expr.forallE _ y _ _) => k fvars y
| 1, (Expr.forallE n y b c) => withLocalDecl n c.binderInfo (y.instantiateRev fvars) fun x => k (fvars.push x) b
| 1, (Expr.forallE n y b c) => withLocalDecl n c (y.instantiateRev fvars) fun x => k (fvars.push x) b
| 0, (Expr.letE _ y _ _ _) => k fvars y
| 1, (Expr.letE _ _ a _ _) => k fvars a
| 2, (Expr.letE n y a b _) => withLetDecl n (y.instantiateRev fvars) (a.instantiateRev fvars) fun x => k (fvars.push x) b
| 0, (Expr.proj _ _ b _) => k fvars b
| n, (Expr.mdata _ a _) => viewCoordAux k fvars n a
| 0, (Expr.proj _ _ b) => k fvars b
| n, (Expr.mdata _ a) => viewCoordAux k fvars n a
| c, e => throwError "Invalid coordinate {c} for {e}"
private def viewAux (k : Array Expr → Expr → M α) (fvars : Array Expr) : List Nat → Expr → M α
@ -123,8 +123,8 @@ variable {M} [Monad M] [MonadError M]
/-- Get the raw subexpression without performing any instantiation. -/
private def viewCoordRaw: Expr → Nat → M Expr
| e , 3 => throwError "Can't viewRaw the type of {e}"
| (Expr.app f _ _) , 0 => pure f
| (Expr.app _ a _) , 1 => pure a
| (Expr.app f _) , 0 => pure f
| (Expr.app _ a) , 1 => pure a
| (Expr.lam _ y _ _) , 0 => pure y
| (Expr.lam _ _ b _) , 1 => pure b
| (Expr.forallE _ y _ _), 0 => pure y
@ -132,8 +132,8 @@ private def viewCoordRaw: Expr → Nat → M Expr
| (Expr.letE _ y _ _ _) , 0 => pure y
| (Expr.letE _ _ a _ _) , 1 => pure a
| (Expr.letE _ _ _ b _) , 2 => pure b
| (Expr.proj _ _ b _) , 0 => pure b
| (Expr.mdata _ a _) , n => viewCoordRaw a n
| (Expr.proj _ _ b) , 0 => pure b
| (Expr.mdata _ a) , n => viewCoordRaw a n
| e , c => throwError "Bad coordinate {c} for {e}"

8
stage0/src/Lean/Meta/ExprTraverse.lean generated
View file

@ -23,7 +23,7 @@ def traverseLambdaWithPos
where visit (fvars : Array Expr) (p : Pos) : Expr → M Expr
| (Expr.lam n d b c) => do
let d ← f p.pushBindingDomain <| d.instantiateRev fvars
withLocalDecl n c.binderInfo d fun x =>
withLocalDecl n c d fun x =>
visit (fvars.push x) p.pushBindingBody b
| e => do
let body ← f p <| e.instantiateRev fvars
@ -35,7 +35,7 @@ def traverseForallWithPos
where visit fvars (p : Pos): Expr → M Expr
| (Expr.forallE n d b c) => do
let d ← f p.pushBindingDomain <| d.instantiateRev fvars
withLocalDecl n c.binderInfo d fun x =>
withLocalDecl n c d fun x =>
visit (fvars.push x) p.pushBindingBody b
| e => do
let body ← f p <| e.instantiateRev fvars
@ -64,8 +64,8 @@ def traverseChildrenWithPos (visit : Pos → Expr → M Expr) (p : Pos) (e: Expr
| Expr.lam .. => traverseLambdaWithPos visit p e
| Expr.letE .. => traverseLetWithPos visit p e
| Expr.app .. => Expr.traverseAppWithPos visit p e
| Expr.mdata _ b _ => e.updateMData! <$> visit p b
| Expr.proj _ _ b _ => e.updateProj! <$> visit p.pushProj b
| Expr.mdata _ b => e.updateMData! <$> visit p b
| Expr.proj _ _ b => e.updateProj! <$> visit p.pushProj b
| _ => pure e
/-- Given an expression `fun (x₁ : α₁) ... (xₙ : αₙ) => b`, will run

12
stage0/src/Lean/Meta/ForEachExpr.lean generated
View file

@ -18,12 +18,12 @@ private partial def visitBinder (fn : Expr → MetaM Bool) : Array Expr → Nat
| fvars, j, Expr.lam n d b c => do
let d := d.instantiateRevRange j fvars.size fvars
visit fn d
withLocalDecl n c.binderInfo d fun x =>
withLocalDecl n c d fun x =>
visitBinder fn (fvars.push x) j b
| fvars, j, Expr.forallE n d b c => do
let d := d.instantiateRevRange j fvars.size fvars
visit fn d
withLocalDecl n c.binderInfo d fun x =>
withLocalDecl n c d fun x =>
visitBinder fn (fvars.push x) j b
| fvars, j, Expr.letE n t v b _ => do
let t := t.instantiateRevRange j fvars.size fvars
@ -41,9 +41,9 @@ partial def visit (fn : Expr → MetaM Bool) (e : Expr) : M Unit :=
| .forallE .. => visitBinder fn #[] 0 e
| .lam .. => visitBinder fn #[] 0 e
| .letE .. => visitBinder fn #[] 0 e
| .app f a _ => visit fn f; visit fn a
| .mdata _ b _ => visit fn b
| .proj _ _ b _ => visit fn b
| .app f a => visit fn f; visit fn a
| .mdata _ b => visit fn b
| .proj _ _ b => visit fn b
| _ => return ()
end
@ -63,7 +63,7 @@ def forEachExpr (e : Expr) (f : Expr → MetaM Unit) : MetaM Unit :=
/-- Return true iff `x` is a metavariable with an anonymous user facing name. -/
private def shouldInferBinderName (x : Expr) : MetaM Bool := do
match x with
| .mvar mvarId _ => return (← Meta.getMVarDecl mvarId).userName.isAnonymous
| .mvar mvarId => return (← Meta.getMVarDecl mvarId).userName.isAnonymous
| _ => return false
/--

6
stage0/src/Lean/Meta/FunInfo.lean generated
View file

@ -24,12 +24,12 @@ namespace Lean.Meta
private def collectDeps (fvars : Array Expr) (e : Expr) : Array Nat :=
let rec visit (e : Expr) (deps : Array Nat) : Array Nat :=
match e with
| .app f a _ => whenHasVar e deps (visit a ∘ visit f)
| .app f a => whenHasVar e deps (visit a ∘ visit f)
| .forallE _ d b _ => whenHasVar e deps (visit b ∘ visit d)
| .lam _ d b _ => whenHasVar e deps (visit b ∘ visit d)
| .letE _ t v b _ => whenHasVar e deps (visit b ∘ visit v ∘ visit t)
| .proj _ _ e _ => visit e deps
| .mdata _ e _ => visit e deps
| .proj _ _ e => visit e deps
| .mdata _ e => visit e deps
| .fvar .. =>
match fvars.indexOf? e with
| none => deps

2
stage0/src/Lean/Meta/GeneralizeTelescope.lean generated
View file

@ -38,7 +38,7 @@ partial def generalizeTelescopeAux {α} (k : Array Expr → MetaM α)
let entries ← updateTypes e x entries (i+1)
generalizeTelescopeAux k entries (i+1) (fvars.push x)
match entries.get ⟨i, h⟩ with
| ⟨e@(.fvar fvarId _), type, false⟩ =>
| ⟨e@(.fvar fvarId), type, false⟩ =>
let localDecl ← getLocalDecl fvarId
match localDecl with
| .cdecl .. => generalizeTelescopeAux k entries (i+1) (fvars.push e)

98
stage0/src/Lean/Meta/InferType.lean generated
View file

@ -38,8 +38,8 @@ where
| .forallE _ d b _ => return e.updateForallE! (← visit d offset) (← visit b (offset+1))
| .lam _ d b _ => return e.updateLambdaE! (← visit d offset) (← visit b (offset+1))
| .letE _ t v b _ => return e.updateLet! (← visit t offset) (← visit v offset) (← visit b (offset+1))
| .mdata _ b _ => return e.updateMData! (← visit b offset)
| .proj _ _ b _ => return e.updateProj! (← visit b offset)
| .mdata _ b => return e.updateMData! (← visit b offset)
| .proj _ _ b => return e.updateProj! (← visit b offset)
| .app .. =>
e.withAppRev fun f revArgs => do
let fNew ← visit f offset
@ -49,7 +49,7 @@ where
return fNew.betaRev revArgs
else
return mkAppRev fNew revArgs
| Expr.bvar vidx _ =>
| Expr.bvar vidx =>
-- Recall that looseBVarRange for `Expr.bvar` is `vidx+1`.
-- So, we must have offset ≤ vidx, since we are in the "else" branch of `if offset >= e.looseBVarRange`
let n := stop - start
@ -126,8 +126,8 @@ def getLevel (type : Expr) : MetaM Level := do
let typeType ← inferType type
let typeType ← whnfD typeType
match typeType with
| Expr.sort lvl _ => return lvl
| Expr.mvar mvarId _ =>
| Expr.sort lvl => return lvl
| Expr.mvar mvarId =>
if (← isReadOnlyOrSyntheticOpaqueExprMVar mvarId) then
throwTypeExcepted type
else
@ -183,16 +183,16 @@ private def inferFVarType (fvarId : FVarId) : MetaM Expr := do
def inferTypeImp (e : Expr) : MetaM Expr :=
let rec infer (e : Expr) : MetaM Expr := do
match e with
| .const c [] _ => inferConstType c []
| .const c us _ => checkInferTypeCache e (inferConstType c us)
| .proj n i s _ => checkInferTypeCache e (inferProjType n i s)
| .const c [] => inferConstType c []
| .const c us => checkInferTypeCache e (inferConstType c us)
| .proj n i s => checkInferTypeCache e (inferProjType n i s)
| .app f .. => checkInferTypeCache e (inferAppType f.getAppFn e.getAppArgs)
| .mvar mvarId _ => inferMVarType mvarId
| .fvar fvarId _ => inferFVarType fvarId
| .bvar bidx _ => throwError "unexpected bound variable {mkBVar bidx}"
| .mdata _ e _ => infer e
| .lit v _ => return v.type
| .sort lvl _ => return mkSort (mkLevelSucc lvl)
| .mvar mvarId => inferMVarType mvarId
| .fvar fvarId => inferFVarType fvarId
| .bvar bidx => throwError "unexpected bound variable {mkBVar bidx}"
| .mdata _ e => infer e
| .lit v => return v.type
| .sort lvl => return mkSort (mkLevelSucc lvl)
| .forallE .. => checkInferTypeCache e (inferForallType e)
| .lam .. => checkInferTypeCache e (inferLambdaType e)
| .letE .. => checkInferTypeCache e (inferLambdaType e)
@ -206,30 +206,30 @@ private def isAlwaysZero : Level → Bool
| .mvar .. => false
| .param .. => false
| .succ .. => false
| .max u v _ => isAlwaysZero u && isAlwaysZero v
| .imax _ u _ => isAlwaysZero u
| .max u v => isAlwaysZero u && isAlwaysZero v
| .imax _ u => isAlwaysZero u
/--
`isArrowProp type n` is an "approximate" predicate which returns `LBool.true`
if `type` is of the form `A_1 -> ... -> A_n -> Prop`.
Remark: `type` can be a dependent arrow. -/
private partial def isArrowProp : Expr → Nat → MetaM LBool
| .sort u _, 0 => return isAlwaysZero (← instantiateLevelMVars u) |>.toLBool
| .sort u, 0 => return isAlwaysZero (← instantiateLevelMVars u) |>.toLBool
| .forallE .., 0 => return LBool.false
| .forallE _ _ b _, n+1 => isArrowProp b n
| .letE _ _ _ b _, n => isArrowProp b n
| .mdata _ e _, n => isArrowProp e n
| .mdata _ e, n => isArrowProp e n
| _, _ => return LBool.undef
/--
`isPropQuickApp f n` is an "approximate" predicate which returns `LBool.true`
if `f` applied to `n` arguments is a proposition. -/
private partial def isPropQuickApp : Expr → Nat → MetaM LBool
| .const c lvls _, arity => do let constType ← inferConstType c lvls; isArrowProp constType arity
| .fvar fvarId _, arity => do let fvarType ← inferFVarType fvarId; isArrowProp fvarType arity
| .mvar mvarId _, arity => do let mvarType ← inferMVarType mvarId; isArrowProp mvarType arity
| .const c lvls, arity => do let constType ← inferConstType c lvls; isArrowProp constType arity
| .fvar fvarId, arity => do let fvarType ← inferFVarType fvarId; isArrowProp fvarType arity
| .mvar mvarId, arity => do let mvarType ← inferMVarType mvarId; isArrowProp mvarType arity
| .app f .., arity => isPropQuickApp f (arity+1)
| .mdata _ e _, arity => isPropQuickApp e arity
| .mdata _ e, arity => isPropQuickApp e arity
| .letE _ _ _ b _, arity => isPropQuickApp b arity
| .lam .., 0 => return LBool.false
| .lam _ _ b _, arity+1 => isPropQuickApp b arity
@ -246,10 +246,10 @@ partial def isPropQuick : Expr → MetaM LBool
| .letE _ _ _ b _ => isPropQuick b
| .proj .. => return LBool.undef
| .forallE _ _ b _ => isPropQuick b
| .mdata _ e _ => isPropQuick e
| .const c lvls _ => do let constType ← inferConstType c lvls; isArrowProp constType 0
| .fvar fvarId _ => do let fvarType ← inferFVarType fvarId; isArrowProp fvarType 0
| .mvar mvarId _ => do let mvarType ← inferMVarType mvarId; isArrowProp mvarType 0
| .mdata _ e => isPropQuick e
| .const c lvls => do let constType ← inferConstType c lvls; isArrowProp constType 0
| .fvar fvarId => do let fvarType ← inferFVarType fvarId; isArrowProp fvarType 0
| .mvar mvarId => do let mvarType ← inferMVarType mvarId; isArrowProp mvarType 0
| .app f .. => isPropQuickApp f 1
/-- `isProp whnf e` return `true` if `e` is a proposition.
@ -266,8 +266,8 @@ def isProp (e : Expr) : MetaM Bool := do
let type ← inferType e
let type ← whnfD type
match type with
| Expr.sort u _ => return isAlwaysZero (← instantiateLevelMVars u)
| _ => return false
| Expr.sort u => return isAlwaysZero (← instantiateLevelMVars u)
| _ => return false
/--
`isArrowProposition type n` is an "approximate" predicate which returns `LBool.true`
@ -276,7 +276,7 @@ def isProp (e : Expr) : MetaM Bool := do
private partial def isArrowProposition : Expr → Nat → MetaM LBool
| .forallE _ _ b _, n+1 => isArrowProposition b n
| .letE _ _ _ b _, n => isArrowProposition b n
| .mdata _ e _, n => isArrowProposition e n
| .mdata _ e, n => isArrowProposition e n
| type, 0 => isPropQuick type
| _, _ => return LBool.undef
@ -285,11 +285,11 @@ mutual
`isProofQuickApp f n` is an "approximate" predicate which returns `LBool.true`
if `f` applied to `n` arguments is a proof. -/
private partial def isProofQuickApp : Expr → Nat → MetaM LBool
| .const c lvls _, arity => do let constType ← inferConstType c lvls; isArrowProposition constType arity
| .fvar fvarId _, arity => do let fvarType ← inferFVarType fvarId; isArrowProposition fvarType arity
| .mvar mvarId _, arity => do let mvarType ← inferMVarType mvarId; isArrowProposition mvarType arity
| .app f _ _, arity => isProofQuickApp f (arity+1)
| .mdata _ e _, arity => isProofQuickApp e arity
| .const c lvls, arity => do let constType ← inferConstType c lvls; isArrowProposition constType arity
| .fvar fvarId, arity => do let fvarType ← inferFVarType fvarId; isArrowProposition fvarType arity
| .mvar mvarId, arity => do let mvarType ← inferMVarType mvarId; isArrowProposition mvarType arity
| .app f _, arity => isProofQuickApp f (arity+1)
| .mdata _ e, arity => isProofQuickApp e arity
| .letE _ _ _ b _, arity => isProofQuickApp b arity
| .lam _ _ b _, 0 => isProofQuick b
| .lam _ _ b _, arity+1 => isProofQuickApp b arity
@ -306,10 +306,10 @@ partial def isProofQuick : Expr → MetaM LBool
| .letE _ _ _ b _ => isProofQuick b
| .proj .. => return LBool.undef
| .forallE .. => return LBool.false
| .mdata _ e _ => isProofQuick e
| .const c lvls _ => do let constType ← inferConstType c lvls; isArrowProposition constType 0
| .fvar fvarId _ => do let fvarType ← inferFVarType fvarId; isArrowProposition fvarType 0
| .mvar mvarId _ => do let mvarType ← inferMVarType mvarId; isArrowProposition mvarType 0
| .mdata _ e => isProofQuick e
| .const c lvls => do let constType ← inferConstType c lvls; isArrowProposition constType 0
| .fvar fvarId => do let fvarType ← inferFVarType fvarId; isArrowProposition fvarType 0
| .mvar mvarId => do let mvarType ← inferMVarType mvarId; isArrowProposition mvarType 0
| .app f .. => isProofQuickApp f 1
end
@ -329,18 +329,18 @@ private partial def isArrowType : Expr → Nat → MetaM LBool
| .forallE .., 0 => return LBool.false
| .forallE _ _ b _, n+1 => isArrowType b n
| .letE _ _ _ b _, n => isArrowType b n
| .mdata _ e _, n => isArrowType e n
| .mdata _ e, n => isArrowType e n
| _, _ => return LBool.undef
/--
`isTypeQuickApp f n` is an "approximate" predicate which returns `LBool.true`
if `f` applied to `n` arguments is a type. -/
private partial def isTypeQuickApp : Expr → Nat → MetaM LBool
| .const c lvls _, arity => do let constType ← inferConstType c lvls; isArrowType constType arity
| .fvar fvarId _, arity => do let fvarType ← inferFVarType fvarId; isArrowType fvarType arity
| .mvar mvarId _, arity => do let mvarType ← inferMVarType mvarId; isArrowType mvarType arity
| .app f _ _, arity => isTypeQuickApp f (arity+1)
| .mdata _ e _, arity => isTypeQuickApp e arity
| .const c lvls, arity => do let constType ← inferConstType c lvls; isArrowType constType arity
| .fvar fvarId, arity => do let fvarType ← inferFVarType fvarId; isArrowType fvarType arity
| .mvar mvarId, arity => do let mvarType ← inferMVarType mvarId; isArrowType mvarType arity
| .app f _, arity => isTypeQuickApp f (arity+1)
| .mdata _ e, arity => isTypeQuickApp e arity
| .letE _ _ _ b _, arity => isTypeQuickApp b arity
| .lam .., 0 => return LBool.false
| .lam _ _ b _, arity+1 => isTypeQuickApp b arity
@ -357,10 +357,10 @@ partial def isTypeQuick : Expr → MetaM LBool
| .letE _ _ _ b _ => isTypeQuick b
| .proj .. => return LBool.undef
| .forallE .. => return LBool.true
| .mdata _ e _ => isTypeQuick e
| .const c lvls _ => do let constType ← inferConstType c lvls; isArrowType constType 0
| .fvar fvarId _ => do let fvarType ← inferFVarType fvarId; isArrowType fvarType 0
| .mvar mvarId _ => do let mvarType ← inferMVarType mvarId; isArrowType mvarType 0
| .mdata _ e => isTypeQuick e
| .const c lvls => do let constType ← inferConstType c lvls; isArrowType constType 0
| .fvar fvarId => do let fvarType ← inferFVarType fvarId; isArrowType fvarType 0
| .mvar mvarId => do let mvarType ← inferMVarType mvarId; isArrowType mvarType 0
| .app f .. => isTypeQuickApp f 1
def isType (e : Expr) : MetaM Bool := do
@ -379,7 +379,7 @@ partial def isTypeFormerType (type : Expr) : MetaM Bool := do
match type with
| .sort .. => return true
| .forallE n d b c =>
withLocalDecl' n c.binderInfo d fun fvar => isTypeFormerType (b.instantiate1 fvar)
withLocalDecl' n c d fun fvar => isTypeFormerType (b.instantiate1 fvar)
| _ => return false
/--

2
stage0/src/Lean/Meta/Instances.lean generated
View file

@ -114,7 +114,7 @@ def addDefaultInstance (declName : Name) (prio : Nat := 0) : MetaM Unit := do
| some info =>
forallTelescopeReducing info.type fun _ type => do
match type.getAppFn with
| Expr.const className _ _ =>
| Expr.const className _ =>
unless isClass (← getEnv) className do
throwError "invalid default instance '{declName}', it has type '({className} ...)', but {className}' is not a type class"
setEnv <| defaultInstanceExtension.addEntry (← getEnv) { className := className, instanceName := declName, priority := prio }

6
stage0/src/Lean/Meta/KAbstract.lean generated
View file

@ -19,9 +19,9 @@ def kabstract (e : Expr) (p : Expr) (occs : Occurrences := Occurrences.all) : Me
let rec visit (e : Expr) (offset : Nat) : StateRefT Nat MetaM Expr := do
let visitChildren : Unit → StateRefT Nat MetaM Expr := fun _ => do
match e with
| Expr.app f a _ => return e.updateApp! (← visit f offset) (← visit a offset)
| Expr.mdata _ b _ => return e.updateMData! (← visit b offset)
| Expr.proj _ _ b _ => return e.updateProj! (← visit b offset)
| Expr.app f a => return e.updateApp! (← visit f offset) (← visit a offset)
| Expr.mdata _ b => return e.updateMData! (← visit b offset)
| Expr.proj _ _ b => return e.updateProj! (← visit b offset)
| Expr.letE _ t v b _ => return e.updateLet! (← visit t offset) (← visit v offset) (← visit b (offset+1))
| Expr.lam _ d b _ => return e.updateLambdaE! (← visit d offset) (← visit b (offset+1))
| Expr.forallE _ d b _ => return e.updateForallE! (← visit d offset) (← visit b (offset+1))

22
stage0/src/Lean/Meta/LevelDefEq.lean generated
View file

@ -14,17 +14,17 @@ namespace Lean.Meta
Return true iff `lvl` occurs in `max u_1 ... u_n` and `lvl != u_i` for all `i in [1, n]`.
That is, `lvl` is a proper level subterm of some `u_i`. -/
private def strictOccursMax (lvl : Level) : Level → Bool
| Level.max u v _ => visit u || visit v
| Level.max u v => visit u || visit v
| _ => false
where
visit : Level → Bool
| Level.max u v _ => visit u || visit v
| Level.max u v => visit u || visit v
| u => u != lvl && lvl.occurs u
/-- `mkMaxArgsDiff mvarId (max u_1 ... (mvar mvarId) ... u_n) v` => `max v u_1 ... u_n` -/
private def mkMaxArgsDiff (mvarId : MVarId) : Level → Level → Level
| Level.max u v _, acc => mkMaxArgsDiff mvarId v <| mkMaxArgsDiff mvarId u acc
| l@(Level.mvar id _), acc => if id != mvarId then mkLevelMax' acc l else acc
| Level.max u v, acc => mkMaxArgsDiff mvarId v <| mkMaxArgsDiff mvarId u acc
| l@(Level.mvar id), acc => if id != mvarId then mkLevelMax' acc l else acc
| l, acc => mkLevelMax' acc l
/--
@ -43,14 +43,14 @@ private def postponeIsLevelDefEq (lhs : Level) (rhs : Level) : MetaM Unit := do
private def isMVarWithGreaterDepth (v : Level) (mvarId : MVarId) : MetaM Bool :=
match v with
| Level.mvar mvarId' _ => return (← getLevelMVarDepth mvarId') > (← getLevelMVarDepth mvarId)
| Level.mvar mvarId' => return (← getLevelMVarDepth mvarId') > (← getLevelMVarDepth mvarId)
| _ => return false
mutual
private partial def solve (u v : Level) : MetaM LBool := do
match u, v with
| Level.mvar mvarId _, _ =>
| Level.mvar mvarId, _ =>
if (← isReadOnlyLevelMVar mvarId) then
return LBool.undef
else if (← getConfig).ignoreLevelMVarDepth && (← isMVarWithGreaterDepth v mvarId) then
@ -67,12 +67,12 @@ mutual
else
return LBool.undef
| _, Level.mvar .. => return LBool.undef -- Let `solve v u` to handle this case
| Level.zero _, Level.max v₁ v₂ _ =>
| Level.zero, Level.max v₁ v₂ =>
Bool.toLBool <$> (isLevelDefEqAux levelZero v₁ <&&> isLevelDefEqAux levelZero v₂)
| Level.zero _, Level.imax _ v₂ _ =>
| Level.zero, Level.imax _ v₂ =>
Bool.toLBool <$> isLevelDefEqAux levelZero v₂
| Level.zero _, Level.succ .. => return LBool.false
| Level.succ u _, v =>
| Level.zero, Level.succ .. => return LBool.false
| Level.succ u, v =>
if v.isParam then
return LBool.false
else if u.isMVar && u.occurs v then
@ -85,7 +85,7 @@ mutual
@[export lean_is_level_def_eq]
partial def isLevelDefEqAuxImpl : Level → Level → MetaM Bool
| Level.succ lhs _, Level.succ rhs _ => isLevelDefEqAux lhs rhs
| Level.succ lhs, Level.succ rhs => isLevelDefEqAux lhs rhs
| lhs, rhs => do
if lhs.getLevelOffset == rhs.getLevelOffset then
return lhs.getOffset == rhs.getOffset

8
stage0/src/Lean/Meta/Match/Basic.lean generated
View file

@ -230,8 +230,8 @@ partial def replaceFVarId (fvarId : FVarId) (ex : Example) : Example → Example
partial def applyFVarSubst (s : FVarSubst) : Example → Example
| var fvarId =>
match s.get fvarId with
| Expr.fvar fvarId' _ => var fvarId'
| _ => underscore
| Expr.fvar fvarId' => var fvarId'
| _ => underscore
| ctor n exs => ctor n $ exs.map (applyFVarSubst s)
| arrayLit exs => arrayLit $ exs.map (applyFVarSubst s)
| ex => ex
@ -306,8 +306,8 @@ partial def toPattern (e : Expr) : MetaM Pattern := do
if let some e := isNamedPattern? e then
let p ← toPattern <| e.getArg! 2
match e.getArg! 1, e.getArg! 3 with
| Expr.fvar x _, Expr.fvar h _ => return Pattern.as x p h
| _, _ => throwError "unexpected occurrence of auxiliary declaration 'namedPattern'"
| Expr.fvar x, Expr.fvar h => return Pattern.as x p h
| _, _ => throwError "unexpected occurrence of auxiliary declaration 'namedPattern'"
else if isMatchValue e then
return Pattern.val e
else if e.isFVar then

4
stage0/src/Lean/Meta/Match/CaseValues.lean generated
View file

@ -87,8 +87,8 @@ def caseValues (mvarId : MVarId) (fvarId : FVarId) (values : Array Expr) (hNameP
appendTagSuffix thenSubgoal.mvarId ((`case).appendIndexAfter i)
let thenMVarId ← hs.foldlM
(fun thenMVarId h => match thenSubgoal.subst.get h with
| Expr.fvar fvarId _ => tryClear thenMVarId fvarId
| _ => pure thenMVarId)
| Expr.fvar fvarId => tryClear thenMVarId fvarId
| _ => pure thenMVarId)
thenSubgoal.mvarId
let subgoals ← if substNewEqs then
let (subst, mvarId) ← substCore thenMVarId thenSubgoal.newH false thenSubgoal.subst true

2
stage0/src/Lean/Meta/Match/MVarRenaming.lean generated
View file

@ -27,7 +27,7 @@ def MVarRenaming.apply (s : MVarRenaming) (e : Expr) : Expr :=
if !e.hasMVar then e
else if s.map.isEmpty then e
else e.replace fun e => match e with
| Expr.mvar mvarId _ => match s.map.find? mvarId with
| Expr.mvar mvarId => match s.map.find? mvarId with
| none => e
| some newMVarId => mkMVar newMVarId
| _ => none

34
stage0/src/Lean/Meta/Match/Match.lean generated
View file

@ -89,8 +89,8 @@ private def isDone (p : Problem) : Bool :=
/-- Return true if the next element on the `p.vars` list is a variable. -/
private def isNextVar (p : Problem) : Bool :=
match p.vars with
| Expr.fvar _ _ :: _ => true
| _ => false
| Expr.fvar _ :: _ => true
| _ => false
private def hasAsPattern (p : Problem) : Bool :=
p.alts.any fun alt => match alt.patterns with
@ -249,12 +249,12 @@ def isAltVar (fvarId : FVarId) : M Bool := do
def expandIfVar (e : Expr) : M Expr := do
match e with
| Expr.fvar _ _ => return (← get).fvarSubst.apply e
| _ => return e
| Expr.fvar _ => return (← get).fvarSubst.apply e
| _ => return e
def occurs (fvarId : FVarId) (v : Expr) : Bool :=
Option.isSome <| v.find? fun e => match e with
| Expr.fvar fvarId' _ => fvarId == fvarId'
| Expr.fvar fvarId' => fvarId == fvarId'
| _=> false
def assign (fvarId : FVarId) (v : Expr) : M Bool := do
@ -330,10 +330,10 @@ partial def unify (a : Expr) (b : Expr) : M Bool := do
if a != a' || b != b' then
unify a' b'
else match a, b with
| Expr.fvar aFvarId _, Expr.fvar bFVarId _ => assign aFvarId b <||> assign bFVarId a
| Expr.fvar aFvarId _, b => assign aFvarId b
| a, Expr.fvar bFVarId _ => assign bFVarId a
| Expr.app aFn aArg _, Expr.app bFn bArg _ => unify aFn bFn <&&> unify aArg bArg
| Expr.fvar aFvarId, Expr.fvar bFVarId => assign aFvarId b <||> assign bFVarId a
| Expr.fvar aFvarId, b => assign aFvarId b
| a, Expr.fvar bFVarId => assign bFVarId a
| Expr.app aFn aArg, Expr.app bFn bArg => unify aFn bFn <&&> unify aArg bArg
| _, _ => return false
end Unify
@ -372,15 +372,15 @@ private def expandVarIntoCtor? (alt : Alt) (fvarId : FVarId) (ctorName : Name) :
let patterns := alt.patterns.map fun p => p.applyFVarSubst subst
let rhs := subst.apply alt.rhs
let ctorFieldPatterns := ctorFields.toList.map fun ctorField => match subst.get ctorField.fvarId! with
| e@(Expr.fvar fvarId _) => if inLocalDecls newAltDecls fvarId then Pattern.var fvarId else Pattern.inaccessible e
| e => Pattern.inaccessible e
| e@(Expr.fvar fvarId) => if inLocalDecls newAltDecls fvarId then Pattern.var fvarId else Pattern.inaccessible e
| e => Pattern.inaccessible e
return some { alt with fvarDecls := newAltDecls, rhs := rhs, patterns := ctorFieldPatterns ++ patterns }
private def getInductiveVal? (x : Expr) : MetaM (Option InductiveVal) := do
let xType ← inferType x
let xType ← whnfD xType
match xType.getAppFn with
| Expr.const constName _ _ =>
| Expr.const constName _ =>
let cinfo ← getConstInfo constName
match cinfo with
| ConstantInfo.inductInfo val => return some val
@ -471,8 +471,8 @@ private def processConstructor (p : Problem) : MetaM (Array Problem) := do
let newVars := fields ++ xs
let newVars := newVars.map fun x => x.applyFVarSubst subst
let subex := Example.ctor subgoal.ctorName <| fields.map fun field => match field with
| Expr.fvar fvarId _ => Example.var fvarId
| _ => Example.underscore -- This case can happen due to dependent elimination
| Expr.fvar fvarId => Example.var fvarId
| _ => Example.underscore -- This case can happen due to dependent elimination
let examples := p.examples.map <| Example.replaceFVarId x.fvarId! subex
let examples := examples.map <| Example.applyFVarSubst subst
let newAlts := p.alts.filter fun alt => match alt.patterns with
@ -625,9 +625,9 @@ private def processArrayLit (p : Problem) : MetaM (Array Problem) := do
private def expandNatValuePattern (p : Problem) : Problem :=
let alts := p.alts.map fun alt => match alt.patterns with
| Pattern.val (Expr.lit (Literal.natVal 0) _) :: ps => { alt with patterns := Pattern.ctor `Nat.zero [] [] [] :: ps }
| Pattern.val (Expr.lit (Literal.natVal (n+1)) _) :: ps => { alt with patterns := Pattern.ctor `Nat.succ [] [] [Pattern.val (mkRawNatLit n)] :: ps }
| _ => alt
| Pattern.val (Expr.lit (Literal.natVal 0)) :: ps => { alt with patterns := Pattern.ctor `Nat.zero [] [] [] :: ps }
| Pattern.val (Expr.lit (Literal.natVal (n+1))) :: ps => { alt with patterns := Pattern.ctor `Nat.succ [] [] [Pattern.val (mkRawNatLit n)] :: ps }
| _ => alt
{ p with alts := alts }
private def traceStep (msg : String) : StateRefT State MetaM Unit := do

2
stage0/src/Lean/Meta/Match/MatchEqs.lean generated
View file

@ -25,7 +25,7 @@ partial def casesOnStuckLHS (mvarId : MVarId) : MetaM (Array MVarId) := do
where
findFVar? (e : Expr) : MetaM (Option FVarId) := do
match e.getAppFn with
| Expr.proj _ _ e _ => findFVar? e
| Expr.proj _ _ e => findFVar? e
| f =>
if !f.isConst then
return none

2
stage0/src/Lean/Meta/Match/MatcherInfo.lean generated
View file

@ -135,7 +135,7 @@ structure MatcherApp where
def matchMatcherApp? [Monad m] [MonadEnv m] (e : Expr) : m (Option MatcherApp) := do
match e.getAppFn with
| Expr.const declName declLevels _ =>
| Expr.const declName declLevels =>
match (← getMatcherInfo? declName) with
| none => return none
| some info =>

14
stage0/src/Lean/Meta/Offset.lean generated
View file

@ -25,8 +25,8 @@ def isNatProjInst (declName : Name) (numArgs : Nat) : Bool :=
Evaluate simple `Nat` expressions.
Remark: this method assumes the given expression has type `Nat`. -/
partial def evalNat : Expr → OptionT MetaM Nat
| Expr.lit (Literal.natVal n) _ => return n
| Expr.mdata _ e _ => evalNat e
| Expr.lit (Literal.natVal n) => return n
| Expr.mdata _ e => evalNat e
| Expr.const `Nat.zero .. => return 0
| e@(Expr.app ..) => visit e
| e@(Expr.mvar ..) => visit e
@ -36,7 +36,7 @@ where
let f := e.getAppFn
match f with
| Expr.mvar .. => withInstantiatedMVars e evalNat
| Expr.const c _ _ =>
| Expr.const c _ =>
let nargs := e.getAppNumArgs
if c == ``Nat.succ && nargs == 1 then
let v ← evalNat (e.getArg! 0)
@ -61,11 +61,11 @@ where
/- Quick function for converting `e` into `s + k` s.t. `e` is definitionally equal to `Nat.add s k`. -/
private partial def getOffsetAux : Expr → Bool → OptionT MetaM (Expr × Nat)
| e@(Expr.app _ a _), top => do
| e@(Expr.app _ a), top => do
let f := e.getAppFn
match f with
| Expr.mvar .. => withInstantiatedMVars e (getOffsetAux · top)
| Expr.const c _ _ =>
| Expr.const c _ =>
let nargs := e.getAppNumArgs
if c == ``Nat.succ && nargs == 1 then
let (s, k) ← getOffsetAux a false
@ -84,11 +84,11 @@ private def getOffset (e : Expr) : OptionT MetaM (Expr × Nat) :=
getOffsetAux e true
private partial def isOffset : Expr → OptionT MetaM (Expr × Nat)
| e@(Expr.app _ _ _) =>
| e@(Expr.app _ _) =>
let f := e.getAppFn
match f with
| Expr.mvar .. => withInstantiatedMVars e isOffset
| Expr.const c _ _ =>
| Expr.const c _ =>
let nargs := e.getAppNumArgs
if (c == ``Nat.succ && nargs == 1) || (c == ``Nat.add && nargs == 2) || (c == ``Add.add && nargs == 4) || (c == ``HAdd.hAdd && nargs == 6) then
getOffset e

8
stage0/src/Lean/Meta/PPGoal.lean generated
View file

@ -89,10 +89,10 @@ where
| Expr.forallE _ d b _ => visit d; visit b
| Expr.lam _ d b _ => visit d; visit b
| Expr.letE _ t v b _ => visit t; visit v; visit b
| Expr.app f a _ => visit f; visit a
| Expr.mdata _ b _ => visit b
| Expr.proj _ _ b _ => visit b
| Expr.fvar fvarId _ => if (← isMarked fvarId) then unmark fvarId
| Expr.app f a => visit f; visit a
| Expr.mdata _ b => visit b
| Expr.proj _ _ b => visit b
| Expr.fvar fvarId => if (← isMarked fvarId) then unmark fvarId
| _ => pure ()
def fixpointStep : M Unit := do

10
stage0/src/Lean/Meta/RecursorInfo.lean generated
View file

@ -95,7 +95,7 @@ private def getMajorPosIfAuxRecursor? (declName : Name) (majorPos? : Option Nat)
let env ← getEnv
if !isAuxRecursor env declName then pure none
else match declName with
| Name.str p s _ =>
| .str p s =>
if s != recOnSuffix && s != casesOnSuffix && s != brecOnSuffix then
pure none
else do
@ -160,9 +160,9 @@ private def getIndicesPos (declName : Name) (xs : Array Expr) (majorPos numIndic
private def getMotiveLevel (declName : Name) (motiveResultType : Expr) : MetaM Level :=
match motiveResultType with
| Expr.sort u@(Level.zero _) _ => pure u
| Expr.sort u@(Level.param _ _) _ => pure u
| _ =>
| Expr.sort u@(Level.zero) => pure u
| Expr.sort u@(Level.param _) => pure u
| _ =>
throwError "invalid user defined recursor '{declName}', motive result sort must be Prop or (Sort u) where u is a universe level parameter"
private def getUnivLevelPos (declName : Name) (lparams : List Name) (motiveLvl : Level) (Ilevels : List Level) : MetaM (List RecursorUnivLevelPos) := do
@ -214,7 +214,7 @@ private def mkRecursorInfoAux (cinfo : ConstantInfo) (majorPos? : Option Nat) :
let majorType ← inferType major
majorType.withApp fun I Iargs =>
match I with
| Expr.const Iname Ilevels _ => do
| Expr.const Iname Ilevels => do
let paramsPos ← getParamsPos declName xs numParams Iargs
let indicesPos ← getIndicesPos declName xs majorPos numIndices Iargs
let motiveType ← inferType motive

8
stage0/src/Lean/Meta/ReduceEval.lean generated
View file

@ -36,19 +36,19 @@ instance [ReduceEval α] : ReduceEval (Option α) where
instance : ReduceEval String where
reduceEval e := do
let Expr.lit (Literal.strVal s) _ ← whnf e | throwFailedToEval e
let Expr.lit (Literal.strVal s) ← whnf e | throwFailedToEval e
pure s
private partial def evalName (e : Expr) : MetaM Name := do
let e ← whnf e
let Expr.const c _ _ ← pure e.getAppFn | throwFailedToEval e
let Expr.const c _ ← pure e.getAppFn | throwFailedToEval e
let nargs := e.getAppNumArgs
if c == ``Lean.Name.anonymous && nargs == 0 then pure Name.anonymous
else if c == ``Lean.Name.str && nargs == 3 then do
else if c == ``Lean.Name.str && nargs == 2 then do
let n ← evalName $ e.getArg! 0
let s ← reduceEval $ e.getArg! 1
pure $ Name.mkStr n s
else if c == ``Lean.Name.num && nargs == 3 then do
else if c == ``Lean.Name.num && nargs == 2 then do
let n ← evalName $ e.getArg! 0
let u ← reduceEval $ e.getArg! 1
pure $ Name.mkNum n u

2
stage0/src/Lean/Meta/SizeOf.lean generated
View file

@ -340,7 +340,7 @@ mutual
| none => throwFailed
| some (fName, us) =>
let thmLevelParams ← us.mapM fun
| Level.param n _ => return n
| Level.param n => return n
| _ => throwFailed
let thmName := fName.appendAfter "_eq"
if (← getEnv).contains thmName then

30
stage0/src/Lean/Meta/SynthInstance.lean generated
View file

@ -98,10 +98,10 @@ partial def normLevel (u : Level) : M Level := do
if !u.hasMVar then
return u
else match u with
| Level.succ v _ => return u.updateSucc! (← normLevel v)
| Level.max v w _ => return u.updateMax! (← normLevel v) (← normLevel w)
| Level.imax v w _ => return u.updateIMax! (← normLevel v) (← normLevel w)
| Level.mvar mvarId _ =>
| Level.succ v => return u.updateSucc! (← normLevel v)
| Level.max v w => return u.updateMax! (← normLevel v) (← normLevel w)
| Level.imax v w => return u.updateIMax! (← normLevel v) (← normLevel w)
| Level.mvar mvarId =>
if !(← isLevelMVarAssignable mvarId) then
return u
else
@ -118,15 +118,15 @@ partial def normExpr (e : Expr) : M Expr := do
if !e.hasMVar then
pure e
else match e with
| Expr.const _ us _ => return e.updateConst! (← us.mapM normLevel)
| Expr.sort u _ => return e.updateSort! (← normLevel u)
| Expr.app f a _ => return e.updateApp! (← normExpr f) (← normExpr a)
| Expr.const _ us => return e.updateConst! (← us.mapM normLevel)
| Expr.sort u => return e.updateSort! (← normLevel u)
| Expr.app f a => return e.updateApp! (← normExpr f) (← normExpr a)
| Expr.letE _ t v b _ => return e.updateLet! (← normExpr t) (← normExpr v) (← normExpr b)
| Expr.forallE _ d b _ => return e.updateForallE! (← normExpr d) (← normExpr b)
| Expr.lam _ d b _ => return e.updateLambdaE! (← normExpr d) (← normExpr b)
| Expr.mdata _ b _ => return e.updateMData! (← normExpr b)
| Expr.proj _ _ b _ => return e.updateProj! (← normExpr b)
| Expr.mvar mvarId _ =>
| Expr.mdata _ b => return e.updateMData! (← normExpr b)
| Expr.proj _ _ b => return e.updateProj! (← normExpr b)
| Expr.mvar mvarId =>
if !(← isExprMVarAssignable mvarId) then
return e
else
@ -201,7 +201,7 @@ def getInstances (type : Expr) : MetaM (Array Expr) := do
let result := result.insertionSort fun e₁ e₂ => e₁.priority < e₂.priority
let erasedInstances ← getErasedInstances
let result ← result.filterMapM fun e => match e.val with
| Expr.const constName us _ =>
| Expr.const constName us =>
if erasedInstances.contains constName then
return none
else
@ -272,13 +272,13 @@ structure SubgoalsResult where
private partial def getSubgoalsAux (lctx : LocalContext) (localInsts : LocalInstances) (xs : Array Expr)
: Array Expr → Nat → List Expr → Expr → Expr → MetaM SubgoalsResult
| args, j, subgoals, instVal, Expr.forallE _ d b c => do
| args, j, subgoals, instVal, Expr.forallE _ d b bi => do
let d := d.instantiateRevRange j args.size args
let mvarType ← mkForallFVars xs d
let mvar ← mkFreshExprMVarAt lctx localInsts mvarType
let arg := mkAppN mvar xs
let instVal := mkApp instVal arg
let subgoals := if c.binderInfo.isInstImplicit then mvar::subgoals else subgoals
let subgoals := if bi.isInstImplicit then mvar::subgoals else subgoals
let args := args.push (mkAppN mvar xs)
getSubgoalsAux lctx localInsts xs args j subgoals instVal b
| args, j, subgoals, instVal, type => do
@ -308,7 +308,7 @@ def getSubgoals (lctx : LocalContext) (localInsts : LocalInstances) (xs : Array
let instType ← inferType inst
let result ← getSubgoalsAux lctx localInsts xs #[] 0 [] inst instType
match inst.getAppFn with
| Expr.const constName _ _ =>
| Expr.const constName _ =>
let env ← getEnv
if hasInferTCGoalsRLAttribute env constName then
return result
@ -644,7 +644,7 @@ private partial def preprocessArgs (type : Expr) (i : Nat) (args : Array Expr) :
private def preprocessOutParam (type : Expr) : MetaM Expr :=
forallTelescope type fun xs typeBody => do
match typeBody.getAppFn with
| c@(Expr.const constName _ _) =>
| c@(Expr.const constName _) =>
let env ← getEnv
if !hasOutParams env constName then
return type

4
stage0/src/Lean/Meta/Tactic/AC/Main.lean generated
View file

@ -57,8 +57,8 @@ inductive PreExpr
| op (lhs rhs : PreExpr)
| var (e : Expr)
@[matchPattern] def bin {x₁ x₂} (op l r : Expr) :=
Expr.app (Expr.app op l x₁) r x₂
@[matchPattern] def bin (op l r : Expr) :=
Expr.app (Expr.app op l) r
def toACExpr (op l r : Expr) : MetaM (Array Expr × ACExpr) := do
let (preExpr, vars) ←

2
stage0/src/Lean/Meta/Tactic/Cases.lean generated
View file

@ -181,7 +181,7 @@ private def elimAuxIndices (s₁ : GeneralizeIndicesSubgoal) (s₂ : Array Cases
s₂.mapM fun s => do
indicesFVarIds.foldlM (init := s) fun s indexFVarId =>
match s.subst.get indexFVarId with
| Expr.fvar indexFVarId' _ =>
| Expr.fvar indexFVarId' =>
(do let mvarId ← clear s.mvarId indexFVarId'; pure { s with mvarId := mvarId, subst := s.subst.erase indexFVarId })
<|>
(pure s)

4
stage0/src/Lean/Meta/Tactic/ElimInfo.lean generated
View file

@ -67,9 +67,9 @@ partial def addImplicitTargets (elimInfo : ElimInfo) (targets : Array Expr) : Me
where
collect (type : Expr) (argIdx targetIdx : Nat) (targets' : Array Expr) : MetaM (Array Expr) := do
match (← whnfD type) with
| Expr.forallE _ d b c =>
| Expr.forallE _ d b bi =>
if elimInfo.targetsPos.contains argIdx then
if c.binderInfo.isExplicit then
if bi.isExplicit then
unless targetIdx < targets.size do
throwError "insufficient number of targets for '{elimInfo.name}'"
let target := targets[targetIdx]!

2
stage0/src/Lean/Meta/Tactic/FVarSubst.lean generated
View file

@ -52,7 +52,7 @@ def apply (s : FVarSubst) (e : Expr) : Expr :=
if s.map.isEmpty then e
else if !e.hasFVar then e
else e.replace fun e => match e with
| Expr.fvar fvarId _ => match s.map.find? fvarId with
| Expr.fvar fvarId => match s.map.find? fvarId with
| none => e
| some v => v
| _ => none

6
stage0/src/Lean/Meta/Tactic/Induction.lean generated
View file

@ -14,7 +14,7 @@ import Lean.Meta.Tactic.FVarSubst
namespace Lean.Meta
private partial def getTargetArity : Expr → Nat
| Expr.mdata _ b _ => getTargetArity b
| Expr.mdata _ b => getTargetArity b
| Expr.forallE _ _ b _ => getTargetArity b + 1
| e => if e.isHeadBetaTarget then getTargetArity e.headBeta else 0
@ -79,7 +79,7 @@ private partial def finalize
| Expr.forallE n d _ c =>
let d := d.headBeta
-- Remark is givenNames is not empty, then user provided explicit alternatives for each minor premise
if c.binderInfo.isInstImplicit && givenNames.isEmpty then
if c.isInstImplicit && givenNames.isEmpty then
match (← synthInstance? d) with
| some inst =>
let recursor := mkApp recursor inst
@ -181,7 +181,7 @@ def induction (mvarId : MVarId) (majorFVarId : FVarId) (recursorName : Name) (gi
let some majorType ← whnfUntil majorLocalDecl.type recursorInfo.typeName | throwUnexpectedMajorType mvarId majorLocalDecl.type
majorType.withApp fun majorTypeFn majorTypeArgs => do
match majorTypeFn with
| Expr.const _ majorTypeFnLevels _ => do
| Expr.const _ majorTypeFnLevels => do
let majorTypeFnLevels := majorTypeFnLevels.toArray
let (recursorLevels, foundTargetLevel) ← recursorInfo.univLevelPos.foldlM (init := (#[], false))
fun (recursorLevels, foundTargetLevel) (univPos : RecursorUnivLevelPos) => do

6
stage0/src/Lean/Meta/Tactic/Intro.lean generated
View file

@ -38,8 +38,8 @@ namespace Lean.Meta
let type := type.instantiateRevRange j fvars.size fvars
let type := type.headBeta
let fvarId ← mkFreshFVarId
let (n, s) ← mkName lctx n c.binderInfo.isExplicit s
let lctx := lctx.mkLocalDecl fvarId n type c.binderInfo
let (n, s) ← mkName lctx n c.isExplicit s
let lctx := lctx.mkLocalDecl fvarId n type c
let fvar := mkFVar fvarId
let fvars := fvars.push fvar
loop i lctx fvars j s body
@ -123,7 +123,7 @@ abbrev intro1P (mvarId : MVarId) : MetaM (FVarId × MVarId) :=
private def getIntrosSize : Expr → Nat
| Expr.forallE _ _ b _ => getIntrosSize b + 1
| Expr.letE _ _ _ b _ => getIntrosSize b + 1
| Expr.mdata _ b _ => getIntrosSize b
| Expr.mdata _ b => getIntrosSize b
| _ => 0
def intros (mvarId : MVarId) : MetaM (Array FVarId × MVarId) := do

12
stage0/src/Lean/Meta/Tactic/LinearArith/Nat/Basic.lean generated
View file

@ -73,12 +73,12 @@ def addAsVar (e : Expr) : M LinearExpr := do
partial def toLinearExpr (e : Expr) : M LinearExpr := do
match e with
| Expr.lit (Literal.natVal n) _ => return num n
| Expr.mdata _ e _ => toLinearExpr e
| Expr.const ``Nat.zero .. => return num 0
| Expr.app .. => visit e
| Expr.mvar .. => visit e
| _ => addAsVar e
| Expr.lit (Literal.natVal n) => return num n
| Expr.mdata _ e => toLinearExpr e
| Expr.const ``Nat.zero .. => return num 0
| Expr.app .. => visit e
| Expr.mvar .. => visit e
| _ => addAsVar e
where
visit (e : Expr) : M LinearExpr := do
let f := e.getAppFn

2
stage0/src/Lean/Meta/Tactic/Replace.lean generated
View file

@ -111,7 +111,7 @@ def changeLocalDecl (mvarId : MVarId) (fvarId : FVarId) (typeNew : Expr) (checkD
let (_, mvarId) ← introNP mvarId numReverted
pure mvarId
match target with
| Expr.forallE n d b c => do check d; finalize (mkForall n c.binderInfo typeNew b)
| Expr.forallE n d b c => do check d; finalize (mkForall n c typeNew b)
| Expr.letE n t v b _ => do check t; finalize (mkLet n typeNew v b)
| _ => throwTacticEx `changeHypothesis mvarId "unexpected auxiliary target"

4
stage0/src/Lean/Meta/Tactic/Simp/Main.lean generated
View file

@ -199,7 +199,7 @@ partial def lambdaTelescopeDSimp (e : Expr) (k : Array Expr → Expr → M α) :
where
go (xs : Array Expr) (e : Expr) : M α := do
match e with
| .lam n d b c => withLocalDecl n c.binderInfo (← dsimp d) fun x => go (xs.push x) (b.instantiate1 x)
| .lam n d b c => withLocalDecl n c (← dsimp d) fun x => go (xs.push x) (b.instantiate1 x)
| e => k xs e
inductive SimpLetCase where
@ -283,7 +283,7 @@ where
simpStep (e : Expr) : M Result := do
match e with
| Expr.mdata m e _ => let r ← simp e; return { r with expr := mkMData m r.expr }
| Expr.mdata m e => let r ← simp e; return { r with expr := mkMData m r.expr }
| Expr.proj .. => simpProj e
| Expr.app .. => simpApp e
| Expr.lam .. => simpLambda e

8
stage0/src/Lean/Meta/Tactic/Simp/SimpTheorems.lean generated
View file

@ -141,15 +141,15 @@ def SimpTheorems.erase [Monad m] [MonadError m] (d : SimpTheorems) (declName : N
return d.eraseCore declName
private partial def isPerm : Expr → Expr → MetaM Bool
| Expr.app f₁ a₁ _, Expr.app f₂ a₂ _ => isPerm f₁ f₂ <&&> isPerm a₁ a₂
| Expr.mdata _ s _, t => isPerm s t
| s, Expr.mdata _ t _ => isPerm s t
| Expr.app f₁ a₁, Expr.app f₂ a₂ => isPerm f₁ f₂ <&&> isPerm a₁ a₂
| Expr.mdata _ s, t => isPerm s t
| s, Expr.mdata _ t => isPerm s t
| s@(Expr.mvar ..), t@(Expr.mvar ..) => isDefEq s t
| Expr.forallE n₁ d₁ b₁ _, Expr.forallE _ d₂ b₂ _ => isPerm d₁ d₂ <&&> withLocalDeclD n₁ d₁ fun x => isPerm (b₁.instantiate1 x) (b₂.instantiate1 x)
| Expr.lam n₁ d₁ b₁ _, Expr.lam _ d₂ b₂ _ => isPerm d₁ d₂ <&&> withLocalDeclD n₁ d₁ fun x => isPerm (b₁.instantiate1 x) (b₂.instantiate1 x)
| Expr.letE n₁ t₁ v₁ b₁ _, Expr.letE _ t₂ v₂ b₂ _ =>
isPerm t₁ t₂ <&&> isPerm v₁ v₂ <&&> withLetDecl n₁ t₁ v₁ fun x => isPerm (b₁.instantiate1 x) (b₂.instantiate1 x)
| Expr.proj _ i₁ b₁ _, Expr.proj _ i₂ b₂ _ => pure (i₁ == i₂) <&&> isPerm b₁ b₂
| Expr.proj _ i₁ b₁, Expr.proj _ i₂ b₂ => pure (i₁ == i₂) <&&> isPerm b₁ b₂
| s, t => return s == t
private def checkBadRewrite (lhs rhs : Expr) : MetaM Unit := do

2
stage0/src/Lean/Meta/Tactic/Split.lean generated
View file

@ -187,7 +187,7 @@ private def substDiscrEqs (mvarId : MVarId) (fvarSubst : FVarSubst) (discrEqs :
let mut mvarId := mvarId
let mut fvarSubst := fvarSubst
for fvarId in discrEqs do
if let .fvar fvarId _ := fvarSubst.apply (mkFVar fvarId) then
if let .fvar fvarId := fvarSubst.apply (mkFVar fvarId) then
let (fvarId, mvarId') ← heqToEq mvarId fvarId
match (← substCore? mvarId' fvarId (symm := false) fvarSubst) with
| some (fvarSubst', mvarId') => mvarId := mvarId'; fvarSubst := fvarSubst'

2
stage0/src/Lean/Meta/Tactic/Subst.lean generated
View file

@ -26,7 +26,7 @@ def substCore (mvarId : MVarId) (hFVarId : FVarId) (symm := false) (fvarSubst :
let a ← instantiateMVars <| if symm then rhs else lhs
let b ← instantiateMVars <| if symm then lhs else rhs
match a with
| Expr.fvar aFVarId _ => do
| Expr.fvar aFVarId => do
let aFVarIdOriginal := aFVarId
trace[Meta.Tactic.subst] "substituting {a} (id: {aFVarId.name}) with {b}"
if (← exprDependsOn b aFVarId) then

Some files were not shown because too many files have changed in this diff Show more