Module Qcert.TypeSystem.TBrandContext

Require Import String.
Require Import List.
Require Import ListSet.
Require Import Sumbool.
Require Import Arith.
Require Import Bool.
Require Import Morphisms.
Require Import Basics.
Require Import EquivDec.
Require Import Eqdep_dec.
Require Import Utils.
Require Import BrandRelation.
Require Import ForeignType.
Require Import RType.

Section TBrandContext.

  Definition Any {ftype:foreign_type} {br:brand_relation} := Brand nil.

  Section Brand_Context.
    Context {ftype:foreign_type}.
    Context {br:brand_relation}.
    
    Definition brand_context_decls : Set := list (string*rtype).
    Class brand_context :=
      mkBrand_context {
          brand_context_types : brand_context_decls;
          brand_context_types_sorted : is_list_sorted ODT_lt_dec (domain brand_context_types) = true
        }.

    Lemma brand_context_nodup {m:brand_context} : NoDup (domain brand_context_types).

    Lemma brand_context_ext m pf1 pf1':
      mkBrand_context m pf1 = mkBrand_context m pf1'.
  
    Lemma brand_context_fequal {m₁ m₂}:
      @brand_context_types m₁ = @brand_context_types m₂ -> m₁ = m₂.

    Definition brand_context_Rec (m:brand_context) := Rec Open _ (brand_context_types_sorted).

    Lemma brand_context_Rec_inj (m1 m2:brand_context) :
      brand_context_Rec m1 = brand_context_Rec m2 -> m1 = m2.

  End Brand_Context.
End TBrandContext.