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 = ignore (*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 (* In this versions of auto_tac we maintain an hash table of all inspected
  36    goals. We assume that the context is invariant for application.
  37    To this aim, it is essential to sall hint_verbose, that in turns calls
  38    apply_verbose. *)
  39
  40 type exitus =
  41     No of int
  42   | Yes of Cic.term * int
  43   | NotYetInspected
  44
  45 let inspected_goals = Hashtbl.create 503;;
  46
  47 let search_theorems_in_context status =
  48   let (proof, goal) = status in
  49   let module C = Cic in
  50   let module R = CicReduction in
  51   let module S = CicSubstitution in
  52   let module PET = ProofEngineTypes in
  53   let module PT = PrimitiveTactics in
  54   let _,metasenv,_,_ = proof in
  55   let _,context,ty = CicUtil.lookup_meta goal metasenv in
  56   let ctxlen = List.length context in
  57   let rec find n = function
  58     | [] -> []
  59     | hd::tl ->
  60         let res =
  61           (* we should check that the hypothesys has not been cleared *)
  62           if List.nth context (ctxlen - n) = None then
  63             None
  64           else
  65             try
  66               let (subst,(proof, goal_list)) =
  67                 PT.apply_tac_verbose ~term:(C.Rel n) status
  68               in
  69               (*
  70                  let goal_list =
  71                    List.stable_sort (compare_goal_list proof) goal_list in
  72               *)
  73               Some (subst,(proof, goal_list))
  74             with
  75               PET.Fail _ -> None
  76         in
  77         (match res with
  78         | Some res -> res::(find (n+1) tl)
  79         | None -> find (n+1) tl)
  80   in
  81   try
  82     find 1 context
  83   with Failure s -> []
  84 ;;
  85
  86
  87 let compare_goals proof goal1 goal2 =
  88   let _,metasenv,_,_ = proof in
  89   let (_, ey1, ty1) = CicUtil.lookup_meta goal1 metasenv in
  90   let (_, ey2, ty2) =  CicUtil.lookup_meta goal2 metasenv in
  91   let ty_sort1,_ = CicTypeChecker.type_of_aux' metasenv ey1 ty1
  92                      CicUniv.empty_ugraph in
  93   let ty_sort2,_ = CicTypeChecker.type_of_aux' metasenv ey2 ty2
  94                      CicUniv.empty_ugraph in
  95   let prop1 =
  96     let b,_ = CicReduction.are_convertible ey1 (Cic.Sort Cic.Prop) ty_sort1
  97                 CicUniv.empty_ugraph in
  98       if b then 0 else 1
  99   in
 100   let prop2 =
 101     let b,_ = CicReduction.are_convertible ey2 (Cic.Sort Cic.Prop) ty_sort2
 102                 CicUniv.empty_ugraph in
 103       if b then 0 else 1
 104   in
 105   prop1 - prop2
 106
 107
 108 let new_search_theorems f dbd proof goal depth sign =
 109   let choices = f (proof,goal)
 110   in
 111   List.map
 112     (function (subst,(proof, goallist)) ->
 113        (* let goallist = reorder_goals dbd sign proof goallist in *)
 114         let goallist = List.sort (compare_goals proof) goallist in
 115        (subst,(proof,(List.map (function g -> (g,depth)) goallist), sign)))
 116     choices
 117 ;;
 118
 119 exception NoOtherChoices;;
 120
 121 let is_in_metasenv goal metasenv =
 122   try
 123     let (_, ey ,ty) =
 124       CicUtil.lookup_meta goal metasenv in
 125       true
 126   with CicUtil.Meta_not_found _ -> false
 127
 128 let rec auto_single dbd proof goal ey ty depth width sign already_seen_goals
 129  universe
 130   =
 131   if depth = 0 then [] else
 132   if List.mem ty already_seen_goals then [] else
 133   let already_seen_goals = ty::already_seen_goals in
 134   let facts = (depth = 1) in
 135   let _,metasenv,p,_ = proof in
 136     (* first of all we check if the goal has been already
 137        inspected *)
 138   assert (is_in_metasenv goal metasenv);
 139   let exitus =
 140     try Hashtbl.find inspected_goals ty
 141     with Not_found -> NotYetInspected in
 142   let is_meta_closed = CicUtil.is_meta_closed ty in
 143     begin
 144       match exitus with
 145           Yes (bo,_) ->
 146             (*
 147               debug_print "ALREADY PROVED!!!!!!!!!!!!!!!!!!!!!!!!!!!!";
 148               debug_print (CicPp.ppterm ty);
 149             *)
 150             let subst_in =
 151               (* if we just apply the subtitution, the type
 152                  is irrelevant: we may use Implicit, since it will
 153                  be dropped *)
 154               CicMetaSubst.apply_subst
 155                 [(goal,(ey, bo, Cic.Implicit None))] in
 156             let (proof,_) =
 157               ProofEngineHelpers.subst_meta_and_metasenv_in_proof
 158                 proof goal subst_in metasenv in
 159               [(subst_in,(proof,[],sign))]
 160         | No d when (d >= depth) ->
 161             (* debug_print "PRUNED!!!!!!!!!!!!!!!!!!!!!!!!!!!!"; *)
 162             [] (* the empty list means no choices, i.e. failure *)
 163         | No _
 164         | NotYetInspected ->
 165               debug_print ("CURRENT GOAL = " ^ CicPp.ppterm ty);
 166               debug_print ("CURRENT PROOF = " ^ CicPp.ppterm p);
 167               debug_print ("CURRENT HYP = " ^ CicPp.ppcontext ey);
 168             let sign, new_sign =
 169               if is_meta_closed then
 170                 None, Some (MetadataConstraints.signature_of ty)
 171               else sign,sign in (* maybe the union ? *)
 172             let local_choices =
 173               new_search_theorems
 174                 search_theorems_in_context dbd
 175                 proof goal (depth-1) new_sign in
 176             let global_choices =
 177               new_search_theorems
 178                 (fun status ->
 179                    List.map snd
 180                    (new_experimental_hint
 181                       ~dbd ~facts:facts ?signature:sign ~universe status))
 182                 dbd proof goal (depth-1) new_sign in
 183             let all_choices =
 184               local_choices@global_choices in
 185             let sorted_choices =
 186               List.stable_sort
 187                 (fun (_, (_, goals1, _)) (_, (_, goals2, _)) ->
 188                    Pervasives.compare
 189                    (List.length goals1) (List.length goals2))
 190                 all_choices in
 191               (match (auto_new dbd width already_seen_goals universe sorted_choices)
 192                with
 193                    [] ->
 194                      (* no proof has been found; we update the
 195                         hastable *)
 196                      (* if is_meta_closed then *)
 197                        Hashtbl.add inspected_goals ty (No depth);
 198                      []
 199                  | (subst,(proof,[],sign))::tl1 ->
 200                      (* a proof for goal has been found:
 201                         in order to get the proof we apply subst to
 202                         Meta[goal] *)
 203                      if is_meta_closed  then
 204                        begin
 205                          let irl =
 206                            CicMkImplicit.identity_relocation_list_for_metavariable ey in
 207                          let meta_proof =
 208                            subst (Cic.Meta(goal,irl)) in
 209                            Hashtbl.add inspected_goals
 210                              ty (Yes (meta_proof,depth));
 211 (*
 212                            begin
 213                              let cty,_ =
 214                                CicTypeChecker.type_of_aux' metasenv ey meta_proof CicUniv.empty_ugraph
 215                              in
 216                                if not (cty = ty) then
 217                                  begin
 218                                    debug_print ("ty =  "^CicPp.ppterm ty);
 219                                    debug_print ("cty =  "^CicPp.ppterm cty);
 220                                    assert false
 221                                  end
 222                                    Hashtbl.add inspected_goals
 223                                    ty (Yes (meta_proof,depth));
 224                            end;
 225 *)
 226                        end;
 227                      (subst,(proof,[],sign))::tl1
 228                  | _ -> assert false)
 229     end
 230
 231 and auto_new dbd width already_seen_goals universe = function
 232   | [] -> []
 233   | (subst,(proof, goals, sign))::tl ->
 234       let _,metasenv,_,_ = proof in
 235       let is_in_metasenv (goal, _) =
 236         try
 237           let (_, ey ,ty) = CicUtil.lookup_meta goal metasenv in
 238           true
 239         with CicUtil.Meta_not_found _ -> false
 240       in
 241       let goals'= List.filter is_in_metasenv goals in
 242         auto_new_aux dbd
 243         width already_seen_goals universe ((subst,(proof, goals', sign))::tl)
 244
 245 and auto_new_aux dbd width already_seen_goals universe = function
 246   | [] -> []
 247   | (subst,(proof, [], sign))::tl -> (subst,(proof, [], sign))::tl
 248   | (subst,(proof, (goal,0)::_, _))::tl ->
 249       auto_new dbd width already_seen_goals universe tl
 250   | (subst,(proof, goals, _))::tl when
 251       (List.length goals) > width ->
 252       auto_new dbd width already_seen_goals universe tl
 253   | (subst,(proof, (goal,depth)::gtl, sign))::tl ->
 254       let _,metasenv,p,_ = proof in
 255       let (_, ey ,ty) = CicUtil.lookup_meta goal metasenv in
 256       match (auto_single dbd proof goal ey ty depth
 257         (width - (List.length gtl)) sign already_seen_goals) universe
 258       with
 259           [] -> auto_new dbd width already_seen_goals universe tl
 260         | (local_subst,(proof,[],sign))::tl1 ->
 261             let new_subst f t = f (subst t) in
 262             let is_meta_closed = CicUtil.is_meta_closed ty in
 263             let all_choices =
 264               if is_meta_closed then
 265                 (new_subst local_subst,(proof,gtl,sign))::tl
 266               else
 267                 let tl2 =
 268                   (List.map
 269                      (function (f,(p,l,s)) -> (new_subst f,(p,l@gtl,s))) tl1)
 270                 in
 271                   (new_subst local_subst,(proof,gtl,sign))::tl2@tl in
 272               auto_new dbd width already_seen_goals universe all_choices
 273         | _ -> assert false
 274  ;;
 275
 276 let default_depth = 5
 277 let default_width = 3
 278
 279 let auto_tac ?(depth=default_depth) ?(width=default_width) ~(dbd:Mysql.dbd)
 280   ()
 281 =
 282   let auto_tac dbd (proof,goal) =
 283   let universe = MetadataQuery.signature_of_goal ~dbd (proof,goal) in
 284   Hashtbl.clear inspected_goals;
 285   debug_print "Entro in Auto";
 286   let id t = t in
 287   match auto_new dbd width [] universe [id,(proof, [(goal,depth)],None)] with
 288       [] ->  debug_print("Auto failed");
 289         raise (ProofEngineTypes.Fail "No Applicable theorem")
 290     | (_,(proof,[],_))::_ ->
 291         debug_print "AUTO_TAC HA FINITO";
 292         let _,_,p,_ = proof in
 293         debug_print (CicPp.ppterm p);
 294         (proof,[])
 295     | _ -> assert false
 296   in
 297   ProofEngineTypes.mk_tactic (auto_tac dbd)
 298 ;;
 299
 300