Module Qcert.Data.Operators.SortBy

Require Import Orders.
Require Import Equivalence.
Require Import EquivDec.
Require Import Compare_dec.
Require Import Lia.
Require Import String.
Require Import List.
Require Import ZArith.
Require Import Utils.
Require Import ForeignData.
Require Import Data.
Require Import DataNorm.

Section SortBy.
  Context {fdata:foreign_data}.

  Definition sdata_of_data (d:data) : option sdata :=
    match d with
    | dnat n => Some (sdnat n)
    | dstring s => Some (sdstring s)
    | _ => None
    end.

  Definition data_of_sdata (d:sdata) : data :=
    match d with
    | sdnat n => dnat n
    | sdstring s => dstring s
    end.

  Lemma data_of_sdata_idem sd d :
    sdata_of_data d = Some sd <-> data_of_sdata sd = d.

Proof.

  Definition get_criteria (sc:SortCriteria) (r:list (string * data)) : option sdata :=
    let (att,sk) := sc in
    match edot r att with
    | Some d => sdata_of_data d
    | None => None
    end.

  Definition table_of_data (d:data) : option (list (list (string * data))):=
    match d with
    | dcoll coll =>
      lift_map (fun d =>
                  match d with
                  | drec r => Some r
                  | _ => None
                  end) coll
    | _ => None
    end.

  Definition data_of_table (t: list (list (string * data))) : data :=
    dcoll (map drec t).

  Definition data_sort
             (scl:list (list (string * data) -> option sdata))
             (d:data) : option data :=
    lift data_of_table (olift (table_sort scl) (table_of_data d)).

End SortBy.

Section SortByProps.
  Context {fdata:foreign_data}.

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

Proof.

  Lemma fsortable_data_of_data_snd_inv {A:Set} (l0: list (string * A))
        (s:list (list (string * A) -> option sdata)) (s0:sortable_data) :
    fsortable_data_of_data l0 s = Some s0 ->
    l0 = snd s0.

Proof.

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

Proof.

End SortByProps.