%%% Simply Typed Lambda Calculus w/ small-step, allocation semantics
%%% Author: Matthew Fluet (June 2005)
%%% store.elf

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% Stores
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
nil_st         : st.
cons_st        : loc -> val -> st -> st.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% Store WF
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
st_wf          : st -> type.
%mode st_wf +S.
st_wf_nil      : st_wf nil_st.
st_wf_cons_nil : st_wf (cons_st L V nil_st).
st_wf_cons_cons
               : st_wf (cons_st L' V' S') ->
		 loc_lt L' L
		  -> st_wf (cons_st L V (cons_st L' V' S')).
%terminates S (st_wf S).
%worlds () (st_wf _).
%covers st_wf +S.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% Store Lookup
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
st_lookup      : st -> loc -> val -> type.
%mode st_lookup +S +L -V.
st_lookup_hit  : st_lookup (cons_st L V _) L V.
st_lookup_miss : st_lookup S' L V ->
                 loc_lt L L'
                  -> st_lookup (cons_st L' _ S') L V.
%terminates S (st_lookup S _ _).
%worlds () (st_lookup _ _ _).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% Store Alloc
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
st_alloc       : st -> val -> st -> loc -> type.
%mode st_alloc +S1 +V -S2 -L.
st_alloc_nil   : st_alloc nil_st 
		          V'' 
		          (cons_st (mkLoc z_nat) V'' nil_st) 
		          (mkLoc z_nat).
st_alloc_cons  : st_alloc (cons_st (mkLoc N') V' S) 
		          V'' 
		          (cons_st (mkLoc (s_nat N')) V'' (cons_st (mkLoc N') V' S)) 
		          (mkLoc (s_nat N')).
%terminates S (st_alloc S _ _ _).
%worlds () (st_alloc _ _ _ _).
%covers st_alloc +S1 +V -S2 -L.
%total S (st_alloc S _ _ _).