Require Import List.
Require Import listT.
Require Import chanlist.
Require Import applpi.
Require Import util_for_tactics.
Require Import datatypes_for_tactics.
Require Import logic.
Ltac search_out2 c p lst cur P :=
match constr:P with
| (?X1 << ?X2 >> ?X3) =>
test_chan2 X1 c (consIO c p cur lst) lst
| (parP ?X1 ?X2) =>
let l1 := search_out2 c p lst (one :: cur) X1 in
search_out2 c p l1 (two :: cur) X2
| zeroP => lst
| (?X1 ?? ?X2) => lst
| (?X1 ??* ?X2) => lst
| (nuP ?X1) => fail
| (nuPl ?X1) => fail
| _ => fail
end.
Ltac search_inout2' lst cur whole P :=
match constr:P with
| (?X1 ?? ?X2) =>
let tmp := search_out2 X1 cur nilIO eps whole in
eval compute in (appP tmp lst)
| (?X1 ??* ?X2) =>
let tmp := search_out2 X1 cur nilIO eps whole in
eval compute in (appP tmp lst)
| (parP ?X1 ?X2) =>
let l1 := search_inout2' lst (one :: cur) whole X1 in
search_inout2' l1 (two :: cur) whole X2
| zeroP => lst
| (?X1 << ?X2 >> ?X3) => lst
| (nuP ?X1) => fail
| (nuPl ?X1) => fail
| _ => fail
end.
Ltac search_inout2 P := search_inout2' nilIO eps P P.
Ltac subst_cont2' P Q p :=
match constr:p with
| nil => Q
| (?X1 :: ?X2) => subst_cont2'' X1 X2 P Q
end
with subst_cont2'' hd tl P Q :=
match constr:hd with
| one => subst_cont2_one P Q tl
| two => subst_cont2_two P Q tl
end
with subst_cont2_one P Q tl :=
match constr:P with
| (parP ?X3 ?X4) =>
let tmp := subst_cont2' X3 Q tl in
constr:(parP tmp X4)
| _ => fail
end
with subst_cont2_two P Q tl :=
match constr:P with
| (parP ?X3 ?X4) =>
let tmp := subst_cont2' X4 Q tl in
constr:(parP X3 tmp)
| _ => fail
end.
Ltac subst_cont2 P Q p :=
let rev_p := eval compute in (rev p) in
subst_cont2' P Q rev_p.
Ltac pickup_val2' P pos :=
match constr:pos with
| nil => pickup_val2_atom P
| (?X1 :: ?X2) => pickup_val2l X1 X2 P
end
with pickup_val2l hd tl P :=
match constr:hd with
| one => pickup_val2_one P tl
| two => pickup_val2_two P tl
end
with pickup_val2_one P tl :=
match constr:P with
| (parP ?X3 ?X4) => pickup_val2' X3 tl
| _ => fail
end
with pickup_val2_two P tl :=
match constr:P with
| (parP ?X3 ?X4) => pickup_val2' X4 tl
| _ => fail
end
with pickup_val2_atom P :=
match constr:P with
| (?X1 << ?X2 >> ?X3) => constr:X2
| _ => fail
end.
Ltac pickup_val2 P p :=
let rev_p := eval compute in (rev p) in
pickup_val2' P rev_p.
Ltac pickup_out2_cont' P pos :=
match constr:pos with
| nil => pickup_out2_cont_atom P
| (?X1 :: ?X2) => pickup_out2_cont'' X1 X2 P
end
with pickup_out2_cont'' hd tl P :=
match constr:hd with
| one => pickup_out2_cont_one P tl
| two => pickup_out2_cont_two P tl
end
with pickup_out2_cont_one P tl :=
match constr:P with
| (parP ?X3 ?X4) => pickup_out2_cont' X3 tl
| _ => fail
end
with pickup_out2_cont_two P tl :=
match constr:P with
| (parP ?X3 ?X4) => pickup_out2_cont' X4 tl
| _ => fail
end
with pickup_out2_cont_atom P :=
match constr:P with
| (?X1 << ?X2 >> ?X3) => constr:X3
| _ => fail
end.
Ltac pickup_out2_cont P p :=
let rev_p := eval compute in (rev p) in
pickup_out2_cont' P rev_p.
Ltac pickup_in2_cont' P pos :=
match constr:pos with
| nil => pickup_in2_cont_atom P
| (?X1 :: ?X2) => pickup_in2_cont'' X1 X2 P
end
with pickup_in2_cont'' hd tl P :=
match constr:hd with
| one => pickup_in2_cont_one P tl
| two => pickup_in2_cont_two P tl
end
with pickup_in2_cont_one P tl :=
match constr:P with
| (parP ?X3 ?X4) => pickup_in2_cont' X3 tl
| _ => fail
end
with pickup_in2_cont_two P tl :=
match constr:P with
| (parP ?X3 ?X4) => pickup_in2_cont' X4 tl
| _ => fail
end
with pickup_in2_cont_atom P :=
match constr:P with
| (?X1 ?? ?X2) => constr:X2
| (?X1 ??* ?X2) => constr:(fun x => parP (X1 ??* X2) (X2 x))
| _ => fail
end.
Ltac pickup_in2_cont P p :=
let rev_p := eval compute in (rev p) in
pickup_in2_cont' P rev_p.
Ltac rep_cont2_simp P in_pos out_pos :=
let v := pickup_val2 P out_pos in
let out_cont := pickup_out2_cont P out_pos in
let in_cont := pickup_in2_cont P in_pos in
let new_in := eval cbv beta iota zeta in (in_cont v) in
let (* instead of solely Compute *)
new_p0 := subst_cont2 P out_cont out_pos in
subst_cont2 new_p0 new_in in_pos.
Ltac rep_cont2 P lst :=
match constr:lst with
| nilIO => constr:(nilT proc)
| (consIO ?X1 ?X2 ?X3 ?X4) => rep_cont2' P X2 X3 X4
end
with rep_cont2' P in_pos out_pos tl :=
let tmp := rep_cont2_simp P in_pos out_pos in
let newtl := rep_cont2 P tl in
constr:(consT proc tmp newtl).
(** We conjecture that our tactic NextComms is complete. *)
Axiom NextComms_conjecture : False.
Ltac NextComms :=
match goal with
| id0:(Red (?X1 # ?X2) (?X1 # ?X3)) |- (tsat (FMUSTEV ?X4) (?X1 # ?X3)) =>
let lst := search_inout2 X2 in
let ns := rep_cont2 X2 lst in
(cut (in_listT proc X3 ns);
[ clear id0 | generalize NextComms_conjecture; contradiction ])
end.