Module TData

Section TData.
  Require Import String.
  Require Import List.
  Require Import Sumbool.
  Require Import Arith.
  Require Import Bool.
  Require Import Morphisms.
  Require Import Basics.

  Require Import BrandRelation.
  Require Import Utils Types BasicRuntime.
  Require Import ForeignDataTyping.


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

  Definition Rrec (r1 r2:(string*data)) :=
    ODT_lt_dec (fst r1) (fst r2).

  Inductive data_type : data -> rtype -> Prop :=
  | dttop d : data_normalized brand_relation_brands d -> data_type d Top
  | dtunit : data_type dunit Unit
  | dtnat n : data_type (dnat n) Nat
  | dtbool b : data_type (dbool b) Bool
  | dtstring s : data_type (dstring s) String
  | dtcoll dl r : Forall (fun d => data_type d r) dl ->
                  data_type (dcoll dl) (Coll r)
  | dtrec k dl rl rl_sub pf
          (pf':is_list_sorted ODT_lt_dec (domain rl) = true) :
      sublist rl_sub rl ->
      (k = Closed -> rl_sub = rl) ->
      Forall2
        (fun d r => (fst d) = (fst r) /\ data_type (snd d) (snd r))
        dl rl ->
      data_type (drec dl) (Rec k rl_sub pf)
  | dtleft {d τl} τr : data_type d τl -> data_type (dleft d) (Either τl τr)
  | dtright {d} τl {τr} : data_type d τr -> data_type (dright d) (Either τl τr)
  | dtbrand b b' d :
      is_canon_brands brand_relation_brands b ->
      data_normalized brand_relation_brands d ->
      Forall (fun bb =>
                forall τ,
                  lookup string_dec brand_context_types bb = Some τ ->
                  data_type d τ
                ) b ->
      b ≤ b' ->
      data_type (dbrand b d) (Brand b')
  | dtforeign {fd fτ} :
      foreign_data_typing_has_type fd fτ ->
      data_type (dforeign fd) (Foreign fτ)
  .
  
  Notation "d ▹ r" := (data_type d r) (at level 70).

  Section opt.

    Lemma dtsome {d τ} :
      data_type d τ ->
      data_type (dsome d) (Option τ).

    Lemma dtnone τ :
      data_type dnone (Option τ).

    Lemma dtsome_inv {d τ} :
      data_type (dsome d) (Option τ) ->
      data_type d τ.

  End opt.
  
  Lemma dtrec_closed_inv {dl rl pf} :
    data_type (drec dl) (Rec Closed rl pf) ->
    Forall2
      (fun d r => (fst d) = (fst r) /\ data_type (snd d) (snd r))
      dl rl.
  
  Lemma dtrec_full k {dl rl} pf:
       Forall2
         (fun d r => (fst d) = (fst r) /\ data_type (snd d) (snd r))
         dl rl ->
       data_type (drec dl) (Rec k rl pf).

  Lemma dtrec_open {dl : list (string*data)} {rl rl_sub : list (string*rtype)}
        pf (pf':is_list_sorted ODT_lt_dec (domain rl) = true) :
       sublist rl_sub rl ->
       Forall2
         (fun d r => (fst d) = (fst r) /\ data_type (snd d) (snd r))
         dl rl ->
       data_type (drec dl) (Rec Open rl_sub pf).

  Lemma dtrec_open_pf {dl : list (string*data)} {rl rl_sub : list (string*rtype)}
        (pf':is_list_sorted ODT_lt_dec (domain rl) = true) :
    forall (sub:sublist rl_sub rl),
       Forall2
         (fun d r => (fst d) = (fst r) /\ data_type (snd d) (snd r))
         dl rl ->
       data_type (drec dl) (Rec Open rl_sub (is_list_sorted_sublist pf' (sublist_domain sub))).

  Lemma dtrec_closed_is_open k dl rl pf :
    data_type (drec dl) (Rec Closed rl pf) ->
    data_type (drec dl) (Rec k rl pf).

  Lemma dtbrand_inv b b' d :
    data_type (dbrand b d) (Brand b') ->
      is_canon_brands brand_relation_brands b /\
      data_normalized brand_relation_brands d /\
      Forall (fun bb =>
                forall τ,
                  lookup string_dec brand_context_types bb = Some τ ->
                  data_type d τ
                ) b /\
      b ≤ b'.

  Lemma dtbrand_refl {b d}:
    is_canon_brands brand_relation_brands b ->
    data_normalized brand_relation_brands d ->
    Forall (fun bb =>
                forall τ,
                  lookup string_dec brand_context_types bb = Some τ ->
                  data_type d τ
           ) b ->
    data_type (dbrand b d) (Brand b).

  Lemma data_type_ext d τ₀ pf1 pf2:
    d ▹ (exist _ τ₀ pf1) <-> d ▹ (exist _ τ₀ pf2).

  Lemma data_type_fequal d τ₁ τ₂:
    (proj1_sig τ₁) = (proj1_sig τ₂) ->
    (d ▹ τ₁ <-> d ▹ τ₂).

  Lemma data_type_not_bottom {d} : d ▹ ⊥ -> False.
    
Section inv.

  Lemma data_type_dunit_inv {τ}:
    isTop τ = false ->
    dunit ▹ τ -> τ = Unit.

  Lemma data_type_dnat_inv {n τ}:
    isTop τ = false ->
    dnat n ▹ τ -> τ = Nat.

  Lemma data_type_dbool_inv {b τ}:
    isTop τ = false ->
    dbool b ▹ τ -> τ = Bool.

  Lemma data_type_dstring_inv {s τ}:
    isTop τ = false ->
    dstring s ▹ τ -> τ = String.

  Lemma data_type_dcoll_inv {d τ}:
    isTop τ = false ->
    dcoll d ▹ τ ->
    {τ' | τ = Coll τ'}.

  Lemma data_type_drec_inv {sdl τ}:
    isTop τ = false ->
    drec sdl ▹ τ ->
    {k : record_kind & {τ' | exists pf, τ = Rec k τ' pf}}.

  Lemma data_type_dleft_inv {d τ} :
    isTop τ = false ->
    dleft d ▹ τ ->
    {τl : rtype & {τr | τ = Either τl τr}}.

    Lemma data_type_dright_inv {d τ} :
    isTop τ = false ->
    dright d ▹ τ ->
    {τl : rtype & {τr | τ = Either τl τr}}.

  Lemma data_type_dsome_inv {d τ} :
    isTop τ = false ->
    dsome d ▹ τ ->
    {τl : rtype & {τr | τ = Either τl τr}}.

    Lemma data_type_dnone_inv {τ} :
    isTop τ = false ->
    dnone ▹ τ ->
    {τl : rtype & {τr | τ = Either τl τr}}.

  Lemma data_type_Unit_inv {d}:
    d ▹ Unit ->
    d = dunit.

  Lemma data_type_Nat_inv {d}:
    d ▹ Nat ->
    {n | d = dnat n}.

  Lemma data_type_Bool_inv {d}:
    d ▹ Bool ->
    {b | d = dbool b}.

  Lemma data_type_String_inv {d}:
    d ▹ String ->
    {s | d = dstring s}.

  Lemma data_type_Col_inv {d τ}:
    d ▹ Coll τ ->
    {dl | d = dcoll dl}.

  Lemma Col_inv {d τ}:
    dcoll d ▹ Coll τ ->
    Forall (fun c => c ▹ τ) d.

  Lemma data_type_Rec_inv {d k τ pf} :
    d ▹ Rec k τ pf ->
    {dl | d = drec dl}.

    Lemma data_type_Arrow_inv {d τin τout}:
    d ▹ Arrow τin τout ->
    False.

    Lemma data_type_Foreign_inv {d ft}:
    d ▹ Foreign ft ->
    {fd | d = dforeign fd}.

  Lemma data_type_Either_inv {d τl τr}:
    d ▹ Either τl τr ->
    {dl | d = dleft dl /\ dl ▹ τl} + {dr | d = dright dr /\ dr ▹ τr}.

    Lemma data_type_Option_inv {d τ}:
    d ▹ Option τ ->
    {ds | d = dsome ds /\ ds ▹ τ} + {d = dnone}.

    Lemma data_type_Brand_inv {d br} :
    d ▹ Brand br ->
    {bs:brands & {d' | d = dbrand bs d'}}.

End inv.

    Ltac data_type_inverter :=
  match goal with
    | [H: dunit ▹ ?τ, H1: isTop ?τ = false |- _ ] =>
      match τ with
        | Unit => fail 1
        | _ => generalize (data_type_dunit_inv H1 H); intros ?; try subst
      end
    | [H: dnat _ ▹ ?τ, H1: isTop ?τ = false |- _ ] =>
      match τ with
        | Nat => fail 1
        | _ => generalize (data_type_dnat_inv H1 H); intros ?; try subst
      end
    | [H: dbool _ ▹ ?τ, H1: isTop ?τ = false |- _ ] =>
      match τ with
        | Bool => fail 1
        | _ => generalize (data_type_dbool_inv H1 H); intros ?; try subst
      end
    | [H: dstring _ ▹ ?τ, H1: isTop ?τ = false |- _ ] =>
      match τ with
        | String => fail 1
        | _ => generalize (data_type_dstring_inv H1 H); intros ?; try subst
      end
    | [H: dcoll _ ▹ ?τ, H1: isTop ?τ = false |- _ ] =>
      match τ with
        | Coll _ => fail 1
        | _ => destruct (data_type_dcoll_inv H1 H); try subst
      end
    | [H: drec _ ▹ ?τ, H1: isTop ?τ = false |- _ ] =>
      match τ with
        | Rec _ _ => fail 1
        | _ => destruct (data_type_drec_inv H1 H) as [?[?[??]]]; try subst
      end
  end.

Lemma data_type_Rec_sublist {r k l l' pf} pf' :
      drec r ▹ Rec k l pf ->
      sublist l' l ->
      drec r ▹ Rec Open l' pf'.

Lemma sorted_forall_same_domain {dl τ}:
    Forall2 (fun (d : string * data) (r : string * rtype) =>
          fst d = fst r /\ data_type (snd d) (snd r)) dl τ ->
    (domain dl) = (domain τ).

Lemma data_type_Rec_domain {r k l pf} :
      drec r ▹ Rec k l pf ->
      sublist (domain l) (domain r).

Lemma data_type_Rec_closed_domain {r l pf} :
      drec r ▹ Rec Closed l pf ->
      domain r = domain l.

Lemma data_type_Recs_domain {r k l pf l' pf'} :
  drec r ▹ Rec k l pf ->
  drec r ▹ Rec Closed l' pf' ->
  sublist (domain l) (domain l').

Lemma data_type_Recs_closed_domain {r l l' pf pf'} :
  drec r ▹ Rec Closed l pf ->
  drec r ▹ Rec Closed l' pf' ->
  domain l = domain l'.

Lemma dtrec_edot_parts a k τ pf s x y:
  drec a ▹ Rec k τ pf ->
  edot a s = Some x ->
  edot τ s = Some y ->
  x ▹ y.

Lemma coll_type_cons a c x:
  dcoll (a :: c) ▹ Coll x ->
  a ▹ x /\ dcoll c ▹ Coll x.

Lemma dcoll_coll_in_inv {d τ a} :
  In a d -> dcoll d ▹ Coll τ -> a ▹ τ.

Lemma rec_type_closed_cons {x y l l' pf} pf':
  drec (x :: l) ▹ Rec Closed (y :: l') pf ->
  (snd x) ▹ (snd y) /\ drec l ▹ Rec Closed l' pf'.

Lemma rec_type_cons {k x y l l' pf} pf':
  drec (x :: l) ▹ Rec k (y :: l') pf ->
  ((fst x) = (fst y) /\ (snd x) ▹ (snd y) /\ drec l ▹ Rec k l' pf')
  \/ ((fst x) <> (fst y) /\ drec l ▹ Rec k (y::l') pf).
  
  Lemma sorted_forall_sorted (dl:list (string*data)) (τ:list (string*rtype)):
    is_list_sorted ODT_lt_dec (domain τ) = true ->
    Forall2 (fun (d : string * data) (r : string * rtype) =>
          fst d = fst r /\ data_type (snd d) (snd r)) dl τ ->
    is_list_sorted ODT_lt_dec (domain dl) = true.

  Lemma insert_and_foralls_mean_same_sort l1 l2 τ₁ τ₂ x y:
    is_list_sorted ODT_lt_dec (domain (rec_sort (τ₁ ++ τ₂))) = true ->
    Forall2
      (fun (d : string * data) (r : string * rtype) =>
         fst d = fst r /\ data_type (snd d) (snd r))
      (rec_sort (l1 ++ l2)) (rec_sort (τ₁ ++ τ₂)) ->
    (fst x = fst y) ->
    is_list_sorted
      ODT_lt_dec
      (domain
         (insertion_sort_insert rec_field_lt_dec y (rec_sort (τ₁ ++ τ₂)))) = true ->
    is_list_sorted
      ODT_lt_dec
      (domain
         (insertion_sort_insert rec_field_lt_dec x (rec_sort (l1 ++ l2)))) = true.

  Lemma sorted_cons_skip {A} (l:list (string*A)) (x x0:string*A) :
    is_list_sorted
      ODT_lt_dec
      (domain (rec_cons_sort x (x0 :: l))) = true
    -> is_list_sorted
         ODT_lt_dec
         (domain (rec_cons_sort x l)) = true.

  Lemma Forall2_cons_sorted l1 l2 x y :
    Forall2
      (fun (d : string * data) (r : string * rtype) =>
         fst d = fst r /\ data_type (snd d) (snd r))
      l1 l2 ->
    is_list_sorted ODT_lt_dec
                   (domain
                      (insertion_sort_insert rec_field_lt_dec x l1)) =
    true ->
    is_list_sorted ODT_lt_dec
                   (domain
                      (insertion_sort_insert rec_field_lt_dec y l2)) =
    true -> fst x = fst y -> data_type (snd x) (snd y) ->
    Forall2
      (fun (d : string * data) (r : string * rtype) =>
         fst d = fst r /\ data_type (snd d) (snd r))
      (insertion_sort_insert rec_field_lt_dec x l1)
      (insertion_sort_insert rec_field_lt_dec y l2).

  Lemma dtrec_rec_concat_sort {x xt pfx y yt pfy} pxyt :
    drec x ▹ Rec Closed xt pfx ->
    drec y ▹ Rec Closed yt pfy ->
    drec (rec_concat_sort x y) ▹ Rec Closed (rec_concat_sort xt yt) pxyt.
  
  Lemma dttop' d : data_normalized brand_relation_brands d -> d ▹ ⊤.
  Hint Resolve dttop dttop'.

  Lemma Forall_map {A B} P (f:A->B) l :
    Forall P (map f l) <-> Forall (fun x => P (f x)) l.

  Lemma data_type_normalized d τ :
    d ▹ τ -> data_normalized brand_relation_brands d.

  Lemma normalize_preserves_type d τ :
    d ▹ τ -> normalize_data brand_relation_brands d ▹ τ.
  
  Lemma dttop_weaken {d τ} : data_type d τ -> data_type d ⊤.

End TData.

Notation "d ▹ r" := (data_type d r) (at level 70).

Ltac dtype_inverter
  := repeat progress
            match goal with
            | [H:?d ▹ Unit |- _ ] =>
              apply data_type_Unit_inv in H; try subst d
            | [H:?d ▹ Nat |- _ ] =>
              apply data_type_Nat_inv in H; destruct H; try subst d
            | [H:?d ▹ Bool |- _ ] =>
              apply data_type_Bool_inv in H; destruct H; try subst d
            | [H:?d ▹ String |- _ ] =>
              apply data_type_String_inv in H; destruct H; try subst d
            | [H:?d ▹ (Coll ?τ) |- _ ] =>
              match d with
              | dcoll ?d => fail 1
              | _ =>
                let XX := fresh in
                destruct (data_type_Col_inv H) as [XX ?];
                  (discriminate || (subst d; rename XX into d))
              end
            | [H:?d ▹ Arrow _ _ |- _ ] =>
              apply data_type_Arrow_inv in H; tauto
            | [H:?d ▹ (Foreign ?τ) |- _ ] =>
              match d with
              | dforeign _ => fail 1
              | _ =>
                let XX := fresh in
                destruct (data_type_Foreign_inv H) as [XX ?];
                  (discriminate || (subst d; rename XX into d))
              end
            | [H:?d ▹ (Brand _) |- _ ] =>
              match d with
              | dbrand _ _ => fail 1
              | _ =>
                let XX := fresh in
                destruct (data_type_Brand_inv H) as [? [XX ?]];
                  (discriminate || (subst d; rename XX into d))
              end
            | [H:?d ▹ (Rec ?k ?τ ?pf) |- _ ] =>
              match d with
              | drec _ => fail 1
              | _ =>
                let XX := fresh in
                destruct (data_type_Rec_inv H) as [XX ?];
                  (discriminate || (subst d; rename XX into d))
              end
            | [H:?d ▹ Bool |- _ ] =>
                let XX := fresh in
                destruct (data_type_Bool_inv H) as [XX ?]; try subst d; clear H;
                rename XX into d
            | [H:proj1_sig _ =
                 Rec₀ Closed
                   (map
                      (fun x : string * {τ₀ : rtype₀ | wf_rtype₀ τ₀ = true} =>
                         (fst x, proj1_sig (snd x))) _) |- _ ]
              => apply Rec₀_eq_proj1_Rec in H; destruct H as [??]
            end; simpl.

  Ltac dtype_inverter_with_either
    := repeat progress
              try dtype_inverter;
      try match goal with
            | [H:?d ▹ (Either _ _) |- _ ] =>
              match d with
                | dleft ?d => fail 1
                | dright ?d => fail 1
                | _ =>
                let XX := fresh in
                destruct (data_type_Either_inv H) as [[XX [??]]|[XX [??]]];
                  (discriminate || (subst d; rename XX into d))
              end
          end.

Ltac dtype_enrich :=
  match goal with
    | [H: In ?a ?l, H2: (dcoll ?l) ▹ (Coll ?τ) |- _ ] =>
      extend (dcoll_coll_in_inv H H2)
  end.

Hint Immediate dttop dttop'.
Hint Resolve dttop_weaken.

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

  Lemma rmap_concat_empty_right τ pf l:
    Forall (fun d : data => d ▹ Rec Closed τ pf) l ->
    (rmap_concat (fun _ : data => Some (dcoll (drec nil :: nil))) l) = Some l.
  
  Lemma rmap_concat_empty_left τ pf l:
    Forall (fun d : data => d ▹ Rec Closed τ pf) l ->
    (rmap_concat (fun _ : data => Some (dcoll l)) (drec nil::nil)) = Some l.
    
End rmap.

Section subtype.

  Lemma subtype_Rec_sublist_strengthen
        {fdata:foreign_data}
        {ftype:foreign_type}
        {fdtyping:foreign_data_typing}
        {m:brand_model} {dl rl srl k1 pf srl0 pf0 k2} :
  forall (f2:Forall2
         (fun (d : string * data) (r : string * rtype) =>
            fst d = fst r /\ data_type (snd d) (snd r)) dl rl)
         (subl:sublist srl rl)
         (subt:Rec k1 srl pf <: Rec k2 srl0 pf0)
         (pf3:is_list_sorted ODT_lt_dec (domain rl) = true)
         (ft:Forallt
        (fun ab : string * rtype =>
         forall (d : data) (τ₂ : rtype),
         snd ab <: τ₂ -> data_type d (snd ab) -> data_type d τ₂) srl),
  exists l2,
    Forall2
         (fun (d : string * data) (r : string * rtype) =>
            fst d = fst r /\ data_type (snd d) (snd r)) dl l2
    /\
    sublist srl0 l2.

Global Instance data_type_subtype_prop
       {fdata:foreign_data}
       {ftype:foreign_type}
       {fdtyping:foreign_data_typing}
       {m:brand_model} : Proper (eq ==> subtype ==> impl) (data_type).

  Global Instance data_type_subtype_prop'
         {fdata:foreign_data}
         {ftype:foreign_type}
         {fdtyping:foreign_data_typing}
         {m:brand_model} d : Proper (subtype ==> impl) (data_type d).

  Lemma join_preserves_data_type
        {fdata:foreign_data}
        {ftype:foreign_type}
        {fdtyping:foreign_data_typing}
        {m:brand_model} {d τ}:
    d ▹ τ -> forall τ₀, d ▹ (τ ⊔ τ₀).

  Theorem subtyping_preserves_data_type
          {fdata:foreign_data}
          {ftype:foreign_type}
          {fdtyping:foreign_data_typing}
          {m:brand_model} {d τ₁ τ₂}:
    d ▹ τ₁ -> τ₁ ≤ τ₂ -> d ▹ τ₂.

  Lemma map_rtype_meet_cons2_nin
        {ftype:foreign_type}
        {br:brand_relation} s x l1 l2 :
    ~ In s (domain l1) ->
    map_rtype_meet l1 ((s, x) :: l2)
    = map_rtype_meet l1 l2.

  Lemma lookup_diff_cons2_nin {A B C} dec s x (l1:list (A*B)) (l2:list (A*C)) :
    ~ In s (domain l1) ->
  lookup_diff dec l1 ((s, x) :: l2)
  = lookup_diff dec l1 l2.

  Lemma lookup_diff_sublist {A B C} (dec:forall a a':A, {a=a'} + {a<>a'})
        (l1:list (A*B)) (l2:list (A*C)):
    sublist (lookup_diff dec l1 l2) l1.
  
  Theorem meet_preserves_data_type
          {fdata:foreign_data}
          {ftype:foreign_type}
          {fdtyping:foreign_data_typing}
          {m:brand_model} {d τ₁ τ₂}:
    d ▹ τ₁ -> d ▹ τ₂ -> d ▹ (τ₁ ⊓ τ₂).

  Theorem meet_data_type_iff
          {fdata:foreign_data}
          {ftype:foreign_type}
          {fdtyping:foreign_data_typing}
          {m:brand_model} d τ₁ τ₂:
    d ▹ (τ₁ ⊓ τ₂) <-> (d ▹ τ₁ /\ d ▹ τ₂).
  
  Lemma brands_type_Forall
        {fdata:foreign_data}
        {ftype:foreign_type}
        {fdtyping:foreign_data_typing}
        {m:brand_model} d b :
    d ▹ (brands_type b)
     <->
     (data_normalized brand_relation_brands d /\
    Forall (fun bb =>
              forall τ,
                lookup string_dec brand_context_types bb = Some τ ->
                d ▹ τ
           ) b).

  Lemma dtbrand'
        {fdata:foreign_data}
        {ftype:foreign_type}
        {fdtyping:foreign_data_typing}
        {m:brand_model} b b' d:
      is_canon_brands brand_relation_brands b ->
      d ▹ (brands_type b) ->
      b ≤ b' ->
      data_type (dbrand b d) (Brand b').

  Lemma dtbrand'_inv
        {fdata:foreign_data}
        {ftype:foreign_type}
        {fdtyping:foreign_data_typing}
        {m:brand_model} b b' d:
    data_type (dbrand b d) (Brand b') ->
    is_canon_brands brand_relation_brands b /\
    d ▹ (brands_type b) /\
    b ≤ b'.
    
End subtype.

Hint Resolve data_type_normalized.