Skip to main content

🍃 Bytes.v

Environment

Gitlab , OCaml

Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.

Require Import TezosOfOCaml.Proto_alpha.Environment.String.

Definition length : bytes int := String.length.

Definition get : bytes int ascii := String.get.

Parameter set : bytes int ascii unit.

Parameter make : int ascii bytes.

Parameter init_value : int (int ascii) bytes.

Definition empty : bytes := "".

Definition copy : bytes bytes := fun bb.

Definition of_string : string bytes := fun bb.

Definition to_string : bytes string := fun bb.

Definition sub : bytes int int bytes := String.sub.

Parameter sub_string : bytes int int string.

Parameter extend : bytes int int bytes.

Parameter fill : bytes int int ascii unit.

Parameter blit : bytes int bytes int int unit.

Parameter blit_string : string int bytes int int unit.

Parameter concat : bytes list bytes bytes.

Definition cat : bytes bytes bytes :=
  String.append.

Parameter iter : (ascii unit) bytes unit.

Definition iteri : (int ascii unit) bytes unit := String.iteri.

Definition map : (ascii ascii) bytes bytes := String.map.

Definition mapi : (int ascii ascii) bytes bytes := String.mapi.

Definition trim : bytes bytes := String.trim.

Definition escaped : bytes bytes := String.escaped.

Definition index_opt : bytes ascii option int := String.index_opt.

Definition rindex_opt : bytes ascii option int := String.rindex_opt.

Definition index_from_opt : bytes int ascii option int := String.index_from_opt.

Definition rindex_from_opt : bytes int ascii option int := String.rindex_from_opt.

Definition contains : bytes ascii bool := String.contains.

Definition contains_from : bytes int ascii bool := String.contains_from.

Definition rcontains_from : bytes int ascii bool := String.rcontains_from.

Definition uppercase_ascii : bytes bytes := String.uppercase_ascii.

Definition lowercase_ascii : bytes bytes := String.lowercase_ascii.

Definition capitalize_ascii : bytes bytes := String.capitalize_ascii.

Definition uncapitalize_ascii : bytes bytes := String.uncapitalize_ascii.

Definition t : Set := bytes.

Definition compare : t t int := String.compare.

Definition equal : t t bool := String.equal.

Axiom of_string_to_string : b : bytes,
  Bytes.of_string (Bytes.to_string b) = b.

Axiom to_string_of_string : b : bytes,
  Bytes.to_string (Bytes.of_string b) = b.