Skip to main content

🍃 String.v

Environment

See proofs, Gitlab , OCaml

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

Require TezosOfOCaml.Proto_alpha.Environment.Char.

Definition length : string int := String.length.

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
  | EmptyStrings
  | String c sString (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
  | EmptyStringNone
  | String hd tailif (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
  | Nonefalse
  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
  | EmptyStringEmptyString
  | String c str'
      String (Char.uppercase_ascii c) str'
  end.

Definition uncapitalize_ascii(str : string) : string :=
  match str with
  | EmptyStringEmptyString
  | 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.