-
Notifications
You must be signed in to change notification settings - Fork 2
/
Generic.cbs
49 lines (37 loc) · 1.03 KB
/
Generic.cbs
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
### 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