Module DType

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

  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.