Skip to main content

🍬 Script_string.v

Translated OCaml

See proofs, Gitlab , OCaml

File generated by coq-of-ocaml
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Environment.V8.

Definition repr : Set := string.

Inductive t : Set :=
| String_tag : repr t.

Init function; without side-effects in Coq
Definition init_module : unit :=
  Error_monad.register_error_kind Error_monad.Permanent
    "michelson_v1.non_printable_character"
    "Non printable character in a Michelson string"
    "Michelson strings are only allowed to contain printable characters (either the newline character or characters in the [32, 126] ASCII range)."
    (Some
      (fun (ppf : Format.formatter) ⇒
        fun (function_parameter : int × string) ⇒
          let '(pos, s_value) := function_parameter in
          Format.fprintf ppf
            (CamlinternalFormatBasics.Format
              (CamlinternalFormatBasics.String_literal "In Michelson string """
                (CamlinternalFormatBasics.String
                  CamlinternalFormatBasics.No_padding
                  (CamlinternalFormatBasics.String_literal
                    """, character at position "
                    (CamlinternalFormatBasics.Int CamlinternalFormatBasics.Int_d
                      CamlinternalFormatBasics.No_padding
                      CamlinternalFormatBasics.No_precision
                      (CamlinternalFormatBasics.String_literal
                        " has ASCII code "
                        (CamlinternalFormatBasics.Int
                          CamlinternalFormatBasics.Int_d
                          CamlinternalFormatBasics.No_padding
                          CamlinternalFormatBasics.No_precision
                          (CamlinternalFormatBasics.String_literal
                            ". Expected: either a newline character (ASCII code 10) or a printable character (ASCII code between 32 and 126)."
                            CamlinternalFormatBasics.End_of_format)))))))
              "In Michelson string ""%s"", character at position %d has ASCII code %d. Expected: either a newline character (ASCII code 10) or a printable character (ASCII code between 32 and 126).")
            s_value pos (Char.code (String.get s_value pos))))
    (Data_encoding.obj2
      (Data_encoding.req None None "position" Data_encoding.int31)
      (Data_encoding.req None None "string" Data_encoding.string_value))
    (fun (function_parameter : Error_monad._error) ⇒
      match function_parameter with
      | Build_extensible tag _ payload
        if String.eqb tag "Non_printable_character" then
          let '(pos, s_value) := cast (int × string) payload in
          Some (pos, s_value)
        else None
      end)
    (fun (function_parameter : int × string) ⇒
      let '(pos, s_value) := function_parameter in
      Build_extensible "Non_printable_character" (int × string) (pos, s_value)).

Definition empty : t := String_tag "".

#[bypass_check(guard)]
Definition of_string (v_value : repr) : M? t :=
  let fix check_printable_ascii (i_value : int) {struct i_value} : M? t :=
    if i_value <i 0 then
      return? (String_tag v_value)
    else
      match String.get v_value i_value with
      |
        ("010" % char | " " % char | "!" % char | """" % char | "" % char |
        "$" % char | "%" % char | "&" % char | "'" % char | "(" % char |
        ")" % char | "*" % char | "+" % char | "," % char | "-" % char |
        "." % char | "/" % char | "0" % char | "1" % char | "2" % char |
        "3" % char | "4" % char | "5" % char | "6" % char | "7" % char |
        "8" % char | "9" % char | ":" % char | ";" % char | "<" % char |
        "=" % char | ">" % char | "?" % char | "@" % char | "A" % char |
        "B" % char | "C" % char | "D" % char | "E" % char | "F" % char |
        "G" % char | "H" % char | "I" % char | "J" % char | "K" % char |
        "L" % char | "M" % char | "N" % char | "O" % char | "P" % char |
        "Q" % char | "R" % char | "S" % char | "T" % char | "U" % char |
        "V" % char | "W" % char | "X" % char | "Y" % char | "Z" % char |
        "[" % char | "\" % char | "]" % char | "^" % char | "_" % char |
        "`" % char | "a" % char | "b" % char | "c" % char | "d" % char |
        "e" % char | "f" % char | "g" % char | "h" % char | "i" % char |
        "j" % char | "k" % char | "l" % char | "m" % char | "n" % char |
        "o" % char | "p" % char | "q" % char | "r" % char | "s" % char |
        "t" % char | "u" % char | "v" % char | "w" % char | "x" % char |
        "y" % char | "z" % char | "{" % char | "|" % char | "}" % char |
        "~" % char) ⇒ check_printable_ascii (i_value -i 1)
      | _
        Error_monad.error_value
          (Build_extensible "Non_printable_character" (int × repr)
            (i_value, v_value))
      end in
  check_printable_ascii ((String.length v_value) -i 1).

Definition to_string (function_parameter : t) : repr :=
  let 'String_tag s_value := function_parameter in
  s_value.

Definition compare (function_parameter : t) : t int :=
  let 'String_tag x_value := function_parameter in
  fun (function_parameter : t) ⇒
    let 'String_tag y_value := function_parameter in
    Compare.String.(Compare.S.compare) x_value y_value.

Definition length (function_parameter : t) : int :=
  let 'String_tag s_value := function_parameter in
  String.length s_value.

Definition concat_pair (function_parameter : t) : t t :=
  let 'String_tag x_value := function_parameter in
  fun (function_parameter : t) ⇒
    let 'String_tag y_value := function_parameter in
    String_tag (Pervasives.op_caret x_value y_value).

Definition concat (l_value : list t) : t :=
  let l_value :=
    List.map
      (fun (function_parameter : t) ⇒
        let 'String_tag s_value := function_parameter in
        s_value) l_value in
  String_tag (String.concat "" l_value).

Definition sub (function_parameter : t) : int int t :=
  let 'String_tag s_value := function_parameter in
  fun (offset : int) ⇒
    fun (length : int) ⇒ String_tag (String.sub s_value offset length).