Qcert.Basic.Data.DData
Localized Data is:
- Dlocal - single, non-distributed value
- Ddistr - distributed collection of values
Context {fdata:foreign_data}.
Inductive ddata :=
| Dlocal : data → ddata
| Ddistr : list data → ddata.
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).
Lemma dlocalization_eq_dec : EqDec dlocalization eq.
End DData.