(****************************************************************************************************)
(****************************************** Static Semantics ****************************************)
(****************************************************************************************************)
Require Export syntax.
Require Export configurations.
Require Export auxiliary_functions.

Inductive has_type_b : Gamma_env -> store -> exp_b 
  -> val_ty -> beta_ty_var -> omega_bhvr -> Prop := 
  | has_type_b_inv : forall Gamma x x' n e C beta beta' beta'' m_name T 
    T' tv_list tv_pair v_list beta_list'' default default' default'' H, 
    has_type_b Gamma H (var_exp_b x) (act_val_ty C) (beta) (empty_omega_bhvr) -> 
    m_body C m_name (meth_decl T  m_name tv_list e) -> 
    n < length(tv_list) ->
    tv_pair = nth n tv_list (default) -> 
    x' = snd(tv_pair) -> 
    T' = fst(tv_pair) -> 
    has_type_b Gamma H (var_exp_b x') (T') (beta'') (empty_omega_bhvr) -> 
    x' = nth n v_list (default') -> 
    beta'' = nth n beta_list'' (default'') -> 
    In x' v_list ->
    In beta'' beta_list'' ->
    has_type_b Gamma H (inv_exp_b x beta' m_name v_list) (T) (beta'') (theta_bhvr_omega_bhvr (inv_theta_bhvr beta beta' m_name beta_list''))
  | has_type_b_wait : forall Gamma x T beta beta' H, 
    has_type_b Gamma H (var_exp_b x) (fut_val_ty T) (fut_beta_ty_var beta beta') (empty_omega_bhvr) -> 
    has_type_b Gamma H (wait_exp_b (x)) (T) (beta') (theta_bhvr_omega_bhvr (sync_theta_bhvr (fut_beta_ty_var beta beta')))
  | has_type_b_fut : forall Gamma x T beta beta' beta'' H,
    has_type_b Gamma H (var_exp_b x) (T) (beta'') (empty_omega_bhvr) -> 
    has_type_b Gamma H (new_fut_exp_b beta beta' T x) (fut_val_ty T) (fut_beta_ty_var beta beta') (theta_bhvr_omega_bhvr (flow_theta_bhvr beta'' beta'))
  | has_type_b_new : forall Gamma C st_list m_list AT x T beta beta'' 
    beta_list' beta_list'' n1 n2 default default' default'' v_list omega_bfr 
    s H,
    (AT C) = act_decl C st_list m_list -> 
    n1 < length(st_list) -> 
    (state_decl T s) = nth n1 st_list default -> 
    n2 < length(v_list) -> 
    x = nth n2 v_list default' -> 
    In x v_list -> 
    has_type_b Gamma H (var_exp_b x) (T) (beta'') (empty_omega_bhvr) -> 
    beta'' = nth n2 beta_list'' (default'') -> 
    new_expr_b_hpns_bfr omega_bfr beta_list'' beta_list' ->
    has_type_b Gamma H (new_act_exp_b beta beta_list' C v_list) (act_val_ty C) (beta) (hpns_bfr_omega_bhvr omega_bfr (theta_bhvr_omega_bhvr (new_act_theta_bhvr beta beta_list' C beta)))
  | has_type_b_asgn : forall Gamma s T beta e beta' omega H,
    has_type_b Gamma H (st_read_exp_b s) (T) (beta) (empty_omega_bhvr) ->
    has_type_b Gamma H e (T) (beta') (omega) -> 
    has_type_b Gamma H (st_asgn_exp_b s e) (T) (beta) (hpns_bfr_omega_bhvr omega (theta_bhvr_omega_bhvr (flow_theta_bhvr beta' beta)))
  | has_type_b_let : forall Gamma e' T' beta' omega e'' T'' beta'' omega' x H,
    has_type_b Gamma H e' T' beta' omega -> 
    has_type_b (update Gamma (x) (pair T' (Gamma_snd_beta beta'))) H e'' T'' beta'' omega' -> 
    has_type_b Gamma H (let_exp_b x e' e'') T'' beta'' (hpns_bfr_omega_bhvr omega omega')
  | has_type_b_read : forall Gamma s v S T beta H n C beta_list' default_S 
    default_b beta',
    In (act_record beta beta_list' C S) H ->
    n < length(S) ->
    (state_decl T s, v) = nth n S default_S ->
    val_b v ->
    beta' = nth n beta_list' default_b ->
    has_type_b Gamma H (st_read_exp_b s) T beta' empty_omega_bhvr
  | has_type_b_var : forall Gamma x T beta H,
    Gamma x = Some(pair T (Gamma_snd_beta beta)) ->
    has_type_b Gamma H (var_exp_b x) T beta empty_omega_bhvr
  | has_type_b_null : forall Gamma T H, 
    has_type_b Gamma H (null_exp_b) T null_beta_ty_var empty_omega_bhvr
  | has_type_b_ctxt : forall Gamma e T beta beta' omega' omega delta l 
    C m_name Delta Delta' H, 
    has_type_b Gamma H (loc_exp_b l) (act_val_ty C) beta empty_omega_bhvr ->
    delta = delta_decl beta C m_name ->
    Delta = add_Delta delta Delta' ->
    has_type_b Gamma H e T beta' omega' -> 
    omega = (ctxt_omega_bhvr omega' delta) ->
    has_type_b Gamma H (ctxt_exp_b e l C m_name) T beta' omega
  | has_type_b_resl : forall Gamma e T beta omega l H, 
    has_type_b Gamma H e T beta omega -> 
    has_type_b Gamma H (resl_exp_b l e) T beta omega
  | has_type_b_loc_act : forall Gamma l S beta beta_list' C T H ln default, 
    l = Id ln ->
    ln < length(H) ->
    act_record beta beta_list' C S = nth ln H default->
    T = act_val_ty C ->
    has_type_b Gamma H (loc_exp_b l) T beta empty_omega_bhvr
  | has_type_b_loc_fut : forall Gamma l beta beta' v T H ln default, 
    l = Id ln -> 
    ln < length(H) -> 
    fut_record beta beta' T v = nth ln H default ->
    has_type_b Gamma H (loc_exp_b l) T (fut_beta_ty_var beta beta') empty_omega_bhvr
  | has_type_b_unresl : forall Gamma T H,
    has_type_b Gamma H unresl_exp_b T null_beta_ty_var empty_omega_bhvr.

Inductive env_weakening : Gamma_env -> Gamma_env -> Prop :=
  | environment_weakening : forall Gamma Gamma', 
    (forall H e T beta omega, 
    has_type_b Gamma H e T beta omega -> 
    has_type_b Gamma' H e T beta omega) -> 
    env_weakening Gamma Gamma'.