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

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% Store Typings
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
nil_sttp       : sttp.
cons_sttp      : loc -> tp -> sttp -> sttp.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% Store Typings WF
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
sttp_wf        : sttp -> type.
%mode sttp_wf +ST.
sttp_wf_nil    : sttp_wf nil_sttp.
sttp_wf_cons_nil 
               : sttp_wf (cons_sttp L T nil_sttp).
sttp_wf_cons_cons
               : sttp_wf (cons_sttp L' T' ST'') ->
		 loc_lt L' L
		  -> sttp_wf (cons_sttp L T (cons_sttp L' T' ST'')).
%terminates ST (sttp_wf ST).
%worlds () (sttp_wf _).
%covers sttp_wf +ST.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% Store Typing Lookup
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
sttp_lookup    : sttp -> loc -> tp -> type.
%mode sttp_lookup +ST +L -T.
sttp_lookup_hit
               : sttp_lookup (cons_sttp L T _) L T.
sttp_lookup_miss 
               : sttp_lookup ST' L T ->
                 loc_lt L L'
		  -> sttp_lookup (cons_sttp L' _ ST') L T.
%terminates ST (sttp_lookup ST _ _).
%worlds () (sttp_lookup _ _ _).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% Store Typing Alloc
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
sttp_alloc     : sttp -> tp -> sttp -> loc -> type.
%mode sttp_alloc +ST1 +V -ST2 -L.
sttp_alloc_nil : sttp_alloc nil_sttp 
		            T'' 
		            (cons_sttp (mkLoc z_nat) T'' nil_sttp) 
		            (mkLoc z_nat).
sttp_alloc_cons 
               : sttp_alloc (cons_sttp (mkLoc N) T ST) 
		            T'' 
		            (cons_sttp (mkLoc (s_nat N)) T'' (cons_sttp (mkLoc N) T ST)) 
		            (mkLoc (s_nat N)).
%terminates ST (sttp_alloc ST _ _ _).
%worlds () (sttp_alloc _ _ _ _).
%covers sttp_alloc +ST1 +V -ST2 -L.
%total ST (sttp_alloc ST _ _ _).

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% Store Typing Extend
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
sttp_extend    : sttp -> sttp -> type.
%mode sttp_extend +ST1 +ST2.
sttp_extend_nil
               : sttp_extend nil_sttp ST2.
sttp_extend_cons_hit
               : sttp_extend ST1' ST2'
		  -> sttp_extend (cons_sttp L T ST1') 
		                 (cons_sttp L T ST2').
sttp_extend_cons_miss
               : sttp_extend (cons_sttp L1 T1 ST1') ST2' ->
		 loc_lt L1 L2
                  -> sttp_extend (cons_sttp L1 T1 ST1') 
                                 (cons_sttp L2 T2 ST2').
%terminates ST2 (sttp_extend _ ST2).
%worlds () (sttp_extend _ _).