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 2021-04-04 11:39:31 -07:00
parent 5ab3ed5314
commit dbbb7bf9f6
17 changed files with 6313 additions and 335 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

1
stage0/src/Init/Data.lean generated
View file

@ -17,6 +17,7 @@ import Init.Data.Fin
import Init.Data.UInt
import Init.Data.Float
import Init.Data.Option
import Init.Data.Ord
import Init.Data.Random
import Init.Data.ToString
import Init.Data.Range

39
stage0/src/Init/Data/Ord.lean generated Normal file
View file

@ -0,0 +1,39 @@
/-
Copyright (c) 2021 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Dany Fabian
-/
prelude
import Init.Data.Int
import Init.Data.String
inductive Ordering where
| lt | eq | gt
deriving Inhabited
class Ord (α : Type u) where
compare : α → α → Ordering
export Ord (compare)
def compareOfLessAndEq {α} (x y : α) [HasLess α] [Decidable (x < y)] [DecidableEq α] : Ordering :=
if x < y then Ordering.lt
else if x = y then Ordering.eq
else Ordering.gt
instance : Ord Nat where
compare x y := compareOfLessAndEq x y
instance : Ord Int where
compare x y := compareOfLessAndEq x y
instance : Ord Bool where
compare
| false, true => Ordering.lt
| true, false => Ordering.gt
| _, _ => Ordering.eq
instance : Ord String where
compare x y := compareOfLessAndEq x y

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

@ -690,8 +690,8 @@ private def elabAppLValsAux (namedArgs : Array NamedArg) (args : Array Arg) (exp
let rec loop : Expr → List LVal → TermElabM Expr
| f, [] => elabAppArgs f namedArgs args expectedType? explicit ellipsis
| f, lval::lvals => do
if let LVal.fieldName (ref := fieldStx) (stx := stx) .. := lval then
addDotCompletionInfo stx f expectedType? fieldStx
if let LVal.fieldName (ref := fieldStx) (targetStx := targetStx) .. := lval then
addDotCompletionInfo targetStx f expectedType? fieldStx
let (f, lvalRes) ← resolveLVal f lval
match lvalRes with
| LValResolution.projIdx structName idx =>
@ -805,7 +805,7 @@ private partial def elabAppFn (f : Syntax) (lvals : List LVal) (namedArgs : Arra
let elabFieldName (e field : Syntax) := do
let newLVals := field.getId.eraseMacroScopes.components.map fun n =>
-- We use `none` here since `field` can't be part of a composite name
LVal.fieldName field (toString n) none f
LVal.fieldName field (toString n) none e
elabAppFn e (newLVals ++ lvals) namedArgs args expectedType? explicit ellipsis overloaded acc
let elabFieldIdx (e idxStx : Syntax) := do
let idx := idxStx.isFieldIdx?.get!

1
stage0/src/Lean/Elab/Deriving.lean generated
View file

@ -12,3 +12,4 @@ import Lean.Elab.Deriving.Repr
import Lean.Elab.Deriving.FromToJson
import Lean.Elab.Deriving.SizeOf
import Lean.Elab.Deriving.Hashable
import Lean.Elab.Deriving.Ord

107
stage0/src/Lean/Elab/Deriving/Ord.lean generated Normal file
View file

@ -0,0 +1,107 @@
/-
Copyright (c) 2021 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Dany Fabian
-/
import Lean.Meta.Transform
import Lean.Elab.Deriving.Basic
import Lean.Elab.Deriving.Util
namespace Lean.Elab.Deriving.Ord
open Lean.Parser.Term
open Meta
def mkOrdHeader (ctx : Context) (indVal : InductiveVal) : TermElabM Header := do
mkHeader ctx `Ord 2 indVal
def mkMatch (ctx : Context) (header : Header) (indVal : InductiveVal) (auxFunName : Name) : TermElabM Syntax := do
let discrs ← mkDiscrs header indVal
let alts ← mkAlts
`(match $[$discrs],* with $alts:matchAlt*)
where
mkAlts : TermElabM (Array Syntax) := do
let mut alts := #[]
for ctorName in indVal.ctors do
let ctorInfo ← getConstInfoCtor ctorName
let alt ← forallTelescopeReducing ctorInfo.type fun xs type => do
let type ← Core.betaReduce type -- we 'beta-reduce' to eliminate "artificial" dependencies
let mut indPatterns := #[]
-- add `_` pattern for indices
for i in [:indVal.numIndices] do
indPatterns := indPatterns.push (← `(_))
let mut ctorArgs1 := #[]
let mut ctorArgs2 := #[]
let mut rhs ← `(Ordering.eq)
-- add `_` for inductive parameters, they are inaccessible
for i in [:indVal.numParams] do
ctorArgs1 := ctorArgs1.push (← `(_))
ctorArgs2 := ctorArgs2.push (← `(_))
for i in [:ctorInfo.numFields] do
let x := xs[indVal.numParams + i]
if type.containsFVar x.fvarId! || (←isProp (←inferType x)) then
-- If resulting type depends on this field or is a proof, we don't need to compare
ctorArgs1 := ctorArgs1.push (← `(_))
ctorArgs2 := ctorArgs2.push (← `(_))
else
let a := mkIdent (← mkFreshUserName `a)
let b := mkIdent (← mkFreshUserName `b)
ctorArgs1 := ctorArgs1.push a
ctorArgs2 := ctorArgs2.push b
rhs ← `(match compare $a:ident $b:ident with
| Ordering.lt => Ordering.lt
| Ordering.gt => Ordering.gt
| Ordering.eq => $rhs)
let lPat ← `(@$(mkIdent ctorName):ident $ctorArgs1.reverse:term*)
let rPat ← `(@$(mkIdent ctorName):ident $ctorArgs2.reverse:term*)
let patterns := indPatterns ++ #[lPat, rPat]
let ltPatterns := indPatterns ++ #[lPat, ←`(_)]
let gtPatterns := indPatterns ++ #[←`(_), rPat]
#[←`(matchAltExpr| | $[$(patterns):term],* => $rhs:term),
←`(matchAltExpr| | $[$(ltPatterns):term],* => Ordering.lt),
←`(matchAltExpr| | $[$(gtPatterns):term],* => Ordering.gt)]
alts := alts ++ alt
return alts.pop.pop
def mkAuxFunction (ctx : Context) (i : Nat) : TermElabM Syntax := do
let auxFunName ← ctx.auxFunNames[i]
let indVal ← ctx.typeInfos[i]
let header ← mkOrdHeader ctx indVal
let mut body ← mkMatch ctx header indVal auxFunName
if ctx.usePartial || indVal.isRec then
let letDecls ← mkLocalInstanceLetDecls ctx `Ord header.argNames
body ← mkLet letDecls body
let binders := header.binders
if ctx.usePartial || indVal.isRec then
`(private partial def $(mkIdent auxFunName):ident $binders:explicitBinder* : Ordering := $body:term)
else
`(private def $(mkIdent auxFunName):ident $binders:explicitBinder* : Ordering := $body:term)
def mkMutualBlock (ctx : Context) : TermElabM Syntax := do
let mut auxDefs := #[]
for i in [:ctx.typeInfos.size] do
auxDefs := auxDefs.push (← mkAuxFunction ctx i)
`(mutual
$auxDefs:command*
end)
private def mkOrdInstanceCmds (declNames : Array Name) : TermElabM (Array Syntax) := do
let ctx ← mkContext "ord" declNames[0]
let cmds := #[← mkMutualBlock ctx] ++ (← mkInstanceCmds ctx `Ord declNames)
trace[Elab.Deriving.ord] "\n{cmds}"
return cmds
open Command
def mkOrdInstanceHandler (declNames : Array Name) : CommandElabM Bool := do
if (← declNames.allM isInductive) && declNames.size > 0 then
let cmds ← liftTermElabM none <| mkOrdInstanceCmds declNames
cmds.forM elabCommand
return true
else
return false
builtin_initialize
registerBuiltinDerivingHandler `Ord mkOrdInstanceHandler
registerTraceClass `Elab.Deriving.ord
end Lean.Elab.Deriving.Ord

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

@ -161,8 +161,8 @@ def TermInfo.format (ctx : ContextInfo) (info : TermInfo) : IO Format := do
def CompletionInfo.format (ctx : ContextInfo) (info : CompletionInfo) : IO Format :=
match info with
| CompletionInfo.dot i .. => return f!"[.] {← i.format ctx}"
| CompletionInfo.id stx lctx expectedType? => ctx.runMetaM lctx do return f!"[.] {stx} : {expectedType?}"
| _ => return f!"[.] {info.stx}"
| CompletionInfo.id stx lctx expectedType? => ctx.runMetaM lctx do return f!"[.] {stx} : {expectedType?} @ {formatStxRange ctx info.stx}"
| _ => return f!"[.] {info.stx} @ {formatStxRange ctx info.stx}"
def CommandInfo.format (ctx : ContextInfo) (info : CommandInfo) : IO Format := do
return f!"command @ {formatStxRange ctx info.stx}"

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

@ -309,8 +309,8 @@ builtin_initialize termElabAttribute : KeyedDeclsAttribute TermElab ← mkTermEl
inductive LVal where
| fieldIdx (ref : Syntax) (i : Nat)
/- Field `suffix?` is for producing better error messages because `x.y` may be a field access or a hierachical/composite name.
`ref` is the syntax object representing the field only. `stx` contains the object + field -/
| fieldName (ref : Syntax) (name : String) (suffix? : Option Name) (stx : Syntax)
`ref` is the syntax object representing the field. `targetStx` is the target object being accessed. -/
| fieldName (ref : Syntax) (name : String) (suffix? : Option Name) (targetStx : Syntax)
| getOp (ref : Syntax) (idx : Syntax)
def LVal.getRef : LVal → Syntax

8
stage0/src/Lean/Server/Completion.lean generated
View file

@ -6,6 +6,7 @@ Authors: Leonardo de Moura
import Lean.Environment
import Lean.Data.Lsp.LanguageFeatures
import Lean.Meta.Tactic.Apply
import Lean.Meta.Match.MatcherInfo
import Lean.Server.InfoUtils
import Lean.Parser.Extension
@ -22,7 +23,12 @@ def addToBlackList (env : Environment) (declName : Name) : Environment :=
private def isBlackListed (declName : Name) : MetaM Bool := do
let env ← getEnv
return declName.isInternal || isAuxRecursor env declName || isNoConfusion env declName || (← isRec declName) || completionBlackListExt.isTagged env declName
declName.isInternal
<||> isAuxRecursor env declName
<||> isNoConfusion env declName
<||> isRec declName
<||> completionBlackListExt.isTagged env declName
<||> isMatcher declName
private partial def consumeImplicitPrefix (e : Expr) : MetaM Expr := do
match e with

4
stage0/stdlib/CMakeLists.txt generated
View file

File diff suppressed because one or more lines are too long

6
stage0/stdlib/Init/Data.c generated
View file

@ -1,6 +1,6 @@
// Lean compiler output
// Module: Init.Data
// Imports: Init.Data.Basic Init.Data.Nat Init.Data.Char Init.Data.String Init.Data.List Init.Data.Int Init.Data.Array Init.Data.ByteArray Init.Data.FloatArray Init.Data.Fin Init.Data.UInt Init.Data.Float Init.Data.Option Init.Data.Random Init.Data.ToString Init.Data.Range Init.Data.Hashable Init.Data.OfScientific Init.Data.Format Init.Data.Stream
// Imports: Init.Data.Basic Init.Data.Nat Init.Data.Char Init.Data.String Init.Data.List Init.Data.Int Init.Data.Array Init.Data.ByteArray Init.Data.FloatArray Init.Data.Fin Init.Data.UInt Init.Data.Float Init.Data.Option Init.Data.Ord Init.Data.Random Init.Data.ToString Init.Data.Range Init.Data.Hashable Init.Data.OfScientific Init.Data.Format Init.Data.Stream
#include <lean/lean.h>
#if defined(__clang__)
#pragma clang diagnostic ignored "-Wunused-parameter"
@ -26,6 +26,7 @@ lean_object* initialize_Init_Data_Fin(lean_object*);
lean_object* initialize_Init_Data_UInt(lean_object*);
lean_object* initialize_Init_Data_Float(lean_object*);
lean_object* initialize_Init_Data_Option(lean_object*);
lean_object* initialize_Init_Data_Ord(lean_object*);
lean_object* initialize_Init_Data_Random(lean_object*);
lean_object* initialize_Init_Data_ToString(lean_object*);
lean_object* initialize_Init_Data_Range(lean_object*);
@ -77,6 +78,9 @@ lean_dec_ref(res);
res = initialize_Init_Data_Option(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Init_Data_Ord(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Init_Data_Random(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);

423
stage0/stdlib/Init/Data/Ord.c generated Normal file
View file

@ -0,0 +1,423 @@
// Lean compiler output
// Module: Init.Data.Ord
// Imports: Init.Data.Int Init.Data.String
#include <lean/lean.h>
#if defined(__clang__)
#pragma clang diagnostic ignored "-Wunused-parameter"
#pragma clang diagnostic ignored "-Wunused-label"
#elif defined(__GNUC__) && !defined(__CLANG__)
#pragma GCC diagnostic ignored "-Wunused-parameter"
#pragma GCC diagnostic ignored "-Wunused-label"
#pragma GCC diagnostic ignored "-Wunused-but-set-variable"
#endif
#ifdef __cplusplus
extern "C" {
#endif
uint8_t l_instOrdBool(uint8_t, uint8_t);
lean_object* l_compareOfLessAndEq___at_instOrdString___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_instOrdNat___boxed(lean_object*, lean_object*);
uint8_t lean_nat_dec_eq(lean_object*, lean_object*);
lean_object* l_instOrdBool_match__1(lean_object*);
uint8_t l_instInhabitedOrdering;
lean_object* l_instOrdBool_match__1___rarg(uint8_t, uint8_t, lean_object*, lean_object*, lean_object*);
lean_object* l_compareOfLessAndEq___at_instOrdNat___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_compareOfLessAndEq___at_instOrdInt___spec__1(lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_instOrdInt(lean_object*, lean_object*);
uint8_t l_instOrdNat(lean_object*, lean_object*);
lean_object* l_compareOfLessAndEq___at_instOrdInt___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_instOrdString___boxed(lean_object*, lean_object*);
lean_object* l_instOrdBool___boxed(lean_object*, lean_object*);
uint8_t l_compareOfLessAndEq___rarg(lean_object*, lean_object*, lean_object*, uint8_t, lean_object*);
uint8_t lean_int_dec_lt(lean_object*, lean_object*);
lean_object* l_instOrdInt___boxed(lean_object*, lean_object*);
uint8_t l_instOrdString(lean_object*, lean_object*);
uint8_t l_compareOfLessAndEq___at_instOrdNat___spec__1(lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t lean_int_dec_eq(lean_object*, lean_object*);
lean_object* l_instOrdBool_match__1___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_compareOfLessAndEq(lean_object*);
lean_object* l_compareOfLessAndEq___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_compareOfLessAndEq___at_instOrdString___spec__1(lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t lean_string_dec_lt(lean_object*, lean_object*);
uint8_t lean_string_dec_eq(lean_object*, lean_object*);
uint8_t lean_nat_dec_lt(lean_object*, lean_object*);
static uint8_t _init_l_instInhabitedOrdering() {
_start:
{
uint8_t x_1;
x_1 = 0;
return x_1;
}
}
uint8_t l_compareOfLessAndEq___rarg(lean_object* x_1, lean_object* x_2, lean_object* x_3, uint8_t x_4, lean_object* x_5) {
_start:
{
if (x_4 == 0)
{
lean_object* x_6; uint8_t x_7;
x_6 = lean_apply_2(x_5, x_1, x_2);
x_7 = lean_unbox(x_6);
lean_dec(x_6);
if (x_7 == 0)
{
uint8_t x_8;
x_8 = 2;
return x_8;
}
else
{
uint8_t x_9;
x_9 = 1;
return x_9;
}
}
else
{
uint8_t x_10;
lean_dec(x_5);
lean_dec(x_2);
lean_dec(x_1);
x_10 = 0;
return x_10;
}
}
}
lean_object* l_compareOfLessAndEq(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l_compareOfLessAndEq___rarg___boxed), 5, 0);
return x_2;
}
}
lean_object* l_compareOfLessAndEq___rarg___boxed(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; uint8_t x_7; lean_object* x_8;
x_6 = lean_unbox(x_4);
lean_dec(x_4);
x_7 = l_compareOfLessAndEq___rarg(x_1, x_2, x_3, x_6, x_5);
lean_dec(x_3);
x_8 = lean_box(x_7);
return x_8;
}
}
uint8_t l_compareOfLessAndEq___at_instOrdNat___spec__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
uint8_t x_5;
x_5 = lean_nat_dec_lt(x_1, x_2);
if (x_5 == 0)
{
uint8_t x_6;
x_6 = lean_nat_dec_eq(x_3, x_4);
if (x_6 == 0)
{
uint8_t x_7;
x_7 = 2;
return x_7;
}
else
{
uint8_t x_8;
x_8 = 1;
return x_8;
}
}
else
{
uint8_t x_9;
x_9 = 0;
return x_9;
}
}
}
uint8_t l_instOrdNat(lean_object* x_1, lean_object* x_2) {
_start:
{
uint8_t x_3;
x_3 = l_compareOfLessAndEq___at_instOrdNat___spec__1(x_1, x_2, x_1, x_2);
return x_3;
}
}
lean_object* l_compareOfLessAndEq___at_instOrdNat___spec__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
uint8_t x_5; lean_object* x_6;
x_5 = l_compareOfLessAndEq___at_instOrdNat___spec__1(x_1, x_2, x_3, x_4);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_2);
lean_dec(x_1);
x_6 = lean_box(x_5);
return x_6;
}
}
lean_object* l_instOrdNat___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
uint8_t x_3; lean_object* x_4;
x_3 = l_instOrdNat(x_1, x_2);
lean_dec(x_2);
lean_dec(x_1);
x_4 = lean_box(x_3);
return x_4;
}
}
uint8_t l_compareOfLessAndEq___at_instOrdInt___spec__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
uint8_t x_5;
x_5 = lean_int_dec_lt(x_1, x_2);
if (x_5 == 0)
{
uint8_t x_6;
x_6 = lean_int_dec_eq(x_3, x_4);
if (x_6 == 0)
{
uint8_t x_7;
x_7 = 2;
return x_7;
}
else
{
uint8_t x_8;
x_8 = 1;
return x_8;
}
}
else
{
uint8_t x_9;
x_9 = 0;
return x_9;
}
}
}
uint8_t l_instOrdInt(lean_object* x_1, lean_object* x_2) {
_start:
{
uint8_t x_3;
x_3 = l_compareOfLessAndEq___at_instOrdInt___spec__1(x_1, x_2, x_1, x_2);
return x_3;
}
}
lean_object* l_compareOfLessAndEq___at_instOrdInt___spec__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
uint8_t x_5; lean_object* x_6;
x_5 = l_compareOfLessAndEq___at_instOrdInt___spec__1(x_1, x_2, x_3, x_4);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_2);
lean_dec(x_1);
x_6 = lean_box(x_5);
return x_6;
}
}
lean_object* l_instOrdInt___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
uint8_t x_3; lean_object* x_4;
x_3 = l_instOrdInt(x_1, x_2);
lean_dec(x_2);
lean_dec(x_1);
x_4 = lean_box(x_3);
return x_4;
}
}
lean_object* l_instOrdBool_match__1___rarg(uint8_t x_1, uint8_t x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5) {
_start:
{
if (x_1 == 0)
{
lean_dec(x_4);
if (x_2 == 0)
{
lean_object* x_6; lean_object* x_7; lean_object* x_8;
lean_dec(x_3);
x_6 = lean_box(x_2);
x_7 = lean_box(x_2);
x_8 = lean_apply_2(x_5, x_6, x_7);
return x_8;
}
else
{
lean_object* x_9; lean_object* x_10;
lean_dec(x_5);
x_9 = lean_box(0);
x_10 = lean_apply_1(x_3, x_9);
return x_10;
}
}
else
{
lean_dec(x_3);
if (x_2 == 0)
{
lean_object* x_11; lean_object* x_12;
lean_dec(x_5);
x_11 = lean_box(0);
x_12 = lean_apply_1(x_4, x_11);
return x_12;
}
else
{
lean_object* x_13; lean_object* x_14; lean_object* x_15;
lean_dec(x_4);
x_13 = lean_box(x_2);
x_14 = lean_box(x_2);
x_15 = lean_apply_2(x_5, x_13, x_14);
return x_15;
}
}
}
}
lean_object* l_instOrdBool_match__1(lean_object* x_1) {
_start:
{
lean_object* x_2;
x_2 = lean_alloc_closure((void*)(l_instOrdBool_match__1___rarg___boxed), 5, 0);
return x_2;
}
}
lean_object* l_instOrdBool_match__1___rarg___boxed(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; uint8_t x_7; lean_object* x_8;
x_6 = lean_unbox(x_1);
lean_dec(x_1);
x_7 = lean_unbox(x_2);
lean_dec(x_2);
x_8 = l_instOrdBool_match__1___rarg(x_6, x_7, x_3, x_4, x_5);
return x_8;
}
}
uint8_t l_instOrdBool(uint8_t x_1, uint8_t x_2) {
_start:
{
if (x_1 == 0)
{
if (x_2 == 0)
{
uint8_t x_3;
x_3 = 1;
return x_3;
}
else
{
uint8_t x_4;
x_4 = 0;
return x_4;
}
}
else
{
if (x_2 == 0)
{
uint8_t x_5;
x_5 = 2;
return x_5;
}
else
{
uint8_t x_6;
x_6 = 1;
return x_6;
}
}
}
}
lean_object* l_instOrdBool___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
uint8_t x_3; uint8_t x_4; uint8_t x_5; lean_object* x_6;
x_3 = lean_unbox(x_1);
lean_dec(x_1);
x_4 = lean_unbox(x_2);
lean_dec(x_2);
x_5 = l_instOrdBool(x_3, x_4);
x_6 = lean_box(x_5);
return x_6;
}
}
uint8_t l_compareOfLessAndEq___at_instOrdString___spec__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
uint8_t x_5;
x_5 = lean_string_dec_lt(x_1, x_2);
if (x_5 == 0)
{
uint8_t x_6;
x_6 = lean_string_dec_eq(x_3, x_4);
if (x_6 == 0)
{
uint8_t x_7;
x_7 = 2;
return x_7;
}
else
{
uint8_t x_8;
x_8 = 1;
return x_8;
}
}
else
{
uint8_t x_9;
x_9 = 0;
return x_9;
}
}
}
uint8_t l_instOrdString(lean_object* x_1, lean_object* x_2) {
_start:
{
uint8_t x_3;
x_3 = l_compareOfLessAndEq___at_instOrdString___spec__1(x_1, x_2, x_1, x_2);
return x_3;
}
}
lean_object* l_compareOfLessAndEq___at_instOrdString___spec__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4) {
_start:
{
uint8_t x_5; lean_object* x_6;
x_5 = l_compareOfLessAndEq___at_instOrdString___spec__1(x_1, x_2, x_3, x_4);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_2);
lean_dec(x_1);
x_6 = lean_box(x_5);
return x_6;
}
}
lean_object* l_instOrdString___boxed(lean_object* x_1, lean_object* x_2) {
_start:
{
uint8_t x_3; lean_object* x_4;
x_3 = l_instOrdString(x_1, x_2);
lean_dec(x_2);
lean_dec(x_1);
x_4 = lean_box(x_3);
return x_4;
}
}
lean_object* initialize_Init_Data_Int(lean_object*);
lean_object* initialize_Init_Data_String(lean_object*);
static bool _G_initialized = false;
lean_object* initialize_Init_Data_Ord(lean_object* w) {
lean_object * res;
if (_G_initialized) return lean_io_result_mk_ok(lean_box(0));
_G_initialized = true;
res = initialize_Init_Data_Int(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Init_Data_String(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
l_instInhabitedOrdering = _init_l_instInhabitedOrdering();
return lean_io_result_mk_ok(lean_box(0));
}
#ifdef __cplusplus
}
#endif

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

@ -27670,10 +27670,12 @@ goto block_348;
else
{
lean_object* x_1753; lean_object* x_1754; lean_object* x_1755; lean_object* x_1756; lean_object* x_1757;
lean_dec(x_1);
x_1753 = l_Lean_Syntax_getId(x_1409);
x_1754 = lean_erase_macro_scopes(x_1753);
x_1755 = l_Lean_Name_components(x_1754);
x_1756 = l_List_map___at___private_Lean_Elab_App_0__Lean_Elab_Term_elabAppFn___spec__3(x_1, x_1409, x_1755);
lean_inc(x_1407);
x_1756 = l_List_map___at___private_Lean_Elab_App_0__Lean_Elab_Term_elabAppFn___spec__3(x_1407, x_1409, x_1755);
x_1757 = l_List_append___rarg(x_1756, x_2);
x_1 = x_1407;
x_2 = x_1757;
@ -29338,10 +29340,12 @@ return x_2096;
else
{
lean_object* x_2118; lean_object* x_2119; lean_object* x_2120; lean_object* x_2121; lean_object* x_2122;
lean_dec(x_1);
x_2118 = l_Lean_Syntax_getId(x_1783);
x_2119 = lean_erase_macro_scopes(x_2118);
x_2120 = l_Lean_Name_components(x_2119);
x_2121 = l_List_map___at___private_Lean_Elab_App_0__Lean_Elab_Term_elabAppFn___spec__4(x_1, x_1783, x_2120);
lean_inc(x_1781);
x_2121 = l_List_map___at___private_Lean_Elab_App_0__Lean_Elab_Term_elabAppFn___spec__4(x_1781, x_1783, x_2120);
x_2122 = l_List_append___rarg(x_2121, x_2);
x_1 = x_1781;
x_2 = x_2122;

6
stage0/stdlib/Lean/Elab/Deriving.c generated
View file

@ -1,6 +1,6 @@
// Lean compiler output
// Module: Lean.Elab.Deriving
// Imports: Init Lean.Elab.Deriving.Basic Lean.Elab.Deriving.Util Lean.Elab.Deriving.Inhabited Lean.Elab.Deriving.BEq Lean.Elab.Deriving.DecEq Lean.Elab.Deriving.Repr Lean.Elab.Deriving.FromToJson Lean.Elab.Deriving.SizeOf Lean.Elab.Deriving.Hashable
// Imports: Init Lean.Elab.Deriving.Basic Lean.Elab.Deriving.Util Lean.Elab.Deriving.Inhabited Lean.Elab.Deriving.BEq Lean.Elab.Deriving.DecEq Lean.Elab.Deriving.Repr Lean.Elab.Deriving.FromToJson Lean.Elab.Deriving.SizeOf Lean.Elab.Deriving.Hashable Lean.Elab.Deriving.Ord
#include <lean/lean.h>
#if defined(__clang__)
#pragma clang diagnostic ignored "-Wunused-parameter"
@ -23,6 +23,7 @@ lean_object* initialize_Lean_Elab_Deriving_Repr(lean_object*);
lean_object* initialize_Lean_Elab_Deriving_FromToJson(lean_object*);
lean_object* initialize_Lean_Elab_Deriving_SizeOf(lean_object*);
lean_object* initialize_Lean_Elab_Deriving_Hashable(lean_object*);
lean_object* initialize_Lean_Elab_Deriving_Ord(lean_object*);
static bool _G_initialized = false;
lean_object* initialize_Lean_Elab_Deriving(lean_object* w) {
lean_object * res;
@ -58,6 +59,9 @@ lean_dec_ref(res);
res = initialize_Lean_Elab_Deriving_Hashable(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Lean_Elab_Deriving_Ord(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
return lean_io_result_mk_ok(lean_box(0));
}
#ifdef __cplusplus

5322
stage0/stdlib/Lean/Elab/Deriving/Ord.c generated Normal file
View file

File diff suppressed because it is too large Load diff

66
stage0/stdlib/Lean/Elab/InfoTree.c generated
View file

@ -2967,14 +2967,13 @@ return x_22;
}
case 1:
{
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; lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; lean_object* x_34; lean_object* x_35; lean_object* x_36;
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; lean_object* x_30; lean_object* x_31; lean_object* x_32; lean_object* x_33; 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; lean_object* x_41;
x_23 = lean_ctor_get(x_2, 0);
lean_inc(x_23);
x_24 = lean_ctor_get(x_2, 1);
lean_inc(x_24);
x_25 = lean_ctor_get(x_2, 2);
lean_inc(x_25);
lean_dec(x_2);
x_26 = l_Std_fmt___at_Lean_Elab_CompletionInfo_format___spec__1(x_23);
x_27 = l_Lean_Elab_CompletionInfo_format___closed__2;
x_28 = lean_alloc_ctor(4, 2, 0);
@ -2989,35 +2988,56 @@ lean_dec(x_25);
x_32 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_32, 0, x_30);
lean_ctor_set(x_32, 1, x_31);
x_33 = l_Std_Format_join___closed__1;
x_33 = l_Lean_Elab_TermInfo_format___lambda__1___closed__2;
x_34 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_34, 0, x_32);
lean_ctor_set(x_34, 1, x_33);
x_35 = lean_alloc_closure((void*)(l_ReaderT_pure___at_Lean_Elab_CompletionInfo_format___spec__3___rarg___boxed), 6, 1);
lean_closure_set(x_35, 0, x_34);
x_36 = l_Lean_Elab_ContextInfo_runMetaM___rarg(x_1, x_24, x_35, x_3);
x_35 = l_Lean_Elab_CompletionInfo_stx(x_2);
lean_dec(x_2);
x_36 = l___private_Lean_Elab_InfoTree_0__Lean_Elab_formatStxRange(x_1, x_35);
lean_dec(x_35);
x_37 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_37, 0, x_34);
lean_ctor_set(x_37, 1, x_36);
x_38 = l_Std_Format_join___closed__1;
x_39 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_39, 0, x_37);
lean_ctor_set(x_39, 1, x_38);
x_40 = lean_alloc_closure((void*)(l_ReaderT_pure___at_Lean_Elab_CompletionInfo_format___spec__3___rarg___boxed), 6, 1);
lean_closure_set(x_40, 0, x_39);
x_41 = l_Lean_Elab_ContextInfo_runMetaM___rarg(x_1, x_24, x_40, x_3);
lean_dec(x_1);
return x_36;
return x_41;
}
default:
{
lean_object* x_37; lean_object* x_38; lean_object* x_39; lean_object* x_40; lean_object* x_41; lean_object* x_42; lean_object* x_43;
lean_dec(x_1);
x_37 = l_Lean_Elab_CompletionInfo_stx(x_2);
lean_object* x_42; lean_object* x_43; lean_object* x_44; lean_object* x_45; lean_object* x_46; lean_object* x_47; lean_object* x_48; lean_object* x_49; lean_object* x_50; lean_object* x_51; lean_object* x_52;
x_42 = l_Lean_Elab_CompletionInfo_stx(x_2);
lean_dec(x_2);
x_38 = l_Std_fmt___at_Lean_Elab_CompletionInfo_format___spec__1(x_37);
x_39 = l_Lean_Elab_CompletionInfo_format___closed__2;
x_40 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_40, 0, x_39);
lean_ctor_set(x_40, 1, x_38);
x_41 = l_Std_Format_join___closed__1;
x_42 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_42, 0, x_40);
lean_ctor_set(x_42, 1, x_41);
x_43 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_43, 0, x_42);
lean_ctor_set(x_43, 1, x_3);
return x_43;
lean_inc(x_42);
x_43 = l_Std_fmt___at_Lean_Elab_CompletionInfo_format___spec__1(x_42);
x_44 = l_Lean_Elab_CompletionInfo_format___closed__2;
x_45 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_45, 0, x_44);
lean_ctor_set(x_45, 1, x_43);
x_46 = l_Lean_Elab_TermInfo_format___lambda__1___closed__2;
x_47 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_47, 0, x_45);
lean_ctor_set(x_47, 1, x_46);
x_48 = l___private_Lean_Elab_InfoTree_0__Lean_Elab_formatStxRange(x_1, x_42);
lean_dec(x_42);
lean_dec(x_1);
x_49 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_49, 0, x_47);
lean_ctor_set(x_49, 1, x_48);
x_50 = l_Std_Format_join___closed__1;
x_51 = lean_alloc_ctor(4, 2, 0);
lean_ctor_set(x_51, 0, x_49);
lean_ctor_set(x_51, 1, x_50);
x_52 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_52, 0, x_51);
lean_ctor_set(x_52, 1, x_3);
return x_52;
}
}
}

397
stage0/stdlib/Lean/Server/Completion.c generated
View file

@ -1,6 +1,6 @@
// Lean compiler output
// Module: Lean.Server.Completion
// Imports: Init Lean.Environment Lean.Data.Lsp.LanguageFeatures Lean.Meta.Tactic.Apply Lean.Server.InfoUtils Lean.Parser.Extension
// Imports: Init Lean.Environment Lean.Data.Lsp.LanguageFeatures Lean.Meta.Tactic.Apply Lean.Meta.Match.MatcherInfo Lean.Server.InfoUtils Lean.Parser.Extension
#include <lean/lean.h>
#if defined(__clang__)
#pragma clang diagnostic ignored "-Wunused-parameter"
@ -188,6 +188,7 @@ lean_object* l_Std_PersistentHashMap_find_x3f___at_Lean_Parser_getCategory___spe
lean_object* l_Std_PersistentHashMap_foldlM___at___private_Lean_Server_Completion_0__Lean_Server_Completion_idCompletionCore___spec__34(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_List_forIn_loop___at___private_Lean_Server_Completion_0__Lean_Server_Completion_idCompletionCore___spec__19___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_format_pretty(lean_object*, lean_object*);
lean_object* l_Lean_Meta_isMatcher(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Std_PersistentHashMap_foldlMAux_traverse___at___private_Lean_Server_Completion_0__Lean_Server_Completion_dotCompletion___spec__8___rarg(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___private_Lean_Server_Completion_0__Lean_Server_Completion_runM_match__1(lean_object*);
lean_object* l___private_Lean_Server_Completion_0__Lean_Server_Completion_runM_match__1___rarg(lean_object*, lean_object*, lean_object*);
@ -584,187 +585,281 @@ return x_18;
lean_object* l___private_Lean_Server_Completion_0__Lean_Server_Completion_isBlackListed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
_start:
{
lean_object* x_7; lean_object* x_8; lean_object* x_9; lean_object* x_10; lean_object* x_11; uint8_t x_12;
lean_object* x_7; uint8_t x_8;
x_7 = lean_st_ref_get(x_5, x_6);
x_8 = lean_ctor_get(x_7, 0);
lean_inc(x_8);
x_9 = lean_ctor_get(x_7, 1);
lean_inc(x_9);
lean_dec(x_7);
x_10 = lean_ctor_get(x_8, 0);
lean_inc(x_10);
lean_dec(x_8);
lean_inc(x_1);
x_11 = l_Lean_isRec___at___private_Lean_Server_Completion_0__Lean_Server_Completion_isBlackListed___spec__1(x_1, x_2, x_3, x_4, x_5, x_9);
x_12 = !lean_is_exclusive(x_11);
x_8 = !lean_is_exclusive(x_7);
if (x_8 == 0)
{
lean_object* x_9; lean_object* x_10; lean_object* x_11; uint8_t x_12;
x_9 = lean_ctor_get(x_7, 0);
x_10 = lean_ctor_get(x_7, 1);
x_11 = lean_ctor_get(x_9, 0);
lean_inc(x_11);
lean_dec(x_9);
x_12 = l_Lean_Name_isInternal(x_1);
if (x_12 == 0)
{
lean_object* x_13; uint8_t x_14;
x_13 = lean_ctor_get(x_11, 0);
x_14 = l_Lean_Name_isInternal(x_1);
x_13 = l_Lean_auxRecExt;
x_14 = l_Lean_TagDeclarationExtension_isTagged(x_13, x_11, x_1);
if (x_14 == 0)
{
lean_object* x_15; uint8_t x_16;
x_15 = l_Lean_auxRecExt;
x_16 = l_Lean_TagDeclarationExtension_isTagged(x_15, x_10, x_1);
x_15 = l_Lean_noConfusionExt;
x_16 = l_Lean_TagDeclarationExtension_isTagged(x_15, x_11, x_1);
if (x_16 == 0)
{
lean_object* x_17; uint8_t x_18;
x_17 = l_Lean_noConfusionExt;
x_18 = l_Lean_TagDeclarationExtension_isTagged(x_17, x_10, x_1);
if (x_18 == 0)
{
uint8_t x_19;
x_19 = lean_unbox(x_13);
lean_dec(x_13);
lean_object* x_17; lean_object* x_18; uint8_t x_19;
lean_free_object(x_7);
lean_inc(x_1);
x_17 = l_Lean_isRec___at___private_Lean_Server_Completion_0__Lean_Server_Completion_isBlackListed___spec__1(x_1, x_2, x_3, x_4, x_5, x_10);
x_18 = lean_ctor_get(x_17, 0);
lean_inc(x_18);
x_19 = lean_unbox(x_18);
if (x_19 == 0)
{
lean_object* x_20; uint8_t x_21; lean_object* x_22;
x_20 = l_Lean_Server_Completion_completionBlackListExt;
x_21 = l_Lean_TagDeclarationExtension_isTagged(x_20, x_10, x_1);
lean_dec(x_1);
lean_dec(x_10);
x_22 = lean_box(x_21);
lean_ctor_set(x_11, 0, x_22);
return x_11;
}
else
uint8_t x_20;
lean_dec(x_18);
x_20 = !lean_is_exclusive(x_17);
if (x_20 == 0)
{
uint8_t x_23; lean_object* x_24;
lean_dec(x_10);
lean_dec(x_1);
x_23 = 1;
x_24 = lean_box(x_23);
lean_ctor_set(x_11, 0, x_24);
return x_11;
}
}
else
{
uint8_t x_25; lean_object* x_26;
lean_dec(x_13);
lean_dec(x_10);
lean_dec(x_1);
x_25 = 1;
x_26 = lean_box(x_25);
lean_ctor_set(x_11, 0, x_26);
return x_11;
}
}
else
{
uint8_t x_27; lean_object* x_28;
lean_dec(x_13);
lean_dec(x_10);
lean_dec(x_1);
x_27 = 1;
x_28 = lean_box(x_27);
lean_ctor_set(x_11, 0, x_28);
return x_11;
}
}
else
{
uint8_t x_29; lean_object* x_30;
lean_dec(x_13);
lean_dec(x_10);
lean_dec(x_1);
x_29 = 1;
x_30 = lean_box(x_29);
lean_ctor_set(x_11, 0, x_30);
return x_11;
}
}
else
{
lean_object* x_31; lean_object* x_32; uint8_t x_33;
x_31 = lean_ctor_get(x_11, 0);
x_32 = lean_ctor_get(x_11, 1);
lean_inc(x_32);
lean_inc(x_31);
lean_object* x_21; lean_object* x_22; lean_object* x_23; uint8_t x_24;
x_21 = lean_ctor_get(x_17, 1);
x_22 = lean_ctor_get(x_17, 0);
lean_dec(x_22);
x_23 = l_Lean_Server_Completion_completionBlackListExt;
x_24 = l_Lean_TagDeclarationExtension_isTagged(x_23, x_11, x_1);
lean_dec(x_11);
x_33 = l_Lean_Name_isInternal(x_1);
if (x_24 == 0)
{
lean_object* x_25;
lean_free_object(x_17);
x_25 = l_Lean_Meta_isMatcher(x_1, x_2, x_3, x_4, x_5, x_21);
lean_dec(x_1);
return x_25;
}
else
{
lean_object* x_26;
lean_dec(x_1);
x_26 = lean_box(x_24);
lean_ctor_set(x_17, 0, x_26);
return x_17;
}
}
else
{
lean_object* x_27; lean_object* x_28; uint8_t x_29;
x_27 = lean_ctor_get(x_17, 1);
lean_inc(x_27);
lean_dec(x_17);
x_28 = l_Lean_Server_Completion_completionBlackListExt;
x_29 = l_Lean_TagDeclarationExtension_isTagged(x_28, x_11, x_1);
lean_dec(x_11);
if (x_29 == 0)
{
lean_object* x_30;
x_30 = l_Lean_Meta_isMatcher(x_1, x_2, x_3, x_4, x_5, x_27);
lean_dec(x_1);
return x_30;
}
else
{
lean_object* x_31; lean_object* x_32;
lean_dec(x_1);
x_31 = lean_box(x_29);
x_32 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_32, 0, x_31);
lean_ctor_set(x_32, 1, x_27);
return x_32;
}
}
}
else
{
uint8_t x_33;
lean_dec(x_11);
lean_dec(x_1);
x_33 = !lean_is_exclusive(x_17);
if (x_33 == 0)
{
lean_object* x_34; uint8_t x_35;
x_34 = l_Lean_auxRecExt;
x_35 = l_Lean_TagDeclarationExtension_isTagged(x_34, x_10, x_1);
if (x_35 == 0)
{
lean_object* x_36; uint8_t x_37;
x_36 = l_Lean_noConfusionExt;
x_37 = l_Lean_TagDeclarationExtension_isTagged(x_36, x_10, x_1);
if (x_37 == 0)
{
uint8_t x_38;
x_38 = lean_unbox(x_31);
lean_dec(x_31);
if (x_38 == 0)
{
lean_object* x_39; uint8_t x_40; lean_object* x_41; lean_object* x_42;
x_39 = l_Lean_Server_Completion_completionBlackListExt;
x_40 = l_Lean_TagDeclarationExtension_isTagged(x_39, x_10, x_1);
lean_dec(x_1);
lean_dec(x_10);
x_41 = lean_box(x_40);
x_42 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_42, 0, x_41);
lean_ctor_set(x_42, 1, x_32);
return x_42;
lean_object* x_34;
x_34 = lean_ctor_get(x_17, 0);
lean_dec(x_34);
return x_17;
}
else
{
uint8_t x_43; lean_object* x_44; lean_object* x_45;
lean_dec(x_10);
lean_dec(x_1);
x_43 = 1;
x_44 = lean_box(x_43);
x_45 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_45, 0, x_44);
lean_ctor_set(x_45, 1, x_32);
return x_45;
lean_object* x_35; lean_object* x_36;
x_35 = lean_ctor_get(x_17, 1);
lean_inc(x_35);
lean_dec(x_17);
x_36 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_36, 0, x_18);
lean_ctor_set(x_36, 1, x_35);
return x_36;
}
}
}
else
{
uint8_t x_46; lean_object* x_47; lean_object* x_48;
lean_dec(x_31);
lean_dec(x_10);
lean_object* x_37;
lean_dec(x_11);
lean_dec(x_1);
x_46 = 1;
x_47 = lean_box(x_46);
x_48 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_48, 0, x_47);
lean_ctor_set(x_48, 1, x_32);
return x_48;
x_37 = lean_box(x_16);
lean_ctor_set(x_7, 0, x_37);
return x_7;
}
}
else
{
uint8_t x_49; lean_object* x_50; lean_object* x_51;
lean_dec(x_31);
lean_dec(x_10);
lean_object* x_38;
lean_dec(x_11);
lean_dec(x_1);
x_49 = 1;
x_50 = lean_box(x_49);
x_51 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_51, 0, x_50);
lean_ctor_set(x_51, 1, x_32);
return x_51;
x_38 = lean_box(x_14);
lean_ctor_set(x_7, 0, x_38);
return x_7;
}
}
else
{
uint8_t x_52; lean_object* x_53; lean_object* x_54;
lean_dec(x_31);
lean_dec(x_10);
lean_object* x_39;
lean_dec(x_11);
lean_dec(x_1);
x_52 = 1;
x_53 = lean_box(x_52);
x_54 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_54, 0, x_53);
lean_ctor_set(x_54, 1, x_32);
return x_54;
x_39 = lean_box(x_12);
lean_ctor_set(x_7, 0, x_39);
return x_7;
}
}
else
{
lean_object* x_40; lean_object* x_41; lean_object* x_42; uint8_t x_43;
x_40 = lean_ctor_get(x_7, 0);
x_41 = lean_ctor_get(x_7, 1);
lean_inc(x_41);
lean_inc(x_40);
lean_dec(x_7);
x_42 = lean_ctor_get(x_40, 0);
lean_inc(x_42);
lean_dec(x_40);
x_43 = l_Lean_Name_isInternal(x_1);
if (x_43 == 0)
{
lean_object* x_44; uint8_t x_45;
x_44 = l_Lean_auxRecExt;
x_45 = l_Lean_TagDeclarationExtension_isTagged(x_44, x_42, x_1);
if (x_45 == 0)
{
lean_object* x_46; uint8_t x_47;
x_46 = l_Lean_noConfusionExt;
x_47 = l_Lean_TagDeclarationExtension_isTagged(x_46, x_42, x_1);
if (x_47 == 0)
{
lean_object* x_48; lean_object* x_49; uint8_t x_50;
lean_inc(x_1);
x_48 = l_Lean_isRec___at___private_Lean_Server_Completion_0__Lean_Server_Completion_isBlackListed___spec__1(x_1, x_2, x_3, x_4, x_5, x_41);
x_49 = lean_ctor_get(x_48, 0);
lean_inc(x_49);
x_50 = lean_unbox(x_49);
if (x_50 == 0)
{
lean_object* x_51; lean_object* x_52; lean_object* x_53; uint8_t x_54;
lean_dec(x_49);
x_51 = lean_ctor_get(x_48, 1);
lean_inc(x_51);
if (lean_is_exclusive(x_48)) {
lean_ctor_release(x_48, 0);
lean_ctor_release(x_48, 1);
x_52 = x_48;
} else {
lean_dec_ref(x_48);
x_52 = lean_box(0);
}
x_53 = l_Lean_Server_Completion_completionBlackListExt;
x_54 = l_Lean_TagDeclarationExtension_isTagged(x_53, x_42, x_1);
lean_dec(x_42);
if (x_54 == 0)
{
lean_object* x_55;
lean_dec(x_52);
x_55 = l_Lean_Meta_isMatcher(x_1, x_2, x_3, x_4, x_5, x_51);
lean_dec(x_1);
return x_55;
}
else
{
lean_object* x_56; lean_object* x_57;
lean_dec(x_1);
x_56 = lean_box(x_54);
if (lean_is_scalar(x_52)) {
x_57 = lean_alloc_ctor(0, 2, 0);
} else {
x_57 = x_52;
}
lean_ctor_set(x_57, 0, x_56);
lean_ctor_set(x_57, 1, x_51);
return x_57;
}
}
else
{
lean_object* x_58; lean_object* x_59; lean_object* x_60;
lean_dec(x_42);
lean_dec(x_1);
x_58 = lean_ctor_get(x_48, 1);
lean_inc(x_58);
if (lean_is_exclusive(x_48)) {
lean_ctor_release(x_48, 0);
lean_ctor_release(x_48, 1);
x_59 = x_48;
} else {
lean_dec_ref(x_48);
x_59 = lean_box(0);
}
if (lean_is_scalar(x_59)) {
x_60 = lean_alloc_ctor(0, 2, 0);
} else {
x_60 = x_59;
}
lean_ctor_set(x_60, 0, x_49);
lean_ctor_set(x_60, 1, x_58);
return x_60;
}
}
else
{
lean_object* x_61; lean_object* x_62;
lean_dec(x_42);
lean_dec(x_1);
x_61 = lean_box(x_47);
x_62 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_62, 0, x_61);
lean_ctor_set(x_62, 1, x_41);
return x_62;
}
}
else
{
lean_object* x_63; lean_object* x_64;
lean_dec(x_42);
lean_dec(x_1);
x_63 = lean_box(x_45);
x_64 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_64, 0, x_63);
lean_ctor_set(x_64, 1, x_41);
return x_64;
}
}
else
{
lean_object* x_65; lean_object* x_66;
lean_dec(x_42);
lean_dec(x_1);
x_65 = lean_box(x_43);
x_66 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_66, 0, x_65);
lean_ctor_set(x_66, 1, x_41);
return x_66;
}
}
}
@ -13862,6 +13957,7 @@ lean_object* initialize_Init(lean_object*);
lean_object* initialize_Lean_Environment(lean_object*);
lean_object* initialize_Lean_Data_Lsp_LanguageFeatures(lean_object*);
lean_object* initialize_Lean_Meta_Tactic_Apply(lean_object*);
lean_object* initialize_Lean_Meta_Match_MatcherInfo(lean_object*);
lean_object* initialize_Lean_Server_InfoUtils(lean_object*);
lean_object* initialize_Lean_Parser_Extension(lean_object*);
static bool _G_initialized = false;
@ -13881,6 +13977,9 @@ lean_dec_ref(res);
res = initialize_Lean_Meta_Tactic_Apply(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Lean_Meta_Match_MatcherInfo(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);
res = initialize_Lean_Server_InfoUtils(lean_io_mk_world());
if (lean_io_result_is_error(res)) return res;
lean_dec_ref(res);

246
stage0/stdlib/Lean/Server/FileWorker.c generated
View file

@ -19,7 +19,6 @@ lean_object* l_Lean_Server_FileWorker_leanpkgSetupSearchPath___closed__3;
lean_object* l_ReaderT_pure___at_Lean_Server_FileWorker_handleCompletion___spec__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_MapDeclarationExtension_find_x3f___at_Lean_findDeclarationRangesCore_x3f___spec__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Server_FileWorker_handleWaitForDiagnostics___lambda__3(lean_object*, lean_object*);
uint8_t l_Lean_isRecCore(lean_object*, lean_object*);
lean_object* lean_string_push(lean_object*, uint32_t);
extern lean_object* l_Lean_Name_toString___closed__1;
lean_object* l_IO_FS_Handle_readToEnd_read___at_IO_Process_output___spec__3(lean_object*, lean_object*, lean_object*);
@ -29,6 +28,7 @@ lean_object* l_Lean_Server_FileWorker_handleWaitForDiagnostics___lambda__1___box
size_t l_USize_add(size_t, size_t);
extern lean_object* l_Lean_Name_getString_x21___closed__3;
lean_object* l_Lean_Server_FileWorker_handleSemanticTokensRange(lean_object*, lean_object*, lean_object*);
lean_object* l_Std_PersistentArray_forIn___at_Lean_Server_FileWorker_handleDefinition___spec__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Server_FileWorker_parseParams___at_Lean_Server_FileWorker_handleNotification___spec__1___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Array_forInUnsafe_loop___at_Lean_Server_FileWorker_handleCompletion___spec__6___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Server_FileWorker_leanpkgSetupSearchPath___closed__5;
@ -80,6 +80,7 @@ lean_object* l___private_Lean_Data_Lsp_Extra_0__Lean_Lsp_fromJsonPlainGoalParams
lean_object* l_IO_FS_Stream_writeLspResponse___at_Lean_Server_FileWorker_handleRequest___spec__7(lean_object*, lean_object*, lean_object*);
lean_object* l_List_map___at_Lean_Server_FileWorker_handleDocumentSymbol___spec__1(lean_object*);
lean_object* l_Array_append___rarg(lean_object*, lean_object*);
lean_object* l_Std_PersistentArray_forInAux___at_Lean_Server_FileWorker_handleDefinition___spec__5(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_forInUnsafe_loop___at_Lean_Server_FileWorker_handlePlainGoal___spec__7(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Server_FileWorker_handleWaitForDiagnostics___lambda__3___closed__6;
lean_object* l_String_split___at_Lean_stringToMessageData___spec__1(lean_object*);
@ -93,8 +94,10 @@ lean_object* l_Lean_Server_FileWorker_RequestError_fileChanged___closed__1;
extern lean_object* l_Lean_Parser_Command_namedPrio___elambda__1___closed__2;
lean_object* l_Lean_Server_FileWorker_handleDocumentHighlight___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_Lsp_instFromJsonDiagnosticSeverity___closed__4;
lean_object* l_Std_PersistentArray_forInAux___at_Lean_Server_FileWorker_handleDefinition___spec__5___boxed(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_Server_FileWorker_parseParams___at_Lean_Server_FileWorker_handleNotification___spec__2___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Server_FileWorker_handleDocumentSymbol_toDocumentSymbols___lambda__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_findDeclarationRangesCore_x3f___at_Lean_Server_FileWorker_handleDefinition___spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Server_FileWorker_handleSemanticTokens_highlightId_match__2(lean_object*);
lean_object* lean_array_uset(lean_object*, size_t, lean_object*);
extern lean_object* l_Lean_Lsp_Ipc_collectDiagnostics___closed__1;
@ -231,7 +234,7 @@ extern lean_object* l_Lean_Elab_parseImports___closed__1;
extern lean_object* l_Lean_LocalContext_mkEmpty___closed__1;
lean_object* l_IO_AsyncList_waitAll___rarg___lambda__1(lean_object*, lean_object*);
lean_object* l_Std_PersistentArray_forIn___at_Lean_Server_FileWorker_handleCompletion___spec__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_forInUnsafe_loop___at_Lean_Server_FileWorker_handleDefinition___spec__7___boxed(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*);
lean_object* l_Array_forInUnsafe_loop___at_Lean_Server_FileWorker_handleDefinition___spec__7___boxed(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_Server_FileWorker_initAndRunWorker___closed__2;
lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Server_FileWorker_0__Lean_Server_FileWorker_nextCmdSnap___spec__11(lean_object*, size_t, size_t, lean_object*, lean_object*);
lean_object* l_Lean_Server_FileWorker_withWaitFindSnap(lean_object*);
@ -255,11 +258,9 @@ extern lean_object* l_Lean_maxRecDepth;
lean_object* l_Lean_Server_FileWorker_compileHeader(lean_object*, lean_object*, lean_object*);
lean_object* lean_io_bind_task(lean_object*, lean_object*, lean_object*, lean_object*);
uint8_t l_Lean_Server_FileWorker_handleWaitForDiagnostics___lambda__1(lean_object*);
lean_object* l_Lean_findDeclarationRangesCore_x3f___at_Lean_Server_FileWorker_handleDefinition___spec__4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Server_FileWorker_handleRequest_match__2___rarg___closed__9;
extern lean_object* l_Lean_JsonRpc_instToJsonMessage___closed__10;
lean_object* l_Lean_Server_FileWorker_queueRequest___lambda__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Std_PersistentArray_forIn___at_Lean_Server_FileWorker_handleDefinition___spec__5___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_JsonRpc_instToJsonMessage___closed__5;
lean_object* l_Lean_Server_FileWorker_handleRequest_match__2___rarg___closed__8;
lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Server_FileWorker_0__Lean_Server_FileWorker_nextCmdSnap___spec__4(lean_object*, size_t, size_t, lean_object*, lean_object*);
@ -268,7 +269,6 @@ lean_object* l_Lean_Server_FileWorker_updateDocument_match__1___rarg(lean_object
lean_object* l_Lean_Server_FileWorker_initAndRunWorker_match__3___rarg(lean_object*, lean_object*);
lean_object* l_Lean_Server_FileWorker_handleNotification___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Server_FileWorker_instInhabitedEditableDocument___closed__4;
lean_object* l_Lean_isRec___at_Lean_Server_FileWorker_handleDefinition___spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Server_FileWorker_handleWaitForDiagnostics___lambda__3___closed__4;
lean_object* l_Lean_Json_toStructured_x3f___at___private_Lean_Server_FileWorker_0__Lean_Server_FileWorker_nextCmdSnap___spec__8(lean_object*);
lean_object* l_IO_getStdin___at_Lean_Server_FileWorker_workerMain___spec__1(lean_object*);
@ -277,7 +277,6 @@ lean_object* l_Lean_Server_FileWorker_handleWaitForDiagnostics_waitLoop(lean_obj
lean_object* l_Lean_Server_FileWorker_handleRequest___lambda__5(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Std_PersistentArray_mapM___at___private_Lean_Server_FileWorker_0__Lean_Server_FileWorker_nextCmdSnap___spec__9___boxed__const__1;
lean_object* l_Lean_Server_FileWorker_compileHeader___closed__2;
lean_object* l_Std_PersistentArray_forIn___at_Lean_Server_FileWorker_handleDefinition___spec__5(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Server_FileWorker_handleDocumentHighlight(lean_object*, lean_object*, lean_object*);
lean_object* l_Std_RBNode_setBlack___rarg(lean_object*);
extern lean_object* l___private_Lean_Data_Lsp_InitShutdown_0__Lean_Lsp_toJsonInitializeParams____x40_Lean_Data_Lsp_InitShutdown___hyg_222____closed__3;
@ -336,6 +335,7 @@ lean_object* l_Lean_Server_Snapshots_reparseHeader(lean_object*, lean_object*, l
lean_object* l_List_mapM___at_Lean_Server_FileWorker_handlePlainGoal___spec__4___closed__1;
extern lean_object* l_Lean_JsonRpc_instToJsonMessage___closed__7;
lean_object* l_List_mapM___at_Lean_Server_FileWorker_leanpkgSetupSearchPath___spec__2(lean_object*, lean_object*);
lean_object* l_Lean_findDeclarationRangesCore_x3f___at_Lean_Server_FileWorker_handleDefinition___spec__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Server_FileWorker_0__Lean_Server_FileWorker_nextCmdSnap___spec__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_IO_AsyncList_append___rarg(lean_object*, lean_object*);
lean_object* l_Lean_Server_FileWorker_handlePlainGoal_match__2___rarg(lean_object*, lean_object*, lean_object*);
@ -355,6 +355,7 @@ lean_object* l_Lean_Server_FileWorker_handleSemanticTokensFull___rarg___boxed(le
lean_object* l_Lean_Server_FileWorker_instInhabitedEditableDocument___closed__3;
lean_object* l_ST_Prim_Ref_get___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
extern uint8_t l_Lean_expandExternPatternAux___closed__2;
lean_object* l_Array_forInUnsafe_loop___at_Lean_Server_FileWorker_handleDefinition___spec__7___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Server_FileWorker_handleNotification_match__1___rarg___closed__1;
lean_object* l_Lean_Server_FileWorker_handleDefinition___closed__2;
lean_object* l_Lean_Server_FileWorker_unfoldCmdSnaps___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -382,7 +383,7 @@ extern lean_object* l_Lean_Lsp_Ipc_collectDiagnostics_loop_match__2___rarg___clo
lean_object* l_Lean_Server_FileWorker_handleWaitForDiagnostics___lambda__3___closed__5;
lean_object* l_Lean_Server_FileWorker_initAndRunWorker___boxed__const__1;
lean_object* l_Lean_Server_FileWorker_handleSemanticTokens_highlightId_match__3___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Array_forInUnsafe_loop___at_Lean_Server_FileWorker_handleDefinition___spec__7(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_forInUnsafe_loop___at_Lean_Server_FileWorker_handleDefinition___spec__7(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*);
lean_object* lean_task_map(lean_object*, lean_object*, lean_object*);
lean_object* l_Nat_repr(lean_object*);
lean_object* l_List_getLast_x21___at_Lean_Server_FileWorker_handleDocumentSymbol_sectionLikeToDocumentSymbols___spec__1(lean_object*);
@ -399,10 +400,10 @@ lean_object* l_IO_FS_Stream_readNotificationAs___at_Lean_Server_FileWorker_initA
lean_object* l_IO_FS_Stream_writeLspResponse___at_Lean_Server_FileWorker_handleRequest___spec__19___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Syntax_getId(lean_object*);
lean_object* l_Lean_Server_FileWorker_updateDocument___lambda__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_forInUnsafe_loop___at_Lean_Server_FileWorker_handleDefinition___spec__8___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_format_pretty(lean_object*, lean_object*);
lean_object* l_Lean_Server_FileWorker_updateDocument___lambda__3___closed__1;
extern lean_object* l_Lean_choiceKind;
lean_object* l_Array_forInUnsafe_loop___at_Lean_Server_FileWorker_handleDefinition___spec__7___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Server_FileWorker_queueRequest___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Server_FileWorker_compileHeader___lambda__1___closed__3;
lean_object* l_Lean_Server_FileWorker_handleWaitForDiagnostics___lambda__3___closed__2;
@ -489,6 +490,7 @@ extern lean_object* l_Lean_Lsp_instToJsonWaitForDiagnostics___closed__1;
extern lean_object* l___private_Lean_Data_Lsp_InitShutdown_0__Lean_Lsp_toJsonInitializeParams____x40_Lean_Data_Lsp_InitShutdown___hyg_222____closed__1;
lean_object* l_Lean_Server_FileWorker_mainLoop(lean_object*, lean_object*);
lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonCompletionParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_302_(lean_object*);
lean_object* l_Std_PersistentArray_forIn___at_Lean_Server_FileWorker_handleDefinition___spec__4(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Task_Priority_default;
lean_object* lean_io_has_finished(lean_object*, lean_object*);
lean_object* l_Array_mapMUnsafe_map___at___private_Lean_Server_FileWorker_0__Lean_Server_FileWorker_nextCmdSnap___spec__11___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -496,6 +498,7 @@ lean_object* l_Lean_Server_FileWorker_handleDocumentSymbol_sectionLikeToDocument
lean_object* l_Lean_Server_FileWorker_rangeOfSyntax(lean_object*, lean_object*);
lean_object* l_List_mapM___at_Lean_Server_FileWorker_handlePlainGoal___spec__4(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Server_FileWorker_handleDocumentSymbol_toDocumentSymbols___lambda__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_isRec___at___private_Lean_Server_Completion_0__Lean_Server_Completion_isBlackListed___spec__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
size_t lean_usize_of_nat(lean_object*);
extern lean_object* l_Lean_nullKind___closed__1;
lean_object* l_IO_AsyncList_waitFind_x3f___at_Lean_Server_FileWorker_withWaitFindSnap___spec__1___lambda__1(lean_object*, lean_object*, lean_object*);
@ -508,9 +511,7 @@ lean_object* l_Lean_Json_getObjValAs_x3f___at_Lean_Lsp_instFromJsonInitializePar
lean_object* l_Lean_Server_FileWorker_handleDocumentSymbol_match__1(lean_object*);
extern lean_object* l_Lean_Parser_Term_doReturn___elambda__1___closed__2;
lean_object* l_Array_forInUnsafe_loop___at_Lean_Server_FileWorker_handleCompletion___spec__5___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Std_PersistentArray_forInAux___at_Lean_Server_FileWorker_handleDefinition___spec__6___boxed(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_Std_PersistentArray_forIn___at_Lean_Server_FileWorker_handlePlainGoal___spec__5(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_forInUnsafe_loop___at_Lean_Server_FileWorker_handleDefinition___spec__9(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Server_AsyncList_0__IO_AsyncList_coeErr___at_Lean_Server_FileWorker_unfoldCmdSnaps___spec__3___lambda__1(lean_object*);
lean_object* l_Lean_Server_FileWorker_handleNotification_match__1(lean_object*);
lean_object* l_IO_mkRef___at_Lean_Server_FileWorker_CancelToken_new___spec__1(uint8_t, lean_object*);
@ -596,6 +597,7 @@ lean_object* l_Lean_Server_FileWorker_handleWaitForDiagnostics___lambda__3___clo
lean_object* l_Std_PersistentArray_forInAux___at_Lean_Server_FileWorker_handleSemanticTokens_highlightId___spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Server_FileWorker_handleRequest_match__2___rarg___closed__2;
extern lean_object* l_Lean_myMacro____x40_Init_NotationExtra___hyg_1139____closed__7;
lean_object* l_Array_forInUnsafe_loop___at_Lean_Server_FileWorker_handleDefinition___spec__7___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Server_FileWorker_handleCompletion_match__2___rarg(lean_object*, lean_object*, lean_object*);
uint8_t l_Std_RBNode_isRed___rarg(lean_object*);
lean_object* l_Lean_Server_FileWorker_handleSemanticTokens___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -624,7 +626,6 @@ lean_object* l_Lean_addSearchPathFromEnv(lean_object*, lean_object*);
lean_object* l_Array_forInUnsafe_loop___at_Lean_Server_FileWorker_handlePlainGoal___spec__9(lean_object*, lean_object*, lean_object*, lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_forInUnsafe_loop___at_Lean_Server_FileWorker_handleSemanticTokens_highlightId___spec__5___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* lean_get_stdout(lean_object*);
lean_object* l_Array_forInUnsafe_loop___at_Lean_Server_FileWorker_handleDefinition___spec__8___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Server_FileWorker_handleDocumentSymbol_sectionLikeToDocumentSymbols(lean_object*, lean_object*, lean_object*, lean_object*, uint8_t, lean_object*);
lean_object* l_Lean_Server_FileWorker_updateDocument(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Server_FileWorker_0__Lean_Server_FileWorker_nextCmdSnap___closed__3;
@ -632,7 +633,6 @@ lean_object* l_Lean_findDeclarationRanges_x3f___at_Lean_Server_FileWorker_handle
lean_object* l_Std_PersistentArray_forInAux___at_Lean_Server_FileWorker_handleSemanticTokens_highlightId___spec__3___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Data_Lsp_Communication_0__IO_FS_Stream_readLspHeader(lean_object*, lean_object*);
lean_object* l_Lean_Server_FileWorker_updateDocument_match__2___rarg(lean_object*, lean_object*);
lean_object* l_Array_forInUnsafe_loop___at_Lean_Server_FileWorker_handleDefinition___spec__8___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_JsonRpc_instToJsonErrorCode___closed__4;
lean_object* l_Lean_Server_FileWorker_handleSemanticTokens_highlightId_match__1(lean_object*);
extern lean_object* l_Lean_JsonRpc_instToJsonErrorCode___closed__40;
@ -640,7 +640,6 @@ lean_object* l_Lean_Server_FileWorker_leanpkgSetupSearchPath___closed__6;
lean_object* l_Array_forInUnsafe_loop___at_Lean_Server_FileWorker_handleDocumentHighlight_highlightReturn_x3f___spec__3___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Server_FileWorker_parseParams___at_Lean_Server_FileWorker_handleRequest___spec__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_findDeclarationRanges_x3f___at_Lean_Server_FileWorker_handleDefinition___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_isRec___at_Lean_Server_FileWorker_handleDefinition___spec__3(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Std_PersistentArray_forInAux___at_Lean_Server_FileWorker_handleHover___spec__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Server_FileWorker_handleDocumentSymbol_toDocumentSymbols___lambda__2(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Server_FileWorker_parseParams___at_Lean_Server_FileWorker_handleRequest___spec__1___boxed(lean_object*, lean_object*, lean_object*);
@ -728,15 +727,12 @@ lean_object* l_Lean_Server_FileWorker_handleRequest_match__2___rarg___closed__5;
lean_object* l_Lean_Server_FileWorker_handleSemanticTokens(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Server_FileWorker_handleWaitForDiagnostics(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Server_FileWorker_updatePendingRequests(lean_object*, lean_object*, lean_object*);
lean_object* l_Array_forInUnsafe_loop___at_Lean_Server_FileWorker_handleDefinition___spec__8___lambda__2___closed__1;
lean_object* l_Lean_Server_FileWorker_handleSemanticTokens_highlightId_match__2___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_IO_FS_Stream_writeLspResponse___at_Lean_Server_FileWorker_handleRequest___spec__17(lean_object*, lean_object*, lean_object*);
lean_object* l_Array_forInUnsafe_loop___at_Lean_Server_FileWorker_handleDefinition___spec__8___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Server_FileWorker_handleWaitForDiagnostics___lambda__4(lean_object*);
lean_object* l_Lean_Server_FileWorker_handleHover_match__3(lean_object*);
lean_object* l_ReaderT_pure___at_Lean_Server_FileWorker_handleCompletion___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Server_FileWorker_unfoldCmdSnaps(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Std_PersistentArray_forInAux___at_Lean_Server_FileWorker_handleDefinition___spec__6(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_forInUnsafe_loop___at_Lean_Server_FileWorker_handleHover___spec__4(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Server_FileWorker_handleHover___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Server_FileWorker_CancelToken_set(lean_object*, lean_object*);
@ -755,7 +751,6 @@ lean_object* l_Lean_Server_FileWorker_handleSemanticTokens___lambda__2___closed_
lean_object* l_Lean_Server_FileWorker_parseParams___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Elab_Info_pos_x3f(lean_object*);
lean_object* l_Lean_Server_FileWorker_handleNotification_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_findDeclarationRangesCore_x3f___at_Lean_Server_FileWorker_handleDefinition___spec__4___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_ReaderT_pure___at_Lean_Server_FileWorker_handleCompletion___spec__1(lean_object*);
extern lean_object* l_IO_instInhabitedError;
lean_object* l_Lean_Server_FileWorker_handleDocumentSymbol___rarg(lean_object*, lean_object*);
@ -774,13 +769,17 @@ extern lean_object* l_System_FilePath_exeSuffix;
uint8_t l_List_isEmpty___rarg(lean_object*);
lean_object* l_List_lengthAux___rarg(lean_object*, lean_object*);
lean_object* l_Lean_Server_FileWorker_handleWaitForDiagnostics_waitLoop___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Array_forInUnsafe_loop___at_Lean_Server_FileWorker_handleDefinition___spec__6(uint8_t, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Server_FileWorker_handlePlainGoal_match__3(lean_object*);
lean_object* l_Lean_Server_FileWorker_handleDocumentSymbol_toDocumentSymbols___closed__2;
lean_object* l___private_Lean_Data_Lsp_TextSync_0__Lean_Lsp_fromJsonDidChangeTextDocumentParams____x40_Lean_Data_Lsp_TextSync___hyg_309_(lean_object*);
lean_object* l_Lean_Server_FileWorker_handlePlainGoal___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_JsonRpc_instToJsonErrorCode___closed__12;
extern lean_object* l___private_Lean_Data_Lsp_Basic_0__Lean_Lsp_toJsonRange____x40_Lean_Data_Lsp_Basic___hyg_361____closed__1;
lean_object* l_Array_forInUnsafe_loop___at_Lean_Server_FileWorker_handleDefinition___spec__7___lambda__2___closed__1;
lean_object* l_Lean_Server_FileWorker_withWaitFindSnap___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_forInUnsafe_loop___at_Lean_Server_FileWorker_handleDefinition___spec__7___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_forInUnsafe_loop___at_Lean_Server_FileWorker_handleDefinition___spec__6___boxed(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*);
lean_object* l_Lean_Server_FileWorker_handleDocumentSymbol_sectionLikeToDocumentSymbols_match__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_List_getLast_x21___at_Lean_Server_FileWorker_updateDocument___spec__1(lean_object*);
lean_object* l_Lean_Server_FileWorker_workerMain___boxed__const__1;
@ -836,7 +835,6 @@ lean_object* l_Lean_Server_FileWorker_handleDefinition_match__4___rarg(lean_obje
lean_object* l_Lean_Server_Snapshots_compileNextCmd(lean_object*, lean_object*, lean_object*);
lean_object* l_List_forIn_loop___at_Lean_Server_FileWorker_handleSemanticTokens___spec__2___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_term_x5b___x5d___closed__3;
lean_object* l_Array_forInUnsafe_loop___at_Lean_Server_FileWorker_handleDefinition___spec__9___boxed(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_findModuleOf_x3f___at_Lean_Server_FileWorker_handleDefinition___spec__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Std_PersistentArray_mapM___at___private_Lean_Server_FileWorker_0__Lean_Server_FileWorker_nextCmdSnap___spec__9(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Server_FileWorker_handleRequest_match__2___rarg(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*);
@ -14314,45 +14312,7 @@ return x_64;
}
}
}
lean_object* l_Lean_isRec___at_Lean_Server_FileWorker_handleDefinition___spec__3(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
_start:
{
lean_object* x_7; uint8_t x_8;
x_7 = lean_st_ref_get(x_5, x_6);
x_8 = !lean_is_exclusive(x_7);
if (x_8 == 0)
{
lean_object* x_9; lean_object* x_10; uint8_t x_11; lean_object* x_12;
x_9 = lean_ctor_get(x_7, 0);
x_10 = lean_ctor_get(x_9, 0);
lean_inc(x_10);
lean_dec(x_9);
x_11 = l_Lean_isRecCore(x_10, x_1);
x_12 = lean_box(x_11);
lean_ctor_set(x_7, 0, x_12);
return x_7;
}
else
{
lean_object* x_13; lean_object* x_14; lean_object* x_15; uint8_t x_16; lean_object* x_17; lean_object* x_18;
x_13 = lean_ctor_get(x_7, 0);
x_14 = lean_ctor_get(x_7, 1);
lean_inc(x_14);
lean_inc(x_13);
lean_dec(x_7);
x_15 = lean_ctor_get(x_13, 0);
lean_inc(x_15);
lean_dec(x_13);
x_16 = l_Lean_isRecCore(x_15, x_1);
x_17 = lean_box(x_16);
x_18 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_18, 0, x_17);
lean_ctor_set(x_18, 1, x_14);
return x_18;
}
}
}
lean_object* l_Lean_findDeclarationRangesCore_x3f___at_Lean_Server_FileWorker_handleDefinition___spec__4(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
lean_object* l_Lean_findDeclarationRangesCore_x3f___at_Lean_Server_FileWorker_handleDefinition___spec__3(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
_start:
{
lean_object* x_7; uint8_t x_8;
@ -14406,7 +14366,7 @@ x_10 = lean_ctor_get(x_8, 0);
lean_inc(x_10);
lean_dec(x_8);
lean_inc(x_1);
x_11 = l_Lean_isRec___at_Lean_Server_FileWorker_handleDefinition___spec__3(x_1, x_2, x_3, x_4, x_5, x_9);
x_11 = l_Lean_isRec___at___private_Lean_Server_Completion_0__Lean_Server_Completion_isBlackListed___spec__1(x_1, x_2, x_3, x_4, x_5, x_9);
x_12 = lean_ctor_get(x_11, 0);
lean_inc(x_12);
x_13 = lean_ctor_get(x_11, 1);
@ -14428,7 +14388,7 @@ lean_dec(x_12);
if (x_18 == 0)
{
lean_object* x_19;
x_19 = l_Lean_findDeclarationRangesCore_x3f___at_Lean_Server_FileWorker_handleDefinition___spec__4(x_1, x_2, x_3, x_4, x_5, x_13);
x_19 = l_Lean_findDeclarationRangesCore_x3f___at_Lean_Server_FileWorker_handleDefinition___spec__3(x_1, x_2, x_3, x_4, x_5, x_13);
return x_19;
}
else
@ -14436,7 +14396,7 @@ else
lean_object* x_20; lean_object* x_21;
x_20 = l_Lean_Name_getPrefix(x_1);
lean_dec(x_1);
x_21 = l_Lean_findDeclarationRangesCore_x3f___at_Lean_Server_FileWorker_handleDefinition___spec__4(x_20, x_2, x_3, x_4, x_5, x_13);
x_21 = l_Lean_findDeclarationRangesCore_x3f___at_Lean_Server_FileWorker_handleDefinition___spec__3(x_20, x_2, x_3, x_4, x_5, x_13);
return x_21;
}
}
@ -14446,7 +14406,7 @@ lean_object* x_22; lean_object* x_23;
lean_dec(x_12);
x_22 = l_Lean_Name_getPrefix(x_1);
lean_dec(x_1);
x_23 = l_Lean_findDeclarationRangesCore_x3f___at_Lean_Server_FileWorker_handleDefinition___spec__4(x_22, x_2, x_3, x_4, x_5, x_13);
x_23 = l_Lean_findDeclarationRangesCore_x3f___at_Lean_Server_FileWorker_handleDefinition___spec__3(x_22, x_2, x_3, x_4, x_5, x_13);
return x_23;
}
}
@ -14457,12 +14417,12 @@ lean_dec(x_12);
lean_dec(x_10);
x_24 = l_Lean_Name_getPrefix(x_1);
lean_dec(x_1);
x_25 = l_Lean_findDeclarationRangesCore_x3f___at_Lean_Server_FileWorker_handleDefinition___spec__4(x_24, x_2, x_3, x_4, x_5, x_13);
x_25 = l_Lean_findDeclarationRangesCore_x3f___at_Lean_Server_FileWorker_handleDefinition___spec__3(x_24, x_2, x_3, x_4, x_5, x_13);
return x_25;
}
}
}
lean_object* l_Array_forInUnsafe_loop___at_Lean_Server_FileWorker_handleDefinition___spec__7(uint8_t x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, size_t x_10, size_t x_11, lean_object* x_12, lean_object* x_13, lean_object* x_14) {
lean_object* l_Array_forInUnsafe_loop___at_Lean_Server_FileWorker_handleDefinition___spec__6(uint8_t x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, size_t x_10, size_t x_11, lean_object* x_12, lean_object* x_13, lean_object* x_14) {
_start:
{
lean_object* x_15; lean_object* x_16; uint8_t x_39;
@ -14489,7 +14449,7 @@ lean_inc(x_43);
lean_dec(x_12);
lean_inc(x_6);
lean_inc(x_5);
x_44 = l_Std_PersistentArray_forInAux___at_Lean_Server_FileWorker_handleDefinition___spec__6(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_42, x_43, x_13, x_14);
x_44 = l_Std_PersistentArray_forInAux___at_Lean_Server_FileWorker_handleDefinition___spec__5(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_42, x_43, x_13, x_14);
lean_dec(x_42);
if (lean_obj_tag(x_44) == 0)
{
@ -14785,7 +14745,7 @@ goto _start;
}
}
}
lean_object* l_Array_forInUnsafe_loop___at_Lean_Server_FileWorker_handleDefinition___spec__8___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9) {
lean_object* l_Array_forInUnsafe_loop___at_Lean_Server_FileWorker_handleDefinition___spec__7___lambda__1(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9) {
_start:
{
lean_object* x_10; lean_object* x_11;
@ -15152,7 +15112,7 @@ return x_115;
}
}
}
static lean_object* _init_l_Array_forInUnsafe_loop___at_Lean_Server_FileWorker_handleDefinition___spec__8___lambda__2___closed__1() {
static lean_object* _init_l_Array_forInUnsafe_loop___at_Lean_Server_FileWorker_handleDefinition___spec__7___lambda__2___closed__1() {
_start:
{
lean_object* x_1;
@ -15160,7 +15120,7 @@ x_1 = lean_mk_string(".lean");
return x_1;
}
}
lean_object* l_Array_forInUnsafe_loop___at_Lean_Server_FileWorker_handleDefinition___spec__8___lambda__2(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9) {
lean_object* l_Array_forInUnsafe_loop___at_Lean_Server_FileWorker_handleDefinition___spec__7___lambda__2(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9) {
_start:
{
lean_object* x_10;
@ -15207,7 +15167,7 @@ lean_dec(x_18);
x_21 = lean_ctor_get(x_5, 0);
lean_inc(x_21);
lean_ctor_set(x_10, 0, x_21);
x_22 = l_Array_forInUnsafe_loop___at_Lean_Server_FileWorker_handleDefinition___spec__8___lambda__1(x_15, x_3, x_16, x_1, x_2, x_4, x_10, x_8, x_20);
x_22 = l_Array_forInUnsafe_loop___at_Lean_Server_FileWorker_handleDefinition___spec__7___lambda__1(x_15, x_3, x_16, x_1, x_2, x_4, x_10, x_8, x_20);
lean_dec(x_2);
return x_22;
}
@ -15222,7 +15182,7 @@ x_24 = lean_ctor_get(x_19, 0);
lean_inc(x_24);
lean_dec(x_19);
x_25 = lean_ctor_get(x_6, 3);
x_26 = l_Array_forInUnsafe_loop___at_Lean_Server_FileWorker_handleDefinition___spec__8___lambda__2___closed__1;
x_26 = l_Array_forInUnsafe_loop___at_Lean_Server_FileWorker_handleDefinition___spec__7___lambda__2___closed__1;
x_27 = l_Lean_SearchPath_findWithExt(x_25, x_26, x_24, x_23);
lean_dec(x_24);
if (lean_obj_tag(x_27) == 0)
@ -15237,7 +15197,7 @@ x_29 = lean_ctor_get(x_27, 1);
lean_inc(x_29);
lean_dec(x_27);
x_30 = lean_box(0);
x_31 = l_Array_forInUnsafe_loop___at_Lean_Server_FileWorker_handleDefinition___spec__8___lambda__1(x_15, x_3, x_16, x_1, x_2, x_4, x_30, x_8, x_29);
x_31 = l_Array_forInUnsafe_loop___at_Lean_Server_FileWorker_handleDefinition___spec__7___lambda__1(x_15, x_3, x_16, x_1, x_2, x_4, x_30, x_8, x_29);
lean_dec(x_2);
return x_31;
}
@ -15254,7 +15214,7 @@ lean_object* x_34; lean_object* x_35; lean_object* x_36;
x_34 = lean_ctor_get(x_28, 0);
x_35 = l_Lean_Server_toFileUri(x_34);
lean_ctor_set(x_28, 0, x_35);
x_36 = l_Array_forInUnsafe_loop___at_Lean_Server_FileWorker_handleDefinition___spec__8___lambda__1(x_15, x_3, x_16, x_1, x_2, x_4, x_28, x_8, x_32);
x_36 = l_Array_forInUnsafe_loop___at_Lean_Server_FileWorker_handleDefinition___spec__7___lambda__1(x_15, x_3, x_16, x_1, x_2, x_4, x_28, x_8, x_32);
lean_dec(x_2);
return x_36;
}
@ -15267,7 +15227,7 @@ lean_dec(x_28);
x_38 = l_Lean_Server_toFileUri(x_37);
x_39 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_39, 0, x_38);
x_40 = l_Array_forInUnsafe_loop___at_Lean_Server_FileWorker_handleDefinition___spec__8___lambda__1(x_15, x_3, x_16, x_1, x_2, x_4, x_39, x_8, x_32);
x_40 = l_Array_forInUnsafe_loop___at_Lean_Server_FileWorker_handleDefinition___spec__7___lambda__1(x_15, x_3, x_16, x_1, x_2, x_4, x_39, x_8, x_32);
lean_dec(x_2);
return x_40;
}
@ -15357,7 +15317,7 @@ x_55 = lean_ctor_get(x_5, 0);
lean_inc(x_55);
x_56 = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(x_56, 0, x_55);
x_57 = l_Array_forInUnsafe_loop___at_Lean_Server_FileWorker_handleDefinition___spec__8___lambda__1(x_49, x_3, x_50, x_1, x_2, x_4, x_56, x_8, x_54);
x_57 = l_Array_forInUnsafe_loop___at_Lean_Server_FileWorker_handleDefinition___spec__7___lambda__1(x_49, x_3, x_50, x_1, x_2, x_4, x_56, x_8, x_54);
lean_dec(x_2);
return x_57;
}
@ -15371,7 +15331,7 @@ x_59 = lean_ctor_get(x_53, 0);
lean_inc(x_59);
lean_dec(x_53);
x_60 = lean_ctor_get(x_6, 3);
x_61 = l_Array_forInUnsafe_loop___at_Lean_Server_FileWorker_handleDefinition___spec__8___lambda__2___closed__1;
x_61 = l_Array_forInUnsafe_loop___at_Lean_Server_FileWorker_handleDefinition___spec__7___lambda__2___closed__1;
x_62 = l_Lean_SearchPath_findWithExt(x_60, x_61, x_59, x_58);
lean_dec(x_59);
if (lean_obj_tag(x_62) == 0)
@ -15386,7 +15346,7 @@ x_64 = lean_ctor_get(x_62, 1);
lean_inc(x_64);
lean_dec(x_62);
x_65 = lean_box(0);
x_66 = l_Array_forInUnsafe_loop___at_Lean_Server_FileWorker_handleDefinition___spec__8___lambda__1(x_49, x_3, x_50, x_1, x_2, x_4, x_65, x_8, x_64);
x_66 = l_Array_forInUnsafe_loop___at_Lean_Server_FileWorker_handleDefinition___spec__7___lambda__1(x_49, x_3, x_50, x_1, x_2, x_4, x_65, x_8, x_64);
lean_dec(x_2);
return x_66;
}
@ -15412,7 +15372,7 @@ if (lean_is_scalar(x_69)) {
x_71 = x_69;
}
lean_ctor_set(x_71, 0, x_70);
x_72 = l_Array_forInUnsafe_loop___at_Lean_Server_FileWorker_handleDefinition___spec__8___lambda__1(x_49, x_3, x_50, x_1, x_2, x_4, x_71, x_8, x_67);
x_72 = l_Array_forInUnsafe_loop___at_Lean_Server_FileWorker_handleDefinition___spec__7___lambda__1(x_49, x_3, x_50, x_1, x_2, x_4, x_71, x_8, x_67);
lean_dec(x_2);
return x_72;
}
@ -15479,7 +15439,7 @@ return x_80;
}
}
}
lean_object* l_Array_forInUnsafe_loop___at_Lean_Server_FileWorker_handleDefinition___spec__8(uint8_t x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, size_t x_9, size_t x_10, lean_object* x_11, lean_object* x_12, lean_object* x_13) {
lean_object* l_Array_forInUnsafe_loop___at_Lean_Server_FileWorker_handleDefinition___spec__7(uint8_t x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, size_t x_9, size_t x_10, lean_object* x_11, lean_object* x_12, lean_object* x_13) {
_start:
{
lean_object* x_14; lean_object* x_15; lean_object* x_38; lean_object* x_39; uint8_t x_67;
@ -15538,7 +15498,7 @@ lean_dec(x_75);
x_78 = lean_ctor_get(x_77, 1);
lean_inc(x_78);
lean_inc(x_6);
x_79 = l_Array_forInUnsafe_loop___at_Lean_Server_FileWorker_handleDefinition___spec__8___lambda__2(x_6, x_77, x_76, x_4, x_3, x_2, x_78, x_12, x_13);
x_79 = l_Array_forInUnsafe_loop___at_Lean_Server_FileWorker_handleDefinition___spec__7___lambda__2(x_6, x_77, x_76, x_4, x_3, x_2, x_78, x_12, x_13);
lean_dec(x_78);
lean_dec(x_76);
if (lean_obj_tag(x_79) == 0)
@ -15604,7 +15564,7 @@ x_93 = lean_ctor_get(x_91, 1);
lean_inc(x_93);
lean_dec(x_91);
lean_inc(x_6);
x_94 = l_Array_forInUnsafe_loop___at_Lean_Server_FileWorker_handleDefinition___spec__8___lambda__2(x_6, x_87, x_86, x_4, x_3, x_2, x_92, x_12, x_93);
x_94 = l_Array_forInUnsafe_loop___at_Lean_Server_FileWorker_handleDefinition___spec__7___lambda__2(x_6, x_87, x_86, x_4, x_3, x_2, x_92, x_12, x_93);
lean_dec(x_92);
lean_dec(x_86);
if (lean_obj_tag(x_94) == 0)
@ -15940,7 +15900,7 @@ goto block_37;
}
}
}
lean_object* l_Std_PersistentArray_forInAux___at_Lean_Server_FileWorker_handleDefinition___spec__6(uint8_t x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10, lean_object* x_11) {
lean_object* l_Std_PersistentArray_forInAux___at_Lean_Server_FileWorker_handleDefinition___spec__5(uint8_t x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10, lean_object* x_11) {
_start:
{
if (lean_obj_tag(x_8) == 0)
@ -15955,7 +15915,7 @@ x_15 = lean_array_get_size(x_12);
x_16 = lean_usize_of_nat(x_15);
lean_dec(x_15);
x_17 = 0;
x_18 = l_Array_forInUnsafe_loop___at_Lean_Server_FileWorker_handleDefinition___spec__7(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_13, x_12, x_16, x_17, x_14, x_10, x_11);
x_18 = l_Array_forInUnsafe_loop___at_Lean_Server_FileWorker_handleDefinition___spec__6(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_13, x_12, x_16, x_17, x_14, x_10, x_11);
if (lean_obj_tag(x_18) == 0)
{
lean_object* x_19;
@ -16158,7 +16118,7 @@ x_61 = lean_array_get_size(x_58);
x_62 = lean_usize_of_nat(x_61);
lean_dec(x_61);
x_63 = 0;
x_64 = l_Array_forInUnsafe_loop___at_Lean_Server_FileWorker_handleDefinition___spec__8(x_1, x_2, x_3, x_4, x_5, x_6, x_59, x_58, x_62, x_63, x_60, x_10, x_11);
x_64 = l_Array_forInUnsafe_loop___at_Lean_Server_FileWorker_handleDefinition___spec__7(x_1, x_2, x_3, x_4, x_5, x_6, x_59, x_58, x_62, x_63, x_60, x_10, x_11);
if (lean_obj_tag(x_64) == 0)
{
lean_object* x_65;
@ -16351,7 +16311,7 @@ return x_103;
}
}
}
lean_object* l_Array_forInUnsafe_loop___at_Lean_Server_FileWorker_handleDefinition___spec__9(uint8_t x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, size_t x_9, size_t x_10, lean_object* x_11, lean_object* x_12, lean_object* x_13) {
lean_object* l_Array_forInUnsafe_loop___at_Lean_Server_FileWorker_handleDefinition___spec__8(uint8_t x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, size_t x_9, size_t x_10, lean_object* x_11, lean_object* x_12, lean_object* x_13) {
_start:
{
lean_object* x_14; lean_object* x_15; lean_object* x_38; lean_object* x_39; uint8_t x_72;
@ -16410,7 +16370,7 @@ lean_dec(x_80);
x_83 = lean_ctor_get(x_82, 1);
lean_inc(x_83);
lean_inc(x_6);
x_84 = l_Array_forInUnsafe_loop___at_Lean_Server_FileWorker_handleDefinition___spec__8___lambda__2(x_6, x_82, x_81, x_4, x_3, x_2, x_83, x_12, x_13);
x_84 = l_Array_forInUnsafe_loop___at_Lean_Server_FileWorker_handleDefinition___spec__7___lambda__2(x_6, x_82, x_81, x_4, x_3, x_2, x_83, x_12, x_13);
lean_dec(x_83);
lean_dec(x_81);
if (lean_obj_tag(x_84) == 0)
@ -16476,7 +16436,7 @@ x_98 = lean_ctor_get(x_96, 1);
lean_inc(x_98);
lean_dec(x_96);
lean_inc(x_6);
x_99 = l_Array_forInUnsafe_loop___at_Lean_Server_FileWorker_handleDefinition___spec__8___lambda__2(x_6, x_92, x_91, x_4, x_3, x_2, x_97, x_12, x_98);
x_99 = l_Array_forInUnsafe_loop___at_Lean_Server_FileWorker_handleDefinition___spec__7___lambda__2(x_6, x_92, x_91, x_4, x_3, x_2, x_97, x_12, x_98);
lean_dec(x_97);
lean_dec(x_91);
if (lean_obj_tag(x_99) == 0)
@ -16846,7 +16806,7 @@ goto block_37;
}
}
}
lean_object* l_Std_PersistentArray_forIn___at_Lean_Server_FileWorker_handleDefinition___spec__5(uint8_t x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10) {
lean_object* l_Std_PersistentArray_forIn___at_Lean_Server_FileWorker_handleDefinition___spec__4(uint8_t x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10) {
_start:
{
lean_object* x_11; lean_object* x_12;
@ -16854,7 +16814,7 @@ x_11 = lean_ctor_get(x_7, 0);
lean_inc(x_8);
lean_inc(x_6);
lean_inc(x_5);
x_12 = l_Std_PersistentArray_forInAux___at_Lean_Server_FileWorker_handleDefinition___spec__6(x_1, x_2, x_3, x_4, x_5, x_6, x_8, x_11, x_8, x_9, x_10);
x_12 = l_Std_PersistentArray_forInAux___at_Lean_Server_FileWorker_handleDefinition___spec__5(x_1, x_2, x_3, x_4, x_5, x_6, x_8, x_11, x_8, x_9, x_10);
lean_dec(x_8);
if (lean_obj_tag(x_12) == 0)
{
@ -16976,7 +16936,7 @@ x_37 = lean_array_get_size(x_34);
x_38 = lean_usize_of_nat(x_37);
lean_dec(x_37);
x_39 = 0;
x_40 = l_Array_forInUnsafe_loop___at_Lean_Server_FileWorker_handleDefinition___spec__9(x_1, x_2, x_3, x_4, x_5, x_6, x_35, x_34, x_38, x_39, x_36, x_9, x_32);
x_40 = l_Array_forInUnsafe_loop___at_Lean_Server_FileWorker_handleDefinition___spec__8(x_1, x_2, x_3, x_4, x_5, x_6, x_35, x_34, x_38, x_39, x_36, x_9, x_32);
if (lean_obj_tag(x_40) == 0)
{
lean_object* x_41;
@ -17221,7 +17181,7 @@ x_91 = lean_array_get_size(x_88);
x_92 = lean_usize_of_nat(x_91);
lean_dec(x_91);
x_93 = 0;
x_94 = l_Array_forInUnsafe_loop___at_Lean_Server_FileWorker_handleDefinition___spec__9(x_1, x_2, x_3, x_4, x_5, x_6, x_89, x_88, x_92, x_93, x_90, x_9, x_86);
x_94 = l_Array_forInUnsafe_loop___at_Lean_Server_FileWorker_handleDefinition___spec__8(x_1, x_2, x_3, x_4, x_5, x_6, x_89, x_88, x_92, x_93, x_90, x_9, x_86);
if (lean_obj_tag(x_94) == 0)
{
lean_object* x_95;
@ -17392,7 +17352,7 @@ x_12 = lean_ctor_get(x_11, 1);
lean_inc(x_12);
lean_dec(x_11);
x_13 = l_Array_findSomeM_x3f___rarg___closed__1;
x_14 = l_Std_PersistentArray_forIn___at_Lean_Server_FileWorker_handleDefinition___spec__5(x_1, x_2, x_3, x_4, x_5, x_13, x_12, x_13, x_8, x_9);
x_14 = l_Std_PersistentArray_forIn___at_Lean_Server_FileWorker_handleDefinition___spec__4(x_1, x_2, x_3, x_4, x_5, x_13, x_12, x_13, x_8, x_9);
lean_dec(x_12);
if (lean_obj_tag(x_14) == 0)
{
@ -17680,23 +17640,11 @@ lean_dec(x_2);
return x_7;
}
}
lean_object* l_Lean_isRec___at_Lean_Server_FileWorker_handleDefinition___spec__3___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
lean_object* l_Lean_findDeclarationRangesCore_x3f___at_Lean_Server_FileWorker_handleDefinition___spec__3___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
_start:
{
lean_object* x_7;
x_7 = l_Lean_isRec___at_Lean_Server_FileWorker_handleDefinition___spec__3(x_1, x_2, x_3, x_4, x_5, x_6);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_2);
return x_7;
}
}
lean_object* l_Lean_findDeclarationRangesCore_x3f___at_Lean_Server_FileWorker_handleDefinition___spec__4___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6) {
_start:
{
lean_object* x_7;
x_7 = l_Lean_findDeclarationRangesCore_x3f___at_Lean_Server_FileWorker_handleDefinition___spec__4(x_1, x_2, x_3, x_4, x_5, x_6);
x_7 = l_Lean_findDeclarationRangesCore_x3f___at_Lean_Server_FileWorker_handleDefinition___spec__3(x_1, x_2, x_3, x_4, x_5, x_6);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_3);
@ -17716,7 +17664,7 @@ lean_dec(x_2);
return x_7;
}
}
lean_object* l_Array_forInUnsafe_loop___at_Lean_Server_FileWorker_handleDefinition___spec__7___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10, lean_object* x_11, lean_object* x_12, lean_object* x_13, lean_object* x_14) {
lean_object* l_Array_forInUnsafe_loop___at_Lean_Server_FileWorker_handleDefinition___spec__6___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10, lean_object* x_11, lean_object* x_12, lean_object* x_13, lean_object* x_14) {
_start:
{
uint8_t x_15; size_t x_16; size_t x_17; lean_object* x_18;
@ -17726,7 +17674,7 @@ x_16 = lean_unbox_usize(x_10);
lean_dec(x_10);
x_17 = lean_unbox_usize(x_11);
lean_dec(x_11);
x_18 = l_Array_forInUnsafe_loop___at_Lean_Server_FileWorker_handleDefinition___spec__7(x_15, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_16, x_17, x_12, x_13, x_14);
x_18 = l_Array_forInUnsafe_loop___at_Lean_Server_FileWorker_handleDefinition___spec__6(x_15, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_16, x_17, x_12, x_13, x_14);
lean_dec(x_13);
lean_dec(x_9);
lean_dec(x_7);
@ -17736,11 +17684,11 @@ lean_dec(x_2);
return x_18;
}
}
lean_object* l_Array_forInUnsafe_loop___at_Lean_Server_FileWorker_handleDefinition___spec__8___lambda__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9) {
lean_object* l_Array_forInUnsafe_loop___at_Lean_Server_FileWorker_handleDefinition___spec__7___lambda__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9) {
_start:
{
lean_object* x_10;
x_10 = l_Array_forInUnsafe_loop___at_Lean_Server_FileWorker_handleDefinition___spec__8___lambda__1(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9);
x_10 = l_Array_forInUnsafe_loop___at_Lean_Server_FileWorker_handleDefinition___spec__7___lambda__1(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9);
lean_dec(x_8);
lean_dec(x_6);
lean_dec(x_5);
@ -17748,11 +17696,11 @@ lean_dec(x_2);
return x_10;
}
}
lean_object* l_Array_forInUnsafe_loop___at_Lean_Server_FileWorker_handleDefinition___spec__8___lambda__2___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9) {
lean_object* l_Array_forInUnsafe_loop___at_Lean_Server_FileWorker_handleDefinition___spec__7___lambda__2___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9) {
_start:
{
lean_object* x_10;
x_10 = l_Array_forInUnsafe_loop___at_Lean_Server_FileWorker_handleDefinition___spec__8___lambda__2(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9);
x_10 = l_Array_forInUnsafe_loop___at_Lean_Server_FileWorker_handleDefinition___spec__7___lambda__2(x_1, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9);
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_6);
@ -17762,6 +17710,41 @@ lean_dec(x_3);
return x_10;
}
}
lean_object* l_Array_forInUnsafe_loop___at_Lean_Server_FileWorker_handleDefinition___spec__7___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, 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:
{
uint8_t x_14; size_t x_15; size_t x_16; lean_object* x_17;
x_14 = lean_unbox(x_1);
lean_dec(x_1);
x_15 = lean_unbox_usize(x_9);
lean_dec(x_9);
x_16 = lean_unbox_usize(x_10);
lean_dec(x_10);
x_17 = l_Array_forInUnsafe_loop___at_Lean_Server_FileWorker_handleDefinition___spec__7(x_14, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_15, x_16, x_11, x_12, x_13);
lean_dec(x_12);
lean_dec(x_8);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_2);
return x_17;
}
}
lean_object* l_Std_PersistentArray_forInAux___at_Lean_Server_FileWorker_handleDefinition___spec__5___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10, lean_object* x_11) {
_start:
{
uint8_t x_12; lean_object* x_13;
x_12 = lean_unbox(x_1);
lean_dec(x_1);
x_13 = l_Std_PersistentArray_forInAux___at_Lean_Server_FileWorker_handleDefinition___spec__5(x_12, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_11);
lean_dec(x_10);
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_2);
return x_13;
}
}
lean_object* l_Array_forInUnsafe_loop___at_Lean_Server_FileWorker_handleDefinition___spec__8___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, 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:
{
@ -17781,48 +17764,13 @@ lean_dec(x_2);
return x_17;
}
}
lean_object* l_Std_PersistentArray_forInAux___at_Lean_Server_FileWorker_handleDefinition___spec__6___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10, lean_object* x_11) {
_start:
{
uint8_t x_12; lean_object* x_13;
x_12 = lean_unbox(x_1);
lean_dec(x_1);
x_13 = l_Std_PersistentArray_forInAux___at_Lean_Server_FileWorker_handleDefinition___spec__6(x_12, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10, x_11);
lean_dec(x_10);
lean_dec(x_8);
lean_dec(x_7);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_2);
return x_13;
}
}
lean_object* l_Array_forInUnsafe_loop___at_Lean_Server_FileWorker_handleDefinition___spec__9___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, 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:
{
uint8_t x_14; size_t x_15; size_t x_16; lean_object* x_17;
x_14 = lean_unbox(x_1);
lean_dec(x_1);
x_15 = lean_unbox_usize(x_9);
lean_dec(x_9);
x_16 = lean_unbox_usize(x_10);
lean_dec(x_10);
x_17 = l_Array_forInUnsafe_loop___at_Lean_Server_FileWorker_handleDefinition___spec__9(x_14, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_15, x_16, x_11, x_12, x_13);
lean_dec(x_12);
lean_dec(x_8);
lean_dec(x_4);
lean_dec(x_3);
lean_dec(x_2);
return x_17;
}
}
lean_object* l_Std_PersistentArray_forIn___at_Lean_Server_FileWorker_handleDefinition___spec__5___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10) {
lean_object* l_Std_PersistentArray_forIn___at_Lean_Server_FileWorker_handleDefinition___spec__4___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3, lean_object* x_4, lean_object* x_5, lean_object* x_6, lean_object* x_7, lean_object* x_8, lean_object* x_9, lean_object* x_10) {
_start:
{
uint8_t x_11; lean_object* x_12;
x_11 = lean_unbox(x_1);
lean_dec(x_1);
x_12 = l_Std_PersistentArray_forIn___at_Lean_Server_FileWorker_handleDefinition___spec__5(x_11, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10);
x_12 = l_Std_PersistentArray_forIn___at_Lean_Server_FileWorker_handleDefinition___spec__4(x_11, x_2, x_3, x_4, x_5, x_6, x_7, x_8, x_9, x_10);
lean_dec(x_9);
lean_dec(x_7);
lean_dec(x_4);
@ -39218,8 +39166,8 @@ l_Lean_Server_FileWorker_handleCompletion___closed__3 = _init_l_Lean_Server_File
lean_mark_persistent(l_Lean_Server_FileWorker_handleCompletion___closed__3);
l_Lean_Server_FileWorker_handleHover___closed__1 = _init_l_Lean_Server_FileWorker_handleHover___closed__1();
lean_mark_persistent(l_Lean_Server_FileWorker_handleHover___closed__1);
l_Array_forInUnsafe_loop___at_Lean_Server_FileWorker_handleDefinition___spec__8___lambda__2___closed__1 = _init_l_Array_forInUnsafe_loop___at_Lean_Server_FileWorker_handleDefinition___spec__8___lambda__2___closed__1();
lean_mark_persistent(l_Array_forInUnsafe_loop___at_Lean_Server_FileWorker_handleDefinition___spec__8___lambda__2___closed__1);
l_Array_forInUnsafe_loop___at_Lean_Server_FileWorker_handleDefinition___spec__7___lambda__2___closed__1 = _init_l_Array_forInUnsafe_loop___at_Lean_Server_FileWorker_handleDefinition___spec__7___lambda__2___closed__1();
lean_mark_persistent(l_Array_forInUnsafe_loop___at_Lean_Server_FileWorker_handleDefinition___spec__7___lambda__2___closed__1);
l_Lean_Server_FileWorker_handleDefinition___closed__1 = _init_l_Lean_Server_FileWorker_handleDefinition___closed__1();
lean_mark_persistent(l_Lean_Server_FileWorker_handleDefinition___closed__1);
l_Lean_Server_FileWorker_handleDefinition___closed__2 = _init_l_Lean_Server_FileWorker_handleDefinition___closed__2();