Module TOps

Section TOps.
  Require Import String List ZArith.
  Require Import Compare_dec.
  
  Require Import Utils Types BasicRuntime.
  Require Import ForeignDataTyping ForeignOpsTyping TUtil TData TDataSort.

  Require Import Program.


  Section u.
    Context {fdata:foreign_data}.
    Context {fuop:foreign_unary_op}.
    Context {ftype:foreign_type}.
    Context {fdtyping:foreign_data_typing}.
    Context {m:brand_model}.
    Context {fuoptyping:foreign_unary_op_typing}.

    Inductive unaryOp_type : unaryOp -> rtype -> rtype -> Prop :=
    | ATIdOp τ : unaryOp_type AIdOp τ τ
    | ATNeg: unaryOp_type ANeg Bool Bool
    | ATColl {τ} : unaryOp_type AColl τ (Coll τ)
    | ATSingleton τ :
        unaryOp_type ASingleton (Coll τ) (Option τ)
    | ATFlatten τ: unaryOp_type AFlatten (Coll (Coll τ)) (Coll τ)
    | ATDistinct τ: unaryOp_type ADistinct (Coll τ) (Coll τ)
    | ATOrderBy {τ} k sl pf1 pf2:
        sublist (List.map fst sl) (domain τ) ->
        order_by_has_sortable_type τ (List.map fst sl) ->
        unaryOp_type (AOrderBy sl) (Coll (Rec k τ pf1)) (Coll (Rec k τ pf2))
    | ATRec {τ} s pf : unaryOp_type (ARec s) τ (Rec Closed ((s,τ)::nil) pf)
    | ATDot {τ' τout} k s pf :
        tdot τ' s = Some τout ->
        unaryOp_type (ADot s) (Rec k τ' pf) τout
    | ATRecRemove {τ} k s pf1 pf2 :
        unaryOp_type (ARecRemove s) (Rec k τ pf1) (Rec k (rremove τ s) pf2)
    | ATRecProject {τ} k sl pf1 pf2 :
        sublist sl (domain τ) ->
        unaryOp_type (ARecProject sl) (Rec k τ pf1) (Rec Closed (rproject τ sl) pf2)
    | ATCount τ: unaryOp_type ACount (Coll τ) Nat
    | ATSum : unaryOp_type ASum (Coll Nat) Nat
    | ATNumMin : unaryOp_type ANumMin (Coll Nat) Nat
    | ATNumMax : unaryOp_type ANumMax (Coll Nat) Nat
    | ATArithMean : unaryOp_type AArithMean (Coll Nat) Nat
    | ATToString τ: unaryOp_type AToString τ String
    | ATSubstring start olen: unaryOp_type (ASubstring start olen) String String
    | ATLike pat oescape: unaryOp_type (ALike pat oescape) String Bool
    | ATLeft τl τr: unaryOp_type ALeft τl (Either τl τr)
    | ATRight τl τr: unaryOp_type ARight τr (Either τl τr)
    | ATBrand b :
        unaryOp_type (ABrand b) (brands_type b) (Brand b)
    | ATUnbrand {bs} :
        unaryOp_type AUnbrand (Brand bs) (brands_type bs)
    | ATCast br {bs} :
        unaryOp_type (ACast br) (Brand bs) (Option (Brand br))
    | ATUArith (u:ArithUOp) : unaryOp_type (AUArith u) Nat Nat
    | ATForeignUnaryOp {fu τin τout} :
        foreign_unary_op_typing_has_type fu τin τout ->
        unaryOp_type (AForeignUnaryOp fu) τin τout.
  End u.

  Tactic Notation "unaryOp_type_cases" tactic(first) ident(c) :=
  first;
    [ Case_aux c "ATIdOp"%string
    | Case_aux c "ATNeg"%string
    | Case_aux c "ATColl"%string
    | Case_aux c "ATSingleton"%string
    | Case_aux c "ATFlatten"%string
    | Case_aux c "ATDistinct"%string
    | Case_aux c "ATOrderBy"%string
    | Case_aux c "ATRec"%string
    | Case_aux c "ATDot"%string
    | Case_aux c "ATRecRemove"%string
    | Case_aux c "ATRecProject"%string
    | Case_aux c "ATCount"%string
    | Case_aux c "ATSum"%string
    | Case_aux c "ATNumMin"%string
    | Case_aux c "ATNumMax"%string
    | Case_aux c "ATArithMean"%string
    | Case_aux c "ATToString"%string
    | Case_aux c "ATSubstring"%string
    | Case_aux c "ATLike"%string
    | Case_aux c "ATLeft"%string
    | Case_aux c "ATRight"%string
    | Case_aux c "ATBrand"%string
    | Case_aux c "ATUnbrand"%string
    | Case_aux c "ATCast"%string
    | Case_aux c "ATUArith"%string
    | Case_aux c "ATForeignUnaryOp"%string].


  Section b.

    Context {fdata:foreign_data}.
    Context {fbop:foreign_binary_op}.
    Context {ftype:foreign_type}.
    Context {fdtyping:foreign_data_typing}.
    Context {m:brand_model}.
    Context {fboptyping:foreign_binary_op_typing}.
    
    Inductive binOp_type: binOp -> rtype -> rtype -> rtype -> Prop :=
    | ATEq {τ} : binOp_type AEq τ τ Bool
    | ATConcat {τ₁ τ₂ τ₃} pf1 pf2 pf3 :
        rec_concat_sort τ₁ τ₂ = τ₃ ->
        binOp_type AConcat (Rec Closed τ₁ pf1) (Rec Closed τ₂ pf2) (Rec Closed τ₃ pf3)
    | ATMergeConcat {τ₁ τ₂ τ₃} pf1 pf2 pf3 :
        merge_bindings τ₁ τ₂ = Some τ₃ ->
        binOp_type AMergeConcat (Rec Closed τ₁ pf1) (Rec Closed τ₂ pf2) (Coll (Rec Closed τ₃ pf3))
    | ATMergeConcatOpen {τ₁ τ₂ τ₃} pf1 pf2 pf3 :
        merge_bindings τ₁ τ₂ = Some τ₃ ->
        binOp_type AMergeConcat (Rec Open τ₁ pf1) (Rec Open τ₂ pf2) (Coll (Rec Open τ₃ pf3))
    | ATAnd : binOp_type AAnd Bool Bool Bool
    | ATOr : binOp_type AOr Bool Bool Bool
    | ATBArith (b:ArithBOp) : binOp_type (ABArith b) Nat Nat Nat
    | ATLt : binOp_type ALt Nat Nat Bool
    | ATLe : binOp_type ALe Nat Nat Bool
    | ATUnion {τ} : binOp_type AUnion (Coll τ) (Coll τ) (Coll τ)
    | ATMinus {τ} : binOp_type AMinus (Coll τ) (Coll τ) (Coll τ)
    | ATMin {τ} : binOp_type AMin (Coll τ) (Coll τ) (Coll τ)
    | ATMax {τ} : binOp_type AMax (Coll τ) (Coll τ) (Coll τ)
    | ATContains {τ} : binOp_type AContains τ (Coll τ) Bool
    | ATSConcat : binOp_type ASConcat String String String
    | ATForeignBinaryOp {fb τin₁ τin₂ τout} :
        foreign_binary_op_typing_has_type fb τin₁ τin₂ τout ->
        binOp_type (AForeignBinaryOp fb) τin₁ τin₂ τout
    .
  End b.

  Tactic Notation "binOp_type_cases" tactic(first) ident(c) :=
    first;
    [ Case_aux c "ATEq"%string
    | Case_aux c "ATConcat"%string
    | Case_aux c "ATMergeConcat"%string
    | Case_aux c "ATMergeConcatOpen"%string
    | Case_aux c "ATAnd"%string
    | Case_aux c "ATOr"%string
    | Case_aux c "ATBArith"%string
    | Case_aux c "ATLt"%string
    | Case_aux c "ATLe"%string
    | Case_aux c "ATUnion"%string
    | Case_aux c "ATMinus"%string
    | Case_aux c "ATMin"%string
    | Case_aux c "ATMax"%string
    | Case_aux c "ATContains"%string
    | Case_aux c "ATSConcat"%string
    | Case_aux c "ATForeignBinaryOp"%string].

    Context {fdata:foreign_data}.
    Context {fuop:foreign_unary_op}.
    Context {fbop:foreign_binary_op}.
    Context {ftype:foreign_type}.
    Context {fdtyping:foreign_data_typing}.
    Context {h:brand_model}.
    Context {fuoptyping:foreign_unary_op_typing}.
    Context {fboptyping:foreign_binary_op_typing}.

  Lemma forall_typed_bunion {τ} d1 d2:
    Forall (fun d : data => data_type d τ) d1 ->
    Forall (fun d : data => data_type d τ) d2 ->
    Forall (fun d : data => data_type d τ) (bunion d1 d2).

  Lemma bminus_in_remove (x a:data) (d1 d2:list data) :
    In x (bminus d1 (remove_one a d2)) -> In x (bminus d1 d2).
    
  Lemma forall_typed_bminus {τ} d1 d2:
    Forall (fun d : data => data_type d τ) d1 ->
    Forall (fun d : data => data_type d τ) d2 ->
    Forall (fun d : data => data_type d τ) (bminus d1 d2).

  Lemma forall_typed_bmin {τ} d1 d2:
    Forall (fun d : data => data_type d τ) d1 ->
    Forall (fun d : data => data_type d τ) d2 ->
    Forall (fun d : data => data_type d τ) (bmin d1 d2).

  Lemma forall_typed_bmax {τ} d1 d2:
    Forall (fun d : data => data_type d τ) d1 ->
    Forall (fun d : data => data_type d τ) d2 ->
    Forall (fun d : data => data_type d τ) (bmax d1 d2).

  Lemma forall_in_weaken {A} (P Q:A -> Prop) l:
    (forall x : A, P x \/ In x l -> Q x)
    -> (forall x : A, In x l -> Q x).
  
  Lemma forall_typed_bdistinct {τ} d1:
    Forall (fun d : data => data_type d τ) d1 ->
    Forall (fun d : data => data_type d τ) (bdistinct d1).

  Lemma Forall2_lookupr_none (l : list (string * data)) (l' : list (string * rtype)) (s:string):
    (Forall2
       (fun (d : string * data) (r : string * rtype) =>
          fst d = fst r /\ data_type (snd d) (snd r)) l l') ->
    assoc_lookupr ODT_eqdec l' s = None ->
    assoc_lookupr ODT_eqdec l s = None.

  Lemma Forall2_lookupr_some (l : list (string * data)) (l' : list (string * rtype)) (s:string) (d':rtype):
    (Forall2
       (fun (d : string * data) (r : string * rtype) =>
          fst d = fst r /\ data_type (snd d) (snd r)) l l') ->
    assoc_lookupr ODT_eqdec l' s = Some d' ->
    (exists d'', assoc_lookupr ODT_eqdec l s = Some d'' /\ data_type d'' d').

  Lemma rec_concat_with_drec_concat_well_typed dl dl0 τ₁ τ₂:
    is_list_sorted ODT_lt_dec (domain τ₁) = true ->
    is_list_sorted ODT_lt_dec (domain τ₂) = true ->
      is_list_sorted ODT_lt_dec (domain (rec_concat_sort τ₁ τ₂)) = true ->
      Forall2
        (fun (d : string * data) (r : string * rtype) =>
           fst d = fst r /\ data_type (snd d) (snd r)) dl τ₁ ->
      Forall2
        (fun (d : string * data) (r : string * rtype) =>
           fst d = fst r /\ data_type (snd d) (snd r)) dl0 τ₂ ->
      Forall2
        (fun (d : string * data) (r : string * rtype) =>
           fst d = fst r /\ data_type (snd d) (snd r)) (rec_sort (dl ++ dl0))
        (rec_concat_sort τ₁ τ₂).

  Lemma concat_well_typed {τ₁ τ₂ τ₃} d1 d2 pf1 pf2 pf3:
    rec_concat_sort τ₁ τ₂ = τ₃ ->
    data_type d1 (Rec Closed τ₁ pf1) ->
    data_type d2 (Rec Closed τ₂ pf2) ->
    exists dl dl0 d3,
      d1 = drec dl /\
      d2 = drec dl0 /\
      ((rec_sort (dl ++ dl0)) = d3) /\
      data_type (drec d3) (Rec Closed τ₃ pf3).

  Lemma rremove_well_typed τ s dl:
    Forall2
      (fun (d : string * data) (r : string * rtype) =>
         fst d = fst r /\ data_type (snd d) (snd r)) dl τ ->
    Forall2
      (fun (d : string * data) (r : string * rtype) =>
         fst d = fst r /\ data_type (snd d) (snd r)) (rremove dl s)
      (rremove τ s).

  Lemma rproject_well_typed τ rl s dl:
    Forall2
      (fun (d : string * data) (r : string * rtype) =>
         fst d = fst r /\ data_type (snd d) (snd r)) dl rl ->
    sublist s (domain τ) ->
    sublist τ rl ->
    is_list_sorted ODT_lt_dec (domain τ) = true ->
    is_list_sorted ODT_lt_dec (domain rl) = true ->
    Forall2
      (fun (d : string * data) (r : string * rtype) =>
         fst d = fst r /\ data_type (snd d) (snd r)) (rproject dl s)
      (rproject τ s).
  

  Require Import RelationClasses EquivDec.
  Existing Instance rec_field_lt_strict.

  Definition mapTopNotSub s l2 (l:list (string*rtype)) :=
    map (fun xy => (fst xy, if in_dec string_dec (fst xy) s
                            then snd xy
                            else match lookup string_dec l2 (fst xy) with
                                   | Some y' => y'
                                   | None => Top
                                 end
                   )) l.

  Lemma mapTopNotSub_domain s l2 l :
    domain (mapTopNotSub s l2 l) = domain l.
  
  Lemma mapTopNotSub_in {s l x} l2:
    In (fst x) s -> In x l -> In x (mapTopNotSub s l2 l).

  Lemma mapTopNotSub_in2 {s l x y} l2:
      ~ In x s -> In x (domain l) -> lookup string_dec l2 x = Some y -> In (x,y) (mapTopNotSub s l2 l).

    Lemma in_mapTopNotSub {s l x} l2:
    In (fst x) s -> In x (mapTopNotSub s l2 l) -> In x l.
    
  Lemma mapTopNotSub_in_sublist {s l x} l2 :
    sublist s l ->
      In x s -> In x (mapTopNotSub (domain s) l2 l).
    
  Lemma mapTopNotSub_sublist {s l s'} l2:
    sublist s l ->
    sublist s s' ->
    sublist s (mapTopNotSub (domain s') l2 l).

  Lemma mapTopNotSub_sublist_same {s l} l2:
    sublist s l ->
    sublist s (mapTopNotSub (domain s) l2 l).
  

  Lemma mapTopNotSub_in_inv {s l2 l x} :
    In x (mapTopNotSub s l2 l) ->
    (In (fst x) s /\ In x l) \/
    (~ In (fst x) s /\
     (In x l2 \/
      (~ In (fst x) (domain l2) /\ snd x = Top))).

  Lemma mapTopNotSub_compatible {t1 t2} rl1 rl2 :
    NoDup (domain rl1) -> NoDup (domain rl2) ->
    sublist t1 rl1 ->
    sublist t2 rl2 ->
  compatible t1 t2 = true ->
    compatible (mapTopNotSub (domain t1) t2 rl1)
               (mapTopNotSub (domain t2) t1 rl2) = true.

  Require Import Bool.

  Lemma Forall2_compat_mapTopNotSub {x x0 rl rl0 t2} t1:
    is_list_sorted ODT_lt_dec (domain rl) = true ->
    is_list_sorted ODT_lt_dec (domain rl0) = true ->
    sublist t2 rl0 ->
    Forall2 (fun (d : string * data) (r : string * rtype) =>
                fst d = fst r /\ snd d ▹ snd r) x rl ->
        Forall2 (fun (d : string * data) (r : string * rtype) =>
                fst d = fst r /\ snd d ▹ snd r) x0 rl0 ->
        compatible x x0 = true ->
        Forall2
          (fun (d : string * data) (r : string * rtype) =>
             fst d = fst r /\ snd d ▹ snd r) x (mapTopNotSub t1 t2 rl).

  Lemma Forall2_compat_app_strengthen {x x0 rl rl0 t1 t2}:
    is_list_sorted ODT_lt_dec (domain rl) = true ->
    is_list_sorted ODT_lt_dec (domain rl0) = true ->
    sublist t1 rl ->
    sublist t2 rl0 ->
    compatible t1 t2 = true ->
    Forall2 (fun (d : string * data) (r : string * rtype) =>
                fst d = fst r /\ snd d ▹ snd r) x rl ->
        Forall2 (fun (d : string * data) (r : string * rtype) =>
                fst d = fst r /\ snd d ▹ snd r) x0 rl0 ->
        compatible x x0 = true ->
        exists rl' rl0',
          compatible rl' rl0' = true /\
          sublist t1 rl' /\
          sublist t2 rl0' /\
          Forall2 (fun (d : string * data) (r : string * rtype) =>
                      fst d = fst r /\ snd d ▹ snd r) x rl' /\
          Forall2 (fun (d : string * data) (r : string * rtype) =>
                      fst d = fst r /\ snd d ▹ snd r) x0 rl0'.

  Lemma sorted_sublists_sorted_concat (τ₁ τ₂ rl rl0:list (string*rtype)):
    is_list_sorted ODT_lt_dec (domain τ₁) = true ->
    is_list_sorted ODT_lt_dec (domain τ₂) = true ->
    is_list_sorted ODT_lt_dec (domain rl) = true ->
    is_list_sorted ODT_lt_dec (domain rl0) = true ->
    compatible rl rl0 = true ->
    sublist τ₁ rl ->
    sublist τ₂ rl0 ->
    sublist (rec_sort (τ₁ ++ τ₂)) (rec_sort (rl ++ rl0)).

  Lemma typed_binop_yields_typed_data {τ₁ τ₂ τout} (d1 d2:data) (b:binOp) :
    (d1 ▹ τ₁) -> (d2 ▹ τ₂) -> (binOp_type b τ₁ τ₂ τout) ->
    (exists x, fun_of_binop brand_relation_brands b d1 d2 = Some x /\ x ▹ τout).

  Definition canon_brands_alt {br:brand_relation} (b:brands) :=
    fold_right meet [] (map (fun x => x::nil) b).

  Lemma canon_brands_alt_is_canon {br:brand_relation} (b:brands) :
    is_canon_brands brand_relation_brands (canon_brands_alt b).

  Lemma canon_brands_fold_right_hoist {br:brand_relation} (l:list brands) :
    fold_right
      (fun a b : brands => canon_brands brand_relation_brands (a ++ b))
      [] l =
    canon_brands brand_relation_brands
                 (fold_right (fun a b : brands => (a ++ b))
                             [] l).
  
  Lemma canon_brands_alt_equiv {br:brand_relation} (b:brands) :
    canon_brands brand_relation_brands b
    = canon_brands_alt b.

  Require Import Permutation.

  Lemma typed_unop_yields_typed_data {τ₁ τout} (d1:data) (u:unaryOp) :
    (d1 ▹ τ₁) -> (unaryOp_type u τ₁ τout) ->
    (exists x, fun_of_unaryop brand_relation_brands u d1 = Some x /\ x ▹ τout).


  Lemma tdot_rec_concat_sort_neq {A} (l:list (string*A)) a b xv :
       a <> b ->
       tdot (rec_concat_sort l [(a, xv)]) b =
       tdot (rec_sort l) b.

  Lemma tdot_rec_concat_sort_eq {A} (l : list (string * A)) a b :
               ~ In a (domain l) ->
               tdot (rec_concat_sort l [(a, b)]) a = Some b.
  
End TOps.

  Tactic Notation "unaryOp_type_cases" tactic(first) ident(c) :=
  first;
    [ Case_aux c "ATIdOp"%string
    | Case_aux c "ATNeg"%string
    | Case_aux c "ATColl"%string
    | Case_aux c "ATSingleton"%string
    | Case_aux c "ATFlatten"%string
    | Case_aux c "ATDistinct"%string
    | Case_aux c "ATOrderBy"%string
    | Case_aux c "ATRec"%string
    | Case_aux c "ATDot"%string
    | Case_aux c "ATRecRemove"%string
    | Case_aux c "ATRecProject"%string
    | Case_aux c "ATCount"%string
    | Case_aux c "ATSum"%string
    | Case_aux c "ATNumMin"%string
    | Case_aux c "ATNumMax"%string
    | Case_aux c "ATArithMean"%string
    | Case_aux c "ATToString"%string
    | Case_aux c "ATSubstring"%string
    | Case_aux c "ATLike"%string
    | Case_aux c "ATLeft"%string
    | Case_aux c "ATRight"%string
    | Case_aux c "ATBrand"%string
    | Case_aux c "ATUnbrand"%string
    | Case_aux c "ATCast"%string
    | Case_aux c "ATUArith"%string
    | Case_aux c "ATForeignUnaryOp"%string].


  Tactic Notation "binOp_type_cases" tactic(first) ident(c) :=
    first;
    [ Case_aux c "ATEq"%string
    | Case_aux c "ATConcat"%string
    | Case_aux c "ATMergeConcat"%string
    | Case_aux c "ATMergeConcatOpen"%string
    | Case_aux c "ATAnd"%string
    | Case_aux c "ATOr"%string
    | Case_aux c "ATBArith"%string
    | Case_aux c "ATLt"%string
    | Case_aux c "ATLe"%string
    | Case_aux c "ATUnion"%string
    | Case_aux c "ATMinus"%string
    | Case_aux c "ATMin"%string
    | Case_aux c "ATMax"%string
    | Case_aux c "ATContains"%string
    | Case_aux c "ATSConcat"%string
    | Case_aux c "ATForeignBinaryOp"%string].