Qcert.DNNRC.Typing.TOpsInferSub

Section TOpsInferSub.

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

  Section b.

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

    Definition infer_binop_type_sub
               (b:binOp) (τ₁ τ₂:rtype) : option (rtype ×rtype ×rtype) :=
      match b with
      | AEq ⇒
        let τcommon := τ ₁ ⊔ τ ₂ in
        Some (Bool , τ common , τ common )
      | AConcat ⇒
        match τ ₁ ==b ⊥, τ ₂ ==b ⊥ with
        | true, true ⇒ Some (⊥, ⊥, ⊥)
        | true, false ⇒
           lift (fun _ ⇒ (τ ₂ , ⊥, τ ₂ )) (tunrec τ ₂)
        | false, true ⇒
           lift (fun _ ⇒ (τ ₁ , τ ₁ , ⊥)) (tunrec τ ₁)
        | false, false ⇒
          lift (fun τ ⇒ (τ , τ ₁ , τ ₂ )) (trecConcat τ ₁ τ ₂)
        end
      | AMergeConcat ⇒
        match τ ₁ ==b ⊥, τ ₂ ==b ⊥ with
        | true, true ⇒ Some (Coll ⊥, ⊥, ⊥)
        | true, false ⇒
           lift (fun _ ⇒ (Coll τ ₂ , ⊥, τ ₂ )) (tunrec τ ₂)
        | false, true ⇒
           lift (fun _ ⇒ (Coll τ ₁ , τ ₁ , ⊥)) (tunrec τ ₁)
        | false, false ⇒
          lift (fun τ ⇒ (Coll τ , τ ₁ , τ ₂ )) (tmergeConcat τ ₁ τ ₂)
        end
      | AAnd ⇒
        match subtype_dec τ ₁ Bool, subtype_dec τ ₂ Bool with
        | left _, left _ ⇒ Some (Bool , Bool , Bool )
        | _, _ ⇒ None
      end
      | AOr ⇒
        match subtype_dec τ ₁ Bool, subtype_dec τ ₂ Bool with
        | left _, left _ ⇒ Some (Bool , Bool , Bool )
        | _, _ ⇒ None
        end
      | ABArith _ ⇒
        match subtype_dec τ ₁ Nat, subtype_dec τ ₂ Nat with
        | left _, left _ ⇒ Some (Nat , Nat , Nat )
        | _, _ ⇒ None
        end
      | ALt
      | ALe ⇒
        match subtype_dec τ ₁ Nat, subtype_dec τ ₂ Nat with
        | left _, left _ ⇒ Some (Bool , Nat , Nat )
        | _, _ ⇒ None
        end
      | AUnion | AMinus | AMin | AMax ⇒
        let τcommon := τ ₁ ⊔ τ ₂ in
        if (tuncoll τ common)
        then Some (τ common , τ common , τ common )
        else None

      | AContains ⇒
        if τ ₂ ==b ⊥
        then Some (Bool , τ ₁ , τ ₂ )
        else lift (fun τ₂' ⇒
                     let τ := τ ₁ ⊔ τ ₂' in
                     (Bool , τ , Coll τ ))
                  (tuncoll τ ₂)
      | ASConcat ⇒
        match subtype_dec τ ₁ String, subtype_dec τ ₂ String with
        | left _, left _ ⇒ Some (String , String , String )
        | _, _ ⇒ None
        end
      | AForeignBinaryOp fb ⇒
        foreign_binary_op_typing_infer_sub fb τ ₁ τ ₂
      end.

  End b.

  Section u.
    Context {fuop:foreign_unary_op}.
    Context {fuoptyping:foreign_unary_op_typing}.

    Definition infer_unop_type_sub (u:unaryOp) (τ₁:rtype) : option (rtype ×rtype) :=
      match u with
      | AIdOp ⇒ Some (τ ₁ ,τ ₁ )
      | ANeg ⇒
        if subtype_dec τ ₁ Bool
        then Some (Bool , Bool )
        else None
      | AColl ⇒ Some (Coll τ ₁ ,τ ₁ )
      | ASingleton ⇒
        let τ₁' := τ ₁ ⊔ (Coll ⊥) in
        lift (fun τ ⇒ (τ , τ ₁')) (tsingleton τ ₁')
      | AFlatten ⇒
        let τ₁' := τ ₁ ⊔ (Coll (Coll ⊥)) in
        bind (tuncoll τ ₁')
             (fun τ₁in ⇒
                lift (fun _ ⇒ (τ ₁in , τ ₁'))
                     (tuncoll τ ₁in))
      | ADistinct ⇒
        let τ₁' := τ ₁ ⊔ (Coll ⊥) in
        lift (fun τ ⇒ (Coll τ , τ ₁')) (tuncoll τ ₁')
      | AOrderBy sl ⇒
        let τ₁' := τ ₁ ⊔ (Coll ⊥) in
        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 ⇒
        if τ ₁ == ⊥
        then Some (⊥, ⊥)
        else lift (fun τ ⇒ (τ , τ ₁ )) (tunrecdot s τ ₁)
      | ARecRemove s ⇒
        if τ ₁ == ⊥
        then Some (⊥, ⊥)
        else lift (fun τ ⇒ (τ , τ ₁ )) (tunrecremove s τ ₁)
      | ARecProject sl ⇒
        if τ ₁ == ⊥
        then Some (⊥, ⊥)
        else lift (fun τ ⇒ (τ , τ ₁ )) (tunrecproject sl τ ₁)
      | ACount ⇒
        let τ₁' := τ ₁ ⊔ (Coll ⊥) in
        lift (fun τ ⇒ (Nat , τ ₁')) (tuncoll τ ₁')
      | ASum
      | ANumMin
      | ANumMax
      | AArithMean ⇒
        if subtype_dec τ ₁ (Coll Nat)
        then Some (Nat , Coll Nat )
        else None
      | AToString ⇒
        Some (String , τ ₁ )
      | ASubstring _ _ ⇒
        if (subtype_dec τ ₁ String)
        then Some (String , String )
        else None
      | ALike _ _ ⇒
        if (subtype_dec τ ₁ String)
        then Some (Bool , String )
        else None
      | ALeft ⇒
        Some (Either τ ₁ ⊥, τ ₁ )
      | ARight ⇒
        Some (Either ⊥ τ ₁ , τ ₁ )
      | ABrand b ⇒
        if (subtype_dec τ ₁ (brands_type b))
        then Some (Brand b, τ ₁ )
        else None
    | AUnbrand ⇒
        if τ ₁ == ⊥
        then
          Some (⊥, ⊥)
        else
          match `τ ₁ with
          | Brand₀ b ⇒ Some (brands_type b, τ ₁ )
          | _ ⇒ None
          end
    | ACast b ⇒
      if τ ₁ == ⊥
      then
        Some (⊥, ⊥)
      else
        match `τ ₁ with
        | Brand₀ _ ⇒ Some (Option (Brand b), τ ₁ )
        | _ ⇒ None
        end
    | AUArith op ⇒
      if subtype_dec τ ₁ Nat
      then Some (Nat , Nat )
      else None
    | AForeignUnaryOp fu ⇒
        foreign_unary_op_typing_infer_sub fu τ ₁
      end.

  End u.
End TOpsInferSub.