Qcert.Basic.Typing.TDData

Section TDData.


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

  Inductive ddata_type : ddata → drtype → Prop :=
  | dtlocal d τ : data_type d τ → ddata_type (Dlocal d) (Tlocal τ)
  | dtdistr dl τ : Forall (fun d ⇒ data_type d τ) dl → ddata_type (Ddistr dl) (Tdistr τ).

  Lemma ddata_dtype_normalized d dτ :
    ddata_type d dτ → ddata_normalized brand_relation_brands d.

  Definition drtype_sub (dτ₁ dτ₂:drtype) : Prop
    := match dτ₁, dτ₂ with
       | Tlocal τ₁, Tlocal τ₂ ⇒ τ₁ ≤ τ₂
       | Tdistr τ₁, Tdistr τ₂ ⇒ τ₁ ≤ τ₂
       | _, _ ⇒ False
       end.

  Global Instance drtype_sub_pre : PreOrder drtype_sub.

  Global Instance drtype_sub_part : PartialOrder eq drtype_sub.

  Global Instance ddata_type_sub :
    Proper (eq ==> drtype_sub ==> impl) ddata_type.

  Lemma drtype_sub_dec (dτ₁ dτ₂:drtype) :
    {drtype_sub dτ₁ dτ₂} + {¬ drtype_sub dτ₁ dτ₂}.

End TDData.