components/tactics/auto.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 open AutoTypes;;
  27 open AutoCache;;
  28
  29 let debug_print s = () (* prerr_endline s;; *)
  30
  31 (* {{{ *********** local given_clause wrapper ***********)
  32
  33 let given_clause dbd ?tables maxm auto cache subst flags smart_flag status =
  34   let active,passive,bag,cache,maxmeta,goal_steps,saturation_steps,timeout =
  35     match tables with
  36     | None ->
  37         (* first time, do a huge saturation *)
  38         let bag, equalities, cache, maxmeta =
  39           Saturation.find_equalities dbd status smart_flag auto cache
  40         in
  41         let passive = Saturation.make_passive equalities in
  42         let active = Saturation.make_active [] in
  43         let goal_steps, saturation_steps, timeout =
  44           if flags.use_only_paramod then max_int,max_int,flags.timeout
  45           else 82, 82, infinity
  46         in
  47         let maxm = max maxm maxmeta in
  48         active,passive,bag,cache,maxm,goal_steps,saturation_steps,timeout
  49     | Some (active,passive,bag,oldcache) ->
  50         (* saturate a bit more if cache cahnged *)
  51         let bag, equalities, cache, maxm =
  52           if cache_size oldcache <> cache_size cache then
  53             Saturation.close_more
  54               bag active maxm status smart_flag auto cache
  55           else
  56             bag, [], cache, maxm
  57         in
  58         let minsteps = List.length equalities in
  59         let passive = Saturation.add_to_passive equalities passive in
  60         let goal_steps, saturation_steps, timeout =
  61           if flags.use_only_paramod then max_int,max_int,flags.timeout
  62           else max 50 minsteps, minsteps, infinity
  63         in
  64         active,passive,bag,cache,maxm,goal_steps,saturation_steps,timeout
  65   in
  66   let res,actives,passives,maxmeta =
  67     Saturation.given_clause bag maxmeta status active passive
  68       goal_steps saturation_steps timeout
  69   in
  70   res,actives,passives,bag,cache,maxmeta
  71 ;;
  72
  73 (* }}} ****************************************************************)
  74
  75 (* {{{ **************** applyS *******************)
  76
  77 let new_metasenv_and_unify_and_t
  78  dbd flags proof goal ?tables newmeta' metasenv' context term' ty termty
  79  goal_arity
  80 =
  81  let (consthead,newmetasenv,arguments,_) =
  82    ProofEngineHelpers.saturate_term newmeta' metasenv' context termty goal_arity in
  83  let term'' =
  84    match arguments with [] -> term' | _ -> Cic.Appl (term'::arguments)
  85  in
  86  let proof',oldmetasenv =
  87   let (puri,metasenv,pbo,pty) = proof in
  88    (puri,newmetasenv,pbo,pty),metasenv
  89  in
  90  let goal_for_paramod =
  91   match LibraryObjects.eq_URI () with
  92   | Some uri ->
  93       Cic.Appl [Cic.MutInd (uri,0,[]); Cic.Sort Cic.Prop; consthead; ty]
  94   | None -> raise (ProofEngineTypes.Fail (lazy "No equality defined"))
  95  in
  96  let newmeta = CicMkImplicit.new_meta newmetasenv (*subst*) [] in
  97  let metasenv_for_paramod = (newmeta,context,goal_for_paramod)::newmetasenv in
  98  let proof'' = let uri,_,p,ty = proof' in uri,metasenv_for_paramod,p,ty in
  99  let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
 100  let proof''',goals =
 101   ProofEngineTypes.apply_tactic
 102     (EqualityTactics.rewrite_tac ~direction:`RightToLeft
 103       ~pattern:(ProofEngineTypes.conclusion_pattern None)
 104         (Cic.Meta(newmeta,irl)))
 105    (proof'',goal)
 106  in
 107  let goal = match goals with [g] -> g | _ -> assert false in
 108  let subst, (proof'''', _), _ =
 109    PrimitiveTactics.apply_with_subst ~term:term'' ~subst:[] (proof''',goal)
 110  in
 111  match
 112    let cache = cache_empty in
 113    given_clause dbd ?tables 0 None cache [] flags true (proof'''',newmeta)
 114  with
 115  | None, active, passive, bag,_,_ ->
 116      raise (ProofEngineTypes.Fail (lazy ("FIXME: propaga le tabelle")))
 117  | Some (_,proof''''',_), active, passive,bag,_,_  ->
 118      subst,proof''''',
 119      ProofEngineHelpers.compare_metasenvs ~oldmetasenv
 120        ~newmetasenv:(let _,m,_,_ = proof''''' in m),  active, passive
 121 ;;
 122
 123 let rec count_prods context ty =
 124  match CicReduction.whd context ty with
 125     Cic.Prod (n,s,t) -> 1 + count_prods (Some (n,Cic.Decl s)::context) t
 126   | _ -> 0
 127
 128 let apply_smart ~dbd ~term ~subst ?tables flags (proof, goal) =
 129  let module T = CicTypeChecker in
 130  let module R = CicReduction in
 131  let module C = Cic in
 132   let (_,metasenv,_,_) = proof in
 133   let metano,context,ty = CicUtil.lookup_meta goal metasenv in
 134   let newmeta = CicMkImplicit.new_meta metasenv subst in
 135    let exp_named_subst_diff,newmeta',newmetasenvfragment,term' =
 136     match term with
 137        C.Var (uri,exp_named_subst) ->
 138         let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff =
 139          PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri
 140           exp_named_subst
 141         in
 142          exp_named_subst_diff,newmeta',newmetasenvfragment,
 143           C.Var (uri,exp_named_subst')
 144      | C.Const (uri,exp_named_subst) ->
 145         let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff =
 146          PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri
 147           exp_named_subst
 148         in
 149          exp_named_subst_diff,newmeta',newmetasenvfragment,
 150           C.Const (uri,exp_named_subst')
 151      | C.MutInd (uri,tyno,exp_named_subst) ->
 152         let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff =
 153          PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri
 154           exp_named_subst
 155         in
 156          exp_named_subst_diff,newmeta',newmetasenvfragment,
 157           C.MutInd (uri,tyno,exp_named_subst')
 158      | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
 159         let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff =
 160          PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri
 161           exp_named_subst
 162         in
 163          exp_named_subst_diff,newmeta',newmetasenvfragment,
 164           C.MutConstruct (uri,tyno,consno,exp_named_subst')
 165      | _ -> [],newmeta,[],term
 166    in
 167    let metasenv' = metasenv@newmetasenvfragment in
 168    let termty,_ =
 169      CicTypeChecker.type_of_aux' metasenv' context term' CicUniv.empty_ugraph
 170    in
 171    let termty = CicSubstitution.subst_vars exp_named_subst_diff termty in
 172    let goal_arity = count_prods context ty in
 173    let subst, proof, gl, active, passive =
 174     new_metasenv_and_unify_and_t dbd flags proof goal ?tables
 175      newmeta' metasenv' context term' ty termty goal_arity
 176    in
 177     subst, proof, gl, active, passive
 178 ;;
 179
 180 (* }}} **************** applyS **************)
 181
 182 (* {{{ ***************** AUTO ********************)
 183
 184 let mk_irl ctx = CicMkImplicit.identity_relocation_list_for_metavariable ctx;;
 185 let ugraph = CicUniv.empty_ugraph;;
 186 let typeof = CicTypeChecker.type_of_aux';;
 187 let ppterm ctx t =
 188   let names = List.map (function None -> None | Some (x,_) -> Some x) ctx in
 189   CicPp.pp t names
 190 ;;
 191 let is_in_prop context subst metasenv ty =
 192   let sort,u = typeof ~subst metasenv context ty CicUniv.empty_ugraph in
 193   fst (CicReduction.are_convertible context (Cic.Sort Cic.Prop) sort u)
 194 ;;
 195 let assert_proof_is_valid proof metasenv context goalty =
 196   let ty,u = typeof metasenv context proof CicUniv.empty_ugraph in
 197   let b,_ = CicReduction.are_convertible context ty goalty u in
 198   if not b then
 199     begin
 200       let names =
 201         List.map (function None -> None | Some (x,_) -> Some x) context
 202       in
 203       prerr_endline ("PROOF:" ^ CicPp.pp proof names);
 204       prerr_endline ("PROOFTY:" ^ CicPp.pp ty names);
 205       prerr_endline ("GOAL:" ^ CicPp.pp goalty names);
 206       prerr_endline ("METASENV:" ^ CicMetaSubst.ppmetasenv [] metasenv);
 207     end;
 208   assert b
 209 ;;
 210 let assert_subst_are_disjoint subst subst' =
 211   assert(List.for_all
 212     (fun (i,_) -> List.for_all (fun (j,_) -> i<>j) subst')
 213     subst)
 214 ;;
 215 let sort_new_elems =
 216   List.sort (fun (_,_,l1) (_,_,l2) -> List.length l1 - List.length l2)
 217 ;;
 218
 219 let split_goals_in_prop metasenv subst gl =
 220   List.partition
 221     (fun g ->
 222       let _,context,ty = CicUtil.lookup_meta g metasenv in
 223       try
 224         let sort,u = typeof ~subst metasenv context ty ugraph in
 225         fst (CicReduction.are_convertible context (Cic.Sort Cic.Prop) sort u)
 226       with
 227       | CicTypeChecker.AssertFailure s
 228       | CicTypeChecker.TypeCheckerFailure s ->
 229           debug_print (ppterm context (CicMetaSubst.apply_subst subst ty));
 230           debug_print (Lazy.force s);
 231           false)
 232     (* FIXME... they should type! *)
 233     gl
 234 ;;
 235
 236 let split_goals_with_metas metasenv subst gl =
 237   List.partition
 238     (fun g ->
 239       let _,context,ty = CicUtil.lookup_meta g metasenv in
 240       let ty = CicMetaSubst.apply_subst subst ty in
 241       CicUtil.is_meta_closed ty)
 242     gl
 243 ;;
 244
 245 let order_new_goals metasenv subst open_goals ppterm =
 246   let prop,rest = split_goals_in_prop metasenv subst open_goals in
 247   let open_prop,closed_prop = split_goals_with_metas metasenv subst prop in
 248   let open_goals =
 249     (List.map (fun x -> x,P) (closed_prop @ open_prop))
 250     @
 251     (List.map (fun x -> x,T) rest)
 252   in
 253   let tys =
 254     List.map
 255       (fun (i,_) ->
 256         let _,_,ty = CicUtil.lookup_meta i metasenv in i,ty) open_goals
 257   in
 258   debug_print ("   OPEN: "^
 259     String.concat " "
 260       (List.map (fun (i,t) -> string_of_int i ^":"^ppterm t) tys));
 261   open_goals
 262 ;;
 263
 264 let is_an_equational_goal = function
 265   | Cic.Appl [Cic.MutInd(u,_,_);_;_;_] when LibraryObjects.is_eq_URI u -> true
 266   | _ -> false
 267 ;;
 268
 269 let equational_case
 270   dbd tables maxm auto cache depth fake_proof goalno goalty subst context
 271     flags
 272 =
 273   let ppterm = ppterm context in
 274   prerr_endline ("PARAMOD SU: " ^ string_of_int goalno ^ " " ^ ppterm goalty );
 275 (*
 276   prerr_endline "<CACHE>";
 277   prerr_endline (cache_print context cache);
 278   prerr_endline "</CACHE>";
 279 *)
 280   match
 281     given_clause dbd ?tables maxm auto cache subst flags false (fake_proof,goalno)
 282   with
 283   | None, active,passive, bag, cache, maxmeta ->
 284       let tables = Some (active,passive,bag,cache) in
 285       None, tables, cache, maxmeta
 286   | Some(subst',(_,metasenv,proof,_),open_goals),active,passive,bag,cache,maxmeta ->
 287       let tables = Some (active,passive,bag,cache) in
 288       assert_subst_are_disjoint subst subst';
 289       let subst = subst@subst' in
 290       let open_goals = order_new_goals metasenv subst open_goals ppterm in
 291       let open_goals = List.map (fun (x,sort) -> x,depth-1,sort) open_goals in
 292       Some [metasenv,subst,open_goals], tables, cache, maxmeta
 293 ;;
 294
 295 let try_candidate
 296   goalty dbd tables maxm subst fake_proof goalno depth context cand
 297 =
 298   let ppterm = ppterm context in
 299   try
 300     let subst', ((_,metasenv,_,_), open_goals), maxmeta =
 301       PrimitiveTactics.apply_with_subst
 302         ~maxmeta:maxm ~term:cand ~subst (fake_proof,goalno)
 303     in
 304     debug_print ("   OK: " ^ ppterm cand);
 305     assert (maxmeta >= maxm);
 306     (*FIXME:sicuro che posso @?*)
 307     assert_subst_are_disjoint subst subst';
 308     let subst = subst@subst' in
 309     let open_goals = order_new_goals metasenv subst open_goals ppterm in
 310     let open_goals = List.map (fun (x,sort) -> x,depth-1,sort) open_goals in
 311     Some (metasenv,subst,open_goals), tables , maxmeta
 312   with ProofEngineTypes.Fail s ->
 313     (*debug_print("   KO: "^Lazy.force s);*)None,tables, maxm
 314 ;;
 315
 316 let applicative_case
 317   dbd tables maxm depth subst fake_proof goalno goalty metasenv context cache
 318 =
 319   let candidates = get_candidates cache goalty in
 320   let tables, elems, maxm =
 321     List.fold_left
 322       (fun (tables,elems,maxm) cand ->
 323         match
 324           try_candidate goalty
 325             dbd tables maxm subst fake_proof goalno depth context cand
 326         with
 327         | None, tables,maxm  -> tables,elems, maxm
 328         | Some x, tables, maxm -> tables,x::elems, maxm)
 329       (tables,[],maxm) candidates
 330   in
 331   let elems = sort_new_elems elems in
 332   elems, tables, cache, maxm
 333 ;;
 334
 335 (* Works if there is no dependency over proofs *)
 336 let is_a_green_cut goalty =
 337   CicUtil.is_meta_closed goalty
 338 ;;
 339 let prop = function (_,_,P) -> true | _ -> false;;
 340 let calculate_timeout flags =
 341     if flags.timeout = 0. then
 342       (prerr_endline "AUTO WITH NO TIMEOUT";{flags with timeout = infinity})
 343     else
 344       flags
 345 ;;
 346 let is_equational_case goalty flags =
 347   let ensure_equational t =
 348     if is_an_equational_goal t then true
 349     else false
 350     (*
 351       let msg="Not an equational goal.\nYou cant use the paramodulation flag"in
 352       raise (ProofEngineTypes.Fail (lazy msg))
 353     *)
 354   in
 355   (flags.use_paramod && is_an_equational_goal goalty) ||
 356   (flags.use_only_paramod && ensure_equational goalty)
 357 ;;
 358 let cache_add_success sort cache k v =
 359   if sort = P then cache_add_success cache k v else cache_remove_underinspection
 360   cache k
 361 ;;
 362
 363 let rec auto_main dbd tables maxm context flags elems cache =
 364   let callback_for_paramod maxm flags proof commonctx cache l =
 365     let flags = {flags with use_paramod = false;dont_cache_failures=true} in
 366     let _,metasenv,_,_ = proof in
 367     let oldmetasenv = metasenv in
 368     match
 369       auto_all_solutions
 370         dbd tables maxm cache commonctx metasenv l flags
 371     with
 372     | [],cache,maxm -> [],cache,maxm
 373     | solutions,cache,maxm ->
 374         let solutions =
 375           HExtlib.filter_map
 376             (fun (subst,newmetasenv) ->
 377               let opened =
 378                 ProofEngineHelpers.compare_metasenvs ~oldmetasenv ~newmetasenv
 379               in
 380               if opened = [] then Some subst else None)
 381             solutions
 382         in
 383          solutions,cache,maxm
 384   in
 385   let flags = calculate_timeout flags in
 386   let ppterm = ppterm context in
 387   let irl = mk_irl context in
 388   let rec aux tables maxm cache = function (* elems in OR *)
 389     | [] -> Fail "no more steps can be done", tables, cache, maxm
 390          (*COMPLETE FAILURE*)
 391     | (metasenv,subst,[])::tl ->
 392         Success (metasenv,subst,tl), tables, cache,maxm (* solution::cont *)
 393     | (metasenv,subst,goals)::tl when
 394       List.length (List.filter prop goals) > flags.maxwidth ->
 395         debug_print (" FAILURE(width): " ^ string_of_int (List.length goals));
 396         aux tables maxm cache tl (* FAILURE (width) *)
 397     | (metasenv,subst,((goalno,depth,sort) as elem)::gl)::tl ->
 398         if Unix.gettimeofday() > flags.timeout then
 399           Fail "timeout",tables,cache,maxm
 400         else
 401         try
 402           let _,cc,goalty = CicUtil.lookup_meta goalno metasenv in
 403           debug_print ("INSPECTING " ^ string_of_int goalno^ ":"^ppterm goalty);
 404           if sort = T && tl <> [] then (* FIXME!!!! *)
 405             (debug_print (" FAILURE(not in prop)");
 406             aux tables maxm cache tl (* FAILURE (not in prop) *))
 407           else
 408           match aux_single tables maxm cache metasenv subst elem goalty cc with
 409           | Fail s, tables, cache, maxm' ->
 410               assert(maxm' >= maxm);let maxm = maxm' in
 411               debug_print
 412                 (" FAIL "^s^": "^string_of_int goalno^":"^ppterm goalty);
 413               let cache =
 414                 if flags.dont_cache_failures then
 415                   cache_remove_underinspection cache goalty
 416                 else cache_add_failure cache goalty depth
 417               in
 418               aux tables maxm cache tl
 419           | Success (metasenv,subst,others), tables, cache, maxm' ->
 420               assert(maxm' >= maxm);let maxm = maxm' in
 421               (* others are alternatives in OR *)
 422               try
 423                 let goal = Cic.Meta(goalno,irl) in
 424                 let proof = CicMetaSubst.apply_subst subst goal in
 425                 debug_print ("DONE: " ^ ppterm goalty^" with: "^ppterm proof);
 426                 if is_a_green_cut goalty then
 427                   (assert_proof_is_valid proof metasenv context goalty;
 428                   let cache = cache_add_success sort cache goalty proof in
 429                   aux tables maxm cache ((metasenv,subst,gl)::tl))
 430                 else
 431                   (let goalty = CicMetaSubst.apply_subst subst goalty in
 432                   assert_proof_is_valid proof metasenv context goalty;
 433                   let cache =
 434                     if is_a_green_cut goalty then
 435                       cache_add_success sort cache goalty proof
 436                     else
 437                       cache
 438                   in
 439                   let others =
 440                     List.map
 441                       (fun (metasenv,subst,goals) -> (metasenv,subst,goals@gl))
 442                     others
 443                   in
 444                   aux tables maxm cache ((metasenv,subst,gl)::others@tl))
 445               with CicUtil.Meta_not_found i when i = goalno ->
 446                 assert false
 447         with CicUtil.Meta_not_found i when i = goalno ->
 448           (* goalno was closed by sideeffect *)
 449           debug_print ("Goal "^string_of_int goalno^" closed by sideeffect");
 450           aux tables maxm cache ((metasenv,subst,gl)::tl)
 451   and aux_single tables maxm cache metasenv subst (goalno, depth, _) goalty cc =
 452     let goalty = CicMetaSubst.apply_subst subst goalty in
 453 (*     else if not (is_in_prop context subst metasenv goalty) then Fail,cache *)
 454       (* FAILURE (euristic cut) *)
 455     match cache_examine cache goalty with
 456     | Failed_in d when d >= depth ->
 457         Fail ("depth " ^ string_of_int d ^ ">=" ^ string_of_int depth),
 458         tables,cache,maxm(*FAILURE(depth)*)
 459     | Succeded t ->
 460         assert(List.for_all (fun (i,_) -> i <> goalno) subst);
 461         let entry = goalno, (cc, t,goalty) in
 462         assert_subst_are_disjoint subst [entry];
 463         let subst = entry :: subst in
 464         let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
 465         debug_print ("  CACHE HIT!");
 466         Success (metasenv, subst, []), tables, cache, maxm
 467     | UnderInspection -> Fail "looping",tables,cache, maxm
 468     | Notfound
 469     | Failed_in _ when depth > 0 -> (* we have more depth now *)
 470         let cache = cache_add_underinspection cache goalty depth in
 471         let fake_proof = None,metasenv,Cic.Meta(goalno,irl),goalty in
 472         let elems, tables, cache, maxm =
 473           if is_equational_case goalty flags then
 474             match
 475               equational_case dbd tables maxm
 476                 (Some callback_for_paramod) cache
 477                 depth fake_proof goalno goalty subst context flags
 478             with
 479             | Some elems, tables, cache, maxm ->
 480                 elems, tables, cache, maxm
 481             | None, tables,cache,maxm ->
 482                 applicative_case dbd tables maxm depth subst fake_proof goalno
 483                   goalty metasenv context cache
 484           else
 485             applicative_case dbd tables maxm depth subst fake_proof goalno
 486               goalty metasenv context cache
 487         in
 488         aux tables maxm cache elems
 489     | _ -> Fail "??",tables,cache,maxm
 490   in
 491     aux tables maxm cache elems
 492
 493 and
 494   auto_all_solutions dbd tables maxm cache context metasenv gl flags
 495 =
 496   let goals = order_new_goals metasenv [] gl CicPp.ppterm in
 497   let goals = List.map (fun (x,s) -> x,flags.maxdepth,s) goals in
 498   let elems = [metasenv,[],goals] in
 499   let rec aux tables maxm solutions cache elems flags =
 500     match auto_main dbd tables maxm context flags elems cache with
 501     | Fail s,tables,cache,maxm ->prerr_endline s; solutions,cache,maxm
 502     | Success (metasenv,subst,others),tables,cache,maxm ->
 503         if Unix.gettimeofday () > flags.timeout then
 504           ((subst,metasenv)::solutions), cache, maxm
 505         else
 506           aux tables maxm ((subst,metasenv)::solutions) cache others flags
 507   in
 508   let rc = aux tables maxm [] cache elems flags in
 509   prerr_endline "fine auto all solutions";
 510   rc
 511 ;;
 512
 513 (* }}} ****************** AUTO ***************)
 514
 515 let auto_all_solutions dbd cache context metasenv gl flags =
 516   let solutions, cache, _ =
 517     auto_all_solutions dbd None 0 cache context metasenv gl flags
 518   in
 519   solutions, cache
 520 ;;
 521
 522 let auto dbd cache context metasenv gl flags =
 523   let initial_time = Unix.gettimeofday() in
 524   let goals = order_new_goals metasenv [] gl CicPp.ppterm in
 525   let goals = List.map (fun (x,s) -> x,flags.maxdepth,s) goals in
 526   let elems = [metasenv,[],goals] in
 527   match auto_main dbd None 0 context flags elems cache with
 528   | Success (metasenv,subst,_), tables,cache,_ ->
 529       prerr_endline("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time));
 530       Some (subst,metasenv), cache
 531   | Fail s,tables,cache,maxm -> None,cache
 532 ;;
 533
 534 let bool params name default =
 535     try
 536       let s = List.assoc name params in
 537       if s = "" || s = "1" || s = "true" || s = "yes" || s = "on" then true
 538       else if s = "0" || s = "false" || s = "no" || s= "off" then false
 539       else
 540         let msg = "Unrecognized value for parameter "^name^"\n" in
 541         let msg = msg^"Accepted values are 1,true,yes,on and 0,false,no,off" in
 542         raise (ProofEngineTypes.Fail (lazy msg))
 543     with Not_found -> default
 544 ;;
 545
 546 let string params name default =
 547     try List.assoc name params with
 548     | Not_found -> default
 549 ;;
 550
 551 let int params name default =
 552     try int_of_string (List.assoc name params) with
 553     | Not_found -> default
 554     | Failure _ ->
 555         raise (ProofEngineTypes.Fail (lazy (name ^ " must be an integer")))
 556 ;;
 557
 558 let flags_of_params params ?(for_applyS=false) () =
 559  let int = int params in
 560  let bool = bool params in
 561  let use_paramod = bool "use_paramod" true in
 562  let use_only_paramod =
 563   if for_applyS then true else bool "paramodulation" false in
 564  let depth = int "depth" ((AutoTypes.default_flags()).AutoTypes.maxdepth) in
 565  let width = int "width" ((AutoTypes.default_flags()).AutoTypes.maxwidth) in
 566  let timeout = int "timeout" 0 in
 567   { AutoTypes.maxdepth =
 568       if use_only_paramod then 2 else depth;
 569     AutoTypes.maxwidth = width;
 570     AutoTypes.timeout =
 571       if timeout = 0 then
 572        if for_applyS then Unix.gettimeofday () +. 30.0
 573        else
 574          infinity
 575       else
 576        Unix.gettimeofday() +. (float_of_int timeout);
 577     AutoTypes.use_paramod = use_paramod;
 578     AutoTypes.use_only_paramod = use_only_paramod;
 579     AutoTypes.dont_cache_failures = false
 580   }
 581
 582 let applyS_tac ~dbd ~term ~params =
 583  ProofEngineTypes.mk_tactic
 584   (fun status ->
 585     try
 586       let _, proof, gl,_,_ =
 587        apply_smart ~dbd ~term ~subst:[]
 588         (flags_of_params params ~for_applyS:true ()) status
 589       in
 590        proof, gl
 591     with
 592     | CicUnification.UnificationFailure msg
 593     | CicTypeChecker.TypeCheckerFailure msg ->
 594         raise (ProofEngineTypes.Fail msg))
 595
 596 let auto_tac ~(dbd:HMysql.dbd) ~params (proof, goal) =
 597   (* argument parsing *)
 598   let string = string params in
 599   let bool = bool params in
 600   let use_only_paramod = bool "paramodulation" false in
 601   (* hacks to debug paramod *)
 602   let superposition = bool "superposition" false in
 603   let target = string "target" "" in
 604   let table = string "table" "" in
 605   let subterms_only = bool "subterms_only" false in
 606   let demod_table = string "demod_table" "" in
 607   match superposition with
 608   | true ->
 609       (* this is the ugly hack to debug paramod *)
 610       Saturation.superposition_tac
 611         ~target ~table ~subterms_only ~demod_table (proof,goal)
 612   | false ->
 613       (* this is the real auto *)
 614       let _, metasenv, _, _ = proof in
 615       let _, context, goalty = CicUtil.lookup_meta goal metasenv in
 616       let cache =
 617         let cache =
 618           AutoCache.cache_add_context context metasenv AutoCache.cache_empty
 619         in
 620         if use_only_paramod then (* only paramod *)
 621           cache
 622         else
 623           AutoCache.cache_add_library dbd proof [goal] cache
 624       in
 625       let oldmetasenv = metasenv in
 626       let flags = flags_of_params params () in
 627       match auto dbd cache context metasenv [goal] flags with
 628       | None,cache ->
 629           raise (ProofEngineTypes.Fail (lazy "Auto gave up"))
 630       | Some (subst,metasenv),cache ->
 631           let proof,metasenv =
 632             ProofEngineHelpers.subst_meta_and_metasenv_in_proof
 633               proof goal (CicMetaSubst.apply_subst subst) metasenv
 634           in
 635           let opened =
 636             ProofEngineHelpers.compare_metasenvs ~oldmetasenv
 637               ~newmetasenv:metasenv
 638           in
 639           proof,opened
 640 ;;
 641
 642 let auto_tac ~dbd ~params = ProofEngineTypes.mk_tactic (auto_tac ~params ~dbd);;