🍃 String.v
Environment
Require Import CoqOfOCaml.CoqOfOCaml.
Require Import CoqOfOCaml.Settings.
Require TezosOfOCaml.Environment.Structs.V0.Char.
Require TezosOfOCaml.Environment.Structs.V0.Pervasives.
Definition length (s : string) : int :=
Pervasives.normalize_int (Z.of_nat (Strings.String.length s)).
Definition get : string → int → ascii := String.get.
Definition make : int → ascii → string := String.make.
Parameter init_value : int → (int → ascii) → string.
Definition sub (s : string) (start end_ : int) : string :=
Coq.Strings.String.substring (Z.to_nat start) (Z.to_nat end_) s.
Parameter blit : string → int → bytes → int → int → unit.
Definition concat : string → list string → string := String.concat.
Parameter iter : (ascii → unit) → string → unit.
Parameter iteri : (int → ascii → unit) → string → unit.
Fixpoint map (f : ascii → ascii) (s : string) : string :=
match s with
| EmptyString ⇒ s
| String c s ⇒ String (f c) (map f s)
end.
Parameter mapi : (int → ascii → ascii) → string → string.
Parameter trim : string → string.
Parameter escaped : string → string.
Fixpoint index_opt_fix (str : string) (sep : ascii) (n : int) : option int :=
match str with
| EmptyString ⇒ None
| String hd tail ⇒ if (hd =? sep)%char then Some n else index_opt_fix tail sep (n + 1)%Z
end.
Definition index_opt str sep : option int :=
index_opt_fix str sep 0.
Parameter rindex_opt : string → ascii → option int.
Parameter index_from_opt : string → int → ascii → option int.
Parameter rindex_from_opt : string → int → ascii → option int.
Definition contains str sep : bool :=
match index_opt str sep with
| Some _ ⇒ true
| None ⇒ false
end.
Parameter contains_from : string → int → ascii → bool.
Parameter rcontains_from : string → int → ascii → bool.
Definition uppercase_ascii : string → string :=
map Char.uppercase_ascii.
Definition lowercase_ascii : string → string :=
map Char.lowercase_ascii.
Definition capitalize_ascii(str : string) : string :=
match str with
| EmptyString ⇒ EmptyString
| String c str' ⇒
String (Char.uppercase_ascii c) str'
end.
Definition uncapitalize_ascii(str : string) : string :=
match str with
| EmptyString ⇒ EmptyString
| String c str' ⇒
String (Char.lowercase_ascii c) str'
end.
Definition t : Set := string.
Definition compare : t → t → int :=
fun s1 s2 ⇒
match compare s1 s2 with
| Lt ⇒ -1
| Eq ⇒ 0
| Gt ⇒ 1
end.
Definition equal : t → t → bool := String.eqb.
Parameter split_on_char : ascii → string → list string.
Require Import CoqOfOCaml.Settings.
Require TezosOfOCaml.Environment.Structs.V0.Char.
Require TezosOfOCaml.Environment.Structs.V0.Pervasives.
Definition length (s : string) : int :=
Pervasives.normalize_int (Z.of_nat (Strings.String.length s)).
Definition get : string → int → ascii := String.get.
Definition make : int → ascii → string := String.make.
Parameter init_value : int → (int → ascii) → string.
Definition sub (s : string) (start end_ : int) : string :=
Coq.Strings.String.substring (Z.to_nat start) (Z.to_nat end_) s.
Parameter blit : string → int → bytes → int → int → unit.
Definition concat : string → list string → string := String.concat.
Parameter iter : (ascii → unit) → string → unit.
Parameter iteri : (int → ascii → unit) → string → unit.
Fixpoint map (f : ascii → ascii) (s : string) : string :=
match s with
| EmptyString ⇒ s
| String c s ⇒ String (f c) (map f s)
end.
Parameter mapi : (int → ascii → ascii) → string → string.
Parameter trim : string → string.
Parameter escaped : string → string.
Fixpoint index_opt_fix (str : string) (sep : ascii) (n : int) : option int :=
match str with
| EmptyString ⇒ None
| String hd tail ⇒ if (hd =? sep)%char then Some n else index_opt_fix tail sep (n + 1)%Z
end.
Definition index_opt str sep : option int :=
index_opt_fix str sep 0.
Parameter rindex_opt : string → ascii → option int.
Parameter index_from_opt : string → int → ascii → option int.
Parameter rindex_from_opt : string → int → ascii → option int.
Definition contains str sep : bool :=
match index_opt str sep with
| Some _ ⇒ true
| None ⇒ false
end.
Parameter contains_from : string → int → ascii → bool.
Parameter rcontains_from : string → int → ascii → bool.
Definition uppercase_ascii : string → string :=
map Char.uppercase_ascii.
Definition lowercase_ascii : string → string :=
map Char.lowercase_ascii.
Definition capitalize_ascii(str : string) : string :=
match str with
| EmptyString ⇒ EmptyString
| String c str' ⇒
String (Char.uppercase_ascii c) str'
end.
Definition uncapitalize_ascii(str : string) : string :=
match str with
| EmptyString ⇒ EmptyString
| String c str' ⇒
String (Char.lowercase_ascii c) str'
end.
Definition t : Set := string.
Definition compare : t → t → int :=
fun s1 s2 ⇒
match compare s1 s2 with
| Lt ⇒ -1
| Eq ⇒ 0
| Gt ⇒ 1
end.
Definition equal : t → t → bool := String.eqb.
Parameter split_on_char : ascii → string → list string.