Qcert.Basic.Typing.ForeignOpsTyping

Section ForeignOpsTyping.

  Class foreign_unary_op_typing
        {fdata:foreign_data}
        {fuop:foreign_unary_op}
        {ftype:foreign_type}
        {fdtyping:foreign_data_typing}
        {model:brand_model}
    : Type
    := mk_foreign_unary_op_typing {
           foreign_unary_op_typing_has_type
             (fu:foreign_unary_op_type)
             (τin τout : rtype) : Prop
           ; foreign_unary_op_typing_sound
               {fu:foreign_unary_op_type}
               {τin τout : rtype}
               (optyp:foreign_unary_op_typing_has_type fu τin τ out)
               {din:data}
               (dtin:din ▹ τin) :
               (∃ dout,
                   foreign_unary_op_interp brand_relation_brands fu din
                   = Some dout
                   ∧ dout ▹ τ out)
           ; foreign_unary_op_typing_infer (fu:foreign_unary_op_type)
             : rtype → option rtype
           ; foreign_unary_op_typing_infer_correct
               {fu:foreign_unary_op_type}
               {τ₁ τout} :
               foreign_unary_op_typing_infer fu τ ₁ = Some τ out →
               foreign_unary_op_typing_has_type fu τ ₁ τ out
           ; foreign_unary_op_typing_infer_least
               {fu:foreign_unary_op_type}
               {τ₁ τout₁ τout₂} :
               foreign_unary_op_typing_infer fu τ ₁ = Some τ out₁ →
               foreign_unary_op_typing_has_type fu τ ₁ τ out₂ →
               τ out₁ ≤ τ out₂
           ; foreign_unary_op_typing_infer_complete
               {fu:foreign_unary_op_type}
               {τ₁ τout} :
               foreign_unary_op_typing_infer fu τ ₁ = None →
               ¬ foreign_unary_op_typing_has_type fu τ ₁ τ out

           ; foreign_unary_op_typing_infer_sub (fu:foreign_unary_op_type)
             : rtype → option (rtype ×rtype)
         }.

    Class foreign_binary_op_typing
        {fdata:foreign_data}
        {fbop:foreign_binary_op}
        {ftype:foreign_type}
        {fdtyping:foreign_data_typing}
        {model:brand_model}
    : Type
    := mk_foreign_binary_op_typing {
           foreign_binary_op_typing_has_type
             (fb:foreign_binary_op_type)
             (τin₁ τin₂ τout : rtype) : Prop
           ; foreign_binary_op_typing_sound
               {fb:foreign_binary_op_type}
               {τin₁ τin₂ τout : rtype}
               (optyp:foreign_binary_op_typing_has_type fb τ in₁ τ in₂ τ out)
               {din₁ din₂:data}
               (dtin:din₁ ▹ τ in₁)
               (dtin:din₂ ▹ τ in₂) :
               (∃ dout,
                   foreign_binary_op_interp brand_relation_brands fb din₁ din₂
                   = Some dout
                   ∧ dout ▹ τ out)
           ; foreign_binary_op_typing_infer (fb:foreign_binary_op_type)
             : rtype → rtype → option rtype
           ; foreign_binary_op_typing_infer_correct
               {fb:foreign_binary_op_type}
               {τ₁ τ₂ τout} :
               foreign_binary_op_typing_infer fb τ ₁ τ ₂ = Some τ out →
               foreign_binary_op_typing_has_type fb τ ₁ τ ₂ τ out
           ; foreign_binary_op_typing_infer_least
               {fb:foreign_binary_op_type}
               {τ₁ τ₂ τout₁ τout₂} :
               foreign_binary_op_typing_infer fb τ ₁ τ ₂ = Some τ out₁ →
               foreign_binary_op_typing_has_type fb τ ₁ τ ₂ τ out₂ →
               τ out₁ ≤ τ out₂
           ; foreign_binary_op_typing_infer_complete
               {fb:foreign_binary_op_type}
               {τ₁ τ₂ τout} :
               foreign_binary_op_typing_infer fb τ ₁ τ ₂ = None →
               ¬ foreign_binary_op_typing_has_type fb τ ₁ τ ₂ τ out

           ; foreign_binary_op_typing_infer_sub (fb:foreign_binary_op_type)
             : rtype → rtype → option (rtype ×rtype ×rtype)

         }.

End ForeignOpsTyping.