% $Id: store.mod,v 1.2 2007/05/10 05:51:45 leavens Exp $
%
% Stores, adapted from David 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.

  accumulate finite_function.
  
  %%% clients aren't supposed to use the following
  local mkStore        (finite_fun int Storable) -> (store Storable).
  local nextFree       (store Storable) -> int -> o.
  local max_loc        (finite_fun int Storable) -> int -> o.
  local max_loc_helper (finite_fun int Storable) -> int -> int -> o.
  local max            int -> int -> int -> o.
  local show_store_help Storable -> (finite_fun int Storable) -> int
                        -> list Storable -> list Storable -> o.

  %% ``initial_store S'' succeeds if S is an initial store.
  initial_store (mkStore empty_f_fun).

  %% ``show_store Default S L'' succeeds if S is represented by the list L,
  %% which has all locations from 0 to the max location defined,
  %% and any locations not assigned have Default as their value.
  show_store Default (mkStore FF) L :-
       max_loc FF N,
       show_store_help Default FF N nil L.

  show_store_help Default FF N L L :- N < 0.
  show_store_help Default FF N L L2 :- N >= 0,
       access (mkStore FF) N VN,
       !,
       Nminus1 is N - 1,
       show_store_help Default FF Nminus1 (VN::L) L2.
  show_store_help Default FF N L L2 :- N >= 0,
       Nminus1 is N - 1,
       show_store_help Default FF Nminus1 (Default::L) L2.
  
  %% ``max N M I'' succeeds if I is the maximum of M and N.
  max N M N :- N >= M.
  max N M M :- N < M.
  
  %% ``max_loc FF N'' succeeds if N is the largest location bound in FF.
  max_loc FF N :-
        Negative1 is ~ 1,
        max_loc_helper FF Negative1 N.
  max_loc_helper empty_f_fun M M :- !.
  max_loc_helper (f_fun_extend I SV FF) N M :-
        !,
        max I N MaxOfIandN,
        max_loc_helper FF MaxOfIandN M.
  max_loc_helper (f_fun_extend I SV FF) N M :-
        max_loc_helper FF N M.
  
  %% ``nextFree S N'' succeeds if N is the next free location in FF.
  nextFree (mkStore FF) Np1 :-
        max_loc FF N,
        Np1 is N + 1.
  
  %% ``alloc SV S L S2'' succeeds if S2 is the store that results from
  %% extending S by assigning SV to location L, where L was the next free
  %% location in S.
  alloc SV (mkStore FF) L (mkStore (f_fun_extend L SV FF)) :-
        nextFree (mkStore FF) L.
  
  %% ``update S L SV S2'' succeeds if S2 is the store that results from
  %% extending S by assigning SV to location L.  L doesn't have to have had
  %% a value previously.
  update (mkStore FF) L SV (mkStore (f_fun_extend L SV FF)).
  
  %% ``access S L SV'' succeeds if the latest assignment of L recorded in S
  %% was for the value SV.
  access (mkStore FF) L SV :- f_fun_apply FF L SV.

end