Permalink
Browse files

Added a CString module.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@15968 85f007b7-540e-0410-9357-904b9bb8a0f7
  • Loading branch information...
ppedrot
ppedrot committed Nov 13, 2012
1 parent 81ca535 commit 1d436a18f2f72b57ea09a6d27709a36b63be863a
View
@@ -10,6 +10,7 @@ Unicode
Errors
CObj
CList
+CString
CArray
Util
Option
View
@@ -12,6 +12,7 @@ Unicode
Errors
CObj
CList
+CString
CArray
Util
Bigint
View
@@ -8,6 +8,7 @@ Loc
Compat
Errors
CList
+CString
CArray
Util
Bigint
View
@@ -282,7 +282,7 @@ let drop_implicits_in_patt cst nb_expl args =
let has_curly_brackets ntn =
String.length ntn >= 6 & (String.sub ntn 0 6 = "{ _ } " or
String.sub ntn (String.length ntn - 6) 6 = " { _ }" or
- string_string_contains ~where:ntn ~what:" { _ } ")
+ String.string_contains ~where:ntn ~what:" { _ } ")
let rec wildcards ntn n =
if n = String.length ntn then []
View
@@ -137,7 +137,7 @@ let explain_non_linear_pattern id =
str "The variable " ++ pr_id id ++ str " is bound several times in pattern"
let explain_bad_patterns_number n1 n2 =
- str "Expecting " ++ int n1 ++ str (plural n1 " pattern") ++
+ str "Expecting " ++ int n1 ++ str (String.plural n1 " pattern") ++
str " but found " ++ int n2
let explain_internalization_error e =
View
@@ -641,7 +641,7 @@ let decompose_notation_key s =
let tok =
match String.sub s n (pos-n) with
| "_" -> NonTerminal (id_of_string "_")
- | s -> Terminal (drop_simple_quotes s) in
+ | s -> Terminal (String.drop_simple_quotes s) in
decomp_ntn (tok::dirs) (pos+1)
in
decomp_ntn [] 0
View
@@ -0,0 +1,152 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(** FIXME: use module type of *)
+module type S =
+sig
+ external length : string -> int = "%string_length"
+ external get : string -> int -> char = "%string_safe_get"
+ external set : string -> int -> char -> unit = "%string_safe_set"
+ external create : int -> string = "caml_create_string"
+ val make : int -> char -> string
+ val copy : string -> string
+ val sub : string -> int -> int -> string
+ val fill : string -> int -> int -> char -> unit
+ val blit : string -> int -> string -> int -> int -> unit
+ val concat : string -> string list -> string
+ val iter : (char -> unit) -> string -> unit
+ val escaped : string -> string
+ val index : string -> char -> int
+ val rindex : string -> char -> int
+ val index_from : string -> int -> char -> int
+ val rindex_from : string -> int -> char -> int
+ val contains : string -> char -> bool
+ val contains_from : string -> int -> char -> bool
+ val rcontains_from : string -> int -> char -> bool
+ val uppercase : string -> string
+ val lowercase : string -> string
+ val capitalize : string -> string
+ val uncapitalize : string -> string
+ type t = string
+ val compare: t -> t -> int
+ external unsafe_get : string -> int -> char = "%string_unsafe_get"
+ external unsafe_set : string -> int -> char -> unit = "%string_unsafe_set"
+ external unsafe_blit :
+ string -> int -> string -> int -> int -> unit = "caml_blit_string" "noalloc"
+ external unsafe_fill :
+ string -> int -> int -> char -> unit = "caml_fill_string" "noalloc"
+end
+
+module type ExtS =
+sig
+ include S
+ external equal : string -> string -> bool = "caml_string_equal"
+ val explode : string -> string list
+ val implode : string list -> string
+ val strip : string -> string
+ val map : (char -> char) -> string -> string
+ val drop_simple_quotes : string -> string
+ val string_index_from : string -> int -> string -> int
+ val string_contains : where:string -> what:string -> bool
+ val plural : int -> string -> string
+ val ordinal : int -> string
+ val split : char -> string -> string list
+end
+
+include String
+
+external equal : string -> string -> bool = "caml_string_equal"
+
+
+let explode s =
+ let rec explode_rec n =
+ if n >= String.length s then
+ []
+ else
+ String.make 1 (String.get s n) :: explode_rec (succ n)
+ in
+ explode_rec 0
+
+let implode sl = String.concat "" sl
+
+let is_blank = function
+ | ' ' | '\r' | '\t' | '\n' -> true
+ | _ -> false
+
+let strip s =
+ let n = String.length s in
+ let rec lstrip_rec i =
+ if i < n && is_blank s.[i] then
+ lstrip_rec (i+1)
+ else i
+ in
+ let rec rstrip_rec i =
+ if i >= 0 && is_blank s.[i] then
+ rstrip_rec (i-1)
+ else i
+ in
+ let a = lstrip_rec 0 and b = rstrip_rec (n-1) in
+ String.sub s a (b-a+1)
+
+let map f s =
+ let l = String.length s in
+ let r = String.create l in
+ for i = 0 to (l - 1) do r.[i] <- f (s.[i]) done;
+ r
+
+let drop_simple_quotes s =
+ let n = String.length s in
+ if n > 2 & s.[0] = '\'' & s.[n-1] = '\'' then String.sub s 1 (n-2) else s
+
+(* substring searching... *)
+
+(* gdzie = where, co = what *)
+(* gdzie=gdzie(string) gl=gdzie(length) gi=gdzie(index) *)
+let rec is_sub gdzie gl gi co cl ci =
+ (ci>=cl) ||
+ ((String.unsafe_get gdzie gi = String.unsafe_get co ci) &&
+ (is_sub gdzie gl (gi+1) co cl (ci+1)))
+
+let rec raw_str_index i gdzie l c co cl =
+ (* First adapt to ocaml 3.11 new semantics of index_from *)
+ if (i+cl > l) then raise Not_found;
+ (* Then proceed as in ocaml < 3.11 *)
+ let i' = String.index_from gdzie i c in
+ if (i'+cl <= l) && (is_sub gdzie l i' co cl 0) then i' else
+ raw_str_index (i'+1) gdzie l c co cl
+
+let string_index_from gdzie i co =
+ if co="" then i else
+ raw_str_index i gdzie (String.length gdzie)
+ (String.unsafe_get co 0) co (String.length co)
+
+let string_contains ~where ~what =
+ try
+ let _ = string_index_from where 0 what in true
+ with
+ Not_found -> false
+
+let plural n s = if n<>1 then s^"s" else s
+
+let ordinal n =
+ let s = match n mod 10 with 1 -> "st" | 2 -> "nd" | 3 -> "rd" | _ -> "th" in
+ string_of_int n ^ s
+
+(* string parsing *)
+
+let split c s =
+ let len = String.length s in
+ let rec split n =
+ try
+ let pos = String.index_from s n c in
+ let dir = String.sub s n (pos-n) in
+ dir :: split (succ pos)
+ with
+ | Not_found -> [String.sub s n (len-n)]
+ in
+ if Int.equal len 0 then [] else split 0
View
@@ -0,0 +1,63 @@
+(************************************************************************)
+(* v * The Coq Proof Assistant / The Coq Development Team *)
+(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2012 *)
+(* \VV/ **************************************************************)
+(* // * This file is distributed under the terms of the *)
+(* * GNU Lesser General Public License Version 2.1 *)
+(************************************************************************)
+
+(** FIXME: From OCaml 3.12 onwards, that would only be a [module type of] *)
+
+(** Module type [S] is the one from OCaml Stdlib. *)
+module type S =
+sig
+ external length : string -> int = "%string_length"
+ external get : string -> int -> char = "%string_safe_get"
+ external set : string -> int -> char -> unit = "%string_safe_set"
+ external create : int -> string = "caml_create_string"
+ val make : int -> char -> string
+ val copy : string -> string
+ val sub : string -> int -> int -> string
+ val fill : string -> int -> int -> char -> unit
+ val blit : string -> int -> string -> int -> int -> unit
+ val concat : string -> string list -> string
+ val iter : (char -> unit) -> string -> unit
+ val escaped : string -> string
+ val index : string -> char -> int
+ val rindex : string -> char -> int
+ val index_from : string -> int -> char -> int
+ val rindex_from : string -> int -> char -> int
+ val contains : string -> char -> bool
+ val contains_from : string -> int -> char -> bool
+ val rcontains_from : string -> int -> char -> bool
+ val uppercase : string -> string
+ val lowercase : string -> string
+ val capitalize : string -> string
+ val uncapitalize : string -> string
+ type t = string
+ val compare: t -> t -> int
+ external unsafe_get : string -> int -> char = "%string_unsafe_get"
+ external unsafe_set : string -> int -> char -> unit = "%string_unsafe_set"
+ external unsafe_blit :
+ string -> int -> string -> int -> int -> unit = "caml_blit_string" "noalloc"
+ external unsafe_fill :
+ string -> int -> int -> char -> unit = "caml_fill_string" "noalloc"
+end
+
+module type ExtS =
+sig
+ include S
+ external equal : string -> string -> bool = "caml_string_equal"
+ val explode : string -> string list
+ val implode : string list -> string
+ val strip : string -> string
+ val map : (char -> char) -> string -> string
+ val drop_simple_quotes : string -> string
+ val string_index_from : string -> int -> string -> int
+ val string_contains : where:string -> what:string -> bool
+ val plural : int -> string -> string
+ val ordinal : int -> string
+ val split : char -> string -> string list
+end
+
+include ExtS
View
@@ -5,6 +5,7 @@ Coq_config
Deque
CObj
CList
+CString
CArray
Util
Serialize
View
@@ -102,7 +102,7 @@ let docdir () =
let path_to_list p =
let sep = if Sys.os_type = "Win32" then ';' else ':' in
- Util.split_string_at sep p
+ Util.String.split sep p
let xdg_data_home warning =
coqify
@@ -170,7 +170,7 @@ let camllib () =
let camlbin = camlbin () in
let com = (Filename.concat camlbin "ocamlc") ^ " -where" in
let _,res = CUnix.run_command (fun x -> x) (fun _ -> ()) com in
- Util.strip res
+ Util.String.strip res
let camlp4bin () =
if !Flags.camlp4bin_spec then !Flags.camlp4bin else
@@ -187,5 +187,5 @@ let camlp4lib () =
let com = (Filename.concat camlp4bin Coq_config.camlp4) ^ " -where" in
let ex,res = CUnix.run_command (fun x -> x) (fun _ -> ()) com in
match ex with
- |Unix.WEXITED 0 -> Util.strip res
+ |Unix.WEXITED 0 -> Util.String.strip res
|_ -> "/dev/null"
Oops, something went wrong.

0 comments on commit 1d436a1

Please sign in to comment.