Require Import List.
Require Import util_for_tactics.
Require Import applpi.
Require Import set.
Require Import logic.
Require Import conf_red.
Require Import datatypes_for_tactics.
Require Import conf_red_com_always_tactic.

 (*** 
   * (search_nul 'eps P) optionally returns one nul subprocess of P
   * (pickup_nul_cont P p) returns the continuation of the nul subprocess
   *  at position p
   * (rep_nul_cont_simp P new_c nul_pos) returns the process obtained
   *  from P by reducing the nul subprocess at position nul_pos using
   *  new_c channel
   ***)

Ltac search_nul cur P :=
  match constr:P with
  | (nuPl ?X1) => constr:(Some cur)
  | (parP ?X1 ?X2) =>
      let tmp := search_nul (one :: cur) X1 in
      test_option2 tmp ltac:(search_nul (two :: cur) X2)
  | zeroP => constr:(None (A:=cur))
  | (?X1 ?? ?X2) => constr:(None (A:=pos))
  | (?X1 ??* ?X2) => constr:(None (A:=pos))
  | (?X1 << ?X2 >> ?X3) => constr:(None (A:=pos))
  | (nuP ?X1) => constr:(None (A:=pos))
  | _ => constr:(None (A:=pos))
  end. (* Instead of Fail, so that we can process processes with variable in lieu of subprocesses *)

Ltac pickup_nul_cont' P pos :=
  match constr:pos with
  | nil => pickup_nul_cont_atom P
  | (?X1 :: ?X2) => pickup_nul_cont'' X1 X2 P
  end
 with pickup_nul_cont'' hd tl P :=
  match constr:hd with
  | one => pickup_nul_cont_one P tl
  | two => pickup_nul_cont_two P tl
  end
 with pickup_nul_cont_one P tl :=
  match constr:P with
  | (parP ?X1 ?X2) => pickup_nul_cont' X1 tl
  | _ => fail
  end
 with pickup_nul_cont_two P tl :=
  match constr:P with
  | (parP ?X1 ?X2) => pickup_nul_cont' X2 tl
  | _ => fail
  end
 with pickup_nul_cont_atom P :=
  match constr:P with
  | (nuPl ?X1) => constr:X1
  | _ => fail
  end.

Ltac pickup_nul_cont P p :=
  let rev_p := eval compute in (rev p) in
  pickup_nul_cont' P rev_p.

Ltac rep_nul_cont_simp P new_c nul_pos :=
  let nul_cont := pickup_nul_cont P nul_pos in
  let new_nul := eval cbv beta iota zeta in (nul_cont new_c) in
  subst_cont P new_nul nul_pos.

(***
   * (ConfRedNewL c) where c is supposed to be a fresh linearized
   *  channel applies to (sat (FMUSTEV ?1) ?2#?3) goals, it picks up
   *  one nul subprocess, performs the reduction and proves it correct
   *
   * This tactic performs ok even if the interface of the process is
   * not completely visible (there may be variables in lieu of processes)
   ***)

Ltac ConfRedNewL new_c :=
match goal with
  | |- (tsat (FMUSTEV ?A) (?B#?C))  =>
let some_pos := (search_nul eps C) in
let nul_pos := (extract_option some_pos) in
let new_P := (rep_nul_cont_simp C new_c nul_pos) in
eapply conf_red_new with (P':=new_P) (c:=new_c);
[(apply red_new; [tr_nu | auto]) | auto | idtac | idtac | idtac | idtac]
end.

Ltac ConfRedNewL_set c :=
ConfRedNewL c;
[apply chanlist_fresh; auto | idtac | idtac].

Ltac search_nu cur P :=
  match constr:P with
  | (nuP ?X1) => constr:(Some cur)
  | (parP ?X1 ?X2) =>
      let tmp := search_nu (one :: cur) X1 in
      test_option2 tmp ltac:(search_nu (two :: cur) X2)
  | zeroP => constr:(None (A:=cur))
  | (?X1 ?? ?X2) => constr:(None (A:=pos))
  | (?X1 ??* ?X2) => constr:(None (A:=pos))
  | (?X1 << ?X2 >> ?X3) => constr:(None (A:=pos))
  | (nuPl ?X1) => constr:(None (A:=pos))
  | _ => constr:(None (A:=pos))
  end.

Ltac pickup_nu_cont' P p :=
  match constr:p with
  | nil => pickup_nu_cont_atom P
  | (?X1 :: ?X2) => pickup_nu_cont'' X1 X2 P
  end
 with pickup_nu_cont'' hd tl P :=
  match constr:hd with
  | one => pickup_nu_cont_one P tl
  | two => pickup_nu_cont_two P tl
  end
 with pickup_nu_cont_one P tl :=
  match constr:P with
  | (parP ?X1 ?X2) => pickup_nu_cont' X1 tl
  | _ => fail
  end
 with pickup_nu_cont_two P tl :=
  match constr:P with
  | (parP ?X1 ?X2) => pickup_nu_cont' X2 tl
  | _ => fail
  end
 with pickup_nu_cont_atom P :=
  match constr:P with
  | (nuP ?X1) => constr:X1
  | _ => fail
  end.

Ltac pickup_nu_cont P p :=
  let rev_p := eval compute in (rev p) in
  pickup_nu_cont' P rev_p.

Ltac rep_nu_cont_simp P new_c nu_pos :=
  let nu_cont := pickup_nu_cont P nu_pos in
  let new_nu := eval cbv beta iota zeta in (nu_cont new_c) in
  subst_cont P new_nu nu_pos.

Ltac ConfRedNew new_c :=
match goal with
  | |- (tsat (FMUSTEV ?A) (?B#?C)) =>
let some_pos := (search_nu eps C) in
let nu_pos := (extract_option some_pos) in
let new_P := (rep_nu_cont_simp C new_c nu_pos) in
eapply conf_red_new with (P':=new_P) (c:=new_c);
[apply red_new; [tr_nu | auto] | auto | idtac | idtac | idtac | idtac ]
end.

Ltac ConfRedNew_set c :=
ConfRedNew c;
[apply chanlist_fresh; auto | idtac | idtac].