Module RDataSort

Require Import Orders.
Require Import Equivalence.
Require Import EquivDec.
Require Import Compare_dec.
Require Import Omega.
Require Import String RString.
Require Import List.
Require Import ZArith.

Section SortableData.
  Inductive SortDesc : Set := | Descending | Ascending.
  Definition SortCriteria : Set := string * SortDesc.
  Definition SortCriterias : Set := list SortCriteria.


  Inductive sdata :=
  | sdnat : Z -> sdata
  | sdstring : string -> sdata
  .

  Lemma sort_desc_eq_dec : forall x y:SortDesc, {x=y}+{x<>y}.
  
  Lemma sdata_eq_dec : forall x y:sdata, {x=y}+{x<>y}.

  Global Instance oql_eqdec : EqDec SortDesc eq := sort_desc_eq_dec.
    
  Global Instance sdata_eqdec : EqDec sdata eq := sdata_eq_dec.

End SortableData.

Module SortableDataOrder <: OrderedTypeFull with Definition t:=sdata.
  Definition t:=sdata.
  Definition eq := @eq t.
  Definition eq_equiv : (Equivalence eq) := eq_equivalence.
  Definition eq_dec := sdata_eq_dec.

  Definition compare (d1 d2:t) : comparison :=
    match d1,d2 with
    | sdnat n, sdstring s => Lt
    | sdstring s, sdnat n => Gt
    | sdnat n1, sdnat n2 => Z.compare n1 n2
    | sdstring s1, sdstring s2 => StringOrder.compare s1 s2
    end.

  Definition lt (d1 d2:sdata) : Prop
    := compare d1 d2 = Lt.

  Lemma compare_spec :
    forall x y : sdata,
      CompareSpec (eq x y) (lt x y) (lt y x) (compare x y).

  Lemma trichotemy a b : {lt a b} + {eq a b} + {lt b a}.

  Lemma compare_refl_eq a: compare a a = Eq.

  Lemma compare_eq_iff a b: compare a b = Eq <-> a = b.

  Instance lt_strorder : StrictOrder lt.

  Lemma lt_compat : Proper (eq ==> eq ==> iff) lt.

  Program Definition lt_dec (a b:sdata) : {lt a b} + {~lt a b}
    := match compare a b with
         | Lt => left _
         | Eq => right _
         | Gt => right _
       end.

  Definition le (a b:sdata) :=
    match compare a b with
      | Lt => True
      | Eq => True
      | Gt => False
    end.

  Lemma le_lteq : forall x y : t, le x y <-> lt x y \/ eq x y.

  Program Definition le_dec (a b:sdata) : {le a b} + {~le a b}
    := match compare a b with
         | Lt => left _
         | Eq => left _
         | Gt => right _
       end.

End SortableDataOrder.

Section LexicographicData.
  Lemma list_sdata_eq_dec : forall x y:list sdata, {x=y}+{x<>y}.

  Global Instance list_sdata_eqdec : EqDec (list sdata) eq := list_sdata_eq_dec.

End LexicographicData.

Module LexicographicDataOrder <: OrderedTypeFull with Definition t:=list sdata.
  Definition t := list sdata.
  Definition eq := @eq t.
  Definition eq_equiv : (Equivalence eq) := eq_equivalence.
  Definition eq_dec := list_sdata_eq_dec.

  Fixpoint compare (l1 l2:list sdata) : comparison :=
    match l1, l2 with
    | nil, nil => Eq
    | nil, _ :: _ => Lt
    | _ :: _, nil => Gt
    | d1 :: l1', d2 :: l2' =>
      match SortableDataOrder.compare d1 d2 with
      | Lt => Lt
      | Eq => compare l1' l2'
      | Gt => Gt
      end
    end.
  
  Definition lt (l1 l2:t) : Prop
    := compare l1 l2 = Lt.

  Lemma compare_spec :
    forall x y : t, CompareSpec (eq x y) (lt x y) (lt y x) (compare x y).
  
  Lemma trichotemy a b : {lt a b} + {eq a b} + {lt b a}.

  Lemma compare_refl_eq a: compare a a = Eq.

  Lemma compare_eq_iff a b: compare a b = Eq <-> a = b.

  Instance lt_strorder : StrictOrder lt.

  Lemma lt_compat : Proper (eq ==> eq ==> iff) lt.

  Program Definition lt_dec (a b:list sdata) : {lt a b} + {~lt a b}
    := match compare a b with
       | Lt => left _
       | Eq => right _
       | Gt => right _
       end.

  Definition le (a b:t) :=
    match compare a b with
      | Lt => True
      | Eq => True
      | Gt => False
    end.

  Lemma le_lteq : forall x y : t, le x y <-> lt x y \/ eq x y.

  Program Definition le_dec (a b:t) : {le a b} + {~le a b}
    := match compare a b with
         | Lt => left _
         | Eq => left _
         | Gt => right _
       end.

End LexicographicDataOrder.
  
Section DataSort.
  Require Import RSort.
  Require Import RData.
  Require Import RBindings.

  Global Program Instance ODT_lexdata : (@ODT (list sdata))
    := mkODT _ _ LexicographicDataOrder.lt
             LexicographicDataOrder.lt_strorder
             LexicographicDataOrder.lt_dec
             LexicographicDataOrder.compare _.

  Require Import RRelation.
  Require Import ForeignData.
  Context {fdata:foreign_data}.
  
  Definition theotherdot d s :=
    match d with
    | drec r => edot r s
    | _ => None
    end.
  

  Require Import RLift.
  Require Import RSort.

  Definition sortable_data : Set := (list sdata) * data.
  Definition sortable_coll : Set := list sortable_data.


  Definition dict_field_le {A} (a b:(list sdata)*A) :=
    LexicographicDataOrder.le (fst a) (fst b).

  Lemma dict_field_le_dec {A} (a b:(list sdata)*A) :
    {dict_field_le a b} + {~dict_field_le a b}.

  Definition dict_sort {A} :=
    @insertion_sort ((list sdata)*A) dict_field_le dict_field_le_dec.

  Definition sort_sortable_coll (sc:sortable_coll) : sortable_coll :=
    dict_sort sc.

  Definition coll_of_sortable_coll (sc:sortable_coll) : list data :=
    map snd sc.
  
  Example scoll1 :=
    ((sdnat 2::sdstring "a"::nil,dnat 10)
     :: (sdnat 3::sdstring "x"::nil,dnat 11)
     :: (sdnat 2::sdstring "b"::nil,dnat 12)
     :: (sdnat 2::sdstring "b"::nil,dnat 2000)
     :: (sdnat 1::sdstring "a"::nil,dnat 13)
       ::nil).

  
  Definition get_criteria (d:data) (sc:SortCriteria) : option sdata :=
    let (att,sk) := sc in
    match theotherdot d att with
    | Some (dnat n) => Some (sdnat n)
    | Some (dstring s) => Some (sdstring s)
    | Some _ => None
    | None => None
    end.

  Definition get_criterias (d:data) (scl:SortCriterias) : option (list sdata) :=
    lift_map (get_criteria d) scl.

  Definition sortable_data_of_data (d:data) (scl:SortCriterias) : option sortable_data :=
    lift (fun c => (c,d)) (get_criterias d scl).

  Definition sortable_coll_of_coll (scl:SortCriterias) (coll:list data) :
    option (list sortable_data)
    := lift_map (fun d => sortable_data_of_data d scl) coll.
  
  Definition data_sort (scl:SortCriterias) (d:data) : option data :=
    match d with
    | dcoll coll =>
      lift dcoll
           (lift coll_of_sortable_coll
                 (lift sort_sortable_coll
                       (sortable_coll_of_coll scl coll)))
    | _ => None
    end.

  Definition mkperson (name:string) (age:Z) (zip:Z) (company:string) :=
    drec (("name", dstring name)
          :: ("age", dnat age)
          :: ("zip", dnat zip)
          :: ("company", dstring company)
          :: nil)%string.
  Definition mkpersons_aux l :=
    map (fun x =>
           match x with (name, age, zip, company) => mkperson name age zip company
           end) l.
  Definition mkpersons l :=
    dcoll (mkpersons_aux l).

  Open Scope Z_scope.
  Definition persons :=
    mkpersons
      (("John",23,1008,"IBM")
         :: ("Jane",24,1009,"AIG")
         :: ("Jill",25,1010,"IBM")
         :: ("Jack",27,1010,"CMU")
         :: nil)%string.


End DataSort.

Section DataSortProps.
  Require Import RDataNorm.
  Require Import ForeignData.
  Require Import Utils.
  Context {fdata:foreign_data}.

  Lemma dict_field_le_anti :
    forall x y : sortable_data, ~ dict_field_le x y -> ~ dict_field_le y x -> x = y.

  Lemma in_sort_sortable d l :
    In d (sort_sortable_coll l) <-> In d l.
    
  Lemma in_csc_ssc d l :
    In d (coll_of_sortable_coll (sort_sortable_coll l)) <->
    In d (coll_of_sortable_coll l).

  Lemma in_csc_cons d s l :
      In d (coll_of_sortable_coll (s :: l)) <->
      (d = snd s \/ In d (coll_of_sortable_coll l)).

  Lemma sortable_data_normalized h a sc sd :
    data_normalized h a ->
    sortable_data_of_data a sc = Some sd ->
    data_normalized h (snd sd).

  Lemma data_sort_normalized h s (d sd:data) :
    data_sort s d = Some sd -> data_normalized h d -> data_normalized h sd.

End DataSortProps.