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