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:
Leonardo de Moura 2020-01-28 13:11:04 -08:00
parent e9e4dfe1ff
commit a9c06230b2
32 changed files with 13289 additions and 12923 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

215
stage0/src/Init/Coe.lean
View file

@ -1,195 +1,74 @@
/-
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
Copyright (c) 2020 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
/-
The Elaborator tries to insert coercions automatically.
Only instances of HasCoe type class are considered in the process.
Lean also provides a "lifting" operator: ↑a.
It uses all instances of HasLift type class.
Every HasCoe instance is also a HasLift instance.
We recommend users only use HasCoe for coercions that do not produce a lot
of ambiguity.
All coercions and lifts can be identified with the constant coe.
We use the HasCoeToFun type class for encoding coercions from
a Type to a Function space.
We use the HasCoeToSort type class for encoding coercions from
a Type to a sort.
-/
prelude
import Init.Data.List.Basic
universes u v
import Init.HasCoe -- import legacy HasCoe
import Init.Core
class HasLift (a : Sort u) (b : Sort v) :=
(lift : a → b)
universes u v w
/-- Auxiliary class that contains the transitive closure of HasLift. -/
class HasLiftT (a : Sort u) (b : Sort v) :=
(lift : a → b)
class Coe (α : Sort u) (β : Sort v) :=
(coe : α → β)
class HasCoe (a : Sort u) (b : Sort v) :=
(coe : a → b)
class CoeDep (α : Sort u) (a : α) (β : Sort v) :=
(coe : β)
/-- Auxiliary class that contains the transitive closure of HasCoe. -/
class HasCoeT (a : Sort u) (b : Sort v) :=
(coe : a → b)
/-- Auxiliary class that contains the transitive closure of `Coe` and `CoeDep`. -/
class CoeT (α : Sort u) (a : α) (β : Sort v) :=
(coe : β)
class HasCoeToFun (a : Sort u) : Sort (max u (v+1)) :=
(F : a → Sort v) (coe : ∀ x, F x)
class CoeFun (α : Sort u) (a : α) (γ : outParam (Sort v)) :=
(coe : γ)
class HasCoeToSort (a : Sort u) : Type (max u (v+1)) :=
(S : Sort v) (coe : a → S)
class CoeSort (α : Sort u) (a : α) (β : outParam (Sort v)) :=
(coe : β)
@[inline] def lift {a : Sort u} {b : Sort v} [HasLift a b] : a → b :=
@HasLift.lift a b _
abbrev coeB {α : Sort u} {β : Sort v} (a : α) [Coe α β] : β :=
@Coe.coe α β _ a
@[inline] def liftT {a : Sort u} {b : Sort v} [HasLiftT a b] : a → b :=
@HasLiftT.lift a b _
abbrev coeD {α : Sort u} {β : Sort v} (a : α) [CoeDep α a β] : β :=
@CoeDep.coe α a β _
@[inline] def oldCoeB {a : Sort u} {b : Sort v} [HasCoe a b] : a → b :=
@HasCoe.coe a b _
/-- Apply coercion manually. -/
abbrev coe {α : Sort u} {β : Sort v} (a : α) [CoeT α a β] : β :=
@CoeT.coe α a β _
@[inline] def oldCoeT {a : Sort u} {b : Sort v} [HasCoeT a b] : a → b :=
@HasCoeT.coe a b _
abbrev coeFun {α : Sort u} {γ : Sort v} (a : α) [CoeFun α a γ] : γ :=
@CoeFun.coe α a γ _
@[inline] def oldCoeFnB {a : Sort u} [HasCoeToFun.{u, v} a] : ∀ (x : a), HasCoeToFun.F.{u, v} x :=
HasCoeToFun.coe
abbrev coeSort {α : Sort u} {γ : Sort v} (a : α) [CoeSort α a γ] : γ :=
@CoeSort.coe α a γ _
/- User Level coercion operators -/
instance coeDepTrans {α : Sort u} {β : Sort v} {δ : Sort w} (a : α) [CoeT α a β] [CoeDep β (coe a) δ] : CoeT α a δ :=
{ coe := coeD (coe a : β) }
@[reducible, inline] def oldCoe {a : Sort u} {b : Sort v} [HasLiftT a b] : a → b :=
liftT
instance coeTrans {α : Sort u} {β : Sort v} {δ : Sort w} (a : α) [CoeT α a β] [Coe β δ] : CoeT α a δ :=
{ coe := coeB (coe a : β) }
@[reducible, inline] def oldCoeFn {a : Sort u} [HasCoeToFun.{u, v} a] : ∀ (x : a), HasCoeToFun.F.{u, v} x :=
HasCoeToFun.coe
instance coeBase {α : Sort u} {β : Sort v} (a : α) [Coe α β] : CoeT α a β :=
{ coe := coeB a }
@[reducible, inline] def oldCoeSort {a : Sort u} [HasCoeToSort.{u, v} a] : a → HasCoeToSort.S.{u, v} a :=
HasCoeToSort.coe
instance coeDepBase {α : Sort u} {β : Sort v} (a : α) [CoeDep α a β] : CoeT α a β :=
{ coe := coeD a }
@[reducible, inline] def coe {a : Sort u} {b : Sort v} [HasLiftT a b] : a → b :=
liftT
instance coeFunTrans {α : Sort u} {β : Sort v} {γ : Sort w} (a : α) [CoeT α a β] [CoeFun β (coe a) γ] : CoeFun α a γ :=
{ coe := coeFun (coe a : β) }
@[reducible, inline] def coeFn {a : Sort u} [HasCoeToFun.{u, v} a] : ∀ (x : a), HasCoeToFun.F.{u, v} x :=
HasCoeToFun.coe
instance coeSortTrans {α : Sort u} {β : Sort v} {δ : Sort w} (a : α) [CoeT α a β] [CoeSort β (coe a) δ] : CoeFun α a δ :=
{ coe := coeSort (coe a : β) }
@[reducible, inline] def coeSort {a : Sort u} [HasCoeToSort.{u, v} a] : a → HasCoeToSort.S.{u, v} a :=
HasCoeToSort.coe
/- Basic instances -/
/- Notation -/
instance boolToProp : Coe Bool Prop :=
{ coe := fun b => b = true }
universes u₁ u₂ u₃
instance decPropToBool (p : Prop) [Decidable p] : CoeDep Prop p Bool :=
{ coe := decide p }
/- Transitive closure for HasLift, HasCoe, HasCoeToFun -/
instance optionCoe {α : Type u} : Coe α (Option α) :=
{ coe := some }
instance liftTrans {a : Sort u₁} {b : Sort u₂} {c : Sort u₃} [HasLiftT b c] [HasLift a b] : HasLiftT a c :=
⟨fun x => liftT (lift x : b)⟩
instance liftRefl {a : Sort u} : HasLiftT a a :=
⟨id⟩
instance coeTrans {a : Sort u₁} {b : Sort u₂} {c : Sort u₃} [HasCoeT b c] [HasCoe a b] : HasCoeT a c :=
⟨fun x => oldCoeT (oldCoeB x : b)⟩
instance coeBase {a : Sort u} {b : Sort v} [HasCoe a b] : HasCoeT a b :=
⟨oldCoeB⟩
/- We add this instance directly into HasCoeT to avoid non-termination.
Suppose coeOption had Type (HasCoe a (Option a)).
Then, we can loop when searching a coercion from α to β (HasCoeT α β)
1- coeTrans at (HasCoeT α β)
(HasCoe α ?b₁) and (HasCoeT ?b₁ c)
2- coeOption at (HasCoe α ?b₁)
?b₁ := Option α
3- coeTrans at (HasCoeT (Option α) β)
(HasCoe (Option α) ?b₂) and (HasCoeT ?b₂ β)
4- coeOption at (HasCoe (Option α) ?b₂)
?b₂ := Option (Option α))
...
-/
instance coeOption {a : Type u} : HasCoeT a (Option a) :=
⟨fun x => some x⟩
/- Auxiliary transitive closure for HasCoe which does not contain
instances such as coeOption.
They would produce non-termination when combined with coeFnTrans and coeSortTrans.
-/
class HasCoeTAux (a : Sort u) (b : Sort v) :=
(coe : a → b)
instance coeTransAux {a : Sort u₁} {b : Sort u₂} {c : Sort u₃} [HasCoeTAux b c] [HasCoe a b] : HasCoeTAux a c :=
⟨fun x => @HasCoeTAux.coe b c _ (oldCoeB x)⟩
instance coeBaseAux {a : Sort u} {b : Sort v} [HasCoe a b] : HasCoeTAux a b :=
⟨oldCoeB⟩
instance coeFnTrans {a : Sort u₁} {b : Sort u₂} [HasCoeToFun.{u₂, u₃} b] [HasCoeTAux a b] : HasCoeToFun.{u₁, u₃} a :=
{ F := fun x => @HasCoeToFun.F.{u₂, u₃} b _ (@HasCoeTAux.coe a b _ x),
coe := fun x => oldCoeFn (@HasCoeTAux.coe a b _ x) }
instance coeSortTrans {a : Sort u₁} {b : Sort u₂} [HasCoeToSort.{u₂, u₃} b] [HasCoeTAux a b] : HasCoeToSort.{u₁, u₃} a :=
{ S := HasCoeToSort.S.{u₂, u₃} b,
coe := fun x => oldCoeSort (@HasCoeTAux.coe a b _ x) }
/- Every coercion is also a lift -/
instance coeToLift {a : Sort u} {b : Sort v} [HasCoeT a b] : HasLiftT a b :=
⟨oldCoeT⟩
instance oldCoeToLift {a : Sort u} {b : Sort v} [HasCoeT a b] : HasLiftT a b :=
⟨oldCoeT⟩
/- basic coercions -/
instance coeBoolToProp : HasCoe Bool Prop :=
⟨fun y => y = true⟩
/- Tactics such as the simplifier only unfold reducible constants when checking whether two terms are definitionally
equal or a Term is a proposition. The motivation is performance.
In particular, when simplifying `p -> q`, the tactic `simp` only visits `p` if it can establish that it is a proposition.
Thus, we mark the following instance as @[reducible], otherwise `simp` will not visit `↑p` when simplifying `↑p -> q`.
-/
@[reducible] instance coeSortBool : HasCoeToSort Bool :=
⟨Prop, fun y => y = true⟩
instance coeDecidableEq (x : Bool) : Decidable (oldCoe x) :=
inferInstanceAs (Decidable (x = true))
instance coeSubtype {a : Sort u} {p : a → Prop} : HasCoe {x // p x} a :=
⟨Subtype.val⟩
/- basic lifts -/
universes ua ua₁ ua₂ ub ub₁ ub₂
/- Remark: we can't use [HasLiftT a₂ a₁] since it will produce non-termination whenever a type class resolution
problem does not have a solution. -/
instance liftFn {a₁ : Sort ua₁} {a₂ : Sort ua₂} {b₁ : Sort ub₁} {b₂ : Sort ub₂} [HasLiftT b₁ b₂] [HasLift a₂ a₁] : HasLift (a₁ → b₁) (a₂ → b₂) :=
⟨fun f x => oldCoe (f (oldCoe x))⟩
instance liftFnRange {a : Sort ua} {b₁ : Sort ub₁} {b₂ : Sort ub₂} [HasLiftT b₁ b₂] : HasLift (a → b₁) (a → b₂) :=
⟨fun f x => oldCoe (f x)⟩
instance liftFnDom {a₁ : Sort ua₁} {a₂ : Sort ua₂} {b : Sort ub} [HasLift a₂ a₁] : HasLift (a₁ → b) (a₂ → b) :=
⟨fun f x => f (oldCoe x)⟩
instance liftPair {a₁ : Type ua₁} {a₂ : Type ub₂} {b₁ : Type ub₁} {b₂ : Type ub₂} [HasLiftT a₁ a₂] [HasLiftT b₁ b₂] : HasLift (a₁ × b₁) (a₂ × b₂) :=
⟨fun p => Prod.casesOn p (fun x y => (oldCoe x, oldCoe y))⟩
instance liftPair₁ {a₁ : Type ua₁} {a₂ : Type ua₂} {b : Type ub} [HasLiftT a₁ a₂] : HasLift (a₁ × b) (a₂ × b) :=
⟨fun p => Prod.casesOn p (fun x y => (oldCoe x, y))⟩
instance liftPair₂ {a : Type ua} {b₁ : Type ub₁} {b₂ : Type ub₂} [HasLiftT b₁ b₂] : HasLift (a × b₁) (a × b₂) :=
⟨fun p => Prod.casesOn p (fun x y => (x, oldCoe y))⟩
instance liftList {a : Type u} {b : Type v} [HasLiftT a b] : HasLift (List a) (List b) :=
⟨fun l => List.map (@oldCoe a b _) l⟩
instance subtypeCoe {α : Sort u} {p : α → Prop} (v : { x // p x }) : CoeT { x // p x } v α :=
{ coe := v.val }

6
stage0/src/Init/Control/Lift.lean
View file

@ -9,7 +9,6 @@ This theory is roughly modeled after the Haskell 'layers' package https://hackag
Please see https://hackage.haskell.org/package/layers-0.1/docs/Documentation-Layers-Overview.html for an exhaustive discussion of the different approaches to lift functions.
-/
prelude
import Init.Coe
import Init.Control.Monad
universes u v w
@ -31,11 +30,6 @@ export HasMonadLiftT (monadLift)
abbrev liftM := @monadLift
/-- A coercion that may reduce the need for explicit lifting.
Because of [limitations of the current coercion resolution](https://github.com/leanprover/Lean/issues/1402), this definition is not marked as a global instance and should be marked locally instead. -/
@[reducible] def hasMonadLiftToHasCoe {m n} [HasMonadLiftT m n] {α} : HasCoe (m α) (n α) :=
⟨monadLift⟩
instance hasMonadLiftTTrans (m n o) [HasMonadLift n o] [HasMonadLiftT m n] : HasMonadLiftT m o :=
⟨fun α ma => HasMonadLift.monadLift (monadLift ma : n α)⟩

1
stage0/src/Init/Data/BinomialHeap/Basic.lean
View file

@ -5,7 +5,6 @@ Authors: Leonardo de Moura
-/
prelude
import Init.Data.List
import Init.Coe
universes u
namespace BinomialHeapImp

1
stage0/src/Init/Data/Int/Basic.lean
View file

@ -8,7 +8,6 @@ The integers, with addition, multiplication, and subtraction.
prelude
import Init.Data.Nat.Basic
import Init.Data.List
import Init.Coe
import Init.Data.Repr
import Init.Data.ToString
open Nat

1
stage0/src/Init/Default.lean
View file

@ -7,7 +7,6 @@ prelude
import Init.Core
import Init.Control
import Init.Data.Basic
import Init.Coe
import Init.WF
import Init.Data
import Init.System

189
stage0/src/Init/HasCoe.lean Normal file
View file

@ -0,0 +1,189 @@
/-
Copyright (c) 2016 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
/-
The Elaborator tries to insert coercions automatically.
Only instances of HasCoe type class are considered in the process.
Lean also provides a "lifting" operator: ↑a.
It uses all instances of HasLift type class.
Every HasCoe instance is also a HasLift instance.
We recommend users only use HasCoe for coercions that do not produce a lot
of ambiguity.
All coercions and lifts can be identified with the constant coe.
We use the HasCoeToFun type class for encoding coercions from
a Type to a Function space.
We use the HasCoeToSort type class for encoding coercions from
a Type to a sort.
-/
prelude
import Init.Data.List.Basic
universes u v
class HasLift (a : Sort u) (b : Sort v) :=
(lift : a → b)
/-- Auxiliary class that contains the transitive closure of HasLift. -/
class HasLiftT (a : Sort u) (b : Sort v) :=
(lift : a → b)
class HasCoe (a : Sort u) (b : Sort v) :=
(coe : a → b)
/-- Auxiliary class that contains the transitive closure of HasCoe. -/
class HasCoeT (a : Sort u) (b : Sort v) :=
(coe : a → b)
class HasCoeToFun (a : Sort u) : Sort (max u (v+1)) :=
(F : a → Sort v) (coe : ∀ x, F x)
class HasCoeToSort (a : Sort u) : Type (max u (v+1)) :=
(S : Sort v) (coe : a → S)
@[inline] def lift {a : Sort u} {b : Sort v} [HasLift a b] : a → b :=
@HasLift.lift a b _
@[inline] def liftT {a : Sort u} {b : Sort v} [HasLiftT a b] : a → b :=
@HasLiftT.lift a b _
@[inline] def oldCoeB {a : Sort u} {b : Sort v} [HasCoe a b] : a → b :=
@HasCoe.coe a b _
@[inline] def oldCoeT {a : Sort u} {b : Sort v} [HasCoeT a b] : a → b :=
@HasCoeT.coe a b _
@[inline] def oldCoeFnB {a : Sort u} [HasCoeToFun.{u, v} a] : ∀ (x : a), HasCoeToFun.F.{u, v} x :=
HasCoeToFun.coe
/- User Level coercion operators -/
@[reducible, inline] def oldCoe {a : Sort u} {b : Sort v} [HasLiftT a b] : a → b :=
liftT
@[reducible, inline] def oldCoeFn {a : Sort u} [HasCoeToFun.{u, v} a] : ∀ (x : a), HasCoeToFun.F.{u, v} x :=
HasCoeToFun.coe
@[reducible, inline] def oldCoeSort {a : Sort u} [HasCoeToSort.{u, v} a] : a → HasCoeToSort.S.{u, v} a :=
HasCoeToSort.coe
/- Notation -/
universes u₁ u₂ u₃
/- Transitive closure for HasLift, HasCoe, HasCoeToFun -/
namespace Legacy
instance liftTrans {a : Sort u₁} {b : Sort u₂} {c : Sort u₃} [HasLiftT b c] [HasLift a b] : HasLiftT a c :=
⟨fun x => liftT (lift x : b)⟩
instance liftRefl {a : Sort u} : HasLiftT a a :=
⟨id⟩
instance coeoeTrans {a : Sort u₁} {b : Sort u₂} {c : Sort u₃} [HasCoeT b c] [HasCoe a b] : HasCoeT a c :=
⟨fun x => oldCoeT (oldCoeB x : b)⟩
instance coeBase {a : Sort u} {b : Sort v} [HasCoe a b] : HasCoeT a b :=
⟨oldCoeB⟩
/- We add this instance directly into HasCoeT to avoid non-termination.
Suppose coeOption had Type (HasCoe a (Option a)).
Then, we can loop when searching a coercion from α to β (HasCoeT α β)
1- coeTrans at (HasCoeT α β)
(HasCoe α ?b₁) and (HasCoeT ?b₁ c)
2- coeOption at (HasCoe α ?b₁)
?b₁ := Option α
3- coeTrans at (HasCoeT (Option α) β)
(HasCoe (Option α) ?b₂) and (HasCoeT ?b₂ β)
4- coeOption at (HasCoe (Option α) ?b₂)
?b₂ := Option (Option α))
...
-/
instance oldCoeOption {a : Type u} : HasCoeT a (Option a) :=
⟨fun x => some x⟩
/- Auxiliary transitive closure for HasCoe which does not contain
instances such as coeOption.
They would produce non-termination when combined with coeFnTrans and coeSortTrans.
-/
class HasCoeTAux (a : Sort u) (b : Sort v) :=
(coe : a → b)
instance coeTransAux {a : Sort u₁} {b : Sort u₂} {c : Sort u₃} [HasCoeTAux b c] [HasCoe a b] : HasCoeTAux a c :=
⟨fun x => @HasCoeTAux.coe b c _ (oldCoeB x)⟩
instance coeBaseAux {a : Sort u} {b : Sort v} [HasCoe a b] : HasCoeTAux a b :=
⟨oldCoeB⟩
instance coeFnTrans {a : Sort u₁} {b : Sort u₂} [HasCoeToFun.{u₂, u₃} b] [HasCoeTAux a b] : HasCoeToFun.{u₁, u₃} a :=
{ F := fun x => @HasCoeToFun.F.{u₂, u₃} b _ (@HasCoeTAux.coe a b _ x),
coe := fun x => oldCoeFn (@HasCoeTAux.coe a b _ x) }
instance coeSortTrans {a : Sort u₁} {b : Sort u₂} [HasCoeToSort.{u₂, u₃} b] [HasCoeTAux a b] : HasCoeToSort.{u₁, u₃} a :=
{ S := HasCoeToSort.S.{u₂, u₃} b,
coe := fun x => oldCoeSort (@HasCoeTAux.coe a b _ x) }
/- Every coercion is also a lift -/
instance coeToLift {a : Sort u} {b : Sort v} [HasCoeT a b] : HasLiftT a b :=
⟨oldCoeT⟩
/- basic coercions -/
instance coeBoolToProp : HasCoe Bool Prop :=
⟨fun y => y = true⟩
/- Tactics such as the simplifier only unfold reducible constants when checking whether two terms are definitionally
equal or a Term is a proposition. The motivation is performance.
In particular, when simplifying `p -> q`, the tactic `simp` only visits `p` if it can establish that it is a proposition.
Thus, we mark the following instance as @[reducible], otherwise `simp` will not visit `↑p` when simplifying `↑p -> q`.
-/
@[reducible] instance coeSortBool : HasCoeToSort Bool :=
⟨Prop, fun y => y = true⟩
instance coeDecidableEq (x : Bool) : Decidable (oldCoe x) :=
inferInstanceAs (Decidable (x = true))
instance coeSubtype {a : Sort u} {p : a → Prop} : HasCoe {x // p x} a :=
⟨Subtype.val⟩
/- basic lifts -/
universes ua ua₁ ua₂ ub ub₁ ub₂
/- Remark: we can't use [HasLiftT a₂ a₁] since it will produce non-termination whenever a type class resolution
problem does not have a solution. -/
instance liftFn {a₁ : Sort ua₁} {a₂ : Sort ua₂} {b₁ : Sort ub₁} {b₂ : Sort ub₂} [HasLiftT b₁ b₂] [HasLift a₂ a₁] : HasLift (a₁ → b₁) (a₂ → b₂) :=
⟨fun f x => oldCoe (f (oldCoe x))⟩
instance liftFnRange {a : Sort ua} {b₁ : Sort ub₁} {b₂ : Sort ub₂} [HasLiftT b₁ b₂] : HasLift (a → b₁) (a → b₂) :=
⟨fun f x => oldCoe (f x)⟩
instance liftFnDom {a₁ : Sort ua₁} {a₂ : Sort ua₂} {b : Sort ub} [HasLift a₂ a₁] : HasLift (a₁ → b) (a₂ → b) :=
⟨fun f x => f (oldCoe x)⟩
instance liftPair {a₁ : Type ua₁} {a₂ : Type ub₂} {b₁ : Type ub₁} {b₂ : Type ub₂} [HasLiftT a₁ a₂] [HasLiftT b₁ b₂] : HasLift (a₁ × b₁) (a₂ × b₂) :=
⟨fun p => Prod.casesOn p (fun x y => (oldCoe x, oldCoe y))⟩
instance liftPair₁ {a₁ : Type ua₁} {a₂ : Type ua₂} {b : Type ub} [HasLiftT a₁ a₂] : HasLift (a₁ × b) (a₂ × b) :=
⟨fun p => Prod.casesOn p (fun x y => (oldCoe x, y))⟩
instance liftPair₂ {a : Type ua} {b₁ : Type ub₁} {b₂ : Type ub₂} [HasLiftT b₁ b₂] : HasLift (a × b₁) (a × b₂) :=
⟨fun p => Prod.casesOn p (fun x y => (x, oldCoe y))⟩
instance liftList {a : Type u} {b : Type v} [HasLiftT a b] : HasLift (List a) (List b) :=
⟨fun l => List.map (@oldCoe a b _) l⟩
end Legacy
instance oldCoeToLift {a : Sort u} {b : Sort v} [HasCoeT a b] : HasLiftT a b :=
⟨oldCoeT⟩

1
stage0/src/Init/Lean/Data/Name.lean
View file

@ -4,7 +4,6 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
-/
prelude
import Init.Coe
import Init.LeanInit
import Init.Data.UInt
import Init.Data.ToString

4
stage0/src/Init/Lean/Meta/Message.lean
View file

@ -71,8 +71,8 @@ def toMessageData : Exception → MessageData
| invalidProjection s i e ctx => mkCtx ctx $ "invalid projection" ++ indentExpr (mkProj s i e)
| revertFailure xs decl ctx => mkCtx ctx $ "revert failure"
| readOnlyMVar mvarId ctx => mkCtx ctx $ "tried to update read only metavariable " ++ mkMVar mvarId
| isLevelDefEqStuck u v ctx => mkCtx ctx $ "stuck at " ++ u ++ " =?= " ++ v
| isExprDefEqStuck t s ctx => mkCtx ctx $ "stuck at " ++ t ++ " =?= " ++ s
| isLevelDefEqStuck u v ctx => mkCtx ctx $ "stuck at universe level constraint " ++ u ++ " =?= " ++ v
| isExprDefEqStuck t s ctx => mkCtx ctx $ "stuck at constraint " ++ t ++ " =?= " ++ s
| letTypeMismatch fvarId ctx => mkLetTypeMismatchMessage fvarId ctx
| appTypeMismatch f a ctx => mkAppTypeMismatchMessage f a ctx
| notInstance i ctx => mkCtx ctx $ "not a type class instance " ++ i

62
stage0/src/Init/Lean/Meta/SynthInstance.lean
View file

@ -483,21 +483,18 @@ us ← us.foldlM
[];
pure $ us.reverse
private partial def preprocessArgs (ys : Array Expr) : Nat → Array Expr → MetaM (Array Expr)
| i, args => do
if h : i < ys.size then do
let y := ys.get ⟨i, h⟩;
yType ← inferType y;
if isOutParam yType then do
if h : i < args.size then do
let arg := args.get ⟨i, h⟩;
argType ← inferType arg;
arg' ← mkFreshExprMVar argType;
preprocessArgs (i+1) (args.set ⟨i, h⟩ arg')
else
throw $ Exception.other "type class resolution failed, insufficient number of arguments" -- TODO improve error message
else
preprocessArgs (i+1) args
private partial def preprocessArgs : Expr → Nat → Array Expr → MetaM (Array Expr)
| type, i, args =>
if h : i < args.size then do
type ← whnf type;
match type with
| Expr.forallE _ d b _ => do
let arg := args.get ⟨i, h⟩;
arg ← if isOutParam d then mkFreshExprMVar d else pure arg;
let args := args.set ⟨i, h⟩ arg;
preprocessArgs (b.instantiate1 arg) (i+1) args
| _ =>
throw $ Exception.other "type class resolution failed, insufficient number of arguments" -- TODO improve error message
else
pure args
@ -509,15 +506,13 @@ forallTelescope type $ fun xs typeBody =>
if !hasOutParams env constName then pure type
else do
let args := typeBody.getAppArgs;
us ← preprocessLevels us;
let c := mkConst constName us;
cType ← inferType c;
forallTelescopeReducing cType $ fun ys _ => do
us ← preprocessLevels us;
args ← preprocessArgs ys 0 args;
type ← mkForall xs (mkAppN (mkConst constName us) args);
pure type
args ← preprocessArgs cType 0 args;
mkForall xs (mkAppN c args)
| _ => pure type
@[init] def maxStepsOption : IO Unit :=
registerOption `synthInstance.maxSteps { defValue := (10000 : Nat), group := "", descr := "maximum steps for the type class instance synthesis procedure" }
@ -535,25 +530,34 @@ withConfig (fun config => { transparency := TransparencyMode.reducible, foApprox
match s.cache.synthInstance.find? type with
| some result => pure result
| none => do
result ← withNewMCtxDepth $ do {
result? ← withNewMCtxDepth $ do {
normType ← preprocessOutParam type;
trace! `Meta.synthInstance (type ++ " ==> " ++ normType);
result? ← SynthInstance.main normType fuel;
match result? with
| none => pure none
| some result => do
trace! `Meta.synthInstance ("FOUND result " ++ result);
result ← instantiateMVars result;
condM (hasAssignableMVar result)
(pure none)
(pure (some result))
};
result? ← match result? with
| none => pure none
| some result => do {
trace! `Meta.synthInstance ("result " ++ result);
resultType ← inferType result;
condM (withConfig (fun _ => inputConfig) $ isDefEq type resultType)
(do result ← instantiateMVars result;
condM (hasAssignableMVar result)
(pure none)
(pure (some result)))
pure (some result))
(pure none)
};
};
if type.hasMVar then
pure result
pure result?
else do
modify $ fun s => { cache := { synthInstance := s.cache.synthInstance.insert type result, .. s.cache }, .. s };
pure result
modify $ fun s => { cache := { synthInstance := s.cache.synthInstance.insert type result?, .. s.cache }, .. s };
pure result?
/--
Return `LOption.some r` if succeeded, `LOption.none` if it failed, and `LOption.undef` if

2
stage0/stdlib/CMakeLists.txt
View file

File diff suppressed because one or more lines are too long

1022
stage0/stdlib/Init/Coe.c
View file

File diff suppressed because it is too large Load diff

65
stage0/stdlib/Init/Control/Lift.c
View file

@ -1,6 +1,6 @@
// Lean compiler output
// Module: Init.Control.Lift
// Imports: Init.Coe Init.Control.Monad
// Imports: Init.Control.Monad
#include "runtime/lean.h"
#if defined(__clang__)
#pragma clang diagnostic ignored "-Wunused-parameter"
@ -20,22 +20,16 @@ lean_object* l_hasMonadLiftTTrans___rarg(lean_object*, lean_object*, lean_object
lean_object* l_hasMonadLiftTRefl(lean_object*, lean_object*);
lean_object* l_monadFunctorTRefl___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_liftM___boxed(lean_object*, lean_object*);
lean_object* l_hasMonadLiftToHasCoe___boxed(lean_object*, lean_object*);
lean_object* l_monadFunctorTTrans___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_monadFunctorTTrans___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_hasMonadLiftToHasCoe___elambda__1(lean_object*, lean_object*, lean_object*);
lean_object* l_hasMonadLiftTTrans(lean_object*, lean_object*, lean_object*);
lean_object* l_monadFunctorTRefl(lean_object*, lean_object*, lean_object*);
lean_object* l_hasMonadLiftTTrans___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_hasMonadLiftToHasCoe___elambda__1___rarg(lean_object*, lean_object*);
lean_object* l_hasMonadLiftToHasCoe(lean_object*, lean_object*);
lean_object* l_liftM(lean_object*, lean_object*);
lean_object* l_hasMonadLiftTRefl___rarg___boxed(lean_object*);
lean_object* l_monadFunctorTTrans___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_hasMonadLiftToHasCoe___elambda__1___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_monadFunctorTRefl___rarg(lean_object*, lean_object*);
lean_object* l_liftM___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_hasMonadLiftToHasCoe___rarg(lean_object*, lean_object*);
lean_object* l_liftM___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
@ -62,59 +56,6 @@ lean_dec(x_1);
return x_3;
}
}
lean_object* l_hasMonadLiftToHasCoe___elambda__1___rarg(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = lean_apply_2(x_1, lean_box(0), x_2);
return x_3;
}
}
lean_object* l_hasMonadLiftToHasCoe___elambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
x_4 = lean_alloc_closure((void*)(l_hasMonadLiftToHasCoe___elambda__1___rarg), 2, 0);
return x_4;
}
}
lean_object* l_hasMonadLiftToHasCoe___rarg(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = lean_alloc_closure((void*)(l_hasMonadLiftToHasCoe___elambda__1___rarg), 2, 1);
lean_closure_set(x_3, 0, x_1);
return x_3;
}
}
lean_object* l_hasMonadLiftToHasCoe(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = lean_alloc_closure((void*)(l_hasMonadLiftToHasCoe___rarg), 2, 0);
return x_3;
}
}
lean_object* l_hasMonadLiftToHasCoe___elambda__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
x_4 = l_hasMonadLiftToHasCoe___elambda__1(x_1, x_2, x_3);
lean_dec(x_2);
lean_dec(x_1);
return x_4;
}
}
lean_object* l_hasMonadLiftToHasCoe___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = l_hasMonadLiftToHasCoe(x_1, x_2);
lean_dec(x_2);
lean_dec(x_1);
return x_3;
}
}
lean_object* l_hasMonadLiftTTrans___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
@ -243,16 +184,12 @@ lean_dec(x_1);
return x_4;
}
}
lean_object* initialize_Init_Coe(lean_object*);
lean_object* initialize_Init_Control_Monad(lean_object*);
static bool _G_initialized = false;
lean_object* initialize_Init_Control_Lift(lean_object* w) {
lean_object * res;
if (_G_initialized) return lean_mk_io_result(lean_box(0));
_G_initialized = true;
res = initialize_Init_Coe(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Init_Control_Monad(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);

6
stage0/stdlib/Init/Data/BinomialHeap/Basic.c
View file

@ -1,6 +1,6 @@
// Lean compiler output
// Module: Init.Data.BinomialHeap.Basic
// Imports: Init.Data.List Init.Coe
// Imports: Init.Data.List
#include "runtime/lean.h"
#if defined(__clang__)
#pragma clang diagnostic ignored "-Wunused-parameter"
@ -1434,7 +1434,6 @@ return x_2;
}
}
lean_object* initialize_Init_Data_List(lean_object*);
lean_object* initialize_Init_Coe(lean_object*);
static bool _G_initialized = false;
lean_object* initialize_Init_Data_BinomialHeap_Basic(lean_object* w) {
lean_object * res;
@ -1443,9 +1442,6 @@ _G_initialized = true;
res = initialize_Init_Data_List(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Init_Coe(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
return lean_mk_io_result(lean_box(0));
}
#ifdef __cplusplus

6
stage0/stdlib/Init/Data/Int/Basic.c
View file

@ -1,6 +1,6 @@
// Lean compiler output
// Module: Init.Data.Int.Basic
// Imports: Init.Data.Nat.Basic Init.Data.List Init.Coe Init.Data.Repr Init.Data.ToString
// Imports: Init.Data.Nat.Basic Init.Data.List Init.Data.Repr Init.Data.ToString
#include "runtime/lean.h"
#if defined(__clang__)
#pragma clang diagnostic ignored "-Wunused-parameter"
@ -744,7 +744,6 @@ return x_3;
}
lean_object* initialize_Init_Data_Nat_Basic(lean_object*);
lean_object* initialize_Init_Data_List(lean_object*);
lean_object* initialize_Init_Coe(lean_object*);
lean_object* initialize_Init_Data_Repr(lean_object*);
lean_object* initialize_Init_Data_ToString(lean_object*);
static bool _G_initialized = false;
@ -758,9 +757,6 @@ lean_dec_ref(res);
res = initialize_Init_Data_List(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Init_Coe(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Init_Data_Repr(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);

6
stage0/stdlib/Init/Default.c
View file

@ -1,6 +1,6 @@
// Lean compiler output
// Module: Init.Default
// Imports: Init.Core Init.Control Init.Data.Basic Init.Coe Init.WF Init.Data Init.System Init.Util Init.Fix Init.LeanInit
// Imports: Init.Core Init.Control Init.Data.Basic Init.WF Init.Data Init.System Init.Util Init.Fix Init.LeanInit
#include "runtime/lean.h"
#if defined(__clang__)
#pragma clang diagnostic ignored "-Wunused-parameter"
@ -16,7 +16,6 @@ extern "C" {
lean_object* initialize_Init_Core(lean_object*);
lean_object* initialize_Init_Control(lean_object*);
lean_object* initialize_Init_Data_Basic(lean_object*);
lean_object* initialize_Init_Coe(lean_object*);
lean_object* initialize_Init_WF(lean_object*);
lean_object* initialize_Init_Data(lean_object*);
lean_object* initialize_Init_System(lean_object*);
@ -37,9 +36,6 @@ lean_dec_ref(res);
res = initialize_Init_Data_Basic(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Init_Coe(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Init_WF(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);

708
stage0/stdlib/Init/HasCoe.c Normal file
View file

@ -0,0 +1,708 @@
// Lean compiler output
// Module: Init.HasCoe
// Imports: Init.Data.List.Basic
#include "runtime/lean.h"
#if defined(__clang__)
#pragma clang diagnostic ignored "-Wunused-parameter"
#pragma clang diagnostic ignored "-Wunused-label"
#elif defined(__GNUC__) && !defined(__CLANG__)
#pragma GCC diagnostic ignored "-Wunused-parameter"
#pragma GCC diagnostic ignored "-Wunused-label"
#pragma GCC diagnostic ignored "-Wunused-but-set-variable"
#endif
#ifdef __cplusplus
extern "C" {
#endif
lean_object* l_Legacy_coeSubtype(lean_object*, lean_object*);
lean_object* l_Legacy_liftPair_u2082(lean_object*, lean_object*, lean_object*);
lean_object* l_Legacy_coeoeTrans(lean_object*, lean_object*, lean_object*);
lean_object* l_oldCoeSort___rarg(lean_object*, lean_object*);
lean_object* l_Legacy_liftFnRange___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Legacy_coeSubtype___rarg(lean_object*);
lean_object* l_Legacy_liftTrans___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Legacy_coeToLift(lean_object*, lean_object*);
lean_object* l_oldCoeT___rarg(lean_object*, lean_object*);
lean_object* l_Legacy_liftFnDom(lean_object*, lean_object*, lean_object*);
lean_object* l_lift(lean_object*, lean_object*);
lean_object* l_oldCoeFnB___rarg(lean_object*, lean_object*);
lean_object* l_Legacy_coeBase___rarg(lean_object*);
lean_object* l_Legacy_coeBaseAux___rarg(lean_object*);
uint8_t l_Legacy_coeDecidableEq(uint8_t);
lean_object* l_oldCoeFn(lean_object*);
lean_object* l_Legacy_oldCoeOption___rarg(lean_object*);
lean_object* l_oldCoe(lean_object*, lean_object*);
lean_object* l_oldCoeFn___rarg(lean_object*, lean_object*);
extern lean_object* l_Nat_HasOfNat___closed__1;
lean_object* l_Legacy_liftFn___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_oldCoe___rarg(lean_object*, lean_object*);
lean_object* l_Legacy_coeBase(lean_object*, lean_object*);
lean_object* l_oldCoeToLift(lean_object*, lean_object*);
lean_object* l_Legacy_liftRefl(lean_object*);
lean_object* l_Legacy_coeBaseAux(lean_object*, lean_object*);
lean_object* l_Legacy_liftList___rarg(lean_object*, lean_object*);
lean_object* l_Legacy_coeSortTrans(lean_object*, lean_object*);
lean_object* l_liftT(lean_object*, lean_object*);
lean_object* l_Legacy_coeBoolToProp;
lean_object* l_Legacy_liftList(lean_object*, lean_object*);
lean_object* l_oldCoeB___rarg(lean_object*, lean_object*);
lean_object* l_oldCoeSort(lean_object*);
lean_object* l_Legacy_liftPair_u2081(lean_object*, lean_object*, lean_object*);
lean_object* l_Legacy_coeFnTrans___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Legacy_coeSortBool;
lean_object* l_Legacy_liftFnDom___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Legacy_coeSubtype___boxed(lean_object*, lean_object*);
lean_object* l_Legacy_coeTransAux(lean_object*, lean_object*, lean_object*);
lean_object* l_oldCoeFnB(lean_object*);
lean_object* l_Legacy_coeoeTrans___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Legacy_coeTransAux___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Legacy_liftPair_u2081___rarg(lean_object*, lean_object*);
lean_object* l_Legacy_liftFn(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Legacy_coeSubtype___rarg___boxed(lean_object*);
lean_object* l_Legacy_coeSortTrans___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Legacy_liftPair(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Legacy_oldCoeOption(lean_object*);
lean_object* l_Legacy_coeToLift___rarg(lean_object*);
lean_object* l_oldCoeToLift___rarg(lean_object*);
lean_object* l_Legacy_coeFnTrans(lean_object*, lean_object*);
lean_object* l_List_map___main___at_Legacy_liftList___spec__1(lean_object*, lean_object*);
lean_object* l_oldCoeT(lean_object*, lean_object*);
lean_object* l_List_map___main___at_Legacy_liftList___spec__1___rarg(lean_object*, lean_object*);
lean_object* l_oldCoeB(lean_object*, lean_object*);
lean_object* l_lift___rarg(lean_object*, lean_object*);
lean_object* l_Legacy_liftTrans(lean_object*, lean_object*, lean_object*);
lean_object* l_Legacy_liftPair___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Legacy_liftFnRange(lean_object*, lean_object*, lean_object*);
lean_object* l_Legacy_coeDecidableEq___boxed(lean_object*);
lean_object* l_Legacy_liftPair_u2082___rarg(lean_object*, lean_object*);
lean_object* l_liftT___rarg(lean_object*, lean_object*);
lean_object* l_lift___rarg(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = lean_apply_1(x_1, x_2);
return x_3;
}
}
lean_object* l_lift(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = lean_alloc_closure((void*)(l_lift___rarg), 2, 0);
return x_3;
}
}
lean_object* l_liftT___rarg(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = lean_apply_1(x_1, x_2);
return x_3;
}
}
lean_object* l_liftT(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = lean_alloc_closure((void*)(l_liftT___rarg), 2, 0);
return x_3;
}
}
lean_object* l_oldCoeB___rarg(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = lean_apply_1(x_1, x_2);
return x_3;
}
}
lean_object* l_oldCoeB(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = lean_alloc_closure((void*)(l_oldCoeB___rarg), 2, 0);
return x_3;
}
}
lean_object* l_oldCoeT___rarg(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = lean_apply_1(x_1, x_2);
return x_3;
}
}
lean_object* l_oldCoeT(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = lean_alloc_closure((void*)(l_oldCoeT___rarg), 2, 0);
return x_3;
}
}
lean_object* l_oldCoeFnB___rarg(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = lean_apply_1(x_1, x_2);
return x_3;
}
}
lean_object* l_oldCoeFnB(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l_oldCoeFnB___rarg), 2, 0);
return x_2;
}
}
lean_object* l_oldCoe___rarg(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = lean_apply_1(x_1, x_2);
return x_3;
}
}
lean_object* l_oldCoe(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = lean_alloc_closure((void*)(l_oldCoe___rarg), 2, 0);
return x_3;
}
}
lean_object* l_oldCoeFn___rarg(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = lean_apply_1(x_1, x_2);
return x_3;
}
}
lean_object* l_oldCoeFn(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l_oldCoeFn___rarg), 2, 0);
return x_2;
}
}
lean_object* l_oldCoeSort___rarg(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = lean_apply_1(x_1, x_2);
return x_3;
}
}
lean_object* l_oldCoeSort(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l_oldCoeSort___rarg), 2, 0);
return x_2;
}
}
lean_object* l_Legacy_liftTrans___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4; lean_object* x_5;
x_4 = lean_apply_1(x_2, x_3);
x_5 = lean_apply_1(x_1, x_4);
return x_5;
}
}
lean_object* l_Legacy_liftTrans(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
x_4 = lean_alloc_closure((void*)(l_Legacy_liftTrans___rarg), 3, 0);
return x_4;
}
}
lean_object* l_Legacy_liftRefl(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = l_Nat_HasOfNat___closed__1;
return x_2;
}
}
lean_object* l_Legacy_coeoeTrans___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4; lean_object* x_5;
x_4 = lean_apply_1(x_2, x_3);
x_5 = lean_apply_1(x_1, x_4);
return x_5;
}
}
lean_object* l_Legacy_coeoeTrans(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
x_4 = lean_alloc_closure((void*)(l_Legacy_coeoeTrans___rarg), 3, 0);
return x_4;
}
}
lean_object* l_Legacy_coeBase___rarg(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l_oldCoeB___rarg), 2, 1);
lean_closure_set(x_2, 0, x_1);
return x_2;
}
}
lean_object* l_Legacy_coeBase(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = lean_alloc_closure((void*)(l_Legacy_coeBase___rarg), 1, 0);
return x_3;
}
}
lean_object* l_Legacy_oldCoeOption___rarg(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
}
}
lean_object* l_Legacy_oldCoeOption(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l_Legacy_oldCoeOption___rarg), 1, 0);
return x_2;
}
}
lean_object* l_Legacy_coeTransAux___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4; lean_object* x_5;
x_4 = lean_apply_1(x_2, x_3);
x_5 = lean_apply_1(x_1, x_4);
return x_5;
}
}
lean_object* l_Legacy_coeTransAux(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
x_4 = lean_alloc_closure((void*)(l_Legacy_coeTransAux___rarg), 3, 0);
return x_4;
}
}
lean_object* l_Legacy_coeBaseAux___rarg(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l_oldCoeB___rarg), 2, 1);
lean_closure_set(x_2, 0, x_1);
return x_2;
}
}
lean_object* l_Legacy_coeBaseAux(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = lean_alloc_closure((void*)(l_Legacy_coeBaseAux___rarg), 1, 0);
return x_3;
}
}
lean_object* l_Legacy_coeFnTrans___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4; lean_object* x_5;
x_4 = lean_apply_1(x_2, x_3);
x_5 = lean_apply_1(x_1, x_4);
return x_5;
}
}
lean_object* l_Legacy_coeFnTrans(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = lean_alloc_closure((void*)(l_Legacy_coeFnTrans___rarg), 3, 0);
return x_3;
}
}
lean_object* l_Legacy_coeSortTrans___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4; lean_object* x_5;
x_4 = lean_apply_1(x_2, x_3);
x_5 = lean_apply_1(x_1, x_4);
return x_5;
}
}
lean_object* l_Legacy_coeSortTrans(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = lean_alloc_closure((void*)(l_Legacy_coeSortTrans___rarg), 3, 0);
return x_3;
}
}
lean_object* l_Legacy_coeToLift___rarg(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l_oldCoeT___rarg), 2, 1);
lean_closure_set(x_2, 0, x_1);
return x_2;
}
}
lean_object* l_Legacy_coeToLift(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = lean_alloc_closure((void*)(l_Legacy_coeToLift___rarg), 1, 0);
return x_3;
}
}
lean_object* _init_l_Legacy_coeBoolToProp() {
_start:
{
return lean_box(0);
}
}
lean_object* _init_l_Legacy_coeSortBool() {
_start:
{
return lean_box(0);
}
}
uint8_t l_Legacy_coeDecidableEq(uint8_t x_1) {
_start:
{
if (x_1 == 0)
{
uint8_t x_2;
x_2 = 0;
return x_2;
}
else
{
uint8_t x_3;
x_3 = 1;
return x_3;
}
}
}
lean_object* l_Legacy_coeDecidableEq___boxed(lean_object* x_1) {
_start:
{
uint8_t x_2; uint8_t x_3; lean_object* x_4;
x_2 = lean_unbox(x_1);
lean_dec(x_1);
x_3 = l_Legacy_coeDecidableEq(x_2);
x_4 = lean_box(x_3);
return x_4;
}
}
lean_object* l_Legacy_coeSubtype___rarg(lean_object* x_1) {
_start:
{
lean_inc(x_1);
return x_1;
}
}
lean_object* l_Legacy_coeSubtype(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = lean_alloc_closure((void*)(l_Legacy_coeSubtype___rarg___boxed), 1, 0);
return x_3;
}
}
lean_object* l_Legacy_coeSubtype___rarg___boxed(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = l_Legacy_coeSubtype___rarg(x_1);
lean_dec(x_1);
return x_2;
}
}
lean_object* l_Legacy_coeSubtype___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = l_Legacy_coeSubtype(x_1, x_2);
lean_dec(x_2);
return x_3;
}
}
lean_object* l_Legacy_liftFn___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
lean_object* x_5; lean_object* x_6; lean_object* x_7;
x_5 = lean_apply_1(x_2, x_4);
x_6 = lean_apply_1(x_3, x_5);
x_7 = lean_apply_1(x_1, x_6);
return x_7;
}
}
lean_object* l_Legacy_liftFn(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
lean_object* x_5;
x_5 = lean_alloc_closure((void*)(l_Legacy_liftFn___rarg), 4, 0);
return x_5;
}
}
lean_object* l_Legacy_liftFnRange___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4; lean_object* x_5;
x_4 = lean_apply_1(x_2, x_3);
x_5 = lean_apply_1(x_1, x_4);
return x_5;
}
}
lean_object* l_Legacy_liftFnRange(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
x_4 = lean_alloc_closure((void*)(l_Legacy_liftFnRange___rarg), 3, 0);
return x_4;
}
}
lean_object* l_Legacy_liftFnDom___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4; lean_object* x_5;
x_4 = lean_apply_1(x_1, x_3);
x_5 = lean_apply_1(x_2, x_4);
return x_5;
}
}
lean_object* l_Legacy_liftFnDom(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
x_4 = lean_alloc_closure((void*)(l_Legacy_liftFnDom___rarg), 3, 0);
return x_4;
}
}
lean_object* l_Legacy_liftPair___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
uint8_t x_4;
x_4 = !lean_is_exclusive(x_3);
if (x_4 == 0)
{
lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8;
x_5 = lean_ctor_get(x_3, 0);
x_6 = lean_ctor_get(x_3, 1);
x_7 = lean_apply_1(x_1, x_5);
x_8 = lean_apply_1(x_2, x_6);
lean_ctor_set(x_3, 1, x_8);
lean_ctor_set(x_3, 0, x_7);
return x_3;
}
else
{
lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13;
x_9 = lean_ctor_get(x_3, 0);
x_10 = lean_ctor_get(x_3, 1);
lean_inc(x_10);
lean_inc(x_9);
lean_dec(x_3);
x_11 = lean_apply_1(x_1, x_9);
x_12 = lean_apply_1(x_2, x_10);
x_13 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_13, 0, x_11);
lean_ctor_set(x_13, 1, x_12);
return x_13;
}
}
}
lean_object* l_Legacy_liftPair(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
lean_object* x_5;
x_5 = lean_alloc_closure((void*)(l_Legacy_liftPair___rarg), 3, 0);
return x_5;
}
}
lean_object* l_Legacy_liftPair_u2081___rarg(lean_object* x_1, lean_object* x_2) {
_start:
{
uint8_t x_3;
x_3 = !lean_is_exclusive(x_2);
if (x_3 == 0)
{
lean_object* x_4; lean_object* x_5;
x_4 = lean_ctor_get(x_2, 0);
x_5 = lean_apply_1(x_1, x_4);
lean_ctor_set(x_2, 0, x_5);
return x_2;
}
else
{
lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9;
x_6 = lean_ctor_get(x_2, 0);
x_7 = lean_ctor_get(x_2, 1);
lean_inc(x_7);
lean_inc(x_6);
lean_dec(x_2);
x_8 = lean_apply_1(x_1, x_6);
x_9 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_9, 0, x_8);
lean_ctor_set(x_9, 1, x_7);
return x_9;
}
}
}
lean_object* l_Legacy_liftPair_u2081(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
x_4 = lean_alloc_closure((void*)(l_Legacy_liftPair_u2081___rarg), 2, 0);
return x_4;
}
}
lean_object* l_Legacy_liftPair_u2082___rarg(lean_object* x_1, lean_object* x_2) {
_start:
{
uint8_t x_3;
x_3 = !lean_is_exclusive(x_2);
if (x_3 == 0)
{
lean_object* x_4; lean_object* x_5;
x_4 = lean_ctor_get(x_2, 1);
x_5 = lean_apply_1(x_1, x_4);
lean_ctor_set(x_2, 1, x_5);
return x_2;
}
else
{
lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9;
x_6 = lean_ctor_get(x_2, 0);
x_7 = lean_ctor_get(x_2, 1);
lean_inc(x_7);
lean_inc(x_6);
lean_dec(x_2);
x_8 = lean_apply_1(x_1, x_7);
x_9 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_9, 0, x_6);
lean_ctor_set(x_9, 1, x_8);
return x_9;
}
}
}
lean_object* l_Legacy_liftPair_u2082(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
x_4 = lean_alloc_closure((void*)(l_Legacy_liftPair_u2082___rarg), 2, 0);
return x_4;
}
}
lean_object* l_List_map___main___at_Legacy_liftList___spec__1___rarg(lean_object* x_1, lean_object* x_2) {
_start:
{
if (lean_obj_tag(x_2) == 0)
{
lean_object* x_3;
lean_dec(x_1);
x_3 = lean_box(0);
return x_3;
}
else
{
uint8_t x_4;
x_4 = !lean_is_exclusive(x_2);
if (x_4 == 0)
{
lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8;
x_5 = lean_ctor_get(x_2, 0);
x_6 = lean_ctor_get(x_2, 1);
lean_inc(x_1);
x_7 = lean_apply_1(x_1, x_5);
x_8 = l_List_map___main___at_Legacy_liftList___spec__1___rarg(x_1, x_6);
lean_ctor_set(x_2, 1, x_8);
lean_ctor_set(x_2, 0, x_7);
return x_2;
}
else
{
lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13;
x_9 = lean_ctor_get(x_2, 0);
x_10 = lean_ctor_get(x_2, 1);
lean_inc(x_10);
lean_inc(x_9);
lean_dec(x_2);
lean_inc(x_1);
x_11 = lean_apply_1(x_1, x_9);
x_12 = l_List_map___main___at_Legacy_liftList___spec__1___rarg(x_1, x_10);
x_13 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_13, 0, x_11);
lean_ctor_set(x_13, 1, x_12);
return x_13;
}
}
}
}
lean_object* l_List_map___main___at_Legacy_liftList___spec__1(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = lean_alloc_closure((void*)(l_List_map___main___at_Legacy_liftList___spec__1___rarg), 2, 0);
return x_3;
}
}
lean_object* l_Legacy_liftList___rarg(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = l_List_map___main___at_Legacy_liftList___spec__1___rarg(x_1, x_2);
return x_3;
}
}
lean_object* l_Legacy_liftList(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = lean_alloc_closure((void*)(l_Legacy_liftList___rarg), 2, 0);
return x_3;
}
}
lean_object* l_oldCoeToLift___rarg(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l_oldCoeT___rarg), 2, 1);
lean_closure_set(x_2, 0, x_1);
return x_2;
}
}
lean_object* l_oldCoeToLift(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = lean_alloc_closure((void*)(l_oldCoeToLift___rarg), 1, 0);
return x_3;
}
}
lean_object* initialize_Init_Data_List_Basic(lean_object*);
static bool _G_initialized = false;
lean_object* initialize_Init_HasCoe(lean_object* w) {
lean_object * res;
if (_G_initialized) return lean_mk_io_result(lean_box(0));
_G_initialized = true;
res = initialize_Init_Data_List_Basic(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l_Legacy_coeBoolToProp = _init_l_Legacy_coeBoolToProp();
l_Legacy_coeSortBool = _init_l_Legacy_coeSortBool();
return lean_mk_io_result(lean_box(0));
}
#ifdef __cplusplus
}
#endif

31
stage0/stdlib/Init/Lean/Compiler/IR/ElimDeadBranches.c
View file

@ -119,7 +119,6 @@ lean_object* l_Lean_IR_UnreachableBranches_Value_format___main___closed__2;
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
lean_object* l_Lean_IR_UnreachableBranches_Value_format(lean_object*);
lean_object* l_Array_umapMAux___main___at_Lean_IR_UnreachableBranches_elimDeadAux___main___spec__1___boxed(lean_object*, lean_object*, lean_object*);
extern lean_object* l_List_Monad;
lean_object* l_Lean_IR_UnreachableBranches_Value_format___main___closed__1;
lean_object* l_HashMapImp_insert___at_Lean_IR_UnreachableBranches_updateVarAssignment___spec__2(lean_object*, lean_object*, lean_object*);
lean_object* l_Array_iterateMAux___main___at_Lean_IR_UnreachableBranches_mkFunctionSummariesExtension___spec__5(size_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -291,7 +290,6 @@ lean_object* l_Lean_IR_UnreachableBranches_elimDeadAux___boxed(lean_object*, lea
lean_object* l_Lean_IR_UnreachableBranches_Value_format___main___closed__5;
extern lean_object* l_Lean_Format_paren___closed__3;
lean_object* l_Lean_IR_UnreachableBranches_elimDeadAux(lean_object*, lean_object*);
lean_object* l_Lean_IR_UnreachableBranches_Value_addChoice___main___closed__4;
lean_object* l_Lean_IR_UnreachableBranches_Value_Lean_HasFormat;
lean_object* l_Array_findIdxAux___main___at_Lean_IR_UnreachableBranches_interpExpr___spec__2___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_PersistentArray_get_x21___at_Lean_IR_UnreachableBranches_interpExpr___spec__3(lean_object*, lean_object*);
@ -327,7 +325,6 @@ lean_object* l_Lean_IR_UnreachableBranches_functionSummariesExt___closed__9;
lean_object* l_HashMapImp_find_x3f___at_Lean_IR_UnreachableBranches_getFunctionSummary_x3f___spec__5(lean_object*, lean_object*);
lean_object* l_List_map___main___at_Lean_IR_UnreachableBranches_Value_truncate___main___spec__2(lean_object*, lean_object*, lean_object*);
uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
lean_object* l_monadInhabited___rarg(lean_object*, lean_object*);
lean_object* l_Lean_registerEnvExtensionUnsafe___at_Lean_IR_UnreachableBranches_mkFunctionSummariesExtension___spec__22(lean_object*, lean_object*);
lean_object* _init_l_Lean_IR_UnreachableBranches_Value_Inhabited() {
_start:
@ -715,22 +712,12 @@ return x_1;
lean_object* _init_l_Lean_IR_UnreachableBranches_Value_addChoice___main___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_List_Monad;
x_2 = l_Lean_IR_UnreachableBranches_Value_Inhabited;
x_3 = l_monadInhabited___rarg(x_1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_IR_UnreachableBranches_Value_addChoice___main___closed__2() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("Init.Lean.Compiler.IR.ElimDeadBranches");
return x_1;
}
}
lean_object* _init_l_Lean_IR_UnreachableBranches_Value_addChoice___main___closed__3() {
lean_object* _init_l_Lean_IR_UnreachableBranches_Value_addChoice___main___closed__2() {
_start:
{
lean_object* x_1;
@ -738,14 +725,14 @@ x_1 = lean_mk_string("invalid addChoice");
return x_1;
}
}
lean_object* _init_l_Lean_IR_UnreachableBranches_Value_addChoice___main___closed__4() {
lean_object* _init_l_Lean_IR_UnreachableBranches_Value_addChoice___main___closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_1 = l_Lean_IR_UnreachableBranches_Value_addChoice___main___closed__2;
x_1 = l_Lean_IR_UnreachableBranches_Value_addChoice___main___closed__1;
x_2 = lean_unsigned_to_nat(46u);
x_3 = lean_unsigned_to_nat(10u);
x_4 = l_Lean_IR_UnreachableBranches_Value_addChoice___main___closed__3;
x_4 = l_Lean_IR_UnreachableBranches_Value_addChoice___main___closed__2;
x_5 = l___private_Init_Util_1__mkPanicMessage(x_1, x_2, x_3, x_4);
return x_5;
}
@ -841,8 +828,8 @@ lean_dec(x_5);
lean_dec(x_3);
lean_dec(x_2);
lean_dec(x_1);
x_22 = l_Lean_IR_UnreachableBranches_Value_addChoice___main___closed__1;
x_23 = l_Lean_IR_UnreachableBranches_Value_addChoice___main___closed__4;
x_22 = lean_box(0);
x_23 = l_Lean_IR_UnreachableBranches_Value_addChoice___main___closed__3;
x_24 = lean_panic_fn(x_22, x_23);
return x_24;
}
@ -854,8 +841,8 @@ lean_dec(x_5);
lean_dec(x_3);
lean_dec(x_2);
lean_dec(x_1);
x_25 = l_Lean_IR_UnreachableBranches_Value_addChoice___main___closed__1;
x_26 = l_Lean_IR_UnreachableBranches_Value_addChoice___main___closed__4;
x_25 = lean_box(0);
x_26 = l_Lean_IR_UnreachableBranches_Value_addChoice___main___closed__3;
x_27 = lean_panic_fn(x_25, x_26);
return x_27;
}
@ -7521,8 +7508,6 @@ l_Lean_IR_UnreachableBranches_Value_addChoice___main___closed__2 = _init_l_Lean_
lean_mark_persistent(l_Lean_IR_UnreachableBranches_Value_addChoice___main___closed__2);
l_Lean_IR_UnreachableBranches_Value_addChoice___main___closed__3 = _init_l_Lean_IR_UnreachableBranches_Value_addChoice___main___closed__3();
lean_mark_persistent(l_Lean_IR_UnreachableBranches_Value_addChoice___main___closed__3);
l_Lean_IR_UnreachableBranches_Value_addChoice___main___closed__4 = _init_l_Lean_IR_UnreachableBranches_Value_addChoice___main___closed__4();
lean_mark_persistent(l_Lean_IR_UnreachableBranches_Value_addChoice___main___closed__4);
l_List_foldl___main___at_Lean_IR_UnreachableBranches_Value_merge___main___spec__2___closed__1 = _init_l_List_foldl___main___at_Lean_IR_UnreachableBranches_Value_merge___main___spec__2___closed__1();
lean_mark_persistent(l_List_foldl___main___at_Lean_IR_UnreachableBranches_Value_merge___main___spec__2___closed__1);
l_Lean_IR_UnreachableBranches_Value_format___main___closed__1 = _init_l_Lean_IR_UnreachableBranches_Value_format___main___closed__1();

6
stage0/stdlib/Init/Lean/Data/Name.c
View file

@ -1,6 +1,6 @@
// Lean compiler output
// Module: Init.Lean.Data.Name
// Imports: Init.Coe Init.LeanInit Init.Data.UInt Init.Data.ToString Init.Data.Hashable Init.Data.RBMap Init.Data.RBTree
// Imports: Init.LeanInit Init.Data.UInt Init.Data.ToString Init.Data.Hashable Init.Data.RBMap Init.Data.RBTree
#include "runtime/lean.h"
#if defined(__clang__)
#pragma clang diagnostic ignored "-Wunused-parameter"
@ -8868,7 +8868,6 @@ lean_dec(x_2);
return x_3;
}
}
lean_object* initialize_Init_Coe(lean_object*);
lean_object* initialize_Init_LeanInit(lean_object*);
lean_object* initialize_Init_Data_UInt(lean_object*);
lean_object* initialize_Init_Data_ToString(lean_object*);
@ -8880,9 +8879,6 @@ lean_object* initialize_Init_Lean_Data_Name(lean_object* w) {
lean_object * res;
if (_G_initialized) return lean_mk_io_result(lean_box(0));
_G_initialized = true;
res = initialize_Init_Coe(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Init_LeanInit(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);

6652
stage0/stdlib/Init/Lean/Elab/BuiltinNotation.c
View file

File diff suppressed because it is too large Load diff

429
stage0/stdlib/Init/Lean/Elab/Command.c
View file

@ -76,7 +76,6 @@ lean_object* l_Lean_Elab_Command_elabUniverse(lean_object*, lean_object*, lean_o
lean_object* lean_array_fswap(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_identKind___closed__2;
lean_object* l_Lean_Elab_Command_withNamespace___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern uint8_t l___private_Init_Lean_Elab_Term_4__isCDot___closed__1;
lean_object* l___private_Init_Lean_Elab_Command_10__toCommandResult(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_runTermElabM___rarg___closed__1;
lean_object* l___regBuiltinCommandElab_Lean_Elab_Command_elabSetOption___closed__2;
@ -208,7 +207,6 @@ lean_object* l_List_foldl___main___at_Lean_Elab_Command_sortDeclLevelParams___sp
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
extern lean_object* l_Lean_Elab_Term_termElabAttribute___closed__4;
lean_object* l_Lean_Elab_Command_modifyScope___at_Lean_Elab_Command_withDeclId___spec__2(lean_object*, lean_object*, lean_object*);
extern lean_object* l_List_Monad;
lean_object* l_Lean_Elab_Command_CommandElabM_monadLog___closed__1;
lean_object* l_Lean_Elab_Command_CommandElabM_monadLog___closed__3;
lean_object* l_Lean_Elab_Command_CommandElabM_monadLog___lambda__3___boxed(lean_object*, lean_object*, lean_object*);
@ -301,7 +299,6 @@ extern lean_object* l_Lean_Options_empty;
extern lean_object* l_Lean_Parser_Command_variable___elambda__1___closed__2;
lean_object* l_Array_iterateMAux___main___at_Lean_Elab_Command_elabOpenSimple___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_ReaderT_read___at_Lean_Elab_Command_CommandElabM_monadLog___spec__1(lean_object*, lean_object*);
uint8_t l_coeDecidableEq(uint8_t);
lean_object* l_Lean_Elab_Command_addUnivLevel___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l___regBuiltinCommandElab_Lean_Elab_Command_elabExport___closed__1;
size_t lean_usize_modn(size_t, lean_object*);
@ -339,7 +336,6 @@ lean_object* l_mkHashMapImp___rarg(lean_object*);
lean_object* l___regBuiltinCommandElab_Lean_Elab_Command_elabOpen(lean_object*);
lean_object* l_Lean_Elab_Command_elabEnd(lean_object*, lean_object*, lean_object*);
lean_object* l_Array_iterateMAux___main___at_Array_append___spec__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_modifyScope___closed__1;
lean_object* l___regBuiltinCommandElab_Lean_Elab_Command_elabCheck(lean_object*);
lean_object* l_Array_filterAux___main___at_Lean_Elab_Command_sortDeclLevelParams___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_registerAttributeImplBuilder___closed__2;
@ -582,7 +578,6 @@ uint8_t lean_string_dec_eq(lean_object*, lean_object*);
uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
lean_object* l_HashMapImp_contains___at_Lean_Elab_Command_addBuiltinCommandElab___spec__2___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Elab_log___at_Lean_Elab_Command_logTrace___spec__1(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*);
lean_object* l_monadInhabited___rarg(lean_object*, lean_object*);
lean_object* l___regBuiltinCommandElab_Lean_Elab_Command_elabEnd___closed__2;
lean_object* lean_add_decl(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_logTrace(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -9000,66 +8995,47 @@ lean_inc(x_1);
x_5 = l_Lean_Syntax_isOfKind(x_1, x_4);
if (x_5 == 0)
{
uint8_t x_6;
x_6 = l___private_Init_Lean_Elab_Term_4__isCDot___closed__1;
if (x_6 == 0)
{
lean_object* x_7; lean_object* x_8;
lean_object* x_6; lean_object* x_7;
lean_dec(x_2);
lean_dec(x_1);
x_7 = lean_box(1);
x_8 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_8, 0, x_7);
lean_ctor_set(x_8, 1, x_3);
return x_8;
x_6 = lean_box(1);
x_7 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_7, 0, x_6);
lean_ctor_set(x_7, 1, x_3);
return x_7;
}
else
{
lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; uint8_t x_13; lean_object* x_14;
x_9 = lean_unsigned_to_nat(1u);
x_10 = l_Lean_Syntax_getArg(x_1, x_9);
x_11 = l_Lean_Syntax_getId(x_10);
lean_dec(x_10);
x_12 = l_Lean_Parser_Command_namespace___elambda__1___closed__1;
x_13 = 1;
x_14 = l___private_Init_Lean_Elab_Command_12__addScopes___main(x_1, x_12, x_13, x_11, x_2, x_3);
lean_object* x_8; lean_object* x_9; lean_object* x_10; uint8_t x_11;
x_8 = l_Lean_Syntax_getArgs(x_1);
x_9 = lean_array_get_size(x_8);
lean_dec(x_8);
x_10 = lean_unsigned_to_nat(2u);
x_11 = lean_nat_dec_eq(x_9, x_10);
lean_dec(x_9);
if (x_11 == 0)
{
lean_object* x_12; lean_object* x_13;
lean_dec(x_2);
lean_dec(x_1);
return x_14;
}
x_12 = lean_box(1);
x_13 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_13, 0, x_12);
lean_ctor_set(x_13, 1, x_3);
return x_13;
}
else
{
lean_object* x_15; lean_object* x_16; lean_object* x_17; uint8_t x_18; uint8_t x_19;
x_15 = l_Lean_Syntax_getArgs(x_1);
x_16 = lean_array_get_size(x_15);
lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; uint8_t x_18; lean_object* x_19;
x_14 = lean_unsigned_to_nat(1u);
x_15 = l_Lean_Syntax_getArg(x_1, x_14);
x_16 = l_Lean_Syntax_getId(x_15);
lean_dec(x_15);
x_17 = lean_unsigned_to_nat(2u);
x_18 = lean_nat_dec_eq(x_16, x_17);
lean_dec(x_16);
x_19 = l_coeDecidableEq(x_18);
if (x_19 == 0)
{
lean_object* x_20; lean_object* x_21;
lean_dec(x_2);
x_17 = l_Lean_Parser_Command_namespace___elambda__1___closed__1;
x_18 = 1;
x_19 = l___private_Init_Lean_Elab_Command_12__addScopes___main(x_1, x_17, x_18, x_16, x_2, x_3);
lean_dec(x_1);
x_20 = lean_box(1);
x_21 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_21, 0, x_20);
lean_ctor_set(x_21, 1, x_3);
return x_21;
}
else
{
lean_object* x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; uint8_t x_26; lean_object* x_27;
x_22 = lean_unsigned_to_nat(1u);
x_23 = l_Lean_Syntax_getArg(x_1, x_22);
x_24 = l_Lean_Syntax_getId(x_23);
lean_dec(x_23);
x_25 = l_Lean_Parser_Command_namespace___elambda__1___closed__1;
x_26 = 1;
x_27 = l___private_Init_Lean_Elab_Command_12__addScopes___main(x_1, x_25, x_26, x_24, x_2, x_3);
lean_dec(x_1);
return x_27;
return x_19;
}
}
}
@ -9104,33 +9080,10 @@ return x_5;
lean_object* l_Lean_Elab_Command_elabSection(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
uint8_t x_4; lean_object* x_61; uint8_t x_62;
x_61 = l_Lean_Parser_Command_section___elambda__1___closed__2;
lean_object* x_4; uint8_t x_5;
x_4 = l_Lean_Parser_Command_section___elambda__1___closed__2;
lean_inc(x_1);
x_62 = l_Lean_Syntax_isOfKind(x_1, x_61);
if (x_62 == 0)
{
uint8_t x_63;
x_63 = 0;
x_4 = x_63;
goto block_60;
}
else
{
lean_object* x_64; lean_object* x_65; lean_object* x_66; uint8_t x_67;
x_64 = l_Lean_Syntax_getArgs(x_1);
x_65 = lean_array_get_size(x_64);
lean_dec(x_64);
x_66 = lean_unsigned_to_nat(2u);
x_67 = lean_nat_dec_eq(x_65, x_66);
lean_dec(x_65);
x_4 = x_67;
goto block_60;
}
block_60:
{
uint8_t x_5;
x_5 = l_coeDecidableEq(x_4);
x_5 = l_Lean_Syntax_isOfKind(x_1, x_4);
if (x_5 == 0)
{
lean_object* x_6; lean_object* x_7;
@ -9144,192 +9097,144 @@ return x_7;
}
else
{
lean_object* x_8; lean_object* x_9; lean_object* x_10; uint8_t x_11; uint8_t x_12;
x_8 = lean_unsigned_to_nat(1u);
x_9 = l_Lean_Syntax_getArg(x_1, x_8);
x_10 = l_Lean_nullKind___closed__2;
lean_inc(x_9);
x_11 = l_Lean_Syntax_isOfKind(x_9, x_10);
if (x_11 == 0)
{
uint8_t x_56;
x_56 = 0;
x_12 = x_56;
goto block_55;
}
else
{
lean_object* x_57; lean_object* x_58; uint8_t x_59;
x_57 = l_Lean_Syntax_getArgs(x_9);
x_58 = lean_array_get_size(x_57);
lean_dec(x_57);
x_59 = lean_nat_dec_eq(x_58, x_8);
lean_dec(x_58);
x_12 = x_59;
goto block_55;
}
block_55:
{
uint8_t x_13;
x_13 = l_coeDecidableEq(x_12);
if (x_13 == 0)
{
lean_dec(x_1);
if (x_11 == 0)
{
uint8_t x_14;
lean_object* x_8; lean_object* x_9; lean_object* x_10; uint8_t x_11;
x_8 = l_Lean_Syntax_getArgs(x_1);
x_9 = lean_array_get_size(x_8);
lean_dec(x_8);
x_10 = lean_unsigned_to_nat(2u);
x_11 = lean_nat_dec_eq(x_9, x_10);
lean_dec(x_9);
x_14 = l___private_Init_Lean_Elab_Term_4__isCDot___closed__1;
if (x_14 == 0)
if (x_11 == 0)
{
lean_object* x_15; lean_object* x_16;
lean_object* x_12; lean_object* x_13;
lean_dec(x_2);
x_15 = lean_box(1);
x_16 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_16, 0, x_15);
lean_ctor_set(x_16, 1, x_3);
return x_16;
lean_dec(x_1);
x_12 = lean_box(1);
x_13 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_13, 0, x_12);
lean_ctor_set(x_13, 1, x_3);
return x_13;
}
else
{
lean_object* x_17;
lean_inc(x_2);
x_17 = l_Lean_Elab_Command_getCurrNamespace(x_2, x_3);
if (lean_obj_tag(x_17) == 0)
lean_object* x_14; lean_object* x_15; lean_object* x_16; uint8_t x_17;
x_14 = lean_unsigned_to_nat(1u);
x_15 = l_Lean_Syntax_getArg(x_1, x_14);
x_16 = l_Lean_nullKind___closed__2;
lean_inc(x_15);
x_17 = l_Lean_Syntax_isOfKind(x_15, x_16);
if (x_17 == 0)
{
lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22;
x_18 = lean_ctor_get(x_17, 0);
lean_inc(x_18);
x_19 = lean_ctor_get(x_17, 1);
lean_inc(x_19);
lean_dec(x_17);
x_20 = l_Lean_Parser_Command_section___elambda__1___closed__1;
x_21 = l_String_splitAux___main___closed__1;
x_22 = l___private_Init_Lean_Elab_Command_11__addScope(x_20, x_21, x_18, x_2, x_19);
return x_22;
}
else
{
uint8_t x_23;
lean_object* x_18; lean_object* x_19;
lean_dec(x_15);
lean_dec(x_2);
x_23 = !lean_is_exclusive(x_17);
if (x_23 == 0)
{
return x_17;
lean_dec(x_1);
x_18 = lean_box(1);
x_19 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_19, 0, x_18);
lean_ctor_set(x_19, 1, x_3);
return x_19;
}
else
{
lean_object* x_24; lean_object* x_25; lean_object* x_26;
x_24 = lean_ctor_get(x_17, 0);
x_25 = lean_ctor_get(x_17, 1);
lean_inc(x_25);
lean_inc(x_24);
lean_dec(x_17);
lean_object* x_20; lean_object* x_21; uint8_t x_22;
x_20 = l_Lean_Syntax_getArgs(x_15);
x_21 = lean_array_get_size(x_20);
lean_dec(x_20);
x_22 = lean_nat_dec_eq(x_21, x_14);
if (x_22 == 0)
{
lean_object* x_23; uint8_t x_24;
lean_dec(x_15);
lean_dec(x_1);
x_23 = lean_unsigned_to_nat(0u);
x_24 = lean_nat_dec_eq(x_21, x_23);
lean_dec(x_21);
if (x_24 == 0)
{
lean_object* x_25; lean_object* x_26;
lean_dec(x_2);
x_25 = lean_box(1);
x_26 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_26, 0, x_24);
lean_ctor_set(x_26, 1, x_25);
lean_ctor_set(x_26, 0, x_25);
lean_ctor_set(x_26, 1, x_3);
return x_26;
}
}
}
}
else
{
lean_object* x_27; lean_object* x_28; lean_object* x_29; uint8_t x_30; uint8_t x_31;
x_27 = l_Lean_Syntax_getArgs(x_9);
lean_dec(x_9);
x_28 = lean_array_get_size(x_27);
lean_dec(x_27);
x_29 = lean_unsigned_to_nat(0u);
x_30 = lean_nat_dec_eq(x_28, x_29);
lean_dec(x_28);
x_31 = l_coeDecidableEq(x_30);
if (x_31 == 0)
{
lean_object* x_32; lean_object* x_33;
lean_dec(x_2);
x_32 = lean_box(1);
x_33 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_33, 0, x_32);
lean_ctor_set(x_33, 1, x_3);
return x_33;
}
else
{
lean_object* x_34;
lean_object* x_27;
lean_inc(x_2);
x_34 = l_Lean_Elab_Command_getCurrNamespace(x_2, x_3);
if (lean_obj_tag(x_34) == 0)
x_27 = l_Lean_Elab_Command_getCurrNamespace(x_2, x_3);
if (lean_obj_tag(x_27) == 0)
{
lean_object* x_35; lean_object* x_36; lean_object* x_37; lean_object* x_38; lean_object* x_39;
x_35 = lean_ctor_get(x_34, 0);
lean_inc(x_35);
x_36 = lean_ctor_get(x_34, 1);
lean_inc(x_36);
lean_dec(x_34);
x_37 = l_Lean_Parser_Command_section___elambda__1___closed__1;
x_38 = l_String_splitAux___main___closed__1;
x_39 = l___private_Init_Lean_Elab_Command_11__addScope(x_37, x_38, x_35, x_2, x_36);
return x_39;
lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32;
x_28 = lean_ctor_get(x_27, 0);
lean_inc(x_28);
x_29 = lean_ctor_get(x_27, 1);
lean_inc(x_29);
lean_dec(x_27);
x_30 = l_Lean_Parser_Command_section___elambda__1___closed__1;
x_31 = l_String_splitAux___main___closed__1;
x_32 = l___private_Init_Lean_Elab_Command_11__addScope(x_30, x_31, x_28, x_2, x_29);
return x_32;
}
else
{
uint8_t x_40;
uint8_t x_33;
lean_dec(x_2);
x_40 = !lean_is_exclusive(x_34);
x_33 = !lean_is_exclusive(x_27);
if (x_33 == 0)
{
return x_27;
}
else
{
lean_object* x_34; lean_object* x_35; lean_object* x_36;
x_34 = lean_ctor_get(x_27, 0);
x_35 = lean_ctor_get(x_27, 1);
lean_inc(x_35);
lean_inc(x_34);
lean_dec(x_27);
x_36 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_36, 0, x_34);
lean_ctor_set(x_36, 1, x_35);
return x_36;
}
}
}
}
else
{
lean_object* x_37; lean_object* x_38; lean_object* x_39; uint8_t x_40;
lean_dec(x_21);
x_37 = lean_unsigned_to_nat(0u);
x_38 = l_Lean_Syntax_getArg(x_15, x_37);
lean_dec(x_15);
x_39 = l_Lean_identKind___closed__2;
lean_inc(x_38);
x_40 = l_Lean_Syntax_isOfKind(x_38, x_39);
if (x_40 == 0)
{
return x_34;
}
else
{
lean_object* x_41; lean_object* x_42; lean_object* x_43;
x_41 = lean_ctor_get(x_34, 0);
x_42 = lean_ctor_get(x_34, 1);
lean_inc(x_42);
lean_inc(x_41);
lean_dec(x_34);
x_43 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_43, 0, x_41);
lean_ctor_set(x_43, 1, x_42);
return x_43;
}
}
}
}
}
else
{
lean_object* x_44; lean_object* x_45; lean_object* x_46; uint8_t x_47; uint8_t x_48;
x_44 = lean_unsigned_to_nat(0u);
x_45 = l_Lean_Syntax_getArg(x_9, x_44);
lean_dec(x_9);
x_46 = l_Lean_identKind___closed__2;
lean_inc(x_45);
x_47 = l_Lean_Syntax_isOfKind(x_45, x_46);
x_48 = l_coeDecidableEq(x_47);
if (x_48 == 0)
{
lean_object* x_49; lean_object* x_50;
lean_dec(x_45);
lean_object* x_41; lean_object* x_42;
lean_dec(x_38);
lean_dec(x_2);
lean_dec(x_1);
x_49 = lean_box(1);
x_50 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_50, 0, x_49);
lean_ctor_set(x_50, 1, x_3);
return x_50;
x_41 = lean_box(1);
x_42 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_42, 0, x_41);
lean_ctor_set(x_42, 1, x_3);
return x_42;
}
else
{
lean_object* x_51; lean_object* x_52; uint8_t x_53; lean_object* x_54;
x_51 = l_Lean_Syntax_getId(x_45);
lean_dec(x_45);
x_52 = l_Lean_Parser_Command_section___elambda__1___closed__1;
x_53 = 0;
x_54 = l___private_Init_Lean_Elab_Command_12__addScopes___main(x_1, x_52, x_53, x_51, x_2, x_3);
lean_object* x_43; lean_object* x_44; uint8_t x_45; lean_object* x_46;
x_43 = l_Lean_Syntax_getId(x_38);
lean_dec(x_38);
x_44 = l_Lean_Parser_Command_section___elambda__1___closed__1;
x_45 = 0;
x_46 = l___private_Init_Lean_Elab_Command_12__addScopes___main(x_1, x_44, x_45, x_43, x_2, x_3);
lean_dec(x_1);
return x_54;
return x_46;
}
}
}
@ -10438,16 +10343,6 @@ lean_dec(x_1);
return x_6;
}
}
lean_object* _init_l_Lean_Elab_Command_modifyScope___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_List_Monad;
x_2 = l_Lean_Elab_Command_Scope_inhabited;
x_3 = l_monadInhabited___rarg(x_1, x_2);
return x_3;
}
}
lean_object* l_Lean_Elab_Command_modifyScope(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
@ -10474,7 +10369,7 @@ if (x_8 == 0)
lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12;
x_9 = lean_ctor_get(x_5, 2);
lean_dec(x_9);
x_10 = l_Lean_Elab_Command_modifyScope___closed__1;
x_10 = lean_box(0);
x_11 = l_unreachable_x21___rarg(x_10);
lean_ctor_set(x_5, 2, x_11);
x_12 = l___private_Init_Lean_Elab_Command_3__setState(x_5, x_2, x_7);
@ -10539,7 +10434,7 @@ lean_inc(x_25);
lean_inc(x_24);
lean_inc(x_23);
lean_dec(x_5);
x_27 = l_Lean_Elab_Command_modifyScope___closed__1;
x_27 = lean_box(0);
x_28 = l_unreachable_x21___rarg(x_27);
x_29 = lean_alloc_ctor(0, 5, 0);
lean_ctor_set(x_29, 0, x_23);
@ -11017,7 +10912,7 @@ if (x_8 == 0)
lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12;
x_9 = lean_ctor_get(x_5, 2);
lean_dec(x_9);
x_10 = l_Lean_Elab_Command_modifyScope___closed__1;
x_10 = lean_box(0);
x_11 = l_unreachable_x21___rarg(x_10);
lean_ctor_set(x_5, 2, x_11);
x_12 = l___private_Init_Lean_Elab_Command_3__setState(x_5, x_2, x_7);
@ -11082,7 +10977,7 @@ lean_inc(x_25);
lean_inc(x_24);
lean_inc(x_23);
lean_dec(x_5);
x_27 = l_Lean_Elab_Command_modifyScope___closed__1;
x_27 = lean_box(0);
x_28 = l_unreachable_x21___rarg(x_27);
x_29 = lean_alloc_ctor(0, 5, 0);
lean_ctor_set(x_29, 0, x_23);
@ -12828,7 +12723,7 @@ if (x_8 == 0)
lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12;
x_9 = lean_ctor_get(x_5, 2);
lean_dec(x_9);
x_10 = l_Lean_Elab_Command_modifyScope___closed__1;
x_10 = lean_box(0);
x_11 = l_unreachable_x21___rarg(x_10);
lean_ctor_set(x_5, 2, x_11);
x_12 = l___private_Init_Lean_Elab_Command_3__setState(x_5, x_2, x_7);
@ -12893,7 +12788,7 @@ lean_inc(x_25);
lean_inc(x_24);
lean_inc(x_23);
lean_dec(x_5);
x_27 = l_Lean_Elab_Command_modifyScope___closed__1;
x_27 = lean_box(0);
x_28 = l_unreachable_x21___rarg(x_27);
x_29 = lean_alloc_ctor(0, 5, 0);
lean_ctor_set(x_29, 0, x_23);
@ -14365,7 +14260,7 @@ if (x_8 == 0)
lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12;
x_9 = lean_ctor_get(x_5, 2);
lean_dec(x_9);
x_10 = l_Lean_Elab_Command_modifyScope___closed__1;
x_10 = lean_box(0);
x_11 = l_unreachable_x21___rarg(x_10);
lean_ctor_set(x_5, 2, x_11);
x_12 = l___private_Init_Lean_Elab_Command_3__setState(x_5, x_2, x_7);
@ -14430,7 +14325,7 @@ lean_inc(x_25);
lean_inc(x_24);
lean_inc(x_23);
lean_dec(x_5);
x_27 = l_Lean_Elab_Command_modifyScope___closed__1;
x_27 = lean_box(0);
x_28 = l_unreachable_x21___rarg(x_27);
x_29 = lean_alloc_ctor(0, 5, 0);
lean_ctor_set(x_29, 0, x_23);
@ -15421,7 +15316,7 @@ if (x_8 == 0)
lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12;
x_9 = lean_ctor_get(x_5, 2);
lean_dec(x_9);
x_10 = l_Lean_Elab_Command_modifyScope___closed__1;
x_10 = lean_box(0);
x_11 = l_unreachable_x21___rarg(x_10);
lean_ctor_set(x_5, 2, x_11);
x_12 = l___private_Init_Lean_Elab_Command_3__setState(x_5, x_2, x_7);
@ -15486,7 +15381,7 @@ lean_inc(x_25);
lean_inc(x_24);
lean_inc(x_23);
lean_dec(x_5);
x_27 = l_Lean_Elab_Command_modifyScope___closed__1;
x_27 = lean_box(0);
x_28 = l_unreachable_x21___rarg(x_27);
x_29 = lean_alloc_ctor(0, 5, 0);
lean_ctor_set(x_29, 0, x_23);
@ -17878,7 +17773,7 @@ if (x_9 == 0)
lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13;
x_10 = lean_ctor_get(x_6, 2);
lean_dec(x_10);
x_11 = l_Lean_Elab_Command_modifyScope___closed__1;
x_11 = lean_box(0);
x_12 = l_unreachable_x21___rarg(x_11);
lean_ctor_set(x_6, 2, x_12);
x_13 = l___private_Init_Lean_Elab_Command_3__setState(x_6, x_3, x_8);
@ -17943,7 +17838,7 @@ lean_inc(x_26);
lean_inc(x_25);
lean_inc(x_24);
lean_dec(x_6);
x_28 = l_Lean_Elab_Command_modifyScope___closed__1;
x_28 = lean_box(0);
x_29 = l_unreachable_x21___rarg(x_28);
x_30 = lean_alloc_ctor(0, 5, 0);
lean_ctor_set(x_30, 0, x_24);
@ -19213,7 +19108,7 @@ if (x_8 == 0)
lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12;
x_9 = lean_ctor_get(x_5, 2);
lean_dec(x_9);
x_10 = l_Lean_Elab_Command_modifyScope___closed__1;
x_10 = lean_box(0);
x_11 = l_unreachable_x21___rarg(x_10);
lean_ctor_set(x_5, 2, x_11);
x_12 = l___private_Init_Lean_Elab_Command_3__setState(x_5, x_2, x_7);
@ -19278,7 +19173,7 @@ lean_inc(x_25);
lean_inc(x_24);
lean_inc(x_23);
lean_dec(x_5);
x_27 = l_Lean_Elab_Command_modifyScope___closed__1;
x_27 = lean_box(0);
x_28 = l_unreachable_x21___rarg(x_27);
x_29 = lean_alloc_ctor(0, 5, 0);
lean_ctor_set(x_29, 0, x_23);
@ -19760,7 +19655,7 @@ if (x_8 == 0)
lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12;
x_9 = lean_ctor_get(x_5, 2);
lean_dec(x_9);
x_10 = l_Lean_Elab_Command_modifyScope___closed__1;
x_10 = lean_box(0);
x_11 = l_unreachable_x21___rarg(x_10);
lean_ctor_set(x_5, 2, x_11);
x_12 = l___private_Init_Lean_Elab_Command_3__setState(x_5, x_2, x_7);
@ -19825,7 +19720,7 @@ lean_inc(x_25);
lean_inc(x_24);
lean_inc(x_23);
lean_dec(x_5);
x_27 = l_Lean_Elab_Command_modifyScope___closed__1;
x_27 = lean_box(0);
x_28 = l_unreachable_x21___rarg(x_27);
x_29 = lean_alloc_ctor(0, 5, 0);
lean_ctor_set(x_29, 0, x_23);
@ -20307,7 +20202,7 @@ if (x_8 == 0)
lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12;
x_9 = lean_ctor_get(x_5, 2);
lean_dec(x_9);
x_10 = l_Lean_Elab_Command_modifyScope___closed__1;
x_10 = lean_box(0);
x_11 = l_unreachable_x21___rarg(x_10);
lean_ctor_set(x_5, 2, x_11);
x_12 = l___private_Init_Lean_Elab_Command_3__setState(x_5, x_2, x_7);
@ -20372,7 +20267,7 @@ lean_inc(x_25);
lean_inc(x_24);
lean_inc(x_23);
lean_dec(x_5);
x_27 = l_Lean_Elab_Command_modifyScope___closed__1;
x_27 = lean_box(0);
x_28 = l_unreachable_x21___rarg(x_27);
x_29 = lean_alloc_ctor(0, 5, 0);
lean_ctor_set(x_29, 0, x_23);
@ -20854,7 +20749,7 @@ if (x_8 == 0)
lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12;
x_9 = lean_ctor_get(x_5, 2);
lean_dec(x_9);
x_10 = l_Lean_Elab_Command_modifyScope___closed__1;
x_10 = lean_box(0);
x_11 = l_unreachable_x21___rarg(x_10);
lean_ctor_set(x_5, 2, x_11);
x_12 = l___private_Init_Lean_Elab_Command_3__setState(x_5, x_2, x_7);
@ -20919,7 +20814,7 @@ lean_inc(x_25);
lean_inc(x_24);
lean_inc(x_23);
lean_dec(x_5);
x_27 = l_Lean_Elab_Command_modifyScope___closed__1;
x_27 = lean_box(0);
x_28 = l_unreachable_x21___rarg(x_27);
x_29 = lean_alloc_ctor(0, 5, 0);
lean_ctor_set(x_29, 0, x_23);
@ -23199,8 +23094,6 @@ lean_mark_persistent(l___regBuiltinCommandElab_Lean_Elab_Command_elabEnd___close
res = l___regBuiltinCommandElab_Lean_Elab_Command_elabEnd(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l_Lean_Elab_Command_modifyScope___closed__1 = _init_l_Lean_Elab_Command_modifyScope___closed__1();
lean_mark_persistent(l_Lean_Elab_Command_modifyScope___closed__1);
l_Lean_Elab_Command_throwAlreadyDeclaredUniverseLevel___rarg___closed__1 = _init_l_Lean_Elab_Command_throwAlreadyDeclaredUniverseLevel___rarg___closed__1();
lean_mark_persistent(l_Lean_Elab_Command_throwAlreadyDeclaredUniverseLevel___rarg___closed__1);
l_Lean_Elab_Command_throwAlreadyDeclaredUniverseLevel___rarg___closed__2 = _init_l_Lean_Elab_Command_throwAlreadyDeclaredUniverseLevel___rarg___closed__2();

17
stage0/stdlib/Init/Lean/Elab/Declaration.c
View file

@ -89,7 +89,6 @@ lean_object* l___private_Init_Lean_Elab_Command_6__mkTermContext(lean_object*, l
lean_object* l_Lean_Elab_Command_elabConstant___closed__7;
lean_object* l_Lean_Elab_Command_modifyScope___at_Lean_Elab_Command_elabAxiom___spec__3(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_elabTheorem(lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Elab_Command_modifyScope___closed__1;
lean_object* l_Lean_Elab_Command_elabDef(lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Elab_Command_withDeclId___closed__3;
lean_object* l_Lean_Elab_Command_elabAxiom___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -839,7 +838,7 @@ if (x_8 == 0)
lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12;
x_9 = lean_ctor_get(x_5, 2);
lean_dec(x_9);
x_10 = l_Lean_Elab_Command_modifyScope___closed__1;
x_10 = lean_box(0);
x_11 = l_unreachable_x21___rarg(x_10);
lean_ctor_set(x_5, 2, x_11);
x_12 = l___private_Init_Lean_Elab_Command_3__setState(x_5, x_2, x_7);
@ -904,7 +903,7 @@ lean_inc(x_25);
lean_inc(x_24);
lean_inc(x_23);
lean_dec(x_5);
x_27 = l_Lean_Elab_Command_modifyScope___closed__1;
x_27 = lean_box(0);
x_28 = l_unreachable_x21___rarg(x_27);
x_29 = lean_alloc_ctor(0, 5, 0);
lean_ctor_set(x_29, 0, x_23);
@ -1386,7 +1385,7 @@ if (x_8 == 0)
lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12;
x_9 = lean_ctor_get(x_5, 2);
lean_dec(x_9);
x_10 = l_Lean_Elab_Command_modifyScope___closed__1;
x_10 = lean_box(0);
x_11 = l_unreachable_x21___rarg(x_10);
lean_ctor_set(x_5, 2, x_11);
x_12 = l___private_Init_Lean_Elab_Command_3__setState(x_5, x_2, x_7);
@ -1451,7 +1450,7 @@ lean_inc(x_25);
lean_inc(x_24);
lean_inc(x_23);
lean_dec(x_5);
x_27 = l_Lean_Elab_Command_modifyScope___closed__1;
x_27 = lean_box(0);
x_28 = l_unreachable_x21___rarg(x_27);
x_29 = lean_alloc_ctor(0, 5, 0);
lean_ctor_set(x_29, 0, x_23);
@ -1933,7 +1932,7 @@ if (x_8 == 0)
lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12;
x_9 = lean_ctor_get(x_5, 2);
lean_dec(x_9);
x_10 = l_Lean_Elab_Command_modifyScope___closed__1;
x_10 = lean_box(0);
x_11 = l_unreachable_x21___rarg(x_10);
lean_ctor_set(x_5, 2, x_11);
x_12 = l___private_Init_Lean_Elab_Command_3__setState(x_5, x_2, x_7);
@ -1998,7 +1997,7 @@ lean_inc(x_25);
lean_inc(x_24);
lean_inc(x_23);
lean_dec(x_5);
x_27 = l_Lean_Elab_Command_modifyScope___closed__1;
x_27 = lean_box(0);
x_28 = l_unreachable_x21___rarg(x_27);
x_29 = lean_alloc_ctor(0, 5, 0);
lean_ctor_set(x_29, 0, x_23);
@ -2480,7 +2479,7 @@ if (x_8 == 0)
lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12;
x_9 = lean_ctor_get(x_5, 2);
lean_dec(x_9);
x_10 = l_Lean_Elab_Command_modifyScope___closed__1;
x_10 = lean_box(0);
x_11 = l_unreachable_x21___rarg(x_10);
lean_ctor_set(x_5, 2, x_11);
x_12 = l___private_Init_Lean_Elab_Command_3__setState(x_5, x_2, x_7);
@ -2545,7 +2544,7 @@ lean_inc(x_25);
lean_inc(x_24);
lean_inc(x_23);
lean_dec(x_5);
x_27 = l_Lean_Elab_Command_modifyScope___closed__1;
x_27 = lean_box(0);
x_28 = l_unreachable_x21___rarg(x_27);
x_29 = lean_alloc_ctor(0, 5, 0);
lean_ctor_set(x_29, 0, x_23);

17
stage0/stdlib/Init/Lean/Elab/Definition.c
View file

@ -90,7 +90,6 @@ lean_object* l_Lean_CollectFVars_main___main(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Command_withUsedWhen_x27(lean_object*);
lean_object* l_Lean_Elab_Command_DefKind_isDefOrOpaque___boxed(lean_object*);
lean_object* l_Lean_Elab_Term_getLocalInsts(lean_object*, lean_object*);
extern lean_object* l_Lean_Elab_Command_modifyScope___closed__1;
lean_object* l_Lean_Elab_Command_elabDefLike___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_Elab_Command_DefKind_isTheorem(uint8_t);
extern lean_object* l_Lean_Elab_Command_withDeclId___closed__3;
@ -2051,7 +2050,7 @@ if (x_8 == 0)
lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12;
x_9 = lean_ctor_get(x_5, 2);
lean_dec(x_9);
x_10 = l_Lean_Elab_Command_modifyScope___closed__1;
x_10 = lean_box(0);
x_11 = l_unreachable_x21___rarg(x_10);
lean_ctor_set(x_5, 2, x_11);
x_12 = l___private_Init_Lean_Elab_Command_3__setState(x_5, x_2, x_7);
@ -2116,7 +2115,7 @@ lean_inc(x_25);
lean_inc(x_24);
lean_inc(x_23);
lean_dec(x_5);
x_27 = l_Lean_Elab_Command_modifyScope___closed__1;
x_27 = lean_box(0);
x_28 = l_unreachable_x21___rarg(x_27);
x_29 = lean_alloc_ctor(0, 5, 0);
lean_ctor_set(x_29, 0, x_23);
@ -2598,7 +2597,7 @@ if (x_8 == 0)
lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12;
x_9 = lean_ctor_get(x_5, 2);
lean_dec(x_9);
x_10 = l_Lean_Elab_Command_modifyScope___closed__1;
x_10 = lean_box(0);
x_11 = l_unreachable_x21___rarg(x_10);
lean_ctor_set(x_5, 2, x_11);
x_12 = l___private_Init_Lean_Elab_Command_3__setState(x_5, x_2, x_7);
@ -2663,7 +2662,7 @@ lean_inc(x_25);
lean_inc(x_24);
lean_inc(x_23);
lean_dec(x_5);
x_27 = l_Lean_Elab_Command_modifyScope___closed__1;
x_27 = lean_box(0);
x_28 = l_unreachable_x21___rarg(x_27);
x_29 = lean_alloc_ctor(0, 5, 0);
lean_ctor_set(x_29, 0, x_23);
@ -3145,7 +3144,7 @@ if (x_8 == 0)
lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12;
x_9 = lean_ctor_get(x_5, 2);
lean_dec(x_9);
x_10 = l_Lean_Elab_Command_modifyScope___closed__1;
x_10 = lean_box(0);
x_11 = l_unreachable_x21___rarg(x_10);
lean_ctor_set(x_5, 2, x_11);
x_12 = l___private_Init_Lean_Elab_Command_3__setState(x_5, x_2, x_7);
@ -3210,7 +3209,7 @@ lean_inc(x_25);
lean_inc(x_24);
lean_inc(x_23);
lean_dec(x_5);
x_27 = l_Lean_Elab_Command_modifyScope___closed__1;
x_27 = lean_box(0);
x_28 = l_unreachable_x21___rarg(x_27);
x_29 = lean_alloc_ctor(0, 5, 0);
lean_ctor_set(x_29, 0, x_23);
@ -3692,7 +3691,7 @@ if (x_8 == 0)
lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12;
x_9 = lean_ctor_get(x_5, 2);
lean_dec(x_9);
x_10 = l_Lean_Elab_Command_modifyScope___closed__1;
x_10 = lean_box(0);
x_11 = l_unreachable_x21___rarg(x_10);
lean_ctor_set(x_5, 2, x_11);
x_12 = l___private_Init_Lean_Elab_Command_3__setState(x_5, x_2, x_7);
@ -3757,7 +3756,7 @@ lean_inc(x_25);
lean_inc(x_24);
lean_inc(x_23);
lean_dec(x_5);
x_27 = l_Lean_Elab_Command_modifyScope___closed__1;
x_27 = lean_box(0);
x_28 = l_unreachable_x21___rarg(x_27);
x_29 = lean_alloc_ctor(0, 5, 0);
lean_ctor_set(x_29, 0, x_23);

565
stage0/stdlib/Init/Lean/Elab/Quotation.c
View file

@ -86,7 +86,6 @@ lean_object* l___private_Init_Lean_Elab_Quotation_9__compileStxMatch___main___cl
extern lean_object* l_Lean_nameToExprAux___main___closed__4;
lean_object* l___private_Init_Lean_Elab_Quotation_7__getHeadInfo___lambda__3(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Elab_Quotation_5__quoteSyntax___main___closed__50;
extern uint8_t l___private_Init_Lean_Elab_Term_4__isCDot___closed__1;
extern lean_object* l_Prod_HasRepr___rarg___closed__1;
lean_object* l_Array_umapMAux___main___at___private_Init_Lean_Elab_Quotation_7__getHeadInfo___spec__2___closed__1;
lean_object* l___private_Init_Lean_Elab_Quotation_9__compileStxMatch___main___closed__21;
@ -344,7 +343,6 @@ extern lean_object* l_Lean_Options_empty;
lean_object* l_List_map___main___at_Lean_Elab_Term_Quotation_oldExpandMatchSyntax___spec__2(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Parser_Term_beq___elambda__1___closed__1;
lean_object* l_List_mapM___main___at___private_Init_Lean_Elab_Quotation_9__compileStxMatch___main___spec__10___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_coeDecidableEq(uint8_t);
lean_object* l___private_Init_Lean_Elab_Quotation_3__quoteOption___rarg___closed__5;
lean_object* l_Lean_Array_hasQuote___rarg___boxed(lean_object*, lean_object*);
extern lean_object* l_Lean_Elab_Term_expandCDot_x3f___closed__2;
@ -5746,37 +5744,107 @@ x_50 = l_Lean_Elab_Term_Quotation_isAntiquotSplice(x_14);
if (x_46 == 0)
{
x_51 = x_16;
goto block_98;
goto block_82;
}
else
{
lean_object* x_99;
lean_object* x_83;
lean_dec(x_16);
x_99 = lean_box(0);
x_51 = x_99;
goto block_98;
x_83 = lean_box(0);
x_51 = x_83;
goto block_82;
}
block_98:
block_82:
{
lean_object* x_52; uint8_t x_64;
lean_object* x_52;
if (x_49 == 0)
{
uint8_t x_93;
x_93 = 0;
x_64 = x_93;
goto block_92;
x_52 = x_47;
goto block_63;
}
else
{
lean_object* x_94; lean_object* x_95; lean_object* x_96; uint8_t x_97;
x_94 = l_Lean_Syntax_getArgs(x_47);
x_95 = lean_array_get_size(x_94);
lean_dec(x_94);
x_96 = lean_unsigned_to_nat(3u);
x_97 = lean_nat_dec_eq(x_95, x_96);
lean_dec(x_95);
x_64 = x_97;
goto block_92;
lean_object* x_64; lean_object* x_65; lean_object* x_66; uint8_t x_67;
x_64 = l_Lean_Syntax_getArgs(x_47);
x_65 = lean_array_get_size(x_64);
lean_dec(x_64);
x_66 = lean_unsigned_to_nat(3u);
x_67 = lean_nat_dec_eq(x_65, x_66);
lean_dec(x_65);
if (x_67 == 0)
{
x_52 = x_47;
goto block_63;
}
else
{
lean_object* x_68; lean_object* x_69; uint8_t x_70;
x_68 = l_Lean_Syntax_getArg(x_47, x_13);
x_69 = l_Lean_nullKind___closed__2;
lean_inc(x_68);
x_70 = l_Lean_Syntax_isOfKind(x_68, x_69);
if (x_70 == 0)
{
lean_dec(x_68);
x_52 = x_47;
goto block_63;
}
else
{
lean_object* x_71; lean_object* x_72; lean_object* x_73; uint8_t x_74;
x_71 = l_Lean_Syntax_getArgs(x_68);
x_72 = lean_array_get_size(x_71);
lean_dec(x_71);
x_73 = lean_unsigned_to_nat(2u);
x_74 = lean_nat_dec_eq(x_72, x_73);
lean_dec(x_72);
if (x_74 == 0)
{
lean_dec(x_68);
x_52 = x_47;
goto block_63;
}
else
{
lean_object* x_75; lean_object* x_76; lean_object* x_77; uint8_t x_78;
x_75 = lean_unsigned_to_nat(0u);
x_76 = l_Lean_Syntax_getArg(x_68, x_75);
x_77 = l_Lean_Syntax_getArg(x_68, x_13);
lean_dec(x_68);
lean_inc(x_77);
x_78 = l_Lean_Syntax_isOfKind(x_77, x_69);
if (x_78 == 0)
{
lean_dec(x_77);
lean_dec(x_76);
x_52 = x_47;
goto block_63;
}
else
{
lean_object* x_79; lean_object* x_80; uint8_t x_81;
x_79 = l_Lean_Syntax_getArgs(x_77);
lean_dec(x_77);
x_80 = lean_array_get_size(x_79);
lean_dec(x_79);
x_81 = lean_nat_dec_eq(x_80, x_75);
lean_dec(x_80);
if (x_81 == 0)
{
lean_dec(x_76);
x_52 = x_47;
goto block_63;
}
else
{
lean_dec(x_47);
x_52 = x_76;
goto block_63;
}
}
}
}
}
}
block_63:
{
@ -5827,177 +5895,40 @@ lean_ctor_set(x_62, 2, x_60);
return x_62;
}
}
block_92:
{
uint8_t x_65;
x_65 = l_coeDecidableEq(x_64);
if (x_65 == 0)
{
x_52 = x_47;
goto block_63;
}
else
{
lean_object* x_66; lean_object* x_67; uint8_t x_68;
x_66 = l_Lean_Syntax_getArg(x_47, x_13);
x_67 = l_Lean_nullKind___closed__2;
lean_inc(x_66);
x_68 = l_Lean_Syntax_isOfKind(x_66, x_67);
if (x_68 == 0)
{
uint8_t x_69;
x_69 = l___private_Init_Lean_Elab_Term_4__isCDot___closed__1;
if (x_69 == 0)
{
lean_dec(x_66);
x_52 = x_47;
goto block_63;
}
else
{
lean_object* x_70; lean_object* x_71; lean_object* x_72; uint8_t x_73;
x_70 = lean_unsigned_to_nat(0u);
x_71 = l_Lean_Syntax_getArg(x_66, x_70);
x_72 = l_Lean_Syntax_getArg(x_66, x_13);
lean_dec(x_66);
lean_inc(x_72);
x_73 = l_Lean_Syntax_isOfKind(x_72, x_67);
if (x_73 == 0)
{
lean_dec(x_72);
lean_dec(x_47);
x_52 = x_71;
goto block_63;
}
else
{
lean_object* x_74; lean_object* x_75; uint8_t x_76; uint8_t x_77;
x_74 = l_Lean_Syntax_getArgs(x_72);
lean_dec(x_72);
x_75 = lean_array_get_size(x_74);
lean_dec(x_74);
x_76 = lean_nat_dec_eq(x_75, x_70);
lean_dec(x_75);
x_77 = l_coeDecidableEq(x_76);
if (x_77 == 0)
{
lean_dec(x_71);
x_52 = x_47;
goto block_63;
}
else
{
lean_dec(x_47);
x_52 = x_71;
goto block_63;
}
}
}
}
else
{
lean_object* x_78; lean_object* x_79; lean_object* x_80; uint8_t x_81; uint8_t x_82;
x_78 = l_Lean_Syntax_getArgs(x_66);
x_79 = lean_array_get_size(x_78);
lean_dec(x_78);
x_80 = lean_unsigned_to_nat(2u);
x_81 = lean_nat_dec_eq(x_79, x_80);
lean_dec(x_79);
x_82 = l_coeDecidableEq(x_81);
if (x_82 == 0)
{
lean_dec(x_66);
x_52 = x_47;
goto block_63;
}
else
{
lean_object* x_83; lean_object* x_84; lean_object* x_85; uint8_t x_86;
x_83 = lean_unsigned_to_nat(0u);
x_84 = l_Lean_Syntax_getArg(x_66, x_83);
x_85 = l_Lean_Syntax_getArg(x_66, x_13);
lean_dec(x_66);
lean_inc(x_85);
x_86 = l_Lean_Syntax_isOfKind(x_85, x_67);
if (x_86 == 0)
{
uint8_t x_87;
lean_dec(x_85);
x_87 = l___private_Init_Lean_Elab_Term_4__isCDot___closed__1;
if (x_87 == 0)
{
lean_dec(x_84);
x_52 = x_47;
goto block_63;
}
else
{
lean_dec(x_47);
x_52 = x_84;
goto block_63;
}
}
else
{
lean_object* x_88; lean_object* x_89; uint8_t x_90; uint8_t x_91;
x_88 = l_Lean_Syntax_getArgs(x_85);
lean_dec(x_85);
x_89 = lean_array_get_size(x_88);
lean_dec(x_88);
x_90 = lean_nat_dec_eq(x_89, x_83);
lean_dec(x_89);
x_91 = l_coeDecidableEq(x_90);
if (x_91 == 0)
{
lean_dec(x_84);
x_52 = x_47;
goto block_63;
}
else
{
lean_dec(x_47);
x_52 = x_84;
goto block_63;
}
}
}
}
}
}
}
}
}
else
{
lean_object* x_100;
lean_object* x_84;
lean_dec(x_14);
x_100 = l___private_Init_Lean_Elab_Quotation_7__getHeadInfo___closed__4;
return x_100;
x_84 = l___private_Init_Lean_Elab_Quotation_7__getHeadInfo___closed__4;
return x_84;
}
}
}
else
{
lean_object* x_101;
lean_object* x_85;
lean_dec(x_3);
x_101 = l___private_Init_Lean_Elab_Quotation_7__getHeadInfo___closed__4;
return x_101;
x_85 = l___private_Init_Lean_Elab_Quotation_7__getHeadInfo___closed__4;
return x_85;
}
}
else
{
lean_object* x_102; lean_object* x_103; lean_object* x_104; lean_object* x_105;
x_102 = l_Lean_mkAppStx___closed__6;
x_103 = lean_alloc_closure((void*)(l___private_Init_Lean_Elab_Quotation_7__getHeadInfo___lambda__5___boxed), 6, 3);
lean_closure_set(x_103, 0, x_102);
lean_closure_set(x_103, 1, x_3);
lean_closure_set(x_103, 2, x_4);
x_104 = lean_box(0);
x_105 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_105, 0, x_104);
lean_ctor_set(x_105, 1, x_104);
lean_ctor_set(x_105, 2, x_103);
return x_105;
lean_object* x_86; lean_object* x_87; lean_object* x_88; lean_object* x_89;
x_86 = l_Lean_mkAppStx___closed__6;
x_87 = lean_alloc_closure((void*)(l___private_Init_Lean_Elab_Quotation_7__getHeadInfo___lambda__5___boxed), 6, 3);
lean_closure_set(x_87, 0, x_86);
lean_closure_set(x_87, 1, x_3);
lean_closure_set(x_87, 2, x_4);
x_88 = lean_box(0);
x_89 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_89, 0, x_88);
lean_ctor_set(x_89, 1, x_88);
lean_ctor_set(x_89, 2, x_87);
return x_89;
}
}
}
@ -11060,7 +10991,7 @@ return x_6;
}
else
{
lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; uint8_t x_11; uint8_t x_12;
lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; uint8_t x_11;
x_7 = l_Lean_Syntax_inhabited;
x_8 = lean_unsigned_to_nat(1u);
x_9 = lean_array_get(x_7, x_2, x_8);
@ -11069,154 +11000,110 @@ lean_inc(x_9);
x_11 = l_Lean_Syntax_isOfKind(x_9, x_10);
if (x_11 == 0)
{
uint8_t x_66;
x_66 = 0;
x_12 = x_66;
goto block_65;
}
else
{
lean_object* x_67; lean_object* x_68; lean_object* x_69; uint8_t x_70;
x_67 = l_Lean_Syntax_getArgs(x_9);
x_68 = lean_array_get_size(x_67);
lean_dec(x_67);
x_69 = lean_unsigned_to_nat(3u);
x_70 = lean_nat_dec_eq(x_68, x_69);
lean_dec(x_68);
x_12 = x_70;
goto block_65;
}
block_65:
{
uint8_t x_13;
x_13 = l_coeDecidableEq(x_12);
lean_object* x_12; uint8_t x_13;
x_12 = l_Lean_mkTermIdFromIdent___closed__2;
lean_inc(x_9);
x_13 = l_Lean_Syntax_isOfKind(x_9, x_12);
if (x_13 == 0)
{
lean_object* x_14; uint8_t x_15;
x_14 = l_Lean_mkTermIdFromIdent___closed__2;
lean_inc(x_9);
x_15 = l_Lean_Syntax_isOfKind(x_9, x_14);
if (x_15 == 0)
{
lean_object* x_16;
lean_object* x_14;
lean_dec(x_9);
x_16 = lean_box(0);
x_14 = lean_box(0);
return x_14;
}
else
{
lean_object* x_15; lean_object* x_16;
x_15 = lean_box(0);
x_16 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_16, 0, x_9);
lean_ctor_set(x_16, 1, x_15);
return x_16;
}
else
{
lean_object* x_17; lean_object* x_18;
x_17 = lean_box(0);
x_18 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_18, 0, x_9);
lean_ctor_set(x_18, 1, x_17);
return x_18;
}
}
else
{
lean_object* x_19; uint8_t x_20; lean_object* x_58; uint8_t x_59;
x_19 = l_Lean_Syntax_getArg(x_9, x_8);
x_58 = l_Lean_nullKind___closed__2;
lean_inc(x_19);
x_59 = l_Lean_Syntax_isOfKind(x_19, x_58);
if (x_59 == 0)
lean_object* x_17; lean_object* x_18; lean_object* x_19; uint8_t x_20;
x_17 = l_Lean_Syntax_getArgs(x_9);
x_18 = lean_array_get_size(x_17);
lean_dec(x_17);
x_19 = lean_unsigned_to_nat(3u);
x_20 = lean_nat_dec_eq(x_18, x_19);
lean_dec(x_18);
if (x_20 == 0)
{
uint8_t x_60;
x_60 = 0;
x_20 = x_60;
goto block_57;
}
else
{
lean_object* x_61; lean_object* x_62; lean_object* x_63; uint8_t x_64;
x_61 = l_Lean_Syntax_getArgs(x_19);
x_62 = lean_array_get_size(x_61);
lean_dec(x_61);
x_63 = lean_unsigned_to_nat(2u);
x_64 = lean_nat_dec_eq(x_62, x_63);
lean_dec(x_62);
x_20 = x_64;
goto block_57;
}
block_57:
{
uint8_t x_21;
x_21 = l_coeDecidableEq(x_20);
if (x_21 == 0)
{
lean_object* x_22; uint8_t x_23;
lean_dec(x_19);
x_22 = l_Lean_mkTermIdFromIdent___closed__2;
lean_object* x_21; uint8_t x_22;
x_21 = l_Lean_mkTermIdFromIdent___closed__2;
lean_inc(x_9);
x_23 = l_Lean_Syntax_isOfKind(x_9, x_22);
if (x_23 == 0)
x_22 = l_Lean_Syntax_isOfKind(x_9, x_21);
if (x_22 == 0)
{
lean_object* x_24;
lean_object* x_23;
lean_dec(x_9);
x_23 = lean_box(0);
return x_23;
}
else
{
lean_object* x_24; lean_object* x_25;
x_24 = lean_box(0);
return x_24;
}
else
{
lean_object* x_25; lean_object* x_26;
x_25 = lean_box(0);
x_26 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_26, 0, x_9);
lean_ctor_set(x_26, 1, x_25);
return x_26;
x_25 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_25, 0, x_9);
lean_ctor_set(x_25, 1, x_24);
return x_25;
}
}
else
{
lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; uint8_t x_31;
x_27 = lean_unsigned_to_nat(0u);
x_28 = l_Lean_Syntax_getArg(x_19, x_27);
x_29 = l_Lean_Syntax_getArg(x_19, x_8);
lean_dec(x_19);
x_30 = l_Lean_nullKind___closed__2;
lean_inc(x_29);
x_31 = l_Lean_Syntax_isOfKind(x_29, x_30);
if (x_31 == 0)
lean_object* x_26; lean_object* x_27; uint8_t x_28;
x_26 = l_Lean_Syntax_getArg(x_9, x_8);
x_27 = l_Lean_nullKind___closed__2;
lean_inc(x_26);
x_28 = l_Lean_Syntax_isOfKind(x_26, x_27);
if (x_28 == 0)
{
uint8_t x_32;
lean_dec(x_29);
x_32 = l___private_Init_Lean_Elab_Term_4__isCDot___closed__1;
if (x_32 == 0)
{
lean_object* x_33; uint8_t x_34;
lean_dec(x_28);
x_33 = l_Lean_mkTermIdFromIdent___closed__2;
lean_object* x_29; uint8_t x_30;
lean_dec(x_26);
x_29 = l_Lean_mkTermIdFromIdent___closed__2;
lean_inc(x_9);
x_34 = l_Lean_Syntax_isOfKind(x_9, x_33);
if (x_34 == 0)
x_30 = l_Lean_Syntax_isOfKind(x_9, x_29);
if (x_30 == 0)
{
lean_object* x_35;
lean_object* x_31;
lean_dec(x_9);
x_35 = lean_box(0);
return x_35;
x_31 = lean_box(0);
return x_31;
}
else
{
lean_object* x_36; lean_object* x_37;
x_36 = lean_box(0);
x_37 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_37, 0, x_9);
lean_ctor_set(x_37, 1, x_36);
return x_37;
lean_object* x_32; lean_object* x_33;
x_32 = lean_box(0);
x_33 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_33, 0, x_9);
lean_ctor_set(x_33, 1, x_32);
return x_33;
}
}
else
{
lean_object* x_34; lean_object* x_35; lean_object* x_36; uint8_t x_37;
x_34 = l_Lean_Syntax_getArgs(x_26);
x_35 = lean_array_get_size(x_34);
lean_dec(x_34);
x_36 = lean_unsigned_to_nat(2u);
x_37 = lean_nat_dec_eq(x_35, x_36);
lean_dec(x_35);
if (x_37 == 0)
{
lean_object* x_38; uint8_t x_39;
lean_dec(x_9);
lean_dec(x_26);
x_38 = l_Lean_mkTermIdFromIdent___closed__2;
lean_inc(x_28);
x_39 = l_Lean_Syntax_isOfKind(x_28, x_38);
lean_inc(x_9);
x_39 = l_Lean_Syntax_isOfKind(x_9, x_38);
if (x_39 == 0)
{
lean_object* x_40;
lean_dec(x_28);
lean_dec(x_9);
x_40 = lean_box(0);
return x_40;
}
@ -11225,26 +11112,25 @@ else
lean_object* x_41; lean_object* x_42;
x_41 = lean_box(0);
x_42 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_42, 0, x_28);
lean_ctor_set(x_42, 0, x_9);
lean_ctor_set(x_42, 1, x_41);
return x_42;
}
}
}
else
{
lean_object* x_43; lean_object* x_44; uint8_t x_45; uint8_t x_46;
x_43 = l_Lean_Syntax_getArgs(x_29);
lean_dec(x_29);
x_44 = lean_array_get_size(x_43);
lean_dec(x_43);
x_45 = lean_nat_dec_eq(x_44, x_27);
lean_dec(x_44);
x_46 = l_coeDecidableEq(x_45);
lean_object* x_43; lean_object* x_44; lean_object* x_45; uint8_t x_46;
x_43 = lean_unsigned_to_nat(0u);
x_44 = l_Lean_Syntax_getArg(x_26, x_43);
x_45 = l_Lean_Syntax_getArg(x_26, x_8);
lean_dec(x_26);
lean_inc(x_45);
x_46 = l_Lean_Syntax_isOfKind(x_45, x_27);
if (x_46 == 0)
{
lean_object* x_47; uint8_t x_48;
lean_dec(x_28);
lean_dec(x_45);
lean_dec(x_44);
x_47 = l_Lean_mkTermIdFromIdent___closed__2;
lean_inc(x_9);
x_48 = l_Lean_Syntax_isOfKind(x_9, x_47);
@ -11267,26 +11153,59 @@ return x_51;
}
else
{
lean_object* x_52; uint8_t x_53;
lean_object* x_52; lean_object* x_53; uint8_t x_54;
x_52 = l_Lean_Syntax_getArgs(x_45);
lean_dec(x_45);
x_53 = lean_array_get_size(x_52);
lean_dec(x_52);
x_54 = lean_nat_dec_eq(x_53, x_43);
lean_dec(x_53);
if (x_54 == 0)
{
lean_object* x_55; uint8_t x_56;
lean_dec(x_44);
x_55 = l_Lean_mkTermIdFromIdent___closed__2;
lean_inc(x_9);
x_56 = l_Lean_Syntax_isOfKind(x_9, x_55);
if (x_56 == 0)
{
lean_object* x_57;
lean_dec(x_9);
x_52 = l_Lean_mkTermIdFromIdent___closed__2;
lean_inc(x_28);
x_53 = l_Lean_Syntax_isOfKind(x_28, x_52);
if (x_53 == 0)
{
lean_object* x_54;
lean_dec(x_28);
x_54 = lean_box(0);
return x_54;
x_57 = lean_box(0);
return x_57;
}
else
{
lean_object* x_55; lean_object* x_56;
x_55 = lean_box(0);
x_56 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_56, 0, x_28);
lean_ctor_set(x_56, 1, x_55);
return x_56;
lean_object* x_58; lean_object* x_59;
x_58 = lean_box(0);
x_59 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_59, 0, x_9);
lean_ctor_set(x_59, 1, x_58);
return x_59;
}
}
else
{
lean_object* x_60; uint8_t x_61;
lean_dec(x_9);
x_60 = l_Lean_mkTermIdFromIdent___closed__2;
lean_inc(x_44);
x_61 = l_Lean_Syntax_isOfKind(x_44, x_60);
if (x_61 == 0)
{
lean_object* x_62;
lean_dec(x_44);
x_62 = lean_box(0);
return x_62;
}
else
{
lean_object* x_63; lean_object* x_64;
x_63 = lean_box(0);
x_64 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_64, 0, x_44);
lean_ctor_set(x_64, 1, x_63);
return x_64;
}
}
}
@ -11298,9 +11217,9 @@ return x_56;
}
else
{
lean_object* x_71;
x_71 = lean_box(0);
return x_71;
lean_object* x_65;
x_65 = lean_box(0);
return x_65;
}
}
}

1720
stage0/stdlib/Init/Lean/Elab/Syntax.c
View file

File diff suppressed because it is too large Load diff

1131
stage0/stdlib/Init/Lean/Elab/Tactic/Basic.c
View file

File diff suppressed because it is too large Load diff

598
stage0/stdlib/Init/Lean/Elab/Tactic/ElabTerm.c
View file

@ -38,7 +38,6 @@ lean_object* l___regBuiltinTactic_Lean_Elab_Tactic_evalApply(lean_object*);
lean_object* lean_name_mk_string(lean_object*, lean_object*);
lean_object* l_Lean_Elab_Term_synthesizeSyntheticMVars___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_getMainGoal(lean_object*, lean_object*, lean_object*);
uint8_t l_coeDecidableEq(uint8_t);
lean_object* l_Lean_Elab_Tactic_evalApply___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_evalExact___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Tactic_evalExact___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -437,33 +436,10 @@ return x_30;
lean_object* l_Lean_Elab_Tactic_evalExact(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
uint8_t x_4; lean_object* x_29; uint8_t x_30;
x_29 = l_Lean_Parser_Tactic_exact___elambda__1___closed__2;
lean_object* x_4; uint8_t x_5;
x_4 = l_Lean_Parser_Tactic_exact___elambda__1___closed__2;
lean_inc(x_1);
x_30 = l_Lean_Syntax_isOfKind(x_1, x_29);
if (x_30 == 0)
{
uint8_t x_31;
x_31 = 0;
x_4 = x_31;
goto block_28;
}
else
{
lean_object* x_32; lean_object* x_33; lean_object* x_34; uint8_t x_35;
x_32 = l_Lean_Syntax_getArgs(x_1);
x_33 = lean_array_get_size(x_32);
lean_dec(x_32);
x_34 = lean_unsigned_to_nat(2u);
x_35 = lean_nat_dec_eq(x_33, x_34);
lean_dec(x_33);
x_4 = x_35;
goto block_28;
}
block_28:
{
uint8_t x_5;
x_5 = l_coeDecidableEq(x_4);
x_5 = l_Lean_Syntax_isOfKind(x_1, x_4);
if (x_5 == 0)
{
lean_object* x_6;
@ -473,97 +449,113 @@ return x_6;
}
else
{
lean_object* x_7; lean_object* x_8; lean_object* x_9;
x_7 = lean_unsigned_to_nat(1u);
x_8 = l_Lean_Syntax_getArg(x_1, x_7);
lean_object* x_7; lean_object* x_8; lean_object* x_9; uint8_t x_10;
x_7 = l_Lean_Syntax_getArgs(x_1);
x_8 = lean_array_get_size(x_7);
lean_dec(x_7);
x_9 = lean_unsigned_to_nat(2u);
x_10 = lean_nat_dec_eq(x_8, x_9);
lean_dec(x_8);
if (x_10 == 0)
{
lean_object* x_11;
lean_dec(x_1);
x_11 = l_Lean_Elab_Tactic_throwUnsupportedSyntax___rarg(x_2, x_3);
return x_11;
}
else
{
lean_object* x_12; lean_object* x_13; lean_object* x_14;
x_12 = lean_unsigned_to_nat(1u);
x_13 = l_Lean_Syntax_getArg(x_1, x_12);
lean_inc(x_2);
lean_inc(x_1);
x_9 = l_Lean_Elab_Tactic_getMainGoal(x_1, x_2, x_3);
if (lean_obj_tag(x_9) == 0)
x_14 = l_Lean_Elab_Tactic_getMainGoal(x_1, x_2, x_3);
if (lean_obj_tag(x_14) == 0)
{
lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17;
x_10 = lean_ctor_get(x_9, 0);
lean_inc(x_10);
x_11 = lean_ctor_get(x_9, 1);
lean_inc(x_11);
lean_dec(x_9);
x_12 = lean_ctor_get(x_10, 0);
lean_inc(x_12);
x_13 = lean_ctor_get(x_10, 1);
lean_inc(x_13);
lean_dec(x_10);
lean_inc(x_12);
x_14 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_getMVarDecl___boxed), 3, 1);
lean_closure_set(x_14, 0, x_12);
lean_inc(x_12);
x_15 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_evalExact___lambda__1___boxed), 6, 3);
lean_closure_set(x_15, 0, x_8);
lean_closure_set(x_15, 1, x_1);
lean_closure_set(x_15, 2, x_12);
x_16 = lean_alloc_closure((void*)(l_ReaderT_bind___at_Lean_Elab_Tactic_monadLog___spec__2___rarg), 4, 2);
lean_closure_set(x_16, 0, x_14);
lean_closure_set(x_16, 1, x_15);
lean_inc(x_2);
x_17 = l_Lean_Elab_Tactic_withMVarContext___rarg(x_12, x_16, x_2, x_11);
lean_dec(x_12);
if (lean_obj_tag(x_17) == 0)
{
lean_object* x_18; lean_object* x_19;
x_18 = lean_ctor_get(x_17, 1);
lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22;
x_15 = lean_ctor_get(x_14, 0);
lean_inc(x_15);
x_16 = lean_ctor_get(x_14, 1);
lean_inc(x_16);
lean_dec(x_14);
x_17 = lean_ctor_get(x_15, 0);
lean_inc(x_17);
x_18 = lean_ctor_get(x_15, 1);
lean_inc(x_18);
lean_dec(x_15);
lean_inc(x_17);
x_19 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_getMVarDecl___boxed), 3, 1);
lean_closure_set(x_19, 0, x_17);
lean_inc(x_17);
x_20 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_evalExact___lambda__1___boxed), 6, 3);
lean_closure_set(x_20, 0, x_13);
lean_closure_set(x_20, 1, x_1);
lean_closure_set(x_20, 2, x_17);
x_21 = lean_alloc_closure((void*)(l_ReaderT_bind___at_Lean_Elab_Tactic_monadLog___spec__2___rarg), 4, 2);
lean_closure_set(x_21, 0, x_19);
lean_closure_set(x_21, 1, x_20);
lean_inc(x_2);
x_22 = l_Lean_Elab_Tactic_withMVarContext___rarg(x_17, x_21, x_2, x_16);
lean_dec(x_17);
x_19 = l_Lean_Elab_Tactic_setGoals(x_13, x_2, x_18);
if (lean_obj_tag(x_22) == 0)
{
lean_object* x_23; lean_object* x_24;
x_23 = lean_ctor_get(x_22, 1);
lean_inc(x_23);
lean_dec(x_22);
x_24 = l_Lean_Elab_Tactic_setGoals(x_18, x_2, x_23);
lean_dec(x_2);
return x_19;
return x_24;
}
else
{
uint8_t x_20;
uint8_t x_25;
lean_dec(x_18);
lean_dec(x_2);
x_25 = !lean_is_exclusive(x_22);
if (x_25 == 0)
{
return x_22;
}
else
{
lean_object* x_26; lean_object* x_27; lean_object* x_28;
x_26 = lean_ctor_get(x_22, 0);
x_27 = lean_ctor_get(x_22, 1);
lean_inc(x_27);
lean_inc(x_26);
lean_dec(x_22);
x_28 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_28, 0, x_26);
lean_ctor_set(x_28, 1, x_27);
return x_28;
}
}
}
else
{
uint8_t x_29;
lean_dec(x_13);
lean_dec(x_2);
x_20 = !lean_is_exclusive(x_17);
if (x_20 == 0)
{
return x_17;
}
else
{
lean_object* x_21; lean_object* x_22; lean_object* x_23;
x_21 = lean_ctor_get(x_17, 0);
x_22 = lean_ctor_get(x_17, 1);
lean_inc(x_22);
lean_inc(x_21);
lean_dec(x_17);
x_23 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_23, 0, x_21);
lean_ctor_set(x_23, 1, x_22);
return x_23;
}
}
}
else
{
uint8_t x_24;
lean_dec(x_8);
lean_dec(x_2);
lean_dec(x_1);
x_24 = !lean_is_exclusive(x_9);
if (x_24 == 0)
x_29 = !lean_is_exclusive(x_14);
if (x_29 == 0)
{
return x_9;
return x_14;
}
else
{
lean_object* x_25; lean_object* x_26; lean_object* x_27;
x_25 = lean_ctor_get(x_9, 0);
x_26 = lean_ctor_get(x_9, 1);
lean_inc(x_26);
lean_inc(x_25);
lean_dec(x_9);
x_27 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_27, 0, x_25);
lean_ctor_set(x_27, 1, x_26);
return x_27;
lean_object* x_30; lean_object* x_31; lean_object* x_32;
x_30 = lean_ctor_get(x_14, 0);
x_31 = lean_ctor_get(x_14, 1);
lean_inc(x_31);
lean_inc(x_30);
lean_dec(x_14);
x_32 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_32, 0, x_30);
lean_ctor_set(x_32, 1, x_31);
return x_32;
}
}
}
@ -815,33 +807,10 @@ return x_43;
lean_object* l_Lean_Elab_Tactic_evalRefine(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
uint8_t x_4; lean_object* x_31; uint8_t x_32;
x_31 = l_Lean_Parser_Tactic_refine___elambda__1___closed__2;
lean_object* x_4; uint8_t x_5;
x_4 = l_Lean_Parser_Tactic_refine___elambda__1___closed__2;
lean_inc(x_1);
x_32 = l_Lean_Syntax_isOfKind(x_1, x_31);
if (x_32 == 0)
{
uint8_t x_33;
x_33 = 0;
x_4 = x_33;
goto block_30;
}
else
{
lean_object* x_34; lean_object* x_35; lean_object* x_36; uint8_t x_37;
x_34 = l_Lean_Syntax_getArgs(x_1);
x_35 = lean_array_get_size(x_34);
lean_dec(x_34);
x_36 = lean_unsigned_to_nat(2u);
x_37 = lean_nat_dec_eq(x_35, x_36);
lean_dec(x_35);
x_4 = x_37;
goto block_30;
}
block_30:
{
uint8_t x_5;
x_5 = l_coeDecidableEq(x_4);
x_5 = l_Lean_Syntax_isOfKind(x_1, x_4);
if (x_5 == 0)
{
lean_object* x_6;
@ -851,100 +820,116 @@ return x_6;
}
else
{
lean_object* x_7; lean_object* x_8; lean_object* x_9;
x_7 = lean_unsigned_to_nat(1u);
x_8 = l_Lean_Syntax_getArg(x_1, x_7);
lean_object* x_7; lean_object* x_8; lean_object* x_9; uint8_t x_10;
x_7 = l_Lean_Syntax_getArgs(x_1);
x_8 = lean_array_get_size(x_7);
lean_dec(x_7);
x_9 = lean_unsigned_to_nat(2u);
x_10 = lean_nat_dec_eq(x_8, x_9);
lean_dec(x_8);
if (x_10 == 0)
{
lean_object* x_11;
lean_dec(x_1);
x_11 = l_Lean_Elab_Tactic_throwUnsupportedSyntax___rarg(x_2, x_3);
return x_11;
}
else
{
lean_object* x_12; lean_object* x_13; lean_object* x_14;
x_12 = lean_unsigned_to_nat(1u);
x_13 = l_Lean_Syntax_getArg(x_1, x_12);
lean_inc(x_2);
lean_inc(x_1);
x_9 = l_Lean_Elab_Tactic_getMainGoal(x_1, x_2, x_3);
if (lean_obj_tag(x_9) == 0)
x_14 = l_Lean_Elab_Tactic_getMainGoal(x_1, x_2, x_3);
if (lean_obj_tag(x_14) == 0)
{
lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17;
x_10 = lean_ctor_get(x_9, 0);
lean_inc(x_10);
x_11 = lean_ctor_get(x_9, 1);
lean_inc(x_11);
lean_dec(x_9);
x_12 = lean_ctor_get(x_10, 0);
lean_inc(x_12);
x_13 = lean_ctor_get(x_10, 1);
lean_inc(x_13);
lean_dec(x_10);
lean_inc(x_12);
x_14 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_getMVarDecl___boxed), 3, 1);
lean_closure_set(x_14, 0, x_12);
lean_inc(x_12);
x_15 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_evalRefine___lambda__1), 6, 3);
lean_closure_set(x_15, 0, x_8);
lean_closure_set(x_15, 1, x_1);
lean_closure_set(x_15, 2, x_12);
x_16 = lean_alloc_closure((void*)(l_ReaderT_bind___at_Lean_Elab_Tactic_monadLog___spec__2___rarg), 4, 2);
lean_closure_set(x_16, 0, x_14);
lean_closure_set(x_16, 1, x_15);
lean_inc(x_2);
x_17 = l_Lean_Elab_Tactic_withMVarContext___rarg(x_12, x_16, x_2, x_11);
lean_dec(x_12);
if (lean_obj_tag(x_17) == 0)
{
lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21;
x_18 = lean_ctor_get(x_17, 0);
lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22;
x_15 = lean_ctor_get(x_14, 0);
lean_inc(x_15);
x_16 = lean_ctor_get(x_14, 1);
lean_inc(x_16);
lean_dec(x_14);
x_17 = lean_ctor_get(x_15, 0);
lean_inc(x_17);
x_18 = lean_ctor_get(x_15, 1);
lean_inc(x_18);
x_19 = lean_ctor_get(x_17, 1);
lean_inc(x_19);
lean_dec(x_15);
lean_inc(x_17);
x_19 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_getMVarDecl___boxed), 3, 1);
lean_closure_set(x_19, 0, x_17);
lean_inc(x_17);
x_20 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_evalRefine___lambda__1), 6, 3);
lean_closure_set(x_20, 0, x_13);
lean_closure_set(x_20, 1, x_1);
lean_closure_set(x_20, 2, x_17);
x_21 = lean_alloc_closure((void*)(l_ReaderT_bind___at_Lean_Elab_Tactic_monadLog___spec__2___rarg), 4, 2);
lean_closure_set(x_21, 0, x_19);
lean_closure_set(x_21, 1, x_20);
lean_inc(x_2);
x_22 = l_Lean_Elab_Tactic_withMVarContext___rarg(x_17, x_21, x_2, x_16);
lean_dec(x_17);
x_20 = l_List_append___rarg(x_18, x_13);
x_21 = l_Lean_Elab_Tactic_setGoals(x_20, x_2, x_19);
if (lean_obj_tag(x_22) == 0)
{
lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26;
x_23 = lean_ctor_get(x_22, 0);
lean_inc(x_23);
x_24 = lean_ctor_get(x_22, 1);
lean_inc(x_24);
lean_dec(x_22);
x_25 = l_List_append___rarg(x_23, x_18);
x_26 = l_Lean_Elab_Tactic_setGoals(x_25, x_2, x_24);
lean_dec(x_2);
return x_21;
return x_26;
}
else
{
uint8_t x_22;
uint8_t x_27;
lean_dec(x_18);
lean_dec(x_2);
x_27 = !lean_is_exclusive(x_22);
if (x_27 == 0)
{
return x_22;
}
else
{
lean_object* x_28; lean_object* x_29; lean_object* x_30;
x_28 = lean_ctor_get(x_22, 0);
x_29 = lean_ctor_get(x_22, 1);
lean_inc(x_29);
lean_inc(x_28);
lean_dec(x_22);
x_30 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_30, 0, x_28);
lean_ctor_set(x_30, 1, x_29);
return x_30;
}
}
}
else
{
uint8_t x_31;
lean_dec(x_13);
lean_dec(x_2);
x_22 = !lean_is_exclusive(x_17);
if (x_22 == 0)
{
return x_17;
}
else
{
lean_object* x_23; lean_object* x_24; lean_object* x_25;
x_23 = lean_ctor_get(x_17, 0);
x_24 = lean_ctor_get(x_17, 1);
lean_inc(x_24);
lean_inc(x_23);
lean_dec(x_17);
x_25 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_25, 0, x_23);
lean_ctor_set(x_25, 1, x_24);
return x_25;
}
}
}
else
{
uint8_t x_26;
lean_dec(x_8);
lean_dec(x_2);
lean_dec(x_1);
x_26 = !lean_is_exclusive(x_9);
if (x_26 == 0)
x_31 = !lean_is_exclusive(x_14);
if (x_31 == 0)
{
return x_9;
return x_14;
}
else
{
lean_object* x_27; lean_object* x_28; lean_object* x_29;
x_27 = lean_ctor_get(x_9, 0);
x_28 = lean_ctor_get(x_9, 1);
lean_inc(x_28);
lean_inc(x_27);
lean_dec(x_9);
x_29 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_29, 0, x_27);
lean_ctor_set(x_29, 1, x_28);
return x_29;
lean_object* x_32; lean_object* x_33; lean_object* x_34;
x_32 = lean_ctor_get(x_14, 0);
x_33 = lean_ctor_get(x_14, 1);
lean_inc(x_33);
lean_inc(x_32);
lean_dec(x_14);
x_34 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_34, 0, x_32);
lean_ctor_set(x_34, 1, x_33);
return x_34;
}
}
}
@ -1132,33 +1117,10 @@ return x_33;
lean_object* l_Lean_Elab_Tactic_evalApply(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
uint8_t x_4; lean_object* x_31; uint8_t x_32;
x_31 = l_Lean_Parser_Tactic_apply___elambda__1___closed__2;
lean_object* x_4; uint8_t x_5;
x_4 = l_Lean_Parser_Tactic_apply___elambda__1___closed__2;
lean_inc(x_1);
x_32 = l_Lean_Syntax_isOfKind(x_1, x_31);
if (x_32 == 0)
{
uint8_t x_33;
x_33 = 0;
x_4 = x_33;
goto block_30;
}
else
{
lean_object* x_34; lean_object* x_35; lean_object* x_36; uint8_t x_37;
x_34 = l_Lean_Syntax_getArgs(x_1);
x_35 = lean_array_get_size(x_34);
lean_dec(x_34);
x_36 = lean_unsigned_to_nat(2u);
x_37 = lean_nat_dec_eq(x_35, x_36);
lean_dec(x_35);
x_4 = x_37;
goto block_30;
}
block_30:
{
uint8_t x_5;
x_5 = l_coeDecidableEq(x_4);
x_5 = l_Lean_Syntax_isOfKind(x_1, x_4);
if (x_5 == 0)
{
lean_object* x_6;
@ -1168,100 +1130,116 @@ return x_6;
}
else
{
lean_object* x_7; lean_object* x_8; lean_object* x_9;
x_7 = lean_unsigned_to_nat(1u);
x_8 = l_Lean_Syntax_getArg(x_1, x_7);
lean_object* x_7; lean_object* x_8; lean_object* x_9; uint8_t x_10;
x_7 = l_Lean_Syntax_getArgs(x_1);
x_8 = lean_array_get_size(x_7);
lean_dec(x_7);
x_9 = lean_unsigned_to_nat(2u);
x_10 = lean_nat_dec_eq(x_8, x_9);
lean_dec(x_8);
if (x_10 == 0)
{
lean_object* x_11;
lean_dec(x_1);
x_11 = l_Lean_Elab_Tactic_throwUnsupportedSyntax___rarg(x_2, x_3);
return x_11;
}
else
{
lean_object* x_12; lean_object* x_13; lean_object* x_14;
x_12 = lean_unsigned_to_nat(1u);
x_13 = l_Lean_Syntax_getArg(x_1, x_12);
lean_inc(x_2);
lean_inc(x_1);
x_9 = l_Lean_Elab_Tactic_getMainGoal(x_1, x_2, x_3);
if (lean_obj_tag(x_9) == 0)
x_14 = l_Lean_Elab_Tactic_getMainGoal(x_1, x_2, x_3);
if (lean_obj_tag(x_14) == 0)
{
lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17;
x_10 = lean_ctor_get(x_9, 0);
lean_inc(x_10);
x_11 = lean_ctor_get(x_9, 1);
lean_inc(x_11);
lean_dec(x_9);
x_12 = lean_ctor_get(x_10, 0);
lean_inc(x_12);
x_13 = lean_ctor_get(x_10, 1);
lean_inc(x_13);
lean_dec(x_10);
lean_inc(x_12);
x_14 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_getMVarDecl___boxed), 3, 1);
lean_closure_set(x_14, 0, x_12);
lean_inc(x_12);
x_15 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_evalApply___lambda__1___boxed), 6, 3);
lean_closure_set(x_15, 0, x_8);
lean_closure_set(x_15, 1, x_12);
lean_closure_set(x_15, 2, x_1);
x_16 = lean_alloc_closure((void*)(l_ReaderT_bind___at_Lean_Elab_Tactic_monadLog___spec__2___rarg), 4, 2);
lean_closure_set(x_16, 0, x_14);
lean_closure_set(x_16, 1, x_15);
lean_inc(x_2);
x_17 = l_Lean_Elab_Tactic_withMVarContext___rarg(x_12, x_16, x_2, x_11);
lean_dec(x_12);
if (lean_obj_tag(x_17) == 0)
{
lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21;
x_18 = lean_ctor_get(x_17, 0);
lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22;
x_15 = lean_ctor_get(x_14, 0);
lean_inc(x_15);
x_16 = lean_ctor_get(x_14, 1);
lean_inc(x_16);
lean_dec(x_14);
x_17 = lean_ctor_get(x_15, 0);
lean_inc(x_17);
x_18 = lean_ctor_get(x_15, 1);
lean_inc(x_18);
x_19 = lean_ctor_get(x_17, 1);
lean_inc(x_19);
lean_dec(x_15);
lean_inc(x_17);
x_19 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_getMVarDecl___boxed), 3, 1);
lean_closure_set(x_19, 0, x_17);
lean_inc(x_17);
x_20 = lean_alloc_closure((void*)(l_Lean_Elab_Tactic_evalApply___lambda__1___boxed), 6, 3);
lean_closure_set(x_20, 0, x_13);
lean_closure_set(x_20, 1, x_17);
lean_closure_set(x_20, 2, x_1);
x_21 = lean_alloc_closure((void*)(l_ReaderT_bind___at_Lean_Elab_Tactic_monadLog___spec__2___rarg), 4, 2);
lean_closure_set(x_21, 0, x_19);
lean_closure_set(x_21, 1, x_20);
lean_inc(x_2);
x_22 = l_Lean_Elab_Tactic_withMVarContext___rarg(x_17, x_21, x_2, x_16);
lean_dec(x_17);
x_20 = l_List_append___rarg(x_18, x_13);
x_21 = l_Lean_Elab_Tactic_setGoals(x_20, x_2, x_19);
if (lean_obj_tag(x_22) == 0)
{
lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26;
x_23 = lean_ctor_get(x_22, 0);
lean_inc(x_23);
x_24 = lean_ctor_get(x_22, 1);
lean_inc(x_24);
lean_dec(x_22);
x_25 = l_List_append___rarg(x_23, x_18);
x_26 = l_Lean_Elab_Tactic_setGoals(x_25, x_2, x_24);
lean_dec(x_2);
return x_21;
return x_26;
}
else
{
uint8_t x_22;
uint8_t x_27;
lean_dec(x_18);
lean_dec(x_2);
x_27 = !lean_is_exclusive(x_22);
if (x_27 == 0)
{
return x_22;
}
else
{
lean_object* x_28; lean_object* x_29; lean_object* x_30;
x_28 = lean_ctor_get(x_22, 0);
x_29 = lean_ctor_get(x_22, 1);
lean_inc(x_29);
lean_inc(x_28);
lean_dec(x_22);
x_30 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_30, 0, x_28);
lean_ctor_set(x_30, 1, x_29);
return x_30;
}
}
}
else
{
uint8_t x_31;
lean_dec(x_13);
lean_dec(x_2);
x_22 = !lean_is_exclusive(x_17);
if (x_22 == 0)
{
return x_17;
}
else
{
lean_object* x_23; lean_object* x_24; lean_object* x_25;
x_23 = lean_ctor_get(x_17, 0);
x_24 = lean_ctor_get(x_17, 1);
lean_inc(x_24);
lean_inc(x_23);
lean_dec(x_17);
x_25 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_25, 0, x_23);
lean_ctor_set(x_25, 1, x_24);
return x_25;
}
}
}
else
{
uint8_t x_26;
lean_dec(x_8);
lean_dec(x_2);
lean_dec(x_1);
x_26 = !lean_is_exclusive(x_9);
if (x_26 == 0)
x_31 = !lean_is_exclusive(x_14);
if (x_31 == 0)
{
return x_9;
return x_14;
}
else
{
lean_object* x_27; lean_object* x_28; lean_object* x_29;
x_27 = lean_ctor_get(x_9, 0);
x_28 = lean_ctor_get(x_9, 1);
lean_inc(x_28);
lean_inc(x_27);
lean_dec(x_9);
x_29 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_29, 0, x_27);
lean_ctor_set(x_29, 1, x_28);
return x_29;
lean_object* x_32; lean_object* x_33; lean_object* x_34;
x_32 = lean_ctor_get(x_14, 0);
x_33 = lean_ctor_get(x_14, 1);
lean_inc(x_33);
lean_inc(x_32);
lean_dec(x_14);
x_34 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_34, 0, x_32);
lean_ctor_set(x_34, 1, x_33);
return x_34;
}
}
}

2687
stage0/stdlib/Init/Lean/Elab/Term.c
View file

File diff suppressed because it is too large Load diff

3756
stage0/stdlib/Init/Lean/Elab/TermApp.c
View file

File diff suppressed because it is too large Load diff

1747
stage0/stdlib/Init/Lean/Elab/TermBinders.c
View file

File diff suppressed because it is too large Load diff

29
stage0/stdlib/Init/Lean/Environment.c
View file

@ -108,7 +108,6 @@ lean_object* l_Array_iterateMAux___main___at_Lean_mkModuleData___spec__4___boxed
extern lean_object* l_Lean_Name_inhabited;
lean_object* l_Lean_namespacesExt___elambda__4___rarg(lean_object*);
extern lean_object* l_String_splitAux___main___closed__1;
lean_object* l_Lean_registerEnvExtensionUnsafe___at_Lean_regModListExtension___spec__1___closed__1;
lean_object* l_Lean_PersistentEnvExtension_modifyState___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Environment_evalConst___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_registerPersistentEnvExtension___rarg(lean_object*);
@ -7790,18 +7789,6 @@ x_1 = l_NonScalar_Inhabited;
return x_1;
}
}
lean_object* _init_l_Lean_registerEnvExtensionUnsafe___at_Lean_regModListExtension___spec__1___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = lean_unsigned_to_nat(0u);
x_3 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_3, 0, x_2);
lean_ctor_set(x_3, 1, x_1);
return x_3;
}
}
lean_object* l_Lean_registerEnvExtensionUnsafe___at_Lean_regModListExtension___spec__1(lean_object* x_1, lean_object* x_2) {
_start:
{
@ -7860,7 +7847,7 @@ lean_inc(x_16);
lean_dec(x_14);
x_17 = lean_array_get_size(x_15);
lean_dec(x_15);
x_18 = l_Lean_registerEnvExtensionUnsafe___at_Lean_regModListExtension___spec__1___closed__1;
x_18 = lean_box(0);
x_19 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_19, 0, x_17);
lean_ctor_set(x_19, 1, x_1);
@ -8075,13 +8062,13 @@ lean_object* _init_l_Lean_modListExtension___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_1 = lean_unsigned_to_nat(0u);
x_2 = l_Lean_modListExtension___closed__1;
x_3 = l_Lean_registerEnvExtensionUnsafe___at_Lean_regModListExtension___spec__1___closed__1;
x_1 = lean_box(0);
x_2 = lean_unsigned_to_nat(0u);
x_3 = l_Lean_modListExtension___closed__1;
x_4 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_4, 0, x_1);
lean_ctor_set(x_4, 1, x_2);
lean_ctor_set(x_4, 2, x_3);
lean_ctor_set(x_4, 0, x_2);
lean_ctor_set(x_4, 1, x_3);
lean_ctor_set(x_4, 2, x_1);
return x_4;
}
}
@ -12666,8 +12653,6 @@ l_Lean_CPPExtensionState_inhabited = _init_l_Lean_CPPExtensionState_inhabited();
lean_mark_persistent(l_Lean_CPPExtensionState_inhabited);
l_Lean_Modification_inhabited = _init_l_Lean_Modification_inhabited();
lean_mark_persistent(l_Lean_Modification_inhabited);
l_Lean_registerEnvExtensionUnsafe___at_Lean_regModListExtension___spec__1___closed__1 = _init_l_Lean_registerEnvExtensionUnsafe___at_Lean_regModListExtension___spec__1___closed__1();
lean_mark_persistent(l_Lean_registerEnvExtensionUnsafe___at_Lean_regModListExtension___spec__1___closed__1);
l_Lean_regModListExtension___closed__1 = _init_l_Lean_regModListExtension___closed__1();
lean_mark_persistent(l_Lean_regModListExtension___closed__1);
l_Lean_modListExtension___closed__1 = _init_l_Lean_modListExtension___closed__1();

77
stage0/stdlib/Init/Lean/Meta/Message.c
View file

@ -21,6 +21,7 @@ lean_object* l_Lean_Meta_Exception_toMessageData___closed__12;
lean_object* l___private_Init_Lean_Meta_Message_1__run_x3f(lean_object*);
lean_object* l_Lean_KernelException_toMessageData___closed__19;
lean_object* l_unreachable_x21___rarg(lean_object*);
lean_object* l_Lean_Meta_Exception_toMessageData___closed__51;
lean_object* l___private_Init_Lean_Meta_Message_3__inferDomain_x3f___boxed(lean_object*, lean_object*);
extern lean_object* l_Lean_MessageData_ofList___closed__3;
lean_object* l___private_Init_Lean_Meta_Message_3__inferDomain_x3f___lambda__1(lean_object*, lean_object*, lean_object*);
@ -119,6 +120,7 @@ lean_object* l_Lean_KernelException_toMessageData___closed__1;
lean_object* l___private_Init_Lean_Meta_Message_1__run_x3f___rarg___closed__2;
lean_object* l_Lean_Meta_Exception_mkAppTypeMismatchMessage___closed__8;
lean_object* l_Lean_Meta_Exception_toMessageData___closed__22;
lean_object* l_Lean_Meta_Exception_toMessageData___closed__50;
lean_object* l_Lean_KernelException_toMessageData___closed__8;
lean_object* l_Lean_KernelException_toMessageData___closed__4;
lean_object* l_Lean_Meta_Exception_toMessageData___closed__38;
@ -144,6 +146,7 @@ lean_object* l_Lean_KernelException_toMessageData___closed__35;
lean_object* l_Lean_KernelException_toMessageData___closed__41;
lean_object* l_Lean_KernelException_toMessageData___closed__23;
lean_object* l_Lean_Meta_Exception_toMessageData___closed__7;
lean_object* l_Lean_Meta_Exception_toMessageData___closed__49;
lean_object* l_Lean_Meta_Exception_mkAppTypeMismatchMessage___closed__5;
extern lean_object* l_Lean_TraceState_Inhabited___closed__1;
lean_object* l_Lean_Meta_inferType(lean_object*, lean_object*, lean_object*);
@ -1196,7 +1199,7 @@ lean_object* _init_l_Lean_Meta_Exception_toMessageData___closed__32() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("stuck at ");
x_1 = lean_mk_string("stuck at universe level constraint ");
return x_1;
}
}
@ -1224,7 +1227,7 @@ lean_object* _init_l_Lean_Meta_Exception_toMessageData___closed__35() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("not a type class instance ");
x_1 = lean_mk_string("stuck at constraint ");
return x_1;
}
}
@ -1252,7 +1255,7 @@ lean_object* _init_l_Lean_Meta_Exception_toMessageData___closed__38() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("application builder failure ");
x_1 = lean_mk_string("not a type class instance ");
return x_1;
}
}
@ -1280,7 +1283,7 @@ lean_object* _init_l_Lean_Meta_Exception_toMessageData___closed__41() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("failed to synthesize");
x_1 = lean_mk_string("application builder failure ");
return x_1;
}
}
@ -1307,11 +1310,9 @@ return x_2;
lean_object* _init_l_Lean_Meta_Exception_toMessageData___closed__44() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Meta_Exception_toStr___closed__19;
x_2 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
lean_object* x_1;
x_1 = lean_mk_string("failed to synthesize");
return x_1;
}
}
lean_object* _init_l_Lean_Meta_Exception_toMessageData___closed__45() {
@ -1319,7 +1320,7 @@ _start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Meta_Exception_toMessageData___closed__44;
x_2 = lean_alloc_ctor(0, 1, 0);
x_2 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
}
@ -1327,16 +1328,18 @@ return x_2;
lean_object* _init_l_Lean_Meta_Exception_toMessageData___closed__46() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("' failed ");
return x_1;
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Meta_Exception_toMessageData___closed__45;
x_2 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
}
}
lean_object* _init_l_Lean_Meta_Exception_toMessageData___closed__47() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Meta_Exception_toMessageData___closed__46;
x_1 = l_Lean_Meta_Exception_toStr___closed__19;
x_2 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
@ -1352,6 +1355,34 @@ lean_ctor_set(x_2, 0, x_1);
return x_2;
}
}
lean_object* _init_l_Lean_Meta_Exception_toMessageData___closed__49() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("' failed ");
return x_1;
}
}
lean_object* _init_l_Lean_Meta_Exception_toMessageData___closed__50() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Meta_Exception_toMessageData___closed__49;
x_2 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
}
}
lean_object* _init_l_Lean_Meta_Exception_toMessageData___closed__51() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Meta_Exception_toMessageData___closed__50;
x_2 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
}
}
lean_object* l_Lean_Meta_Exception_toMessageData(lean_object* x_1) {
_start:
{
@ -1609,7 +1640,7 @@ lean_inc(x_86);
lean_dec(x_1);
x_87 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_87, 0, x_84);
x_88 = l_Lean_Meta_Exception_toMessageData___closed__34;
x_88 = l_Lean_Meta_Exception_toMessageData___closed__37;
x_89 = lean_alloc_ctor(9, 2, 0);
lean_ctor_set(x_89, 0, x_88);
lean_ctor_set(x_89, 1, x_87);
@ -1661,7 +1692,7 @@ lean_inc(x_103);
lean_dec(x_1);
x_104 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_104, 0, x_102);
x_105 = l_Lean_Meta_Exception_toMessageData___closed__37;
x_105 = l_Lean_Meta_Exception_toMessageData___closed__40;
x_106 = lean_alloc_ctor(9, 2, 0);
lean_ctor_set(x_106, 0, x_105);
lean_ctor_set(x_106, 1, x_104);
@ -1684,7 +1715,7 @@ lean_inc(x_111);
lean_dec(x_1);
x_112 = lean_alloc_ctor(4, 1, 0);
lean_ctor_set(x_112, 0, x_108);
x_113 = l_Lean_Meta_Exception_toMessageData___closed__40;
x_113 = l_Lean_Meta_Exception_toMessageData___closed__43;
x_114 = lean_alloc_ctor(9, 2, 0);
lean_ctor_set(x_114, 0, x_113);
lean_ctor_set(x_114, 1, x_112);
@ -1725,7 +1756,7 @@ lean_dec(x_1);
x_128 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_128, 0, x_126);
x_129 = l_Lean_indentExpr(x_128);
x_130 = l_Lean_Meta_Exception_toMessageData___closed__43;
x_130 = l_Lean_Meta_Exception_toMessageData___closed__46;
x_131 = lean_alloc_ctor(9, 2, 0);
lean_ctor_set(x_131, 0, x_130);
lean_ctor_set(x_131, 1, x_129);
@ -1748,11 +1779,11 @@ lean_inc(x_136);
lean_dec(x_1);
x_137 = lean_alloc_ctor(4, 1, 0);
lean_ctor_set(x_137, 0, x_133);
x_138 = l_Lean_Meta_Exception_toMessageData___closed__45;
x_138 = l_Lean_Meta_Exception_toMessageData___closed__48;
x_139 = lean_alloc_ctor(9, 2, 0);
lean_ctor_set(x_139, 0, x_138);
lean_ctor_set(x_139, 1, x_137);
x_140 = l_Lean_Meta_Exception_toMessageData___closed__48;
x_140 = l_Lean_Meta_Exception_toMessageData___closed__51;
x_141 = lean_alloc_ctor(9, 2, 0);
lean_ctor_set(x_141, 0, x_139);
lean_ctor_set(x_141, 1, x_140);
@ -2706,6 +2737,12 @@ l_Lean_Meta_Exception_toMessageData___closed__47 = _init_l_Lean_Meta_Exception_t
lean_mark_persistent(l_Lean_Meta_Exception_toMessageData___closed__47);
l_Lean_Meta_Exception_toMessageData___closed__48 = _init_l_Lean_Meta_Exception_toMessageData___closed__48();
lean_mark_persistent(l_Lean_Meta_Exception_toMessageData___closed__48);
l_Lean_Meta_Exception_toMessageData___closed__49 = _init_l_Lean_Meta_Exception_toMessageData___closed__49();
lean_mark_persistent(l_Lean_Meta_Exception_toMessageData___closed__49);
l_Lean_Meta_Exception_toMessageData___closed__50 = _init_l_Lean_Meta_Exception_toMessageData___closed__50();
lean_mark_persistent(l_Lean_Meta_Exception_toMessageData___closed__50);
l_Lean_Meta_Exception_toMessageData___closed__51 = _init_l_Lean_Meta_Exception_toMessageData___closed__51();
lean_mark_persistent(l_Lean_Meta_Exception_toMessageData___closed__51);
l_Lean_KernelException_toMessageData___closed__1 = _init_l_Lean_KernelException_toMessageData___closed__1();
lean_mark_persistent(l_Lean_KernelException_toMessageData___closed__1);
l_Lean_KernelException_toMessageData___closed__2 = _init_l_Lean_KernelException_toMessageData___closed__2();

4455
stage0/stdlib/Init/Lean/Meta/SynthInstance.c
View file

File diff suppressed because it is too large Load diff