(****************************************************************************************************)
(*****************************************      Config      *****************************************)
(****************************************************************************************************)
Require Export syntax.

Inductive eval_ctxt := 
  | empty_ctxt : eval_ctxt
  | inv_ctxt_one : eval_ctxt -> beta_ty_var -> meth_id -> list exp 
      -> eval_ctxt
  | inv_ctxt_two : id -> beta_ty_var -> meth_id -> id -> eval_ctxt 
      -> list exp -> eval_ctxt
  | new_act_ctxt : beta_ty_var -> list beta_ty_var -> act_id -> id -> eval_ctxt 
      -> list exp -> eval_ctxt
  | fut_ctxt : beta_ty_var -> beta_ty_var -> eval_ctxt -> eval_ctxt
  | wait_ctxt : eval_ctxt -> eval_ctxt
  | let_ctxt_one : id -> eval_ctxt -> exp -> eval_ctxt
  | let_ctxt_two : id -> id -> eval_ctxt -> eval_ctxt
  | st_ctxt : id -> eval_ctxt -> eval_ctxt
  | ctxt_ctxt : eval_ctxt -> id -> act_id -> meth_id -> eval_ctxt
  | resl_ctxt : id -> eval_ctxt -> eval_ctxt.

Definition st_map := list (state * exp_b).

Inductive record := 
  | act_record : beta_ty_var -> list beta_ty_var -> act_id -> st_map -> record
  | fut_record : beta_ty_var -> beta_ty_var -> val_ty -> exp_b -> record.

Definition store := list (record).

Definition Phi_trace := list theta_bhvr.

Definition Queue := list exp_b.

Inductive Psi_act_cnfg := 
  | act_cnfg : Queue -> Phi_trace -> id -> Psi_act_cnfg.

(* Environment definitions based on Software Foundations definitions. *)

Definition id_elem_dec : 
  forall idA idB : id, 
  {idA = idB} + {idA <> idB}.
  Proof.
  intros. destruct idA, idB. destruct (eq_nat_dec n n0).
  left. rewrite <- e. auto.
  right. intro. inversion H. contradiction H1.
  Defined.

Definition beq_Gid x y :=
  if id_elem_dec x y then true else false.

Definition total_map (A : Type) := id -> A.

Definition t_empty {A:Type} (v : A) : total_map A :=
  (fun _ => v).

Definition t_update {A:Type} (m : total_map A) (x : id) (v : A) :=
  fun x' => if beq_Gid x x' then v else m x'.

Definition partial_map (A:Type) := total_map (option A).

Definition empty {A:Type} : partial_map A :=
  t_empty None.

Definition update {A:Type} (m : partial_map A) (x : id) (v : A) :=
  t_update m x (Some v).

Inductive Gamma_snd : Type := 
  | Gamma_snd_alpha : alpha_ty_var -> Gamma_snd
  | Gamma_snd_beta : beta_ty_var -> Gamma_snd
  | Gamma_snd_record : record -> Gamma_snd
  | Gamma_snd_Delta : Delta_seq -> Gamma_snd.

Definition Gamma_env := partial_map (prod val_ty Gamma_snd).

Definition var_val_map := partial_map (exp_b).

Inductive glbl_cnfg := 
  | empty_glbl_cnfg : glbl_cnfg
  | add_glbl_cnfg : Psi_act_cnfg -> glbl_cnfg -> (var_val_map * store) -> glbl_cnfg.