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