Module Qcert.Data.ModelTyping.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.
Require Import Types.
Require Import ForeignData.
Require Import DataModel.
Require Import ForeignDataTyping.
Require Import TData.

Section TBindings.
  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).

  Lemma bindings_type_app l1 l2 r1 r2 :
    bindings_type l1 r1 -> bindings_type l2 r2 ->
    bindings_type (l1 ++ l2) (r1 ++ r2) .

  Lemma bindings_type_rec_concat_sort l1 l2 r1 r2 :
    bindings_type l1 r1 -> bindings_type l2 r2 ->
    bindings_type (rec_concat_sort l1 l2) (rec_concat_sort r1 r2) .
  
  Local Hint Resolve data_type_normalized : qcert.
  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.

Global Hint Resolve bindings_type_Forall_normalized : qcert.