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