Module Qcert.Data.Model.DData

Require Import String.
Require Import List.
Require Import Sumbool.
Require Import ZArith.
Require Import Bool.
Require Import EquivDec.
Require Import Utils.
Require Import BrandRelation.
Require Import ForeignData.
Require Import Data.

Section DData.

  Unset Elimination Schemes.

  Context {fdata:foreign_data}.

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

  Lemma ddata_eq_dec : EqDec ddata eq.
    
  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).

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

  Definition vdbindings := list (string*dlocalization).

  Lemma dlocalization_eq_dec : EqDec dlocalization eq.
  
End DData.