Require Import Linking Errors Smallstep.

Pass with an implementation

Local Set Implicit Arguments.

Record IPass {L0 L1 : Language} (sem0 : L0 -> semantics) (sem1 : L1 -> semantics) := {
  ipass_spec : Pass L0 L1;
  ipass_impl : L0 -> res L1;
  ipass_match : forall p0 p1, ipass_impl p0 = OK p1 -> ipass_spec p0 p1;
  ipass_correct : forall p0 p1, ipass_spec p0 p1 -> forward_simulation (sem0 p0) (sem1 p1);
}.

Local Unset Implicit Arguments.


Program Definition ipass_simu [L : Language] [sem0 sem1 : L -> semantics]
  (p : forall p, forward_simulation (sem0 p) (sem1 p))
  : @IPass L L sem0 sem1 :=
  {|
    ipass_spec := pass_identity L;
    ipass_impl := fun p => OK p;
  |}.

Program Definition ipass_refl {L} sem : @IPass L L sem sem := ipass_simu _.

Program Definition ipass_seq [L0 L1 L2 sem0 sem1 sem2]
  (tr0 : @IPass L0 L1 sem0 sem1) (tr1 : @IPass L1 L2 sem1 sem2)
  : @IPass L0 L2 sem0 sem2 :=
  {|
    ipass_spec := pass_compose (ipass_spec tr0) (ipass_spec tr1);
    ipass_impl := fun p0 => bind (ipass_impl tr0 p0) (ipass_impl tr1);
  |}.

Program Definition ipass_if_dep [L0 L1 : Language]
  (sem0 : bool -> L0 -> semantics) (sem1 : bool -> L1 -> semantics)
  (b : unit -> bool) (trA : @IPass L0 L1 (sem0 true) (sem1 true)) (trB : @IPass L0 L1 (sem0 false) (sem1 false))
  : @IPass L0 L1 (sem0 (b tt)) (sem1 (b tt)) :=
  {|
    ipass_spec := if b tt then ipass_spec trA else ipass_spec trB;
    ipass_impl := fun p => if b tt then ipass_impl trA p else ipass_impl trB p;
  |}.

Definition ipass_if [L0 L1 sem0 sem1] (b : unit -> bool) (trA trB : @IPass L0 L1 sem0 sem1) : IPass sem0 sem1
  := ipass_if_dep (fun _ => sem0) (fun _ => sem1) b trA trB.

Definition ipass_opt [L sem] (opt : unit -> bool) (tr : @IPass L L sem sem) : IPass sem sem
  := ipass_if opt tr (ipass_refl sem).


Declare Scope ipass_scope.

Infix ":::" := ipass_seq (at level 60, right associativity) : ipass_scope.