From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Wed, 20 Oct 2004 10:54:33 +0000 (+0000)
Subject: added term_of_uri
X-Git-Tag: V_0_0_10~64
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e466e614d63da993d6380cf166bbb041b46f04cd;p=helm.git

added term_of_uri
---

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
+