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 2022-11-15 16:49:07 -08:00
parent 8225be2f0e
commit 8a012c83d3
34 changed files with 40597 additions and 30065 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

23
stage0/src/Lean/Elab/Import.lean generated
View file

@ -40,27 +40,4 @@ def printImports (input : String) (fileName : Option String) : IO Unit := do
let fname ← findOLean dep.module
IO.println fname
deriving instance ToJson for Import
structure PrintImportResult where
imports? : Option (Array Import) := none
errors : Array String := #[]
deriving ToJson
structure PrintImportsResult where
imports : Array PrintImportResult
deriving ToJson
@[export lean_print_imports_json]
def printImportsJson (fileNames : Array String) : IO Unit := do
let rs ← fileNames.mapM fun fn => do
try
let (deps, _, msgs) ← parseImports (← IO.FS.readFile ⟨fn⟩) fn
if msgs.hasErrors then
return { errors := (← msgs.toList.toArray.mapM (·.toString)) }
else
return { imports? := some deps.toArray }
catch e => return { errors := #[e.toString] }
IO.println (toJson { imports := rs : PrintImportsResult })
end Lean.Elab

28
stage0/src/Lean/Elab/ParseImportsFast.lean generated
View file

@ -118,9 +118,6 @@ partial def whitespace : Parser := fun input s =>
@[inline] partial def keyword (k : String) : Parser :=
keywordCore k (fun _ s => s.mkError s!"`{k}` expected") (fun _ s => s)
@[inline] partial def keywordOpt (k : String) : Parser :=
keywordCore k (fun _ s => s) (fun _ s => s)
@[inline] def isIdCont : String → State → Bool := fun input s =>
let i := s.pos
let curr := input.get i
@ -186,8 +183,11 @@ partial def moduleIdent (runtimeOnly : Bool) : Parser := fun input s =>
| none => many p input s
| some _ => { pos, error? := none, imports := s.imports.shrink size }
@[inline] partial def preludeOpt (k : String) : Parser :=
keywordCore k (fun _ s => s.pushModule `Init false) (fun _ s => s)
def main : Parser :=
keywordOpt "prelude" >>
preludeOpt "prelude" >>
many (keyword "import" >> keywordCore "runtime" (moduleIdent false) (moduleIdent true))
end ParseImports
@ -201,4 +201,24 @@ def parseImports' (input : String) (fileName : String) : IO (Array Lean.Import)
| none => return s.imports
| some err => throw <| IO.userError s!"{fileName}: {err}"
deriving instance ToJson for Import
structure PrintImportResult where
imports? : Option (Array Import) := none
errors : Array String := #[]
deriving ToJson
structure PrintImportsResult where
imports : Array PrintImportResult
deriving ToJson
@[export lean_print_imports_json]
def printImportsJson (fileNames : Array String) : IO Unit := do
let rs ← fileNames.mapM fun fn => do
try
let deps ← parseImports' (← IO.FS.readFile ⟨fn⟩) fn
return { imports? := some deps }
catch e => return { errors := #[e.toString] }
IO.println (toJson { imports := rs : PrintImportsResult } |>.compress)
end Lean

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

@ -97,14 +97,11 @@ structure Config where
the type of `t` with the goal target type. We claim this is not a hack and is defensible behavior because
this last unification step is not really part of the term elaboration. -/
assignSyntheticOpaque : Bool := false
/-- When `ignoreLevelDepth` is `false`, only universe level metavariables with depth == metavariable context depth
/-- When `ignoreLevelDepth` is `false`, only universe level metavariables with `depth == metavariable` context depth
can be assigned.
We used to have `ignoreLevelDepth == false` always, but this setting produced counterintuitive behavior in a few
cases. Recall that universe levels are often ignored by users, they may not even be aware they exist.
We still use this restriction for regular metavariables. See discussion at the beginning of `MetavarContext.lean`.
We claim it is reasonable to ignore this restriction for universe metavariables because their values are often
contrained by the terms is instances and simp theorems.
TODO: we should delete this configuration option and the method `isReadOnlyLevelMVar` after we have more tests.
We set `ignoreLevelMVarDepth := false` during `simp`. See comment at `withSimpConfig` and issue #1829.
-/
ignoreLevelMVarDepth : Bool := true
/-- Enable/Disable support for offset constraints such as `?x + 1 =?= e` -/
@ -1325,12 +1322,11 @@ private def withNewMCtxDepthImp (x : MetaM α) : MetaM α := do
modify fun s => { s with mctx := saved.mctx, postponed := saved.postponed }
/--
Save cache and `MetavarContext`, bump the `MetavarContext` depth, execute `x`,
and restore saved data.
Metavariable context depths are used to control which metavariables may be assigned in `isDefEq`.
`withNewMCtxDepth k` executes `k` with a higher metavariable context depth,
where metavariables created outside the `withNewMCtxDepth` (with a lower depth) cannot be assigned.
Note that this does not affect level metavariables (by default).
See the docstring of `isDefEq` for more information.
-/
-/
def withNewMCtxDepth : n α → n α :=
mapMetaM withNewMCtxDepthImp
@ -1667,6 +1663,10 @@ def isExprDefEq (t s : Expr) : MetaM Bool :=
So, `withNewMCtxDepth (isDefEq a b)` is `isDefEq` without any mvar assignment happening
whereas `isDefEq a b` will assign any metavariables of the current depth in `a` and `b` to unify them.
By default, level metavariables can be assigned at any depth.
That is, `withNewMCtxDepth (isDefEq a b)` will still assign level mvars in `a` and `b`.
Setting the option `ignoreLevelMVarDepth := false` will disable this behavior.
For matching (where only mvars in `b` should be assigned), we create the term inside the `withNewMCtxDepth`.
For an example, see [Lean.Meta.Simp.tryTheoremWithExtraArgs?](https://github.com/leanprover/lean4/blob/master/src/Lean/Meta/Tactic/Simp/Rewrite.lean#L100-L106)
-/

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

@ -47,7 +47,7 @@ namespace Lean.Meta.DiscrTree
2- Distinguish partial applications `f a`, `f a b`, and `f a b c`.
-/
def Key.ctorIdx : Key → Nat
def Key.ctorIdx : Key s → Nat
| .star => 0
| .other => 1
| .lit .. => 2
@ -56,17 +56,17 @@ def Key.ctorIdx : Key → Nat
| .arrow => 5
| .proj .. => 6
def Key.lt : Key → Key → Bool
def Key.lt : Key s → Key s → Bool
| .lit v₁, .lit v₂ => v₁ < v₂
| .fvar n₁ a₁, .fvar n₂ a₂ => Name.quickLt n₁.name n₂.name || (n₁ == n₂ && a₁ < a₂)
| .const n₁ a₁, .const n₂ a₂ => Name.quickLt n₁ n₂ || (n₁ == n₂ && a₁ < a₂)
| .proj s₁ i₁, .proj s₂ i₂ => Name.quickLt s₁ s₂ || (s₁ == s₂ && i₁ < i₂)
| k₁, k₂ => k₁.ctorIdx < k₂.ctorIdx
instance : LT Key := ⟨fun a b => Key.lt a b⟩
instance (a b : Key) : Decidable (a < b) := inferInstanceAs (Decidable (Key.lt a b))
instance : LT (Key s) := ⟨fun a b => Key.lt a b⟩
instance (a b : Key s) : Decidable (a < b) := inferInstanceAs (Decidable (Key.lt a b))
def Key.format : Key → Format
def Key.format : Key s → Format
| .star => "*"
| .other => "◾"
| .lit (Literal.natVal v) => Std.format v
@ -76,41 +76,41 @@ def Key.format : Key → Format
| .fvar k _ => Std.format k.name
| .arrow => "→"
instance : ToFormat Key := ⟨Key.format⟩
instance : ToFormat (Key s) := ⟨Key.format⟩
def Key.arity : Key → Nat
def Key.arity : (Key s) → Nat
| .const _ a => a
| .fvar _ a => a
| .arrow => 2
| .proj .. => 1
| _ => 0
instance : Inhabited (Trie α) := ⟨.node #[] #[]⟩
instance : Inhabited (Trie α s) := ⟨.node #[] #[]⟩
def empty : DiscrTree α := { root := {} }
def empty : DiscrTree α s := { root := {} }
partial def Trie.format [ToFormat α] : Trie α → Format
partial def Trie.format [ToFormat α] : Trie α s → Format
| .node vs cs => Format.group $ Format.paren $
"node" ++ (if vs.isEmpty then Format.nil else " " ++ Std.format vs)
++ Format.join (cs.toList.map fun ⟨k, c⟩ => Format.line ++ Format.paren (Std.format k ++ " => " ++ format c))
instance [ToFormat α] : ToFormat (Trie α) := ⟨Trie.format⟩
instance [ToFormat α] : ToFormat (Trie α s) := ⟨Trie.format⟩
partial def format [ToFormat α] (d : DiscrTree α) : Format :=
partial def format [ToFormat α] (d : DiscrTree α s) : Format :=
let (_, r) := d.root.foldl
(fun (p : Bool × Format) k c =>
(false, p.2 ++ (if p.1 then Format.nil else Format.line) ++ Format.paren (Std.format k ++ " => " ++ Std.format c)))
(true, Format.nil)
Format.group r
instance [ToFormat α] : ToFormat (DiscrTree α) := ⟨format⟩
instance [ToFormat α] : ToFormat (DiscrTree α s) := ⟨format⟩
/-- The discrimination tree ignores implicit arguments and proofs.
We use the following auxiliary id as a "mark". -/
private def tmpMVarId : MVarId := { name := `_discr_tree_tmp }
private def tmpStar := mkMVar tmpMVarId
instance : Inhabited (DiscrTree α) where
instance : Inhabited (DiscrTree α s) where
default := {}
/--
@ -223,11 +223,19 @@ def mkNoindexAnnotation (e : Expr) : Expr :=
def hasNoindexAnnotation (e : Expr) : Bool :=
annotation? `noindex e |>.isSome
private partial def whnfEta (e : Expr) : MetaM Expr := do
let e ← whnf e
match e.etaExpandedStrict? with
| some e => whnfEta e
| none => return e
/--
Reduction procedure for the discrimination tree indexing.
The parameter `simpleReduce` controls how aggressive the term is reduced.
The parameter at type `DiscrTree` controls this value.
See comment at `DiscrTree`.
-/
partial def reduce (e : Expr) (simpleReduce : Bool) : MetaM Expr := do
let e ← whnfCore e (simpleReduceOnly := simpleReduce)
match (← unfoldDefinition? e) with
| some e => reduce e simpleReduce
| none => match e.etaExpandedStrict? with
| some e => reduce e simpleReduce
| none => return e
/--
Return `true` if `fn` is a "bad" key. That is, `pushArgs` would add `Key.other` or `Key.star`.
@ -247,32 +255,32 @@ private def isBadKey (fn : Expr) : Bool :=
/--
Reduce `e` until we get an irreducible term (modulo current reducibility setting) or the resulting term
is a bad key (see comment at `isBadKey`).
We use this method instead of `whnfEta` for root terms at `pushArgs`. -/
private partial def whnfUntilBadKey (e : Expr) : MetaM Expr := do
We use this method instead of `reduce` for root terms at `pushArgs`. -/
private partial def reduceUntilBadKey (e : Expr) (simpleReduce : Bool) : MetaM Expr := do
let e ← step e
match e.etaExpandedStrict? with
| some e => whnfUntilBadKey e
| some e => reduceUntilBadKey e simpleReduce
| none => return e
where
step (e : Expr) := do
let e ← whnfCore e
let e ← whnfCore e (simpleReduceOnly := simpleReduce)
match (← unfoldDefinition? e) with
| some e' => if isBadKey e'.getAppFn then return e else step e'
| none => return e
/-- whnf for the discrimination tree module -/
def whnfDT (e : Expr) (root : Bool) : MetaM Expr :=
if root then whnfUntilBadKey e else whnfEta e
def reduceDT (e : Expr) (root : Bool) (simpleReduce : Bool) : MetaM Expr :=
if root then reduceUntilBadKey e simpleReduce else reduce e simpleReduce
/- Remark: we use `shouldAddAsStar` only for nested terms, and `root == false` for nested terms -/
private def pushArgs (root : Bool) (todo : Array Expr) (e : Expr) : MetaM (Key × Array Expr) := do
private def pushArgs (root : Bool) (todo : Array Expr) (e : Expr) : MetaM (Key s × Array Expr) := do
if hasNoindexAnnotation e then
return (.star, todo)
else
let e ← whnfDT e root
let e ← reduceDT e root (simpleReduce := s)
let fn := e.getAppFn
let push (k : Key) (nargs : Nat) : MetaM (Key × Array Expr) := do
let push (k : Key s) (nargs : Nat) : MetaM (Key s × Array Expr) := do
let info ← getFunInfoNArgs fn nargs
let todo ← pushArgsAux info.paramInfo (nargs-1) e todo
return (k, todo)
@ -305,7 +313,7 @@ private def pushArgs (root : Bool) (todo : Array Expr) (e : Expr) : MetaM (Key
| _ =>
return (.other, todo)
partial def mkPathAux (root : Bool) (todo : Array Expr) (keys : Array Key) : MetaM (Array Key) := do
partial def mkPathAux (root : Bool) (todo : Array Expr) (keys : Array (Key s)) : MetaM (Array (Key s)) := do
if todo.isEmpty then
return keys
else
@ -316,13 +324,13 @@ partial def mkPathAux (root : Bool) (todo : Array Expr) (keys : Array Key) : Met
private def initCapacity := 8
def mkPath (e : Expr) : MetaM (Array Key) := do
def mkPath (e : Expr) : MetaM (Array (Key s)) := do
withReducible do
let todo : Array Expr := .mkEmpty initCapacity
let keys : Array Key := .mkEmpty initCapacity
let keys : Array (Key s) := .mkEmpty initCapacity
mkPathAux (root := true) (todo.push e) keys
private partial def createNodes (keys : Array Key) (v : α) (i : Nat) : Trie α :=
private partial def createNodes (keys : Array (Key s)) (v : α) (i : Nat) : Trie α s :=
if h : i < keys.size then
let k := keys.get ⟨i, h⟩
let c := createNodes keys v (i+1)
@ -333,7 +341,7 @@ private partial def createNodes (keys : Array Key) (v : α) (i : Nat) : Trie α
private def insertVal [BEq α] (vs : Array α) (v : α) : Array α :=
if vs.contains v then vs else vs.push v
private partial def insertAux [BEq α] (keys : Array Key) (v : α) : Nat → Trie α → Trie α
private partial def insertAux [BEq α] (keys : Array (Key s)) (v : α) : Nat → Trie α s → Trie α s
| i, .node vs cs =>
if h : i < keys.size then
let k := keys.get ⟨i, h⟩
@ -346,7 +354,7 @@ private partial def insertAux [BEq α] (keys : Array Key) (v : α) : Nat → Tri
else
.node (insertVal vs v) cs
def insertCore [BEq α] (d : DiscrTree α) (keys : Array Key) (v : α) : DiscrTree α :=
def insertCore [BEq α] (d : DiscrTree α s) (keys : Array (Key s)) (v : α) : DiscrTree α s :=
if keys.isEmpty then panic! "invalid key sequence"
else
let k := keys[0]!
@ -358,12 +366,12 @@ def insertCore [BEq α] (d : DiscrTree α) (keys : Array Key) (v : α) : DiscrTr
let c := insertAux keys v 1 c
{ root := d.root.insert k c }
def insert [BEq α] (d : DiscrTree α) (e : Expr) (v : α) : MetaM (DiscrTree α) := do
def insert [BEq α] (d : DiscrTree α s) (e : Expr) (v : α) : MetaM (DiscrTree α s) := do
let keys ← mkPath e
return d.insertCore keys v
private def getKeyArgs (e : Expr) (isMatch root : Bool) : MetaM (Key × Array Expr) := do
let e ← whnfDT e root
private def getKeyArgs (e : Expr) (isMatch root : Bool) : MetaM (Key s × Array Expr) := do
let e ← reduceDT e root (simpleReduce := s)
match e.getAppFn with
| .lit v => return (.lit v, #[])
| .const c _ =>
@ -435,22 +443,22 @@ private def getKeyArgs (e : Expr) (isMatch root : Bool) : MetaM (Key × Array Ex
| _ =>
return (.other, #[])
private abbrev getMatchKeyArgs (e : Expr) (root : Bool) : MetaM (Key × Array Expr) :=
private abbrev getMatchKeyArgs (e : Expr) (root : Bool) : MetaM (Key s × Array Expr) :=
getKeyArgs e (isMatch := true) (root := root)
private abbrev getUnifyKeyArgs (e : Expr) (root : Bool) : MetaM (Key × Array Expr) :=
private abbrev getUnifyKeyArgs (e : Expr) (root : Bool) : MetaM (Key s × Array Expr) :=
getKeyArgs e (isMatch := false) (root := root)
private def getStarResult (d : DiscrTree α) : Array α :=
private def getStarResult (d : DiscrTree α s) : Array α :=
let result : Array α := .mkEmpty initCapacity
match d.root.find? .star with
| none => result
| some (.node vs _) => result ++ vs
private abbrev findKey (cs : Array (Key × Trie α)) (k : Key) : Option (Key × Trie α) :=
private abbrev findKey (cs : Array (Key s × Trie α s)) (k : Key s) : Option (Key s × Trie α s) :=
cs.binSearch (k, default) (fun a b => a.1 < b.1)
private partial def getMatchLoop (todo : Array Expr) (c : Trie α) (result : Array α) : MetaM (Array α) := do
private partial def getMatchLoop (todo : Array Expr) (c : Trie α s) (result : Array α) : MetaM (Array α) := do
match c with
| .node vs cs =>
if todo.isEmpty then
@ -470,7 +478,7 @@ private partial def getMatchLoop (todo : Array Expr) (c : Trie α) (result : Arr
getMatchLoop todo first.2 result
else
return result
let visitNonStar (k : Key) (args : Array Expr) (result : Array α) : MetaM (Array α) :=
let visitNonStar (k : Key s) (args : Array Expr) (result : Array α) : MetaM (Array α) :=
match findKey cs k with
| none => return result
| some c => getMatchLoop (todo ++ args) c.2 result
@ -485,12 +493,12 @@ private partial def getMatchLoop (todo : Array Expr) (c : Trie α) (result : Arr
| .arrow => visitNonStar .other #[] (← visitNonStar k args result)
| _ => visitNonStar k args result
private def getMatchRoot (d : DiscrTree α) (k : Key) (args : Array Expr) (result : Array α) : MetaM (Array α) :=
private def getMatchRoot (d : DiscrTree α s) (k : Key s) (args : Array Expr) (result : Array α) : MetaM (Array α) :=
match d.root.find? k with
| none => return result
| some c => getMatchLoop args c result
private def getMatchCore (d : DiscrTree α) (e : Expr) : MetaM (Key × Array α) :=
private def getMatchCore (d : DiscrTree α s) (e : Expr) : MetaM (Key s × Array α) :=
withReducible do
let result := getStarResult d
let (k, args) ← getMatchKeyArgs e (root := true)
@ -503,13 +511,13 @@ private def getMatchCore (d : DiscrTree α) (e : Expr) : MetaM (Key × Array α)
/--
Find values that match `e` in `d`.
-/
def getMatch (d : DiscrTree α) (e : Expr) : MetaM (Array α) :=
def getMatch (d : DiscrTree α s) (e : Expr) : MetaM (Array α) :=
return (← getMatchCore d e).2
/--
Similar to `getMatch`, but returns solutions that are prefixes of `e`.
We store the number of ignored arguments in the result.-/
partial def getMatchWithExtra (d : DiscrTree α) (e : Expr) : MetaM (Array (α × Nat)) := do
partial def getMatchWithExtra (d : DiscrTree α s) (e : Expr) : MetaM (Array (α × Nat)) := do
let (k, result) ← getMatchCore d e
let result := result.map (·, 0)
if !e.isApp then
@ -519,8 +527,8 @@ partial def getMatchWithExtra (d : DiscrTree α) (e : Expr) : MetaM (Array (α
else
go e.appFn! 1 result
where
mayMatchPrefix (k : Key) : MetaM Bool :=
let cont (k : Key) : MetaM Bool :=
mayMatchPrefix (k : Key s) : MetaM Bool :=
let cont (k : Key s) : MetaM Bool :=
if d.root.find? k |>.isSome then
return true
else
@ -537,7 +545,7 @@ where
else
return result
partial def getUnify (d : DiscrTree α) (e : Expr) : MetaM (Array α) :=
partial def getUnify (d : DiscrTree α s) (e : Expr) : MetaM (Array α) :=
withReducible do
let (k, args) ← getUnifyKeyArgs e (root := true)
match k with
@ -548,7 +556,7 @@ partial def getUnify (d : DiscrTree α) (e : Expr) : MetaM (Array α) :=
| none => return result
| some c => process 0 args c result
where
process (skip : Nat) (todo : Array Expr) (c : Trie α) (result : Array α) : MetaM (Array α) := do
process (skip : Nat) (todo : Array Expr) (c : Trie α s) (result : Array α) : MetaM (Array α) := do
match skip, c with
| skip+1, .node _ cs =>
if cs.isEmpty then
@ -570,7 +578,7 @@ where
process 0 todo first.2 result
else
return result
let visitNonStar (k : Key) (args : Array Expr) (result : Array α) : MetaM (Array α) :=
let visitNonStar (k : Key s) (args : Array Expr) (result : Array α) : MetaM (Array α) :=
match findKey cs k with
| none => return result
| some c => process 0 (todo ++ args) c.2 result

71
stage0/src/Lean/Meta/DiscrTreeTypes.lean generated
View file

@ -10,18 +10,20 @@ namespace Lean.Meta
/-! See file `DiscrTree.lean` for the actual implementation and documentation. -/
namespace DiscrTree
inductive Key where
| const : Name → Nat → Key
| fvar : FVarId → Nat → Key
| lit : Literal → Key
| star : Key
| other : Key
| arrow : Key
| proj : Name → Nat → Key
/--
Discrimination tree key. See `DiscrTree`
-/
inductive Key (simpleReduce : Bool) where
| const : Name → Nat → Key simpleReduce
| fvar : FVarId → Nat → Key simpleReduce
| lit : Literal → Key simpleReduce
| star : Key simpleReduce
| other : Key simpleReduce
| arrow : Key simpleReduce
| proj : Name → Nat → Key simpleReduce
deriving Inhabited, BEq, Repr
protected def Key.hash : Key → UInt64
protected def Key.hash : Key s → UInt64
| Key.const n a => mixHash 5237 $ mixHash (hash n) (hash a)
| Key.fvar n a => mixHash 3541 $ mixHash (hash n) (hash a)
| Key.lit v => mixHash 1879 $ hash v
@ -30,16 +32,55 @@ protected def Key.hash : Key → UInt64
| Key.arrow => 17
| Key.proj s i => mixHash 11 $ mixHash (hash s) (hash i)
instance : Hashable Key := ⟨Key.hash⟩
instance : Hashable (Key s) := ⟨Key.hash⟩
inductive Trie (α : Type) where
| node (vs : Array α) (children : Array (Key × Trie α)) : Trie α
/--
Discrimination tree trie. See `DiscrTree`.
-/
inductive Trie (α : Type) (simpleReduce : Bool) where
| node (vs : Array α) (children : Array (Key simpleReduce × Trie α simpleReduce)) : Trie α simpleReduce
end DiscrTree
open DiscrTree
structure DiscrTree (α : Type) where
root : PersistentHashMap Key (Trie α) := {}
/--
Discrimination trees. It is an index from terms to values of type `α`.
If `simpleReduce := true`, then only simple reduction are performed while
indexing/retrieving terms. For example, `iota` reduction is not performed.
We use `simpleReduce := false` in the type class resolution module,
and `simpleReduce := true` in `simp`.
Motivations:
- In `simp`, we want to have `simp` theorem such as
```
@[simp] theorem liftOn_mk (a : α) (f : α → γ) (h : ∀ a₁ a₂, r a₁ a₂ → f a₁ = f a₂) :
Quot.liftOn (Quot.mk r a) f h = f a := rfl
```
If we enable `iota`, then the lhs is reduced to `f a`.
- During type class resolution, we often want to reduce types using even `iota`.
Example:
```
inductive Ty where
| int
| bool
@[reducible] def Ty.interp (ty : Ty) : Type :=
Ty.casesOn (motive := fun _ => Type) ty Int Bool
def test {a b c : Ty} (f : a.interp → b.interp → c.interp) (x : a.interp) (y : b.interp) : c.interp :=
f x y
def f (a b : Ty.bool.interp) : Ty.bool.interp :=
-- We want to synthesize `BEq Ty.bool.interp` here, and it will fail
-- if we do not reduce `Ty.bool.interp` to `Bool`.
test (.==.) a b
```
-/
structure DiscrTree (α : Type) (simpleReduce : Bool) where
root : PersistentHashMap (Key simpleReduce) (Trie α simpleReduce) := {}
end Lean.Meta

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

@ -9,8 +9,32 @@ import Lean.Meta.DiscrTree
namespace Lean.Meta
/-
Note: we want to use iota reduction when indexing instaces. Otherwise,
we cannot elaborate examples such as
```
inductive Ty where
| int
| bool
@[reducible] def Ty.interp (ty : Ty) : Type :=
Ty.casesOn (motive := fun _ => Type) ty Int Bool
def test {a b c : Ty} (f : a.interp → b.interp → c.interp) (x : a.interp) (y : b.interp) : c.interp :=
f x y
def f (a b : Ty.bool.interp) : Ty.bool.interp :=
-- We want to synthesize `BEq Ty.bool.interp` here, and it will fail
-- if we do not reduce `Ty.bool.interp` to `Bool`.
test (.==.) a b
```
See comment at `DiscrTree`.
-/
abbrev InstanceKey := DiscrTree.Key (simpleReduce := false)
structure InstanceEntry where
keys : Array DiscrTree.Key
keys : Array InstanceKey
val : Expr
priority : Nat
globalName? : Option Name := none
@ -24,8 +48,10 @@ instance : ToFormat InstanceEntry where
| some n => format n
| _ => "<local>"
abbrev InstanceTree := DiscrTree InstanceEntry (simpleReduce := false)
structure Instances where
discrTree : DiscrTree InstanceEntry := DiscrTree.empty
discrTree : InstanceTree := DiscrTree.empty
instanceNames : PHashSet Name := {}
erased : PHashSet Name := {}
deriving Inhabited
@ -49,7 +75,7 @@ builtin_initialize instanceExtension : SimpleScopedEnvExtension InstanceEntry In
addEntry := addInstanceEntry
}
private def mkInstanceKey (e : Expr) : MetaM (Array DiscrTree.Key) := do
private def mkInstanceKey (e : Expr) : MetaM (Array InstanceKey) := do
let type ← inferType e
withNewMCtxDepth do
let (_, _, type) ← forallMetaTelescopeReducing type
@ -74,7 +100,7 @@ builtin_initialize
modifyEnv fun env => instanceExtension.modifyState env fun _ => s
}
def getGlobalInstancesIndex : CoreM (DiscrTree InstanceEntry) :=
def getGlobalInstancesIndex : CoreM (DiscrTree InstanceEntry (simpleReduce := false)) :=
return Meta.instanceExtension.getState (← getEnv) |>.discrTree
def getErasedInstances : CoreM (PHashSet Name) :=

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

@ -668,7 +668,6 @@ def synthInstance? (type : Expr) (maxResultSize? : Option Nat := none) : MetaM (
-/
withConfig (fun config => { config with isDefEqStuckEx := true, transparency := TransparencyMode.instances,
foApprox := true, ctxApprox := true, constApprox := false,
ignoreLevelMVarDepth := true,
etaStruct := .notClasses }) do
let type ← instantiateMVars type
let type ← preprocess type

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

@ -701,9 +701,31 @@ where
modify fun s => { s with cache := s.cache.insert e { r with dischargeDepth } }
return r
@[inline] def withSimpConfig (ctx : Context) (x : MetaM α) : MetaM α :=
/-
We set `ignoreLevelMVarDepth := false` because we don't want a `simp` theorem to constraint a universe level metavariable.
For example, consider the following example from issue #1829
```
@[simp] theorem eq_iff_true_of_subsingleton [Subsingleton α] (x y : α) : x = y ↔ True :=
⟨fun _ => ⟨⟩, fun _ => (Subsingleton.elim ..)⟩
structure Func' (α : Sort _) (β : Sort _) :=
(toFun : α → β)
def r : Func' α α := ⟨id⟩
example (x y : α) (h : x = y) : r.toFun x = y := by simp <;> rw [h]
```
`α` has type `Sort ?u`. If `ignoreLevelMVarDepth := true`, then `eq_iff_true_of_subsingleton` is applicable
by setting `?u := 0` and using instance `instance (p : Prop) : Subsingleton p`.
Moreover, the assignment is lost since `simp`, and a type error is produced later. Even if we prevented the assignment
from being lost, the situation is far from ideal since `simp` would be restricting the universe level.
-/
withConfig (fun c => { c with etaStruct := ctx.config.etaStruct, ignoreLevelMVarDepth := false }) <| withReducible x
def main (e : Expr) (ctx : Context) (usedSimps : UsedSimps := {}) (methods : Methods := {}) : MetaM (Result × UsedSimps) := do
let ctx := { ctx with config := (← ctx.config.updateArith) }
withConfig (fun c => { c with etaStruct := ctx.config.etaStruct }) <| withReducible do
withSimpConfig ctx do
try
let (r, s) ← simp e methods ctx |>.run { usedTheorems := usedSimps }
pure (r, s.usedTheorems)
@ -711,7 +733,7 @@ def main (e : Expr) (ctx : Context) (usedSimps : UsedSimps := {}) (methods : Met
if ex.isMaxHeartbeat then throwNestedTacticEx `simp ex else throw ex
def dsimpMain (e : Expr) (ctx : Context) (usedSimps : UsedSimps := {}) (methods : Methods := {}) : MetaM (Expr × UsedSimps) := do
withConfig (fun c => { c with etaStruct := ctx.config.etaStruct }) <| withReducible do
withSimpConfig ctx do
try
let (r, s) ← dsimp e methods ctx |>.run { usedTheorems := usedSimps }
pure (r, s.usedTheorems)

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

@ -134,7 +134,7 @@ def tryTheorem? (e : Expr) (thm : SimpTheorem) (discharge? : Expr → SimpM (Opt
/--
Remark: the parameter tag is used for creating trace messages. It is irrelevant otherwise.
-/
def rewrite? (e : Expr) (s : DiscrTree SimpTheorem) (erased : PHashSet Origin) (discharge? : Expr → SimpM (Option Expr)) (tag : String) (rflOnly : Bool) : SimpM (Option Result) := do
def rewrite? (e : Expr) (s : SimpTheoremTree) (erased : PHashSet Origin) (discharge? : Expr → SimpM (Option Expr)) (tag : String) (rflOnly : Bool) : SimpM (Option Result) := do
let candidates ← s.getMatchWithExtra e
if candidates.isEmpty then
trace[Debug.Meta.Tactic.simp] "no theorems found for {tag}-rewriting {e}"

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

@ -50,6 +50,19 @@ def Origin.key : Origin → Name
instance : BEq Origin := ⟨(·.key == ·.key)⟩
instance : Hashable Origin := ⟨(hash ·.key)⟩
/-
Note: we want to use iota reduction when indexing instaces. Otherwise,
we cannot use simp theorems such as
```
@[simp] theorem liftOn_mk (a : α) (f : α → γ) (h : ∀ a₁ a₂, r a₁ a₂ → f a₁ = f a₂) :
Quot.liftOn (Quot.mk r a) f h = f a := rfl
```
If we use `iota`, then the lhs is reduced to `f a`.
See comment at `DiscrTree`.
-/
abbrev SimpTheoremKey := DiscrTree.Key (simpleReduce := true)
/--
The fields `levelParams` and `proof` are used to encode the proof of the simp theorem.
If the `proof` is a global declaration `c`, we store `Expr.const c []` at `proof` without the universe levels, and `levelParams` is set to `#[]`
@ -60,7 +73,7 @@ instance : Hashable Origin := ⟨(hash ·.key)⟩
Then, we use `abstractMVars` to abstract the universe metavariables and create new fresh universe parameters that are stored at the field `levelParams`.
-/
structure SimpTheorem where
keys : Array DiscrTree.Key := #[]
keys : Array SimpTheoremKey := #[]
/--
It stores universe parameter names for universe polymorphic proofs.
Recall that it is non-empty only when we elaborate an expression provided by the user.
@ -137,9 +150,11 @@ def ppSimpTheorem [Monad m] [MonadLiftT IO m] [MonadEnv m] [MonadError m] (s : S
instance : BEq SimpTheorem where
beq e₁ e₂ := e₁.proof == e₂.proof
abbrev SimpTheoremTree := DiscrTree SimpTheorem (simpleReduce := true)
structure SimpTheorems where
pre : DiscrTree SimpTheorem := DiscrTree.empty
post : DiscrTree SimpTheorem := DiscrTree.empty
pre : SimpTheoremTree := DiscrTree.empty
post : SimpTheoremTree := DiscrTree.empty
lemmaNames : PHashSet Origin := {}
toUnfold : PHashSet Name := {}
erased : PHashSet Origin := {}
@ -202,7 +217,7 @@ private partial def isPerm : Expr → Expr → MetaM Bool
| s, t => return s == t
private def checkBadRewrite (lhs rhs : Expr) : MetaM Unit := do
let lhs ← DiscrTree.whnfDT lhs (root := true)
let lhs ← DiscrTree.reduceDT lhs (root := true) (simpleReduce := true)
if lhs == rhs && lhs.isFVar then
throwError "invalid `simp` theorem, equation is equivalent to{indentExpr (← mkEq lhs rhs)}"

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

@ -10,13 +10,17 @@ import Lean.Meta.SynthInstance
namespace Lean.Meta
abbrev UnificationHintKey := DiscrTree.Key (simpleReduce := true)
structure UnificationHintEntry where
keys : Array DiscrTree.Key
keys : Array UnificationHintKey
val : Name
deriving Inhabited
abbrev UnificationHintTree := DiscrTree Name (simpleReduce := true)
structure UnificationHints where
discrTree : DiscrTree Name := DiscrTree.empty
discrTree : UnificationHintTree := DiscrTree.empty
deriving Inhabited
instance : ToFormat UnificationHints where

59
stage0/src/Lean/Meta/WHNF.lean generated
View file

@ -485,14 +485,17 @@ private def whnfDelayedAssigned? (f' : Expr) (e : Expr) : MetaM (Option Expr) :=
return none
/--
Apply beta-reduction, zeta-reduction (i.e., unfold let local-decls), iota-reduction,
expand let-expressions, expand assigned meta-variables.
Apply beta-reduction, zeta-reduction (i.e., unfold let local-decls), iota-reduction,
expand let-expressions, expand assigned meta-variables.
The parameter `deltaAtProj` controls how to reduce projections `s.i`. If `deltaAtProj == true`,
then delta reduction is used to reduce `s` (i.e., `whnf` is used), otherwise `whnfCore`.
We only set this flag to `false` when implementing `isDefEq`.
The parameter `deltaAtProj` controls how to reduce projections `s.i`. If `deltaAtProj == true`,
then delta reduction is used to reduce `s` (i.e., `whnf` is used), otherwise `whnfCore`.
We only set this flag to `false` when implementing `isDefEq`.
If `simpleReduceOnly`, then `iota` and projection reduction are not performed.
Note that the value of `deltaAtProj` is irrelevant if `simpleReduceOnly = true`.
-/
partial def whnfCore (e : Expr) (deltaAtProj : Bool := true) : MetaM Expr :=
partial def whnfCore (e : Expr) (deltaAtProj : Bool := true) (simpleReduceOnly := false) : MetaM Expr :=
go e
where
go (e : Expr) : MetaM Expr :=
@ -511,26 +514,32 @@ where
go eNew
else
let e := if f == f' then e else e.updateFn f'
match (← reduceMatcher? e) with
| ReduceMatcherResult.reduced eNew => go eNew
| ReduceMatcherResult.partialApp => pure e
| ReduceMatcherResult.stuck _ => pure e
| ReduceMatcherResult.notMatcher =>
matchConstAux f' (fun _ => return e) fun cinfo lvls =>
match cinfo with
| ConstantInfo.recInfo rec => reduceRec rec lvls e.getAppArgs (fun _ => return e) go
| ConstantInfo.quotInfo rec => reduceQuotRec rec lvls e.getAppArgs (fun _ => return e) go
| c@(ConstantInfo.defnInfo _) => do
if (← isAuxDef c.name) then
deltaBetaDefinition c lvls e.getAppRevArgs (fun _ => return e) go
else
return e
| _ => return e
if simpleReduceOnly then
return e
else
match (← reduceMatcher? e) with
| ReduceMatcherResult.reduced eNew => go eNew
| ReduceMatcherResult.partialApp => pure e
| ReduceMatcherResult.stuck _ => pure e
| ReduceMatcherResult.notMatcher =>
matchConstAux f' (fun _ => return e) fun cinfo lvls =>
match cinfo with
| ConstantInfo.recInfo rec => reduceRec rec lvls e.getAppArgs (fun _ => return e) go
| ConstantInfo.quotInfo rec => reduceQuotRec rec lvls e.getAppArgs (fun _ => return e) go
| c@(ConstantInfo.defnInfo _) => do
if (← isAuxDef c.name) then
deltaBetaDefinition c lvls e.getAppRevArgs (fun _ => return e) go
else
return e
| _ => return e
| Expr.proj _ i c =>
let c ← if deltaAtProj then whnf c else whnfCore c
match (← projectCore? c i) with
| some e => go e
| none => return e
if simpleReduceOnly then
return e
else
let c ← if deltaAtProj then whnf c else whnfCore c
match (← projectCore? c i) with
| some e => go e
| none => return e
| _ => unreachable!
/--

6
stage0/src/runtime/mpz.cpp generated
View file

@ -47,7 +47,7 @@ mpz::mpz(uint64 v):
mpz::mpz(int64 v) {
uint64 w;
if (v < 0) w = -v;
if (v < 0) w = -static_cast<uint64>(v);
else w = v;
mpz_init_set_ui(m_val, static_cast<unsigned>(w));
mpz tmp(static_cast<unsigned>(w >> 32));
@ -146,13 +146,13 @@ mpz & mpz::operator+=(mpz const & o) { mpz_add(m_val, m_val, o.m_val); return *t
mpz & mpz::operator+=(unsigned u) { mpz_add_ui(m_val, m_val, u); return *this; }
mpz & mpz::operator+=(int u) { if (u >= 0) mpz_add_ui(m_val, m_val, u); else mpz_sub_ui(m_val, m_val, -u); return *this; }
mpz & mpz::operator+=(int u) { if (u >= 0) mpz_add_ui(m_val, m_val, u); else mpz_sub_ui(m_val, m_val, -static_cast<unsigned>(u)); return *this; }
mpz & mpz::operator-=(mpz const & o) { mpz_sub(m_val, m_val, o.m_val); return *this; }
mpz & mpz::operator-=(unsigned u) { mpz_sub_ui(m_val, m_val, u); return *this; }
mpz & mpz::operator-=(int u) { if (u >= 0) mpz_sub_ui(m_val, m_val, u); else mpz_add_ui(m_val, m_val, -u); return *this; }
mpz & mpz::operator-=(int u) { if (u >= 0) mpz_sub_ui(m_val, m_val, u); else mpz_add_ui(m_val, m_val, -static_cast<unsigned>(u)); return *this; }
mpz & mpz::operator*=(mpz const & o) { mpz_mul(m_val, m_val, o.m_val); return *this; }

1205
stage0/stdlib/Lean/Elab/App.c generated
View file

File diff suppressed because it is too large Load diff

1532
stage0/stdlib/Lean/Elab/ComputedFields.c generated
View file

File diff suppressed because it is too large Load diff

181
stage0/stdlib/Lean/Elab/Do.c generated
View file

@ -1258,7 +1258,7 @@ static lean_object* l___private_Lean_Elab_Do_0__Lean_Elab_Term_getDoSeqElems___c
LEAN_EXPORT lean_object* l_Lean_addTrace___at_Lean_Elab_Term_Do_mkJmp___spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Array_forInUnsafe_loop___at___private_Lean_Elab_Do_0__Lean_Elab_Term_Do_expandDoIf_x3f___spec__5___lambda__2___closed__22;
LEAN_EXPORT lean_object* l_Lean_Elab_Term_Do_getDoReassignVars___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_whnfEasyCases___at_Lean_Meta_whnfCore_go___spec__3(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_whnfEasyCases___at_Lean_Meta_whnfCore_go___spec__3(uint8_t, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Name_mkStr4(lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_Term_Do_ToTerm_breakToTerm___closed__3;
static lean_object* l_Lean_Elab_Term_Do_ToCodeBlock_doTryToCode___lambda__4___closed__4;
@ -2666,186 +2666,187 @@ x_9 = lean_ctor_get(x_8, 0);
lean_inc(x_9);
if (lean_obj_tag(x_9) == 0)
{
lean_object* x_10; uint8_t x_11; lean_object* x_12;
lean_object* x_10; uint8_t x_11; uint8_t x_12; lean_object* x_13;
x_10 = lean_ctor_get(x_8, 1);
lean_inc(x_10);
lean_dec(x_8);
x_11 = 1;
x_12 = 0;
lean_inc(x_6);
lean_inc(x_5);
lean_inc(x_4);
lean_inc(x_3);
lean_inc(x_2);
x_12 = l_Lean_Meta_whnfEasyCases___at_Lean_Meta_whnfCore_go___spec__3(x_11, x_2, x_3, x_4, x_5, x_6, x_10);
if (lean_obj_tag(x_12) == 0)
x_13 = l_Lean_Meta_whnfEasyCases___at_Lean_Meta_whnfCore_go___spec__3(x_11, x_12, x_2, x_3, x_4, x_5, x_6, x_10);
if (lean_obj_tag(x_13) == 0)
{
lean_object* x_13; lean_object* x_14; uint8_t x_15;
x_13 = lean_ctor_get(x_12, 0);
lean_inc(x_13);
x_14 = lean_ctor_get(x_12, 1);
lean_object* x_14; lean_object* x_15; uint8_t x_16;
x_14 = lean_ctor_get(x_13, 0);
lean_inc(x_14);
lean_dec(x_12);
x_15 = lean_expr_eqv(x_13, x_2);
x_15 = lean_ctor_get(x_13, 1);
lean_inc(x_15);
lean_dec(x_13);
x_16 = lean_expr_eqv(x_14, x_2);
lean_dec(x_2);
if (x_15 == 0)
if (x_16 == 0)
{
x_2 = x_13;
x_7 = x_14;
x_2 = x_14;
x_7 = x_15;
goto _start;
}
else
{
lean_object* x_17; uint8_t x_18;
x_17 = l_Lean_Expr_getAppFn(x_13);
x_18 = l_Lean_Expr_isMVar(x_17);
lean_dec(x_17);
if (x_18 == 0)
lean_object* x_18; uint8_t x_19;
x_18 = l_Lean_Expr_getAppFn(x_14);
x_19 = l_Lean_Expr_isMVar(x_18);
lean_dec(x_18);
if (x_19 == 0)
{
lean_object* x_19;
lean_object* x_20;
lean_inc(x_6);
lean_inc(x_5);
lean_inc(x_4);
lean_inc(x_3);
x_19 = l_Lean_Meta_unfoldDefinition_x3f(x_13, x_3, x_4, x_5, x_6, x_14);
if (lean_obj_tag(x_19) == 0)
{
lean_object* x_20;
x_20 = lean_ctor_get(x_19, 0);
lean_inc(x_20);
x_20 = l_Lean_Meta_unfoldDefinition_x3f(x_14, x_3, x_4, x_5, x_6, x_15);
if (lean_obj_tag(x_20) == 0)
{
lean_object* x_21; lean_object* x_22; lean_object* x_23;
lean_object* x_21;
x_21 = lean_ctor_get(x_20, 0);
lean_inc(x_21);
if (lean_obj_tag(x_21) == 0)
{
lean_object* x_22; lean_object* x_23; lean_object* x_24;
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_1);
x_21 = lean_ctor_get(x_19, 1);
lean_inc(x_21);
lean_dec(x_19);
x_22 = lean_box(0);
x_23 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_23, 0, x_22);
lean_ctor_set(x_23, 1, x_21);
return x_23;
x_22 = lean_ctor_get(x_20, 1);
lean_inc(x_22);
lean_dec(x_20);
x_23 = lean_box(0);
x_24 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_24, 0, x_23);
lean_ctor_set(x_24, 1, x_22);
return x_24;
}
else
{
lean_object* x_24; lean_object* x_25;
x_24 = lean_ctor_get(x_19, 1);
lean_inc(x_24);
lean_dec(x_19);
x_25 = lean_ctor_get(x_20, 0);
lean_object* x_25; lean_object* x_26;
x_25 = lean_ctor_get(x_20, 1);
lean_inc(x_25);
lean_dec(x_20);
x_2 = x_25;
x_7 = x_24;
x_26 = lean_ctor_get(x_21, 0);
lean_inc(x_26);
lean_dec(x_21);
x_2 = x_26;
x_7 = x_25;
goto _start;
}
}
else
{
lean_object* x_27; lean_object* x_28; lean_object* x_29;
lean_object* x_28; lean_object* x_29; lean_object* x_30;
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_1);
x_27 = lean_ctor_get(x_19, 0);
lean_inc(x_27);
x_28 = lean_ctor_get(x_19, 1);
x_28 = lean_ctor_get(x_20, 0);
lean_inc(x_28);
lean_dec(x_19);
x_29 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_29, 0, x_27);
lean_ctor_set(x_29, 1, x_28);
return x_29;
x_29 = lean_ctor_get(x_20, 1);
lean_inc(x_29);
lean_dec(x_20);
x_30 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_30, 0, x_28);
lean_ctor_set(x_30, 1, x_29);
return x_30;
}
}
else
{
lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34;
lean_dec(x_13);
lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34; lean_object* x_35;
lean_dec(x_14);
lean_dec(x_1);
x_30 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_mkUnknownMonadResult(x_3, x_4, x_5, x_6, x_14);
x_31 = l___private_Lean_Elab_Do_0__Lean_Elab_Term_mkUnknownMonadResult(x_3, x_4, x_5, x_6, x_15);
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_4);
x_31 = lean_ctor_get(x_30, 0);
lean_inc(x_31);
x_32 = lean_ctor_get(x_30, 1);
x_32 = lean_ctor_get(x_31, 0);
lean_inc(x_32);
lean_dec(x_30);
x_33 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_33, 0, x_31);
x_34 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_34, 0, x_33);
lean_ctor_set(x_34, 1, x_32);
return x_34;
x_33 = lean_ctor_get(x_31, 1);
lean_inc(x_33);
lean_dec(x_31);
x_34 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_34, 0, x_32);
x_35 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_35, 0, x_34);
lean_ctor_set(x_35, 1, x_33);
return x_35;
}
}
}
else
{
lean_object* x_35; lean_object* x_36; lean_object* x_37;
lean_object* x_36; lean_object* x_37; lean_object* x_38;
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_2);
lean_dec(x_1);
x_35 = lean_ctor_get(x_12, 0);
lean_inc(x_35);
x_36 = lean_ctor_get(x_12, 1);
x_36 = lean_ctor_get(x_13, 0);
lean_inc(x_36);
lean_dec(x_12);
x_37 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_37, 0, x_35);
lean_ctor_set(x_37, 1, x_36);
return x_37;
x_37 = lean_ctor_get(x_13, 1);
lean_inc(x_37);
lean_dec(x_13);
x_38 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_38, 0, x_36);
lean_ctor_set(x_38, 1, x_37);
return x_38;
}
}
else
{
lean_object* x_38; lean_object* x_39; lean_object* x_40; lean_object* x_41;
lean_object* x_39; lean_object* x_40; lean_object* x_41; lean_object* x_42;
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_2);
lean_dec(x_1);
x_38 = lean_ctor_get(x_8, 1);
lean_inc(x_38);
lean_dec(x_8);
x_39 = lean_ctor_get(x_9, 0);
x_39 = lean_ctor_get(x_8, 1);
lean_inc(x_39);
lean_dec(x_8);
x_40 = lean_ctor_get(x_9, 0);
lean_inc(x_40);
lean_dec(x_9);
x_40 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_40, 0, x_39);
x_41 = lean_alloc_ctor(0, 2, 0);
x_41 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_41, 0, x_40);
lean_ctor_set(x_41, 1, x_38);
return x_41;
x_42 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_42, 0, x_41);
lean_ctor_set(x_42, 1, x_39);
return x_42;
}
}
else
{
lean_object* x_42; lean_object* x_43; lean_object* x_44;
lean_object* x_43; lean_object* x_44; lean_object* x_45;
lean_dec(x_6);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_2);
lean_dec(x_1);
x_42 = lean_ctor_get(x_8, 0);
lean_inc(x_42);
x_43 = lean_ctor_get(x_8, 1);
x_43 = lean_ctor_get(x_8, 0);
lean_inc(x_43);
x_44 = lean_ctor_get(x_8, 1);
lean_inc(x_44);
lean_dec(x_8);
x_44 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_44, 0, x_42);
lean_ctor_set(x_44, 1, x_43);
return x_44;
x_45 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_45, 0, x_43);
lean_ctor_set(x_45, 1, x_44);
return x_45;
}
}
}

685
stage0/stdlib/Lean/Elab/Import.c generated
View file

@ -14,87 +14,40 @@
extern "C" {
#endif
lean_object* l_List_reverse___rarg(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_instToJsonImport;
static lean_object* l___private_Lean_Elab_Import_0__Lean_Elab_toJsonImport____x40_Lean_Elab_Import___hyg_683____closed__2;
lean_object* lean_string_push(lean_object*, uint32_t);
size_t lean_usize_add(size_t, size_t);
lean_object* lean_mk_empty_array_with_capacity(lean_object*);
lean_object* l_Lean_Name_str___override(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_printImportsJson___spec__1(size_t, size_t, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Elab_Import_0__Lean_Elab_toJsonPrintImportsResult____x40_Lean_Elab_Import___hyg_833_(lean_object*);
static lean_object* l_Lean_Elab_headerToImports___closed__4;
lean_object* l_Lean_Parser_parseHeader(lean_object*, lean_object*);
lean_object* lean_array_uget(lean_object*, size_t);
lean_object* lean_io_error_to_string(lean_object*);
lean_object* lean_array_uset(lean_object*, size_t, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_PrintImportResult_imports_x3f___default;
static lean_object* l_Lean_Elab_headerToImports___closed__2;
LEAN_EXPORT lean_object* l_Lean_Elab_headerToImports(lean_object*);
lean_object* l_Lean_Parser_mkInputContext(lean_object*, lean_object*);
lean_object* lean_array_push(lean_object*, lean_object*);
lean_object* lean_array_get_size(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Json_opt___at___private_Lean_Elab_Import_0__Lean_Elab_toJsonPrintImportResult____x40_Lean_Elab_Import___hyg_761____spec__1(lean_object*, lean_object*);
static lean_object* l_Lean_Elab_PrintImportResult_errors___default___closed__1;
lean_object* l_List_join___rarg(lean_object*);
uint8_t lean_usize_dec_lt(size_t, size_t);
static lean_object* l_Lean_Elab_headerToImports___closed__1;
LEAN_EXPORT lean_object* l_Lean_Elab_headerToImports___boxed(lean_object*);
static lean_object* l___private_Lean_Elab_Import_0__Lean_Elab_toJsonImport____x40_Lean_Elab_Import___hyg_683____closed__1;
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Import_0__Lean_Elab_toJsonPrintImportsResult____x40_Lean_Elab_Import___hyg_833____spec__1___boxed(lean_object*, lean_object*, lean_object*);
static lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_printImportsJson___spec__2___closed__1;
lean_object* l_Lean_findOLean(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_processHeader(lean_object*, lean_object*, lean_object*, lean_object*, uint32_t, lean_object*);
static lean_object* l_Lean_Elab_parseImports___closed__1;
lean_object* l_Lean_MessageLog_toList(lean_object*);
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_printImportsJson___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Elab_headerToImports___closed__3;
lean_object* l_Lean_Name_toString(lean_object*, uint8_t);
lean_object* l_IO_print___at_IO_println___spec__1(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_List_forIn_loop___at_Lean_Elab_printImports___spec__2(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Syntax_getId(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_processHeader___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_array_to_list(lean_object*, lean_object*);
static lean_object* l_Lean_Elab_processHeader___closed__1;
LEAN_EXPORT lean_object* l_Lean_Elab_PrintImportResult_errors___default;
lean_object* l_Lean_FileMap_toPosition(lean_object*, lean_object*);
lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Data_Lsp_CodeActions_0__Lean_Lsp_toJsonResolveSupport____x40_Lean_Data_Lsp_CodeActions___hyg_1822____spec__1(size_t, size_t, lean_object*);
lean_object* l_Lean_FileMap_ofString(lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Elab_Import_0__Lean_Elab_toJsonPrintImportResult____x40_Lean_Elab_Import___hyg_761_(lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Elab_Import_0__Lean_Elab_toJsonImport____x40_Lean_Elab_Import___hyg_683_(lean_object*);
size_t lean_usize_of_nat(lean_object*);
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Import_0__Lean_Elab_toJsonPrintImportsResult____x40_Lean_Elab_Import___hyg_833____spec__1(size_t, size_t, lean_object*);
lean_object* l_Lean_PersistentArray_push___rarg(lean_object*, lean_object*);
lean_object* l_Lean_Syntax_getPos_x3f(lean_object*, uint8_t);
lean_object* lean_mk_empty_environment(uint32_t, lean_object*);
lean_object* lean_import_modules(lean_object*, lean_object*, uint32_t, lean_object*);
lean_object* l_List_redLength___rarg(lean_object*);
static lean_object* l_Lean_Elab_instToJsonPrintImportsResult___closed__1;
lean_object* l_Lean_Syntax_getArgs(lean_object*);
static lean_object* l_Lean_Elab_instToJsonPrintImportResult___closed__1;
lean_object* l_Lean_Json_mkObj(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_instToJsonPrintImportResult;
lean_object* l_Lean_Json_pretty(lean_object*, lean_object*);
static lean_object* l_Lean_Elab_instToJsonImport___closed__1;
lean_object* l_List_toArrayAux___rarg(lean_object*, lean_object*);
uint8_t l_Lean_Syntax_isNone(lean_object*);
LEAN_EXPORT lean_object* l_List_mapTRAux___at_Lean_Elab_headerToImports___spec__1(lean_object*, lean_object*);
static lean_object* l___private_Lean_Elab_Import_0__Lean_Elab_toJsonPrintImportResult____x40_Lean_Elab_Import___hyg_761____closed__2;
LEAN_EXPORT lean_object* l_Lean_Elab_parseImports(lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_PersistentArray_anyM___at_Lean_MessageLog_hasErrors___spec__1(lean_object*);
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_printImportsJson___spec__2(size_t, size_t, lean_object*, lean_object*);
static lean_object* l___private_Lean_Elab_Import_0__Lean_Elab_toJsonPrintImportResult____x40_Lean_Elab_Import___hyg_761____closed__1;
lean_object* l_IO_FS_readFile(lean_object*, lean_object*);
LEAN_EXPORT lean_object* lean_print_imports(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Import_0__Lean_Elab_toJsonPrintImportResult____x40_Lean_Elab_Import___hyg_761____spec__2(size_t, size_t, lean_object*);
lean_object* l_Lean_Syntax_getArg(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_IO_println___at_Lean_Elab_printImports___spec__1(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_IO_println___at_Lean_Elab_printImportsJson___spec__3(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_printImportsJson___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Message_toString(lean_object*, uint8_t, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_instToJsonPrintImportsResult;
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Import_0__Lean_Elab_toJsonPrintImportResult____x40_Lean_Elab_Import___hyg_761____spec__2___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_List_appendTR___rarg(lean_object*, lean_object*);
LEAN_EXPORT lean_object* lean_print_imports_json(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_List_mapTRAux___at_Lean_Elab_headerToImports___spec__1(lean_object* x_1, lean_object* x_2) {
_start:
{
@ -1111,616 +1064,6 @@ return x_21;
}
}
}
static lean_object* _init_l___private_Lean_Elab_Import_0__Lean_Elab_toJsonImport____x40_Lean_Elab_Import___hyg_683____closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string_from_bytes("module", 6);
return x_1;
}
}
static lean_object* _init_l___private_Lean_Elab_Import_0__Lean_Elab_toJsonImport____x40_Lean_Elab_Import___hyg_683____closed__2() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string_from_bytes("runtimeOnly", 11);
return x_1;
}
}
LEAN_EXPORT lean_object* l___private_Lean_Elab_Import_0__Lean_Elab_toJsonImport____x40_Lean_Elab_Import___hyg_683_(lean_object* x_1) {
_start:
{
lean_object* x_2; uint8_t 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; uint8_t 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;
x_2 = lean_ctor_get(x_1, 0);
lean_inc(x_2);
x_3 = 1;
x_4 = l_Lean_Name_toString(x_2, x_3);
x_5 = lean_alloc_ctor(3, 1, 0);
lean_ctor_set(x_5, 0, x_4);
x_6 = l___private_Lean_Elab_Import_0__Lean_Elab_toJsonImport____x40_Lean_Elab_Import___hyg_683____closed__1;
x_7 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_7, 0, x_6);
lean_ctor_set(x_7, 1, x_5);
x_8 = lean_box(0);
x_9 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_9, 0, x_7);
lean_ctor_set(x_9, 1, x_8);
x_10 = lean_ctor_get_uint8(x_1, sizeof(void*)*1);
lean_dec(x_1);
x_11 = lean_alloc_ctor(1, 0, 1);
lean_ctor_set_uint8(x_11, 0, x_10);
x_12 = l___private_Lean_Elab_Import_0__Lean_Elab_toJsonImport____x40_Lean_Elab_Import___hyg_683____closed__2;
x_13 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_13, 0, x_12);
lean_ctor_set(x_13, 1, x_11);
x_14 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_14, 0, x_13);
lean_ctor_set(x_14, 1, x_8);
x_15 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_15, 0, x_14);
lean_ctor_set(x_15, 1, x_8);
x_16 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_16, 0, x_9);
lean_ctor_set(x_16, 1, x_15);
x_17 = l_List_join___rarg(x_16);
x_18 = l_Lean_Json_mkObj(x_17);
return x_18;
}
}
static lean_object* _init_l_Lean_Elab_instToJsonImport___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l___private_Lean_Elab_Import_0__Lean_Elab_toJsonImport____x40_Lean_Elab_Import___hyg_683_), 1, 0);
return x_1;
}
}
static lean_object* _init_l_Lean_Elab_instToJsonImport() {
_start:
{
lean_object* x_1;
x_1 = l_Lean_Elab_instToJsonImport___closed__1;
return x_1;
}
}
static lean_object* _init_l_Lean_Elab_PrintImportResult_imports_x3f___default() {
_start:
{
lean_object* x_1;
x_1 = lean_box(0);
return x_1;
}
}
static lean_object* _init_l_Lean_Elab_PrintImportResult_errors___default___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2;
x_1 = lean_unsigned_to_nat(0u);
x_2 = lean_mk_empty_array_with_capacity(x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_Elab_PrintImportResult_errors___default() {
_start:
{
lean_object* x_1;
x_1 = l_Lean_Elab_PrintImportResult_errors___default___closed__1;
return x_1;
}
}
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Import_0__Lean_Elab_toJsonPrintImportResult____x40_Lean_Elab_Import___hyg_761____spec__2(size_t x_1, size_t x_2, lean_object* x_3) {
_start:
{
uint8_t x_4;
x_4 = lean_usize_dec_lt(x_2, x_1);
if (x_4 == 0)
{
return x_3;
}
else
{
lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; size_t x_9; size_t x_10; lean_object* x_11;
x_5 = lean_array_uget(x_3, x_2);
x_6 = lean_unsigned_to_nat(0u);
x_7 = lean_array_uset(x_3, x_2, x_6);
x_8 = l___private_Lean_Elab_Import_0__Lean_Elab_toJsonImport____x40_Lean_Elab_Import___hyg_683_(x_5);
x_9 = 1;
x_10 = lean_usize_add(x_2, x_9);
x_11 = lean_array_uset(x_7, x_2, x_8);
x_2 = x_10;
x_3 = x_11;
goto _start;
}
}
}
LEAN_EXPORT lean_object* l_Lean_Json_opt___at___private_Lean_Elab_Import_0__Lean_Elab_toJsonPrintImportResult____x40_Lean_Elab_Import___hyg_761____spec__1(lean_object* x_1, lean_object* x_2) {
_start:
{
if (lean_obj_tag(x_2) == 0)
{
lean_object* x_3;
lean_dec(x_1);
x_3 = lean_box(0);
return x_3;
}
else
{
lean_object* x_4; lean_object* x_5; size_t x_6; size_t x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12;
x_4 = lean_ctor_get(x_2, 0);
lean_inc(x_4);
lean_dec(x_2);
x_5 = lean_array_get_size(x_4);
x_6 = lean_usize_of_nat(x_5);
lean_dec(x_5);
x_7 = 0;
x_8 = l_Array_mapMUnsafe_map___at___private_Lean_Elab_Import_0__Lean_Elab_toJsonPrintImportResult____x40_Lean_Elab_Import___hyg_761____spec__2(x_6, x_7, x_4);
x_9 = lean_alloc_ctor(4, 1, 0);
lean_ctor_set(x_9, 0, x_8);
x_10 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_10, 0, x_1);
lean_ctor_set(x_10, 1, x_9);
x_11 = lean_box(0);
x_12 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_12, 0, x_10);
lean_ctor_set(x_12, 1, x_11);
return x_12;
}
}
}
static lean_object* _init_l___private_Lean_Elab_Import_0__Lean_Elab_toJsonPrintImportResult____x40_Lean_Elab_Import___hyg_761____closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string_from_bytes("imports", 7);
return x_1;
}
}
static lean_object* _init_l___private_Lean_Elab_Import_0__Lean_Elab_toJsonPrintImportResult____x40_Lean_Elab_Import___hyg_761____closed__2() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string_from_bytes("errors", 6);
return x_1;
}
}
LEAN_EXPORT lean_object* l___private_Lean_Elab_Import_0__Lean_Elab_toJsonPrintImportResult____x40_Lean_Elab_Import___hyg_761_(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; size_t x_7; size_t 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;
x_2 = lean_ctor_get(x_1, 0);
lean_inc(x_2);
x_3 = l___private_Lean_Elab_Import_0__Lean_Elab_toJsonPrintImportResult____x40_Lean_Elab_Import___hyg_761____closed__1;
x_4 = l_Lean_Json_opt___at___private_Lean_Elab_Import_0__Lean_Elab_toJsonPrintImportResult____x40_Lean_Elab_Import___hyg_761____spec__1(x_3, x_2);
x_5 = lean_ctor_get(x_1, 1);
lean_inc(x_5);
lean_dec(x_1);
x_6 = lean_array_get_size(x_5);
x_7 = lean_usize_of_nat(x_6);
lean_dec(x_6);
x_8 = 0;
x_9 = l_Array_mapMUnsafe_map___at___private_Lean_Data_Lsp_CodeActions_0__Lean_Lsp_toJsonResolveSupport____x40_Lean_Data_Lsp_CodeActions___hyg_1822____spec__1(x_7, x_8, x_5);
x_10 = lean_alloc_ctor(4, 1, 0);
lean_ctor_set(x_10, 0, x_9);
x_11 = l___private_Lean_Elab_Import_0__Lean_Elab_toJsonPrintImportResult____x40_Lean_Elab_Import___hyg_761____closed__2;
x_12 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_12, 0, x_11);
lean_ctor_set(x_12, 1, x_10);
x_13 = lean_box(0);
x_14 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_14, 0, x_12);
lean_ctor_set(x_14, 1, x_13);
x_15 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_15, 0, x_14);
lean_ctor_set(x_15, 1, x_13);
x_16 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_16, 0, x_4);
lean_ctor_set(x_16, 1, x_15);
x_17 = l_List_join___rarg(x_16);
x_18 = l_Lean_Json_mkObj(x_17);
return x_18;
}
}
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Import_0__Lean_Elab_toJsonPrintImportResult____x40_Lean_Elab_Import___hyg_761____spec__2___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
size_t x_4; size_t x_5; lean_object* x_6;
x_4 = lean_unbox_usize(x_1);
lean_dec(x_1);
x_5 = lean_unbox_usize(x_2);
lean_dec(x_2);
x_6 = l_Array_mapMUnsafe_map___at___private_Lean_Elab_Import_0__Lean_Elab_toJsonPrintImportResult____x40_Lean_Elab_Import___hyg_761____spec__2(x_4, x_5, x_3);
return x_6;
}
}
static lean_object* _init_l_Lean_Elab_instToJsonPrintImportResult___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l___private_Lean_Elab_Import_0__Lean_Elab_toJsonPrintImportResult____x40_Lean_Elab_Import___hyg_761_), 1, 0);
return x_1;
}
}
static lean_object* _init_l_Lean_Elab_instToJsonPrintImportResult() {
_start:
{
lean_object* x_1;
x_1 = l_Lean_Elab_instToJsonPrintImportResult___closed__1;
return x_1;
}
}
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Import_0__Lean_Elab_toJsonPrintImportsResult____x40_Lean_Elab_Import___hyg_833____spec__1(size_t x_1, size_t x_2, lean_object* x_3) {
_start:
{
uint8_t x_4;
x_4 = lean_usize_dec_lt(x_2, x_1);
if (x_4 == 0)
{
return x_3;
}
else
{
lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; size_t x_9; size_t x_10; lean_object* x_11;
x_5 = lean_array_uget(x_3, x_2);
x_6 = lean_unsigned_to_nat(0u);
x_7 = lean_array_uset(x_3, x_2, x_6);
x_8 = l___private_Lean_Elab_Import_0__Lean_Elab_toJsonPrintImportResult____x40_Lean_Elab_Import___hyg_761_(x_5);
x_9 = 1;
x_10 = lean_usize_add(x_2, x_9);
x_11 = lean_array_uset(x_7, x_2, x_8);
x_2 = x_10;
x_3 = x_11;
goto _start;
}
}
}
LEAN_EXPORT lean_object* l___private_Lean_Elab_Import_0__Lean_Elab_toJsonPrintImportsResult____x40_Lean_Elab_Import___hyg_833_(lean_object* x_1) {
_start:
{
lean_object* x_2; size_t x_3; size_t 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; lean_object* x_13;
x_2 = lean_array_get_size(x_1);
x_3 = lean_usize_of_nat(x_2);
lean_dec(x_2);
x_4 = 0;
x_5 = l_Array_mapMUnsafe_map___at___private_Lean_Elab_Import_0__Lean_Elab_toJsonPrintImportsResult____x40_Lean_Elab_Import___hyg_833____spec__1(x_3, x_4, x_1);
x_6 = lean_alloc_ctor(4, 1, 0);
lean_ctor_set(x_6, 0, x_5);
x_7 = l___private_Lean_Elab_Import_0__Lean_Elab_toJsonPrintImportResult____x40_Lean_Elab_Import___hyg_761____closed__1;
x_8 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_8, 0, x_7);
lean_ctor_set(x_8, 1, x_6);
x_9 = lean_box(0);
x_10 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_10, 0, x_8);
lean_ctor_set(x_10, 1, x_9);
x_11 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_11, 0, x_10);
lean_ctor_set(x_11, 1, x_9);
x_12 = l_List_join___rarg(x_11);
x_13 = l_Lean_Json_mkObj(x_12);
return x_13;
}
}
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_Import_0__Lean_Elab_toJsonPrintImportsResult____x40_Lean_Elab_Import___hyg_833____spec__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
size_t x_4; size_t x_5; lean_object* x_6;
x_4 = lean_unbox_usize(x_1);
lean_dec(x_1);
x_5 = lean_unbox_usize(x_2);
lean_dec(x_2);
x_6 = l_Array_mapMUnsafe_map___at___private_Lean_Elab_Import_0__Lean_Elab_toJsonPrintImportsResult____x40_Lean_Elab_Import___hyg_833____spec__1(x_4, x_5, x_3);
return x_6;
}
}
static lean_object* _init_l_Lean_Elab_instToJsonPrintImportsResult___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l___private_Lean_Elab_Import_0__Lean_Elab_toJsonPrintImportsResult____x40_Lean_Elab_Import___hyg_833_), 1, 0);
return x_1;
}
}
static lean_object* _init_l_Lean_Elab_instToJsonPrintImportsResult() {
_start:
{
lean_object* x_1;
x_1 = l_Lean_Elab_instToJsonPrintImportsResult___closed__1;
return x_1;
}
}
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_printImportsJson___spec__1(size_t x_1, size_t x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
uint8_t x_5;
x_5 = lean_usize_dec_lt(x_2, x_1);
if (x_5 == 0)
{
lean_object* x_6;
x_6 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_6, 0, x_3);
lean_ctor_set(x_6, 1, x_4);
return x_6;
}
else
{
lean_object* x_7; lean_object* x_8; lean_object* x_9; uint8_t x_10; lean_object* x_11;
x_7 = lean_array_uget(x_3, x_2);
x_8 = lean_unsigned_to_nat(0u);
x_9 = lean_array_uset(x_3, x_2, x_8);
x_10 = 0;
x_11 = l_Lean_Message_toString(x_7, x_10, x_4);
if (lean_obj_tag(x_11) == 0)
{
lean_object* x_12; lean_object* x_13; size_t x_14; size_t x_15; lean_object* x_16;
x_12 = lean_ctor_get(x_11, 0);
lean_inc(x_12);
x_13 = lean_ctor_get(x_11, 1);
lean_inc(x_13);
lean_dec(x_11);
x_14 = 1;
x_15 = lean_usize_add(x_2, x_14);
x_16 = lean_array_uset(x_9, x_2, x_12);
x_2 = x_15;
x_3 = x_16;
x_4 = x_13;
goto _start;
}
else
{
uint8_t x_18;
lean_dec(x_9);
x_18 = !lean_is_exclusive(x_11);
if (x_18 == 0)
{
return x_11;
}
else
{
lean_object* x_19; lean_object* x_20; lean_object* x_21;
x_19 = lean_ctor_get(x_11, 0);
x_20 = lean_ctor_get(x_11, 1);
lean_inc(x_20);
lean_inc(x_19);
lean_dec(x_11);
x_21 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_21, 0, x_19);
lean_ctor_set(x_21, 1, x_20);
return x_21;
}
}
}
}
}
static lean_object* _init_l_Array_mapMUnsafe_map___at_Lean_Elab_printImportsJson___spec__2___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_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_printImportsJson___spec__2(size_t x_1, size_t x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
uint8_t x_5;
x_5 = lean_usize_dec_lt(x_2, x_1);
if (x_5 == 0)
{
lean_object* x_6;
x_6 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_6, 0, x_3);
lean_ctor_set(x_6, 1, x_4);
return x_6;
}
else
{
lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_22;
x_7 = lean_array_uget(x_3, x_2);
x_8 = lean_unsigned_to_nat(0u);
x_9 = lean_array_uset(x_3, x_2, x_8);
x_22 = l_IO_FS_readFile(x_7, x_4);
if (lean_obj_tag(x_22) == 0)
{
lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26;
x_23 = lean_ctor_get(x_22, 0);
lean_inc(x_23);
x_24 = lean_ctor_get(x_22, 1);
lean_inc(x_24);
lean_dec(x_22);
x_25 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_25, 0, x_7);
x_26 = l_Lean_Elab_parseImports(x_23, x_25, x_24);
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; uint8_t x_32;
x_27 = lean_ctor_get(x_26, 0);
lean_inc(x_27);
x_28 = lean_ctor_get(x_27, 1);
lean_inc(x_28);
x_29 = lean_ctor_get(x_26, 1);
lean_inc(x_29);
lean_dec(x_26);
x_30 = lean_ctor_get(x_27, 0);
lean_inc(x_30);
lean_dec(x_27);
x_31 = lean_ctor_get(x_28, 1);
lean_inc(x_31);
lean_dec(x_28);
lean_inc(x_31);
x_32 = l_Lean_PersistentArray_anyM___at_Lean_MessageLog_hasErrors___spec__1(x_31);
if (x_32 == 0)
{
lean_object* x_33; lean_object* x_34; lean_object* x_35; lean_object* x_36; lean_object* x_37; lean_object* x_38; size_t x_39; size_t x_40; lean_object* x_41;
lean_dec(x_31);
x_33 = l_List_redLength___rarg(x_30);
x_34 = lean_mk_empty_array_with_capacity(x_33);
lean_dec(x_33);
x_35 = l_List_toArrayAux___rarg(x_30, x_34);
x_36 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_36, 0, x_35);
x_37 = l_Lean_Elab_PrintImportResult_errors___default___closed__1;
x_38 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_38, 0, x_36);
lean_ctor_set(x_38, 1, x_37);
x_39 = 1;
x_40 = lean_usize_add(x_2, x_39);
x_41 = lean_array_uset(x_9, x_2, x_38);
x_2 = x_40;
x_3 = x_41;
x_4 = x_29;
goto _start;
}
else
{
lean_object* x_43; lean_object* x_44; lean_object* x_45; lean_object* x_46; lean_object* x_47; size_t x_48; size_t x_49; lean_object* x_50;
lean_dec(x_30);
x_43 = l_Lean_MessageLog_toList(x_31);
x_44 = l_List_redLength___rarg(x_43);
x_45 = lean_mk_empty_array_with_capacity(x_44);
lean_dec(x_44);
x_46 = l_List_toArrayAux___rarg(x_43, x_45);
x_47 = lean_array_get_size(x_46);
x_48 = lean_usize_of_nat(x_47);
lean_dec(x_47);
x_49 = 0;
x_50 = l_Array_mapMUnsafe_map___at_Lean_Elab_printImportsJson___spec__1(x_48, x_49, x_46, x_29);
if (lean_obj_tag(x_50) == 0)
{
lean_object* x_51; lean_object* x_52; lean_object* x_53; lean_object* x_54; size_t x_55; size_t x_56; lean_object* x_57;
x_51 = lean_ctor_get(x_50, 0);
lean_inc(x_51);
x_52 = lean_ctor_get(x_50, 1);
lean_inc(x_52);
lean_dec(x_50);
x_53 = lean_box(0);
x_54 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_54, 0, x_53);
lean_ctor_set(x_54, 1, x_51);
x_55 = 1;
x_56 = lean_usize_add(x_2, x_55);
x_57 = lean_array_uset(x_9, x_2, x_54);
x_2 = x_56;
x_3 = x_57;
x_4 = x_52;
goto _start;
}
else
{
lean_object* x_59; lean_object* x_60;
x_59 = lean_ctor_get(x_50, 0);
lean_inc(x_59);
x_60 = lean_ctor_get(x_50, 1);
lean_inc(x_60);
lean_dec(x_50);
x_10 = x_59;
x_11 = x_60;
goto block_21;
}
}
}
else
{
lean_object* x_61; lean_object* x_62;
x_61 = lean_ctor_get(x_26, 0);
lean_inc(x_61);
x_62 = lean_ctor_get(x_26, 1);
lean_inc(x_62);
lean_dec(x_26);
x_10 = x_61;
x_11 = x_62;
goto block_21;
}
}
else
{
lean_object* x_63; lean_object* x_64;
lean_dec(x_7);
x_63 = lean_ctor_get(x_22, 0);
lean_inc(x_63);
x_64 = lean_ctor_get(x_22, 1);
lean_inc(x_64);
lean_dec(x_22);
x_10 = x_63;
x_11 = x_64;
goto block_21;
}
block_21:
{
lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; size_t x_17; size_t x_18; lean_object* x_19;
x_12 = lean_box(0);
x_13 = lean_io_error_to_string(x_10);
x_14 = l_Array_mapMUnsafe_map___at_Lean_Elab_printImportsJson___spec__2___closed__1;
x_15 = lean_array_push(x_14, x_13);
x_16 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_16, 0, x_12);
lean_ctor_set(x_16, 1, x_15);
x_17 = 1;
x_18 = lean_usize_add(x_2, x_17);
x_19 = lean_array_uset(x_9, x_2, x_16);
x_2 = x_18;
x_3 = x_19;
x_4 = x_11;
goto _start;
}
}
}
}
LEAN_EXPORT lean_object* l_IO_println___at_Lean_Elab_printImportsJson___spec__3(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3; lean_object* x_4; uint32_t x_5; lean_object* x_6; lean_object* x_7;
x_3 = lean_unsigned_to_nat(80u);
x_4 = l_Lean_Json_pretty(x_1, x_3);
x_5 = 10;
x_6 = lean_string_push(x_4, x_5);
x_7 = l_IO_print___at_IO_println___spec__1(x_6, x_2);
return x_7;
}
}
LEAN_EXPORT lean_object* lean_print_imports_json(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3; size_t x_4; size_t 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_array_get_size(x_1);
x_4 = lean_usize_of_nat(x_3);
lean_dec(x_3);
x_5 = 0;
x_6 = l_Array_mapMUnsafe_map___at_Lean_Elab_printImportsJson___spec__2(x_4, x_5, x_1, x_2);
x_7 = lean_ctor_get(x_6, 0);
lean_inc(x_7);
x_8 = lean_ctor_get(x_6, 1);
lean_inc(x_8);
lean_dec(x_6);
x_9 = l___private_Lean_Elab_Import_0__Lean_Elab_toJsonPrintImportsResult____x40_Lean_Elab_Import___hyg_833_(x_7);
x_10 = l_IO_println___at_Lean_Elab_printImportsJson___spec__3(x_9, x_8);
return x_10;
}
}
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_printImportsJson___spec__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
size_t x_5; size_t x_6; lean_object* x_7;
x_5 = lean_unbox_usize(x_1);
lean_dec(x_1);
x_6 = lean_unbox_usize(x_2);
lean_dec(x_2);
x_7 = l_Array_mapMUnsafe_map___at_Lean_Elab_printImportsJson___spec__1(x_5, x_6, x_3, x_4);
return x_7;
}
}
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_Elab_printImportsJson___spec__2___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
size_t x_5; size_t x_6; lean_object* x_7;
x_5 = lean_unbox_usize(x_1);
lean_dec(x_1);
x_6 = lean_unbox_usize(x_2);
lean_dec(x_2);
x_7 = l_Array_mapMUnsafe_map___at_Lean_Elab_printImportsJson___spec__2(x_5, x_6, x_3, x_4);
return x_7;
}
}
lean_object* initialize_Init(uint8_t builtin, lean_object*);
lean_object* initialize_Lean_Parser_Module(uint8_t builtin, lean_object*);
lean_object* initialize_Lean_Data_Json(uint8_t builtin, lean_object*);
@ -1750,34 +1093,6 @@ l_Lean_Elab_processHeader___closed__1 = _init_l_Lean_Elab_processHeader___closed
lean_mark_persistent(l_Lean_Elab_processHeader___closed__1);
l_Lean_Elab_parseImports___closed__1 = _init_l_Lean_Elab_parseImports___closed__1();
lean_mark_persistent(l_Lean_Elab_parseImports___closed__1);
l___private_Lean_Elab_Import_0__Lean_Elab_toJsonImport____x40_Lean_Elab_Import___hyg_683____closed__1 = _init_l___private_Lean_Elab_Import_0__Lean_Elab_toJsonImport____x40_Lean_Elab_Import___hyg_683____closed__1();
lean_mark_persistent(l___private_Lean_Elab_Import_0__Lean_Elab_toJsonImport____x40_Lean_Elab_Import___hyg_683____closed__1);
l___private_Lean_Elab_Import_0__Lean_Elab_toJsonImport____x40_Lean_Elab_Import___hyg_683____closed__2 = _init_l___private_Lean_Elab_Import_0__Lean_Elab_toJsonImport____x40_Lean_Elab_Import___hyg_683____closed__2();
lean_mark_persistent(l___private_Lean_Elab_Import_0__Lean_Elab_toJsonImport____x40_Lean_Elab_Import___hyg_683____closed__2);
l_Lean_Elab_instToJsonImport___closed__1 = _init_l_Lean_Elab_instToJsonImport___closed__1();
lean_mark_persistent(l_Lean_Elab_instToJsonImport___closed__1);
l_Lean_Elab_instToJsonImport = _init_l_Lean_Elab_instToJsonImport();
lean_mark_persistent(l_Lean_Elab_instToJsonImport);
l_Lean_Elab_PrintImportResult_imports_x3f___default = _init_l_Lean_Elab_PrintImportResult_imports_x3f___default();
lean_mark_persistent(l_Lean_Elab_PrintImportResult_imports_x3f___default);
l_Lean_Elab_PrintImportResult_errors___default___closed__1 = _init_l_Lean_Elab_PrintImportResult_errors___default___closed__1();
lean_mark_persistent(l_Lean_Elab_PrintImportResult_errors___default___closed__1);
l_Lean_Elab_PrintImportResult_errors___default = _init_l_Lean_Elab_PrintImportResult_errors___default();
lean_mark_persistent(l_Lean_Elab_PrintImportResult_errors___default);
l___private_Lean_Elab_Import_0__Lean_Elab_toJsonPrintImportResult____x40_Lean_Elab_Import___hyg_761____closed__1 = _init_l___private_Lean_Elab_Import_0__Lean_Elab_toJsonPrintImportResult____x40_Lean_Elab_Import___hyg_761____closed__1();
lean_mark_persistent(l___private_Lean_Elab_Import_0__Lean_Elab_toJsonPrintImportResult____x40_Lean_Elab_Import___hyg_761____closed__1);
l___private_Lean_Elab_Import_0__Lean_Elab_toJsonPrintImportResult____x40_Lean_Elab_Import___hyg_761____closed__2 = _init_l___private_Lean_Elab_Import_0__Lean_Elab_toJsonPrintImportResult____x40_Lean_Elab_Import___hyg_761____closed__2();
lean_mark_persistent(l___private_Lean_Elab_Import_0__Lean_Elab_toJsonPrintImportResult____x40_Lean_Elab_Import___hyg_761____closed__2);
l_Lean_Elab_instToJsonPrintImportResult___closed__1 = _init_l_Lean_Elab_instToJsonPrintImportResult___closed__1();
lean_mark_persistent(l_Lean_Elab_instToJsonPrintImportResult___closed__1);
l_Lean_Elab_instToJsonPrintImportResult = _init_l_Lean_Elab_instToJsonPrintImportResult();
lean_mark_persistent(l_Lean_Elab_instToJsonPrintImportResult);
l_Lean_Elab_instToJsonPrintImportsResult___closed__1 = _init_l_Lean_Elab_instToJsonPrintImportsResult___closed__1();
lean_mark_persistent(l_Lean_Elab_instToJsonPrintImportsResult___closed__1);
l_Lean_Elab_instToJsonPrintImportsResult = _init_l_Lean_Elab_instToJsonPrintImportsResult();
lean_mark_persistent(l_Lean_Elab_instToJsonPrintImportsResult);
l_Array_mapMUnsafe_map___at_Lean_Elab_printImportsJson___spec__2___closed__1 = _init_l_Array_mapMUnsafe_map___at_Lean_Elab_printImportsJson___spec__2___closed__1();
lean_mark_persistent(l_Array_mapMUnsafe_map___at_Lean_Elab_printImportsJson___spec__2___closed__1);
return lean_io_result_mk_ok(lean_box(0));
}
#ifdef __cplusplus

763
stage0/stdlib/Lean/Elab/ParseImportsFast.c generated
View file

@ -13,21 +13,35 @@
#ifdef __cplusplus
extern "C" {
#endif
LEAN_EXPORT lean_object* l_Lean_ParseImports_keywordCore_go___at_Lean_ParseImports_preludeOpt___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_ParseImports_takeUntil___at_Lean_ParseImports_takeWhile___spec__1(lean_object*, lean_object*, lean_object*);
size_t lean_usize_add(size_t, size_t);
LEAN_EXPORT lean_object* l_Lean_ParseImports_instInhabitedState;
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_printImportsJson___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Array_mapMUnsafe_map___at_Lean_printImportsJson___spec__1___closed__1;
static lean_object* l_Lean_ParseImports_keywordCore_go___at_Lean_ParseImports_preludeOpt___spec__1___closed__1;
static lean_object* l_Lean_ParseImports_keywordCore_go___at_Lean_ParseImports_keyword___spec__1___closed__1;
lean_object* lean_mk_empty_array_with_capacity(lean_object*);
LEAN_EXPORT lean_object* l_Lean_ParseImports_keyword(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_Json_opt___at___private_Lean_Elab_ParseImportsFast_0__Lean_toJsonPrintImportResult____x40_Lean_Elab_ParseImportsFast___hyg_1704____spec__1(lean_object*, lean_object*);
lean_object* l_Lean_Name_str___override(lean_object*, lean_object*);
static lean_object* l_Lean_ParseImports_many___at_Lean_ParseImports_main___spec__3___closed__1;
static lean_object* l_Lean_ParseImports_keywordCore_go___at_Lean_ParseImports_preludeOpt___spec__1___closed__2;
lean_object* lean_array_uget(lean_object*, size_t);
lean_object* lean_io_error_to_string(lean_object*);
extern uint32_t l_Lean_idBeginEscape;
static lean_object* l_Lean_ParseImports_keywordCore_go___at_Lean_ParseImports_keyword___spec__1___closed__2;
LEAN_EXPORT lean_object* l_Lean_instToJsonPrintImportResult;
LEAN_EXPORT lean_object* l_Lean_ParseImports_takeUntil___at_Lean_ParseImports_takeWhile___spec__1___boxed(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* lean_print_imports_json(lean_object*, lean_object*);
static lean_object* l___private_Lean_Elab_ParseImportsFast_0__Lean_toJsonImport____x40_Lean_Elab_ParseImportsFast___hyg_1620____closed__2;
lean_object* lean_array_uset(lean_object*, size_t, lean_object*);
LEAN_EXPORT lean_object* l_Lean_ParseImports_isIdRestCold___boxed(lean_object*);
static lean_object* l_Lean_ParseImports_instInhabitedState___closed__1;
static lean_object* l_Lean_ParseImports_moduleIdent_parse___closed__4;
LEAN_EXPORT uint8_t l_Lean_ParseImports_isIdRestCold(uint32_t);
LEAN_EXPORT lean_object* l_Lean_ParseImports_keywordCore_go___at_Lean_ParseImports_keywordOpt___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_ParseImports_keywordCore_go___at_Lean_ParseImports_preludeOpt___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Elab_ParseImportsFast_0__Lean_toJsonPrintImportResult____x40_Lean_Elab_ParseImportsFast___hyg_1704_(lean_object*);
extern uint32_t l_Lean_idEndEscape;
static lean_object* l_Lean_ParseImports_finishCommentBlock_eoi___closed__1;
static lean_object* l_Lean_parseImports_x27___closed__1;
@ -43,10 +57,12 @@ uint8_t l_Char_isWhitespace(uint32_t);
LEAN_EXPORT lean_object* l_Lean_ParseImports_keywordCore_go___at_Lean_ParseImports_keyword___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_shrink___rarg(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_ParseImports_keywordCore_go___at_Lean_ParseImports_keyword___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_instToJsonPrintImportsResult___closed__1;
LEAN_EXPORT lean_object* l_Lean_ParseImports_moduleIdent(uint8_t, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_ParseImports_State_error_x3f___default;
lean_object* l_List_join___rarg(lean_object*);
uint8_t lean_usize_dec_lt(size_t, size_t);
static lean_object* l_Lean_ParseImports_keywordCore_go___at_Lean_ParseImports_main___spec__1___closed__3;
LEAN_EXPORT lean_object* l_Lean_ParseImports_keywordOpt___boxed(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_ParseImports_takeUntil___boxed(lean_object*, lean_object*, lean_object*);
lean_object* lean_nat_add(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_ParseImports_State_next_x27___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
@ -54,14 +70,21 @@ LEAN_EXPORT lean_object* l_Lean_ParseImports_instInhabitedParser___boxed(lean_ob
lean_object* lean_string_utf8_next(lean_object*, lean_object*);
static lean_object* l_Lean_ParseImports_main___closed__1;
LEAN_EXPORT lean_object* l_Lean_ParseImports_State_mkEOIError(lean_object*);
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_printImportsJson___spec__1(size_t, size_t, lean_object*, lean_object*);
static lean_object* l___private_Lean_Elab_ParseImportsFast_0__Lean_toJsonPrintImportResult____x40_Lean_Elab_ParseImportsFast___hyg_1704____closed__2;
LEAN_EXPORT lean_object* l_Lean_ParseImports_moduleIdent_parse(uint8_t, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_instToJsonImport;
lean_object* l_Lean_Json_compress(lean_object*);
LEAN_EXPORT lean_object* l_Lean_ParseImports_moduleIdent___boxed(lean_object*, lean_object*, lean_object*);
lean_object* lean_nat_sub(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_ParseImports_andthen(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_ParseImports_State_imports___default;
LEAN_EXPORT lean_object* l_Lean_ParseImports_takeUntil___at_Lean_ParseImports_moduleIdent_parse___spec__2___boxed(lean_object*, lean_object*);
static lean_object* l___private_Lean_Elab_ParseImportsFast_0__Lean_toJsonPrintImportResult____x40_Lean_Elab_ParseImportsFast___hyg_1704____closed__1;
lean_object* l_Lean_Name_toString(lean_object*, uint8_t);
lean_object* lean_string_utf8_next_fast(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_ParseImports_isIdCont___boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Elab_ParseImportsFast_0__Lean_toJsonImport____x40_Lean_Elab_ParseImportsFast___hyg_1620_(lean_object*);
static lean_object* l_Lean_ParseImports_State_mkEOIError___closed__1;
static lean_object* l_Lean_ParseImports_moduleIdent_parse___closed__3;
LEAN_EXPORT lean_object* l_Lean_ParseImports_keywordCore(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -69,26 +92,33 @@ LEAN_EXPORT lean_object* l_Lean_ParseImports_keywordCore_go(lean_object*, lean_o
LEAN_EXPORT lean_object* l_Lean_ParseImports_keywordCore_go___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint32_t lean_string_utf8_get(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_ParseImports_instInhabitedParser___rarg___boxed(lean_object*);
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_ParseImportsFast_0__Lean_toJsonPrintImportResult____x40_Lean_Elab_ParseImportsFast___hyg_1704____spec__2(size_t, size_t, lean_object*);
LEAN_EXPORT lean_object* l_Lean_ParseImports_takeUntil___at_Lean_ParseImports_moduleIdent_parse___spec__1___boxed(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_ParseImports_takeUntil(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT uint8_t l_Lean_ParseImports_isIdRestFast(uint32_t);
lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Data_Lsp_CodeActions_0__Lean_Lsp_toJsonResolveSupport____x40_Lean_Data_Lsp_CodeActions___hyg_1822____spec__1(size_t, size_t, lean_object*);
LEAN_EXPORT lean_object* l_Lean_ParseImports_isIdRestFast___boxed(lean_object*);
static lean_object* l_Lean_ParseImports_moduleIdent_parse___closed__1;
LEAN_EXPORT lean_object* l_Lean_parseImports_x27(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_ParseImports_keywordCore_go___at_Lean_ParseImports_main___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_ParseImports_State_mkError(lean_object*, lean_object*);
static lean_object* l_Lean_ParseImports_keywordCore_go___at_Lean_ParseImports_main___spec__1___closed__1;
size_t lean_usize_of_nat(lean_object*);
LEAN_EXPORT lean_object* l_Lean_ParseImports_takeUntil___at_Lean_ParseImports_moduleIdent_parse___spec__1(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_ParseImports_keywordCore_go___at_Lean_ParseImports_main___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_ParseImports_keywordCore___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_ParseImports_preludeOpt___boxed(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_instToJsonPrintImportsResult;
LEAN_EXPORT lean_object* l_Lean_ParseImports_State_pushModule___boxed(lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_isLetterLike(uint32_t);
LEAN_EXPORT lean_object* l_Lean_ParseImports_preludeOpt(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_ParseImports_takeWhile___boxed(lean_object*, lean_object*, lean_object*);
uint8_t lean_uint32_dec_eq(uint32_t, uint32_t);
LEAN_EXPORT lean_object* l_Lean_ParseImports_State_next(lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_ParseImports_State_mkEOIError___closed__2;
static lean_object* l_Lean_ParseImports_keywordCore_go___at_Lean_ParseImports_main___spec__1___closed__2;
LEAN_EXPORT lean_object* l_Lean_ParseImports_keywordCore_go___at_Lean_ParseImports_main___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_PrintImportResult_errors___default;
LEAN_EXPORT lean_object* l_Lean_ParseImports_many___at_Lean_ParseImports_main___spec__3(lean_object*, lean_object*, lean_object*);
uint8_t l_Char_isAlphanum(uint32_t);
static lean_object* l_Lean_ParseImports_moduleIdent_parse___closed__2;
@ -96,27 +126,35 @@ LEAN_EXPORT lean_object* l_Lean_ParseImports_State_pushModule(lean_object*, uint
LEAN_EXPORT lean_object* l_Lean_ParseImports_whitespace___boxed(lean_object*, lean_object*);
static lean_object* l_Lean_ParseImports_whitespace___closed__1;
LEAN_EXPORT lean_object* l_Lean_ParseImports_many(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Json_mkObj(lean_object*);
static lean_object* l_Lean_ParseImports_whitespace___closed__2;
LEAN_EXPORT lean_object* l_Lean_ParseImports_keywordCore_go___at_Lean_ParseImports_main___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_ParseImports_keywordCore_go___at_Lean_ParseImports_main___spec__1___closed__4;
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_ParseImports_keywordCore_go___at_Lean_ParseImports_keywordOpt___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_PrintImportResult_imports_x3f___default;
static lean_object* l_Lean_instToJsonImport___closed__1;
LEAN_EXPORT lean_object* l_Lean_ParseImports_takeUntil___at_Lean_ParseImports_whitespace___spec__1(lean_object*, lean_object*);
static lean_object* l_Lean_instToJsonPrintImportResult___closed__1;
LEAN_EXPORT lean_object* l_Lean_ParseImports_takeUntil___at_Lean_ParseImports_moduleIdent_parse___spec__2(lean_object*, lean_object*);
uint8_t l_Lean_isIdFirst(uint32_t);
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_ParseImportsFast_0__Lean_toJsonPrintImportsResult____x40_Lean_Elab_ParseImportsFast___hyg_1774____spec__1___boxed(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_ParseImports_State_next___boxed(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_ParseImports_instInhabitedParser(lean_object*);
lean_object* l_IO_FS_readFile(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_ParseImports_takeWhile(lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_isSubScriptAlnum(uint32_t);
lean_object* l_IO_println___at_Lean_instEval___spec__1(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_ParseImports_moduleIdent_parse___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_ParseImports_whitespace(lean_object*, lean_object*);
static lean_object* l_Lean_ParseImports_State_imports___default___closed__1;
LEAN_EXPORT lean_object* l_Lean_ParseImports_finishCommentBlock___boxed(lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_ParseImports_finishCommentBlock_eoi___closed__2;
LEAN_EXPORT lean_object* l_Lean_ParseImports_State_pos___default;
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_ParseImportsFast_0__Lean_toJsonPrintImportResult____x40_Lean_Elab_ParseImportsFast___hyg_1704____spec__2___boxed(lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_parseImports_x27___closed__2;
LEAN_EXPORT lean_object* l_Lean_ParseImports_State_next_x27(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_ParseImports_State_setPos(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_ParseImportsFast_0__Lean_toJsonPrintImportsResult____x40_Lean_Elab_ParseImportsFast___hyg_1774____spec__1(size_t, size_t, lean_object*);
LEAN_EXPORT lean_object* l_Lean_ParseImports_finishCommentBlock(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_ParseImports_instAndThenParser(lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_ParseImports_main(lean_object*, lean_object*);
@ -124,7 +162,8 @@ uint8_t lean_string_utf8_at_end(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_ParseImports_instInhabitedParser___rarg(lean_object*);
LEAN_EXPORT lean_object* l_Lean_ParseImports_many___at_Lean_ParseImports_main___spec__3___boxed(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_ParseImports_keyword___boxed(lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l_Lean_ParseImports_keywordOpt(lean_object*, lean_object*, lean_object*);
static lean_object* l___private_Lean_Elab_ParseImportsFast_0__Lean_toJsonImport____x40_Lean_Elab_ParseImportsFast___hyg_1620____closed__1;
LEAN_EXPORT lean_object* l___private_Lean_Elab_ParseImportsFast_0__Lean_toJsonPrintImportsResult____x40_Lean_Elab_ParseImportsFast___hyg_1774_(lean_object*);
LEAN_EXPORT uint8_t l_Lean_ParseImports_isIdCont(lean_object*, lean_object*);
static lean_object* _init_l_Lean_ParseImports_State_imports___default___closed__1() {
_start:
@ -1634,109 +1673,6 @@ lean_dec(x_1);
return x_4;
}
}
LEAN_EXPORT lean_object* l_Lean_ParseImports_keywordCore_go___at_Lean_ParseImports_keywordOpt___spec__1(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_4);
if (x_6 == 0)
{
uint8_t x_7;
x_7 = lean_string_utf8_at_end(x_2, x_5);
if (x_7 == 0)
{
uint32_t x_8; uint32_t x_9; uint8_t x_10;
x_8 = lean_string_utf8_get_fast(x_1, x_4);
x_9 = lean_string_utf8_get_fast(x_2, x_5);
x_10 = lean_uint32_dec_eq(x_8, x_9);
if (x_10 == 0)
{
lean_dec(x_5);
lean_dec(x_4);
return x_3;
}
else
{
lean_object* x_11; lean_object* x_12;
x_11 = lean_string_utf8_next_fast(x_1, x_4);
lean_dec(x_4);
x_12 = lean_string_utf8_next_fast(x_2, x_5);
lean_dec(x_5);
x_4 = x_11;
x_5 = x_12;
goto _start;
}
}
else
{
lean_dec(x_5);
lean_dec(x_4);
return x_3;
}
}
else
{
uint8_t x_14;
lean_dec(x_4);
x_14 = !lean_is_exclusive(x_3);
if (x_14 == 0)
{
lean_object* x_15; lean_object* x_16;
x_15 = lean_ctor_get(x_3, 1);
lean_dec(x_15);
lean_ctor_set(x_3, 1, x_5);
x_16 = l_Lean_ParseImports_whitespace(x_2, x_3);
return x_16;
}
else
{
lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20;
x_17 = lean_ctor_get(x_3, 0);
x_18 = lean_ctor_get(x_3, 2);
lean_inc(x_18);
lean_inc(x_17);
lean_dec(x_3);
x_19 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_19, 0, x_17);
lean_ctor_set(x_19, 1, x_5);
lean_ctor_set(x_19, 2, x_18);
x_20 = l_Lean_ParseImports_whitespace(x_2, x_19);
return x_20;
}
}
}
}
LEAN_EXPORT lean_object* l_Lean_ParseImports_keywordOpt(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, 1);
lean_inc(x_4);
x_5 = lean_unsigned_to_nat(0u);
x_6 = l_Lean_ParseImports_keywordCore_go___at_Lean_ParseImports_keywordOpt___spec__1(x_1, x_2, x_3, x_5, x_4);
return x_6;
}
}
LEAN_EXPORT lean_object* l_Lean_ParseImports_keywordCore_go___at_Lean_ParseImports_keywordOpt___spec__1___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_Lean_ParseImports_keywordCore_go___at_Lean_ParseImports_keywordOpt___spec__1(x_1, x_2, x_3, x_4, x_5);
lean_dec(x_2);
lean_dec(x_1);
return x_6;
}
}
LEAN_EXPORT lean_object* l_Lean_ParseImports_keywordOpt___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
x_4 = l_Lean_ParseImports_keywordOpt(x_1, x_2, x_3);
lean_dec(x_2);
lean_dec(x_1);
return x_4;
}
}
LEAN_EXPORT uint8_t l_Lean_ParseImports_isIdCont(lean_object* x_1, lean_object* x_2) {
_start:
{
@ -3157,6 +3093,135 @@ return x_22;
}
}
}
static lean_object* _init_l_Lean_ParseImports_keywordCore_go___at_Lean_ParseImports_preludeOpt___spec__1___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string_from_bytes("Init", 4);
return x_1;
}
}
static lean_object* _init_l_Lean_ParseImports_keywordCore_go___at_Lean_ParseImports_preludeOpt___spec__1___closed__2() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3;
x_1 = lean_box(0);
x_2 = l_Lean_ParseImports_keywordCore_go___at_Lean_ParseImports_preludeOpt___spec__1___closed__1;
x_3 = l_Lean_Name_str___override(x_1, x_2);
return x_3;
}
}
LEAN_EXPORT lean_object* l_Lean_ParseImports_keywordCore_go___at_Lean_ParseImports_preludeOpt___spec__1(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_4);
if (x_6 == 0)
{
uint8_t x_7;
x_7 = lean_string_utf8_at_end(x_2, x_5);
if (x_7 == 0)
{
uint32_t x_8; uint32_t x_9; uint8_t x_10;
x_8 = lean_string_utf8_get_fast(x_1, x_4);
x_9 = lean_string_utf8_get_fast(x_2, x_5);
x_10 = lean_uint32_dec_eq(x_8, x_9);
if (x_10 == 0)
{
lean_object* x_11; uint8_t x_12; lean_object* x_13;
lean_dec(x_5);
lean_dec(x_4);
x_11 = l_Lean_ParseImports_keywordCore_go___at_Lean_ParseImports_preludeOpt___spec__1___closed__2;
x_12 = 0;
x_13 = l_Lean_ParseImports_State_pushModule(x_11, x_12, x_3);
return x_13;
}
else
{
lean_object* x_14; lean_object* x_15;
x_14 = lean_string_utf8_next_fast(x_1, x_4);
lean_dec(x_4);
x_15 = lean_string_utf8_next_fast(x_2, x_5);
lean_dec(x_5);
x_4 = x_14;
x_5 = x_15;
goto _start;
}
}
else
{
lean_object* x_17; uint8_t x_18; lean_object* x_19;
lean_dec(x_5);
lean_dec(x_4);
x_17 = l_Lean_ParseImports_keywordCore_go___at_Lean_ParseImports_preludeOpt___spec__1___closed__2;
x_18 = 0;
x_19 = l_Lean_ParseImports_State_pushModule(x_17, x_18, x_3);
return x_19;
}
}
else
{
uint8_t x_20;
lean_dec(x_4);
x_20 = !lean_is_exclusive(x_3);
if (x_20 == 0)
{
lean_object* x_21; lean_object* x_22;
x_21 = lean_ctor_get(x_3, 1);
lean_dec(x_21);
lean_ctor_set(x_3, 1, x_5);
x_22 = l_Lean_ParseImports_whitespace(x_2, x_3);
return x_22;
}
else
{
lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26;
x_23 = lean_ctor_get(x_3, 0);
x_24 = lean_ctor_get(x_3, 2);
lean_inc(x_24);
lean_inc(x_23);
lean_dec(x_3);
x_25 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_25, 0, x_23);
lean_ctor_set(x_25, 1, x_5);
lean_ctor_set(x_25, 2, x_24);
x_26 = l_Lean_ParseImports_whitespace(x_2, x_25);
return x_26;
}
}
}
}
LEAN_EXPORT lean_object* l_Lean_ParseImports_preludeOpt(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, 1);
lean_inc(x_4);
x_5 = lean_unsigned_to_nat(0u);
x_6 = l_Lean_ParseImports_keywordCore_go___at_Lean_ParseImports_preludeOpt___spec__1(x_1, x_2, x_3, x_5, x_4);
return x_6;
}
}
LEAN_EXPORT lean_object* l_Lean_ParseImports_keywordCore_go___at_Lean_ParseImports_preludeOpt___spec__1___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_Lean_ParseImports_keywordCore_go___at_Lean_ParseImports_preludeOpt___spec__1(x_1, x_2, x_3, x_4, x_5);
lean_dec(x_2);
lean_dec(x_1);
return x_6;
}
}
LEAN_EXPORT lean_object* l_Lean_ParseImports_preludeOpt___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
x_4 = l_Lean_ParseImports_preludeOpt(x_1, x_2, x_3);
lean_dec(x_2);
lean_dec(x_1);
return x_4;
}
}
static lean_object* _init_l_Lean_ParseImports_keywordCore_go___at_Lean_ParseImports_main___spec__1___closed__1() {
_start:
{
@ -3565,7 +3630,7 @@ x_3 = lean_ctor_get(x_2, 1);
lean_inc(x_3);
x_4 = l_Lean_ParseImports_main___closed__1;
x_5 = lean_unsigned_to_nat(0u);
x_6 = l_Lean_ParseImports_keywordCore_go___at_Lean_ParseImports_keywordOpt___spec__1(x_4, x_1, x_2, x_5, x_3);
x_6 = l_Lean_ParseImports_keywordCore_go___at_Lean_ParseImports_preludeOpt___spec__1(x_4, x_1, x_2, x_5, x_3);
x_7 = lean_ctor_get(x_6, 2);
lean_inc(x_7);
if (lean_obj_tag(x_7) == 0)
@ -3680,6 +3745,458 @@ lean_dec(x_2);
return x_4;
}
}
static lean_object* _init_l___private_Lean_Elab_ParseImportsFast_0__Lean_toJsonImport____x40_Lean_Elab_ParseImportsFast___hyg_1620____closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string_from_bytes("module", 6);
return x_1;
}
}
static lean_object* _init_l___private_Lean_Elab_ParseImportsFast_0__Lean_toJsonImport____x40_Lean_Elab_ParseImportsFast___hyg_1620____closed__2() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string_from_bytes("runtimeOnly", 11);
return x_1;
}
}
LEAN_EXPORT lean_object* l___private_Lean_Elab_ParseImportsFast_0__Lean_toJsonImport____x40_Lean_Elab_ParseImportsFast___hyg_1620_(lean_object* x_1) {
_start:
{
lean_object* x_2; uint8_t 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; uint8_t 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;
x_2 = lean_ctor_get(x_1, 0);
lean_inc(x_2);
x_3 = 1;
x_4 = l_Lean_Name_toString(x_2, x_3);
x_5 = lean_alloc_ctor(3, 1, 0);
lean_ctor_set(x_5, 0, x_4);
x_6 = l___private_Lean_Elab_ParseImportsFast_0__Lean_toJsonImport____x40_Lean_Elab_ParseImportsFast___hyg_1620____closed__1;
x_7 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_7, 0, x_6);
lean_ctor_set(x_7, 1, x_5);
x_8 = lean_box(0);
x_9 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_9, 0, x_7);
lean_ctor_set(x_9, 1, x_8);
x_10 = lean_ctor_get_uint8(x_1, sizeof(void*)*1);
lean_dec(x_1);
x_11 = lean_alloc_ctor(1, 0, 1);
lean_ctor_set_uint8(x_11, 0, x_10);
x_12 = l___private_Lean_Elab_ParseImportsFast_0__Lean_toJsonImport____x40_Lean_Elab_ParseImportsFast___hyg_1620____closed__2;
x_13 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_13, 0, x_12);
lean_ctor_set(x_13, 1, x_11);
x_14 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_14, 0, x_13);
lean_ctor_set(x_14, 1, x_8);
x_15 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_15, 0, x_14);
lean_ctor_set(x_15, 1, x_8);
x_16 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_16, 0, x_9);
lean_ctor_set(x_16, 1, x_15);
x_17 = l_List_join___rarg(x_16);
x_18 = l_Lean_Json_mkObj(x_17);
return x_18;
}
}
static lean_object* _init_l_Lean_instToJsonImport___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l___private_Lean_Elab_ParseImportsFast_0__Lean_toJsonImport____x40_Lean_Elab_ParseImportsFast___hyg_1620_), 1, 0);
return x_1;
}
}
static lean_object* _init_l_Lean_instToJsonImport() {
_start:
{
lean_object* x_1;
x_1 = l_Lean_instToJsonImport___closed__1;
return x_1;
}
}
static lean_object* _init_l_Lean_PrintImportResult_imports_x3f___default() {
_start:
{
lean_object* x_1;
x_1 = lean_box(0);
return x_1;
}
}
static lean_object* _init_l_Lean_PrintImportResult_errors___default() {
_start:
{
lean_object* x_1;
x_1 = l_Lean_ParseImports_State_imports___default___closed__1;
return x_1;
}
}
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_ParseImportsFast_0__Lean_toJsonPrintImportResult____x40_Lean_Elab_ParseImportsFast___hyg_1704____spec__2(size_t x_1, size_t x_2, lean_object* x_3) {
_start:
{
uint8_t x_4;
x_4 = lean_usize_dec_lt(x_2, x_1);
if (x_4 == 0)
{
return x_3;
}
else
{
lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; size_t x_9; size_t x_10; lean_object* x_11;
x_5 = lean_array_uget(x_3, x_2);
x_6 = lean_unsigned_to_nat(0u);
x_7 = lean_array_uset(x_3, x_2, x_6);
x_8 = l___private_Lean_Elab_ParseImportsFast_0__Lean_toJsonImport____x40_Lean_Elab_ParseImportsFast___hyg_1620_(x_5);
x_9 = 1;
x_10 = lean_usize_add(x_2, x_9);
x_11 = lean_array_uset(x_7, x_2, x_8);
x_2 = x_10;
x_3 = x_11;
goto _start;
}
}
}
LEAN_EXPORT lean_object* l_Lean_Json_opt___at___private_Lean_Elab_ParseImportsFast_0__Lean_toJsonPrintImportResult____x40_Lean_Elab_ParseImportsFast___hyg_1704____spec__1(lean_object* x_1, lean_object* x_2) {
_start:
{
if (lean_obj_tag(x_2) == 0)
{
lean_object* x_3;
lean_dec(x_1);
x_3 = lean_box(0);
return x_3;
}
else
{
lean_object* x_4; lean_object* x_5; size_t x_6; size_t x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12;
x_4 = lean_ctor_get(x_2, 0);
lean_inc(x_4);
lean_dec(x_2);
x_5 = lean_array_get_size(x_4);
x_6 = lean_usize_of_nat(x_5);
lean_dec(x_5);
x_7 = 0;
x_8 = l_Array_mapMUnsafe_map___at___private_Lean_Elab_ParseImportsFast_0__Lean_toJsonPrintImportResult____x40_Lean_Elab_ParseImportsFast___hyg_1704____spec__2(x_6, x_7, x_4);
x_9 = lean_alloc_ctor(4, 1, 0);
lean_ctor_set(x_9, 0, x_8);
x_10 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_10, 0, x_1);
lean_ctor_set(x_10, 1, x_9);
x_11 = lean_box(0);
x_12 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_12, 0, x_10);
lean_ctor_set(x_12, 1, x_11);
return x_12;
}
}
}
static lean_object* _init_l___private_Lean_Elab_ParseImportsFast_0__Lean_toJsonPrintImportResult____x40_Lean_Elab_ParseImportsFast___hyg_1704____closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string_from_bytes("imports", 7);
return x_1;
}
}
static lean_object* _init_l___private_Lean_Elab_ParseImportsFast_0__Lean_toJsonPrintImportResult____x40_Lean_Elab_ParseImportsFast___hyg_1704____closed__2() {
_start:
{
lean_object* x_1;
x_1 = lean_mk_string_from_bytes("errors", 6);
return x_1;
}
}
LEAN_EXPORT lean_object* l___private_Lean_Elab_ParseImportsFast_0__Lean_toJsonPrintImportResult____x40_Lean_Elab_ParseImportsFast___hyg_1704_(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; size_t x_7; size_t 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;
x_2 = lean_ctor_get(x_1, 0);
lean_inc(x_2);
x_3 = l___private_Lean_Elab_ParseImportsFast_0__Lean_toJsonPrintImportResult____x40_Lean_Elab_ParseImportsFast___hyg_1704____closed__1;
x_4 = l_Lean_Json_opt___at___private_Lean_Elab_ParseImportsFast_0__Lean_toJsonPrintImportResult____x40_Lean_Elab_ParseImportsFast___hyg_1704____spec__1(x_3, x_2);
x_5 = lean_ctor_get(x_1, 1);
lean_inc(x_5);
lean_dec(x_1);
x_6 = lean_array_get_size(x_5);
x_7 = lean_usize_of_nat(x_6);
lean_dec(x_6);
x_8 = 0;
x_9 = l_Array_mapMUnsafe_map___at___private_Lean_Data_Lsp_CodeActions_0__Lean_Lsp_toJsonResolveSupport____x40_Lean_Data_Lsp_CodeActions___hyg_1822____spec__1(x_7, x_8, x_5);
x_10 = lean_alloc_ctor(4, 1, 0);
lean_ctor_set(x_10, 0, x_9);
x_11 = l___private_Lean_Elab_ParseImportsFast_0__Lean_toJsonPrintImportResult____x40_Lean_Elab_ParseImportsFast___hyg_1704____closed__2;
x_12 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_12, 0, x_11);
lean_ctor_set(x_12, 1, x_10);
x_13 = lean_box(0);
x_14 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_14, 0, x_12);
lean_ctor_set(x_14, 1, x_13);
x_15 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_15, 0, x_14);
lean_ctor_set(x_15, 1, x_13);
x_16 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_16, 0, x_4);
lean_ctor_set(x_16, 1, x_15);
x_17 = l_List_join___rarg(x_16);
x_18 = l_Lean_Json_mkObj(x_17);
return x_18;
}
}
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_ParseImportsFast_0__Lean_toJsonPrintImportResult____x40_Lean_Elab_ParseImportsFast___hyg_1704____spec__2___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
size_t x_4; size_t x_5; lean_object* x_6;
x_4 = lean_unbox_usize(x_1);
lean_dec(x_1);
x_5 = lean_unbox_usize(x_2);
lean_dec(x_2);
x_6 = l_Array_mapMUnsafe_map___at___private_Lean_Elab_ParseImportsFast_0__Lean_toJsonPrintImportResult____x40_Lean_Elab_ParseImportsFast___hyg_1704____spec__2(x_4, x_5, x_3);
return x_6;
}
}
static lean_object* _init_l_Lean_instToJsonPrintImportResult___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l___private_Lean_Elab_ParseImportsFast_0__Lean_toJsonPrintImportResult____x40_Lean_Elab_ParseImportsFast___hyg_1704_), 1, 0);
return x_1;
}
}
static lean_object* _init_l_Lean_instToJsonPrintImportResult() {
_start:
{
lean_object* x_1;
x_1 = l_Lean_instToJsonPrintImportResult___closed__1;
return x_1;
}
}
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_ParseImportsFast_0__Lean_toJsonPrintImportsResult____x40_Lean_Elab_ParseImportsFast___hyg_1774____spec__1(size_t x_1, size_t x_2, lean_object* x_3) {
_start:
{
uint8_t x_4;
x_4 = lean_usize_dec_lt(x_2, x_1);
if (x_4 == 0)
{
return x_3;
}
else
{
lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; size_t x_9; size_t x_10; lean_object* x_11;
x_5 = lean_array_uget(x_3, x_2);
x_6 = lean_unsigned_to_nat(0u);
x_7 = lean_array_uset(x_3, x_2, x_6);
x_8 = l___private_Lean_Elab_ParseImportsFast_0__Lean_toJsonPrintImportResult____x40_Lean_Elab_ParseImportsFast___hyg_1704_(x_5);
x_9 = 1;
x_10 = lean_usize_add(x_2, x_9);
x_11 = lean_array_uset(x_7, x_2, x_8);
x_2 = x_10;
x_3 = x_11;
goto _start;
}
}
}
LEAN_EXPORT lean_object* l___private_Lean_Elab_ParseImportsFast_0__Lean_toJsonPrintImportsResult____x40_Lean_Elab_ParseImportsFast___hyg_1774_(lean_object* x_1) {
_start:
{
lean_object* x_2; size_t x_3; size_t 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; lean_object* x_13;
x_2 = lean_array_get_size(x_1);
x_3 = lean_usize_of_nat(x_2);
lean_dec(x_2);
x_4 = 0;
x_5 = l_Array_mapMUnsafe_map___at___private_Lean_Elab_ParseImportsFast_0__Lean_toJsonPrintImportsResult____x40_Lean_Elab_ParseImportsFast___hyg_1774____spec__1(x_3, x_4, x_1);
x_6 = lean_alloc_ctor(4, 1, 0);
lean_ctor_set(x_6, 0, x_5);
x_7 = l___private_Lean_Elab_ParseImportsFast_0__Lean_toJsonPrintImportResult____x40_Lean_Elab_ParseImportsFast___hyg_1704____closed__1;
x_8 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_8, 0, x_7);
lean_ctor_set(x_8, 1, x_6);
x_9 = lean_box(0);
x_10 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_10, 0, x_8);
lean_ctor_set(x_10, 1, x_9);
x_11 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_11, 0, x_10);
lean_ctor_set(x_11, 1, x_9);
x_12 = l_List_join___rarg(x_11);
x_13 = l_Lean_Json_mkObj(x_12);
return x_13;
}
}
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Elab_ParseImportsFast_0__Lean_toJsonPrintImportsResult____x40_Lean_Elab_ParseImportsFast___hyg_1774____spec__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
size_t x_4; size_t x_5; lean_object* x_6;
x_4 = lean_unbox_usize(x_1);
lean_dec(x_1);
x_5 = lean_unbox_usize(x_2);
lean_dec(x_2);
x_6 = l_Array_mapMUnsafe_map___at___private_Lean_Elab_ParseImportsFast_0__Lean_toJsonPrintImportsResult____x40_Lean_Elab_ParseImportsFast___hyg_1774____spec__1(x_4, x_5, x_3);
return x_6;
}
}
static lean_object* _init_l_Lean_instToJsonPrintImportsResult___closed__1() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l___private_Lean_Elab_ParseImportsFast_0__Lean_toJsonPrintImportsResult____x40_Lean_Elab_ParseImportsFast___hyg_1774_), 1, 0);
return x_1;
}
}
static lean_object* _init_l_Lean_instToJsonPrintImportsResult() {
_start:
{
lean_object* x_1;
x_1 = l_Lean_instToJsonPrintImportsResult___closed__1;
return x_1;
}
}
static lean_object* _init_l_Array_mapMUnsafe_map___at_Lean_printImportsJson___spec__1___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_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_printImportsJson___spec__1(size_t x_1, size_t x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
uint8_t x_5;
x_5 = lean_usize_dec_lt(x_2, x_1);
if (x_5 == 0)
{
lean_object* x_6;
x_6 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_6, 0, x_3);
lean_ctor_set(x_6, 1, x_4);
return x_6;
}
else
{
lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10;
x_7 = lean_array_uget(x_3, x_2);
x_8 = lean_unsigned_to_nat(0u);
x_9 = lean_array_uset(x_3, x_2, x_8);
x_10 = l_IO_FS_readFile(x_7, x_4);
if (lean_obj_tag(x_10) == 0)
{
lean_object* x_11; lean_object* x_12; lean_object* x_13;
x_11 = lean_ctor_get(x_10, 0);
lean_inc(x_11);
x_12 = lean_ctor_get(x_10, 1);
lean_inc(x_12);
lean_dec(x_10);
x_13 = l_Lean_parseImports_x27(x_11, x_7, x_12);
lean_dec(x_7);
if (lean_obj_tag(x_13) == 0)
{
lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; size_t x_19; size_t x_20; lean_object* x_21;
x_14 = lean_ctor_get(x_13, 0);
lean_inc(x_14);
x_15 = lean_ctor_get(x_13, 1);
lean_inc(x_15);
lean_dec(x_13);
x_16 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_16, 0, x_14);
x_17 = l_Lean_ParseImports_State_imports___default___closed__1;
x_18 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_18, 0, x_16);
lean_ctor_set(x_18, 1, x_17);
x_19 = 1;
x_20 = lean_usize_add(x_2, x_19);
x_21 = lean_array_uset(x_9, x_2, x_18);
x_2 = x_20;
x_3 = x_21;
x_4 = x_15;
goto _start;
}
else
{
lean_object* x_23; lean_object* x_24; lean_object* x_25; lean_object* x_26; lean_object* x_27; lean_object* x_28; lean_object* x_29; size_t x_30; size_t x_31; lean_object* x_32;
x_23 = lean_ctor_get(x_13, 0);
lean_inc(x_23);
x_24 = lean_ctor_get(x_13, 1);
lean_inc(x_24);
lean_dec(x_13);
x_25 = lean_box(0);
x_26 = lean_io_error_to_string(x_23);
x_27 = l_Array_mapMUnsafe_map___at_Lean_printImportsJson___spec__1___closed__1;
x_28 = lean_array_push(x_27, x_26);
x_29 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_29, 0, x_25);
lean_ctor_set(x_29, 1, x_28);
x_30 = 1;
x_31 = lean_usize_add(x_2, x_30);
x_32 = lean_array_uset(x_9, x_2, x_29);
x_2 = x_31;
x_3 = x_32;
x_4 = x_24;
goto _start;
}
}
else
{
lean_object* x_34; lean_object* x_35; lean_object* x_36; lean_object* x_37; lean_object* x_38; lean_object* x_39; lean_object* x_40; size_t x_41; size_t x_42; lean_object* x_43;
lean_dec(x_7);
x_34 = lean_ctor_get(x_10, 0);
lean_inc(x_34);
x_35 = lean_ctor_get(x_10, 1);
lean_inc(x_35);
lean_dec(x_10);
x_36 = lean_box(0);
x_37 = lean_io_error_to_string(x_34);
x_38 = l_Array_mapMUnsafe_map___at_Lean_printImportsJson___spec__1___closed__1;
x_39 = lean_array_push(x_38, x_37);
x_40 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_40, 0, x_36);
lean_ctor_set(x_40, 1, x_39);
x_41 = 1;
x_42 = lean_usize_add(x_2, x_41);
x_43 = lean_array_uset(x_9, x_2, x_40);
x_2 = x_42;
x_3 = x_43;
x_4 = x_35;
goto _start;
}
}
}
}
LEAN_EXPORT lean_object* lean_print_imports_json(lean_object* x_1, lean_object* x_2) {
_start:
{
lean_object* x_3; size_t x_4; size_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;
x_3 = lean_array_get_size(x_1);
x_4 = lean_usize_of_nat(x_3);
lean_dec(x_3);
x_5 = 0;
x_6 = l_Array_mapMUnsafe_map___at_Lean_printImportsJson___spec__1(x_4, x_5, x_1, x_2);
x_7 = lean_ctor_get(x_6, 0);
lean_inc(x_7);
x_8 = lean_ctor_get(x_6, 1);
lean_inc(x_8);
lean_dec(x_6);
x_9 = l___private_Lean_Elab_ParseImportsFast_0__Lean_toJsonPrintImportsResult____x40_Lean_Elab_ParseImportsFast___hyg_1774_(x_7);
x_10 = l_Lean_Json_compress(x_9);
x_11 = l_IO_println___at_Lean_instEval___spec__1(x_10, x_8);
return x_11;
}
}
LEAN_EXPORT lean_object* l_Array_mapMUnsafe_map___at_Lean_printImportsJson___spec__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
size_t x_5; size_t x_6; lean_object* x_7;
x_5 = lean_unbox_usize(x_1);
lean_dec(x_1);
x_6 = lean_unbox_usize(x_2);
lean_dec(x_2);
x_7 = l_Array_mapMUnsafe_map___at_Lean_printImportsJson___spec__1(x_5, x_6, x_3, x_4);
return x_7;
}
}
lean_object* initialize_Init(uint8_t builtin, lean_object*);
lean_object* initialize_Lean_Parser_Module(uint8_t builtin, lean_object*);
static bool _G_initialized = false;
@ -3729,6 +4246,10 @@ l_Lean_ParseImports_moduleIdent_parse___closed__3 = _init_l_Lean_ParseImports_mo
lean_mark_persistent(l_Lean_ParseImports_moduleIdent_parse___closed__3);
l_Lean_ParseImports_moduleIdent_parse___closed__4 = _init_l_Lean_ParseImports_moduleIdent_parse___closed__4();
lean_mark_persistent(l_Lean_ParseImports_moduleIdent_parse___closed__4);
l_Lean_ParseImports_keywordCore_go___at_Lean_ParseImports_preludeOpt___spec__1___closed__1 = _init_l_Lean_ParseImports_keywordCore_go___at_Lean_ParseImports_preludeOpt___spec__1___closed__1();
lean_mark_persistent(l_Lean_ParseImports_keywordCore_go___at_Lean_ParseImports_preludeOpt___spec__1___closed__1);
l_Lean_ParseImports_keywordCore_go___at_Lean_ParseImports_preludeOpt___spec__1___closed__2 = _init_l_Lean_ParseImports_keywordCore_go___at_Lean_ParseImports_preludeOpt___spec__1___closed__2();
lean_mark_persistent(l_Lean_ParseImports_keywordCore_go___at_Lean_ParseImports_preludeOpt___spec__1___closed__2);
l_Lean_ParseImports_keywordCore_go___at_Lean_ParseImports_main___spec__1___closed__1 = _init_l_Lean_ParseImports_keywordCore_go___at_Lean_ParseImports_main___spec__1___closed__1();
lean_mark_persistent(l_Lean_ParseImports_keywordCore_go___at_Lean_ParseImports_main___spec__1___closed__1);
l_Lean_ParseImports_keywordCore_go___at_Lean_ParseImports_main___spec__1___closed__2 = _init_l_Lean_ParseImports_keywordCore_go___at_Lean_ParseImports_main___spec__1___closed__2();
@ -3745,6 +4266,32 @@ l_Lean_parseImports_x27___closed__1 = _init_l_Lean_parseImports_x27___closed__1(
lean_mark_persistent(l_Lean_parseImports_x27___closed__1);
l_Lean_parseImports_x27___closed__2 = _init_l_Lean_parseImports_x27___closed__2();
lean_mark_persistent(l_Lean_parseImports_x27___closed__2);
l___private_Lean_Elab_ParseImportsFast_0__Lean_toJsonImport____x40_Lean_Elab_ParseImportsFast___hyg_1620____closed__1 = _init_l___private_Lean_Elab_ParseImportsFast_0__Lean_toJsonImport____x40_Lean_Elab_ParseImportsFast___hyg_1620____closed__1();
lean_mark_persistent(l___private_Lean_Elab_ParseImportsFast_0__Lean_toJsonImport____x40_Lean_Elab_ParseImportsFast___hyg_1620____closed__1);
l___private_Lean_Elab_ParseImportsFast_0__Lean_toJsonImport____x40_Lean_Elab_ParseImportsFast___hyg_1620____closed__2 = _init_l___private_Lean_Elab_ParseImportsFast_0__Lean_toJsonImport____x40_Lean_Elab_ParseImportsFast___hyg_1620____closed__2();
lean_mark_persistent(l___private_Lean_Elab_ParseImportsFast_0__Lean_toJsonImport____x40_Lean_Elab_ParseImportsFast___hyg_1620____closed__2);
l_Lean_instToJsonImport___closed__1 = _init_l_Lean_instToJsonImport___closed__1();
lean_mark_persistent(l_Lean_instToJsonImport___closed__1);
l_Lean_instToJsonImport = _init_l_Lean_instToJsonImport();
lean_mark_persistent(l_Lean_instToJsonImport);
l_Lean_PrintImportResult_imports_x3f___default = _init_l_Lean_PrintImportResult_imports_x3f___default();
lean_mark_persistent(l_Lean_PrintImportResult_imports_x3f___default);
l_Lean_PrintImportResult_errors___default = _init_l_Lean_PrintImportResult_errors___default();
lean_mark_persistent(l_Lean_PrintImportResult_errors___default);
l___private_Lean_Elab_ParseImportsFast_0__Lean_toJsonPrintImportResult____x40_Lean_Elab_ParseImportsFast___hyg_1704____closed__1 = _init_l___private_Lean_Elab_ParseImportsFast_0__Lean_toJsonPrintImportResult____x40_Lean_Elab_ParseImportsFast___hyg_1704____closed__1();
lean_mark_persistent(l___private_Lean_Elab_ParseImportsFast_0__Lean_toJsonPrintImportResult____x40_Lean_Elab_ParseImportsFast___hyg_1704____closed__1);
l___private_Lean_Elab_ParseImportsFast_0__Lean_toJsonPrintImportResult____x40_Lean_Elab_ParseImportsFast___hyg_1704____closed__2 = _init_l___private_Lean_Elab_ParseImportsFast_0__Lean_toJsonPrintImportResult____x40_Lean_Elab_ParseImportsFast___hyg_1704____closed__2();
lean_mark_persistent(l___private_Lean_Elab_ParseImportsFast_0__Lean_toJsonPrintImportResult____x40_Lean_Elab_ParseImportsFast___hyg_1704____closed__2);
l_Lean_instToJsonPrintImportResult___closed__1 = _init_l_Lean_instToJsonPrintImportResult___closed__1();
lean_mark_persistent(l_Lean_instToJsonPrintImportResult___closed__1);
l_Lean_instToJsonPrintImportResult = _init_l_Lean_instToJsonPrintImportResult();
lean_mark_persistent(l_Lean_instToJsonPrintImportResult);
l_Lean_instToJsonPrintImportsResult___closed__1 = _init_l_Lean_instToJsonPrintImportsResult___closed__1();
lean_mark_persistent(l_Lean_instToJsonPrintImportsResult___closed__1);
l_Lean_instToJsonPrintImportsResult = _init_l_Lean_instToJsonPrintImportsResult();
lean_mark_persistent(l_Lean_instToJsonPrintImportsResult);
l_Array_mapMUnsafe_map___at_Lean_printImportsJson___spec__1___closed__1 = _init_l_Array_mapMUnsafe_map___at_Lean_printImportsJson___spec__1___closed__1();
lean_mark_persistent(l_Array_mapMUnsafe_map___at_Lean_printImportsJson___spec__1___closed__1);
return lean_io_result_mk_ok(lean_box(0));
}
#ifdef __cplusplus

9
stage0/stdlib/Lean/Elab/Tactic/Simp.c generated
View file

@ -535,7 +535,7 @@ LEAN_EXPORT lean_object* l___regBuiltin_Lean_Elab_Tactic_evalSimpAll(lean_object
static lean_object* l___regBuiltin_Lean_Elab_Tactic_evalSimpAll_declRange___closed__6;
LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_elabSimpArgs___boxed__const__1;
LEAN_EXPORT lean_object* l_Lean_mkFreshId___at_Lean_Elab_Tactic_elabSimpArgs___spec__2___rarg(lean_object*, lean_object*);
lean_object* l_Lean_Meta_DiscrTree_empty(lean_object*);
lean_object* l_Lean_Meta_DiscrTree_empty(lean_object*, uint8_t);
LEAN_EXPORT lean_object* l___regBuiltin_Lean_Elab_Tactic_evalSimpAll_declRange(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Elab_Tactic_SimpKind_noConfusion___rarg___lambda__1___boxed(lean_object*);
lean_object* l_Lean_Meta_getSimpCongrTheorems___rarg(lean_object*, lean_object*);
@ -9835,9 +9835,10 @@ return x_113;
static lean_object* _init_l_Lean_Elab_Tactic_mkSimpContext___lambda__2___closed__1() {
_start:
{
lean_object* x_1;
x_1 = l_Lean_Meta_DiscrTree_empty(lean_box(0));
return x_1;
uint8_t x_1; lean_object* x_2;
x_1 = 1;
x_2 = l_Lean_Meta_DiscrTree_empty(lean_box(0), x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_Elab_Tactic_mkSimpContext___lambda__2___closed__2() {

26877
stage0/stdlib/Lean/Meta/DiscrTree.c generated
View file

File diff suppressed because it is too large Load diff

574
stage0/stdlib/Lean/Meta/DiscrTreeTypes.c generated
View file

File diff suppressed because it is too large Load diff

4121
stage0/stdlib/Lean/Meta/ExprDefEq.c generated
View file

File diff suppressed because it is too large Load diff

5062
stage0/stdlib/Lean/Meta/Instances.c generated
View file

File diff suppressed because it is too large Load diff

15
stage0/stdlib/Lean/Meta/Match/MatchEqs.c generated
View file

@ -384,7 +384,7 @@ size_t lean_usize_shift_left(size_t, size_t);
lean_object* lean_array_to_list(lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Meta_Match_MatchEqs_0__Lean_Meta_Match_mkSplitterProof_mkMap___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l___private_Lean_Meta_Match_MatchEqs_0__Lean_Meta_Match_mkSplitterProof_proveSubgoalLoop___closed__1;
lean_object* l_Lean_Meta_whnfCore_go___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_whnfCore_go___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_MVarId_refl(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Meta_Match_MatchEqs_0__Lean_Meta_Match_withSplitterAlts_go___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_panic___at___private_Lean_Meta_Match_MatchEqs_0__Lean_Meta_Match_mkSplitterProof_convertCastEqRec_go___spec__1___closed__1;
@ -11530,12 +11530,15 @@ return x_10;
static lean_object* _init_l_Lean_Meta_Match_proveCondEqThm_go___lambda__2___closed__1() {
_start:
{
uint8_t x_1; lean_object* x_2; lean_object* x_3;
uint8_t x_1; uint8_t x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
x_1 = 1;
x_2 = lean_box(x_1);
x_3 = lean_alloc_closure((void*)(l_Lean_Meta_whnfCore_go___boxed), 7, 1);
lean_closure_set(x_3, 0, x_2);
return x_3;
x_2 = 0;
x_3 = lean_box(x_1);
x_4 = lean_box(x_2);
x_5 = lean_alloc_closure((void*)(l_Lean_Meta_whnfCore_go___boxed), 8, 2);
lean_closure_set(x_5, 0, x_3);
lean_closure_set(x_5, 1, x_4);
return x_5;
}
}
static lean_object* _init_l_Lean_Meta_Match_proveCondEqThm_go___lambda__2___closed__2() {

1020
stage0/stdlib/Lean/Meta/SynthInstance.c generated
View file

File diff suppressed because it is too large Load diff

2015
stage0/stdlib/Lean/Meta/Tactic/Simp/Main.c generated
View file

File diff suppressed because it is too large Load diff

279
stage0/stdlib/Lean/Meta/Tactic/Simp/Rewrite.c generated
View file

@ -224,7 +224,7 @@ LEAN_EXPORT lean_object* l_Array_forInUnsafe_loop___at_Lean_Meta_Simp_rewrite_x3
static lean_object* l_Lean_Meta_Simp_rewriteUsingDecide_x3f___closed__2;
LEAN_EXPORT lean_object* l_Lean_Meta_Simp_rewritePre___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
LEAN_EXPORT lean_object* l___private_Lean_Meta_Tactic_Simp_Rewrite_0__Lean_Meta_Simp_tryTheoremCore_go___lambda__4(lean_object*, lean_object*, 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_DiscrTree_getMatchWithExtra___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_DiscrTree_getMatchWithExtra___rarg(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_List_redLength___rarg(lean_object*);
LEAN_EXPORT lean_object* l_Lean_Meta_Simp_rewritePost(lean_object*, lean_object*, uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Meta_Simp_synthesizeArgs_synthesizeInstance___closed__10;
@ -10154,181 +10154,182 @@ return x_2;
LEAN_EXPORT lean_object* l_Lean_Meta_Simp_rewrite_x3f(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, uint8_t 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) {
_start:
{
lean_object* x_14;
uint8_t x_14; lean_object* x_15;
x_14 = 1;
lean_inc(x_12);
lean_inc(x_11);
lean_inc(x_10);
lean_inc(x_9);
lean_inc(x_1);
x_14 = l_Lean_Meta_DiscrTree_getMatchWithExtra___rarg(x_2, x_1, x_9, x_10, x_11, x_12, x_13);
if (lean_obj_tag(x_14) == 0)
x_15 = l_Lean_Meta_DiscrTree_getMatchWithExtra___rarg(x_14, x_2, x_1, x_9, x_10, x_11, x_12, x_13);
if (lean_obj_tag(x_15) == 0)
{
lean_object* x_15; lean_object* x_16; uint8_t x_17;
x_15 = lean_ctor_get(x_14, 0);
lean_inc(x_15);
x_16 = lean_ctor_get(x_14, 1);
lean_object* x_16; lean_object* x_17; uint8_t x_18;
x_16 = lean_ctor_get(x_15, 0);
lean_inc(x_16);
lean_dec(x_14);
x_17 = l_Array_isEmpty___rarg(x_15);
if (x_17 == 0)
x_17 = lean_ctor_get(x_15, 1);
lean_inc(x_17);
lean_dec(x_15);
x_18 = l_Array_isEmpty___rarg(x_16);
if (x_18 == 0)
{
lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; size_t x_23; size_t x_24; lean_object* x_25; lean_object* x_26;
x_18 = lean_array_get_size(x_15);
x_19 = lean_unsigned_to_nat(0u);
x_20 = l_Array_insertionSort_traverse___at_Lean_Meta_Simp_rewrite_x3f___spec__1(x_15, x_19, x_18);
x_21 = lean_box(0);
x_22 = lean_array_get_size(x_20);
x_23 = lean_usize_of_nat(x_22);
lean_dec(x_22);
x_24 = 0;
x_25 = l_Lean_Meta_Simp_rewrite_x3f___closed__1;
x_26 = l_Array_forInUnsafe_loop___at_Lean_Meta_Simp_rewrite_x3f___spec__3(x_1, x_3, x_4, x_6, x_25, x_20, x_23, x_24, x_25, x_7, x_8, x_9, x_10, x_11, x_12, x_16);
lean_dec(x_20);
if (lean_obj_tag(x_26) == 0)
lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; lean_object* x_23; size_t x_24; size_t x_25; lean_object* x_26; lean_object* x_27;
x_19 = lean_array_get_size(x_16);
x_20 = lean_unsigned_to_nat(0u);
x_21 = l_Array_insertionSort_traverse___at_Lean_Meta_Simp_rewrite_x3f___spec__1(x_16, x_20, x_19);
x_22 = lean_box(0);
x_23 = lean_array_get_size(x_21);
x_24 = lean_usize_of_nat(x_23);
lean_dec(x_23);
x_25 = 0;
x_26 = l_Lean_Meta_Simp_rewrite_x3f___closed__1;
x_27 = l_Array_forInUnsafe_loop___at_Lean_Meta_Simp_rewrite_x3f___spec__3(x_1, x_3, x_4, x_6, x_26, x_21, x_24, x_25, x_26, x_7, x_8, x_9, x_10, x_11, x_12, x_17);
lean_dec(x_21);
if (lean_obj_tag(x_27) == 0)
{
lean_object* x_27; lean_object* x_28;
x_27 = lean_ctor_get(x_26, 0);
lean_inc(x_27);
lean_object* x_28; lean_object* x_29;
x_28 = lean_ctor_get(x_27, 0);
lean_inc(x_28);
x_29 = lean_ctor_get(x_28, 0);
lean_inc(x_29);
lean_dec(x_28);
if (lean_obj_tag(x_29) == 0)
{
uint8_t x_30;
x_30 = !lean_is_exclusive(x_27);
if (x_30 == 0)
{
lean_object* x_31;
x_31 = lean_ctor_get(x_27, 0);
lean_dec(x_31);
lean_ctor_set(x_27, 0, x_22);
return x_27;
}
else
{
lean_object* x_32; lean_object* x_33;
x_32 = lean_ctor_get(x_27, 1);
lean_inc(x_32);
lean_dec(x_27);
if (lean_obj_tag(x_28) == 0)
{
uint8_t x_29;
x_29 = !lean_is_exclusive(x_26);
if (x_29 == 0)
{
lean_object* x_30;
x_30 = lean_ctor_get(x_26, 0);
lean_dec(x_30);
lean_ctor_set(x_26, 0, x_21);
return x_26;
}
else
{
lean_object* x_31; lean_object* x_32;
x_31 = lean_ctor_get(x_26, 1);
lean_inc(x_31);
lean_dec(x_26);
x_32 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_32, 0, x_21);
lean_ctor_set(x_32, 1, x_31);
return x_32;
x_33 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_33, 0, x_22);
lean_ctor_set(x_33, 1, x_32);
return x_33;
}
}
else
{
uint8_t x_33;
x_33 = !lean_is_exclusive(x_26);
if (x_33 == 0)
uint8_t x_34;
x_34 = !lean_is_exclusive(x_27);
if (x_34 == 0)
{
lean_object* x_34; lean_object* x_35;
x_34 = lean_ctor_get(x_26, 0);
lean_dec(x_34);
x_35 = lean_ctor_get(x_28, 0);
lean_inc(x_35);
lean_dec(x_28);
lean_ctor_set(x_26, 0, x_35);
return x_26;
}
else
{
lean_object* x_36; lean_object* x_37; lean_object* x_38;
x_36 = lean_ctor_get(x_26, 1);
lean_object* x_35; lean_object* x_36;
x_35 = lean_ctor_get(x_27, 0);
lean_dec(x_35);
x_36 = lean_ctor_get(x_29, 0);
lean_inc(x_36);
lean_dec(x_26);
x_37 = lean_ctor_get(x_28, 0);
lean_dec(x_29);
lean_ctor_set(x_27, 0, x_36);
return x_27;
}
else
{
lean_object* x_37; lean_object* x_38; lean_object* x_39;
x_37 = lean_ctor_get(x_27, 1);
lean_inc(x_37);
lean_dec(x_28);
x_38 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_38, 0, x_37);
lean_ctor_set(x_38, 1, x_36);
return x_38;
lean_dec(x_27);
x_38 = lean_ctor_get(x_29, 0);
lean_inc(x_38);
lean_dec(x_29);
x_39 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_39, 0, x_38);
lean_ctor_set(x_39, 1, x_37);
return x_39;
}
}
}
else
{
uint8_t x_39;
x_39 = !lean_is_exclusive(x_26);
if (x_39 == 0)
uint8_t x_40;
x_40 = !lean_is_exclusive(x_27);
if (x_40 == 0)
{
return x_26;
return x_27;
}
else
{
lean_object* x_40; lean_object* x_41; lean_object* x_42;
x_40 = lean_ctor_get(x_26, 0);
x_41 = lean_ctor_get(x_26, 1);
lean_object* x_41; lean_object* x_42; lean_object* x_43;
x_41 = lean_ctor_get(x_27, 0);
x_42 = lean_ctor_get(x_27, 1);
lean_inc(x_42);
lean_inc(x_41);
lean_inc(x_40);
lean_dec(x_26);
x_42 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_42, 0, x_40);
lean_ctor_set(x_42, 1, x_41);
return x_42;
lean_dec(x_27);
x_43 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_43, 0, x_41);
lean_ctor_set(x_43, 1, x_42);
return x_43;
}
}
}
else
{
lean_object* x_43; lean_object* x_44; lean_object* x_45; lean_object* x_46; lean_object* x_47; uint8_t x_48;
lean_dec(x_15);
lean_object* x_44; lean_object* x_45; lean_object* x_46; lean_object* x_47; lean_object* x_48; uint8_t x_49;
lean_dec(x_16);
lean_dec(x_4);
lean_dec(x_3);
x_43 = l_Array_forInUnsafe_loop___at_Lean_Meta_Simp_rewrite_x3f___spec__3___closed__2;
x_44 = l_Lean_isTracingEnabledFor___at_Lean_Meta_Simp_synthesizeArgs_synthesizeInstance___spec__1(x_43, x_7, x_8, x_9, x_10, x_11, x_12, x_16);
x_45 = lean_ctor_get(x_44, 0);
lean_inc(x_45);
x_46 = lean_ctor_get(x_44, 1);
x_44 = l_Array_forInUnsafe_loop___at_Lean_Meta_Simp_rewrite_x3f___spec__3___closed__2;
x_45 = l_Lean_isTracingEnabledFor___at_Lean_Meta_Simp_synthesizeArgs_synthesizeInstance___spec__1(x_44, x_7, x_8, x_9, x_10, x_11, x_12, x_17);
x_46 = lean_ctor_get(x_45, 0);
lean_inc(x_46);
lean_dec(x_44);
x_47 = l___private_Lean_Meta_Tactic_Simp_Rewrite_0__Lean_Meta_Simp_tryTheoremCore_go___lambda__4___closed__1;
x_48 = lean_unbox(x_45);
x_47 = lean_ctor_get(x_45, 1);
lean_inc(x_47);
lean_dec(x_45);
if (x_48 == 0)
x_48 = l___private_Lean_Meta_Tactic_Simp_Rewrite_0__Lean_Meta_Simp_tryTheoremCore_go___lambda__4___closed__1;
x_49 = lean_unbox(x_46);
lean_dec(x_46);
if (x_49 == 0)
{
lean_object* x_49; lean_object* x_50;
lean_object* x_50; lean_object* x_51;
lean_dec(x_1);
x_49 = lean_box(0);
x_50 = lean_apply_8(x_47, x_49, x_7, x_8, x_9, x_10, x_11, x_12, x_46);
return x_50;
x_50 = lean_box(0);
x_51 = lean_apply_8(x_48, x_50, x_7, x_8, x_9, x_10, x_11, x_12, x_47);
return x_51;
}
else
{
lean_object* x_51; lean_object* x_52; lean_object* x_53; lean_object* x_54; lean_object* x_55; lean_object* x_56; lean_object* x_57; lean_object* x_58; lean_object* x_59; lean_object* x_60; lean_object* x_61; lean_object* x_62; lean_object* x_63;
x_51 = l_Lean_stringToMessageData(x_5);
x_52 = l_Lean_Meta_Simp_rewrite_x3f___closed__3;
x_53 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_53, 0, x_52);
lean_ctor_set(x_53, 1, x_51);
x_54 = l_Lean_Meta_Simp_rewrite_x3f___closed__5;
x_55 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_55, 0, x_53);
lean_ctor_set(x_55, 1, x_54);
x_56 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_56, 0, x_1);
x_57 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_57, 0, x_55);
lean_ctor_set(x_57, 1, x_56);
x_58 = l_Lean_Meta_Simp_synthesizeArgs_synthesizeInstance___closed__8;
x_59 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_59, 0, x_57);
lean_ctor_set(x_59, 1, x_58);
x_60 = l_Lean_addTrace___at_Lean_Meta_Simp_synthesizeArgs_synthesizeInstance___spec__6(x_43, x_59, x_7, x_8, x_9, x_10, x_11, x_12, x_46);
x_61 = lean_ctor_get(x_60, 0);
lean_inc(x_61);
x_62 = lean_ctor_get(x_60, 1);
lean_object* x_52; lean_object* x_53; lean_object* x_54; lean_object* x_55; lean_object* x_56; lean_object* x_57; lean_object* x_58; lean_object* x_59; lean_object* x_60; lean_object* x_61; lean_object* x_62; lean_object* x_63; lean_object* x_64;
x_52 = l_Lean_stringToMessageData(x_5);
x_53 = l_Lean_Meta_Simp_rewrite_x3f___closed__3;
x_54 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_54, 0, x_53);
lean_ctor_set(x_54, 1, x_52);
x_55 = l_Lean_Meta_Simp_rewrite_x3f___closed__5;
x_56 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_56, 0, x_54);
lean_ctor_set(x_56, 1, x_55);
x_57 = lean_alloc_ctor(2, 1, 0);
lean_ctor_set(x_57, 0, x_1);
x_58 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_58, 0, x_56);
lean_ctor_set(x_58, 1, x_57);
x_59 = l_Lean_Meta_Simp_synthesizeArgs_synthesizeInstance___closed__8;
x_60 = lean_alloc_ctor(10, 2, 0);
lean_ctor_set(x_60, 0, x_58);
lean_ctor_set(x_60, 1, x_59);
x_61 = l_Lean_addTrace___at_Lean_Meta_Simp_synthesizeArgs_synthesizeInstance___spec__6(x_44, x_60, x_7, x_8, x_9, x_10, x_11, x_12, x_47);
x_62 = lean_ctor_get(x_61, 0);
lean_inc(x_62);
lean_dec(x_60);
x_63 = lean_apply_8(x_47, x_61, x_7, x_8, x_9, x_10, x_11, x_12, x_62);
return x_63;
x_63 = lean_ctor_get(x_61, 1);
lean_inc(x_63);
lean_dec(x_61);
x_64 = lean_apply_8(x_48, x_62, x_7, x_8, x_9, x_10, x_11, x_12, x_63);
return x_64;
}
}
}
else
{
uint8_t x_64;
uint8_t x_65;
lean_dec(x_12);
lean_dec(x_11);
lean_dec(x_10);
@ -10338,23 +10339,23 @@ lean_dec(x_7);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_1);
x_64 = !lean_is_exclusive(x_14);
if (x_64 == 0)
x_65 = !lean_is_exclusive(x_15);
if (x_65 == 0)
{
return x_14;
return x_15;
}
else
{
lean_object* x_65; lean_object* x_66; lean_object* x_67;
x_65 = lean_ctor_get(x_14, 0);
x_66 = lean_ctor_get(x_14, 1);
lean_object* x_66; lean_object* x_67; lean_object* x_68;
x_66 = lean_ctor_get(x_15, 0);
x_67 = lean_ctor_get(x_15, 1);
lean_inc(x_67);
lean_inc(x_66);
lean_inc(x_65);
lean_dec(x_14);
x_67 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_67, 0, x_65);
lean_ctor_set(x_67, 1, x_66);
return x_67;
lean_dec(x_15);
x_68 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_68, 0, x_66);
lean_ctor_set(x_68, 1, x_67);
return x_68;
}
}
}

4879
stage0/stdlib/Lean/Meta/Tactic/Simp/SimpTheorems.c generated
View file

File diff suppressed because it is too large Load diff

9
stage0/stdlib/Lean/Meta/Tactic/SplitIf.c generated
View file

@ -199,7 +199,7 @@ lean_object* l_Lean_isTracingEnabledFor___at_Lean_Meta_Simp_synthesizeArgs_synth
static lean_object* l_Lean_Meta_SplitIf_discharge_x3f___lambda__2___closed__1;
static lean_object* l_Lean_Meta_SplitIf_initFn____x40_Lean_Meta_Tactic_SplitIf___hyg_5____lambda__1___closed__1;
lean_object* l_Lean_mkApp3(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Meta_DiscrTree_empty(lean_object*);
lean_object* l_Lean_Meta_DiscrTree_empty(lean_object*, uint8_t);
static lean_object* l_Lean_Meta_initFn____x40_Lean_Meta_Tactic_SplitIf___hyg_1870____closed__12;
extern lean_object* l_Lean_PersistentHashMap_empty___at_Lean_Meta_Instances_instanceNames___default___spec__1;
lean_object* l_Lean_Meta_getSimpCongrTheorems___rarg(lean_object*, lean_object*);
@ -509,9 +509,10 @@ return x_59;
static lean_object* _init_l_Lean_Meta_SplitIf_initFn____x40_Lean_Meta_Tactic_SplitIf___hyg_5____closed__1() {
_start:
{
lean_object* x_1;
x_1 = l_Lean_Meta_DiscrTree_empty(lean_box(0));
return x_1;
uint8_t x_1; lean_object* x_2;
x_1 = 1;
x_2 = l_Lean_Meta_DiscrTree_empty(lean_box(0), x_1);
return x_2;
}
}
static lean_object* _init_l_Lean_Meta_SplitIf_initFn____x40_Lean_Meta_Tactic_SplitIf___hyg_5____closed__2() {

5533
stage0/stdlib/Lean/Meta/UnificationHint.c generated
View file

File diff suppressed because it is too large Load diff

7210
stage0/stdlib/Lean/Meta/WHNF.c generated
View file

File diff suppressed because it is too large Load diff

86
stage0/stdlib/Lean/Parser/Syntax.c generated
View file

@ -190,6 +190,7 @@ static lean_object* l_Lean_Parser_Command_syntaxAbbrev___closed__4;
static lean_object* l___regBuiltin_Lean_Parser_Syntax_sepBy_declRange___closed__1;
LEAN_EXPORT lean_object* l_Lean_Parser_Command_elab__rules_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Parser_Syntax_sepBy___closed__18;
LEAN_EXPORT lean_object* l___regBuiltin_Lean_Parser_Command_macro__rules_formatter(lean_object*);
static lean_object* l_Lean_Parser_Command_mixfix_formatter___closed__3;
static lean_object* l_Lean_Parser_Command_catBehavior_formatter___closed__3;
static lean_object* l___regBuiltin_Lean_Parser_Command_elab_declRange___closed__4;
@ -1163,6 +1164,7 @@ static lean_object* l_Lean_Parser_Command_postfix_formatter___closed__1;
static lean_object* l_Lean_Parser_Syntax_binary___closed__2;
LEAN_EXPORT lean_object* l___regBuiltin_Lean_Parser_Command_syntaxAbbrev(lean_object*);
static lean_object* l_Lean_Parser_Syntax_paren___closed__10;
LEAN_EXPORT lean_object* l___regBuiltin_Lean_Parser_Command_macro__rules_parenthesizer(lean_object*);
static lean_object* l___regBuiltin_Lean_Parser_Command_infixr_parenthesizer___closed__1;
LEAN_EXPORT lean_object* l___regBuiltin_Lean_Parser_Syntax_cat_parenthesizer(lean_object*);
static lean_object* l_Lean_Parser_Syntax_cat_parenthesizer___closed__5;
@ -1231,6 +1233,7 @@ static lean_object* l_Lean_Parser_Command_postfix_parenthesizer___closed__2;
static lean_object* l_Lean_Parser_Command_elab___closed__9;
LEAN_EXPORT lean_object* l___regBuiltin_Lean_Parser_Command_prefix_parenthesizer(lean_object*);
static lean_object* l_Lean_Parser_Command_catBehaviorSymbol___closed__3;
static lean_object* l___regBuiltin_Lean_Parser_Command_macro__rules_formatter___closed__2;
static lean_object* l_Lean_Parser_Command_macroArg___closed__12;
static lean_object* l___regBuiltin_Lean_Parser_Syntax_sepBy1_parenthesizer___closed__1;
static lean_object* l___regBuiltin_Lean_Parser_Command_notation_declRange___closed__3;
@ -1293,6 +1296,7 @@ static lean_object* l_Lean_Parser_Syntax_atom_parenthesizer___closed__1;
static lean_object* l_Lean_Parser_Command_notation_parenthesizer___closed__2;
static lean_object* l_Lean_Parser_Command_postfix_formatter___closed__2;
static lean_object* l_Lean_Parser_Command_elab___closed__4;
static lean_object* l___regBuiltin_Lean_Parser_Command_macro__rules_formatter___closed__1;
static lean_object* l___regBuiltin_Lean_Parser_Syntax_nonReserved_declRange___closed__2;
static lean_object* l_Lean_Parser_Command_postfix___closed__7;
LEAN_EXPORT lean_object* l_Lean_Parser_Command_postfix_formatter(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -1309,6 +1313,7 @@ static lean_object* l_Lean_Parser_Command_elab_formatter___closed__12;
static lean_object* l_Lean_Parser_Command_mixfix___closed__18;
lean_object* l_Lean_Parser_orelse(lean_object*, lean_object*);
static lean_object* l_Lean_Parser_Command_macroArg_parenthesizer___closed__1;
static lean_object* l___regBuiltin_Lean_Parser_Command_macro__rules_parenthesizer___closed__2;
static lean_object* l_Lean_Parser_Command_optKind___closed__5;
static lean_object* l_Lean_Parser_Command_macroArg___closed__9;
static lean_object* l_Lean_Parser_Command_macro__rules___closed__2;
@ -1333,6 +1338,7 @@ static lean_object* l_Lean_Parser_Command_prefix___closed__7;
static lean_object* l_Lean_Parser_Command_optKind___closed__3;
static lean_object* l_Lean_Parser_Command_infixr___closed__4;
static lean_object* l_Lean_Parser_Syntax_binary___closed__9;
static lean_object* l___regBuiltin_Lean_Parser_Command_macro__rules_parenthesizer___closed__1;
LEAN_EXPORT lean_object* l_Lean_Parser_Command_infix_parenthesizer(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
static lean_object* l_Lean_Parser_Command_catBehaviorSymbol_formatter___closed__1;
LEAN_EXPORT lean_object* l___regBuiltin_Lean_Parser_Command_namedName_formatter(lean_object*);
@ -10970,6 +10976,39 @@ x_8 = l_Lean_PrettyPrinter_Formatter_orelse_formatter(x_6, x_7, x_1, x_2, x_3, x
return x_8;
}
}
static lean_object* _init_l___regBuiltin_Lean_Parser_Command_macro__rules_formatter___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Parser_initFn____x40_Lean_Parser_Syntax___hyg_5____closed__3;
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Syntax___hyg_5____closed__4;
x_3 = l_Lean_Parser_Command_namedName___closed__1;
x_4 = l_Lean_Parser_Command_macro__rules___closed__1;
x_5 = l___regBuiltin_Lean_Parser_Syntax_paren_formatter___closed__1;
x_6 = l_Lean_Name_mkStr5(x_1, x_2, x_3, x_4, x_5);
return x_6;
}
}
static lean_object* _init_l___regBuiltin_Lean_Parser_Command_macro__rules_formatter___closed__2() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Lean_Parser_Command_macro__rules_formatter), 5, 0);
return x_1;
}
}
LEAN_EXPORT lean_object* l___regBuiltin_Lean_Parser_Command_macro__rules_formatter(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 = l___regBuiltin_Lean_Parser_Syntax_paren_formatter___closed__3;
x_3 = l_Lean_Parser_Command_macro__rules___closed__2;
x_4 = l___regBuiltin_Lean_Parser_Command_macro__rules_formatter___closed__1;
x_5 = l___regBuiltin_Lean_Parser_Command_macro__rules_formatter___closed__2;
x_6 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_5, x_1);
return x_6;
}
}
static lean_object* _init_l_Lean_Parser_Command_optKind_parenthesizer___closed__1() {
_start:
{
@ -11168,6 +11207,39 @@ x_8 = l_Lean_PrettyPrinter_Parenthesizer_withAntiquot_parenthesizer(x_6, x_7, x_
return x_8;
}
}
static lean_object* _init_l___regBuiltin_Lean_Parser_Command_macro__rules_parenthesizer___closed__1() {
_start:
{
lean_object* x_1; lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5; lean_object* x_6;
x_1 = l_Lean_Parser_initFn____x40_Lean_Parser_Syntax___hyg_5____closed__3;
x_2 = l_Lean_Parser_initFn____x40_Lean_Parser_Syntax___hyg_5____closed__4;
x_3 = l_Lean_Parser_Command_namedName___closed__1;
x_4 = l_Lean_Parser_Command_macro__rules___closed__1;
x_5 = l___regBuiltin_Lean_Parser_Syntax_paren_parenthesizer___closed__1;
x_6 = l_Lean_Name_mkStr5(x_1, x_2, x_3, x_4, x_5);
return x_6;
}
}
static lean_object* _init_l___regBuiltin_Lean_Parser_Command_macro__rules_parenthesizer___closed__2() {
_start:
{
lean_object* x_1;
x_1 = lean_alloc_closure((void*)(l_Lean_Parser_Command_macro__rules_parenthesizer), 5, 0);
return x_1;
}
}
LEAN_EXPORT lean_object* l___regBuiltin_Lean_Parser_Command_macro__rules_parenthesizer(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 = l___regBuiltin_Lean_Parser_Syntax_paren_parenthesizer___closed__3;
x_3 = l_Lean_Parser_Command_macro__rules___closed__2;
x_4 = l___regBuiltin_Lean_Parser_Command_macro__rules_parenthesizer___closed__1;
x_5 = l___regBuiltin_Lean_Parser_Command_macro__rules_parenthesizer___closed__2;
x_6 = l_Lean_KeyedDeclsAttribute_addBuiltin___rarg(x_2, x_3, x_4, x_5, x_1);
return x_6;
}
}
static lean_object* _init_l_Lean_Parser_Command_syntax___closed__1() {
_start:
{
@ -18880,6 +18952,13 @@ l_Lean_Parser_Command_macro__rules_formatter___closed__9 = _init_l_Lean_Parser_C
lean_mark_persistent(l_Lean_Parser_Command_macro__rules_formatter___closed__9);
l_Lean_Parser_Command_macro__rules_formatter___closed__10 = _init_l_Lean_Parser_Command_macro__rules_formatter___closed__10();
lean_mark_persistent(l_Lean_Parser_Command_macro__rules_formatter___closed__10);
l___regBuiltin_Lean_Parser_Command_macro__rules_formatter___closed__1 = _init_l___regBuiltin_Lean_Parser_Command_macro__rules_formatter___closed__1();
lean_mark_persistent(l___regBuiltin_Lean_Parser_Command_macro__rules_formatter___closed__1);
l___regBuiltin_Lean_Parser_Command_macro__rules_formatter___closed__2 = _init_l___regBuiltin_Lean_Parser_Command_macro__rules_formatter___closed__2();
lean_mark_persistent(l___regBuiltin_Lean_Parser_Command_macro__rules_formatter___closed__2);
res = l___regBuiltin_Lean_Parser_Command_macro__rules_formatter(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l_Lean_Parser_Command_optKind_parenthesizer___closed__1 = _init_l_Lean_Parser_Command_optKind_parenthesizer___closed__1();
lean_mark_persistent(l_Lean_Parser_Command_optKind_parenthesizer___closed__1);
l_Lean_Parser_Command_optKind_parenthesizer___closed__2 = _init_l_Lean_Parser_Command_optKind_parenthesizer___closed__2();
@ -18910,6 +18989,13 @@ l_Lean_Parser_Command_macro__rules_parenthesizer___closed__9 = _init_l_Lean_Pars
lean_mark_persistent(l_Lean_Parser_Command_macro__rules_parenthesizer___closed__9);
l_Lean_Parser_Command_macro__rules_parenthesizer___closed__10 = _init_l_Lean_Parser_Command_macro__rules_parenthesizer___closed__10();
lean_mark_persistent(l_Lean_Parser_Command_macro__rules_parenthesizer___closed__10);
l___regBuiltin_Lean_Parser_Command_macro__rules_parenthesizer___closed__1 = _init_l___regBuiltin_Lean_Parser_Command_macro__rules_parenthesizer___closed__1();
lean_mark_persistent(l___regBuiltin_Lean_Parser_Command_macro__rules_parenthesizer___closed__1);
l___regBuiltin_Lean_Parser_Command_macro__rules_parenthesizer___closed__2 = _init_l___regBuiltin_Lean_Parser_Command_macro__rules_parenthesizer___closed__2();
lean_mark_persistent(l___regBuiltin_Lean_Parser_Command_macro__rules_parenthesizer___closed__2);
res = l___regBuiltin_Lean_Parser_Command_macro__rules_parenthesizer(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l_Lean_Parser_Command_syntax___closed__1 = _init_l_Lean_Parser_Command_syntax___closed__1();
lean_mark_persistent(l_Lean_Parser_Command_syntax___closed__1);
l_Lean_Parser_Command_syntax___closed__2 = _init_l_Lean_Parser_Command_syntax___closed__2();

684
stage0/stdlib/Lean/Parser/Term.c generated
View file

File diff suppressed because it is too large Load diff

7510
stage0/stdlib/Lean/ParserCompiler.c generated
View file

File diff suppressed because it is too large Load diff