added term_of_uri

diff --git a/helm/ocaml/cic/cicUtil.ml b/helm/ocaml/cic/cicUtil.ml
index 29b03a07ea130a687d097e9d6a4d9228ef26c95c..36c266ba7b7054ebbfec0941c6e4a48d13262219 100644 (file)
--- 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 24383061caa120b0b01ffa146497b8aa858afde8..0b98e51fa1b66dd0c6fbed83b60992abbfc508e4 100644 (file)
--- 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
+