%{
   A formalization of Chapter 13 from _Types and Programming Languages_:
   the simply typed lambda-calculus with references. Only basic definitions
   are included here.
   
   Author: Brian E. Aydemir (baydemir [at] cis.upenn.edu).
}%



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% Types.

tp : type.              %name tp T.

=>   : tp -> tp -> tp.  %% type of functions.
unit : tp.              %% unit type.
ref  : tp -> tp.        %% type of reference cells.

%name tp T.
%infix right 5 =>.



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% Labels (isomorphic to the natural numbers).

label : type.   %name label L.

lbl : nat -> label.



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% Expressions.

exp : type.                             %name exp E.

@     : exp -> exp -> exp.              %% application.
lam   : tp -> (exp -> exp) -> exp.      %% lambda abstraction.
dot   : exp.                            %% constant of type unit.
alloc : exp -> exp.                     %% reference cell creation (ref).
deref : exp -> exp.                     %% dereference a reference cell (!).
gets  : exp -> exp -> exp.              %% assignment (:=).
loc   : label -> exp.                   %% locations.

%name exp E.
%infix left 9999 @.
%prefix 9000 deref.
%infix none 8000 gets.



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% Values.

value : exp -> type.
%name value V.
%mode value +E.

v_lam : value (lam _ _).
v_dot : value dot.
v_loc : value (loc _).

%terminates {} (value _).



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% Store typings.
%%% Represented by length-indexed lists.

%{
   Store typings are represented by length-indexed lists, starting from zero
   (z). Thus in the list "store_cons T1 (store_cons T2 store_nil)" index z
   corresponds to T1 and index (s z) corresponds to T2.
}%

store : type.    %name store S.

store_nil  : store.
store_cons : tp -> store -> store.



%%% Compute the length of a store typing.

length_store : store -> nat -> type.
%mode length_store +S -N.

length_store_nil : length_store store_nil z.

length_store_cons :
   length_store (store_cons _ S) (s N)
   <- length_store S N.

%worlds () (length_store _ _).
%total S (length_store S _).
%unique length_store +S -1N.



%%% Look up a label in a store typing.

find_in_store : label -> store -> tp -> type.
%mode find_in_store +L +S -T.

find_in_store_yes :
   find_in_store (lbl z) (store_cons T _) T.
   
find_in_store_no :
   find_in_store (lbl (s N)) (store_cons _ S) T
   <- find_in_store (lbl N) S T.

%worlds () (find_in_store _ _ _).
%terminates S (find_in_store _ S _).
%unique find_in_store +L +S -1T.



%%% (store_extends S S') holds if S' extends S.

store_extends : store -> store -> type.
%mode store_extends +S1 +S2.

store_extends_base :
   store_extends store_nil S.

store_extends_ind :
   store_extends (store_cons T S1) (store_cons T S2)
   <- store_extends S1 S2.
   
%terminates S (store_extends S _).



%%% Append a type to a store typing, returning the new store typing.

append_store : store -> tp -> store -> type.
%mode append_store +S1 +T -S2.

append_store_nil :
   append_store store_nil T (store_cons T store_nil).
   
append_store_cons :
   append_store (store_cons T1 S) T2 (store_cons T1 S')
   <- append_store S T2 S'.
   
%worlds () (append_store _ _ _).
%total S (append_store S _ _).
%unique append_store +S1 +E -1S2.



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% Typing relation.

%{
   Typing assumptions for variables are represented by the var judgment. We
   use this auxiliary judgment since assumptions in the typing environment
   do not mention store typings, and hence we shouldn't confuse them with
   typing judgments.
}%

of : store -> exp -> tp -> type.
%name of Q.
%mode of +S +E *T.

var : exp -> tp -> type.
%name var V.
%mode var +E *T.
%freeze var.

t_var :
   of S E T
   <- var E T.

t_abs :
   of S (lam T1 E) (T1 => T2)
   <- ({x:exp} var x T1 -> of S (E x) T2).
   
t_app :
   of S (E1 @ E2) T2
   <- of S E1 (T1 => T2)
   <- of S E2 T1.
   
t_unit :
   of S dot unit.

t_loc :
   of S (loc L) (ref T)
   <- find_in_store L S T.

t_ref :
   of S (alloc E) (ref T)
   <- of S E T.
   
t_deref :
   of S (deref E) T
   <- of S E (ref T).

t_assign :
   of S (E1 gets E2) unit
   <- of S E1 (ref T)
   <- of S E2 T.

%terminates E (var E _).
%terminates E (of _ E _).



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% Heaps.
%%% Represented by length-indexed lists (similar to store typings).

heap : type.     %name heap H.

heap_nil  : heap.
heap_cons : exp -> heap -> heap.



%%% Compute the length of a heap.

length_heap : heap -> nat -> type.
%mode length_heap +H -N.

length_heap_nil : length_heap heap_nil z.

length_heap_cons :
   length_heap (heap_cons _ H) (s N)
   <- length_heap H N.

%worlds () (length_heap _ _).
%total H (length_heap H _).
%unique length_heap +H -1N.



%%% Look up a label in a heap.

find_in_heap : label -> heap -> exp -> type.
%mode find_in_heap +L +H -E.

find_in_heap_yes :
   find_in_heap (lbl z) (heap_cons E _) E.
   
find_in_heap_no :
   find_in_heap (lbl (s N)) (heap_cons _ H) E
   <- find_in_heap (lbl N) H E.

%worlds () (find_in_heap _ _ _).
%terminates H (find_in_heap _ H _).
%unique find_in_heap +L +H -1E.



%%% Replace the binding for a label in a heap.

replace_in_heap : heap -> label -> exp -> heap -> type.
%mode replace_in_heap +H1 +L +E -H2.

replace_in_heap_yes :
   replace_in_heap (heap_cons E1 H) (lbl z) E2 (heap_cons E2 H).

replace_in_heap_no :
   replace_in_heap (heap_cons E1 H) (lbl (s N)) E2 (heap_cons E1 H')
   <- replace_in_heap H (lbl N) E2 H'.

%worlds () (replace_in_heap _ _ _ _).
%terminates H (replace_in_heap H _ _ _).
%unique replace_in_heap +H1 +L +E -1H2.



%%% Append an expression to a heap, returning the new heap.

append_heap : heap -> exp -> heap -> type.
%mode append_heap +H1 +E -H2.

append_heap_nil :
   append_heap heap_nil E (heap_cons E heap_nil).
   
append_heap_cons :
   append_heap (heap_cons E1 H) E2 (heap_cons E1 H')
   <- append_heap H E2 H'.
   
%worlds () (append_heap _ _ _).
%total H (append_heap H _ _).
%unique append_heap +H1 +E -1H2.



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% Well-typed heaps (with respect to a store typing).



%%% This auxiliary judgments walks down a store typing and heap (in order to
%%% ensure that they have the same domain) and uses the first store typing
%%% to check that expressions in the heap are well-typed.

check_wt : store -> store -> heap -> type.
%mode check_wt +S1 +S2 +H.

check_wt_nil :
   check_wt _ store_nil heap_nil.
   
check_wt_cons :
   check_wt S1 (store_cons T S2) (heap_cons E H)
   <- of S1 E T
   <- check_wt S1 S2 H.
   
%terminates H (check_wt _ _ H).



%%% (wt_heap S H) holds if H is well-typed with respect to S.

wt_heap : store -> heap -> type.
%mode wt_heap +S +H.

wt_heap_def :
   wt_heap S H
   <- check_wt S S H.
   
%terminates {} (wt_heap _ _).



%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% Evaluation relation.

step : heap -> exp -> heap -> exp -> type.
%name step S.
%mode step +H1 +E1 -H2 -E2.



%%% Congruence rules.

e_app1 :
   step H (E1 @ E2) H' (E1' @ E2)
   <- step H E1 H' E1'.

e_app2 :
   step H (E1 @ E2) H' (E1 @ E2')
   <- value E1
   <- step H E2 H' E2'.

e_alloc :
   step H (alloc E) H' (alloc E')
   <- step H E H' E'.

e_deref :
   step H (deref E) H' (deref E')
   <- step H E H' E'.

e_gets1 :
   step H (E1 gets E2) H' (E1' gets E2)
   <- step H E1 H' E1'.

e_gets2 :
   step H (E1 gets E2) H' (E1 gets E2')
   <- value E1
   <- step H E2 H' E2'.



%%% Computation rules.

e_appabs :
   step H (lam _ E1 @ E2) H (E1 E2)
   <- value E2.

e_allocVal :
   step H (alloc E) H' (loc (lbl N'))
   <- value E
   <- append_heap H E H'
   <- length_heap H N'.

e_derefVal :
   step H (deref (loc L)) H E
   <- find_in_heap L H E.

e_getsVal :
   step H ((loc L) gets E) H' dot
   <- value E
   <- replace_in_heap H L E H'.

%terminates E (step _ E _ _).