Module TBindings

Section TBindings.
  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 Types BasicRuntime.
  Require Import ForeignDataTyping.
  Require Import TData.

  Context {ftype:foreign_type}.
  Context {m:brand_model}.

  Definition tbindings := list (string*rtype).

  Context {fdata:foreign_data}.
  Context {fdtyping:foreign_data_typing}.
  Definition bindings_type (b:list (string*data)) (t:tbindings)
    := Forall2 (fun xy1 xy2 =>
                      (fst xy1) = (fst xy2)
                  /\ data_type (snd xy1) (snd xy2)) b t.

  Lemma bindings_type_has_type {env Γ} pf :
      bindings_type env Γ ->
      data_type (drec env) (Rec Closed Γ pf).

  Lemma bindings_type_sort c τc :
    bindings_type c τc ->
    bindings_type (rec_sort c) (rec_sort τc).

  Hint Resolve data_type_normalized.
  Lemma bindings_type_Forall_normalized c τc :
    bindings_type c τc ->
    Forall
      (fun d : string * data => data_normalized brand_relation_brands (snd d))
      c.

End TBindings.

Hint Resolve bindings_type_Forall_normalized.