From 05b125d1855a127fa829ba13c76aa91eed590a3c Mon Sep 17 00:00:00 2001
From: herbelin
Date: Tue, 10 Jun 2003 20:55:36 +0000
Subject: Ajout fonctions de recherche de sous-chaines (merci a Jacek)

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@4106 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 lib/util.ml  | 27 +++++++++++++++++++++++++++
 lib/util.mli |  1 +
 2 files changed, 28 insertions(+)

diff --git a/lib/util.ml b/lib/util.ml
index 32ebb30ad1..46ac2e5ceb 100644
--- a/lib/util.ml
+++ b/lib/util.ml
@@ -57,6 +57,33 @@ let explode s =
 
 let implode sl = String.concat "" sl
 
+(* 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 = 
+  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 str_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_string_contains ~where ~what =
+  try
+    let _ = str_index_from where 0 what in true
+  with
+      Not_found -> false
+
+(* string parsing *)
+
 let parse_loadpath s =
   let len = String.length s in
   let rec decoupe_dirs n =
diff --git a/lib/util.mli b/lib/util.mli
index 349a323669..82e547d3e8 100644
--- a/lib/util.mli
+++ b/lib/util.mli
@@ -51,6 +51,7 @@ val is_ident_tail : char -> bool
 
 val explode : string -> string list
 val implode : string list -> string
+val string_string_contains : where:string -> what:string -> bool
 
 val parse_loadpath : string -> string list
 
-- 
cgit v1.2.3