sdgoij/lean4
1
0
Fork 0
mirror of https://github.com/leanprover/lean4.git synced 2026-03-17 10:24:07 +00:00
Code Issues Packages Projects Releases Wiki Activity

feat: zero cost BaseIO (#10625)

Browse Source 
This PR implements zero cost `BaseIO` by erasing the `IO.RealWorld`
parameter from argument lists and structures. This is a **major breaking
change for FFI**.

Concretely:
- `BaseIO` is defined in terms of `ST IO.RealWorld`
- `EIO` (and thus `IO`) is defined in terms of `EST IO.RealWorld`
- The opaque `Void` type is introduced and the trivial structure
optimization updated to account for it. Furthermore, arguments of type
`Void s` are removed from the argument lists of the C functions.
- `ST` is redefined as `Void s -> ST.Out s a` where `ST.Out` is a pair
of `Void s` and `a`

This together has the following major effects on our generated code:
- Functions that return `BaseIO`/`ST`/`EIO`/`IO`/`EST` now do not take
the dummy world parameter anymore. To account for this FFI code needs to
delete the dummy world parameter from the argument lists.
- Functions that return `BaseIO`/`ST` now return their wrapped value
directly. In particular `BaseIO UInt32` now returns a `uint32_t` instead
of a `lean_object*`. To account for this FFI code might have to change
the return type and does not need to call `lean_io_result_mk_ok` anymore
but can instead just `return` values right away (same with extracting
values from `BaseIO` computations.
- Functions that return `EIO`/`IO`/`EST` now only return the equivalent
of an `Except` node which reduces the allocation size. The
`lean_io_result_mk_ok`/`lean_io_result_mk_error` functions were updated
to account for this already so no change is required.

Besides improving performance by dropping allocation (sizes) we can now
also do fun new things such as:
```lean
@[extern "malloc"]
opaque malloc (size : USize) : BaseIO USize
```
This commit is contained in:
Henrik Böving
2025-10-22 10:55:12 +02:00
committed by GitHub
parent 6ee8511ae3
commit 52b1b342ab
848 changed files with 1219 additions and 1073 deletions
Download Patch File Download Diff File Expand all files Collapse all files

10
doc/dev/ffi.md
View File

@@ -52,7 +52,7 @@ In the case of `@[extern]` all *irrelevant* types are removed first; see next se
Similarly, the signed integer types `Int8`, ..., `Int64`, `ISize` are also represented by the unsigned C types `uint8_t`, ..., `uint64_t`, `size_t`, respectively, because they have a trivial structure.
* `Nat` and `Int` are represented by `lean_object *`.
Their runtime values is either a pointer to an opaque bignum object or, if the lowest bit of the "pointer" is 1 (`lean_is_scalar`), an encoded unboxed natural number or integer (`lean_box`/`lean_unbox`).
* A universe `Sort u`, type constructor `... → Sort u`, or proposition `p : Prop` is *irrelevant* and is either statically erased (see above) or represented as a `lean_object *` with the runtime value `lean_box(0)`
* A universe `Sort u`, type constructor `... → Sort u`, `Void α` or proposition `p : Prop` is *irrelevant* and is either statically erased (see above) or represented as a `lean_object *` with the runtime value `lean_box(0)`
* Any other type is represented by `lean_object *`.
Its runtime value is a pointer to an object of a subtype of `lean_object` (see the "Inductive types" section below) or the unboxed value `lean_box(cidx)` for the `cidx`th constructor of an inductive type if this constructor does not have any relevant parameters.
@@ -141,8 +141,8 @@ void lean_initialize_runtime_module();
void lean_initialize();
char ** lean_setup_args(int argc, char ** argv);
lean_object * initialize_A_B(uint8_t builtin, lean_object *);
lean_object * initialize_C(uint8_t builtin, lean_object *);
lean_object * initialize_A_B(uint8_t builtin);
lean_object * initialize_C(uint8_t builtin);
...
argv = lean_setup_args(argc, argv); // if using process-related functionality
@@ -152,7 +152,7 @@ lean_initialize_runtime_module();
lean_object * res;
// use same default as for Lean executables
uint8_t builtin = 1;
res = initialize_A_B(builtin, lean_io_mk_world());
res = initialize_A_B(builtin);
if (lean_io_result_is_ok(res)) {
lean_dec_ref(res);
} else {
@@ -160,7 +160,7 @@ if (lean_io_result_is_ok(res)) {
lean_dec(res);
return ...; // do not access Lean declarations if initialization failed
}
res = initialize_C(builtin, lean_io_mk_world());
res = initialize_C(builtin);
if (lean_io_result_is_ok(res)) {
...

25
src/Init/Internal/Order/Basic.lean
View File

@@ -11,7 +11,7 @@ public import Init.System.IO -- for `MonoBind` instance
import all Init.Control.Except -- for `MonoBind` instance
import all Init.Control.StateRef -- for `MonoBind` instance
import all Init.Control.Option -- for `MonoBind` instance
import all Init.System.IO -- for `MonoBind` instance
import all Init.System.ST -- for `MonoBind` instance
public section
@@ -921,16 +921,17 @@ theorem monotone_stateTRun [PartialOrder γ]
monotone (fun (x : γ) => StateT.run (f x) s) :=
monotone_apply s _ hmono
-- TODO: axiomatize these instances (ideally without `Nonempty ε`) when EIO is opaque
noncomputable instance [Nonempty ε] : CCPO (EIO ε α) :=
-- TODO: axiomatize these instances (ideally without `Nonempty ε`) when EIO and friends are opaque
noncomputable instance [Nonempty ε] : CCPO (EST ε σ α) :=
inferInstanceAs (CCPO ((s : _) → FlatOrder (.error Classical.ofNonempty (Classical.choice ⟨s⟩))))
noncomputable instance [Nonempty ε] : MonoBind (EIO ε) where
noncomputable instance [Nonempty ε] : MonoBind (EST ε σ) where
bind_mono_left {_ _ a₁ a₂ f} h₁₂ := by
intro s
specialize h₁₂ s
change FlatOrder.rel (a₁.bind f s) (a₂.bind f s)
simp only [EStateM.bind]
simp only [EST.bind]
generalize a₁ s = a₁ at h₁₂; generalize a₂ s = a₂ at h₁₂
cases h₁₂
· exact .bot
@@ -938,11 +939,23 @@ noncomputable instance [Nonempty ε] : MonoBind (EIO ε) where
bind_mono_right {_ _ a f₁ f₂} h₁₂ := by
intro w
change FlatOrder.rel (a.bind f₁ w) (a.bind f₂ w)
simp only [EStateM.bind]
simp only [EST.bind]
split
· apply h₁₂
· exact .refl
noncomputable instance [Nonempty α] : CCPO (ST σ α) :=
inferInstanceAs (CCPO ((s : _) → FlatOrder (.mk Classical.ofNonempty (Classical.choice ⟨s⟩))))
noncomputable instance [Nonempty α] : CCPO (BaseIO α) :=
inferInstanceAs (CCPO (ST IO.RealWorld α))
noncomputable instance [Nonempty ε] : CCPO (EIO ε α) :=
inferInstanceAs (CCPO (EST ε IO.RealWorld α))
noncomputable instance [Nonempty ε] : MonoBind (EIO ε) :=
inferInstanceAs (MonoBind (EST ε IO.RealWorld))
end mono_bind
section implication_order

19
src/Init/Prelude.lean
View File

@@ -23,6 +23,16 @@ use `PUnit` in the desugaring of `do` notation, or in the pattern match compiler
universe u v w
/-- Marker for information that has been erased by the code generator. -/
unsafe axiom lcErased : Type
/-- Marker for type dependency that has been erased by the code generator. -/
unsafe axiom lcAny : Type
/-- Internal representation of `Void` in the compiler. -/
unsafe axiom lcVoid : Type
/--
The identity function. `id` takes an implicit argument `α : Sort u`
(a type in any universe), and an argument `a : α`, and returns `a`.
@@ -135,15 +145,6 @@ It can be written as an empty tuple: `()`.
-/
@[match_pattern] abbrev Unit.unit : Unit := PUnit.unit
/-- Marker for information that has been erased by the code generator. -/
unsafe axiom lcErased : Type
/-- Marker for type dependency that has been erased by the code generator. -/
unsafe axiom lcAny : Type
/-- Internal representation of `IO.RealWorld` in the compiler. -/
unsafe axiom lcRealWorld : Type
/--
Auxiliary unsafe constant used by the Compiler when erasing proofs from code.

83
src/Init/System/IO.lean
View File

@@ -1,7 +1,7 @@
/-
Copyright (c) 2017 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Luke Nelson, Jared Roesch, Leonardo de Moura, Sebastian Ullrich, Mac Malone
Authors: Luke Nelson, Jared Roesch, Leonardo de Moura, Sebastian Ullrich, Mac Malone, Henrik Böving
-/
module
@@ -15,7 +15,6 @@ public section
open System
opaque IO.RealWorld.nonemptyType : NonemptyType.{0}
/--
A representation of “the real world” that's used in `IO` monads to ensure that `IO` actions are not
reordered.
@@ -25,6 +24,18 @@ reordered.
instance IO.RealWorld.instNonempty : Nonempty IO.RealWorld :=
by exact IO.RealWorld.nonemptyType.property
/--
An `IO` monad that cannot throw exceptions.
-/
@[expose] def BaseIO (α : Type) := ST IO.RealWorld α
instance : Monad BaseIO := inferInstanceAs (Monad (ST IO.RealWorld))
instance : MonadFinally BaseIO := inferInstanceAs (MonadFinally (ST IO.RealWorld))
@[always_inline, inline]
def BaseIO.map (f : α → β) (x : BaseIO α) : BaseIO β :=
f <$> x
/--
A monad that can have side effects on the external world or throw exceptions of type `ε`.
@@ -38,21 +49,7 @@ A monad that can have side effects on the external world or throw exceptions of
def getWorld : IO (IO.RealWorld) := get
```
-/
@[expose] def EIO (ε : Type) : Type → Type := EStateM ε IO.RealWorld
instance : Monad (EIO ε) := inferInstanceAs (Monad (EStateM ε IO.RealWorld))
instance : MonadFinally (EIO ε) := inferInstanceAs (MonadFinally (EStateM ε IO.RealWorld))
instance : MonadExceptOf ε (EIO ε) := inferInstanceAs (MonadExceptOf ε (EStateM ε IO.RealWorld))
instance : OrElse (EIO ε α) := ⟨MonadExcept.orElse⟩
instance [Inhabited ε] : Inhabited (EIO ε α) := inferInstanceAs (Inhabited (EStateM ε IO.RealWorld α))
/--
An `IO` monad that cannot throw exceptions.
-/
@[expose] def BaseIO := EIO Empty
instance : Monad BaseIO := inferInstanceAs (Monad (EIO Empty))
instance : MonadFinally BaseIO := inferInstanceAs (MonadFinally (EIO Empty))
@[expose] def EIO (ε : Type) (α : Type) : Type := EST ε IO.RealWorld α
/--
Runs a `BaseIO` action, which cannot throw an exception, in any other `EIO` monad.
@@ -63,7 +60,7 @@ lifting](lean-manual://section/lifting-monads) rather being than called explicit
@[always_inline, inline]
def BaseIO.toEIO (act : BaseIO α) : EIO ε α :=
fun s => match act s with
| EStateM.Result.ok a s => EStateM.Result.ok a s
| .mk a s => .ok a s
instance : MonadLift BaseIO (EIO ε) := ⟨BaseIO.toEIO⟩
@@ -74,8 +71,8 @@ action that returns an `Except` value.
@[always_inline, inline]
def EIO.toBaseIO (act : EIO ε α) : BaseIO (Except ε α) :=
fun s => match act s with
| EStateM.Result.ok a s => EStateM.Result.ok (Except.ok a) s
| EStateM.Result.error ex s => EStateM.Result.ok (Except.error ex) s
| .ok a s => .mk (.ok a) s
| .error ex s => .mk (.error ex) s
/--
Handles any exception that might be thrown by an `EIO ε` action, transforming it into an
@@ -84,8 +81,25 @@ exception-free `BaseIO` action.
@[always_inline, inline]
def EIO.catchExceptions (act : EIO ε α) (h : ε → BaseIO α) : BaseIO α :=
fun s => match act s with
| EStateM.Result.ok a s => EStateM.Result.ok a s
| EStateM.Result.error ex s => h ex s
| .ok a s => .mk a s
| .error ex s => h ex s
instance : Monad (EIO ε) := inferInstanceAs (Monad (EST ε IO.RealWorld))
instance : MonadFinally (EIO ε) := inferInstanceAs (MonadFinally (EST ε IO.RealWorld))
instance : MonadExceptOf ε (EIO ε) := inferInstanceAs (MonadExceptOf ε (EST ε IO.RealWorld))
instance : OrElse (EIO ε α) := ⟨MonadExcept.orElse⟩
instance [Inhabited ε] : Inhabited (EIO ε α) := inferInstanceAs (Inhabited (EST ε IO.RealWorld α))
@[always_inline, inline]
def EIO.map (f : α → β) (x : EIO ε α) : EIO ε β :=
f <$> x
@[always_inline, inline]
protected def EIO.throw (e : ε) : EIO ε α := throw e
@[always_inline, inline]
protected def EIO.tryCatch (x : EIO ε α) (handle : ε → EIO ε α) : EIO ε α :=
MonadExceptOf.tryCatch x handle
/--
Converts an `Except ε` action into an `EIO ε` action.
@@ -93,11 +107,21 @@ Converts an `Except ε` action into an `EIO ε` action.
If the `Except ε` action throws an exception, then the resulting `EIO ε` action throws the same
exception. Otherwise, the value is returned.
-/
@[always_inline, inline]
def EIO.ofExcept (e : Except ε α) : EIO ε α :=
match e with
| Except.ok a => pure a
| Except.error e => throw e
@[always_inline, inline]
def EIO.adapt (f : ε → ε') (m : EIO ε α) : EIO ε' α :=
fun s => match m s with
| .ok a s => .ok a s
| .error e s => .error (f e) s
@[deprecated EIO.adapt (since := "2025-09-29"), always_inline, inline]
def EIO.adaptExcept (f : ε → ε') (m : EIO ε α) : EIO ε' α := EIO.adapt f m
open IO (Error) in
/--
A monad that supports arbitrary side effects and throwing exceptions of type `IO.Error`.
@@ -118,7 +142,7 @@ Converts an `EIO ε` action into an `IO` action by translating any exceptions th
`IO.Error`s using `f`.
-/
@[inline] def EIO.toIO (f : ε → IO.Error) (act : EIO ε α) : IO α :=
act.adaptExcept f
act.adapt f
/--
Converts an `EIO ε` action that might throw an exception of type `ε` into an exception-free `IO`
@@ -131,7 +155,7 @@ action that returns an `Except` value.
Runs an `IO` action in some other `EIO` monad, using `f` to translate `IO` exceptions.
-/
@[inline] def IO.toEIO (f : IO.Error → ε) (act : IO α) : EIO ε α :=
act.adaptExcept f
act.adapt f
/- After we inline `EState.run'`, the closed term `((), ())` is generated, where the second `()`
represents the "initial world". We don't want to cache this closed term. So, we disable
@@ -151,8 +175,8 @@ duplicate, or delete calls to this function. The side effect may even be hoisted
causing the side effect to occur at initialization time, even if it would otherwise never be called.
-/
@[noinline] unsafe def unsafeBaseIO (fn : BaseIO α) : α :=
match fn.run (unsafeCast Unit.unit) with
| EStateM.Result.ok a _ => a
match fn (unsafeCast Unit.unit) with
| .mk a _ => a
/--
Executes arbitrary side effects in a pure context, with exceptions indicated via `Except`. This a
@@ -397,7 +421,7 @@ Pauses execution for the specified number of milliseconds.
-/
opaque sleep (ms : UInt32) : BaseIO Unit :=
-- TODO: add a proper primitive for IO.sleep
fun s => dbgSleep ms fun _ => EStateM.Result.ok () s
fun s => dbgSleep ms fun _ => .mk () s
/--
Runs `act` in a separate `Task`, with priority `prio`. Because `IO` actions may throw an exception
@@ -1606,7 +1630,10 @@ the `IO` monad.
-/
abbrev Ref (α : Type) := ST.Ref IO.RealWorld α
instance : MonadLift (ST IO.RealWorld) BaseIO := ⟨id⟩
instance : MonadLift (ST IO.RealWorld) BaseIO where
monadLift mx := fun s =>
match mx s with
| .mk s a => .mk s a
/--
Creates a new mutable reference cell that contains `a`.

123
src/Init/System/ST.lean
View File

@@ -12,24 +12,112 @@ public import Init.Control.Reader
public section
/--
A restricted version of `IO` in which mutable state and exceptions are the only side effects.
opaque Void.nonemptyType (σ : Type) : NonemptyType.{0}
It is possible to run `EST` computations in a non-monadic context using `runEST`.
-/
@[expose] def EST (ε : Type) (σ : Type) : Type → Type := EStateM ε σ
@[expose] def Void (σ : Type) : Type := Void.nonemptyType σ |>.type
instance Void.instNonempty : Nonempty (Void σ) :=
by exact (Void.nonemptyType σ).property
@[extern "lean_void_mk"]
opaque Void.mk (x : σ) : Void σ
structure ST.Out (σ : Type) (α : Type) where
val : α
state : Void σ
/--
A restricted version of `IO` in which mutable state is the only side effect.
It is possible to run `ST` computations in a non-monadic context using `runST`.
-/
abbrev ST (σ : Type) := EST Empty σ
abbrev ST (σ : Type) (α : Type) := Void σ → ST.Out σ α
instance (ε σ : Type) : Monad (EST ε σ) := inferInstanceAs (Monad (EStateM _ _))
instance (ε σ : Type) : MonadExceptOf ε (EST ε σ) := inferInstanceAs (MonadExceptOf ε (EStateM _ _))
instance {ε σ : Type} {α : Type} [Inhabited ε] : Inhabited (EST ε σ α) := inferInstanceAs (Inhabited (EStateM _ _ _))
instance (σ : Type) : Monad (ST σ) := inferInstanceAs (Monad (EST _ _))
namespace ST
@[always_inline, inline]
protected def pure (x : α) : ST σ α := fun s => .mk x s
@[always_inline, inline]
protected def bind (x : ST σ α) (f : α → ST σ β) : ST σ β :=
fun s =>
match x s with
| .mk x s => f x s
end ST
instance (σ : Type) : Monad (ST σ) where
pure := ST.pure
bind := ST.bind
@[always_inline]
instance : MonadFinally (ST σ) where
tryFinally' x f := fun s =>
match x s with
| .mk x s =>
match f (some x) s with
| .mk y s => .mk (x, y) s
instance {σ : Type} {α : Type} [Inhabited α] : Inhabited (ST σ α) where
default := fun s => .mk default s
inductive EST.Out (ε : Type) (σ : Type) (α : Type) where
| ok : α → Void σ → EST.Out ε σ α
| error : ε → Void σ → EST.Out ε σ α
/--
A restricted version of `IO` in which mutable state and exceptions are the only side effects.
It is possible to run `EST` computations in a non-monadic context using `runEST`.
-/
@[expose] def EST (ε : Type) (σ : Type) (α : Type) : Type := Void σ → EST.Out ε σ α
namespace EST
@[always_inline, inline]
protected def pure (a : α) : EST ε σ α := fun s => .ok a s
@[always_inline, inline]
protected def bind (x : EST ε σ α) (f : α → EST ε σ β) : EST ε σ β :=
fun s => match x s with
| .ok a s => f a s
| .error e s => .error e s
@[always_inline, inline]
protected def throw (e : ε) : EST ε σ α := fun s => .error e s
@[always_inline, inline]
protected def tryCatch (x : EST ε σ α) (handle : ε → EST ε σ α) : EST ε σ α :=
fun s => match x s with
| .ok a s => .ok a s
| .error e s => handle e s
end EST
instance (ε σ : Type) : Monad (EST ε σ) where
pure := EST.pure
bind := EST.bind
@[always_inline]
instance : MonadFinally (EST ε σ) where
tryFinally' x f := fun s =>
let r := x s
match r with
| .ok x s =>
match f (some x) s with
| .ok y s => .ok (x, y) s
| .error e s => .error e s
| .error e s =>
match f none s with
| .ok _ s => .error e s
| .error e s => .error e s
instance (ε σ : Type) : MonadExceptOf ε (EST ε σ) where
throw := EST.throw
tryCatch := EST.tryCatch
instance {ε σ : Type} {α : Type} [Inhabited ε] : Inhabited (EST ε σ α) where
default := fun s => .error default s
/--
An auxiliary class used to infer the “state” of `EST` and `ST` monads.
@@ -37,6 +125,7 @@ An auxiliary class used to infer the “state” of `EST` and `ST` monads.
class STWorld (σ : outParam Type) (m : Type → Type)
instance {σ m n} [MonadLift m n] [STWorld σ m] : STWorld σ n := ⟨⟩
instance {σ} : STWorld σ (ST σ) := ⟨⟩
instance {ε σ} : STWorld σ (EST ε σ) := ⟨⟩
/--
@@ -44,24 +133,22 @@ Runs an `EST` computation, in which mutable state and exceptions are the only si
-/
@[noinline, nospecialize]
def runEST {ε α : Type} (x : (σ : Type) → EST ε σ α) : Except ε α :=
match x Unit () with
| EStateM.Result.ok a _ => Except.ok a
| EStateM.Result.error ex _ => Except.error ex
match x Unit (Void.mk ()) with
| .ok a _ => Except.ok a
| .error ex _ => Except.error ex
/--
Runs an `ST` computation, in which mutable state via `ST.Ref` is the only side effect.
-/
@[noinline, nospecialize]
def runST {α : Type} (x : (σ : Type) → ST σ α) : α :=
match x Unit () with
| EStateM.Result.ok a _ => a
| EStateM.Result.error ex _ => nomatch ex
match x Unit (Void.mk ()) with
| .mk a _ => a
@[always_inline]
instance {ε σ} : MonadLift (ST σ) (EST ε σ) := ⟨fun x s =>
match x s with
| EStateM.Result.ok a s => EStateM.Result.ok a s
| EStateM.Result.error ex _ => nomatch ex⟩
| .mk a s => .ok a s⟩
namespace ST

11
src/Lean/Compiler/IR/Basic.lean
View File

@@ -51,6 +51,9 @@ instance : ToString JoinPointId := ⟨fun a => "block_" ++ toString a.idx⟩
- `tobject` an `object` or a `tagged` pointer
- `void` is used to identify uses of the state token from `BaseIO` which do no longer need
to be passed around etc. at this point in the pipeline.
- `struct` and `union` are used to return small values (e.g., `Option`, `Prod`, `Except`)
on the stack.
@@ -78,6 +81,7 @@ inductive IRType where
| union (leanTypeName : Name) (types : Array IRType) : IRType
-- TODO: Move this upwards after a stage0 update.
| tagged
| void
deriving Inhabited, BEq, Repr
namespace IRType
@@ -96,6 +100,7 @@ def isObj : IRType → Bool
| object => true
| tagged => true
| tobject => true
| void => true
| _ => false
def isPossibleRef : IRType → Bool
@@ -110,9 +115,13 @@ def isErased : IRType → Bool
| erased => true
| _ => false
def isVoid : IRType → Bool
| void => true
| _ => false
def boxed : IRType → IRType
| object | float | float32 => object
| tagged | uint8 | uint16 => tagged
| void | tagged | uint8 | uint16 => tagged
| _ => tobject
end IRType

2
src/Lean/Compiler/IR/Boxing.lean
View File

@@ -39,7 +39,7 @@ private def N.mkFresh : N VarId :=
def requiresBoxedVersion (env : Environment) (decl : Decl) : Bool :=
let ps := decl.params
(ps.size > 0 && (decl.resultType.isScalar || ps.any (fun p => p.ty.isScalar || p.borrow) || isExtern env decl.name))
(ps.size > 0 && (decl.resultType.isScalar || ps.any (fun p => p.ty.isScalar || p.borrow || p.ty.isVoid) || isExtern env decl.name))
|| ps.size > closureMaxArgs
def mkBoxedVersionAux (decl : Decl) : N Decl := do

38
src/Lean/Compiler/IR/EmitC.lean
View File

@@ -65,6 +65,7 @@ def toCType : IRType → String
| IRType.tagged => "lean_object*"
| IRType.tobject => "lean_object*"
| IRType.erased => "lean_object*"
| IRType.void => "lean_object*"
| IRType.struct _ _ => panic! "not implemented yet"
| IRType.union _ _ => panic! "not implemented yet"
@@ -105,6 +106,8 @@ def emitFnDeclAux (decl : Decl) (cppBaseName : String) (isExternal : Bool) : M U
emit (toCType decl.resultType ++ " " ++ cppBaseName)
unless ps.isEmpty do
emit "("
-- We omit void parameters, note that they are guaranteed not to occur in boxed functions
let ps := ps.filter (fun p => !p.ty.isVoid)
-- We omit erased parameters for extern constants
let ps := if isExternC env decl.name then ps.filter (fun p => !p.ty.isErased) else ps
if ps.size > closureMaxArgs && isBoxedName decl.name then
@@ -169,7 +172,7 @@ def emitMainFn : M Unit := do
/- We disable panic messages because they do not mesh well with extracted closed terms.
See issue #534. We can remove this workaround after we implement issue #467. -/
emitLn "lean_set_panic_messages(false);"
emitLn ("res = " ++ mkModuleInitializationFunctionName modName ++ "(1 /* builtin */, lean_io_mk_world());")
emitLn ("res = " ++ mkModuleInitializationFunctionName modName ++ "(1 /* builtin */);")
emitLn "lean_set_panic_messages(true);"
emitLns ["lean_io_mark_end_initialization();",
"if (lean_io_result_is_ok(res)) {",
@@ -184,9 +187,9 @@ def emitMainFn : M Unit := do
" n = lean_alloc_ctor(1,2,0); lean_ctor_set(n, 0, lean_mk_string(argv[i])); lean_ctor_set(n, 1, in);",
" in = n;",
"}"]
emitLn ("res = " ++ leanMainFn ++ "(in, lean_io_mk_world());")
emitLn ("res = " ++ leanMainFn ++ "(in);")
else
emitLn ("res = " ++ leanMainFn ++ "(lean_io_mk_world());")
emitLn ("res = " ++ leanMainFn ++ "();")
emitLn "}"
-- `IO _`
let retTy := env.find? `main |>.get! |>.type |>.getForallBody
@@ -409,7 +412,8 @@ def emitSimpleExternalCall (f : String) (ps : Array Param) (ys : Array Arg) : M
-- We must remove erased arguments to extern calls.
discard <| ys.size.foldM
(fun i _ (first : Bool) =>
if ps[i]!.ty.isErased then
let ty := ps[i]!.ty
if ty.isErased || ty.isVoid then
pure first
else do
unless first do emit ", "
@@ -429,9 +433,11 @@ def emitFullApp (z : VarId) (f : FunId) (ys : Array Arg) : M Unit := do
emitLhs z
let decl ← getDecl f
match decl with
| .fdecl .. | .extern _ _ _ { entries := [.opaque _], .. } =>
| .fdecl (xs := ps) .. | .extern (xs := ps) (ext := { entries := [.opaque _], .. }) .. =>
emitCName f
if ys.size > 0 then emit "("; emitArgs ys; emit ")"
if ys.size > 0 then
let (ys, _) := ys.zip ps |>.filter (fun (_, p) => !p.ty.isVoid) |>.unzip
emit "("; emitArgs ys; emit ")"
emitLn ";"
| Decl.extern _ ps _ extData => emitExternCall f ps extData ys
@@ -571,22 +577,23 @@ def emitTailCall (v : Expr) : M Unit :=
let ctx ← read
let ps := ctx.mainParams
if h : ps.size = ys.size then
let (ps, ys) := ps.zip ys |>.filter (fun (p, _) => !p.ty.isVoid) |>.unzip
if overwriteParam ps ys then
emitLn "{"
ps.size.forM fun i _ => do
let p := ps[i]
let y := ys[i]
let y := ys[i]!
unless paramEqArg p y do
emit (toCType p.ty); emit " _tmp_"; emit i; emit " = "; emitArg y; emitLn ";"
ps.size.forM fun i _ => do
let p := ps[i]
let y := ys[i]
let y := ys[i]!
unless paramEqArg p y do emit p.x; emit " = _tmp_"; emit i; emitLn ";"
emitLn "}"
else
ys.size.forM fun i _ => do
ps.size.forM fun i _ => do
let p := ps[i]
let y := ys[i]
let y := ys[i]!
unless paramEqArg p y do emit p.x; emit " = "; emitArg y; emitLn ";"
emitLn "goto _start;"
else
@@ -667,6 +674,7 @@ def emitDeclAux (d : Decl) : M Unit := do
emit "LEAN_EXPORT " -- make symbol visible to the interpreter
emit (toCType t); emit " ";
if xs.size > 0 then
let xs := xs.filter (fun p => !p.ty.isVoid)
emit baseName;
emit "(";
if xs.size > closureMaxArgs && isBoxedName d.name then
@@ -713,7 +721,7 @@ def emitDeclInit (d : Decl) : M Unit := do
if isIOUnitInitFn env n then
if isIOUnitBuiltinInitFn env n then
emit "if (builtin) {"
emit "res = "; emitCName n; emitLn "(lean_io_mk_world());"
emit "res = "; emitCName n; emitLn "();"
emitLn "if (lean_io_result_is_error(res)) return res;"
emitLn "lean_dec_ref(res);"
if isIOUnitBuiltinInitFn env n then
@@ -723,7 +731,7 @@ def emitDeclInit (d : Decl) : M Unit := do
| some initFn =>
if getBuiltinInitFnNameFor? env d.name |>.isSome then
emit "if (builtin) {"
emit "res = "; emitCName initFn; emitLn "(lean_io_mk_world());"
emit "res = "; emitCName initFn; emitLn "();"
emitLn "if (lean_io_result_is_error(res)) return res;"
emitCName n
if d.resultType.isScalar then
@@ -740,16 +748,16 @@ def emitDeclInit (d : Decl) : M Unit := do
def emitInitFn : M Unit := do
let env ← getEnv
let modName ← getModName
env.imports.forM fun imp => emitLn ("lean_object* " ++ mkModuleInitializationFunctionName imp.module ++ "(uint8_t builtin, lean_object*);")
env.imports.forM fun imp => emitLn ("lean_object* " ++ mkModuleInitializationFunctionName imp.module ++ "(uint8_t builtin);")
emitLns [
"static bool _G_initialized = false;",
"LEAN_EXPORT lean_object* " ++ mkModuleInitializationFunctionName modName ++ "(uint8_t builtin, lean_object* w) {",
"LEAN_EXPORT lean_object* " ++ mkModuleInitializationFunctionName modName ++ "(uint8_t builtin) {",
"lean_object * res;",
"if (_G_initialized) return lean_io_result_mk_ok(lean_box(0));",
"_G_initialized = true;"
]
env.imports.forM fun imp => emitLns [
"res = " ++ mkModuleInitializationFunctionName imp.module ++ "(builtin, lean_io_mk_world());",
"res = " ++ mkModuleInitializationFunctionName imp.module ++ "(builtin);",
"if (lean_io_result_is_error(res)) return res;",
"lean_dec_ref(res);"]
let decls := getDecls env

13
src/Lean/Compiler/IR/EmitLLVM.lean
View File

@@ -19,6 +19,18 @@ public section
open Lean.IR.ExplicitBoxing (isBoxedName)
namespace Lean.IR
/-
TODO: At the time of writing this our CI for LLVM is dysfunctional so this code is not actually
tested. When we get back to fixing it we need to account for changes made to the ABI in the mean
time. These changes can likely be done similar to the ones in EmitC:
- IO.RealWorld elimination:
- init functions don't take a real world parameter anymore
- parameters that are `void` are erased and do not appear in function signatures or call sites
anymore. This means in particular:
- function decls need to be fixed
- full applications need to be fixed
- tail calls need to be fixed
-/
def leanMainFn := "_lean_main"
@@ -325,6 +337,7 @@ def toLLVMType (t : IRType) : M llvmctx (LLVM.LLVMType llvmctx) := do
| IRType.tagged => do LLVM.pointerType (← LLVM.i8Type llvmctx)
| IRType.tobject => do LLVM.pointerType (← LLVM.i8Type llvmctx)
| IRType.erased => do LLVM.pointerType (← LLVM.i8Type llvmctx)
| IRType.void => do LLVM.pointerType (← LLVM.i8Type llvmctx)
| IRType.struct _ _ => panic! "not implemented yet"
| IRType.union _ _ => panic! "not implemented yet"

1
src/Lean/Compiler/IR/Format.lean
View File

@@ -66,6 +66,7 @@ private partial def formatIRType : IRType → Format
| IRType.uint64 => "u64"
| IRType.usize => "usize"
| IRType.erased => "◾"
| IRType.void => "void"
| IRType.object => "obj"
| IRType.tagged => "tagged"
| IRType.tobject => "tobj"

162
src/Lean/Compiler/IR/ToIR.lean
View File

@@ -14,7 +14,8 @@ public section
namespace Lean.IR
open Lean.Compiler (LCNF.Alt LCNF.Arg LCNF.Code LCNF.Decl LCNF.DeclValue LCNF.LCtx LCNF.LetDecl
LCNF.LetValue LCNF.LitValue LCNF.Param LCNF.getMonoDecl?)
LCNF.LetValue LCNF.LitValue LCNF.Param LCNF.getMonoDecl? LCNF.FVarSubst LCNF.MonadFVarSubst
LCNF.MonadFVarSubstState LCNF.addSubst LCNF.normLetValue LCNF.normFVar)
namespace ToIR
@@ -22,14 +23,32 @@ structure BuilderState where
vars : Std.HashMap FVarId Arg := {}
joinPoints : Std.HashMap FVarId JoinPointId := {}
nextId : Nat := 1
/--
We keep around a substitution here because we run a second trivial structure elimination when
converting to IR. This elimination is aware of the fact that `Void` is irrelevant while the first
one in LCNF isn't because LCNF is still pure. However, IR does not allow us to have bindings of
the form `let x := y` which might occur when for example projecting out of a trivial structure
where previously a binding would've been `let x := proj y i` and now becomes `let x := y`.
For this reason we carry around these kinds of bindings in this substitution and apply it whenever
we access an fvar in the conversion.
-/
subst : LCNF.FVarSubst := {}
abbrev M := StateRefT BuilderState CoreM
instance : LCNF.MonadFVarSubst M false where
getSubst := return (← get).subst
instance : LCNF.MonadFVarSubstState M where
modifySubst f := modify fun s => { s with subst := f s.subst }
def M.run (x : M α) : CoreM α := do
x.run' {}
def getFVarValue (fvarId : FVarId) : M Arg := do
return (← get).vars.get! fvarId
match ← LCNF.normFVar fvarId with
| .fvar fvarId => return (← get).vars.get! fvarId
| .erased => return .erased
def getJoinPointValue (fvarId : FVarId) : M JoinPointId := do
return (← get).joinPoints.get! fvarId
@@ -92,10 +111,13 @@ def lowerProj (base : VarId) (ctorInfo : CtorInfo) (field : CtorFieldInfo)
| .usize i => ⟨.expr (.uproj i base), .usize⟩
| .scalar _ offset irType => ⟨.expr (.sproj (ctorInfo.size + ctorInfo.usize) offset base), irType⟩
| .erased => ⟨.erased, .erased⟩
| .void => ⟨.erased, .void⟩
def lowerParam (p : LCNF.Param) : M Param := do
let x ← bindVar p.fvarId
let ty ← toIRType p.type
if ty.isVoid || ty.isErased then
Compiler.LCNF.addSubst p.fvarId .erased
return { x, borrow := p.borrow, ty }
mutual
@@ -111,40 +133,61 @@ partial def lowerCode (c : LCNF.Code) : M FnBody := do
let joinPointId ← getJoinPointValue fvarId
return .jmp joinPointId (← args.mapM lowerArg)
| .cases cases =>
-- `casesOn` for inductive predicates should have already been expanded.
let .var varId := (← getFVarValue cases.discr) | unreachable!
return .case cases.typeName
varId
(← nameToIRType cases.typeName)
(← cases.alts.mapM (lowerAlt varId))
if let some info ← hasTrivialStructure? cases.typeName then
assert! cases.alts.size == 1
let .alt ctorName ps k := cases.alts[0]! | unreachable!
assert! ctorName == info.ctorName
assert! info.fieldIdx < ps.size
for idx in 0...ps.size do
let p := ps[idx]!
if idx == info.fieldIdx then
LCNF.addSubst p.fvarId (.fvar cases.discr)
else
bindErased p.fvarId
lowerCode k
else
-- `casesOn` for inductive predicates should have already been expanded.
let .var varId := (← getFVarValue cases.discr) | unreachable!
return .case cases.typeName
varId
(← nameToIRType cases.typeName)
(← cases.alts.mapM (lowerAlt varId))
| .return fvarId =>
return .ret (← getFVarValue fvarId)
| .unreach .. => return .unreachable
| .fun .. => panic! "all local functions should be λ-lifted"
partial def lowerLet (decl : LCNF.LetDecl) (k : LCNF.Code) : M FnBody := do
match decl.value with
let value ← LCNF.normLetValue decl.value
match value with
| .lit litValue =>
let var ← bindVar decl.fvarId
let ⟨litValue, type⟩ := lowerLitValue litValue
return .vdecl var type (.lit litValue) (← lowerCode k)
| .proj typeName i fvarId =>
match (← getFVarValue fvarId) with
| .var varId =>
let some (.inductInfo { ctors := [ctorName], .. }) := (← Lean.getEnv).find? typeName
| panic! "projection of non-structure type"
let ⟨ctorInfo, fields⟩ ← getCtorLayout ctorName
let ⟨result, type⟩ := lowerProj varId ctorInfo fields[i]!
match result with
| .expr e =>
let var ← bindVar decl.fvarId
return .vdecl var type e (← lowerCode k)
if let some info ← hasTrivialStructure? typeName then
if info.fieldIdx == i then
LCNF.addSubst decl.fvarId (.fvar fvarId)
else
bindErased decl.fvarId
lowerCode k
else
match (← getFVarValue fvarId) with
| .var varId =>
let some (.inductInfo { ctors := [ctorName], .. }) := (← Lean.getEnv).find? typeName
| panic! "projection of non-structure type"
let ⟨ctorInfo, fields⟩ ← getCtorLayout ctorName
let ⟨result, type⟩ := lowerProj varId ctorInfo fields[i]!
match result with
| .expr e =>
let var ← bindVar decl.fvarId
return .vdecl var type e (← lowerCode k)
| .erased =>
bindErased decl.fvarId
lowerCode k
| .erased =>
bindErased decl.fvarId
lowerCode k
| .erased =>
bindErased decl.fvarId
lowerCode k
| .const name _ args =>
let irArgs ← args.mapM lowerArg
if let some decl ← findDecl name then
@@ -154,43 +197,48 @@ partial def lowerLet (decl : LCNF.LetDecl) (k : LCNF.Code) : M FnBody := do
let env ← Lean.getEnv
match env.find? name with
| some (.ctorInfo ctorVal) =>
let type ← nameToIRType ctorVal.induct
if type.isScalar then
let var ← bindVar decl.fvarId
return .vdecl var type (.lit (.num ctorVal.cidx)) (← lowerCode k)
if let some info ← hasTrivialStructure? ctorVal.induct then
let arg := args[info.numParams + info.fieldIdx]!
LCNF.addSubst decl.fvarId arg
lowerCode k
else
let type ← nameToIRType ctorVal.induct
if type.isScalar then
let var ← bindVar decl.fvarId
return .vdecl var type (.lit (.num ctorVal.cidx)) (← lowerCode k)
let ⟨ctorInfo, fields⟩ ← getCtorLayout name
let irArgs := irArgs.extract (start := ctorVal.numParams)
if irArgs.size != fields.size then
-- An overapplied constructor arises from compiler
-- transformations on unreachable code
return .unreachable
let ⟨ctorInfo, fields⟩ ← getCtorLayout name
let irArgs := irArgs.extract (start := ctorVal.numParams)
if irArgs.size != fields.size then
-- An overapplied constructor arises from compiler
-- transformations on unreachable code
return .unreachable
let objArgs : Array Arg ← do
let mut result : Array Arg := #[]
for h : i in *...fields.size do
match fields[i] with
| .object .. =>
result := result.push irArgs[i]!
| .usize .. | .scalar .. | .erased => pure ()
pure result
let objVar ← bindVar decl.fvarId
let rec lowerNonObjectFields (_ : Unit) : M FnBody :=
let rec loop (i : Nat) : M FnBody := do
match irArgs[i]? with
| some (.var varId) =>
match fields[i]! with
| .usize usizeIdx =>
let k ← loop (i + 1)
return .uset objVar usizeIdx varId k
| .scalar _ offset argType =>
let k ← loop (i + 1)
return .sset objVar (ctorInfo.size + ctorInfo.usize) offset varId argType k
| .object .. | .erased => loop (i + 1)
| some .erased => loop (i + 1)
| none => lowerCode k
loop 0
return .vdecl objVar ctorInfo.type (.ctor ctorInfo objArgs) (← lowerNonObjectFields ())
let objArgs : Array Arg ← do
let mut result : Array Arg := #[]
for h : i in *...fields.size do
match fields[i] with
| .object .. =>
result := result.push irArgs[i]!
| .usize .. | .scalar .. | .erased | .void => pure ()
pure result
let objVar ← bindVar decl.fvarId
let rec lowerNonObjectFields (_ : Unit) : M FnBody :=
let rec loop (i : Nat) : M FnBody := do
match irArgs[i]? with
| some (.var varId) =>
match fields[i]! with
| .usize usizeIdx =>
let k ← loop (i + 1)
return .uset objVar usizeIdx varId k
| .scalar _ offset argType =>
let k ← loop (i + 1)
return .sset objVar (ctorInfo.size + ctorInfo.usize) offset varId argType k
| .object .. | .erased | .void => loop (i + 1)
| some .erased => loop (i + 1)
| none => lowerCode k
loop 0
return .vdecl objVar ctorInfo.type (.ctor ctorInfo objArgs) (← lowerNonObjectFields ())
| some (.defnInfo ..) | some (.opaqueInfo ..) =>
mkFap name irArgs
| some (.axiomInfo ..) | .some (.quotInfo ..) | .some (.inductInfo ..) | .some (.thmInfo ..) =>

44
src/Lean/Compiler/IR/ToIRType.lean
View File

@@ -14,7 +14,9 @@ public section
namespace Lean
namespace IR
open Lean.Compiler (LCNF.CacheExtension LCNF.isTypeFormerType LCNF.toLCNFType LCNF.toMonoType)
open Lean.Compiler (LCNF.CacheExtension LCNF.isTypeFormerType LCNF.toLCNFType LCNF.toMonoType
LCNF.TrivialStructureInfo LCNF.getOtherDeclBaseType LCNF.getParamTypes LCNF.instantiateForall
LCNF.Irrelevant.hasTrivialStructure?)
def irTypeForEnum (numCtors : Nat) : IRType :=
if numCtors == 1 then
@@ -31,6 +33,23 @@ def irTypeForEnum (numCtors : Nat) : IRType :=
builtin_initialize irTypeExt : LCNF.CacheExtension Name IRType ←
LCNF.CacheExtension.register
builtin_initialize trivialStructureInfoExt :
LCNF.CacheExtension Name (Option LCNF.TrivialStructureInfo) ←
LCNF.CacheExtension.register
/--
The idea of this function is the same as in `ToMono`, however the notion of "irrelevancy" has
changed because we now have the `void` type which can only be erased in impure context and thus at
earliest at the conversion from mono to IR.
-/
def hasTrivialStructure? (declName : Name) : CoreM (Option LCNF.TrivialStructureInfo) := do
let isVoidType type := do
let type ← Meta.whnfD type
return type matches .proj ``Subtype 0 (.app (.const ``Void.nonemptyType []) _)
let irrelevantType type :=
Meta.isProp type <||> Meta.isTypeFormerType type <||> isVoidType type
LCNF.Irrelevant.hasTrivialStructure? trivialStructureInfoExt irrelevantType declName
def nameToIRType (name : Name) : CoreM IRType := do
match (← irTypeExt.find? name) with
| some type => return type
@@ -51,7 +70,7 @@ where fillCache : CoreM IRType := do
-- `Int` is specified as an inductive type with two constructors that have relevant arguments,
-- but it has the same runtime representation as `Nat` and thus needs to be special-cased here.
| ``Int => return .tobject
| ``lcRealWorld => return .tagged
| ``lcVoid => return .void
| _ =>
let env ← Lean.getEnv
let some (.inductInfo inductiveVal) := env.find? name | return .tobject
@@ -83,13 +102,13 @@ private def isAnyProducingType (type : Lean.Expr) : Bool :=
| .forallE _ _ b _ => isAnyProducingType b
| _ => false
def toIRType (type : Lean.Expr) : CoreM IRType := do
partial def toIRType (type : Lean.Expr) : CoreM IRType := do
match type with
| .const name _ => nameToIRType name
| .const name _ => visitApp name #[]
| .app .. =>
-- All mono types are in headBeta form.
let .const name _ := type.getAppFn | unreachable!
nameToIRType name
visitApp name type.getAppArgs
| .forallE _ _ b _ =>
-- Type formers are erased, but can be used polymorphically as
-- an arrow type producing `lcAny`. The runtime representation of
@@ -101,18 +120,28 @@ def toIRType (type : Lean.Expr) : CoreM IRType := do
return .object
| .mdata _ b => toIRType b
| _ => unreachable!
where
visitApp (declName : Name) (args : Array Lean.Expr) : CoreM IRType := do
if let some info ← hasTrivialStructure? declName then
let ctorType ← LCNF.getOtherDeclBaseType info.ctorName []
let monoType ← LCNF.toMonoType (LCNF.getParamTypes (← LCNF.instantiateForall ctorType args[*...info.numParams]))[info.fieldIdx]!
toIRType monoType
else
nameToIRType declName
inductive CtorFieldInfo where
| erased
| object (i : Nat) (type : IRType)
| usize (i : Nat)
| scalar (sz : Nat) (offset : Nat) (type : IRType)
| void
deriving Inhabited
namespace CtorFieldInfo
def format : CtorFieldInfo → Format
| erased => "◾"
| void => "void"
| object i type => f!"obj@{i}:{type}"
| usize i => f!"usize@{i}"
| scalar sz offset type => f!"scalar#{sz}@{offset}:{type}"
@@ -157,6 +186,7 @@ where fillCache := do
pure <| .object i irFieldType
| .usize => pure <| .usize 0
| .erased => .pure <| .erased
| .void => .pure <| .void
| .uint8 =>
has1BScalar := true
.pure <| .scalar 1 0 .uint8
@@ -183,7 +213,7 @@ where fillCache := do
| .usize _ => do
let i ← modifyGet fun nextIdx => (nextIdx, nextIdx + 1)
return .usize i
| .object .. | .scalar .. | .erased => return field
| .object .. | .scalar .. | .erased | .void => return field
let numUSize := nextIdx - numObjs
let adjustScalarsForSize (fields : Array CtorFieldInfo) (size : Nat) (nextOffset : Nat)
: Array CtorFieldInfo × Nat :=
@@ -195,7 +225,7 @@ where fillCache := do
return .scalar sz offset type
else
return field
| .object .. | .usize _ | .erased => return field
| .object .. | .usize _ | .erased | .void => return field
let mut nextOffset := 0
if has8BScalar then
⟨fields, nextOffset⟩ := adjustScalarsForSize fields 8 nextOffset

1
src/Lean/Compiler/LCNF.lean
View File

@@ -44,3 +44,4 @@ public import Lean.Compiler.LCNF.Closure
public import Lean.Compiler.LCNF.LambdaLifting
public import Lean.Compiler.LCNF.ReduceArity
public import Lean.Compiler.LCNF.Probing
public import Lean.Compiler.LCNF.Irrelevant

71
src/Lean/Compiler/LCNF/Irrelevant.lean Normal file
View File

@@ -0,0 +1,71 @@
/-
Copyright (c) 2025 Lean FRO, LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Henrik Böving
-/
module
prelude
public import Lean.Compiler.LCNF.CompilerM
import Lean.Compiler.LCNF.BaseTypes
import Lean.Compiler.LCNF.Util
namespace Lean.Compiler.LCNF
/--
Given a constructor, return a bitmask `m` s.t. `m[i]` is true if field `i` is
computationally relevant.
-/
def getRelevantCtorFields (ctorName : Name) (trivialType : Expr → MetaM Bool) :
CoreM (Array Bool) := do
let .ctorInfo info ← getConstInfo ctorName | unreachable!
Meta.MetaM.run' do
Meta.forallTelescopeReducing info.type fun xs _ => do
let mut result := #[]
for x in xs[info.numParams...*] do
let type ← Meta.inferType x
result := result.push !(← trivialType type)
return result
/--
We say a structure has a trivial structure if it has not builtin support in the runtime,
it has only one constructor, and this constructor has only one relevant field.
-/
public structure TrivialStructureInfo where
ctorName : Name
numParams : Nat
fieldIdx : Nat
deriving Inhabited, Repr
/--
Return `some fieldIdx` if `declName` is the name of an inductive datatype s.t.
- It does not have builtin support in the runtime.
- It has only one constructor.
- This constructor has only one computationally relevant field.
-/
public def Irrelevant.hasTrivialStructure?
(cacheExt : CacheExtension Name (Option TrivialStructureInfo))
(trivialType : Expr → MetaM Bool) (declName : Name) : CoreM (Option TrivialStructureInfo) := do
match (← cacheExt.find? declName) with
| some info? => return info?
| none =>
let info? ← fillCache
cacheExt.insert declName info?
return info?
where fillCache : CoreM (Option TrivialStructureInfo) := do
if isRuntimeBuiltinType declName then return none
let .inductInfo info ← getConstInfo declName | return none
if info.isUnsafe || info.isRec then return none
let [ctorName] := info.ctors | return none
let ctorType ← getOtherDeclBaseType ctorName []
if ctorType.isErased then return none
let mask ← getRelevantCtorFields ctorName trivialType
let mut result := none
for h : i in *...mask.size do
if mask[i] then
if result.isSome then return none
result := some { ctorName, fieldIdx := i, numParams := info.numParams }
return result
end Lean.Compiler.LCNF

50
src/Lean/Compiler/LCNF/MonoTypes.lean
View File

@@ -8,36 +8,14 @@ module
prelude
public import Lean.Compiler.LCNF.Util
public import Lean.Compiler.LCNF.BaseTypes
public import Lean.Compiler.LCNF.CompilerM
public import Lean.Compiler.LCNF.Irrelevant
public section
namespace Lean.Compiler.LCNF
/--
Given a constructor, return a bitmask `m` s.t. `m[i]` is true if field `i` is
computationally relevant.
-/
def getRelevantCtorFields (ctorName : Name) : CoreM (Array Bool) := do
let .ctorInfo info ← getConstInfo ctorName | unreachable!
Meta.MetaM.run' do
Meta.forallTelescopeReducing info.type fun xs _ => do
let mut result := #[]
for x in xs[info.numParams...*] do
let type ← Meta.inferType x
result := result.push !(← Meta.isProp type <||> Meta.isTypeFormerType type)
return result
/--
We say a structure has a trivial structure if it has not builtin support in the runtime,
it has only one constructor, and this constructor has only one relevant field.
-/
structure TrivialStructureInfo where
ctorName : Name
numParams : Nat
fieldIdx : Nat
deriving Inhabited, Repr
builtin_initialize trivialStructureInfoExt : CacheExtension Name (Option TrivialStructureInfo) ←
private builtin_initialize trivialStructureInfoExt : CacheExtension Name (Option TrivialStructureInfo) ←
CacheExtension.register
/--
@@ -47,26 +25,8 @@ Return `some fieldIdx` if `declName` is the name of an inductive datatype s.t.
- This constructor has only one computationally relevant field.
-/
def hasTrivialStructure? (declName : Name) : CoreM (Option TrivialStructureInfo) := do
match (← trivialStructureInfoExt.find? declName) with
| some info? => return info?
| none =>
let info? ← fillCache
trivialStructureInfoExt.insert declName info?
return info?
where fillCache : CoreM (Option TrivialStructureInfo) := do
if isRuntimeBuiltinType declName then return none
let .inductInfo info ← getConstInfo declName | return none
if info.isUnsafe || info.isRec then return none
let [ctorName] := info.ctors | return none
let ctorType ← getOtherDeclBaseType ctorName []
if ctorType.isErased then return none
let mask ← getRelevantCtorFields ctorName
let mut result := none
for h : i in *...mask.size do
if mask[i] then
if result.isSome then return none
result := some { ctorName, fieldIdx := i, numParams := info.numParams }
return result
let irrelevantType type := Meta.isProp type <||> Meta.isTypeFormerType type
Irrelevant.hasTrivialStructure? trivialStructureInfoExt irrelevantType declName
def getParamTypes (type : Expr) : Array Expr :=
go type #[]

4
src/Lean/Compiler/LCNF/Types.lean
View File

@@ -163,8 +163,8 @@ where
| .forallE .. => visitForall type #[]
| .app .. => type.withApp visitApp
| .fvar .. => visitApp type #[]
| .proj ``Subtype 0 (.const ``IO.RealWorld.nonemptyType []) =>
return mkConst ``lcRealWorld
| .proj ``Subtype 0 (.app (.const ``Void.nonemptyType []) _) =>
return mkConst ``lcVoid
| _ => return mkConst ``lcAny
whnfEta (type : Expr) : MetaM Expr := do

2
src/Lean/LoadDynlib.lean
View File

@@ -38,7 +38,7 @@ opaque Dynlib.get? (dynlib : @& Dynlib) (sym : @& String) : Option dynlib.Symbol
/--
Runs a module initializer function.
The symbol should have the signature `(builtin : Bool) → IO Unit`
(e.g., `initialize_Foo(uint8_t builtin, obj_arg)`).
(e.g., `initialize_Foo(uint8_t builtin)`).
This function is unsafe because there is no guarantee the symbol has the
expected signature. An invalid symbol can thus produce undefined behavior.

2
src/Lean/Server/Requests.lean
View File

@@ -252,7 +252,7 @@ open FileWorker
open Snapshots
def runInIO (x : RequestM α) (ctx : RequestContext) : IO α := do
x.run ctx |>.adaptExcept (IO.userError ·.message)
x.run ctx |>.adapt (IO.userError ·.message)
def readDoc [Monad m] [MonadReaderOf RequestContext m] : m EditableDocument := do
let rc ← readThe RequestContext

1
src/Std/Do/WP.lean
View File

@@ -8,5 +8,4 @@ module
prelude
public import Std.Do.WP.Basic
public import Std.Do.WP.Monad
public import Std.Do.WP.IO
public import Std.Do.WP.SimpLemmas

43
src/Std/Do/WP/IO.lean
View File

@@ -1,43 +0,0 @@
/-
Copyright (c) 2025 Lean FRO LLC. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Sebastian Graf
-/
module
prelude
public import Init.System.IO
public import Std.Do.WP.Monad
@[expose] public section
/-!
# Barebones `WP` instance for `IO`
This module defines a `WP` instance for `IO` without any synthetic model of the `IO.RealWorld` whatsoever.
This is useful for reasoning about `IO` programs when the precise result of a side-effect is irrelevant;
for example it can be used to reason about random number generation.
It is however inadequate for reasoning about, e.g., `IO.Ref`s.
-/
namespace Std.Do.IO.Bare
open Std.Do
/--
This is pretty much the instance for `EStateM` specialized to `σ = IO.RealWorld`.
However, `IO.RealWorld` is omitted in the `PredShape`.
-/
noncomputable scoped instance instWP : WP (EIO ε) (.except ε .pure) where
wp x := -- Could define as PredTrans.mkExcept (PredTrans.modifyGetM (fun s => pure (EStateM.Result.toExceptState (x s))))
{ apply := fun Q => match x Classical.ofNonempty with
| .ok a _rw => Q.1 a
| .error e _rw => Q.2.1 e
conjunctive := by
intro _ _
apply SPred.bientails.of_eq
dsimp
cases (x Classical.ofNonempty) <;> rfl
}
instance instLawfulMonad : LawfulMonad (EIO ε) := inferInstanceAs (LawfulMonad (EStateM ε IO.RealWorld))

18
src/Std/Internal/Async/Basic.lean
View File

@@ -164,7 +164,7 @@ Similar to `bind`, however `f` has access to the `EIO` monad. If `f` throws an e
protected def bindEIO (x : ETask ε α) (f : α → EIO ε (ETask ε β)) (prio := Task.Priority.default) (sync := false) : EIO ε (ETask ε β) :=
EIO.bindTask x (prio := prio) (sync := sync) fun
| .ok a => f a
| .error e => .error e
| .error e => throw e
/--
Similar to `bind`, however `f` has access to the `EIO` monad. If `f` throws an error, the returned
@@ -174,7 +174,7 @@ Similar to `bind`, however `f` has access to the `EIO` monad. If `f` throws an e
protected def mapEIO (f : α → EIO ε β) (x : ETask ε α) (prio := Task.Priority.default) (sync := false) : BaseIO (ETask ε β) :=
EIO.mapTask (t := x) (prio := prio) (sync := sync) fun
| .ok a => f a
| .error e => .error e
| .error e => throw e
/--
Block until the `ETask` in `x` finishes and returns its value. Propagates any error encountered
@@ -184,7 +184,7 @@ during execution.
def block (x : ETask ε α) : EIO ε α := do
match x.get with
| .ok a => return a
| .error e => .error e
| .error e => throw e
/--
Create an `ETask` that resolves to the value of the promise `x`. If the promise gets dropped then it
@@ -233,7 +233,7 @@ Similar to `map`, however `f` has access to the `IO` monad. If `f` throws an err
protected def mapIO (f : α → IO β) (x : AsyncTask α) (prio := Task.Priority.default) (sync := false) : BaseIO (AsyncTask β) :=
EIO.mapTask (t := x) (prio := prio) (sync := sync) fun
| .ok a => f a
| .error e => .error e
| .error e => throw e
/--
Construct an `AsyncTask` that is already resolved with value `x`.
@@ -272,7 +272,7 @@ Similar to `bind`, however `f` has access to the `IO` monad. If `f` throws an er
def bindIO (x : AsyncTask α) (f : α → IO (AsyncTask β)) (prio := Task.Priority.default) (sync := false) : BaseIO (AsyncTask β) :=
IO.bindTask x (prio := prio) (sync := sync) fun
| .ok a => f a
| .error e => .error e
| .error e => throw e
/--
Similar to `map`, however `f` has access to the `IO` monad. If `f` throws an error, the returned
@@ -282,7 +282,7 @@ Similar to `map`, however `f` has access to the `IO` monad. If `f` throws an err
def mapTaskIO (f : α → IO β) (x : AsyncTask α) (prio := Task.Priority.default) (sync := false) : BaseIO (AsyncTask β) :=
IO.mapTask (t := x) (prio := prio) (sync := sync) fun
| .ok a => f a
| .error e => .error e
| .error e => throw e
/--
Block until the `AsyncTask` in `x` finishes.
@@ -290,7 +290,7 @@ Block until the `AsyncTask` in `x` finishes.
def block (x : AsyncTask α) : IO α :=
match x.get with
| .ok a => return a
| .error e => .error e
| .error e => throw e
/--
Create an `AsyncTask` that resolves to the value of `x`.
@@ -448,7 +448,7 @@ Lifts a `BaseIO` action into a `BaseAsync` computation.
-/
@[inline]
protected def lift (x : BaseIO α) : BaseAsync α :=
.mk <| (.pure ∘ .pure) =<< x
.mk <| (pure ∘ pure) =<< x
/--
Waits for the result of the `BaseAsync` computation, blocking if necessary.
@@ -636,7 +636,7 @@ protected def wait (self : EAsync ε α) : EIO ε α := do
let result ← self |> BaseAsync.wait
match result with
| .ok a => return a
| .error e => .error e
| .error e => throw e
/--
Lifts an `EAsync` computation into an `ETask` that can be awaited and joined.

24
src/include/lean/lean.h
View File

@@ -2828,10 +2828,17 @@ LEAN_EXPORT lean_obj_res lean_decode_io_error(int errnum, b_lean_obj_arg fname);
LEAN_EXPORT lean_obj_res lean_decode_uv_error(int errnum, b_lean_obj_arg fname);
static inline lean_obj_res lean_io_mk_world() { return lean_box(0); }
static inline lean_obj_res lean_void_mk(lean_obj_arg a) {
lean_dec(a);
return lean_box(0);
}
static inline bool lean_io_result_is_ok(b_lean_obj_arg r) { return lean_ptr_tag(r) == 0; }
static inline bool lean_io_result_is_error(b_lean_obj_arg r) { return lean_ptr_tag(r) == 1; }
static inline b_lean_obj_res lean_io_result_get_value(b_lean_obj_arg r) { assert(lean_io_result_is_ok(r)); return lean_ctor_get(r, 0); }
static inline b_lean_obj_res lean_io_result_get_error(b_lean_obj_arg r) { assert(lean_io_result_is_error(r)); return lean_ctor_get(r, 0); }
static inline lean_obj_res lean_io_result_take_value(lean_obj_arg r) {
assert(lean_io_result_is_ok(r));
lean_object* v = lean_ctor_get(r, 0);
@@ -2839,18 +2846,17 @@ static inline lean_obj_res lean_io_result_take_value(lean_obj_arg r) {
lean_dec(r);
return v;
}
LEAN_EXPORT void lean_io_result_show_error(b_lean_obj_arg r);
LEAN_EXPORT void lean_io_mark_end_initialization(void);
static inline lean_obj_res lean_io_result_mk_ok(lean_obj_arg a) {
lean_object * r = lean_alloc_ctor(0, 2, 0);
lean_object * r = lean_alloc_ctor(0, 1, 0);
lean_ctor_set(r, 0, a);
lean_ctor_set(r, 1, lean_box(0));
return r;
}
static inline lean_obj_res lean_io_result_mk_error(lean_obj_arg e) {
lean_object * r = lean_alloc_ctor(1, 2, 0);
lean_object * r = lean_alloc_ctor(1, 1, 0);
lean_ctor_set(r, 0, e);
lean_ctor_set(r, 1, lean_box(0));
return r;
}
@@ -2882,11 +2888,11 @@ LEAN_EXPORT lean_obj_res lean_mk_io_user_error(lean_obj_arg str);
/* ST Ref primitives */
LEAN_EXPORT lean_obj_res lean_st_mk_ref(lean_obj_arg, lean_obj_arg);
LEAN_EXPORT lean_obj_res lean_st_ref_get(b_lean_obj_arg, lean_obj_arg);
LEAN_EXPORT lean_obj_res lean_st_ref_set(b_lean_obj_arg, lean_obj_arg, lean_obj_arg);
LEAN_EXPORT lean_obj_res lean_st_ref_reset(b_lean_obj_arg, lean_obj_arg);
LEAN_EXPORT lean_obj_res lean_st_ref_swap(b_lean_obj_arg, lean_obj_arg, lean_obj_arg);
LEAN_EXPORT lean_obj_res lean_st_mk_ref(lean_obj_arg);
LEAN_EXPORT lean_obj_res lean_st_ref_get(b_lean_obj_arg);
LEAN_EXPORT lean_obj_res lean_st_ref_set(b_lean_obj_arg, lean_obj_arg);
LEAN_EXPORT lean_obj_res lean_st_ref_reset(b_lean_obj_arg);
LEAN_EXPORT lean_obj_res lean_st_ref_swap(b_lean_obj_arg, lean_obj_arg);
/* pointer address unsafe primitive */
static inline size_t lean_ptr_addr(b_lean_obj_arg a) { return (size_t)a; }

12
src/initialize/init.cpp
View File

@@ -16,9 +16,9 @@ Author: Leonardo de Moura
#include "initialize/init.h"
namespace lean {
extern "C" object* initialize_Init(uint8_t, object* w);
extern "C" object* initialize_Std(uint8_t, object* w);
extern "C" object* initialize_Lean(uint8_t, object* w);
extern "C" object* initialize_Init(uint8_t);
extern "C" object* initialize_Std(uint8_t);
extern "C" object* initialize_Lean(uint8_t);
/* Initializes the Lean runtime. Before executing any code which uses the Lean package,
you must first call this function, and then `lean::io_mark_end_initialization`. In between
@@ -32,9 +32,9 @@ extern "C" LEAN_EXPORT void lean_initialize() {
// * calling exported Lean functions from C++
// * calling into native code of the current module from a previous stage when `prefer_native`
// is set
consume_io_result(initialize_Init(builtin, io_mk_world()));
consume_io_result(initialize_Std(builtin, io_mk_world()));
consume_io_result(initialize_Lean(builtin, io_mk_world()));
consume_io_result(initialize_Init(builtin));
consume_io_result(initialize_Std(builtin));
consume_io_result(initialize_Lean(builtin));
initialize_kernel_module();
init_default_print_fn();
initialize_library_core_module();

4
src/kernel/trace.cpp
View File

@@ -122,9 +122,9 @@ scope_trace_env::~scope_trace_env() {
get_disabled_trace_classes().resize(m_disable_sz);
}
extern "C" obj_res lean_io_eprint(obj_arg s, obj_arg w);
extern "C" obj_res lean_io_eprint(obj_arg s);
static void io_eprint(obj_arg s) {
object * r = lean_io_eprint(s, lean_io_mk_world());
object * r = lean_io_eprint(s);
if (!lean_io_result_is_ok(r))
lean_io_result_show_error(r);
lean_dec(r);

2
src/lake/Lake/CLI/Main.lean
View File

@@ -102,7 +102,7 @@ def LakeOptions.getInstall (opts : LakeOptions) : Except CliError (LeanInstall
/-- Compute the Lake environment based on `opts`. Error if an install is missing. -/
def LakeOptions.computeEnv (opts : LakeOptions) : EIO CliError Lake.Env := do
Env.compute (← opts.getLakeInstall) (← opts.getLeanInstall) opts.elanInstall?
opts.noCache |>.adaptExcept fun msg => .invalidEnv msg
opts.noCache |>.adapt fun msg => .invalidEnv msg
/-- Make a `LoadConfig` from a `LakeOptions`. -/
public def LakeOptions.mkLoadConfig (opts : LakeOptions) : EIO CliError LoadConfig := do

16
src/library/dynlib.cpp
View File

@@ -67,7 +67,7 @@ static inline void * symbol_ptr(b_obj_arg sym) {
}
/* Dynlib.load : System.FilePath -> IO Dynlib */
extern "C" LEAN_EXPORT obj_res lean_dynlib_load(b_obj_arg path, obj_arg) {
extern "C" LEAN_EXPORT obj_res lean_dynlib_load(b_obj_arg path) {
#ifdef LEAN_WINDOWS
HMODULE h = LoadLibrary(string_cstr(path));
if (!h) {
@@ -114,22 +114,22 @@ extern "C" LEAN_EXPORT obj_res lean_dynlib_get(b_obj_arg dynlib, b_obj_arg name)
}
/* Dynlib.Symbol.runAsInit : {Dynlib} -> Symbol -> IO Unit */
extern "C" LEAN_EXPORT obj_res lean_dynlib_symbol_run_as_init(b_obj_arg /* dynlib */, b_obj_arg sym, obj_arg) {
auto init_fn = reinterpret_cast<object *(*)(uint8_t, object *)>(symbol_ptr(sym));
return init_fn(1 /* builtin */, io_mk_world());
extern "C" LEAN_EXPORT obj_res lean_dynlib_symbol_run_as_init(b_obj_arg /* dynlib */, b_obj_arg sym) {
auto init_fn = reinterpret_cast<object *(*)(uint8_t)>(symbol_ptr(sym));
return init_fn(1 /* builtin */);
}
/* Lean.loadDynlib : System.FilePath -> IO Unit */
extern "C" obj_res lean_load_dynlib(obj_arg path, obj_arg);
extern "C" obj_res lean_load_dynlib(obj_arg path);
void load_dynlib(std::string path) {
consume_io_result(lean_load_dynlib(mk_string(path), io_mk_world()));
consume_io_result(lean_load_dynlib(mk_string(path)));
}
/* Lean.loadPlugin : System.FilePath -> IO Unit */
extern "C" obj_res lean_load_plugin(obj_arg path, obj_arg);
extern "C" obj_res lean_load_plugin(obj_arg path);
void load_plugin(std::string path) {
consume_io_result(lean_load_plugin(mk_string(path), io_mk_world()));
consume_io_result(lean_load_plugin(mk_string(path)));
}
}

19
src/library/ir_interpreter.cpp
View File

@@ -218,7 +218,8 @@ std::string format_fn_body_head(fn_body const & b) {
}
static bool type_is_scalar(type t) {
return t != type::Object && t != type::Tagged && t != type::TObject && t != type::Irrelevant;
return t != type::Object && t != type::Tagged && t != type::TObject && t != type::Irrelevant
&& t != type::Void;
}
extern "C" object* lean_get_regular_init_fn_name_for(object* env, object* fn);
@@ -272,6 +273,7 @@ object * box_t(value v, type t) {
case type::Tagged:
case type::TObject:
case type::Irrelevant:
case type::Void:
return v.m_obj;
case type::Struct:
case type::Union:
@@ -290,6 +292,7 @@ value unbox_t(object * o, type t) {
case type::UInt64: return unbox_uint64(o);
case type::USize: return unbox_size_t(o);
case type::Irrelevant:
case type::Void:
case type::Object:
case type::Tagged:
case type::TObject:
@@ -520,6 +523,7 @@ private:
case type::UInt64: return cnstr_get_uint64(o, offset);
case type::USize:
case type::Irrelevant:
case type::Void:
case type::Object:
case type::Tagged:
case type::TObject:
@@ -591,6 +595,7 @@ private:
case type::TObject:
return n.to_obj_arg();
case type::Irrelevant:
case type::Void:
break;
case type::Union:
case type::Struct:
@@ -713,6 +718,7 @@ private:
case type::UInt64: cnstr_set_uint64(o, offset, v.m_num); break;
case type::USize:
case type::Irrelevant:
case type::Void:
case type::Object:
case type::Tagged:
case type::TObject:
@@ -889,6 +895,7 @@ private:
case type::Tagged:
case type::TObject:
case type::Irrelevant:
case type::Void:
return *static_cast<object **>(e.m_native.m_addr);
case type::Struct:
case type::Union:
@@ -1104,7 +1111,7 @@ public:
object * run_init(name const & decl, name const & init_decl) {
try {
object * args[] = { io_mk_world() };
object * args[] = {};
object * r = call_boxed(init_decl, 1, args);
if (io_result_is_ok(r)) {
object * o = io_result_get_value(r);
@@ -1154,9 +1161,9 @@ uint32 run_main(elab_environment const & env, options const & opts, list_ref<str
}
/* runMain (env : Environment) (opts : Iptions) (args : List String) : BaseIO UInt32 */
extern "C" LEAN_EXPORT obj_res lean_run_main(b_obj_arg env, b_obj_arg opts, b_obj_arg args, obj_arg) {
extern "C" LEAN_EXPORT uint32_t lean_run_main(b_obj_arg env, b_obj_arg opts, b_obj_arg args) {
uint32 ret = run_main(TO_REF(elab_environment, env), TO_REF(options, opts), TO_REF(list_ref<string_ref>, args));
return io_result_mk_ok(box(ret));
return ret;
}
extern "C" LEAN_EXPORT object * lean_eval_const(object * env, object * opts, object * c) {
@@ -1173,9 +1180,9 @@ extern "C" obj_res lean_mk_module_initialization_function_name(obj_arg);
extern "C" LEAN_EXPORT object * lean_run_mod_init(object * mod, object *) {
string_ref mangled = string_ref(lean_mk_module_initialization_function_name(mod));
if (void * init = lookup_symbol_in_cur_exe(mangled.data())) {
auto init_fn = reinterpret_cast<object *(*)(uint8_t, object *)>(init);
auto init_fn = reinterpret_cast<object *(*)(uint8_t)>(init);
uint8_t builtin = 0;
object * r = init_fn(builtin, io_mk_world());
object * r = init_fn(builtin);
if (io_result_is_ok(r)) {
dec_ref(r);
return lean_io_result_mk_ok(box(true));

3
src/library/ir_types.h
View File

@@ -16,10 +16,11 @@ inductive IRType
| struct (leanTypeName : Option Name) (types : Array IRType) : IRType
| union (leanTypeName : Name) (types : Array IRType) : IRType
| tagged
| void
Remark: we don't create struct/union types from C++.
*/
enum class type { Float, UInt8, UInt16, UInt32, UInt64, USize, Irrelevant, Object, TObject, Float32, Struct, Union, Tagged };
enum class type { Float, UInt8, UInt16, UInt32, UInt64, USize, Irrelevant, Object, TObject, Float32, Struct, Union, Tagged, Void };
typedef nat var_id;
typedef nat jp_id;

493
src/library/llvm.cpp
View File

File diff suppressed because it is too large Load Diff

4
src/library/time_task.cpp
View File

@@ -39,9 +39,9 @@ void display_cumulative_profiling_times(std::ostream & out) {
}
/* displayCumulativeProfilingTimes : BaseIO Unit */
extern "C" LEAN_EXPORT obj_res lean_display_cumulative_profiling_times(obj_arg) {
extern "C" LEAN_EXPORT obj_res lean_display_cumulative_profiling_times() {
display_cumulative_profiling_times(std::cerr);
return lean_io_result_mk_ok(box(0));
return box(0);
}
void initialize_time_task() {

8
src/runtime/interrupt.cpp
View File

@@ -16,7 +16,7 @@ namespace lean {
LEAN_THREAD_VALUE(size_t, g_max_heartbeat, 0);
LEAN_THREAD_VALUE(size_t, g_heartbeat, 0);
extern "C" LEAN_EXPORT obj_res lean_internal_get_default_max_heartbeat(obj_arg) {
extern "C" LEAN_EXPORT obj_res lean_internal_get_default_max_heartbeat() {
#ifdef LEAN_DEFAULT_MAX_HEARTBEAT
return lean_box(LEAN_DEFAULT_MAX_HEARTBEAT);
#else
@@ -32,7 +32,7 @@ void set_max_heartbeat(size_t max) { g_max_heartbeat = max; }
extern "C" LEAN_EXPORT obj_res lean_internal_set_max_heartbeat(usize max) {
set_max_heartbeat(max);
return lean_io_result_mk_ok(lean_box(0));
return lean_box(0);
}
size_t get_max_heartbeat() { return g_max_heartbeat; }
@@ -58,12 +58,12 @@ LEAN_THREAD_VALUE(lean_object *, g_cancel_tk, nullptr);
LEAN_EXPORT scope_cancel_tk::scope_cancel_tk(lean_object * o):flet<lean_object *>(g_cancel_tk, o) {}
/* CancelToken.isSet : @& IO.CancelToken → BaseIO Bool */
extern "C" lean_obj_res lean_io_cancel_token_is_set(b_lean_obj_arg cancel_tk, lean_obj_arg);
extern "C" lean_obj_res lean_io_cancel_token_is_set(b_lean_obj_arg cancel_tk);
void check_interrupted() {
if (g_cancel_tk) {
inc_ref(g_cancel_tk);
if (get_io_scalar_result<bool>(lean_io_cancel_token_is_set(g_cancel_tk, lean_io_mk_world())) &&
if (lean_io_cancel_token_is_set(g_cancel_tk) &&
!std::uncaught_exception()) {
throw interrupted();
}

234
src/runtime/io.cpp
View File

@@ -78,8 +78,8 @@ static bool g_initializing = true;
extern "C" LEAN_EXPORT void lean_io_mark_end_initialization() {
g_initializing = false;
}
extern "C" LEAN_EXPORT obj_res lean_io_initializing(obj_arg) {
return io_result_mk_ok(box(g_initializing));
extern "C" LEAN_EXPORT uint8_t lean_io_initializing() {
return g_initializing;
}
static obj_res mk_file_not_found_error(b_obj_arg fname) {
@@ -116,49 +116,49 @@ MK_THREAD_LOCAL_GET(object_ref, get_stream_current_stdout, g_stream_stdout);
MK_THREAD_LOCAL_GET(object_ref, get_stream_current_stderr, g_stream_stderr);
/* getStdin : BaseIO FS.Stream */
extern "C" LEAN_EXPORT obj_res lean_get_stdin(obj_arg /* w */) {
return io_result_mk_ok(get_stream_current_stdin().to_obj_arg());
extern "C" LEAN_EXPORT obj_res lean_get_stdin() {
return get_stream_current_stdin().to_obj_arg();
}
/* getStdout : BaseIO FS.Stream */
extern "C" LEAN_EXPORT obj_res lean_get_stdout(obj_arg /* w */) {
return io_result_mk_ok(get_stream_current_stdout().to_obj_arg());
extern "C" LEAN_EXPORT obj_res lean_get_stdout() {
return get_stream_current_stdout().to_obj_arg();
}
/* getStderr : BaseIO FS.Stream */
extern "C" LEAN_EXPORT obj_res lean_get_stderr(obj_arg /* w */) {
return io_result_mk_ok(get_stream_current_stderr().to_obj_arg());
extern "C" LEAN_EXPORT obj_res lean_get_stderr() {
return get_stream_current_stderr().to_obj_arg();
}
/* setStdin : FS.Stream -> BaseIO FS.Stream */
extern "C" LEAN_EXPORT obj_res lean_get_set_stdin(obj_arg h, obj_arg /* w */) {
extern "C" LEAN_EXPORT obj_res lean_get_set_stdin(obj_arg h) {
object_ref & x = get_stream_current_stdin();
object * r = x.steal();
x = object_ref(h);
return io_result_mk_ok(r);
return r;
}
/* setStdout : FS.Stream -> BaseIO FS.Stream */
extern "C" LEAN_EXPORT obj_res lean_get_set_stdout(obj_arg h, obj_arg /* w */) {
extern "C" LEAN_EXPORT obj_res lean_get_set_stdout(obj_arg h) {
object_ref & x = get_stream_current_stdout();
object * r = x.steal();
x = object_ref(h);
return io_result_mk_ok(r);
return r;
}
/* setStderr : FS.Stream -> BaseIO FS.Stream */
extern "C" LEAN_EXPORT obj_res lean_get_set_stderr(obj_arg h, obj_arg /* w */) {
extern "C" LEAN_EXPORT obj_res lean_get_set_stderr(obj_arg h) {
object_ref & x = get_stream_current_stderr();
object * r = x.steal();
x = object_ref(h);
return io_result_mk_ok(r);
return r;
}
static FILE * io_get_handle(lean_object * hfile) {
return static_cast<FILE *>(lean_get_external_data(hfile));
}
extern "C" LEAN_EXPORT obj_res lean_decode_io_error(int errnum, b_obj_arg fname) {
extern "C" LEAN_EXPORT obj_res lean_decode_io_error(int errnum, b_lean_obj_arg fname) {
object * details = mk_string(strerror(errnum));
// Keep in sync with lean_decode_uv_error below
switch (errnum) {
@@ -255,7 +255,7 @@ extern "C" LEAN_EXPORT obj_res lean_decode_io_error(int errnum, b_obj_arg fname)
}
}
extern "C" LEAN_EXPORT obj_res lean_decode_uv_error(int errnum, b_obj_arg fname) {
extern "C" LEAN_EXPORT obj_res lean_decode_uv_error(int errnum, b_lean_obj_arg fname) {
object * details = mk_string(uv_strerror(errnum));
// Keep in sync with lean_decode_io_error above
switch (errnum) {
@@ -369,7 +369,7 @@ obj_res mk_embedded_nul_error(b_obj_arg str) {
}
/* IO.setAccessRights (filename : @& String) (mode : UInt32) : IO Unit */
extern "C" LEAN_EXPORT obj_res lean_chmod (b_obj_arg filename, uint32_t mode, obj_arg /* w */) {
extern "C" LEAN_EXPORT obj_res lean_chmod (b_obj_arg filename, uint32_t mode) {
const char* fname = string_cstr(filename);
if (strlen(fname) != lean_string_size(filename) - 1) {
return mk_embedded_nul_error(filename);
@@ -382,7 +382,7 @@ extern "C" LEAN_EXPORT obj_res lean_chmod (b_obj_arg filename, uint32_t mode, ob
}
/* Handle.mk (filename : @& String) (mode : FS.Mode) : IO Handle */
extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_mk(b_obj_arg filename, uint8 mode, obj_arg /* w */) {
extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_mk(b_obj_arg filename, uint8 mode) {
int flags = 0;
#ifdef LEAN_WINDOWS
// do not translate line endings
@@ -431,7 +431,7 @@ static inline HANDLE win_handle(FILE * fp) {
}
/* Handle.lock : (@& Handle) → (exclusive : Bool) → IO Unit */
extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_lock(b_obj_arg h, uint8_t x, obj_arg /* w */) {
extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_lock(b_obj_arg h, uint8_t x) {
OVERLAPPED o = {0};
HANDLE wh = win_handle(io_get_handle(h));
DWORD flags = x ? LOCKFILE_EXCLUSIVE_LOCK : 0;
@@ -443,7 +443,7 @@ extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_lock(b_obj_arg h, uint8_t x,
}
/* Handle.tryLock : (@& Handle) → (exclusive : Bool) → IO Bool */
extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_try_lock(b_obj_arg h, uint8_t x, obj_arg /* w */) {
extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_try_lock(b_obj_arg h, uint8_t x) {
OVERLAPPED o = {0};
HANDLE wh = win_handle(io_get_handle(h));
DWORD flags = (x ? LOCKFILE_EXCLUSIVE_LOCK : 0) | LOCKFILE_FAIL_IMMEDIATELY;
@@ -459,7 +459,7 @@ extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_try_lock(b_obj_arg h, uint8_t
}
/* Handle.unlock : (@& Handle) → IO Unit */
extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_unlock(b_obj_arg h, obj_arg /* w */) {
extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_unlock(b_obj_arg h) {
OVERLAPPED o = {0};
HANDLE wh = win_handle(io_get_handle(h));
if (UnlockFileEx(wh, 0, MAXDWORD, MAXDWORD, &o)) {
@@ -477,7 +477,7 @@ extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_unlock(b_obj_arg h, obj_arg /
#else
/* Handle.lock : (@& Handle) → (exclusive : Bool) → IO Unit */
extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_lock(b_obj_arg h, uint8_t x, obj_arg /* w */) {
extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_lock(b_obj_arg h, uint8_t x) {
FILE * fp = io_get_handle(h);
if (!flock(fileno(fp), x ? LOCK_EX : LOCK_SH)) {
return io_result_mk_ok(box(0));
@@ -487,7 +487,7 @@ extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_lock(b_obj_arg h, uint8_t x,
}
/* Handle.tryLock : (@& Handle) → (exclusive : Bool) → IO Bool */
extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_try_lock(b_obj_arg h, uint8_t x, obj_arg /* w */) {
extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_try_lock(b_obj_arg h, uint8_t x) {
FILE * fp = io_get_handle(h);
if (!flock(fileno(fp), (x ? LOCK_EX : LOCK_SH) | LOCK_NB)) {
return io_result_mk_ok(box(1));
@@ -501,7 +501,7 @@ extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_try_lock(b_obj_arg h, uint8_t
}
/* Handle.unlock : (@& Handle) → IO Unit */
extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_unlock(b_obj_arg h, obj_arg /* w */) {
extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_unlock(b_obj_arg h) {
FILE * fp = io_get_handle(h);
if (!flock(fileno(fp), LOCK_UN)) {
return io_result_mk_ok(box(0));
@@ -513,7 +513,7 @@ extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_unlock(b_obj_arg h, obj_arg /
#endif
/* Handle.isTty : (@& Handle) → BaseIO Bool */
extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_is_tty(b_obj_arg h, obj_arg /* w */) {
extern "C" LEAN_EXPORT uint8_t lean_io_prim_handle_is_tty(b_obj_arg h) {
FILE * fp = io_get_handle(h);
#ifdef LEAN_WINDOWS
/*
@@ -533,21 +533,21 @@ extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_is_tty(b_obj_arg h, obj_arg /
and Lean does not support pre-Windows 10.
*/
DWORD mode;
return io_result_mk_ok(box(GetConsoleMode(win_handle(fp), &mode) != 0));
return GetConsoleMode(win_handle(fp), &mode) != 0;
#else
// We ignore errors for consistency with Windows.
return io_result_mk_ok(box(isatty(fileno(fp))));
return isatty(fileno(fp));
#endif
}
/* Handle.isEof : (@& Handle) → BaseIO Bool */
extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_is_eof(b_obj_arg h, obj_arg /* w */) {
extern "C" LEAN_EXPORT uint8_t lean_io_prim_handle_is_eof(b_obj_arg h) {
FILE * fp = io_get_handle(h);
return io_result_mk_ok(box(std::feof(fp) != 0));
return std::feof(fp) != 0;
}
/* Handle.flush : (@& Handle) → IO Unit */
extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_flush(b_obj_arg h, obj_arg /* w */) {
extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_flush(b_obj_arg h) {
FILE * fp = io_get_handle(h);
if (!std::fflush(fp)) {
return io_result_mk_ok(box(0));
@@ -557,7 +557,7 @@ extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_flush(b_obj_arg h, obj_arg /*
}
/* Handle.rewind : (@& Handle) → IO Unit */
extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_rewind(b_obj_arg h, obj_arg /* w */) {
extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_rewind(b_obj_arg h) {
FILE * fp = io_get_handle(h);
if (!std::fseek(fp, 0, SEEK_SET)) {
return io_result_mk_ok(box(0));
@@ -567,7 +567,7 @@ extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_rewind(b_obj_arg h, obj_arg /
}
/* Handle.truncate : (@& Handle) → IO Unit */
extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_truncate(b_obj_arg h, obj_arg /* w */) {
extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_truncate(b_obj_arg h) {
FILE * fp = io_get_handle(h);
#ifdef LEAN_WINDOWS
if (!_chsize_s(_fileno(fp), _ftelli64(fp))) {
@@ -581,7 +581,7 @@ extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_truncate(b_obj_arg h, obj_arg
}
/* Handle.read : (@& Handle) → USize → IO ByteArray */
extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_read(b_obj_arg h, usize nbytes, obj_arg /* w */) {
extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_read(b_obj_arg h, usize nbytes) {
FILE * fp = io_get_handle(h);
obj_res res = lean_alloc_sarray(1, 0, nbytes);
usize n = std::fread(lean_sarray_cptr(res), 1, nbytes, fp);
@@ -599,7 +599,7 @@ extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_read(b_obj_arg h, usize nbyte
}
/* Handle.write : (@& Handle) → (@& ByteArray) → IO Unit */
extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_write(b_obj_arg h, b_obj_arg buf, obj_arg /* w */) {
extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_write(b_obj_arg h, b_obj_arg buf) {
FILE * fp = io_get_handle(h);
usize n = lean_sarray_size(buf);
usize m = std::fwrite(lean_sarray_cptr(buf), 1, n, fp);
@@ -611,7 +611,7 @@ extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_write(b_obj_arg h, b_obj_arg
}
/* Handle.getLine : (@& Handle) → IO Unit */
extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_get_line(b_obj_arg h, obj_arg /* w */) {
extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_get_line(b_obj_arg h) {
FILE * fp = io_get_handle(h);
std::string result;
@@ -635,7 +635,7 @@ extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_get_line(b_obj_arg h, obj_arg
}
/* Handle.putStr : (@& Handle) → (@& String) → IO Unit */
extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_put_str(b_obj_arg h, b_obj_arg s, obj_arg /* w */) {
extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_put_str(b_obj_arg h, b_obj_arg s) {
FILE * fp = io_get_handle(h);
usize n = lean_string_size(s) - 1; // - 1 to ignore the terminal NULL byte.
usize m = std::fwrite(lean_string_cstr(s), 1, n, fp);
@@ -647,7 +647,7 @@ extern "C" LEAN_EXPORT obj_res lean_io_prim_handle_put_str(b_obj_arg h, b_obj_ar
}
/* Std.Time.Timestamp.now : IO Timestamp */
extern "C" LEAN_EXPORT obj_res lean_get_current_time(obj_arg /* w */) {
extern "C" LEAN_EXPORT obj_res lean_get_current_time() {
using namespace std::chrono;
std::chrono::system_clock::time_point now = std::chrono::system_clock::now();
@@ -664,7 +664,7 @@ extern "C" LEAN_EXPORT obj_res lean_get_current_time(obj_arg /* w */) {
}
/* Std.Time.Database.Windows.getNextTransition : @&String -> Int64 -> Bool -> IO (Option (Int64 × TimeZone)) */
extern "C" LEAN_EXPORT obj_res lean_windows_get_next_transition(b_obj_arg timezone_str, uint64_t tm_obj, uint8 default_time, obj_arg /* w */) {
extern "C" LEAN_EXPORT obj_res lean_windows_get_next_transition(b_obj_arg timezone_str, uint64_t tm_obj, uint8 default_time) {
#if defined(LEAN_WINDOWS)
UErrorCode status = U_ZERO_ERROR;
const char* dst_name_id = lean_string_cstr(timezone_str);
@@ -778,7 +778,7 @@ extern "C" LEAN_EXPORT obj_res lean_windows_get_next_transition(b_obj_arg timezo
}
/* Std.Time.Database.Windows.getLocalTimeZoneIdentifierAt : Int64 → IO String */
extern "C" LEAN_EXPORT obj_res lean_get_windows_local_timezone_id_at(uint64_t tm_obj, obj_arg /* w */) {
extern "C" LEAN_EXPORT obj_res lean_get_windows_local_timezone_id_at(uint64_t tm_obj) {
#if defined(LEAN_WINDOWS)
UErrorCode status = U_ZERO_ERROR;
UCalendar* cal = ucal_open(NULL, -1, NULL, UCAL_GREGORIAN, &status);
@@ -817,23 +817,23 @@ extern "C" LEAN_EXPORT obj_res lean_get_windows_local_timezone_id_at(uint64_t tm
}
/* monoMsNow : BaseIO Nat */
extern "C" LEAN_EXPORT obj_res lean_io_mono_ms_now(obj_arg /* w */) {
extern "C" LEAN_EXPORT obj_res lean_io_mono_ms_now() {
static_assert(sizeof(std::chrono::milliseconds::rep) <= sizeof(uint64), "size of std::chrono::nanoseconds::rep may not exceed 64");
auto now = std::chrono::steady_clock::now();
auto tm = std::chrono::duration_cast<std::chrono::milliseconds>(now.time_since_epoch());
return io_result_mk_ok(uint64_to_nat(tm.count()));
return uint64_to_nat(tm.count());
}
/* monoNanosNow : BaseIO Nat */
extern "C" LEAN_EXPORT obj_res lean_io_mono_nanos_now(obj_arg /* w */) {
extern "C" LEAN_EXPORT obj_res lean_io_mono_nanos_now() {
static_assert(sizeof(std::chrono::nanoseconds::rep) <= sizeof(uint64), "size of std::chrono::nanoseconds::rep may not exceed 64");
auto now = std::chrono::steady_clock::now();
auto tm = std::chrono::duration_cast<std::chrono::nanoseconds>(now.time_since_epoch());
return io_result_mk_ok(uint64_to_nat(tm.count()));
return uint64_to_nat(tm.count());
}
/* getRandomBytes (nBytes : USize) : IO ByteArray */
extern "C" LEAN_EXPORT obj_res lean_io_get_random_bytes (size_t nbytes, obj_arg /* w */) {
extern "C" LEAN_EXPORT obj_res lean_io_get_random_bytes (size_t nbytes) {
// Adapted from https://github.com/rust-random/getrandom/blob/30308ae845b0bf3839e5a92120559eaf56048c28/src/
if (nbytes == 0) return io_result_mk_ok(lean_alloc_sarray(1, 0, 0));
@@ -894,9 +894,9 @@ extern "C" LEAN_EXPORT obj_res lean_io_get_random_bytes (size_t nbytes, obj_arg
}
/* timeit {α : Type} (msg : @& String) (fn : IO α) : IO α */
extern "C" LEAN_EXPORT obj_res lean_io_timeit(b_obj_arg msg, obj_arg fn, obj_arg w) {
extern "C" LEAN_EXPORT obj_res lean_io_timeit(b_obj_arg msg, obj_arg fn) {
auto start = std::chrono::steady_clock::now();
w = apply_1(fn, w);
obj_arg w = apply_1(fn, lean_io_mk_world());
auto end = std::chrono::steady_clock::now();
auto diff = std::chrono::duration<double>(end - start);
sstream out;
@@ -911,33 +911,33 @@ extern "C" LEAN_EXPORT obj_res lean_io_timeit(b_obj_arg msg, obj_arg fn, obj_arg
}
/* allocprof {α : Type} (msg : @& String) (fn : IO α) : IO α */
extern "C" LEAN_EXPORT obj_res lean_io_allocprof(b_obj_arg msg, obj_arg fn, obj_arg w) {
extern "C" LEAN_EXPORT obj_res lean_io_allocprof(b_obj_arg msg, obj_arg fn) {
std::ostringstream out;
obj_res res;
{
allocprof prof(out, string_cstr(msg));
res = apply_1(fn, w);
res = apply_1(fn, lean_io_mk_world());
}
io_eprintln(mk_string(out.str()));
return res;
}
/* getNumHeartbeats : BaseIO Nat */
extern "C" LEAN_EXPORT obj_res lean_io_get_num_heartbeats(obj_arg /* w */) {
return io_result_mk_ok(lean_uint64_to_nat(get_num_heartbeats()));
extern "C" LEAN_EXPORT obj_res lean_io_get_num_heartbeats() {
return lean_uint64_to_nat(get_num_heartbeats());
}
/* setHeartbeats (count : Nat) : BaseIO Unit */
extern "C" LEAN_EXPORT obj_res lean_io_set_heartbeats(obj_arg count, obj_arg /* w */) {
extern "C" LEAN_EXPORT obj_res lean_io_set_heartbeats(obj_arg count) {
set_heartbeats(lean_uint64_of_nat(count));
lean_dec(count);
return io_result_mk_ok(box(0));
return box(0);
}
extern "C" LEAN_EXPORT obj_res lean_io_getenv(b_obj_arg env_var, obj_arg) {
extern "C" LEAN_EXPORT obj_res lean_io_getenv(b_obj_arg env_var) {
const char* env_var_str = string_cstr(env_var);
if (strlen(env_var_str) != lean_string_size(env_var) - 1) {
return io_result_mk_ok(mk_option_none());
return mk_option_none();
}
#if defined(LEAN_EMSCRIPTEN)
// HACK(WN): getenv doesn't seem to work in Emscripten even though it should
@@ -958,21 +958,21 @@ extern "C" LEAN_EXPORT obj_res lean_io_getenv(b_obj_arg env_var, obj_arg) {
if (val) {
object * valLean = mk_string(val);
free(val);
return io_result_mk_ok(mk_option_some(valLean));
return mk_option_some(valLean);
} else {
return io_result_mk_ok(mk_option_none());
return mk_option_none();
}
#else
char * val = std::getenv(env_var_str);
if (val) {
return io_result_mk_ok(mk_option_some(mk_string(val)));
return mk_option_some(mk_string(val));
} else {
return io_result_mk_ok(mk_option_none());
return mk_option_none();
}
#endif
}
extern "C" LEAN_EXPORT obj_res lean_io_realpath(obj_arg filename, obj_arg) {
extern "C" LEAN_EXPORT obj_res lean_io_realpath(obj_arg filename) {
const char* fname = string_cstr(filename);
if (strlen(fname) != lean_string_size(filename) - 1) {
obj_res res = mk_embedded_nul_error(filename);
@@ -1034,7 +1034,7 @@ structure DirEntry where
constant readDir : @& FilePath → IO (Array DirEntry)
*/
extern "C" LEAN_EXPORT obj_res lean_io_read_dir(b_obj_arg dirname, obj_arg) {
extern "C" LEAN_EXPORT obj_res lean_io_read_dir(b_obj_arg dirname) {
const char* dirname_ptr = string_cstr(dirname);
if (strlen(dirname_ptr) != lean_string_size(dirname) - 1) {
return mk_embedded_nul_error(dirname);
@@ -1109,7 +1109,7 @@ static obj_res metadata_core(struct stat const & st) {
return io_result_mk_ok(mdata);
}
extern "C" LEAN_EXPORT obj_res lean_io_metadata(b_obj_arg filename, obj_arg) {
extern "C" LEAN_EXPORT obj_res lean_io_metadata(b_obj_arg filename) {
const char* fname = string_cstr(filename);
if (strlen(fname) != lean_string_size(filename) - 1) {
return mk_embedded_nul_error(filename);
@@ -1121,9 +1121,9 @@ extern "C" LEAN_EXPORT obj_res lean_io_metadata(b_obj_arg filename, obj_arg) {
return metadata_core(st);
}
extern "C" LEAN_EXPORT obj_res lean_io_symlink_metadata(b_obj_arg filename, obj_arg) {
extern "C" LEAN_EXPORT obj_res lean_io_symlink_metadata(b_obj_arg filename) {
#ifdef LEAN_WINDOWS
return lean_io_metadata(filename, io_mk_world());
return lean_io_metadata(filename);
#else
const char* fname = string_cstr(filename);
if (strlen(fname) != lean_string_size(filename) - 1) {
@@ -1137,7 +1137,7 @@ extern "C" LEAN_EXPORT obj_res lean_io_symlink_metadata(b_obj_arg filename, obj_
#endif
}
extern "C" LEAN_EXPORT obj_res lean_io_create_dir(b_obj_arg p, obj_arg) {
extern "C" LEAN_EXPORT obj_res lean_io_create_dir(b_obj_arg p) {
const char* str = string_cstr(p);
if (strlen(str) != lean_string_size(p) - 1) {
return mk_embedded_nul_error(p);
@@ -1153,7 +1153,7 @@ extern "C" LEAN_EXPORT obj_res lean_io_create_dir(b_obj_arg p, obj_arg) {
}
}
extern "C" LEAN_EXPORT obj_res lean_io_remove_dir(b_obj_arg p, obj_arg) {
extern "C" LEAN_EXPORT obj_res lean_io_remove_dir(b_obj_arg p) {
const char* str = string_cstr(p);
if (strlen(str) != lean_string_size(p) - 1) {
return mk_embedded_nul_error(p);
@@ -1165,7 +1165,7 @@ extern "C" LEAN_EXPORT obj_res lean_io_remove_dir(b_obj_arg p, obj_arg) {
}
}
extern "C" LEAN_EXPORT obj_res lean_io_rename(b_obj_arg from, b_obj_arg to, lean_object * /* w */) {
extern "C" LEAN_EXPORT obj_res lean_io_rename(b_obj_arg from, b_obj_arg to) {
const char* from_str = string_cstr(from);
if (strlen(from_str) != lean_string_size(from) - 1) {
return mk_embedded_nul_error(from);
@@ -1197,7 +1197,7 @@ extern "C" LEAN_EXPORT obj_res lean_io_rename(b_obj_arg from, b_obj_arg to, lean
}
/* hardLink (orig link : @& FilePath) : IO Unit */
extern "C" LEAN_EXPORT obj_res lean_io_hard_link(b_obj_arg orig, b_obj_arg link, lean_object * /* w */) {
extern "C" LEAN_EXPORT obj_res lean_io_hard_link(b_obj_arg orig, b_obj_arg link) {
const char* orig_str = string_cstr(orig);
if (strlen(orig_str) != lean_string_size(orig) - 1) {
return mk_embedded_nul_error(orig);
@@ -1307,7 +1307,7 @@ extern "C" LEAN_EXPORT obj_res lean_io_create_tempdir(lean_object * /* w */) {
}
}
extern "C" LEAN_EXPORT obj_res lean_io_remove_file(b_obj_arg filename, obj_arg) {
extern "C" LEAN_EXPORT obj_res lean_io_remove_file(b_obj_arg filename) {
const char* fname = string_cstr(filename);
if (strlen(fname) != lean_string_size(filename) - 1) {
return mk_embedded_nul_error(filename);
@@ -1319,7 +1319,7 @@ extern "C" LEAN_EXPORT obj_res lean_io_remove_file(b_obj_arg filename, obj_arg)
}
}
extern "C" LEAN_EXPORT obj_res lean_io_app_path(obj_arg) {
extern "C" LEAN_EXPORT obj_res lean_io_app_path() {
#if defined(LEAN_WINDOWS)
HMODULE hModule = GetModuleHandle(NULL);
char path[MAX_PATH];
@@ -1374,7 +1374,7 @@ extern "C" LEAN_EXPORT obj_res lean_io_app_path(obj_arg) {
#endif
}
extern "C" LEAN_EXPORT obj_res lean_io_current_dir(obj_arg) {
extern "C" LEAN_EXPORT obj_res lean_io_current_dir() {
char buffer[PATH_MAX];
char * cwd = getcwd(buffer, sizeof(buffer));
if (cwd) {
@@ -1386,15 +1386,15 @@ extern "C" LEAN_EXPORT obj_res lean_io_current_dir(obj_arg) {
// =======================================
// ST ref primitives
extern "C" LEAN_EXPORT obj_res lean_st_mk_ref(obj_arg a, obj_arg) {
extern "C" LEAN_EXPORT obj_res lean_st_mk_ref(obj_arg a) {
lean_ref_object * o = (lean_ref_object*)lean_alloc_small_object(sizeof(lean_ref_object));
lean_set_st_header((lean_object*)o, LeanRef, 0);
o->m_value = a;
return io_result_mk_ok((lean_object*)o);
return (lean_object*)o;
}
static object * g_io_error_nullptr_read = nullptr;
static inline atomic<object*> * mt_ref_val_addr(object * o) {
return reinterpret_cast<atomic<object*> *>(&(lean_to_ref(o)->m_value));
}
@@ -1412,7 +1412,7 @@ static inline atomic<object*> * mt_ref_val_addr(object * o) {
*/
static inline bool ref_maybe_mt(b_obj_arg ref) { return lean_is_mt(ref) || lean_is_persistent(ref); }
extern "C" LEAN_EXPORT obj_res lean_st_ref_get(b_obj_arg ref, obj_arg) {
extern "C" LEAN_EXPORT obj_res lean_st_ref_get(b_obj_arg ref) {
if (ref_maybe_mt(ref)) {
atomic<object *> * val_addr = mt_ref_val_addr(ref);
while (true) {
@@ -1428,36 +1428,36 @@ extern "C" LEAN_EXPORT obj_res lean_st_ref_get(b_obj_arg ref, obj_arg) {
/* this may happen if another thread wrote `ref` */
dec(tmp);
}
return io_result_mk_ok(val);
return val;
}
}
} else {
object * val = lean_to_ref(ref)->m_value;
lean_assert(val != nullptr);
inc(val);
return io_result_mk_ok(val);
return val;
}
}
extern "C" LEAN_EXPORT obj_res lean_st_ref_take(b_obj_arg ref, obj_arg) {
extern "C" LEAN_EXPORT obj_res lean_st_ref_take(b_obj_arg ref) {
if (ref_maybe_mt(ref)) {
atomic<object *> * val_addr = mt_ref_val_addr(ref);
while (true) {
object * val = val_addr->exchange(nullptr);
if (val != nullptr)
return io_result_mk_ok(val);
return val;
}
} else {
object * val = lean_to_ref(ref)->m_value;
lean_assert(val != nullptr);
lean_to_ref(ref)->m_value = nullptr;
return io_result_mk_ok(val);
return val;
}
}
static_assert(sizeof(atomic<unsigned short>) == sizeof(unsigned short), "`atomic<unsigned short>` and `unsigned short` must have the same size"); // NOLINT
extern "C" LEAN_EXPORT obj_res lean_st_ref_set(b_obj_arg ref, obj_arg a, obj_arg) {
extern "C" LEAN_EXPORT obj_res lean_st_ref_set(b_obj_arg ref, obj_arg a) {
if (ref_maybe_mt(ref)) {
/* We must mark `a` as multi-threaded if `ref` is marked as multi-threaded.
Reason: our runtime relies on the fact that a single-threaded object
@@ -1467,16 +1467,16 @@ extern "C" LEAN_EXPORT obj_res lean_st_ref_set(b_obj_arg ref, obj_arg a, obj_arg
object * old_a = val_addr->exchange(a);
if (old_a != nullptr)
dec(old_a);
return io_result_mk_ok(box(0));
return box(0);
} else {
if (lean_to_ref(ref)->m_value != nullptr)
dec(lean_to_ref(ref)->m_value);
lean_to_ref(ref)->m_value = a;
return io_result_mk_ok(box(0));
return box(0);
}
}
extern "C" LEAN_EXPORT obj_res lean_st_ref_swap(b_obj_arg ref, obj_arg a, obj_arg) {
extern "C" LEAN_EXPORT obj_res lean_st_ref_swap(b_obj_arg ref, obj_arg a) {
if (ref_maybe_mt(ref)) {
/* See io_ref_write */
mark_mt(a);
@@ -1484,94 +1484,92 @@ extern "C" LEAN_EXPORT obj_res lean_st_ref_swap(b_obj_arg ref, obj_arg a, obj_ar
while (true) {
object * old_a = val_addr->exchange(a);
if (old_a != nullptr)
return io_result_mk_ok(old_a);
return old_a;
}
} else {
object * old_a = lean_to_ref(ref)->m_value;
if (old_a == nullptr)
return io_result_mk_error(g_io_error_nullptr_read);
lean_internal_panic("null reference read");
lean_to_ref(ref)->m_value = a;
return io_result_mk_ok(old_a);
return old_a;
}
}
extern "C" LEAN_EXPORT obj_res lean_st_ref_ptr_eq(b_obj_arg ref1, b_obj_arg ref2, obj_arg) {
extern "C" LEAN_EXPORT obj_res lean_st_ref_ptr_eq(b_obj_arg ref1, b_obj_arg ref2) {
// TODO(Leo): ref_maybe_mt
bool r = lean_to_ref(ref1)->m_value == lean_to_ref(ref2)->m_value;
return io_result_mk_ok(box(r));
return box(r);
}
/* {α : Type} (act : BaseIO α) (_ : IO.RealWorld) : α */
static obj_res lean_io_as_task_fn(obj_arg act, obj_arg) {
/* {α : Type} (act : BaseIO α) : α */
static obj_res lean_io_as_task_fn(obj_arg act) {
object_ref r(apply_1(act, io_mk_world()));
return object_ref(io_result_get_value(r.raw()), true).steal();
return object_ref(r.raw(), true).steal();
}
/* asTask {α : Type} (act : BaseIO α) (prio : Nat) : BaseIO (Task α) */
extern "C" LEAN_EXPORT obj_res lean_io_as_task(obj_arg act, obj_arg prio, obj_arg) {
extern "C" LEAN_EXPORT obj_res lean_io_as_task(obj_arg act, obj_arg prio) {
object * c = lean_alloc_closure((void*)lean_io_as_task_fn, 2, 1);
lean_closure_set(c, 0, act);
object * t = lean_task_spawn_core(c, lean_unbox(prio), /* keep_alive */ true);
return io_result_mk_ok(t);
return t;
}
/* {α β : Type} (f : α → BaseIO β) (a : α) : β */
static obj_res lean_io_bind_task_fn(obj_arg f, obj_arg a) {
object_ref r(apply_2(f, a, io_mk_world()));
return object_ref(io_result_get_value(r.raw()), true).steal();
return object_ref(r.raw(), true).steal();
}
/* mapTask (f : α → BaseIO β) (t : Task α) (prio : Nat) (sync : Bool) : BaseIO (Task β) */
extern "C" LEAN_EXPORT obj_res lean_io_map_task(obj_arg f, obj_arg t, obj_arg prio, uint8 sync,
obj_arg) {
extern "C" LEAN_EXPORT obj_res lean_io_map_task(obj_arg f, obj_arg t, obj_arg prio, uint8 sync) {
object * c = lean_alloc_closure((void*)lean_io_bind_task_fn, 2, 1);
lean_closure_set(c, 0, f);
object * t2 = lean_task_map_core(c, t, lean_unbox(prio), sync, /* keep_alive */ true);
return io_result_mk_ok(t2);
return t2;
}
/* bindTask (t : Task α) (f : α → BaseIO (Task β)) (prio : Nat) (sync : Bool) : BaseIO (Task β) */
extern "C" LEAN_EXPORT obj_res lean_io_bind_task(obj_arg t, obj_arg f, obj_arg prio, uint8 sync,
obj_arg) {
extern "C" LEAN_EXPORT obj_res lean_io_bind_task(obj_arg t, obj_arg f, obj_arg prio, uint8 sync) {
object * c = lean_alloc_closure((void*)lean_io_bind_task_fn, 2, 1);
lean_closure_set(c, 0, f);
object * t2 = lean_task_bind_core(t, c, lean_unbox(prio), sync, /* keep_alive */ true);
return io_result_mk_ok(t2);
return t2;
}
extern "C" LEAN_EXPORT obj_res lean_io_check_canceled(obj_arg) {
return io_result_mk_ok(box(lean_io_check_canceled_core()));
extern "C" LEAN_EXPORT uint8_t lean_io_check_canceled() {
return lean_io_check_canceled_core();
}
extern "C" LEAN_EXPORT obj_res lean_io_cancel(b_obj_arg t, obj_arg) {
extern "C" LEAN_EXPORT obj_res lean_io_cancel(b_obj_arg t) {
lean_io_cancel_core(t);
return io_result_mk_ok(box(0));
return box(0);
}
extern "C" LEAN_EXPORT obj_res lean_io_get_task_state(b_obj_arg t, obj_arg) {
return io_result_mk_ok(box(lean_io_get_task_state_core(t)));
extern "C" LEAN_EXPORT uint8_t lean_io_get_task_state(b_obj_arg t) {
return lean_io_get_task_state_core(t);
}
extern "C" LEAN_EXPORT obj_res lean_io_wait(obj_arg t, obj_arg) {
return io_result_mk_ok(lean_task_get_own(t));
extern "C" LEAN_EXPORT obj_res lean_io_wait(obj_arg t) {
return lean_task_get_own(t);
}
extern "C" LEAN_EXPORT obj_res lean_io_exit(uint8_t code, obj_arg /* w */) {
extern "C" LEAN_EXPORT obj_res lean_io_exit(uint8_t code) {
exit(code);
}
extern "C" LEAN_EXPORT obj_res lean_io_force_exit(uint8_t code, obj_arg /* w */) {
extern "C" LEAN_EXPORT obj_res lean_io_force_exit(uint8_t code) {
std::_Exit((int)code);
}
extern "C" LEAN_EXPORT obj_res lean_runtime_mark_multi_threaded(obj_arg a, obj_arg /* w */) {
extern "C" LEAN_EXPORT obj_res lean_runtime_mark_multi_threaded(obj_arg a) {
lean_mark_mt(a);
return io_result_mk_ok(a);
return a;
}
extern "C" LEAN_EXPORT obj_res lean_runtime_mark_persistent(obj_arg a, obj_arg /* w */) {
extern "C" LEAN_EXPORT obj_res lean_runtime_mark_persistent(obj_arg a) {
lean_mark_persistent(a);
return io_result_mk_ok(a);
return a;
}
#if defined(__has_feature)
@@ -1580,13 +1578,13 @@ extern "C" LEAN_EXPORT obj_res lean_runtime_mark_persistent(obj_arg a, obj_arg /
#endif
#endif
extern "C" LEAN_EXPORT obj_res lean_runtime_forget(obj_arg o, obj_arg /* w */) {
extern "C" LEAN_EXPORT obj_res lean_runtime_forget(obj_arg o) {
#if defined(__has_feature)
#if __has_feature(address_sanitizer)
__lsan_ignore_object(o);
#endif
#endif
return io_result_mk_ok(box(0));
return box(0);
}
extern "C" LEAN_EXPORT obj_res lean_option_get_or_block(obj_arg o_opt) {
@@ -1604,8 +1602,6 @@ extern "C" LEAN_EXPORT obj_res lean_option_get_or_block(obj_arg o_opt) {
}
void initialize_io() {
g_io_error_nullptr_read = lean_mk_io_user_error(mk_ascii_string_unchecked("null reference read"));
mark_persistent(g_io_error_nullptr_read);
g_io_handle_external_class = lean_register_external_class(io_handle_finalizer, io_handle_foreach);
#if defined(LEAN_WINDOWS)
_setmode(_fileno(stdout), _O_BINARY);

4
src/runtime/memory.cpp
View File

@@ -114,7 +114,7 @@ namespace lean {
static size_t g_max_memory = 0;
LEAN_THREAD_VALUE(size_t, g_counter, 0);
extern "C" LEAN_EXPORT lean_obj_res lean_internal_get_default_max_memory(lean_obj_arg) {
extern "C" LEAN_EXPORT lean_obj_res lean_internal_get_default_max_memory() {
#ifdef LEAN_DEFAULT_MAX_MEMORY
return lean_box(LEAN_DEFAULT_MAX_MEMORY);
#else
@@ -128,7 +128,7 @@ void set_max_memory(size_t max) {
extern "C" LEAN_EXPORT lean_obj_res lean_internal_set_max_memory(size_t max) {
set_max_memory(max);
return lean_io_result_mk_ok(lean_box(0));
return lean_box(0);
}
void set_max_memory_megabyte(unsigned max) {

76
src/runtime/mutex.cpp
View File

@@ -22,23 +22,23 @@ static mutex * basemutex_get(lean_object * mtx) {
return static_cast<mutex *>(lean_get_external_data(mtx));
}
extern "C" LEAN_EXPORT obj_res lean_io_basemutex_new(obj_arg) {
return io_result_mk_ok(lean_alloc_external(g_basemutex_external_class, new mutex));
extern "C" LEAN_EXPORT obj_res lean_io_basemutex_new() {
return lean_alloc_external(g_basemutex_external_class, new mutex);
}
extern "C" LEAN_EXPORT obj_res lean_io_basemutex_lock(b_obj_arg mtx, obj_arg) {
extern "C" LEAN_EXPORT obj_res lean_io_basemutex_lock(b_obj_arg mtx) {
basemutex_get(mtx)->lock();
return io_result_mk_ok(box(0));
return box(0);
}
extern "C" LEAN_EXPORT obj_res lean_io_basemutex_try_lock(b_obj_arg mtx, obj_arg) {
extern "C" LEAN_EXPORT uint8_t lean_io_basemutex_try_lock(b_obj_arg mtx) {
bool success = basemutex_get(mtx)->try_lock();
return io_result_mk_ok(box(success));
return success;
}
extern "C" LEAN_EXPORT obj_res lean_io_basemutex_unlock(b_obj_arg mtx, obj_arg) {
extern "C" LEAN_EXPORT obj_res lean_io_basemutex_unlock(b_obj_arg mtx) {
basemutex_get(mtx)->unlock();
return io_result_mk_ok(box(0));
return box(0);
}
static lean_external_class * g_condvar_external_class = nullptr;
@@ -51,25 +51,25 @@ static condition_variable * condvar_get(lean_object * mtx) {
return static_cast<condition_variable *>(lean_get_external_data(mtx));
}
extern "C" LEAN_EXPORT obj_res lean_io_condvar_new(obj_arg) {
return io_result_mk_ok(lean_alloc_external(g_condvar_external_class, new condition_variable));
extern "C" LEAN_EXPORT obj_res lean_io_condvar_new() {
return lean_alloc_external(g_condvar_external_class, new condition_variable);
}
extern "C" LEAN_EXPORT obj_res lean_io_condvar_wait(b_obj_arg condvar, b_obj_arg mtx, obj_arg) {
extern "C" LEAN_EXPORT obj_res lean_io_condvar_wait(b_obj_arg condvar, b_obj_arg mtx) {
unique_lock<mutex> lock(*basemutex_get(mtx), std::adopt_lock_t());
condvar_get(condvar)->wait(lock);
lock.release();
return io_result_mk_ok(box(0));
return box(0);
}
extern "C" LEAN_EXPORT obj_res lean_io_condvar_notify_one(b_obj_arg condvar, obj_arg) {
extern "C" LEAN_EXPORT obj_res lean_io_condvar_notify_one(b_obj_arg condvar) {
condvar_get(condvar)->notify_one();
return io_result_mk_ok(box(0));
return box(0);
}
extern "C" LEAN_EXPORT obj_res lean_io_condvar_notify_all(b_obj_arg condvar, obj_arg) {
extern "C" LEAN_EXPORT obj_res lean_io_condvar_notify_all(b_obj_arg condvar) {
condvar_get(condvar)->notify_all();
return io_result_mk_ok(box(0));
return box(0);
}
static lean_external_class * g_baserecmutex_external_class = nullptr;
@@ -82,23 +82,23 @@ static recursive_mutex * baserecmutex_get(lean_object * mtx) {
return static_cast<recursive_mutex *>(lean_get_external_data(mtx));
}
extern "C" LEAN_EXPORT obj_res lean_io_baserecmutex_new(obj_arg) {
return io_result_mk_ok(lean_alloc_external(g_baserecmutex_external_class, new recursive_mutex));
extern "C" LEAN_EXPORT obj_res lean_io_baserecmutex_new() {
return lean_alloc_external(g_baserecmutex_external_class, new recursive_mutex);
}
extern "C" LEAN_EXPORT obj_res lean_io_baserecmutex_lock(b_obj_arg mtx, obj_arg) {
extern "C" LEAN_EXPORT obj_res lean_io_baserecmutex_lock(b_obj_arg mtx) {
baserecmutex_get(mtx)->lock();
return io_result_mk_ok(box(0));
return box(0);
}
extern "C" LEAN_EXPORT obj_res lean_io_baserecmutex_try_lock(b_obj_arg mtx, obj_arg) {
extern "C" LEAN_EXPORT uint8_t lean_io_baserecmutex_try_lock(b_obj_arg mtx) {
bool success = baserecmutex_get(mtx)->try_lock();
return io_result_mk_ok(box(success));
return success;
}
extern "C" LEAN_EXPORT obj_res lean_io_baserecmutex_unlock(b_obj_arg mtx, obj_arg) {
extern "C" LEAN_EXPORT obj_res lean_io_baserecmutex_unlock(b_obj_arg mtx) {
baserecmutex_get(mtx)->unlock();
return io_result_mk_ok(box(0));
return box(0);
}
// We use a `shared_timed_mutex` instead of a `shared_mutex` for now as the latter is only available
@@ -113,38 +113,38 @@ static shared_timed_mutex * basesharedmutex_get(lean_object * mtx) {
return static_cast<shared_timed_mutex *>(lean_get_external_data(mtx));
}
extern "C" LEAN_EXPORT obj_res lean_io_basesharedmutex_new(obj_arg) {
return io_result_mk_ok(lean_alloc_external(g_basesharedmutex_external_class, new shared_timed_mutex));
extern "C" LEAN_EXPORT obj_res lean_io_basesharedmutex_new() {
return lean_alloc_external(g_basesharedmutex_external_class, new shared_timed_mutex);
}
extern "C" LEAN_EXPORT obj_res lean_io_basesharedmutex_write(b_obj_arg mtx, obj_arg) {
extern "C" LEAN_EXPORT obj_res lean_io_basesharedmutex_write(b_obj_arg mtx) {
basesharedmutex_get(mtx)->lock();
return io_result_mk_ok(box(0));
return box(0);
}
extern "C" LEAN_EXPORT obj_res lean_io_basesharedmutex_try_write(b_obj_arg mtx, obj_arg) {
extern "C" LEAN_EXPORT uint8_t lean_io_basesharedmutex_try_write(b_obj_arg mtx) {
bool success = basesharedmutex_get(mtx)->try_lock();
return io_result_mk_ok(box(success));
return success;
}
extern "C" LEAN_EXPORT obj_res lean_io_basesharedmutex_unlock_write(b_obj_arg mtx, obj_arg) {
extern "C" LEAN_EXPORT obj_res lean_io_basesharedmutex_unlock_write(b_obj_arg mtx) {
basesharedmutex_get(mtx)->unlock();
return io_result_mk_ok(box(0));
return box(0);
}
extern "C" LEAN_EXPORT obj_res lean_io_basesharedmutex_read(b_obj_arg mtx, obj_arg) {
extern "C" LEAN_EXPORT obj_res lean_io_basesharedmutex_read(b_obj_arg mtx) {
basesharedmutex_get(mtx)->lock_shared();
return io_result_mk_ok(box(0));
return box(0);
}
extern "C" LEAN_EXPORT obj_res lean_io_basesharedmutex_try_read(b_obj_arg mtx, obj_arg) {
extern "C" LEAN_EXPORT uint8_t lean_io_basesharedmutex_try_read(b_obj_arg mtx) {
bool success = basesharedmutex_get(mtx)->try_lock_shared();
return io_result_mk_ok(box(success));
return success;
}
extern "C" LEAN_EXPORT obj_res lean_io_basesharedmutex_unlock_read(b_obj_arg mtx, obj_arg) {
extern "C" LEAN_EXPORT obj_res lean_io_basesharedmutex_unlock_read(b_obj_arg mtx) {
basesharedmutex_get(mtx)->unlock_shared();
return io_result_mk_ok(box(0));
return box(0);
}
void initialize_mutex() {

14
src/runtime/object.cpp
View File

@@ -1065,7 +1065,7 @@ extern "C" LEAN_EXPORT obj_res lean_task_pure(obj_arg a) {
return (lean_object*)alloc_task(a);
}
static obj_res task_map_fn(obj_arg f, obj_arg t, obj_arg) {
static obj_res task_map_fn(obj_arg f, obj_arg t, obj_arg w) {
b_obj_res v = lean_to_task(t)->m_value;
lean_assert(v != nullptr);
lean_inc(v);
@@ -1188,14 +1188,14 @@ void lean_promise_resolve(obj_arg value, b_obj_arg promise) {
g_task_manager->resolve(lean_to_promise(promise)->m_result, mk_option_some(value));
}
extern "C" LEAN_EXPORT obj_res lean_io_promise_new(obj_arg) {
extern "C" LEAN_EXPORT obj_res lean_io_promise_new() {
lean_object * o = lean_promise_new();
return io_result_mk_ok(o);
return o;
}
extern "C" LEAN_EXPORT obj_res lean_io_promise_resolve(obj_arg value, b_obj_arg promise, obj_arg) {
extern "C" LEAN_EXPORT obj_res lean_io_promise_resolve(obj_arg value, b_obj_arg promise) {
lean_promise_resolve(value, promise);
return io_result_mk_ok(box(0));
return box(0);
}
extern "C" LEAN_EXPORT obj_res lean_io_promise_result_opt(b_obj_arg promise) {
@@ -2636,9 +2636,9 @@ extern "C" LEAN_EXPORT object * lean_max_small_nat(object *) {
// =======================================
// Debugging helper functions
extern "C" obj_res lean_io_eprintln(obj_arg s, obj_arg w);
extern "C" obj_res lean_io_eprintln(obj_arg s);
void io_eprintln(obj_arg s) {
object * r = lean_io_eprintln(s, lean_io_mk_world());
object * r = lean_io_eprintln(s);
lean_assert(lean_io_result_is_ok(r));
lean_dec(r);
}

14
src/runtime/object.h
View File

@@ -466,17 +466,17 @@ LEAN_EXPORT void io_eprintln(obj_arg s);
// =======================================
// ST ref primitives
inline obj_res st_mk_ref(obj_arg v, obj_arg w) { return lean_st_mk_ref(v, w); }
inline obj_res st_ref_get(b_obj_arg r, obj_arg w) { return lean_st_ref_get(r, w); }
inline obj_res st_ref_set(b_obj_arg r, obj_arg v, obj_arg w) { return lean_st_ref_set(r, v, w); }
inline obj_res st_ref_reset(b_obj_arg r, obj_arg w) { return lean_st_ref_reset(r, w); }
inline obj_res st_ref_swap(b_obj_arg r, obj_arg v, obj_arg w) { return lean_st_ref_swap(r, v, w); }
inline obj_res st_mk_ref(obj_arg v) { return lean_st_mk_ref(v); }
inline obj_res st_ref_get(b_obj_arg r) { return lean_st_ref_get(r); }
inline obj_res st_ref_set(b_obj_arg r, obj_arg v) { return lean_st_ref_set(r, v); }
inline obj_res st_ref_reset(b_obj_arg r) { return lean_st_ref_reset(r); }
inline obj_res st_ref_swap(b_obj_arg r, obj_arg v) { return lean_st_ref_swap(r, v); }
obj_res lean_promise_new();
void lean_promise_resolve(obj_arg value, b_obj_arg promise);
extern "C" LEAN_EXPORT obj_res lean_io_promise_new(obj_arg);
extern "C" LEAN_EXPORT obj_res lean_io_promise_resolve(obj_arg value, b_obj_arg promise, obj_arg);
extern "C" LEAN_EXPORT obj_res lean_io_promise_new();
extern "C" LEAN_EXPORT obj_res lean_io_promise_resolve(obj_arg value, b_obj_arg promise);
extern "C" LEAN_EXPORT obj_res lean_io_promise_result_opt(obj_arg promise);
extern "C" LEAN_EXPORT obj_res lean_get_or_block(obj_arg opt);

42
src/runtime/process.cpp
View File

@@ -62,7 +62,7 @@ lean_object * wrap_win_handle(HANDLE h) {
return lean_alloc_external(g_win_handle_external_class, static_cast<void *>(h));
}
extern "C" LEAN_EXPORT obj_res lean_io_process_get_current_dir(obj_arg) {
extern "C" LEAN_EXPORT obj_res lean_io_process_get_current_dir() {
char path[MAX_PATH];
DWORD sz = GetCurrentDirectory(MAX_PATH, path);
if (sz != 0) {
@@ -72,7 +72,7 @@ extern "C" LEAN_EXPORT obj_res lean_io_process_get_current_dir(obj_arg) {
}
}
extern "C" LEAN_EXPORT obj_res lean_io_process_set_current_dir(b_obj_arg path, obj_arg) {
extern "C" LEAN_EXPORT obj_res lean_io_process_set_current_dir(b_obj_arg path) {
if (SetCurrentDirectory(string_cstr(path))) {
return io_result_mk_ok(box(0));
} else {
@@ -80,15 +80,15 @@ extern "C" LEAN_EXPORT obj_res lean_io_process_set_current_dir(b_obj_arg path, o
}
}
extern "C" LEAN_EXPORT obj_res lean_io_process_get_pid(obj_arg) {
return lean_io_result_mk_ok(box_uint32(GetCurrentProcessId()));
extern "C" LEAN_EXPORT uint32_t lean_io_process_get_pid() {
return GetCurrentProcessId();
}
extern "C" LEAN_EXPORT obj_res lean_io_get_tid(obj_arg) {
return lean_io_result_mk_ok(box_uint64(GetCurrentThreadId()));
extern "C" LEAN_EXPORT uint64_t lean_io_get_tid() {
return GetCurrentThreadId();
}
extern "C" LEAN_EXPORT obj_res lean_io_process_child_wait(b_obj_arg, b_obj_arg child, obj_arg) {
extern "C" LEAN_EXPORT obj_res lean_io_process_child_wait(b_obj_arg, b_obj_arg child) {
HANDLE h = static_cast<HANDLE>(lean_get_external_data(cnstr_get(child, 3)));
DWORD exit_code;
if (WaitForSingleObject(h, INFINITE) == WAIT_FAILED) {
@@ -100,7 +100,7 @@ extern "C" LEAN_EXPORT obj_res lean_io_process_child_wait(b_obj_arg, b_obj_arg c
return lean_io_result_mk_ok(box_uint32(exit_code));
}
extern "C" LEAN_EXPORT obj_res lean_io_process_child_try_wait(b_obj_arg, b_obj_arg child, obj_arg) {
extern "C" LEAN_EXPORT obj_res lean_io_process_child_try_wait(b_obj_arg, b_obj_arg child) {
HANDLE h = static_cast<HANDLE>(lean_get_external_data(cnstr_get(child, 3)));
DWORD exit_code;
DWORD ret = WaitForSingleObject(h, 0);
@@ -116,7 +116,7 @@ extern "C" LEAN_EXPORT obj_res lean_io_process_child_try_wait(b_obj_arg, b_obj_a
}
}
extern "C" LEAN_EXPORT obj_res lean_io_process_child_kill(b_obj_arg, b_obj_arg child, obj_arg) {
extern "C" LEAN_EXPORT obj_res lean_io_process_child_kill(b_obj_arg, b_obj_arg child) {
HANDLE h = static_cast<HANDLE>(lean_get_external_data(cnstr_get(child, 3)));
if (!TerminateProcess(h, 1)) {
return io_result_mk_error((sstream() << GetLastError()).str());
@@ -300,7 +300,7 @@ static obj_res spawn(string_ref const & proc_name, array_ref<string_ref> const &
return lean_io_result_mk_ok(r.steal());
}
extern "C" LEAN_EXPORT obj_res lean_io_process_child_take_stdin(b_obj_arg, obj_arg lchild, obj_arg) {
extern "C" LEAN_EXPORT obj_res lean_io_process_child_take_stdin(b_obj_arg, obj_arg lchild) {
object_ref child(lchild);
object_ref child2 = mk_cnstr(0, object_ref(box(0)), cnstr_get_ref(child, 1), cnstr_get_ref(child, 2), cnstr_get_ref(child, 3));
object_ref r = mk_cnstr(0, cnstr_get_ref(child, 0), child2);
@@ -314,7 +314,7 @@ void finalize_process() {}
#else
extern "C" LEAN_EXPORT obj_res lean_io_process_get_current_dir(obj_arg) {
extern "C" LEAN_EXPORT obj_res lean_io_process_get_current_dir() {
char path[PATH_MAX];
if (getcwd(path, PATH_MAX)) {
return io_result_mk_ok(mk_string(path));
@@ -323,7 +323,7 @@ extern "C" LEAN_EXPORT obj_res lean_io_process_get_current_dir(obj_arg) {
}
}
extern "C" LEAN_EXPORT obj_res lean_io_process_set_current_dir(b_obj_arg path, obj_arg) {
extern "C" LEAN_EXPORT obj_res lean_io_process_set_current_dir(b_obj_arg path) {
if (!chdir(string_cstr(path))) {
return io_result_mk_ok(box(0));
} else {
@@ -331,12 +331,12 @@ extern "C" LEAN_EXPORT obj_res lean_io_process_set_current_dir(b_obj_arg path, o
}
}
extern "C" LEAN_EXPORT obj_res lean_io_process_get_pid(obj_arg) {
extern "C" LEAN_EXPORT uint32_t lean_io_process_get_pid() {
static_assert(sizeof(pid_t) == sizeof(uint32), "pid_t is expected to be a 32-bit type"); // NOLINT
return lean_io_result_mk_ok(box_uint32(getpid()));
return getpid();
}
extern "C" LEAN_EXPORT obj_res lean_io_get_tid(obj_arg) {
extern "C" LEAN_EXPORT uint64_t lean_io_get_tid() {
uint64_t tid;
#ifdef __APPLE__
lean_always_assert(pthread_threadid_np(NULL, &tid) == 0);
@@ -347,10 +347,10 @@ extern "C" LEAN_EXPORT obj_res lean_io_get_tid(obj_arg) {
// glibc 2.30 would provide a wrapper
tid = (pid_t)syscall(SYS_gettid);
#endif
return lean_io_result_mk_ok(box_uint64(tid));
return tid;
}
extern "C" LEAN_EXPORT obj_res lean_io_process_child_wait(b_obj_arg, b_obj_arg child, obj_arg) {
extern "C" LEAN_EXPORT obj_res lean_io_process_child_wait(b_obj_arg, b_obj_arg child) {
static_assert(sizeof(pid_t) == sizeof(uint32), "pid_t is expected to be a 32-bit type"); // NOLINT
pid_t pid = cnstr_get_uint32(child, 3 * sizeof(object *));
int status;
@@ -366,7 +366,7 @@ extern "C" LEAN_EXPORT obj_res lean_io_process_child_wait(b_obj_arg, b_obj_arg c
}
}
extern "C" LEAN_EXPORT obj_res lean_io_process_child_try_wait(b_obj_arg, b_obj_arg child, obj_arg) {
extern "C" LEAN_EXPORT obj_res lean_io_process_child_try_wait(b_obj_arg, b_obj_arg child) {
static_assert(sizeof(pid_t) == sizeof(uint32), "pid_t is expected to be a 32-bit type"); // NOLINT
pid_t pid = cnstr_get_uint32(child, 3 * sizeof(object *));
int status;
@@ -388,7 +388,7 @@ extern "C" LEAN_EXPORT obj_res lean_io_process_child_try_wait(b_obj_arg, b_obj_a
}
}
extern "C" LEAN_EXPORT obj_res lean_io_process_child_kill(b_obj_arg, b_obj_arg child, obj_arg) {
extern "C" LEAN_EXPORT obj_res lean_io_process_child_kill(b_obj_arg, b_obj_arg child) {
static_assert(sizeof(pid_t) == sizeof(uint32), "pid_t is expected to be a 32-bit type"); // NOLINT
pid_t pid = cnstr_get_uint32(child, 3 * sizeof(object *));
bool setsid = cnstr_get_uint8(child, 3 * sizeof(object *) + sizeof(pid_t));
@@ -534,7 +534,7 @@ static obj_res spawn(string_ref const & proc_name, array_ref<string_ref> const &
return lean_io_result_mk_ok(r.steal());
}
extern "C" LEAN_EXPORT obj_res lean_io_process_child_take_stdin(b_obj_arg, obj_arg lchild, obj_arg) {
extern "C" LEAN_EXPORT obj_res lean_io_process_child_take_stdin(b_obj_arg, obj_arg lchild) {
object_ref child(lchild);
object_ref child2 = mk_cnstr(0, object_ref(box(0)), cnstr_get_ref(child, 1), cnstr_get_ref(child, 2), sizeof(pid_t));
cnstr_set_uint32(child2.raw(), 3 * sizeof(object *), cnstr_get_uint32(child.raw(), 3 * sizeof(object *)));
@@ -549,7 +549,7 @@ void finalize_process() {}
extern "C" lean_object* lean_mk_io_error_other_error(uint32_t, lean_object*);
extern "C" LEAN_EXPORT obj_res lean_io_process_spawn(obj_arg args_, obj_arg) {
extern "C" LEAN_EXPORT obj_res lean_io_process_spawn(obj_arg args_) {
object_ref args(args_);
object_ref stdio_cfg = cnstr_get_ref(args, 0);
stdio stdin_mode = static_cast<stdio>(cnstr_get_uint8(stdio_cfg.raw(), 0));

8
src/runtime/uv/dns.cpp
View File

@@ -33,7 +33,7 @@ bool is_safe_ascii_str(const char *s, size_t len) {
}
// Std.Internal.IO.Async.DNS.getAddrInfo (host service : @& String) (family : UInt8) : IO (IO.Promise (Except IO.Error (Array IPAddr)))
extern "C" LEAN_EXPORT lean_obj_res lean_uv_dns_get_info(b_obj_arg name, b_obj_arg service, uint8_t family, obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_dns_get_info(b_obj_arg name, b_obj_arg service, uint8_t family) {
char const * name_cstr = lean_string_cstr(name);
char const * service_cstr = lean_string_cstr(service);
@@ -122,7 +122,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_dns_get_info(b_obj_arg name, b_obj_a
}
// Std.Internal.IO.Async.DNS.getNameInfo (host : @& SocketAddress) : IO (IO.Promise (Except IO.Error (String × String)))
extern "C" LEAN_EXPORT lean_obj_res lean_uv_dns_get_name(b_obj_arg addr, obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_dns_get_name(b_obj_arg addr) {
lean_object* promise = lean_promise_new();
mark_mt(promise);
@@ -173,14 +173,14 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_dns_get_name(b_obj_arg addr, obj_arg
#else
// Std.Internal.IO.Async.DNS.getAddrInfo (host service : @& String) (family : UInt8) : IO (IO.Promise (Except IO.Error (Array IPAddr)))
extern "C" LEAN_EXPORT lean_obj_res lean_uv_dns_get_info(b_obj_arg name, b_obj_arg service, uint8_t family, int8_t protocol, obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_dns_get_info(b_obj_arg name, b_obj_arg service, uint8_t family, int8_t protocol) {
lean_always_assert(
false && ("Please build a version of Lean4 with libuv to invoke this.")
);
}
// Std.Internal.IO.Async.DNS.getNameInfo (host : @& SocketAddress) : IO (IO.Promise (Except IO.Error (String × String)))
extern "C" LEAN_EXPORT lean_obj_res lean_uv_dns_get_name(b_obj_arg ip_addr, obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_dns_get_name(b_obj_arg ip_addr) {
lean_always_assert(
false && ("Please build a version of Lean4 with libuv to invoke this.")
);

4
src/runtime/uv/dns.h
View File

@@ -19,7 +19,7 @@ using namespace std;
// =======================================
// DNS functions
extern "C" LEAN_EXPORT lean_obj_res lean_uv_dns_get_info(b_obj_arg name, b_obj_arg service, uint8_t family, obj_arg /* w */);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_dns_get_name(b_obj_arg ip_addr, obj_arg /* w */);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_dns_get_info(b_obj_arg name, b_obj_arg service, uint8_t family);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_dns_get_name(b_obj_arg ip_addr);
}

16
src/runtime/uv/event_loop.cpp
View File

@@ -102,7 +102,7 @@ void event_loop_run_loop(event_loop_t * event_loop) {
}
/* Std.Internal.UV.Loop.configure (options : Loop.Options) : BaseIO Unit */
extern "C" LEAN_EXPORT lean_obj_res lean_uv_event_loop_configure(b_obj_arg options, obj_arg /* w */ ) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_event_loop_configure(b_obj_arg options) {
bool accum = lean_ctor_get_uint8(options, 0);
bool block = lean_ctor_get_uint8(options, 1);
@@ -122,16 +122,16 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_event_loop_configure(b_obj_arg optio
event_loop_unlock(&global_ev);
return lean_io_result_mk_ok(lean_box(0));
return lean_box(0);
}
/* Std.Internal.UV.Loop.alive : BaseIO UInt64 */
extern "C" LEAN_EXPORT lean_obj_res lean_uv_event_loop_alive(obj_arg /* w */ ) {
/* Std.Internal.UV.Loop.alive : BaseIO Bool */
extern "C" LEAN_EXPORT uint8_t lean_uv_event_loop_alive() {
event_loop_lock(&global_ev);
int is_alive = uv_loop_alive(global_ev.loop);
event_loop_unlock(&global_ev);
return lean_io_result_mk_ok(lean_box(is_alive));
return is_alive;
}
void initialize_libuv_loop() {
@@ -141,15 +141,15 @@ void initialize_libuv_loop() {
#else
/* Std.Internal.UV.Loop.configure (options : Loop.Options) : BaseIO Unit */
extern "C" LEAN_EXPORT lean_obj_res lean_uv_event_loop_configure(b_obj_arg options, obj_arg /* w */ ) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_event_loop_configure(b_obj_arg options) {
return io_result_mk_error("lean_uv_event_loop_configure is not supported");
}
/* Std.Internal.UV.Loop.alive : BaseIO UInt64 */
extern "C" LEAN_EXPORT lean_obj_res lean_uv_event_loop_alive(obj_arg /* w */ ) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_event_loop_alive() {
return io_result_mk_error("lean_uv_event_loop_alive is not supported");
}
#endif
}
}

4
src/runtime/uv/event_loop.h
View File

@@ -44,8 +44,8 @@ void event_loop_run_loop(event_loop_t *event_loop);
// =======================================
// Global event loop manipulation functions
extern "C" LEAN_EXPORT lean_obj_res lean_uv_event_loop_configure(b_obj_arg options, obj_arg /* w */ );
extern "C" LEAN_EXPORT lean_obj_res lean_uv_event_loop_alive(obj_arg /* w */ );
extern "C" LEAN_EXPORT lean_obj_res lean_uv_event_loop_configure(b_obj_arg options);
extern "C" LEAN_EXPORT uint8_t lean_uv_event_loop_alive();
// Helpers

4
src/runtime/uv/net_addr.cpp
View File

@@ -217,7 +217,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_ntop_v6(b_obj_arg ipv6_addr) {
}
/* Std.Net.networkInterface : IO (Array InterfaceAddress) */
extern "C" LEAN_EXPORT lean_obj_res lean_uv_interface_addresses(obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_interface_addresses() {
uv_interface_address_t* info;
int count;
@@ -291,7 +291,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_ntop_v6(b_obj_arg ipv6_addr) {
}
/* Std.Net.networkInterface : IO (Array InterfaceAddress) */
extern "C" LEAN_EXPORT lean_obj_res lean_uv_interface_addresses(obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_interface_addresses() {
lean_always_assert(
false && ("Please build a version of Lean4 with libuv to invoke this.")
);

2
src/runtime/uv/net_addr.h
View File

@@ -38,7 +38,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_pton_v4(b_obj_arg str_obj);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_ntop_v4(b_obj_arg ipv4_addr);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_pton_v6(b_obj_arg str_obj);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_ntop_v6(b_obj_arg ipv6_addr);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_interface_addresses(obj_arg /* w */);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_interface_addresses();
}

29
src/runtime/uv/signal.cpp
View File

@@ -50,12 +50,12 @@ void handle_signal_event(uv_signal_t* handle, int signum) {
if (signal->m_repeating) {
if (!signal_promise_is_finished(signal)) {
lean_object* res = lean_io_promise_resolve(lean_box(signum), signal->m_promise, lean_io_mk_world());
lean_object* res = lean_io_promise_resolve(lean_box(signum), signal->m_promise);
lean_dec(res);
}
} else {
if (signal->m_promise != NULL) {
lean_object* res = lean_io_promise_resolve(lean_box(signum), signal->m_promise, lean_io_mk_world());
lean_object* res = lean_io_promise_resolve(lean_box(signum), signal->m_promise);
lean_dec(res);
}
@@ -67,7 +67,7 @@ void handle_signal_event(uv_signal_t* handle, int signum) {
}
/* Std.Internal.UV.Signal.mk (signum : Int32) (repeating : Bool) : IO Signal */
extern "C" LEAN_EXPORT lean_obj_res lean_uv_signal_mk(uint32_t signum_obj, uint8_t repeating, obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_signal_mk(uint32_t signum_obj, uint8_t repeating) {
int signum = (int)(int32_t)signum_obj;
lean_uv_signal_object * signal = (lean_uv_signal_object*)malloc(sizeof(lean_uv_signal_object));
@@ -98,16 +98,11 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_signal_mk(uint32_t signum_obj, uint8
}
/* Std.Internal.UV.Signal.next (signal : @& Signal) : IO (IO.Promise Int) */
extern "C" LEAN_EXPORT lean_obj_res lean_uv_signal_next(b_obj_arg obj, obj_arg /* w */ ) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_signal_next(b_obj_arg obj) {
lean_uv_signal_object * signal = lean_to_uv_signal(obj);
auto create_promise = []() {
lean_object * prom_res = lean_io_promise_new(lean_io_mk_world());
lean_object * promise = lean_ctor_get(prom_res, 0);
lean_inc(promise);
lean_dec(prom_res);
return promise;
return lean_io_promise_new();
};
auto setup_signal = [create_promise, obj, signal]() {
@@ -190,7 +185,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_signal_next(b_obj_arg obj, obj_arg /
}
/* Std.Internal.UV.Signal.stop (signal : @& Signal) : IO Unit */
extern "C" LEAN_EXPORT lean_obj_res lean_uv_signal_stop(b_obj_arg obj, obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_signal_stop(b_obj_arg obj) {
lean_uv_signal_object * signal = lean_to_uv_signal(obj);
if (signal->m_state == SIGNAL_STATE_RUNNING) {
@@ -219,7 +214,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_signal_stop(b_obj_arg obj, obj_arg /
}
/* Std.Internal.UV.Signal.cancel (signal : @& Signal) : IO Unit */
extern "C" LEAN_EXPORT lean_obj_res lean_uv_signal_cancel(b_obj_arg obj, obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_signal_cancel(b_obj_arg obj) {
lean_uv_signal_object * signal = lean_to_uv_signal(obj);
// It's locking here to avoid changing the state during other operations.
@@ -246,28 +241,28 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_signal_cancel(b_obj_arg obj, obj_arg
#else
/* Std.Internal.UV.Signal.mk (signum : Int32) (repeating : Bool) : IO Signal */
extern "C" LEAN_EXPORT lean_obj_res lean_uv_signal_mk(uint32_t signum_obj, uint8_t repeating, obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_signal_mk(uint32_t signum_obj, uint8_t repeating) {
lean_always_assert(
false && ("Please build a version of Lean4 with libuv to invoke this.")
);
}
/* Std.Internal.UV.Signal.next (signal : @& Signal) : IO (IO.Promise Int) */
extern "C" LEAN_EXPORT lean_obj_res lean_uv_signal_next(b_obj_arg signal, obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_signal_next(b_obj_arg signal) {
lean_always_assert(
false && ("Please build a version of Lean4 with libuv to invoke this.")
);
}
/* Std.Internal.UV.Signal.stop (signal : @& Signal) : IO Unit */
extern "C" LEAN_EXPORT lean_obj_res lean_uv_signal_stop(b_obj_arg signal, obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_signal_stop(b_obj_arg signal) {
lean_always_assert(
false && ("Please build a version of Lean4 with libuv to invoke this.")
);
}
/* Std.Internal.UV.Signal.cancel (signal : @& Signal) : IO Unit */
extern "C" LEAN_EXPORT lean_obj_res lean_uv_signal_cancel(b_obj_arg obj, obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_signal_cancel(b_obj_arg obj) {
lean_always_assert(
false && ("Please build a version of Lean4 with libuv to invoke this.")
);
@@ -275,4 +270,4 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_signal_cancel(b_obj_arg obj, obj_arg
#endif
}
}

8
src/runtime/uv/signal.h
View File

@@ -48,9 +48,9 @@ static inline lean_uv_signal_object* lean_to_uv_signal(lean_object * o) { return
// =======================================
// Signal manipulation functions
extern "C" LEAN_EXPORT lean_obj_res lean_uv_signal_mk(uint32_t signum_obj, uint8_t repeating, obj_arg /* w */);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_signal_next(b_obj_arg signal, obj_arg /* w */);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_signal_stop(b_obj_arg signal, obj_arg /* w */);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_signal_cancel(b_obj_arg obj, obj_arg /* w */);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_signal_mk(uint32_t signum_obj, uint8_t repeating);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_signal_next(b_obj_arg signal);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_signal_stop(b_obj_arg signal);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_signal_cancel(b_obj_arg obj);
}

112
src/runtime/uv/system.cpp
View File

@@ -19,7 +19,7 @@ typedef struct {
} random_req_t;
// Std.Internal.UV.System.getProcessTitle : IO String
extern "C" LEAN_EXPORT lean_obj_res lean_uv_get_process_title(obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_get_process_title() {
char title[512];
int result = uv_get_process_title(title, sizeof(title));
@@ -32,7 +32,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_get_process_title(obj_arg /* w */) {
}
// Std.Internal.UV.System.setProcessTitle : String → IO Unit
extern "C" LEAN_EXPORT lean_obj_res lean_uv_set_process_title(b_obj_arg title, obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_set_process_title(b_obj_arg title) {
const char* title_str = lean_string_cstr(title);
if (strlen(title_str) != lean_string_size(title) - 1) {
return mk_embedded_nul_error(title);
@@ -47,7 +47,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_set_process_title(b_obj_arg title, o
}
// Std.Internal.UV.System.uptime : IO UInt64
extern "C" LEAN_EXPORT lean_obj_res lean_uv_uptime(obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_uptime() {
double uptime;
int result = uv_uptime(&uptime);
@@ -62,19 +62,19 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_uptime(obj_arg /* w */) {
}
// Std.Internal.UV.System.osGetPid : IO UInt64
extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_getpid(obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_getpid() {
uv_pid_t pid = uv_os_getpid();
return lean_io_result_mk_ok(lean_box_uint64(pid));
}
// Std.Internal.UV.System.osGetPpid : IO UInt64
extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_getppid(obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_getppid() {
uv_pid_t ppid = uv_os_getppid();
return lean_io_result_mk_ok(lean_box_uint64(ppid));
}
// Std.Internal.UV.System.cpuInfo : IO (Array CPUInfo)
extern "C" LEAN_EXPORT lean_obj_res lean_uv_cpu_info(obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_cpu_info() {
uv_cpu_info_t* cpu_infos;
int count;
@@ -110,7 +110,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_cpu_info(obj_arg /* w */) {
}
// Std.Internal.UV.System.cwd : IO String
extern "C" LEAN_EXPORT lean_obj_res lean_uv_cwd(obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_cwd() {
char buffer[PATH_MAX];
size_t size = sizeof(buffer);
@@ -125,7 +125,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_cwd(obj_arg /* w */) {
}
// Std.Internal.UV.System.chdir : String → IO Unit
extern "C" LEAN_EXPORT lean_obj_res lean_uv_chdir(b_obj_arg path, obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_chdir(b_obj_arg path) {
const char* path_str = lean_string_cstr(path);
if (strlen(path_str) != lean_string_size(path) - 1) {
return mk_embedded_nul_error(path);
@@ -142,7 +142,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_chdir(b_obj_arg path, obj_arg /* w *
}
// Std.Internal.UV.System.osHomedir : IO String
extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_homedir(obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_homedir() {
char buffer[PATH_MAX];
size_t size = sizeof(buffer);
@@ -157,7 +157,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_homedir(obj_arg /* w */) {
}
// Std.Internal.UV.System.osTmpdir : IO String
extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_tmpdir(obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_tmpdir() {
char buffer[PATH_MAX];
size_t size = sizeof(buffer);
@@ -172,7 +172,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_tmpdir(obj_arg /* w */) {
}
// Std.Internal.UV.System.osGetPasswd : IO PasswdInfo
extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_get_passwd(obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_get_passwd() {
uv_passwd_t passwd;
int result = uv_os_get_passwd(&passwd);
@@ -200,7 +200,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_get_passwd(obj_arg /* w */) {
}
// Std.Internal.UV.System.osGetGroup : IO (Option GroupInfo)
extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_get_group(uint64_t gid, obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_get_group(uint64_t gid) {
#if UV_VERSION_HEX >= 0x012D00
uv_group_t group;
int result = uv_os_get_group(&group, gid);
@@ -244,7 +244,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_get_group(uint64_t gid, obj_arg /
}
// Std.Internal.UV.System.osEnviron : IO (Array (String × String))
extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_environ(obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_environ() {
uv_env_item_t* env;
int count;
int result = uv_os_environ(&env, &count);
@@ -272,7 +272,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_environ(obj_arg /* w */) {
}
// Std.Internal.UV.System.osGetenv : String → IO (Option String)
extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_getenv(b_obj_arg name, obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_getenv(b_obj_arg name) {
const char* name_str = lean_string_cstr(name);
if (strlen(name_str) != lean_string_size(name) - 1) {
return lean_io_result_mk_ok(lean_box(0));
@@ -314,7 +314,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_getenv(b_obj_arg name, obj_arg /*
// Std.Internal.UV.System.osSetenv : String → String → IO Unit
extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_setenv(b_obj_arg name, b_obj_arg value, obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_setenv(b_obj_arg name, b_obj_arg value) {
const char* name_str = lean_string_cstr(name);
const char* value_str = lean_string_cstr(value);
if (strlen(name_str) != lean_string_size(name) - 1) {
@@ -334,7 +334,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_setenv(b_obj_arg name, b_obj_arg
}
// Std.Internal.UV.System.osUnsetenv : String → IO Unit
extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_unsetenv(b_obj_arg name, obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_unsetenv(b_obj_arg name) {
const char* name_str = lean_string_cstr(name);
if (strlen(name_str) != lean_string_size(name) - 1) {
return mk_embedded_nul_error(name);
@@ -350,7 +350,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_unsetenv(b_obj_arg name, obj_arg
}
// Std.Internal.UV.System.osGetHostname : IO String
extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_gethostname(obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_gethostname() {
char hostname[256];
size_t size = sizeof(hostname);
@@ -365,7 +365,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_gethostname(obj_arg /* w */) {
}
// Std.Internal.UV.System.osGetPriority : UInt64 → IO Int64
extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_getpriority(uint64_t pid, obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_getpriority(uint64_t pid) {
int priority;
int result = uv_os_getpriority(pid, &priority);
@@ -378,7 +378,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_getpriority(uint64_t pid, obj_arg
}
// Std.Internal.UV.System.osSetPriority : UInt64 → Int → IO Unit
extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_setpriority(uint64_t pid, int64_t priority, obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_setpriority(uint64_t pid, int64_t priority) {
int result = uv_os_setpriority(pid, priority);
if (result < 0) {
@@ -389,7 +389,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_setpriority(uint64_t pid, int64_t
}
// Std.Internal.UV.System.osUname : IO UnameInfo
extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_uname(obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_uname() {
uv_utsname_t uname_info;
int result = uv_os_uname(&uname_info);
@@ -413,13 +413,13 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_uname(obj_arg /* w */) {
}
// Std.Internal.UV.System.hrtime : IO UInt64
extern "C" LEAN_EXPORT lean_obj_res lean_uv_hrtime(obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_hrtime() {
uint64_t time = uv_hrtime();
return lean_io_result_mk_ok(lean_box_uint64(time));
}
// Std.Internal.UV.System.random : UInt64 → IO (IO.Promise (Except IO.Error (Array UInt8)))
extern "C" LEAN_EXPORT lean_obj_res lean_uv_random(uint64_t size, obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_random(uint64_t size) {
lean_object* promise = lean_promise_new();
mark_mt(promise);
@@ -476,7 +476,7 @@ static inline uint64_t timeval_to_millis(uv_timeval_t t) {
}
// Std.Internal.UV.System.getrusage : IO RUsage
extern "C" LEAN_EXPORT lean_obj_res lean_uv_getrusage(obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_getrusage() {
uv_rusage_t usage;
int result = uv_getrusage(&usage);
if (result < 0) {
@@ -505,7 +505,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_getrusage(obj_arg /* w */) {
}
// Std.Internal.UV.System.exePath : IO String
extern "C" LEAN_EXPORT lean_obj_res lean_uv_exepath(obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_exepath() {
char buffer[PATH_MAX];
size_t size = sizeof(buffer);
@@ -519,25 +519,25 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_exepath(obj_arg /* w */) {
}
// Std.Internal.UV.System.freeMemory : IO UInt64
extern "C" LEAN_EXPORT lean_obj_res lean_uv_get_free_memory(obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_get_free_memory() {
uint64_t mem = uv_get_free_memory();
return lean_io_result_mk_ok(lean_box_uint64(mem));
}
// Std.Internal.UV.System.totalMemory : IO UInt64
extern "C" LEAN_EXPORT lean_obj_res lean_uv_get_total_memory(obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_get_total_memory() {
uint64_t mem = uv_get_total_memory();
return lean_io_result_mk_ok(lean_box_uint64(mem));
}
// Std.Internal.UV.System.constrainedMemory : IO UInt64
extern "C" LEAN_EXPORT lean_obj_res lean_uv_get_constrained_memory(obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_get_constrained_memory() {
uint64_t mem = uv_get_constrained_memory();
return lean_io_result_mk_ok(lean_box_uint64(mem));
}
// Std.Internal.UV.System.availableMemory : IO UInt64
extern "C" LEAN_EXPORT lean_obj_res lean_uv_get_available_memory(obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_get_available_memory() {
#if UV_VERSION_HEX >= 0x012D00
uint64_t mem = uv_get_available_memory();
return lean_io_result_mk_ok(lean_box_uint64(mem));
@@ -551,191 +551,191 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_get_available_memory(obj_arg /* w */
#else
// Std.Internal.UV.System.getProcessTitle : IO String
extern "C" LEAN_EXPORT lean_obj_res lean_uv_get_process_title(obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_get_process_title() {
lean_always_assert(
false && ("Please build a version of Lean4 with libuv to invoke this.")
);
}
// Std.Internal.UV.System.setProcessTitle : @& String → IO Unit
extern "C" LEAN_EXPORT lean_obj_res lean_uv_set_process_title(b_obj_arg title, obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_set_process_title(b_obj_arg title) {
lean_always_assert(
false && ("Please build a version of Lean4 with libuv to invoke this.")
);
}
// Std.Internal.UV.System.uptime : IO UInt64
extern "C" LEAN_EXPORT lean_obj_res lean_uv_uptime(obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_uptime() {
lean_always_assert(
false && ("Please build a version of Lean4 with libuv to invoke this.")
);
}
// Std.Internal.UV.System.osGetPid : IO UInt64
extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_getpid(obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_getpid() {
lean_always_assert(
false && ("Please build a version of Lean4 with libuv to invoke this.")
);
}
// Std.Internal.UV.System.osGetPpid : IO UInt64
extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_getppid(obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_getppid() {
lean_always_assert(
false && ("Please build a version of Lean4 with libuv to invoke this.")
);
}
// Std.Internal.UV.System.cpuInfo : IO (Array CPUInfo)
extern "C" LEAN_EXPORT lean_obj_res lean_uv_cpu_info(obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_cpu_info() {
lean_always_assert(
false && ("Please build a version of Lean4 with libuv to invoke this.")
);
}
// Std.Internal.UV.System.cwd : IO String
extern "C" LEAN_EXPORT lean_obj_res lean_uv_cwd(obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_cwd() {
lean_always_assert(
false && ("Please build a version of Lean4 with libuv to invoke this.")
);
}
// Std.Internal.UV.System.chdir : String → IO Unit
extern "C" LEAN_EXPORT lean_obj_res lean_uv_chdir(b_obj_arg path, obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_chdir(b_obj_arg path) {
lean_always_assert(
false && ("Please build a version of Lean4 with libuv to invoke this.")
);
}
// Std.Internal.UV.System.osHomedir : IO String
extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_homedir(obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_homedir() {
lean_always_assert(
false && ("Please build a version of Lean4 with libuv to invoke this.")
);
}
// Std.Internal.UV.System.osTmpdir : IO String
extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_tmpdir(obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_tmpdir() {
lean_always_assert(
false && ("Please build a version of Lean4 with libuv to invoke this.")
);
}
// Std.Internal.UV.System.osGetPasswd : IO PasswdInfo
extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_get_passwd(obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_get_passwd() {
lean_always_assert(
false && ("Please build a version of Lean4 with libuv to invoke this.")
);
}
// Std.Internal.UV.System.osGetGroup : IO (Option GroupInfo)
extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_get_group(obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_get_group() {
lean_always_assert(
false && ("Please build a version of Lean4 with libuv to invoke this.")
);
}
// Std.Internal.UV.System.osEnviron : IO (Array (String × String))
extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_environ(obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_environ() {
lean_always_assert(
false && ("Please build a version of Lean4 with libuv to invoke this.")
);
}
// Std.Internal.UV.System.osGetenv : String → IO (Option String)
extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_getenv(b_obj_arg name, obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_getenv(b_obj_arg name) {
lean_always_assert(
false && ("Please build a version of Lean4 with libuv to invoke this.")
);
}
// Std.Internal.UV.System.osSetenv : String → String → IO Unit
extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_setenv(b_obj_arg name, b_obj_arg value, obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_setenv(b_obj_arg name, b_obj_arg value) {
lean_always_assert(
false && ("Please build a version of Lean4 with libuv to invoke this.")
);
}
// Std.Internal.UV.System.osUnsetenv : String → IO Unit
extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_unsetenv(b_obj_arg name, obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_unsetenv(b_obj_arg name) {
lean_always_assert(
false && ("Please build a version of Lean4 with libuv to invoke this.")
);
}
// Std.Internal.UV.System.osGetHostname : IO String
extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_gethostname(obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_gethostname() {
lean_always_assert(
false && ("Please build a version of Lean4 with libuv to invoke this.")
);
}
// Std.Internal.UV.System.osGetPriority : UInt64 → IO Int
extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_getpriority(uint64_t pid, obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_getpriority(uint64_t pid) {
lean_always_assert(
false && ("Please build a version of Lean4 with libuv to invoke this.")
);
}
// Std.Internal.UV.System.osSetPriority : UInt64 → Int → IO Unit
extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_setpriority(uint64_t pid, int64_t priority, obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_setpriority(uint64_t pid, int64_t priority) {
lean_always_assert(
false && ("Please build a version of Lean4 with libuv to invoke this.")
);
}
// Std.Internal.UV.System.osUname : IO UnameInfo
extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_uname(obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_uname() {
lean_always_assert(
false && ("Please build a version of Lean4 with libuv to invoke this.")
);
}
// Std.Internal.UV.System.hrtime : IO UInt64
extern "C" LEAN_EXPORT lean_obj_res lean_uv_hrtime(obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_hrtime() {
lean_always_assert(
false && ("Please build a version of Lean4 with libuv to invoke this.")
);
}
// Std.Internal.UV.System.random : UInt64 → IO (IO.Promise (Except IO.Error (Array UInt8)))
extern "C" LEAN_EXPORT lean_obj_res lean_uv_random(uint64_t size, obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_random(uint64_t size) {
lean_always_assert(
false && ("Please build a version of Lean4 with libuv to invoke this.")
);
}
// Std.Internal.UV.System.getrusage : IO RUsage
extern "C" LEAN_EXPORT lean_obj_res lean_uv_getrusage(obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_getrusage() {
lean_always_assert(
false && ("Please build a version of Lean4 with libuv to invoke this.")
);
}
// Std.Internal.UV.System.exePath : IO String
extern "C" LEAN_EXPORT lean_obj_res lean_uv_exepath(obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_exepath() {
lean_always_assert(
false && ("Please build a version of Lean4 with libuv to invoke this.")
);
}
// Std.Internal.UV.System.freeMemory : IO UInt64
extern "C" LEAN_EXPORT lean_obj_res lean_uv_get_free_memory(obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_get_free_memory() {
lean_always_assert(
false && ("Please build a version of Lean4 with libuv to invoke this.")
);
}
// Std.Internal.UV.System.totalMemory : IO UInt64
extern "C" LEAN_EXPORT lean_obj_res lean_uv_get_total_memory(obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_get_total_memory() {
lean_always_assert(
false && ("Please build a version of Lean4 with libuv to invoke this.")
);
}
// Std.Internal.UV.System.constrainedMemory : IO UInt64
extern "C" LEAN_EXPORT lean_obj_res lean_uv_get_constrained_memory(obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_get_constrained_memory() {
lean_always_assert(
false && ("Please build a version of Lean4 with libuv to invoke this.")
);
}
// Std.Internal.UV.System.availableMemory : IO UInt64
extern "C" LEAN_EXPORT lean_obj_res lean_uv_get_available_memory(obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_get_available_memory() {
lean_always_assert(
false && ("Please build a version of Lean4 with libuv to invoke this.")
);

56
src/runtime/uv/system.h
View File

@@ -12,33 +12,33 @@ using namespace std;
// =======================================
// System information functions
extern "C" LEAN_EXPORT lean_obj_res lean_uv_get_process_title(obj_arg /* w */);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_set_process_title(b_obj_arg title, obj_arg /* w */);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_uptime(obj_arg /* w */);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_getpid(obj_arg /* w */);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_getppid(obj_arg /* w */);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_cpu_info(obj_arg /* w */);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_cwd(obj_arg /* w */);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_chdir(b_obj_arg path, obj_arg /* w */);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_homedir(obj_arg /* w */);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_tmpdir(obj_arg /* w */);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_get_passwd(obj_arg /* w */);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_get_group(uint64_t gid, obj_arg /* w */);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_environ(obj_arg /* w */);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_getenv(b_obj_arg name, obj_arg /* w */);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_setenv(b_obj_arg name, b_obj_arg value, obj_arg /* w */);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_unsetenv(b_obj_arg name, obj_arg /* w */);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_gethostname(obj_arg /* w */);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_getpriority(uint64_t pid, obj_arg /* w */);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_setpriority(uint64_t pid, int64_t priority, obj_arg /* w */);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_uname(obj_arg /* w */);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_hrtime(obj_arg /* w */);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_random(uint64_t size, obj_arg /* w */);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_getrusage(obj_arg /* w */);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_exepath(obj_arg /* w */);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_get_free_memory(obj_arg /* w */);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_get_total_memory(obj_arg /* w */);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_get_constrained_memory(obj_arg /* w */);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_get_available_memory(obj_arg /* w */);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_get_process_title();
extern "C" LEAN_EXPORT lean_obj_res lean_uv_set_process_title(b_obj_arg title);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_uptime();
extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_getpid();
extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_getppid();
extern "C" LEAN_EXPORT lean_obj_res lean_uv_cpu_info();
extern "C" LEAN_EXPORT lean_obj_res lean_uv_cwd();
extern "C" LEAN_EXPORT lean_obj_res lean_uv_chdir(b_obj_arg path);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_homedir();
extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_tmpdir();
extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_get_passwd();
extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_get_group(uint64_t gid);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_environ();
extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_getenv(b_obj_arg name);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_setenv(b_obj_arg name, b_obj_arg value);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_unsetenv(b_obj_arg name);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_gethostname();
extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_getpriority(uint64_t pid);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_setpriority(uint64_t pid, int64_t priority);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_os_uname();
extern "C" LEAN_EXPORT lean_obj_res lean_uv_hrtime();
extern "C" LEAN_EXPORT lean_obj_res lean_uv_random(uint64_t size);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_getrusage();
extern "C" LEAN_EXPORT lean_obj_res lean_uv_exepath();
extern "C" LEAN_EXPORT lean_obj_res lean_uv_get_free_memory();
extern "C" LEAN_EXPORT lean_obj_res lean_uv_get_total_memory();
extern "C" LEAN_EXPORT lean_obj_res lean_uv_get_constrained_memory();
extern "C" LEAN_EXPORT lean_obj_res lean_uv_get_available_memory();
}

64
src/runtime/uv/tcp.cpp
View File

@@ -81,7 +81,7 @@ void initialize_libuv_tcp_socket() {
// TCP Socket Operations
/* Std.Internal.UV.TCP.Socket.new : IO Socket */
extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_new(obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_new() {
lean_uv_tcp_socket_object* tcp_socket = (lean_uv_tcp_socket_object*)malloc(sizeof(lean_uv_tcp_socket_object));
tcp_socket->m_promise_accept = nullptr;
@@ -114,7 +114,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_new(obj_arg /* w */) {
}
/* Std.Internal.UV.TCP.Socket.connect (socket : @& Socket) (addr : @& SocketAddress) : IO (IO.Promise (Except IO.Error Unit)) */
extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_connect(b_obj_arg socket, b_obj_arg addr, obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_connect(b_obj_arg socket, b_obj_arg addr) {
lean_uv_tcp_socket_object* tcp_socket = lean_to_uv_tcp_socket(socket);
lean_object* promise = lean_promise_new();
@@ -166,7 +166,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_connect(b_obj_arg socket, b_obj_
}
/* Std.Internal.UV.TCP.Socket.send (socket : @& Socket) (data : Array ByteArray) : IO (IO.Promise (Except IO.Error Unit)) */
extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_send(b_obj_arg socket, obj_arg data_array, obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_send(b_obj_arg socket, obj_arg data_array) {
lean_uv_tcp_socket_object* tcp_socket = lean_to_uv_tcp_socket(socket);
size_t array_len = lean_array_size(data_array);
@@ -242,7 +242,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_send(b_obj_arg socket, obj_arg d
}
/* Std.Internal.UV.TCP.Socket.recv? (socket : @& Socket) (size : UInt64) : IO (IO.Promise (Except IO.Error (Option ByteArray))) */
extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_recv(b_obj_arg socket, uint64_t buffer_size, obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_recv(b_obj_arg socket, uint64_t buffer_size) {
lean_uv_tcp_socket_object* tcp_socket = lean_to_uv_tcp_socket(socket);
// Locking early prevents potential parallelism issues setting the byte_array.
@@ -317,7 +317,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_recv(b_obj_arg socket, uint64_t
}
/* Std.Internal.UV.TCP.Socket.waitReadable (socket : @& Socket) : IO (IO.Promise (Except IO.Error Bool)) */
extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_wait_readable(b_obj_arg socket, obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_wait_readable(b_obj_arg socket) {
lean_uv_tcp_socket_object* tcp_socket = lean_to_uv_tcp_socket(socket);
event_loop_lock(&global_ev);
@@ -384,7 +384,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_wait_readable(b_obj_arg socket,
}
/* Std.Internal.UV.TCP.Socket.cancelRecv (socket : @& Socket) : IO Unit */
extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_cancel_recv(b_obj_arg socket, obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_cancel_recv(b_obj_arg socket) {
lean_uv_tcp_socket_object* tcp_socket = lean_to_uv_tcp_socket(socket);
event_loop_lock(&global_ev);
@@ -413,7 +413,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_cancel_recv(b_obj_arg socket, ob
}
/* Std.Internal.UV.TCP.Socket.bind (socket : @& Socket) (addr : @& SocketAddress) : IO Unit */
extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_bind(b_obj_arg socket, b_obj_arg addr, obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_bind(b_obj_arg socket, b_obj_arg addr) {
lean_uv_tcp_socket_object* tcp_socket = lean_to_uv_tcp_socket(socket);
sockaddr_storage addr_ptr;
@@ -431,7 +431,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_bind(b_obj_arg socket, b_obj_arg
}
/* Std.Internal.UV.TCP.Socket.listen (socket : @& Socket) (backlog : Int32) : IO Unit */
extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_listen(b_obj_arg socket, int32_t backlog, obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_listen(b_obj_arg socket, int32_t backlog) {
lean_uv_tcp_socket_object* tcp_socket = lean_to_uv_tcp_socket(socket);
event_loop_lock(&global_ev);
@@ -484,7 +484,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_listen(b_obj_arg socket, int32_t
}
/* Std.Internal.UV.TCP.Socket.accept (socket : @& Socket) : IO (IO.Promise (Except IO.Error Socket)) */
extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_accept(b_obj_arg socket, obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_accept(b_obj_arg socket) {
lean_uv_tcp_socket_object* tcp_socket = lean_to_uv_tcp_socket(socket);
// Locking early prevents potential parallelism issues setting m_promise_accept.
@@ -497,7 +497,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_accept(b_obj_arg socket, obj_arg
lean_object* promise = lean_promise_new();
mark_mt(promise);
lean_object* client = lean_io_result_take_value(lean_uv_tcp_new(lean_box(0)));
lean_object* client = lean_io_result_take_value(lean_uv_tcp_new());
lean_uv_tcp_socket_object* client_socket = lean_to_uv_tcp_socket(client);
@@ -525,7 +525,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_accept(b_obj_arg socket, obj_arg
}
/* Std.Internal.UV.TCP.Socket.tryAccept (socket : @& Socket) : IO (Except IO.Error (Option Socket)) */
extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_try_accept(b_obj_arg socket, obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_try_accept(b_obj_arg socket) {
lean_uv_tcp_socket_object* tcp_socket = lean_to_uv_tcp_socket(socket);
// Locking early prevents potential parallelism issues setting m_promise_accept.
@@ -535,7 +535,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_try_accept(b_obj_arg socket, obj
return lean_io_result_mk_error(lean_decode_uv_error(UV_EALREADY, mk_string("parallel accept is not allowed! consider binding multiple sockets to the same address and accepting on them instead")));
}
lean_object* client = lean_io_result_take_value(lean_uv_tcp_new(lean_box(0)));
lean_object* client = lean_io_result_take_value(lean_uv_tcp_new());
lean_uv_tcp_socket_object* client_socket = lean_to_uv_tcp_socket(client);
int result = uv_accept((uv_stream_t*)tcp_socket->m_uv_tcp, (uv_stream_t*)client_socket->m_uv_tcp);
@@ -557,7 +557,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_try_accept(b_obj_arg socket, obj
/* Std.Internal.UV.TCP.Socket.cancelAccept (socket : @& Socket) : IO Unit */
extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_cancel_accept(b_obj_arg socket, obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_cancel_accept(b_obj_arg socket) {
lean_uv_tcp_socket_object* tcp_socket = lean_to_uv_tcp_socket(socket);
event_loop_lock(&global_ev);
@@ -585,7 +585,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_cancel_accept(b_obj_arg socket,
}
/* Std.Internal.UV.TCP.Socket.shutdown (socket : @& Socket) : IO (IO.Promise (Except IO.Error Unit)) */
extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_shutdown(b_obj_arg socket, obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_shutdown(b_obj_arg socket) {
lean_uv_tcp_socket_object* tcp_socket = lean_to_uv_tcp_socket(socket);
// Locking early prevents potential parallelism issues setting the m_promise_shutdown.
@@ -641,7 +641,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_shutdown(b_obj_arg socket, obj_a
}
/* Std.Internal.UV.TCP.Socket.getPeerName (socket : @& Socket) : IO SocketAddress */
extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_getpeername(b_obj_arg socket, obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_getpeername(b_obj_arg socket) {
lean_uv_tcp_socket_object* tcp_socket = lean_to_uv_tcp_socket(socket);
sockaddr_storage addr_storage;
@@ -661,7 +661,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_getpeername(b_obj_arg socket, ob
}
/* Std.Internal.UV.TCP.Socket.getSockName (socket : @& Socket) : IO SocketAddress */
extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_getsockname(b_obj_arg socket, obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_getsockname(b_obj_arg socket) {
lean_uv_tcp_socket_object* tcp_socket = lean_to_uv_tcp_socket(socket);
struct sockaddr_storage addr_storage;
@@ -680,7 +680,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_getsockname(b_obj_arg socket, ob
}
/* Std.Internal.UV.TCP.Socket.noDelay (socket : @& Socket) : IO Unit */
extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_nodelay(b_obj_arg socket, obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_nodelay(b_obj_arg socket) {
lean_uv_tcp_socket_object* tcp_socket = lean_to_uv_tcp_socket(socket);
event_loop_lock(&global_ev);
@@ -695,7 +695,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_nodelay(b_obj_arg socket, obj_ar
}
/* Std.Internal.UV.TCP.Socket.keepAlive (socket : @& Socket) (enable : Int8) (delay : UInt32) : IO Unit */
extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_keepalive(b_obj_arg socket, int32_t enable, uint32_t delay, obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_keepalive(b_obj_arg socket, int32_t enable, uint32_t delay) {
lean_uv_tcp_socket_object* tcp_socket = lean_to_uv_tcp_socket(socket);
event_loop_lock(&global_ev);
@@ -713,55 +713,55 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_keepalive(b_obj_arg socket, int3
// =======================================
// TCP Socket Operations
extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_new(obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_new() {
lean_always_assert(
false && ("Please build a version of Lean4 with libuv to invoke this.")
);
}
extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_connect(b_obj_arg socket, b_obj_arg addr, obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_connect(b_obj_arg socket, b_obj_arg addr) {
lean_always_assert(
false && ("Please build a version of Lean4 with libuv to invoke this.")
);
}
extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_send(b_obj_arg socket, obj_arg data, obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_send(b_obj_arg socket, obj_arg data) {
lean_always_assert(
false && ("Please build a version of Lean4 with libuv to invoke this.")
);
}
extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_recv(b_obj_arg socket, uint64_t buffer_size, obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_recv(b_obj_arg socket, uint64_t buffer_size) {
lean_always_assert(
false && ("Please build a version of Lean4 with libuv to invoke this.")
);
}
extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_bind(b_obj_arg socket, b_obj_arg addr, obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_bind(b_obj_arg socket, b_obj_arg addr) {
lean_always_assert(
false && ("Please build a version of Lean4 with libuv to invoke this.")
);
}
extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_listen(b_obj_arg socket, int32_t backlog, obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_listen(b_obj_arg socket, int32_t backlog) {
lean_always_assert(
false && ("Please build a version of Lean4 with libuv to invoke this.")
);
}
extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_cancel_accept(b_obj_arg socket, obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_cancel_accept(b_obj_arg socket) {
lean_always_assert(
false && ("Please build a version of Lean4 with libuv to invoke this.")
);
}
extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_accept(b_obj_arg socket, obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_accept(b_obj_arg socket) {
lean_always_assert(
false && ("Please build a version of Lean4 with libuv to invoke this.")
);
}
extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_shutdown(b_obj_arg socket, obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_shutdown(b_obj_arg socket) {
lean_always_assert(
false && ("Please build a version of Lean4 with libuv to invoke this.")
);
@@ -771,29 +771,29 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_shutdown(b_obj_arg socket, obj_a
// =======================================
// TCP Socket Utility Functions
extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_getpeername(b_obj_arg socket, obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_getpeername(b_obj_arg socket) {
lean_always_assert(
false && ("Please build a version of Lean4 with libuv to invoke this.")
);
}
extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_getsockname(b_obj_arg socket, obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_getsockname(b_obj_arg socket) {
lean_always_assert(
false && ("Please build a version of Lean4 with libuv to invoke this.")
);
}
extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_nodelay(b_obj_arg socket, obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_nodelay(b_obj_arg socket) {
lean_always_assert(
false && ("Please build a version of Lean4 with libuv to invoke this.")
);
}
extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_keepalive(b_obj_arg socket, int32_t enable, uint32_t delay, obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_keepalive(b_obj_arg socket, int32_t enable, uint32_t delay) {
lean_always_assert(
false && ("Please build a version of Lean4 with libuv to invoke this.")
);
}
#endif
}
}

33
src/runtime/uv/tcp.h
View File

@@ -40,26 +40,25 @@ static inline lean_uv_tcp_socket_object* lean_to_uv_tcp_socket(lean_object* o) {
// =======================================
// TCP Socket Operations
extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_new(obj_arg /* w */);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_connect(b_obj_arg socket, b_obj_arg addr, obj_arg /* w */);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_send(b_obj_arg socket, obj_arg data_array, obj_arg /* w */);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_recv(b_obj_arg socket, uint64_t buffer_size, obj_arg /* w */);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_wait_readable(b_obj_arg socket, obj_arg /* w */);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_cancel_recv(b_obj_arg socket, obj_arg /* w */);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_bind(b_obj_arg socket, b_obj_arg addr, obj_arg /* w */);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_listen(b_obj_arg socket, int32_t backlog, obj_arg /* w */);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_accept(b_obj_arg socket, obj_arg /* w */);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_cancel_accept(b_obj_arg socket, obj_arg /* w */);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_try_accept(b_obj_arg socket, obj_arg /* w */);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_shutdown(b_obj_arg socket, obj_arg /* w */);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_try_accept(b_obj_arg socket, obj_arg /* w */);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_new();
extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_connect(b_obj_arg socket, b_obj_arg addr);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_send(b_obj_arg socket, obj_arg data_array);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_recv(b_obj_arg socket, uint64_t buffer_size);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_wait_readable(b_obj_arg socket);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_cancel_recv(b_obj_arg socket);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_bind(b_obj_arg socket, b_obj_arg addr);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_listen(b_obj_arg socket, int32_t backlog);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_accept(b_obj_arg socket);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_cancel_accept(b_obj_arg socket);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_try_accept(b_obj_arg socket);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_shutdown(b_obj_arg socket);
// =======================================
// TCP Socket Utility Functions
extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_getpeername(b_obj_arg socket, obj_arg /* w */);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_getsockname(b_obj_arg socket, obj_arg /* w */);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_nodelay(b_obj_arg socket, obj_arg /* w */);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_keepalive(b_obj_arg socket, int32_t enable, uint32_t delay, obj_arg /* w */);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_getpeername(b_obj_arg socket);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_getsockname(b_obj_arg socket);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_nodelay(b_obj_arg socket);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_tcp_keepalive(b_obj_arg socket, int32_t enable, uint32_t delay);
}

31
src/runtime/uv/timer.cpp
View File

@@ -55,14 +55,14 @@ void handle_timer_event(uv_timer_t* handle) {
if (timer->m_repeating) {
// For repeating timers, only resolves if the promise exists and is not finished
if (timer->m_promise != NULL && !timer_promise_is_finished(timer)) {
lean_object* res = lean_io_promise_resolve(lean_box(0), timer->m_promise, lean_io_mk_world());
lean_object* res = lean_io_promise_resolve(lean_box(0), timer->m_promise);
lean_dec(res);
}
} else {
// For non-repeating timers, resolves if the promise exists
if (timer->m_promise != NULL) {
lean_assert(!timer_promise_is_finished(timer));
lean_object* res = lean_io_promise_resolve(lean_box(0), timer->m_promise, lean_io_mk_world());
lean_object* res = lean_io_promise_resolve(lean_box(0), timer->m_promise);
lean_dec(res);
}
@@ -75,7 +75,7 @@ void handle_timer_event(uv_timer_t* handle) {
}
/* Std.Internal.UV.Timer.mk (timeout : UInt64) (repeating : Bool) : IO Timer */
extern "C" LEAN_EXPORT lean_obj_res lean_uv_timer_mk(uint64_t timeout, uint8_t repeating, obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_timer_mk(uint64_t timeout, uint8_t repeating) {
lean_uv_timer_object * timer = (lean_uv_timer_object*)malloc(sizeof(lean_uv_timer_object));
timer->m_timeout = timeout;
timer->m_repeating = repeating;
@@ -104,16 +104,11 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_timer_mk(uint64_t timeout, uint8_t r
}
/* Std.Internal.UV.Timer.next (timer : @& Timer) : IO (IO.Promise Unit) */
extern "C" LEAN_EXPORT lean_obj_res lean_uv_timer_next(b_obj_arg obj, obj_arg /* w */ ) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_timer_next(b_obj_arg obj) {
lean_uv_timer_object * timer = lean_to_uv_timer(obj);
auto create_promise = []() {
lean_object * prom_res = lean_io_promise_new(lean_io_mk_world());
lean_object * promise = lean_ctor_get(prom_res, 0);
lean_inc(promise);
lean_dec(prom_res);
return promise;
return lean_io_promise_new();
};
auto setup_timer = [create_promise, obj, timer]() {
@@ -199,7 +194,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_timer_next(b_obj_arg obj, obj_arg /*
}
/* Std.Internal.UV.Timer.reset (timer : @& Timer) : IO Unit */
extern "C" LEAN_EXPORT lean_obj_res lean_uv_timer_reset(b_obj_arg obj, obj_arg /* w */ ) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_timer_reset(b_obj_arg obj) {
lean_uv_timer_object * timer = lean_to_uv_timer(obj);
// Locking to access the state in order to avoid data-race
@@ -230,7 +225,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_timer_reset(b_obj_arg obj, obj_arg /
}
/* Std.Internal.UV.Timer.stop (timer : @& Timer) : IO Unit */
extern "C" LEAN_EXPORT lean_obj_res lean_uv_timer_stop(b_obj_arg obj, obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_timer_stop(b_obj_arg obj) {
lean_uv_timer_object * timer = lean_to_uv_timer(obj);
// Locking to access the state in order to avoid data-race
@@ -258,7 +253,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_timer_stop(b_obj_arg obj, obj_arg /*
}
/* Std.Internal.UV.Timer.cancel (timer : @& Timer) : IO Unit */
extern "C" LEAN_EXPORT lean_obj_res lean_uv_timer_cancel(b_obj_arg obj, obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_timer_cancel(b_obj_arg obj) {
lean_uv_timer_object * timer = lean_to_uv_timer(obj);
// It's locking here to avoid changing the state during other operations.
@@ -289,31 +284,31 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_timer_cancel(b_obj_arg obj, obj_arg
void lean_uv_timer_finalizer(void* ptr);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_timer_mk(uint64_t timeout, uint8_t repeating, obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_timer_mk(uint64_t timeout, uint8_t repeating) {
lean_always_assert(
false && ("Please build a version of Lean4 with libuv to invoke this.")
);
}
extern "C" LEAN_EXPORT lean_obj_res lean_uv_timer_next(b_obj_arg timer, obj_arg /* w */ ) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_timer_next(b_obj_arg timer) {
lean_always_assert(
false && ("Please build a version of Lean4 with libuv to invoke this.")
);
}
extern "C" LEAN_EXPORT lean_obj_res lean_uv_timer_reset(b_obj_arg timer, obj_arg /* w */ ) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_timer_reset(b_obj_arg timer) {
lean_always_assert(
false && ("Please build a version of Lean4 with libuv to invoke this.")
);
}
extern "C" LEAN_EXPORT lean_obj_res lean_uv_timer_stop(b_obj_arg timer, obj_arg /* w */ ) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_timer_stop(b_obj_arg timer) {
lean_always_assert(
false && ("Please build a version of Lean4 with libuv to invoke this.")
);
}
extern "C" LEAN_EXPORT lean_obj_res lean_uv_timer_cancel(b_obj_arg obj, obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_timer_cancel(b_obj_arg obj) {
lean_always_assert(
false && ("Please build a version of Lean4 with libuv to invoke this.")
);

10
src/runtime/uv/timer.h
View File

@@ -47,11 +47,11 @@ static inline lean_uv_timer_object* lean_to_uv_timer(lean_object * o) { return (
// =======================================
// Timer manipulation functions
extern "C" LEAN_EXPORT lean_obj_res lean_uv_timer_mk(uint64_t timeout, uint8_t repeating, obj_arg /* w */);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_timer_next(b_obj_arg timer, obj_arg /* w */);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_timer_reset(b_obj_arg timer, obj_arg /* w */);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_timer_stop(b_obj_arg timer, obj_arg /* w */);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_timer_cancel(b_obj_arg timer, obj_arg /* w */);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_timer_mk(uint64_t timeout, uint8_t repeating);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_timer_next(b_obj_arg timer);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_timer_reset(b_obj_arg timer);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_timer_stop(b_obj_arg timer);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_timer_cancel(b_obj_arg timer);
#endif

54
src/runtime/uv/udp.cpp
View File

@@ -60,7 +60,7 @@ void initialize_libuv_udp_socket() {
// UDP Socket Operations
/* Std.Internal.UV.UDP.Socket.new : IO Socket */
extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_new(obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_new() {
lean_uv_udp_socket_object* udp_socket = (lean_uv_udp_socket_object*)malloc(sizeof(lean_uv_udp_socket_object));
udp_socket->m_promise_read = nullptr;
@@ -89,7 +89,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_new(obj_arg /* w */) {
}
/* Std.Internal.UV.UDP.Socket.bind (socket : @& Socket) (addr : @& SocketAddress) : IO Unit */
extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_bind(b_obj_arg socket, b_obj_arg addr, obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_bind(b_obj_arg socket, b_obj_arg addr) {
lean_uv_udp_socket_object* udp_socket = lean_to_uv_udp_socket(socket);
sockaddr_storage addr_ptr;
@@ -107,7 +107,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_bind(b_obj_arg socket, b_obj_arg
}
/* Std.Internal.UV.UDP.Socket.connect (socket : @& Socket) (addr : @& SocketAddress) : IO Unit */
extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_connect(b_obj_arg socket, b_obj_arg addr, obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_connect(b_obj_arg socket, b_obj_arg addr) {
lean_uv_udp_socket_object* udp_socket = lean_to_uv_udp_socket(socket);
sockaddr_storage addr_ptr;
@@ -125,7 +125,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_connect(b_obj_arg socket, b_obj_
}
/* Std.Internal.UV.UDP.Socket.send (socket : @& Socket) (data : Array ByteArray) (addr : @& Option SocketAddress) : IO (IO.Promise (Except IO.Error Unit)) */
extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_send(b_obj_arg socket, obj_arg data_array, b_obj_arg opt_addr, obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_send(b_obj_arg socket, obj_arg data_array, b_obj_arg opt_addr) {
lean_uv_udp_socket_object* udp_socket = lean_to_uv_udp_socket(socket);
size_t array_len = lean_array_size(data_array);
@@ -211,7 +211,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_send(b_obj_arg socket, obj_arg d
}
/* Std.Internal.UV.UDP.Socket.recv (socket : @& Socket) (size : UInt64) : IO (IO.Promise (Except IO.Error (ByteArray × SocketAddress))) */
extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_recv(b_obj_arg socket, uint64_t buffer_size, obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_recv(b_obj_arg socket, uint64_t buffer_size) {
lean_uv_udp_socket_object *udp_socket = lean_to_uv_udp_socket(socket);
// Locking earlier to avoid parallelism issues with m_promise_read.
@@ -295,7 +295,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_recv(b_obj_arg socket, uint64_t
}
/* Std.Internal.UV.UDP.Socket.waitReadable (socket : @& Socket) : IO (IO.Promise (Except IO.Error Unit)) */
extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_wait_readable(b_obj_arg socket, obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_wait_readable(b_obj_arg socket) {
lean_uv_udp_socket_object* udp_socket = lean_to_uv_udp_socket(socket);
// Locking earlier to avoid parallelism issues with m_promise_read.
@@ -361,7 +361,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_wait_readable(b_obj_arg socket,
}
/* Std.Internal.UV.UDP.Socket.cancelRecv (socket : @& Socket) : IO Unit */
extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_cancel_recv(b_obj_arg socket, obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_cancel_recv(b_obj_arg socket) {
lean_uv_udp_socket_object* udp_socket = lean_to_uv_udp_socket(socket);
lean_inc(socket);
@@ -397,7 +397,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_cancel_recv(b_obj_arg socket, ob
// UDP Socket Utility Functions
/* Std.Internal.UV.UDP.Socket.getPeerName (socket : @& Socket) : IO SocketAddress */
extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_getpeername(b_obj_arg socket, obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_getpeername(b_obj_arg socket) {
lean_uv_udp_socket_object *udp_socket = lean_to_uv_udp_socket(socket);
struct sockaddr_storage addr_storage;
@@ -436,7 +436,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_getsockname(b_obj_arg socket) {
}
/* Std.Internal.UV.UDP.Socket.setBroadcast (socket : @& Socket) (on : Bool) : IO Unit */
extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_set_broadcast(b_obj_arg socket, uint8_t enable, obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_set_broadcast(b_obj_arg socket, uint8_t enable) {
lean_uv_udp_socket_object *udp_socket = lean_to_uv_udp_socket(socket);
event_loop_lock(&global_ev);
@@ -451,7 +451,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_set_broadcast(b_obj_arg socket,
}
/* Std.Internal.UV.UDP.Socket.setMulticastLoop (socket : @& Socket) (on : Bool) : IO Unit */
extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_set_multicast_loop(b_obj_arg socket, uint8_t enable, obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_set_multicast_loop(b_obj_arg socket, uint8_t enable) {
lean_uv_udp_socket_object *udp_socket = lean_to_uv_udp_socket(socket);
event_loop_lock(&global_ev);
@@ -466,7 +466,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_set_multicast_loop(b_obj_arg soc
}
/* Std.Internal.UV.UDP.Socket.setMulticastTTL (socket : @& Socket) (ttl : UInt32) : IO Unit */
extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_set_multicast_ttl(b_obj_arg socket, uint32_t ttl, obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_set_multicast_ttl(b_obj_arg socket, uint32_t ttl) {
lean_uv_udp_socket_object *udp_socket = lean_to_uv_udp_socket(socket);
event_loop_lock(&global_ev);
@@ -481,7 +481,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_set_multicast_ttl(b_obj_arg sock
}
/* Std.Internal.UV.UDP.Socket.setMembership (socket : @& Socket) (multicastAddr : @& IpAddr) (interfaceAddr : @& Option IpAddr) (membership : UInt8) : IO Unit */
extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_set_membership(b_obj_arg socket, b_obj_arg multicast_addr, b_obj_arg interface_addr, uint8_t membership, obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_set_membership(b_obj_arg socket, b_obj_arg multicast_addr, b_obj_arg interface_addr, uint8_t membership) {
lean_uv_udp_socket_object *udp_socket = lean_to_uv_udp_socket(socket);
char multicast_addr_str[INET_ADDRSTRLEN];
@@ -507,7 +507,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_set_membership(b_obj_arg socket,
}
/* Std.Internal.UV.UDP.Socket.setMulticastInterface (socket : @& Socket) (interfaceAddr : @& IPAddr) : IO Unit */
extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_set_multicast_interface(b_obj_arg socket, b_obj_arg interface_addr, obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_set_multicast_interface(b_obj_arg socket, b_obj_arg interface_addr) {
lean_uv_udp_socket_object *udp_socket = lean_to_uv_udp_socket(socket);
char interface_addr_str[INET_ADDRSTRLEN];
@@ -525,7 +525,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_set_multicast_interface(b_obj_ar
}
/* Std.Internal.UV.UDP.Socket.setTTL (socket : @& Socket) (ttl : UInt32) : IO Unit */
extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_set_ttl(b_obj_arg socket, uint32_t ttl, obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_set_ttl(b_obj_arg socket, uint32_t ttl) {
lean_uv_udp_socket_object *udp_socket = lean_to_uv_udp_socket(socket);
event_loop_lock(&global_ev);
@@ -541,31 +541,31 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_set_ttl(b_obj_arg socket, uint32
#else
extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_new(obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_new() {
lean_always_assert(
false && ("Please build a version of Lean4 with libuv to invoke this.")
);
}
extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_bind(b_obj_arg socket, b_obj_arg addr, obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_bind(b_obj_arg socket, b_obj_arg addr) {
lean_always_assert(
false && ("Please build a version of Lean4 with libuv to invoke this.")
);
}
extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_connect(b_obj_arg socket, b_obj_arg addr, obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_connect(b_obj_arg socket, b_obj_arg addr) {
lean_always_assert(
false && ("Please build a version of Lean4 with libuv to invoke this.")
);
}
extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_send(b_obj_arg socket, obj_arg data, b_obj_arg opt_addr, obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_send(b_obj_arg socket, obj_arg data, b_obj_arg opt_addr) {
lean_always_assert(
false && ("Please build a version of Lean4 with libuv to invoke this.")
);
}
extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_recv(b_obj_arg socket, uint64_t buffer_size, obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_recv(b_obj_arg socket, uint64_t buffer_size) {
lean_always_assert(
false && ("Please build a version of Lean4 with libuv to invoke this.")
);
@@ -574,7 +574,7 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_recv(b_obj_arg socket, uint64_t
// =======================================
// UDP Socket Utility Functions
extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_getpeername(b_obj_arg socket, obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_getpeername(b_obj_arg socket) {
lean_always_assert(
false && ("Please build a version of Lean4 with libuv to invoke this.")
);
@@ -586,41 +586,41 @@ extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_getsockname(b_obj_arg socket) {
);
}
extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_set_broadcast(b_obj_arg socket, uint8_t enable, obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_set_broadcast(b_obj_arg socket, uint8_t enable) {
lean_always_assert(
false && ("Please build a version of Lean4 with libuv to invoke this.")
);
}
extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_set_multicast_loop(b_obj_arg socket, uint8_t enable, obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_set_multicast_loop(b_obj_arg socket, uint8_t enable) {
lean_always_assert(
false && ("Please build a version of Lean4 with libuv to invoke this.")
);
}
extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_set_multicast_ttl(b_obj_arg socket, uint32_t ttl, obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_set_multicast_ttl(b_obj_arg socket, uint32_t ttl) {
lean_always_assert(
false && ("Please build a version of Lean4 with libuv to invoke this.")
);
}
extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_set_membership(b_obj_arg socket, b_obj_arg multicast_addr, b_obj_arg interface_addr, uint8_t membership, obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_set_membership(b_obj_arg socket, b_obj_arg multicast_addr, b_obj_arg interface_addr, uint8_t membership) {
lean_always_assert(
false && ("Please build a version of Lean4 with libuv to invoke this.")
);
}
extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_set_multicast_interface(b_obj_arg socket, b_obj_arg interface_addr, obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_set_multicast_interface(b_obj_arg socket, b_obj_arg interface_addr) {
lean_always_assert(
false && ("Please build a version of Lean4 with libuv to invoke this.")
);
}
extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_set_ttl(b_obj_arg socket, uint32_t ttl, obj_arg /* w */) {
extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_set_ttl(b_obj_arg socket, uint32_t ttl) {
lean_always_assert(
false && ("Please build a version of Lean4 with libuv to invoke this.")
);
}
#endif
}
}

28
src/runtime/uv/udp.h
View File

@@ -38,24 +38,24 @@ static inline lean_uv_udp_socket_object* lean_to_uv_udp_socket(lean_object * o)
// =======================================
// UDP Socket Operations
extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_new(obj_arg /* w */);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_bind(b_obj_arg socket, b_obj_arg addr, obj_arg /* w */);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_connect(b_obj_arg socket, b_obj_arg addr, obj_arg /* w */);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_send(b_obj_arg socket, obj_arg data_array, b_obj_arg opt_addr, obj_arg /* w */);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_recv(b_obj_arg socket, uint64_t buffer_size, obj_arg /* w */);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_wait_readable(b_obj_arg socket, obj_arg /* w */);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_cancel_recv(b_obj_arg socket, obj_arg /* w */);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_new();
extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_bind(b_obj_arg socket, b_obj_arg addr);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_connect(b_obj_arg socket, b_obj_arg addr);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_send(b_obj_arg socket, obj_arg data_array, b_obj_arg opt_addr);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_recv(b_obj_arg socket, uint64_t buffer_size);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_wait_readable(b_obj_arg socket);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_cancel_recv(b_obj_arg socket);
// =======================================
// UDP Socket Utility Functions
extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_getpeername(b_obj_arg socket, obj_arg /* w */);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_getpeername(b_obj_arg socket);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_getsockname(b_obj_arg socket);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_set_broadcast(b_obj_arg socket, uint8_t enable, obj_arg /* w */);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_set_multicast_loop(b_obj_arg socket, uint8_t enable, obj_arg /* w */);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_set_multicast_ttl(b_obj_arg socket, uint32_t ttl, obj_arg /* w */);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_set_membership(b_obj_arg socket, b_obj_arg multicast_addr, b_obj_arg interface_addr, uint8_t membership, obj_arg /* w */);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_set_multicast_interface(b_obj_arg socket, b_obj_arg interface_addr, obj_arg /* w */);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_set_ttl(b_obj_arg socket, uint32_t ttl, obj_arg /* w */);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_set_broadcast(b_obj_arg socket, uint8_t enable);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_set_multicast_loop(b_obj_arg socket, uint8_t enable);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_set_multicast_ttl(b_obj_arg socket, uint32_t ttl);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_set_membership(b_obj_arg socket, b_obj_arg multicast_addr, b_obj_arg interface_addr, uint8_t membership);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_set_multicast_interface(b_obj_arg socket, b_obj_arg interface_addr);
extern "C" LEAN_EXPORT lean_obj_res lean_uv_udp_set_ttl(b_obj_arg socket, uint32_t ttl);
}

1
src/util/io.h
View File

@@ -50,4 +50,5 @@ template<typename T> T get_io_scalar_result(object * o) {
return r;
}
}
}

8
src/util/option_declarations.cpp
View File

@@ -14,10 +14,10 @@ typedef object_ref option_decl;
extern "C" object * lean_data_value_to_string (obj_arg d);
extern "C" object * lean_get_option_decls_array(obj_arg w);
extern "C" object * lean_get_option_decls_array();
option_declarations get_option_declarations() {
auto decl_array = get_io_result<array_ref<pair_ref<name, option_decl> > > (lean_get_option_decls_array(io_mk_world()));
auto decl_array = get_io_result<array_ref<pair_ref<name, option_decl> > > (lean_get_option_decls_array());
option_declarations r;
for (pair_ref<name, option_decl> const & p : decl_array) {
option_decl decl = p.snd();
@@ -46,10 +46,10 @@ data_value mk_data_value(data_value_kind k, char const * val) {
}
}
extern "C" object * lean_register_option(obj_arg name, obj_arg decl, obj_arg w);
extern "C" object * lean_register_option(obj_arg name, obj_arg decl);
void register_option(name const & n, name const & decl_name, data_value_kind k, char const * default_value, char const * description) {
object_ref decl = mk_cnstr(0, decl_name, mk_data_value(k, default_value), string_ref(""), string_ref(description));
consume_io_result(lean_register_option(n.to_obj_arg(), decl.to_obj_arg(), io_mk_world()));
consume_io_result(lean_register_option(n.to_obj_arg(), decl.to_obj_arg()));
}
}

26
src/util/shell.cpp
View File

@@ -157,9 +157,9 @@ int getopt_long(int argc, char *in_argv[], const char *optstring, const option *
using namespace lean; // NOLINT
extern "C" obj_res lean_display_header(obj_arg);
extern "C" obj_res lean_display_header();
static void display_header() {
consume_io_result(lean_display_header(io_mk_world()));
consume_io_result(lean_display_header());
}
static void display_version(std::ostream & out) {
@@ -174,9 +174,9 @@ static void display_features(std::ostream & out) {
out << "]\n";
}
extern "C" obj_res lean_display_help(uint8 use_stderr, obj_arg);
extern "C" obj_res lean_display_help(uint8 use_stderr);
static void display_help(bool use_stderr) {
consume_io_result(lean_display_help(use_stderr, io_mk_world()));
consume_io_result(lean_display_help(use_stderr));
}
static int only_src_deps = 0;
@@ -292,8 +292,7 @@ extern "C" obj_res lean_shell_main(
uint8 json_output,
obj_arg error_kinds,
uint8 print_stats,
uint8 run,
obj_arg w
uint8 run
);
uint32 run_shell_main(
int argc, char* argv[],
@@ -342,19 +341,18 @@ uint32 run_shell_main(
json_output,
error_kinds.to_obj_arg(),
print_stats,
run,
io_mk_world()
run
));
}
extern "C" object* lean_init_search_path(object* w);
extern "C" object* lean_init_search_path();
void init_search_path() {
get_io_scalar_result<unsigned>(lean_init_search_path(io_mk_world()));
get_io_scalar_result<unsigned>(lean_init_search_path());
}
extern "C" object* lean_environment_free_regions(object * env, object * w);
extern "C" object* lean_environment_free_regions(object * env);
void environment_free_regions(elab_environment && env) {
consume_io_result(lean_environment_free_regions(env.steal(), io_mk_world()));
consume_io_result(lean_environment_free_regions(env.steal()));
}
}
@@ -365,7 +363,7 @@ void check_optarg(char const * option_name) {
}
}
extern "C" object * lean_enable_initializer_execution(object * w);
extern "C" object * lean_enable_initializer_execution();
namespace lean {
extern void (*g_lean_report_task_get_blocked_time)(std::chrono::nanoseconds);
@@ -437,7 +435,7 @@ extern "C" LEAN_EXPORT int lean_main(int argc, char ** argv) {
std::cerr << "error: " << ex.what() << std::endl;
return 1;
}
consume_io_result(lean_enable_initializer_execution(io_mk_world()));
consume_io_result(lean_enable_initializer_execution());
options opts = get_default_options();
optional<std::string> c_output;

BIN
stage0/src/CMakeLists.txt generated
View File

Binary file not shown.

BIN
stage0/src/include/lean/lean.h generated
View File

Binary file not shown.

BIN
stage0/src/kernel/trace.cpp generated
View File

Binary file not shown.

BIN
stage0/src/kernel/trace.h generated
View File

Binary file not shown.

BIN
stage0/src/library/ir_interpreter.cpp generated
View File

Binary file not shown.

BIN
stage0/src/library/ir_types.h generated
View File

Binary file not shown.

BIN
stage0/src/library/llvm.cpp generated
View File

Binary file not shown.

BIN
stage0/src/library/time_task.cpp generated
View File

Binary file not shown.

BIN
stage0/src/runtime/interrupt.cpp generated
View File

Binary file not shown.

BIN
stage0/src/runtime/io.cpp generated
View File

Binary file not shown.

BIN
stage0/src/runtime/memory.cpp generated
View File

Binary file not shown.

BIN
stage0/src/runtime/mutex.cpp generated
View File

Binary file not shown.

BIN
stage0/src/runtime/object.cpp generated
View File

Binary file not shown.

BIN
stage0/src/runtime/process.cpp generated
View File

Binary file not shown.

BIN
stage0/src/runtime/uv/dns.cpp generated
View File

Binary file not shown.

BIN
stage0/src/runtime/uv/event_loop.cpp generated
View File

Binary file not shown.

BIN
stage0/src/util/io.h generated
View File

Binary file not shown.

BIN
stage0/src/util/timeit.h generated
View File

Binary file not shown.

BIN
stage0/stdlib/Init/Control/Option.c generated
View File

Binary file not shown.

BIN
stage0/stdlib/Init/Data/BitVec/Basic.c generated
View File

Binary file not shown.

BIN
stage0/stdlib/Init/Data/Format/Basic.c generated
View File

Binary file not shown.

BIN
stage0/stdlib/Init/Data/Format/Syntax.c generated
View File

Binary file not shown.

BIN
stage0/stdlib/Init/Data/Iterators/Consumers/Loop.c generated
View File

Binary file not shown.

BIN
stage0/stdlib/Init/Data/Iterators/Consumers/Monadic/Loop.c generated
View File

Binary file not shown.

BIN
stage0/stdlib/Init/Data/Iterators/Lemmas/Consumers/Loop.c generated
View File

Binary file not shown.

BIN
stage0/stdlib/Init/Data/Iterators/Lemmas/Consumers/Monadic/Loop.c generated
View File

Binary file not shown.

BIN
stage0/stdlib/Init/Data/List/Monadic.c generated
View File

Binary file not shown.

BIN
stage0/stdlib/Init/Data/Random.c generated
View File

Binary file not shown.

BIN
stage0/stdlib/Init/Data/Repr.c generated
View File

Binary file not shown.

BIN
stage0/stdlib/Init/Data/String/Basic.c generated
View File

Binary file not shown.

BIN
stage0/stdlib/Init/Data/String/Pattern/Basic.c generated
View File

Binary file not shown.

BIN
stage0/stdlib/Init/Data/String/Pattern/String.c generated
View File

Binary file not shown.

BIN
stage0/stdlib/Init/Data/String/Slice.c generated
View File

Binary file not shown.

BIN
stage0/stdlib/Init/Data/ToString/Basic.c generated
View File

Binary file not shown.

BIN
stage0/stdlib/Init/Data/ToString/Name.c generated
View File

Binary file not shown.

BIN
stage0/stdlib/Init/Grind/Interactive.c generated
View File

Binary file not shown.

BIN
stage0/stdlib/Init/Grind/Ordered/Linarith.c generated
View File

Binary file not shown.

BIN
stage0/stdlib/Init/Grind/Ring/CommSolver.c generated
View File

Binary file not shown.

BIN
stage0/stdlib/Init/Internal/Order/Basic.c generated
View File

Binary file not shown.

BIN
stage0/stdlib/Init/NotationExtra.c generated
View File

Binary file not shown.

BIN
stage0/stdlib/Init/Prelude.c generated
View File

Binary file not shown.

BIN
stage0/stdlib/Init/Simproc.c generated
View File

Binary file not shown.

BIN
stage0/stdlib/Init/System/IO.c generated
View File

Binary file not shown.

BIN
stage0/stdlib/Init/System/ST.c generated
View File

Binary file not shown.

Some files were not shown because too many files have changed in this diff Show More