### Storing

[
  Datatype locations                     Alias locs
  Type     stores
  Entity   store
  Funcon   initialise-storing
  Funcon   store-clear
  Datatype variables                     Alias vars
  Funcon   variable                      Alias var
  Funcon   allocate-variable             Alias alloc
  Funcon   recycle-variables             Alias recycle
  Funcon   initialise-variable           Alias init
  Funcon   allocate-initialised-variable Alias alloc-init
  Funcon   assign
  Funcon   assigned
  Funcon   current-value
  Funcon   un-assign
  Funcon   structural-assign
  Funcon   structural-assigned
]


Meta-variables
  T, T' <: values


#### Stores

Type
  locations ~> atoms
Alias
  locs = locations
/*
  A storage location is represented by an atom.
*/
 
 
Type
  stores ~> maps(locations, values?)
/*
  The domain of a store is the set of currently allocated locations.
  Mapping a location to `( )` models the absence of its stored value;
  removing it from the store allows it to be re-allocated.
*/


Entity
  < _ , store(_:stores) > ---> < _ , store(_:stores) >
/*
  The current store is a mutable entity.
  A transition ``< X , store(Sigma) > ---> < X' , store(Sigma') >`` models
  a step from `X` to `X'` where the difference between `Sigma` and `Sigma'`
  (if any) corresponds to storage effects.
*/


Funcon
  store-clear : =>null-type
Rule
  < store-clear , store(_) > ---> < null-value , store(map( )) >
/*
  `store-clear` ensures the store is empty.
*/


Funcon 
  initialise-storing(X:=>T) : =>T
   ~> sequential(store-clear, 
        initialise-giving(initialise-generating(X)))
Alias
  init-storing = initialise-storing
/*
  `initialise-storing(X)` ensures that the entities used by the funcons for
  storing are properly initialised.
*/


#### Simple variables

/*  
  Simple variables may store primitive or structured values. The type of
  values stored by a variable is fixed when it is allocated. For instance,
  `allocate-variable(integers)` allocates a simple integer variable, and
  `allocate-variable(vectors(integers))` allocates a structured variable for
  storing vectors of integers, which can be updated only monolithically.
*/

Datatype
  variables ::= variable(_:locations, _:value-types)
Alias
  vars = variables
Alias
  var = variable
/*
  `variables` is the type of simple variables that can store values of
  a particular type.

  `variable(L, T)` constructs a simple variable for storing values of
  type `T` at location `L`. Variables at different locations are independent. 
  
  Note that `variables` is a subtype of `datatype-values`.
*/


Funcon
  allocate-variable(T:types) : =>variables
Alias
  alloc = allocate-variable
/*
  `allocate-variable(T)` gives a simple variable whose location is not in the
  current store. Subsequent uses of `allocate-variable(T')` give independent
  variables, except after `recycle-variables(V,...)` or `store-clear`.
*/
Rule
  < use-atom-not-in(dom(Sigma)) , store(Sigma) > ---> < L , store(Sigma') >
  map-override({L |-> ( )}, Sigma') ~> Sigma''
  -------------------------------------------------------------------------
  < allocate-variable(T:types) , store(Sigma) >
    ---> < variable(L, T) , store(Sigma'') >


Funcon
  recycle-variables(_:variables+) : =>null-type
Alias
  recycle = recycle-variables
/*
  `recycle-variables(Var,...)` removes the locations of `Var`, ..., from the
  current store, so that they may subsequently be re-allocated.
*/
Rule
  is-in-set(L, dom(Sigma)) == true
  ---------------------------------------------------------------------
  < recycle-variables(variable(L:locations, T:types)) , store(Sigma) >
    ---> < null-value , store(map-delete(Sigma, {L})) >
Rule
  is-in-set(L, dom(Sigma)) == false
  ---------------------------------------------------------------------
  < recycle-variables(variable(L:locations, T:types)) , store(Sigma) >
    ---> < fail , store(Sigma) >
Rule
  recycle-variables(Var:variables, Var+:variables+)
    ~> sequential(recycle-variables(Var), recycle-variables(Var+))


Funcon
  initialise-variable(_:variables, _:values) : =>null-type
Alias
  init = initialise-variable
/*
  `initialise-variable(Var, Val)` assigns `Val` as the initial value of `Var`,
  and gives `null-value`. If `Var` already has an assigned value, it fails.
*/
Rule
  and(is-in-set(L, dom(Sigma)),
      not is-value(map-lookup(Sigma, L)),
      is-in-type(Val, T)) 
    == true
  ----------------------------------------------------------------------------
  < initialise-variable(variable(L:locations, T:types), Val:values) , 
    store(Sigma) > ---> < null-value , store(map-override({L|->Val}, Sigma)) >
Rule
  and(is-in-set(L, dom(Sigma)),
      not is-value(map-lookup(Sigma, L)),
      is-in-type(Val, T)) 
    == false
  ----------------------------------------------------------------------------
  < initialise-variable(variable(L:locations, T:types), Val:values) , 
    store(Sigma) > ---> < fail , store(Sigma) >


Funcon
  allocate-initialised-variable(T, Val:T) : =>variables
    ~> give(allocate-variable(T),
         sequential(initialise-variable(given, Val), given))
Alias
  alloc-init = allocate-initialised-variable
/*
  `allocate-initialised-variable(T, Val)` allocates a simple variable for
  storing values of type `T`, initialises its value to `Val`, and returns the
  variable.
*/


Funcon
  assign(_:variables, _:values) : =>null-type
/*
  `assign(Var, Val)` assigns the value `Val` to the variable `Var`,
  provided that `Var` was allocated with a type that contains `Val`.
*/
Rule
  and(is-in-set(L, dom(Sigma)), is-in-type(Val, T)) == true
  -----------------------------------------------------------------------
  < assign(variable(L:locations, T:types), Val:values) ,
    store(Sigma) > ---> < null-value , store(map-override({L|->Val}, Sigma)) >
Rule
   and(is-in-set(L, dom(Sigma)), is-in-type(Val, T)) == false
  --------------------------------------------------------------------------
  < assign(variable(L:locations,T:types), Val:values) ,
    store(Sigma) > ---> < fail , store(Sigma) >


Funcon
  assigned(_:variables) : =>values
/*
  `assigned(Var)` gives the value assigned to the variable `Var`,
  failing if no value is currently assigned.
*/
Rule
  map-lookup(Sigma, L) ~> (Val:values)
  ------------------------------------------------------------------
  < assigned(variable(L:locations, T:types)) , store(Sigma) >
    ---> < Val , store(Sigma) >
Rule
  map-lookup(Sigma, L) == ( )
  ------------------------------------------------------------------
  < assigned(variable(L:locations, T:types)) , store(Sigma) >
    ---> < fail , store(Sigma) >


Funcon
  current-value(_:values) : =>values
/*
  `current-value(V)` gives the same result as `assigned(V)` when `V` is a
  simple variable, and otherwise gives `V`. 
  
  It represents implicit dereferencing of a value that might be a variable.
*/
Rule
  current-value(Var:variables) ~> assigned(Var)
Rule
  current-value(U:~variables) ~> U


Funcon
  un-assign(_:variables) : =>null-type
/*
  `un-assign(Var)` remove the value assigned to the variable `Var`.
*/
Rule
  is-in-set(L, dom(Sigma)) == true
  --------------------------------------------------------------------------
  < un-assign(variable(L:locations, T:types)) , store(Sigma) >
    ---> < null-value , store(map-override({L |-> ( )}, Sigma)) >
Rule
   is-in-set(L, dom(Sigma)) == false
  --------------------------------------------------------------------------
  < un-assign(variable(L:locations, T:types)) , store(Sigma) >
    ---> < fail , store(Sigma) >


#### Structured variables

/*
  Structured variables are structured values where some components are
  simple variables. Such component variables can be selected using the
  same funcons as for selecting components of structured values. 

  Structured variables containing both simple variables and values correspond
  to hybrid structures where particular components are mutable.
  
  All datatypes (except for abstractions) can be used to form structured
  variables. So can maps, but not sets or multisets. 
  
  Structural generalisations of `assign(Var, Val)` and 
  `assigned(Var)` access all the simple variables contained in a
  structured variable. Assignment requires each component value of a hybrid
  structured variable to be equal to the corresponding component of the
  structured value.
*/

Funcon
  structural-assign(_:values, _:values) : =>null-type
/*
  `structural-assign(V1, V2)` takes a (potentially) structured variable
  `V1`and a (potentially) structured value `V2`. Provided that the structure
  and all non-variable values in `V1` match the structure and corresponding
  values of `V2`, all the simple variables in `V1` are assigned the
  corresponding values of `V2`; otherwise the assignment fails.
*/
Rule
  structural-assign(V1:variables, V2:values)
    ~> assign(V1, V2)
Rule
  V1 : ~(variables)
  V1 ~> datatype-value(I1:identifiers, V1*:values*)
  V2 ~> datatype-value(I2:identifiers, V2*:values*)
  -----------------------------------------------------------------------
  structural-assign(V1:datatype-values, V2:datatype-values)
    ~> sequential(
         check-true(is-equal(I1, I2)),
         effect(tuple(interleave-map(
           structural-assign(tuple-elements(given)),
           tuple-zip(tuple(V1*), tuple(V2*))))),
         null-value)
/*
  Note that simple variables are datatype values.
*/
Rule
  dom(M1) == {}
  ------------------------------------------------------
  structural-assign(M1:maps(_,_), M2:maps(_,_))
    ~> check-true(is-equal(dom(M2), { }))
Rule
  some-element(dom(M1)) ~> K
  ----------------------------------------------------------------------------
  structural-assign(M1:maps(_, _), M2:maps(_, _))
    ~> sequential(check-true(is-in-set(K, dom(M2))),
         structural-assign(map-lookup(M1, K), map-lookup(M2, K)),
         structural-assign(map-delete(M1, {K}), map-delete(M2, {K})))
Rule
  V1 : ~(datatype-values|maps(_, _))
  ---------------------------------------------------------------
  structural-assign(V1:values,V2:values)
    ~> check-true(is-equal(V1, V2))


Funcon
  structural-assigned(_:values) : =>values
/*
  `structural-assigned(V)` takes a (potentially) structured variable `V`,
  and computes the value of `V` with all simple variables in `V` replaced by
  their assigned values, failing if any of them do not have assigned values.
  
  When `V` is just a simple variable or a (possibly structured) value with no
  component variables, `structural-assigned(V)` gives the same result as
  `current-value(V)`.
*/
Rule
  structural-assigned(Var:variables) ~> assigned(Var)
Rule
  V : ~(variables)
  V ~> datatype-value(I:identifiers, V*:values*)
  ----------------------------------------------------------------------------
  structural-assigned(V:datatype-values)
    ~> datatype-value(I, interleave-map(structural-assigned(given), V*))
/*
  Note that simple variables are datatype values.
*/
Rule
  structural-assigned(M:maps(_, _))
    ~> map(interleave-map(structural-assigned(given), map-elements(M)))
Rule
  U : ~(datatype-values|maps(_, _))
  ------------------------------------------
  structural-assigned(U:values) ~> U