Module Qcert.Data.ModelTyping.TDData

Require Import String.
Require Import List.
Require Import Sumbool.
Require Import Arith.
Require Import Bool.
Require Import Morphisms.
Require Import Basics.
Require Import BrandRelation.
Require Import Utils.
Require Import Types.
Require Import ForeignData.
Require Import DataModel.
Require Import ForeignDataTyping.
Require Import TData.

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.