### Binding
[ Type environments Alias envs Datatype identifiers Alias ids Funcon identifier-tagged Alias id-tagged Funcon fresh-identifier Entity environment Alias env Funcon initialise-binding Funcon bind-value Alias bind Funcon unbind Funcon bound-directly Funcon bound-value Alias bound Funcon closed Funcon scope Funcon accumulate Funcon collateral Funcon bind-recursively Funcon recursive ] Meta-variables T <: values
#### Environments
Type environments ~> maps(identifiers, values?) Alias envs = environments
*/ Datatype identifiers ::= {_:strings} | identifier-tagged(_:identifiers, _:values) Alias ids = identifiers Alias id-tagged = identifier-tagged
/* An identifier is either a string of characters, or an identifier tagged with
some value (e.g., with the identifier of a namespace).
*/ Funcon fresh-identifier : =>identifiers
/* `fresh-identifier` computes an identifier distinct from all previously
computed identifiers.
*/
Rulefresh-identifier ~> identifier-tagged("generated", fresh-atom)
#### Current bindings
Entity environment(_:environments) |- _ ---> _ Alias env = environment
/* The environment entity allows a computation to refer to the current bindings
of identifiers to values.
*/
Funcon initialise-binding(X:=>T) : =>T~> initialise-linking(initialise-generating(closed(X)))
/* `initialise-binding(X)` ensures that `X` does not depend on non-local bindings.
It also ensures that the linking entity (used to represent potentially cyclic
bindings) and the generating entity (for creating fresh identifiers) are
initialised.
*/
Funcon bind-value(I:identifiers, V:values) : =>environments ~> { I |-> V }Alias bind = bind-value
/* `bind-value(I, X)` computes the environment that binds only `I` to the value
computed by `X`.
*/
Funcon unbind(I:identifiers) : =>environments ~> { I |-> ( ) }/* `unbind(I)` computes the environment that hides the binding of `I`.
*/ Funcon bound-directly(_:identifiers) : =>values
/* `bound-directly(I)` returns the value to which `I` is currently bound, if any,
and otherwise fails.
`bound-directly(I)` does *not* follow links. It is used only in connection with
recursively-bound values when references are not encapsulated in abstractions.
*/
Rule lookup(Rho, I) ~> (V:values) -------------------------------------------------------- environment(Rho) |- bound-directly(I:identifiers) ---> V Rule lookup(Rho, I) ~> ( ) ----------------------------------------------------------- environment(Rho) |- bound-directly(I:identifiers) ---> fail
Funcon bound-value(I:identifiers) : =>values~> follow-if-link(bound-directly(I))
Alias bound = bound-value
/* `bound-value(I)` inspects the value to which `I` is currently bound, if any,
and otherwise fails. If the value is a link, `bound-value(I)` returns the
value obtained by following the link, if any, and otherwise fails. If the
inspected value is not a link, `bound-value(I)` returns it.
`bound-value(I)` is used for references to non-recursive bindings and to
recursively-bound values when references are encapsulated in abstractions.
*/
#### Scope
Funcon closed(X:=>T) : =>T
/* `closed(X)` ensures that `X` does not depend on non-local bindings.
*/
Ruleenvironment(map( )) |- X ---> X′ ------------------------------------------- environment(_) |- closed(X) ---> closed(X′) Rule closed(V:T) ~> V
Funcon scope(_:environments, _:=>T) : =>T
/* `scope(D,X)` executes `D` with the current bindings, to compute an environment
`Rho` representing local bindings. It then executes `X` to compute the result,
with the current bindings extended by `Rho`, which may shadow or hide previous
bindings.
`closed(scope(Rho, X))` ensures that `X` can reference only the bindings
provided by `Rho`.
*/
Ruleenvironment(map-override(Rho1, Rho0)) |- X ---> X′ --------------------------------------------------------------------- environment(Rho0) |- scope(Rho1:environments, X) ---> scope(Rho1, X′) Rule scope(_:environments, V:T) ~> V
Funcon accumulate(_:(=>environments)*) : =>environments
/* `accumulate(D1, D2)` executes `D1` with the current bindings, to compute an
environment `Rho1` representing some local bindings. It then executes `D2` to
compute an environment `Rho2` representing further local bindings, with the
current bindings extended by `Rho1`, which may shadow or hide previous
current bindings. The result is `Rho1` extended by `Rho2`, which may shadow
or hide the bindings of `Rho1`.
`accumulate(_, _)` is associative, with `map( )` as unit, and extends to any
number of arguments.
*/
RuleD1 ---> D1'′ ------------------------------------------- accumulate(D1, D2) ---> accumulate(D1'′, D2) Rule accumulate(Rho1:environments, D2) ~> scope(Rho1, map-override(D2, Rho1)) Rule accumulate( ) ~> map( ) Rule accumulate(D1) ~> D1 Rule accumulate(D1, D2, D+) ~> accumulate(D1, accumulate(D2, D+))
Funcon collateral(Rho*:environments*) : =>environments~> checked map-unite(Rho*)
/* `collateral(D1, ...)` pre-evaluates its arguments with the current bindings,
and unites the resulting maps, which fails if the domains are not pairwise
disjoint.
`collateral(D1, D2)` is associative and commutative with `map( )` as unit,
and extends to any number of arguments.
*/
#### Recurse
Funcon bind-recursively(I:identifiers, E:=>values) : =>environments~> recursive({I}, bind-value(I, E))
/* `bind-recursively(I, E)` binds `I` to a link that refers to the value of `E`,
representing a recursive binding of `I` to the value of `E`.
Since `bound-value(I)` follows links, it should not be executed during the
evaluation of `E`.
*/
Funcon recursive(SI:sets(identifiers), D:=>environments) : =>environments~> re-close(bind-to-forward-links(SI), D)
/* `recursive(SI, D)` executes `D` with potential recursion on the bindings of
the identifiers in the set `SI` (which need not be the same as the set of
identifiers bound by `D`).
*/ Auxiliary
Funcon re-close(M:maps(identifiers, links), D:=>environments) : =>environments~> accumulate(scope(M, D), sequential(set-forward-links(M), map( )))
/* `re-close(M, D)` first executes `D` in the scope `M`, which maps identifiers
to freshly allocated links. This computes an environment `Rho` where the bound
values may contain links, or implicit references to links in abstraction
values. It then sets the link for each identifier in the domain of `M` to
refer to its bound value in `Rho`, and returns `Rho` as the result.
*/ Auxiliary
Funcon bind-to-forward-links(SI:sets(identifiers)) : =>maps(identifiers, links)~> map-unite(interleave-map(bind-value(given, fresh-link(values)), set-elements(SI)))
/* `bind-to-forward-links(SI)` binds each identifier in the set `SI` to a
freshly allocated link.
*/ Auxiliary
Funcon set-forward-links(M:maps(identifiers, links)) : =>null-type~> effect(interleave-map(set-link(map-lookup(M, given), bound-value(given)), set-elements(map-domain(M))))
/* For each identifier `I` in the domain of `M`, `set-forward-links(M)` sets the
link to which `I` is mapped by `M` to the current bound value of `I`.
*/
/*An environment represents bindings of identifiers to values. Mapping an identifier to `( )` represents that its binding is hidden. Circularity in environments (due to recursive bindings) is represented using bindings to cut-points called `links`. Funcons are provided for making declarations recursive and for referring to bound values without explicit mention of links, so their existence can generally be ignored.