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