Module Qcert.Data.Operators.Iterators

Require Import List.
Require Import ListSet.
Require Import String.
Require Import ZArith.
Require Import Permutation.
Require Import Equivalence.
Require Import Morphisms.
Require Import Program.
Require Import EquivDec.
Require Import Bool.
Require Import Utils.
Require Import ForeignData.
Require Import Data.
Require Import DataLift.
Require Import RecOperators.

Section Iterators.
  Context {fdata:foreign_data}.

  Section MapUtils.
    Lemma lift_map_data_exists {A} (f: A -> option data) dl x :
      match lift_map f dl with
      | Some a' => Some (dcoll a')
      | None => None
      end = Some x ->
      exists x1, lift_map f dl = Some x1 /\ (dcoll x1) = x.

    Lemma lift_map_with_rproject sl l :
      (lift_map
         (fun d1 : data =>
            match d1 with
            | dunit => None
            | dnat _ => None
            | dfloat _ => None
            | dbool _ => None
            | dstring _ => None
            | dcoll _ => None
            | drec r => Some (drec (rproject r sl))
            | dleft _ => None
            | dright _ => None
            | dbrand _ _ => None
            | dforeign _ => None
            end) l) =
      (lift_map
         (fun d1 : data =>
            olift
              (fun d0 : data =>
                 match d0 with
                 | dunit => None
                 | dnat _ => None
                 | dfloat _ => None
                 | dbool _ => None
                 | dstring _ => None
                 | dcoll _ => None
                 | drec r => Some (drec (rproject r sl))
                 | dleft _ => None
                 | dright _ => None
                 | dbrand _ _ => None
                 | dforeign _ => None
                 end) (Some d1)) l).
  End MapUtils.

  Section MapConcatUtils.

    Inductive map_concat_sem: data -> list data -> list data -> Prop :=
    | sem_map_concat_empty : forall d,
        map_concat_sem d nil nil (* d χ⊕ {} ⇓ {} *)
    | sem_map_concat_cons : forall d d1 d2 c1 c2,
        rec_concat_sem d d1 d2 -> (* d ⊕ d₁ ⇓ d₂ *)
        map_concat_sem d c1 c2 -> (* ∧ d χ⊕ {c₁} ⇓ {c₂} *)
        map_concat_sem d (d1::c1) (d2::c2). (* ⇒ d χ⊕ {d₁::c₁} ⇓ {d₂::c₂} *)
    
    Definition omap_concat (a:data) (d1:list data) : option (list data) :=
      lift_map (fun x => orecconcat a x) d1.

      
    Lemma omap_concat_correct d c1 c2:
      omap_concat d c1 = Some c2 ->
      map_concat_sem d c1 c2.
      
    Lemma omap_concat_complete d c1 c2:
      map_concat_sem d c1 c2 ->
      omap_concat d c1 = Some c2.
      
    Lemma omap_concat_correct_and_complete d c1 c2:
      omap_concat d c1 = Some c2 <->
      map_concat_sem d c1 c2.

  End MapConcatUtils.

  Section MapProductUtils.
    Definition oncoll_map_concat
               (f:data -> option data)
               (a:data) :=
      match f a with
      | Some (dcoll y) => omap_concat a y
      | _ => None
      end.

    Lemma oncoll_map_concat_ext_weak f g a :
      (f a = g a) ->
      oncoll_map_concat f a = oncoll_map_concat g a.
  
    Definition omap_product (f:data -> option data) (d:list data) : option (list data) :=
      lift_flat_map (oncoll_map_concat f) d.

    Lemma omap_product_cons f d a x y :
      omap_product f d = Some x ->
      (oncoll_map_concat f a) = Some y ->
      omap_product f (a :: d) = Some (y ++ x).

    Lemma omap_product_cons_none f d a :
      omap_product f d = None -> omap_product f ((drec a) :: d) = None.

    Lemma omap_product_cons_none_first f d a :
      (oncoll_map_concat f a) = None -> omap_product f (a :: d) = None.

    Lemma omap_product_cons_inv f d a l :
      omap_product f (a :: d) = Some l ->
      exists x, exists y,
          (oncoll_map_concat f a) = Some x /\
          omap_product f d = Some y /\
          x ++ y = l.

    Lemma omap_product_ext f g l :
      (forall x, In x l -> f x = g x) ->
      omap_product f l = omap_product g l.

  End MapProductUtils.

  Section ProductUtils.

    Inductive product_sem: list data -> list data -> list data -> Prop :=
    | sem_product_empty : forall c,
        product_sem nil c nil (* {c} × {} ⇓ {} *)
    | sem_product_cons : forall d1 c1 c2 c3 c4,
        map_concat_sem d1 c2 c3 -> (* ∧ d₁ χ⊕ {c₂} ⇓ {c₃} *)
        product_sem c1 c2 c4 -> (* ∧ {c₁} × {c₂} ⇓ {c₄} *)
        product_sem (d1::c1) c2 (c3 ++ c4). (* ⇒ {d₁::c₁} × {c₂} ⇓ {c₃}∪{c₄} *)

    Definition oproduct (d1 d2:list data) : option (list data) :=
      lift_flat_map (fun x => omap_concat x d2) d1.
  
    Lemma oproduct_cons (d1 d2:list data) a x y:
      oproduct d1 d2 = Some x ->
      (omap_concat a d2) = Some y ->
      oproduct (a::d1) d2 = Some (y ++ x).

      
    Lemma oproduct_correct c1 c2 c3:
      oproduct c1 c2 = Some c3 ->
      product_sem c1 c2 c3.

    Lemma oproduct_complete c1 c2 c3:
      product_sem c1 c2 c3 ->
      oproduct c1 c2 = Some c3.

    Lemma oproduct_correct_and_complete c1 c2 c3:
      oproduct c1 c2 = Some c3 <->
      product_sem c1 c2 c3.

  End ProductUtils.

  Section FlattenUtils.
    Definition oflatten (d:list data) : option (list data) :=
      lift_flat_map (fun x =>
                   match x with
                   | dcoll y => Some y
                   | _ => None end) d.

    Lemma oflatten_cons (l:list data) rest r' :
      oflatten rest = Some r' ->
      oflatten ((dcoll l) :: rest) = Some (l ++ r').

    Lemma oflatten_app (l1 l2:list data) r1 r2 :
      oflatten l1 = Some r1 ->
      oflatten l2 = Some r2 ->
      oflatten (l1 ++ l2) = Some (r1 ++ r2).

    Lemma oflatten_map_dcoll_id coll :
      oflatten (map (fun d : data => dcoll (d::nil)) coll) = Some coll.

    Lemma oflatten_cons_none (d:data) rest :
      oflatten rest = None ->
      oflatten (d :: rest) = None.

    Lemma oflatten_app_none1 l1 l2 :
      oflatten l1 = None ->
      oflatten (l1 ++ l2) = None.

    Lemma oflatten_app_none2 l1 l2 :
      oflatten l2 = None ->
      oflatten (l1 ++ l2) = None.

    Lemma oflatten_lift_empty_dcoll l :
      olift oflatten (lift (fun t' : list data => dcoll nil :: t') l) = olift oflatten l.

    Lemma oflatten_lift_cons_dcoll a l:
      olift oflatten
            (lift (fun t' : list data => dcoll (a::nil) :: t') l) =
      lift (fun t' => a::t') (olift oflatten l).

    Lemma oflatten_through_match l1 l2:
      olift oflatten
            match lift dcoll (Some l1) with
            | Some x' =>
              lift (fun t' : list data => x' :: t') l2
            | None => None
            end =
      lift (fun t' : list data => l1 ++ t')
           (olift oflatten l2).
    
  End FlattenUtils.

End Iterators.

Global Hint Rewrite @oflatten_map_dcoll_id : alg.