Qcert.Basic.Env.DConstants

Section DConstants.





  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.