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

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
%%% Expressions
%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
loc_e          : loc -> exp.
lam_e          : tp -> (exp -> exp) -> exp.
app_e          : exp -> exp -> exp.
unit_e         : exp.
letunit_e      : exp -> exp -> exp.
pair_e         : exp -> exp -> exp.
letpair_e      : exp -> (exp -> exp -> exp) -> exp.

%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
exp_irred      : exp -> type.
%mode exp_irred +E.
exp_irred_loc  : exp_irred (loc_e _).
%terminates {} (exp_irred _).
%worlds () (exp_irred _).