(****************************************************************************************************)
(***************************************** Dynamic Semantics ****************************************)
(****************************************************************************************************)
Require Export syntax.
Require Export configurations.
Require Export auxiliary_functions.
Require Export static_semantics.

Inductive step_dyn : glbl_cnfg -> glbl_cnfg -> Prop := 
  | step_dyn_fut : forall l' H' H beta beta' T x v Q Phi G l V,
    V x = Some(v) ->
    val_b v ->
    l' = Id (length(H)) ->
    H' = H ++ (fut_record beta beta' (fut_val_ty T) v) :: nil ->
    step_dyn 
    (add_glbl_cnfg (act_cnfg ((new_fut_exp_b beta beta' T x) :: Q) Phi l) G (V, H)) 
    (add_glbl_cnfg (act_cnfg ((loc_exp_b l') :: Q) Phi l) G (V, H'))
  | step_dyn_wait : forall H l' ln' beta beta' T v Phi' Phi Q G'
    l default x_l' V, 
    lookup_var_loc V x_l' (loc_exp_b l') ->
    l' = Id ln' ->
    ln' < length(H) ->
    fut_record beta beta' T v = nth ln' H default -> 
    val_b v -> 
    ~(v = unresl_exp_b) ->
    Phi' = (sync_theta_bhvr (fut_beta_ty_var beta beta')) :: Phi ->
    step_dyn 
    (add_glbl_cnfg (act_cnfg ((wait_exp_b x_l') :: Q) Phi l) G' (V, H))
    (add_glbl_cnfg (act_cnfg (v :: Q) Phi' l) G' (V, H))
  | step_dyn_read : forall H l B B_list C S s v Q  Phi G n default
    T_tmp V, 
    In (act_record B B_list C S) H ->
    n < length(S) ->
    (state_decl T_tmp s, v) = nth n S default ->
    val_b v ->
    step_dyn 
    (add_glbl_cnfg (act_cnfg ((st_read_exp_b s) :: Q) Phi l) G (V, H))
    (add_glbl_cnfg (act_cnfg (v :: Q) Phi l) G (V, H))
  | step_dyn_asgn : forall H' H s v beta''' Phi' Phi beta'' Q G l ln T 
    Gamma' V sn,
    s = Id sn ->
    l = Id ln ->
    H' = replace_state ln sn ((state_decl T s), v) H -> 
    val_b v ->
    has_type_b Gamma' H (st_read_exp_b s) T beta'' empty_omega_bhvr ->
    beta''' = staticize v H' ->
    Phi' = (flow_theta_bhvr beta''' beta'') :: Phi ->
    step_dyn 
    (add_glbl_cnfg (act_cnfg ((st_asgn_exp_b s v) :: Q) Phi l) G (V, H)) 
    (add_glbl_cnfg (act_cnfg (v :: Q) Phi' l) G (V, H'))
  | step_dyn_let : forall x v e Phi l H Q G V, 
    val_b v ->
    V x = Some(v) ->
    step_dyn 
    (add_glbl_cnfg (act_cnfg ((let_exp_b x v e) :: Q) Phi l) G (V, H)) 
    (add_glbl_cnfg (act_cnfg ((e) :: Q) Phi l) G (V, H))
  | step_dyn_ctxt : forall v l_ctxt C_ctxt m_ctxt Q Phi l G H, 
    val_b v -> 
    step_dyn 
    (add_glbl_cnfg (act_cnfg ((ctxt_exp_b v l_ctxt C_ctxt m_ctxt) :: Q) Phi l) G H) 
    (add_glbl_cnfg (act_cnfg ((v) :: Q) Phi l) G H)
  | step_dyn_act : forall Q beta beta_list' C l' G Phi l H st_list H'
    AT m_list S beta_list'' beta_list''' Phi' Phi_tmp x_list v_list V G',
    v_list = lookup_varlist_val V x_list ->
    l' = Id (length(H)) ->
    AT C = act_decl C st_list m_list -> 
    beta_list'' = new_act_betalist 1 C st_list ->
    S = new_act_st_map st_list v_list -> 
    H' = H ++ (act_record (act_beta_ty_var C) beta_list' C S) :: nil ->
    beta_list''' = staticize_list v_list H' ->
    Phi_tmp = new_act_Phi Phi beta_list''' beta_list'' ->
    Phi' = (new_act_theta_bhvr beta beta_list' C beta) :: Phi_tmp -> 
    G' = act_glbl_cnfg G l' (V, H') ->
    step_dyn 
    (add_glbl_cnfg (act_cnfg ((new_act_exp_b beta beta_list' C x_list) :: Q) Phi l) G (V, H))
    (add_glbl_cnfg (act_cnfg ((loc_exp_b l') :: Q) Phi' l) G' (V, H'))
  | step_dyn_inv : forall Q x_l' beta m_name  l'' G Phi l H Phi' l' 
    e tv_list C beta_list'' beta' S  beta''' beta'''' theta 
    beta_list_tmp v_list H' e'' e' T' alpha_list Delta G' Delta' 
    beta_list default_H ln' x_list V,
    lookup_var_loc V x_l' (loc_exp_b l')->
    l' = Id ln' ->
    ln' < length(H) ->
    (act_record beta' beta_list'' C S) = nth ln' H default_H ->
    m_body C m_name (meth_decl T'  m_name tv_list e) ->
    alpha_list = label e ->
    Delta' = d2s Delta H ->
    beta_list = refresh Delta' alpha_list H C 0 m_name->
    v_list = lookup_varlist_val V x_list ->
    e' = inv_e_replace e beta_list alpha_list ->
    l'' = Id (length(H)) ->
    beta''' = inv_fresh_beta C 0 beta_list ->
    beta'''' = inv_fresh_beta C 0 (beta''' :: beta_list) ->
    beta_list_tmp = staticize_list v_list H' ->
    theta = inv_theta_bhvr beta' beta m_name beta_list_tmp ->
    e'' = resl_exp_b l'' (ctxt_exp_b e' l' C m_name) ->
    H' = H ++ (fut_record beta''' beta'''' T' unresl_exp_b) :: nil ->
    Phi' = theta :: Phi ->
    G' = inv_glbl_cnfg G l' e'' (V, H') ->
    step_dyn 
    (add_glbl_cnfg (act_cnfg ((inv_exp_b x_l' beta m_name x_list) :: Q) Phi l) G (V, H)) 
    (add_glbl_cnfg (act_cnfg ((loc_exp_b l'') :: Q) Phi' l) G' (V, H'))
  | step_dyn_resl : forall H' H l' rec' beta beta' T v Phi' Phi Q G l 
    ln' V, 
    rec' = fut_record beta beta' T v -> 
    val_b v ->
    l' = Id ln' ->
    H' = replace ln' rec' H ->
    Phi' = (resl_theta_bhvr beta) :: Phi -> 
    step_dyn 
    (add_glbl_cnfg (act_cnfg ((resl_exp_b l' v) :: Q) Phi l) G (V, H)) 
    (add_glbl_cnfg (act_cnfg (v :: Q) Phi' l) G (V, H'))
  | step_dyn_asgn_congr : forall e Q Phi l G H e' Phi' G' H' s,
    ~ (val_b e) ->
    step_dyn 
    (add_glbl_cnfg (act_cnfg ((e) :: Q) Phi l) G H)
    (add_glbl_cnfg (act_cnfg ((e') :: Q) Phi' l) G' H')-> 
    step_dyn 
    (add_glbl_cnfg (act_cnfg ((st_asgn_exp_b s e) :: Q) Phi l) G H) 
    (add_glbl_cnfg (act_cnfg ((st_asgn_exp_b s e') :: Q) Phi' l) G' H') 
  | step_dyn_let_congr : forall x e' e Phi l H Q G Phi' G' H' e'',
    ~ (val_b e') ->
    step_dyn 
    (add_glbl_cnfg (act_cnfg ((e') :: Q) Phi l) G H) 
    (add_glbl_cnfg (act_cnfg ((e'') :: Q) Phi' l) G' H')-> 
     step_dyn 
    (add_glbl_cnfg (act_cnfg ((let_exp_b x e' e) :: Q) Phi l) G H) 
    (add_glbl_cnfg (act_cnfg ((let_exp_b x e'' e) :: Q) Phi' l) G' H')
  | step_dyn_ctxt_congr : forall e' e'' Phi l H Q G l_ctxt C_ctxt 
    m_ctxt Phi' G' H', 
    ~ (val_b e') ->
    step_dyn 
    (add_glbl_cnfg (act_cnfg ((e') :: Q) Phi l) G H) 
    (add_glbl_cnfg (act_cnfg ((e'') :: Q) Phi' l) G' H') -> 
    step_dyn
    (add_glbl_cnfg (act_cnfg ((ctxt_exp_b e' l_ctxt C_ctxt m_ctxt) :: Q) Phi l) G H)
    (add_glbl_cnfg (act_cnfg ((ctxt_exp_b e'' l_ctxt C_ctxt m_ctxt) :: Q) Phi' l) G' H') 
  | step_dyn_resl_congr :  forall e' e'' Phi l VH Q G l' Phi' G' VH', 
    ~ (val_b e') ->
    step_dyn 
    (add_glbl_cnfg (act_cnfg ((e') :: Q) Phi l) G VH) 
    (add_glbl_cnfg (act_cnfg ((e'') :: Q) Phi' l) G' VH') -> 
    step_dyn
    (add_glbl_cnfg (act_cnfg ((resl_exp_b l' e') :: Q) Phi l) G VH) 
    (add_glbl_cnfg (act_cnfg ((resl_exp_b l' e'') :: Q) Phi' l) G' VH')
  | step_dyn_XCPT_var : forall x Phi l VH Q G, 
    step_dyn
    (add_glbl_cnfg (act_cnfg ((var_exp_b x) :: Q) Phi l) G VH)
    (add_glbl_cnfg (act_cnfg ((null_exp_b) :: Q) Phi l) G VH)
  | step_dyn_loc_dequeue : forall l'' Phi l VH Q G, 
    step_dyn 
    (add_glbl_cnfg (act_cnfg ((loc_exp_b l'') :: Q) Phi l) G VH)
    (add_glbl_cnfg (act_cnfg Q Phi l) G VH)
  | step_dyn_null_dequeue : forall Phi l VH Q G, 
    step_dyn 
    (add_glbl_cnfg (act_cnfg ((null_exp_b) :: Q) Phi l) G VH)
    (add_glbl_cnfg (act_cnfg Q Phi l) G VH)
  | step_dyn_unresl_dequeue : forall Phi l VH Q G, 
    step_dyn 
    (add_glbl_cnfg (act_cnfg (unresl_exp_b :: Q) Phi l) G VH)
    (add_glbl_cnfg (act_cnfg Q Phi l) G VH)
  | step_dyn_empty : forall Phi l VH G G', 
    step_dyn G G' -> 
    step_dyn 
    (add_glbl_cnfg (act_cnfg nil Phi l) G VH)
    (add_glbl_cnfg (act_cnfg nil Phi l) G' VH).

Inductive wellformed_V : var_val_map -> store -> exp_b -> Prop :=
  | wellformed_V_inv : forall V H x_l' l' ln' beta x_list beta' 
    beta_list'' C S default_H T m_name tv_list e,
    lookup_var_loc V x_l' (loc_exp_b l')->
    l' = Id ln' ->
    ln' < length(H) ->
    m_body C m_name (meth_decl T m_name tv_list e) -> 
    (act_record beta' beta_list'' C S) = nth ln' H default_H -> 
    wellformed_V V H (inv_exp_b x_l' beta m_name x_list)
  | wellformed_V_act : forall V H beta beta_list' C x_list v_list,
    v_list = lookup_varlist_val V x_list ->
    wellformed_V V H (new_act_exp_b beta beta_list' C x_list)
  | wellformed_V_fut : forall V H beta beta' T x v,
    V x = Some(v) ->
    val_b v ->
    wellformed_V V H (new_fut_exp_b beta beta' T x)
  | wellformed_V_wait : forall V H x_l' l' ln' beta beta' T v default,
    lookup_var_loc V x_l' (loc_exp_b l') ->
    l' = Id ln' ->
    ln' < length(H) ->
    fut_record beta beta' T v = nth ln' H default -> 
    val_b v -> 
    ~(v = unresl_exp_b) ->
    wellformed_V V H (wait_exp_b x_l')
  | wellformed_V_let : forall V H x e' e'',
    wellformed_V V H e' -> 
    wellformed_V V H e'' ->
    (val_b e' -> V x = Some(e')) ->
    wellformed_V V H (let_exp_b x e' e'')
  | wellformed_V_asgn : forall V H s e,
    wellformed_V V H e ->
    wellformed_V V H (st_asgn_exp_b s e)
  | wellformed_V_read : forall V H s,
    wellformed_V V H (st_read_exp_b s)
  | wellformed_V_var : forall V H x,
    wellformed_V V H (var_exp_b x)
  | wellformed_V_null : forall V H,
    wellformed_V V H (null_exp_b)
  | wellformed_V_loc : forall V H l,
    wellformed_V V H (loc_exp_b l)
  | wellformed_V_ctxt : forall V H e l_ctxt C_ctxt m_ctxt,
    wellformed_V V H e ->
    wellformed_V V H (ctxt_exp_b e l_ctxt C_ctxt m_ctxt)
  | wellformed_V_resl : forall V H l' e,
    wellformed_V V H e ->
    wellformed_V V H (resl_exp_b l' e).

Inductive wellformed_GVH : Gamma_env -> var_val_map -> store -> exp_b 
  -> Prop :=
  | wellformed_GVH_inv : forall V H x_l' l' ln' beta x_list beta' 
    beta_list'' C S default_H T m_name tv_list e Gamma,
    lookup_var_loc V x_l' (loc_exp_b l')->
    l' = Id ln' ->
    ln' < length(H) ->
    m_body C m_name (meth_decl T m_name tv_list e) -> 
    (act_record beta' beta_list'' C S) = nth ln' H default_H -> 
    wellformed_GVH Gamma V H (inv_exp_b x_l' beta m_name x_list)
  | wellformed_GVH_act : forall V H beta beta_list' C x_list v_list 
    Gamma,
    v_list = lookup_varlist_val V x_list ->
    wellformed_GVH Gamma V H (new_act_exp_b beta beta_list' C x_list)
  | wellformed_GVH_fut : forall V H beta beta' T x v Gamma,
    V x = Some(v) ->
    val_b v ->
    wellformed_GVH Gamma V H (new_fut_exp_b beta beta' T x)
  | wellformed_GVH_wait : forall V H x_l' l' ln' beta beta' T v 
    default beta'' Gamma,
    lookup_var_loc V x_l' (loc_exp_b l') ->
    l' = Id ln' ->
    ln' < length(H) ->
    fut_record beta beta' T v = nth ln' H default -> 
    val_b v -> 
    ~(v = unresl_exp_b) ->
    (forall l' l'' ln' ln'' beta beta' beta'' beta''' default default'
    T v T' v', 
    lookup_var_loc V x_l' (loc_exp_b l') /\ 
    lookup_var_loc V x_l' (loc_exp_b l'') /\ 
    l' = Id ln' /\ 
    l'' = Id ln'' /\
    fut_record beta beta' T v = nth ln' H default /\ 
    fut_record beta'' beta''' T' v' = nth ln'' H default' -> 
    v = v') ->
    (forall T beta beta',
    has_type_b Gamma H (var_exp_b x_l') (fut_val_ty T) 
    (fut_beta_ty_var beta beta') empty_omega_bhvr -> 
    has_type_b Gamma H v T beta'' empty_omega_bhvr ) ->
    wellformed_GVH Gamma V H (wait_exp_b x_l')
  | wellformed_GVH_let : forall V H x e' e'' Gamma,
    wellformed_GVH Gamma V H e' -> 
    wellformed_GVH Gamma V H e'' ->
    (forall T' beta' omega,
    has_type_b Gamma H e' T' beta' omega -> 
    env_weakening Gamma (update Gamma x (T', Gamma_snd_beta beta'))) ->
    (val_b e' -> V x = Some(e')) ->
    (forall Gamma' T beta, 
    env_weakening Gamma Gamma' -> 
    env_weakening 
    (update Gamma x (T, Gamma_snd_beta beta))
    (update Gamma' x (T, Gamma_snd_beta beta))) ->
    wellformed_GVH Gamma V H (let_exp_b x e' e'')
  | wellformed_GVH_asgn : forall V H s e Gamma,
    wellformed_GVH Gamma V H e ->
    wellformed_GVH Gamma V H (st_asgn_exp_b s e)
  | wellformed_GVH_read : forall V H s beta' Gamma,
    (forall beta beta_list' C S n T v default_S, 
    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) /\ (has_type_b empty H v T beta' empty_omega_bhvr)) ->
    (forall beta beta_list' C S n T v default_S
    beta' beta_list'' C' S' n' T' v' default_S',
    In (act_record beta beta_list' C S) H /\ 
    n < length S /\
    (state_decl T s, v) = nth n S default_S /\ 
    In (act_record beta' beta_list'' C' S') H /\ 
    n' < length S' /\
    (state_decl T' s, v') = nth n' S' default_S' ->
    (S = S') /\ (T = T') /\ (v = v') )->
    wellformed_GVH Gamma V H (st_read_exp_b s)
  | wellformed_GVH_var : forall V H x Gamma,
    wellformed_GVH Gamma V H (var_exp_b x)
  | wellformed_GVH_null : forall V H Gamma,
    wellformed_GVH Gamma V H (null_exp_b)
  | wellformed_GVH_loc : forall V H l Gamma,
    wellformed_GVH Gamma V H (loc_exp_b l)
  | wellformed_GVH_ctxt : forall V H e l_ctxt C_ctxt m_ctxt Gamma,
    wellformed_GVH Gamma V H e ->
    wellformed_GVH Gamma V H (ctxt_exp_b e l_ctxt C_ctxt m_ctxt)
  | wellformed_GVH_resl : forall V H l' e Gamma,
    wellformed_GVH Gamma V H e ->
    wellformed_GVH Gamma V H (resl_exp_b l' e).