Lvc.Infra.Status

Require Import String List Get.

Set Implicit Arguments.

Inductive status A :=
  | Success : Astatus A
  | Error : stringstatus A.


Definition bind (A B : Type) (f : status A) (g : Astatus B) : status B :=
  match f with
    | Success ag a
    | Error eError e
  end.

Notation "´sdo´ X <- A ; B" := (bind A (fun XB))
 (at level 200, X ident, A at level 100, B at level 200).

Definition option2status {A} : option Astringstatus A.
Defined.

Lemma option2status_inv {A} o s (v:A)
      : option2status o s = Success v
      → o = Some v.


Lemma bind_inversion (A B : Type) (f : status A) (g : Astatus B) (y : B) :
  bind f g = Success y x, f = Success x g x = Success y.

Lemma bind_inversion´ (A B : Type) (f : status A) (g : Astatus B) (y : B) :
  bind f g = Success y{ x : A | f = Success x g x = Success y }.

Reasoning over monadic computations

The monadInv H tactic below simplifies hypotheses of the form
        H: (do x <- a; b) = OK res
By definition of the bind operation, both computations a and b must succeed for their composition to succeed. The tactic therefore generates the following hypotheses:
x: ... H1: a = OK x H2: b x = OK res

Ltac monadS_inv1 H :=
  match type of H with
  | (Success _ = Success _) ⇒
      inversion H; clear H; try subst
  | (Error _ = Success _) ⇒
      discriminate
  | (bind ?F ?G = Success ?X) ⇒
      let x := fresh "x" in (
      let EQ1 := fresh "EQ" in (
      let EQ2 := fresh "EQ" in (
        destruct (bind_inversion´ F G H) as [x [EQ1 EQ2]];
        clear H;
        try (monadS_inv1 EQ2))))
  end.

Ltac monadS_inv H :=
  match type of H with
  | (Success _ = Success _) ⇒ monadS_inv1 H
  | (Error _ = Success _) ⇒ monadS_inv1 H
  | (bind ?F ?G = Success ?X) ⇒ monadS_inv1 H
  | (@eq _ (@bind _ _ _ _ _ ?G) (?X)) ⇒
    let X := fresh in remember G as X; simpl in H; subst X; monadS_inv1 H
  end.

Section ParametricOptionMapIndex.
  Variables X Y : Type.
  Hypothesis f : natXstatus Y : Type.

  Fixpoint smapi_impl (n:nat) (L:list X) : status (list Y) :=
    match L with
      | x::L
        sdo v <- f n x;
          sdo vl <- smapi_impl (S n) L;
          Success (v::vl)
      | _Success nil
    end.

  Definition smapi := smapi_impl 0.

End ParametricOptionMapIndex.

Section ParametricZip.
  Variables X Y Z : Type.
  Hypothesis f : XYstatus Z : Type.

  Fixpoint szip (L:list X) (:list Y) : status (list Z) :=
    match L, with
      | x::L, y::
        sdo z <- f x y;
          sdo ZL <- szip L ;
          Success (z::ZL)
      | _, _Success nil
    end.

End ParametricZip.

Section ParametricStatusMap.
  Variables X Y : Type.
  Hypothesis f : Xstatus Y : Type.

  Fixpoint smap (L:list X) : status (list Y) :=
    match L with
      | x::L
        sdo v <- f x;
          sdo vl <- smap L;
          Success (v::vl)
      | _Success nil
    end.

  Lemma smap_spec L
  : smap L = Success
    → n x, get L n x y, f x = Success y get n y.

  Lemma smap_length L
  : smap L = Success
    → length = length L.

End ParametricStatusMap.

Lemma smap_agree_2 X Y (f: Xstatus Y) (g: status Y) L
: ( n x y, get L n xget n yf x = g y)
  → length L = length
  → smap f L = smap g .