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