% $Id: store.mod,v 1.1 1994/04/27 15:23:27 leavens Exp leavens $
%
% Stores as in Schmidt's book "Denotational Semantics"
% (Allyn and Bacon, 1986), chapter 5.  See also Watt's book,
% "Programming Language Syntax and Semantics", section 3.2.
%
% AUTHOR: Gary T. Leavens

module store.

import finite_function mini_cecil_abstract_syntax.

%%% domains
kind	location	type.
kind	store		type -> type.

%%% locations
type loc		typeExpr -> int -> location.

%%% stores
type	empty_store	(store Storable) -> o.
type	alloc		typeExpr -> Storable -> (store Storable)
				-> location -> (store Storable) -> o.
type	update		(store Storable) -> location -> Storable
				-> (store Storable) -> o.
type	access		(store Storable) -> location -> Storable -> o.

%%% clients aren't supposed to use the following...
%%% but in elp 0.1x the data abstraction stuff isn't available.
type	nextFree	typeExpr -> (store Storable) -> location -> o.
type	mkStore	       (finite_fun location Storable) -> (store Storable).
type	max_loc_of_type	typeExpr -> (finite_fun location Storable) -> int -> o.
type	max_loc_of_type_helper
			typeExpr -> (finite_fun location Storable)
					-> int -> int -> o.
type	max		int -> int -> int -> o.

empty_store (mkStore empty_f_fun).

max N M N :- N >= M.
max N M M :- N < M.

max_loc_of_type T FF N :-
	Negative1 is ~ 1,
	max_loc_of_type_helper T FF Negative1 N.
max_loc_of_type_helper T empty_f_fun M M :- !.
max_loc_of_type_helper T (f_fun_extend (loc T I) SV FF) N M :-
	!,
	max I N MaxOfIandN,
	max_loc_of_type_helper T FF MaxOfIandN M.
max_loc_of_type_helper T (f_fun_extend (loc S I) SV FF) N M :-
	max_loc_of_type_helper T FF N M.

nextFree T (mkStore FF) (loc T Np1) :-
	max_loc_of_type T FF N,
	Np1 is N + 1.

alloc T SV (mkStore FF) L (mkStore (f_fun_extend L SV FF)) :-
	nextFree T (mkStore FF) L.

update (mkStore FF) L SV (mkStore (f_fun_extend L SV FF)).

access (mkStore FF) L SV :- f_fun_apply FF L SV.