Module CldMRSanitize

This contains support functions in order to emit code which follows lexical constraints imposed by Cloudant.

Section CldMRSanitize.
  Require Import String.
  Require Import List.
  Require Import Sorting.Mergesort.
  Require Import EquivDec.

  Require Import Utils BasicRuntime.
  Require Import NNRCRuntime NNRCMRRuntime.
  Require Import CldMRUtil ForeignCloudant.

  Local Open Scope list_scope.

  Context {fruntime:foreign_runtime}.
  Context {fredop:foreign_reduce_op}.
  Context {fcloudant:foreign_cloudant}.

  Context (h:list(string*string)).

  Require Import Ascii String List.
  Import ListNotations.
  Definition cldAllowedIdentifierInitialCharacters :=
    ["a";"b";"c";"d";"e";"f";"g";"h";"i";"j";"k";"l";"m";"n";"o";"p";"q";"r";"s";"t";"u";"v";"w";"x";"y";"z"]%char.

According to https://docs.cloudant.com/database.html, this cldAllowedIdentifierCharacters_fromdocs work. But $ at least has been reported as causing problems with the UI. So we conservatively use cldAllowedIdentifierCharacters instead.

  Definition cldAllowedIdentifierCharacters_fromdocs := ["a";"b";"c";"d";"e";"f";"g";"h";"i";"j";"k";"l";"m";"n";"o";"p";"q";"r";"s";"t";"u";"v";"w";"x";"y";"z";"0";"1";"2";"3";"4";"5";"6";"7";"8";"9";"_";"$";",";"+";"-";"/"]%char.

  Definition cldAllowedIdentifierCharacters := ["a";"b";"c";"d";"e";"f";"g";"h";"i";"j";"k";"l";"m";"n";"o";"p";"q";"r";"s";"t";"u";"v";"w";"x";"y";"z";"0";"1";"2";"3";"4";"5";"6";"7";"8";"9";"_"]%char.

  Definition cldIdentifierInitialCharacterToAdd := "z"%char.
  Definition cldIdenitiferCharacterForReplacement := "z"%char.

  Definition cldIdentifierFixInitial (ident:string) : string
    := match ident with
       | EmptyString =>
         String cldIdentifierInitialCharacterToAdd EmptyString
       | String a _ =>
         if in_dec ascii_dec a cldAllowedIdentifierInitialCharacters
         then ident
         else String cldIdentifierInitialCharacterToAdd ident
       end.

  Definition cldIdentifierSanitizeChar (a:ascii)
    := if a == "$"%char
       then "_"%char
       else if in_dec ascii_dec a cldAllowedIdentifierCharacters
            then a
            else cldIdenitiferCharacterForReplacement.

  Definition cldIdentifierSanitizeBody (ident:string)
    := map_string cldIdentifierSanitizeChar ident.

  Definition cldIdentifierSanitize (ident:string)
    := cldIdentifierFixInitial (cldIdentifierSanitizeBody (mk_lower ident)).

  Definition cldSafeSeparator := "_"%string.

  Definition cldAvoidList : list string := [].

End CldMRSanitize.