From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Fri, 23 Jan 2004 16:37:30 +0000 (+0000)
Subject: moved here term_of_uri
X-Git-Tag: V_0_2_3~162
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=892c8a3420c36f192b2afdb6ffe146f98f92e2f5;p=helm.git

moved here term_of_uri
---

diff --git a/helm/ocaml/cic/helmLibraryObjects.ml b/helm/ocaml/cic/helmLibraryObjects.ml
index 1d7e9285e..4a1a1dad0 100644
--- a/helm/ocaml/cic/helmLibraryObjects.ml
+++ b/helm/ocaml/cic/helmLibraryObjects.ml
@@ -1,4 +1,3 @@
-
 (** {2 Auxiliary functions} *)
 
 let uri = UriManager.uri_of_string
@@ -7,6 +6,47 @@ let const ?(subst = []) uri = Cic.Const (uri, subst)
 let var ?(subst = []) uri = Cic.Var (uri, subst)
 let mutconstruct ?(subst = []) uri typeno consno =
   Cic.MutConstruct (uri, typeno, consno, subst)
+let mutind ?(subst = []) uri typeno = Cic.MutInd (uri, typeno, subst)
+
+let indtyuri_of_uri uri =
+  let index_sharp =  String.index uri '#' in
+  let index_num = index_sharp + 3 in
+  (UriManager.uri_of_string (String.sub uri 0 index_sharp),
+   int_of_string(String.sub uri index_num (String.length uri - index_num)) - 1)
+
+let indconuri_of_uri uri =
+  let index_sharp =  String.index uri '#' in
+  let index_div = String.rindex uri '/' in
+  let index_con = index_div + 1 in
+    (UriManager.uri_of_string (String.sub uri 0 index_sharp),
+    int_of_string
+      (String.sub uri (index_sharp + 3) (index_div - index_sharp - 3)) - 1,
+    int_of_string
+      (String.sub uri index_con (String.length uri - index_con)))
+
+let term_of_uri uri =
+  let s = UriManager.string_of_uri uri in
+  try
+  (* Constant *)
+  (* TODO explicit substitutions? *)
+  let len = String.length s in
+  let sub = String.sub s (len -4) 4 in
+  if sub = ".con" then
+    const uri
+  else if sub = ".var" then
+    var uri
+  else
+    (try
+      (* Inductive Type *)
+      let (uri, typeno) = indtyuri_of_uri s in
+      mutind uri typeno
+     with
+      | UriManager.IllFormedUri _ | Failure _ | Invalid_argument _ ->
+          (* Constructor of an Inductive Type *)
+          let (uri, typeno, consno) = indconuri_of_uri s in
+          mutconstruct uri typeno consno)
+ with
+ | Invalid_argument _ -> raise (UriManager.IllFormedUri s)
 
 (** {2 Helm's objects shorthands} *)