🍬 Script_string.v
Translated 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.
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).
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).