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-01-21 17:45:55 -08:00
parent d6eb5a9ff2
commit 9fb5118990
10 changed files with 5743 additions and 4600 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
stage0/src/Init/Data/Hashable.lean generated
View file

@ -25,3 +25,12 @@ instance [Hashable α] : Hashable (Option α) where
instance [Hashable α] : Hashable (List α) where
hash as := as.foldl (fun r a => mixHash r (hash a)) 7
instance : Hashable UInt32 where
hash n := n.toUSize
instance : Hashable UInt64 where
hash n := n.toUSize
instance : Hashable USize where
hash n := n

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

@ -770,8 +770,7 @@ private partial def elabAppFnId (fIdent : Syntax) (fExplicitUnivs : List Level)
-- Set `errToSorry` to `false` if `funLVals` > 1. See comment above about the interaction between `errToSorry` and `observing`.
withReader (fun ctx => { ctx with errToSorry := funLVals.length == 1 && ctx.errToSorry }) do
funLVals.foldlM (init := acc) fun acc (f, fIdent, fields) => do
unless lvals.isEmpty && args.isEmpty && namedArgs.isEmpty && fields.isEmpty do
addTermInfo fIdent f
addTermInfo fIdent f
let lvals' := fields.map fun field => LVal.fieldName field field.getId.toString
let s ← observing do
let e ← elabAppLVals f (lvals' ++ lvals) namedArgs args expectedType? explicit ellipsis

95
stage0/src/Lean/Meta/SizeOf.lean generated
View file

@ -32,18 +32,33 @@ where
loop (i+1) (insts.push inst)
else
k insts
/--
Return `some x` if `fvar` has type of the form `... -> motive ... fvar` where `motive` in `motiveFVars`.
That is, `x` "produces" one of the recursor motives.
-/
private def isInductiveHypothesis? (motiveFVars : Array Expr) (fvar : Expr) : MetaM (Option Expr) := do
forallTelescopeReducing (← inferType fvar) fun _ type =>
if type.isApp && motiveFVars.contains type.getAppFn then
return some type.appArg!
else
return none
private def isInductiveHypothesis (motiveFVars : Array Expr) (fvar : Expr) : MetaM Bool :=
return (← isInductiveHypothesis? motiveFVars fvar).isSome
/--
Let `motiveFVars` be free variables for each motive in a kernel recursor, and `minorFVars` the free variables for a minor premise.
Then, return `true` is `fvar` (an element of `minorFVars`) corresponds to a recursive field.
That is, there is a free variable `minorFVar` in `minorFVars` with type `... -> motive ... fvar` where `motive` is an element of `motiveFVars`.
Then, return `some idx` if `minorFVars[idx]` has a type of the form `... -> motive ... fvar` for some `motive` in `motiveFVars`.
-/
private def isRecField (motiveFVars : Array Expr) (minorFVars : Array Expr) (fvar : Expr) : MetaM Bool := do
private def isRecField? (motiveFVars : Array Expr) (minorFVars : Array Expr) (fvar : Expr) : MetaM (Option Nat) := do
let mut idx := 0
for minorFVar in minorFVars do
let found ← forallTelescopeReducing (← inferType minorFVar) fun _ type =>
return motiveFVars.contains type.getAppFn && type.appArg! == fvar
if found then
return true
return false
if let some fvar' ← isInductiveHypothesis? motiveFVars minorFVar then
if fvar == fvar' then
return some idx
idx := idx + 1
return none
private partial def mkSizeOfMotives {α} (motiveFVars : Array Expr) (k : Array Expr → MetaM α) : MetaM α :=
loop 0 #[]
@ -68,22 +83,11 @@ where
forallBoundedTelescope (← inferType minorFVars'[i]) xs.size fun xs' _ => do
let mut minor ← mkNumeral (mkConst ``Nat) 1
for x in xs, x' in xs' do
-- If `x` is a recursive field, we skip it since we use the inductive hypothesis occurring later
unless (← isRecField motiveFVars xs x) do
let xType ← inferType x
minor ← forallTelescopeReducing xType fun ys xTypeResult => do
if motiveFVars.contains xTypeResult.getAppFn then
-- `x` is an inductive hypothesis
if ys.size > 0 then
-- ignore `x` because it is a function
return minor
else
mkAdd minor x'
else
try
mkAdd minor (← mkAppM ``SizeOf.sizeOf #[x'])
catch _ =>
return minor
unless (← isInductiveHypothesis motiveFVars x) do
unless (← whnf (← inferType x)).isForall do -- we suppress higher-order fields
match (← isRecField? motiveFVars xs x) with
| some idx => minor ← mkAdd minor xs'[idx]
| none => minor ← mkAdd minor (← mkAppM ``SizeOf.sizeOf #[x'])
minor ← mkLambdaFVars xs' minor
trace[Meta.sizeOf]! "minor: {minor}"
loop (i+1) (minors.push minor)
@ -150,12 +154,53 @@ def mkSizeOfFns (typeName : Name) : MetaM (Array Name) := do
i := i + 1
return result
private def mkSizeOfSpecTheorem (indInfo : InductiveVal) (sizeOfFns : Array Name) (ctorName : Name) : MetaM Unit := do
let ctorInfo ← getConstInfoCtor ctorName
let us := ctorInfo.levelParams.map mkLevelParam
forallTelescopeReducing ctorInfo.type fun xs _ => do
let params := xs[:ctorInfo.numParams]
let fields := xs[ctorInfo.numParams:]
let ctorApp := mkAppN (mkConst ctorName us) xs
mkLocalInstances params fun localInsts => do
let lhs ← mkAppM ``SizeOf.sizeOf #[ctorApp]
let mut rhs ← mkNumeral (mkConst ``Nat) 1
for field in fields do
unless (← whnf (← inferType field)).isForall do
rhs ← mkAdd rhs (← mkAppM ``SizeOf.sizeOf #[field])
let target ← mkEq lhs rhs
let thmName := ctorName ++ `sizeOf_spec
let thmParams := params ++ localInsts ++ fields
let thmType ← mkForallFVars thmParams target
let thmValue ←
if indInfo.isNested then
return () -- TODO
else
mkEqRefl rhs
let thmValue ← mkLambdaFVars thmParams thmValue
addDecl <| Declaration.thmDecl {
name := thmName
levelParams := ctorInfo.levelParams
type := thmType
value := thmValue
}
private def mkSizeOfSpecTheorems (indTypeNames : Array Name) (sizeOfFns : Array Name) : MetaM Unit := do
for indTypeName in indTypeNames do
let indInfo ← getConstInfoInduct indTypeName
for ctorName in indInfo.ctors do
mkSizeOfSpecTheorem indInfo sizeOfFns ctorName
return ()
builtin_initialize
registerOption `genSizeOf { defValue := true, group := "", descr := "generate `SizeOf` instance for inductive types and structures" }
registerOption `genSizeOfSpec { defValue := true, group := "", descr := "generate `SizeOf` specificiation theorems for automatically generated instances" }
def generateSizeOfInstance (opts : Options) : Bool :=
opts.get `genSizeOf true
def generateSizeOfSpec (opts : Options) : Bool :=
opts.get `genSizeOfSpec true
def mkSizeOfInstances (typeName : Name) : MetaM Unit := do
if (← getEnv).contains ``SizeOf && generateSizeOfInstance (← getOptions) && !(← isInductivePredicate typeName) then
let indInfo ← getConstInfoInduct typeName
@ -185,6 +230,8 @@ def mkSizeOfInstances (typeName : Name) : MetaM Unit := do
hints := ReducibilityHints.abbrev
}
addInstance instDeclName AttributeKind.global (evalPrio! default)
if generateSizeOfSpec (← getOptions) then
mkSizeOfSpecTheorems indInfo.all.toArray fns
builtin_initialize
registerTraceClass `Meta.sizeOf

17
stage0/src/Lean/Server/FileWorker.lean generated
View file

@ -204,9 +204,9 @@ section Initialization
let leanpkgPath ← match ← IO.getEnv "LEAN_SYSROOT" with
| some path => s!"{path}/bin/leanpkg{System.FilePath.exeSuffix}"
| _ => s!"{← appDir}/leanpkg{System.FilePath.exeSuffix}"
let mut srcSearchPath := match (← IO.getEnv "LEAN_SRC_PATH") with
| some p => parseSearchPath p
| none => []
let mut srcSearchPath := [s!"{← appDir}/../lib/lean/src"]
if let some p := (← IO.getEnv "LEAN_SRC_PATH") then
srcSearchPath := srcSearchPath ++ parseSearchPath p
-- NOTE: leanpkg does not exist in stage 0 (yet?)
if (← fileExists leanpkgPath) then
let pkgSearchPath ← leanpkgSetupSearchPath leanpkgPath m (Lean.Elab.headerToImports headerStx).toArray hOut
@ -405,15 +405,14 @@ section RequestHandling
(notFoundX := pure #[]) fun snap => do
for t in snap.toCmdState.infoState.trees do
if let some (ci, i) := t.hoverableTermAt? hoverPos then
let expr := if goToType? then ← ci.runMetaM i.lctx <| Meta.inferType i.expr
else i.expr
let expr ← if goToType? then ci.runMetaM i.lctx <| Meta.inferType i.expr else i.expr
if let some n := expr.constName? then
let mod? ← ci.runMetaM i.lctx <| findModuleOf? n
let modUri? ← match mod? with
| some modName =>
let modFname? ← st.srcSearchPath.findWithExt ".lean" modName
pure <| modFname?.map ("file://" ++ ·)
| none => pure <| some doc.meta.uri
| some modName =>
let modFname? ← st.srcSearchPath.findWithExt ".lean" modName
pure <| modFname?.map ("file://" ++ ·)
| none => pure <| some doc.meta.uri
let ranges? ← ci.runMetaM i.lctx <| findDeclarationRanges? n

3
stage0/src/Lean/Server/Watchdog.lean generated
View file

@ -213,8 +213,7 @@ section ServerM
let workerProc ← Process.spawn {
toStdioConfig := workerCfg
cmd := st.workerPath
-- append file and imports for Nix support; ignored otherwise
args := #["--worker"] ++ (Lean.Elab.headerToImports headerAst).toArray.map (toString ·.module) ++ st.args.toArray
args := #["--worker"] ++ st.args.toArray
}
let pendingRequestsRef ← IO.mkRef (RBMap.empty : PendingRequestMap)
-- The task will never access itself, so this is fine

63
stage0/stdlib/Init/Data/Hashable.c generated
View file

@ -14,18 +14,25 @@
extern "C" {
#endif
lean_object* l_instHashableProd_match__1(lean_object*, lean_object*, lean_object*);
size_t l_UInt32_toUSize(uint32_t);
size_t l_instHashableProd___rarg(lean_object*, lean_object*, lean_object*);
size_t l_instHashableUSize(size_t);
lean_object* l_instHashableList(lean_object*);
lean_object* l_instHashableUSize___boxed(lean_object*);
lean_object* l_List_foldl___at_instHashableList___spec__1___rarg___boxed(lean_object*, lean_object*, lean_object*);
size_t l_Option_hash___rarg(lean_object*, lean_object*);
lean_object* l_instHashableOption(lean_object*);
lean_object* l_Option_hash_match__1(lean_object*, lean_object*);
size_t l_UInt64_toUSize(uint64_t);
lean_object* l_List_foldl___at_instHashableList___spec__1(lean_object*);
lean_object* l_instHashableUInt64___boxed(lean_object*);
lean_object* l_instHashableProd(lean_object*, lean_object*);
lean_object* l_Option_hash___rarg___boxed(lean_object*, lean_object*);
lean_object* l_instHashableOption_match__1(lean_object*, lean_object*);
size_t l_instHashableUInt64(uint64_t);
lean_object* l_instHashableList___rarg___boxed(lean_object*, lean_object*);
lean_object* l_Option_hash_match__1___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_instHashableUInt32___boxed(lean_object*);
size_t lean_usize_of_nat(lean_object*);
size_t l_instHashableNat(lean_object*);
size_t l_instHashableList___rarg(lean_object*, lean_object*);
@ -36,6 +43,7 @@ lean_object* l_instHashableNat___boxed(lean_object*);
size_t lean_usize_mix_hash(size_t, size_t);
size_t l_instHashableOption___rarg(lean_object*, lean_object*);
lean_object* l_instHashableProd_match__1___rarg(lean_object*, lean_object*);
size_t l_instHashableUInt32(uint32_t);
lean_object* l_Option_hash(lean_object*);
size_t l_List_foldl___at_instHashableList___spec__1___rarg(lean_object*, size_t, lean_object*);
size_t l_instHashableNat(lean_object* x_1) {
@ -331,6 +339,61 @@ x_4 = lean_box_usize(x_3);
return x_4;
}
}
size_t l_instHashableUInt32(uint32_t x_1) {
_start:
{
size_t x_2;
x_2 = x_1;
return x_2;
}
}
lean_object* l_instHashableUInt32___boxed(lean_object* x_1) {
_start:
{
uint32_t x_2; size_t x_3; lean_object* x_4;
x_2 = lean_unbox_uint32(x_1);
lean_dec(x_1);
x_3 = l_instHashableUInt32(x_2);
x_4 = lean_box_usize(x_3);
return x_4;
}
}
size_t l_instHashableUInt64(uint64_t x_1) {
_start:
{
size_t x_2;
x_2 = ((size_t)x_1);
return x_2;
}
}
lean_object* l_instHashableUInt64___boxed(lean_object* x_1) {
_start:
{
uint64_t x_2; size_t x_3; lean_object* x_4;
x_2 = lean_unbox_uint64(x_1);
lean_dec(x_1);
x_3 = l_instHashableUInt64(x_2);
x_4 = lean_box_usize(x_3);
return x_4;
}
}
size_t l_instHashableUSize(size_t x_1) {
_start:
{
return x_1;
}
}
lean_object* l_instHashableUSize___boxed(lean_object* x_1) {
_start:
{
size_t x_2; size_t x_3; lean_object* x_4;
x_2 = lean_unbox_usize(x_1);
lean_dec(x_1);
x_3 = l_instHashableUSize(x_2);
x_4 = lean_box_usize(x_3);
return x_4;
}
}
lean_object* initialize_Init_Data_UInt(lean_object*);
lean_object* initialize_Init_Data_String(lean_object*);
static bool _G_initialized = false;

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

File diff suppressed because it is too large Load diff

5942
stage0/stdlib/Lean/Meta/SizeOf.c generated
View file

File diff suppressed because it is too large Load diff

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

File diff suppressed because it is too large Load diff

482
stage0/stdlib/Lean/Server/Watchdog.c generated
View file

@ -18,7 +18,6 @@ lean_object* l_Array_mapMUnsafe_map___at_Lean_Server_Watchdog_handleRequest___sp
lean_object* l_Array_mapMUnsafe_map___at_Lean_Server_Watchdog_tryWriteMessage___spec__2___rarg(lean_object*, size_t, size_t, lean_object*);
lean_object* l_Lean_Server_Watchdog_handleRequest_match__1___rarg___closed__3;
lean_object* lean_string_push(lean_object*, uint32_t);
extern lean_object* l_Lean_Name_toString___closed__1;
lean_object* l_Array_mapMUnsafe_map___at_Lean_Server_Watchdog_tryWriteMessage___spec__3___rarg___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_forInUnsafe_loop___at_Lean_Server_Watchdog_handleRequest___spec__6___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Server_Watchdog_FileWorker_readMessage___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*);
@ -103,10 +102,8 @@ lean_object* l_Lean_Server_Watchdog_eraseFileWorker___boxed(lean_object*, lean_o
lean_object* l_IO_getStdin___at_Lean_Server_Watchdog_watchdogMain___spec__1(lean_object*);
lean_object* l_IO_FS_Stream_readLspMessage(lean_object*, lean_object*);
lean_object* l_Lean_Server_Watchdog_parseParams___at_Lean_Server_Watchdog_handleNotification___spec__2___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_IO_FS_Stream_writeLspNotification___at_Lean_Server_Watchdog_startFileWorker___spec__6(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Server_Watchdog_runClientTask(lean_object*, lean_object*);
lean_object* l_Lean_Server_Watchdog_watchdogMain___boxed__const__2;
lean_object* l_Lean_Elab_headerToImports(lean_object*);
lean_object* l_Lean_Server_Watchdog_terminateFileWorker___closed__1;
lean_object* l_Lean_Server_Watchdog_FileWorker_readMessage_match__2___rarg(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Parser_mkInputContext(lean_object*, lean_object*);
@ -114,6 +111,7 @@ lean_object* l_Std_RBNode_del___at_Lean_Server_Watchdog_FileWorker_readMessage__
lean_object* l_IO_FS_Stream_readLspRequestAs___at_Lean_Server_Watchdog_initAndRunWatchdog___spec__2(lean_object*, lean_object*, lean_object*);
lean_object* lean_array_push(lean_object*, lean_object*);
lean_object* lean_array_get_size(lean_object*);
lean_object* l_Lean_Json_toStructured_x3f___at_Lean_Server_Watchdog_startFileWorker___spec__6(lean_object*);
lean_object* lean_string_append(lean_object*, lean_object*);
lean_object* l_Lean_Server_Watchdog_FileWorker_writeNotification___at_Lean_Server_Watchdog_handleDidChange___spec__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Server_Watchdog_FileWorker_writeRequest___at_Lean_Server_Watchdog_handleRequest___spec__9(lean_object*, lean_object*, lean_object*);
@ -127,12 +125,11 @@ lean_object* l_Lean_Server_Watchdog_handleCancelRequest_match__3(lean_object*, l
lean_object* l___private_Lean_Server_Watchdog_0__Lean_Server_Watchdog_forwardMessages_loop_match__1___boxed(lean_object*, lean_object*);
lean_object* l_IO_throwServerError___rarg(lean_object*, lean_object*);
lean_object* l_Lean_Server_Watchdog_parseParams___at_Lean_Server_Watchdog_handleRequest___spec__22(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Server_Watchdog_FileWorker_writeNotification___at_Lean_Server_Watchdog_startFileWorker___spec__5(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Json_toStructured_x3f___at_Lean_Server_Watchdog_startFileWorker___spec__3(lean_object*);
lean_object* l___private_Lean_Server_Watchdog_0__Lean_Server_Watchdog_forwardMessages_loop___closed__5;
lean_object* l___private_Lean_Server_Watchdog_0__Lean_Server_Watchdog_parseHeaderAst_match__1(lean_object*);
lean_object* l_Lean_Server_Watchdog_handleRequest___closed__7;
lean_object* l_Lean_Server_Watchdog_FileWorker_readMessage___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_IO_FS_Stream_writeLspRequest___at_Lean_Server_Watchdog_startFileWorker___spec__3(lean_object*, lean_object*, lean_object*);
lean_object* l_Std_RBNode_insert___at_Lean_Server_Watchdog_FileWorker_writeRequest___spec__1(lean_object*, lean_object*, lean_object*);
lean_object* l_IO_FS_Stream_readLspNotificationAs___at_Lean_Server_Watchdog_initAndRunWatchdogAux___spec__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Server_Watchdog_tryWriteMessage___at_Lean_Server_Watchdog_handleRequest___spec__33___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -152,7 +149,6 @@ lean_object* l_Lean_Server_Watchdog_parseParams___at_Lean_Server_Watchdog_handle
extern lean_object* l_Lean_Elab_parseImports___closed__1;
lean_object* l_Lean_Server_Watchdog_parseParams(lean_object*);
lean_object* l_Lean_Server_Watchdog_handleDidChange_match__1___rarg(lean_object*, lean_object*);
lean_object* l_Lean_Name_toStringWithSep(lean_object*, lean_object*);
lean_object* l_IO_FS_Stream_writeLspResponse___at_Lean_Server_Watchdog_mainLoop___spec__2(lean_object*, lean_object*, lean_object*);
lean_object* l_IO_FS_Stream_writeLspNotification___at_Lean_Server_Watchdog_handleCancelRequest___spec__3___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Server_Watchdog_tryWriteMessage___at_Lean_Server_Watchdog_handleRequest___spec__26___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -163,7 +159,6 @@ lean_object* l_Lean_Server_Watchdog_FileWorker_writeMessage___boxed(lean_object*
lean_object* l___private_Lean_Server_Watchdog_0__Lean_Server_Watchdog_forwardMessages(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_JsonRpc_instToJsonMessage___closed__10;
lean_object* l_Lean_Server_Watchdog_workerCfg;
lean_object* l_Lean_Json_toStructured_x3f___at_Lean_Server_Watchdog_startFileWorker___spec__4(lean_object*);
lean_object* l_Lean_Server_Watchdog_tryWriteMessage___at_Lean_Server_Watchdog_handleRequest___spec__5___lambda__2(uint8_t, 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_Watchdog_FileWorker_errorPendingRequests_match__1___rarg(lean_object*, lean_object*);
@ -178,12 +173,14 @@ lean_object* lean_io_as_task(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Server_Watchdog_initAndRunWatchdog___lambda__1___closed__3;
lean_object* l_Std_RBNode_erase___at_Lean_Server_Watchdog_eraseFileWorker___spec__1(lean_object*, lean_object*);
lean_object* l_Std_RBNode_setBlack___rarg(lean_object*);
lean_object* l_IO_mkRef___at_Lean_Server_Watchdog_startFileWorker___spec__1(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Server_Watchdog_mainLoop___closed__1;
lean_object* l_Lean_Server_Watchdog_terminateFileWorker(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Server_Watchdog_tryWriteMessage___rarg___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l___private_Lean_Server_Watchdog_0__Lean_Server_Watchdog_forwardMessages_loop_match__1___rarg(lean_object*);
lean_object* l_Lean_Server_Watchdog_handleDidChange_match__1(lean_object*);
lean_object* l_Std_RBNode_find___at_Lean_Server_Watchdog_findFileWorker___spec__1___boxed(lean_object*, lean_object*);
lean_object* l_IO_mkRef___at_Lean_Server_Watchdog_startFileWorker___spec__1___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Std_RBNode_forIn_visit___at_Lean_Server_Watchdog_shutdown___spec__2(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_forInUnsafe_loop___at_Lean_Server_Watchdog_handleCancelRequest___spec__6___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Server_Watchdog_parseParams___at_Lean_Server_Watchdog_handleNotification___spec__3(lean_object*, lean_object*, lean_object*);
@ -295,7 +292,6 @@ lean_object* l_Array_mapMUnsafe_map___at_Lean_Server_Watchdog_handleRequest___sp
lean_object* l_Lean_Server_Watchdog_FileWorker_stdout(lean_object*);
lean_object* lean_server_watchdog_main(lean_object*, lean_object*);
lean_object* l_Lean_Json_opt___at_Lean_JsonRpc_instToJsonMessage___spec__1(lean_object*, lean_object*);
lean_object* l_IO_mkRef___at_Lean_Server_Watchdog_startFileWorker___spec__2___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Server_Watchdog_handleNotification_match__1(lean_object*);
lean_object* l___private_Lean_Data_Lsp_LanguageFeatures_0__Lean_Lsp_fromJsonDocumentSymbolParams____x40_Lean_Data_Lsp_LanguageFeatures___hyg_239_(lean_object*);
lean_object* l_Lean_Server_Watchdog_tryWriteMessage___at_Lean_Server_Watchdog_handleRequest___spec__26___closed__1;
@ -317,6 +313,7 @@ lean_object* l_Lean_Server_Watchdog_FileWorker_errorPendingRequests___boxed(lean
lean_object* l_Lean_Server_Watchdog_parseParams___at_Lean_Server_Watchdog_handleNotification___spec__3___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Server_Watchdog_mainLoop(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Json_toStructured_x3f___at_Lean_Server_Watchdog_handleRequest___spec__32(lean_object*);
lean_object* l_IO_FS_Stream_writeLspRequest___at_Lean_Server_Watchdog_startFileWorker___spec__2(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Server_Watchdog_tryWriteMessage___at_Lean_Server_Watchdog_handleRequest___spec__12___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
extern lean_object* l_Task_Priority_default;
lean_object* l_Lean_Server_Watchdog_tryWriteMessage___at_Lean_Server_Watchdog_handleDidChange___spec__4___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -330,6 +327,7 @@ lean_object* l___private_Lean_Server_Watchdog_0__Lean_Server_Watchdog_forwardMes
lean_object* l_Lean_Server_Watchdog_tryWriteMessage(lean_object*);
lean_object* l_Lean_Json_getObjValAs_x3f___at_Lean_Lsp_instFromJsonInitializeParams___spec__5(lean_object*, lean_object*);
lean_object* l_Lean_Server_Watchdog_handleCancelRequest_match__3___boxed(lean_object*, lean_object*);
lean_object* l_IO_FS_Stream_writeLspNotification___at_Lean_Server_Watchdog_startFileWorker___spec__5(lean_object*, lean_object*, lean_object*);
lean_object* l_IO_FS_Stream_readRequestAs___at_Lean_Server_Watchdog_initAndRunWatchdog___spec__3(lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Server_Watchdog_parseParams_match__1(lean_object*, lean_object*);
extern lean_object* l_Lean_JsonRpc_instToJsonErrorCode___closed__36;
@ -352,7 +350,6 @@ lean_object* l_Lean_Server_Watchdog_tryWriteMessage___at_Lean_Server_Watchdog_ha
lean_object* l_Lean_Server_Watchdog_shutdown(lean_object*, lean_object*);
lean_object* l_Lean_Server_Watchdog_FileWorker_writeNotification___at_Lean_Server_Watchdog_handleCancelRequest___spec__2___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Server_Watchdog_tryWriteMessage___at_Lean_Server_Watchdog_handleCancelRequest___spec__5___closed__2;
lean_object* l_Lean_Json_toStructured_x3f___at_Lean_Server_Watchdog_startFileWorker___spec__7(lean_object*);
uint8_t l_UInt32_decEq(uint32_t, uint32_t);
lean_object* l_Lean_Json_toStructured_x3f___at_Lean_Server_Watchdog_handleRequest___spec__11(lean_object*);
lean_object* l_Lean_Server_Watchdog_tryWriteMessage___at_Lean_Server_Watchdog_handleRequest___spec__38___lambda__1(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
@ -383,7 +380,6 @@ lean_object* lean_io_process_child_wait(lean_object*, lean_object*, lean_object*
uint8_t lean_nat_dec_le(lean_object*, lean_object*);
lean_object* l_Lean_Server_Watchdog_parseParams___at_Lean_Server_Watchdog_handleNotification___spec__5(lean_object*, lean_object*, lean_object*);
lean_object* l_Array_forInUnsafe_loop___at_Lean_Server_Watchdog_handleRequest___spec__13(lean_object*, lean_object*, size_t, size_t, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_mapMUnsafe_map___at_Lean_Server_Watchdog_startFileWorker___spec__1___boxed(lean_object*, lean_object*, lean_object*);
uint8_t l_Std_RBNode_isRed___rarg(lean_object*);
extern lean_object* l_Lean_JsonRpc_instToJsonErrorCode___closed__32;
lean_object* l___private_Lean_Data_Lsp_TextSync_0__Lean_Lsp_toJsonDidChangeTextDocumentParams____x40_Lean_Data_Lsp_TextSync___hyg_275_(lean_object*);
@ -416,7 +412,6 @@ lean_object* l_Lean_Server_Watchdog_tryWriteMessage___at_Lean_Server_Watchdog_ha
lean_object* l_Lean_Server_Watchdog_tryWriteMessage___at_Lean_Server_Watchdog_handleRequest___spec__38___lambda__1___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Server_Watchdog_tryWriteMessage___at_Lean_Server_Watchdog_handleRequest___spec__38___closed__2;
lean_object* l_Lean_Json_mkObj(lean_object*);
lean_object* l_IO_mkRef___at_Lean_Server_Watchdog_startFileWorker___spec__2(lean_object*, lean_object*, lean_object*);
extern lean_object* l_Lean_getBuiltinSearchPath___closed__4;
extern lean_object* l_Lean_JsonRpc_instToJsonMessage___closed__11;
lean_object* l_Array_mapMUnsafe_map___at_Lean_Server_Watchdog_handleDidChange___spec__6___boxed(lean_object*, lean_object*, lean_object*);
@ -521,11 +516,11 @@ lean_object* l_Lean_Server_Watchdog_shutdown_match__4___rarg(lean_object*);
lean_object* lean_task_pure(lean_object*);
lean_object* l_Lean_Server_Watchdog_handleNotification_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_IO_FS_Stream_writeLspResponse___at_Lean_Server_Watchdog_mainLoop___spec__2___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Server_Watchdog_FileWorker_writeNotification___at_Lean_Server_Watchdog_startFileWorker___spec__4(lean_object*, lean_object*, lean_object*);
lean_object* l_Array_mapMUnsafe_map___at_Lean_Server_Watchdog_handleRequest___spec__35___boxed(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Server_Watchdog_findFileWorker(lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Server_Watchdog_handleDidChange___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_Watchdog_handleRequest_match__1___rarg(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Array_mapMUnsafe_map___at_Lean_Server_Watchdog_startFileWorker___spec__1(size_t, size_t, lean_object*);
lean_object* l_Lean_Server_Watchdog_tryWriteMessage___at_Lean_Server_Watchdog_handleCancelRequest___spec__5___lambda__2___boxed(lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*, lean_object*);
lean_object* l_Lean_Server_Watchdog_handleCancelRequest_match__3___rarg(lean_object*);
lean_object* l_Lean_Server_Watchdog_handleDidChange___lambda__1___closed__2;
@ -7503,40 +7498,7 @@ lean_dec(x_1);
return x_2;
}
}
lean_object* l_Array_mapMUnsafe_map___at_Lean_Server_Watchdog_startFileWorker___spec__1(size_t x_1, size_t x_2, lean_object* x_3) {
_start:
{
uint8_t x_4;
x_4 = x_2 < x_1;
if (x_4 == 0)
{
lean_object* x_5;
x_5 = x_3;
return x_5;
}
else
{
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; size_t x_13; size_t x_14; lean_object* x_15; lean_object* x_16;
x_6 = lean_array_uget(x_3, x_2);
x_7 = lean_unsigned_to_nat(0u);
x_8 = lean_array_uset(x_3, x_2, x_7);
x_9 = x_6;
x_10 = lean_ctor_get(x_9, 0);
lean_inc(x_10);
lean_dec(x_9);
x_11 = l_Lean_Name_toString___closed__1;
x_12 = l_Lean_Name_toStringWithSep(x_11, x_10);
x_13 = 1;
x_14 = x_2 + x_13;
x_15 = x_12;
x_16 = lean_array_uset(x_8, x_2, x_15);
x_2 = x_14;
x_3 = x_16;
goto _start;
}
}
}
lean_object* l_IO_mkRef___at_Lean_Server_Watchdog_startFileWorker___spec__2(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
lean_object* l_IO_mkRef___at_Lean_Server_Watchdog_startFileWorker___spec__1(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4; uint8_t x_5;
@ -7561,7 +7523,7 @@ return x_8;
}
}
}
lean_object* l_Lean_Json_toStructured_x3f___at_Lean_Server_Watchdog_startFileWorker___spec__4(lean_object* x_1) {
lean_object* l_Lean_Json_toStructured_x3f___at_Lean_Server_Watchdog_startFileWorker___spec__3(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
@ -7576,7 +7538,7 @@ lean_ctor_set(x_5, 0, x_4);
return x_5;
}
}
lean_object* l_IO_FS_Stream_writeLspRequest___at_Lean_Server_Watchdog_startFileWorker___spec__3(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
lean_object* l_IO_FS_Stream_writeLspRequest___at_Lean_Server_Watchdog_startFileWorker___spec__2(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8; lean_object* x_9;
@ -7587,7 +7549,7 @@ lean_inc(x_5);
x_6 = lean_ctor_get(x_2, 2);
lean_inc(x_6);
lean_dec(x_2);
x_7 = l_Lean_Json_toStructured_x3f___at_Lean_Server_Watchdog_startFileWorker___spec__4(x_6);
x_7 = l_Lean_Json_toStructured_x3f___at_Lean_Server_Watchdog_startFileWorker___spec__3(x_6);
x_8 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_8, 0, x_4);
lean_ctor_set(x_8, 1, x_5);
@ -7597,7 +7559,7 @@ lean_dec(x_8);
return x_9;
}
}
lean_object* l_Lean_Json_toStructured_x3f___at_Lean_Server_Watchdog_startFileWorker___spec__7(lean_object* x_1) {
lean_object* l_Lean_Json_toStructured_x3f___at_Lean_Server_Watchdog_startFileWorker___spec__6(lean_object* x_1) {
_start:
{
lean_object* x_2; lean_object* x_3; lean_object* x_4; lean_object* x_5;
@ -7612,7 +7574,7 @@ lean_ctor_set(x_5, 0, x_4);
return x_5;
}
}
lean_object* l_IO_FS_Stream_writeLspNotification___at_Lean_Server_Watchdog_startFileWorker___spec__6(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
lean_object* l_IO_FS_Stream_writeLspNotification___at_Lean_Server_Watchdog_startFileWorker___spec__5(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4; lean_object* x_5; lean_object* x_6; lean_object* x_7; lean_object* x_8;
@ -7621,7 +7583,7 @@ lean_inc(x_4);
x_5 = lean_ctor_get(x_2, 1);
lean_inc(x_5);
lean_dec(x_2);
x_6 = l_Lean_Json_toStructured_x3f___at_Lean_Server_Watchdog_startFileWorker___spec__7(x_5);
x_6 = l_Lean_Json_toStructured_x3f___at_Lean_Server_Watchdog_startFileWorker___spec__6(x_5);
x_7 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_7, 0, x_4);
lean_ctor_set(x_7, 1, x_6);
@ -7630,12 +7592,12 @@ lean_dec(x_7);
return x_8;
}
}
lean_object* l_Lean_Server_Watchdog_FileWorker_writeNotification___at_Lean_Server_Watchdog_startFileWorker___spec__5(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
lean_object* l_Lean_Server_Watchdog_FileWorker_writeNotification___at_Lean_Server_Watchdog_startFileWorker___spec__4(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4; lean_object* x_5;
x_4 = l_Lean_Server_Watchdog_FileWorker_stdin(x_1);
x_5 = l_IO_FS_Stream_writeLspNotification___at_Lean_Server_Watchdog_startFileWorker___spec__6(x_4, x_2, x_3);
x_5 = l_IO_FS_Stream_writeLspNotification___at_Lean_Server_Watchdog_startFileWorker___spec__5(x_4, x_2, x_3);
return x_5;
}
}
@ -7701,7 +7663,7 @@ lean_inc(x_7);
x_8 = l___private_Lean_Server_Watchdog_0__Lean_Server_Watchdog_parseHeaderAst(x_7, x_3);
if (lean_obj_tag(x_8) == 0)
{
lean_object* x_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; size_t x_17; size_t x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22; 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_9; lean_object* x_10; lean_object* x_11; lean_object* x_12; lean_object* x_13; lean_object* x_14; lean_object* x_15; lean_object* x_16; lean_object* x_17; lean_object* x_18; lean_object* x_19; lean_object* x_20; lean_object* x_21; lean_object* x_22;
x_9 = lean_ctor_get(x_8, 0);
lean_inc(x_9);
x_10 = lean_ctor_get(x_8, 1);
@ -7709,281 +7671,255 @@ lean_inc(x_10);
lean_dec(x_8);
x_11 = lean_ctor_get(x_2, 6);
lean_inc(x_11);
x_12 = l_Lean_Elab_headerToImports(x_9);
x_12 = lean_ctor_get(x_2, 3);
lean_inc(x_12);
x_13 = l_List_redLength___rarg(x_12);
x_14 = lean_mk_empty_array_with_capacity(x_13);
lean_dec(x_13);
x_15 = l_List_toArrayAux___rarg(x_12, x_14);
x_16 = lean_array_get_size(x_15);
x_17 = lean_usize_of_nat(x_16);
lean_dec(x_16);
x_18 = 0;
x_19 = x_15;
x_20 = l_Array_mapMUnsafe_map___at_Lean_Server_Watchdog_startFileWorker___spec__1(x_17, x_18, x_19);
x_21 = x_20;
x_22 = l_Lean_Server_Watchdog_startFileWorker___closed__2;
x_23 = l_Array_append___rarg(x_22, x_21);
lean_dec(x_21);
x_24 = lean_ctor_get(x_2, 3);
x_16 = l_Lean_Server_Watchdog_startFileWorker___closed__2;
x_17 = l_Array_append___rarg(x_16, x_15);
lean_dec(x_15);
x_18 = lean_box(0);
x_19 = l_Lean_Server_Watchdog_workerCfg;
x_20 = l_Array_empty___closed__1;
x_21 = lean_alloc_ctor(0, 5, 0);
lean_ctor_set(x_21, 0, x_19);
lean_ctor_set(x_21, 1, x_11);
lean_ctor_set(x_21, 2, x_17);
lean_ctor_set(x_21, 3, x_18);
lean_ctor_set(x_21, 4, x_20);
x_22 = lean_io_process_spawn(x_21, x_10);
if (lean_obj_tag(x_22) == 0)
{
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;
x_23 = lean_ctor_get(x_22, 0);
lean_inc(x_23);
x_24 = lean_ctor_get(x_22, 1);
lean_inc(x_24);
x_25 = l_List_redLength___rarg(x_24);
x_26 = lean_mk_empty_array_with_capacity(x_25);
lean_dec(x_25);
x_27 = l_List_toArrayAux___rarg(x_24, x_26);
x_28 = l_Array_append___rarg(x_23, x_27);
lean_dec(x_27);
x_29 = lean_box(0);
x_30 = l_Lean_Server_Watchdog_workerCfg;
x_31 = l_Array_empty___closed__1;
lean_dec(x_22);
x_25 = lean_box(0);
x_26 = l_IO_mkRef___at_Lean_Server_Watchdog_startFileWorker___spec__1(x_25, x_2, x_24);
x_27 = lean_ctor_get(x_26, 0);
lean_inc(x_27);
x_28 = lean_ctor_get(x_26, 1);
lean_inc(x_28);
lean_dec(x_26);
x_29 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_29, 0, x_1);
lean_ctor_set(x_29, 1, x_9);
x_30 = l_Lean_Server_Watchdog_startFileWorker___closed__3;
x_31 = lean_box(1);
lean_inc(x_27);
lean_inc(x_23);
lean_inc(x_29);
x_32 = lean_alloc_ctor(0, 5, 0);
lean_ctor_set(x_32, 0, x_30);
lean_ctor_set(x_32, 1, x_11);
lean_ctor_set(x_32, 2, x_28);
lean_ctor_set(x_32, 3, x_29);
lean_ctor_set(x_32, 4, x_31);
x_33 = lean_io_process_spawn(x_32, x_10);
lean_ctor_set(x_32, 0, x_29);
lean_ctor_set(x_32, 1, x_23);
lean_ctor_set(x_32, 2, x_30);
lean_ctor_set(x_32, 3, x_31);
lean_ctor_set(x_32, 4, x_27);
lean_inc(x_2);
x_33 = l___private_Lean_Server_Watchdog_0__Lean_Server_Watchdog_forwardMessages(x_32, x_2, x_28);
if (lean_obj_tag(x_33) == 0)
{
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; lean_object* x_42; lean_object* x_43; lean_object* x_44;
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; lean_object* x_42;
x_34 = lean_ctor_get(x_33, 0);
lean_inc(x_34);
x_35 = lean_ctor_get(x_33, 1);
lean_inc(x_35);
lean_dec(x_33);
x_36 = lean_box(0);
x_37 = l_IO_mkRef___at_Lean_Server_Watchdog_startFileWorker___spec__2(x_36, x_2, x_35);
x_38 = lean_ctor_get(x_37, 0);
x_36 = lean_alloc_ctor(0, 5, 0);
lean_ctor_set(x_36, 0, x_29);
lean_ctor_set(x_36, 1, x_23);
lean_ctor_set(x_36, 2, x_34);
lean_ctor_set(x_36, 3, x_31);
lean_ctor_set(x_36, 4, x_27);
lean_inc(x_36);
x_37 = l_Lean_Server_Watchdog_FileWorker_stdin(x_36);
x_38 = lean_ctor_get(x_2, 5);
lean_inc(x_38);
x_39 = lean_ctor_get(x_37, 1);
lean_inc(x_39);
lean_dec(x_37);
x_40 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_40, 0, x_1);
lean_ctor_set(x_40, 1, x_9);
x_41 = l_Lean_Server_Watchdog_startFileWorker___closed__3;
x_42 = lean_box(1);
lean_inc(x_38);
lean_inc(x_34);
lean_inc(x_40);
x_43 = lean_alloc_ctor(0, 5, 0);
lean_ctor_set(x_43, 0, x_40);
lean_ctor_set(x_43, 1, x_34);
lean_ctor_set(x_43, 2, x_41);
lean_ctor_set(x_43, 3, x_42);
lean_ctor_set(x_43, 4, x_38);
lean_inc(x_2);
x_44 = l___private_Lean_Server_Watchdog_0__Lean_Server_Watchdog_forwardMessages(x_43, x_2, x_39);
if (lean_obj_tag(x_44) == 0)
x_39 = l_Lean_Server_Watchdog_startFileWorker___closed__4;
x_40 = l_Lean_Parser_Command_initialize___elambda__1___closed__1;
x_41 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_41, 0, x_39);
lean_ctor_set(x_41, 1, x_40);
lean_ctor_set(x_41, 2, x_38);
x_42 = l_IO_FS_Stream_writeLspRequest___at_Lean_Server_Watchdog_startFileWorker___spec__2(x_37, x_41, x_35);
if (lean_obj_tag(x_42) == 0)
{
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; lean_object* x_53;
x_45 = lean_ctor_get(x_44, 0);
lean_inc(x_45);
x_46 = lean_ctor_get(x_44, 1);
lean_inc(x_46);
lean_dec(x_44);
x_47 = lean_alloc_ctor(0, 5, 0);
lean_ctor_set(x_47, 0, x_40);
lean_ctor_set(x_47, 1, x_34);
lean_ctor_set(x_47, 2, x_45);
lean_ctor_set(x_47, 3, x_42);
lean_ctor_set(x_47, 4, x_38);
lean_inc(x_47);
x_48 = l_Lean_Server_Watchdog_FileWorker_stdin(x_47);
x_49 = lean_ctor_get(x_2, 5);
lean_object* x_43; lean_object* x_44; lean_object* x_45; lean_object* x_46; lean_object* x_47; lean_object* x_48;
x_43 = lean_ctor_get(x_42, 1);
lean_inc(x_43);
lean_dec(x_42);
x_44 = l_Lean_getBuiltinSearchPath___closed__4;
x_45 = lean_alloc_ctor(0, 4, 0);
lean_ctor_set(x_45, 0, x_4);
lean_ctor_set(x_45, 1, x_44);
lean_ctor_set(x_45, 2, x_5);
lean_ctor_set(x_45, 3, x_7);
x_46 = l_Lean_Server_Watchdog_startFileWorker___closed__5;
x_47 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_47, 0, x_46);
lean_ctor_set(x_47, 1, x_45);
lean_inc(x_36);
x_48 = l_Lean_Server_Watchdog_FileWorker_writeNotification___at_Lean_Server_Watchdog_startFileWorker___spec__4(x_36, x_47, x_43);
if (lean_obj_tag(x_48) == 0)
{
lean_object* x_49; lean_object* x_50;
x_49 = lean_ctor_get(x_48, 1);
lean_inc(x_49);
x_50 = l_Lean_Server_Watchdog_startFileWorker___closed__4;
x_51 = l_Lean_Parser_Command_initialize___elambda__1___closed__1;
x_52 = lean_alloc_ctor(0, 3, 0);
lean_ctor_set(x_52, 0, x_50);
lean_ctor_set(x_52, 1, x_51);
lean_ctor_set(x_52, 2, x_49);
x_53 = l_IO_FS_Stream_writeLspRequest___at_Lean_Server_Watchdog_startFileWorker___spec__3(x_48, x_52, x_46);
if (lean_obj_tag(x_53) == 0)
lean_dec(x_48);
x_50 = l_Lean_Server_Watchdog_updateFileWorkers(x_36, x_2, x_49);
lean_dec(x_2);
return x_50;
}
else
{
lean_object* x_54; lean_object* x_55; lean_object* x_56; lean_object* x_57; lean_object* x_58; lean_object* x_59;
x_54 = lean_ctor_get(x_53, 1);
lean_inc(x_54);
lean_dec(x_53);
x_55 = l_Lean_getBuiltinSearchPath___closed__4;
x_56 = lean_alloc_ctor(0, 4, 0);
lean_ctor_set(x_56, 0, x_4);
lean_ctor_set(x_56, 1, x_55);
lean_ctor_set(x_56, 2, x_5);
lean_ctor_set(x_56, 3, x_7);
x_57 = l_Lean_Server_Watchdog_startFileWorker___closed__5;
x_58 = lean_alloc_ctor(0, 2, 0);
lean_ctor_set(x_58, 0, x_57);
lean_ctor_set(x_58, 1, x_56);
lean_inc(x_47);
x_59 = l_Lean_Server_Watchdog_FileWorker_writeNotification___at_Lean_Server_Watchdog_startFileWorker___spec__5(x_47, x_58, x_54);
if (lean_obj_tag(x_59) == 0)
uint8_t x_51;
lean_dec(x_36);
lean_dec(x_2);
x_51 = !lean_is_exclusive(x_48);
if (x_51 == 0)
{
lean_object* x_60; lean_object* x_61;
x_60 = lean_ctor_get(x_59, 1);
return x_48;
}
else
{
lean_object* x_52; lean_object* x_53; lean_object* x_54;
x_52 = lean_ctor_get(x_48, 0);
x_53 = lean_ctor_get(x_48, 1);
lean_inc(x_53);
lean_inc(x_52);
lean_dec(x_48);
x_54 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_54, 0, x_52);
lean_ctor_set(x_54, 1, x_53);
return x_54;
}
}
}
else
{
uint8_t x_55;
lean_dec(x_36);
lean_dec(x_7);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_2);
x_55 = !lean_is_exclusive(x_42);
if (x_55 == 0)
{
return x_42;
}
else
{
lean_object* x_56; lean_object* x_57; lean_object* x_58;
x_56 = lean_ctor_get(x_42, 0);
x_57 = lean_ctor_get(x_42, 1);
lean_inc(x_57);
lean_inc(x_56);
lean_dec(x_42);
x_58 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_58, 0, x_56);
lean_ctor_set(x_58, 1, x_57);
return x_58;
}
}
}
else
{
uint8_t x_59;
lean_dec(x_29);
lean_dec(x_27);
lean_dec(x_23);
lean_dec(x_7);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_2);
x_59 = !lean_is_exclusive(x_33);
if (x_59 == 0)
{
return x_33;
}
else
{
lean_object* x_60; lean_object* x_61; lean_object* x_62;
x_60 = lean_ctor_get(x_33, 0);
x_61 = lean_ctor_get(x_33, 1);
lean_inc(x_61);
lean_inc(x_60);
lean_dec(x_59);
x_61 = l_Lean_Server_Watchdog_updateFileWorkers(x_47, x_2, x_60);
lean_dec(x_2);
return x_61;
}
else
{
uint8_t x_62;
lean_dec(x_47);
lean_dec(x_2);
x_62 = !lean_is_exclusive(x_59);
if (x_62 == 0)
{
return x_59;
}
else
{
lean_object* x_63; lean_object* x_64; lean_object* x_65;
x_63 = lean_ctor_get(x_59, 0);
x_64 = lean_ctor_get(x_59, 1);
lean_inc(x_64);
lean_inc(x_63);
lean_dec(x_59);
x_65 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_65, 0, x_63);
lean_ctor_set(x_65, 1, x_64);
return x_65;
lean_dec(x_33);
x_62 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_62, 0, x_60);
lean_ctor_set(x_62, 1, x_61);
return x_62;
}
}
}
else
{
uint8_t x_66;
lean_dec(x_47);
lean_dec(x_7);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_2);
x_66 = !lean_is_exclusive(x_53);
if (x_66 == 0)
{
return x_53;
}
else
{
lean_object* x_67; lean_object* x_68; lean_object* x_69;
x_67 = lean_ctor_get(x_53, 0);
x_68 = lean_ctor_get(x_53, 1);
lean_inc(x_68);
lean_inc(x_67);
lean_dec(x_53);
x_69 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_69, 0, x_67);
lean_ctor_set(x_69, 1, x_68);
return x_69;
}
}
}
else
{
uint8_t x_70;
lean_dec(x_40);
lean_dec(x_38);
lean_dec(x_34);
lean_dec(x_7);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_2);
x_70 = !lean_is_exclusive(x_44);
if (x_70 == 0)
{
return x_44;
}
else
{
lean_object* x_71; lean_object* x_72; lean_object* x_73;
x_71 = lean_ctor_get(x_44, 0);
x_72 = lean_ctor_get(x_44, 1);
lean_inc(x_72);
lean_inc(x_71);
lean_dec(x_44);
x_73 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_73, 0, x_71);
lean_ctor_set(x_73, 1, x_72);
return x_73;
}
}
}
else
{
uint8_t x_74;
uint8_t x_63;
lean_dec(x_9);
lean_dec(x_7);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_2);
lean_dec(x_1);
x_74 = !lean_is_exclusive(x_33);
if (x_74 == 0)
x_63 = !lean_is_exclusive(x_22);
if (x_63 == 0)
{
return x_33;
return x_22;
}
else
{
lean_object* x_75; lean_object* x_76; lean_object* x_77;
x_75 = lean_ctor_get(x_33, 0);
x_76 = lean_ctor_get(x_33, 1);
lean_inc(x_76);
lean_inc(x_75);
lean_dec(x_33);
x_77 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_77, 0, x_75);
lean_ctor_set(x_77, 1, x_76);
return x_77;
lean_object* x_64; lean_object* x_65; lean_object* x_66;
x_64 = lean_ctor_get(x_22, 0);
x_65 = lean_ctor_get(x_22, 1);
lean_inc(x_65);
lean_inc(x_64);
lean_dec(x_22);
x_66 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_66, 0, x_64);
lean_ctor_set(x_66, 1, x_65);
return x_66;
}
}
}
else
{
uint8_t x_78;
uint8_t x_67;
lean_dec(x_7);
lean_dec(x_5);
lean_dec(x_4);
lean_dec(x_2);
lean_dec(x_1);
x_78 = !lean_is_exclusive(x_8);
if (x_78 == 0)
x_67 = !lean_is_exclusive(x_8);
if (x_67 == 0)
{
return x_8;
}
else
{
lean_object* x_79; lean_object* x_80; lean_object* x_81;
x_79 = lean_ctor_get(x_8, 0);
x_80 = lean_ctor_get(x_8, 1);
lean_inc(x_80);
lean_inc(x_79);
lean_object* x_68; lean_object* x_69; lean_object* x_70;
x_68 = lean_ctor_get(x_8, 0);
x_69 = lean_ctor_get(x_8, 1);
lean_inc(x_69);
lean_inc(x_68);
lean_dec(x_8);
x_81 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_81, 0, x_79);
lean_ctor_set(x_81, 1, x_80);
return x_81;
x_70 = lean_alloc_ctor(1, 2, 0);
lean_ctor_set(x_70, 0, x_68);
lean_ctor_set(x_70, 1, x_69);
return x_70;
}
}
}
}
lean_object* l_Array_mapMUnsafe_map___at_Lean_Server_Watchdog_startFileWorker___spec__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
size_t x_4; size_t x_5; lean_object* x_6;
x_4 = lean_unbox_usize(x_1);
lean_dec(x_1);
x_5 = lean_unbox_usize(x_2);
lean_dec(x_2);
x_6 = l_Array_mapMUnsafe_map___at_Lean_Server_Watchdog_startFileWorker___spec__1(x_4, x_5, x_3);
return x_6;
}
}
lean_object* l_IO_mkRef___at_Lean_Server_Watchdog_startFileWorker___spec__2___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
lean_object* l_IO_mkRef___at_Lean_Server_Watchdog_startFileWorker___spec__1___boxed(lean_object* x_1, lean_object* x_2, lean_object* x_3) {
_start:
{
lean_object* x_4;
x_4 = l_IO_mkRef___at_Lean_Server_Watchdog_startFileWorker___spec__2(x_1, x_2, x_3);
x_4 = l_IO_mkRef___at_Lean_Server_Watchdog_startFileWorker___spec__1(x_1, x_2, x_3);
lean_dec(x_2);
return x_4;
}