Require Import ABP.INTERPRETER.Processes.

Section Lists.
Variable A : Set.
CoInductive List : Set :=
  | NIL : List
  | CONS : A → List → List.
End Lists.

Section Interpreter.

Variable Chnl : Set.
Variable compare : ∀ c1 c2 : Chnl, {c1 = c2} + {c1 ≠ c2}.

Variable A : Chnl → Set.

Inductive Pointer : Set :=
  | Succ : Pointer
  | Fail : Pointer
  | Left : Pointer → Pointer
  | Right : Pointer → Pointer.

Inductive Wright : Process Chnl A → Pointer → Prop :=
  | wright_s :
      ∀ (c1 : Chnl) (v : A c1) (c2 : Chnl) (f : A c2 → Guarded Chnl A)
        (p : Guarded Chnl A), Wright (TALK Chnl A c1 v p c2 f) Succ
  | wright_f :
      ∀ (c1 : Chnl) (v : A c1) (c2 : Chnl) (f : A c2 → Guarded Chnl A)
        (p : Guarded Chnl A), Wright (TALK Chnl A c1 v p c2 f) Fail
  | wright_r :
      ∀ (p1 p2 : Process Chnl A) (o : Pointer),
      Wright p2 o → Wright (PAR Chnl A p1 p2) (Right o)
  | wright_l :
      ∀ (p1 p2 : Process Chnl A) (o : Pointer),
      Wright p1 o → Wright (PAR Chnl A p1 p2) (Left o).

Inductive Result (o : Pointer) (p : Process Chnl A) : Set :=
  | Tuple :
      ∀ (c : Chnl) (w : Signal Chnl A c) (q : Process Chnl A),
      UnrelProcTrans Chnl A c p w q → Result o p
  | Error : ¬ Wright p o → Result o p.

CoInductive Trace : List Pointer → Process Chnl A → Set :=
  | Stop : ∀ p : Process Chnl A, Trace (NIL Pointer) p
  | Evolve :
      ∀ (o : Pointer) (x : List Pointer) (c : Chnl)
        (p q : Process Chnl A) (w : Signal Chnl A c),
      UnrelProcTrans Chnl A c p w q → Trace x q → Trace (CONS _ o x) p
  | Refuse :
      ∀ (o : Pointer) (x : List Pointer) (p : Process Chnl A),
      ¬ Wright p o → Trace x p → Trace (CONS _ o x) p.

Lemma listen :
 ∀ (p : Process Chnl A) (c : Chnl) (v : A c),
 {q : Process Chnl A | UnrelProcTrans Chnl A c p (Receive _ _ c v) q}.
fix 1.
simple destruct p.
simple destruct g.
intros c1 a0 p0 c2 f c0.
case (compare c2 c0).
intros H.
pattern c0 in |- ×.
case H.
intros.
∃ (INJ Chnl A (f v)).
apply uttalk2.
trivial.
intros.
∃ (INJ Chnl A (TALK Chnl A c1 a0 p0 c2 f)).
apply uttalk3.
assumption.
intros c p0 c0.
case (compare c c0).
intros H.
pattern c0 in |- ×.
case H.
intros.
∃ (INJ Chnl A (p0 v)).
apply utlisten1.
trivial.
intros.
∃ (INJ Chnl A (LISTEN Chnl A c p0)).
apply utlisten2.
assumption.
intros.
case (listen p0 c v).
intros.
case (listen p1 c v).
intros.
∃ (PAR Chnl A x x0).
apply utpar3.
assumption.
assumption.
Defined.

Lemma say : ∀ (o : Pointer) (p : Process Chnl A), Result o p.
fix 1.
simple destruct p.
simple destruct g.
case o.

intros c1 a0 p0 c2 p1.
apply (Tuple Succ (TALK Chnl A c1 a0 p0 c2 p1) c1 (Noise Chnl A c1) p0).
apply uttalk4.

intros c1 a0 p0 c2 p1.
apply (Tuple Fail (TALK Chnl A c1 a0 p0 c2 p1) c1 (Clear Chnl A c1 a0) p0).
apply uttalk1.

intros.
apply Error.
red in |- ×.
intro.
inversion_clear H.

intros.
apply Error.
red in |- ×.
intro.
inversion_clear H.

intros.
apply Error.
red in |- ×.
intro.
inversion_clear H.

case o.

intros.
apply Error.
red in |- ×.
intro.
inversion_clear H.

intros.
apply Error.
red in |- ×.
intro.
inversion_clear H.

intros ol p0 p1.
case (say ol p0).
simple destruct w.
intros q H0.
apply
 (Tuple (Left ol) (PAR Chnl A p0 p1) c (Noise Chnl A c) (PAR Chnl A q p1)).
apply utpar4.
assumption.
intros a q H0.
case (listen p1 c a).
intros.
apply
 (Tuple (Left ol) (PAR Chnl A p0 p1) c (Clear Chnl A c a) (PAR Chnl A q x)).
apply utpar1.
assumption.
assumption.
intros.
apply Error.
red in |- ×.
intro H.
inversion_clear H.
absurd (Wright p0 ol).
assumption.
assumption.
intros or p0 p1.
case (say or p1).
simple destruct w.
intros.
apply
 (Tuple (Right or) (PAR Chnl A p0 p1) c (Noise Chnl A c) (PAR Chnl A p0 q)).
apply utpar5.
assumption.
intros a q H0.
case (listen p0 c a).
intros.
apply
 (Tuple (Right or) (PAR Chnl A p0 p1) c (Clear Chnl A c a) (PAR Chnl A x q)).
apply utpar2.
assumption.
assumption.
intros.
apply Error.
red in |- ×.
intro H.
inversion_clear H.
absurd (Wright p1 or).
assumption.
assumption.
Defined.

Theorem simulator : ∀ (x : List Pointer) (p : Process Chnl A), Trace x p.
cofix.
intros x p.
case x.
apply Stop.
intros o y.
case (say o p).
intros c w q H0.
apply (Evolve o y c p q w).
assumption.
apply simulator.
intros H.
apply (Refuse o y p).
assumption.
apply simulator.
Defined.

End Interpreter.