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 (*
  43 let add_depth_constr depth_opt cur_tbl where =
  44   match depth_opt with
  45   | None -> where
  46   | Some depth -> (sprintf "%s.h_depth = %d" cur_tbl depth) :: where
  47 *)
  48
  49 let mk_positions positions cur_tbl =
  50   "(" ^
  51   String.concat " or "
  52     (List.map
  53       (fun pos ->
  54         let pos_str = MetadataPp.pp_position_tag pos in
  55         match pos with
  56         | `InBody
  57         | `InConclusion
  58         | `InHypothesis
  59         | `MainConclusion None
  60         | `MainHypothesis None ->
  61             sprintf "%s.h_position = \"%s\"" cur_tbl pos_str
  62         | `MainConclusion (Some d)
  63         | `MainHypothesis (Some d) ->
  64             sprintf "(%s.h_position = \"%s\" and %s.h_depth = %d)"
  65               cur_tbl pos_str cur_tbl d)
  66       (positions :> MetadataTypes.position list)) ^
  67   ")"
  68
  69 let add_card_constr tbl (n,from,where) = function
  70   | None -> (n,from,where)
  71   | Some (Eq card) ->
  72       let cur_tbl = tbln n in
  73       (n+1,
  74        (sprintf "%s as %s" tbl cur_tbl :: from),
  75        (sprintf "%s.no=%d" cur_tbl card ::
  76         (if n=0 then []
  77         else [sprintf "table0.source = %s.source" cur_tbl]) @
  78         where))
  79   | Some (Gt card) ->
  80       let cur_tbl = tbln n in
  81       (n+1,
  82        (sprintf "%s as %s" tbl cur_tbl :: from),
  83        (sprintf "%s.no>%d" cur_tbl card ::
  84         (if n=0 then []
  85         else [sprintf "table0.source = %s.source" cur_tbl]) @
  86         where))
  87
  88 let at_least ~(dbd:Mysql.dbd) ?concl_card ?full_card
  89   (metadata: MetadataTypes.constr list)
  90 =
  91   if (metadata = []) && concl_card = None && full_card = None then
  92     failwith "MetadataQuery.at_least: no constraints given";
  93   let add_constraint (n,from,where) metadata =
  94     let cur_tbl = tbln n in
  95     match metadata with
  96     | `Obj (uri, positions) ->
  97         let tbl = MetadataTypes.obj_tbl in
  98         let from = (sprintf "%s as %s" tbl cur_tbl) :: from in
  99         let where =
 100           (sprintf "%s.h_occurrence = \"%s\"" cur_tbl uri) ::
 101           mk_positions positions cur_tbl ::
 102           (if n=0 then []
 103           else [sprintf "table0.source = %s.source" cur_tbl]) @
 104           where
 105         in
 106         ((n+1), from, where)
 107     | `Rel positions ->
 108         let tbl = MetadataTypes.rel_tbl in
 109         let from = (sprintf "%s as %s" tbl cur_tbl) :: from in
 110         let where =
 111           mk_positions positions cur_tbl ::
 112           (if n=0 then []
 113           else [sprintf "table0.source = %s.source" cur_tbl]) @
 114           where
 115         in
 116         ((n+1), from, where)
 117     | `Sort (sort, positions) ->
 118         let tbl = MetadataTypes.sort_tbl in
 119         let sort_str = MetadataPp.pp_sort sort in
 120         let from = (sprintf "%s as %s" tbl cur_tbl) :: from in
 121         let where =
 122           (sprintf "%s.h_sort = \"%s\"" cur_tbl sort_str) ::
 123           mk_positions positions cur_tbl ::
 124           (if n=0 then []
 125           else [sprintf "table0.source = %s.source" cur_tbl]) @
 126           where
 127         in
 128         ((n+1), from, where)
 129   in
 130   let (n,from,where) = List.fold_left add_constraint (0,[],[]) metadata in
 131   let (n,from,where) =
 132     add_card_constr MetadataTypes.conclno_tbl (n,from,where) concl_card
 133   in
 134   let (n,from,where) =
 135     add_card_constr MetadataTypes.conclno_hyp_tbl (n,from,where) full_card
 136   in
 137   let from = String.concat ", " from in
 138   let where = String.concat " and " where in
 139   let query = sprintf "select table0.source from %s where %s" from where in
 140   let result = Mysql.exec dbd query in
 141   Mysql.map result
 142     (fun row -> match row.(0) with Some s -> s | _ -> assert false)
 143
 144   (** Prefix handling *)
 145
 146 let filter_by_card n =
 147   SetSet.filter (fun t -> (StringSet.cardinal t) <= n)
 148
 149 let merge n a b =
 150   let init = SetSet.union a b in
 151   let merge_single_set s1 b =
 152     SetSet.fold
 153       (fun s2 res -> SetSet.add (StringSet.union s1 s2) res)
 154       b SetSet.empty in
 155   let res =
 156     SetSet.fold (fun s1 res -> SetSet.union (merge_single_set s1 b) res) a init
 157   in
 158   filter_by_card n res
 159
 160 let rec inspect_children n childs =
 161   List.fold_left
 162     (fun res term -> merge n (inspect_conclusion n term) res)
 163     SetSet.empty childs
 164
 165 and add_root n root childs =
 166   let childunion = inspect_children n childs in
 167   let addroot = StringSet.add root in
 168     SetSet.fold
 169       (fun child newsets -> SetSet.add (addroot child) newsets)
 170       childunion
 171       (SetSet.singleton (StringSet.singleton root))
 172
 173 and inspect_conclusion n t =
 174   if n = 0 then SetSet.empty
 175   else match t with
 176       Cic.Rel _
 177     | Cic.Meta _
 178     | Cic.Sort _
 179     | Cic.Implicit _ -> SetSet.empty
 180     | Cic.Var (u,exp_named_subst) -> SetSet.empty
 181     | Cic.Const (u,exp_named_subst) ->
 182         SetSet.singleton (StringSet.singleton (UriManager.string_of_uri u))
 183     | Cic.MutInd (u, t, exp_named_subst) ->
 184         SetSet.singleton (StringSet.singleton
 185           (UriManager.string_of_uriref (u, [t])))
 186     | Cic.MutConstruct (u, t, c, exp_named_subst) ->
 187         SetSet.singleton (StringSet.singleton
 188           (UriManager.string_of_uriref (u, [t; c])))
 189     | Cic.Cast (t, _) -> inspect_conclusion n t
 190     | Cic.Prod (_, s, t) ->
 191         merge n (inspect_conclusion n s) (inspect_conclusion n t)
 192     | Cic.Lambda (_, s, t) ->
 193         merge n (inspect_conclusion n s) (inspect_conclusion n t)
 194     | Cic.LetIn (_, s, t) ->
 195         merge n (inspect_conclusion n s) (inspect_conclusion n t)
 196     | Cic.Appl ((Cic.Const (u,exp_named_subst))::l) ->
 197         let suri = UriManager.string_of_uri u in
 198         add_root (n-1) suri l
 199     | Cic.Appl ((Cic.MutInd (u, t, exp_named_subst))::l) ->
 200         let suri = UriManager.string_of_uriref (u, [t]) in
 201         add_root (n-1) suri l
 202     | Cic.Appl ((Cic.MutConstruct (u, t, c, exp_named_subst))::l)  ->
 203         let suri = UriManager.string_of_uriref (u, [t; c]) in
 204         add_root (n-1) suri l
 205     | Cic.Appl l ->
 206         SetSet.empty
 207     | Cic.MutCase (u, t, tt, uu, m) ->
 208         SetSet.empty
 209     | Cic.Fix (_, m) ->
 210         SetSet.empty
 211     | Cic.CoFix (_, m) ->
 212         SetSet.empty
 213
 214 let rec inspect_term n t =
 215   if n = 0 then
 216     assert false
 217   else
 218     match t with
 219       Cic.Rel _
 220     | Cic.Meta _
 221     | Cic.Sort _
 222     | Cic.Implicit _ -> None, SetSet.empty
 223     | Cic.Var (u,exp_named_subst) -> None, SetSet.empty
 224     | Cic.Const (u,exp_named_subst) ->
 225         Some (UriManager.string_of_uri u), SetSet.empty
 226     | Cic.MutInd (u, t, exp_named_subst) ->
 227         let uri = UriManager.string_of_uriref (u, [t]) in
 228         Some uri, SetSet.empty
 229     | Cic.MutConstruct (u, t, c, exp_named_subst) ->
 230         let uri = UriManager.string_of_uriref (u, [t; c]) in
 231         Some uri, SetSet.empty
 232     | Cic.Cast (t, _) -> inspect_term n t
 233     | Cic.Prod (_, _, t) -> inspect_term n t
 234     | Cic.LetIn (_, _, t) -> inspect_term n t
 235     | Cic.Appl ((Cic.Const (u,exp_named_subst))::l) ->
 236         let suri = UriManager.string_of_uri u in
 237         let childunion = inspect_children (n-1) l in
 238         Some suri, childunion
 239     | Cic.Appl ((Cic.MutInd (u, t, exp_named_subst))::l) ->
 240         let suri = UriManager.string_of_uriref (u, [t]) in
 241         if u = HelmLibraryObjects.Logic.eq_URI && n>1 then
 242           (* equality is handled in a special way: in particular,
 243              the type, if defined, is always added to the prefix,
 244              and n is not decremented - it should have been n-2 *)
 245           match l with
 246               Cic.Const (u1,exp_named_subst1)::l1 ->
 247                 let suri1 = UriManager.string_of_uri u1 in
 248                 let inconcl = add_root (n-1) suri1 l1 in
 249                 Some suri, inconcl
 250             | Cic.MutInd (u1, t1, exp_named_subst1)::l1 ->
 251                 let suri1 = UriManager.string_of_uriref (u1, [t1]) in
 252                 let inconcl = add_root (n-1) suri1 l1 in
 253                 Some suri, inconcl
 254             | Cic.MutConstruct (u1, t1, c1, exp_named_subst1)::l1 ->
 255                 let suri1 = UriManager.string_of_uriref (u1, [t1; c1]) in
 256                 let inconcl = add_root (n-1) suri1 l1 in
 257                 Some suri, inconcl
 258             | _ :: _ -> Some suri, SetSet.empty
 259             | _ -> assert false (* args number must be > 0 *)
 260         else
 261           let childunion = inspect_children (n-1) l in
 262           Some suri, childunion
 263     | Cic.Appl ((Cic.MutConstruct (u, t, c, exp_named_subst))::l)  ->
 264         let suri = UriManager.string_of_uriref (u, [t; c]) in
 265         let childunion = inspect_children (n-1) l in
 266         Some suri, childunion
 267     | _ -> None, SetSet.empty
 268
 269 let add_cardinality s =
 270   let l = SetSet.elements s in
 271   let res =
 272     List.map
 273       (fun set ->
 274          let el = StringSet.elements set in
 275          (List.length el, el)) l in
 276     (* ordered by descending cardinality *)
 277     List.sort (fun (n,_) (m,_) -> m - n) ((0,[])::res)
 278
 279 let prefixes n t =
 280   match inspect_term n t with
 281       Some a, set -> Some a, add_cardinality set
 282     | None, set when (SetSet.is_empty set) -> None, []
 283     | _, _ -> assert false
 284
 285
 286 let rec add children =
 287   List.fold_left
 288     (fun acc t -> StringSet.union (signature_concl t) acc)
 289     (StringSet.empty) children
 290
 291 (* this function creates the set of all different constants appearing in
 292    the conclusion of the term *)
 293 and signature_concl =
 294   function
 295       Cic.Rel _
 296     | Cic.Meta _
 297     | Cic.Sort _
 298     | Cic.Implicit _ -> StringSet.empty
 299     | Cic.Var (u,exp_named_subst) -> StringSet.empty
 300     | Cic.Const (u,exp_named_subst) ->
 301         StringSet.singleton (UriManager.string_of_uri u)
 302     | Cic.MutInd (u, t, exp_named_subst) ->
 303         let uri = UriManager.string_of_uriref (u, [t]) in
 304         StringSet.singleton uri
 305     | Cic.MutConstruct (u, t, c, exp_named_subst) ->
 306         let uri = UriManager.string_of_uriref (u, [t;c]) in
 307         StringSet.singleton uri
 308     | Cic.Cast (t, _) -> signature_concl t
 309     | Cic.Prod (_, s, t) ->
 310         StringSet.union (signature_concl s) (signature_concl t)
 311     | Cic.Lambda (_, s, t) ->
 312         StringSet.union (signature_concl s) (signature_concl t)
 313     | Cic.LetIn (_, s, t) ->
 314         StringSet.union (signature_concl s) (signature_concl t)
 315     | Cic.Appl l  -> add l
 316     | Cic.MutCase _
 317     | Cic.Fix _
 318     | Cic.CoFix _ ->
 319         StringSet.empty
 320
 321 let rec signature_of = function
 322   | Cic.Cast (t, _)      -> signature_of t
 323   | Cic.Prod (_, _, t)   -> signature_of t
 324   | Cic.LetIn (_, _, t) -> signature_of t
 325   | Cic.Appl ((Cic.Const (u,exp_named_subst))::l) ->
 326       let suri = UriManager.string_of_uri u in
 327       Some (suri, []), add l
 328   | Cic.Appl ((Cic.MutInd (u, t, exp_named_subst))::l) ->
 329       let suri = UriManager.string_of_uriref (u, [t]) in
 330       if u = HelmLibraryObjects.Logic.eq_URI then
 331           (* equality is handled in a special way: in particular,
 332              the type, if defined, is always added to the prefix,
 333              and n is not decremented - it should have been n-2 *)
 334       match l with
 335           Cic.Const (u1,exp_named_subst1)::l1 ->
 336             let suri1 = UriManager.string_of_uri u1 in
 337             let inconcl = StringSet.remove suri1 (add l1) in
 338             Some (suri, [suri1]), inconcl
 339         | Cic.MutInd (u1, t1, exp_named_subst1)::l1 ->
 340             let suri1 = UriManager.string_of_uriref (u1, [t1]) in
 341             let inconcl =  StringSet.remove suri1 (add l1) in
 342               Some (suri, [suri1]), inconcl
 343         | Cic.MutConstruct (u1, t1, c1, exp_named_subst1)::l1 ->
 344             let suri1 = UriManager.string_of_uriref (u1, [t1;c1]) in
 345             let inconcl =  StringSet.remove suri1 (add l1) in
 346             Some (suri, [suri1]), inconcl
 347         | _ :: _ -> Some (suri, []), StringSet.empty
 348         | _ -> assert false (* args number must be > 0 *)
 349       else
 350         Some (suri, []), add l
 351   | Cic.Appl ((Cic.MutConstruct (u, t, c, exp_named_subst))::l)  ->
 352       let suri = UriManager.string_of_uriref (u, [t;c]) in
 353       Some (suri, []), add l
 354   | t -> None, signature_concl t
 355
 356 (* takes a list of lists and returns the list of all elements
 357    without repetitions *)
 358 let union l =
 359   let rec drop_repetitions = function
 360       [] -> []
 361     | [a] -> [a]
 362     | u1::u2::l when u1 = u2 -> drop_repetitions (u2::l)
 363     | u::l -> u::(drop_repetitions l) in
 364   drop_repetitions (List.sort Pervasives.compare (List.concat l))
 365
 366 let must_of_prefix ?(where = `Conclusion) m s =
 367   let positions =
 368     match where with
 369     | `Conclusion -> [`InConclusion]
 370     | `Statement -> [`InConclusion; `InHypothesis; `MainHypothesis None]
 371   in
 372   let s' = List.map (fun u -> `Obj (u, positions)) s in
 373   `Obj (m, [`MainConclusion None]) :: s'
 374
 375 let escape = Str.global_replace (Str.regexp_string "\'") "\\'"
 376
 377 let get_constants (dbd:Mysql.dbd) ~where uri =
 378   let uri = escape uri in
 379   let positions =
 380     match where with
 381     | `Conclusion -> ["\"MainConclusion\""; "\"InConclusion\""]
 382     | `Statement ->
 383         ["\"MainConclusion\""; "\"InConclusion\""; "\"InHypothesis\"";
 384          "\"MainHypothesis\""]
 385   in
 386   let query =
 387     sprintf "select h_occurrence from refObj where source=\"%s\" and (%s)"
 388       uri (String.concat " or " positions)
 389   in
 390   let result = Mysql.exec dbd query in
 391   let set = ref StringSet.empty in
 392   Mysql.iter result
 393     (fun col ->
 394       match col.(0) with
 395       | Some uri -> set := StringSet.add uri !set
 396       | _ -> assert false);
 397   !set
 398
 399 let at_most ~(dbd:Mysql.dbd) ?(where = `Conclusion) only u =
 400   let inconcl = get_constants dbd ~where u in
 401   StringSet.subset inconcl only
 402
 403   (* Special handling of equality. The problem is filtering out theorems just
 404   * containing variables (e.g. all the theorems in cic:/Coq/Ring/). Really
 405   * ad-hoc, no better solution found at the moment *)
 406 let myspeciallist =
 407   [0,"cic:/Coq/Init/Logic/eq.ind#xpointer(1/1/1)";
 408    0,"cic:/Coq/Init/Logic/sym_eq.con";
 409    0,"cic:/Coq/Init/Logic/trans_eq.con";
 410    0,"cic:/Coq/Init/Logic/f_equal.con";
 411    0,"cic:/Coq/Init/Logic/f_equal2.con";
 412    0,"cic:/Coq/Init/Logic/f_equal3.con"]
 413
 414 let compute_exactly ~(dbd:Mysql.dbd) where main prefixes =
 415   List.concat
 416     (List.map
 417       (fun (m,s) ->
 418         if (m = 0) then
 419           myspeciallist
 420         else
 421           let res =
 422             let must = must_of_prefix ~where main s in
 423             match where with
 424             | `Conclusion -> at_least ~dbd ~concl_card:(Eq (m+1)) must
 425             | `Statement -> at_least ~dbd ~full_card:(Eq (m+1)) must
 426           in
 427           List.map (fun uri -> (m, uri)) res)
 428       prefixes)
 429
 430   (* critical value reached, fallback to "only" constraints *)
 431 let compute_with_only ~(dbd:Mysql.dbd) ?(where = `Conclusion) main
 432   prefixes constants
 433 =
 434   let max_prefix_length =
 435     match prefixes with
 436     | [] -> assert false
 437     | (max,_)::_ -> max in
 438   let maximal_prefixes =
 439     let rec filter res = function
 440         [] -> res
 441       | (n,s)::l when n = max_prefix_length -> filter ((n,s)::res) l
 442       | _::_-> res in
 443     filter [] prefixes in
 444   let greater_than =
 445     let all =
 446       union
 447         (List.map
 448           (fun (m,s) ->
 449             let must = must_of_prefix ~where main s in
 450             (let res =
 451               match where with
 452               | `Conclusion -> at_least ~dbd ~concl_card:(Gt (m+1)) must
 453               | `Statement -> at_least ~dbd ~full_card:(Gt (m+1)) must
 454             in
 455             (* we tag the uri with m+1, for sorting purposes *)
 456             List.map (fun uri -> (m+1, uri)) res))
 457           maximal_prefixes)
 458     in
 459     List.filter (function (_,uri) -> at_most ~dbd ~where constants uri) all in
 460     let equal_to = compute_exactly ~dbd where main prefixes in
 461     greater_than @ equal_to
 462
 463   (* real match query implementation *)
 464 let cmatch ~(dbd:Mysql.dbd) t =
 465   let (main, constants) = signature_of t in
 466   match main with
 467   | None -> []
 468   | Some (main, types) ->
 469       (* the type of eq is not counted in constants_no *)
 470       let types_no = List.length types in
 471       let constants_no = StringSet.cardinal constants + types_no in
 472       if (constants_no > critical_value) then
 473         let prefixes = prefixes just_factor t in
 474         (match prefixes with
 475         | Some main, all_concl ->
 476             let all_constants =
 477               List.fold_right StringSet.add types (StringSet.add main constants)
 478             in
 479             compute_with_only ~dbd main all_concl all_constants
 480          | _, _ -> [])
 481       else
 482         (* in this case we compute all prefixes, and we do not need
 483            to apply the only constraints *)
 484         let prefixes =
 485           if constants_no = types_no then
 486             Some main, [0, []; types_no, types]
 487           else
 488             prefixes constants_no t
 489         in
 490         (match prefixes with
 491            Some main, all_concl ->
 492              List.concat
 493                (List.map
 494                   (fun (m,s) ->
 495                     let must = must_of_prefix ~where:`Conclusion main s in
 496                     let res = at_least ~dbd ~concl_card:(Eq (m+1)) must in
 497                     List.map (fun uri -> (m, uri)) res)
 498                   all_concl)
 499          | _, _ -> [])
 500
 501 let power_upto upto consts =
 502   let l = StringSet.elements consts in
 503   List.sort (fun (n,_) (m,_) -> m - n)
 504   (List.fold_left
 505     (fun res a ->
 506        List.filter (function (n,l) -> n <= upto)
 507        res@(List.map (function (n,l) -> (n+1,a::l)) res))
 508      [(0,[])] l)
 509
 510 let power consts =
 511   let l = StringSet.elements consts in
 512   List.sort (fun (n,_) (m,_) -> m - n)
 513   (List.fold_left
 514     (fun res a -> res@(List.map (function (n,l) -> (n+1,a::l)) res))
 515      [(0,[])] l)
 516
 517 type where = [ `Conclusion | `Statement ]
 518
 519 let sigmatch ~(dbd:Mysql.dbd) ?(where = `Conclusion) (main, constants) =
 520   match main with
 521     None -> []
 522   | Some (main, types) ->
 523       let constants_no = StringSet.cardinal constants in
 524       if (constants_no > critical_value) then
 525         let subsets =
 526           let subsets = power_upto just_factor constants in
 527           let types_no = List.length types in
 528           List.map (function (n,l) -> (n+types_no,types@l)) subsets
 529         in
 530         let all_constants =
 531           List.fold_right StringSet.add types (StringSet.add main constants)
 532         in
 533         compute_with_only ~dbd ~where main subsets all_constants
 534       else
 535         let subsets =
 536           let subsets = power constants in
 537           let types_no = List.length types in
 538           (0,[]) :: List.map (function (n,l) -> (n+types_no,types@l)) subsets
 539         in
 540         compute_exactly ~dbd where main subsets
 541
 542   (* match query wrappers *)
 543 let cmatch' = cmatch
 544 let cmatch ~dbd term =
 545   List.map snd
 546     (List.sort
 547       (fun x y -> Pervasives.compare (fst y) (fst x))
 548       (cmatch' ~dbd term))
 549
 550 let constants_of = signature_concl
 551