helm/ocaml/tactics/autoTactic.ml

   1 (* Copyright (C) 2002, 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://cs.unibo.it/helm/.
  24  *)
  25
  26  let debug_print = prerr_endline
  27
  28 (* let debug_print = fun _ -> () *)
  29
  30 let new_experimental_hint =
  31  let profile = CicUtil.profile "new_experimental_hint" in
  32  fun ~dbd ~facts ?signature ~universe status ->
  33   profile (MetadataQuery.new_experimental_hint ~dbd ~facts ?signature ~universe) status
  34
  35 let search_theorems_in_context status =
  36   let (proof, goal) = status in
  37   let module C = Cic in
  38   let module R = CicReduction in
  39   let module S = CicSubstitution in
  40   let module PET = ProofEngineTypes in
  41   let module PT = PrimitiveTactics in
  42   let _,metasenv,_,_ = proof in
  43   let _,context,ty = CicUtil.lookup_meta goal metasenv in
  44   let rec find n = function
  45       [] -> []
  46     | hd::tl ->
  47         let res =
  48           try
  49             Some (PET.apply_tactic
  50                     (PT.apply_tac ~term:(C.Rel n)) status )
  51           with
  52             PET.Fail _ -> None in
  53         (match res with
  54           Some res -> res::(find (n+1) tl)
  55         | None -> find (n+1) tl)
  56   in
  57   try
  58     find 1 context
  59   with Failure s ->
  60     []
  61 ;;
  62
  63 let depth = 5;;
  64 let width = 3;;
  65
  66 let new_search_theorems f proof goal depth gtl sign =
  67   let choices = f (proof,goal)
  68   in
  69   List.map
  70     (function (proof, goallist) ->
  71        (proof,(List.map (function g -> (g,depth)) goallist)@gtl, sign))
  72     choices
  73 ;;
  74
  75 exception NoOtherChoices;;
  76 let rec auto dbd = function
  77     [] -> []
  78   | (proof, [], sign)::tl -> (proof, [], sign)::tl
  79   | (proof, (goal,0)::_, _)::tl -> auto dbd tl
  80   | (proof, (((goal,depth)::gtl) as allg), sign)::tl ->
  81       (* first we check if the metavariable has not been already
  82          closed as a side effect by some other application *)
  83       let facts = (depth = 1) in
  84       let name,metasenv,p,statement = proof in
  85       let meta_inf =
  86         (try
  87            let (_, ey ,ty) = CicUtil.lookup_meta goal metasenv in
  88              Some (ey, ty)
  89          with _ -> None) in
  90       match meta_inf with
  91           Some (ey, ty) ->
  92             (* the goal is still there *)
  93             (*
  94             debug_print ("CURRENT GOAL = " ^ CicPp.ppterm ty);
  95             debug_print ("CURRENT PROOF = " ^ CicPp.ppterm p);
  96             debug_print ("CURRENT HYP = " ^ CicPp.ppcontext ey);
  97             *)
  98             (* if the goal contains metavariables we use the input
  99                signature for at_most constraints *)
 100             let is_meta_closed = CicUtil.is_meta_closed ty in
 101             let sign, new_sign =
 102               if is_meta_closed then
 103                 None, Some (MetadataConstraints.signature_of ty)
 104               else sign,sign in (* maybe the union ? *)
 105             let local_choices =
 106               new_search_theorems
 107                 search_theorems_in_context
 108                 proof goal (depth-1) [] new_sign in
 109             let global_choices =
 110               new_search_theorems
 111                 (fun status ->
 112                    List.map snd
 113                    (MetadataQuery.hint
 114                       ~dbd ~facts:facts ?signature:sign status))
 115                 proof goal (depth-1) [] new_sign in
 116             (* we proceed depth-first on the current goal. This is
 117                a MAJOR optimization, since in case of success, and
 118                if the goal is meta_closed, we may just drop the alternatives
 119                tl1, avoiding useless backtracking. *)
 120             let all_choices =
 121               local_choices@global_choices in
 122               (match (auto dbd all_choices)
 123                with
 124                    [] -> auto dbd tl
 125                  | (proof,[],_)::tl1 ->
 126                      let all_choices =
 127                        let gtl' = List.map fst gtl in
 128                          if (gtl = [] || is_meta_closed) then
 129                            (proof,gtl,sign)::tl
 130                          else
 131                            let tl2 =
 132                              (List.map
 133                                 (function (p,l,s) -> (p,l@gtl,s)) tl1)
 134                            in
 135                              (proof,gtl,sign)::tl2@tl in
 136                        auto dbd all_choices
 137                  | _ -> assert false)
 138         | None -> auto dbd ((proof,gtl,sign)::tl)
 139 ;;
 140
 141
 142 let auto_tac ?num dbd =
 143   let auto_tac dbh (proof,goal) =
 144   debug_print "Entro in Auto";
 145   match (auto dbd [(proof, [(goal,depth)],None)]) with
 146       [] ->  debug_print("Auto failed");
 147         raise (ProofEngineTypes.Fail "No Applicable theorem")
 148     | (proof,[],_)::_ ->
 149         debug_print "AUTO_TAC HA FINITO";
 150         (proof,[])
 151     | _ -> assert false
 152   in
 153   ProofEngineTypes.mk_tactic (auto_tac dbd)
 154 ;;
 155
 156
 157 (************************** EXPERIMENTAL VERSION ****************************)
 158
 159 (* In this versions of auto_tac we maintain an hash table of all inspected
 160    goals. We assume that the context is invariant for application.
 161    To this aim, it is essential to sall hint_verbose, that in turns calls
 162    apply_verbose. *)
 163
 164
 165
 166 type exitus =
 167     No of int
 168   | Yes of Cic.term * int
 169   | NotYetInspected
 170
 171 let inspected_goals = Hashtbl.create 503;;
 172
 173 let search_theorems_in_context status =
 174   let (proof, goal) = status in
 175   let module C = Cic in
 176   let module R = CicReduction in
 177   let module S = CicSubstitution in
 178   let module PET = ProofEngineTypes in
 179   let module PT = PrimitiveTactics in
 180   let _,metasenv,_,_ = proof in
 181   let _,context,ty = CicUtil.lookup_meta goal metasenv in
 182   let rec find n = function
 183       [] -> []
 184     | hd::tl ->
 185         let res =
 186           try
 187             let (subst,(proof, goal_list)) =
 188               PT.apply_tac_verbose ~term:(C.Rel n) status  in
 189             (*
 190             let goal_list =
 191               List.stable_sort (compare_goal_list proof) goal_list in
 192             *)
 193             Some (subst,(proof, goal_list))
 194           with
 195             PET.Fail _ -> None in
 196         (match res with
 197           Some res -> res::(find (n+1) tl)
 198         | None -> find (n+1) tl)
 199   in
 200   try
 201     find 1 context
 202   with Failure s ->
 203     []
 204 ;;
 205
 206
 207 let compare_goals proof goal1 goal2 =
 208   let _,metasenv,_,_ = proof in
 209   let (_, ey1, ty1) = CicUtil.lookup_meta goal1 metasenv in
 210   let (_, ey2, ty2) =  CicUtil.lookup_meta goal2 metasenv in
 211   let ty_sort1,_ = CicTypeChecker.type_of_aux' metasenv ey1 ty1
 212                      CicUniv.empty_ugraph in
 213   let ty_sort2,_ = CicTypeChecker.type_of_aux' metasenv ey2 ty2
 214                      CicUniv.empty_ugraph in
 215   let prop1 =
 216     let b,_ = CicReduction.are_convertible ey1 (Cic.Sort Cic.Prop) ty_sort1
 217                 CicUniv.empty_ugraph in
 218       if b then 0 else 1
 219   in
 220   let prop2 =
 221     let b,_ = CicReduction.are_convertible ey2 (Cic.Sort Cic.Prop) ty_sort2
 222                 CicUniv.empty_ugraph in
 223       if b then 0 else 1
 224   in
 225   prop1 - prop2
 226
 227
 228 let new_search_theorems f dbd proof goal depth sign =
 229   let choices = f (proof,goal)
 230   in
 231   List.map
 232     (function (subst,(proof, goallist)) ->
 233        (* let goallist = reorder_goals dbd sign proof goallist in *)
 234         let goallist = List.sort (compare_goals proof) goallist in
 235        (subst,(proof,(List.map (function g -> (g,depth)) goallist), sign)))
 236     choices
 237 ;;
 238
 239 exception NoOtherChoices;;
 240
 241 let is_in_metasenv goal metasenv =
 242   try
 243     let (_, ey ,ty) =
 244       CicUtil.lookup_meta goal metasenv in
 245       true
 246   with _ -> false
 247
 248 let rec auto_single dbd proof goal ey ty depth width sign already_seen_goals
 249  universe
 250   =
 251   if depth = 0 then [] else
 252   if List.mem ty already_seen_goals then [] else
 253   let already_seen_goals = ty::already_seen_goals in
 254   let facts = (depth = 1) in
 255   let _,metasenv,p,_ = proof in
 256     (* first of all we check if the goal has been already
 257        inspected *)
 258   assert (is_in_metasenv goal metasenv);
 259   let exitus =
 260     try Hashtbl.find inspected_goals ty
 261     with Not_found -> NotYetInspected in
 262   let is_meta_closed = CicUtil.is_meta_closed ty in
 263     begin
 264       match exitus with
 265           Yes (bo,_) ->
 266             (*
 267               debug_print "ALREADY PROVED!!!!!!!!!!!!!!!!!!!!!!!!!!!!";
 268               debug_print (CicPp.ppterm ty);
 269             *)
 270             let subst_in =
 271               (* if we just apply the subtitution, the type
 272                  is irrelevant: we may use Implicit, since it will
 273                  be dropped *)
 274               CicMetaSubst.apply_subst
 275                 [(goal,(ey, bo, Cic.Implicit None))] in
 276             let (proof,_) =
 277               ProofEngineHelpers.subst_meta_and_metasenv_in_proof
 278                 proof goal subst_in metasenv in
 279               [(subst_in,(proof,[],sign))]
 280         | No d when (d >= depth) ->
 281             (* debug_print "PRUNED!!!!!!!!!!!!!!!!!!!!!!!!!!!!"; *)
 282             [] (* the empty list means no choices, i.e. failure *)
 283         | No _
 284         | NotYetInspected ->
 285               debug_print ("CURRENT GOAL = " ^ CicPp.ppterm ty);
 286               debug_print ("CURRENT PROOF = " ^ CicPp.ppterm p);
 287               debug_print ("CURRENT HYP = " ^ CicPp.ppcontext ey);
 288             let sign, new_sign =
 289               if is_meta_closed then
 290                 None, Some (MetadataConstraints.signature_of ty)
 291               else sign,sign in (* maybe the union ? *)
 292             let local_choices =
 293               new_search_theorems
 294                 search_theorems_in_context dbd
 295                 proof goal (depth-1) new_sign in
 296             let global_choices =
 297               new_search_theorems
 298                 (fun status ->
 299                    List.map snd
 300                    (new_experimental_hint
 301                       ~dbd ~facts:facts ?signature:sign ~universe status))
 302                 dbd proof goal (depth-1) new_sign in
 303             let all_choices =
 304               local_choices@global_choices in
 305             let sorted_choices =
 306               List.stable_sort
 307                 (fun (_, (_, goals1, _)) (_, (_, goals2, _)) ->
 308                    Pervasives.compare
 309                    (List.length goals1) (List.length goals2))
 310                 all_choices in
 311               (match (auto_new dbd width already_seen_goals universe sorted_choices)
 312                with
 313                    [] ->
 314                      (* no proof has been found; we update the
 315                         hastable *)
 316                      (* if is_meta_closed then *)
 317                        Hashtbl.add inspected_goals ty (No depth);
 318                      []
 319                  | (subst,(proof,[],sign))::tl1 ->
 320                      (* a proof for goal has been found:
 321                         in order to get the proof we apply subst to
 322                         Meta[goal] *)
 323                      if is_meta_closed  then
 324                        begin
 325                          let irl =
 326                            CicMkImplicit.identity_relocation_list_for_metavariable ey in
 327                          let meta_proof =
 328                            subst (Cic.Meta(goal,irl)) in
 329                            Hashtbl.add inspected_goals
 330                              ty (Yes (meta_proof,depth));
 331 (*
 332                            begin
 333                              let cty,_ =
 334                                CicTypeChecker.type_of_aux' metasenv ey meta_proof CicUniv.empty_ugraph
 335                              in
 336                                if not (cty = ty) then
 337                                  begin
 338                                    debug_print ("ty =  "^CicPp.ppterm ty);
 339                                    debug_print ("cty =  "^CicPp.ppterm cty);
 340                                    assert false
 341                                  end
 342                                    Hashtbl.add inspected_goals
 343                                    ty (Yes (meta_proof,depth));
 344                            end;
 345 *)
 346                        end;
 347                      (subst,(proof,[],sign))::tl1
 348                  | _ -> assert false)
 349     end
 350
 351 and auto_new dbd width already_seen_goals universe = function
 352     [] -> []
 353   | (subst,(proof, goals, sign))::tl ->
 354       let _,metasenv,_,_ = proof in
 355       let is_in_metasenv (goal, _) =
 356         try
 357           let (_, ey ,ty) =
 358             CicUtil.lookup_meta goal metasenv in
 359             true
 360         with _ -> false in
 361       let goals'= List.filter is_in_metasenv goals in
 362         auto_new_aux dbd width already_seen_goals universe
 363           ((subst,(proof, goals', sign))::tl)
 364
 365 and auto_new_aux dbd width already_seen_goals universe = function
 366   [] -> []
 367   | (subst,(proof, [], sign))::tl -> (subst,(proof, [], sign))::tl
 368   | (subst,(proof, (goal,0)::_, _))::tl ->
 369       auto_new dbd width already_seen_goals universe tl
 370   | (subst,(proof, goals, _))::tl when
 371       (List.length goals) > width ->
 372       auto_new dbd width already_seen_goals universe tl
 373   | (subst,(proof, (goal,depth)::gtl, sign))::tl ->
 374       let _,metasenv,p,_ = proof in
 375       let (_, ey ,ty) = CicUtil.lookup_meta goal metasenv in
 376       match (auto_single dbd proof goal ey ty depth
 377         (width - (List.length gtl)) sign already_seen_goals) universe
 378       with
 379           [] -> auto_new dbd width already_seen_goals universe tl
 380         | (local_subst,(proof,[],sign))::tl1 ->
 381             let new_subst f t = f (subst t) in
 382             let is_meta_closed = CicUtil.is_meta_closed ty in
 383             let all_choices =
 384               if is_meta_closed then
 385                 (new_subst local_subst,(proof,gtl,sign))::tl
 386               else
 387                 let tl2 =
 388                   (List.map
 389                      (function (f,(p,l,s)) -> (new_subst f,(p,l@gtl,s))) tl1)
 390                 in
 391                   (new_subst local_subst,(proof,gtl,sign))::tl2@tl in
 392               auto_new dbd width already_seen_goals universe all_choices
 393         | _ -> assert false
 394  ;;
 395
 396 let default_depth = 5
 397 let default_width = 3
 398
 399 let auto_tac_new ?(depth=default_depth) ?(width=default_width) ~(dbd:Mysql.dbd)
 400   ()
 401 =
 402   let auto_tac dbd (proof,goal) =
 403   let universe = MetadataQuery.signature_of_goal ~dbd (proof,goal) in
 404   Hashtbl.clear inspected_goals;
 405   debug_print "Entro in Auto";
 406   let id t = t in
 407   match auto_new dbd width [] universe [id,(proof, [(goal,depth)],None)] with
 408       [] ->  debug_print("Auto failed");
 409         raise (ProofEngineTypes.Fail "No Applicable theorem")
 410     | (_,(proof,[],_))::_ ->
 411         debug_print "AUTO_TAC HA FINITO";
 412         let _,_,p,_ = proof in
 413         debug_print (CicPp.ppterm p);
 414         (proof,[])
 415     | _ -> assert false
 416   in
 417   ProofEngineTypes.mk_tactic (auto_tac dbd)
 418 ;;
 419
 420