(****************************************************************************************************)
(***************************************** Auxiliary Functions **************************************)
(****************************************************************************************************)
Require Export syntax.
Require Export configurations.

(* The function m_body is based on Panini's proc_body. *)

Inductive m_body1 : act_id -> meth_id -> meth -> Prop :=
  | meth_body1 : forall ATbl C st_list T m_name tv_list e m_list,
    ATbl C = Some (act_decl C st_list m_list) -> 
    In (meth_decl T m_name tv_list e) m_list ->
    m_body1 C m_name (meth_decl T m_name tv_list e).

Inductive m_body : act_id -> meth_id -> meth -> Prop :=
  | meth_body : forall C m_name T tv_list e ,
    m_body1 C m_name (meth_decl T m_name tv_list e) ->
    (forall m_name C1 C2 T1 T2 tv_list1 tv_list2 e1 e2,
    m_body1 C1 m_name (meth_decl T1 m_name tv_list1 e1) -> 
    m_body1 C2 m_name (meth_decl T2 m_name tv_list2 e2) -> 
    (C1 = C2 /\ T1 = T2 /\ tv_list1 = tv_list2 /\ e1 = e2)) ->
    m_body C m_name (meth_decl T m_name tv_list e).

Fixpoint new_expr_hpns_bfr (bfr:sigma_bhvr) (l1:list alpha_ty_var) (l2:list alpha_ty_var) : Prop :=
    match (bfr, l1, l2) with
      | (empty_sigma_bhvr, nil, nil) => True
      | (hpns_bfr_sigma_bhvr (eta_bhvr_sigma_bhvr (flow_eta_bhvr alpha_ty_varb'' alpha_ty_varb') ) moreb, alpha'' :: more1, alpha' :: more2) 
        => (alpha_ty_varb'' = alpha'') /\ (alpha_ty_varb' = alpha') /\ (new_expr_hpns_bfr moreb more1 more2)
      | (_, _, _) => False
    end.

Fixpoint new_expr_b_hpns_bfr (bfr:omega_bhvr) (l1:list beta_ty_var) (l2:list beta_ty_var) : Prop :=
  match (bfr, l1, l2) with
    | (empty_omega_bhvr, nil, nil) => True
    | (hpns_bfr_omega_bhvr (theta_bhvr_omega_bhvr (flow_theta_bhvr beta_ty_var_b'' beta_ty_var_b') ) moreb, beta'' :: more1, beta' :: more2) 
      => (beta_ty_var_b'' = beta'') /\ (beta_ty_var_b' = beta') /\ (new_expr_b_hpns_bfr moreb more1 more2)
    | (_, _, _) => False
  end.

(*replace is from Software Foundations.*)
Fixpoint replace {A:Type} (n:nat) (x:A) (l:list A) : list A :=
  match l with
  | nil    => nil
  | h :: t =>
    match n with
    | O    => x :: t
    | S n' => h :: replace n' x t
    end
  end.

Fixpoint replace_state (ln:nat) (sn:nat) (state_val:state * exp_b) 
  (H:store) : store :=
  match H with 
    | nil => nil
    | (act_record beta beta_list' C s) :: H' => 
      match ln with
        | 0 => (act_record beta beta_list' C (replace sn state_val s))
            :: H'
        | S ln' => (act_record beta beta_list' C s) 
            :: (replace_state ln' sn state_val H')
      end
    | fut_record beta beta' T v :: H' => 
      match ln with 
        | 0 => fut_record beta beta' T v :: H' 
        | S ln' => (fut_record beta beta' T v) 
            :: (replace_state ln' sn state_val H')
      end
  end.

Fixpoint staticize (e:exp_b) (H:store) : beta_ty_var :=
  match e with 
    | loc_exp_b (Id ln) => 
      match nth ln H (fut_record null_beta_ty_var null_beta_ty_var (act_val_ty (Id 0)) npe_exp_b) with
        | act_record beta beta_list' C s => beta
        | fut_record beta beta' T v => beta
      end
    | _ => null_beta_ty_var
  end.

Fixpoint staticize_list (v_list:list exp_b) (H:store) : list beta_ty_var :=
  match v_list with
    | nil => nil
    | v' :: v_list' => (staticize v' H) 
                    :: staticize_list v_list' H
  end.

Fixpoint new_act_betalist (n:nat) (C:act_id) (st_list:list state) : 
  list beta_ty_var :=
  match st_list with 
    | nil => nil
    | st' :: st_list' => 
            (fut_beta_ty_var (act_beta_ty_var C) (act_beta_ty_var (Id n))) 
            :: (new_act_betalist (n + 1) C (st_list'))
  end.

Fixpoint new_act_st_map (st_list:list state) (v_list:list exp_b) : 
  st_map := 
  match st_list with 
    | nil => nil
    | st' :: st_list' => 
      match v_list with 
        | nil => 
            (st', npe_exp_b) :: new_act_st_map st_list' v_list
        | v' :: v_list' =>
            (st', v') :: new_act_st_map st_list' v_list'
      end
  end.

Fixpoint label (e : exp) : list alpha_ty_var :=
  match e with 
    | inv_exp x alpha m_name x_list => (alpha :: nil) 
    | new_act_exp alpha alpha_list' C x_list => (alpha :: alpha_list')
    | new_fut_exp alpha alpha' T x => (alpha :: (alpha' :: nil))
    | let_exp x e' e'' => (label e') ++ (label e'')
    | st_asgn_exp s e' => (label e')
    | _ => nil
  end.

Fixpoint label_b (e : exp_b) : list beta_ty_var :=
  match e with 
    | inv_exp_b x beta m_name x_list => (beta :: nil) 
    | new_act_exp_b beta beta_list' C x_list => (beta :: beta_list')
    | new_fut_exp_b beta beta' T x => (beta :: (beta' :: nil))
    | let_exp_b x e' e'' => (label_b e') ++ (label_b e'')
    | st_asgn_exp_b s e' => (label_b e')
    | _ => nil
  end.

Fixpoint inv_new_beta_index (C:act_id) (n:nat) (beta_list : list beta_ty_var)
  : nat :=
  match beta_list with 
    | (fut_beta_ty_var (act_beta_ty_var C) (act_beta_ty_var (Id n'))) 
      :: beta_list' => if n' <? n then inv_new_beta_index C n beta_list'
        else inv_new_beta_index C (n' + 1) beta_list'
    | _ :: beta_list' => inv_new_beta_index C n beta_list'
    | nil => n
  end.

Fixpoint inv_fresh_beta (C:act_id) (n:nat) (beta_list : list beta_ty_var)
  : beta_ty_var :=
  match beta_list with 
    | (fut_beta_ty_var (act_beta_ty_var C) (act_beta_ty_var (Id n'))) 
      :: beta_list' => if n' <? n then inv_fresh_beta C n beta_list'
        else inv_fresh_beta C (n' + 1) beta_list'
    | _ :: beta_list' => inv_fresh_beta C n beta_list'
    | nil => (fut_beta_ty_var (act_beta_ty_var C) (act_beta_ty_var (Id n))) 
  end.

Fixpoint inv_refresh_betalist (C:act_id) (n:nat) (alpha_list : list alpha_ty_var)
  : list beta_ty_var :=
  match alpha_list with 
    | alpha' :: alpha_list' => 
      (fut_beta_ty_var (act_beta_ty_var C) (act_beta_ty_var (Id n))) ::
      inv_refresh_betalist C (n + 1) alpha_list'
    | nil => nil
  end.

Fixpoint refresh' (Delta:Delta_seq) (alpha_list:list alpha_ty_var)
  (H:store) (C:act_id) (n:nat): list beta_ty_var := 
  match H with 
    | act_record beta beta_list' C Smap :: H' => 
        refresh' Delta alpha_list H' C 
        (inv_new_beta_index C n (beta :: beta_list'))
    | fut_record beta beta' T v :: H' =>  
        refresh' Delta alpha_list H' C 
        (inv_new_beta_index C n (beta :: beta' :: nil))
    | nil => inv_refresh_betalist C n alpha_list
  end.

Fixpoint collapse_in_call_seq (Delta:Delta_seq) (C:act_id) (mname:meth_id)
  : list beta_ty_var := 
  match Delta with 
    | empty_Delta => nil
    | add_Delta (delta_decl beta C' mname') Delta' =>
      if (id_elem_dec C' C) then 
        if (id_elem_dec mname mname') then
            beta :: (collapse_in_call_seq Delta' C mname) 
        else (collapse_in_call_seq Delta' C mname)
      else (collapse_in_call_seq Delta' C mname)
  end.

Fixpoint refresh (Delta:Delta_seq) (alpha_list:list alpha_ty_var)
  (H:store) (C:act_id) (n:nat) (mname:meth_id): list beta_ty_var := 
  match collapse_in_call_seq Delta C mname with 
    | nil => refresh' Delta alpha_list H C n
    | beta_list => beta_list
  end.

Fixpoint d2s (Delta:list (id * act_id * meth_id)) (H:store) : (Delta_seq) := 
  match Delta with 
    | nil => empty_Delta
    | ((Id ln, C, m) :: Delta' ) => 
    match nth_error H ln with
      | Some(act_record beta beta_list' C Smap) => 
          add_Delta (delta_decl beta C m) (d2s Delta' H)
      | _ => empty_Delta
    end
  end.

Fixpoint new_act_Phi (Phi : Phi_trace) (beta_list' : list beta_ty_var) 
  (beta_list'' : list beta_ty_var ): (Phi_trace) := 
  match beta_list' with 
    | nil => Phi
    | beta' :: beta_rmndr' =>
        match beta_list'' with 
          | nil => Phi
          | beta'' :: beta_rmndr'' => 
            (flow_theta_bhvr beta' beta'') 
            :: (new_act_Phi (Phi) (beta_rmndr') (beta_rmndr''))
        end
  end.

Fixpoint inv_alpha_to_beta (alpha:alpha_ty_var) 
  (alpha_list:list alpha_ty_var) (beta_list:list beta_ty_var) : beta_ty_var :=
  match alpha_list with 
    | nil => null_beta_ty_var
    | alpha' :: alpha_list' => 
      match beta_list with 
        | nil => null_beta_ty_var
        | beta' :: beta_list' => 
          if eq_alpha_dec alpha alpha then beta' else 
          inv_alpha_to_beta alpha alpha_list' beta_list'
      end
  end.

Fixpoint inv_alphalist_to_betalist (alpha_in:list alpha_ty_var) 
  (alpha_list:list alpha_ty_var) (beta_list:list beta_ty_var) : 
  list beta_ty_var := 
  match alpha_in with 
    | nil => nil
    | alpha' :: alpha_in' => (inv_alpha_to_beta alpha' alpha_list beta_list)
        :: (inv_alphalist_to_betalist alpha_in' alpha_list beta_list)
  end.

Fixpoint inv_e_replace (e : exp) (beta_list:list beta_ty_var) 
  (alpha_list:list alpha_ty_var) : exp_b := 
  match e with 
    | inv_exp C alpha m x_list => 
        inv_exp_b C (inv_alpha_to_beta alpha alpha_list beta_list) m x_list
    | new_act_exp alpha alpha_list' C x_list => 
        new_act_exp_b (inv_alpha_to_beta alpha alpha_list beta_list)
        (inv_alphalist_to_betalist alpha_list' alpha_list beta_list)
        C x_list
    | new_fut_exp alpha alpha' T x => 
        new_fut_exp_b (inv_alpha_to_beta alpha alpha_list beta_list)
        (inv_alpha_to_beta alpha' alpha_list beta_list) T x
    | wait_exp x => wait_exp_b x
    | let_exp x e' e'' => 
        let_exp_b x (inv_e_replace e' beta_list alpha_list)
        (inv_e_replace e'' beta_list alpha_list)
    | st_asgn_exp s e' => 
        st_asgn_exp_b s (inv_e_replace e' beta_list alpha_list)
    | st_read_exp s => st_read_exp_b s
    | var_exp x => var_exp_b x
    | self_exp slf => self_exp_b slf
    | null_exp => null_exp_b
    | loc_exp l => loc_exp_b l
    | unresl_exp => unresl_exp_b
    | ctxt_exp e' l C m => 
      ctxt_exp_b (inv_e_replace e' beta_list alpha_list) l C m
    | resl_exp l e' => 
      resl_exp_b l (inv_e_replace e' beta_list alpha_list)
    | npe_exp => npe_exp_b
  end.

Inductive lookup_var_loc : var_val_map -> id -> exp_b -> Prop :=
  lookup_variable_location : forall V x l,
  V x = Some(loc_exp_b l) -> 
  lookup_var_loc V x (loc_exp_b l).

Fixpoint lookup_varlist_val (V:var_val_map) (x_list:list id) : list exp_b :=
  match x_list with
   | nil => nil
   | (x :: x_list') => 
    match (V x) with 
      | Some(loc_exp_b l) => (loc_exp_b l) :: (lookup_varlist_val V x_list')
      | Some(null_exp_b) => (null_exp_b) :: (lookup_varlist_val V x_list')
      | Some(unresl_exp_b) => (unresl_exp_b) :: (lookup_varlist_val V x_list')
      | None => npe_exp_b :: (lookup_varlist_val V x_list')
      | _ => npe_exp_b :: (lookup_varlist_val V x_list')
    end
  end.

Fixpoint act_glbl_cnfg (G:glbl_cnfg) (l':id) (VH:var_val_map * store)
   : glbl_cnfg :=
  match G with 
    | empty_glbl_cnfg => (add_glbl_cnfg 
                         (act_cnfg nil nil l') 
                         empty_glbl_cnfg VH)
    | add_glbl_cnfg A G' VH' => act_glbl_cnfg G' l' VH'
  end.

Fixpoint inv_glbl_cnfg (G:glbl_cnfg) (l':id) (e'':exp_b)
  (VH:var_val_map * store) : glbl_cnfg :=
  match G with 
    | empty_glbl_cnfg => (add_glbl_cnfg 
                         (act_cnfg (e'' :: nil) nil (l'))
                         empty_glbl_cnfg VH)
    | add_glbl_cnfg (act_cnfg Q' Phi' l) G' VH' =>
        if id_elem_dec l l' then 
          (add_glbl_cnfg 
          (act_cnfg (Q' ++ (e'' :: nil)) Phi' l') 
          G' VH)
        else 
          add_glbl_cnfg (act_cnfg Q' Phi' l) 
          (inv_glbl_cnfg G' l' e'' VH)
          VH'
  end.