☰
open
io.file.open
Functions
does this effect support abort?
Redefining this to return `false` helps to detect unexptected calls to
`abort` at runtime and ensure that the static analysis finds that the
code executed with this effect will always return normally and produce
a result. This is used, e.g, in `mutate` to avoid static analysis
reporting `panic` as an effect of the use of a local mutate instance.
Redefining this to return `false` helps to detect unexptected calls to
`abort` at runtime and ensure that the static analysis finds that the
code executed with this effect will always return normally and produce
a result. This is used, e.g, in `mutate` to avoid static analysis
reporting `panic` as an effect of the use of a local mutate instance.
create a String from this instance. Unless redefined, `a.as_string` will
create `"instance[T]"` where `T` is the dynamic type of `a`
create `"instance[T]"` where `T` is the dynamic type of `a`
convenience version of `type.default` for effect values whose type is
exactly the effect type (i.e., the value type does not inherit
from the effect type).
set default instance for effect type `effect.this` to value `effect.this`.
NYI: UNDER DEVELOPMENT: See type.default
exactly the effect type (i.e., the value type does not inherit
from the effect type).
set default instance for effect type `effect.this` to value `effect.this`.
NYI: UNDER DEVELOPMENT: See type.default
Get the dynamic type of this instance. For value instances `x`, this is
equal to `type_of x`, but for `x` with a `ref` type `x.dynamic_type` gives
the actual runtime type, while `type_of x` results in the static
compile-time type.
There is no dynamic type of a type instance since this would result in an
endless hierarchy of types. So for Type values, dynamic_type is redefined
to just return Type.type.
equal to `type_of x`, but for `x` with a `ref` type `x.dynamic_type` gives
the actual runtime type, while `type_of x` results in the static
compile-time type.
There is no dynamic type of a type instance since this would result in an
endless hierarchy of types. So for Type values, dynamic_type is redefined
to just return Type.type.
get the current byte position in the file
feature that will be called on the final instance of this effect
after it has been de-instated.
This happens either on a normal return form the code passed to
`instate`, on an abort perfomed on this effect or on an abort
performed on an effect instated prior to this effect's instation.
This can be used to perform actions when leaving an effect such
a cleanup up resources that were created or opened by operations
of this effect.
after it has been de-instated.
This happens either on a normal return form the code passed to
`instate`, on an abort perfomed on this effect or on an abort
performed on an effect instated prior to this effect's instation.
This can be used to perform actions when leaving an effect such
a cleanup up resources that were created or opened by operations
of this effect.
convenience version of `instate` for effect values whose type is
exactly the effect type (i.e., the value type does not inherit
from the effect type).
Execute 'code' in a context where this effect instance has been
instated for effect type `effect.this`.
In case `f` returns normally, this will return `f`'s result.
In case `f` aborts this effect, this will panic.
exactly the effect type (i.e., the value type does not inherit
from the effect type).
Execute 'code' in a context where this effect instance has been
instated for effect type `effect.this`.
In case `f` returns normally, this will return `f`'s result.
In case `f` aborts this effect, this will panic.
§(R type, offset i64, size i64, code Unary io.file.open.mmap.R (io.this.file.this.open.this io.file.open.T).mapped_buffer):Any => outcome io.file.open.mmap.R
§(R
type
, offset i64, size i64, code Unary io.file.open.mmap.R (io.this.file.this.open.this io.file.open.T).mapped_buffer):
Any =>
outcome io.file.open.mmap.Rinstall mmap effect an run code
note: the offset must be a multiple of the pagesize which usually is 4096, windows 65536?
note: offset+size must not exceed size of file
example usage:
_ := io.file.use unit "/some_file" io.file.mode.append ()->
io.file.open.mmap (i64 0) (i64 100) ()->
note: the offset must be a multiple of the pagesize which usually is 4096, windows 65536?
note: offset+size must not exceed size of file
example usage:
_ := io.file.use unit "/some_file" io.file.mode.append ()->
io.file.open.mmap (i64 0) (i64 100) ()->
convenience prefix operator to create a string from a value.
This permits usage of `$` as a prefix operator in a similar way both
inside and outside of constant strings: $x and "$x" will produce the
same string.
This permits usage of `$` as a prefix operator in a similar way both
inside and outside of constant strings: $x and "$x" will produce the
same string.
reads all bytes from the file in the path
returns outcome array u8, a byte array representing the content of the file if the operation was successful
returns an error in case the operation fails
returns outcome array u8, a byte array representing the content of the file if the operation was successful
returns an error in case the operation fails
replace existing effect of type `effect.this` by the new effect value `effect.this`.
This is a convenience feature for value type effects for which the type of
the effect instance equals the effect type. `ref` type effects typically have
values that may be children of the effect type that are of a different type, so
`effect_type.replace new_value` must be used.
replace may only be called during the execution of an operation of a currently instated
effect of the same effect type.
This is a convenience feature for value type effects for which the type of
the effect instance equals the effect type. `ref` type effects typically have
values that may be children of the effect type that are of a different type, so
`effect_type.replace new_value` must be used.
replace may only be called during the execution of an operation of a currently instated
effect of the same effect type.
writes the content of an array of bytes to a file opened as fd
this might overwrite parts or all of an existing file.
this might overwrite parts or all of an existing file.
Value Types
mapped buffer gives access to the memory region a file is mapped
to via `mmap`.
to via `mmap`.
Type Features
Abort code execution for the instated effect.this.env and return to the point
where the effect was instated.
where the effect was instated.
replace existing effect for type `effect.this` by the new effect value `e`
and abort code execution to return to the point where the effect was instated.
and abort code execution to return to the point where the effect was instated.
string representation of this type to be used for debugging.
result has the form "Type of '<name>'", but this might change in the future
result has the form "Type of '<name>'", but this might change in the future
set default instance for effect type `effect.this` to `e`
NYI: UNDER DEVELOPMENT: This is a manual work-around to automatically install
default effects. It should be replaced by a effect configuration file that
is defined locally to a fuzion project or globally to the fuzion installation
the defines the default effects to be used. The DFA should then automatically
determine the required effects and create code to instate them at the beginning
of an application.
NYI: UNDER DEVELOPMENT: This is a manual work-around to automatically install
default effects. It should be replaced by a effect configuration file that
is defined locally to a fuzion project or globally to the fuzion installation
the defines the default effects to be used. The DFA should then automatically
determine the required effects and create code to instate them at the beginning
of an application.
There is no dynamic type of a type instance since this would result in an
endless hierarchy of types, so dynamic_type is redefined to just return
Type.type here.
endless hierarchy of types, so dynamic_type is redefined to just return
Type.type here.
has an effect of the given type been instated?
Is this type assignable to a type parameter with constraint `T`?
The result of this is a compile-time constant that can be used to specialize
code for a particular type.
is_of_integer_type(n T : numeric) => T : integer
say (is_of_integer_type 1234) # true
say (is_of_integer_type 3.14) # false
it is most useful in conjunction preconditions or `if` statements as in
pair(a,b T) is
=>
or
val(n T) is
The result of this is a compile-time constant that can be used to specialize
code for a particular type.
is_of_integer_type(n T : numeric) => T : integer
say (is_of_integer_type 1234) # true
say (is_of_integer_type 3.14) # false
it is most useful in conjunction preconditions or `if` statements as in
pair(a,b T) is
=>
or
val(n T) is
execute 'code' in a context where the effect instance `e` has been
installed for effect type `effect.this`.
In case `f` returns normally, this will return `f`'s result.
In case `f` aborts this effect, this will panic.
installed for effect type `effect.this`.
In case `f` returns normally, this will return `f`'s result.
In case `f` aborts this effect, this will panic.
§(R type, e effect.this.type, code Function effect.type.instate.R, def Unary effect.type.instate.R effect.this.type):Any is [Inherited from effect]
§(R
type
, e effect.this.type, code Function effect.type.instate.R, def Unary effect.type.instate.R effect.this.type):
Any is
[Inherited from effect]
execute 'code' in a context where the effect instance `e` has been
installed for effect type `effect.this`.
In case `f` returns normally, this will return `f`'s result.
In case `f` aborts this effect, return `def()`.
installed for effect type `effect.this`.
In case `f` returns normally, this will return `f`'s result.
In case `f` aborts this effect, return `def()`.
has an effect of this type been instated?
name of this type, including type parameters, e.g. 'option (list i32)'.
replace existing effect for type `effect.this` by the new effect value `e`.
For effects that model the outside world (e.g., i/o, time, sensors and actuators, etc.),
the effect might be a unit type, so the replace is effectively a no-operation. However,
the call to `replace` is used ot model the change of the outside world and must be
included for analysis tools to appreciate this.
replace may only be called during the execution of an operation of a currently instated
effect of the same effect type.
NYI: BUG: It is currently not enforced that replace is only called during the execution
of an operation of a currenlty instated effect of the same effect type.
For effects that model the outside world (e.g., i/o, time, sensors and actuators, etc.),
the effect might be a unit type, so the replace is effectively a no-operation. However,
the call to `replace` is used ot model the change of the outside world and must be
included for analysis tools to appreciate this.
replace may only be called during the execution of an operation of a currently instated
effect of the same effect type.
NYI: BUG: It is currently not enforced that replace is only called during the execution
of an operation of a currenlty instated effect of the same effect type.
abort the current execution and return from the surrounding call to
`instate`.
NYI: CLEANUP: `return` is the same as `abort`. The term `return` seems
common for algebraic effects, but is confusing since it is different to
returning from a call. We need to decide to break with algebraic effect
jargon (and remove `return`) or to stick with it (and rename `abort` as
`return`).
`instate`.
NYI: CLEANUP: `return` is the same as `abort`. The term `return` seems
common for algebraic effects, but is confusing since it is different to
returning from a call. We need to decide to break with algebraic effect
jargon (and remove `return`) or to stick with it (and rename `abort` as
`return`).
Get a type as a value.
This is a feature with the effect equivalent to Fuzion's `expr.type` call tail.
It is recommended to use `expr.type` and not `expr.type_value`.
`type_value` is here to show how this can be implemented and to illustrate the
difference to `dynamic_type`.
This is a feature with the effect equivalent to Fuzion's `expr.type` call tail.
It is recommended to use `expr.type` and not `expr.type_value`.
`type_value` is here to show how this can be implemented and to illustrate the
difference to `dynamic_type`.
T is used to distinguish several open files