Qcert.Basic.Typing.TDBindings

Section TDBindings.


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

  Definition tdbindings := list (string×drtype).

  Definition dbindings_type (b:list (string×ddata)) (t:tdbindings)
    := Forall2 (fun xy1 xy2 ⇒
                      (fst xy1) = (fst xy2)
                  ∧ ddata_type (snd xy1) (snd xy2)) b t.

  Lemma dbindings_type_Forall_normalized c τc :
    dbindings_type c τc →
    Forall
      (fun d : string × ddata ⇒ ddata_normalized brand_relation_brands (snd d))
      c.

  Definition tdbindings_sub : tdbindings → tdbindings → Prop
      := Forall2
         (fun (xy1 : string × drtype) (xy2 : string × drtype) ⇒
            fst xy1 = fst xy2 ∧ drtype_sub (snd xy1) (snd xy2)).

  Global Instance eq_and_drtype_pre : PreOrder
                                        (fun xy1 xy2 : string × drtype ⇒ fst xy1 = fst xy2 ∧ drtype_sub (snd xy1) (snd xy2)).

  Global Instance tdbindings_sub_pre : PreOrder tdbindings_sub.

  Global Instance tdbindings_sub_part : PartialOrder eq tdbindings_sub.

  Global Instance tdbindings_type_sub :
    Proper (eq ==> tdbindings_sub ==> impl) dbindings_type.

  Section unlocalize.
    Definition unlocalize_tdbindings (binds:tdbindings) : tbindings :=
      map (fun xy ⇒ ((fst xy), unlocalize_drtype (snd xy))) binds.
  End unlocalize.

  Section vdbindings.

    Definition dt_to_v (bind:string × drtype) : string × dlocalization :=
      match snd bind with
      | Tlocal _ ⇒ (fst bind, Vlocal)
      | Tdistr _ ⇒ (fst bind, Vdistr)
      end.

    Definition vdbindings_of_tdbindings (binds:tdbindings) : vdbindings :=
      map dt_to_v binds.

    Definition v_and_t_to_dt_opt (v:dlocalization) (t:rtype) : option drtype :=
      match v with
      | Vlocal ⇒ Some (Tlocal t)
      | Vdistr ⇒ lift Tdistr (tuncoll t)
      end.

    Definition v_and_t_to_dt (v:dlocalization) (t:rtype) : drtype :=
      match v with
      | Vlocal ⇒ Tlocal t
      | Vdistr ⇒ Tdistr t
      end.

  End vdbindings.

End TDBindings.