helm/ocaml/metadata/metadataConstraints.ml

   1 (* Copyright (C) 2004, HELM Team.
   2  *
   3  * This file is part of HELM, an Hypertextual, Electronic
   4  * Library of Mathematics, developed at the Computer Science
   5  * Department, University of Bologna, Italy.
   6  *
   7  * HELM is free software; you can redistribute it and/or
   8  * modify it under the terms of the GNU General Public License
   9  * as published by the Free Software Foundation; either version 2
  10  * of the License, or (at your option) any later version.
  11  *
  12  * HELM is distributed in the hope that it will be useful,
  13  * but WITHOUT ANY WARRANTY; without even the implied warranty of
  14  * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
  15  * GNU General Public License for more details.
  16  *
  17  * You should have received a copy of the GNU General Public License
  18  * along with HELM; if not, write to the Free Software
  19  * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
  20  * MA  02111-1307, USA.
  21  *
  22  * For details, see the HELM World-Wide-Web page,
  23  * http://helm.cs.unibo.it/
  24  *)
  25
  26 open Printf
  27
  28 let critical_value = 6
  29 let just_factor = 3
  30
  31 module StringSet = Set.Make (String)
  32 module SetSet = Set.Make (StringSet)
  33
  34 type term_signature = (string * string list) option * StringSet.t
  35
  36 type cardinality_condition =
  37   | Eq of int
  38   | Gt of int
  39
  40 let tbln n = "table" ^ string_of_int n
  41
  42 let add_depth_constr depth_opt cur_tbl where =
  43   match depth_opt with
  44   | None -> where
  45   | Some depth -> (sprintf "%s.h_depth = %d" cur_tbl depth) :: where
  46
  47 let add_card_constr tbl (n,from,where) = function
  48   | None -> (n,from,where)
  49   | Some (Eq card) ->
  50       (n+1,
  51        (sprintf "%s as %s" tbl (tbln n) :: from),
  52        (sprintf "no=%d" card ::
  53         (if n=0 then []
  54         else [sprintf "table0.source = %s.source" (tbln n)]) @
  55         where))
  56   | Some (Gt card) ->
  57       (n+1,
  58        (sprintf "%s as %s" tbl (tbln n) :: from),
  59        (sprintf "no>%d" card ::
  60         (if n=0 then []
  61         else [sprintf "table0.source = %s.source" (tbln n)]) @
  62         where))
  63
  64 let at_least ~(dbh:Dbi.connection) ?concl_card ?full_card
  65   (metadata: MetadataTypes.metadata list)
  66 =
  67   if (metadata = []) && concl_card = None && full_card = None then
  68     failwith "MetadataQuery.at_least: no constraints given";
  69   let add_constraint (n,from,where) metadata =
  70     let cur_tbl = tbln n in
  71     match metadata with
  72     | `Obj (uri, pos, depth_opt) ->
  73         let tbl = MetadataTypes.obj_tbl in
  74         let pos_str = MetadataPp.pp_position pos in
  75         let from = (sprintf "%s as %s" tbl cur_tbl) :: from in
  76         let where =
  77           (sprintf "%s.h_position = \"%s\"" cur_tbl pos_str) ::
  78           (sprintf "%s.h_occurrence = \"%s\"" cur_tbl uri) ::
  79           (if n=0 then []
  80           else [sprintf "table0.source = %s.source" cur_tbl]) @
  81           where
  82         in
  83         let where = add_depth_constr depth_opt cur_tbl where in
  84         ((n+1), from, where)
  85     | `Rel (pos, depth) ->
  86         let tbl = MetadataTypes.rel_tbl in
  87         let pos_str = MetadataPp.pp_position (pos :> MetadataTypes.position) in
  88         let from = (sprintf "%s as %s" tbl cur_tbl) :: from in
  89         let where =
  90           (sprintf "%s.h_position = \"%s\"" cur_tbl pos_str) ::
  91           (if n=0 then []
  92           else [sprintf "table0.source = %s.source" cur_tbl]) @
  93           where
  94         in
  95         let where = add_depth_constr (Some depth) cur_tbl where in
  96         ((n+1), from, where)
  97     | `Sort (sort, pos, depth) ->
  98         let tbl = MetadataTypes.sort_tbl in
  99         let pos_str = MetadataPp.pp_position (pos :> MetadataTypes.position) in
 100         let sort_str = MetadataPp.pp_sort sort in
 101         let from = (sprintf "%s as %s" tbl cur_tbl) :: from in
 102         let where =
 103           (sprintf "%s.h_position = \"%s\"" cur_tbl pos_str) ::
 104           (sprintf "%s.h_sort = \"%s\"" cur_tbl sort_str) ::
 105           (if n=0 then []
 106           else [sprintf "table0.source = %s.source" cur_tbl]) @
 107           where
 108         in
 109         let where = add_depth_constr (Some depth) cur_tbl where in
 110         ((n+1), from, where)
 111   in
 112   let (n,from,where) = List.fold_left add_constraint (0,[],[]) metadata in
 113   let (n,from,where) =
 114     add_card_constr MetadataTypes.conclno_tbl (n,from,where) concl_card
 115   in
 116   let (n,from,where) =
 117     add_card_constr MetadataTypes.conclno_hyp_tbl (n,from,where) full_card
 118   in
 119   let from = String.concat ", " from in
 120   let where = String.concat " and " where in
 121   let query = sprintf "select table0.source from %s where %s" from where in
 122 prerr_endline query;
 123   let query = dbh#prepare query in
 124   query#execute [];
 125   List.map (function [`String s] -> s | _ -> assert false) (query#fetchall ())
 126
 127   (** Prefix handling *)
 128
 129 let filter_by_card n =
 130   SetSet.filter (fun t -> (StringSet.cardinal t) <= n)
 131
 132 let merge n a b =
 133   let init = SetSet.union a b in
 134   let merge_single_set s1 b =
 135     SetSet.fold
 136       (fun s2 res -> SetSet.add (StringSet.union s1 s2) res)
 137       b SetSet.empty in
 138   let res =
 139     SetSet.fold (fun s1 res -> SetSet.union (merge_single_set s1 b) res) a init
 140   in
 141   filter_by_card n res
 142
 143 let rec inspect_children n childs =
 144   List.fold_left
 145     (fun res term -> merge n (inspect_conclusion n term) res)
 146     SetSet.empty childs
 147
 148 and add_root n root childs =
 149   let childunion = inspect_children n childs in
 150   let addroot = StringSet.add root in
 151     SetSet.fold
 152       (fun child newsets -> SetSet.add (addroot child) newsets)
 153       childunion
 154       (SetSet.singleton (StringSet.singleton root))
 155
 156 and inspect_conclusion n t =
 157 if n = 0 then SetSet.empty
 158 else match t with
 159       Cic.Rel _
 160     | Cic.Meta _
 161     | Cic.Sort _
 162     | Cic.Implicit _ -> SetSet.empty
 163     | Cic.Var (u,exp_named_subst) -> SetSet.empty
 164     | Cic.Const (u,exp_named_subst) ->
 165         SetSet.singleton (StringSet.singleton (UriManager.string_of_uri u))
 166     | Cic.MutInd (u, t, exp_named_subst) ->
 167         SetSet.singleton (StringSet.singleton
 168           (UriManager.string_of_uriref (u, [t])))
 169     | Cic.MutConstruct (u, t, c, exp_named_subst) ->
 170         SetSet.singleton (StringSet.singleton
 171           (UriManager.string_of_uriref (u, [t; c])))
 172     | Cic.Cast (t, _) -> inspect_conclusion n t
 173     | Cic.Prod (_, s, t) ->
 174         merge n (inspect_conclusion n s) (inspect_conclusion n t)
 175     | Cic.Lambda (_, s, t) ->
 176         merge n (inspect_conclusion n s) (inspect_conclusion n t)
 177     | Cic.LetIn (_, s, t) ->
 178         merge n (inspect_conclusion n s) (inspect_conclusion n t)
 179     | Cic.Appl ((Cic.Const (u,exp_named_subst))::l) ->
 180         let suri = UriManager.string_of_uri u in
 181         add_root (n-1) suri l
 182     | Cic.Appl ((Cic.MutInd (u, t, exp_named_subst))::l) ->
 183         let suri = UriManager.string_of_uriref (u, [t]) in
 184         add_root (n-1) suri l
 185     | Cic.Appl ((Cic.MutConstruct (u, t, c, exp_named_subst))::l)  ->
 186         let suri = UriManager.string_of_uriref (u, [t; c]) in
 187         add_root (n-1) suri l
 188     | Cic.Appl l ->
 189         SetSet.empty
 190     | Cic.MutCase (u, t, tt, uu, m) ->
 191         SetSet.empty
 192     | Cic.Fix (_, m) ->
 193         SetSet.empty
 194     | Cic.CoFix (_, m) ->
 195         SetSet.empty
 196
 197 let rec inspect_term n t =
 198   if n = 0 then
 199     assert false
 200   else
 201     match t with
 202       Cic.Rel _
 203     | Cic.Meta _
 204     | Cic.Sort _
 205     | Cic.Implicit _ -> None, SetSet.empty
 206     | Cic.Var (u,exp_named_subst) -> None, SetSet.empty
 207     | Cic.Const (u,exp_named_subst) ->
 208         Some (UriManager.string_of_uri u), SetSet.empty
 209     | Cic.MutInd (u, t, exp_named_subst) ->
 210         let uri = UriManager.string_of_uriref (u, [t]) in
 211         Some uri, SetSet.empty
 212     | Cic.MutConstruct (u, t, c, exp_named_subst) ->
 213         let uri = UriManager.string_of_uriref (u, [t; c]) in
 214         Some uri, SetSet.empty
 215     | Cic.Cast (t, _) -> inspect_term n t
 216     | Cic.Prod (_, _, t) -> inspect_term n t
 217     | Cic.LetIn (_, _, t) -> inspect_term n t
 218     | Cic.Appl ((Cic.Const (u,exp_named_subst))::l) ->
 219         let suri = UriManager.string_of_uri u in
 220         let childunion = inspect_children (n-1) l in
 221         Some suri, childunion
 222     | Cic.Appl ((Cic.MutInd (u, t, exp_named_subst))::l) ->
 223         let suri = UriManager.string_of_uriref (u, [t]) in
 224         if u = HelmLibraryObjects.Logic.eq_URI && n>1 then
 225           (* equality is handled in a special way: in particular,
 226              the type, if defined, is always added to the prefix,
 227              and n is not decremented - it should have been n-2 *)
 228           match l with
 229               Cic.Const (u1,exp_named_subst1)::l1 ->
 230                 let suri1 = UriManager.string_of_uri u1 in
 231                 let inconcl = add_root (n-1) suri1 l1 in
 232                 Some suri, inconcl
 233             | Cic.MutInd (u1, t1, exp_named_subst1)::l1 ->
 234                 let suri1 = UriManager.string_of_uriref (u1, [t1]) in
 235                 let inconcl = add_root (n-1) suri1 l1 in
 236                 Some suri, inconcl
 237             | Cic.MutConstruct (u1, t1, c1, exp_named_subst1)::l1 ->
 238                 let suri1 = UriManager.string_of_uriref (u1, [t1; c1]) in
 239                 let inconcl = add_root (n-1) suri1 l1 in
 240                 Some suri, inconcl
 241             | _ :: _ -> Some suri, SetSet.empty
 242             | _ -> assert false (* args number must be > 0 *)
 243         else
 244           let childunion = inspect_children (n-1) l in
 245           Some suri, childunion
 246     | Cic.Appl ((Cic.MutConstruct (u, t, c, exp_named_subst))::l)  ->
 247         let suri = UriManager.string_of_uriref (u, [t; c]) in
 248         let childunion = inspect_children (n-1) l in
 249         Some suri, childunion
 250     | _ -> None, SetSet.empty
 251
 252 let add_cardinality s =
 253   let l = SetSet.elements s in
 254   let res =
 255     List.map
 256       (fun set ->
 257          let el = StringSet.elements set in
 258          (List.length el, el)) l in
 259     (* ordered by descending cardinality *)
 260     List.sort (fun (n,_) (m,_) -> m - n) ((0,[])::res)
 261
 262 let prefixes n t =
 263   match inspect_term n t with
 264       Some a, set -> Some a, add_cardinality set
 265     | None, set when (SetSet.is_empty set) -> None, []
 266     | _, _ -> assert false
 267
 268
 269 let rec add children =
 270   List.fold_left
 271     (fun acc t -> StringSet.union (signature_concl t) acc)
 272     (StringSet.empty) children
 273
 274 (* this function creates the set of all different constants appearing in
 275    the conclusion of the term *)
 276 and signature_concl =
 277   function
 278       Cic.Rel _
 279     | Cic.Meta _
 280     | Cic.Sort _
 281     | Cic.Implicit _ -> StringSet.empty
 282     | Cic.Var (u,exp_named_subst) -> StringSet.empty
 283     | Cic.Const (u,exp_named_subst) ->
 284         StringSet.singleton (UriManager.string_of_uri u)
 285     | Cic.MutInd (u, t, exp_named_subst) ->
 286         let uri = UriManager.string_of_uriref (u, [t]) in
 287         StringSet.singleton uri
 288     | Cic.MutConstruct (u, t, c, exp_named_subst) ->
 289         let uri = UriManager.string_of_uriref (u, [t;c]) in
 290         StringSet.singleton uri
 291     | Cic.Cast (t, _) -> signature_concl t
 292     | Cic.Prod (_, s, t) ->
 293         StringSet.union (signature_concl s) (signature_concl t)
 294     | Cic.Lambda (_, s, t) ->
 295         StringSet.union (signature_concl s) (signature_concl t)
 296     | Cic.LetIn (_, s, t) ->
 297         StringSet.union (signature_concl s) (signature_concl t)
 298     | Cic.Appl l  -> add l
 299     | Cic.MutCase _
 300     | Cic.Fix _
 301     | Cic.CoFix _ ->
 302         StringSet.empty
 303
 304 let rec signature_of = function
 305   | Cic.Cast (t, _)      -> signature_of t
 306   | Cic.Prod (_, _, t)   -> signature_of t
 307   | Cic.LetIn (_, _, t) -> signature_of t
 308   | Cic.Appl ((Cic.Const (u,exp_named_subst))::l) ->
 309       let suri = UriManager.string_of_uri u in
 310       Some (suri, []), add l
 311   | Cic.Appl ((Cic.MutInd (u, t, exp_named_subst))::l) ->
 312       let suri = UriManager.string_of_uriref (u, [t]) in
 313       if u = HelmLibraryObjects.Logic.eq_URI then
 314           (* equality is handled in a special way: in particular,
 315              the type, if defined, is always added to the prefix,
 316              and n is not decremented - it should have been n-2 *)
 317       match l with
 318           Cic.Const (u1,exp_named_subst1)::l1 ->
 319             let suri1 = UriManager.string_of_uri u1 in
 320             let inconcl = StringSet.remove suri1 (add l1) in
 321             Some (suri, [suri1]), inconcl
 322         | Cic.MutInd (u1, t1, exp_named_subst1)::l1 ->
 323             let suri1 = UriManager.string_of_uriref (u1, [t1]) in
 324             let inconcl =  StringSet.remove suri1 (add l1) in
 325               Some (suri, [suri1]), inconcl
 326         | Cic.MutConstruct (u1, t1, c1, exp_named_subst1)::l1 ->
 327             let suri1 = UriManager.string_of_uriref (u1, [t1;c1]) in
 328             let inconcl =  StringSet.remove suri1 (add l1) in
 329             Some (suri, [suri1]), inconcl
 330         | _ :: _ -> Some (suri, []), StringSet.empty
 331         | _ -> assert false (* args number must be > 0 *)
 332       else
 333         Some (suri, []), add l
 334   | Cic.Appl ((Cic.MutConstruct (u, t, c, exp_named_subst))::l)  ->
 335       let suri = UriManager.string_of_uriref (u, [t;c]) in
 336       Some (suri, []), add l
 337   | t -> None, signature_concl t
 338
 339 (* takes a list of lists and returns the list of all elements
 340    without repetitions *)
 341 let union l =
 342   let rec drop_repetitions = function
 343       [] -> []
 344     | [a] -> [a]
 345     | u1::u2::l when u1 = u2 -> drop_repetitions (u2::l)
 346     | u::l -> u::(drop_repetitions l) in
 347   drop_repetitions (List.sort Pervasives.compare (List.concat l))
 348
 349 let must_of_prefix m s =
 350   let s' = List.map (fun u -> `Obj (u, `InConclusion, None)) s in
 351   `Obj (m, `MainConclusion, None) :: s'
 352
 353 let escape = Str.global_replace (Str.regexp_string "\'") "\\'"
 354
 355 let get_inconcl (dbh:Dbi.connection) uri =
 356   let uri = escape uri in
 357   let query =
 358     dbh#prepare (sprintf "select h_occurrence from refObj where source=\"%s\" and (h_position=\"MainConclusion\" or h_position=\"InConclusion\")"
 359       uri)
 360   in
 361   query#execute [];
 362   query#fold_left (* transform the result in a set *)
 363     (fun set fields ->
 364       let uri = match fields with [`String uri] -> uri | _ -> assert false in
 365       StringSet.add uri set)
 366     StringSet.empty
 367
 368 let test_only ~(dbh:Dbi.connection) only u =
 369   let inconcl = get_inconcl dbh u in
 370   StringSet.subset inconcl only
 371
 372   (* Special handling of equality. The problem is filtering out theorems just
 373   * containing variables (e.g. all the theorems in cic:/Coq/Ring/). Really
 374   * ad-hoc, no better solution found at the moment *)
 375 let myspeciallist =
 376   [0,"cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)";
 377    0,"cic:/Coq/Init/Logic/sym_eq.con";
 378    0,"cic:/Coq/Init/Logic/trans_eq.con";
 379    0,"cic:/Coq/Init/Logic/f_equal.con";
 380    0,"cic:/Coq/Init/Logic/f_equal2.con";
 381    0,"cic:/Coq/Init/Logic/f_equal3.con"]
 382
 383 let compute_exactly ~(dbh:Dbi.connection) main prefixes =
 384   List.concat
 385     (List.map
 386       (fun (m,s) ->
 387         if (m = 0) then
 388           myspeciallist
 389         else
 390           let res =
 391             at_least ~dbh ~concl_card:(Eq (m+1)) (must_of_prefix main s)
 392           in
 393           List.map (fun uri -> (m, uri)) res)
 394       prefixes)
 395
 396   (* critical value reached, fallback to "only" constraints *)
 397 let compute_with_only ~(dbh:Dbi.connection) main prefixes constants =
 398   let max_prefix_length =
 399     match prefixes with
 400     | [] -> assert false
 401     | (max,_)::_ -> max in
 402   let maximal_prefixes =
 403     let rec filter res = function
 404         [] -> res
 405       | (n,s)::l when n = max_prefix_length -> filter ((n,s)::res) l
 406       | _::_-> res in
 407     filter [] prefixes in
 408   let greater_than =
 409     let all =
 410       union
 411         (List.map
 412           (fun (m,s) ->
 413             (let res =
 414               at_least ~dbh ~concl_card:(Gt (m+1)) (must_of_prefix main s)
 415             in
 416             (* we tag the uri with m+1, for sorting purposes *)
 417             List.map (fun uri -> (m+1, uri)) res))
 418           maximal_prefixes)
 419     in
 420     List.filter (function (_,uri) -> test_only ~dbh constants uri) all in
 421     let equal_to = compute_exactly ~dbh main prefixes in
 422     greater_than @ equal_to
 423
 424   (* real match query implementation *)
 425 let cmatch ~(dbh:Dbi.connection) t =
 426   let (main, constants) = signature_of t in
 427   match main with
 428   | None -> []
 429   | Some (main, types) ->
 430       (* the type of eq is not counted in constants_no *)
 431       let constants_no = StringSet.cardinal constants in
 432       if (constants_no > critical_value) then
 433         let prefixes = prefixes just_factor t in
 434         (match prefixes with
 435         | Some main, all_concl ->
 436             let all_constants =
 437               List.fold_right StringSet.add types (StringSet.add main constants)
 438             in
 439             compute_with_only ~dbh main all_concl all_constants
 440          | _, _ -> [])
 441       else if constants_no = 0 then []
 442       else
 443         (* in this case we compute all prefixes, and we do not need
 444            to apply the only constraints *)
 445         let prefixes = prefixes constants_no t in
 446         (match prefixes with
 447              Some main, all_concl ->
 448                List.concat
 449                  (List.map
 450                     (fun (m,s) ->
 451                       (let res =
 452                         at_least ~dbh ~concl_card:(Eq (m+1))
 453                           (must_of_prefix main s)
 454                       in
 455                       List.map (fun uri -> (m, uri)) res))
 456                     all_concl)
 457            | _, _ -> [])
 458
 459 let power_upto upto consts =
 460   let l = StringSet.elements consts in
 461   List.sort (fun (n,_) (m,_) -> m - n)
 462   (List.fold_left
 463     (fun res a ->
 464        List.filter (function (n,l) -> n <= upto)
 465        res@(List.map (function (n,l) -> (n+1,a::l)) res))
 466      [(0,[])] l)
 467
 468 let power consts =
 469   let l = StringSet.elements consts in
 470   List.sort (fun (n,_) (m,_) -> m - n)
 471   (List.fold_left
 472     (fun res a -> res@(List.map (function (n,l) -> (n+1,a::l)) res))
 473      [(0,[])] l)
 474
 475 let sigmatch ~(dbh:Dbi.connection) (main, constants) =
 476   match main with
 477     None -> []
 478   | Some (main, types) ->
 479       let constants_no = StringSet.cardinal constants in
 480       if (constants_no > critical_value) then
 481         let subsets =
 482           let subsets = power_upto just_factor constants in
 483           let types_no = List.length types in
 484           List.map (function (n,l) -> (n+types_no,types@l)) subsets
 485         in
 486         let all_constants =
 487           List.fold_right StringSet.add types (StringSet.add main constants)
 488         in
 489         compute_with_only ~dbh main subsets all_constants
 490       else
 491         let subsets =
 492           let subsets = power constants in
 493           let types_no = List.length types in
 494           List.map (function (n,l) -> (n+types_no,types@l)) subsets
 495         in
 496         compute_exactly ~dbh main subsets
 497
 498   (* match query wrappers *)
 499 let cmatch' = cmatch
 500 let cmatch ~dbh term =
 501   List.map snd
 502     (List.sort
 503       (fun x y -> Pervasives.compare (fst y) (fst x))
 504       (cmatch' ~dbh term))
 505
 506 let constants_of = signature_concl
 507