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 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 None 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 (*
 278   prerr_endline "<CACHE>";
 279   prerr_endline (cache_print context cache);
 280   prerr_endline "</CACHE>";
 281 *)
 282   match
 283     given_clause dbd ?tables maxm auto cache subst flags false (fake_proof,goalno)
 284   with
 285   | None, active,passive, bag, cache, maxmeta ->
 286       let tables = Some (active,passive,bag,cache) in
 287       None, tables, cache, maxmeta
 288   | Some(subst',(_,metasenv,proof,_),open_goals),active,passive,bag,cache,maxmeta ->
 289       let tables = Some (active,passive,bag,cache) in
 290       assert_subst_are_disjoint subst subst';
 291       let subst = subst@subst' in
 292       let open_goals = order_new_goals metasenv subst open_goals ppterm in
 293       let open_goals = List.map (fun (x,sort) -> x,depth-1,sort) open_goals in
 294       Some [metasenv,subst,open_goals], tables, cache, maxmeta
 295 ;;
 296
 297 let try_candidate
 298   goalty dbd tables maxm subst fake_proof goalno depth context cand
 299 =
 300   let ppterm = ppterm context in
 301   try
 302     let subst', ((_,metasenv,_,_), open_goals), maxmeta =
 303       PrimitiveTactics.apply_with_subst
 304         ~maxmeta:maxm ~term:cand ~subst (fake_proof,goalno)
 305     in
 306     debug_print ("   OK: " ^ ppterm cand);
 307     assert (maxmeta >= maxm);
 308     (*FIXME:sicuro che posso @?*)
 309     assert_subst_are_disjoint subst subst';
 310     let subst = subst@subst' in
 311     let open_goals = order_new_goals metasenv subst open_goals ppterm in
 312     let open_goals = List.map (fun (x,sort) -> x,depth-1,sort) open_goals in
 313     Some (metasenv,subst,open_goals), tables , maxmeta
 314   with ProofEngineTypes.Fail s ->
 315     (*debug_print("   KO: "^Lazy.force s);*)None,tables, maxm
 316 ;;
 317
 318 let applicative_case
 319   dbd tables maxm depth subst fake_proof goalno goalty metasenv context cache
 320 =
 321   let candidates = get_candidates cache goalty in
 322   let tables, elems, maxm =
 323     List.fold_left
 324       (fun (tables,elems,maxm) cand ->
 325         match
 326           try_candidate goalty
 327             dbd tables maxm subst fake_proof goalno depth context cand
 328         with
 329         | None, tables,maxm  -> tables,elems, maxm
 330         | Some x, tables, maxm -> tables,x::elems, maxm)
 331       (tables,[],maxm) candidates
 332   in
 333   let elems = sort_new_elems elems in
 334   elems, tables, cache, maxm
 335 ;;
 336
 337 (* Works if there is no dependency over proofs *)
 338 let is_a_green_cut goalty =
 339   CicUtil.is_meta_closed goalty
 340 ;;
 341 let prop = function (_,_,P) -> true | _ -> false;;
 342 let calculate_timeout flags =
 343     if flags.timeout = 0. then
 344       (prerr_endline "AUTO WITH NO TIMEOUT";{flags with timeout = infinity})
 345     else
 346       flags
 347 ;;
 348 let is_equational_case goalty flags =
 349   let ensure_equational t =
 350     if is_an_equational_goal t then true
 351     else false
 352     (*
 353       let msg="Not an equational goal.\nYou cant use the paramodulation flag"in
 354       raise (ProofEngineTypes.Fail (lazy msg))
 355     *)
 356   in
 357   (flags.use_paramod && is_an_equational_goal goalty) ||
 358   (flags.use_only_paramod && ensure_equational goalty)
 359 ;;
 360 let cache_add_success sort cache k v =
 361   if sort = P then cache_add_success cache k v else cache_remove_underinspection
 362   cache k
 363 ;;
 364
 365 let rec auto_main dbd tables maxm context flags elems cache =
 366   let callback_for_paramod maxm flags proof commonctx cache l =
 367     let flags = {flags with use_paramod = false;dont_cache_failures=true} in
 368     let _,metasenv,_,_ = proof in
 369     let oldmetasenv = metasenv in
 370     match
 371       auto_all_solutions
 372         dbd tables maxm cache commonctx metasenv l flags
 373     with
 374     | [],cache,maxm -> [],cache,maxm
 375     | solutions,cache,maxm ->
 376         let solutions =
 377           HExtlib.filter_map
 378             (fun (subst,newmetasenv) ->
 379               let opened =
 380                 ProofEngineHelpers.compare_metasenvs ~oldmetasenv ~newmetasenv
 381               in
 382               if opened = [] then Some subst else None)
 383             solutions
 384         in
 385          solutions,cache,maxm
 386   in
 387   let flags = calculate_timeout flags in
 388   let ppterm = ppterm context in
 389   let irl = mk_irl context in
 390   let rec aux tables maxm cache = function (* elems in OR *)
 391     | [] -> Fail "no more steps can be done", tables, cache, maxm
 392          (*COMPLETE FAILURE*)
 393     | (metasenv,subst,[])::tl ->
 394         Success (metasenv,subst,tl), tables, cache,maxm (* solution::cont *)
 395     | (metasenv,subst,goals)::tl when
 396       List.length (List.filter prop goals) > flags.maxwidth ->
 397         debug_print (" FAILURE(width): " ^ string_of_int (List.length goals));
 398         aux tables maxm cache tl (* FAILURE (width) *)
 399     | (metasenv,subst,((goalno,depth,sort) as elem)::gl)::tl ->
 400         if Unix.gettimeofday() > flags.timeout then
 401           Fail "timeout",tables,cache,maxm
 402         else
 403         try
 404           let _,cc,goalty = CicUtil.lookup_meta goalno metasenv in
 405           debug_print ("INSPECTING " ^ string_of_int goalno^ ":"^ppterm goalty);
 406           if sort = T && tl <> [] then (* FIXME!!!! *)
 407             (debug_print (" FAILURE(not in prop)");
 408             aux tables maxm cache tl (* FAILURE (not in prop) *))
 409           else
 410           match aux_single tables maxm cache metasenv subst elem goalty cc with
 411           | Fail s, tables, cache, maxm' ->
 412               assert(maxm' >= maxm);let maxm = maxm' in
 413               debug_print
 414                 (" FAIL "^s^": "^string_of_int goalno^":"^ppterm goalty);
 415               let cache =
 416                 if flags.dont_cache_failures then
 417                   cache_remove_underinspection cache goalty
 418                 else cache_add_failure cache goalty depth
 419               in
 420               aux tables maxm cache tl
 421           | Success (metasenv,subst,others), tables, cache, maxm' ->
 422               assert(maxm' >= maxm);let maxm = maxm' in
 423               (* others are alternatives in OR *)
 424               try
 425                 let goal = Cic.Meta(goalno,irl) in
 426                 let proof = CicMetaSubst.apply_subst subst goal in
 427                 debug_print ("DONE: " ^ ppterm goalty^" with: "^ppterm proof);
 428                 if is_a_green_cut goalty then
 429                   (assert_proof_is_valid proof metasenv context goalty;
 430                   let cache = cache_add_success sort cache goalty proof in
 431                   aux tables maxm cache ((metasenv,subst,gl)::tl))
 432                 else
 433                   (let goalty = CicMetaSubst.apply_subst subst goalty in
 434                   assert_proof_is_valid proof metasenv context goalty;
 435                   let cache =
 436                     if is_a_green_cut goalty then
 437                       cache_add_success sort cache goalty proof
 438                     else
 439                       cache
 440                   in
 441                   let others =
 442                     List.map
 443                       (fun (metasenv,subst,goals) -> (metasenv,subst,goals@gl))
 444                     others
 445                   in
 446                   aux tables maxm cache ((metasenv,subst,gl)::others@tl))
 447               with CicUtil.Meta_not_found i when i = goalno ->
 448                 assert false
 449         with CicUtil.Meta_not_found i when i = goalno ->
 450           (* goalno was closed by sideeffect *)
 451           debug_print ("Goal "^string_of_int goalno^" closed by sideeffect");
 452           aux tables maxm cache ((metasenv,subst,gl)::tl)
 453   and aux_single tables maxm cache metasenv subst (goalno, depth, _) goalty cc =
 454     let goalty = CicMetaSubst.apply_subst subst goalty in
 455 (*     else if not (is_in_prop context subst metasenv goalty) then Fail,cache *)
 456       (* FAILURE (euristic cut) *)
 457     match cache_examine cache goalty with
 458     | Failed_in d when d >= depth ->
 459         Fail ("depth " ^ string_of_int d ^ ">=" ^ string_of_int depth),
 460         tables,cache,maxm(*FAILURE(depth)*)
 461     | Succeded t ->
 462         assert(List.for_all (fun (i,_) -> i <> goalno) subst);
 463         let entry = goalno, (cc, t,goalty) in
 464         assert_subst_are_disjoint subst [entry];
 465         let subst = entry :: subst in
 466         let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
 467         debug_print ("  CACHE HIT!");
 468         Success (metasenv, subst, []), tables, cache, maxm
 469     | UnderInspection -> Fail "looping",tables,cache, maxm
 470     | Notfound
 471     | Failed_in _ when depth > 0 -> (* we have more depth now *)
 472         let cache = cache_add_underinspection cache goalty depth in
 473         let fake_proof = None,metasenv,Cic.Meta(goalno,irl),goalty in
 474         let elems, tables, cache, maxm =
 475           if is_equational_case goalty flags then
 476             match
 477               equational_case dbd tables maxm
 478                 (Some callback_for_paramod) cache
 479                 depth fake_proof goalno goalty subst context flags
 480             with
 481             | Some elems, tables, cache, maxm ->
 482                 elems, tables, cache, maxm
 483             | None, tables,cache,maxm ->
 484                 applicative_case dbd tables maxm depth subst fake_proof goalno
 485                   goalty metasenv context cache
 486           else
 487             applicative_case dbd tables maxm depth subst fake_proof goalno
 488               goalty metasenv context cache
 489         in
 490         aux tables maxm cache elems
 491     | _ -> Fail "??",tables,cache,maxm
 492   in
 493     aux tables maxm cache elems
 494
 495 and
 496   auto_all_solutions dbd tables maxm cache context metasenv gl flags
 497 =
 498   let goals = order_new_goals metasenv [] gl CicPp.ppterm in
 499   let goals = List.map (fun (x,s) -> x,flags.maxdepth,s) goals in
 500   let elems = [metasenv,[],goals] in
 501   let rec aux tables maxm solutions cache elems flags =
 502     match auto_main dbd tables maxm context flags elems cache with
 503     | Fail s,tables,cache,maxm ->prerr_endline s; solutions,cache,maxm
 504     | Success (metasenv,subst,others),tables,cache,maxm ->
 505         if Unix.gettimeofday () > flags.timeout then
 506           ((subst,metasenv)::solutions), cache, maxm
 507         else
 508           aux tables maxm ((subst,metasenv)::solutions) cache others flags
 509   in
 510   let rc = aux tables maxm [] cache elems flags in
 511   prerr_endline "fine auto all solutions";
 512   rc
 513 ;;
 514
 515 (* }}} ****************** AUTO ***************)
 516
 517 let auto_all_solutions dbd cache context metasenv gl flags =
 518   let solutions, cache, _ =
 519     auto_all_solutions dbd None 0 cache context metasenv gl flags
 520   in
 521   solutions, cache
 522 ;;
 523
 524 let auto dbd cache context metasenv gl flags =
 525   let initial_time = Unix.gettimeofday() in
 526   let goals = order_new_goals metasenv [] gl CicPp.ppterm in
 527   let goals = List.map (fun (x,s) -> x,flags.maxdepth,s) goals in
 528   let elems = [metasenv,[],goals] in
 529   match auto_main dbd None 0 context flags elems cache with
 530   | Success (metasenv,subst,_), tables,cache,_ ->
 531       prerr_endline("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time));
 532       Some (subst,metasenv), cache
 533   | Fail s,tables,cache,maxm -> None,cache
 534 ;;
 535
 536 let applyS_tac ~dbd ~term ~params =
 537  ProofEngineTypes.mk_tactic
 538   (fun status ->
 539     try
 540       let _, proof, gl,_,_ = apply_smart ~dbd ~term ~subst:[] status in
 541       proof, gl
 542     with
 543     | CicUnification.UnificationFailure msg
 544     | CicTypeChecker.TypeCheckerFailure msg ->
 545         raise (ProofEngineTypes.Fail msg))
 546