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 2019-12-04 17:03:42 -08:00
parent 021fda2d80
commit 223b136a9e
72 changed files with 33574 additions and 803 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

78
stage0/src/Init/Core.lean
View file

@ -50,7 +50,7 @@ reserve infix ` ≤ `:50
reserve infix ` < `:50
reserve infix ` >= `:50
reserve infix ` ≥ `:50
reserve infix ` > `:50
reserve infix ` > `:50
/- boolean operations -/
@ -205,8 +205,8 @@ constant Quot.ind {α : Sort u} {r : α → α → Prop} {β : Quot r → Prop}
-/
init_quot
inductive Heq {α : Sort u} (a : α) : ∀ {β : Sort u}, β → Prop
| refl : Heq a
inductive HEq {α : Sort u} (a : α) : ∀ {β : Sort u}, β → Prop
| refl : HEq a
structure Prod (α : Type u) (β : Type v) :=
(fst : α) (snd : β)
@ -242,14 +242,14 @@ h₂ ▸ h₁
theorem Eq.symm {α : Sort u} {a b : α} (h : a = b) : b = a :=
h ▸ rfl
infix `~=` := Heq
infix `≅` := Heq
infix `~=` := HEq
infix `≅` := HEq
@[matchPattern] def Heq.rfl {α : Sort u} {a : α} : a ≅ a := Heq.refl a
@[matchPattern] def HEq.rfl {α : Sort u} {a : α} : a ≅ a := HEq.refl a
theorem eqOfHeq {α : Sort u} {a a' : α} (h : a ≅ a') : a = a' :=
have ∀ (α' : Sort u) (a' : α') (h₁ : @Heq α a α' a') (h₂ : α = α'), (Eq.recOn h₂ a : α') = a' :=
fun (α' : Sort u) (a' : α') (h₁ : @Heq α a α' a') => Heq.recOn h₁ (fun (h₂ : α = α) => rfl);
theorem eqOfHEq {α : Sort u} {a a' : α} (h : a ≅ a') : a = a' :=
have ∀ (α' : Sort u) (a' : α') (h₁ : @HEq α a α' a') (h₂ : α = α'), (Eq.recOn h₂ a : α') = a' :=
fun (α' : Sort u) (a' : α') (h₁ : @HEq α a α' a') => HEq.recOn h₁ (fun (h₂ : α = α) => rfl);
show (Eq.ndrecOn (Eq.refl α) a : α) = a' from
this α a' h (Eq.refl α)
@ -659,10 +659,10 @@ fun h₁ => h (h₁.symm)
theorem falseOfNe : a ≠ a → False := Ne.irrefl
theorem neFalseOfSelf : p → p ≠ False :=
fun (hp : p) (Heq : p = False) => Heq ▸ hp
fun (hp : p) (h : p = False) => h ▸ hp
theorem neTrueOfNot : ¬p → p ≠ True :=
fun (hnp : ¬p) (Heq : p = True) => (Heq ▸ hnp) trivial
fun (hnp : ¬p) (h : p = True) => (h ▸ hnp) trivial
theorem trueNeFalse : ¬True = False :=
neFalseOfSelf trivial
@ -680,46 +680,46 @@ section
variables {α β φ : Sort u} {a a' : α} {b b' : β} {c : φ}
@[elabAsEliminator]
theorem Heq.ndrec.{u1, u2} {α : Sort u2} {a : α} {C : ∀ {β : Sort u2}, β → Sort u1} (m : C a) {β : Sort u2} {b : β} (h : a ≅ b) : C b :=
@Heq.rec α a (fun β b _ => C b) m β b h
theorem HEq.ndrec.{u1, u2} {α : Sort u2} {a : α} {C : ∀ {β : Sort u2}, β → Sort u1} (m : C a) {β : Sort u2} {b : β} (h : a ≅ b) : C b :=
@HEq.rec α a (fun β b _ => C b) m β b h
@[elabAsEliminator]
theorem Heq.ndrecOn.{u1, u2} {α : Sort u2} {a : α} {C : ∀ {β : Sort u2}, β → Sort u1} {β : Sort u2} {b : β} (h : a ≅ b) (m : C a) : C b :=
@Heq.rec α a (fun β b _ => C b) m β b h
theorem HEq.ndrecOn.{u1, u2} {α : Sort u2} {a : α} {C : ∀ {β : Sort u2}, β → Sort u1} {β : Sort u2} {b : β} (h : a ≅ b) (m : C a) : C b :=
@HEq.rec α a (fun β b _ => C b) m β b h
theorem Heq.elim {α : Sort u} {a : α} {p : α → Sort v} {b : α} (h₁ : a ≅ b) (h₂ : p a) : p b :=
Eq.recOn (eqOfHeq h₁) h₂
theorem HEq.elim {α : Sort u} {a : α} {p : α → Sort v} {b : α} (h₁ : a ≅ b) (h₂ : p a) : p b :=
Eq.recOn (eqOfHEq h₁) h₂
theorem Heq.subst {p : ∀ (T : Sort u), T → Prop} (h₁ : a ≅ b) (h₂ : p α a) : p β b :=
Heq.ndrecOn h₁ h₂
theorem HEq.subst {p : ∀ (T : Sort u), T → Prop} (h₁ : a ≅ b) (h₂ : p α a) : p β b :=
HEq.ndrecOn h₁ h₂
theorem Heq.symm (h : a ≅ b) : b ≅ a :=
Heq.ndrecOn h (Heq.refl a)
theorem HEq.symm (h : a ≅ b) : b ≅ a :=
HEq.ndrecOn h (HEq.refl a)
theorem heqOfEq (h : a = a') : a ≅ a' :=
Eq.subst h (Heq.refl a)
Eq.subst h (HEq.refl a)
theorem Heq.trans (h₁ : a ≅ b) (h₂ : b ≅ c) : a ≅ c :=
Heq.subst h₂ h₁
theorem HEq.trans (h₁ : a ≅ b) (h₂ : b ≅ c) : a ≅ c :=
HEq.subst h₂ h₁
theorem heqOfHeqOfEq (h₁ : a ≅ b) (h₂ : b = b') : a ≅ b' :=
Heq.trans h₁ (heqOfEq h₂)
theorem heqOfHEqOfEq (h₁ : a ≅ b) (h₂ : b = b') : a ≅ b' :=
HEq.trans h₁ (heqOfEq h₂)
theorem heqOfEqOfHeq (h₁ : a = a') (h₂ : a' ≅ b) : a ≅ b :=
Heq.trans (heqOfEq h₁) h₂
theorem heqOfEqOfHEq (h₁ : a = a') (h₂ : a' ≅ b) : a ≅ b :=
HEq.trans (heqOfEq h₁) h₂
def typeEqOfHeq (h : a ≅ b) : α = β :=
Heq.ndrecOn h (Eq.refl α)
def typeEqOfHEq (h : a ≅ b) : α = β :=
HEq.ndrecOn h (Eq.refl α)
end
theorem eqRecHeq {α : Sort u} {φ : α → Sort v} : ∀ {a a' : α} (h : a = a') (p : φ a), (Eq.recOn h p : φ a') ≅ p
| a, _, rfl, p => Heq.refl p
theorem eqRecHEq {α : Sort u} {φ : α → Sort v} : ∀ {a a' : α} (h : a = a') (p : φ a), (Eq.recOn h p : φ a') ≅ p
| a, _, rfl, p => HEq.refl p
theorem ofHeqTrue {a : Prop} (h : a ≅ True) : a :=
ofEqTrue (eqOfHeq h)
theorem ofHEqTrue {a : Prop} (h : a ≅ True) : a :=
ofEqTrue (eqOfHEq h)
theorem castHeq : ∀ {α β : Sort u} (h : α = β) (a : α), cast h a ≅ a
| α, _, rfl, a => Heq.refl a
theorem castHEq : ∀ {α β : Sort u} (h : α = β) (a : α), cast h a ≅ a
| α, _, rfl, a => HEq.refl a
variables {a b c d : Prop}
@ -1385,9 +1385,9 @@ Quot.rec f (fun a b h => Subsingleton.elim _ (f b)) q
protected def hrecOn
(q : Quot r) (f : ∀ a, β (Quot.mk r a)) (c : ∀ (a b : α) (p : r a b), f a ≅ f b) : β q :=
Quot.recOn q f $
fun a b p => eqOfHeq $
have p₁ : (Eq.rec (f a) (sound p) : β (Quot.mk r b)) ≅ f a := eqRecHeq (sound p) (f a);
Heq.trans p₁ (c a b p)
fun a b p => eqOfHEq $
have p₁ : (Eq.rec (f a) (sound p) : β (Quot.mk r b)) ≅ f a := eqRecHEq (sound p) (f a);
HEq.trans p₁ (c a b p)
end
end Quot

6
stage0/src/Init/Lean/Compiler/IR/Basic.lean
View file

@ -5,9 +5,9 @@ Authors: Leonardo de Moura
-/
prelude
import Init.Data.Array
import Init.Lean.Name
import Init.Lean.KVMap
import Init.Lean.Format
import Init.Lean.Data.KVMap
import Init.Lean.Data.Name
import Init.Lean.Data.Format
import Init.Lean.Compiler.ExternAttr
/-
Implements (extended) λPure and λRc proposed in the article

2
stage0/src/Init/Lean/Compiler/IR/Format.lean
View file

@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
prelude
import Init.Lean.Data.Format
import Init.Lean.Compiler.IR.Basic
import Init.Lean.Format
namespace Lean
namespace IR

2
stage0/src/Init/Lean/Compiler/IR/UnboxResult.lean
View file

@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
prelude
import Init.Lean.Format
import Init.Lean.Data.Format
import Init.Lean.Compiler.IR.Basic
import Init.Lean.Compiler.IR.CtorLayout

2
stage0/src/Init/Lean/Compiler/NameMangling.lean
View file

@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
-/
prelude
import Init.Lean.Name
import Init.Lean.Data.Name
namespace Lean
private def String.mangleAux : Nat → String.Iterator → String → String

2
stage0/src/Init/Lean/Format.lean → stage0/src/Init/Lean/Data/Format.lean
View file

@ -4,8 +4,8 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Leonardo de Moura
-/
prelude
import Init.Lean.Options
import Init.Data.Array
import Init.Lean.Data.Options
universes u v
namespace Lean

2
stage0/src/Init/Lean/KVMap.lean → stage0/src/Init/Lean/Data/KVMap.lean
View file

@ -4,9 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
prelude
import Init.Lean.Name
import Init.Data.Option.Basic
import Init.Data.Int
import Init.Lean.Data.Name
namespace Lean

0
stage0/src/Init/Lean/LBool.lean → stage0/src/Init/Lean/Data/LBool.lean
View file

0
stage0/src/Init/Lean/LOption.lean → stage0/src/Init/Lean/Data/LOption.lean
View file

0
stage0/src/Init/Lean/Name.lean → stage0/src/Init/Lean/Data/Name.lean
View file

2
stage0/src/Init/Lean/NameGenerator.lean → stage0/src/Init/Lean/Data/NameGenerator.lean
View file

@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
prelude
import Init.Lean.Name
import Init.Lean.Data.Name
namespace Lean

2
stage0/src/Init/Lean/Options.lean → stage0/src/Init/Lean/Data/Options.lean
View file

@ -6,7 +6,7 @@ Authors: Sebastian Ullrich and Leonardo de Moura
prelude
import Init.System.IO
import Init.Data.ToString
import Init.Lean.KVMap
import Init.Lean.Data.KVMap
namespace Lean

2
stage0/src/Init/Lean/Position.lean → stage0/src/Init/Lean/Data/Position.lean
View file

@ -6,7 +6,7 @@ Authors: Leonardo de Moura, Sebastian Ullrich
prelude
import Init.Data.Nat
import Init.Data.RBMap
import Init.Lean.Format
import Init.Lean.Data.Format
namespace Lean

0
stage0/src/Init/Lean/SMap.lean → stage0/src/Init/Lean/Data/SMap.lean
View file

2
stage0/src/Init/Lean/Parser/Trie.lean → stage0/src/Init/Lean/Data/Trie.lean
View file

@ -7,7 +7,7 @@ Trie for tokenizing the Lean language
-/
prelude
import Init.Data.RBMap
import Init.Lean.Format
import Init.Lean.Data.Format
namespace Lean
namespace Parser

3
stage0/src/Init/Lean/Elaborator/Basic.lean
View file

@ -6,7 +6,6 @@ Authors: Leonardo de Moura, Sebastian Ullrich
prelude
import Init.Control.Reader
import Init.Lean.MetavarContext
import Init.Lean.NameGenerator
import Init.Lean.Scopes
import Init.Lean.Parser.Module
@ -123,7 +122,7 @@ match attrParamSyntaxToIdentifier arg with
def declareBuiltinElab (env : Environment) (addFn : Name) (kind : SyntaxNodeKind) (declName : Name) : IO Environment :=
let name := `_regBuiltinTermElab ++ declName;
let type := mkApp (mkConst `IO) (mkConst `Unit);
let val := mkCAppN addFn #[toExpr kind, toExpr declName, mkConst declName];
let val := mkAppN (mkConst addFn) #[toExpr kind, toExpr declName, mkConst declName];
let decl := Declaration.defnDecl { name := name, lparams := [], type := type, value := val, hints := ReducibilityHints.opaque, isUnsafe := false };
match env.addAndCompile {} decl with
-- TODO: pretty print error

2
stage0/src/Init/Lean/Environment.lean
View file

@ -7,8 +7,8 @@ prelude
import Init.System.IO
import Init.Util
import Init.Data.ByteArray
import Init.Lean.Data.SMap
import Init.Lean.Declaration
import Init.Lean.SMap
import Init.Lean.Path
import Init.Lean.LocalContext

25
stage0/src/Init/Lean/Expr.lean
View file

@ -4,12 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
prelude
import Init.Lean.Level
import Init.Lean.KVMap
import Init.Data.HashMap
import Init.Data.HashSet
import Init.Data.PersistentHashMap
import Init.Data.PersistentHashSet
import Init.Lean.Data.KVMap
import Init.Lean.Level
namespace Lean
@ -330,9 +330,6 @@ Expr.localE x u t $ mkDataForBinder (mixHash 43 $ hash t) t.looseBVarRange true
@[export lean_expr_mk_proj] def mkProjEx : Name → Nat → Expr → Expr := mkProj
@[export lean_expr_mk_local] def mkLocalEx : Name → Name → Expr → BinderInfo → Expr := mkLocal
def mkCApp (f : Name) (a : Expr) : Expr :=
mkApp (mkConst f) a
def mkAppN (f : Expr) (args : Array Expr) : Expr :=
args.foldl mkApp f
@ -583,14 +580,16 @@ instance : HasRepr Expr :=
end Expr
def mkCAppN (n : Name) (args : Array Expr) : Expr :=
mkAppN (mkConst n) args
def mkAppB (f a b : Expr) :=
mkApp (mkApp f a) b
def mkCAppB (n : Name) (a b : Expr) :=
mkAppB (mkConst n) a b
def mkAppB (f a b : Expr) := mkApp (mkApp f a) b
def mkApp2 (f a b : Expr) := mkAppB f a b
def mkApp3 (f a b c : Expr) := mkApp (mkAppB f a b) c
def mkApp4 (f a b c d : Expr) := mkAppB (mkAppB f a b) c d
def mkApp5 (f a b c d e : Expr) := mkApp (mkApp4 f a b c d) e
def mkApp6 (f a b c d e₁ e₂ : Expr) := mkAppB (mkApp4 f a b c d) e₁ e₂
def mkApp7 (f a b c d e₁ e₂ e₃ : Expr) := mkApp3 (mkApp4 f a b c d) e₁ e₂ e₃
def mkApp8 (f a b c d e₁ e₂ e₃ e₄ : Expr) := mkApp4 (mkApp4 f a b c d) e₁ e₂ e₃ e₄
def mkApp9 (f a b c d e₁ e₂ e₃ e₄ e₅ : Expr) := mkApp5 (mkApp4 f a b c d) e₁ e₂ e₃ e₄ e₅
def mkApp10 (f a b c d e₁ e₂ e₃ e₄ e₅ e₆ : Expr) := mkApp6 (mkApp4 f a b c d) e₁ e₂ e₃ e₄ e₅ e₆
def mkDecIsTrue (pred proof : Expr) :=
mkAppB (mkConst `Decidable.isTrue) pred proof

4
stage0/src/Init/Lean/Level.lean
View file

@ -7,8 +7,8 @@ prelude
import Init.Data.Option.Basic
import Init.Data.HashMap
import Init.Data.PersistentHashMap
import Init.Lean.Name
import Init.Lean.Format
import Init.Lean.Data.Name
import Init.Lean.Data.Format
def Nat.imax (n m : Nat) : Nat :=
if m = 0 then 0 else Nat.max n m

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

@ -7,7 +7,7 @@ Message Type used by the Lean frontend
-/
prelude
import Init.Data.ToString
import Init.Lean.Position
import Init.Lean.Data.Position
import Init.Lean.Syntax
import Init.Lean.MetavarContext
import Init.Lean.Environment

1
stage0/src/Init/Lean/Meta.lean
View file

@ -15,3 +15,4 @@ import Init.Lean.Meta.Reduce
import Init.Lean.Meta.Instances
import Init.Lean.Meta.AbstractMVars
import Init.Lean.Meta.SynthInstance
import Init.Lean.Meta.AppBuilder

157
stage0/src/Init/Lean/Meta/AppBuilder.lean
View file

@ -6,12 +6,167 @@ Authors: Leonardo de Moura
import Init.Lean.Meta.SynthInstance
namespace Lean
@[inline] def Expr.eq? (p : Expr) : Option (Expr × Expr × Expr) :=
if p.isAppOfArity `Eq 3 then
some (p.getArg! 0, p.getArg! 1, p.getArg! 2)
else
none
@[inline] def Expr.heq? (p : Expr) : Option (Expr × Expr × Expr × Expr) :=
if p.isAppOfArity `HEq 4 then
some (p.getArg! 0, p.getArg! 1, p.getArg! 2, p.getArg! 4)
else
none
@[inline] def Expr.arrow? : Expr → Option (Expr × Expr)
| Expr.forallE _ α β _ => if β.hasLooseBVars then none else some (α, β)
| _ => none
namespace Meta
def mkEq (a b : Expr) : MetaM Expr :=
do aType ← inferType a;
u ← getLevel aType;
pure $ mkAppB (mkApp (mkConst `Eq [u]) aType) a b
pure $ mkApp3 (mkConst `Eq [u]) aType a b
def mkHEq (a b : Expr) : MetaM Expr :=
do aType ← inferType a;
bType ← inferType b;
u ← getLevel aType;
pure $ mkApp4 (mkConst `HEq [u]) aType a bType b
def mkEqRefl (a : Expr) : MetaM Expr :=
do aType ← inferType a;
u ← getLevel aType;
pure $ mkApp2 (mkConst `Eq.refl [u]) aType a
def mkHEqRefl (a : Expr) : MetaM Expr :=
do aType ← inferType a;
u ← getLevel aType;
pure $ mkApp2 (mkConst `HEq.refl [u]) aType a
private def infer (h : Expr) : MetaM Expr :=
do hType ← inferType h;
whnfD hType
def mkEqSymm (h : Expr) : MetaM Expr :=
if h.isAppOf `Eq.refl then pure h
else do
hType ← infer h;
match hType.eq? with
| some (α, a, b) => do u ← getLevel α; pure $ mkApp4 (mkConst `Eq.symm [u]) α a b h
| none => throwEx $ Exception.appBuilder `Eq.symm "equality proof expected" #[h]
def mkEqTrans (h₁ h₂ : Expr) : MetaM Expr :=
if h₁.isAppOf `Eq.refl then pure h₂
else if h₂.isAppOf `Eq.refl then pure h₁
else do
hType₁ ← infer h₁;
hType₂ ← infer h₂;
match hType₁.eq?, hType₂.eq? with
| some (α, a, b), some (_, _, c) =>
do u ← getLevel α; pure $ mkApp6 (mkConst `Eq.trans [u]) α a b c h₁ h₂
| _, _ => throwEx $ Exception.appBuilder `Eq.trans "equality proof expected" #[h₁, h₂]
def mkHEqSymm (h : Expr) : MetaM Expr :=
if h.isAppOf `HEq.refl then pure h
else do
hType ← infer h;
match hType.heq? with
| some (α, a, β, b) => do u ← getLevel α; pure $ mkApp5 (mkConst `HEq.symm [u]) α β a b h
| none => throwEx $ Exception.appBuilder `HEq.symm "heterogeneous equality proof expected" #[h]
def mkHEqTrans (h₁ h₂ : Expr) : MetaM Expr :=
if h₁.isAppOf `HEq.refl then pure h₂
else if h₂.isAppOf `HEq.refl then pure h₁
else do
hType₁ ← infer h₁;
hType₂ ← infer h₂;
match hType₁.heq?, hType₂.heq? with
| some (α, a, β, b), some (_, _, γ, c) => do
u ← getLevel α; pure $ mkApp8 (mkConst `HEq.trans [u]) α β γ a b c h₁ h₂
| _, _ => throwEx $ Exception.appBuilder `HEq.trans "heterogeneous equality proof expected" #[h₁, h₂]
def mkCongrArg (f h : Expr) : MetaM Expr :=
do hType ← infer h;
fType ← infer f;
match fType.arrow?, hType.eq? with
| some (α, β), some (_, a, b) => do
u ← getLevel α; v ← getLevel β; pure $ mkApp6 (mkConst `congrArg [u, v]) α β a b f h
| none, _ => throwEx $ Exception.appBuilder `congrArg "non-dependent function expected" #[f, h]
| _, none => throwEx $ Exception.appBuilder `congrArg "equality proof expected" #[f, h]
def mkCongrFun (h a : Expr) : MetaM Expr :=
do hType ← infer h;
match hType.eq? with
| some (ρ, f, g) => do
ρ ← whnfD ρ;
match ρ with
| Expr.forallE n α β _ => do
let β' := Lean.mkLambda n BinderInfo.default α β;
u ← getLevel α;
v ← getLevel (mkApp β' a);
pure $ mkApp6 (mkConst `congrFun [u, v]) α β' f g h a
| _ => throwEx $ Exception.appBuilder `congrFun "equality proof between functions expected" #[h, a]
| _ => throwEx $ Exception.appBuilder `congrFun "equality proof expected" #[h, a]
def mkCongr (h₁ h₂ : Expr) : MetaM Expr :=
do hType₁ ← infer h₁;
hType₂ ← infer h₂;
match hType₁.eq?, hType₂.eq? with
| some (ρ, f, g), some (α, a, b) => do
ρ ← whnfD ρ;
match ρ.arrow? with
| some (_, β) => do
u ← getLevel α;
v ← getLevel β;
pure $ mkApp8 (mkConst `congr [u, v]) α β f g a b h₁ h₂
| _ => throwEx $ Exception.appBuilder `congr "non-dependent function expected" #[h₁, h₂]
| _, _ => throwEx $ Exception.appBuilder `congr "equality proof expected" #[h₁, h₂]
private def mkAppMFinal (f : Expr) (args : Array Expr) (instMVars : Array MVarId) : MetaM Expr :=
do instMVars.forM $ fun mvarId => do {
mvarDecl ← getMVarDecl mvarId;
mvarVal ← synthInstance mvarDecl.type;
assignExprMVar mvarId mvarVal
};
result ← instantiateMVars (mkAppN f args);
whenM (hasAssignableMVar result) $ throwEx $ Exception.appBuilder `mkAppM "result contains metavariables" #[result];
pure result
private partial def mkAppMAux (f : Expr) (xs : Array Expr) : Nat → Array Expr → Nat → Array MVarId → Expr → MetaM Expr
| i, args, j, instMVars, Expr.forallE n d b c => do
let d := d.instantiateRevRange j args.size args;
match c.binderInfo with
| BinderInfo.implicit => do mvar ← mkFreshExprMVar d n; mkAppMAux i (args.push mvar) j instMVars b
| BinderInfo.instImplicit => do mvar ← mkFreshExprMVar d n true; mkAppMAux i (args.push mvar) j (instMVars.push mvar.mvarId!) b
| _ =>
if h : i < xs.size then do
let x := xs.get ⟨i, h⟩;
xType ← inferType x;
condM (isDefEq d xType)
(mkAppMAux (i+1) (args.push x) j instMVars b)
(throwEx $ Exception.appTypeMismatch (mkAppN f args) x)
else
mkAppMFinal f args instMVars
| i, args, j, instMVars, type => do
let type := type.instantiateRevRange j args.size args;
type ← whnfD type;
if type.isForall then
mkAppMAux i args args.size instMVars type
else if i == xs.size then
mkAppMFinal f args instMVars
else
throwEx $ Exception.appBuilder `mkAppM "too many explicit arguments provided" (#[f] ++ xs)
def mkAppM (constName : Name) (xs : Array Expr) : MetaM Expr :=
traceCtx `Meta.appBuilder $ withNewMCtxDepth $ do
cinfo ← getConstInfo constName;
us ← cinfo.lparams.mapM $ fun _ => mkFreshLevelMVar;
let f := mkConst constName us;
let fType := cinfo.instantiateTypeLevelParams us;
mkAppMAux f xs 0 #[] 0 #[] fType
end Meta
end Lean

19
stage0/src/Init/Lean/Meta/Basic.lean
View file

@ -5,9 +5,9 @@ Authors: Leonardo de Moura
-/
prelude
import Init.Control.Reader
import Init.Lean.NameGenerator
import Init.Lean.Data.LOption
import Init.Lean.Data.NameGenerator
import Init.Lean.Environment
import Init.Lean.LOption
import Init.Lean.Trace
import Init.Lean.Class
import Init.Lean.ReducibilityAttrs
@ -340,6 +340,12 @@ getConstAux constName true
@[inline] def getConstNoEx (constName : Name) : MetaM (Option ConstantInfo) :=
getConstAux constName false
def getConstInfo (constName : Name) : MetaM ConstantInfo :=
do env ← getEnv;
match env.find constName with
| some info => pure info
| none => throwEx $ Exception.unknownConst constName
def getLocalDecl (fvarId : FVarId) : MetaM LocalDecl :=
do lctx ← getLCtx;
match lctx.find fvarId with
@ -680,6 +686,8 @@ do mvarId ← mkFreshId;
def whnfUsingDefault : Expr → MetaM Expr :=
fun e => usingTransparency TransparencyMode.default $ whnf e
abbrev whnfD := whnfUsingDefault
/-- Execute `x` using approximate unification. -/
@[inline] def approxDefEq {α} (x : MetaM α) : MetaM α :=
adaptReader (fun (ctx : Context) => { config := { foApprox := true, ctxApprox := true, quasiPatternApprox := true, .. ctx.config }, .. ctx })
@ -691,7 +699,7 @@ do c? ← isClass fvarType;
| none => k fvar
| some c => withNewLocalInstance c fvar $ k fvar
@[inline] def withLocalDecl {α} (n : Name) (type : Expr) (bi : BinderInfo) (k : Expr → MetaM α) : MetaM α :=
def withLocalDecl {α} (n : Name) (type : Expr) (bi : BinderInfo) (k : Expr → MetaM α) : MetaM α :=
do fvarId ← mkFreshId;
ctx ← read;
let lctx := ctx.lctx.mkLocalDecl fvarId n type bi;
@ -699,7 +707,10 @@ do fvarId ← mkFreshId;
adaptReader (fun (ctx : Context) => { lctx := lctx, .. ctx }) $
withNewFVar fvar type k
@[inline] def withLetDecl {α} (n : Name) (type : Expr) (val : Expr) (k : Expr → MetaM α) : MetaM α :=
def withLocalDeclD {α} (n : Name) (type : Expr) (k : Expr → MetaM α) : MetaM α :=
withLocalDecl n type BinderInfo.default k
def withLetDecl {α} (n : Name) (type : Expr) (val : Expr) (k : Expr → MetaM α) : MetaM α :=
do fvarId ← mkFreshId;
ctx ← read;
let lctx := ctx.lctx.mkLetDecl fvarId n type val;

6
stage0/src/Init/Lean/Meta/Exception.lean
View file

@ -34,6 +34,8 @@ inductive Exception
| letTypeMismatch (fvarId : FVarId) (ctx : ExceptionContext)
| appTypeMismatch (f a : Expr) (ctx : ExceptionContext)
| notInstance (e : Expr) (ctx : ExceptionContext)
| appBuilder (op : Name) (msg : String) (args : Array Expr) (ctx : ExceptionContext)
| synthInstance (inst : Expr) (ctx : ExceptionContext)
| bug (b : Bug) (ctx : ExceptionContext)
| other (msg : String)
@ -58,6 +60,8 @@ def toStr : Exception → String
| letTypeMismatch _ _ => "type mismatch at let-expression"
| appTypeMismatch _ _ _ => "application type mismatch"
| notInstance _ _ => "type class instance expected"
| appBuilder _ _ _ _ => "application builder failure"
| synthInstance _ _ => "type class instance synthesis failed"
| bug _ _ => "bug"
| other s => s
@ -83,6 +87,8 @@ def toMessageData : Exception → MessageData
| letTypeMismatch fvarId ctx => mkCtx ctx $ `letTypeMismatch ++ " " ++ mkFVar fvarId
| appTypeMismatch f a ctx => mkCtx ctx $ `appTypeMismatch ++ " " ++ mkApp f a
| notInstance i ctx => mkCtx ctx $ `notInstance ++ " " ++ i
| appBuilder op msg args ctx => mkCtx ctx $ `appBuilder ++ " " ++ op ++ " " ++ args ++ " " ++ msg
| synthInstance inst ctx => mkCtx ctx $ `synthInstance ++ " " ++ inst
| bug _ _ => "internal bug" -- TODO improve
| other s => s

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

@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
prelude
import Init.Lean.LBool
import Init.Lean.Data.LBool
import Init.Lean.Meta.Basic
namespace Lean
@ -69,7 +69,7 @@ do let failed : Unit → MetaM Expr := fun _ => throwEx $ Exception.invalidProje
def getLevel (type : Expr) : MetaM Level :=
do typeType ← inferType type;
typeType ← whnf typeType;
typeType ← whnfUsingDefault typeType;
match typeType with
| Expr.sort lvl _ => pure lvl
| Expr.mvar mvarId _ =>

6
stage0/src/Init/Lean/Meta/Offset.lean
View file

@ -4,7 +4,7 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
prelude
import Init.Lean.LBool
import Init.Lean.Data.LBool
import Init.Lean.Meta.InferType
namespace Lean
@ -95,8 +95,8 @@ match isOffset s with
| some (s, k₁) => match isOffset t with
| some (t, k₂) => -- s+k₁ =?= t+k₂
if k₁ == k₂ then isDefEq s t
else if k₁ < k₂ then isDefEq s (mkCAppB `Nat.add t (mkNatLit $ k₂ - k₁))
else isDefEq (mkCAppB `Nat.add s (mkNatLit $ k₁ - k₂)) t
else if k₁ < k₂ then isDefEq s (mkAppB (mkConst `Nat.add) t (mkNatLit $ k₂ - k₁))
else isDefEq (mkAppB (mkConst `Nat.add) s (mkNatLit $ k₁ - k₂)) t
| none => match evalNat t with
| some v₂ => -- s+k₁ =?= v₂
if v₂ ≥ k₁ then isDefEq s (mkNatLit $ v₂ - k₁) else pure LBool.false

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

@ -509,7 +509,7 @@ try $
<&&>
r.exprReplacements.allM (fun ⟨e, e'⟩ => isExprDefEqAux e e')
def synthInstance (type : Expr) (fuel : Nat := 10000) : MetaM (Option Expr) :=
def synthInstance? (type : Expr) (fuel : Nat := 10000) : MetaM (Option Expr) :=
usingTransparency TransparencyMode.reducible $ do
type ← instantiateMVars type;
type ← preprocess type;
@ -530,10 +530,10 @@ usingTransparency TransparencyMode.reducible $ do
(pure (some result)))
(pure none)
};
if type.hasMVar then do
modify $ fun s => { cache := { synthInstance := s.cache.synthInstance.insert type result, .. s.cache }, .. s };
if type.hasMVar then
pure result
else
else do
modify $ fun s => { cache := { synthInstance := s.cache.synthInstance.insert type result, .. s.cache }, .. s };
pure result
/--
@ -542,11 +542,17 @@ usingTransparency TransparencyMode.reducible $ do
def trySynthInstance (type : Expr) (fuel : Nat := 10000) : MetaM (LOption Expr) :=
adaptReader (fun (ctx : Context) => { config := { isDefEqStuckEx := true, .. ctx.config }, .. ctx }) $
catch
(toLOptionM $ synthInstance type fuel)
(toLOptionM $ synthInstance? type fuel)
(fun ex => match ex with
| Exception.isExprDefEqStuck _ _ _ => pure LOption.undef
| Exception.isLevelDefEqStuck _ _ _ => pure LOption.undef
| _ => throw ex)
def synthInstance (type : Expr) (fuel : Nat := 10000) : MetaM Expr :=
do result? ← synthInstance? type fuel;
match result? with
| some result => pure result
| none => throwEx $ Exception.synthInstance type
end Meta
end Lean

4
stage0/src/Init/Lean/MetavarContext.lean
View file

@ -4,12 +4,12 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura
-/
prelude
import Init.Control.Reader
import Init.Data.Nat
import Init.Data.Option
import Init.Control.Reader
import Init.Lean.Data.NameGenerator
import Init.Lean.LocalContext
import Init.Lean.MonadCache
import Init.Lean.NameGenerator
namespace Lean

6
stage0/src/Init/Lean/Parser/Parser.lean
View file

@ -4,13 +4,13 @@ Released under Apache 2.0 license as described in the file LICENSE.
Authors: Leonardo de Moura, Sebastian Ullrich
-/
prelude
import Init.Lean.Position
import Init.Lean.Data.Trie
import Init.Lean.Data.Position
import Init.Lean.Syntax
import Init.Lean.ToExpr
import Init.Lean.Message
import Init.Lean.Environment
import Init.Lean.Attributes
import Init.Lean.Parser.Trie
import Init.Lean.Parser.Identifier
import Init.Lean.Compiler.InitAttr
@ -1443,7 +1443,7 @@ do tables ← tablesRef.get;
def declareBuiltinParser (env : Environment) (addFnName : Name) (refDeclName : Name) (declName : Name) : IO Environment :=
let name := `_regBuiltinParser ++ declName;
let type := mkApp (mkConst `IO) (mkConst `Unit);
let val := mkCAppN addFnName #[mkConst refDeclName, toExpr declName, mkConst declName];
let val := mkAppN (mkConst addFnName) #[mkConst refDeclName, toExpr declName, mkConst declName];
let decl := Declaration.defnDecl { name := name, lparams := [], type := type, value := val, hints := ReducibilityHints.opaque, isUnsafe := false };
match env.addAndCompile {} decl with
-- TODO: pretty print error

2
stage0/src/Init/Lean/Path.lean
View file

@ -15,9 +15,9 @@ import Init.System.IO
import Init.System.FilePath
import Init.Data.Array
import Init.Data.List.Control
import Init.Lean.Name
import Init.Data.HashMap
import Init.Data.Nat.Control
import Init.Lean.Data.Name
namespace Lean
open System.FilePath (pathSeparator extSeparator)

4
stage0/src/Init/Lean/Syntax.lean
View file

@ -4,9 +4,9 @@ Released under Apache 2.0 license as described in the file LICENSE.
Author: Sebastian Ullrich, Leonardo de Moura
-/
prelude
import Init.Lean.Name
import Init.Lean.Format
import Init.Data.Array
import Init.Lean.Data.Name
import Init.Lean.Data.Format
namespace Lean
structure SourceInfo :=

4
stage0/src/Init/Lean/ToExpr.lean
View file

@ -22,8 +22,8 @@ instance strToExpr : ToExpr String := ⟨mkStrLit⟩
def nameToExprAux : Name → Expr
| Name.anonymous => mkConst `Lean.Name.anonymous
| Name.str p s _ => mkCAppB `Lean.mkNameStr (nameToExprAux p) (toExpr s)
| Name.num p n _ => mkCAppB `Lean.mkNameNum (nameToExprAux p) (toExpr n)
| Name.str p s _ => mkAppB (mkConst `Lean.mkNameStr) (nameToExprAux p) (toExpr s)
| Name.num p n _ => mkAppB (mkConst `Lean.mkNameNum) (nameToExprAux p) (toExpr n)
instance nameToExpr : ToExpr Name := ⟨nameToExprAux⟩

2
stage0/src/Init/Lean/Util.lean
View file

@ -5,7 +5,7 @@ Author: Sebastian Ullrich
-/
prelude
import Init.System.IO
import Init.Lean.Position
import Init.Lean.Data.Position
namespace Lean

4
stage0/src/Init/WF.lean
View file

@ -233,13 +233,13 @@ Acc.ndrecOn aca $ fun (xa aca) (iha : ∀ y, r y xa → ∀ (b : β y), Acc (Lex
(∀ (y : β xa), s xa y xb → Acc (Lex r s) ⟨xa, y⟩) →
Lex r s p ⟨xa, xb⟩ → ∀ (b₁ : β a), s a b₁ b₂ → b₂ ≅ xb → Acc (Lex r s) ⟨a, b₁⟩
from Eq.subst Eq₂ $ fun xb acb ihb lt b₁ h Eq₃ =>
have newEq₃ : b₂ = xb from eqOfHeq Eq₃;
have newEq₃ : b₂ = xb from eqOfHEq Eq₃;
have aux : (∀ (y : β a), s a y xb → Acc (Lex r s) ⟨a, y⟩) →
∀ (b₁ : β a), s a b₁ b₂ → Acc (Lex r s) ⟨a, b₁⟩
from Eq.subst newEq₃ (fun ihb b₁ h => ihb b₁ h);
aux ihb b₁ h;
aux xb acb ihb lt b₁ h Eq₃);
aux rfl (Heq.refl xb)
aux rfl (HEq.refl xb)
-- The lexicographical order of well founded relations is well-founded
def lexWf (ha : WellFounded r) (hb : ∀ x, WellFounded (s x)) : WellFounded (Lex r s) :=

2
stage0/stdlib/CMakeLists.txt
View file

@ -1 +1 @@
add_library (stage0 OBJECT Init/./Coe.c Init/./Control.c Init/./Control/Alternative.c Init/./Control/Applicative.c Init/./Control/Conditional.c Init/./Control/EState.c Init/./Control/Except.c Init/./Control/Functor.c Init/./Control/Id.c Init/./Control/Lift.c Init/./Control/Monad.c Init/./Control/MonadFail.c Init/./Control/Option.c Init/./Control/Reader.c Init/./Control/State.c Init/./Core.c Init/./Data.c Init/./Data/Array.c Init/./Data/Array/Basic.c Init/./Data/Array/BinSearch.c Init/./Data/Array/QSort.c Init/./Data/AssocList.c Init/./Data/Basic.c Init/./Data/BinomialHeap.c Init/./Data/BinomialHeap/Basic.c Init/./Data/ByteArray.c Init/./Data/ByteArray/Basic.c Init/./Data/Char.c Init/./Data/Char/Basic.c Init/./Data/DList.c Init/./Data/Fin.c Init/./Data/Fin/Basic.c Init/./Data/HashMap.c Init/./Data/HashMap/Basic.c Init/./Data/HashSet.c Init/./Data/Hashable.c Init/./Data/Int.c Init/./Data/Int/Basic.c Init/./Data/List.c Init/./Data/List/Basic.c Init/./Data/List/BasicAux.c Init/./Data/List/Control.c Init/./Data/List/Instances.c Init/./Data/Nat.c Init/./Data/Nat/Basic.c Init/./Data/Nat/Bitwise.c Init/./Data/Nat/Control.c Init/./Data/Nat/Div.c Init/./Data/Option.c Init/./Data/Option/Basic.c Init/./Data/Option/BasicAux.c Init/./Data/Option/Instances.c Init/./Data/PersistentArray.c Init/./Data/PersistentArray/Basic.c Init/./Data/PersistentHashMap.c Init/./Data/PersistentHashMap/Basic.c Init/./Data/PersistentHashSet.c Init/./Data/Queue.c Init/./Data/Queue/Basic.c Init/./Data/RBMap.c Init/./Data/RBMap/Basic.c Init/./Data/RBMap/BasicAux.c Init/./Data/RBTree.c Init/./Data/RBTree/Basic.c Init/./Data/Random.c Init/./Data/Repr.c Init/./Data/Stack.c Init/./Data/Stack/Basic.c Init/./Data/String.c Init/./Data/String/Basic.c Init/./Data/ToString.c Init/./Data/UInt.c Init/./Default.c Init/./Fix.c Init/./Lean.c Init/./Lean/Attributes.c Init/./Lean/AuxRecursor.c Init/./Lean/Class.c Init/./Lean/Compiler.c Init/./Lean/Compiler/ClosedTermCache.c Init/./Lean/Compiler/ConstFolding.c Init/./Lean/Compiler/ExportAttr.c Init/./Lean/Compiler/ExternAttr.c Init/./Lean/Compiler/IR.c Init/./Lean/Compiler/IR/Basic.c Init/./Lean/Compiler/IR/Borrow.c Init/./Lean/Compiler/IR/Boxing.c Init/./Lean/Compiler/IR/Checker.c Init/./Lean/Compiler/IR/CompilerM.c Init/./Lean/Compiler/IR/CtorLayout.c Init/./Lean/Compiler/IR/ElimDeadBranches.c Init/./Lean/Compiler/IR/ElimDeadVars.c Init/./Lean/Compiler/IR/EmitC.c Init/./Lean/Compiler/IR/EmitUtil.c Init/./Lean/Compiler/IR/ExpandResetReuse.c Init/./Lean/Compiler/IR/Format.c Init/./Lean/Compiler/IR/FreeVars.c Init/./Lean/Compiler/IR/LiveVars.c Init/./Lean/Compiler/IR/NormIds.c Init/./Lean/Compiler/IR/PushProj.c Init/./Lean/Compiler/IR/RC.c Init/./Lean/Compiler/IR/ResetReuse.c Init/./Lean/Compiler/IR/SimpCase.c Init/./Lean/Compiler/IR/UnboxResult.c Init/./Lean/Compiler/ImplementedByAttr.c Init/./Lean/Compiler/InitAttr.c Init/./Lean/Compiler/InlineAttrs.c Init/./Lean/Compiler/NameMangling.c Init/./Lean/Compiler/NeverExtractAttr.c Init/./Lean/Compiler/Specialize.c Init/./Lean/Compiler/Util.c Init/./Lean/Declaration.c Init/./Lean/Elaborator.c Init/./Lean/Elaborator/Alias.c Init/./Lean/Elaborator/Basic.c Init/./Lean/Elaborator/Command.c Init/./Lean/Elaborator/ElabStrategyAttrs.c Init/./Lean/Elaborator/PreTerm.c Init/./Lean/Elaborator/ResolveName.c Init/./Lean/Elaborator/Term.c Init/./Lean/Environment.c Init/./Lean/EqnCompiler.c Init/./Lean/EqnCompiler/MatchPattern.c Init/./Lean/Expr.c Init/./Lean/Format.c Init/./Lean/KVMap.c Init/./Lean/LBool.c Init/./Lean/LOption.c Init/./Lean/Level.c Init/./Lean/Linter.c Init/./Lean/LocalContext.c Init/./Lean/Message.c Init/./Lean/Meta.c Init/./Lean/Meta/AbstractMVars.c Init/./Lean/Meta/AppBuilder.c Init/./Lean/Meta/Basic.c Init/./Lean/Meta/Check.c Init/./Lean/Meta/DiscrTree.c Init/./Lean/Meta/DiscrTreeTypes.c Init/./Lean/Meta/Exception.c Init/./Lean/Meta/ExprDefEq.c Init/./Lean/Meta/FunInfo.c Init/./Lean/Meta/InferType.c Init/./Lean/Meta/Instances.c Init/./Lean/Meta/LevelDefEq.c Init/./Lean/Meta/Offset.c Init/./Lean/Meta/Reduce.c Init/./Lean/Meta/SynthInstance.c Init/./Lean/Meta/WHNF.c Init/./Lean/MetavarContext.c Init/./Lean/Modifiers.c Init/./Lean/MonadCache.c Init/./Lean/Name.c Init/./Lean/NameGenerator.c Init/./Lean/Options.c Init/./Lean/Parser.c Init/./Lean/Parser/Command.c Init/./Lean/Parser/Identifier.c Init/./Lean/Parser/Level.c Init/./Lean/Parser/Module.c Init/./Lean/Parser/Parser.c Init/./Lean/Parser/Term.c Init/./Lean/Parser/Transform.c Init/./Lean/Parser/Trie.c Init/./Lean/Path.c Init/./Lean/Position.c Init/./Lean/ProjFns.c Init/./Lean/ReducibilityAttrs.c Init/./Lean/Runtime.c Init/./Lean/SMap.c Init/./Lean/Scopes.c Init/./Lean/Syntax.c Init/./Lean/ToExpr.c Init/./Lean/Trace.c Init/./Lean/Util.c Init/./Lean/WHNF.c Init/./System.c Init/./System/FilePath.c Init/./System/IO.c Init/./System/Platform.c Init/./Util.c Init/./WF.c)
add_library (stage0 OBJECT Init/./Coe.c Init/./Control.c Init/./Control/Alternative.c Init/./Control/Applicative.c Init/./Control/Conditional.c Init/./Control/EState.c Init/./Control/Except.c Init/./Control/Functor.c Init/./Control/Id.c Init/./Control/Lift.c Init/./Control/Monad.c Init/./Control/MonadFail.c Init/./Control/Option.c Init/./Control/Reader.c Init/./Control/State.c Init/./Core.c Init/./Data.c Init/./Data/Array.c Init/./Data/Array/Basic.c Init/./Data/Array/BinSearch.c Init/./Data/Array/QSort.c Init/./Data/AssocList.c Init/./Data/Basic.c Init/./Data/BinomialHeap.c Init/./Data/BinomialHeap/Basic.c Init/./Data/ByteArray.c Init/./Data/ByteArray/Basic.c Init/./Data/Char.c Init/./Data/Char/Basic.c Init/./Data/DList.c Init/./Data/Fin.c Init/./Data/Fin/Basic.c Init/./Data/HashMap.c Init/./Data/HashMap/Basic.c Init/./Data/HashSet.c Init/./Data/Hashable.c Init/./Data/Int.c Init/./Data/Int/Basic.c Init/./Data/List.c Init/./Data/List/Basic.c Init/./Data/List/BasicAux.c Init/./Data/List/Control.c Init/./Data/List/Instances.c Init/./Data/Nat.c Init/./Data/Nat/Basic.c Init/./Data/Nat/Bitwise.c Init/./Data/Nat/Control.c Init/./Data/Nat/Div.c Init/./Data/Option.c Init/./Data/Option/Basic.c Init/./Data/Option/BasicAux.c Init/./Data/Option/Instances.c Init/./Data/PersistentArray.c Init/./Data/PersistentArray/Basic.c Init/./Data/PersistentHashMap.c Init/./Data/PersistentHashMap/Basic.c Init/./Data/PersistentHashSet.c Init/./Data/Queue.c Init/./Data/Queue/Basic.c Init/./Data/RBMap.c Init/./Data/RBMap/Basic.c Init/./Data/RBMap/BasicAux.c Init/./Data/RBTree.c Init/./Data/RBTree/Basic.c Init/./Data/Random.c Init/./Data/Repr.c Init/./Data/Stack.c Init/./Data/Stack/Basic.c Init/./Data/String.c Init/./Data/String/Basic.c Init/./Data/ToString.c Init/./Data/UInt.c Init/./Default.c Init/./Fix.c Init/./Lean.c Init/./Lean/Attributes.c Init/./Lean/AuxRecursor.c Init/./Lean/Class.c Init/./Lean/Compiler.c Init/./Lean/Compiler/ClosedTermCache.c Init/./Lean/Compiler/ConstFolding.c Init/./Lean/Compiler/ExportAttr.c Init/./Lean/Compiler/ExternAttr.c Init/./Lean/Compiler/IR.c Init/./Lean/Compiler/IR/Basic.c Init/./Lean/Compiler/IR/Borrow.c Init/./Lean/Compiler/IR/Boxing.c Init/./Lean/Compiler/IR/Checker.c Init/./Lean/Compiler/IR/CompilerM.c Init/./Lean/Compiler/IR/CtorLayout.c Init/./Lean/Compiler/IR/ElimDeadBranches.c Init/./Lean/Compiler/IR/ElimDeadVars.c Init/./Lean/Compiler/IR/EmitC.c Init/./Lean/Compiler/IR/EmitUtil.c Init/./Lean/Compiler/IR/ExpandResetReuse.c Init/./Lean/Compiler/IR/Format.c Init/./Lean/Compiler/IR/FreeVars.c Init/./Lean/Compiler/IR/LiveVars.c Init/./Lean/Compiler/IR/NormIds.c Init/./Lean/Compiler/IR/PushProj.c Init/./Lean/Compiler/IR/RC.c Init/./Lean/Compiler/IR/ResetReuse.c Init/./Lean/Compiler/IR/SimpCase.c Init/./Lean/Compiler/IR/UnboxResult.c Init/./Lean/Compiler/ImplementedByAttr.c Init/./Lean/Compiler/InitAttr.c Init/./Lean/Compiler/InlineAttrs.c Init/./Lean/Compiler/NameMangling.c Init/./Lean/Compiler/NeverExtractAttr.c Init/./Lean/Compiler/Specialize.c Init/./Lean/Compiler/Util.c Init/./Lean/Data/Format.c Init/./Lean/Data/KVMap.c Init/./Lean/Data/LBool.c Init/./Lean/Data/LOption.c Init/./Lean/Data/Name.c Init/./Lean/Data/NameGenerator.c Init/./Lean/Data/Options.c Init/./Lean/Data/Position.c Init/./Lean/Data/SMap.c Init/./Lean/Data/Trie.c Init/./Lean/Declaration.c Init/./Lean/Elaborator.c Init/./Lean/Elaborator/Alias.c Init/./Lean/Elaborator/Basic.c Init/./Lean/Elaborator/Command.c Init/./Lean/Elaborator/ElabStrategyAttrs.c Init/./Lean/Elaborator/PreTerm.c Init/./Lean/Elaborator/ResolveName.c Init/./Lean/Elaborator/Term.c Init/./Lean/Environment.c Init/./Lean/EqnCompiler.c Init/./Lean/EqnCompiler/MatchPattern.c Init/./Lean/Expr.c Init/./Lean/Level.c Init/./Lean/Linter.c Init/./Lean/LocalContext.c Init/./Lean/Message.c Init/./Lean/Meta.c Init/./Lean/Meta/AbstractMVars.c Init/./Lean/Meta/AppBuilder.c Init/./Lean/Meta/Basic.c Init/./Lean/Meta/Check.c Init/./Lean/Meta/DiscrTree.c Init/./Lean/Meta/DiscrTreeTypes.c Init/./Lean/Meta/Exception.c Init/./Lean/Meta/ExprDefEq.c Init/./Lean/Meta/FunInfo.c Init/./Lean/Meta/InferType.c Init/./Lean/Meta/Instances.c Init/./Lean/Meta/LevelDefEq.c Init/./Lean/Meta/Offset.c Init/./Lean/Meta/Reduce.c Init/./Lean/Meta/SynthInstance.c Init/./Lean/Meta/WHNF.c Init/./Lean/MetavarContext.c Init/./Lean/Modifiers.c Init/./Lean/MonadCache.c Init/./Lean/Parser.c Init/./Lean/Parser/Command.c Init/./Lean/Parser/Identifier.c Init/./Lean/Parser/Level.c Init/./Lean/Parser/Module.c Init/./Lean/Parser/Parser.c Init/./Lean/Parser/Term.c Init/./Lean/Parser/Transform.c Init/./Lean/Path.c Init/./Lean/ProjFns.c Init/./Lean/ReducibilityAttrs.c Init/./Lean/Runtime.c Init/./Lean/Scopes.c Init/./Lean/Syntax.c Init/./Lean/ToExpr.c Init/./Lean/Trace.c Init/./Lean/Util.c Init/./Lean/WHNF.c Init/./System.c Init/./System/FilePath.c Init/./System/IO.c Init/./System/Platform.c Init/./Util.c Init/./WF.c)

14
stage0/stdlib/Init/Lean/Compiler/IR/Basic.c
View file

@ -1,6 +1,6 @@
// Lean compiler output
// Module: Init.Lean.Compiler.IR.Basic
// Imports: Init.Data.Array Init.Lean.Name Init.Lean.KVMap Init.Lean.Format Init.Lean.Compiler.ExternAttr
// Imports: Init.Data.Array Init.Lean.Data.KVMap Init.Lean.Data.Name Init.Lean.Data.Format Init.Lean.Compiler.ExternAttr
#include "runtime/lean.h"
#if defined(__clang__)
#pragma clang diagnostic ignored "-Wunused-parameter"
@ -13293,9 +13293,9 @@ return x_13;
}
}
lean_object* initialize_Init_Data_Array(lean_object*);
lean_object* initialize_Init_Lean_Name(lean_object*);
lean_object* initialize_Init_Lean_KVMap(lean_object*);
lean_object* initialize_Init_Lean_Format(lean_object*);
lean_object* initialize_Init_Lean_Data_KVMap(lean_object*);
lean_object* initialize_Init_Lean_Data_Name(lean_object*);
lean_object* initialize_Init_Lean_Data_Format(lean_object*);
lean_object* initialize_Init_Lean_Compiler_ExternAttr(lean_object*);
static bool _G_initialized = false;
lean_object* initialize_Init_Lean_Compiler_IR_Basic(lean_object* w) {
@ -13305,13 +13305,13 @@ _G_initialized = true;
res = initialize_Init_Data_Array(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Init_Lean_Name(lean_io_mk_world());
res = initialize_Init_Lean_Data_KVMap(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Init_Lean_KVMap(lean_io_mk_world());
res = initialize_Init_Lean_Data_Name(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Init_Lean_Format(lean_io_mk_world());
res = initialize_Init_Lean_Data_Format(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Init_Lean_Compiler_ExternAttr(lean_io_mk_world());

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

@ -13,6 +13,7 @@
#ifdef __cplusplus
extern "C" {
#endif
extern lean_object* l_Lean_Name_toString___closed__1;
lean_object* l_Lean_IR_UnreachableBranches_functionSummariesExt___closed__3;
lean_object* l_Nat_foldMAux___main___at_Lean_IR_UnreachableBranches_inferStep___spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
size_t l_USize_add(size_t, size_t);
@ -297,7 +298,6 @@ 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*);
lean_object* l_Lean_IR_UnreachableBranches_functionSummariesExt___elambda__4(lean_object*);
extern lean_object* l_System_FilePath_dirName___closed__1;
lean_object* l_AssocList_find___main___at_Lean_IR_UnreachableBranches_findVarValue___spec__2___boxed(lean_object*, lean_object*);
lean_object* l_unsafeCast(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Name_toStringWithSep___main(lean_object*, lean_object*);
@ -3410,7 +3410,7 @@ lean_object* x_53; lean_object* x_54; lean_object* x_55; lean_object* x_56; lean
x_53 = lean_ctor_get(x_1, 0);
lean_inc(x_53);
lean_dec(x_1);
x_54 = l_System_FilePath_dirName___closed__1;
x_54 = l_Lean_Name_toString___closed__1;
x_55 = l_Lean_Name_toStringWithSep___main(x_54, x_53);
x_56 = l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__3;
x_57 = lean_string_append(x_56, x_55);
@ -3627,7 +3627,7 @@ lean_object* x_106; lean_object* x_107; lean_object* x_108; lean_object* x_109;
x_106 = lean_ctor_get(x_1, 0);
lean_inc(x_106);
lean_dec(x_1);
x_107 = l_System_FilePath_dirName___closed__1;
x_107 = l_Lean_Name_toString___closed__1;
x_108 = l_Lean_Name_toStringWithSep___main(x_107, x_106);
x_109 = l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__3;
x_110 = lean_string_append(x_109, x_108);

28
stage0/stdlib/Init/Lean/Compiler/IR/Format.c
View file

@ -1,6 +1,6 @@
// Lean compiler output
// Module: Init.Lean.Compiler.IR.Format
// Imports: Init.Lean.Compiler.IR.Basic Init.Lean.Format
// Imports: Init.Lean.Data.Format Init.Lean.Compiler.IR.Basic
#include "runtime/lean.h"
#if defined(__clang__)
#pragma clang diagnostic ignored "-Wunused-parameter"
@ -14,6 +14,7 @@
extern "C" {
#endif
lean_object* l_Lean_IR_litValHasFormat___closed__1;
extern lean_object* l_Lean_Name_toString___closed__1;
lean_object* l_Lean_IR_formatFnBodyHead___closed__15;
lean_object* l_Lean_IR_formatFnBody___main___closed__6;
lean_object* l_Lean_IR_formatFnBodyHead___closed__3;
@ -185,7 +186,6 @@ lean_object* l___private_Init_Lean_Compiler_IR_Format_4__formatExpr___closed__16
extern lean_object* l_Lean_Format_paren___closed__3;
lean_object* l___private_Init_Lean_Compiler_IR_Format_5__formatIRType___main(lean_object*);
lean_object* l_Lean_IR_formatFnBodyHead___closed__4;
extern lean_object* l_System_FilePath_dirName___closed__1;
lean_object* l_Lean_Name_toStringWithSep___main(lean_object*, lean_object*);
lean_object* l_Lean_IR_exprHasFormat;
lean_object* l_Lean_IR_fnBodyHasFormat___closed__1;
@ -421,7 +421,7 @@ lean_object* _init_l___private_Init_Lean_Compiler_IR_Format_3__formatCtorInfo___
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_System_FilePath_dirName___closed__1;
x_1 = l_Lean_Name_toString___closed__1;
x_2 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
@ -469,7 +469,7 @@ x_17 = lean_alloc_ctor(4, 2, 1);
lean_ctor_set(x_17, 0, x_10);
lean_ctor_set(x_17, 1, x_16);
lean_ctor_set_uint8(x_17, sizeof(void*)*2, x_8);
x_18 = l_System_FilePath_dirName___closed__1;
x_18 = l_Lean_Name_toString___closed__1;
x_19 = l_Lean_Name_toStringWithSep___main(x_18, x_2);
x_20 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_20, 0, x_19);
@ -524,7 +524,7 @@ x_34 = lean_alloc_ctor(4, 2, 1);
lean_ctor_set(x_34, 0, x_32);
lean_ctor_set(x_34, 1, x_33);
lean_ctor_set_uint8(x_34, sizeof(void*)*2, x_8);
x_35 = l_System_FilePath_dirName___closed__1;
x_35 = l_Lean_Name_toString___closed__1;
x_36 = l_Lean_Name_toStringWithSep___main(x_35, x_2);
x_37 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_37, 0, x_36);
@ -580,7 +580,7 @@ x_51 = lean_alloc_ctor(4, 2, 1);
lean_ctor_set(x_51, 0, x_49);
lean_ctor_set(x_51, 1, x_50);
lean_ctor_set_uint8(x_51, sizeof(void*)*2, x_8);
x_52 = l_System_FilePath_dirName___closed__1;
x_52 = l_Lean_Name_toString___closed__1;
x_53 = l_Lean_Name_toStringWithSep___main(x_52, x_2);
x_54 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_54, 0, x_53);
@ -1226,7 +1226,7 @@ lean_inc(x_98);
x_99 = lean_ctor_get(x_1, 1);
lean_inc(x_99);
lean_dec(x_1);
x_100 = l_System_FilePath_dirName___closed__1;
x_100 = l_Lean_Name_toString___closed__1;
x_101 = l_Lean_Name_toStringWithSep___main(x_100, x_98);
x_102 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_102, 0, x_101);
@ -1249,7 +1249,7 @@ lean_inc(x_108);
x_109 = lean_ctor_get(x_1, 1);
lean_inc(x_109);
lean_dec(x_1);
x_110 = l_System_FilePath_dirName___closed__1;
x_110 = l_Lean_Name_toString___closed__1;
x_111 = l_Lean_Name_toStringWithSep___main(x_110, x_108);
x_112 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_112, 0, x_111);
@ -2033,7 +2033,7 @@ lean_dec(x_3);
x_6 = lean_ctor_get(x_4, 0);
lean_inc(x_6);
lean_dec(x_4);
x_7 = l_System_FilePath_dirName___closed__1;
x_7 = l_Lean_Name_toString___closed__1;
x_8 = l_Lean_Name_toStringWithSep___main(x_7, x_6);
x_9 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_9, 0, x_8);
@ -4030,7 +4030,7 @@ lean_inc(x_5);
x_6 = lean_ctor_get(x_2, 3);
lean_inc(x_6);
lean_dec(x_2);
x_7 = l_System_FilePath_dirName___closed__1;
x_7 = l_Lean_Name_toString___closed__1;
x_8 = l_Lean_Name_toStringWithSep___main(x_7, x_3);
x_9 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_9, 0, x_8);
@ -4091,7 +4091,7 @@ lean_inc(x_29);
x_30 = lean_ctor_get(x_2, 2);
lean_inc(x_30);
lean_dec(x_2);
x_31 = l_System_FilePath_dirName___closed__1;
x_31 = l_Lean_Name_toString___closed__1;
x_32 = l_Lean_Name_toStringWithSep___main(x_31, x_28);
x_33 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_33, 0, x_32);
@ -4169,17 +4169,17 @@ x_1 = l_Lean_IR_declHasToString___closed__1;
return x_1;
}
}
lean_object* initialize_Init_Lean_Data_Format(lean_object*);
lean_object* initialize_Init_Lean_Compiler_IR_Basic(lean_object*);
lean_object* initialize_Init_Lean_Format(lean_object*);
static bool _G_initialized = false;
lean_object* initialize_Init_Lean_Compiler_IR_Format(lean_object* w) {
lean_object * res;
if (_G_initialized) return lean_mk_io_result(lean_box(0));
_G_initialized = true;
res = initialize_Init_Lean_Compiler_IR_Basic(lean_io_mk_world());
res = initialize_Init_Lean_Data_Format(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Init_Lean_Format(lean_io_mk_world());
res = initialize_Init_Lean_Compiler_IR_Basic(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l___private_Init_Lean_Compiler_IR_Format_1__formatArg___closed__1 = _init_l___private_Init_Lean_Compiler_IR_Format_1__formatArg___closed__1();

6
stage0/stdlib/Init/Lean/Compiler/IR/UnboxResult.c
View file

@ -1,6 +1,6 @@
// Lean compiler output
// Module: Init.Lean.Compiler.IR.UnboxResult
// Imports: Init.Lean.Format Init.Lean.Compiler.IR.Basic Init.Lean.Compiler.IR.CtorLayout
// Imports: Init.Lean.Data.Format Init.Lean.Compiler.IR.Basic Init.Lean.Compiler.IR.CtorLayout
#include "runtime/lean.h"
#if defined(__clang__)
#pragma clang diagnostic ignored "-Wunused-parameter"
@ -211,7 +211,7 @@ x_4 = lean_box(x_3);
return x_4;
}
}
lean_object* initialize_Init_Lean_Format(lean_object*);
lean_object* initialize_Init_Lean_Data_Format(lean_object*);
lean_object* initialize_Init_Lean_Compiler_IR_Basic(lean_object*);
lean_object* initialize_Init_Lean_Compiler_IR_CtorLayout(lean_object*);
static bool _G_initialized = false;
@ -219,7 +219,7 @@ lean_object* initialize_Init_Lean_Compiler_IR_UnboxResult(lean_object* w) {
lean_object * res;
if (_G_initialized) return lean_mk_io_result(lean_box(0));
_G_initialized = true;
res = initialize_Init_Lean_Format(lean_io_mk_world());
res = initialize_Init_Lean_Data_Format(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Init_Lean_Compiler_IR_Basic(lean_io_mk_world());

6
stage0/stdlib/Init/Lean/Compiler/NameMangling.c
View file

@ -1,6 +1,6 @@
// Lean compiler output
// Module: Init.Lean.Compiler.NameMangling
// Imports: Init.Lean.Name
// Imports: Init.Lean.Data.Name
#include "runtime/lean.h"
#if defined(__clang__)
#pragma clang diagnostic ignored "-Wunused-parameter"
@ -294,13 +294,13 @@ lean_dec(x_3);
return x_4;
}
}
lean_object* initialize_Init_Lean_Name(lean_object*);
lean_object* initialize_Init_Lean_Data_Name(lean_object*);
static bool _G_initialized = false;
lean_object* initialize_Init_Lean_Compiler_NameMangling(lean_object* w) {
lean_object * res;
if (_G_initialized) return lean_mk_io_result(lean_box(0));
_G_initialized = true;
res = initialize_Init_Lean_Name(lean_io_mk_world());
res = initialize_Init_Lean_Data_Name(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l___private_Init_Lean_Compiler_NameMangling_1__String_mangleAux___main___closed__1 = _init_l___private_Init_Lean_Compiler_NameMangling_1__String_mangleAux___main___closed__1();

3629
stage0/stdlib/Init/Lean/Data/Format.c Normal file
View file

File diff suppressed because it is too large Load diff

14
stage0/stdlib/Init/Lean/KVMap.c → stage0/stdlib/Init/Lean/Data/KVMap.c
View file

@ -1,6 +1,6 @@
// Lean compiler output
// Module: Init.Lean.KVMap
// Imports: Init.Lean.Name Init.Data.Option.Basic Init.Data.Int
// Module: Init.Lean.Data.KVMap
// Imports: Init.Data.Option.Basic Init.Data.Int Init.Lean.Data.Name
#include "runtime/lean.h"
#if defined(__clang__)
#pragma clang diagnostic ignored "-Wunused-parameter"
@ -1192,23 +1192,23 @@ x_1 = l_Lean_KVMap_stringVal___closed__3;
return x_1;
}
}
lean_object* initialize_Init_Lean_Name(lean_object*);
lean_object* initialize_Init_Data_Option_Basic(lean_object*);
lean_object* initialize_Init_Data_Int(lean_object*);
lean_object* initialize_Init_Lean_Data_Name(lean_object*);
static bool _G_initialized = false;
lean_object* initialize_Init_Lean_KVMap(lean_object* w) {
lean_object* initialize_Init_Lean_Data_KVMap(lean_object* w) {
lean_object * res;
if (_G_initialized) return lean_mk_io_result(lean_box(0));
_G_initialized = true;
res = initialize_Init_Lean_Name(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Init_Data_Option_Basic(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Init_Data_Int(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Init_Lean_Data_Name(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l_Lean_DataValue_HasBeq___closed__1 = _init_l_Lean_DataValue_HasBeq___closed__1();
lean_mark_persistent(l_Lean_DataValue_HasBeq___closed__1);
l_Lean_DataValue_HasBeq = _init_l_Lean_DataValue_HasBeq();

4
stage0/stdlib/Init/Lean/LBool.c → stage0/stdlib/Init/Lean/Data/LBool.c
View file

@ -1,5 +1,5 @@
// Lean compiler output
// Module: Init.Lean.LBool
// Module: Init.Lean.Data.LBool
// Imports: Init.Data.ToString
#include "runtime/lean.h"
#if defined(__clang__)
@ -341,7 +341,7 @@ return x_2;
}
lean_object* initialize_Init_Data_ToString(lean_object*);
static bool _G_initialized = false;
lean_object* initialize_Init_Lean_LBool(lean_object* w) {
lean_object* initialize_Init_Lean_Data_LBool(lean_object* w) {
lean_object * res;
if (_G_initialized) return lean_mk_io_result(lean_box(0));
_G_initialized = true;

4
stage0/stdlib/Init/Lean/LOption.c → stage0/stdlib/Init/Lean/Data/LOption.c
View file

@ -1,5 +1,5 @@
// Lean compiler output
// Module: Init.Lean.LOption
// Module: Init.Lean.Data.LOption
// Imports: Init.Data.ToString
#include "runtime/lean.h"
#if defined(__clang__)
@ -279,7 +279,7 @@ return x_3;
}
lean_object* initialize_Init_Data_ToString(lean_object*);
static bool _G_initialized = false;
lean_object* initialize_Init_Lean_LOption(lean_object* w) {
lean_object* initialize_Init_Lean_Data_LOption(lean_object* w) {
lean_object * res;
if (_G_initialized) return lean_mk_io_result(lean_box(0));
_G_initialized = true;

9113
stage0/stdlib/Init/Lean/Data/Name.c Normal file
View file

File diff suppressed because it is too large Load diff

184
stage0/stdlib/Init/Lean/Data/NameGenerator.c Normal file
View file

@ -0,0 +1,184 @@
// Lean compiler output
// Module: Init.Lean.Data.NameGenerator
// Imports: Init.Lean.Data.Name
#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_Lean_NameGenerator_Inhabited;
lean_object* lean_nat_add(lean_object*, lean_object*);
lean_object* l_Lean_NameGenerator_next(lean_object*);
lean_object* l_Lean_NameGenerator_Inhabited___closed__2;
lean_object* l_Lean_NameGenerator_Inhabited___closed__1;
lean_object* lean_name_mk_string(lean_object*, lean_object*);
lean_object* l_Lean_NameGenerator_mkChild(lean_object*);
lean_object* l_Lean_NameGenerator_curr(lean_object*);
lean_object* lean_name_mk_numeral(lean_object*, lean_object*);
lean_object* l_Lean_NameGenerator_Inhabited___closed__3;
lean_object* _init_l_Lean_NameGenerator_Inhabited___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("_uniq");
return x_1;
}
}
lean_object* _init_l_Lean_NameGenerator_Inhabited___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Lean_NameGenerator_Inhabited___closed__1;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_NameGenerator_Inhabited___closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_NameGenerator_Inhabited___closed__2;
x_2 = lean_unsigned_to_nat(1u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_NameGenerator_Inhabited() {
_start:
{
lean_object* x_1;
x_1 = l_Lean_NameGenerator_Inhabited___closed__3;
return x_1;
}
}
lean_object* l_Lean_NameGenerator_curr(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3; lean_object* x_4;
x_2 = lean_ctor_get(x_1, 0);
lean_inc(x_2);
x_3 = lean_ctor_get(x_1, 1);
lean_inc(x_3);
lean_dec(x_1);
x_4 = lean_name_mk_numeral(x_2, x_3);
return x_4;
}
}
lean_object* l_Lean_NameGenerator_next(lean_object* x_1) {
_start:
{
uint8_t x_2;
x_2 = !lean_is_exclusive(x_1);
if (x_2 == 0)
{
lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_3 = lean_ctor_get(x_1, 1);
x_4 = lean_unsigned_to_nat(1u);
x_5 = lean_nat_add(x_3, x_4);
lean_dec(x_3);
lean_ctor_set(x_1, 1, x_5);
return x_1;
}
else
{
lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10;
x_6 = lean_ctor_get(x_1, 0);
x_7 = lean_ctor_get(x_1, 1);
lean_inc(x_7);
lean_inc(x_6);
lean_dec(x_1);
x_8 = lean_unsigned_to_nat(1u);
x_9 = lean_nat_add(x_7, x_8);
lean_dec(x_7);
x_10 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_10, 0, x_6);
lean_ctor_set(x_10, 1, x_9);
return x_10;
}
}
}
lean_object* l_Lean_NameGenerator_mkChild(lean_object* x_1) {
_start:
{
uint8_t x_2;
x_2 = !lean_is_exclusive(x_1);
if (x_2 == 0)
{
lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9;
x_3 = lean_ctor_get(x_1, 0);
x_4 = lean_ctor_get(x_1, 1);
lean_inc(x_4);
lean_inc(x_3);
x_5 = lean_name_mk_numeral(x_3, x_4);
x_6 = lean_unsigned_to_nat(1u);
lean_ctor_set(x_1, 1, x_6);
lean_ctor_set(x_1, 0, x_5);
x_7 = lean_nat_add(x_4, x_6);
lean_dec(x_4);
x_8 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_8, 0, x_3);
lean_ctor_set(x_8, 1, x_7);
x_9 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_9, 0, x_1);
lean_ctor_set(x_9, 1, x_8);
return x_9;
}
else
{
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_1, 0);
x_11 = lean_ctor_get(x_1, 1);
lean_inc(x_11);
lean_inc(x_10);
lean_dec(x_1);
lean_inc(x_11);
lean_inc(x_10);
x_12 = lean_name_mk_numeral(x_10, x_11);
x_13 = lean_unsigned_to_nat(1u);
x_14 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_14, 0, x_12);
lean_ctor_set(x_14, 1, x_13);
x_15 = lean_nat_add(x_11, x_13);
lean_dec(x_11);
x_16 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_16, 0, x_10);
lean_ctor_set(x_16, 1, x_15);
x_17 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_17, 0, x_14);
lean_ctor_set(x_17, 1, x_16);
return x_17;
}
}
}
lean_object* initialize_Init_Lean_Data_Name(lean_object*);
static bool _G_initialized = false;
lean_object* initialize_Init_Lean_Data_NameGenerator(lean_object* w) {
lean_object * res;
if (_G_initialized) return lean_mk_io_result(lean_box(0));
_G_initialized = true;
res = initialize_Init_Lean_Data_Name(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l_Lean_NameGenerator_Inhabited___closed__1 = _init_l_Lean_NameGenerator_Inhabited___closed__1();
lean_mark_persistent(l_Lean_NameGenerator_Inhabited___closed__1);
l_Lean_NameGenerator_Inhabited___closed__2 = _init_l_Lean_NameGenerator_Inhabited___closed__2();
lean_mark_persistent(l_Lean_NameGenerator_Inhabited___closed__2);
l_Lean_NameGenerator_Inhabited___closed__3 = _init_l_Lean_NameGenerator_Inhabited___closed__3();
lean_mark_persistent(l_Lean_NameGenerator_Inhabited___closed__3);
l_Lean_NameGenerator_Inhabited = _init_l_Lean_NameGenerator_Inhabited();
lean_mark_persistent(l_Lean_NameGenerator_Inhabited);
return lean_mk_io_result(lean_box(0));
}
#ifdef __cplusplus
}
#endif

1056
stage0/stdlib/Init/Lean/Data/Options.c Normal file
View file

File diff suppressed because it is too large Load diff

634
stage0/stdlib/Init/Lean/Data/Position.c Normal file
View file

@ -0,0 +1,634 @@
// Lean compiler output
// Module: Init.Lean.Data.Position
// Imports: Init.Data.Nat Init.Data.RBMap Init.Lean.Data.Format
#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_Lean_fmt___at_Lean_Position_Lean_HasFormat___spec__1(lean_object*);
lean_object* l___private_Init_Lean_Data_Position_3__toPositionAux___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_mk_empty_array_with_capacity(lean_object*);
lean_object* lean_nat_div(lean_object*, lean_object*);
lean_object* l_Lean_FileMap_ofString___closed__2;
lean_object* l_Lean_Position_Inhabited;
lean_object* l_Lean_Position_HasToString(lean_object*);
extern lean_object* l_Array_empty___closed__1;
extern lean_object* l_Sigma_HasRepr___rarg___closed__1;
lean_object* l_Nat_decLt___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Position_Inhabited___closed__1;
lean_object* lean_array_push(lean_object*, lean_object*);
lean_object* lean_array_get_size(lean_object*);
lean_object* lean_string_append(lean_object*, lean_object*);
uint8_t l_prodHasDecidableLt___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_formatKVMap___closed__1;
extern lean_object* l_String_splitAux___main___closed__1;
lean_object* l___private_Init_Lean_Data_Position_2__toColumnAux___main___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_FileMap_ofString___closed__1;
extern lean_object* l_Sigma_HasRepr___rarg___closed__2;
uint8_t l_Lean_Position_lt(lean_object*, lean_object*);
lean_object* lean_nat_add(lean_object*, lean_object*);
lean_object* lean_string_utf8_next(lean_object*, lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
lean_object* l_Lean_Position_Lean_HasFormat(lean_object*);
lean_object* lean_nat_sub(lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Data_Position_3__toPositionAux___main___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_array_get(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Data_Position_3__toPositionAux___main(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Nat_repr(lean_object*);
extern lean_object* l_List_reprAux___main___rarg___closed__1;
uint32_t lean_string_utf8_get(lean_object*, lean_object*);
lean_object* l_Lean_FileMap_toPosition(lean_object*, lean_object*);
lean_object* l_Lean_FileMap_ofString(lean_object*);
lean_object* l_Lean_Position_Lean_HasFormat___closed__2;
lean_object* l_Lean_FileMap_Inhabited;
lean_object* l___private_Init_Lean_Data_Position_2__toColumnAux___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Data_Position_1__ofStringAux(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_UInt32_decEq(uint32_t, uint32_t);
lean_object* l_Lean_Position_Lean_HasFormat___closed__1;
lean_object* l___private_Init_Lean_Data_Position_2__toColumnAux___main(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Position_DecidableEq___boxed(lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Data_Position_2__toColumnAux(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_FileMap_Inhabited___closed__1;
lean_object* l_Lean_Position_lt___closed__1;
lean_object* l___private_Init_Lean_Data_Position_1__ofStringAux___main(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_Position_DecidableEq(lean_object*, lean_object*);
extern lean_object* l_Nat_Inhabited;
lean_object* l_Lean_FileMap_ofString___closed__3;
lean_object* l___private_Init_Lean_Data_Position_3__toPositionAux(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t lean_string_utf8_at_end(lean_object*, lean_object*);
lean_object* l_Lean_Position_lt___boxed(lean_object*, lean_object*);
lean_object* l_Lean_FileMap_toPosition___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Position_lt___closed__2;
lean_object* l_Nat_decEq___boxed(lean_object*, lean_object*);
uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
lean_object* l_String_toFileMap(lean_object*);
uint8_t l_Lean_Position_DecidableEq(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; uint8_t x_7;
x_3 = lean_ctor_get(x_1, 0);
x_4 = lean_ctor_get(x_1, 1);
x_5 = lean_ctor_get(x_2, 0);
x_6 = lean_ctor_get(x_2, 1);
x_7 = lean_nat_dec_eq(x_3, x_5);
if (x_7 == 0)
{
uint8_t x_8;
x_8 = 0;
return x_8;
}
else
{
uint8_t x_9;
x_9 = lean_nat_dec_eq(x_4, x_6);
if (x_9 == 0)
{
uint8_t x_10;
x_10 = 0;
return x_10;
}
else
{
uint8_t x_11;
x_11 = 1;
return x_11;
}
}
}
}
lean_object* l_Lean_Position_DecidableEq___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
uint8_t x_3; lean_object* x_4;
x_3 = l_Lean_Position_DecidableEq(x_1, x_2);
lean_dec(x_2);
lean_dec(x_1);
x_4 = lean_box(x_3);
return x_4;
}
}
lean_object* _init_l_Lean_Position_lt___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Nat_decEq___boxed), 2, 0);
return x_1;
}
}
lean_object* _init_l_Lean_Position_lt___closed__2() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Nat_decLt___boxed), 2, 0);
return x_1;
}
}
uint8_t l_Lean_Position_lt(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; uint8_t x_11;
x_3 = lean_ctor_get(x_1, 0);
x_4 = lean_ctor_get(x_1, 1);
x_5 = lean_ctor_get(x_2, 0);
x_6 = lean_ctor_get(x_2, 1);
lean_inc(x_4);
lean_inc(x_3);
x_7 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_7, 0, x_3);
lean_ctor_set(x_7, 1, x_4);
lean_inc(x_6);
lean_inc(x_5);
x_8 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_8, 0, x_5);
lean_ctor_set(x_8, 1, x_6);
x_9 = l_Lean_Position_lt___closed__1;
x_10 = l_Lean_Position_lt___closed__2;
x_11 = l_prodHasDecidableLt___rarg(x_9, x_9, x_10, x_10, x_7, x_8);
return x_11;
}
}
lean_object* l_Lean_Position_lt___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
uint8_t x_3; lean_object* x_4;
x_3 = l_Lean_Position_lt(x_1, x_2);
lean_dec(x_2);
lean_dec(x_1);
x_4 = lean_box(x_3);
return x_4;
}
}
lean_object* l_Lean_fmt___at_Lean_Position_Lean_HasFormat___spec__1(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3;
x_2 = l_Nat_repr(x_1);
x_3 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_3, 0, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Position_Lean_HasFormat___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Sigma_HasRepr___rarg___closed__1;
x_2 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
}
}
lean_object* _init_l_Lean_Position_Lean_HasFormat___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Sigma_HasRepr___rarg___closed__2;
x_2 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
}
}
lean_object* l_Lean_Position_Lean_HasFormat(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3; lean_object* x_4; uint8_t x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13;
x_2 = lean_ctor_get(x_1, 0);
lean_inc(x_2);
x_3 = lean_ctor_get(x_1, 1);
lean_inc(x_3);
lean_dec(x_1);
x_4 = l_Lean_fmt___at_Lean_Position_Lean_HasFormat___spec__1(x_2);
x_5 = 0;
x_6 = l_Lean_Position_Lean_HasFormat___closed__1;
x_7 = lean_alloc_ctor(4, 2, 1);
lean_ctor_set(x_7, 0, x_6);
lean_ctor_set(x_7, 1, x_4);
lean_ctor_set_uint8(x_7, sizeof(void*)*2, x_5);
x_8 = l_Lean_formatKVMap___closed__1;
x_9 = lean_alloc_ctor(4, 2, 1);
lean_ctor_set(x_9, 0, x_7);
lean_ctor_set(x_9, 1, x_8);
lean_ctor_set_uint8(x_9, sizeof(void*)*2, x_5);
x_10 = l_Lean_fmt___at_Lean_Position_Lean_HasFormat___spec__1(x_3);
x_11 = lean_alloc_ctor(4, 2, 1);
lean_ctor_set(x_11, 0, x_9);
lean_ctor_set(x_11, 1, x_10);
lean_ctor_set_uint8(x_11, sizeof(void*)*2, x_5);
x_12 = l_Lean_Position_Lean_HasFormat___closed__2;
x_13 = lean_alloc_ctor(4, 2, 1);
lean_ctor_set(x_13, 0, x_11);
lean_ctor_set(x_13, 1, x_12);
lean_ctor_set_uint8(x_13, sizeof(void*)*2, x_5);
return x_13;
}
}
lean_object* l_Lean_Position_HasToString(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12;
x_2 = lean_ctor_get(x_1, 0);
lean_inc(x_2);
x_3 = lean_ctor_get(x_1, 1);
lean_inc(x_3);
lean_dec(x_1);
x_4 = l_Nat_repr(x_2);
x_5 = l_Sigma_HasRepr___rarg___closed__1;
x_6 = lean_string_append(x_5, x_4);
lean_dec(x_4);
x_7 = l_List_reprAux___main___rarg___closed__1;
x_8 = lean_string_append(x_6, x_7);
x_9 = l_Nat_repr(x_3);
x_10 = lean_string_append(x_8, x_9);
lean_dec(x_9);
x_11 = l_Sigma_HasRepr___rarg___closed__2;
x_12 = lean_string_append(x_10, x_11);
return x_12;
}
}
lean_object* _init_l_Lean_Position_Inhabited___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_unsigned_to_nat(1u);
x_2 = lean_unsigned_to_nat(0u);
x_3 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Position_Inhabited() {
_start:
{
lean_object* x_1;
x_1 = l_Lean_Position_Inhabited___closed__1;
return x_1;
}
}
lean_object* _init_l_Lean_FileMap_Inhabited___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_String_splitAux___main___closed__1;
x_2 = l_Array_empty___closed__1;
x_3 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
lean_ctor_set(x_3, 2, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_FileMap_Inhabited() {
_start:
{
lean_object* x_1;
x_1 = l_Lean_FileMap_Inhabited___closed__1;
return x_1;
}
}
lean_object* l___private_Init_Lean_Data_Position_1__ofStringAux___main(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
_start:
{
uint8_t x_6;
x_6 = lean_string_utf8_at_end(x_1, x_2);
if (x_6 == 0)
{
uint32_t x_7; lean_object* x_8; uint32_t x_9; uint8_t x_10;
x_7 = lean_string_utf8_get(x_1, x_2);
x_8 = lean_string_utf8_next(x_1, x_2);
lean_dec(x_2);
x_9 = 10;
x_10 = x_7 == x_9;
if (x_10 == 0)
{
x_2 = x_8;
goto _start;
}
else
{
lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15;
x_12 = lean_unsigned_to_nat(1u);
x_13 = lean_nat_add(x_3, x_12);
lean_dec(x_3);
lean_inc(x_8);
x_14 = lean_array_push(x_4, x_8);
lean_inc(x_13);
x_15 = lean_array_push(x_5, x_13);
x_2 = x_8;
x_3 = x_13;
x_4 = x_14;
x_5 = x_15;
goto _start;
}
}
else
{
lean_object* x_17; lean_object* x_18; lean_object* x_19;
x_17 = lean_array_push(x_4, x_2);
x_18 = lean_array_push(x_5, x_3);
x_19 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_19, 0, x_1);
lean_ctor_set(x_19, 1, x_17);
lean_ctor_set(x_19, 2, x_18);
return x_19;
}
}
}
lean_object* l___private_Init_Lean_Data_Position_1__ofStringAux(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
_start:
{
lean_object* x_6;
x_6 = l___private_Init_Lean_Data_Position_1__ofStringAux___main(x_1, x_2, x_3, x_4, x_5);
return x_6;
}
}
lean_object* _init_l_Lean_FileMap_ofString___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = lean_unsigned_to_nat(1u);
x_2 = lean_mk_empty_array_with_capacity(x_1);
return x_2;
}
}
lean_object* _init_l_Lean_FileMap_ofString___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_FileMap_ofString___closed__1;
x_2 = lean_unsigned_to_nat(0u);
x_3 = lean_array_push(x_1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_FileMap_ofString___closed__3() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_FileMap_ofString___closed__1;
x_2 = lean_unsigned_to_nat(1u);
x_3 = lean_array_push(x_1, x_2);
return x_3;
}
}
lean_object* l_Lean_FileMap_ofString(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_2 = lean_unsigned_to_nat(0u);
x_3 = lean_unsigned_to_nat(1u);
x_4 = l_Lean_FileMap_ofString___closed__2;
x_5 = l_Lean_FileMap_ofString___closed__3;
x_6 = l___private_Init_Lean_Data_Position_1__ofStringAux___main(x_1, x_2, x_3, x_4, x_5);
return x_6;
}
}
lean_object* l___private_Init_Lean_Data_Position_2__toColumnAux___main(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
uint8_t x_5;
x_5 = lean_nat_dec_eq(x_3, x_2);
if (x_5 == 0)
{
uint8_t x_6;
x_6 = lean_string_utf8_at_end(x_1, x_3);
if (x_6 == 0)
{
lean_object* x_7; lean_object* x_8; lean_object* x_9;
x_7 = lean_string_utf8_next(x_1, x_3);
lean_dec(x_3);
x_8 = lean_unsigned_to_nat(1u);
x_9 = lean_nat_add(x_4, x_8);
lean_dec(x_4);
x_3 = x_7;
x_4 = x_9;
goto _start;
}
else
{
lean_dec(x_3);
return x_4;
}
}
else
{
lean_dec(x_3);
return x_4;
}
}
}
lean_object* l___private_Init_Lean_Data_Position_2__toColumnAux___main___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
lean_object* x_5;
x_5 = l___private_Init_Lean_Data_Position_2__toColumnAux___main(x_1, x_2, x_3, x_4);
lean_dec(x_2);
lean_dec(x_1);
return x_5;
}
}
lean_object* l___private_Init_Lean_Data_Position_2__toColumnAux(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
_start:
{
lean_object* x_6;
x_6 = l___private_Init_Lean_Data_Position_2__toColumnAux___main(x_1, x_3, x_4, x_5);
return x_6;
}
}
lean_object* l___private_Init_Lean_Data_Position_2__toColumnAux___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
_start:
{
lean_object* x_6;
x_6 = l___private_Init_Lean_Data_Position_2__toColumnAux(x_1, x_2, x_3, x_4, x_5);
lean_dec(x_3);
lean_dec(x_2);
lean_dec(x_1);
return x_6;
}
}
lean_object* l___private_Init_Lean_Data_Position_3__toPositionAux___main(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
_start:
{
lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; uint8_t x_11;
x_7 = l_Nat_Inhabited;
x_8 = lean_array_get(x_7, x_2, x_5);
x_9 = lean_unsigned_to_nat(1u);
x_10 = lean_nat_add(x_5, x_9);
x_11 = lean_nat_dec_eq(x_6, x_10);
lean_dec(x_10);
if (x_11 == 0)
{
lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; uint8_t x_16;
lean_dec(x_8);
x_12 = lean_nat_add(x_5, x_6);
x_13 = lean_unsigned_to_nat(2u);
x_14 = lean_nat_div(x_12, x_13);
lean_dec(x_12);
x_15 = lean_array_get(x_7, x_2, x_14);
x_16 = lean_nat_dec_eq(x_4, x_15);
if (x_16 == 0)
{
uint8_t x_17;
x_17 = lean_nat_dec_lt(x_15, x_4);
lean_dec(x_15);
if (x_17 == 0)
{
lean_dec(x_6);
x_6 = x_14;
goto _start;
}
else
{
lean_dec(x_5);
x_5 = x_14;
goto _start;
}
}
else
{
lean_object* x_20; lean_object* x_21; lean_object* x_22;
lean_dec(x_15);
lean_dec(x_6);
lean_dec(x_5);
x_20 = lean_array_get(x_7, x_3, x_14);
lean_dec(x_14);
x_21 = lean_unsigned_to_nat(0u);
x_22 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_22, 0, x_20);
lean_ctor_set(x_22, 1, x_21);
return x_22;
}
}
else
{
lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26;
lean_dec(x_6);
x_23 = lean_array_get(x_7, x_3, x_5);
lean_dec(x_5);
x_24 = lean_unsigned_to_nat(0u);
x_25 = l___private_Init_Lean_Data_Position_2__toColumnAux___main(x_1, x_4, x_8, x_24);
x_26 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_26, 0, x_23);
lean_ctor_set(x_26, 1, x_25);
return x_26;
}
}
}
lean_object* l___private_Init_Lean_Data_Position_3__toPositionAux___main___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
_start:
{
lean_object* x_7;
x_7 = l___private_Init_Lean_Data_Position_3__toPositionAux___main(x_1, x_2, x_3, x_4, x_5, x_6);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_2);
lean_dec(x_1);
return x_7;
}
}
lean_object* l___private_Init_Lean_Data_Position_3__toPositionAux(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
_start:
{
lean_object* x_7;
x_7 = l___private_Init_Lean_Data_Position_3__toPositionAux___main(x_1, x_2, x_3, x_4, x_5, x_6);
return x_7;
}
}
lean_object* l___private_Init_Lean_Data_Position_3__toPositionAux___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
_start:
{
lean_object* x_7;
x_7 = l___private_Init_Lean_Data_Position_3__toPositionAux(x_1, x_2, x_3, x_4, x_5, x_6);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_2);
lean_dec(x_1);
return x_7;
}
}
lean_object* l_Lean_FileMap_toPosition(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10;
x_3 = lean_ctor_get(x_1, 0);
x_4 = lean_ctor_get(x_1, 1);
x_5 = lean_ctor_get(x_1, 2);
x_6 = lean_array_get_size(x_4);
x_7 = lean_unsigned_to_nat(1u);
x_8 = lean_nat_sub(x_6, x_7);
lean_dec(x_6);
x_9 = lean_unsigned_to_nat(0u);
x_10 = l___private_Init_Lean_Data_Position_3__toPositionAux___main(x_3, x_4, x_5, x_2, x_9, x_8);
return x_10;
}
}
lean_object* l_Lean_FileMap_toPosition___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = l_Lean_FileMap_toPosition(x_1, x_2);
lean_dec(x_2);
lean_dec(x_1);
return x_3;
}
}
lean_object* l_String_toFileMap(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = l_Lean_FileMap_ofString(x_1);
return x_2;
}
}
lean_object* initialize_Init_Data_Nat(lean_object*);
lean_object* initialize_Init_Data_RBMap(lean_object*);
lean_object* initialize_Init_Lean_Data_Format(lean_object*);
static bool _G_initialized = false;
lean_object* initialize_Init_Lean_Data_Position(lean_object* w) {
lean_object * res;
if (_G_initialized) return lean_mk_io_result(lean_box(0));
_G_initialized = true;
res = initialize_Init_Data_Nat(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Init_Data_RBMap(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Init_Lean_Data_Format(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l_Lean_Position_lt___closed__1 = _init_l_Lean_Position_lt___closed__1();
lean_mark_persistent(l_Lean_Position_lt___closed__1);
l_Lean_Position_lt___closed__2 = _init_l_Lean_Position_lt___closed__2();
lean_mark_persistent(l_Lean_Position_lt___closed__2);
l_Lean_Position_Lean_HasFormat___closed__1 = _init_l_Lean_Position_Lean_HasFormat___closed__1();
lean_mark_persistent(l_Lean_Position_Lean_HasFormat___closed__1);
l_Lean_Position_Lean_HasFormat___closed__2 = _init_l_Lean_Position_Lean_HasFormat___closed__2();
lean_mark_persistent(l_Lean_Position_Lean_HasFormat___closed__2);
l_Lean_Position_Inhabited___closed__1 = _init_l_Lean_Position_Inhabited___closed__1();
lean_mark_persistent(l_Lean_Position_Inhabited___closed__1);
l_Lean_Position_Inhabited = _init_l_Lean_Position_Inhabited();
lean_mark_persistent(l_Lean_Position_Inhabited);
l_Lean_FileMap_Inhabited___closed__1 = _init_l_Lean_FileMap_Inhabited___closed__1();
lean_mark_persistent(l_Lean_FileMap_Inhabited___closed__1);
l_Lean_FileMap_Inhabited = _init_l_Lean_FileMap_Inhabited();
lean_mark_persistent(l_Lean_FileMap_Inhabited);
l_Lean_FileMap_ofString___closed__1 = _init_l_Lean_FileMap_ofString___closed__1();
lean_mark_persistent(l_Lean_FileMap_ofString___closed__1);
l_Lean_FileMap_ofString___closed__2 = _init_l_Lean_FileMap_ofString___closed__2();
lean_mark_persistent(l_Lean_FileMap_ofString___closed__2);
l_Lean_FileMap_ofString___closed__3 = _init_l_Lean_FileMap_ofString___closed__3();
lean_mark_persistent(l_Lean_FileMap_ofString___closed__3);
return lean_mk_io_result(lean_box(0));
}
#ifdef __cplusplus
}
#endif

6
stage0/stdlib/Init/Lean/SMap.c → stage0/stdlib/Init/Lean/Data/SMap.c
View file

@ -1,5 +1,5 @@
// Lean compiler output
// Module: Init.Lean.SMap
// Module: Init.Lean.Data.SMap
// Imports: Init.Data.HashMap Init.Data.PersistentHashMap
#include "runtime/lean.h"
#if defined(__clang__)
@ -345,7 +345,7 @@ lean_object* _init_l_Lean_SMap_find_x21___rarg___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("Init.Lean.SMap");
x_1 = lean_mk_string("Init.Lean.Data.SMap");
return x_1;
}
}
@ -916,7 +916,7 @@ return x_5;
lean_object* initialize_Init_Data_HashMap(lean_object*);
lean_object* initialize_Init_Data_PersistentHashMap(lean_object*);
static bool _G_initialized = false;
lean_object* initialize_Init_Lean_SMap(lean_object* w) {
lean_object* initialize_Init_Lean_Data_SMap(lean_object* w) {
lean_object * res;
if (_G_initialized) return lean_mk_io_result(lean_box(0));
_G_initialized = true;

10829
stage0/stdlib/Init/Lean/Data/Trie.c Normal file
View file

File diff suppressed because it is too large Load diff

108
stage0/stdlib/Init/Lean/Elaborator/Basic.c
View file

@ -1,6 +1,6 @@
// Lean compiler output
// Module: Init.Lean.Elaborator.Basic
// Imports: Init.Control.Reader Init.Lean.MetavarContext Init.Lean.NameGenerator Init.Lean.Scopes Init.Lean.Parser.Module
// Imports: Init.Control.Reader Init.Lean.MetavarContext Init.Lean.Scopes Init.Lean.Parser.Module
#include "runtime/lean.h"
#if defined(__clang__)
#pragma clang diagnostic ignored "-Wunused-parameter"
@ -310,7 +310,6 @@ lean_object* l_PersistentHashMap_insertAtCollisionNodeAux___main___at_Lean_addBu
lean_object* l_Lean_registerBuiltinCommandElabAttr___closed__2;
extern lean_object* l_Lean_registerPersistentEnvExtensionUnsafe___rarg___closed__1;
lean_object* l_Lean_registerBuiltinCommandElabAttr___closed__1;
lean_object* l_Lean_mkCAppN(lean_object*, lean_object*);
uint8_t l_HashMapImp_contains___at_Lean_addBuiltinCommandElab___spec__2(lean_object*, lean_object*);
lean_object* l_Lean_Elab_withInPattern(lean_object*);
lean_object* l_Lean_addBuiltinCommandElab(lean_object*, lean_object*, lean_object*, lean_object*);
@ -425,6 +424,7 @@ extern lean_object* l_System_FilePath_dirName___closed__1;
lean_object* l_Lean_Elab_runIO___rarg(lean_object*);
lean_object* l_unsafeCast(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Inhabited(lean_object*, lean_object*);
lean_object* l_Array_iterateMAux___main___at_Lean_mkAppN___spec__1(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Name_toStringWithSep___main(lean_object*, lean_object*);
lean_object* l_Lean_registerBuiltinTermElabAttr___closed__5;
lean_object* l_AssocList_foldlM___main___at_Lean_addBuiltinCommandElab___spec__14(lean_object*, lean_object*);
@ -3863,70 +3863,72 @@ return x_1;
lean_object* l_Lean_declareBuiltinElab(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
_start:
{
lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; 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; lean_object* x_18; lean_object* x_19; uint8_t x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24;
lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; 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; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; uint8_t x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26;
x_6 = l_Lean_declareBuiltinElab___closed__2;
lean_inc(x_4);
x_7 = l_Lean_Name_append___main(x_6, x_4);
x_8 = lean_box(0);
x_9 = l_Lean_nameToExprAux___main(x_3);
x_9 = l_Lean_mkConst(x_2, x_8);
x_10 = l_Lean_nameToExprAux___main(x_3);
lean_inc(x_4);
x_10 = l_Lean_nameToExprAux___main(x_4);
x_11 = l_Lean_nameToExprAux___main(x_4);
lean_inc(x_4);
x_11 = l_Lean_mkConst(x_4, x_8);
x_12 = l_Lean_Parser_declareBuiltinParser___closed__8;
x_13 = lean_array_push(x_12, x_9);
x_12 = l_Lean_mkConst(x_4, x_8);
x_13 = l_Lean_Parser_declareBuiltinParser___closed__8;
x_14 = lean_array_push(x_13, x_10);
x_15 = lean_array_push(x_14, x_11);
x_16 = l_Lean_mkCAppN(x_2, x_15);
lean_dec(x_15);
x_17 = l_Lean_Parser_declareBuiltinParser___closed__7;
x_16 = lean_array_push(x_15, x_12);
x_17 = lean_unsigned_to_nat(0u);
x_18 = l_Array_iterateMAux___main___at_Lean_mkAppN___spec__1(x_16, x_16, x_17, x_9);
lean_dec(x_16);
x_19 = l_Lean_Parser_declareBuiltinParser___closed__7;
lean_inc(x_7);
x_18 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_18, 0, x_7);
lean_ctor_set(x_18, 1, x_8);
lean_ctor_set(x_18, 2, x_17);
x_19 = lean_box(0);
x_20 = 0;
x_21 = lean_alloc_ctor(0, 3, 1);
lean_ctor_set(x_21, 0, x_18);
lean_ctor_set(x_21, 1, x_16);
lean_ctor_set(x_21, 2, x_19);
lean_ctor_set_uint8(x_21, sizeof(void*)*3, x_20);
x_22 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_22, 0, x_21);
x_23 = l_Lean_Options_empty;
x_24 = l_Lean_Environment_addAndCompile(x_1, x_23, x_22);
lean_dec(x_22);
if (lean_obj_tag(x_24) == 0)
{
lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31;
x_20 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_20, 0, x_7);
lean_ctor_set(x_20, 1, x_8);
lean_ctor_set(x_20, 2, x_19);
x_21 = lean_box(0);
x_22 = 0;
x_23 = lean_alloc_ctor(0, 3, 1);
lean_ctor_set(x_23, 0, x_20);
lean_ctor_set(x_23, 1, x_18);
lean_ctor_set(x_23, 2, x_21);
lean_ctor_set_uint8(x_23, sizeof(void*)*3, x_22);
x_24 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_24, 0, x_23);
x_25 = l_Lean_Options_empty;
x_26 = l_Lean_Environment_addAndCompile(x_1, x_25, x_24);
lean_dec(x_24);
lean_dec(x_7);
x_25 = l_System_FilePath_dirName___closed__1;
x_26 = l_Lean_Name_toStringWithSep___main(x_25, x_4);
x_27 = l_Lean_declareBuiltinElab___closed__3;
x_28 = lean_string_append(x_27, x_26);
if (lean_obj_tag(x_26) == 0)
{
lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33;
lean_dec(x_26);
x_29 = l_Char_HasRepr___closed__1;
x_30 = lean_string_append(x_28, x_29);
x_31 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_31, 0, x_30);
lean_ctor_set(x_31, 1, x_5);
return x_31;
lean_dec(x_7);
x_27 = l_System_FilePath_dirName___closed__1;
x_28 = l_Lean_Name_toStringWithSep___main(x_27, x_4);
x_29 = l_Lean_declareBuiltinElab___closed__3;
x_30 = lean_string_append(x_29, x_28);
lean_dec(x_28);
x_31 = l_Char_HasRepr___closed__1;
x_32 = lean_string_append(x_30, x_31);
x_33 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_33, 0, x_32);
lean_ctor_set(x_33, 1, x_5);
return x_33;
}
else
{
lean_object* x_32; lean_object* x_33; lean_object* x_34; lean_object* x_35; lean_object* x_36;
lean_object* x_34; lean_object* x_35; lean_object* x_36; lean_object* x_37; lean_object* x_38;
lean_dec(x_4);
x_32 = lean_ctor_get(x_24, 0);
lean_inc(x_32);
lean_dec(x_24);
x_33 = l_Lean_initAttr;
x_34 = lean_box(0);
x_35 = l_Lean_ParametricAttribute_setParam___rarg(x_33, x_32, x_7, x_34);
x_36 = l_IO_ofExcept___at_Lean_Parser_declareBuiltinParser___spec__1(x_35, x_5);
lean_dec(x_35);
return x_36;
x_34 = lean_ctor_get(x_26, 0);
lean_inc(x_34);
lean_dec(x_26);
x_35 = l_Lean_initAttr;
x_36 = lean_box(0);
x_37 = l_Lean_ParametricAttribute_setParam___rarg(x_35, x_34, x_7, x_36);
x_38 = l_IO_ofExcept___at_Lean_Parser_declareBuiltinParser___spec__1(x_37, x_5);
lean_dec(x_37);
return x_38;
}
}
}
@ -13201,7 +13203,6 @@ return x_4;
}
lean_object* initialize_Init_Control_Reader(lean_object*);
lean_object* initialize_Init_Lean_MetavarContext(lean_object*);
lean_object* initialize_Init_Lean_NameGenerator(lean_object*);
lean_object* initialize_Init_Lean_Scopes(lean_object*);
lean_object* initialize_Init_Lean_Parser_Module(lean_object*);
static bool _G_initialized = false;
@ -13215,9 +13216,6 @@ lean_dec_ref(res);
res = initialize_Init_Lean_MetavarContext(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Init_Lean_NameGenerator(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Init_Lean_Scopes(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);

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

@ -1,6 +1,6 @@
// Lean compiler output
// Module: Init.Lean.Environment
// Imports: Init.System.IO Init.Util Init.Data.ByteArray Init.Lean.Declaration Init.Lean.SMap Init.Lean.Path Init.Lean.LocalContext
// Imports: Init.System.IO Init.Util Init.Data.ByteArray Init.Lean.Data.SMap Init.Lean.Declaration Init.Lean.Path Init.Lean.LocalContext
#include "runtime/lean.h"
#if defined(__clang__)
#pragma clang diagnostic ignored "-Wunused-parameter"
@ -12115,8 +12115,8 @@ return x_2;
lean_object* initialize_Init_System_IO(lean_object*);
lean_object* initialize_Init_Util(lean_object*);
lean_object* initialize_Init_Data_ByteArray(lean_object*);
lean_object* initialize_Init_Lean_Data_SMap(lean_object*);
lean_object* initialize_Init_Lean_Declaration(lean_object*);
lean_object* initialize_Init_Lean_SMap(lean_object*);
lean_object* initialize_Init_Lean_Path(lean_object*);
lean_object* initialize_Init_Lean_LocalContext(lean_object*);
static bool _G_initialized = false;
@ -12133,10 +12133,10 @@ lean_dec_ref(res);
res = initialize_Init_Data_ByteArray(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Init_Lean_Declaration(lean_io_mk_world());
res = initialize_Init_Lean_Data_SMap(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Init_Lean_SMap(lean_io_mk_world());
res = initialize_Init_Lean_Declaration(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Init_Lean_Path(lean_io_mk_world());

205
stage0/stdlib/Init/Lean/Expr.c
View file

@ -1,6 +1,6 @@
// Lean compiler output
// Module: Init.Lean.Expr
// Imports: Init.Lean.Level Init.Lean.KVMap Init.Data.HashMap Init.Data.HashSet Init.Data.PersistentHashMap Init.Data.PersistentHashSet
// Imports: Init.Data.HashMap Init.Data.HashSet Init.Data.PersistentHashMap Init.Data.PersistentHashSet Init.Lean.Data.KVMap Init.Lean.Level
#include "runtime/lean.h"
#if defined(__clang__)
#pragma clang diagnostic ignored "-Wunused-parameter"
@ -40,6 +40,7 @@ lean_object* l_Lean_mkDecIsTrue___closed__3;
lean_object* l_unreachable_x21___rarg(lean_object*);
lean_object* l_Lean_Expr_withApp(lean_object*);
size_t l_UInt32_toUSize(uint32_t);
lean_object* l_Lean_mkApp6(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Expr_eqv___boxed(lean_object*, lean_object*);
uint8_t l_Lean_Expr_isMData(lean_object*);
lean_object* l_Lean_Expr_withAppAux___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
@ -84,7 +85,6 @@ lean_object* l_Lean_Expr_getAppFn___main___boxed(lean_object*);
lean_object* l_Lean_Expr_constName_x21___closed__1;
extern lean_object* l_Lean_Level_mkData___closed__1;
lean_object* l_Lean_Expr_mvarId_x21___closed__1;
lean_object* l_Lean_mkCAppB(lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_Level_hasMVar(lean_object*);
lean_object* l_Lean_Expr_constName_x21___boxed(lean_object*);
lean_object* l_Lean_Expr_withAppRev___rarg(lean_object*, lean_object*);
@ -118,6 +118,7 @@ lean_object* l_List_map___main___rarg(lean_object*, lean_object*);
lean_object* l_Nat_max(lean_object*, lean_object*);
lean_object* l_Lean_Expr_getAppFn___main(lean_object*);
extern lean_object* l_Lean_Name_inhabited;
extern lean_object* l_Lean_Level_Inhabited;
lean_object* l_Lean_Expr_getRevArgD(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Expr_11__getParamSubst___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Expr_getAppArgs___closed__1;
@ -191,6 +192,7 @@ lean_object* l_Lean_Expr_updateApp___boxed(lean_object*, lean_object*, lean_obje
lean_object* l_Lean_ExprStructEq_beq___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Expr_updateSort_x21(lean_object*, lean_object*);
uint8_t lean_expr_has_expr_mvar(lean_object*);
extern lean_object* l_List_Monad;
lean_object* l_Lean_Literal_type___closed__6;
lean_object* l___private_Init_Lean_Expr_2__mkAppRangeAux___main___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_Expr_hasLevelParam(lean_object*);
@ -235,7 +237,6 @@ lean_object* l_Lean_Expr_hasMVarEx___boxed(lean_object*);
lean_object* l_Lean_mkAppRange___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
extern uint64_t l_UInt64_Inhabited;
lean_object* l_Lean_Expr_fvarId_x21___boxed(lean_object*);
lean_object* l_Lean_mkCAppN___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Literal_inhabited;
lean_object* l_Lean_Expr_fvarId_x21___closed__1;
lean_object* lean_expr_mk_bvar(lean_object*);
@ -250,7 +251,6 @@ lean_object* l_Lean_Expr_bindingDomain_x21___closed__1;
lean_object* l_Lean_Expr_InstantiateLevelParams_instantiate(lean_object*, lean_object*);
lean_object* lean_expr_mk_const(lean_object*, lean_object*);
lean_object* l_Lean_mkAppRange(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_mkCApp(lean_object*, lean_object*);
lean_object* l_Lean_Literal_type___closed__4;
lean_object* l_Lean_mkDecIsTrue___closed__4;
lean_object* lean_expr_mk_lit(lean_object*);
@ -302,6 +302,7 @@ size_t l_Lean_ExprStructEq_hash(lean_object*);
lean_object* l_Lean_Level_instantiateParams___main(lean_object*, lean_object*);
uint8_t l_Lean_Expr_isLambda(lean_object*);
lean_object* l_Lean_Expr_updateSort_x21___closed__2;
lean_object* l_Lean_mkApp9(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Expr_data___boxed(lean_object*);
lean_object* lean_expr_update_proj(lean_object*, lean_object*);
lean_object* l_Lean_ExprStructEq_HasToString(lean_object*);
@ -322,7 +323,6 @@ lean_object* l_Lean_Expr_updateProj_x21___closed__1;
uint8_t l_Lean_BinderInfo_inhabited;
lean_object* lean_level_update_imax(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Expr_2__mkAppRangeAux(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_mkCAppN(lean_object*, lean_object*);
lean_object* l_Lean_Expr_HasRepr;
lean_object* l_Lean_Expr_isProj___boxed(lean_object*);
lean_object* l_Lean_Expr_updateLambda_x21___closed__2;
@ -352,6 +352,7 @@ lean_object* l_Lean_Expr_getRevArg_x21___main(lean_object*, lean_object*);
lean_object* l_Lean_Expr_hasAnyFVar(lean_object*, lean_object*);
lean_object* l_Lean_Expr_hasMVar___boxed(lean_object*);
lean_object* l_Lean_mkForall___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Expr_constLevels_x21___closed__2;
lean_object* l_Lean_mkApp(lean_object*, lean_object*);
lean_object* l_Lean_Expr_getAppNumArgsAux___boxed(lean_object*, lean_object*);
size_t l_Lean_Literal_hash(lean_object*);
@ -360,6 +361,7 @@ uint8_t l_Lean_Expr_hasMVar(lean_object*);
lean_object* l_Lean_Expr_betaRev(lean_object*, lean_object*);
lean_object* l_Lean_BinderInfo_isInstImplicit___boxed(lean_object*);
lean_object* l_Lean_Expr_getRevArg_x21___main___boxed(lean_object*, lean_object*);
lean_object* l_Lean_mkApp5(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Expr_Data_looseBVarRange___boxed(lean_object*);
lean_object* l_Lean_mkAppRev(lean_object*, lean_object*);
lean_object* l_Lean_Expr_InstantiateLevelParams_visit(lean_object*, lean_object*);
@ -377,6 +379,7 @@ uint64_t l_UInt64_shiftLeft(uint64_t, uint64_t);
lean_object* l_Lean_Expr_binderInfo___boxed(lean_object*);
lean_object* l_Lean_Literal_lt___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Expr_updateFn___main(lean_object*, lean_object*);
lean_object* l_Lean_mkApp7(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Expr_updateLambda_x21___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_expr_mk_proj(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Expr_appFn_x21___closed__2;
@ -390,6 +393,7 @@ lean_object* l_Lean_Expr_dbgToString___boxed(lean_object*);
lean_object* l_Lean_Expr_isForall___boxed(lean_object*);
lean_object* l_Lean_Expr_isMData___boxed(lean_object*);
lean_object* l_Lean_Expr_bvarIdx_x21___boxed(lean_object*);
lean_object* l_Lean_mkApp4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Expr_withAppRev(lean_object*);
lean_object* l_Lean_Expr_quickLt___boxed(lean_object*, lean_object*);
uint64_t l_UInt32_toUInt64(uint32_t);
@ -429,6 +433,7 @@ uint8_t l_Lean_Expr_binderInfo(lean_object*);
size_t lean_usize_mix_hash(size_t, size_t);
lean_object* lean_expr_abstract(lean_object*, lean_object*);
lean_object* l_Lean_Expr_getArg_x21(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_mkApp2(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Expr_InstantiateLevelParams_instantiate___main___at_Lean_Expr_instantiateLevelParams___spec__1___boxed(lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_Expr_Data_hasBeq(uint64_t, uint64_t);
uint32_t lean_expr_loose_bvar_range(lean_object*);
@ -469,8 +474,10 @@ extern lean_object* l_List_get_x21___main___rarg___closed__2;
lean_object* l___private_Init_Lean_Expr_7__betaRevAux(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_mkAppB(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Expr_getRevArgD___main(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_mkApp10(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Expr_isApp___boxed(lean_object*);
lean_object* l_Lean_Expr_HasBeq;
lean_object* l_Lean_mkApp8(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_mkBVar(lean_object*);
uint8_t l_Lean_Expr_hasFVar(lean_object*);
lean_object* lean_expr_mk_lambda(lean_object*, lean_object*, lean_object*, uint8_t);
@ -499,6 +506,7 @@ size_t lean_string_hash(lean_object*);
lean_object* l___private_Init_Lean_Expr_1__Expr_mkDataCore___boxed__const__1;
lean_object* l___private_Init_Data_Array_Basic_3__iterateRevMAux___main___at_Lean_mkAppRev___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_mkLocal___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_mkApp3(lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_Expr_isSort(lean_object*);
uint8_t l_Lean_Expr_isLet(lean_object*);
uint8_t lean_string_dec_lt(lean_object*, lean_object*);
@ -510,6 +518,7 @@ uint8_t lean_string_dec_eq(lean_object*, lean_object*);
uint32_t l_Lean_Expr_Data_looseBVarRange(uint64_t);
uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
uint64_t l_Lean_Expr_mkData(size_t, lean_object*, uint8_t, uint8_t, uint8_t, uint8_t);
lean_object* l_monadInhabited___rarg(lean_object*, lean_object*);
lean_object* l_Lean_ExprStructEq_HasBeq;
uint8_t lean_expr_has_level_param(lean_object*);
lean_object* _init_l_Lean_Literal_inhabited___closed__1() {
@ -4377,16 +4386,6 @@ x_6 = lean_expr_mk_local(x_1, x_2, x_3, x_5);
return x_6;
}
}
lean_object* l_Lean_mkCApp(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_3 = lean_box(0);
x_4 = l_Lean_mkConst(x_1, x_3);
x_5 = l_Lean_mkApp(x_4, x_2);
return x_5;
}
}
lean_object* l_Array_iterateMAux___main___at_Lean_mkAppN___spec__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
@ -5420,7 +5419,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_1 = l___private_Init_Lean_Expr_1__Expr_mkDataCore___closed__1;
x_2 = lean_unsigned_to_nat(476u);
x_2 = lean_unsigned_to_nat(473u);
x_3 = lean_unsigned_to_nat(20u);
x_4 = l_List_get_x21___main___rarg___closed__2;
x_5 = l___private_Init_Util_1__mkPanicMessage(x_1, x_2, x_3, x_4);
@ -5674,7 +5673,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_1 = l___private_Init_Lean_Expr_1__Expr_mkDataCore___closed__1;
x_2 = lean_unsigned_to_nat(496u);
x_2 = lean_unsigned_to_nat(493u);
x_3 = lean_unsigned_to_nat(15u);
x_4 = l_Lean_Expr_appFn_x21___closed__1;
x_5 = l___private_Init_Util_1__mkPanicMessage(x_1, x_2, x_3, x_4);
@ -5715,7 +5714,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_1 = l___private_Init_Lean_Expr_1__Expr_mkDataCore___closed__1;
x_2 = lean_unsigned_to_nat(500u);
x_2 = lean_unsigned_to_nat(497u);
x_3 = lean_unsigned_to_nat(15u);
x_4 = l_Lean_Expr_appFn_x21___closed__1;
x_5 = l___private_Init_Util_1__mkPanicMessage(x_1, x_2, x_3, x_4);
@ -5764,7 +5763,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_1 = l___private_Init_Lean_Expr_1__Expr_mkDataCore___closed__1;
x_2 = lean_unsigned_to_nat(504u);
x_2 = lean_unsigned_to_nat(501u);
x_3 = lean_unsigned_to_nat(17u);
x_4 = l_Lean_Expr_constName_x21___closed__1;
x_5 = l___private_Init_Util_1__mkPanicMessage(x_1, x_2, x_3, x_4);
@ -5803,9 +5802,19 @@ return x_2;
lean_object* _init_l_Lean_Expr_constLevels_x21___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_List_Monad;
x_2 = l_Lean_Level_Inhabited;
x_3 = l_monadInhabited___rarg(x_1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Expr_constLevels_x21___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_1 = l___private_Init_Lean_Expr_1__Expr_mkDataCore___closed__1;
x_2 = lean_unsigned_to_nat(508u);
x_2 = lean_unsigned_to_nat(505u);
x_3 = lean_unsigned_to_nat(18u);
x_4 = l_Lean_Expr_constName_x21___closed__1;
x_5 = l___private_Init_Util_1__mkPanicMessage(x_1, x_2, x_3, x_4);
@ -5825,8 +5834,8 @@ return x_2;
else
{
lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_3 = lean_box(0);
x_4 = l_Lean_Expr_constLevels_x21___closed__1;
x_3 = l_Lean_Expr_constLevels_x21___closed__1;
x_4 = l_Lean_Expr_constLevels_x21___closed__2;
x_5 = lean_panic_fn(x_4);
return x_5;
}
@ -5854,7 +5863,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_1 = l___private_Init_Lean_Expr_1__Expr_mkDataCore___closed__1;
x_2 = lean_unsigned_to_nat(512u);
x_2 = lean_unsigned_to_nat(509u);
x_3 = lean_unsigned_to_nat(16u);
x_4 = l_Lean_Expr_bvarIdx_x21___closed__1;
x_5 = l___private_Init_Util_1__mkPanicMessage(x_1, x_2, x_3, x_4);
@ -5903,7 +5912,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_1 = l___private_Init_Lean_Expr_1__Expr_mkDataCore___closed__1;
x_2 = lean_unsigned_to_nat(516u);
x_2 = lean_unsigned_to_nat(513u);
x_3 = lean_unsigned_to_nat(14u);
x_4 = l_Lean_Expr_fvarId_x21___closed__1;
x_5 = l___private_Init_Util_1__mkPanicMessage(x_1, x_2, x_3, x_4);
@ -5952,7 +5961,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_1 = l___private_Init_Lean_Expr_1__Expr_mkDataCore___closed__1;
x_2 = lean_unsigned_to_nat(520u);
x_2 = lean_unsigned_to_nat(517u);
x_3 = lean_unsigned_to_nat(14u);
x_4 = l_Lean_Expr_mvarId_x21___closed__1;
x_5 = l___private_Init_Util_1__mkPanicMessage(x_1, x_2, x_3, x_4);
@ -6001,7 +6010,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_1 = l___private_Init_Lean_Expr_1__Expr_mkDataCore___closed__1;
x_2 = lean_unsigned_to_nat(525u);
x_2 = lean_unsigned_to_nat(522u);
x_3 = lean_unsigned_to_nat(21u);
x_4 = l_Lean_Expr_bindingName_x21___closed__1;
x_5 = l___private_Init_Util_1__mkPanicMessage(x_1, x_2, x_3, x_4);
@ -6051,7 +6060,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_1 = l___private_Init_Lean_Expr_1__Expr_mkDataCore___closed__1;
x_2 = lean_unsigned_to_nat(530u);
x_2 = lean_unsigned_to_nat(527u);
x_3 = lean_unsigned_to_nat(21u);
x_4 = l_Lean_Expr_bindingName_x21___closed__1;
x_5 = l___private_Init_Util_1__mkPanicMessage(x_1, x_2, x_3, x_4);
@ -6101,7 +6110,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_1 = l___private_Init_Lean_Expr_1__Expr_mkDataCore___closed__1;
x_2 = lean_unsigned_to_nat(535u);
x_2 = lean_unsigned_to_nat(532u);
x_3 = lean_unsigned_to_nat(21u);
x_4 = l_Lean_Expr_bindingName_x21___closed__1;
x_5 = l___private_Init_Util_1__mkPanicMessage(x_1, x_2, x_3, x_4);
@ -6159,7 +6168,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_1 = l___private_Init_Lean_Expr_1__Expr_mkDataCore___closed__1;
x_2 = lean_unsigned_to_nat(539u);
x_2 = lean_unsigned_to_nat(536u);
x_3 = lean_unsigned_to_nat(20u);
x_4 = l_Lean_Expr_letName_x21___closed__1;
x_5 = l___private_Init_Util_1__mkPanicMessage(x_1, x_2, x_3, x_4);
@ -6324,26 +6333,6 @@ x_1 = l_Lean_Expr_HasToString___closed__1;
return x_1;
}
}
lean_object* l_Lean_mkCAppN(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_3 = lean_box(0);
x_4 = l_Lean_mkConst(x_1, x_3);
x_5 = lean_unsigned_to_nat(0u);
x_6 = l_Array_iterateMAux___main___at_Lean_mkAppN___spec__1(x_2, x_2, x_5, x_4);
return x_6;
}
}
lean_object* l_Lean_mkCAppN___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3;
x_3 = l_Lean_mkCAppN(x_1, x_2);
lean_dec(x_2);
return x_3;
}
}
lean_object* l_Lean_mkAppB(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
@ -6353,16 +6342,86 @@ x_5 = l_Lean_mkApp(x_4, x_3);
return x_5;
}
}
lean_object* l_Lean_mkCAppB(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
lean_object* l_Lean_mkApp2(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_4 = lean_box(0);
x_5 = l_Lean_mkConst(x_1, x_4);
x_6 = l_Lean_mkAppB(x_5, x_2, x_3);
lean_object* x_4;
x_4 = l_Lean_mkAppB(x_1, x_2, x_3);
return x_4;
}
}
lean_object* l_Lean_mkApp3(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;
x_5 = l_Lean_mkAppB(x_1, x_2, x_3);
x_6 = l_Lean_mkApp(x_5, x_4);
return x_6;
}
}
lean_object* l_Lean_mkApp4(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
_start:
{
lean_object* x_6; lean_object* x_7;
x_6 = l_Lean_mkAppB(x_1, x_2, x_3);
x_7 = l_Lean_mkAppB(x_6, x_4, x_5);
return x_7;
}
}
lean_object* l_Lean_mkApp5(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
_start:
{
lean_object* x_7; lean_object* x_8;
x_7 = l_Lean_mkApp4(x_1, x_2, x_3, x_4, x_5);
x_8 = l_Lean_mkApp(x_7, x_6);
return x_8;
}
}
lean_object* l_Lean_mkApp6(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7) {
_start:
{
lean_object* x_8; lean_object* x_9;
x_8 = l_Lean_mkApp4(x_1, x_2, x_3, x_4, x_5);
x_9 = l_Lean_mkAppB(x_8, x_6, x_7);
return x_9;
}
}
lean_object* l_Lean_mkApp7(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8) {
_start:
{
lean_object* x_9; lean_object* x_10;
x_9 = l_Lean_mkApp4(x_1, x_2, x_3, x_4, x_5);
x_10 = l_Lean_mkApp3(x_9, x_6, x_7, x_8);
return x_10;
}
}
lean_object* l_Lean_mkApp8(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9) {
_start:
{
lean_object* x_10; lean_object* x_11;
x_10 = l_Lean_mkApp4(x_1, x_2, x_3, x_4, x_5);
x_11 = l_Lean_mkApp4(x_10, x_6, x_7, x_8, x_9);
return x_11;
}
}
lean_object* l_Lean_mkApp9(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10) {
_start:
{
lean_object* x_11; lean_object* x_12;
x_11 = l_Lean_mkApp4(x_1, x_2, x_3, x_4, x_5);
x_12 = l_Lean_mkApp5(x_11, x_6, x_7, x_8, x_9, x_10);
return x_12;
}
}
lean_object* l_Lean_mkApp10(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10, lean_object* x_11) {
_start:
{
lean_object* x_12; lean_object* x_13;
x_12 = l_Lean_mkApp4(x_1, x_2, x_3, x_4, x_5);
x_13 = l_Lean_mkApp6(x_12, x_6, x_7, x_8, x_9, x_10, x_11);
return x_13;
}
}
lean_object* _init_l_Lean_mkDecIsTrue___closed__1() {
_start:
{
@ -7190,7 +7249,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_1 = l___private_Init_Lean_Expr_1__Expr_mkDataCore___closed__1;
x_2 = lean_unsigned_to_nat(727u);
x_2 = lean_unsigned_to_nat(726u);
x_3 = lean_unsigned_to_nat(18u);
x_4 = l_Lean_Expr_appFn_x21___closed__1;
x_5 = l___private_Init_Util_1__mkPanicMessage(x_1, x_2, x_3, x_4);
@ -7232,7 +7291,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_1 = l___private_Init_Lean_Expr_1__Expr_mkDataCore___closed__1;
x_2 = lean_unsigned_to_nat(736u);
x_2 = lean_unsigned_to_nat(735u);
x_3 = lean_unsigned_to_nat(18u);
x_4 = l_Lean_Expr_constName_x21___closed__1;
x_5 = l___private_Init_Util_1__mkPanicMessage(x_1, x_2, x_3, x_4);
@ -7281,7 +7340,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_1 = l___private_Init_Lean_Expr_1__Expr_mkDataCore___closed__1;
x_2 = lean_unsigned_to_nat(745u);
x_2 = lean_unsigned_to_nat(744u);
x_3 = lean_unsigned_to_nat(14u);
x_4 = l_Lean_Expr_updateSort_x21___closed__1;
x_5 = l___private_Init_Util_1__mkPanicMessage(x_1, x_2, x_3, x_4);
@ -7338,7 +7397,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_1 = l___private_Init_Lean_Expr_1__Expr_mkDataCore___closed__1;
x_2 = lean_unsigned_to_nat(762u);
x_2 = lean_unsigned_to_nat(761u);
x_3 = lean_unsigned_to_nat(17u);
x_4 = l_Lean_Expr_updateMData_x21___closed__1;
x_5 = l___private_Init_Util_1__mkPanicMessage(x_1, x_2, x_3, x_4);
@ -7379,7 +7438,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_1 = l___private_Init_Lean_Expr_1__Expr_mkDataCore___closed__1;
x_2 = lean_unsigned_to_nat(767u);
x_2 = lean_unsigned_to_nat(766u);
x_3 = lean_unsigned_to_nat(18u);
x_4 = l_Lean_Expr_updateProj_x21___closed__1;
x_5 = l___private_Init_Util_1__mkPanicMessage(x_1, x_2, x_3, x_4);
@ -7430,7 +7489,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_1 = l___private_Init_Lean_Expr_1__Expr_mkDataCore___closed__1;
x_2 = lean_unsigned_to_nat(776u);
x_2 = lean_unsigned_to_nat(775u);
x_3 = lean_unsigned_to_nat(21u);
x_4 = l_Lean_Expr_updateForall_x21___closed__1;
x_5 = l___private_Init_Util_1__mkPanicMessage(x_1, x_2, x_3, x_4);
@ -7474,7 +7533,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_1 = l___private_Init_Lean_Expr_1__Expr_mkDataCore___closed__1;
x_2 = lean_unsigned_to_nat(781u);
x_2 = lean_unsigned_to_nat(780u);
x_3 = lean_unsigned_to_nat(21u);
x_4 = l_Lean_Expr_updateForall_x21___closed__1;
x_5 = l___private_Init_Util_1__mkPanicMessage(x_1, x_2, x_3, x_4);
@ -7528,7 +7587,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_1 = l___private_Init_Lean_Expr_1__Expr_mkDataCore___closed__1;
x_2 = lean_unsigned_to_nat(790u);
x_2 = lean_unsigned_to_nat(789u);
x_3 = lean_unsigned_to_nat(17u);
x_4 = l_Lean_Expr_updateLambda_x21___closed__1;
x_5 = l___private_Init_Util_1__mkPanicMessage(x_1, x_2, x_3, x_4);
@ -7572,7 +7631,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_1 = l___private_Init_Lean_Expr_1__Expr_mkDataCore___closed__1;
x_2 = lean_unsigned_to_nat(795u);
x_2 = lean_unsigned_to_nat(794u);
x_3 = lean_unsigned_to_nat(17u);
x_4 = l_Lean_Expr_updateLambda_x21___closed__1;
x_5 = l___private_Init_Util_1__mkPanicMessage(x_1, x_2, x_3, x_4);
@ -7616,7 +7675,7 @@ _start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_1 = l___private_Init_Lean_Expr_1__Expr_mkDataCore___closed__1;
x_2 = lean_unsigned_to_nat(804u);
x_2 = lean_unsigned_to_nat(803u);
x_3 = lean_unsigned_to_nat(20u);
x_4 = l_Lean_Expr_letName_x21___closed__1;
x_5 = l___private_Init_Util_1__mkPanicMessage(x_1, x_2, x_3, x_4);
@ -9434,23 +9493,17 @@ lean_dec(x_2);
return x_4;
}
}
lean_object* initialize_Init_Lean_Level(lean_object*);
lean_object* initialize_Init_Lean_KVMap(lean_object*);
lean_object* initialize_Init_Data_HashMap(lean_object*);
lean_object* initialize_Init_Data_HashSet(lean_object*);
lean_object* initialize_Init_Data_PersistentHashMap(lean_object*);
lean_object* initialize_Init_Data_PersistentHashSet(lean_object*);
lean_object* initialize_Init_Lean_Data_KVMap(lean_object*);
lean_object* initialize_Init_Lean_Level(lean_object*);
static bool _G_initialized = false;
lean_object* initialize_Init_Lean_Expr(lean_object* w) {
lean_object * res;
if (_G_initialized) return lean_mk_io_result(lean_box(0));
_G_initialized = true;
res = initialize_Init_Lean_Level(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Init_Lean_KVMap(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Init_Data_HashMap(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
@ -9463,6 +9516,12 @@ lean_dec_ref(res);
res = initialize_Init_Data_PersistentHashSet(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Init_Lean_Data_KVMap(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Init_Lean_Level(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l_Lean_Literal_inhabited___closed__1 = _init_l_Lean_Literal_inhabited___closed__1();
lean_mark_persistent(l_Lean_Literal_inhabited___closed__1);
l_Lean_Literal_inhabited = _init_l_Lean_Literal_inhabited();
@ -9549,6 +9608,8 @@ l_Lean_Expr_constName_x21___closed__2 = _init_l_Lean_Expr_constName_x21___closed
lean_mark_persistent(l_Lean_Expr_constName_x21___closed__2);
l_Lean_Expr_constLevels_x21___closed__1 = _init_l_Lean_Expr_constLevels_x21___closed__1();
lean_mark_persistent(l_Lean_Expr_constLevels_x21___closed__1);
l_Lean_Expr_constLevels_x21___closed__2 = _init_l_Lean_Expr_constLevels_x21___closed__2();
lean_mark_persistent(l_Lean_Expr_constLevels_x21___closed__2);
l_Lean_Expr_bvarIdx_x21___closed__1 = _init_l_Lean_Expr_bvarIdx_x21___closed__1();
lean_mark_persistent(l_Lean_Expr_bvarIdx_x21___closed__1);
l_Lean_Expr_bvarIdx_x21___closed__2 = _init_l_Lean_Expr_bvarIdx_x21___closed__2();

10
stage0/stdlib/Init/Lean/Level.c
View file

@ -1,6 +1,6 @@
// Lean compiler output
// Module: Init.Lean.Level
// Imports: Init.Data.Option.Basic Init.Data.HashMap Init.Data.PersistentHashMap Init.Lean.Name Init.Lean.Format
// Imports: Init.Data.Option.Basic Init.Data.HashMap Init.Data.PersistentHashMap Init.Lean.Data.Name Init.Lean.Data.Format
#include "runtime/lean.h"
#if defined(__clang__)
#pragma clang diagnostic ignored "-Wunused-parameter"
@ -4078,8 +4078,8 @@ return x_2;
lean_object* initialize_Init_Data_Option_Basic(lean_object*);
lean_object* initialize_Init_Data_HashMap(lean_object*);
lean_object* initialize_Init_Data_PersistentHashMap(lean_object*);
lean_object* initialize_Init_Lean_Name(lean_object*);
lean_object* initialize_Init_Lean_Format(lean_object*);
lean_object* initialize_Init_Lean_Data_Name(lean_object*);
lean_object* initialize_Init_Lean_Data_Format(lean_object*);
static bool _G_initialized = false;
lean_object* initialize_Init_Lean_Level(lean_object* w) {
lean_object * res;
@ -4094,10 +4094,10 @@ lean_dec_ref(res);
res = initialize_Init_Data_PersistentHashMap(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Init_Lean_Name(lean_io_mk_world());
res = initialize_Init_Lean_Data_Name(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Init_Lean_Format(lean_io_mk_world());
res = initialize_Init_Lean_Data_Format(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l_Lean_Level_Data_inhabited = _init_l_Lean_Level_Data_inhabited();

6
stage0/stdlib/Init/Lean/Message.c
View file

@ -1,6 +1,6 @@
// Lean compiler output
// Module: Init.Lean.Message
// Imports: Init.Data.ToString Init.Lean.Position Init.Lean.Syntax Init.Lean.MetavarContext Init.Lean.Environment
// Imports: Init.Data.ToString Init.Lean.Data.Position Init.Lean.Syntax Init.Lean.MetavarContext Init.Lean.Environment
#include "runtime/lean.h"
#if defined(__clang__)
#pragma clang diagnostic ignored "-Wunused-parameter"
@ -939,7 +939,7 @@ return x_2;
}
}
lean_object* initialize_Init_Data_ToString(lean_object*);
lean_object* initialize_Init_Lean_Position(lean_object*);
lean_object* initialize_Init_Lean_Data_Position(lean_object*);
lean_object* initialize_Init_Lean_Syntax(lean_object*);
lean_object* initialize_Init_Lean_MetavarContext(lean_object*);
lean_object* initialize_Init_Lean_Environment(lean_object*);
@ -951,7 +951,7 @@ _G_initialized = true;
res = initialize_Init_Data_ToString(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Init_Lean_Position(lean_io_mk_world());
res = initialize_Init_Lean_Data_Position(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Init_Lean_Syntax(lean_io_mk_world());

6
stage0/stdlib/Init/Lean/Meta.c
View file

@ -1,6 +1,6 @@
// Lean compiler output
// Module: Init.Lean.Meta
// Imports: Init.Lean.Meta.Basic Init.Lean.Meta.LevelDefEq Init.Lean.Meta.WHNF Init.Lean.Meta.InferType Init.Lean.Meta.FunInfo Init.Lean.Meta.ExprDefEq Init.Lean.Meta.DiscrTree Init.Lean.Meta.Reduce Init.Lean.Meta.Instances Init.Lean.Meta.AbstractMVars Init.Lean.Meta.SynthInstance
// Imports: Init.Lean.Meta.Basic Init.Lean.Meta.LevelDefEq Init.Lean.Meta.WHNF Init.Lean.Meta.InferType Init.Lean.Meta.FunInfo Init.Lean.Meta.ExprDefEq Init.Lean.Meta.DiscrTree Init.Lean.Meta.Reduce Init.Lean.Meta.Instances Init.Lean.Meta.AbstractMVars Init.Lean.Meta.SynthInstance Init.Lean.Meta.AppBuilder
#include "runtime/lean.h"
#if defined(__clang__)
#pragma clang diagnostic ignored "-Wunused-parameter"
@ -24,6 +24,7 @@ lean_object* initialize_Init_Lean_Meta_Reduce(lean_object*);
lean_object* initialize_Init_Lean_Meta_Instances(lean_object*);
lean_object* initialize_Init_Lean_Meta_AbstractMVars(lean_object*);
lean_object* initialize_Init_Lean_Meta_SynthInstance(lean_object*);
lean_object* initialize_Init_Lean_Meta_AppBuilder(lean_object*);
static bool _G_initialized = false;
lean_object* initialize_Init_Lean_Meta(lean_object* w) {
lean_object * res;
@ -62,6 +63,9 @@ lean_dec_ref(res);
res = initialize_Init_Lean_Meta_SynthInstance(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Init_Lean_Meta_AppBuilder(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

6750
stage0/stdlib/Init/Lean/Meta/AppBuilder.c
View file

File diff suppressed because it is too large Load diff

105
stage0/stdlib/Init/Lean/Meta/Basic.c
View file

@ -1,6 +1,6 @@
// Lean compiler output
// Module: Init.Lean.Meta.Basic
// Imports: Init.Control.Reader Init.Lean.NameGenerator Init.Lean.Environment Init.Lean.LOption Init.Lean.Trace Init.Lean.Class Init.Lean.ReducibilityAttrs Init.Lean.Meta.Exception Init.Lean.Meta.DiscrTreeTypes
// Imports: Init.Control.Reader Init.Lean.Data.LOption Init.Lean.Data.NameGenerator Init.Lean.Environment Init.Lean.Trace Init.Lean.Class Init.Lean.ReducibilityAttrs Init.Lean.Meta.Exception Init.Lean.Meta.DiscrTreeTypes
#include "runtime/lean.h"
#if defined(__clang__)
#pragma clang diagnostic ignored "-Wunused-parameter"
@ -106,6 +106,7 @@ lean_object* l_Lean_Meta_MetaM_inhabited___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Meta_withNewLocalInstances___main___at_Lean_Meta_forallTelescope___spec__4(lean_object*);
lean_object* l_Lean_Meta_withNewLocalInstances___main___at_Lean_Meta_isClassExpensive___main___spec__6(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Meta_Basic_5__forallTelescopeReducingAuxAux___main___at_Lean_Meta_isClassExpensive___main___spec__2(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_withLocalDeclD(lean_object*);
lean_object* l_Lean_Meta_withNewLocalInstances___main___at_Lean_Meta_forallBoundedTelescope___spec__3___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_getConst___boxed(lean_object*, lean_object*, lean_object*);
lean_object* lean_nat_add(lean_object*, lean_object*);
@ -312,6 +313,7 @@ lean_object* l_Lean_Meta_tracer___closed__1;
lean_object* l_Lean_Meta_lambdaTelescope___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Meta_Basic_4__liftMkBindingM___rarg(lean_object*, lean_object*, lean_object*);
lean_object* lean_io_ref_reset(lean_object*, lean_object*);
lean_object* l_Lean_Meta_withLocalDeclD___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_assignLevelMVar___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_isExprMVarAssigned(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_tracer___lambda__1___boxed(lean_object*, lean_object*, lean_object*);
@ -337,6 +339,7 @@ lean_object* l_Lean_registerEnvExtensionUnsafe___at_Lean_Meta_mkMetaExtension___
uint8_t l_Lean_Meta_TransparencyMode_lt(uint8_t, uint8_t);
lean_object* l_Lean_Meta_assignExprMVar___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_mkInferTypeRef(lean_object*);
lean_object* l_Lean_Meta_getConstInfo(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_mkLambda(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_getMVarDecl(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_getTransparency(lean_object*, lean_object*);
@ -358,6 +361,7 @@ lean_object* l_Lean_Meta_getMCtx___rarg(lean_object*);
lean_object* l___private_Init_Lean_Meta_Basic_7__lambdaTelescopeAux___main(lean_object*);
lean_object* l___private_Init_Lean_Meta_Basic_4__liftMkBindingM(lean_object*);
lean_object* l_Lean_Meta_withNewLocalInstances___main___at_Lean_Meta_forallBoundedTelescope___spec__4___rarg(lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_whnfD(lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Meta_Basic_5__forallTelescopeReducingAuxAux___main___at_Lean_Meta_forallTelescopeReducing___spec__2(lean_object*);
lean_object* l_Lean_Meta_mkWHNFRef___closed__1;
lean_object* l_Lean_Meta_mkFreshLevelMVar___rarg(lean_object*);
@ -400,6 +404,7 @@ lean_object* l___private_Init_Lean_Meta_Basic_5__forallTelescopeReducingAuxAux__
lean_object* l_Lean_Meta_getLCtx(lean_object*, lean_object*);
lean_object* l_Lean_Meta_withMCtx(lean_object*);
lean_object* l_Lean_Meta_isClassExpensive(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_getConstInfo___boxed(lean_object*, lean_object*, lean_object*);
lean_object* lean_name_mk_numeral(lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Meta_Basic_9__lambdaMetaTelescopeAux___main___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_shouldReduceAll___boxed(lean_object*, lean_object*);
@ -970,7 +975,7 @@ _start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Meta_mkWHNFRef___lambda__1___closed__1;
x_2 = lean_alloc_ctor(17, 1, 0);
x_2 = lean_alloc_ctor(19, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
}
@ -1026,7 +1031,7 @@ _start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Meta_mkInferTypeRef___lambda__1___closed__1;
x_2 = lean_alloc_ctor(17, 1, 0);
x_2 = lean_alloc_ctor(19, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
}
@ -1082,7 +1087,7 @@ _start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Meta_mkIsExprDefEqAuxRef___lambda__1___closed__1;
x_2 = lean_alloc_ctor(17, 1, 0);
x_2 = lean_alloc_ctor(19, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
}
@ -2252,7 +2257,7 @@ x_7 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_7, 0, x_4);
lean_ctor_set(x_7, 1, x_5);
lean_ctor_set(x_7, 2, x_6);
x_8 = lean_alloc_ctor(16, 2, 0);
x_8 = lean_alloc_ctor(18, 2, 0);
lean_ctor_set(x_8, 0, x_1);
lean_ctor_set(x_8, 1, x_7);
x_9 = lean_alloc_ctor(1, 2, 0);
@ -3824,6 +3829,59 @@ lean_dec(x_2);
return x_4;
}
}
lean_object* l_Lean_Meta_getConstInfo(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_4 = lean_ctor_get(x_3, 0);
lean_inc(x_4);
x_5 = lean_ctor_get(x_3, 1);
lean_inc(x_5);
lean_inc(x_1);
lean_inc(x_4);
x_6 = lean_environment_find(x_4, x_1);
if (lean_obj_tag(x_6) == 0)
{
lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10;
x_7 = lean_ctor_get(x_2, 1);
lean_inc(x_7);
x_8 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_8, 0, x_4);
lean_ctor_set(x_8, 1, x_5);
lean_ctor_set(x_8, 2, x_7);
x_9 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_9, 0, x_1);
lean_ctor_set(x_9, 1, x_8);
x_10 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_10, 0, x_9);
lean_ctor_set(x_10, 1, x_3);
return x_10;
}
else
{
lean_object* x_11; lean_object* x_12;
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_1);
x_11 = lean_ctor_get(x_6, 0);
lean_inc(x_11);
lean_dec(x_6);
x_12 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_12, 0, x_11);
lean_ctor_set(x_12, 1, x_3);
return x_12;
}
}
}
lean_object* l_Lean_Meta_getConstInfo___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
x_4 = l_Lean_Meta_getConstInfo(x_1, x_2, x_3);
lean_dec(x_2);
return x_4;
}
}
lean_object* l_Lean_Meta_getLocalDecl(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
@ -40703,6 +40761,14 @@ return x_31;
}
}
}
lean_object* l_Lean_Meta_whnfD(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
x_4 = l_Lean_Meta_whnfUsingDefault(x_1, x_2, x_3);
return x_4;
}
}
lean_object* l_Lean_Meta_approxDefEq___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
@ -42987,6 +43053,23 @@ x_8 = l_Lean_Meta_withLocalDecl___rarg(x_1, x_2, x_7, x_4, x_5, x_6);
return x_8;
}
}
lean_object* l_Lean_Meta_withLocalDeclD___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
_start:
{
uint8_t x_6; lean_object* x_7;
x_6 = 0;
x_7 = l_Lean_Meta_withLocalDecl___rarg(x_1, x_2, x_6, x_3, x_4, x_5);
return x_7;
}
}
lean_object* l_Lean_Meta_withLocalDeclD(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l_Lean_Meta_withLocalDeclD___rarg), 5, 0);
return x_2;
}
}
lean_object* l_Lean_Meta_withLetDecl___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
_start:
{
@ -45858,9 +45941,9 @@ return x_2;
}
}
lean_object* initialize_Init_Control_Reader(lean_object*);
lean_object* initialize_Init_Lean_NameGenerator(lean_object*);
lean_object* initialize_Init_Lean_Data_LOption(lean_object*);
lean_object* initialize_Init_Lean_Data_NameGenerator(lean_object*);
lean_object* initialize_Init_Lean_Environment(lean_object*);
lean_object* initialize_Init_Lean_LOption(lean_object*);
lean_object* initialize_Init_Lean_Trace(lean_object*);
lean_object* initialize_Init_Lean_Class(lean_object*);
lean_object* initialize_Init_Lean_ReducibilityAttrs(lean_object*);
@ -45874,15 +45957,15 @@ _G_initialized = true;
res = initialize_Init_Control_Reader(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Init_Lean_NameGenerator(lean_io_mk_world());
res = initialize_Init_Lean_Data_LOption(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Init_Lean_Data_NameGenerator(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Init_Lean_Environment(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Init_Lean_LOption(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Init_Lean_Trace(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);

247
stage0/stdlib/Init/Lean/Meta/Exception.c
View file

@ -34,11 +34,13 @@ lean_object* l_Lean_Meta_Exception_toMessageData___closed__31;
lean_object* l_Lean_mkMVar(lean_object*);
extern lean_object* l_Lean_Format_flatten___main___closed__1;
lean_object* l_Lean_Meta_Exception_toMessageData___closed__59;
lean_object* l_Lean_MessageData_arrayExpr_toMessageData___main(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_Exception_toMessageData___closed__43;
lean_object* l_Lean_Meta_Exception_toStr___closed__13;
lean_object* lean_string_append(lean_object*, lean_object*);
lean_object* l_Lean_Meta_Exception_toStr___closed__1;
lean_object* l_Lean_Meta_Exception_toMessageData___closed__26;
lean_object* l_Lean_Meta_Exception_toMessageData___closed__75;
extern lean_object* l_String_splitAux___main___closed__1;
lean_object* l_Lean_Meta_Exception_Inhabited___closed__1;
extern lean_object* l_List_repr___rarg___closed__3;
@ -63,15 +65,18 @@ lean_object* l_Lean_Meta_Exception_toMessageData___closed__34;
lean_object* l_Lean_Meta_Exception_toMessageData___closed__64;
lean_object* l_Lean_Meta_Exception_toMessageData___closed__69;
lean_object* l_Lean_Meta_Exception_toMessageData___closed__11;
lean_object* l_Lean_Meta_Exception_toStr___closed__19;
lean_object* l_Lean_Meta_Exception_toMessageData___closed__19;
lean_object* l_Nat_repr(lean_object*);
extern lean_object* l_Char_HasRepr___closed__1;
extern lean_object* l_Lean_MessageData_coeOfArrayExpr___closed__2;
lean_object* l_Lean_Meta_Exception_toMessageData___closed__44;
lean_object* l_Lean_Meta_Exception_toMessageData___closed__1;
lean_object* lean_name_mk_string(lean_object*, lean_object*);
extern lean_object* l_List_repr___rarg___closed__2;
extern lean_object* l_List_reprAux___main___rarg___closed__1;
lean_object* l_Lean_Meta_Exception_toStr___closed__11;
lean_object* l_Lean_Meta_Exception_toMessageData___closed__74;
lean_object* l_Lean_Meta_Exception_toMessageData___closed__60;
lean_object* l_Lean_Meta_Exception_toMessageData___closed__2;
lean_object* l_Lean_Meta_Exception_toMessageData___closed__47;
@ -98,14 +103,18 @@ lean_object* l_Lean_Meta_Exception_toMessageData___closed__41;
lean_object* l_Lean_mkApp(lean_object*, lean_object*);
lean_object* l_Lean_Meta_Exception_toMessageData___closed__13;
lean_object* l_Lean_Meta_Exception_toMessageData___closed__62;
lean_object* l_Lean_Meta_Exception_toMessageData___closed__72;
lean_object* l_Lean_Meta_Exception_toMessageData___closed__52;
lean_object* l_Lean_Meta_Exception_toMessageData___closed__54;
lean_object* l_Lean_Meta_Exception_toMessageData___closed__29;
lean_object* l_Lean_Meta_Exception_toMessageData___closed__78;
lean_object* l_Lean_Meta_Exception_toStr___closed__10;
lean_object* l_List_toStringAux___main___at_Lean_Meta_Exception_toStr___spec__2(uint8_t, lean_object*);
lean_object* l_Lean_Meta_Exception_toMessageData___closed__10;
lean_object* l_Lean_Meta_Exception_toMessageData___closed__32;
lean_object* l_Lean_Meta_Exception_toMessageData___closed__73;
lean_object* l_Lean_Meta_Exception_toMessageData___closed__7;
lean_object* l_Lean_Meta_Exception_toMessageData___closed__71;
lean_object* l_Lean_Meta_Exception_toMessageData___closed__49;
lean_object* l___private_Init_Lean_Meta_Exception_1__mkCtx(lean_object*, lean_object*);
lean_object* l_Lean_Meta_Exception_toMessageData___closed__24;
@ -114,9 +123,11 @@ lean_object* l_Lean_Meta_Exception_toStr(lean_object*);
lean_object* l_Lean_Meta_Exception_HasToString___closed__1;
lean_object* l_Lean_Meta_Exception_toStr___closed__6;
lean_object* l_Lean_Meta_Exception_toMessageData___closed__68;
lean_object* l_Lean_Meta_Exception_toStr___closed__18;
lean_object* l_Lean_Meta_Exception_toStr___closed__15;
lean_object* l_Lean_Meta_Exception_toMessageData___closed__18;
lean_object* l_Lean_Meta_Exception_toMessageData___closed__30;
lean_object* l_Lean_Meta_Exception_toMessageData___closed__76;
lean_object* l_Lean_Name_toStringWithSep___main(lean_object*, lean_object*);
lean_object* l_Lean_Meta_Exception_toMessageData___closed__5;
lean_object* l_Lean_Meta_Exception_toStr___closed__5;
@ -130,6 +141,7 @@ lean_object* l_Lean_Meta_Exception_toMessageData___closed__15;
lean_object* l_Lean_Meta_Exception_toMessageData___closed__16;
lean_object* l_Lean_Meta_Exception_toStr___closed__14;
lean_object* l_Lean_Meta_Exception_toMessageData___closed__56;
lean_object* l_Lean_Meta_Exception_toMessageData___closed__77;
lean_object* l_Lean_Meta_Exception_toMessageData___closed__66;
lean_object* l_List_toString___at_Lean_Meta_Exception_toStr___spec__1(lean_object*);
lean_object* l_Lean_Meta_Exception_toMessageData___closed__20;
@ -138,7 +150,7 @@ _start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_String_splitAux___main___closed__1;
x_2 = lean_alloc_ctor(17, 1, 0);
x_2 = lean_alloc_ctor(19, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
}
@ -365,6 +377,22 @@ lean_object* _init_l_Lean_Meta_Exception_toStr___closed__17() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("application builder failure");
return x_1;
}
}
lean_object* _init_l_Lean_Meta_Exception_toStr___closed__18() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("type class instance synthesis failed");
return x_1;
}
}
lean_object* _init_l_Lean_Meta_Exception_toStr___closed__19() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("bug");
return x_1;
}
@ -531,18 +559,32 @@ return x_52;
case 17:
{
lean_object* x_53;
x_53 = lean_ctor_get(x_1, 0);
lean_inc(x_53);
lean_dec(x_1);
x_53 = l_Lean_Meta_Exception_toStr___closed__18;
return x_53;
}
default:
case 18:
{
lean_object* x_54;
lean_dec(x_1);
x_54 = l_Lean_Meta_Exception_toStr___closed__13;
x_54 = l_Lean_Meta_Exception_toStr___closed__19;
return x_54;
}
case 19:
{
lean_object* x_55;
x_55 = lean_ctor_get(x_1, 0);
lean_inc(x_55);
lean_dec(x_1);
return x_55;
}
default:
{
lean_object* x_56;
lean_dec(x_1);
x_56 = l_Lean_Meta_Exception_toStr___closed__13;
return x_56;
}
}
}
}
@ -1269,18 +1311,18 @@ lean_object* _init_l_Lean_Meta_Exception_toMessageData___closed__68() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("internal bug");
x_1 = lean_mk_string("appBuilder");
return x_1;
}
}
lean_object* _init_l_Lean_Meta_Exception_toMessageData___closed__69() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Meta_Exception_toMessageData___closed__68;
x_2 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Lean_Meta_Exception_toMessageData___closed__68;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Meta_Exception_toMessageData___closed__70() {
@ -1288,6 +1330,86 @@ _start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Meta_Exception_toMessageData___closed__69;
x_2 = lean_alloc_ctor(4, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
}
}
lean_object* _init_l_Lean_Meta_Exception_toMessageData___closed__71() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Meta_Exception_toMessageData___closed__70;
x_2 = l_Lean_Meta_Exception_toMessageData___closed__4;
x_3 = lean_alloc_ctor(8, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Meta_Exception_toMessageData___closed__72() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("synthInstance");
return x_1;
}
}
lean_object* _init_l_Lean_Meta_Exception_toMessageData___closed__73() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Lean_Meta_Exception_toMessageData___closed__72;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Meta_Exception_toMessageData___closed__74() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Meta_Exception_toMessageData___closed__73;
x_2 = lean_alloc_ctor(4, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
}
}
lean_object* _init_l_Lean_Meta_Exception_toMessageData___closed__75() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_Meta_Exception_toMessageData___closed__74;
x_2 = l_Lean_Meta_Exception_toMessageData___closed__4;
x_3 = lean_alloc_ctor(8, 2, 0);
lean_ctor_set(x_3, 0, x_1);
lean_ctor_set(x_3, 1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_Meta_Exception_toMessageData___closed__76() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("internal bug");
return x_1;
}
}
lean_object* _init_l_Lean_Meta_Exception_toMessageData___closed__77() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Meta_Exception_toMessageData___closed__76;
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__78() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = l_Lean_Meta_Exception_toMessageData___closed__77;
x_2 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_2, 0, x_1);
return x_2;
@ -1617,22 +1739,83 @@ return x_116;
}
case 16:
{
lean_object* x_117;
lean_object* x_117; lean_object* x_118; lean_object* x_119; lean_object* x_120; lean_object* x_121; lean_object* x_122; lean_object* x_123; lean_object* x_124; lean_object* x_125; lean_object* x_126; lean_object* x_127; lean_object* x_128; lean_object* x_129; lean_object* x_130; lean_object* x_131; lean_object* x_132; lean_object* x_133; lean_object* x_134;
x_117 = lean_ctor_get(x_1, 0);
lean_inc(x_117);
x_118 = lean_ctor_get(x_1, 1);
lean_inc(x_118);
x_119 = lean_ctor_get(x_1, 2);
lean_inc(x_119);
x_120 = lean_ctor_get(x_1, 3);
lean_inc(x_120);
lean_dec(x_1);
x_117 = l_Lean_Meta_Exception_toMessageData___closed__70;
return x_117;
x_121 = lean_alloc_ctor(4, 1, 0);
lean_ctor_set(x_121, 0, x_117);
x_122 = l_Lean_Meta_Exception_toMessageData___closed__71;
x_123 = lean_alloc_ctor(8, 2, 0);
lean_ctor_set(x_123, 0, x_122);
lean_ctor_set(x_123, 1, x_121);
x_124 = l_Lean_Meta_Exception_toMessageData___closed__4;
x_125 = lean_alloc_ctor(8, 2, 0);
lean_ctor_set(x_125, 0, x_123);
lean_ctor_set(x_125, 1, x_124);
x_126 = lean_unsigned_to_nat(0u);
x_127 = l_Lean_MessageData_coeOfArrayExpr___closed__2;
x_128 = l_Lean_MessageData_arrayExpr_toMessageData___main(x_119, x_126, x_127);
lean_dec(x_119);
x_129 = lean_alloc_ctor(8, 2, 0);
lean_ctor_set(x_129, 0, x_125);
lean_ctor_set(x_129, 1, x_128);
x_130 = lean_alloc_ctor(8, 2, 0);
lean_ctor_set(x_130, 0, x_129);
lean_ctor_set(x_130, 1, x_124);
x_131 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_131, 0, x_118);
x_132 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_132, 0, x_131);
x_133 = lean_alloc_ctor(8, 2, 0);
lean_ctor_set(x_133, 0, x_130);
lean_ctor_set(x_133, 1, x_132);
x_134 = l___private_Init_Lean_Meta_Exception_1__mkCtx(x_120, x_133);
lean_dec(x_120);
return x_134;
}
case 17:
{
lean_object* x_135; lean_object* x_136; lean_object* x_137; lean_object* x_138; lean_object* x_139; lean_object* x_140;
x_135 = lean_ctor_get(x_1, 0);
lean_inc(x_135);
x_136 = lean_ctor_get(x_1, 1);
lean_inc(x_136);
lean_dec(x_1);
x_137 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_137, 0, x_135);
x_138 = l_Lean_Meta_Exception_toMessageData___closed__75;
x_139 = lean_alloc_ctor(8, 2, 0);
lean_ctor_set(x_139, 0, x_138);
lean_ctor_set(x_139, 1, x_137);
x_140 = l___private_Init_Lean_Meta_Exception_1__mkCtx(x_136, x_139);
lean_dec(x_136);
return x_140;
}
case 18:
{
lean_object* x_141;
lean_dec(x_1);
x_141 = l_Lean_Meta_Exception_toMessageData___closed__78;
return x_141;
}
default:
{
lean_object* x_118; lean_object* x_119; lean_object* x_120;
x_118 = lean_ctor_get(x_1, 0);
lean_inc(x_118);
lean_object* x_142; lean_object* x_143; lean_object* x_144;
x_142 = lean_ctor_get(x_1, 0);
lean_inc(x_142);
lean_dec(x_1);
x_119 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_119, 0, x_118);
x_120 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_120, 0, x_119);
return x_120;
x_143 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_143, 0, x_142);
x_144 = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(x_144, 0, x_143);
return x_144;
}
}
}
@ -1692,6 +1875,10 @@ l_Lean_Meta_Exception_toStr___closed__16 = _init_l_Lean_Meta_Exception_toStr___c
lean_mark_persistent(l_Lean_Meta_Exception_toStr___closed__16);
l_Lean_Meta_Exception_toStr___closed__17 = _init_l_Lean_Meta_Exception_toStr___closed__17();
lean_mark_persistent(l_Lean_Meta_Exception_toStr___closed__17);
l_Lean_Meta_Exception_toStr___closed__18 = _init_l_Lean_Meta_Exception_toStr___closed__18();
lean_mark_persistent(l_Lean_Meta_Exception_toStr___closed__18);
l_Lean_Meta_Exception_toStr___closed__19 = _init_l_Lean_Meta_Exception_toStr___closed__19();
lean_mark_persistent(l_Lean_Meta_Exception_toStr___closed__19);
l_Lean_Meta_Exception_HasToString___closed__1 = _init_l_Lean_Meta_Exception_HasToString___closed__1();
lean_mark_persistent(l_Lean_Meta_Exception_HasToString___closed__1);
l_Lean_Meta_Exception_HasToString = _init_l_Lean_Meta_Exception_HasToString();
@ -1836,6 +2023,22 @@ l_Lean_Meta_Exception_toMessageData___closed__69 = _init_l_Lean_Meta_Exception_t
lean_mark_persistent(l_Lean_Meta_Exception_toMessageData___closed__69);
l_Lean_Meta_Exception_toMessageData___closed__70 = _init_l_Lean_Meta_Exception_toMessageData___closed__70();
lean_mark_persistent(l_Lean_Meta_Exception_toMessageData___closed__70);
l_Lean_Meta_Exception_toMessageData___closed__71 = _init_l_Lean_Meta_Exception_toMessageData___closed__71();
lean_mark_persistent(l_Lean_Meta_Exception_toMessageData___closed__71);
l_Lean_Meta_Exception_toMessageData___closed__72 = _init_l_Lean_Meta_Exception_toMessageData___closed__72();
lean_mark_persistent(l_Lean_Meta_Exception_toMessageData___closed__72);
l_Lean_Meta_Exception_toMessageData___closed__73 = _init_l_Lean_Meta_Exception_toMessageData___closed__73();
lean_mark_persistent(l_Lean_Meta_Exception_toMessageData___closed__73);
l_Lean_Meta_Exception_toMessageData___closed__74 = _init_l_Lean_Meta_Exception_toMessageData___closed__74();
lean_mark_persistent(l_Lean_Meta_Exception_toMessageData___closed__74);
l_Lean_Meta_Exception_toMessageData___closed__75 = _init_l_Lean_Meta_Exception_toMessageData___closed__75();
lean_mark_persistent(l_Lean_Meta_Exception_toMessageData___closed__75);
l_Lean_Meta_Exception_toMessageData___closed__76 = _init_l_Lean_Meta_Exception_toMessageData___closed__76();
lean_mark_persistent(l_Lean_Meta_Exception_toMessageData___closed__76);
l_Lean_Meta_Exception_toMessageData___closed__77 = _init_l_Lean_Meta_Exception_toMessageData___closed__77();
lean_mark_persistent(l_Lean_Meta_Exception_toMessageData___closed__77);
l_Lean_Meta_Exception_toMessageData___closed__78 = _init_l_Lean_Meta_Exception_toMessageData___closed__78();
lean_mark_persistent(l_Lean_Meta_Exception_toMessageData___closed__78);
return lean_mk_io_result(lean_box(0));
}
#ifdef __cplusplus

8
stage0/stdlib/Init/Lean/Meta/InferType.c
View file

@ -1,6 +1,6 @@
// Lean compiler output
// Module: Init.Lean.Meta.InferType
// Imports: Init.Lean.LBool Init.Lean.Meta.Basic
// Imports: Init.Lean.Data.LBool Init.Lean.Meta.Basic
#include "runtime/lean.h"
#if defined(__clang__)
#pragma clang diagnostic ignored "-Wunused-parameter"
@ -1722,7 +1722,7 @@ x_6 = lean_ctor_get(x_4, 1);
lean_inc(x_6);
lean_dec(x_4);
lean_inc(x_2);
x_7 = l_Lean_Meta_whnf(x_5, x_2, x_6);
x_7 = l_Lean_Meta_whnfUsingDefault(x_5, x_2, x_6);
if (lean_obj_tag(x_7) == 0)
{
lean_object* x_8;
@ -7445,14 +7445,14 @@ return x_56;
}
}
}
lean_object* initialize_Init_Lean_LBool(lean_object*);
lean_object* initialize_Init_Lean_Data_LBool(lean_object*);
lean_object* initialize_Init_Lean_Meta_Basic(lean_object*);
static bool _G_initialized = false;
lean_object* initialize_Init_Lean_Meta_InferType(lean_object* w) {
lean_object * res;
if (_G_initialized) return lean_mk_io_result(lean_box(0));
_G_initialized = true;
res = initialize_Init_Lean_LBool(lean_io_mk_world());
res = initialize_Init_Lean_Data_LBool(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Init_Lean_Meta_Basic(lean_io_mk_world());

30
stage0/stdlib/Init/Lean/Meta/Offset.c
View file

@ -1,6 +1,6 @@
// Lean compiler output
// Module: Init.Lean.Meta.Offset
// Imports: Init.Lean.LBool Init.Lean.Meta.InferType
// Imports: Init.Lean.Data.LBool Init.Lean.Meta.InferType
#include "runtime/lean.h"
#if defined(__clang__)
#pragma clang diagnostic ignored "-Wunused-parameter"
@ -14,10 +14,10 @@
extern "C" {
#endif
lean_object* l_Lean_Meta_isExprDefEqAux(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_mkCAppB(lean_object*, lean_object*, lean_object*);
uint8_t lean_name_eq(lean_object*, lean_object*);
lean_object* l_Lean_Meta_evalNat___main___closed__10;
lean_object* l___private_Init_Lean_Meta_Offset_1__getOffset___main(lean_object*);
lean_object* l_Lean_Meta_isDefEqOffset___closed__1;
lean_object* l___private_Init_Lean_Meta_Offset_1__getOffset(lean_object*);
lean_object* l_Lean_Expr_getAppFn___main(lean_object*);
lean_object* l_Lean_Meta_evalNat(lean_object*);
@ -51,6 +51,8 @@ lean_object* l_Lean_Meta_evalNat___main___closed__1;
lean_object* l_Lean_Meta_evalNat___main___boxed(lean_object*);
lean_object* l_Lean_mkNatLit(lean_object*);
lean_object* l___private_Init_Lean_Meta_Offset_2__isOffset(lean_object*);
lean_object* l_Lean_mkAppB(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_mkConst(lean_object*, lean_object*);
extern lean_object* l___private_Init_Lean_Syntax_9__decodeNatLitVal___closed__1;
uint8_t lean_string_dec_eq(lean_object*, lean_object*);
uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
@ -1427,6 +1429,16 @@ return x_38;
}
}
}
lean_object* _init_l_Lean_Meta_isDefEqOffset___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Lean_Meta_evalNat___main___closed__12;
x_3 = l_Lean_mkConst(x_2, x_1);
return x_3;
}
}
lean_object* l_Lean_Meta_isDefEqOffset(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
@ -1728,8 +1740,8 @@ x_81 = lean_nat_sub(x_47, x_78);
lean_dec(x_78);
lean_dec(x_47);
x_82 = l_Lean_mkNatLit(x_81);
x_83 = l_Lean_Meta_evalNat___main___closed__12;
x_84 = l_Lean_mkCAppB(x_83, x_46, x_82);
x_83 = l_Lean_Meta_isDefEqOffset___closed__1;
x_84 = l_Lean_mkAppB(x_83, x_46, x_82);
x_85 = l_Lean_Meta_isExprDefEqAux(x_84, x_77, x_3, x_4);
if (lean_obj_tag(x_85) == 0)
{
@ -1794,8 +1806,8 @@ x_101 = lean_nat_sub(x_78, x_47);
lean_dec(x_47);
lean_dec(x_78);
x_102 = l_Lean_mkNatLit(x_101);
x_103 = l_Lean_Meta_evalNat___main___closed__12;
x_104 = l_Lean_mkCAppB(x_103, x_77, x_102);
x_103 = l_Lean_Meta_isDefEqOffset___closed__1;
x_104 = l_Lean_mkAppB(x_103, x_77, x_102);
x_105 = l_Lean_Meta_isExprDefEqAux(x_46, x_104, x_3, x_4);
if (lean_obj_tag(x_105) == 0)
{
@ -1920,14 +1932,14 @@ return x_136;
}
}
}
lean_object* initialize_Init_Lean_LBool(lean_object*);
lean_object* initialize_Init_Lean_Data_LBool(lean_object*);
lean_object* initialize_Init_Lean_Meta_InferType(lean_object*);
static bool _G_initialized = false;
lean_object* initialize_Init_Lean_Meta_Offset(lean_object* w) {
lean_object * res;
if (_G_initialized) return lean_mk_io_result(lean_box(0));
_G_initialized = true;
res = initialize_Init_Lean_LBool(lean_io_mk_world());
res = initialize_Init_Lean_Data_LBool(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Init_Lean_Meta_InferType(lean_io_mk_world());
@ -1961,6 +1973,8 @@ l_Lean_Meta_evalNat___main___closed__13 = _init_l_Lean_Meta_evalNat___main___clo
lean_mark_persistent(l_Lean_Meta_evalNat___main___closed__13);
l_Lean_Meta_evalNat___main___closed__14 = _init_l_Lean_Meta_evalNat___main___closed__14();
lean_mark_persistent(l_Lean_Meta_evalNat___main___closed__14);
l_Lean_Meta_isDefEqOffset___closed__1 = _init_l_Lean_Meta_isDefEqOffset___closed__1();
lean_mark_persistent(l_Lean_Meta_isDefEqOffset___closed__1);
return lean_mk_io_result(lean_box(0));
}
#ifdef __cplusplus

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

File diff suppressed because it is too large Load diff

14
stage0/stdlib/Init/Lean/MetavarContext.c
View file

@ -1,6 +1,6 @@
// Lean compiler output
// Module: Init.Lean.MetavarContext
// Imports: Init.Data.Nat Init.Data.Option Init.Control.Reader Init.Lean.LocalContext Init.Lean.MonadCache Init.Lean.NameGenerator
// Imports: Init.Control.Reader Init.Data.Nat Init.Data.Option Init.Lean.Data.NameGenerator Init.Lean.LocalContext Init.Lean.MonadCache
#include "runtime/lean.h"
#if defined(__clang__)
#pragma clang diagnostic ignored "-Wunused-parameter"
@ -32968,24 +32968,27 @@ x_4 = l_Lean_MetavarContext_isWellFormed___main(x_1, x_2, x_3);
return x_4;
}
}
lean_object* initialize_Init_Control_Reader(lean_object*);
lean_object* initialize_Init_Data_Nat(lean_object*);
lean_object* initialize_Init_Data_Option(lean_object*);
lean_object* initialize_Init_Control_Reader(lean_object*);
lean_object* initialize_Init_Lean_Data_NameGenerator(lean_object*);
lean_object* initialize_Init_Lean_LocalContext(lean_object*);
lean_object* initialize_Init_Lean_MonadCache(lean_object*);
lean_object* initialize_Init_Lean_NameGenerator(lean_object*);
static bool _G_initialized = false;
lean_object* initialize_Init_Lean_MetavarContext(lean_object* w) {
lean_object * res;
if (_G_initialized) return lean_mk_io_result(lean_box(0));
_G_initialized = true;
res = initialize_Init_Control_Reader(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Init_Data_Nat(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Init_Data_Option(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Init_Control_Reader(lean_io_mk_world());
res = initialize_Init_Lean_Data_NameGenerator(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Init_Lean_LocalContext(lean_io_mk_world());
@ -32994,9 +32997,6 @@ lean_dec_ref(res);
res = initialize_Init_Lean_MonadCache(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Init_Lean_NameGenerator(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l_Lean_LocalInstance_hasBeq___closed__1 = _init_l_Lean_LocalInstance_hasBeq___closed__1();
lean_mark_persistent(l_Lean_LocalInstance_hasBeq___closed__1);
l_Lean_LocalInstance_hasBeq = _init_l_Lean_LocalInstance_hasBeq();

6
stage0/stdlib/Init/Lean/NameGenerator.c
View file

@ -1,6 +1,6 @@
// Lean compiler output
// Module: Init.Lean.NameGenerator
// Imports: Init.Lean.Name
// Imports: Init.Lean.Data.Name
#include "runtime/lean.h"
#if defined(__clang__)
#pragma clang diagnostic ignored "-Wunused-parameter"
@ -160,13 +160,13 @@ return x_17;
}
}
}
lean_object* initialize_Init_Lean_Name(lean_object*);
lean_object* initialize_Init_Lean_Data_Name(lean_object*);
static bool _G_initialized = false;
lean_object* initialize_Init_Lean_NameGenerator(lean_object* w) {
lean_object * res;
if (_G_initialized) return lean_mk_io_result(lean_box(0));
_G_initialized = true;
res = initialize_Init_Lean_Name(lean_io_mk_world());
res = initialize_Init_Lean_Data_Name(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l_Lean_NameGenerator_Inhabited___closed__1 = _init_l_Lean_NameGenerator_Inhabited___closed__1();

6
stage0/stdlib/Init/Lean/Options.c
View file

@ -1,6 +1,6 @@
// Lean compiler output
// Module: Init.Lean.Options
// Imports: Init.System.IO Init.Data.ToString Init.Lean.KVMap
// Imports: Init.System.IO Init.Data.ToString Init.Lean.Data.KVMap
#include "runtime/lean.h"
#if defined(__clang__)
#pragma clang diagnostic ignored "-Wunused-parameter"
@ -1009,7 +1009,7 @@ return x_129;
}
lean_object* initialize_Init_System_IO(lean_object*);
lean_object* initialize_Init_Data_ToString(lean_object*);
lean_object* initialize_Init_Lean_KVMap(lean_object*);
lean_object* initialize_Init_Lean_Data_KVMap(lean_object*);
static bool _G_initialized = false;
lean_object* initialize_Init_Lean_Options(lean_object* w) {
lean_object * res;
@ -1021,7 +1021,7 @@ lean_dec_ref(res);
res = initialize_Init_Data_ToString(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Init_Lean_KVMap(lean_io_mk_world());
res = initialize_Init_Lean_Data_KVMap(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l_Lean_Options_empty = _init_l_Lean_Options_empty();

136
stage0/stdlib/Init/Lean/Parser/Parser.c
View file

@ -1,6 +1,6 @@
// Lean compiler output
// Module: Init.Lean.Parser.Parser
// Imports: Init.Lean.Position Init.Lean.Syntax Init.Lean.ToExpr Init.Lean.Message Init.Lean.Environment Init.Lean.Attributes Init.Lean.Parser.Trie Init.Lean.Parser.Identifier Init.Lean.Compiler.InitAttr
// Imports: Init.Lean.Data.Trie Init.Lean.Data.Position Init.Lean.Syntax Init.Lean.ToExpr Init.Lean.Message Init.Lean.Environment Init.Lean.Attributes Init.Lean.Parser.Identifier Init.Lean.Compiler.InitAttr
#include "runtime/lean.h"
#if defined(__clang__)
#pragma clang diagnostic ignored "-Wunused-parameter"
@ -212,7 +212,6 @@ lean_object* l_Lean_Parser_identFnAux___main___closed__1;
lean_object* l_Lean_Parser_registerBuiltinParserAttribute___lambda__1___closed__3;
lean_object* l_Lean_Parser_symbolInfo___elambda__1(lean_object*);
lean_object* l_Lean_Parser_symbolFnAux___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Parser_Trie_3__findAux___main___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_insertToken___closed__4;
lean_object* l_Lean_Parser_mkNodeToken___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_initCacheForInput___boxed(lean_object*);
@ -242,7 +241,6 @@ lean_object* l_Lean_Parser_charLitFn___rarg___closed__1;
lean_object* l_Lean_Syntax_mfoldArgsAux___main(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_registerBuiltinParserAttribute___lambda__1___closed__2;
extern lean_object* l_joinM___rarg___closed__1;
lean_object* l___private_Init_Lean_Parser_Trie_2__insertAux___main___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_registerPersistentEnvExtensionUnsafe___at_Lean_Parser_mkTokenTableAttribute___spec__2(lean_object*, lean_object*);
lean_object* l_Lean_Parser_ident___closed__1;
lean_object* l_Lean_Parser_finishCommentBlock___main(lean_object*, lean_object*, lean_object*);
@ -515,6 +513,7 @@ lean_object* l_Lean_Parser_takeWhileFn___at_Lean_Parser_binNumberFn___spec__2___
lean_object* l_Lean_Parser_strLitFnAux___main(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_rawIdent___lambda__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_Error_toString___closed__2;
lean_object* l___private_Init_Lean_Data_Trie_3__findAux___main___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Syntax_mfoldArgsAux___main___at_Lean_Syntax_mforSepArgs___spec__1___rarg___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_Syntax_isOfKind___rarg(lean_object*, lean_object*);
lean_object* l_Lean_Parser_longestMatchMkResult(lean_object*, lean_object*);
@ -600,7 +599,6 @@ lean_object* l_Lean_Parser_numLit(uint8_t);
lean_object* l_Lean_Parser_leadingParser___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_registerParserAttribute___lambda__2___closed__2;
lean_object* l_Lean_Parser_hexDigitFn(lean_object*, lean_object*);
lean_object* l_Lean_mkCAppN(lean_object*, lean_object*);
lean_object* l_Lean_Parser_runBuiltinParser___rarg___boxed(lean_object*);
lean_object* l_Lean_Parser_FirstTokens_HasToString___closed__1;
lean_object* l_Lean_Parser_FirstTokens_HasToString;
@ -802,6 +800,7 @@ lean_object* l_unsafeCast(lean_object*, lean_object*, lean_object*, lean_object*
lean_object* l_List_elem___main___at_Lean_Parser_addBuiltinLeadingParser___spec__4___boxed(lean_object*, lean_object*);
uint8_t l_List_isEmpty___rarg(lean_object*);
lean_object* l_Lean_Parser_unicodeSymbolInfo(lean_object*, lean_object*, lean_object*);
lean_object* l_Array_iterateMAux___main___at_Lean_mkAppN___spec__1(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Name_toStringWithSep___main(lean_object*, lean_object*);
lean_object* l_Lean_Parser_ParserState_keepPrevError___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_strAux(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -846,6 +845,7 @@ lean_object* l_Lean_Parser_unicodeSymbolInfo___closed__1;
lean_object* l_Lean_Parser_checkColGe___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_numLitFn___rarg(lean_object*, lean_object*);
lean_object* l_Lean_Parser_unicodeSymbolFn___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Init_Lean_Data_Trie_2__insertAux___main___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_takeWhileFn___at_Lean_Parser_identFnAux___main___spec__1___boxed(lean_object*, lean_object*);
lean_object* l_Lean_Parser_charLitFn___rarg(lean_object*, lean_object*);
lean_object* l_Lean_Syntax_foldArgs___rarg___boxed(lean_object*, lean_object*, lean_object*);
@ -8892,7 +8892,7 @@ if (x_5 == 0)
lean_object* x_6; lean_object* x_7;
x_6 = lean_unsigned_to_nat(0u);
lean_inc(x_3);
x_7 = l___private_Init_Lean_Parser_Trie_3__findAux___main___rarg(x_1, x_3, x_6);
x_7 = l___private_Init_Lean_Data_Trie_3__findAux___main___rarg(x_1, x_3, x_6);
if (lean_obj_tag(x_7) == 0)
{
lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11;
@ -8902,7 +8902,7 @@ x_9 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_9, 0, x_1);
lean_ctor_set(x_9, 1, x_2);
lean_ctor_set(x_9, 2, x_8);
x_10 = l___private_Init_Lean_Parser_Trie_2__insertAux___main___rarg(x_1, x_9, x_3, x_6);
x_10 = l___private_Init_Lean_Data_Trie_2__insertAux___main___rarg(x_1, x_9, x_3, x_6);
lean_dec(x_1);
x_11 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_11, 0, x_10);
@ -8937,7 +8937,7 @@ lean_object* x_16; lean_object* x_17; lean_object* x_18;
x_16 = lean_ctor_get(x_13, 1);
lean_dec(x_16);
lean_ctor_set(x_13, 1, x_2);
x_17 = l___private_Init_Lean_Parser_Trie_2__insertAux___main___rarg(x_1, x_13, x_3, x_6);
x_17 = l___private_Init_Lean_Data_Trie_2__insertAux___main___rarg(x_1, x_13, x_3, x_6);
lean_dec(x_1);
x_18 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_18, 0, x_17);
@ -8955,7 +8955,7 @@ x_21 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_21, 0, x_19);
lean_ctor_set(x_21, 1, x_2);
lean_ctor_set(x_21, 2, x_20);
x_22 = l___private_Init_Lean_Parser_Trie_2__insertAux___main___rarg(x_1, x_21, x_3, x_6);
x_22 = l___private_Init_Lean_Data_Trie_2__insertAux___main___rarg(x_1, x_21, x_3, x_6);
lean_dec(x_1);
x_23 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_23, 0, x_22);
@ -9847,7 +9847,7 @@ if (x_5 == 0)
lean_object* x_6; lean_object* x_7;
x_6 = lean_unsigned_to_nat(0u);
lean_inc(x_3);
x_7 = l___private_Init_Lean_Parser_Trie_3__findAux___main___rarg(x_1, x_3, x_6);
x_7 = l___private_Init_Lean_Data_Trie_3__findAux___main___rarg(x_1, x_3, x_6);
if (lean_obj_tag(x_7) == 0)
{
lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11;
@ -9857,7 +9857,7 @@ x_9 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_9, 0, x_1);
lean_ctor_set(x_9, 1, x_8);
lean_ctor_set(x_9, 2, x_2);
x_10 = l___private_Init_Lean_Parser_Trie_2__insertAux___main___rarg(x_1, x_9, x_3, x_6);
x_10 = l___private_Init_Lean_Data_Trie_2__insertAux___main___rarg(x_1, x_9, x_3, x_6);
lean_dec(x_1);
x_11 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_11, 0, x_10);
@ -9892,7 +9892,7 @@ lean_object* x_16; lean_object* x_17; lean_object* x_18;
x_16 = lean_ctor_get(x_13, 2);
lean_dec(x_16);
lean_ctor_set(x_13, 2, x_2);
x_17 = l___private_Init_Lean_Parser_Trie_2__insertAux___main___rarg(x_1, x_13, x_3, x_6);
x_17 = l___private_Init_Lean_Data_Trie_2__insertAux___main___rarg(x_1, x_13, x_3, x_6);
lean_dec(x_1);
x_18 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_18, 0, x_17);
@ -9910,7 +9910,7 @@ x_21 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_21, 0, x_19);
lean_ctor_set(x_21, 1, x_20);
lean_ctor_set(x_21, 2, x_2);
x_22 = l___private_Init_Lean_Parser_Trie_2__insertAux___main___rarg(x_1, x_21, x_3, x_6);
x_22 = l___private_Init_Lean_Data_Trie_2__insertAux___main___rarg(x_1, x_21, x_3, x_6);
lean_dec(x_1);
x_23 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_23, 0, x_22);
@ -26680,70 +26680,72 @@ return x_1;
lean_object* l_Lean_Parser_declareBuiltinParser(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
_start:
{
lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; 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; lean_object* x_18; lean_object* x_19; uint8_t x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; lean_object* x_24;
lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9; 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; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; uint8_t x_22; lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26;
x_6 = l_Lean_Parser_declareBuiltinParser___closed__2;
lean_inc(x_4);
x_7 = l_Lean_Name_append___main(x_6, x_4);
x_8 = lean_box(0);
x_9 = l_Lean_mkConst(x_3, x_8);
x_9 = l_Lean_mkConst(x_2, x_8);
x_10 = l_Lean_mkConst(x_3, x_8);
lean_inc(x_4);
x_10 = l_Lean_nameToExprAux___main(x_4);
x_11 = l_Lean_nameToExprAux___main(x_4);
lean_inc(x_4);
x_11 = l_Lean_mkConst(x_4, x_8);
x_12 = l_Lean_Parser_declareBuiltinParser___closed__8;
x_13 = lean_array_push(x_12, x_9);
x_12 = l_Lean_mkConst(x_4, x_8);
x_13 = l_Lean_Parser_declareBuiltinParser___closed__8;
x_14 = lean_array_push(x_13, x_10);
x_15 = lean_array_push(x_14, x_11);
x_16 = l_Lean_mkCAppN(x_2, x_15);
lean_dec(x_15);
x_17 = l_Lean_Parser_declareBuiltinParser___closed__7;
x_16 = lean_array_push(x_15, x_12);
x_17 = lean_unsigned_to_nat(0u);
x_18 = l_Array_iterateMAux___main___at_Lean_mkAppN___spec__1(x_16, x_16, x_17, x_9);
lean_dec(x_16);
x_19 = l_Lean_Parser_declareBuiltinParser___closed__7;
lean_inc(x_7);
x_18 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_18, 0, x_7);
lean_ctor_set(x_18, 1, x_8);
lean_ctor_set(x_18, 2, x_17);
x_19 = lean_box(0);
x_20 = 0;
x_21 = lean_alloc_ctor(0, 3, 1);
lean_ctor_set(x_21, 0, x_18);
lean_ctor_set(x_21, 1, x_16);
lean_ctor_set(x_21, 2, x_19);
lean_ctor_set_uint8(x_21, sizeof(void*)*3, x_20);
x_22 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_22, 0, x_21);
x_23 = l_Lean_Options_empty;
x_24 = l_Lean_Environment_addAndCompile(x_1, x_23, x_22);
lean_dec(x_22);
if (lean_obj_tag(x_24) == 0)
{
lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31;
x_20 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_20, 0, x_7);
lean_ctor_set(x_20, 1, x_8);
lean_ctor_set(x_20, 2, x_19);
x_21 = lean_box(0);
x_22 = 0;
x_23 = lean_alloc_ctor(0, 3, 1);
lean_ctor_set(x_23, 0, x_20);
lean_ctor_set(x_23, 1, x_18);
lean_ctor_set(x_23, 2, x_21);
lean_ctor_set_uint8(x_23, sizeof(void*)*3, x_22);
x_24 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_24, 0, x_23);
x_25 = l_Lean_Options_empty;
x_26 = l_Lean_Environment_addAndCompile(x_1, x_25, x_24);
lean_dec(x_24);
lean_dec(x_7);
x_25 = l_Lean_Name_toString___closed__1;
x_26 = l_Lean_Name_toStringWithSep___main(x_25, x_4);
x_27 = l_Lean_Parser_declareBuiltinParser___closed__9;
x_28 = lean_string_append(x_27, x_26);
if (lean_obj_tag(x_26) == 0)
{
lean_object* x_27; lean_object* x_28; lean_object* x_29; lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33;
lean_dec(x_26);
x_29 = l_Char_HasRepr___closed__1;
x_30 = lean_string_append(x_28, x_29);
x_31 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_31, 0, x_30);
lean_ctor_set(x_31, 1, x_5);
return x_31;
lean_dec(x_7);
x_27 = l_Lean_Name_toString___closed__1;
x_28 = l_Lean_Name_toStringWithSep___main(x_27, x_4);
x_29 = l_Lean_Parser_declareBuiltinParser___closed__9;
x_30 = lean_string_append(x_29, x_28);
lean_dec(x_28);
x_31 = l_Char_HasRepr___closed__1;
x_32 = lean_string_append(x_30, x_31);
x_33 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_33, 0, x_32);
lean_ctor_set(x_33, 1, x_5);
return x_33;
}
else
{
lean_object* x_32; lean_object* x_33; lean_object* x_34; lean_object* x_35; lean_object* x_36;
lean_object* x_34; lean_object* x_35; lean_object* x_36; lean_object* x_37; lean_object* x_38;
lean_dec(x_4);
x_32 = lean_ctor_get(x_24, 0);
lean_inc(x_32);
lean_dec(x_24);
x_33 = l_Lean_initAttr;
x_34 = lean_box(0);
x_35 = l_Lean_ParametricAttribute_setParam___rarg(x_33, x_32, x_7, x_34);
x_36 = l_IO_ofExcept___at_Lean_Parser_declareBuiltinParser___spec__1(x_35, x_5);
lean_dec(x_35);
return x_36;
x_34 = lean_ctor_get(x_26, 0);
lean_inc(x_34);
lean_dec(x_26);
x_35 = l_Lean_initAttr;
x_36 = lean_box(0);
x_37 = l_Lean_ParametricAttribute_setParam___rarg(x_35, x_34, x_7, x_36);
x_38 = l_IO_ofExcept___at_Lean_Parser_declareBuiltinParser___spec__1(x_37, x_5);
lean_dec(x_37);
return x_38;
}
}
}
@ -29401,13 +29403,13 @@ lean_dec(x_2);
return x_3;
}
}
lean_object* initialize_Init_Lean_Position(lean_object*);
lean_object* initialize_Init_Lean_Data_Trie(lean_object*);
lean_object* initialize_Init_Lean_Data_Position(lean_object*);
lean_object* initialize_Init_Lean_Syntax(lean_object*);
lean_object* initialize_Init_Lean_ToExpr(lean_object*);
lean_object* initialize_Init_Lean_Message(lean_object*);
lean_object* initialize_Init_Lean_Environment(lean_object*);
lean_object* initialize_Init_Lean_Attributes(lean_object*);
lean_object* initialize_Init_Lean_Parser_Trie(lean_object*);
lean_object* initialize_Init_Lean_Parser_Identifier(lean_object*);
lean_object* initialize_Init_Lean_Compiler_InitAttr(lean_object*);
static bool _G_initialized = false;
@ -29415,7 +29417,10 @@ lean_object* initialize_Init_Lean_Parser_Parser(lean_object* w) {
lean_object * res;
if (_G_initialized) return lean_mk_io_result(lean_box(0));
_G_initialized = true;
res = initialize_Init_Lean_Position(lean_io_mk_world());
res = initialize_Init_Lean_Data_Trie(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Init_Lean_Data_Position(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Init_Lean_Syntax(lean_io_mk_world());
@ -29433,9 +29438,6 @@ lean_dec_ref(res);
res = initialize_Init_Lean_Attributes(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Init_Lean_Parser_Trie(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Init_Lean_Parser_Identifier(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);

6
stage0/stdlib/Init/Lean/Parser/Trie.c
View file

@ -1,6 +1,6 @@
// Lean compiler output
// Module: Init.Lean.Parser.Trie
// Imports: Init.Data.RBMap Init.Lean.Format
// Imports: Init.Data.RBMap Init.Lean.Data.Format
#include "runtime/lean.h"
#if defined(__clang__)
#pragma clang diagnostic ignored "-Wunused-parameter"
@ -10806,7 +10806,7 @@ return x_2;
}
}
lean_object* initialize_Init_Data_RBMap(lean_object*);
lean_object* initialize_Init_Lean_Format(lean_object*);
lean_object* initialize_Init_Lean_Data_Format(lean_object*);
static bool _G_initialized = false;
lean_object* initialize_Init_Lean_Parser_Trie(lean_object* w) {
lean_object * res;
@ -10815,7 +10815,7 @@ _G_initialized = true;
res = initialize_Init_Data_RBMap(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Init_Lean_Format(lean_io_mk_world());
res = initialize_Init_Lean_Data_Format(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l_Lean_Parser_Trie_empty___closed__1 = _init_l_Lean_Parser_Trie_empty___closed__1();

10
stage0/stdlib/Init/Lean/Path.c
View file

@ -1,6 +1,6 @@
// Lean compiler output
// Module: Init.Lean.Path
// Imports: Init.System.IO Init.System.FilePath Init.Data.Array Init.Data.List.Control Init.Lean.Name Init.Data.HashMap Init.Data.Nat.Control
// Imports: Init.System.IO Init.System.FilePath Init.Data.Array Init.Data.List.Control Init.Data.HashMap Init.Data.Nat.Control Init.Lean.Data.Name
#include "runtime/lean.h"
#if defined(__clang__)
#pragma clang diagnostic ignored "-Wunused-parameter"
@ -2621,9 +2621,9 @@ lean_object* initialize_Init_System_IO(lean_object*);
lean_object* initialize_Init_System_FilePath(lean_object*);
lean_object* initialize_Init_Data_Array(lean_object*);
lean_object* initialize_Init_Data_List_Control(lean_object*);
lean_object* initialize_Init_Lean_Name(lean_object*);
lean_object* initialize_Init_Data_HashMap(lean_object*);
lean_object* initialize_Init_Data_Nat_Control(lean_object*);
lean_object* initialize_Init_Lean_Data_Name(lean_object*);
static bool _G_initialized = false;
lean_object* initialize_Init_Lean_Path(lean_object* w) {
lean_object * res;
@ -2641,15 +2641,15 @@ lean_dec_ref(res);
res = initialize_Init_Data_List_Control(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Init_Lean_Name(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Init_Data_HashMap(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Init_Data_Nat_Control(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Init_Lean_Data_Name(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l___private_Init_Lean_Path_1__pathSep___closed__1 = _init_l___private_Init_Lean_Path_1__pathSep___closed__1();
lean_mark_persistent(l___private_Init_Lean_Path_1__pathSep___closed__1);
l___private_Init_Lean_Path_1__pathSep = _init_l___private_Init_Lean_Path_1__pathSep();

6
stage0/stdlib/Init/Lean/Position.c
View file

@ -1,6 +1,6 @@
// Lean compiler output
// Module: Init.Lean.Position
// Imports: Init.Data.Nat Init.Data.RBMap Init.Lean.Format
// Imports: Init.Data.Nat Init.Data.RBMap Init.Lean.Data.Format
#include "runtime/lean.h"
#if defined(__clang__)
#pragma clang diagnostic ignored "-Wunused-parameter"
@ -590,7 +590,7 @@ return x_2;
}
lean_object* initialize_Init_Data_Nat(lean_object*);
lean_object* initialize_Init_Data_RBMap(lean_object*);
lean_object* initialize_Init_Lean_Format(lean_object*);
lean_object* initialize_Init_Lean_Data_Format(lean_object*);
static bool _G_initialized = false;
lean_object* initialize_Init_Lean_Position(lean_object* w) {
lean_object * res;
@ -602,7 +602,7 @@ lean_dec_ref(res);
res = initialize_Init_Data_RBMap(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Init_Lean_Format(lean_io_mk_world());
res = initialize_Init_Lean_Data_Format(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l_Lean_Position_lt___closed__1 = _init_l_Lean_Position_lt___closed__1();

18
stage0/stdlib/Init/Lean/Syntax.c
View file

@ -1,6 +1,6 @@
// Lean compiler output
// Module: Init.Lean.Syntax
// Imports: Init.Lean.Name Init.Lean.Format Init.Data.Array
// Imports: Init.Data.Array Init.Lean.Data.Name Init.Lean.Data.Format
#include "runtime/lean.h"
#if defined(__clang__)
#pragma clang diagnostic ignored "-Wunused-parameter"
@ -5762,23 +5762,23 @@ lean_dec(x_1);
return x_3;
}
}
lean_object* initialize_Init_Lean_Name(lean_object*);
lean_object* initialize_Init_Lean_Format(lean_object*);
lean_object* initialize_Init_Data_Array(lean_object*);
lean_object* initialize_Init_Lean_Data_Name(lean_object*);
lean_object* initialize_Init_Lean_Data_Format(lean_object*);
static bool _G_initialized = false;
lean_object* initialize_Init_Lean_Syntax(lean_object* w) {
lean_object * res;
if (_G_initialized) return lean_mk_io_result(lean_box(0));
_G_initialized = true;
res = initialize_Init_Lean_Name(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Init_Lean_Format(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Init_Data_Array(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Init_Lean_Data_Name(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Init_Lean_Data_Format(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l_Lean_choiceKind___closed__1 = _init_l_Lean_choiceKind___closed__1();
lean_mark_persistent(l_Lean_choiceKind___closed__1);
l_Lean_choiceKind___closed__2 = _init_l_Lean_choiceKind___closed__2();

48
stage0/stdlib/Init/Lean/ToExpr.c
View file

@ -17,22 +17,24 @@ lean_object* l_Lean_nameToExprAux___main___closed__1;
lean_object* l_Lean_nameToExprAux___main___closed__2;
lean_object* l_Lean_nameToExprAux___main___closed__8;
lean_object* l_Lean_nameToExprAux___main___closed__4;
lean_object* l_Lean_mkCAppB(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_nameToExprAux___main___closed__7;
lean_object* l_Lean_nameToExprAux___main___closed__5;
lean_object* l_Lean_natToExpr___closed__1;
lean_object* l_Lean_nameToExprAux___main___closed__3;
extern lean_object* l_joinM___rarg___closed__1;
lean_object* l_Lean_nameToExpr;
lean_object* l_Lean_nameToExpr___closed__1;
lean_object* l_Lean_natToExpr;
lean_object* lean_name_mk_string(lean_object*, lean_object*);
lean_object* l_Lean_nameToExprAux___main___closed__10;
lean_object* l_Lean_nameToExprAux(lean_object*);
lean_object* l_Lean_nameToExprAux___main___closed__9;
lean_object* l_Lean_nameToExprAux___main(lean_object*);
extern lean_object* l_liftRefl___closed__1;
lean_object* l_Lean_mkNatLit(lean_object*);
lean_object* l_Lean_mkStrLit(lean_object*);
lean_object* l_Lean_exprToExpr;
lean_object* l_Lean_nameToExprAux___main___closed__6;
lean_object* l_Lean_mkAppB(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_strToExpr;
lean_object* l_Lean_mkConst(lean_object*, lean_object*);
lean_object* l_Lean_strToExpr___closed__1;
@ -40,7 +42,7 @@ lean_object* _init_l_Lean_exprToExpr() {
_start:
{
lean_object* x_1;
x_1 = l_liftRefl___closed__1;
x_1 = l_joinM___rarg___closed__1;
return x_1;
}
}
@ -131,21 +133,41 @@ return x_3;
lean_object* _init_l_Lean_nameToExprAux___main___closed__7() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("mkNameNum");
return x_1;
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Lean_nameToExprAux___main___closed__6;
x_3 = l_Lean_mkConst(x_2, x_1);
return x_3;
}
}
lean_object* _init_l_Lean_nameToExprAux___main___closed__8() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string("mkNameNum");
return x_1;
}
}
lean_object* _init_l_Lean_nameToExprAux___main___closed__9() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = l_Lean_nameToExprAux___main___closed__4;
x_2 = l_Lean_nameToExprAux___main___closed__7;
x_2 = l_Lean_nameToExprAux___main___closed__8;
x_3 = lean_name_mk_string(x_1, x_2);
return x_3;
}
}
lean_object* _init_l_Lean_nameToExprAux___main___closed__10() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Lean_nameToExprAux___main___closed__9;
x_3 = l_Lean_mkConst(x_2, x_1);
return x_3;
}
}
lean_object* l_Lean_nameToExprAux___main(lean_object* x_1) {
_start:
{
@ -173,8 +195,8 @@ lean_inc(x_11);
lean_dec(x_1);
x_12 = l_Lean_nameToExprAux___main(x_10);
x_13 = l_Lean_mkStrLit(x_11);
x_14 = l_Lean_nameToExprAux___main___closed__6;
x_15 = l_Lean_mkCAppB(x_14, x_12, x_13);
x_14 = l_Lean_nameToExprAux___main___closed__7;
x_15 = l_Lean_mkAppB(x_14, x_12, x_13);
return x_15;
}
default:
@ -187,8 +209,8 @@ lean_inc(x_17);
lean_dec(x_1);
x_18 = l_Lean_nameToExprAux___main(x_16);
x_19 = l_Lean_mkNatLit(x_17);
x_20 = l_Lean_nameToExprAux___main___closed__8;
x_21 = l_Lean_mkCAppB(x_20, x_18, x_19);
x_20 = l_Lean_nameToExprAux___main___closed__10;
x_21 = l_Lean_mkAppB(x_20, x_18, x_19);
return x_21;
}
}
@ -253,6 +275,10 @@ l_Lean_nameToExprAux___main___closed__7 = _init_l_Lean_nameToExprAux___main___cl
lean_mark_persistent(l_Lean_nameToExprAux___main___closed__7);
l_Lean_nameToExprAux___main___closed__8 = _init_l_Lean_nameToExprAux___main___closed__8();
lean_mark_persistent(l_Lean_nameToExprAux___main___closed__8);
l_Lean_nameToExprAux___main___closed__9 = _init_l_Lean_nameToExprAux___main___closed__9();
lean_mark_persistent(l_Lean_nameToExprAux___main___closed__9);
l_Lean_nameToExprAux___main___closed__10 = _init_l_Lean_nameToExprAux___main___closed__10();
lean_mark_persistent(l_Lean_nameToExprAux___main___closed__10);
l_Lean_nameToExpr___closed__1 = _init_l_Lean_nameToExpr___closed__1();
lean_mark_persistent(l_Lean_nameToExpr___closed__1);
l_Lean_nameToExpr = _init_l_Lean_nameToExpr();

6
stage0/stdlib/Init/Lean/Util.c
View file

@ -1,6 +1,6 @@
// Lean compiler output
// Module: Init.Lean.Util
// Imports: Init.System.IO Init.Lean.Position
// Imports: Init.System.IO Init.Lean.Data.Position
#include "runtime/lean.h"
#if defined(__clang__)
#pragma clang diagnostic ignored "-Wunused-parameter"
@ -58,7 +58,7 @@ return x_5;
}
}
lean_object* initialize_Init_System_IO(lean_object*);
lean_object* initialize_Init_Lean_Position(lean_object*);
lean_object* initialize_Init_Lean_Data_Position(lean_object*);
static bool _G_initialized = false;
lean_object* initialize_Init_Lean_Util(lean_object* w) {
lean_object * res;
@ -67,7 +67,7 @@ _G_initialized = true;
res = initialize_Init_System_IO(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Init_Lean_Position(lean_io_mk_world());
res = initialize_Init_Lean_Data_Position(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));