Module ForeignDataTyping

Section ForeignDataTyping.

  Require Import Utils BasicRuntime Types.
  
  Class foreign_data_typing
        {fdata:foreign_data}
        {ftype:foreign_type}
    : Type
    := mk_foreign_data_typing {
           foreign_data_typing_has_type
             (d:foreign_data_type)
             (τ:foreign_type_type) : Prop
           ; foreign_data_typing_normalized
               {d:foreign_data_type}
               {τ:foreign_type_type} :
               foreign_data_typing_has_type d τ ->
               foreign_data_normalized d
           ; foreign_data_typing_subtype
               {d:foreign_data_type}
               {τ₁ τ₂:foreign_type_type} :
               foreign_data_typing_has_type d τ₁ ->
               τ₁ ≤ τ₂ ->
               foreign_data_typing_has_type d τ₂
           ; foreign_data_typing_meet
               {d:foreign_data_type}
               {τ₁ τ₂:foreign_type_type} :
               foreign_data_typing_has_type d τ₁ ->
               foreign_data_typing_has_type d τ₂ ->
               foreign_data_typing_has_type d (τ₁ ⊓ τ₂)
           ; foreign_data_typing_infer (d:foreign_data_type)
             : option foreign_type_type
           ; foreign_data_typing_infer_normalized {d} :
               foreign_data_normalized d ->
               {τ | foreign_data_typing_infer d = Some τ}
           ; foreign_data_typing_infer_correct {d τ} :
               foreign_data_typing_infer d = Some τ ->
               foreign_data_typing_has_type d τ
           ; foreign_data_typing_infer_least {d τ₁ τ₂} :
               foreign_data_typing_infer d = Some τ₁ ->
               foreign_data_typing_has_type d τ₂ ->
               τ₁ ≤ τ₂
         }.

  Theorem foreign_data_typing_infer_complete
        {fdata:foreign_data}
        {ftype:foreign_type}
        {ftyping:foreign_data_typing}
          {d τ} :
      foreign_data_typing_has_type d τ -> {τ' | foreign_data_typing_infer d = Some τ'}.

End ForeignDataTyping.