Qcert.Basic.Typing.TDataSort

Section TDataSort.



  Context {fdata:foreign_data}.
  Context {ftype:foreign_type}.
  Context {fdtyping:foreign_data_typing}.
  Context {m:brand_model}.

  Definition sortable_type (τ : rtype) : Prop :=
    τ = Nat ∨ τ = String.

  Definition order_by_has_sortable_type
             (τr:list (string×rtype))
             (satts: list string) : Prop :=
    Forall (fun s ⇒
              ∀ τout, edot τr s = Some τout → sortable_type τout)
           satts.

  Lemma sortable_type_dec (τ : rtype) : {sortable_type τ} + {¬ sortable_type τ}.

  Definition order_by_has_sortable_type_dec
             (τr:list (string×rtype))
             (satts: list string) : {order_by_has_sortable_type τr satts} + {¬order_by_has_sortable_type τr satts}.

  Lemma order_by_has_sortable_type_sdd {τ sl a k pf1} :
    sublist (map fst sl) (domain τ) →
    order_by_has_sortable_type τ (map fst sl) →
    a ▹ Rec k τ pf1 →
    {x | sortable_data_of_data a sl = Some x ∧ snd x ▹ Rec k τ pf1}.

  Lemma order_by_well_typed
        (d1:data) (sl:list (string × SortDesc))
        {k τ} {pf1 pf2} :
    d1 ▹ Coll (Rec k τ pf1) →
    sublist (map fst sl) (domain τ) →
    order_by_has_sortable_type τ (map fst sl) →
    ∃ x, data_sort sl d1 = Some x ∧ x ▹ Coll (Rec k τ pf2).

End TDataSort.