### 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
/*
  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.
*/


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.
*/
Rule
  fresh-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.
*/
Rule
  environment(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`.
*/
Rule
  environment(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.
*/
Rule
                  D1 ---> 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`.
*/