Qcert.Basic.Typing.TOpsInfer

Section TOpsInfer.

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

  Definition tunrecsortable (sl:list string) (τ:rtype) : option rtype.

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