Qcert.Basic.Env.RConstants

Section RConstants.


  Definition CONST_PREFIX:string := "CONST$"%string.

  Definition mkConstants {A} (l:list (string×A))
    := map (fun xy ⇒ (append CONST_PREFIX (fst xy), snd xy)) l.

  Section ConstantsProp.
    Definition filterConstants {A} (l:list (string×A))
      := filter (fun xy ⇒ prefix CONST_PREFIX (fst xy)) l.

    Lemma filterConstants_lookup_pre {A} (l:list (string×A)) s :
      lookup equiv_dec (filterConstants l) (append CONST_PREFIX s)
      = lookup equiv_dec l (append CONST_PREFIX s).

    Lemma filter_rev {A} (f:A→bool) l :
      filter f (rev l) = rev (filter f l).

    Lemma filterConstants_rev {A} (l:list (string×A)) :
      filterConstants (rev l) = rev (filterConstants l).

    Lemma mkConstants_rev {A} (l:list (string×A)) :
      mkConstants (rev l) = rev (mkConstants l).

    Lemma filterConstants_assoc_lookupr_pre {A} (l:list (string×A)) s :
      assoc_lookupr equiv_dec (filterConstants l) (append CONST_PREFIX s)
      = assoc_lookupr equiv_dec l (append CONST_PREFIX s).

    Lemma filterConstants_mkConstants {A} (l:list (string×A)) :
      filterConstants (mkConstants l) = mkConstants l.

    Lemma mkConstants_NoDup {A} (l:list (string×A)) :
      NoDup (domain l) ↔ NoDup (domain (mkConstants l)).

    Lemma filterConstants_NoDup {A} (l:list (string×A)) :
      NoDup (domain l) → NoDup (domain (filterConstants l)).

    Lemma mkConstants_indom {A} (l:list (string×A)) x :
      In x (domain (mkConstants l)) →
      prefix CONST_PREFIX x = true.

    Lemma mkConstants_nindom {A} (l:list (string×A)) x :
      prefix CONST_PREFIX x = false →
      ¬ (In x (domain (mkConstants l))).

    Lemma mkConstants_lookup_pre {A} l x (y:A) :
      lookup string_eqdec (mkConstants l) x = Some y →
      prefix CONST_PREFIX x = true.

    Lemma mkConstants_lookup {A} (l:list (string×A)) x :
      lookup string_eqdec (mkConstants l) (append CONST_PREFIX x) =
      lookup string_eqdec l x.

    Lemma mkConstants_assoc_lookupr {A} (l:list (string×A)) x :
      assoc_lookupr string_eqdec (mkConstants l) (append CONST_PREFIX x) =
      assoc_lookupr string_eqdec l x.

  End ConstantsProp.

  Section World.

    Context {fdata:foreign_data}.

    Definition WORLD:string := "WORLD"%string.

    Definition mkWorld (world:list data) : list (string×data)
      := (WORLD,(dcoll world))::nil.

  End World.

  Section unConst.
    Definition unConstVar (fv:string) : string :=
      if (prefix "CONST$" fv)
      then
        substring 6 ((length fv) - 6) fv
      else fv.
  End unConst.

End RConstants.