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 ?auto smart_flag 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.saturate_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 80 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 proof goal ?tables newmeta' metasenv' context term' ty termty goal_arity
  79 =
  80  let (consthead,newmetasenv,arguments,_) =
  81    ProofEngineHelpers.saturate_term newmeta' metasenv' context termty goal_arity in
  82  let term'' =
  83    match arguments with [] -> term' | _ -> Cic.Appl (term'::arguments)
  84  in
  85  let proof',oldmetasenv =
  86   let (puri,metasenv,pbo,pty) = proof in
  87    (puri,newmetasenv,pbo,pty),metasenv
  88  in
  89  let goal_for_paramod =
  90   match LibraryObjects.eq_URI () with
  91   | Some uri ->
  92       Cic.Appl [Cic.MutInd (uri,0,[]); Cic.Sort Cic.Prop; consthead; ty]
  93   | None -> raise (ProofEngineTypes.Fail (lazy "No equality defined"))
  94  in
  95  let newmeta = CicMkImplicit.new_meta newmetasenv (*subst*) [] in
  96  let metasenv_for_paramod = (newmeta,context,goal_for_paramod)::newmetasenv in
  97  let proof'' = let uri,_,p,ty = proof' in uri,metasenv_for_paramod,p,ty in
  98  let irl = CicMkImplicit.identity_relocation_list_for_metavariable context in
  99  let proof''',goals =
 100   ProofEngineTypes.apply_tactic
 101     (EqualityTactics.rewrite_tac ~direction:`RightToLeft
 102       ~pattern:(ProofEngineTypes.conclusion_pattern None)
 103         (Cic.Meta(newmeta,irl)))
 104    (proof'',goal)
 105  in
 106  let goal = match goals with [g] -> g | _ -> assert false in
 107  let subst, (proof'''', _), _ =
 108    PrimitiveTactics.apply_with_subst ~term:term'' ~subst:[] (proof''',goal)
 109  in
 110  match
 111    let cache, flags = cache_empty, default_flags() in
 112    let flags =
 113      {flags with use_only_paramod=true;timeout=Unix.gettimeofday() +. 30.0}
 114    in
 115    given_clause dbd ?tables 0 cache [] flags true (proof'''',newmeta)
 116  with
 117  | None, active, passive, bag,_,_ ->
 118      raise (ProofEngineTypes.Fail (lazy ("FIXME: propaga le tabelle")))
 119  | Some (_,proof''''',_), active, passive,bag,_,_  ->
 120      subst,proof''''',
 121      ProofEngineHelpers.compare_metasenvs ~oldmetasenv
 122        ~newmetasenv:(let _,m,_,_ = proof''''' in m),  active, passive
 123 ;;
 124
 125 let rec count_prods context ty =
 126  match CicReduction.whd context ty with
 127     Cic.Prod (n,s,t) -> 1 + count_prods (Some (n,Cic.Decl s)::context) t
 128   | _ -> 0
 129
 130 let apply_smart ~dbd ~term ~subst ?tables (proof, goal) =
 131  let module T = CicTypeChecker in
 132  let module R = CicReduction in
 133  let module C = Cic in
 134   let (_,metasenv,_,_) = proof in
 135   let metano,context,ty = CicUtil.lookup_meta goal metasenv in
 136   let newmeta = CicMkImplicit.new_meta metasenv subst in
 137    let exp_named_subst_diff,newmeta',newmetasenvfragment,term' =
 138     match term with
 139        C.Var (uri,exp_named_subst) ->
 140         let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff =
 141          PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri
 142           exp_named_subst
 143         in
 144          exp_named_subst_diff,newmeta',newmetasenvfragment,
 145           C.Var (uri,exp_named_subst')
 146      | C.Const (uri,exp_named_subst) ->
 147         let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff =
 148          PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri
 149           exp_named_subst
 150         in
 151          exp_named_subst_diff,newmeta',newmetasenvfragment,
 152           C.Const (uri,exp_named_subst')
 153      | C.MutInd (uri,tyno,exp_named_subst) ->
 154         let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff =
 155          PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri
 156           exp_named_subst
 157         in
 158          exp_named_subst_diff,newmeta',newmetasenvfragment,
 159           C.MutInd (uri,tyno,exp_named_subst')
 160      | C.MutConstruct (uri,tyno,consno,exp_named_subst) ->
 161         let newmeta',newmetasenvfragment,exp_named_subst',exp_named_subst_diff =
 162          PrimitiveTactics.generalize_exp_named_subst_with_fresh_metas context newmeta uri
 163           exp_named_subst
 164         in
 165          exp_named_subst_diff,newmeta',newmetasenvfragment,
 166           C.MutConstruct (uri,tyno,consno,exp_named_subst')
 167      | _ -> [],newmeta,[],term
 168    in
 169    let metasenv' = metasenv@newmetasenvfragment in
 170    let termty,_ =
 171      CicTypeChecker.type_of_aux' metasenv' context term' CicUniv.empty_ugraph
 172    in
 173    let termty = CicSubstitution.subst_vars exp_named_subst_diff termty in
 174    let goal_arity = count_prods context ty in
 175    let subst, proof, gl, active, passive =
 176     new_metasenv_and_unify_and_t dbd proof goal ?tables
 177      newmeta' metasenv' context term' ty termty goal_arity
 178    in
 179     subst, proof, gl, active, passive
 180 ;;
 181
 182 (* }}} **************** applyS **************)
 183
 184 (* {{{ ***************** AUTO ********************)
 185
 186 let mk_irl ctx = CicMkImplicit.identity_relocation_list_for_metavariable ctx;;
 187 let ugraph = CicUniv.empty_ugraph;;
 188 let typeof = CicTypeChecker.type_of_aux';;
 189 let ppterm ctx t =
 190   let names = List.map (function None -> None | Some (x,_) -> Some x) ctx in
 191   CicPp.pp t names
 192 ;;
 193 let is_in_prop context subst metasenv ty =
 194   let sort,u = typeof ~subst metasenv context ty CicUniv.empty_ugraph in
 195   fst (CicReduction.are_convertible context (Cic.Sort Cic.Prop) sort u)
 196 ;;
 197 let assert_proof_is_valid proof metasenv context goalty =
 198   let ty,u = typeof metasenv context proof CicUniv.empty_ugraph in
 199   let b,_ = CicReduction.are_convertible context ty goalty u in
 200   if not b then
 201     begin
 202       let names =
 203         List.map (function None -> None | Some (x,_) -> Some x) context
 204       in
 205       prerr_endline ("PROOF:" ^ CicPp.pp proof names);
 206       prerr_endline ("PROOFTY:" ^ CicPp.pp ty names);
 207       prerr_endline ("GOAL:" ^ CicPp.pp goalty names);
 208       prerr_endline ("METASENV:" ^ CicMetaSubst.ppmetasenv [] metasenv);
 209     end;
 210   assert b
 211 ;;
 212 let assert_subst_are_disjoint subst subst' =
 213   assert(List.for_all
 214     (fun (i,_) -> List.for_all (fun (j,_) -> i<>j) subst')
 215     subst)
 216 ;;
 217 let sort_new_elems =
 218   List.sort (fun (_,_,l1) (_,_,l2) -> List.length l1 - List.length l2)
 219 ;;
 220
 221 let split_goals_in_prop metasenv subst gl =
 222   List.partition
 223     (fun g ->
 224       let _,context,ty = CicUtil.lookup_meta g metasenv in
 225       try
 226         let sort,u = typeof ~subst metasenv context ty ugraph in
 227         fst (CicReduction.are_convertible context (Cic.Sort Cic.Prop) sort u)
 228       with
 229       | CicTypeChecker.AssertFailure s
 230       | CicTypeChecker.TypeCheckerFailure s ->
 231           debug_print (ppterm context (CicMetaSubst.apply_subst subst ty));
 232           debug_print (Lazy.force s);
 233           false)
 234     (* FIXME... they should type! *)
 235     gl
 236 ;;
 237
 238 let split_goals_with_metas metasenv subst gl =
 239   List.partition
 240     (fun g ->
 241       let _,context,ty = CicUtil.lookup_meta g metasenv in
 242       let ty = CicMetaSubst.apply_subst subst ty in
 243       CicUtil.is_meta_closed ty)
 244     gl
 245 ;;
 246
 247 let order_new_goals metasenv subst open_goals ppterm =
 248   let prop,rest = split_goals_in_prop metasenv subst open_goals in
 249   let open_prop,closed_prop = split_goals_with_metas metasenv subst prop in
 250   let open_goals =
 251     (List.map (fun x -> x,P) (closed_prop @ open_prop))
 252     @
 253     (List.map (fun x -> x,T) rest)
 254   in
 255   let tys =
 256     List.map
 257       (fun (i,_) ->
 258         let _,_,ty = CicUtil.lookup_meta i metasenv in i,ty) open_goals
 259   in
 260   debug_print ("   OPEN: "^
 261     String.concat " "
 262       (List.map (fun (i,t) -> string_of_int i ^":"^ppterm t) tys));
 263   open_goals
 264 ;;
 265
 266 let is_an_equational_goal = function
 267   | Cic.Appl [Cic.MutInd(u,_,_);_;_;_] when LibraryObjects.is_eq_URI u -> true
 268   | _ -> false
 269 ;;
 270
 271 let equational_case
 272   dbd tables maxm ?auto cache depth fake_proof goalno goalty subst context
 273     flags
 274 =
 275   let ppterm = ppterm context in
 276   prerr_endline ("PARAMOD SU: " ^ string_of_int goalno ^ " " ^ ppterm goalty );
 277   prerr_endline "<CACHE>";
 278   prerr_endline (cache_print context cache);
 279   prerr_endline "</CACHE>";
 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
 360 ;;
 361
 362 let rec auto_main dbd tables maxm context flags elems cache =
 363   let callback_for_paramod maxm flags proof commonctx cache l =
 364     let flags = {flags with use_paramod = false;dont_cache_failures=true} in
 365     let _,metasenv,_,_ = proof in
 366     let oldmetasenv = metasenv in
 367     match
 368       auto_all_solutions
 369         dbd tables maxm cache commonctx metasenv l flags
 370     with
 371     | [],cache,maxm -> [],cache,maxm
 372     | solutions,cache,maxm ->
 373         let solutions =
 374           HExtlib.filter_map
 375             (fun (subst,newmetasenv) ->
 376               let opened =
 377                 ProofEngineHelpers.compare_metasenvs ~oldmetasenv ~newmetasenv
 378               in
 379               if opened = [] then Some subst else None)
 380             solutions
 381         in
 382          solutions,cache,maxm
 383   in
 384   let flags = calculate_timeout flags in
 385   let ppterm = ppterm context in
 386   let irl = mk_irl context in
 387   let rec aux tables maxm cache = function (* elems in OR *)
 388     | [] -> Fail "no more steps can be done", tables, cache, maxm
 389          (*COMPLETE FAILURE*)
 390     | (metasenv,subst,[])::tl ->
 391         Success (metasenv,subst,tl), tables, cache,maxm (* solution::cont *)
 392     | (metasenv,subst,goals)::tl when
 393       List.length (List.filter prop goals) > flags.maxwidth ->
 394         debug_print (" FAILURE(width): " ^ string_of_int (List.length goals));
 395         aux tables maxm cache tl (* FAILURE (width) *)
 396     | (metasenv,subst,((goalno,depth,sort) as elem)::gl)::tl ->
 397         if Unix.gettimeofday() > flags.timeout then
 398           Fail "timeout",tables,cache,maxm
 399         else
 400         try
 401           let _,cc,goalty = CicUtil.lookup_meta goalno metasenv in
 402           debug_print ("INSPECTING " ^ string_of_int goalno^ ":"^ppterm goalty);
 403           if sort = T && tl <> [] then (* FIXME!!!! *)
 404             (debug_print (" FAILURE(not in prop)");
 405             aux tables maxm cache tl (* FAILURE (not in prop) *))
 406           else
 407           match aux_single tables maxm cache metasenv subst elem goalty cc with
 408           | Fail s, tables, cache, maxm' ->
 409               assert(maxm' >= maxm);let maxm = maxm' in
 410               debug_print
 411                 (" FAIL "^s^": "^string_of_int goalno^":"^ppterm goalty);
 412               let cache =
 413                 if flags.dont_cache_failures then
 414                   cache_remove_underinspection cache goalty
 415                 else cache_add_failure cache goalty depth
 416               in
 417               aux tables maxm cache tl
 418           | Success (metasenv,subst,others), tables, cache, maxm' ->
 419               assert(maxm' >= maxm);let maxm = maxm' in
 420               (* others are alternatives in OR *)
 421               try
 422                 let goal = Cic.Meta(goalno,irl) in
 423                 let proof = CicMetaSubst.apply_subst subst goal in
 424                 debug_print ("DONE: " ^ ppterm goalty^" with: "^ppterm proof);
 425                 if is_a_green_cut goalty then
 426                   (assert_proof_is_valid proof metasenv context goalty;
 427                   let cache = cache_add_success sort cache goalty proof in
 428                   aux tables maxm cache ((metasenv,subst,gl)::tl))
 429                 else
 430                   (let goalty = CicMetaSubst.apply_subst subst goalty in
 431                   assert_proof_is_valid proof metasenv context goalty;
 432                   let cache =
 433                     if is_a_green_cut goalty then
 434                       cache_add_success sort cache goalty proof
 435                     else
 436                       cache
 437                   in
 438                   let others =
 439                     List.map
 440                       (fun (metasenv,subst,goals) -> (metasenv,subst,goals@gl))
 441                     others
 442                   in
 443                   aux tables maxm cache ((metasenv,subst,gl)::others@tl))
 444               with CicUtil.Meta_not_found i when i = goalno ->
 445                 assert false
 446         with CicUtil.Meta_not_found i when i = goalno ->
 447           (* goalno was closed by sideeffect *)
 448           debug_print ("Goal "^string_of_int goalno^" closed by sideeffect");
 449           aux tables maxm cache ((metasenv,subst,gl)::tl)
 450   and aux_single tables maxm cache metasenv subst (goalno, depth, _) goalty cc =
 451     let goalty = CicMetaSubst.apply_subst subst goalty in
 452 (*     else if not (is_in_prop context subst metasenv goalty) then Fail,cache *)
 453       (* FAILURE (euristic cut) *)
 454     match cache_examine cache goalty with
 455     | Failed_in d when d >= depth ->
 456         Fail ("depth " ^ string_of_int d ^ ">=" ^ string_of_int depth),
 457         tables,cache,maxm(*FAILURE(depth)*)
 458     | Succeded t ->
 459         assert(List.for_all (fun (i,_) -> i <> goalno) subst);
 460         let entry = goalno, (cc, t,goalty) in
 461         assert_subst_are_disjoint subst [entry];
 462         let subst = entry :: subst in
 463         let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
 464         debug_print ("  CACHE HIT!");
 465         Success (metasenv, subst, []), tables, cache, maxm
 466     | UnderInspection -> Fail "looping",tables,cache, maxm
 467     | Notfound
 468     | Failed_in _ when depth > 0 -> (* we have more depth now *)
 469         let cache = cache_add_underinspection cache goalty depth in
 470         let fake_proof = None,metasenv,Cic.Meta(goalno,irl),goalty in
 471         let elems, tables, cache, maxm =
 472           if is_equational_case goalty flags then
 473             match
 474               equational_case dbd tables maxm
 475                 ~auto:callback_for_paramod cache
 476                 depth fake_proof goalno goalty subst context flags
 477             with
 478             | Some elems, tables, cache, maxm ->
 479                 elems, tables, cache, maxm (* manca cache *)
 480             | None, tables,cache,maxm ->
 481                 applicative_case dbd tables maxm depth subst fake_proof goalno
 482                   goalty metasenv context cache
 483           else
 484             applicative_case dbd tables maxm depth subst fake_proof goalno
 485               goalty metasenv context cache
 486         in
 487         aux tables maxm cache elems
 488     | _ -> Fail "??",tables,cache,maxm
 489   in
 490     aux tables maxm cache elems
 491
 492 and
 493   auto_all_solutions dbd tables maxm cache context metasenv gl flags
 494 =
 495   let goals = order_new_goals metasenv [] gl CicPp.ppterm in
 496   let goals = List.map (fun (x,s) -> x,flags.maxdepth,s) goals in
 497   let elems = [metasenv,[],goals] in
 498   let rec aux tables maxm solutions cache elems flags =
 499     match auto_main dbd tables maxm context flags elems cache with
 500     | Fail s,tables,cache,maxm ->prerr_endline s; solutions,cache,maxm
 501     | Success (metasenv,subst,others),tables,cache,maxm ->
 502         if Unix.gettimeofday () > flags.timeout then
 503           ((subst,metasenv)::solutions), cache, maxm
 504         else
 505           aux tables maxm ((subst,metasenv)::solutions) cache others flags
 506   in
 507   let rc = aux tables maxm [] cache elems flags in
 508   prerr_endline "fine auto all solutions";
 509   rc
 510 ;;
 511
 512 (* }}} ****************** AUTO ***************)
 513
 514 let auto_all_solutions dbd cache context metasenv gl flags =
 515   let solutions, cache, _ =
 516     auto_all_solutions dbd None 0 cache context metasenv gl flags
 517   in
 518   solutions, cache
 519 ;;
 520
 521 let auto dbd cache context metasenv gl flags =
 522   let initial_time = Unix.gettimeofday() in
 523   let goals = order_new_goals metasenv [] gl CicPp.ppterm in
 524   let goals = List.map (fun (x,s) -> x,flags.maxdepth,s) goals in
 525   let elems = [metasenv,[],goals] in
 526   match auto_main dbd None 0 context flags elems cache with
 527   | Success (metasenv,subst,_), tables,cache,_ ->
 528       prerr_endline("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time));
 529       Some (subst,metasenv), cache
 530   | Fail s,tables,cache,maxm -> None,cache
 531 ;;
 532
 533 let applyS_tac ~dbd ~term =
 534  ProofEngineTypes.mk_tactic
 535   (fun status ->
 536     try
 537       let _, proof, gl,_,_ = apply_smart ~dbd ~term ~subst:[] status in
 538       proof, gl
 539     with
 540     | CicUnification.UnificationFailure msg
 541     | CicTypeChecker.TypeCheckerFailure msg ->
 542         raise (ProofEngineTypes.Fail msg))
 543