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