Module DConstants

Section DConstants.

  Require Import String.
  Require Import List.
  Require Import EquivDec.
  Require Import RList RLift RAssoc.
  Require Import RData DData RRelation.

  Require Import RConstants.
  
  Local Open Scope string.

  Require Import ForeignData.

  Context {fdata:foreign_data}.

  Definition mkDistNames (names: list string) : list (string * dlocalization) :=
    map (fun x => (x, Vdistr)) names.

  Definition mkDistLocs {A} (cenv: list (string * A)) : list (string * dlocalization) :=
    mkDistNames (map fst cenv).

  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
    rmap one vars_loc.

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

    Definition mkDistLoc : 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.
  
End DConstants.