Module TOpsInfer

Section TOpsInfer.
  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 BasicRuntime.
  Require Import ForeignDataTyping.
  Require Import ForeignOpsTyping.
  Require Import TUtil.
  Require Import TData.
  Require Import TOps.
  Require Import TDataSort.

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

  Hint Rewrite Bottom_proj Top_proj Unit_proj Nat_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: ` _ = Bool₀ |- _ ] => apply Bool_canon in H
              | [H: ` _ = String₀ |- _ ] => apply String_canon in H
              | [H: ` _ = Coll₀ ?A |- _] =>
                match A with
                | ` _ => 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:binOp_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).

  Section b.

    Context {fbop:foreign_binary_op}.
    Context {fboptyping:foreign_binary_op_typing}.

    Definition infer_binop_type (b:binOp) (τ₁ τ₂:rtype) : option rtype :=
      match b with
      | AEq =>
        if (τ₁ == τ₂) then Some Bool else None
      | AConcat => trecConcat τ₁ τ₂
      | AMergeConcat => lift Coll (tmergeConcat τ₁ τ₂)
      | AAnd =>
        match (`τ₁, `τ₂) with
        | (Bool₀, Bool₀) => Some Bool
        | _ => None
        end
      | AOr =>
        match (`τ₁, `τ₂) with
        | (Bool₀, Bool₀) => Some Bool
        | _ => None
        end
      | ABArith _ =>
        match (`τ₁, `τ₂) with
        | (Nat₀, Nat₀) => Some Nat
        | _ => None
        end
      | ALt | ALe =>
        match (`τ₁, `τ₂) with
        | (Nat₀, Nat₀) => Some Bool
        | (_, _) => None
        end
      | AUnion | AMinus | AMin | AMax =>
        match (tuncoll τ₁, tuncoll τ₂) with
        | (Some τ₁₀, Some τ₂₀) =>
          if (`τ₁₀ == `τ₂₀) then Some τ₁ else None
        | _ => None
        end
      | AContains =>
        match tuncoll τ₂ with
        | Some τ₂₀ =>
          if (`τ₁ == `τ₂₀) then Some Bool else None
        | None => None
        end
      | ASConcat =>
        match (`τ₁, `τ₂) with
        | (String₀, String₀) => Some String
        | (_, _) => None
        end
      | AForeignBinaryOp fb =>
        foreign_binary_op_typing_infer fb τ₁ τ₂
      end.

    Lemma ATConcat_trec {τ₁ τ₂ τout} :
      trecConcat τ₁ τ₂ = Some τout ->
      binOp_type AConcat τ₁ τ₂ τout.
    
    Lemma ATMergeConcat_tmerge {τ₁ τ₂ τout} :
      tmergeConcat τ₁ τ₂ = Some τout ->
      binOp_type AMergeConcat τ₁ τ₂ (Coll τout).

    Theorem infer_binop_type_correct (b:binOp) (τ₁ τ₂ τout:rtype) :
      infer_binop_type b τ₁ τ₂ = Some τout ->
      binOp_type b τ₁ τ₂ τout.
  
    Theorem infer_binop_type_least {b:binOp} {τ₁ τ₂:rtype} {τout₁ τout₂:rtype} :
      infer_binop_type b τ₁ τ₂ = Some τout₁ ->
      binOp_type b τ₁ τ₂ τout₂ ->
      subtype τout₁ τout₂.

    Theorem infer_binop_type_complete {b:binOp} {τ₁ τ₂:rtype} (τout:rtype) :
      infer_binop_type b τ₁ τ₂ = None ->
      ~ binOp_type b τ₁ τ₂ τout.

  End b.


  Section u.
    Context {fuop:foreign_unary_op}.
    Context {fuoptyping:foreign_unary_op_typing}.
    
    Definition infer_unop_type (u:unaryOp) (τ₁:rtype) : option rtype :=
      match u with
      | AIdOp => Some τ₁
      | ANeg =>
        match `τ₁ with
        | Bool₀ => Some Bool
        | _ => None
        end
      | AColl => Some (Coll τ₁)
      | ASingleton => tsingleton τ₁
      | AFlatten =>
        match (tuncoll τ₁) with
        | Some τ₁₀ =>
          match tuncoll τ₁₀ with
          | Some _ => Some τ₁₀
          | _ => None
          end
        | None => None
        end
      | ADistinct =>
        olift (fun x => Some (Coll x)) (tuncoll τ₁)
      | AOrderBy sl =>
        match (tuncoll τ₁) with
        | Some τ₁₀ =>
          match tunrecsortable (List.map fst sl) τ₁₀ with
          | Some _ => Some τ₁
          | None => None
          end
        | None => None
        end
      | ARec s => Some (Rec Closed ((s, τ₁)::nil) eq_refl)
      | ADot s => tunrecdot s τ₁
      | ARecRemove s => tunrecremove s τ₁
      | ARecProject sl => tunrecproject sl τ₁
      | ACount =>
        match `τ₁ with
        | Coll₀ _ => Some Nat
        | _ => None
        end
      | ASum
      | ANumMin
      | ANumMax
      | AArithMean =>
        match `τ₁ with
        | Coll₀ Nat₀ => Some Nat
        | _ => None
        end
      | AToString => Some String
      | ASubstring _ _ =>
        match `τ₁ with
        | String₀ => Some String
        | _ => None
        end
      | ALike _ _ =>
        match `τ₁ with
        | String₀ => Some Bool
        | _ => None
        end
      | ALeft =>
        Some (Either τ₁ ⊥)
      | ARight =>
        Some (Either ⊥ τ₁)
      | ABrand b =>
        if (rtype_eq_dec τ₁ (brands_type b))
        then Some (Brand b)
        else None
      | AUnbrand =>
        match `τ₁ with
        | Brand₀ b => Some (brands_type b)
        | _ => None
        end
      | ACast b =>
        match `τ₁ with
        | Brand₀ _ => Some (Option (Brand b))
        | _ => None
        end
      | AUArith op =>
        match `τ₁ with
        | Nat₀ => Some Nat
        | _ => None
        end
      | AForeignUnaryOp fu =>
        foreign_unary_op_typing_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 ATDot_tunrec {s} {τ₁ τout} :
      tunrecdot s τ₁ = Some τout ->
      unaryOp_type (ADot s) τ₁ τout.

    Lemma ATRecRemove_tunrec {s} {τ₁ τout} :
      tunrecremove s τ₁ = Some τout ->
      unaryOp_type (ARecRemove s) τ₁ τout.

    Lemma ATRecProject_tunrec {sl} {τ₁ τout} :
      tunrecproject sl τ₁ = Some τout ->
      unaryOp_type (ARecProject sl) τ₁ τout.

    Lemma ATOrderBy_tunrec {sl} {τ₁ τout} :
      tunrecsortable (List.map fst sl) τ₁ = Some τout ->
      unaryOp_type (AOrderBy sl) (Coll τ₁) (Coll τ₁).

    Lemma ATSingleton_tsingleton {τ₁ τout} :
      tsingleton τ₁ = Some τout ->
      unaryOp_type ASingleton τ₁ τout.

    Lemma infer_unop_type_correct (u:unaryOp) (τ₁ τout:rtype) :
      infer_unop_type u τ₁ = Some τout ->
      unaryOp_type u τ₁ τout.

    Lemma infer_unop_type_least (u:unaryOp) (τ₁ τout₁ τout₂:rtype) :
      infer_unop_type u τ₁ = Some τout₁ ->
      unaryOp_type u τ₁ τout₂ ->
      subtype τout₁ τout₂.

    Lemma infer_unop_type_complete (u:unaryOp) (τ₁ τout:rtype) :
      infer_unop_type u τ₁ = None ->
      ~ unaryOp_type u τ₁ τout.

  End u.
    
End TOpsInfer.