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