X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fcomponents%2Fmetadata%2FmetadataConstraints.ml;h=3e8ac2f7250c3aa29ec3bffa835589c0711fe365;hb=e9b09b14538f770b9e65083c24e3e9cf487df648;hp=d7192bd7e75e12c65f1c0d12922ec6e5e3f31673;hpb=2907089ebbbe440dacf8f64d4599d881b2c03fcf;p=helm.git

diff --git a/helm/software/components/metadata/metadataConstraints.ml b/helm/software/components/metadata/metadataConstraints.ml
index d7192bd7e..3e8ac2f72 100644
--- a/helm/software/components/metadata/metadataConstraints.ml
+++ b/helm/software/components/metadata/metadataConstraints.ml
@@ -28,6 +28,9 @@
 open Printf
 open MetadataTypes 
 
+let debug = false
+let debug_print s = if debug then prerr_endline (Lazy.force s)
+
 let critical_value = 7
 let just_factor = 1
 
@@ -153,7 +156,7 @@ let add_constraint ?(start=0) ?(tables=default_tables) (n,from,where) metadata =
       in
       ((n+2), from, where)
 
-let exec ~(dbd:HMysql.dbd) ?rating (n,from,where) =
+let exec dbtype ~(dbd:HSql.dbd) ?rating (n,from,where) =
   let from = String.concat ", " from in
   let where = String.concat " and " where in
   let query =
@@ -165,13 +168,15 @@ let exec ~(dbd:HMysql.dbd) ?rating (n,from,where) =
             and table0.source = hits.source order by hits.no desc")
           from where 
   in
-  (* prerr_endline query; *) 
-  let result = HMysql.exec dbd query in
-  HMysql.map result
-    (fun row -> match row.(0) with Some s -> UriManager.uri_of_string s | _ -> assert false)
-
+  (* debug_print (lazy query); *) 
+  let result = HSql.exec dbtype dbd query in
+  HSql.map result
+    ~f:(fun row -> 
+     match row.(0) with Some s -> UriManager.uri_of_string s 
+     | _ -> assert false)
+;;
 
-let at_least ~(dbd:HMysql.dbd) ?concl_card ?full_card ?diff ?rating tables
+let at_least dbtype ~(dbd:HSql.dbd) ?concl_card ?full_card ?diff ?rating tables
   (metadata: MetadataTypes.constr list)
 =
   let obj_tbl,rel_tbl,sort_tbl, count_tbl = tables in
@@ -187,21 +192,34 @@ let at_least ~(dbd:HMysql.dbd) ?concl_card ?full_card ?diff ?rating tables
     let (n,from,where) =
       add_all_constr ~tbl:count_tbl (n,from,where) concl_card full_card diff
     in
-    exec ~dbd ?rating (n,from,where)
+    exec dbtype ~dbd ?rating (n,from,where)
 ;;
     
 let at_least  
-  ~(dbd:HMysql.dbd) ?concl_card ?full_card ?diff ?rating
+  ~(dbd:HSql.dbd) ?concl_card ?full_card ?diff ?rating
       (metadata: MetadataTypes.constr list)
 =
   if are_tables_ownerized () then
-    (at_least 
-       ~dbd ?concl_card ?full_card ?diff ?rating default_tables metadata) @
-    (at_least 
-       ~dbd ?concl_card ?full_card ?diff ?rating (current_tables ()) metadata)
+    at_least 
+      HSql.Library ~dbd ?concl_card ?full_card ?diff ?rating 
+        default_tables metadata
+    @
+    at_least 
+      HSql.Legacy ~dbd ?concl_card ?full_card ?diff ?rating 
+        default_tables metadata
+    @
+    at_least 
+      HSql.User ~dbd ?concl_card ?full_card ?diff ?rating 
+        (current_tables ()) metadata
+
   else
     at_least 
-      ~dbd ?concl_card ?full_card ?diff ?rating default_tables metadata 
+      HSql.Library ~dbd ?concl_card ?full_card ?diff ?rating 
+        default_tables metadata 
+    @
+    at_least 
+      HSql.Legacy ~dbd ?concl_card ?full_card ?diff ?rating 
+        default_tables metadata 
   
     
   (** Prefix handling *)
@@ -254,8 +272,9 @@ and inspect_conclusion n t =
 	merge n (inspect_conclusion n s) (inspect_conclusion n t)
     | Cic.Lambda (_, s, t) ->
 	merge n (inspect_conclusion n s) (inspect_conclusion n t)
-    | Cic.LetIn (_, s, t) ->
-	merge n (inspect_conclusion n s) (inspect_conclusion n t)
+    | Cic.LetIn (_, s, ty, t) ->
+       merge n (inspect_conclusion n s)
+	(merge n (inspect_conclusion n ty) (inspect_conclusion n t))
     | Cic.Appl ((Cic.Const (u,exp_named_subst))::l) ->
 	add_root (n-1) u l
     | Cic.Appl ((Cic.MutInd (u, t, exp_named_subst))::l) ->
@@ -293,7 +312,7 @@ let rec inspect_term n t =
 	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.LetIn (_, _, _, t) -> inspect_term n t
     | Cic.Appl ((Cic.Const (u,exp_named_subst))::l) ->
 	let childunion = inspect_children (n-1) l in
 	Some u, childunion
@@ -362,18 +381,28 @@ and signature_concl =
     | Cic.Const (u,exp_named_subst) -> 
         UriManagerSet.singleton u
     | Cic.MutInd (u, t, exp_named_subst) -> 
+        let rec projections_of uris =
+          List.flatten
+           (List.map 
+            (fun uri ->
+              let o,_ = CicEnvironment.get_obj CicUniv.oblivion_ugraph uri in
+              projections_of (CicUtil.projections_of_record o uri))
+            uris)
+        in
         let uri = UriManager.uri_of_uriref u t None in
-	UriManagerSet.singleton uri
+        List.fold_right UriManagerSet.add
+          (projections_of [u]) (UriManagerSet.singleton uri)
     | Cic.MutConstruct (u, t, c, exp_named_subst) -> 
         let uri = UriManager.uri_of_uriref u t (Some c) in
-	UriManagerSet.singleton uri
+        UriManagerSet.singleton uri
     | Cic.Cast (t, _) -> signature_concl t
     | Cic.Prod (_, s, t) -> 
 	UriManagerSet.union (signature_concl s) (signature_concl t)
     | Cic.Lambda (_, s, t) ->
 	UriManagerSet.union (signature_concl s) (signature_concl t)
-    | Cic.LetIn (_, s, t) ->
-	UriManagerSet.union (signature_concl s) (signature_concl t)
+    | Cic.LetIn (_, s, ty, t) ->
+       UriManagerSet.union (signature_concl s)
+	(UriManagerSet.union (signature_concl ty) (signature_concl t))
     | Cic.Appl l  -> add l
     | Cic.MutCase _
     | Cic.Fix _
@@ -383,7 +412,7 @@ and signature_concl =
 let rec signature_of = function
   | Cic.Cast (t, _)      -> signature_of t
   | Cic.Prod (_, _, t)   -> signature_of t               
-  | Cic.LetIn (_, _, t) -> signature_of t
+  | Cic.LetIn (_, _, _, t) -> signature_of t
   | Cic.Appl ((Cic.Const (u,exp_named_subst))::l) ->
       Some (u, []), add l
   | Cic.Appl ((Cic.MutInd (u, t, exp_named_subst))::l) ->
@@ -438,7 +467,7 @@ let must_of_prefix ?(where = `Conclusion) m s =
 
 let escape = Str.global_replace (Str.regexp_string "\'") "\\'"
 
-let get_constants (dbd:HMysql.dbd) ~where uri =
+let get_constants (dbd:HSql.dbd) ~where uri =
   let uri = escape (UriManager.string_of_uri uri) in
   let positions =
     match where with
@@ -447,27 +476,33 @@ let get_constants (dbd:HMysql.dbd) ~where uri =
         [ MetadataTypes.mainconcl_pos; MetadataTypes.inconcl_pos;
           MetadataTypes.inhyp_pos; MetadataTypes.mainhyp_pos ]
   in
-  let query = 
-    let pos_predicate =
-      String.concat " OR "
-        (List.map (fun pos -> sprintf "(h_position = \"%s\")" pos) positions)
-    in
-    sprintf ("SELECT h_occurrence FROM %s WHERE source=\"%s\" AND (%s) UNION "^^
-             "SELECT h_occurrence FROM %s WHERE source=\"%s\" AND (%s)")
-      (MetadataTypes.obj_tbl ()) uri pos_predicate
-      MetadataTypes.library_obj_tbl uri pos_predicate
-      
+  let pos_predicate =
+    String.concat " OR "
+      (List.map (fun pos -> sprintf "(h_position = \"%s\")" pos) positions)
+  in
+  let query tbl = 
+    sprintf "SELECT h_occurrence FROM %s WHERE source=\"%s\" AND (%s)"
+      tbl uri pos_predicate
+  in
+  let db = [
+    HSql.Library, MetadataTypes.library_obj_tbl;
+    HSql.Legacy, MetadataTypes.library_obj_tbl;
+    HSql.User, MetadataTypes.obj_tbl ()]
   in
-  let result = HMysql.exec dbd query in
   let set = ref UriManagerSet.empty in
-  HMysql.iter result
-    (fun col ->
-      match col.(0) with
-      | Some uri -> set := UriManagerSet.add (UriManager.uri_of_string uri) !set
-      | _ -> assert false);
+  List.iter
+    (fun (dbtype, table) ->
+      let result = HSql.exec dbtype dbd (query table) in
+      HSql.iter result
+        (fun col ->
+         match col.(0) with
+         | Some uri -> 
+             set := UriManagerSet.add (UriManager.uri_of_string uri) !set
+         | _ -> assert false)) 
+    db;
   !set
 
-let at_most ~(dbd:HMysql.dbd) ?(where = `Conclusion) only u =
+let at_most ~(dbd:HSql.dbd) ?(where = `Conclusion) only u =
   let inconcl = get_constants dbd ~where u in
   UriManagerSet.subset inconcl only
 
@@ -485,7 +520,7 @@ let myspeciallist =
    0,UriManager.uri_of_string "cic:/Coq/Init/Logic/f_equal3.con"]
 
 
-let compute_exactly ~(dbd:HMysql.dbd) ?(facts=false) ~where main prefixes =
+let compute_exactly ~(dbd:HSql.dbd) ?(facts=false) ~where main prefixes =
   List.concat
     (List.map 
       (fun (m,s) -> 
@@ -516,7 +551,7 @@ let compute_exactly ~(dbd:HMysql.dbd) ?(facts=false) ~where main prefixes =
 
   (* critical value reached, fallback to "only" constraints *)
 
-let compute_with_only ~(dbd:HMysql.dbd) ?(facts=false) ?(where = `Conclusion) 
+let compute_with_only ~(dbd:HSql.dbd) ?(facts=false) ?(where = `Conclusion) 
   main prefixes constants
 =
   let max_prefix_length = 
@@ -557,7 +592,7 @@ let compute_with_only ~(dbd:HMysql.dbd) ?(facts=false) ?(where = `Conclusion)
 
   (* real match query implementation *)
 
-let cmatch ~(dbd:HMysql.dbd)  ?(facts=false) t =
+let cmatch ~(dbd:HSql.dbd)  ?(facts=false) t =
   let (main, constants) = signature_of t in
   match main with
   | None -> []
@@ -611,7 +646,7 @@ let power consts =
 
 type where = [ `Conclusion | `Statement ]
 
-let sigmatch ~(dbd:HMysql.dbd) ?(facts=false) ?(where = `Conclusion)
+let sigmatch ~(dbd:HSql.dbd) ?(facts=false) ?(where = `Conclusion)
  (main, constants)
 =
  let main,types =
@@ -620,25 +655,25 @@ let sigmatch ~(dbd:HMysql.dbd) ?(facts=false) ?(where = `Conclusion)
    | Some (main, types) -> Some main,types
  in
   let constants_no = UriManagerSet.cardinal constants in
-  (* prerr_endline (("constants_no: ")^(string_of_int constants_no)); *)
+  (* debug_print (lazy (("constants_no: ")^(string_of_int constants_no))); *)
   if (constants_no > critical_value) then 
     let subsets = 
       let subsets = power_upto just_factor constants in
-      (* let _ = prerr_endline (("subsets: ")^
-	 (string_of_int (List.length subsets))) in *)
+      (* let _ = debug_print (lazy (("subsets: ")^
+	 (string_of_int (List.length subsets)))) in *)
       let types_no = List.length types in 
 	if types_no > 0 then  
           List.map (function (n,l) -> (n+types_no,types@l)) subsets
 	else subsets
     in
-    prerr_endline ("critical_value exceded..." ^ string_of_int constants_no);
+    debug_print (lazy ("critical_value exceded..." ^ string_of_int constants_no));
     let all_constants = 
      let all = match main with None -> types | Some m -> m::types in
       List.fold_right UriManagerSet.add all constants
     in
      compute_with_only ~dbd ~where main subsets all_constants
   else
-    (prerr_endline ("all subsets..." ^ string_of_int constants_no);
+    (debug_print (lazy ("all subsets..." ^ string_of_int constants_no));
     let subsets = 
       let subsets = power constants in
       let types_no = List.length types in
@@ -646,7 +681,7 @@ let sigmatch ~(dbd:HMysql.dbd) ?(facts=false) ?(where = `Conclusion)
         (0,[]) :: List.map (function (n,l) -> (n+types_no,types@l)) subsets
        else subsets
     in
-       prerr_endline "fine1";
+       debug_print (lazy "fine1");
        compute_exactly ~dbd ~facts ~where main subsets)
 
   (* match query wrappers *)