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

moved term_of_uri in cic/
---

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml
index b2df644d2..0e2b59079 100644
--- a/helm/ocaml/cic_disambiguation/disambiguate.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguate.ml
@@ -82,48 +82,10 @@ let refine metasenv context term =
         debug_print ("%%% PRUNED!!! " ^ CicPp.ppterm term) ;
         Ko
 
-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)))
-
-  (* TODO move it to Cic *)
-let term_of_uri uri =
-  try
-  (* Constant *)
-  (* TODO explicit substitutions? *)
-  let len = String.length uri in
-  if String.sub uri (len - 4) 4 = ".con" then
-    Cic.Const (uri_of_string uri, [])
-  else if String.sub uri (len - 4) 4 = ".var" then
-    Cic.Var (uri_of_string uri, [])
-  else
-    (try
-      (* Inductive Type *)
-      let uri',typeno = indtyuri_of_uri uri in
-      Cic.MutInd (uri', typeno, [])
-     with
-      | UriManager.IllFormedUri _ | Failure _ | Invalid_argument _ ->
-          (* Constructor of an Inductive Type *)
-          let uri',typeno,consno = indconuri_of_uri uri in
-          Cic.MutConstruct (uri', typeno, consno, []))
- with
- | Invalid_argument _ -> raise (UriManager.IllFormedUri uri)
-
 let resolve (env: environment) (item: domain_item) ?(num = "") ?(args = []) () =
   snd (Environment.find item env) env num args
 
+  (* TODO move it to Cic *)
 let find_in_environment name context =
   let rec aux acc = function
     | [] -> raise Not_found
@@ -337,7 +299,14 @@ module Make (C: Callbacks) =
              uris
       in
       List.map
-        (fun uri -> (uri, let term = term_of_uri uri in fun _ _ _ -> term))
+        (fun uri ->
+          (uri,
+           let term =
+             try
+               HelmLibraryObjects.term_of_uri (UriManager.uri_of_string uri)
+             with _ -> assert false
+            in
+           fun _ _ _ -> term))
         uris'
 
     let disambiguate_term mqi_handle context metasenv term ~aliases:current_env