more strings to UriManager.uri

diff --git a/helm/matita/matitaEngine.ml b/helm/matita/matitaEngine.ml
index a74df9313cc5a05755e1a883f836dfe0cb4d92e6..14eab882c80dc39f942def9de4d0a052e962c38f 100644 (file)
--- a/helm/matita/matitaEngine.ml
+++ b/helm/matita/matitaEngine.ml
@@ -212,11 +212,11 @@ let eval_coercion status coercion =
   let context = [] in 
   let src_uri = 
     let ty_src = CicReduction.whd context ty_src in
-    UriManager.uri_of_string (CicUtil.uri_of_term ty_src) 
+     CicUtil.uri_of_term ty_src
   in
   let tgt_uri = 
     let ty_tgt = CicReduction.whd context ty_tgt in
-    UriManager.uri_of_string (CicUtil.uri_of_term ty_tgt) 
+     CicUtil.uri_of_term ty_tgt
   in
   let new_coercions =
     (* also adds them to the Db *)
@@ -288,7 +288,7 @@ let eval_command status cmd =
           {status with aliases = 
             DisambiguateTypes.Environment.add 
               (DisambiguateTypes.Id id) 
-              ("boh?",(fun _ _ _ -> CicUtil.term_of_uri uri)) 
+              ("boh?",(fun _ _ _ -> CicUtil.term_of_uri (UriManager.uri_of_string uri)))
               status.aliases }
       | TacticAst.Symbol_alias (symb, instance, desc) ->
           {status with aliases = 

diff --git a/helm/matita/matitaSync.ml b/helm/matita/matitaSync.ml
index 6573e39822f991840d8cbca78fce0779d336de8b..472ab3a923016800a06053c194c4ec5c1072820a 100644 (file)
--- a/helm/matita/matitaSync.ml
+++ b/helm/matita/matitaSync.ml
@@ -41,7 +41,7 @@ let extract_alias types uri =
   ) ([],0) types)
 
 let env_of_list l env =
- let l' = List.map (fun (name,suri) -> name,suri,CicUtil.term_of_uri suri) l in
+ let l' = List.map (fun (name,suri) -> name,suri,CicUtil.term_of_uri (UriManager.uri_of_string suri)) l in
   DisambiguateTypes.env_of_list l' env
 
 let add_aliases_for_inductive_def status types suri = 

diff --git a/helm/ocaml/cic/cicUtil.ml b/helm/ocaml/cic/cicUtil.ml
index a0b03527878f3754325c852f74f1170f78077fd8..a3649ca36ed312874b333d39696a9a2c5bbf8ef0 100644 (file)
--- a/helm/ocaml/cic/cicUtil.ml
+++ b/helm/ocaml/cic/cicUtil.ml
@@ -138,8 +138,8 @@ let rec is_meta_closed =
 let xpointer_RE = Str.regexp "\\([^#]+\\)#xpointer(\\(.*\\))"
 let slash_RE = Str.regexp "/"
 
-let term_of_uri s =
-  let uri = UriManager.uri_of_string s in
+let term_of_uri uri =
+  let s = UriManager.string_of_uri uri in
   try
     (if String.sub s (String.length s - 4) 4 = ".con" then
       Cic.Const (uri, [])
@@ -163,12 +163,14 @@ let term_of_uri s =
 
 let uri_of_term = function
   | Cic.Const (uri, [])
-  | Cic.Var (uri, []) -> UriManager.string_of_uri uri
+  | Cic.Var (uri, []) -> uri
   | Cic.MutInd (baseuri, tyno, []) ->
-      sprintf "%s#xpointer(1/%d)" (UriManager.string_of_uri baseuri) (tyno + 1)
+     UriManager.uri_of_string
+      (sprintf "%s#xpointer(1/%d)" (UriManager.string_of_uri baseuri) (tyno+1))
   | Cic.MutConstruct (baseuri, tyno, consno, []) ->
-      sprintf "%s#xpointer(1/%d/%d)" (UriManager.string_of_uri baseuri)
-        (tyno + 1) consno
+     UriManager.uri_of_string
+      (sprintf "%s#xpointer(1/%d/%d)" (UriManager.string_of_uri baseuri)
+        (tyno + 1) consno)
   | _ -> raise (Invalid_argument "uri_of_term")
 
 let select ~term ~context =

diff --git a/helm/ocaml/cic/cicUtil.mli b/helm/ocaml/cic/cicUtil.mli
index 0b6e2242addebd57c9f9d027173c454372e5cd80..a64a983f7c3033ca60afb792bc345fecec7e4828 100644 (file)
--- a/helm/ocaml/cic/cicUtil.mli
+++ b/helm/ocaml/cic/cicUtil.mli
@@ -41,9 +41,8 @@ val strip_prods: int -> Cic.term -> Cic.term
 
 (** conversions between terms which are fully representable as uris (Var, Const,
  * Mutind, and MutConstruct) and corresponding tree representations *)
-(*CSC: horrible: the strings are URIs. To change also DisambiguateTypes.* *)
-val term_of_uri: string -> Cic.term (** @raise UriManager.IllFormedUri *)
-val uri_of_term: Cic.term -> string (** @raise Invalid_argument "uri_of_term" *)
+val term_of_uri: UriManager.uri -> Cic.term (** @raise UriManager.IllFormedUri *)
+val uri_of_term: Cic.term -> UriManager.uri (** @raise Invalid_argument "uri_of_term" *)
 
 (*
   (** packing/unpacking of several terms into a single one *)

diff --git a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
index bba6fef7c8d68bf936f20626d04a293ede7e12ee..b223eb3fd6eb199bd7818ddf3436e34072c4c7f6 100644 (file)
--- a/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
+++ b/helm/ocaml/cic_disambiguation/cicTextualParser2.ml
@@ -53,9 +53,9 @@ let fresh_num_instance =
   else
     (fun () -> 0)
 
-let choice_of_uri uri =
-  let term = CicUtil.term_of_uri uri in
-  (uri, (fun _ _ _ -> term))
+let choice_of_uri suri =
+  let term = CicUtil.term_of_uri (UriManager.uri_of_string suri) in
+  (suri, (fun _ _ _ -> term))
 
 let grammar = Grammar.gcreate cic_lexer
 
@@ -683,8 +683,8 @@ module EnvironmentP3 =
       alias: [  (* return a pair <domain_item, codomain_item> from an alias *)
         [ IDENT "alias";
           choice =
-            [ IDENT "id"; id = IDENT; SYMBOL "="; uri = URI ->
-                (Id id, choice_of_uri uri)
+            [ IDENT "id"; id = IDENT; SYMBOL "="; suri = URI ->
+                (Id id, choice_of_uri suri)
             | IDENT "symbol"; symbol = QSTRING;
               PAREN "("; IDENT "instance"; instance = NUM; PAREN ")";
               SYMBOL "="; dsc = QSTRING ->

diff --git a/helm/ocaml/cic_disambiguation/disambiguate.ml b/helm/ocaml/cic_disambiguation/disambiguate.ml
index 27122ef1deaf635f594d2931d2a606046fc81069..6b5e3f8332c60e21283486461032d020f12ac60d 100644 (file)
--- a/helm/ocaml/cic_disambiguation/disambiguate.ml
+++ b/helm/ocaml/cic_disambiguation/disambiguate.ml
@@ -230,7 +230,7 @@ let interpretate_term ~context ~env ~uri ~is_path ast =
           let cic =
             if is_uri ast then  (* we have the URI, build the term out of it *)
               try
-                CicUtil.term_of_uri name
+                CicUtil.term_of_uri (UriManager.uri_of_string name)
               with UriManager.IllFormedUri _ ->
                 CicTextualParser2.fail loc "Ill formed URI"
             else
@@ -638,7 +638,7 @@ module Make (C: Callbacks) =
           (UriManager.string_of_uri uri,
            let term =
              try
-               CicUtil.term_of_uri (UriManager.string_of_uri uri)
+               CicUtil.term_of_uri uri
              with exn ->
                debug_print (UriManager.string_of_uri uri);
                debug_print (Printexc.to_string exn);

diff --git a/helm/ocaml/cic_notation/cicNotationMatcher.ml b/helm/ocaml/cic_notation/cicNotationMatcher.ml
index 08a4617f7c97cb672017e5215c9f9f4e2db78100..46469e769928bc0029fbb52f7db98a9cf1171012 100644 (file)
--- a/helm/ocaml/cic_notation/cicNotationMatcher.ml
+++ b/helm/ocaml/cic_notation/cicNotationMatcher.ml
@@ -317,7 +317,7 @@ struct
   struct
     type cic_mask_t =
       Blob
-    | Uri of string
+    | Uri of UriManager.uri
     | Appl of cic_mask_t list
 
     let uri_of_term t = CicUtil.uri_of_term (Deannotate.deannotate_term t)
@@ -335,7 +335,7 @@ struct
       Hashtbl.hash mask, tl
 
     let mask_of_appl_pattern = function
-      | Pt.UriPattern s -> Uri s, []
+      | Pt.UriPattern s -> Uri (UriManager.uri_of_string s), []
       | Pt.VarPattern _ -> Blob, []
       | Pt.ApplPattern pl -> Appl (List.map (fun _ -> Blob) pl), pl
 

diff --git a/helm/ocaml/cic_omdoc/content.mli b/helm/ocaml/cic_omdoc/content.mli
index 99869b9b47623ab226574da143eb625ec3e5bdfe..c1122b8f2b2627d67dccd9ccd3fd4a4e0643af16 100644 (file)
--- a/helm/ocaml/cic_omdoc/content.mli
+++ b/helm/ocaml/cic_omdoc/content.mli
@@ -130,7 +130,7 @@ and premise =
 and lemma =
        { lemma_id: id;
          lemma_name : string;
-         lemma_uri: string 
+         lemma_uri: string
        }
 ;;
  

diff --git a/helm/ocaml/cic_omdoc/content2cic.ml b/helm/ocaml/cic_omdoc/content2cic.ml
index fdc2cea1cee300573c739dfe597ea46896c52242..339492d1985317911dad12a0890d5a89d62fea25 100644 (file)
--- a/helm/ocaml/cic_omdoc/content2cic.ml
+++ b/helm/ocaml/cic_omdoc/content2cic.ml
@@ -210,7 +210,8 @@ let proof2cic deannotate p =
                with Not_found -> 
                   prerr_endline ("Not_found in arg2cic: premise " ^ (match prem.Con.premise_binder with None -> "previous" | Some p -> p) ^ ", xref=" ^ prem.Con.premise_xref);
                   raise Not_found))
-      | Con.Lemma lemma -> CicUtil.term_of_uri lemma.Con.lemma_uri
+      | Con.Lemma lemma ->
+         CicUtil.term_of_uri (UriManager.uri_of_string lemma.Con.lemma_uri)
       | Con.Term t -> deannotate t
       | Con.ArgProof p -> proof2cic [] p (* empty! *)
       | Con.ArgMethod s -> raise TO_DO

diff --git a/helm/ocaml/cic_unification/coercGraph.ml b/helm/ocaml/cic_unification/coercGraph.ml
index fa18530e53cffdf37dca89171cfdc48433a85b1b..c1056b6eca8a912c1ba9b0171ebcf368ea514a3a 100644 (file)
--- a/helm/ocaml/cic_unification/coercGraph.ml
+++ b/helm/ocaml/cic_unification/coercGraph.ml
@@ -31,8 +31,8 @@ let debug_print = if debug then prerr_endline else ignore
 (* searches a coercion fron src to tgt in the !coercions list *)
 let look_for_coercion src tgt =
     try
-      let src = UriManager.uri_of_string (CicUtil.uri_of_term src) in
-      let tgt = UriManager.uri_of_string (CicUtil.uri_of_term tgt) in
+      let src = CicUtil.uri_of_term src in
+      let tgt = CicUtil.uri_of_term tgt in
       let l = 
         CoercDb.find_coercion 
           (fun (s,t) -> UriManager.eq s src && UriManager.eq t tgt) 
@@ -46,7 +46,7 @@ let look_for_coercion src tgt =
               (UriManager.name_of_uri src) 
               (UriManager.name_of_uri tgt)
               (UriManager.name_of_uri u));
-              Some (CicUtil.term_of_uri (UriManager.string_of_uri u))
+              Some (CicUtil.term_of_uri u)
     with Invalid_argument s -> 
       debug_print (":( coercion non trovata (fallita la uri_of_term): " ^ s);
       None
@@ -133,9 +133,7 @@ let close_coercion_graph src tgt uri =
           match l with
           | [] -> assert false 
           | he :: tl ->
-              let term_of_uri' uri = 
-                CicUtil.term_of_uri (UriManager.string_of_uri uri)
-              in
+              let term_of_uri' uri = CicUtil.term_of_uri uri in
               let first_step = 
                 Cic.Constant ("", Some (term_of_uri' he), Cic.Sort Cic.Prop, [],
                   obj_attrs)

diff --git a/helm/ocaml/tactics/metadataQuery.ml b/helm/ocaml/tactics/metadataQuery.ml
index 644e764ef56c18b927777d013cfc6a0dd8bebd3d..c1dd20ecc83badb808fb8e303b7feec3d701bbbf 100644 (file)
--- a/helm/ocaml/tactics/metadataQuery.ml
+++ b/helm/ocaml/tactics/metadataQuery.ml
@@ -211,7 +211,7 @@ let hint ~(dbd:Mysql.dbd) ?(facts=false) ?signature ((proof, goal) as status) =
 (*                debug_print ("STO APPLICANDO " ^ uri); *)
                PET.apply_tactic
                   (PrimitiveTactics.apply_tac
-                   ~term:(CicUtil.term_of_uri (UriManager.string_of_uri uri)))
+                   ~term:(CicUtil.term_of_uri uri))
                   status
               in
               let goal_list =
@@ -242,7 +242,7 @@ let hint ~(dbd:Mysql.dbd) ?(facts=false) ?signature ((proof, goal) as status) =
 let close_with_types s metasenv context =
   Constr.UriManagerSet.fold 
     (fun e bag -> 
-      let t = CicUtil.term_of_uri (UriManager.string_of_uri e) in
+      let t = CicUtil.term_of_uri e in
       let ty, _ = 
         CicTypeChecker.type_of_aux' metasenv context t CicUniv.empty_ugraph  
       in
@@ -281,7 +281,7 @@ let experimental_hint
       | Some (main,_) -> 
           let ty, _ = 
             CicTypeChecker.type_of_aux' 
-              metasenv context (CicUtil.term_of_uri (UriManager.string_of_uri main)) CicUniv.empty_ugraph
+              metasenv context (CicUtil.term_of_uri main) CicUniv.empty_ugraph
           in
           Constr.constants_of ty
     in
@@ -313,7 +313,7 @@ let experimental_hint
               let (subst,(proof, goal_list)) =
                   (* debug_print ("STO APPLICANDO" ^ uri); *)
                   PrimitiveTactics.apply_tac_verbose 
-                   ~term:(CicUtil.term_of_uri (UriManager.string_of_uri uri))
+                   ~term:(CicUtil.term_of_uri uri)
                   status
               in
               let goal_list =
@@ -484,7 +484,9 @@ let fwd_simpl ~dbd t =
    let map inners row = 
       match row.(0), row.(1), row.(2) with  
          | Some source, Some inner, Some index -> 
-           source, List.mem (int_of_string index, inner) inners
+           source,
+             List.mem
+              (int_of_string index, (UriManager.uri_of_string inner)) inners
         | _                                   -> "", false
    in
    let rec rank ranks (source, ok) = 
@@ -505,7 +507,9 @@ let fwd_simpl ~dbd t =
       | Some (outer, inners) ->
          let select = "source, h_inner, h_index" in
         let from = "genLemma" in
-        let where = Printf.sprintf "h_outer = \"%s\"" (Mysql.escape outer) in
+        let where =
+          Printf.sprintf "h_outer = \"%s\""
+           (Mysql.escape (UriManager.string_of_uri outer)) in
          let query = Printf.sprintf "SELECT %s FROM %s WHERE %s" select from where in
         let result = Mysql.exec dbd query in
          let lemmas = Mysql.map result ~f:(map inners) in