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 = 5;;
  79 let width = 3;;
  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  ?num ~(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 search_theorems_in_context status =
 189   let (proof, goal) = status in
 190   let module C = Cic in
 191   let module R = CicReduction in
 192   let module S = CicSubstitution in
 193   let module PET = ProofEngineTypes in
 194   let module PT = PrimitiveTactics in
 195   let _,metasenv,_,_ = proof in
 196   let _,context,ty = CicUtil.lookup_meta goal metasenv in
 197   let rec find n = function
 198       [] -> []
 199     | hd::tl ->
 200         let res =
 201           try
 202             let (subst,(proof, goal_list)) =
 203               PT.apply_tac_verbose ~term:(C.Rel n) status  in
 204             (*
 205             let goal_list =
 206               List.stable_sort (compare_goal_list proof) goal_list in
 207             *)
 208             Some (subst,(proof, goal_list))
 209           with
 210             PET.Fail _ -> None in
 211         (match res with
 212           Some res -> res::(find (n+1) tl)
 213         | None -> find (n+1) tl)
 214   in
 215   try
 216     find 1 context
 217   with Failure s ->
 218     []
 219 ;;
 220
 221 (** splits a list of goals in three groups: closed propositional goals,
 222   open propositional goals and non proposotional goals *)
 223
 224 let split proof l =
 225   let _,metasenv,_,_ = proof in
 226   List.fold_left
 227     (fun (c,o,z,n) g ->
 228        try
 229          let (_, ey, ty) = CicUtil.lookup_meta g metasenv in
 230          let ty_sort,u =
 231            CicTypeChecker.type_of_aux' metasenv ey ty CicUniv.empty_ugraph in
 232          let b,_ =
 233            CicReduction.are_convertible ey (Cic.Sort Cic.Prop) ty_sort u in
 234            if b then
 235              (if CicUtil.is_meta_closed ty then
 236                 (g::c,o,z,n)
 237               else
 238                 (c,g::o,z,n))
 239            else (c,o,z,g::n)
 240        with
 241            CicUtil.Meta_not_found _ -> (c,o,g::z,n)
 242     )
 243     ([],[],[],[]) l
 244 ;;
 245
 246 let my_weight dbd sign proof g =
 247   let res =
 248     search_theorems_in_context (proof,g) in
 249    (* @
 250     (List.map snd (MetadataQuery.experimental_hint
 251       ~dbd ~facts:false ?signature:sign (proof,g))) in *)
 252   List.fold_left
 253     (fun n (_,(_,l)) -> n+(List.length l)+1)
 254     0 res
 255 ;;
 256
 257 let  add_weight dbd sign proof =
 258   List.map (function g -> (g,my_weight dbd sign proof g))
 259
 260 ;;
 261
 262
 263 (* let reorder_goals dbd sign proof goals =
 264   List.rev goals *)
 265
 266 (* let reorder_goals dbd sign proof goals =
 267   let (c,o,z,n) = split proof goals
 268   in c@o@n@z *)
 269
 270 let reorder_goals dbd sign proof goals =
 271   let (c,o,z,n) = split proof goals in
 272     match o with
 273         [] -> c@n@z
 274       | [g] ->c@[g]@n@z
 275       | l ->
 276           let l' = add_weight dbd sign proof l in
 277           c@(List.map fst (List.sort (fun (_,x) (_,y) -> x - y) l'))@n@z
 278
 279 let compare_goals proof goal1 goal2 =
 280   let _,metasenv,_,_ = proof in
 281   let (_, ey1, ty1) = CicUtil.lookup_meta goal1 metasenv in
 282   let (_, ey2, ty2) =  CicUtil.lookup_meta goal2 metasenv in
 283   let ty_sort1,_ = CicTypeChecker.type_of_aux' metasenv ey1 ty1
 284                      CicUniv.empty_ugraph in
 285   let ty_sort2,_ = CicTypeChecker.type_of_aux' metasenv ey2 ty2
 286                      CicUniv.empty_ugraph in
 287   let prop1 =
 288     let b,_ = CicReduction.are_convertible ey1 (Cic.Sort Cic.Prop) ty_sort1
 289                 CicUniv.empty_ugraph in
 290       if b then 0 else 1
 291   in
 292   let prop2 =
 293     let b,_ = CicReduction.are_convertible ey2 (Cic.Sort Cic.Prop) ty_sort2
 294                 CicUniv.empty_ugraph in
 295       if b then 0 else 1
 296   in
 297   prop1 - prop2
 298
 299
 300 let new_search_theorems f dbd proof goal depth sign =
 301   let choices = f (proof,goal)
 302   in
 303   List.map
 304     (function (subst,(proof, goallist)) ->
 305        (* let goallist = reorder_goals dbd sign proof goallist in *)
 306         let goallist = List.sort (compare_goals proof) goallist in
 307        (subst,(proof,(List.map (function g -> (g,depth)) goallist), sign)))
 308     choices
 309 ;;
 310
 311 exception NoOtherChoices;;
 312
 313 let is_in_metasenv goal metasenv =
 314   try
 315     let (_, ey ,ty) =
 316       CicUtil.lookup_meta goal metasenv in
 317       true
 318   with _ -> false
 319
 320 let rec auto_single dbd proof goal ey ty depth width sign already_seen_goals
 321   =
 322   if depth = 0 then [] else
 323   if List.mem ty already_seen_goals then [] else
 324   let already_seen_goals = ty::already_seen_goals in
 325   let facts = (depth = 1) in
 326   let _,metasenv,p,_ = proof in
 327     (* first of all we check if the goal has been already
 328        inspected *)
 329   assert (is_in_metasenv goal metasenv);
 330   let exitus =
 331     try Hashtbl.find inspected_goals ty
 332     with Not_found -> NotYetInspected in
 333   let is_meta_closed = CicUtil.is_meta_closed ty in
 334     begin
 335       match exitus with
 336           Yes (bo,_) ->
 337             (*
 338               prerr_endline "ALREADY PROVED!!!!!!!!!!!!!!!!!!!!!!!!!!!!";
 339               prerr_endline (CicPp.ppterm ty);
 340             *)
 341             let subst_in =
 342               (* if we just apply the subtitution, the type
 343                  is irrelevant: we may use Implicit, since it will
 344                  be dropped *)
 345               CicMetaSubst.apply_subst
 346                 [(goal,(ey, bo, Cic.Implicit None))] in
 347             let (proof,_) =
 348               ProofEngineHelpers.subst_meta_and_metasenv_in_proof
 349                 proof goal subst_in metasenv in
 350               [(subst_in,(proof,[],sign))]
 351         | No d when (d >= depth) ->
 352             (* prerr_endline "PRUNED!!!!!!!!!!!!!!!!!!!!!!!!!!!!"; *)
 353             [] (* the empty list means no choices, i.e. failure *)
 354         | No _
 355         | NotYetInspected ->
 356              (*
 357               prerr_endline ("CURRENT GOAL = " ^ (CicPp.ppterm ty));
 358               prerr_endline ("CURRENT PROOF = " ^ (CicPp.ppterm p));
 359               prerr_endline ("CURRENT HYP = " ^ (fst (print_context ey)));
 360              *)
 361             let sign, new_sign =
 362               if is_meta_closed then
 363                 None, Some (MetadataConstraints.signature_of ty)
 364               else sign,sign in (* maybe the union ? *)
 365             let local_choices =
 366               new_search_theorems
 367                 search_theorems_in_context dbd
 368                 proof goal (depth-1) new_sign in
 369             let global_choices = [] in
 370 (*
 371               new_search_theorems
 372                 (fun status ->
 373                    List.map snd
 374                    (MetadataQuery.experimental_hint
 375                       ~dbd ~facts:facts ?signature:sign status))
 376                 dbd proof goal (depth-1) new_sign in *)
 377             let all_choices =
 378               local_choices@global_choices in
 379             let sorted_choices =
 380               List.stable_sort
 381                 (fun (_, (_, goals1, _)) (_, (_, goals2, _)) ->
 382                    Pervasives.compare
 383                    (List.length goals1) (List.length goals2))
 384                 all_choices in
 385               (match (auto_new dbd width already_seen_goals sorted_choices)
 386                with
 387                    [] ->
 388                      (* no proof has been found; we update the
 389                         hastable *)
 390                      (* if is_meta_closed then *)
 391                        Hashtbl.add inspected_goals ty (No depth);
 392                      []
 393                  | (subst,(proof,[],sign))::tl1 ->
 394                      (* a proof for goal has been found:
 395                         in order to get the proof we apply subst to
 396                         Meta[goal] *)
 397                      if is_meta_closed  then
 398                        begin
 399                          let irl =
 400                            CicMkImplicit.identity_relocation_list_for_metavariable ey in
 401                          let meta_proof =
 402                            subst (Cic.Meta(goal,irl)) in
 403                            Hashtbl.add inspected_goals
 404                              ty (Yes (meta_proof,depth));
 405 (*
 406                            begin
 407                              let cty,_ =
 408                                CicTypeChecker.type_of_aux' metasenv ey meta_proof CicUniv.empty_ugraph
 409                              in
 410                                if not (cty = ty) then
 411                                  begin
 412                                    prerr_endline ("ty =  "^CicPp.ppterm ty);
 413                                    prerr_endline ("cty =  "^CicPp.ppterm cty);
 414                                    assert false
 415                                  end
 416                                    Hashtbl.add inspected_goals
 417                                    ty (Yes (meta_proof,depth));
 418                            end;
 419 *)
 420                        end;
 421                      (subst,(proof,[],sign))::tl1
 422                  | _ -> assert false)
 423     end
 424
 425 and auto_new dbd width already_seen_goals = function
 426     [] -> []
 427   | (subst,(proof, goals, sign))::tl ->
 428       let _,metasenv,_,_ = proof in
 429       let is_in_metasenv (goal, _) =
 430         try
 431           let (_, ey ,ty) =
 432             CicUtil.lookup_meta goal metasenv in
 433             true
 434         with _ -> false in
 435       let goals'= List.filter is_in_metasenv goals in
 436         auto_new_aux dbd width already_seen_goals
 437           ((subst,(proof, goals', sign))::tl)
 438
 439 and auto_new_aux dbd width already_seen_goals = function
 440   [] -> []
 441   | (subst,(proof, [], sign))::tl -> (subst,(proof, [], sign))::tl
 442   | (subst,(proof, (goal,0)::_, _))::tl ->
 443       auto_new dbd width already_seen_goals tl
 444   | (subst,(proof, goals, _))::tl when
 445       (List.length goals) > width+1 ->
 446       auto_new dbd width already_seen_goals tl
 447   | (subst,(proof, (goal,depth)::gtl, sign))::tl ->
 448       let maxdepthgoals,othergoals =
 449         let rec aux acc =
 450           function
 451               (g,d)::l when d=depth -> aux (g::acc) l
 452             |l -> (acc,l) in
 453           aux [goal] gtl in
 454       let _,metasenv,p,_ = proof in
 455       let len1 = List.length maxdepthgoals in
 456       let maxdepthgoals = reorder_goals dbd sign proof maxdepthgoals in
 457       let len2 = List.length maxdepthgoals in
 458         match maxdepthgoals with
 459           [] -> prerr_endline
 460             ("caso sospetto " ^ (string_of_int (List.length othergoals)) ^ " " ^ string_of_int depth);
 461             auto_new dbd
 462               width already_seen_goals((subst,(proof, othergoals, sign))::tl)
 463         | goal::tgs ->
 464             let  gtl = (List.map (fun x->(x,depth)) tgs)@othergoals in
 465               begin
 466       let meta_inf =
 467         try
 468           let (_, ey ,ty) =
 469             CicUtil.lookup_meta goal metasenv in
 470             Some (ey,ty)
 471         with _ -> None
 472       in
 473         match meta_inf with
 474           | Some (ey,ty) ->
 475             begin
 476             match (auto_single dbd proof goal ey ty depth
 477         (width - (List.length gtl) - (len1-len2)) sign already_seen_goals)
 478                 with
 479                     [] -> auto_new dbd width already_seen_goals tl
 480                   | (local_subst,(proof,[],sign))::tl1 ->
 481                       let new_subst f t = f (subst t) in
 482                       let is_meta_closed = CicUtil.is_meta_closed ty in
 483                       let all_choices =
 484                         if is_meta_closed then
 485                           (new_subst local_subst,(proof,gtl,sign))::tl
 486                         else
 487                           let tl2 =
 488                             (List.map
 489                                (function (f,(p,l,s)) -> (new_subst f,(p,l@gtl,s))) tl1)
 490                           in
 491                             (new_subst local_subst,(proof,gtl,sign))::tl2@tl in
 492                         auto_new dbd width already_seen_goals all_choices
 493                   | _ -> assert false
 494             end
 495           | None -> prerr_endline "caso none";
 496               auto_new
 497                 dbd width already_seen_goals ((subst,(proof, gtl, sign))::tl)
 498               end
 499 ;;
 500
 501
 502 let auto_tac_new  ~(dbd:Mysql.dbd) =
 503   let auto_tac dbd (proof,goal) =
 504   Hashtbl.clear inspected_goals;
 505   prerr_endline "Entro in Auto";
 506   let id t = t in
 507   match (auto_new dbd width [] [id,(proof, [(goal,depth)],None)]) with
 508       [] ->  prerr_endline("Auto failed");
 509         raise (ProofEngineTypes.Fail "No Applicable theorem")
 510     | (_,(proof,[],_))::_ ->
 511         prerr_endline "AUTO_TAC HA FINITO";
 512         let _,_,p,_ = proof in
 513         prerr_endline (CicPp.ppterm p);
 514         (proof,[])
 515     | _ -> assert false
 516   in
 517   ProofEngineTypes.mk_tactic (auto_tac dbd)
 518 ;;
 519
 520