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