From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Fri, 22 Apr 2005 08:34:45 +0000 (+0000)
Subject: added filtering criteria on differences between number of constants in
X-Git-Tag: after_svn_merge~24
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=20054808327ccec9d018b8cc54b31ccb44724f49;p=helm.git

added filtering criteria on differences between number of constants in
hypothesis and conclusion, should handle better queries on terms with
metavariables
---

diff --git a/helm/ocaml/metadata/metadataConstraints.ml b/helm/ocaml/metadata/metadataConstraints.ml
index ab8c00f99..870a57d90 100644
--- a/helm/ocaml/metadata/metadataConstraints.ml
+++ b/helm/ocaml/metadata/metadataConstraints.ml
@@ -36,6 +36,7 @@ type term_signature = (string * string list) option * StringSet.t
 type cardinality_condition =
   | Eq of int
   | Gt of int
+  | Lt of int
 
 let tbln n = "table" ^ string_of_int n
 
@@ -66,98 +67,126 @@ let mk_positions positions cur_tbl =
       (positions :> MetadataTypes.position list)) ^
   ")"
 
+let explode_card_constr = function
+  | Eq card -> "=", card
+  | Gt card -> ">", card
+  | Lt card -> "<", card
+
 let add_card_constr tbl (n,from,where) = function
   | None -> (n,from,where)
-  | Some (Eq card) ->
+  | Some constr ->
       let cur_tbl = tbln n in
+      let op, card = explode_card_constr constr in
       (n+1,
        (sprintf "%s as %s" tbl cur_tbl :: from),
-       (sprintf "%s.no=%d" cur_tbl card ::
+       (sprintf "%s.no %s %d" cur_tbl op card ::
         (if n=0 then []
         else [sprintf "table0.source = %s.source" cur_tbl]) @
         where))
-  | Some (Gt card) ->
-      let cur_tbl = tbln n in
-      (n+1,
-       (sprintf "%s as %s" tbl cur_tbl :: from),
-       (sprintf "%s.no>%d" cur_tbl card ::
-        (if n=0 then []
-        else [sprintf "table0.source = %s.source" cur_tbl]) @
+
+let add_diff_constr conclno_tbl hypno_tbl (n,from,where) = function
+  | None -> (n,from,where)
+  | Some constr ->
+      let cur_tbl1, cur_tbl2 = tbln n, tbln (n+1) in
+      let op, card = explode_card_constr constr in
+      (n+2,
+       (sprintf "%s as %s" conclno_tbl cur_tbl1 ::
+        sprintf "%s as %s" hypno_tbl cur_tbl2 :: from),
+       (sprintf "%s.no - %s.no %s %d" cur_tbl2 cur_tbl1 op card ::
+        (if n=0 then assert false
+        else [sprintf "table0.source = %s.source" cur_tbl1;
+              sprintf "table0.source = %s.source" cur_tbl2]) @
         where))
 
-let at_least ~(dbd:Mysql.dbd) ?concl_card ?full_card tables
+let add_constraint tables (n,from,where) metadata =
+  let obj_tbl,rel_tbl,sort_tbl,conclno_tbl,fullno_tbl,hypno_tbl = tables in
+  let cur_tbl = tbln n in
+  match metadata with
+  | `Obj (uri, positions) ->
+      let from = (sprintf "%s as %s" obj_tbl cur_tbl) :: from in
+      let where = 
+        (sprintf "(%s.h_occurrence = \"%s\")" cur_tbl uri) ::
+        mk_positions positions cur_tbl ::
+        (if n=0 then []
+        else [sprintf "table0.source = %s.source" cur_tbl]) @ 
+        where
+      in
+      ((n+2), from, where)
+  | `Rel positions ->
+      let from = (sprintf "%s as %s" rel_tbl cur_tbl) :: from in
+      let where =
+        mk_positions positions cur_tbl ::
+        (if n=0 then []
+        else [sprintf "table0.source = %s.source" cur_tbl]) @ 
+        where
+      in
+      ((n+2), from, where)
+  | `Sort (sort, positions) ->
+      let sort_str = CicPp.ppsort sort in
+      let from = (sprintf "%s as %s" sort_tbl cur_tbl) :: from in
+      let where =
+        (sprintf "%s.h_sort = \"%s\"" cur_tbl sort_str ) ::
+            mk_positions positions cur_tbl ::
+        (if n=0 then 
+          []
+        else 
+          [sprintf "table0.source = %s.source" cur_tbl ]) @ where
+      in
+      ((n+2), from, where)
+
+let at_least ~(dbd:Mysql.dbd) ?concl_card ?full_card ?diff tables
   (metadata: MetadataTypes.constr list)
 =
+  let obj_tbl,rel_tbl,sort_tbl,conclno_tbl,fullno_tbl,hypno_tbl = tables in
   if (metadata = []) && concl_card = None && full_card = None then
     failwith "MetadataQuery.at_least: no constraints given";
-  let obj_tbl,rel_tbl,sort_tbl,conclno_tbl,conclno_hyp_tbl = tables in
-  let add_constraint (n,from,where) metadata =
-    let cur_tbl = tbln n in
-    match metadata with
-    | `Obj (uri, positions) ->
-        let from = (sprintf "%s as %s" obj_tbl cur_tbl) :: from in
-        let where = 
-          (sprintf "(%s.h_occurrence = \"%s\")" cur_tbl uri) ::
-          mk_positions positions cur_tbl ::
-          (if n=0 then []
-          else [sprintf "table0.source = %s.source" cur_tbl]) @ 
-          where
-        in
-        ((n+2), from, where)
-    | `Rel positions ->
-        let from = (sprintf "%s as %s" rel_tbl cur_tbl) :: from in
-        let where =
-          mk_positions positions cur_tbl ::
-          (if n=0 then []
-          else [sprintf "table0.source = %s.source" cur_tbl]) @ 
-          where
-        in
-        ((n+2), from, where)
-    | `Sort (sort, positions) ->
-        let sort_str = CicPp.ppsort sort in
-        let from = (sprintf "%s as %s" sort_tbl cur_tbl) :: from in
-        let where =
-          (sprintf "%s.h_sort = \"%s\"" cur_tbl sort_str ) ::
-              mk_positions positions cur_tbl ::
-          (if n=0 then 
-            []
-          else 
-            [sprintf "table0.source = %s.source" cur_tbl ]) @ where
-        in
-        ((n+2), from, where)
+  let (n,from,where) =
+    List.fold_left (add_constraint tables) (0,[],[]) metadata
   in
-  let (n,from,where) = List.fold_left add_constraint (0,[],[]) metadata in
   let (n,from,where) =
     add_card_constr conclno_tbl (n,from,where) concl_card
   in
   let (n,from,where) =
-    add_card_constr conclno_hyp_tbl (n,from,where) full_card
+    add_card_constr fullno_tbl (n,from,where) full_card
+  in
+  let (n,from,where) =
+    add_diff_constr conclno_tbl hypno_tbl (n,from,where) diff
   in
   let from = String.concat ", " from in
   let where = String.concat " and " where in
-  let query = sprintf "select table0.source from %s where %s" from where in
+  let query =
+(*
+    sprintf
+      ("select table0.source from %s, %s where %s and %s.source = table0.source"
+      ^^ " order by %s.no")
+      from fullno_tbl where fullno_tbl fullno_tbl
+ *)
+    sprintf "select table0.source from %s where %s" from where
+  in
+  prerr_endline query;
   let result = Mysql.exec dbd query in
   Mysql.map result
     (fun row -> match row.(0) with Some s -> s | _ -> assert false)
 
 let at_least  
-  ~(dbd:Mysql.dbd) ?concl_card ?full_card (metadata: MetadataTypes.constr list)
+  ~(dbd:Mysql.dbd) ?concl_card ?full_card ?diff
+      (metadata: MetadataTypes.constr list)
 =
   let module MT = MetadataTypes in
   if MT.are_tables_ownerized () then
-    (at_least ~dbd ?concl_card ?full_card 
+    (at_least ~dbd ?concl_card ?full_card ?diff
       (MT.obj_tbl (),MT.rel_tbl (),MT.sort_tbl (),
-       MT.conclno_tbl (),MT.conclno_hyp_tbl ()) 
+       MT.conclno_tbl (),MT.fullno_tbl (),MT.hypno_tbl ())
         metadata)
         @
-    (at_least ~dbd ?concl_card ?full_card 
+    (at_least ~dbd ?concl_card ?full_card ?diff
       (MT.library_obj_tbl,MT.library_rel_tbl,MT.library_sort_tbl,
-       MT.library_conclno_tbl,MT.library_conclno_hyp_tbl) 
+       MT.library_conclno_tbl,MT.library_fullno_tbl,MT.library_hypno_tbl) 
         metadata)
   else
-    at_least ~dbd ?concl_card ?full_card 
+    at_least ~dbd ?concl_card ?full_card ?diff
       (MT.library_obj_tbl,MT.library_rel_tbl,MT.library_sort_tbl,
-       MT.library_conclno_tbl,MT.library_conclno_hyp_tbl) 
+       MT.library_conclno_tbl,MT.library_fullno_tbl,MT.library_hypno_tbl) 
         metadata 
   
     
diff --git a/helm/ocaml/metadata/metadataConstraints.mli b/helm/ocaml/metadata/metadataConstraints.mli
index 72f808efb..48143490f 100644
--- a/helm/ocaml/metadata/metadataConstraints.mli
+++ b/helm/ocaml/metadata/metadataConstraints.mli
@@ -57,14 +57,18 @@ val sigmatch:
 type cardinality_condition =
   | Eq of int
   | Gt of int
+  | Lt of int
 
   (** @param concl_card cardinality condition on conclusion only
   * @param full_card cardinality condition on the whole statement
+  * @param diff required difference between the number of different constants in
+  * hypothesis and the number of different constants in body
   * @return list of URI satisfying given constraints *)
 val at_least:
   dbd:Mysql.dbd ->
   ?concl_card:cardinality_condition ->
   ?full_card:cardinality_condition ->
+  ?diff:cardinality_condition ->
   MetadataTypes.constr list ->
     string list
 
diff --git a/helm/ocaml/metadata/metadataDb.ml b/helm/ocaml/metadata/metadataDb.ml
index 4b7664c22..30e5912d8 100644
--- a/helm/ocaml/metadata/metadataDb.ml
+++ b/helm/ocaml/metadata/metadataDb.ml
@@ -76,7 +76,7 @@ let insert_const_no dbd uri =
         SELECT \"%s\",COUNT(DISTINCT h_occurrence)
         FROM %s
         WHERE NOT (h_position=\"%s\") AND (source = \"%s\")"
-      (conclno_hyp_tbl ()) uri (obj_tbl ()) inbody_pos uri
+      (fullno_tbl ()) uri (obj_tbl ()) inbody_pos uri
   in
   ignore (Mysql.exec dbd inconcl_no);
   ignore (Mysql.exec dbd concl_hyp)
@@ -121,7 +121,7 @@ let index_inductive_def ~dbd =
     end
 
 let tables_to_clean =
-  [sort_tbl; rel_tbl; obj_tbl; conclno_tbl; conclno_hyp_tbl; name_tbl]
+  [sort_tbl; rel_tbl; obj_tbl; conclno_tbl; fullno_tbl; name_tbl]
 
 let clean ~(dbd:Mysql.dbd) =
   let owned_uris =  (* list of uris in list-of-columns format *)
diff --git a/helm/ocaml/metadata/metadataExtractor.ml b/helm/ocaml/metadata/metadataExtractor.ml
index 8db0d74f5..784de4db6 100644
--- a/helm/ocaml/metadata/metadataExtractor.ml
+++ b/helm/ocaml/metadata/metadataExtractor.ml
@@ -158,6 +158,77 @@ let compute_term pos term =
   in
   aux pos S.empty term
 
+module OrderedInt =
+struct
+  type t = int
+  let compare = Pervasives.compare
+end
+
+module IntSet = Set.Make (OrderedInt)
+
+let compute_metas term =
+  let rec aux in_hyp ((concl_metas, hyp_metas) as acc) cic =
+    match cic with
+    | Cic.Rel _
+    | Cic.Sort _
+    | Cic.Var _ -> acc
+    | Cic.Meta (no, local_context) ->
+        let acc =
+          if in_hyp then
+            (concl_metas, IntSet.add no hyp_metas)
+          else
+            (IntSet.add no concl_metas, hyp_metas)
+        in
+        List.fold_left
+          (fun set context ->
+            match context with
+            | None -> set
+            | Some term -> aux in_hyp set term)
+          acc
+          local_context
+    | Cic.Implicit _ -> assert false
+    | Cic.Cast (term, ty) ->
+        (* TODO consider also ty? *)
+        aux in_hyp acc term
+    | Cic.Prod (_, source, target) ->
+        if in_hyp then
+          let acc = aux in_hyp acc source in
+          aux in_hyp acc target
+        else
+          let acc = aux true acc source in
+          aux in_hyp acc target
+    | Cic.Lambda (_, source, target) ->
+        let acc = aux in_hyp acc source in
+        aux in_hyp acc target
+    | Cic.LetIn (_, term, target) ->
+        aux in_hyp acc (CicSubstitution.subst term target)
+    | Cic.Appl [] -> assert false
+    | Cic.Appl (hd :: tl) ->
+        let acc = aux in_hyp acc hd in
+        List.fold_left (fun acc term -> aux in_hyp acc term) acc tl
+    | Cic.Const (_, subst)
+    | Cic.MutInd (_, _, subst)
+    | Cic.MutConstruct (_, _, _, subst) ->
+        List.fold_left (fun acc (_, term) -> aux in_hyp acc term) acc subst
+    | Cic.MutCase (uri, _, outtype, term, pats) ->
+        let acc = aux in_hyp acc term in
+        let acc = aux in_hyp acc outtype in
+        List.fold_left (fun acc term -> aux in_hyp acc term) acc pats
+    | Cic.Fix (_, funs) ->
+        List.fold_left
+          (fun acc (_, _, ty, body) ->
+            let acc = aux in_hyp acc ty in
+            aux in_hyp acc body)
+          acc funs
+    | Cic.CoFix (_, funs) ->
+        List.fold_left
+          (fun acc (_, ty, body) ->
+            let acc = aux in_hyp acc ty in
+            aux in_hyp acc body)
+          acc funs
+  in
+  aux false (IntSet.empty, IntSet.empty) term
+
 let compute_type uri typeno (name, _, ty, constructors) =
   let consno = ref 0 in
   let type_metadata =
diff --git a/helm/ocaml/metadata/metadataExtractor.mli b/helm/ocaml/metadata/metadataExtractor.mli
index ce057a85a..450c3a525 100644
--- a/helm/ocaml/metadata/metadataExtractor.mli
+++ b/helm/ocaml/metadata/metadataExtractor.mli
@@ -34,3 +34,10 @@ val compute_term:
   MetadataTypes.position -> Cic.term ->
     MetadataTypes.metadata list
 
+module IntSet: Set.S with type elt = int
+
+  (** given a term, returns a pair of sets corresponding respectively to the set
+    * of meta numbers occurring in term's conclusion and the set of meta numbers
+    * occurring in term's hypotheses *)
+val compute_metas: Cic.term -> IntSet.t * IntSet.t
+
diff --git a/helm/ocaml/metadata/metadataTypes.ml b/helm/ocaml/metadata/metadataTypes.ml
index 3f55b886f..948d08678 100644
--- a/helm/ocaml/metadata/metadataTypes.ml
+++ b/helm/ocaml/metadata/metadataTypes.ml
@@ -68,7 +68,8 @@ let sort_tbl_original = "refSort"
 let rel_tbl_original = "refRel"
 let obj_tbl_original = "refObj"
 let conclno_tbl_original = "no_inconcl_aux"
-let conclno_hyp_tbl_original = "no_concl_hyp"
+let fullno_tbl_original = "no_concl_hyp"
+let hypno_tbl_original = "no_hyp"
 let name_tbl_original = "objectName"
 
   (** the names currently used *)
@@ -76,7 +77,8 @@ let sort_tbl_real = ref sort_tbl_original
 let rel_tbl_real = ref rel_tbl_original
 let obj_tbl_real = ref obj_tbl_original
 let conclno_tbl_real = ref conclno_tbl_original
-let conclno_hyp_tbl_real = ref conclno_hyp_tbl_original
+let fullno_tbl_real = ref fullno_tbl_original
+let hypno_tbl_real = ref hypno_tbl_original
 let name_tbl_real = ref name_tbl_original 
 
   (** the exported symbols *)
@@ -84,7 +86,8 @@ let sort_tbl () = ! sort_tbl_real ;;
 let rel_tbl () = ! rel_tbl_real ;; 
 let obj_tbl () = ! obj_tbl_real ;; 
 let conclno_tbl () = ! conclno_tbl_real ;; 
-let conclno_hyp_tbl () = ! conclno_hyp_tbl_real ;; 
+let fullno_tbl () = ! fullno_tbl_real ;; 
+let hypno_tbl () = ! hypno_tbl_real ;; 
 let name_tbl () = ! name_tbl_real ;; 
 
   (** to use the owned tables *)
@@ -93,7 +96,8 @@ let ownerize_tables owner =
   rel_tbl_real := ( rel_tbl_original ^ "_" ^ owner) ;
   obj_tbl_real := ( obj_tbl_original ^ "_" ^ owner) ;
   conclno_tbl_real := ( conclno_tbl_original ^ "_" ^ owner) ;
-  conclno_hyp_tbl_real := ( conclno_hyp_tbl_original ^ "_" ^ owner) ;
+  fullno_tbl_real := ( fullno_tbl_original ^ "_" ^ owner) ;
+  hypno_tbl_real := ( hypno_tbl_original ^ "_" ^ owner) ;
   name_tbl_real := ( name_tbl_original ^ "_" ^ owner) 
 ;;
 
@@ -101,7 +105,8 @@ let library_sort_tbl =   sort_tbl_original
 let library_rel_tbl = rel_tbl_original
 let library_obj_tbl = obj_tbl_original
 let library_conclno_tbl = conclno_tbl_original
-let library_conclno_hyp_tbl = conclno_hyp_tbl_original
+let library_fullno_tbl =  fullno_tbl_original
+let library_hypno_tbl =  hypno_tbl_original
 let library_name_tbl = name_tbl_original
 
 let are_tables_ownerized () =
diff --git a/helm/ocaml/metadata/metadataTypes.mli b/helm/ocaml/metadata/metadataTypes.mli
index b20c8ce14..206967678 100644
--- a/helm/ocaml/metadata/metadataTypes.mli
+++ b/helm/ocaml/metadata/metadataTypes.mli
@@ -66,13 +66,15 @@ val sort_tbl: unit -> string
 val rel_tbl: unit -> string
 val obj_tbl: unit -> string
 val conclno_tbl: unit -> string
-val conclno_hyp_tbl: unit -> string
+val fullno_tbl: unit -> string
+val hypno_tbl: unit -> string
 val name_tbl: unit -> string
 
 val library_sort_tbl:  string  
 val library_rel_tbl:  string
 val library_obj_tbl:  string
 val library_conclno_tbl:  string
-val library_conclno_hyp_tbl:  string
+val library_fullno_tbl:  string
+val library_hypno_tbl:  string
 val library_name_tbl:  string