Files that handle the dialogue with the graphical user-interface pcoq.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@1531 85f007b7-540e-0410-9357-904b9bb8a0f7

1 files changed, 26 insertions, 0 deletions

diff --git a/contrib/interface/paths.ml b/contrib/interface/paths.ml
new file mode 100644
index 0000000000..b1244d1582
--- /dev/null
+++ b/contrib/interface/paths.ml
@@ -0,0 +1,26 @@
+let int_list_to_string s l =
+    List.fold_left 
+       (fun s -> (fun v -> s ^ " " ^ (string_of_int v)))
+       s
+       l;;
+
+(* Given two paths, this function returns the longest common prefix and the
+   two suffixes. *)
+let rec decompose_path
+     : (int list * int list) -> (int list * int list * int list) =
+   function
+       (a::l,b::m) when a = b ->
+         let (c,p1,p2) = decompose_path (l,m) in
+         (a::c,p1,p2)
+     |  p1,p2 -> [], p1, p2;;
+
+let rec is_prefix p1 p2 = match p1,p2 with
+  [], _ -> true
+| a::tl1, b::tl2 when a = b -> is_prefix tl1 tl2
+| _ -> false;;
+
+let rec lex_smaller p1 p2 = match p1,p2 with
+  [], _ -> true
+| a::tl1, b::tl2 when a < b -> true
+| a::tl1, b::tl2 when a = b -> lex_smaller tl1 tl2
+| _ -> false;;
\ No newline at end of file