Module Qcert.Data.Model.DConstants

Require Import String.
Require Import List.
Require Import EquivDec.
Require Import Utils.
Require Import ForeignData.
Require Import Data.
Require Import DData.
Require Import Constants.

Section DConstants.

  Local Open Scope string.

  Context {fdata:foreign_data}.

  Definition source : Set := string.

  Definition mkDistConstant (loc:dlocalization) (d:data) :=
    match loc with
    | Vlocal => Some (Dlocal d)
    | Vdistributed =>
      match d with
      | dcoll coll => Some (Ddistr coll)
      | _ => None
      end
    end.
  
  Definition mkDistConstants
             (vars_loc: list (string * dlocalization)) (env: list (string*data))
    : option (list (string*ddata)) :=
    let one (x_loc: string * dlocalization) :=
        let (x, loc) := x_loc in
        olift (fun d => lift (fun dd => (x, dd)) (mkDistConstant loc d))
              (lookup equiv_dec env x)
    in
    lift_map one vars_loc.

  Section World.
    Definition mkDistWorld (world:list data) : list (string*ddata)
      := (WORLD, Ddistr world)::nil.

    Definition mkDistWorldLoc : list (string*dlocalization)
      := (WORLD, Vdistr)::nil.
  End World.

  Definition unlocalize_constants (env:list (string*ddata)) : list (string*data) :=
    map (fun xy => (fst xy, unlocalize_data (snd xy))) env.

  Lemma unlocalize_constants_cons v d (denv:dbindings) :
    unlocalize_constants ((v,Dlocal d) :: denv) = (v,d) :: unlocalize_constants denv.

  Definition coll_bindings := list (string * (list data)).
  Definition bindings_of_coll_bindings (cb:coll_bindings) : bindings :=
    map (fun xy => (fst xy, dcoll (snd xy))) cb.

End DConstants.