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