From e466e614d63da993d6380cf166bbb041b46f04cd Mon Sep 17 00:00:00 2001
From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Wed, 20 Oct 2004 10:54:33 +0000
Subject: [PATCH] added term_of_uri

---
 helm/ocaml/cic/cicUtil.ml  | 25 +++++++++++++++++++++++++
 helm/ocaml/cic/cicUtil.mli |  3 +++
 2 files changed, 28 insertions(+)

diff --git a/helm/ocaml/cic/cicUtil.ml b/helm/ocaml/cic/cicUtil.ml
index 29b03a07e..36c266ba7 100644
--- a/helm/ocaml/cic/cicUtil.ml
+++ b/helm/ocaml/cic/cicUtil.ml
@@ -141,3 +141,28 @@ let meta_closed t =
          visit_t f r t
    in	  
    try visit_t (fun x -> x) () t; false with Exit -> true
+
+let xpointer_RE = Str.regexp "[^#]+#xpointer(\\(.*\\))"
+let slash_RE = Str.regexp "/"
+
+let term_of_uri s =
+  let uri = UriManager.uri_of_string s in
+  try
+    (if String.sub s (String.length s - 4) 4 = ".con" then
+      Cic.Const (uri, [])
+    else if String.sub s (String.length s - 4) 4 = ".var" then
+      Cic.Var (uri, [])
+    else if not (Str.string_match xpointer_RE s 0) then
+      raise (UriManager.IllFormedUri s)
+    else
+      (match Str.split slash_RE (Str.matched_group 1 s) with
+      | [_; tyno] -> Cic.MutInd (uri, int_of_string tyno - 1, [])
+      | [_; tyno; consno] ->
+          Cic.MutConstruct
+            (uri, int_of_string tyno - 1, int_of_string consno, [])
+      | _ -> raise Exit))
+  with
+  | Exit
+  | Failure _
+  | Not_found -> raise (UriManager.IllFormedUri s)
+
diff --git a/helm/ocaml/cic/cicUtil.mli b/helm/ocaml/cic/cicUtil.mli
index 24383061c..0b98e51fa 100644
--- a/helm/ocaml/cic/cicUtil.mli
+++ b/helm/ocaml/cic/cicUtil.mli
@@ -36,3 +36,6 @@ val clean_up_local_context :
 val is_closed : Cic.term -> bool
 
 val meta_closed : Cic.term -> bool
+
+val term_of_uri: string -> Cic.term
+
-- 
2.39.2