Module Qcert.Data.Model.DataLift

Require Import ZArith.
Require Import String.
Require Import List.
Require Import Utils.
Require Import ForeignData.
Require Import Data.

Section DataLift.

  Context {fdata:foreign_data}.

  Definition unbdbool (f:bool -> bool -> bool) (d1 d2:data) : option data :=
    match d1 with
    | dbool b1 =>
      match d2 with
      | dbool b2 => Some (dbool (f b1 b2))
      | _ => None
      end
    | _ => None
    end.

  Definition unudbool (f:bool -> bool) (d:data) : option data :=
    match d with
    | dbool b =>Some (dbool (f b))
    | _ => None
    end.

  Definition unbdnat (f:Z -> Z -> bool) (d1 d2:data) : option data :=
    match d1 with
    | dnat n1 =>
      match d2 with
      | dnat n2 => Some (dbool (f n1 n2))
      | _ => None
      end
    | _ => None
    end.

  Definition unbdata (f:data -> data -> bool) (d1 d2:data) : option data :=
    Some (dbool (f d1 d2)).

  Definition unndstring (f:string -> Z) (d1:data) : option data :=
    match d1 with
    | dstring s1 => (Some (dnat (f s1)))
    | _ => None
    end.

  Lemma unndstring_is_nat f d1 d2:
    unndstring f d1 = Some d2 -> exists z:Z, d2 = dnat z.

  Definition unsdstring (f:string -> string -> string) (d1 d2:data) : option data :=
    match d1 with
    | dstring s1 =>
      match d2 with
      | dstring s2 => Some (dstring (f s1 s2))
      | _ => None
      end
    | _ => None
    end.

  Lemma unsdstring_is_string f d1 d2 d3:
    unsdstring f d1 d2 = Some d3 -> exists s:string, d3 = dstring s.

  Definition ondcoll2 {A} : (list data -> list data -> A) -> data -> data -> option A.

  Definition rondcoll2 (f:(list data -> list data -> list data)) (d1 d2:data) : option data :=
    lift dcoll (ondcoll2 f d1 d2).

  Definition ondstring {A} (f : string -> A) (d : data) :=
    match d with
    | dstring n => Some (f n)
    | _ => None
    end.

  Definition ondnat {A} (f : Z -> A) (d : data) :=
    match d with
    | dnat n => Some (f n)
    | _ => None
    end.

  Definition ondfloat {A} (f : float -> A) (d : data) :=
    match d with
    | dfloat n => Some (f n)
    | _ => None
    end.

  Definition ondcoll {A} (f : list data -> A) (d : data) :=
    match d with
    | dcoll l => Some (f l)
    | _ => None
    end.

    Definition lift_oncoll {A} (f : list data -> option A) (d : data) :=
      match d with
      | dcoll l => f l
      | _ => None
      end.

    Definition lift_ondcoll2 (f:list data -> list data -> option (list data)) (d1 d2:data) : option data :=
      match d1,d2 with
      | dcoll l1, dcoll l2 => lift dcoll (f l1 l2)
      | _,_ => None
      end.

    Lemma lift_oncoll_dcoll {A} (f : list data -> option A) (dl : list data) :
      lift_oncoll f (dcoll dl) = f dl.

    Lemma olift_on_lift_dcoll (f:list data->option data) (d1:option (list data)):
      olift (lift_oncoll f) (lift dcoll d1) =
      olift f d1.

    Lemma olift_lift_dcoll (f:list data -> option (list data)) (d1:option (list data)):
      olift (fun c1 : list data => lift dcoll (f c1)) d1 =
      lift dcoll (olift f d1).

    Lemma lift_dcoll_inversion d1 d2:
      d1 = d2 -> lift dcoll d1 = lift dcoll d2.

    Definition rondcoll (f:list data -> list data) (d:data) : option data :=
      lift dcoll (ondcoll f d).

    Lemma lift_dcoll_cons d l1 l2 :
      lift dcoll l1 = lift dcoll l2 ->
      lift dcoll (lift (fun t => d :: t) l1) = lift dcoll (lift (fun t => d :: t) l2).

    Lemma rondcoll2_dcoll f (l1 l2:list data):
      rondcoll2 f (dcoll l1) (dcoll l2) = Some (dcoll (f l1 l2)).
  
    Lemma rondcoll_dcoll f (l:list data):
      rondcoll f (dcoll l) = Some (dcoll (f l)).
  
    Lemma ondcoll_dcoll {A} (f:list data -> A) (l:list data):
      ondcoll f (dcoll l) = Some (f l).

    Lemma dcoll_map_app {A} (f:A -> data) (l1 l2:list A) :
      Some (dcoll (map f l1 ++ map f l2)) =
      rondcoll2 bunion (dcoll (map f l1)) (dcoll (map f l2)).

    Lemma lift_oncoll_ext {A : Type} (f g : list data -> option A) (d : data) :
      (forall a, d = dcoll a -> f a = g a) ->
      lift_oncoll f d = lift_oncoll g d.

End DataLift.

Global Hint Rewrite @rondcoll2_dcoll : alg.
Global Hint Rewrite @rondcoll_dcoll : alg.
Global Hint Rewrite @ondcoll_dcoll : alg.
Global Hint Rewrite @lift_oncoll_dcoll : alg.
Global Hint Rewrite @olift_on_lift_dcoll : alg.
Global Hint Rewrite @olift_lift_dcoll : alg.
Global Hint Rewrite @lift_map_id : alg.
Global Hint Rewrite @lift_map_map : alg.
Global Hint Rewrite @lift_dcoll_cons : alg.