Module Qcert.Common.TypeSystem.DType


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

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

  Inductive drtype : Set :=
  | Tlocal : rtype -> drtype
  | Tdistr : rtype -> drtype.
  
  Global Instance drtype_eqdec : EqDec drtype eq.
Proof.
    red; intros.
    destruct x; destruct y.
    - destruct (r == r0); unfold equiv, complement in *; subst.
      * left; reflexivity.
      * right; congruence.
    - right; congruence.
    - right; congruence.
    - destruct (r == r0); unfold equiv, complement in *; subst.
      * left; reflexivity.
      * right; congruence.
  Defined.

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

  End unlocalize.

End DType.