Module DData

Section DData.
  Require Import String.
  Require Import List.
  Require Import Sumbool.
  Require Import ZArith.
  Require Import Bool.

  Require Import Utils.
  Require Import BrandRelation.
  Require Import ForeignData.
  Require Import RData.


  Unset Elimination Schemes.

  Context {fdata:foreign_data}.

  Inductive ddata :=
  | Dlocal : data -> ddata
  | Ddistr : list data -> ddata.

  Require Import EquivDec.
  Lemma ddata_eq_dec : EqDec ddata eq.
    
  Definition localize_data (ld:ddata) :=
    match ld with
    | Dlocal d => d
    | Ddistr coll => dcoll coll
    end.

  Lemma localize_distr_is_id (l:list data) :
    localize_data (Ddistr l) = dcoll l.

  Definition checkLocal (ld:ddata) : option data :=
    match ld with
    | Dlocal d => Some d
    | Ddistr _ => None
    end.

  Definition checkDistrAndCollect (ld:ddata) : option data :=
    match ld with
    | Dlocal _ => None
    | Ddistr coll => Some (dcoll coll)
    end.
  
  Definition unlocalize_data (dd:ddata) :=
    match dd with
    | Ddistr coll => dcoll coll
    | Dlocal d => d
    end.

  Lemma unlocalize_distributed_id (l:list data) :
    unlocalize_data (Ddistr l) = dcoll l.

  Definition dbindings := list (string*ddata).

  Definition localize_denv (denv:dbindings) : bindings :=
    map (fun x => (fst x, localize_data (snd x))) denv.

  Lemma localize_denv_cons v d (denv:dbindings) :
    localize_denv ((v,Dlocal d) :: denv) = (v,d) :: localize_denv denv.

  
  Inductive dlocalization :=
  | Vlocal : dlocalization
  | Vdistr : dlocalization.

  Definition vdbindings := list (string*dlocalization).

  Require Import EquivDec.
  Lemma dlocalization_eq_dec : EqDec dlocalization eq.
  
End DData.