Much simpler (and slightly more performant) implementation of the UriManager.

[helm.git] / helm / ocaml / metadata / metadataConstraints.ml

diff --git a/helm/ocaml/metadata/metadataConstraints.ml b/helm/ocaml/metadata/metadataConstraints.ml
index fb2a494240e786997d7b85b1b9a524b1170658cd..602ee49b93966cac2868be492445bc42b52441d7 100644 (file)
--- a/helm/ocaml/metadata/metadataConstraints.ml
+++ b/helm/ocaml/metadata/metadataConstraints.ml
@@ -214,9 +214,6 @@ let merge n a b =
   in
   filter_by_card n res 
 
-let string_of_uriref i =
- UriManager.uri_of_string (UriManager.string_of_uriref i)
-
 let rec inspect_children n childs =
   List.fold_left 
     (fun res term -> merge n (inspect_conclusion n term) res)
@@ -242,10 +239,10 @@ and inspect_conclusion n t =
         SetSet.singleton (UriManagerSet.singleton u)
     | Cic.MutInd (u, t, exp_named_subst) -> 
        SetSet.singleton (UriManagerSet.singleton
-          (string_of_uriref (u, [t])))
+          (UriManager.uri_of_uriref u t None))
     | Cic.MutConstruct (u, t, c, exp_named_subst) -> 
        SetSet.singleton (UriManagerSet.singleton
-          (string_of_uriref (u, [t; c])))
+          (UriManager.uri_of_uriref u t (Some c)))
     | Cic.Cast (t, _) -> inspect_conclusion n t
     | Cic.Prod (_, s, t) -> 
        merge n (inspect_conclusion n s) (inspect_conclusion n t)
@@ -254,13 +251,12 @@ and inspect_conclusion n t =
     | Cic.LetIn (_, s, t) ->
        merge n (inspect_conclusion n s) (inspect_conclusion n t)
     | Cic.Appl ((Cic.Const (u,exp_named_subst))::l) ->
-        let suri = u in
-       add_root (n-1) suri l
+       add_root (n-1) u l
     | Cic.Appl ((Cic.MutInd (u, t, exp_named_subst))::l) ->
-        let suri = string_of_uriref (u, [t]) in
-       add_root (n-1) suri l
+        let uri = UriManager.uri_of_uriref u t None in
+       add_root (n-1) uri l
     | Cic.Appl ((Cic.MutConstruct (u, t, c, exp_named_subst))::l)  ->
-       let suri = string_of_uriref (u, [t; c]) in
+       let suri = UriManager.uri_of_uriref u t (Some c) in
        add_root (n-1) suri l
     | Cic.Appl l -> 
        SetSet.empty
@@ -284,35 +280,33 @@ let rec inspect_term n t =
     | Cic.Const (u,exp_named_subst) -> 
         Some u, SetSet.empty
     | Cic.MutInd (u, t, exp_named_subst) -> 
-        let uri = string_of_uriref (u, [t]) in
+        let uri = UriManager.uri_of_uriref u t None in
        Some uri, SetSet.empty
     | Cic.MutConstruct (u, t, c, exp_named_subst) -> 
-        let uri = string_of_uriref (u, [t; c]) in
+        let uri = UriManager.uri_of_uriref u t (Some c) in
        Some uri, SetSet.empty
     | Cic.Cast (t, _) -> inspect_term n t
     | Cic.Prod (_, _, t) -> inspect_term n t
     | Cic.LetIn (_, _, t) -> inspect_term n t
     | Cic.Appl ((Cic.Const (u,exp_named_subst))::l) ->
-       let suri = u in
        let childunion = inspect_children (n-1) l in
-       Some suri, childunion
+       Some u, childunion
     | Cic.Appl ((Cic.MutInd (u, t, exp_named_subst))::l) ->
-       let suri = string_of_uriref (u, [t]) in
+       let suri = UriManager.uri_of_uriref u t None in
        if u = HelmLibraryObjects.Logic.eq_URI && n>1 then
          (* equality is handled in a special way: in particular, 
              the type, if defined, is always added to the prefix, 
             and n is not decremented - it should have been n-2 *)
          match l with
              Cic.Const (u1,exp_named_subst1)::l1 ->
-               let suri1 = u1 in
-               let inconcl = add_root (n-1) suri1 l1 in
+               let inconcl = add_root (n-1) u1 l1 in
                Some suri, inconcl
            | Cic.MutInd (u1, t1, exp_named_subst1)::l1 ->
-               let suri1 = string_of_uriref (u1, [t1]) in
+               let suri1 = UriManager.uri_of_uriref u1 t1 None in
                let inconcl = add_root (n-1) suri1 l1 in  
                Some suri, inconcl
            | Cic.MutConstruct (u1, t1, c1, exp_named_subst1)::l1 ->
-                let suri1 = string_of_uriref (u1, [t1; c1]) in
+                let suri1 = UriManager.uri_of_uriref u1 t1 (Some c1) in
                let inconcl = add_root (n-1) suri1 l1 in  
                Some suri, inconcl
            | _ :: _ -> Some suri, SetSet.empty
@@ -321,7 +315,7 @@ let rec inspect_term n t =
          let childunion = inspect_children (n-1) l in
          Some suri, childunion
     | Cic.Appl ((Cic.MutConstruct (u, t, c, exp_named_subst))::l)  ->
-       let suri = string_of_uriref (u, [t; c]) in
+       let suri = UriManager.uri_of_uriref u t(Some c) in
        let childunion = inspect_children (n-1) l in
        Some suri, childunion
     | _ -> None, SetSet.empty
@@ -360,10 +354,10 @@ and signature_concl =
     | Cic.Const (u,exp_named_subst) -> 
         UriManagerSet.singleton u
     | Cic.MutInd (u, t, exp_named_subst) -> 
-        let uri = string_of_uriref (u, [t]) in
+        let uri = UriManager.uri_of_uriref u t None in
        UriManagerSet.singleton uri
     | Cic.MutConstruct (u, t, c, exp_named_subst) -> 
-        let uri = string_of_uriref (u, [t;c]) in
+        let uri = UriManager.uri_of_uriref u t (Some c) in
        UriManagerSet.singleton uri
     | Cic.Cast (t, _) -> signature_concl t
     | Cic.Prod (_, s, t) -> 
@@ -383,25 +377,23 @@ let rec signature_of = function
   | Cic.Prod (_, _, t)   -> signature_of t               
   | Cic.LetIn (_, _, t) -> signature_of t
   | Cic.Appl ((Cic.Const (u,exp_named_subst))::l) ->
-      let suri = u in
-      Some (suri, []), add l
+      Some (u, []), add l
   | Cic.Appl ((Cic.MutInd (u, t, exp_named_subst))::l) ->
-      let suri = string_of_uriref (u, [t]) in
+      let suri = UriManager.uri_of_uriref u t None in
       if u = HelmLibraryObjects.Logic.eq_URI then
          (* equality is handled in a special way: in particular, 
              the type, if defined, is always added to the prefix, 
             and n is not decremented - it should have been n-2 *)
       match l with
          Cic.Const (u1,exp_named_subst1)::l1 ->
-           let suri1 = u1 in
-           let inconcl = UriManagerSet.remove suri1 (add l1) in
-            Some (suri, [suri1]), inconcl
+           let inconcl = UriManagerSet.remove u1 (add l1) in
+            Some (suri, [u1]), inconcl
        | Cic.MutInd (u1, t1, exp_named_subst1)::l1 ->
-           let suri1 = string_of_uriref (u1, [t1]) in
+           let suri1 = UriManager.uri_of_uriref u1 t1 None in
            let inconcl =  UriManagerSet.remove suri1 (add l1) in
              Some (suri, [suri1]), inconcl
        | Cic.MutConstruct (u1, t1, c1, exp_named_subst1)::l1 ->
-            let suri1 = string_of_uriref (u1, [t1;c1]) in
+            let suri1 = UriManager.uri_of_uriref u1 t1 (Some c1) in
            let inconcl =  UriManagerSet.remove suri1 (add l1) in
             Some (suri, [suri1]), inconcl
        | _ :: _ -> Some (suri, []), UriManagerSet.empty
@@ -409,7 +401,7 @@ let rec signature_of = function
       else
        Some (suri, []), add l
   | Cic.Appl ((Cic.MutConstruct (u, t, c, exp_named_subst))::l)  ->
-      let suri = string_of_uriref (u, [t;c]) in
+      let suri = UriManager.uri_of_uriref u t (Some c) in
       Some (suri, []), add l
   | t -> None, signature_concl t
 
@@ -429,7 +421,7 @@ let must_of_prefix ?(where = `Conclusion) m s =
     | `Conclusion -> [`InConclusion]
     | `Statement -> [`InConclusion; `InHypothesis; `MainHypothesis None]
   in
-  let s' = List.map (fun u -> `Obj (u, positions)) s in
+  let s' = List.map (fun (u:UriManager.uri) -> `Obj (u, positions)) s in
   `Obj (m, [`MainConclusion None]) :: s'
 
 let escape = Str.global_replace (Str.regexp_string "\'") "\\'"
@@ -474,7 +466,7 @@ let myspeciallist_of_facts  =
   [0,UriManager.uri_of_string "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)"]
 let myspeciallist =
   [0,UriManager.uri_of_string "cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)";
-   (* 0,UriManager.uri_of_string "cic:/Coq/Init/Logic/sym_eq.con"; *)
+   (* 0,"cic:/Coq/Init/Logic/sym_eq.con"; *)
    0,UriManager.uri_of_string "cic:/Coq/Init/Logic/trans_eq.con";
    0,UriManager.uri_of_string "cic:/Coq/Init/Logic/f_equal.con";
    0,UriManager.uri_of_string "cic:/Coq/Init/Logic/f_equal2.con";
@@ -485,7 +477,7 @@ let compute_exactly ~(dbd:Mysql.dbd) ?(facts=false) ~where main prefixes =
   List.concat
     (List.map 
       (fun (m,s) -> 
-        if ((m = 0) && (main = UriManager.uri_of_string HelmLibraryObjects.Logic.eq_XURI)) then
+        if ((m = 0) && (UriManager.eq main (UriManager.uri_of_string (HelmLibraryObjects.Logic.eq_XURI)))) then
           (if facts then myspeciallist_of_facts
           else myspeciallist)
         else