X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fcomponents%2Fng_kernel%2FnReference.ml;h=102f25046f84187a495d5778deebf1f1c6148d5d;hb=50a9ed8c6207145fccf59e6a5dbbff935cd2c6d7;hp=e209d05bef8e8d3c28b13093addee5f4be070b69;hpb=2c01ff6094173915e7023076ea48b5804dca7778;p=helm.git

diff --git a/matita/components/ng_kernel/nReference.ml b/matita/components/ng_kernel/nReference.ml
index e209d05be..102f25046 100644
--- a/matita/components/ng_kernel/nReference.ml
+++ b/matita/components/ng_kernel/nReference.ml
@@ -30,6 +30,10 @@ let compare (Ref (u1,s1)) (Ref (u2,s2)) =
   if res = 0 then compare s1 s2 else res
 ;;
 
+let hash (Ref (uri,spec)) =
+ Hashtbl.hash spec + NUri.hash uri
+;;
+
 module OrderedStrings =
  struct
   type t = string
@@ -41,14 +45,15 @@ module MapStringsToReference = Map.Make(OrderedStrings);;
 
 let set_of_reference = ref MapStringsToReference.empty;;
 
-(* '.' not allowed in path and foo
+(* Note: valid ELPI constant
+ * '#' not allowed in path and name
  *
- * Decl                   cic:/path/foo.dec
- * Def                    cic:/path/foo.def
- * Fix of int * int       cic:/path/foo.fix(i,j)
- * CoFix of int           cic:/path/foo.cfx(i)
- * Ind of int             cic:/path/foo.ind(i)
- * Con of int * int       cic:/path/foo.con(i,j)
+ * Decl                   cic:/path/name#dec
+ * Def                    cic:/path/name#def:i
+ * Fix of int * int       cic:/path/name#fix:i:j:h
+ * CoFix of int           cic:/path/name#cfx:i
+ * Ind of int             cic:/path/name#ind:b:i:l
+ * Con of int * int       cic:/path/name#con:i:j:l
  *)
 
 let uri_suffix_of_ref_suffix = function
@@ -59,11 +64,11 @@ let uri_suffix_of_ref_suffix = function
 
 let reference_of_string =
   let get3 s dot =
-    let comma2 = String.rindex s ',' in
-    let comma = String.rindex_from s (comma2-1) ',' in
+    let comma2 = String.rindex s ':' in
+    let comma = String.rindex_from s (comma2-1) ':' in
     let s_i = String.sub s (dot+5) (comma-dot-5) in
     let s_j = String.sub s (comma+1) (comma2-comma-1) in
-    let s_h = String.sub s (comma2+1) (String.length s-comma2-2) in
+    let s_h = String.sub s (comma2+1) (String.length s-comma2-1) in
     let i = int_of_string s_i in
     let j = int_of_string s_j in
     let h = int_of_string s_h in
@@ -71,14 +76,14 @@ let reference_of_string =
   in
 (*
   let get2 s dot =
-    let comma = String.rindex s ',' in
+    let comma = String.rindex s ':' in
     let i = int_of_string (String.sub s (dot+5) (comma-dot-5)) in
-    let j = int_of_string (String.sub s (comma+1) (String.length s-comma-2)) in
+    let j = int_of_string (String.sub s (comma+1) (String.length s-comma-1)) in
     i,j
   in
 *)
   let get1 s dot =
-    let i = int_of_string (String.sub s (dot+5) (String.length s-1-dot-5)) in
+    let i = int_of_string (String.sub s (dot+5) (String.length s-dot-5)) in
     i
   in
 fun s ->
@@ -86,10 +91,10 @@ fun s ->
   with Not_found ->
     let new_reference =
       try
-        let dot = String.rindex s '.' in
-        let prefix = String.sub s 0 (dot+1) in
+        let dot = String.rindex s '#' in
+        let prefix = String.sub s 0 dot in
         let suffix = String.sub s (dot+1) 3 in
-        let u = NUri.uri_of_string (prefix ^ uri_suffix_of_ref_suffix suffix) in
+        let u = NUri.uri_of_string (prefix ^ "." ^ uri_suffix_of_ref_suffix suffix) in
         match suffix with
         | "dec" -> Ref (u, Decl)
         | "def" -> let i = get1 s dot in Ref (u, Def i)
@@ -109,16 +114,16 @@ let string_of_reference (Ref (u,indinfo)) =
   let dot = String.rindex s '.' in
   let s2 = String.sub s 0 dot in
   match indinfo with
-  | Decl ->  s2 ^ ".dec"
-  | Def h -> s2 ^ ".def(" ^ string_of_int h ^ ")"
+  | Decl ->  s2 ^ "#dec"
+  | Def h -> s2 ^ "#def:" ^ string_of_int h
   | Fix (i,j,h)  -> 
-      s2 ^ ".fix(" ^ string_of_int i ^ "," ^ 
-      string_of_int j ^ "," ^ string_of_int h ^ ")"
-  | CoFix i -> s2 ^ ".cfx(" ^ string_of_int i ^ ")"
-  | Ind (b,i,l)->s2 ^".ind(" ^(if b then "1" else "0")^ "," ^ string_of_int i ^
-      "," ^ string_of_int l ^ ")"
-  | Con (i,j,l) -> s2 ^ ".con(" ^ string_of_int i ^ "," ^ string_of_int j ^ 
-      "," ^ string_of_int l ^ ")"
+      s2 ^ "#fix:" ^ string_of_int i ^ ":" ^
+      string_of_int j ^ ":" ^ string_of_int h
+  | CoFix i -> s2 ^ "#cfx:" ^ string_of_int i
+  | Ind (b,i,l)->s2 ^"#ind:" ^(if b then "1" else "0")^ ":" ^ string_of_int i ^
+      ":" ^ string_of_int l
+  | Con (i,j,l) -> s2 ^ "#con:" ^ string_of_int i ^ ":" ^ string_of_int j ^
+      ":" ^ string_of_int l
 ;;
 
 let mk_constructor j = function
@@ -151,7 +156,3 @@ let mk_cofix i = function
 let reference_of_spec u spec = 
   reference_of_string (string_of_reference (Ref (u, spec)))
 ;;
-
-
-
-