50 lines
1.0 KiB
Plaintext
50 lines
1.0 KiB
Plaintext
### Generic abstractions
|
|
|
|
[
|
|
Type abstractions
|
|
Funcon abstraction
|
|
Funcon closure
|
|
Funcon enact
|
|
]
|
|
|
|
|
|
Meta-variables
|
|
T <: values
|
|
T? <: values?
|
|
|
|
|
|
Type
|
|
abstractions(_:computation-types)
|
|
|
|
|
|
Funcon
|
|
abstraction(_:T?=>T) : abstractions(T?=>T)
|
|
/*
|
|
The funcon `abstraction(X)` forms abstraction values from computations.
|
|
|
|
References to bindings of identifiers in `X` are dynamic.
|
|
The funcon `closure(X)` forms abstractions with static bindings.
|
|
*/
|
|
|
|
|
|
Funcon
|
|
closure(_:T?=>T) : =>abstractions(T?=>T)
|
|
/*
|
|
`closure(X)` computes a closed abstraction from the computation `X`.
|
|
In contrast to `abstraction(X)`, references to bindings of identifiers
|
|
in `X` are static. Moreover, `closure(X)` is not a value constructor,
|
|
so it cannot be used in pattern terms in rules.
|
|
*/
|
|
Rule
|
|
environment(Rho) |- closure(X) ---> abstraction(closed(scope(Rho, X)))
|
|
|
|
|
|
Funcon
|
|
enact(_:abstractions(T?=>T)) : T?=>T
|
|
/*
|
|
`enact(A)` executes the computation of the abstraction `A`,
|
|
with access to all the current entities.
|
|
*/
|
|
Rule
|
|
enact(abstraction(X)) ~> X
|