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.empty_ugraph
  55               in
  56               let sort,_ =
  57                 CicTypeChecker.type_of_aux'
  58                   metasenv current_ctx ty CicUniv.empty_ugraph
  59               in
  60               match sort with
  61               | Cic.Sort Cic.Prop -> set, hyp::current_ctx
  62               | _ -> Constr.UriManagerSet.union set (Constr.constants_of t),
  63                      hyp::current_ctx
  64             with
  65             | CicTypeChecker.TypeCheckerFailure _ -> set, hyp::current_ctx)
  66       context (Constr.UriManagerSet.empty,[])
  67   in
  68   set
  69 ;;
  70
  71 let intersect uris siguris =
  72   let set1 = List.fold_right Constr.UriManagerSet.add uris Constr.UriManagerSet.empty in
  73   let set2 =
  74     List.fold_right Constr.UriManagerSet.add siguris Constr.UriManagerSet.empty
  75   in
  76   let inter = Constr.UriManagerSet.inter set1 set2 in
  77   List.filter (fun s -> Constr.UriManagerSet.mem s inter) uris
  78
  79 (* Profiling code
  80 let at_most =
  81  let profiler = CicUtil.profile "at_most" in
  82  fun ~dbd ~where uri -> profiler.profile (Constr.at_most ~dbd ~where) uri
  83
  84 let sigmatch =
  85  let profiler = CicUtil.profile "sigmatch" in
  86  fun ~dbd ~facts ~where signature ->
  87   profiler.profile (MetadataConstraints.sigmatch ~dbd ~facts ~where) signature
  88 *)
  89 let at_most = Constr.at_most
  90 let sigmatch = MetadataConstraints.sigmatch
  91
  92 let filter_uris_forward ~dbd (main, constants) uris =
  93   let main_uris =
  94     match main with
  95     | None -> []
  96     | Some (main, types) -> main :: types
  97   in
  98   let full_signature =
  99     List.fold_right Constr.UriManagerSet.add main_uris constants
 100   in
 101   List.filter (at_most ~dbd ~where:`Statement full_signature) uris
 102
 103 let filter_uris_backward ~dbd ~facts signature uris =
 104   let siguris =
 105     List.map snd
 106       (sigmatch ~dbd ~facts ~where:`Statement signature)
 107   in
 108     intersect uris siguris
 109
 110 let compare_goal_list proof goal1 goal2 =
 111   let _,metasenv,_,_ = proof in
 112   let (_, ey1, ty1) = CicUtil.lookup_meta goal1 metasenv in
 113   let (_, ey2, ty2) =  CicUtil.lookup_meta goal2 metasenv in
 114   let ty_sort1,_ =
 115     CicTypeChecker.type_of_aux' metasenv ey1 ty1 CicUniv.empty_ugraph
 116   in
 117   let ty_sort2,_ =
 118     CicTypeChecker.type_of_aux' metasenv ey2 ty2 CicUniv.empty_ugraph
 119   in
 120   let prop1 =
 121     let b,_ =
 122       CicReduction.are_convertible
 123         ey1 (Cic.Sort Cic.Prop) ty_sort1 CicUniv.empty_ugraph
 124     in
 125       if b then 0
 126       else 1
 127   in
 128   let prop2 =
 129     let b,_ =
 130       CicReduction.are_convertible
 131         ey2 (Cic.Sort Cic.Prop) ty_sort2 CicUniv.empty_ugraph
 132     in
 133       if b then 0
 134       else 1
 135   in
 136   prop1 - prop2
 137
 138 (* experimental_hint is a version of hint for experimental
 139     purposes. It uses auto_tac_verbose instead of auto tac.
 140     Auto_tac verbose also returns a substitution - for the moment
 141     as a function from cic to cic, to be changed into an association
 142     list in the future -. This substitution is used to build a
 143     hash table of the inspected goals with their associated proofs.
 144     The cose is a cut and paste of the previous one: at the end
 145     of the experimentation we shall make a choice. *)
 146
 147 let close_with_types s metasenv context =
 148   Constr.UriManagerSet.fold
 149     (fun e bag ->
 150       let t = CicUtil.term_of_uri e in
 151       let ty, _ =
 152         CicTypeChecker.type_of_aux' metasenv context t CicUniv.empty_ugraph
 153       in
 154       Constr.UriManagerSet.union bag (Constr.constants_of ty))
 155     s s
 156
 157 let close_with_constructors s metasenv context =
 158   Constr.UriManagerSet.fold
 159     (fun e bag ->
 160       let t = CicUtil.term_of_uri e in
 161       match t with
 162           Cic.MutInd (uri,_,_)
 163         | Cic.MutConstruct (uri,_,_,_) ->
 164             (match fst (CicEnvironment.get_obj CicUniv.empty_ugraph uri) with
 165                  Cic.InductiveDefinition(tl,_,_,_) ->
 166                    snd
 167                      (List.fold_left
 168                         (fun (i,s) (_,_,_,cl) ->
 169                            let _,s =
 170                              List.fold_left
 171                                (fun (j,s) _ ->
 172                                   let curi = UriManager.uri_of_uriref uri i (Some j) in
 173                                     j+1,Constr.UriManagerSet.add curi s) (1,s) cl in
 174                              (i+1,s)) (0,bag) tl)
 175                | _ -> assert false)
 176         | _ -> bag)
 177     s s
 178
 179 (* Profiling code
 180 let apply_tac_verbose =
 181  let profiler = CicUtil.profile "apply_tac_verbose" in
 182   fun ~term status -> profiler.profile (PrimitiveTactics.apply_tac_verbose ~term) status
 183
 184 let sigmatch =
 185  let profiler = CicUtil.profile "sigmatch" in
 186  fun ~dbd ~facts ?(where=`Conclusion) signature -> profiler.profile (Constr.sigmatch ~dbd ~facts ~where) signature
 187
 188 let cmatch' =
 189  let profiler = CicUtil.profile "cmatch'" in
 190  fun ~dbd ~facts signature -> profiler.profile (Constr.cmatch' ~dbd ~facts) signature
 191 *)
 192 let apply_tac_verbose = PrimitiveTactics.apply_tac_verbose
 193 let cmatch' = Constr.cmatch'
 194
 195 let signature_of_goal ~(dbd:HMysql.dbd) ((proof, goal) as _status) =
 196  let (_, metasenv, _, _) = proof in
 197  let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
 198  let main, sig_constants = Constr.signature_of ty in
 199  let set = signature_of_hypothesis context metasenv in
 200  let set =
 201   match main with
 202      None -> set
 203    | Some (main,l) ->
 204       List.fold_right Constr.UriManagerSet.add (main::l) set in
 205  let set = Constr.UriManagerSet.union set sig_constants in
 206  let all_constants_closed = close_with_types set metasenv context in
 207  let uris =
 208   sigmatch ~dbd ~facts:false ~where:`Statement (None,all_constants_closed) in
 209  let uris = List.filter nonvar (List.map snd uris) in
 210  let uris = List.filter Hashtbl_equiv.not_a_duplicate uris in
 211   uris
 212 ;;
 213
 214 let filter_predicate set ctx menv =
 215   let is_predicate t =
 216     let ty, _ =
 217       try CicTypeChecker.type_of_aux' [] []
 218         (CicUtil.term_of_uri t) CicUniv.empty_ugraph
 219       with CicTypeChecker.TypeCheckerFailure _ -> assert false
 220     in
 221     let rec check_last_pi = function
 222       | Cic.Prod (_,_,tgt) -> check_last_pi tgt
 223       | Cic.Sort Cic.Prop -> true
 224       | _ -> false
 225     in
 226     not (check_last_pi ty)
 227   in
 228   Constr.UriManagerSet.filter is_predicate set
 229 ;;
 230
 231 let equations_for_goal ~(dbd:HMysql.dbd) ?signature ((proof, goal) as _status) =
 232 (*   let to_string set =
 233     "{ " ^
 234       (String.concat ", "
 235          (Constr.UriManagerSet.fold
 236             (fun u l -> (UriManager.string_of_uri u)::l) set []))
 237     ^ " }"
 238   in *)
 239  let (_, metasenv, _, _) = proof in
 240  let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
 241  let main, sig_constants =
 242    match signature with
 243    | None -> Constr.signature_of ty
 244    | Some s -> s
 245  in
 246 (*  Printf.printf "\nsig_constants: %s\n\n" (to_string sig_constants); *)
 247 (*  match main with *)
 248 (*      None -> raise Goal_is_not_an_equation *)
 249 (*    | Some (m,l) -> *)
 250  let l =
 251    let eq_URI =
 252     match LibraryObjects.eq_URI () with
 253        None -> None
 254      | Some s ->
 255         Some
 256          (UriManager.uri_of_string
 257           (UriManager.string_of_uri s ^ "#xpointer(1/1)"))
 258    in
 259    match eq_URI,main with
 260    | Some eq_URI, Some (m, l) when UriManager.eq m eq_URI -> m::l
 261    | _ -> []
 262  in
 263  (*Printf.printf "\nSome (m, l): %s, [%s]\n\n"
 264    (UriManager.string_of_uri (List.hd l))
 265    (String.concat "; " (List.map UriManager.string_of_uri (List.tl l)));
 266  *)
 267  (*        if m == UriManager.uri_of_string HelmLibraryObjects.Logic.eq_XURI then ( *)
 268  let set = signature_of_hypothesis context metasenv in
 269  (*          Printf.printf "\nsignature_of_hypothesis: %s\n\n" (to_string set); *)
 270  let set = Constr.UriManagerSet.union set sig_constants in
 271  let set = filter_predicate set context metasenv in
 272  let set = close_with_types set metasenv context in
 273  (*          Printf.printf "\ndopo close_with_types: %s\n\n" (to_string set); *)
 274  let set = close_with_constructors set metasenv context in
 275  (*          Printf.printf "\ndopo close_with_constructors: %s\n\n" (to_string set); *)
 276  let set = List.fold_right Constr.UriManagerSet.remove l set in
 277  let uris =
 278    sigmatch ~dbd ~facts:false ~where:`Statement (main,set) in
 279  let uris = List.filter nonvar (List.map snd uris) in
 280  let uris = List.filter Hashtbl_equiv.not_a_duplicate uris in
 281  uris
 282    (*        ) *)
 283    (*        else raise Goal_is_not_an_equation *)
 284
 285 let experimental_hint
 286   ~(dbd:HMysql.dbd) ?(facts=false) ?signature ((proof, goal) as status) =
 287   let (_, metasenv, _, _) = proof in
 288   let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
 289   let (uris, (main, sig_constants)) =
 290     match signature with
 291     | Some signature ->
 292         (sigmatch ~dbd ~facts signature, signature)
 293     | None ->
 294         (cmatch' ~dbd ~facts ty, Constr.signature_of ty)
 295   in
 296   let uris = List.filter nonvar (List.map snd uris) in
 297   let uris = List.filter Hashtbl_equiv.not_a_duplicate uris in
 298   let types_constants =
 299     match main with
 300     | None -> Constr.UriManagerSet.empty
 301     | Some (main, types) ->
 302         List.fold_right Constr.UriManagerSet.add (main :: types)
 303           Constr.UriManagerSet.empty
 304   in
 305   let all_constants =
 306     let hyp_and_sug =
 307       Constr.UriManagerSet.union
 308         (signature_of_hypothesis context metasenv)
 309         sig_constants
 310     in
 311     let main =
 312       match main with
 313       | None -> Constr.UriManagerSet.empty
 314       | Some (main,_) ->
 315           let ty, _ =
 316             CicTypeChecker.type_of_aux'
 317               metasenv context (CicUtil.term_of_uri main) CicUniv.empty_ugraph
 318           in
 319           Constr.constants_of ty
 320     in
 321     Constr.UriManagerSet.union main hyp_and_sug
 322   in
 323 (* Constr.UriManagerSet.iter debug_print hyp_constants; *)
 324   let all_constants_closed = close_with_types all_constants metasenv context in
 325   let other_constants =
 326     Constr.UriManagerSet.diff all_constants_closed types_constants
 327   in
 328   debug_print (lazy "all_constants_closed");
 329   if debug then Constr.UriManagerSet.iter (fun s -> debug_print (lazy (UriManager.string_of_uri s))) all_constants_closed;
 330   debug_print (lazy "other_constants");
 331   if debug then Constr.UriManagerSet.iter (fun s -> debug_print (lazy (UriManager.string_of_uri s))) other_constants;
 332   let uris =
 333     let pow = 2 ** (Constr.UriManagerSet.cardinal other_constants) in
 334     if ((List.length uris < pow) or (pow <= 0))
 335     then begin
 336       debug_print (lazy "MetadataQuery: large sig, falling back to old method");
 337       filter_uris_forward ~dbd (main, other_constants) uris
 338     end else
 339       filter_uris_backward ~dbd ~facts (main, other_constants) uris
 340   in
 341   let rec aux = function
 342     | [] -> []
 343     | uri :: tl ->
 344         (let status' =
 345             try
 346               let (subst,(proof, goal_list)) =
 347                   (* debug_print (lazy ("STO APPLICANDO" ^ uri)); *)
 348                   apply_tac_verbose
 349                     ~term:(CicUtil.term_of_uri uri)
 350                   status
 351               in
 352               let goal_list =
 353                 List.stable_sort (compare_goal_list proof) goal_list
 354               in
 355               Some (uri, (subst,(proof, goal_list)))
 356             with ProofEngineTypes.Fail _ -> None
 357           in
 358           match status' with
 359           | None -> aux tl
 360           | Some status' -> status' :: aux tl)
 361   in
 362   List.stable_sort
 363     (fun (_,(_, (_, goals1))) (_,(_, (_, goals2))) ->
 364       Pervasives.compare (List.length goals1) (List.length goals2))
 365     (aux uris)
 366
 367 let new_experimental_hint
 368   ~(dbd:HMysql.dbd) ?(facts=false) ?signature ~universe
 369   ((proof, goal) as status)
 370 =
 371   let (_, metasenv, _, _) = proof in
 372   let (_, context, ty) = CicUtil.lookup_meta goal metasenv in
 373   let (uris, (main, sig_constants)) =
 374     match signature with
 375     | Some signature ->
 376         (sigmatch ~dbd ~facts signature, signature)
 377     | None ->
 378         (cmatch' ~dbd ~facts ty, Constr.signature_of ty) in
 379   let universe =
 380    List.fold_left
 381     (fun res u -> Constr.UriManagerSet.add u res)
 382     Constr.UriManagerSet.empty universe in
 383   let uris =
 384    List.fold_left
 385     (fun res (_,u) -> Constr.UriManagerSet.add u res)
 386     Constr.UriManagerSet.empty uris in
 387   let uris = Constr.UriManagerSet.inter uris universe in
 388   let uris = Constr.UriManagerSet.elements uris in
 389   let rec aux = function
 390     | [] -> []
 391     | uri :: tl ->
 392         (let status' =
 393             try
 394               let (subst,(proof, goal_list)) =
 395                   (* debug_print (lazy ("STO APPLICANDO" ^ uri)); *)
 396                   apply_tac_verbose
 397                     ~term:(CicUtil.term_of_uri uri)
 398                   status
 399               in
 400               let goal_list =
 401                 List.stable_sort (compare_goal_list proof) goal_list
 402               in
 403               Some (uri, (subst,(proof, goal_list)))
 404             with ProofEngineTypes.Fail _ -> None
 405           in
 406           match status' with
 407           | None -> aux tl
 408           | Some status' -> status' :: aux tl)
 409   in
 410   List.stable_sort
 411     (fun (_,(_, (_, goals1))) (_,(_, (_, goals2))) ->
 412       Pervasives.compare (List.length goals1) (List.length goals2))
 413     (aux uris)
 414