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