Lvc.IL.StateType

Require Import List.
Require Export IL.Events.

Set Implicit Arguments.

Definition reducible2 :=
  fun (X Y : Type) (R : XYXProp) (x : X) ⇒ y x', R x y x'.

Definition normal2 :=
  fun (X Y : Type) (R : XYXProp) (x : X) ⇒ ¬ reducible2 R x.

Definition reddec2 :=
  fun (X Y : Type) (R : XYXProp) ⇒ x : X, reducible2 R x normal2 R x.

Definition internally_deterministic {X : Type} (R : X event X Prop)
  := x y x1 x2, R x EvtTau x1 R x y x2 x1 = x2 y = EvtTau.

Definition externally_determined {X : Type} (R : X event X Prop)
  := x e x1 x2, R x e x1 R x e x2 x1 = x2.

Class StateType S := {
  step : S event S Prop;
  result : S option val;
  step_dec : reddec2 step;
  step_internally_deterministic : internally_deterministic step;
  step_externally_determined : externally_determined step
}.

Arguments step : simpl never.

Definition stateType S (ST:StateType S) := S.

Coercion stateType : StateType >-> Sortclass.

Smpl Create single_step [progress].

Ltac single_step := smpl single_step.

Ltac unpack_reducible :=
  repeat match goal with
         | [ H: @reducible2 _ _ _ _ |- _ ] ⇒
           let ev := fresh "evt" in
           let σ := fresh "σ" in
           let STEP := fresh "step" in
           destruct H as [evSTEP]]; inv STEP
         end.