Module Qcert.TypeSystem.DType

Require Import String.
Require Import List.
Require Import Sorting.
Require Import Eqdep_dec.
Require Import Bool.
Require Import EquivDec.
Require Import Morphisms.
Require Import Utils.
Require Import BrandRelation.
Require Import ForeignType.
Require Import RType.

Section DType.

  Context {ftype:foreign_type}.
  Context {br:brand_relation}.

  Inductive drtype : Set :=
  | Tlocal : rtype -> drtype
  | Tdistr : rtype -> drtype.
  
  Global Instance drtype_eqdec : EqDec drtype eq.

  Section unlocalize.
    Definition unlocalize_drtype (dt:drtype) : rtype :=
      match dt with
      | Tlocal t => t
      | Tdistr t => Coll t
      end.

  End unlocalize.

End DType.