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