helm/software/components/tactics/metadataQuery.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 (* $Id$ *)
  27
  28 open Printf
  29
  30 let nonvar uri = not (UriManager.uri_is_var uri)
  31
  32 module Constr = MetadataConstraints
  33
  34 exception Goal_is_not_an_equation
  35
  36 let debug = false
  37 let debug_print s = if debug then prerr_endline (Lazy.force s)
  38
  39 let ( ** ) x y = int_of_float ((float_of_int x) ** (float_of_int y))
  40
  41 let signature_of_hypothesis context metasenv =
  42   let set, _ =
  43     List.fold_right
  44       (fun hyp (set,current_ctx) ->
  45         match hyp with
  46         | None -> set, hyp::current_ctx
  47         | Some (_, Cic.Decl t) ->
  48             Constr.UriManagerSet.union set (Constr.constants_of t),
  49             hyp::current_ctx
  50         | Some (_, Cic.Def (t, _)) ->
  51             try
  52               let ty,_ =
  53                 CicTypeChecker.type_of_aux'
  54                   metasenv current_ctx t CicUniv.oblivion_ugraph
  55               in
  56               let sort,_ =
  57                 CicTypeChecker.type_of_aux'
  58                   metasenv current_ctx ty CicUniv.oblivion_ugraph
  59               in
  60               let set = Constr.UriManagerSet.union set(Constr.constants_of ty)in
  61               match sort with
  62               | Cic.Sort Cic.Prop -> set, hyp::current_ctx
  63               | _ -> Constr.UriManagerSet.union set (Constr.constants_of t),
  64                      hyp::current_ctx
  65             with
  66             | CicTypeChecker.TypeCheckerFailure _ -> set, hyp::current_ctx)
  67       context (Constr.UriManagerSet.empty,[])
  68   in
  69   set
  70 ;;
  71
  72 let intersect uris siguris =
  73   let set1 = List.fold_right Constr.UriManagerSet.add uris Constr.UriManagerSet.empty in
  74   let set2 =
  75     List.fold_right Constr.UriManagerSet.add siguris Constr.UriManagerSet.empty
  76   in
  77   let inter = Constr.UriManagerSet.inter set1 set2 in
  78   List.filter (fun s -> Constr.UriManagerSet.mem s inter) uris
  79
  80 (* Profiling code
  81 let at_most =
  82  let profiler = CicUtil.profile "at_most" in
  83  fun ~dbd ~where uri -> profiler.profile (Constr.at_most ~dbd ~where) uri
  84
  85 let sigmatch =
  86  let profiler = CicUtil.profile "sigmatch" in
  87  fun ~dbd ~facts ~where signature ->
  88   profiler.profile (MetadataConstraints.sigmatch ~dbd ~facts ~where) signature
  89 *)
  90 let at_most = Constr.at_most
  91 let sigmatch = MetadataConstraints.sigmatch
  92
  93 let filter_uris_forward ~dbd (main, constants) uris =
  94   let main_uris =
  95     match main with
  96     | None -> []
  97     | Some (main, types) -> main :: types
  98   in
  99   let full_signature =
 100     List.fold_right Constr.UriManagerSet.add main_uris constants
 101   in
 102   List.filter (at_most ~dbd ~where:`Statement full_signature) uris
 103
 104 let filter_uris_backward ~dbd ~facts signature uris =
 105   let siguris =
 106     List.map snd
 107       (sigmatch ~dbd ~facts ~where:`Statement signature)
 108   in
 109     intersect uris siguris
 110
 111 let compare_goal_list proof goal1 goal2 =
 112   let _,metasenv, _subst, _,_, _ = proof in
 113   let (_, ey1, ty1) = CicUtil.lookup_meta goal1 metasenv in
 114   let (_, ey2, ty2) =  CicUtil.lookup_meta goal2 metasenv in
 115   let ty_sort1,_ =
 116     CicTypeChecker.type_of_aux' metasenv ey1 ty1 CicUniv.oblivion_ugraph
 117   in
 118   let ty_sort2,_ =
 119     CicTypeChecker.type_of_aux' metasenv ey2 ty2 CicUniv.oblivion_ugraph
 120   in
 121   let prop1 =
 122     let b,_ =
 123       CicReduction.are_convertible
 124         ey1 (Cic.Sort Cic.Prop) ty_sort1 CicUniv.oblivion_ugraph
 125     in
 126       if b then 0
 127       else 1
 128   in
 129   let prop2 =
 130     let b,_ =
 131       CicReduction.are_convertible
 132         ey2 (Cic.Sort Cic.Prop) ty_sort2 CicUniv.oblivion_ugraph
 133     in
 134       if b then 0
 135       else 1
 136   in
 137   prop1 - prop2
 138
 139 (* experimental_hint is a version of hint for experimental
 140     purposes. It uses auto_tac_verbose instead of auto tac.
 141     Auto_tac verbose also returns a substitution - for the moment
 142     as a function from cic to cic, to be changed into an association
 143     list in the future -. This substitution is used to build a
 144     hash table of the inspected goals with their associated proofs.
 145     The cose is a cut and paste of the previous one: at the end
 146     of the experimentation we shall make a choice. *)
 147
 148 let close_with_types s metasenv context =
 149   Constr.UriManagerSet.fold
 150     (fun e bag ->
 151       let t = CicUtil.term_of_uri e in
 152       let ty, _ =
 153         CicTypeChecker.type_of_aux' metasenv context t CicUniv.oblivion_ugraph
 154       in
 155       Constr.UriManagerSet.union bag (Constr.constants_of ty))
 156     s s
 157
 158 let close_with_constructors s metasenv context =
 159   Constr.UriManagerSet.fold
 160     (fun e bag ->
 161       let t = CicUtil.term_of_uri e in
 162       match t with
 163           Cic.MutInd (uri,_,_)
 164         | Cic.MutConstruct (uri,_,_,_) ->
 165             (match fst (CicEnvironment.get_obj CicUniv.oblivion_ugraph uri) with
 166                  Cic.InductiveDefinition(tl,_,_,_) ->
 167                    snd
 168                      (List.fold_left
 169                         (fun (i,s) (_,_,_,cl) ->
 170                            let _,s =
 171                              List.fold_left
 172                                (fun (j,s) _ ->
 173                                   let curi = UriManager.uri_of_uriref uri i (Some j) in
 174 (*                                     prerr_endline ("adding " ^
 175  *                                     (UriManager.string_of_uri curi)); *)
 176                                     j+1,Constr.UriManagerSet.add curi s) (1,s) cl in
 177                              (i+1,s)) (0,bag) tl)
 178                | _ -> assert false)
 179         | _ -> bag)
 180     s s
 181
 182 (* Profiling code
 183 let apply_tac_verbose =
 184  let profiler = CicUtil.profile "apply_tac_verbose" in
 185   fun ~term status -> profiler.profile (PrimitiveTactics.apply_tac_verbose ~term) status
 186
 187 let sigmatch =
 188  let profiler = CicUtil.profile "sigmatch" in
 189  fun ~dbd ~facts ?(where=`Conclusion) signature -> profiler.profile (Constr.sigmatch ~dbd ~facts ~where) signature
 190
 191 let cmatch' =
 192  let profiler = CicUtil.profile "cmatch'" in
 193  fun ~dbd ~facts signature -> profiler.profile (Constr.cmatch' ~dbd ~facts) signature
 194 *)
 195 let apply_tac_verbose = PrimitiveTactics.apply_tac_verbose
 196 let cmatch' = Constr.cmatch'
 197
 198 (* used only by te old auto *)
 199 let signature_of_goal ~(dbd:HSql.dbd) ((proof, goal) as _status) =
 200  let (_, metasenv, _subst, _, _, _) = proof in
 201  let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
 202  let main, sig_constants = Constr.signature_of ty in
 203  let set = signature_of_hypothesis context metasenv in
 204  let set =
 205   match main with
 206      None -> set
 207    | Some (main,l) ->
 208       List.fold_right Constr.UriManagerSet.add (main::l) set in
 209  let set = Constr.UriManagerSet.union set sig_constants in
 210  let all_constants_closed = close_with_types set metasenv context in
 211  let uris =
 212   sigmatch ~dbd ~facts:false ~where:`Statement (None,all_constants_closed) in
 213  let uris = List.filter nonvar (List.map snd uris) in
 214  let uris = List.filter Hashtbl_equiv.not_a_duplicate uris in
 215   uris
 216
 217 let is_predicate u =
 218     let ty, _ =
 219       try CicTypeChecker.type_of_aux' [] []
 220         (CicUtil.term_of_uri u) CicUniv.oblivion_ugraph
 221       with CicTypeChecker.TypeCheckerFailure _ -> assert false
 222     in
 223     let rec check_last_pi = function
 224       | Cic.Prod (_,_,tgt) -> check_last_pi tgt
 225       | Cic.Sort Cic.Prop -> true
 226       | _ -> false
 227     in
 228     check_last_pi ty
 229 ;;
 230
 231 let only constants uri =
 232   prerr_endline (UriManager.string_of_uri uri);
 233   let t = CicUtil.term_of_uri uri in (* FIXME: write ty_of_term *)
 234   let ty,_ = CicTypeChecker.type_of_aux' [] [] t CicUniv.oblivion_ugraph in
 235   let consts = Constr.constants_of ty in
 236 (*
 237   prerr_endline ("XXX " ^ UriManager.string_of_uri uri);
 238   Constr.UriManagerSet.iter (fun u -> prerr_endline (" - " ^
 239  UriManager.string_of_uri u)) consts;
 240   Constr.UriManagerSet.iter (fun u -> prerr_endline (" + " ^
 241   UriManager.string_of_uri u)) constants;*)
 242   Constr.UriManagerSet.subset consts constants
 243 ;;
 244
 245 let rec types_of_equality = function
 246   | Cic.Appl [Cic.MutInd (uri, _, _); ty; _; _]
 247     when (LibraryObjects.is_eq_URI uri) ->
 248       let uri_set = Constr.constants_of ty in
 249       if Constr.UriManagerSet.equal uri_set Constr.UriManagerSet.empty then
 250         Constr.SetSet.empty
 251       else Constr.SetSet.singleton uri_set
 252   | Cic.Prod (_, s, t) ->
 253       Constr.SetSet.union (types_of_equality s) (types_of_equality t)
 254   | _ -> Constr.SetSet.empty
 255 ;;
 256
 257 let types_for_equality metasenv goal =
 258   let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
 259   let all = types_of_equality ty in
 260   let _, all =
 261     List.fold_left
 262       (fun (i,acc) _ ->
 263          let ty, _ =
 264            CicTypeChecker.type_of_aux'
 265              metasenv context (Cic.Rel i) CicUniv.oblivion_ugraph in
 266          let newty = types_of_equality ty in
 267            (i+1,Constr.SetSet.union newty acc))
 268       (1,all) context
 269   in all
 270 ;;
 271
 272 let signature_of metasenv goal =
 273   let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
 274   let ty_set = Constr.constants_of ty in
 275   let hyp_set = signature_of_hypothesis context metasenv in
 276   let set = Constr.UriManagerSet.union ty_set hyp_set in
 277     close_with_types
 278      (close_with_constructors (close_with_types set metasenv context)
 279         metasenv context)
 280     metasenv context
 281
 282
 283 let universe_of_goal ~(dbd:HSql.dbd) apply_only metasenv goal =
 284   let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
 285   let ty_set = Constr.constants_of ty in
 286   let hyp_set = signature_of_hypothesis context metasenv in
 287   let set = Constr.UriManagerSet.union ty_set hyp_set in
 288   let all_constants_closed = close_with_types set metasenv context in
 289   (* we split predicates from the rest *)
 290   let predicates, rest =
 291     Constr.UriManagerSet.partition is_predicate all_constants_closed
 292   in
 293   let uris =
 294     Constr.UriManagerSet.fold
 295       (fun u acc ->
 296          debug_print (lazy ("processing "^(UriManager.string_of_uri u)));
 297          let set_for_sigmatch =
 298            Constr.UriManagerSet.remove u all_constants_closed in
 299          if LibraryObjects.is_eq_URI (UriManager.strip_xpointer u) then
 300            (* equality has a special treatment *)
 301            (debug_print (lazy "special treatment");
 302            let tfe =
 303              Constr.SetSet.elements (types_for_equality metasenv goal)
 304            in
 305              List.fold_left
 306                (fun acc l ->
 307                   let tyl = Constr.UriManagerSet.elements l in
 308                   debug_print (lazy ("tyl: "^(String.concat "\n"
 309                         (List.map UriManager.string_of_uri tyl))));
 310                   let set_for_sigmatch =
 311                     Constr.UriManagerSet.diff set_for_sigmatch l in
 312                   let uris =
 313                     sigmatch ~dbd ~facts:false ~where:`Statement
 314                       (Some (u,tyl),set_for_sigmatch) in
 315                     acc @ uris)
 316                acc tfe)
 317          else
 318            (debug_print (lazy "normal treatment");
 319            let uris =
 320              sigmatch ~dbd ~facts:false ~where:`Statement
 321                (Some (u,[]),set_for_sigmatch)
 322            in
 323              acc @ uris))
 324       predicates []
 325   in
 326 (*
 327   let uris =
 328     sigmatch ~dbd ~facts:false ~where:`Statement (None,all_constants_closed)
 329   in
 330 *)
 331   let uris = List.filter nonvar (List.map snd uris) in
 332   let uris = List.filter Hashtbl_equiv.not_a_duplicate uris in
 333   if apply_only then
 334     List.filter (only all_constants_closed) uris
 335   else uris
 336 ;;
 337
 338 let filter_out_predicate set ctx menv =
 339   Constr.UriManagerSet.filter (fun u -> not (is_predicate u)) set
 340 ;;
 341
 342 let equations_for_goal ~(dbd:HSql.dbd) ?signature ((proof, goal) as _status) =
 343 (*
 344   let to_string set =
 345     "{\n" ^
 346       (String.concat "\n"
 347          (Constr.UriManagerSet.fold
 348             (fun u l -> ("  "^UriManager.string_of_uri u)::l) set []))
 349     ^ "\n}"
 350   in
 351 *)
 352  let (_, metasenv, _subst, _, _, _) = proof in
 353  let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
 354  let main, sig_constants =
 355    match signature with
 356    | None -> Constr.signature_of ty
 357    | Some s -> s
 358  in
 359 (*  Printf.printf "\nsig_constants: %s\n\n" (to_string sig_constants); *)
 360 (*  match main with *)
 361 (*      None -> raise Goal_is_not_an_equation *)
 362 (*    | Some (m,l) -> *)
 363  let l =
 364    let eq_URI =
 365     match LibraryObjects.eq_URI () with
 366        None -> None
 367      | Some s ->
 368         Some
 369          (UriManager.uri_of_string
 370           (UriManager.string_of_uri s ^ "#xpointer(1/1)"))
 371    in
 372    match eq_URI,main with
 373    | Some eq_URI, Some (m, l) when UriManager.eq m eq_URI -> m::l
 374    | _ -> []
 375  in
 376  (*Printf.printf "\nSome (m, l): %s, [%s]\n\n"
 377    (UriManager.string_of_uri (List.hd l))
 378    (String.concat "; " (List.map UriManager.string_of_uri (List.tl l)));
 379  *)
 380  (*        if m == UriManager.uri_of_string HelmLibraryObjects.Logic.eq_XURI then ( *)
 381  let set = signature_of_hypothesis context metasenv in
 382  (*          Printf.printf "\nsignature_of_hypothesis: %s\n\n" (to_string set); *)
 383  let set = Constr.UriManagerSet.union set sig_constants in
 384  let set = filter_out_predicate set context metasenv in
 385  let set = close_with_types set metasenv context in
 386  (*          Printf.printf "\ndopo close_with_types: %s\n\n" (to_string set); *)
 387  let set = close_with_constructors set metasenv context in
 388  (*          Printf.printf "\ndopo close_with_constructors: %s\n\n" (to_string set); *)
 389  let set_for_sigmatch = List.fold_right Constr.UriManagerSet.remove l set in
 390  let uris =
 391    sigmatch ~dbd ~facts:false ~where:`Statement (main,set_for_sigmatch) in
 392  let uris = List.filter nonvar (List.map snd uris) in
 393  let uris = List.filter Hashtbl_equiv.not_a_duplicate uris in
 394  let set = List.fold_right Constr.UriManagerSet.add l set in
 395  let uris = List.filter (only set) uris in
 396  uris
 397    (*        ) *)
 398    (*        else raise Goal_is_not_an_equation *)
 399
 400 let experimental_hint
 401   ~(dbd:HSql.dbd) ?(facts=false) ?signature ((proof, goal) as status) =
 402   let (_, metasenv, _subst, _, _, _) = proof in
 403   let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
 404   let (uris, (main, sig_constants)) =
 405     match signature with
 406     | Some signature ->
 407         (sigmatch ~dbd ~facts signature, signature)
 408     | None ->
 409         (cmatch' ~dbd ~facts ty, Constr.signature_of ty)
 410   in
 411   let uris = List.filter nonvar (List.map snd uris) in
 412   let uris = List.filter Hashtbl_equiv.not_a_duplicate uris in
 413   let types_constants =
 414     match main with
 415     | None -> Constr.UriManagerSet.empty
 416     | Some (main, types) ->
 417         List.fold_right Constr.UriManagerSet.add (main :: types)
 418           Constr.UriManagerSet.empty
 419   in
 420   let all_constants =
 421     let hyp_and_sug =
 422       Constr.UriManagerSet.union
 423         (signature_of_hypothesis context metasenv)
 424         sig_constants
 425     in
 426     let main =
 427       match main with
 428       | None -> Constr.UriManagerSet.empty
 429       | Some (main,_) ->
 430           let ty, _ =
 431             CicTypeChecker.type_of_aux'
 432               metasenv context (CicUtil.term_of_uri main)
 433               CicUniv.oblivion_ugraph
 434           in
 435           Constr.constants_of ty
 436     in
 437     Constr.UriManagerSet.union main hyp_and_sug
 438   in
 439 (* Constr.UriManagerSet.iter debug_print hyp_constants; *)
 440   let all_constants_closed = close_with_types all_constants metasenv context in
 441   let other_constants =
 442     Constr.UriManagerSet.diff all_constants_closed types_constants
 443   in
 444   debug_print (lazy "all_constants_closed");
 445   if debug then Constr.UriManagerSet.iter (fun s -> debug_print (lazy (UriManager.string_of_uri s))) all_constants_closed;
 446   debug_print (lazy "other_constants");
 447   if debug then Constr.UriManagerSet.iter (fun s -> debug_print (lazy (UriManager.string_of_uri s))) other_constants;
 448   let uris =
 449     let pow = 2 ** (Constr.UriManagerSet.cardinal other_constants) in
 450     if ((List.length uris < pow) or (pow <= 0))
 451     then begin
 452       debug_print (lazy "MetadataQuery: large sig, falling back to old method");
 453       filter_uris_forward ~dbd (main, other_constants) uris
 454     end else
 455       filter_uris_backward ~dbd ~facts (main, other_constants) uris
 456   in
 457   let rec aux = function
 458     | [] -> []
 459     | uri :: tl ->
 460         (let status' =
 461             try
 462               let (subst,(proof, goal_list)) =
 463                   (* debug_print (lazy ("STO APPLICANDO" ^ uri)); *)
 464                   apply_tac_verbose
 465                     ~term:(CicUtil.term_of_uri uri)
 466                   status
 467               in
 468               let goal_list =
 469                 List.stable_sort (compare_goal_list proof) goal_list
 470               in
 471               Some (uri, (subst,(proof, goal_list)))
 472             with ProofEngineTypes.Fail _ -> None
 473           in
 474           match status' with
 475           | None -> aux tl
 476           | Some status' -> status' :: aux tl)
 477   in
 478   List.stable_sort
 479     (fun (_,(_, (_, goals1))) (_,(_, (_, goals2))) ->
 480       Pervasives.compare (List.length goals1) (List.length goals2))
 481     (aux uris)
 482
 483 let new_experimental_hint
 484   ~(dbd:HSql.dbd) ?(facts=false) ?signature ~universe
 485   ((proof, goal) as status)
 486 =
 487   let (_, metasenv,  _subst, _, _, _) = proof in
 488   let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
 489   let (uris, (main, sig_constants)) =
 490     match signature with
 491     | Some signature ->
 492         (sigmatch ~dbd ~facts signature, signature)
 493     | None ->
 494         (cmatch' ~dbd ~facts ty, Constr.signature_of ty) in
 495   let universe =
 496    List.fold_left
 497     (fun res u -> Constr.UriManagerSet.add u res)
 498     Constr.UriManagerSet.empty universe in
 499   let uris =
 500    List.fold_left
 501     (fun res (_,u) -> Constr.UriManagerSet.add u res)
 502     Constr.UriManagerSet.empty uris in
 503   let uris = Constr.UriManagerSet.inter uris universe in
 504   let uris = Constr.UriManagerSet.elements uris in
 505   let rec aux = function
 506     | [] -> []
 507     | uri :: tl ->
 508         (let status' =
 509             try
 510               let (subst,(proof, goal_list)) =
 511                   (* debug_print (lazy ("STO APPLICANDO" ^ uri)); *)
 512                   apply_tac_verbose
 513                     ~term:(CicUtil.term_of_uri uri)
 514                   status
 515               in
 516               let goal_list =
 517                 List.stable_sort (compare_goal_list proof) goal_list
 518               in
 519               Some (uri, (subst,(proof, goal_list)))
 520             with ProofEngineTypes.Fail _ -> None
 521           in
 522           match status' with
 523           | None -> aux tl
 524           | Some status' -> status' :: aux tl)
 525   in
 526   List.stable_sort
 527     (fun (_,(_, (_, goals1))) (_,(_, (_, goals2))) ->
 528       Pervasives.compare (List.length goals1) (List.length goals2))
 529     (aux uris)
 530