(****************************************************************************************************)
(*****************************************     Syntax       *****************************************)
(****************************************************************************************************)

Require Export List.
Require Export Coq.Arith.Peano_dec.
Require Export Coq.Arith.PeanoNat.

(******************************** Type Syntax ********************************)

Inductive id : Type := 
  Id : nat -> id.

Definition act_id := id.

Definition meth_id := id.

Inductive val_ty : Type := 
  | act_val_ty : act_id -> val_ty
  | fut_val_ty : val_ty -> val_ty.

Inductive alpha_ty_var : Type := 
  | null_alpha_ty_var : alpha_ty_var
  | act_alpha_ty_var : act_id -> alpha_ty_var
  | fut_alpha_ty_var : alpha_ty_var -> alpha_ty_var -> alpha_ty_var.

Definition eq_alpha_dec : 
  forall alpha alpha' : alpha_ty_var, 
  {alpha = alpha'} + {alpha <> alpha'}.
Proof.
decide equality. destruct a. destruct a0. destruct (eq_nat_dec n n0).
left. rewrite <- e. auto. right. contradict n1. inversion n1. auto.
Qed.

Inductive alpha_hat : Type := 
  | alpha_alpha_hat : alpha_ty_var -> alpha_hat
  | act_alpha_hat : alpha_ty_var -> list alpha_ty_var -> act_id -> alpha_hat
  | fut_alpha_hat : alpha_ty_var -> alpha_ty_var -> val_ty -> alpha_hat.

Definition A_list := list alpha_ty_var.

Inductive beta_ty_var : Type := 
  | null_beta_ty_var : beta_ty_var
  | act_beta_ty_var : act_id -> beta_ty_var
  | fut_beta_ty_var : beta_ty_var -> beta_ty_var -> beta_ty_var.

Definition eq_beta_dec : 
  forall beta beta' : beta_ty_var, 
  {beta = beta'} + {beta <> beta'}.
Proof.
decide equality. destruct a. destruct a0. destruct (eq_nat_dec n n0).
left. rewrite <- e. auto. right. contradict n1. inversion n1. auto.
Qed.

Inductive beta_hat : Type := 
  | beta_beta_hat : beta_ty_var -> beta_hat
  | act_beta__hat : beta_ty_var -> list beta_ty_var -> act_id -> beta_hat
  | fut_beta_ty_var_hat : beta_ty_var -> beta_ty_var -> val_ty -> beta_hat.

Definition B_list := list beta_ty_var.

Inductive eta_bhvr : Type := 
  | nil_eta_bhvr : eta_bhvr
  | inv_eta_bhvr : alpha_ty_var -> alpha_ty_var -> meth_id -> list alpha_ty_var -> eta_bhvr
  | sync_eta_bhvr : alpha_ty_var -> eta_bhvr
  | resl_eta_bhvr : alpha_ty_var -> eta_bhvr
  | flow_eta_bhvr : alpha_ty_var -> alpha_ty_var -> eta_bhvr
  | new_act_eta_bhvr : alpha_ty_var -> list alpha_ty_var -> act_id -> alpha_ty_var -> eta_bhvr
  | new_fut_eta_bhvr : alpha_ty_var -> alpha_ty_var -> val_ty -> alpha_ty_var -> eta_bhvr.

Inductive sigma_bhvr : Type := 
  | empty_sigma_bhvr : sigma_bhvr
  | hpns_bfr_sigma_bhvr : sigma_bhvr -> sigma_bhvr -> sigma_bhvr
  | eta_bhvr_sigma_bhvr : eta_bhvr -> sigma_bhvr
  | union_sigma_bhvr : sigma_bhvr -> sigma_bhvr -> sigma_bhvr.

Inductive delta_call : Type := 
  | delta_decl : beta_ty_var -> act_id -> meth_id -> delta_call.

Inductive Delta_seq : Type := 
  | empty_Delta : Delta_seq
  | add_Delta : delta_call -> Delta_seq -> Delta_seq.

Inductive theta_bhvr : Type := 
  | nil_theta_bhvr : theta_bhvr
  | inv_theta_bhvr : beta_ty_var -> beta_ty_var -> meth_id -> list beta_ty_var -> theta_bhvr
  | sync_theta_bhvr : beta_ty_var -> theta_bhvr
  | resl_theta_bhvr : beta_ty_var -> theta_bhvr
  | flow_theta_bhvr : beta_ty_var -> beta_ty_var -> theta_bhvr
  | new_act_theta_bhvr : beta_ty_var -> list beta_ty_var -> act_id -> beta_ty_var -> theta_bhvr
  | new_fut_theta_bhvr : beta_ty_var -> beta_ty_var -> val_ty -> beta_ty_var -> theta_bhvr
  | ctxt_theta_bhvr : theta_bhvr -> delta_call -> theta_bhvr.

Inductive omega_bhvr : Type := 
  | empty_omega_bhvr : omega_bhvr
  | hpns_bfr_omega_bhvr : omega_bhvr -> omega_bhvr -> omega_bhvr
  | theta_bhvr_omega_bhvr : theta_bhvr -> omega_bhvr
  | union_omega_bhvr : omega_bhvr -> omega_bhvr -> omega_bhvr
  | ctxt_omega_bhvr : omega_bhvr -> delta_call -> omega_bhvr.

(******************************** Program Syntax ********************************)

Inductive state : Type := 
  | state_decl : val_ty -> id -> state.

Inductive exp : Type := 
  | inv_exp : id -> alpha_ty_var -> meth_id -> list id -> exp
  | new_act_exp : alpha_ty_var -> list alpha_ty_var -> act_id -> list id -> exp
  | new_fut_exp : alpha_ty_var -> alpha_ty_var -> val_ty -> id -> exp
  | wait_exp : id -> exp
  | let_exp : id -> exp -> exp -> exp
  | st_asgn_exp : id -> exp -> exp 
  | st_read_exp : id -> exp
  | var_exp : id -> exp
  | self_exp : id -> exp
  | null_exp : exp 
  | loc_exp : id -> exp 
  | unresl_exp : exp 
  | ctxt_exp : exp -> id -> act_id -> meth_id -> exp
  | resl_exp : id -> exp -> exp
  | npe_exp : exp.

Inductive val : exp -> Prop := 
  | loc_val : forall l, val (loc_exp l)
  | null_val : val (null_exp)
  | unresl_val : val (unresl_exp).

Inductive meth : Type :=
  | meth_decl : val_ty -> meth_id -> list (val_ty * id) -> exp -> meth.

Inductive actvt_decl : Type := 
  | act_decl : act_id -> list state -> list meth -> actvt_decl.

Inductive prgrm : Type := 
  | prog : list actvt_decl -> prgrm.

Inductive exp_b : Type := 
  | inv_exp_b : id -> beta_ty_var -> meth_id -> list id -> exp_b
  | new_act_exp_b : beta_ty_var -> list beta_ty_var -> act_id -> list id -> exp_b
  | new_fut_exp_b : beta_ty_var -> beta_ty_var -> val_ty -> id -> exp_b
  | wait_exp_b : id -> exp_b
  | let_exp_b : id -> exp_b -> exp_b -> exp_b
  | st_asgn_exp_b : id -> exp_b -> exp_b 
  | st_read_exp_b : id -> exp_b
  | var_exp_b : id -> exp_b
  | self_exp_b : id -> exp_b
  | null_exp_b : exp_b 
  | loc_exp_b : id -> exp_b 
  | unresl_exp_b : exp_b 
  | ctxt_exp_b : exp_b -> id -> act_id -> meth_id -> exp_b
  | resl_exp_b : id -> exp_b -> exp_b
  | npe_exp_b : exp_b.

Inductive val_b : exp_b -> Prop := 
  | loc_val_b : forall l, val_b (loc_exp_b l)
  | null_val_b : val_b (null_exp_b)
  | unresl_val_b : val_b (unresl_exp_b).