Module Qcert.Data.OperatorsTyping.TOperatorsInfer

Require Import String.
Require Import List.
Require Import Compare_dec.
Require Import Program.
Require Import Eqdep_dec.
Require Import Bool.
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.
Require Import TSortBy.
Require Import TUnaryOperators.
Require Import TBinaryOperators.

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

  Local Hint Rewrite Bottom_proj Top_proj Unit_proj Nat_proj Float_proj Bool_proj String_proj : type_canon.
    
  Definition tunrecsortable (sl:list string) (τ:rtype) : option rtype.

  Ltac destructer :=
    repeat progress
           (try
              match goal with
              | [H:context
                     [match ?p with
                      | exist _ _ _ => _
                      end] |- _] => destruct p
              | [H:context [match ?p with | _ => _ end] |- _ ] =>
                case_eq p; intros;
                repeat match goal with
                       | [H1: ?a = ?a |- _ ] => clear H1
                       | [H1: ?a = ?b |- _ ] => rewrite H1 in *
                       end
              | [H:Some _ = Some _ |- _ ] => inversion H; clear H
              | [H:ex _ |- _] => destruct H
              | [H:_ /\ _ |- _] => destruct H
              | [H:lift _ _ = Some _ |- _] => apply some_lift in H; destruct H
              | [H:lift _ _ = None |- _] => apply none_lift in H
                                                                 
              | [H:context [RecMaybe _ (rec_concat_sort _ _ )] |- _ ] => rewrite RecMaybe_rec_concat_sort in H
              | [H:RecMaybe _ _ = Some _ |- _ ] => apply RecMaybe_some_pf in H; destruct H
              | [H1:is_list_sorted StringOrder.lt_dec (domain ?l) = true,
                    H2:context[RecMaybe ?k ?l] |- _ ] =>
                rewrite (RecMaybe_pf_some _ _ H1) in H2
              | [H: tuncoll _ = _ |- _ ] => apply tuncoll_correct in H
              | [H: tsingleton _ = _ |- _ ] => apply tsingleton_correct in H
              | [H: tunrec _ = _ |- _ ] => apply tunrec_correct in H; destruct H

              | [H: ` _ = Bottom₀ |- _ ] => apply Bottom_canon in H
              | [H: ` _ = Brand₀ ?b |- _ ] => apply Brand_canon in H
              | [H: ` _ = Top₀ |- _ ] => apply Top_canon in H
              | [H: ` _ = Unit₀ |- _ ] => apply Unit_canon in H
              | [H: ` _ = Nat₀ |- _ ] => apply Nat_canon in H
              | [H: ` _ = Float₀ |- _ ] => apply Float_canon in H
              | [H: ` _ = Bool₀ |- _ ] => apply Bool_canon in H
              | [H: ` _ = String₀ |- _ ] => apply String_canon in H
              | [H: ` _ = Coll₀ ?A |- _] =>
                match A with
                | String₀ => apply Coll_String_inside in H
                | ` _ => apply Coll_canon in H
                | _ => destruct (Coll_inside _ _ H); subst; apply Coll_canon in H
                end
              | [H: ?a = ?a |- _ ] => clear H
              | [H: ?a = ?b |- _ ] => rewrite H in *
              | [H:binary_op_type _ _ _ _ |- _ ] => inversion H; clear H
              end; try autorewrite with type_canon in *; try unfold equiv, complement, rtype in *; simpl in *; try rtype_equalizer; try subst; try discriminate; try reflexivity).

  Context {foperators:foreign_operators}.
  Context {foptyping:foreign_operators_typing}.

  Section b.

    Definition infer_binary_op_type (b:binary_op) (τ₁ τ₂:rtype) : option rtype :=
      match b with
      | OpEqual =>
        if (τ₁ == τ₂) then Some Bool else None
      | OpRecConcat => trecConcat τ₁ τ₂
      | OpRecMerge => lift Coll (tmergeConcat τ₁ τ₂)
      | OpAnd =>
        match (`τ₁, `τ₂) with
        | (Bool₀, Bool₀) => Some Bool
        | _ => None
        end
      | OpOr =>
        match (`τ₁, `τ₂) with
        | (Bool₀, Bool₀) => Some Bool
        | _ => None
        end
      | OpLt | OpLe =>
        match (`τ₁, `τ₂) with
        | (Nat₀, Nat₀) => Some Bool
        | (_, _) => None
        end
      | OpBagUnion | OpBagDiff | OpBagMin | OpBagMax =>
        match (tuncoll τ₁, tuncoll τ₂) with
        | (Some τ₁₀, Some τ₂₀) =>
          if (`τ₁₀ == `τ₂₀) then Some τ₁ else None
        | _ => None
        end
      | OpBagNth =>
        match (tuncoll τ₁, `τ₂) with
        | (Some τ₁₀, Nat₀) =>
          Some (Option τ₁₀)
        | _ => None
        end
      | OpContains =>
        match tuncoll τ₂ with
        | Some τ₂₀ =>
          if (`τ₁ == `τ₂₀) then Some Bool else None
        | None => None
        end
      | OpStringConcat =>
        match (`τ₁, `τ₂) with
        | (String₀, String₀) => Some String
        | (_, _) => None
        end
      | OpStringJoin =>
        match (`τ₁, `τ₂) with
        | (String₀, Coll₀ String₀) => Some String
        | (_, _) => None
        end
      | OpNatBinary _ =>
        match (`τ₁, `τ₂) with
        | (Nat₀, Nat₀) => Some Nat
        | _ => None
        end
      | OpFloatBinary _ =>
        match (`τ₁, `τ₂) with
        | (Float₀, Float₀) => Some Float
        | _ => None
        end
      | OpFloatCompare _ =>
        match (`τ₁, `τ₂) with
        | (Float₀, Float₀) => Some Bool
        | _ => None
        end
      | OpForeignBinary fb =>
        foreign_operators_typing_binary_infer fb τ₁ τ₂
      end.

    Lemma infer_concat_trec {τ₁ τ₂ τout} :
      trecConcat τ₁ τ₂ = Some τout ->
      binary_op_type OpRecConcat τ₁ τ₂ τout.
    
    Lemma infer_merge_tmerge {τ₁ τ₂ τout} :
      tmergeConcat τ₁ τ₂ = Some τout ->
      binary_op_type OpRecMerge τ₁ τ₂ (Coll τout).

    Theorem infer_binary_op_type_correct (b:binary_op) (τ₁ τ₂ τout:rtype) :
      infer_binary_op_type b τ₁ τ₂ = Some τout ->
      binary_op_type b τ₁ τ₂ τout.
  
    Theorem infer_binary_op_type_least {b:binary_op} {τ₁ τ₂:rtype} {τout₁ τout₂:rtype} :
      infer_binary_op_type b τ₁ τ₂ = Some τout₁ ->
      binary_op_type b τ₁ τ₂ τout₂ ->
      subtype τout₁ τout₂.

    Theorem infer_binary_op_type_complete {b:binary_op} {τ₁ τ₂:rtype} (τout:rtype) :
      infer_binary_op_type b τ₁ τ₂ = None ->
      ~ binary_op_type b τ₁ τ₂ τout.

  End b.



  Section u.
    Definition infer_unary_op_type (u:unary_op) (τ₁:rtype) : option rtype :=
      match u with
      | OpIdentity => Some τ₁
      | OpNeg =>
        match `τ₁ with
        | Bool₀ => Some Bool
        | _ => None
        end
      | OpRec s => Some (Rec Closed ((s, τ₁)::nil) eq_refl)
      | OpDot s => tunrecdot s τ₁
      | OpRecRemove s => tunrecremove s τ₁
      | OpRecProject sl => tunrecproject sl τ₁
      | OpBag => Some (Coll τ₁)
      | OpSingleton => tsingleton τ₁
      | OpFlatten =>
        match (tuncoll τ₁) with
        | Some τ₁₀ =>
          match tuncoll τ₁₀ with
          | Some _ => Some τ₁₀
          | _ => None
          end
        | None => None
        end
      | OpDistinct =>
        olift (fun x => Some (Coll x)) (tuncoll τ₁)
      | OpOrderBy sl =>
        match (tuncoll τ₁) with
        | Some τ₁₀ =>
          match tunrecsortable (List.map fst sl) τ₁₀ with
          | Some _ => Some τ₁
          | None => None
          end
        | None => None
        end
      | OpCount =>
        match `τ₁ with
        | Coll₀ _ => Some Nat
        | _ => None
        end
      | OpToString | OpToText => Some String
      | OpLength =>
        match `τ₁ with
        | String₀ => Some Nat
        | _ => None
        end
      | OpSubstring _ _ =>
        match `τ₁ with
        | String₀ => Some String
        | _ => None
        end
      | OpLike _ =>
        match `τ₁ with
        | String₀ => Some Bool
        | _ => None
        end
      | OpLeft =>
        Some (Either τ₁ ⊥)
      | OpRight =>
        Some (Either ⊥ τ₁)
      | OpBrand b =>
        if (rtype_eq_dec τ₁ (brands_type b))
        then Some (Brand b)
        else None
      | OpUnbrand =>
        match `τ₁ with
        | Brand₀ b => Some (brands_type b)
        | _ => None
        end
      | OpCast b =>
        match `τ₁ with
        | Brand₀ _ => Some (Option (Brand b))
        | _ => None
        end
      | OpNatUnary op =>
        match `τ₁ with
        | Nat₀ => Some Nat
        | _ => None
        end
      | OpNatSum
      | OpNatMin
      | OpNatMax
      | OpNatMean =>
        match `τ₁ with
        | Coll₀ Nat₀ => Some Nat
        | _ => None
        end
      | OpFloatOfNat =>
        match `τ₁ with
        | Nat₀ => Some Float
        | _ => None
        end
      | OpFloatUnary op =>
        match `τ₁ with
        | Float₀ => Some Float
        | _ => None
        end
      | OpFloatTruncate =>
        match `τ₁ with
        | Float₀ => Some Nat
        | _ => None
        end
      | OpFloatSum
      | OpFloatMean
      | OpFloatBagMin
      | OpFloatBagMax =>
        match `τ₁ with
        | Coll₀ Float₀ => Some Float
        | _ => None
        end
      | OpForeignUnary fu =>
        foreign_operators_typing_unary_infer fu τ₁
      end.

    Lemma empty_domain_remove {A} (l:list (string * A)) (s:string):
      domain l = nil -> domain (rremove l s) = nil.
  
    Lemma sorted_rremove_done {A} (l:list (string*A)) (a:(string*A)) (s:string) :
      is_list_sorted ODT_lt_dec (domain (a::l)) = true ->
      StringOrder.lt s (fst a) ->
      domain (rremove (a :: l) s) = domain (a :: l).
    
    Lemma Forall_rremove {A} {a} {l:list (string * A)} :
      Forall (StringOrder.lt a) (domain l) ->
      forall s,
        Forall (StringOrder.lt a) (domain (rremove l s)).

    Lemma is_sorted_rremove {A} (l:list (string * A)) (s:string):
      is_list_sorted ODT_lt_dec (domain l) = true ->
      is_list_sorted ODT_lt_dec (domain (rremove l s)) = true.

    Lemma infer_dot_tunrec {s} {τ₁ τout} :
      tunrecdot s τ₁ = Some τout ->
      unary_op_type (OpDot s) τ₁ τout.

    Lemma infer_recremove_tunrec {s} {τ₁ τout} :
      tunrecremove s τ₁ = Some τout ->
      unary_op_type (OpRecRemove s) τ₁ τout.

    Lemma infer_recproject_tunrec {sl} {τ₁ τout} :
      tunrecproject sl τ₁ = Some τout ->
      unary_op_type (OpRecProject sl) τ₁ τout.

    Lemma infer_orderby_tunrec {sl} {τ₁ τout} :
      tunrecsortable (List.map fst sl) τ₁ = Some τout ->
      unary_op_type (OpOrderBy sl) (Coll τ₁) (Coll τ₁).

    Lemma infer_singleton_tsingleton {τ₁ τout} :
      tsingleton τ₁ = Some τout ->
      unary_op_type OpSingleton τ₁ τout.

    Lemma infer_unary_op_type_correct (u:unary_op) (τ₁ τout:rtype) :
      infer_unary_op_type u τ₁ = Some τout ->
      unary_op_type u τ₁ τout.

    Lemma infer_unary_op_type_least (u:unary_op) (τ₁ τout₁ τout₂:rtype) :
      infer_unary_op_type u τ₁ = Some τout₁ ->
      unary_op_type u τ₁ τout₂ ->
      subtype τout₁ τout₂.

    Lemma infer_unary_op_type_complete (u:unary_op) (τ₁ τout:rtype) :
      infer_unary_op_type u τ₁ = None ->
      ~ unary_op_type u τ₁ τout.

  End u.
    
End TOperatorsInfer.