Module Qcert.Data.OperatorsTyping.TBinaryOperators

Require Import Bool.
Require Import String.
Require Import List.
Require Import ZArith.
Require Import Compare_dec.
Require Import Program.
Require Import RelationClasses.
Require Import EquivDec.
Require Import Utils.
Require Import Types.
Require Import DataModel.
Require Import ForeignData.
Require Import ForeignOperators.
Require Import ForeignDataTyping.
Require Import Operators.
Require Import TUtil.
Require Import TData.
Require Import ForeignOperatorsTyping.

Section TBinaryOperators.

  Context {fdata:foreign_data}.
  Context {foperators:foreign_operators}.
  Context {ftype:foreign_type}.
  Context {fdtyping:foreign_data_typing}.
  Context {h:brand_model}.
  Context {foptyping:foreign_operators_typing}.

  Section typ.
    Inductive binary_op_type: binary_op -> rtype -> rtype -> rtype -> Prop :=
    | type_OpEqual {τ} :
        binary_op_type OpEqual τ τ Bool
    | type_OpRecConcat {τ₁ τ₂ τ₃} pf1 pf2 pf3 :
        rec_concat_sort τ₁ τ₂ = τ₃ ->
        binary_op_type OpRecConcat
                       (Rec Closed τ₁ pf1) (Rec Closed τ₂ pf2)
                       (Rec Closed τ₃ pf3)
    | type_OpRecMerge_closed {τ₁ τ₂ τ₃} pf1 pf2 pf3 :
        merge_bindings τ₁ τ₂ = Some τ₃ ->
        binary_op_type OpRecMerge
                       (Rec Closed τ₁ pf1) (Rec Closed τ₂ pf2)
                       (Coll (Rec Closed τ₃ pf3))
    | type_OpRecMerge_open {τ₁ τ₂ τ₃} pf1 pf2 pf3 :
        merge_bindings τ₁ τ₂ = Some τ₃ ->
        binary_op_type OpRecMerge
                       (Rec Open τ₁ pf1) (Rec Open τ₂ pf2)
                       (Coll (Rec Open τ₃ pf3))
    | type_OpAnd :
        binary_op_type OpAnd Bool Bool Bool
    | type_OpOr :
        binary_op_type OpOr Bool Bool Bool
    | type_OpLt :
        binary_op_type OpLt Nat Nat Bool
    | type_OpLe :
        binary_op_type OpLe Nat Nat Bool
    | type_OpBagUnion {τ} :
        binary_op_type OpBagUnion (Coll τ) (Coll τ) (Coll τ)
    | type_OpBagDiff {τ} :
        binary_op_type OpBagDiff (Coll τ) (Coll τ) (Coll τ)
    | type_OpBagMin {τ} :
        binary_op_type OpBagMin (Coll τ) (Coll τ) (Coll τ)
    | type_OpBagMax {τ} :
        binary_op_type OpBagMax (Coll τ) (Coll τ) (Coll τ)
    | type_OpBagNth {τ} :
        binary_op_type OpBagNth (Coll τ) Nat (Option τ)
    | type_OpContains {τ} :
        binary_op_type OpContains τ (Coll τ) Bool
    | type_OpStringConcat :
        binary_op_type OpStringConcat String String String
    | type_OpStringJoin :
        binary_op_type OpStringJoin String (Coll String) String
    | type_OpNatBinary (b:nat_arith_binary_op) :
        binary_op_type (OpNatBinary b) Nat Nat Nat
    | type_OpFloatBinary (b:float_arith_binary_op) :
        binary_op_type (OpFloatBinary b) Float Float Float
    | type_OpFloatCompare (b:float_compare_binary_op) :
        binary_op_type (OpFloatCompare b) Float Float Bool
    | type_OpForeignBinary {fb τin₁ τin₂ τout} :
        foreign_operators_typing_binary_has_type fb τin₁ τin₂ τout ->
        binary_op_type (OpForeignBinary fb) τin₁ τin₂ τout.

  End typ.

  Tactic Notation "binary_op_type_cases" tactic(first) ident(c) :=
    first;
    [ Case_aux c "type_OpEqual"%string
    | Case_aux c "type_OpRecConcat"%string
    | Case_aux c "type_OpRecMerge_closed"%string
    | Case_aux c "type_OpRecMerge_open"%string
    | Case_aux c "type_OpAnd"%string
    | Case_aux c "type_OpOr"%string
    | Case_aux c "type_OpLt"%string
    | Case_aux c "type_OpLe"%string
    | Case_aux c "type_OpBagUnion"%string
    | Case_aux c "type_OpBagDiff"%string
    | Case_aux c "type_OpBagMin"%string
    | Case_aux c "type_OpBagMax"%string
    | Case_aux c "type_OpBagNth"%string
    | Case_aux c "type_OpContains"%string
    | Case_aux c "type_OpStringConcat"%string
    | Case_aux c "type_OpStringJoin"%string
    | Case_aux c "type_OpNatBinary"%string
    | Case_aux c "type_OpFloatBinary"%string
    | Case_aux c "type_OpFloatCompare"%string
    | Case_aux c "type_OpForeignBinary"%string].


  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 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).


  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.

  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_binary_op_yields_typed_data {τ₁ τ₂ τout} (d1 d2:data) (b:binary_op) :
    (d1 ▹ τ₁) -> (d2 ▹ τ₂) -> (binary_op_type b τ₁ τ₂ τout) ->
    (exists x, binary_op_eval brand_relation_brands b d1 d2 = 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)::nil)) 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)::nil)) a = Some b.
  
End TBinaryOperators.

Tactic Notation "binary_op_type_cases" tactic(first) ident(c) :=
  first;
  [ Case_aux c "type_OpEqual"%string
  | Case_aux c "type_OpRecConcat"%string
  | Case_aux c "type_OpRecMerge_closed"%string
  | Case_aux c "type_OpRecMerge_open"%string
  | Case_aux c "type_OpAnd"%string
  | Case_aux c "type_OpOr"%string
  | Case_aux c "type_OpLt"%string
  | Case_aux c "type_OpLe"%string
  | Case_aux c "type_OpBagUnion"%string
  | Case_aux c "type_OpBagDiff"%string
  | Case_aux c "type_OpBagMin"%string
  | Case_aux c "type_OpBagMax"%string
  | Case_aux c "type_OpBagNth"%string
  | Case_aux c "type_OpContains"%string
  | Case_aux c "type_OpStringConcat"%string
  | Case_aux c "type_OpStringJoin"%string
  | Case_aux c "type_OpNatBinary"%string
  | Case_aux c "type_OpFloatBinary"%string
  | Case_aux c "type_OpFloatCompare"%string
  | Case_aux c "type_OpForeignBinary"%string].