init commit again
This commit is contained in:
Peter
346
IBAF-cbs/Funcons-beta/Computations/Normal/Storing/Storing.cbs
Normal file
346
IBAF-cbs/Funcons-beta/Computations/Normal/Storing/Storing.cbs
Normal file
@@ -0,0 +1,346 @@
|
||||
### 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
|
||||
Reference in New Issue
Block a user