/-
Copyright (c) 2021 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Mario Carneiro
-/
import Lean

/-!
A rudimentary export format, adapted from

with support for lean 4 kernel primitives.
-/
open Lean (HashMap HashSet)

namespace Lean

namespace Export

/- References -/
private opaque 
MethodsRefPointed: NonemptyType
MethodsRefPointed : 
NonemptyType: Type 1
NonemptyType.{0}

private def 
MethodsRef: Type
MethodsRef : 
Type: Type 1
Type := 
MethodsRefPointed: NonemptyType
MethodsRefPointed.
type: NonemptyType → Type ?u.12
type

inductive 
Entry: Sort ?u.14
Entry
| 
name: Name → Entry
name (
n: Name
n : 
Name: Type
Name)
| 
level: Level → Entry
level (
n: Level
n : 
Level: Type
Level)
| 
expr: Expr → Entry
expr (
n: Expr
n : 
Expr: Type
Expr)
| 
defn: Name → Entry
defn (
n: Name
n : 
Name: Type
Name)
deriving 
Inhabited: Sort u → Sort (max1u)
Inhabited

instance: Coe Name Entry
instance : 
Coe: semiOutParam (Sort ?u.759) → Sort ?u.758 → Sort (max(max1?u.759)?u.758)
Coe 
Name: Type
Name 
Entry: Type
Entry := ⟨
Entry.name: Name → Entry
Entry.name⟩
instance: Coe Level Entry
instance : 
Coe: semiOutParam (Sort ?u.803) → Sort ?u.802 → Sort (max(max1?u.803)?u.802)
Coe 
Level: Type
Level 
Entry: Type
Entry := ⟨
Entry.level: Level → Entry
Entry.level⟩
instance: Coe Expr Entry
instance : 
Coe: semiOutParam (Sort ?u.844) → Sort ?u.843 → Sort (max(max1?u.844)?u.843)
Coe 
Expr: Type
Expr 
Entry: Type
Entry := ⟨
Entry.expr: Expr → Entry
Entry.expr⟩

structure 
Alloc: {α : Type u_1} → [inst : BEq α] → [inst_1 : Hashable α] → HashMap α Nat → Nat → Alloc α
Alloc (
α: ?m.884
α) [
BEq: Type ?u.887 → Type ?u.887
BEq 
α: ?m.884
α] [
Hashable: Sort ?u.890 → Sort (max1?u.890)
Hashable 
α: ?m.884
α] where
  
map: {α : Type u_1} → [inst : BEq α] → [inst_1 : Hashable α] → Alloc α → HashMap α Nat
map : 
HashMap: (α : Type ?u.896) → Type ?u.895 → [inst : BEq α] → [inst : Hashable α] → Type (max0?u.896?u.895)
HashMap 
α: ?m.884
α 
Nat: Type
Nat
  
next: {α : Type u_1} → [inst : BEq α] → [inst_1 : Hashable α] → Alloc α → Nat
next : 
Nat: Type
Nat
deriving 
Inhabited: Sort u → Sort (max1u)
Inhabited

structure 
State: Alloc Name → Alloc Level → Alloc Expr → HashSet Name → Array (Bool × Entry) → State
State where
  
names: State → Alloc Name
names : 
Alloc: (α : Type ?u.1773) → [inst : BEq α] → [inst : Hashable α] → Type ?u.1773
Alloc 
Name: Type
Name := ⟨
HashMap.empty: {α : Type ?u.1818} → {β : Type ?u.1817} → [inst : BEq α] → [inst_1 : Hashable α] → HashMap α β
HashMap.empty.
insert: {α : Type ?u.1848} → {β : Type ?u.1847} → {x : BEq α} → {x_1 : Hashable α} → HashMap α β → α → β → HashMap α β
insert 
Name.anonymous: Name
Name.anonymous 
0: ?m.1871
0, 
1: ?m.1880
1⟩
  
levels: State → Alloc Level
levels : 
Alloc: (α : Type ?u.1886) → [inst : BEq α] → [inst : Hashable α] → Type ?u.1886
Alloc 
Level: Type
Level := ⟨
HashMap.empty: {α : Type ?u.1926} → {β : Type ?u.1925} → [inst : BEq α] → [inst_1 : Hashable α] → HashMap α β
HashMap.empty.
insert: {α : Type ?u.1956} → {β : Type ?u.1955} → {x : BEq α} → {x_1 : Hashable α} → HashMap α β → α → β → HashMap α β
insert 
levelZero: Level
levelZero 
0: ?m.1975
0, 
1: ?m.1978
1⟩
  
exprs: State → Alloc Expr
exprs : 
Alloc: (α : Type ?u.1982) → [inst : BEq α] → [inst : Hashable α] → Type ?u.1982
Alloc 
Expr: Type
Expr
  
defs: State → HashSet Name
defs : 
HashSet: (α : Type ?u.1990) → [inst : BEq α] → [inst : Hashable α] → Type ?u.1990
HashSet 
Name: Type
Name
  
stk: State → Array (Bool × Entry)
stk : 
Array: Type ?u.1995 → Type ?u.1995
Array (
Bool: Type
Bool × 
Entry: Type
Entry)
deriving 
Inhabited: Sort u → Sort (max1u)
Inhabited

class 
OfState: {α : Type} →
  [inst : BEq α] → [inst_1 : Hashable α] → (State → Alloc α) → ((Alloc α → Alloc α) → State → State) → OfState α
OfState (
α: Type
α : 
Type: Type 1
Type) [
BEq: Type ?u.3631 → Type ?u.3631
BEq 
α: Type
α] [
Hashable: Sort ?u.3634 → Sort (max1?u.3634)
Hashable 
α: Type
α] where
  
get: {α : Type} → [inst : BEq α] → [inst_1 : Hashable α] → [self : OfState α] → State → Alloc α
get : 
State: Type
State → 
Alloc: (α : Type ?u.3641) → [inst : BEq α] → [inst : Hashable α] → Type ?u.3641
Alloc 
α: Type
α
  
modify: {α : Type} → [inst : BEq α] → [inst_1 : Hashable α] → [self : OfState α] → (Alloc α → Alloc α) → State → State
modify : (
Alloc: (α : Type ?u.3655) → [inst : BEq α] → [inst : Hashable α] → Type ?u.3655
Alloc 
α: Type
α → 
Alloc: (α : Type ?u.3659) → [inst : BEq α] → [inst : Hashable α] → Type ?u.3659
Alloc 
α: Type
α) → 
State: Type
State → 
State: Type
State

instance: OfState Name
instance : 
OfState: (α : Type) → [inst : BEq α] → [inst : Hashable α] → Type
OfState 
Name: Type
Name where
  get 
s: ?m.3686
s := 
s: ?m.3686
s.
names: State → Alloc Name
names
  modify 
f: ?m.3694
f 
s: ?m.3698
s := { 
s: ?m.3698
s with names := 
f: ?m.3694
f 
s: ?m.3698
s.
names: State → Alloc Name
names }

instance: OfState Level
instance : 
OfState: (α : Type) → [inst : BEq α] → [inst : Hashable α] → Type
OfState 
Level: Type
Level where
  get 
s: ?m.4006
s := 
s: ?m.4006
s.
levels: State → Alloc Level
levels
  modify 
f: ?m.4014
f 
s: ?m.4018
s := { 
s: ?m.4018
s with levels := 
f: ?m.4014
f 
s: ?m.4018
s.
levels: State → Alloc Level
levels }

instance: OfState Expr
instance : 
OfState: (α : Type) → [inst : BEq α] → [inst : Hashable α] → Type
OfState 
Expr: Type
Expr where
  get 
s: ?m.4269
s := 
s: ?m.4269
s.
exprs: State → Alloc Expr
exprs
  modify 
f: ?m.4277
f 
s: ?m.4281
s := { 
s: ?m.4281
s with exprs := 
f: ?m.4277
f 
s: ?m.4281
s.
exprs: State → Alloc Expr
exprs }

end Export

abbrev 
ExportM: Type → Type
ExportM := 
StateT: Type ?u.4520 → (Type ?u.4520 → Type ?u.4519) → Type ?u.4520 → Type (max?u.4520?u.4519)
StateT 
Export.State: Type
Export.State 
CoreM: Type → Type
CoreM

namespace Export

def 
alloc: {α : Type} → [inst : BEq α] → [inst_1 : Hashable α] → [inst : OfState α] → α → ExportM Nat
alloc {
α: ?m.4530
α} [
BEq: Type ?u.4533 → Type ?u.4533
BEq 
α: ?m.4530
α] [
Hashable: Sort ?u.4536 → Sort (max1?u.4536)
Hashable 
α: ?m.4530
α] [
OfState: (α : Type) → [inst : BEq α] → [inst : Hashable α] → Type
OfState 
α: ?m.4530
α] (
a: α
a : 
α: ?m.4530
α) : 
ExportM: Type → Type
ExportM 
Nat: Type
Nat := do
  let 
n: ?m.4702
n := (
OfState.get: {α : Type} → [inst : BEq α] → [inst_1 : Hashable α] → [self : OfState α] → State → Alloc α
OfState.get (α := 
α: Type
α) 
(← get): ?m.4699
(← 
get: {σ : outParam (Type ?u.4630)} → {m : Type ?u.4630 → Type ?u.4629} → [self : MonadState σ m] → m σ
get
(← get): ?m.4699
)).
next: {α : Type ?u.4713} → [inst : BEq α] → [inst_1 : Hashable α] → Alloc α → Nat
next
  
modify: {σ : Type ?u.4758} → {m : Type ?u.4758 → Type ?u.4757} → [inst : MonadState σ m] → (σ → σ) → m PUnit
modify $ 
OfState.modify: {α : Type} → [inst : BEq α] → [inst_1 : Hashable α] → [self : OfState α] → (Alloc α → Alloc α) → State → State
OfState.modify (α := 
α: Type
α) fun 
s: ?m.4797
s ↦ {map := 
s: ?m.4797
s.
map: {α : Type ?u.4805} → [inst : BEq α] → [inst_1 : Hashable α] → Alloc α → HashMap α Nat
map.
insert: {α : Type ?u.4810} → {β : Type ?u.4809} → {x : BEq α} → {x_1 : Hashable α} → HashMap α β → α → β → HashMap α β
insert 
a: α
a 
n: ?m.4702
n, next := 
n: ?m.4702
n+
1: ?m.4830
1}
  
pure: {f : Type ?u.4910 → Type ?u.4909} → [self : Pure f] → {α : Type ?u.4910} → α → f α
pure 
n: ?m.4702
n

def 
exportName: Name → ExportM Nat
exportName (
n: Name
n : 
Name: Type
Name) : 
ExportM: Type → Type
ExportM 
Nat: Type
Nat := do
  match 
(← get): ?m.5858
(← 
get: {σ : outParam (Type ?u.5789)} → {m : Type ?u.5789 → Type ?u.5788} → [self : MonadState σ m] → m σ
get
(← get): ?m.5858
).
names: State → Alloc Name
names.
map: {α : Type ?u.5860} → [inst : BEq α] → [inst_1 : Hashable α] → Alloc α → HashMap α Nat
map.
find?: {α : Type ?u.5873} → {β : Type ?u.5872} → {x : BEq α} → {x_1 : Hashable α} → HashMap α β → α → Option β
find? 
n: Name
n with
  | 
some: {α : Type ?u.5889} → α → Option α
some 
i: Nat
i => 
pure: {f : Type ?u.5905 → Type ?u.5904} → [self : Pure f] → {α : Type ?u.5905} → α → f α
pure 
i: Nat
i
  | 
none: {α : Type ?u.6006} → Option α
none => match 
n: Name
n with
    | 
.anonymous: Name
.anonymous => 
pure: {f : Type ?u.6019 → Type ?u.6018} → [self : Pure f] → {α : Type ?u.6019} → α → f α
pure 
0: ?m.6044
0
    | 
.num: Name → Nat → Name
.num 
p: Name
p 
a: Nat
a => let 
i: ?m.6151
i ← 
alloc: {α : Type} → [inst : BEq α] → [inst_1 : Hashable α] → [inst : OfState α] → α → ExportM Nat
alloc 
n: Name
n; 
IO.println: {α : Type ?u.6236} → [inst : ToString α] → α → IO Unit
IO.println s!"{
i: ?m.6151
i} #NI {← 
exportName: Name → ExportM Nat
exportName 
p: Name
p} {
a: Nat
a}"; 
pure: {f : Type ?u.6532 → Type ?u.6531} → [self : Pure f] → {α : Type ?u.6532} → α → f α
pure 
i: ?m.6151
i
    | 
.str: Name → String → Name
.str 
p: Name
p 
s: String
s => let 
i: ?m.6666
i ← 
alloc: {α : Type} → [inst : BEq α] → [inst_1 : Hashable α] → [inst : OfState α] → α → ExportM Nat
alloc 
n: Name
n; 
IO.println: {α : Type ?u.6751} → [inst : ToString α] → α → IO Unit
IO.println s!"{
i: ?m.6666
i} #NS {← 
exportName: Name → ExportM Nat
exportName 
p: Name
p} {
s: String
s}"; 
pure: {f : Type ?u.6937 → Type ?u.6936} → [self : Pure f] → {α : Type ?u.6937} → α → f α
pure 
i: ?m.6666
i

def 
exportLevel: Level → ExportM Nat
exportLevel (
L: Level
L : 
Level: Type
Level) : 
ExportM: Type → Type
ExportM 
Nat: Type
Nat := do
  match 
(← get): ?m.12119
(← 
get: {σ : outParam (Type ?u.12050)} → {m : Type ?u.12050 → Type ?u.12049} → [self : MonadState σ m] → m σ
get
(← get): ?m.12119
).
levels: State → Alloc Level
levels.
map: {α : Type ?u.12121} → [inst : BEq α] → [inst_1 : Hashable α] → Alloc α → HashMap α Nat
map.
find?: {α : Type ?u.12134} → {β : Type ?u.12133} → {x : BEq α} → {x_1 : Hashable α} → HashMap α β → α → Option β
find? 
L: Level
L with
  | 
some: {α : Type ?u.12007} → α → Option α
some 
i: Nat
i => 
pure: {f : Type ?u.12166 → Type ?u.12165} → [self : Pure f] → {α : Type ?u.12166} → α → f α
pure 
i: Nat
i
  | 
none: {α : Type ?u.12011} → Option α
none => match 
L: Level
L with
    | 
.zero: Level
.zero => 
pure: {f : Type ?u.12280 → Type ?u.12279} → [self : Pure f] → {α : Type ?u.12280} → α → f α
pure 
0: ?m.12305
0
    | 
.succ: Level → Level
.succ 
l: Level
l =>
      let 
i: ?m.12407
i ← 
alloc: {α : Type} → [inst : BEq α] → [inst_1 : Hashable α] → [inst : OfState α] → α → ExportM Nat
alloc 
L: Level
L; 
IO.println: {α : Type ?u.12492} → [inst : ToString α] → α → IO Unit
IO.println s!"{
i: ?m.12407
i} #US {← 
exportLevel: Level → ExportM Nat
exportLevel 
l: Level
l}"; 
pure: {f : Type ?u.12740 → Type ?u.12739} → [self : Pure f] → {α : Type ?u.12740} → α → f α
pure 
i: ?m.12407
i
    | 
.max: Level → Level → Level
.max 
l₁: Level
l₁ 
l₂: Level
l₂ =>
      let 
i: ?m.12874
i ← 
alloc: {α : Type} → [inst : BEq α] → [inst_1 : Hashable α] → [inst : OfState α] → α → ExportM Nat
alloc 
L: Level
L; 
IO.println: {α : Type ?u.13006} → [inst : ToString α] → α → IO Unit
IO.println s!"{
i: ?m.12874
i} #UM {← 
exportLevel: Level → ExportM Nat
exportLevel 
l₁: Level
l₁} {← 
exportLevel: Level → ExportM Nat
exportLevel 
l₂: Level
l₂}"; 
pure: {f : Type ?u.13192 → Type ?u.13191} → [self : Pure f] → {α : Type ?u.13192} → α → f α
pure 
i: ?m.12874
i
    | 
.imax: Level → Level → Level
.imax 
l₁: Level
l₁ 
l₂: Level
l₂ =>
      let 
i: ?m.13330
i ← 
alloc: {α : Type} → [inst : BEq α] → [inst_1 : Hashable α] → [inst : OfState α] → α → ExportM Nat
alloc 
L: Level
L; 
IO.println: {α : Type ?u.13462} → [inst : ToString α] → α → IO Unit
IO.println s!"{
i: ?m.13330
i} #UIM {← 
exportLevel: Level → ExportM Nat
exportLevel 
l₁: Level
l₁} {← 
exportLevel: Level → ExportM Nat
exportLevel 
l₂: Level
l₂}"; 
pure: {f : Type ?u.13648 → Type ?u.13647} → [self : Pure f] → {α : Type ?u.13648} → α → f α
pure 
i: ?m.13330
i
    | 
.param: Name → Level
.param 
n: Name
n =>
      let 
i: ?m.13781
i ← 
alloc: {α : Type} → [inst : BEq α] → [inst_1 : Hashable α] → [inst : OfState α] → α → ExportM Nat
alloc 
L: Level
L; 
IO.println: {α : Type ?u.13866} → [inst : ToString α] → α → IO Unit
IO.println s!"{
i: ?m.13781
i} #UP {← 
exportName: Name → ExportM Nat
exportName 
n: Name
n}"; 
pure: {f : Type ?u.14004 → Type ?u.14003} → [self : Pure f] → {α : Type ?u.14004} → α → f α
pure 
i: ?m.13781
i
    | 
.mvar: LMVarId → Level
.mvar _ => 
unreachable!: ?m.14059
unreachable!

def 
biStr: BinderInfo → String
biStr : 
BinderInfo: Type
BinderInfo → 
String: Type
String
| 
BinderInfo.default: BinderInfo
BinderInfo.default        => 
"#BD": String
"#BD"
| 
BinderInfo.implicit: BinderInfo
BinderInfo.implicit       => 
"#BI": String
"#BI"
| 
BinderInfo.strictImplicit: BinderInfo
BinderInfo.strictImplicit => 
"#BS": String
"#BS"
| 
BinderInfo.instImplicit: BinderInfo
BinderInfo.instImplicit   => 
"#BC": String
"#BC"

open ConstantInfo in
mutual

partial def 
exportExpr: Expr → ExportM Nat
exportExpr (
E: Expr
E : 
Expr: Type
Expr) : 
ExportM: Type → Type
ExportM 
Nat: Type
Nat := do
  match 
(← get): ?m.24324
(← 
get: {σ : outParam (Type ?u.24255)} → {m : Type ?u.24255 → Type ?u.24254} → [self : MonadState σ m] → m σ
get
(← get): ?m.24324
).
exprs: State → Alloc Expr
exprs.
map: {α : Type ?u.24326} → [inst : BEq α] → [inst_1 : Hashable α] → Alloc α → HashMap α Nat
map.
find?: {α : Type ?u.24339} → {β : Type ?u.24338} → {x : BEq α} → {x_1 : Hashable α} → HashMap α β → α → Option β
find? 
E: Expr
E with
  | 
some: {α : Type ?u.24355} → α → Option α
some 
i: Nat
i => 
pure: {f : Type ?u.24371 → Type ?u.24370} → [self : Pure f] → {α : Type ?u.24371} → α → f α
pure 
i: Nat
i
  | 
none: {α : Type ?u.24472} → Option α
none => match 
E: Expr
E with
    | 
.bvar: Nat → Expr
.bvar 
n: Nat
n => let 
i: ?m.24570
i ← 
alloc: {α : Type} → [inst : BEq α] → [inst_1 : Hashable α] → [inst : OfState α] → α → ExportM Nat
alloc 
E: Expr
E; 
IO.println: {α : Type ?u.24608} → [inst : ToString α] → α → IO Unit
IO.println s!"{
i: ?m.24570
i} #EV {
n: Nat
n}"; 
pure: {f : Type ?u.24856 → Type ?u.24855} → [self : Pure f] → {α : Type ?u.24856} → α → f α
pure 
i: ?m.24570
i
    | 
.fvar: FVarId → Expr
.fvar _ => 
unreachable!: ?m.24907
unreachable!
    | 
.mvar: MVarId → Expr
.mvar _  => 
unreachable!: ?m.25035
unreachable!
    | 
.sort: Level → Expr
.sort 
l: Level
l => let 
i: ?m.25211
i ← 
alloc: {α : Type} → [inst : BEq α] → [inst_1 : Hashable α] → [inst : OfState α] → α → ExportM Nat
alloc 
E: Expr
E; 
IO.println: {α : Type ?u.25296} → [inst : ToString α] → α → IO Unit
IO.println s!"{
i: ?m.25211
i} #ES {← 
exportLevel: Level → ExportM Nat
exportLevel 
l: Level
l}"; 
pure: {f : Type ?u.25434 → Type ?u.25433} → [self : Pure f] → {α : Type ?u.25434} → α → f α
pure 
i: ?m.25211
i
    | 
.const: Name → List Level → Expr
.const 
n: Name
n 
ls: List Level
ls =>
      
exportDef: Name → ExportM Unit
exportDef 
n: Name
n
      let 
i: ?m.25613
i ← 
alloc: {α : Type} → [inst : BEq α] → [inst_1 : Hashable α] → [inst : OfState α] → α → ExportM Nat
alloc 
E: Expr
E
      let mut 
s: ?m.25663
s := s!"{
i: ?m.25613
i} #EC {← 
exportName: Name → ExportM Nat
exportName 
n: Name
n}"
      for 
l: ?m.25855
l in 
ls: List Level
ls do 
s: ?m.25861
s := 
s: ?m.25861
s ++ 
s!" {← exportLevel l}": ?m.25954
s!
s!" {← exportLevel l}": ?m.25954
" {← 
exportLevel: Level → ExportM Nat
exportLevel
s!" {← exportLevel l}": ?m.25954
 
l: ?m.25855
l
s!" {← exportLevel l}": ?m.25954
}"
      
IO.println: {α : Type ?u.26217} → [inst : ToString α] → α → IO Unit
IO.println 
s: ?m.26179
s; 
pure: {f : Type ?u.26255 → Type ?u.26254} → [self : Pure f] → {α : Type ?u.26255} → α → f α
pure 
i: ?m.25613
i
    | 
.app: Expr → Expr → Expr
.app 
e₁: Expr
e₁ 
e₂: Expr
e₂ =>
      let 
i: ?m.26403
i ← 
alloc: {α : Type} → [inst : BEq α] → [inst_1 : Hashable α] → [inst : OfState α] → α → ExportM Nat
alloc 
E: Expr
E; 
IO.println: {α : Type ?u.26535} → [inst : ToString α] → α → IO Unit
IO.println s!"{
i: ?m.26403
i} #EA {← 
exportExpr: Expr → ExportM Nat
exportExpr 
e₁: Expr
e₁} {← 
exportExpr: Expr → ExportM Nat
exportExpr 
e₂: Expr
e₂}"; 
pure: {f : Type ?u.26721 → Type ?u.26720} → [self : Pure f] → {α : Type ?u.26721} → α → f α
pure 
i: ?m.26403
i
    | 
.lam: Name → Expr → Expr → BinderInfo → Expr
.lam _ 
e₁: Expr
e₁ 
e₂: Expr
e₂ 
d: BinderInfo
d =>
      let 
i: ?m.26868
i ← 
alloc: {α : Type} → [inst : BEq α] → [inst_1 : Hashable α] → [inst : OfState α] → α → ExportM Nat
alloc 
E: Expr
E
      
IO.println: {α : Type ?u.27000} → [inst : ToString α] → α → IO Unit
IO.println s!"{
i: ?m.26868
i} #EL {
biStr: BinderInfo → String
biStr 
d: BinderInfo
d} {← 
exportExpr: Expr → ExportM Nat
exportExpr 
e₁: Expr
e₁} {← 
exportExpr: Expr → ExportM Nat
exportExpr 
e₂: Expr
e₂}"; 
pure: {f : Type ?u.27234 → Type ?u.27233} → [self : Pure f] → {α : Type ?u.27234} → α → f α
pure 
i: ?m.26868
i
    | 
.forallE: Name → Expr → Expr → BinderInfo → Expr
.forallE _ 
e₁: Expr
e₁ 
e₂: Expr
e₂ 
d: BinderInfo
d =>
      let 
i: ?m.27381
i ← 
alloc: {α : Type} → [inst : BEq α] → [inst_1 : Hashable α] → [inst : OfState α] → α → ExportM Nat
alloc 
E: Expr
E
      
IO.println: {α : Type ?u.27513} → [inst : ToString α] → α → IO Unit
IO.println s!"{
i: ?m.27381
i} #EP {
biStr: BinderInfo → String
biStr 
d: BinderInfo
d} {← 
exportExpr: Expr → ExportM Nat
exportExpr 
e₁: Expr
e₁} {← 
exportExpr: Expr → ExportM Nat
exportExpr 
e₂: Expr
e₂}"; 
pure: {f : Type ?u.27747 → Type ?u.27746} → [self : Pure f] → {α : Type ?u.27747} → α → f α
pure 
i: ?m.27381
i
    | 
.letE: Name → Expr → Expr → Expr → Bool → Expr
.letE _ 
e₁: Expr
e₁ 
e₂: Expr
e₂ 
e₃: Expr
e₃ _ =>
      let 
i: ?m.27902
i ← 
alloc: {α : Type} → [inst : BEq α] → [inst_1 : Hashable α] → [inst : OfState α] → α → ExportM Nat
alloc 
E: Expr
E
      
IO.println: {α : Type ?u.28081} → [inst : ToString α] → α → IO Unit
IO.println s!"{
i: ?m.27902
i} #EP {← 
exportExpr: Expr → ExportM Nat
exportExpr 
e₁: Expr
e₁} {← 
exportExpr: Expr → ExportM Nat
exportExpr 
e₂: Expr
e₂} {← 
exportExpr: Expr → ExportM Nat
exportExpr 
e₃: Expr
e₃}"; 
pure: {f : Type ?u.28315 → Type ?u.28314} → [self : Pure f] → {α : Type ?u.28315} → α → f α
pure 
i: ?m.27902
i
    | 
.lit: Literal → Expr
.lit (
.natVal: Nat → Literal
.natVal 
n: Nat
n) => let 
i: ?m.28454
i ← 
alloc: {α : Type} → [inst : BEq α] → [inst_1 : Hashable α] → [inst : OfState α] → α → ExportM Nat
alloc 
E: Expr
E; 
IO.println: {α : Type ?u.28492} → [inst : ToString α] → α → IO Unit
IO.println s!"{
i: ?m.28454
i} #EN {
n: Nat
n}"; 
pure: {f : Type ?u.28630 → Type ?u.28629} → [self : Pure f] → {α : Type ?u.28630} → α → f α
pure 
i: ?m.28454
i
    | 
.lit: Literal → Expr
.lit (
.strVal: String → Literal
.strVal 
s: String
s) => let 
i: ?m.28751
i ← 
alloc: {α : Type} → [inst : BEq α] → [inst_1 : Hashable α] → [inst : OfState α] → α → ExportM Nat
alloc 
E: Expr
E; 
IO.println: {α : Type ?u.28789} → [inst : ToString α] → α → IO Unit
IO.println s!"{
i: ?m.28751
i} #ET {
s: String
s}"; 
pure: {f : Type ?u.28927 → Type ?u.28926} → [self : Pure f] → {α : Type ?u.28927} → α → f α
pure 
i: ?m.28751
i
    | 
.mdata: MData → Expr → Expr
.mdata _ _ => 
unreachable!: ?m.28981
unreachable!
    | 
.proj: Name → Nat → Expr → Expr
.proj 
n: Name
n 
k: Nat
k 
e: Expr
e =>
      let 
i: ?m.29167
i ← 
alloc: {α : Type} → [inst : BEq α] → [inst_1 : Hashable α] → [inst : OfState α] → α → ExportM Nat
alloc 
E: Expr
E; 
IO.println: {α : Type ?u.29299} → [inst : ToString α] → α → IO Unit
IO.println s!"{
i: ?m.29167
i} #EJ {← 
exportName: Name → ExportM Nat
exportName 
n: Name
n} {
k: Nat
k} {← 
exportExpr: Expr → ExportM Nat
exportExpr 
e: Expr
e}"; 
pure: {f : Type ?u.29533 → Type ?u.29532} → [self : Pure f] → {α : Type ?u.29533} → α → f α
pure 
i: ?m.29167
i

partial def 
exportDef: Name → ExportM Unit
exportDef (
n: Name
n : 
Name: Type
Name) : 
ExportM: Type → Type
ExportM 
Unit: Type
Unit := do
  if 
(← get): ?m.36613
(← 
get: {σ : outParam (Type ?u.36545)} → {m : Type ?u.36545 → Type ?u.36544} → [self : MonadState σ m] → m σ
get
(← get): ?m.36613
).
defs: State → HashSet Name
defs.
contains: {α : Type ?u.36624} → {x : BEq α} → {x_1 : Hashable α} → HashSet α → α → Bool
contains 
n: Name
n then 
return: ?m.36730 ?m.36732
return
  let 
ci: ?m.36938
ci ← 
getConstInfo: {m : Type → Type} → [inst : Monad m] → [inst : MonadEnv m] → [inst : MonadError m] → Name → m ConstantInfo
getConstInfo 
n: Name
n
  for 
c: ?m.37025
c in 
ci: ?m.36938
ci.
value!: ConstantInfo → Expr
value!.
getUsedConstants: Expr → Array Name
getUsedConstants do
    unless 
(← get): ?m.37120
(← 
get: {σ : outParam (Type ?u.37067)} → {m : Type ?u.37067 → Type ?u.37066} → [self : MonadState σ m] → m σ
get
(← get): ?m.37120
).
defs: State → HashSet Name
defs.
contains: {α : Type ?u.37122} → {x : BEq α} → {x_1 : Hashable α} → HashSet α → α → Bool
contains 
c: ?m.37025
c do
      
exportDef: Name → ExportM Unit
exportDef 
c: ?m.37025
c
  match 
ci: ?m.36938
ci with
  | 
axiomInfo: AxiomVal → ConstantInfo
axiomInfo   
val: AxiomVal
val => 
axdef: String → Name → Expr → List Name → ExportM Unit
axdef 
"#AX": String
"#AX" 
val: AxiomVal
val.
name: ConstantVal → Name
name 
val: AxiomVal
val.
type: ConstantVal → Expr
type 
val: AxiomVal
val.
levelParams: ConstantVal → List Name
levelParams
  | 
defnInfo: DefinitionVal → ConstantInfo
defnInfo    
val: DefinitionVal
val => 
defn: String → Name → Expr → Expr → List Name → ExportM Unit
defn 
"#DEF": String
"#DEF" 
val: DefinitionVal
val.
name: ConstantVal → Name
name 
val: DefinitionVal
val.
type: ConstantVal → Expr
type 
val: DefinitionVal
val.
value: DefinitionVal → Expr
value 
val: DefinitionVal
val.
levelParams: ConstantVal → List Name
levelParams
  | 
thmInfo: TheoremVal → ConstantInfo
thmInfo     
val: TheoremVal
val => 
defn: String → Name → Expr → Expr → List Name → ExportM Unit
defn 
"#THM": String
"#THM" 
val: TheoremVal
val.
name: ConstantVal → Name
name 
val: TheoremVal
val.
type: ConstantVal → Expr
type 
val: TheoremVal
val.
value: TheoremVal → Expr
value 
val: TheoremVal
val.
levelParams: ConstantVal → List Name
levelParams
  | 
opaqueInfo: OpaqueVal → ConstantInfo
opaqueInfo  
val: OpaqueVal
val => 
defn: String → Name → Expr → Expr → List Name → ExportM Unit
defn 
"#CN": String
"#CN" 
val: OpaqueVal
val.
name: ConstantVal → Name
name 
val: OpaqueVal
val.
type: ConstantVal → Expr
type 
val: OpaqueVal
val.
value: OpaqueVal → Expr
value 
val: OpaqueVal
val.
levelParams: ConstantVal → List Name
levelParams
  | 
quotInfo: QuotVal → ConstantInfo
quotInfo    _ =>
    
IO.println: {α : Type ?u.37536} → [inst : ToString α] → α → IO Unit
IO.println 
"#QUOT": String
"#QUOT"
    for 
n: ?m.37751
n in [``
Quot: {α : Sort u} → (α → α → Prop) → Sort u
Quot, ``
Quot.mk: {α : Sort u} → (r : α → α → Prop) → α → Quot r
Quot.mk, ``
Quot.lift: {α : Sort u} → {r : α → α → Prop} → {β : Sort v} → (f : α → β) → (∀ (a b : α), r a b → f a = f b) → Quot r → β
Quot.lift, ``
Quot.ind: ∀ {α : Sort u} {r : α → α → Prop} {β : Quot r → Prop}, (∀ (a : α), β (Quot.mk r a)) → ∀ (q : Quot r), β q
Quot.ind] do
      
insert: Name → ExportM Unit
insert 
n: ?m.37751
n
  | 
inductInfo: InductiveVal → ConstantInfo
inductInfo  
val: InductiveVal
val => 
ind: List Name → ExportM Unit
ind 
val: InductiveVal
val.
all: InductiveVal → List Name
all
  | 
ctorInfo: ConstructorVal → ConstantInfo
ctorInfo    
val: ConstructorVal
val => 
ind: List Name → ExportM Unit
ind 
(← getConstInfoInduct val.induct): ?m.38027
(← 
getConstInfoInduct: {m : Type → Type} → [inst : Monad m] → [inst : MonadEnv m] → [inst : MonadError m] → Name → m InductiveVal
getConstInfoInduct
(← getConstInfoInduct val.induct): ?m.38027
 
val: ConstructorVal
val
(← getConstInfoInduct val.induct): ?m.38027
.
induct: ConstructorVal → Name
induct
(← getConstInfoInduct val.induct): ?m.38027
).
all: InductiveVal → List Name
all
  | 
recInfo: RecursorVal → ConstantInfo
recInfo     
val: RecursorVal
val => 
ind: List Name → ExportM Unit
ind 
val: RecursorVal
val.
all: RecursorVal → List Name
all
where
  
insert: Name → ExportM Unit
insert (
n: Name
n : 
Name: Type
Name) : 
ExportM: Type → Type
ExportM 
Unit: Type
Unit :=
    
modify: {σ : Type ?u.30156} → {m : Type ?u.30156 → Type ?u.30155} → [inst : MonadState σ m] → (σ → σ) → m PUnit
modify fun 
s: ?m.30190
s ↦ { 
s: ?m.30190
s with defs := 
s: ?m.30190
s.
defs: State → HashSet Name
defs.
insert: {α : Type ?u.30472} → {x : BEq α} → {x_1 : Hashable α} → HashSet α → α → HashSet α
insert 
n: Name
n }
  
defn: String → Name → Expr → Expr → List Name → ExportM Unit
defn (
ty: String
ty : 
String: Type
String) (
n: Name
n : 
Name: Type
Name) (
t: Expr
t 
e: Expr
e : 
Expr: Type
Expr) (
ls: List Name
ls : 
List: Type ?u.30110 → Type ?u.30110
List 
Name: Type
Name) : 
ExportM: Type → Type
ExportM 
Unit: Type
Unit := do
    let mut 
s: ?m.30741
s := s!"{
ty: String
ty} {← 
exportName: Name → ExportM Nat
exportName 
n: Name
n} {← 
exportExpr: Expr → ExportM Nat
exportExpr 
t: Expr
t} {← 
exportExpr: Expr → ExportM Nat
exportExpr 
e: Expr
e}"
    for 
l: ?m.30735
l in 
ls: List Name
ls do 
s: ?m.30791
s := 
s: ?m.30741
s ++ 
s!" {← exportName l}": ?m.30834
s!
s!" {← exportName l}": ?m.30834
" {← 
exportName: Name → ExportM Nat
exportName
s!" {← exportName l}": ?m.30834
 
l: ?m.30735
l
s!" {← exportName l}": ?m.30834
}"
    
IO.println: {α : Type ?u.31119} → [inst : ToString α] → α → IO Unit
IO.println 
s: ?m.31081
s
    
insert: Name → ExportM Unit
insert 
n: Name
n
  
axdef: String → Name → Expr → List Name → ExportM Unit
axdef (
ty: String
ty : 
String: Type
String) (
n: Name
n : 
Name: Type
Name) (
t: Expr
t : 
Expr: Type
Expr) (
ls: List Name
ls : 
List: Type ?u.30121 → Type ?u.30121
List 
Name: Type
Name) : 
ExportM: Type → Type
ExportM 
Unit: Type
Unit := do
    let mut 
s: ?m.31624
s := s!"{
ty: String
ty} {← 
exportName: Name → ExportM Nat
exportName 
n: Name
n} {← 
exportExpr: Expr → ExportM Nat
exportExpr 
t: Expr
t}"
    for 
l: ?m.31618
l in 
ls: List Name
ls do 
s: ?m.31674
s := 
s: ?m.31624
s ++ 
s!" {← exportName l}": ?m.31717
s!
s!" {← exportName l}": ?m.31717
" {← 
exportName: Name → ExportM Nat
exportName
s!" {← exportName l}": ?m.31717
 
l: ?m.31618
l
s!" {← exportName l}": ?m.31717
}"
    
IO.println: {α : Type ?u.31913} → [inst : ToString α] → α → IO Unit
IO.println 
s: ?m.31875
s
    
insert: Name → ExportM Unit
insert 
n: Name
n
  
ind: List Name → ExportM Unit
ind : 
List: Type ?u.30127 → Type ?u.30127
List 
Name: Type
Name → 
ExportM: Type → Type
ExportM 
Unit: Type
Unit
  | [] => 
unreachable!: ?m.31999
unreachable!
  | 
is: List Name
is@(
i: Name
i::_) => do
    let 
val: ?m.32437
val ← 
getConstInfoInduct: {m : Type → Type} → [inst : Monad m] → [inst : MonadEnv m] → [inst : MonadError m] → Name → m InductiveVal
getConstInfoInduct 
i: Name
i
    let mut 
s: ?m.32440
s := match 
is: List Name
is.
length: {α : Type ?u.33495} → List α → Nat
length with
    | 
1: Nat
1 => s!"#IND {
val: ?m.32437
val.
numParams: InductiveVal → Nat
numParams}"
    | 
n: Nat
n => s!"#MUT {
val: ?m.32437
val.
numParams: InductiveVal → Nat
numParams} {
n: Nat
n}"
    for 
j: ?m.32522
j in 
is: List Name
is do 
insert: Name → ExportM Unit
insert 
j: ?m.32522
j; 
insert: Name → ExportM Unit
insert (
mkRecName: Name → Name
mkRecName 
j: ?m.32522
j)
    for 
j: ?m.32763
j in 
is: List Name
is do
      let 
val: ?m.32863
val ← 
getConstInfoInduct: {m : Type → Type} → [inst : Monad m] → [inst : MonadEnv m] → [inst : MonadError m] → Name → m InductiveVal
getConstInfoInduct 
j: ?m.32763
j
      
s: ?m.34106
s := 
s: ?m.32769
s ++ s!" {← 
exportName: Name → ExportM Nat
exportName 
val: ?m.32863
val.
name: ConstantVal → Name
name} {← 
exportExpr: Expr → ExportM Nat
exportExpr 
val: ?m.32863
val.
type: ConstantVal → Expr
type} {
val: ?m.32863
val.
ctors: InductiveVal → List Name
ctors.
length: {α : Type ?u.33001} → List α → Nat
length}"
      for 
c: ?m.33215
c in 
val: ?m.32863
val.
ctors: InductiveVal → List Name
ctors do
        
insert: Name → ExportM Unit
insert 
c: ?m.33215
c
        
s: ?m.33221
s := 
s: ?m.33221
s ++ 
s!" {← exportName c} {← exportExpr (← getConstInfoCtor c).type}": ?m.33825
s!
s!" {← exportName c} {← exportExpr (← getConstInfoCtor c).type}": ?m.33825
" {← 
exportName: Name → ExportM Nat
exportName
s!" {← exportName c} {← exportExpr (← getConstInfoCtor c).type}": ?m.33825
 
c: ?m.33215
c
s!" {← exportName c} {← exportExpr (← getConstInfoCtor c).type}": ?m.33825
} {← 
exportExpr: Expr → ExportM Nat
exportExpr
s!" {← exportName c} {← exportExpr (← getConstInfoCtor c).type}": ?m.33825
 
(← getConstInfoCtor c): ?m.33409
(← 
getConstInfoCtor: {m : Type → Type} → [inst : Monad m] → [inst : MonadEnv m] → [inst : MonadError m] → Name → m ConstructorVal
getConstInfoCtor
(← getConstInfoCtor c): ?m.33409
 
c: ?m.33215
c
(← getConstInfoCtor c): ?m.33409
)
s!" {← exportName c} {← exportExpr (← getConstInfoCtor c).type}": ?m.33825
.
type: ConstantVal → Expr
type
s!" {← exportName c} {← exportExpr (← getConstInfoCtor c).type}": ?m.33825
}"
    for 
j: ?m.34346
j in 
is: List Name
is do 
s: ?m.34403
s ← 
indbody: Name → String → ExportM String
indbody 
j: ?m.34346
j 
s: ?m.34352
s
    for 
l: ?m.34613
l in 
val: ?m.32437
val.
levelParams: ConstantVal → List Name
levelParams do 
s: ?m.34669
s := 
s: ?m.34619
s ++ 
s!" {← exportName l}": ?m.34715
s!
s!" {← exportName l}": ?m.34715
" {← 
exportName: Name → ExportM Nat
exportName
s!" {← exportName l}": ?m.34715
 
l: ?m.34613
l
s!" {← exportName l}": ?m.34715
}"
    
IO.println: {α : Type ?u.34876} → [inst : ToString α] → α → IO Unit
IO.println 
s: ?m.34874
s
  
indbody: Name → String → ExportM String
indbody (
ind: Name
ind : 
Name: Type
Name) (
s: String
s : 
String: Type
String) : 
ExportM: Type → Type
ExportM 
String: Type
String := do
    let 
val: ?m.35458
val ← 
getConstInfoInduct: {m : Type → Type} → [inst : Monad m] → [inst : MonadEnv m] → [inst : MonadError m] → Name → m InductiveVal
getConstInfoInduct 
ind: Name
ind
    let mut 
s: ?m.35555
s := 
s: String
s ++ s!" {← 
exportName: Name → ExportM Nat
exportName 
ind: Name
ind} {← 
exportExpr: Expr → ExportM Nat
exportExpr 
val: ?m.35458
val.
type: ConstantVal → Expr
type} {
val: ?m.35458
val.
ctors: InductiveVal → List Name
ctors.
length: {α : Type ?u.35599} → List α → Nat
length}"
    for 
c: ?m.35844
c in 
val: ?m.35458
val.
ctors: InductiveVal → List Name
ctors do
      
s: ?m.35850
s := 
s: ?m.35850
s ++ 
s!" {← exportName c} {← exportExpr (← getConstInfoCtor c).type}": ?m.36132
s!
s!" {← exportName c} {← exportExpr (← getConstInfoCtor c).type}": ?m.36132
" {← 
exportName: Name → ExportM Nat
exportName
s!" {← exportName c} {← exportExpr (← getConstInfoCtor c).type}": ?m.36132
 
c: ?m.35844
c
s!" {← exportName c} {← exportExpr (← getConstInfoCtor c).type}": ?m.36132
} {← 
exportExpr: Expr → ExportM Nat
exportExpr
s!" {← exportName c} {← exportExpr (← getConstInfoCtor c).type}": ?m.36132
 
(← getConstInfoCtor c): ?m.35991
(← 
getConstInfoCtor: {m : Type → Type} → [inst : Monad m] → [inst : MonadEnv m] → [inst : MonadError m] → Name → m ConstructorVal
getConstInfoCtor
(← getConstInfoCtor c): ?m.35991
 
c: ?m.35844
c
(← getConstInfoCtor c): ?m.35991
)
s!" {← exportName c} {← exportExpr (← getConstInfoCtor c).type}": ?m.36132
.
type: ConstantVal → Expr
type
s!" {← exportName c} {← exportExpr (← getConstInfoCtor c).type}": ?m.36132
}"
    
pure: {f : Type ?u.36387 → Type ?u.36386} → [self : Pure f] → {α : Type ?u.36387} → α → f α
pure 
s: ?m.36384
s

end

def 
runExportM: {α : Type} → ExportM α → CoreM α
runExportM (
m: ExportM α
m : 
ExportM: Type → Type
ExportM 
α: ?m.95311
α) : 
CoreM: Type → Type
CoreM 
α: ?m.95311
α := 
m: ExportM α
m.
run': {σ : Type ?u.95322} →
  {m : Type ?u.95322 → Type ?u.95321} → [inst : Functor m] → {α : Type ?u.95322} → StateT σ m α → σ → m α
run' 
default: {α : Sort ?u.95371} → [self : Inhabited α] → α
default

-- #eval runExportM (exportDef `Lean.Expr)
end Export

end Lean