helm/software/components/ng_tactics/nnAuto.ml

   1 (*
   2     ||M||  This file is part of HELM, an Hypertextual, Electronic
   3     ||A||  Library of Mathematics, developed at the Computer Science
   4     ||T||  Department, University of Bologna, Italy.
   5     ||I||
   6     ||T||  HELM is free software; you can redistribute it and/or
   7     ||A||  modify it under the terms of the GNU General Public License
   8     \   /  version 2 or (at your option) any later version.
   9      \ /   This software is distributed as is, NO WARRANTY.
  10       V_______________________________________________________________ *)
  11
  12 open Printf
  13
  14 let debug = ref false
  15 let debug_print ?(depth=0) s =
  16   if !debug then prerr_endline (String.make depth '\t'^Lazy.force s) else ()
  17 (* let print = debug_print *)
  18 let print ?(depth=0) s =
  19   prerr_endline (String.make depth '\t'^Lazy.force s)
  20
  21 let debug_do f = if !debug then f () else ()
  22
  23 open Continuationals.Stack
  24 open NTacStatus
  25 module Ast = CicNotationPt
  26 let app_counter = ref 0
  27
  28 (* ======================= utility functions ========================= *)
  29 module IntSet = Set.Make(struct type t = int let compare = compare end)
  30
  31 let get_sgoalty status g =
  32  let _,_,metasenv,subst,_ = status#obj in
  33  try
  34    let _, ctx, ty = NCicUtils.lookup_meta g metasenv in
  35    let ty = NCicUntrusted.apply_subst subst ctx ty in
  36    let ctx = NCicUntrusted.apply_subst_context
  37      ~fix_projections:true subst ctx
  38    in
  39      NTacStatus.mk_cic_term ctx ty
  40  with NCicUtils.Meta_not_found _ as exn -> fail ~exn (lazy "get_sgoalty")
  41 ;;
  42
  43 let deps status g =
  44   let gty = get_sgoalty status g in
  45   metas_of_term status gty
  46 ;;
  47
  48 let menv_closure status gl =
  49   let rec closure acc = function
  50     | [] -> acc
  51     | x::l when IntSet.mem x acc -> closure acc l
  52     | x::l -> closure (IntSet.add x acc) (deps status x @ l)
  53   in closure IntSet.empty gl
  54 ;;
  55
  56 (* we call a "fact" an object whose hypothesis occur in the goal
  57    or in types of goal-variables *)
  58 let is_a_fact status ty =
  59   let status, ty, _ = saturate ~delta:0 status ty in
  60   debug_print (lazy (ppterm status ty));
  61   let g_metas = metas_of_term status ty in
  62   let clos = menv_closure status g_metas in
  63   let _,_,metasenv,_,_ = status#obj in
  64   let menv =
  65     List.fold_left
  66       (fun acc (i,_) -> IntSet.add i acc)
  67       IntSet.empty metasenv
  68   in IntSet.equal clos menv;;
  69
  70 let is_a_fact_obj s uri =
  71   let obj = NCicEnvironment.get_checked_obj uri in
  72   match obj with
  73     | (_,_,[],[],NCic.Constant(_,_,Some(t),ty,_)) ->
  74         is_a_fact s (mk_cic_term [] ty)
  75 (* aggiungere i costruttori *)
  76     | _ -> false
  77
  78 let current_goal status =
  79   let open_goals = head_goals status#stack in
  80   assert (List.length open_goals  = 1);
  81   let open_goal = List.hd open_goals in
  82   let gty = get_goalty status open_goal in
  83   let ctx = ctx_of gty in
  84     open_goal, ctx, gty
  85
  86
  87 (* =============================== paramod =========================== *)
  88 let solve fast status eq_cache goal =
  89   let f =
  90     if fast then NCicParamod.fast_eq_check
  91     else NCicParamod.paramod in
  92   let n,h,metasenv,subst,o = status#obj in
  93   let gname, ctx, gty = List.assoc goal metasenv in
  94   let gty = NCicUntrusted.apply_subst subst ctx gty in
  95   let build_status (pt, _, metasenv, subst) =
  96     try
  97       debug_print (lazy ("refining: "^(NCicPp.ppterm ctx subst metasenv pt)));
  98       let stamp = Unix.gettimeofday () in
  99       let metasenv, subst, pt, pty =
 100         NCicRefiner.typeof status
 101          (* (status#set_coerc_db NCicCoercion.empty_db) *)
 102           metasenv subst ctx pt None in
 103         debug_print (lazy ("refined: "^(NCicPp.ppterm ctx subst metasenv pt)));
 104         debug_print (lazy ("synt: "^(NCicPp.ppterm ctx subst metasenv pty)));
 105         let metasenv, subst =
 106           NCicUnification.unify status metasenv subst ctx gty pty
 107         (* the previous code is much less expensive than directly refining
 108            pt with expected type pty
 109            in
 110            prerr_endline ("exp: "^(NCicPp.ppterm ctx subst metasenv gty));
 111            NCicRefiner.typeof
 112              (status#set_coerc_db NCicCoercion.empty_db)
 113              metasenv subst ctx pt (Some gty) *)
 114         in
 115           print (lazy (Printf.sprintf "Refined in %fs"
 116                      (Unix.gettimeofday() -. stamp)));
 117           let status = status#set_obj (n,h,metasenv,subst,o) in
 118           let metasenv = List.filter (fun j,_ -> j <> goal) metasenv in
 119           let subst = (goal,(gname,ctx,pt,pty)) :: subst in
 120             Some (status#set_obj (n,h,metasenv,subst,o))
 121     with
 122         NCicRefiner.RefineFailure msg
 123       | NCicRefiner.Uncertain msg ->
 124           debug_print (lazy ("WARNING: refining in fast_eq_check failed" ^
 125                         snd (Lazy.force msg))); None
 126       | NCicRefiner.AssertFailure msg ->
 127           debug_print (lazy ("WARNING: refining in fast_eq_check failed" ^
 128                         Lazy.force msg)); None
 129       | _ -> None
 130     in
 131     HExtlib.filter_map build_status
 132       (f status metasenv subst ctx eq_cache (NCic.Rel ~-1,gty))
 133 ;;
 134
 135 let fast_eq_check eq_cache status goal =
 136   match solve true status eq_cache goal with
 137   | [] -> raise (Error (lazy "no proof found",None))
 138   | s::_ -> s
 139 ;;
 140
 141 let dist_fast_eq_check eq_cache s =
 142   NTactics.distribute_tac (fast_eq_check eq_cache) s
 143 ;;
 144
 145 let auto_eq_check eq_cache status =
 146   try
 147     let s = dist_fast_eq_check eq_cache status in
 148       [s]
 149   with
 150     | Error _ -> []
 151 ;;
 152
 153 (* warning: ctx is supposed to be already instantiated w.r.t subst *)
 154 let index_local_equations eq_cache status =
 155   let open_goals = head_goals status#stack in
 156   let open_goal = List.hd open_goals in
 157   let ngty = get_goalty status open_goal in
 158   let ctx = ctx_of ngty in
 159   let c = ref 0 in
 160   List.fold_left
 161     (fun eq_cache _ ->
 162        c:= !c+1;
 163        let t = NCic.Rel !c in
 164          try
 165            let ty = NCicTypeChecker.typeof [] [] ctx t in
 166              debug_print(lazy("eq indexing " ^ (NCicPp.ppterm ctx [] [] ty)));
 167              NCicParamod.forward_infer_step eq_cache t ty
 168          with
 169            | NCicTypeChecker.TypeCheckerFailure _
 170            | NCicTypeChecker.AssertFailure _ -> eq_cache)
 171     eq_cache ctx
 172 ;;
 173
 174 let fast_eq_check_tac ~params s =
 175   let unit_eq = index_local_equations s#eq_cache s in
 176   dist_fast_eq_check unit_eq s
 177 ;;
 178
 179 let paramod eq_cache status goal =
 180   match solve false status eq_cache goal with
 181   | [] -> raise (Error (lazy "no proof found",None))
 182   | s::_ -> s
 183 ;;
 184
 185 let paramod_tac ~params s =
 186   let unit_eq = index_local_equations s#eq_cache s in
 187   NTactics.distribute_tac (paramod unit_eq) s
 188 ;;
 189
 190 (*
 191 let fast_eq_check_tac_all  ~params eq_cache status =
 192   let g,_,_ = current_goal status in
 193   let allstates = fast_eq_check_all status eq_cache g in
 194   let pseudo_low_tac s _ _ = s in
 195   let pseudo_low_tactics =
 196     List.map pseudo_low_tac allstates
 197   in
 198     List.map (fun f -> NTactics.distribute_tac f status) pseudo_low_tactics
 199 ;;
 200 *)
 201
 202 (*
 203 let demod status eq_cache goal =
 204   let n,h,metasenv,subst,o = status#obj in
 205   let gname, ctx, gty = List.assoc goal metasenv in
 206   let gty = NCicUntrusted.apply_subst subst ctx gty in
 207
 208 let demod_tac ~params s =
 209   let unit_eq = index_local_equations s#eq_cache s in
 210   dist_fast_eq_check unit_eq s
 211 *)
 212
 213 (*************** subsumption ****************)
 214
 215 let close_wrt_context =
 216   List.fold_left
 217     (fun ty ctx_entry ->
 218         match ctx_entry with
 219        | name, NCic.Decl t -> NCic.Prod(name,t,ty)
 220        | name, NCic.Def(bo, _) -> NCicSubstitution.subst bo ty)
 221 ;;
 222
 223 let args_for_context ?(k=1) ctx =
 224   let _,args =
 225     List.fold_left
 226       (fun (n,l) ctx_entry ->
 227          match ctx_entry with
 228            | name, NCic.Decl t -> n+1,NCic.Rel(n)::l
 229            | name, NCic.Def(bo, _) -> n+1,l)
 230       (k,[]) ctx in
 231     args
 232
 233 let constant_for_meta ctx ty i =
 234   let name = "cic:/foo"^(string_of_int i)^".con" in
 235   let uri = NUri.uri_of_string name in
 236   let ty = close_wrt_context ty ctx in
 237   (* prerr_endline (NCicPp.ppterm [] [] [] ty); *)
 238   let attr = (`Generated,`Definition,`Local) in
 239   let obj = NCic.Constant([],name,None,ty,attr) in
 240     (* Constant  of relevance * string * term option * term * c_attr *)
 241     (uri,0,[],[],obj)
 242
 243 (* not used *)
 244 let refresh metasenv =
 245   List.fold_left
 246     (fun (metasenv,subst) (i,(iattr,ctx,ty)) ->
 247        let ikind = NCicUntrusted.kind_of_meta iattr in
 248        let metasenv,j,instance,ty =
 249          NCicMetaSubst.mk_meta ~attrs:iattr
 250            metasenv ctx ~with_type:ty ikind in
 251        let s_entry = i,(iattr, ctx, instance, ty) in
 252        let metasenv = List.filter (fun x,_ -> i <> x) metasenv in
 253          metasenv,s_entry::subst)
 254       (metasenv,[]) metasenv
 255
 256 (* close metasenv returns a ground instance of all the metas in the
 257 metasenv, insantiatied with axioms, and the list of these axioms *)
 258 let close_metasenv metasenv subst =
 259   (*
 260   let metasenv = NCicUntrusted.apply_subst_metasenv subst metasenv in
 261   *)
 262   let metasenv = NCicUntrusted.sort_metasenv subst metasenv in
 263     List.fold_left
 264       (fun (subst,objs) (i,(iattr,ctx,ty)) ->
 265          let ty = NCicUntrusted.apply_subst subst ctx ty in
 266          let ctx =
 267            NCicUntrusted.apply_subst_context ~fix_projections:true
 268              subst ctx in
 269          let (uri,_,_,_,obj) as okind =
 270            constant_for_meta ctx ty i in
 271          try
 272            NCicEnvironment.check_and_add_obj okind;
 273            let iref = NReference.reference_of_spec uri NReference.Decl in
 274            let iterm =
 275              let args = args_for_context ctx in
 276                if args = [] then NCic.Const iref
 277                else NCic.Appl(NCic.Const iref::args)
 278            in
 279            (* prerr_endline (NCicPp.ppterm ctx [] [] iterm); *)
 280            let s_entry = i, ([], ctx, iterm, ty)
 281            in s_entry::subst,okind::objs
 282          with _ -> assert false)
 283       (subst,[]) metasenv
 284 ;;
 285
 286 let ground_instances status gl =
 287   let _,_,metasenv,subst,_ = status#obj in
 288   let subset = menv_closure status gl in
 289   let submenv = List.filter (fun (x,_) -> IntSet.mem x subset) metasenv in
 290 (*
 291   let submenv = metasenv in
 292 *)
 293   let subst, objs = close_metasenv submenv subst in
 294   try
 295     List.iter
 296       (fun i ->
 297          let (_, ctx, t, _) = List.assoc i subst in
 298            debug_print (lazy (NCicPp.ppterm ctx [] [] t));
 299            List.iter
 300              (fun (uri,_,_,_,_) as obj ->
 301                 NCicEnvironment.invalidate_item (`Obj (uri, obj)))
 302              objs;
 303            ())
 304       gl
 305   with
 306       Not_found -> assert false
 307   (* (ctx,t) *)
 308 ;;
 309
 310 let replace_meta i args target =
 311   let rec aux k = function
 312     (* TODO: local context *)
 313     | NCic.Meta (j,lc) when i = j ->
 314         (match args with
 315            | [] -> NCic.Rel 1
 316            | _ -> let args =
 317                List.map (NCicSubstitution.subst_meta lc) args in
 318                NCic.Appl(NCic.Rel k::args))
 319     | NCic.Meta (j,lc) as m ->
 320         (match lc with
 321            _,NCic.Irl _ -> m
 322          | n,NCic.Ctx l ->
 323             NCic.Meta
 324              (i,(0,NCic.Ctx
 325                  (List.map (fun t ->
 326                    aux k (NCicSubstitution.lift n t)) l))))
 327     | t -> NCicUtils.map (fun _ k -> k+1) k aux t
 328  in
 329    aux 1 target
 330 ;;
 331
 332 let close_wrt_metasenv subst =
 333   List.fold_left
 334     (fun ty (i,(iattr,ctx,mty)) ->
 335        let mty = NCicUntrusted.apply_subst subst ctx mty in
 336        let ctx =
 337          NCicUntrusted.apply_subst_context ~fix_projections:true
 338            subst ctx in
 339        let cty = close_wrt_context mty ctx in
 340        let name = "foo"^(string_of_int i) in
 341        let ty = NCicSubstitution.lift 1 ty in
 342        let args = args_for_context ~k:1 ctx in
 343          (* prerr_endline (NCicPp.ppterm ctx [] [] iterm); *)
 344        let ty = replace_meta i args ty
 345        in
 346        NCic.Prod(name,cty,ty))
 347 ;;
 348
 349 let close status g =
 350   let _,_,metasenv,subst,_ = status#obj in
 351   let subset = menv_closure status [g] in
 352   let subset = IntSet.remove g subset in
 353   let elems = IntSet.elements subset in
 354   let _, ctx, ty = NCicUtils.lookup_meta g metasenv in
 355   let ty = NCicUntrusted.apply_subst subst ctx ty in
 356   debug_print (lazy ("metas in " ^ (NCicPp.ppterm ctx [] metasenv ty)));
 357   debug_print (lazy (String.concat ", " (List.map string_of_int elems)));
 358   let submenv = List.filter (fun (x,_) -> IntSet.mem x subset) metasenv in
 359   let submenv = List.rev (NCicUntrusted.sort_metasenv subst submenv) in
 360 (*
 361     let submenv = metasenv in
 362 *)
 363   let ty = close_wrt_metasenv subst ty submenv in
 364     debug_print (lazy (NCicPp.ppterm ctx [] [] ty));
 365     ctx,ty
 366 ;;
 367
 368
 369
 370 (* =================================== auto =========================== *)
 371 (****************** AUTO ********************
 372
 373 let calculate_timeout flags =
 374     if flags.timeout = 0. then
 375       (debug_print (lazy "AUTO WITH NO TIMEOUT");
 376        {flags with timeout = infinity})
 377     else
 378       flags
 379 ;;
 380 let is_equational_case goalty flags =
 381   let ensure_equational t =
 382     if is_an_equational_goal t then true
 383     else false
 384   in
 385   (flags.use_paramod && is_an_equational_goal goalty) ||
 386   (flags.use_only_paramod && ensure_equational goalty)
 387 ;;
 388
 389 type menv = Cic.metasenv
 390 type subst = Cic.substitution
 391 type goal = ProofEngineTypes.goal * int * AutoTypes.sort
 392 let candidate_no = ref 0;;
 393 type candidate = int * Cic.term Lazy.t
 394 type cache = AutoCache.cache
 395
 396 type fail =
 397   (* the goal (mainly for depth) and key of the goal *)
 398   goal * AutoCache.cache_key
 399 type op =
 400   (* goal has to be proved *)
 401   | D of goal
 402   (* goal has to be cached as a success obtained using candidate as the first
 403    * step *)
 404   | S of goal * AutoCache.cache_key * candidate * int
 405 type elem =
 406   (* menv, subst, size, operations done (only S), operations to do, failures to cache if any op fails *)
 407   menv * subst * int * op list * op list * fail list
 408 type status =
 409   (* list of computations that may lead to the solution: all op list will
 410    * end with the same (S(g,_)) *)
 411   elem list
 412 type auto_result =
 413   (* menv, subst, alternatives, tables, cache *)
 414   | Proved of menv * subst * elem list * AutomationCache.tables * cache
 415   | Gaveup of AutomationCache.tables * cache
 416
 417
 418 (* the status exported to the external observer *)
 419 type auto_status =
 420   (* context, (goal,candidate) list, and_list, history *)
 421   Cic.context * (int * Cic.term * bool * int * (int * Cic.term Lazy.t) list) list *
 422   (int * Cic.term * int) list * Cic.term Lazy.t list
 423
 424 let d_prefix l =
 425   let rec aux acc = function
 426     | (D g)::tl -> aux (acc@[g]) tl
 427     | _ -> acc
 428   in
 429     aux [] l
 430 ;;
 431
 432 let calculate_goal_ty (goalno,_,_) s m =
 433   try
 434     let _,cc,goalty = CicUtil.lookup_meta goalno m in
 435     (* XXX applicare la subst al contesto? *)
 436     Some (cc, CicMetaSubst.apply_subst s goalty)
 437   with CicUtil.Meta_not_found i when i = goalno -> None
 438 ;;
 439
 440 let calculate_closed_goal_ty (goalno,_,_) s =
 441   try
 442     let cc,_,goalty = List.assoc goalno s in
 443     (* XXX applicare la subst al contesto? *)
 444     Some (cc, CicMetaSubst.apply_subst s goalty)
 445   with Not_found ->
 446     None
 447 ;;
 448
 449 let pp_status ctx status =
 450   if debug then
 451   let names = Utils.names_of_context ctx in
 452   let pp x =
 453     let x =
 454       ProofEngineReduction.replace
 455         ~equality:(fun a b -> match b with Cic.Meta _ -> true | _ -> false)
 456           ~what:[Cic.Rel 1] ~with_what:[Cic.Implicit None] ~where:x
 457     in
 458     CicPp.pp x names
 459   in
 460   let string_of_do m s (gi,_,_ as g) d =
 461     match calculate_goal_ty g s m with
 462     | Some (_,gty) -> Printf.sprintf "D(%d, %s, %d)" gi (pp gty) d
 463     | None -> Printf.sprintf "D(%d, _, %d)" gi d
 464   in
 465   let string_of_s m su k (ci,ct) gi =
 466     Printf.sprintf "S(%d, %s, %s, %d)" gi (pp k) (pp (Lazy.force ct)) ci
 467   in
 468   let string_of_ol m su l =
 469     String.concat " | "
 470       (List.map
 471         (function
 472           | D (g,d,s) -> string_of_do m su (g,d,s) d
 473           | S ((gi,_,_),k,c,_) -> string_of_s m su k c gi)
 474         l)
 475   in
 476   let string_of_fl m s fl =
 477     String.concat " | "
 478       (List.map (fun ((i,_,_),ty) ->
 479          Printf.sprintf "(%d, %s)" i (pp ty)) fl)
 480   in
 481   let rec aux = function
 482     | [] -> ()
 483     | (m,s,_,_,ol,fl)::tl ->
 484         Printf.eprintf "< [%s] ;;; [%s]>\n"
 485           (string_of_ol m s ol) (string_of_fl m s fl);
 486         aux tl
 487   in
 488     Printf.eprintf "-------------------------- status -------------------\n";
 489     aux status;
 490     Printf.eprintf "-----------------------------------------------------\n";
 491 ;;
 492
 493 let auto_status = ref [] ;;
 494 let auto_context = ref [];;
 495 let in_pause = ref false;;
 496 let pause b = in_pause := b;;
 497 let cond = Condition.create ();;
 498 let mutex = Mutex.create ();;
 499 let hint = ref None;;
 500 let prune_hint = ref [];;
 501
 502 let step _ = Condition.signal cond;;
 503 let give_hint n = hint := Some n;;
 504 let give_prune_hint hint =
 505   prune_hint := hint :: !prune_hint
 506 ;;
 507
 508 let check_pause _ =
 509   if !in_pause then
 510     begin
 511       Mutex.lock mutex;
 512       Condition.wait cond mutex;
 513       Mutex.unlock mutex
 514     end
 515 ;;
 516
 517 let get_auto_status _ =
 518   let status = !auto_status in
 519   let and_list,elems,last =
 520     match status with
 521     | [] -> [],[],[]
 522     | (m,s,_,don,gl,fail)::tl ->
 523         let and_list =
 524           HExtlib.filter_map
 525             (fun (id,d,_ as g) ->
 526               match calculate_goal_ty g s m with
 527               | Some (_,x) -> Some (id,x,d) | None -> None)
 528             (d_goals gl)
 529         in
 530         let rows =
 531           (* these are the S goalsin the or list *)
 532           let orlist =
 533             List.map
 534               (fun (m,s,_,don,gl,fail) ->
 535                 HExtlib.filter_map
 536                   (function S (g,k,c,_) -> Some (g,k,c) | _ -> None)
 537                   (List.rev don @ gl))
 538               status
 539           in
 540           (* this function eats id from a list l::[id,x] returning x, l *)
 541           let eat_tail_if_eq id l =
 542             let rec aux (s, l) = function
 543               | [] -> s, l
 544               | ((id1,_,_),k1,c)::tl when id = id1 ->
 545                   (match s with
 546                   | None -> aux (Some c,l) tl
 547                   | Some _ -> assert false)
 548               | ((id1,_,_),k1,c as e)::tl -> aux (s, e::l) tl
 549             in
 550             let c, l = aux (None, []) l in
 551             c, List.rev l
 552           in
 553           let eat_in_parallel id l =
 554             let rec aux (b,eaten, new_l as acc) l =
 555               match l with
 556               | [] -> acc
 557               | l::tl ->
 558                   match eat_tail_if_eq id l with
 559                   | None, l -> aux (b@[false], eaten, new_l@[l]) tl
 560                   | Some t,l -> aux (b@[true],eaten@[t], new_l@[l]) tl
 561             in
 562             aux ([],[],[]) l
 563           in
 564           let rec eat_all rows l =
 565             match l with
 566             | [] -> rows
 567             | elem::or_list ->
 568                 match List.rev elem with
 569                 | ((to_eat,depth,_),k,_)::next_lunch ->
 570                     let b, eaten, l = eat_in_parallel to_eat l in
 571                     let eaten = HExtlib.list_uniq eaten in
 572                     let eaten = List.rev eaten in
 573                     let b = true (* List.hd (List.rev b) *) in
 574                     let rows = rows @ [to_eat,k,b,depth,eaten] in
 575                     eat_all rows l
 576                 | [] -> eat_all rows or_list
 577           in
 578           eat_all [] (List.rev orlist)
 579         in
 580         let history =
 581           HExtlib.filter_map
 582             (function (S (_,_,(_,c),_)) -> Some c | _ -> None)
 583             gl
 584         in
 585 (*         let rows = List.filter (fun (_,l) -> l <> []) rows in *)
 586         and_list, rows, history
 587   in
 588   !auto_context, elems, and_list, last
 589 ;;
 590
 591 (* Works if there is no dependency over proofs *)
 592 let is_a_green_cut goalty =
 593   CicUtil.is_meta_closed goalty
 594 ;;
 595 let rec first_s = function
 596   | (D _)::tl -> first_s tl
 597   | (S (g,k,c,s))::tl -> Some ((g,k,c,s),tl)
 598   | [] -> None
 599 ;;
 600 let list_union l1 l2 =
 601   (* TODO ottimizzare compare *)
 602   HExtlib.list_uniq (List.sort compare (l1 @ l1))
 603 ;;
 604 let rec eq_todo l1 l2 =
 605   match l1,l2 with
 606   | (D g1) :: tl1,(D g2) :: tl2 when g1=g2 -> eq_todo tl1 tl2
 607   | (S (g1,k1,(c1,lt1),i1)) :: tl1, (S (g2,k2,(c2,lt2),i2)) :: tl2
 608     when i1 = i2 && g1 = g2 && k1 = k2 && c1 = c2 ->
 609       if Lazy.force lt1 = Lazy.force lt2 then eq_todo tl1 tl2 else false
 610   | [],[] -> true
 611   | _ -> false
 612 ;;
 613 let eat_head todo id fl orlist =
 614   let rec aux acc = function
 615   | [] -> [], acc
 616   | (m, s, _, _, todo1, fl1)::tl as orlist ->
 617       let rec aux1 todo1 =
 618         match first_s todo1 with
 619         | None -> orlist, acc
 620         | Some (((gno,_,_),_,_,_), todo11) ->
 621             (* TODO confronto tra todo da ottimizzare *)
 622             if gno = id && eq_todo todo11 todo then
 623               aux (list_union fl1 acc) tl
 624             else
 625               aux1 todo11
 626       in
 627        aux1 todo1
 628   in
 629     aux fl orlist
 630 ;;
 631 let close_proof p ty menv context =
 632   let metas =
 633     List.map fst (CicUtil.metas_of_term p @ CicUtil.metas_of_term ty)
 634   in
 635   let menv = List.filter (fun (i,_,_) -> List.exists ((=)i) metas) menv in
 636   naif_closure p menv context
 637 ;;
 638 (* XXX capire bene quando aggiungere alla cache *)
 639 let add_to_cache_and_del_from_orlist_if_green_cut
 640   g s m cache key todo orlist fl ctx size minsize
 641 =
 642   let cache = cache_remove_underinspection cache key in
 643   (* prima per fare la irl usavamo il contesto vero e proprio e non quello
 644    * canonico! XXX *)
 645   match calculate_closed_goal_ty g s with
 646   | None -> assert false
 647   | Some (canonical_ctx , gty) ->
 648       let goalno,depth,sort = g in
 649       let irl = mk_irl canonical_ctx in
 650       let goal = Cic.Meta(goalno, irl) in
 651       let proof = CicMetaSubst.apply_subst s goal in
 652       let green_proof, closed_proof =
 653         let b = is_a_green_cut proof in
 654         if not b then
 655           b, (* close_proof proof gty m ctx *) proof
 656         else
 657           b, proof
 658       in
 659       debug_print (lazy ("TENTATIVE CACHE: " ^ CicPp.ppterm key));
 660       if is_a_green_cut key then
 661         (* if the initia goal was closed, we cut alternatives *)
 662         let _ = debug_print (lazy ("MANGIO: " ^ string_of_int goalno)) in
 663         let orlist, fl = eat_head todo goalno fl orlist in
 664         let cache =
 665           if size < minsize then
 666             (debug_print (lazy ("NO CACHE: 2 (size <= minsize)"));cache)
 667           else
 668           (* if the proof is closed we cache it *)
 669           if green_proof then cache_add_success cache key proof
 670           else (* cache_add_success cache key closed_proof *)
 671             (debug_print (lazy ("NO CACHE: (no gree proof)"));cache)
 672         in
 673         cache, orlist, fl, true
 674       else
 675         let cache =
 676           debug_print (lazy ("TENTATIVE CACHE: " ^ CicPp.ppterm gty));
 677           if size < minsize then
 678             (debug_print (lazy ("NO CACHE: (size <= minsize)")); cache) else
 679           (* if the substituted goal and the proof are closed we cache it *)
 680           if is_a_green_cut gty then
 681             if green_proof then cache_add_success cache gty proof
 682             else (* cache_add_success cache gty closed_proof *)
 683               (debug_print (lazy ("NO CACHE: (no green proof (gty))"));cache)
 684           else (*
 685             try
 686               let ty, _ =
 687                 CicTypeChecker.type_of_aux' ~subst:s
 688                   m ctx closed_proof CicUniv.oblivion_ugraph
 689               in
 690               if is_a_green_cut ty then
 691                 cache_add_success cache ty closed_proof
 692               else cache
 693             with
 694             | CicTypeChecker.TypeCheckerFailure _ ->*)
 695           (debug_print (lazy ("NO CACHE: (no green gty )"));cache)
 696         in
 697         cache, orlist, fl, false
 698 ;;
 699 let close_failures (fl : fail list) (cache : cache) =
 700   List.fold_left
 701     (fun cache ((gno,depth,_),gty) ->
 702       if CicUtil.is_meta_closed gty then
 703        ( debug_print (lazy ("FAIL: INDUCED: " ^ string_of_int gno));
 704          cache_add_failure cache gty depth)
 705       else
 706          cache)
 707     cache fl
 708 ;;
 709 let put_in_subst subst metasenv  (goalno,_,_) canonical_ctx t ty =
 710   let entry = goalno, (canonical_ctx, t,ty) in
 711   assert_subst_are_disjoint subst [entry];
 712   let subst = entry :: subst in
 713
 714   let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
 715
 716   subst, metasenv
 717 ;;
 718
 719 let mk_fake_proof metasenv subst (goalno,_,_) goalty context =
 720   None,metasenv,subst ,(lazy (Cic.Meta(goalno,mk_irl context))),goalty, []
 721 ;;
 722
 723 let equational_case
 724   tables cache depth fake_proof goalno goalty subst context
 725     flags
 726 =
 727   let active,passive,bag = tables in
 728   let ppterm = ppterm context in
 729   let status = (fake_proof,goalno) in
 730     if flags.use_only_paramod then
 731       begin
 732         debug_print (lazy ("PARAMODULATION SU: " ^
 733                          string_of_int goalno ^ " " ^ ppterm goalty ));
 734         let goal_steps, saturation_steps, timeout =
 735           max_int,max_int,flags.timeout
 736         in
 737         match
 738           Saturation.given_clause bag status active passive
 739             goal_steps saturation_steps timeout
 740         with
 741           | None, active, passive, bag ->
 742               [], (active,passive,bag), cache, flags
 743           | Some(subst',(_,metasenv,_subst,proof,_, _),open_goals),active,
 744             passive,bag ->
 745               assert_subst_are_disjoint subst subst';
 746               let subst = subst@subst' in
 747               let open_goals =
 748                 order_new_goals metasenv subst open_goals ppterm
 749               in
 750               let open_goals =
 751                 List.map (fun (x,sort) -> x,depth-1,sort) open_goals
 752               in
 753               incr candidate_no;
 754               [(!candidate_no,proof),metasenv,subst,open_goals],
 755                 (active,passive,bag), cache, flags
 756       end
 757     else
 758       begin
 759         debug_print (lazy ("NARROWING DEL GOAL: " ^
 760                          string_of_int goalno ^ " " ^ ppterm goalty ));
 761         let goal_steps, saturation_steps, timeout =
 762           1,0,flags.timeout
 763         in
 764         match
 765           Saturation.solve_narrowing bag status active passive goal_steps
 766         with
 767           | None, active, passive, bag ->
 768               [], (active,passive,bag), cache, flags
 769           | Some(subst',(_,metasenv,_subst,proof,_, _),open_goals),active,
 770             passive,bag ->
 771               assert_subst_are_disjoint subst subst';
 772               let subst = subst@subst' in
 773               let open_goals =
 774                 order_new_goals metasenv subst open_goals ppterm
 775               in
 776               let open_goals =
 777                 List.map (fun (x,sort) -> x,depth-1,sort) open_goals
 778               in
 779               incr candidate_no;
 780               [(!candidate_no,proof),metasenv,subst,open_goals],
 781                 (active,passive,bag), cache, flags
 782       end
 783 (*
 784       begin
 785         let params = ([],["use_context","false"]) in
 786         let automation_cache = {
 787               AutomationCache.tables = tables ;
 788               AutomationCache.univ = Universe.empty; }
 789         in
 790         try
 791           let ((_,metasenv,subst,_,_,_),open_goals) =
 792
 793             solve_rewrite ~params ~automation_cache
 794               (fake_proof, goalno)
 795           in
 796           let proof = lazy (Cic.Meta (-1,[])) in
 797           [(!candidate_no,proof),metasenv,subst,[]],tables, cache, flags
 798         with ProofEngineTypes.Fail _ -> [], tables, cache, flags
 799 (*
 800         let res = Saturation.all_subsumed bag status active passive in
 801         let res' =
 802           List.map
 803             (fun (subst',(_,metasenv,_subst,proof,_, _),open_goals) ->
 804                assert_subst_are_disjoint subst subst';
 805                let subst = subst@subst' in
 806                let open_goals =
 807                  order_new_goals metasenv subst open_goals ppterm
 808                in
 809                let open_goals =
 810                  List.map (fun (x,sort) -> x,depth-1,sort) open_goals
 811                in
 812                incr candidate_no;
 813                  (!candidate_no,proof),metasenv,subst,open_goals)
 814             res
 815           in
 816           res', (active,passive,bag), cache, flags
 817 *)
 818       end
 819 *)
 820 ;;
 821
 822 let sort_new_elems =
 823  List.sort (fun (_,_,_,l1) (_,_,_,l2) ->
 824          let p1 = List.length (prop_only l1) in
 825          let p2 = List.length (prop_only l2) in
 826          if p1 = p2 then List.length l1 - List.length l2 else p1-p2)
 827 ;;
 828
 829
 830 let try_candidate dbd
 831   goalty tables subst fake_proof goalno depth context cand
 832 =
 833   let ppterm = ppterm context in
 834   try
 835     let actives, passives, bag = tables in
 836     let (_,metasenv,subst,_,_,_), open_goals =
 837        ProofEngineTypes.apply_tactic
 838         (PrimitiveTactics.apply_tac ~term:cand)
 839         (fake_proof,goalno)
 840     in
 841     let tables = actives, passives,
 842       Equality.push_maxmeta bag
 843         (max (Equality.maxmeta bag) (CicMkImplicit.new_meta metasenv subst))
 844     in
 845     debug_print (lazy ("   OK: " ^ ppterm cand));
 846     let metasenv = CicRefine.pack_coercion_metasenv metasenv in
 847     let open_goals = order_new_goals metasenv subst open_goals ppterm in
 848     let open_goals = List.map (fun (x,sort) -> x,depth-1,sort) open_goals in
 849     incr candidate_no;
 850     Some ((!candidate_no,lazy cand),metasenv,subst,open_goals), tables
 851   with
 852     | ProofEngineTypes.Fail s -> None,tables
 853     | CicUnification.Uncertain s ->  None,tables
 854 ;;
 855
 856 let applicative_case dbd
 857   tables depth subst fake_proof goalno goalty metasenv context
 858   signature universe cache flags
 859 =
 860   (* let goalty_aux =
 861     match goalty with
 862     | Cic.Appl (hd::tl) ->
 863         Cic.Appl (hd :: HExtlib.mk_list (Cic.Meta (0,[])) (List.length tl))
 864     | _ -> goalty
 865   in *)
 866   let goalty_aux = goalty in
 867   let candidates =
 868     get_candidates flags.skip_trie_filtering universe cache goalty_aux
 869   in
 870   (* if the goal is an equality we skip the congruence theorems
 871   let candidates =
 872     if is_equational_case goalty flags
 873     then List.filter not_default_eq_term candidates
 874     else candidates
 875   in *)
 876   let candidates = List.filter (only signature context metasenv) candidates
 877   in
 878   let tables, elems =
 879     List.fold_left
 880       (fun (tables,elems) cand ->
 881         match
 882           try_candidate dbd goalty
 883             tables subst fake_proof goalno depth context cand
 884         with
 885         | None, tables -> tables, elems
 886         | Some x, tables -> tables, x::elems)
 887       (tables,[]) candidates
 888   in
 889   let elems = sort_new_elems elems in
 890   elems, tables, cache
 891 ;;
 892
 893 let try_smart_candidate dbd
 894   goalty tables subst fake_proof goalno depth context cand
 895 =
 896   let ppterm = ppterm context in
 897   try
 898     let params = ([],[]) in
 899     let automation_cache = {
 900           AutomationCache.tables = tables ;
 901           AutomationCache.univ = Universe.empty; }
 902     in
 903     debug_print (lazy ("candidato per " ^ string_of_int goalno
 904       ^ ": " ^ CicPp.ppterm cand));
 905 (*
 906     let (_,metasenv,subst,_,_,_) = fake_proof in
 907     prerr_endline ("metasenv:\n" ^ CicMetaSubst.ppmetasenv [] metasenv);
 908     prerr_endline ("subst:\n" ^ CicMetaSubst.ppsubst ~metasenv subst);
 909 *)
 910     let ((_,metasenv,subst,_,_,_),open_goals) =
 911       apply_smart ~dbd ~term:cand ~params ~automation_cache
 912         (fake_proof, goalno)
 913     in
 914     let metasenv = CicRefine.pack_coercion_metasenv metasenv in
 915     let open_goals = order_new_goals metasenv subst open_goals ppterm in
 916     let open_goals = List.map (fun (x,sort) -> x,depth-1,sort) open_goals in
 917     incr candidate_no;
 918     Some ((!candidate_no,lazy cand),metasenv,subst,open_goals), tables
 919   with
 920   | ProofEngineTypes.Fail s -> None,tables
 921   | CicUnification.Uncertain s ->  None,tables
 922 ;;
 923
 924 let smart_applicative_case dbd
 925   tables depth subst fake_proof goalno goalty metasenv context signature
 926   universe cache flags
 927 =
 928   let goalty_aux =
 929     match goalty with
 930     | Cic.Appl (hd::tl) ->
 931         Cic.Appl (hd :: HExtlib.mk_list (Cic.Meta (0,[])) (List.length tl))
 932     | _ -> goalty
 933   in
 934   let smart_candidates =
 935     get_candidates flags.skip_trie_filtering universe cache goalty_aux
 936   in
 937   let candidates =
 938     get_candidates flags.skip_trie_filtering universe cache goalty
 939   in
 940   let smart_candidates =
 941     List.filter
 942       (fun x -> not(List.mem x candidates)) smart_candidates
 943   in
 944   let debug_msg =
 945     (lazy ("smart_candidates" ^ " = " ^
 946              (String.concat "\n" (List.map CicPp.ppterm smart_candidates)))) in
 947   debug_print debug_msg;
 948   let candidates = List.filter (only signature context metasenv) candidates in
 949   let smart_candidates =
 950     List.filter (only signature context metasenv) smart_candidates
 951   in
 952 (*
 953   let penalty cand depth =
 954     if only signature context metasenv cand then depth else ((prerr_endline (
 955     "penalizzo " ^ CicPp.ppterm cand));depth -1)
 956   in
 957 *)
 958   let tables, elems =
 959     List.fold_left
 960       (fun (tables,elems) cand ->
 961         match
 962           try_candidate dbd goalty
 963             tables subst fake_proof goalno depth context cand
 964         with
 965         | None, tables ->
 966             (* if normal application fails we try to be smart *)
 967             (match try_smart_candidate dbd goalty
 968                tables subst fake_proof goalno depth context cand
 969              with
 970                | None, tables -> tables, elems
 971                | Some x, tables -> tables, x::elems)
 972         | Some x, tables -> tables, x::elems)
 973       (tables,[]) candidates
 974   in
 975   let tables, smart_elems =
 976       List.fold_left
 977         (fun (tables,elems) cand ->
 978           match
 979             try_smart_candidate dbd goalty
 980               tables subst fake_proof goalno depth context cand
 981           with
 982           | None, tables -> tables, elems
 983           | Some x, tables -> tables, x::elems)
 984         (tables,[]) smart_candidates
 985   in
 986   let elems = sort_new_elems (elems @ smart_elems) in
 987   elems, tables, cache
 988 ;;
 989
 990 let equational_and_applicative_case dbd
 991   signature universe flags m s g gty tables cache context
 992 =
 993   let goalno, depth, sort = g in
 994   let fake_proof = mk_fake_proof m s g gty context in
 995   if is_equational_case gty flags then
 996     let elems,tables,cache, flags =
 997       equational_case tables cache
 998         depth fake_proof goalno gty s context flags
 999     in
1000     let more_elems, tables, cache =
1001       if flags.use_only_paramod then
1002         [],tables, cache
1003       else
1004         applicative_case dbd
1005           tables depth s fake_proof goalno
1006             gty m context signature universe cache flags
1007     in
1008       elems@more_elems, tables, cache, flags
1009   else
1010     let elems, tables, cache =
1011       match LibraryObjects.eq_URI () with
1012       | Some _ ->
1013          smart_applicative_case dbd tables depth s fake_proof goalno
1014            gty m context signature universe cache flags
1015       | None ->
1016          applicative_case dbd tables depth s fake_proof goalno
1017            gty m context signature universe cache flags
1018     in
1019       elems, tables, cache, flags
1020 ;;
1021 let rec condition_for_hint i = function
1022   | [] -> false
1023   | S (_,_,(j,_),_):: tl -> j <> i (* && condition_for_hint i tl *)
1024   | _::tl -> condition_for_hint i tl
1025 ;;
1026 let prunable_for_size flags s m todo =
1027   let rec aux b = function
1028     | (S _)::tl -> aux b tl
1029     | (D (_,_,T))::tl -> aux b tl
1030     | (D g)::tl ->
1031         (match calculate_goal_ty g s m with
1032           | None -> aux b tl
1033           | Some (canonical_ctx, gty) ->
1034             let gsize, _ =
1035               Utils.weight_of_term
1036                 ~consider_metas:false ~count_metas_occurrences:true gty in
1037             let newb = b || gsize > flags.maxgoalsizefactor in
1038             aux newb tl)
1039     | [] -> b
1040   in
1041     aux false todo
1042
1043 (*
1044 let prunable ty todo =
1045   let rec aux b = function
1046     | (S(_,k,_,_))::tl -> aux (b || Equality.meta_convertibility k ty) tl
1047     | (D (_,_,T))::tl -> aux b tl
1048     | D _::_ -> false
1049     | [] -> b
1050   in
1051     aux false todo
1052 ;;
1053 *)
1054
1055 let prunable menv subst ty todo =
1056   let rec aux = function
1057     | (S(_,k,_,_))::tl ->
1058          (match Equality.meta_convertibility_subst k ty menv with
1059           | None -> aux tl
1060           | Some variant ->
1061                no_progress variant tl (* || aux tl*))
1062     | (D (_,_,T))::tl -> aux tl
1063     | _ -> false
1064   and no_progress variant = function
1065     | [] -> (*prerr_endline "++++++++++++++++++++++++ no_progress";*) true
1066     | D ((n,_,P) as g)::tl ->
1067         (match calculate_goal_ty g subst menv with
1068            | None -> no_progress variant tl
1069            | Some (_, gty) ->
1070                (match calculate_goal_ty g variant menv with
1071                   | None -> assert false
1072                   | Some (_, gty') ->
1073                       if gty = gty' then no_progress variant tl
1074 (*
1075 (prerr_endline (string_of_int n);
1076  prerr_endline (CicPp.ppterm gty);
1077  prerr_endline (CicPp.ppterm gty');
1078  prerr_endline "---------- subst";
1079  prerr_endline (CicMetaSubst.ppsubst ~metasenv:menv subst);
1080  prerr_endline "---------- variant";
1081  prerr_endline (CicMetaSubst.ppsubst ~metasenv:menv variant);
1082  prerr_endline "---------- menv";
1083  prerr_endline (CicMetaSubst.ppmetasenv [] menv);
1084                          no_progress variant tl) *)
1085                       else false))
1086     | _::tl -> no_progress variant tl
1087   in
1088     aux todo
1089
1090 ;;
1091 let condition_for_prune_hint prune (m, s, size, don, todo, fl) =
1092   let s =
1093     HExtlib.filter_map (function S (_,_,(c,_),_) -> Some c | _ -> None) todo
1094   in
1095   List.for_all (fun i -> List.for_all (fun j -> i<>j) prune) s
1096 ;;
1097 let filter_prune_hint c l =
1098   let prune = !prune_hint in
1099   prune_hint := []; (* possible race... *)
1100   if prune = [] then c,l
1101   else
1102     cache_reset_underinspection c,
1103     List.filter (condition_for_prune_hint prune) l
1104 ;;
1105
1106
1107
1108 let
1109   auto_all_solutions dbd tables universe cache context metasenv gl flags
1110 =
1111   let signature =
1112     List.fold_left
1113       (fun set g ->
1114          MetadataConstraints.UriManagerSet.union set
1115              (MetadataQuery.signature_of metasenv g)
1116        )
1117       MetadataConstraints.UriManagerSet.empty gl
1118   in
1119   let goals = order_new_goals metasenv [] gl CicPp.ppterm in
1120   let goals =
1121     List.map
1122       (fun (x,s) -> D (x,flags.maxdepth,s)) goals
1123   in
1124   let elems = [metasenv,[],1,[],goals,[]] in
1125   let rec aux tables solutions cache elems flags =
1126     match auto_main dbd tables context flags signature universe cache elems with
1127     | Gaveup (tables,cache) ->
1128         solutions,cache, tables
1129     | Proved (metasenv,subst,others,tables,cache) ->
1130         if Unix.gettimeofday () > flags.timeout then
1131           ((subst,metasenv)::solutions), cache, tables
1132         else
1133           aux tables ((subst,metasenv)::solutions) cache others flags
1134   in
1135   let rc = aux tables [] cache elems flags in
1136     match rc with
1137     | [],cache,tables -> [],cache,tables
1138     | solutions, cache,tables ->
1139         let solutions =
1140           HExtlib.filter_map
1141             (fun (subst,newmetasenv) ->
1142               let opened =
1143                 ProofEngineHelpers.compare_metasenvs ~oldmetasenv:metasenv ~newmetasenv
1144               in
1145               if opened = [] then Some subst else None)
1146             solutions
1147         in
1148          solutions,cache,tables
1149 ;;
1150
1151 (******************* AUTO ***************)
1152
1153
1154 let auto dbd flags metasenv tables universe cache context metasenv gl =
1155   let initial_time = Unix.gettimeofday() in
1156   let signature =
1157     List.fold_left
1158       (fun set g ->
1159          MetadataConstraints.UriManagerSet.union set
1160              (MetadataQuery.signature_of metasenv g)
1161        )
1162       MetadataConstraints.UriManagerSet.empty gl
1163   in
1164   let goals = order_new_goals metasenv [] gl CicPp.ppterm in
1165   let goals = List.map (fun (x,s) -> D(x,flags.maxdepth,s)) goals in
1166   let elems = [metasenv,[],1,[],goals,[]] in
1167   match auto_main dbd tables context flags signature universe cache elems with
1168   | Proved (metasenv,subst,_, tables,cache) ->
1169       debug_print(lazy
1170         ("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time)));
1171       Some (subst,metasenv), cache
1172   | Gaveup (tables,cache) ->
1173       debug_print(lazy
1174         ("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time)));
1175       None,cache
1176 ;;
1177
1178 let auto_tac ~(dbd:HSql.dbd) ~params:(univ,params) ~automation_cache (proof, goal) =
1179   let flags = flags_of_params params () in
1180   let use_library = flags.use_library in
1181   let universe, tables, cache =
1182     init_cache_and_tables
1183      ~dbd ~use_library ~use_context:(not flags.skip_context)
1184      automation_cache univ (proof, goal)
1185   in
1186   let _,metasenv,subst,_,_, _ = proof in
1187   let _,context,goalty = CicUtil.lookup_meta goal metasenv in
1188   let signature = MetadataQuery.signature_of metasenv goal in
1189   let signature =
1190     List.fold_left
1191       (fun set t ->
1192          let ty, _ =
1193            CicTypeChecker.type_of_aux' metasenv context t
1194              CicUniv.oblivion_ugraph
1195          in
1196          MetadataConstraints.UriManagerSet.union set
1197            (MetadataConstraints.constants_of ty)
1198        )
1199       signature univ
1200   in
1201   let tables,cache =
1202     if flags.close_more then
1203       close_more
1204         tables context (proof, goal)
1205           (auto_all_solutions dbd) signature universe cache
1206     else tables,cache in
1207   let initial_time = Unix.gettimeofday() in
1208   let (_,oldmetasenv,_,_,_, _) = proof in
1209     hint := None;
1210   let elem =
1211     metasenv,subst,1,[],[D (goal,flags.maxdepth,P)],[]
1212   in
1213   match auto_main dbd tables context flags signature universe cache [elem] with
1214     | Proved (metasenv,subst,_, tables,cache) ->
1215         debug_print (lazy
1216           ("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time)));
1217         let proof,metasenv =
1218         ProofEngineHelpers.subst_meta_and_metasenv_in_proof
1219           proof goal subst metasenv
1220         in
1221         let opened =
1222           ProofEngineHelpers.compare_metasenvs ~oldmetasenv
1223             ~newmetasenv:metasenv
1224         in
1225           proof,opened
1226     | Gaveup (tables,cache) ->
1227         debug_print
1228           (lazy ("TIME:"^
1229             string_of_float(Unix.gettimeofday()-.initial_time)));
1230         raise (ProofEngineTypes.Fail (lazy "Auto gave up"))
1231 ;;
1232 *)
1233
1234 (****************** smart application ********************)
1235
1236
1237 let smart_apply t unit_eq status g =
1238   let n,h,metasenv,subst,o = status#obj in
1239   let gname, ctx, gty = List.assoc g metasenv in
1240   (* let ggty = mk_cic_term context gty in *)
1241   let status, t = disambiguate status ctx t None in
1242   let status,t = term_of_cic_term status t ctx in
1243   let ty = NCicTypeChecker.typeof subst metasenv ctx t in
1244   let ty,metasenv,args = NCicMetaSubst.saturate metasenv subst ctx ty 0 in
1245   let metasenv,j,inst,_ = NCicMetaSubst.mk_meta metasenv ctx `IsTerm in
1246   let status = status#set_obj (n,h,metasenv,subst,o) in
1247   let pterm = if args=[] then t else NCic.Appl(t::args) in
1248   let eq_coerc =
1249     let uri =
1250       NUri.uri_of_string "cic:/matita/ng/Plogic/equality/eq_coerc.con" in
1251     let ref = NReference.reference_of_spec uri (NReference.Def(2)) in
1252       NCic.Const ref
1253   in
1254   let smart =
1255     NCic.Appl[eq_coerc;ty;NCic.Implicit `Type;pterm;inst] in
1256   let smart = mk_cic_term ctx smart in
1257     try
1258       let status = instantiate status g smart in
1259       let _,_,metasenv,subst,_ = status#obj in
1260       let _,ctx,jty = List.assoc j metasenv in
1261       let jty = NCicUntrusted.apply_subst subst ctx jty in
1262         debug_print(lazy("goal " ^ (NCicPp.ppterm ctx [] [] jty)));
1263         fast_eq_check unit_eq status j
1264     with
1265       | Error _ as e -> debug_print (lazy "error"); raise e
1266
1267 let smart_apply_tac t s =
1268   let unit_eq = index_local_equations s#eq_cache s in
1269   NTactics.distribute_tac (smart_apply t unit_eq) s
1270
1271 let smart_apply_auto t eq_cache =
1272   NTactics.distribute_tac (smart_apply t eq_cache)
1273
1274
1275 (****************** types **************)
1276
1277
1278 type th_cache = (NCic.context * InvRelDiscriminationTree.t) list
1279
1280 let keys_of_term status t =
1281   let status, orig_ty = typeof status (ctx_of t) t in
1282   let _, ty, _ = saturate ~delta:max_int status orig_ty in
1283   let keys = [ty] in
1284   let keys =
1285     let _, ty = term_of_cic_term status ty (ctx_of ty) in
1286     match ty with
1287     | NCic.Const (NReference.Ref (_,NReference.Def h))
1288     | NCic.Appl (NCic.Const(NReference.Ref(_,NReference.Def h))::_)
1289        when h > 0 ->
1290          let _,ty,_= saturate status ~delta:(h-1) orig_ty in
1291          ty::keys
1292     | _ -> keys
1293   in
1294   status, keys
1295 ;;
1296
1297 let mk_th_cache status gl =
1298   List.fold_left
1299     (fun (status, acc) g ->
1300        let gty = get_goalty status g in
1301        let ctx = ctx_of gty in
1302        debug_print(lazy("th cache for: "^ppterm status gty));
1303        debug_print(lazy("th cache in: "^ppcontext status ctx));
1304        if List.mem_assq ctx acc then status, acc else
1305          let idx = InvRelDiscriminationTree.empty in
1306          let status,_,idx =
1307            List.fold_left
1308              (fun (status, i, idx) _ ->
1309                 let t = mk_cic_term ctx (NCic.Rel i) in
1310                 debug_print(lazy("indexing: "^ppterm status t));
1311                 let status, keys = keys_of_term status t in
1312                 let idx =
1313                   List.fold_left (fun idx k ->
1314                     InvRelDiscriminationTree.index idx k t) idx keys
1315                 in
1316                 status, i+1, idx)
1317              (status, 1, idx) ctx
1318           in
1319          status, (ctx, idx) :: acc)
1320     (status,[]) gl
1321 ;;
1322
1323 let add_to_th t c ty =
1324   let key_c = ctx_of t in
1325   if not (List.mem_assq key_c c) then
1326       (key_c ,InvRelDiscriminationTree.index
1327                InvRelDiscriminationTree.empty ty t ) :: c
1328   else
1329     let rec replace = function
1330       | [] -> []
1331       | (x, idx) :: tl when x == key_c ->
1332           (x, InvRelDiscriminationTree.index idx ty t) :: tl
1333       | x :: tl -> x :: replace tl
1334     in
1335       replace c
1336 ;;
1337
1338 let pp_idx status idx =
1339    InvRelDiscriminationTree.iter idx
1340       (fun k set ->
1341          debug_print(lazy("K: " ^ NCicInverseRelIndexable.string_of_path k));
1342          Ncic_termSet.iter
1343            (fun t -> debug_print(lazy("\t"^ppterm status t)))
1344            set)
1345 ;;
1346
1347 let pp_th status =
1348   List.iter
1349     (fun ctx, idx ->
1350        debug_print(lazy( "-----------------------------------------------"));
1351        debug_print(lazy( (NCicPp.ppcontext ~metasenv:[] ~subst:[] ctx)));
1352        debug_print(lazy( "||====>  "));
1353        pp_idx status idx)
1354 ;;
1355
1356 let search_in_th gty th =
1357   let c = ctx_of gty in
1358   let rec aux acc = function
1359    | [] -> (* Ncic_termSet.elements *) acc
1360    | (_::tl) as k ->
1361        try
1362          let idx = List.assq k th in
1363          let acc = Ncic_termSet.union acc
1364            (InvRelDiscriminationTree.retrieve_unifiables idx gty)
1365          in
1366          aux acc tl
1367        with Not_found -> aux acc tl
1368   in
1369     aux Ncic_termSet.empty c
1370 ;;
1371
1372 type flags = {
1373         do_types : bool; (* solve goals in Type *)
1374         maxwidth : int;
1375         maxsize  : int;
1376         maxdepth : int;
1377         timeout  : float;
1378 }
1379
1380 type cache =
1381     {facts : th_cache; (* positive results *)
1382      under_inspection : th_cache; (* to prune looping *)
1383      unit_eq : NCicParamod.state
1384     }
1385
1386 type sort = T | P
1387 type goal = int * sort (* goal, depth, sort *)
1388 type fail = goal * cic_term
1389 type candidate = int * Ast.term (* unique candidate number, candidate *)
1390
1391 exception Gaveup of IntSet.t (* a sublist of unprovable conjunctive
1392                                 atoms of the input goals *)
1393 exception Proved of NTacStatus.tac_status
1394
1395 (* let close_failures _ c = c;; *)
1396 (* let prunable _ _ _ = false;; *)
1397 (* let cache_examine cache gty = `Notfound;; *)
1398 (* let put_in_subst s _ _ _  = s;; *)
1399 (* let add_to_cache_and_del_from_orlist_if_green_cut _ _ c _ _ o f _ = c, o, f, false ;; *)
1400 (* let cache_add_underinspection c _ _ = c;; *)
1401
1402 let init_cache ?(facts=[]) ?(under_inspection=[])
1403     ?(unit_eq=NCicParamod.empty_state) _ =
1404     {facts = facts;
1405      under_inspection = under_inspection;
1406      unit_eq = unit_eq
1407     }
1408
1409 let only _ _ _ = true;;
1410
1411 let candidate_no = ref 0;;
1412
1413 let openg_no status = List.length (head_goals status#stack)
1414
1415 let sort_new_elems l =
1416   List.sort (fun (_,s1) (_,s2) -> openg_no s1 - openg_no s2) l
1417
1418 let try_candidate ?(smart=0) flags depth status eq_cache t =
1419  try
1420    print ~depth (lazy ("------------ try " ^ CicNotationPp.pp_term t));
1421   let status =
1422     if smart= 0 then NTactics.apply_tac ("",0,t) status
1423     else if smart = 1 then smart_apply_auto ("",0,t) eq_cache status
1424     else (* smart = 2: both *)
1425       try NTactics.apply_tac ("",0,t) status
1426       with Error _ ->
1427         smart_apply_auto ("",0,t) eq_cache status in
1428   let og_no = openg_no status in
1429     if (* og_no > flags.maxwidth || *)
1430       (depth = flags.maxdepth && og_no <> 0) then
1431         (print ~depth (lazy "pruned immediately"); None)
1432    else
1433      (incr candidate_no;
1434       Some ((!candidate_no,t),status))
1435  with Error (msg,exn) -> debug_print ~depth (lazy "failed"); None
1436 ;;
1437
1438 let get_candidates ?(smart=true) status cache signature gty =
1439   let universe = status#auto_cache in
1440   let context = ctx_of gty in
1441   let t_ast t =
1442      let _status, t = term_of_cic_term status t context
1443      in Ast.NCic t in
1444   let c_ast = function
1445     | NCic.Const r -> Ast.NRef r | _ -> assert false in
1446   let _, raw_gty = term_of_cic_term status gty context in
1447   let cands = NDiscriminationTree.DiscriminationTree.retrieve_unifiables
1448         universe raw_gty in
1449   let local_cands = search_in_th gty cache in
1450   let together global local =
1451     List.map c_ast
1452       (List.filter (only signature context)
1453         (NDiscriminationTree.TermSet.elements global)) @
1454       List.map t_ast (Ncic_termSet.elements local) in
1455   let candidates = together cands local_cands in
1456   let smart_candidates =
1457     if smart then
1458       match raw_gty with
1459         | NCic.Appl (hd::tl) ->
1460             let weak_gty =
1461               NCic.Appl (hd:: HExtlib.mk_list(NCic.Meta (0,(0,NCic.Irl 0)))
1462                            (List.length tl)) in
1463             let more_cands =
1464               NDiscriminationTree.DiscriminationTree.retrieve_unifiables
1465                 universe weak_gty in
1466             let smart_cands =
1467               NDiscriminationTree.TermSet.diff more_cands cands in
1468             let cic_weak_gty = mk_cic_term context weak_gty in
1469             let more_local_cands = search_in_th cic_weak_gty cache in
1470             let smart_local_cands =
1471               Ncic_termSet.diff more_local_cands local_cands in
1472               together smart_cands smart_local_cands
1473         | _ -> []
1474     else []
1475   in
1476     candidates, smart_candidates
1477 ;;
1478
1479 let applicative_case depth signature status flags gty (cache:cache) =
1480   app_counter:= !app_counter+1;
1481   let _,_,metasenv,subst,_ = status#obj in
1482   let context = ctx_of gty in
1483   let tcache = cache.facts in
1484   let is_eq =
1485     let status, t = term_of_cic_term status gty context  in
1486     NCicParamod.is_equation metasenv subst context t
1487   in
1488   debug_print(lazy (string_of_bool is_eq));
1489   let candidates, smart_candidates =
1490     get_candidates ~smart:(not is_eq) status tcache signature gty in
1491   debug_print ~depth
1492     (lazy ("candidates: " ^ string_of_int (List.length candidates)));
1493   debug_print ~depth
1494     (lazy ("smart candidates: " ^
1495              string_of_int (List.length smart_candidates)));
1496 (*
1497   let sm = 0 in
1498   let smart_candidates = [] in *)
1499   let sm = if is_eq then 0 else 2 in
1500   let elems =
1501     List.fold_left
1502       (fun elems cand ->
1503         match try_candidate (~smart:sm)
1504           flags depth status cache.unit_eq cand with
1505         | None -> elems
1506         | Some x -> x::elems)
1507       [] candidates
1508   in
1509   let more_elems =
1510     List.fold_left
1511       (fun elems cand ->
1512         match try_candidate (~smart:1)
1513           flags depth status cache.unit_eq cand with
1514         | None -> elems
1515         | Some x -> x::elems)
1516       [] smart_candidates
1517   in
1518   elems@more_elems
1519 ;;
1520
1521 exception Found
1522 ;;
1523
1524 (* gty is supposed to be meta-closed *)
1525 let is_subsumed depth status gty cache =
1526   if cache=[] then false else (
1527   debug_print ~depth (lazy("Subsuming " ^ (ppterm status gty)));
1528   let n,h,metasenv,subst,obj = status#obj in
1529   let ctx = ctx_of gty in
1530   let _ , target = term_of_cic_term status gty ctx in
1531   let target = NCicSubstitution.lift 1 target in
1532   (* candidates must only be searched w.r.t the given context *)
1533   let candidates =
1534     try
1535     let idx = List.assq ctx cache in
1536       Ncic_termSet.elements
1537         (InvRelDiscriminationTree.retrieve_generalizations idx gty)
1538     with Not_found -> []
1539   in
1540   debug_print ~depth
1541     (lazy ("failure candidates: " ^ string_of_int (List.length candidates)));
1542     try
1543       List.iter
1544         (fun t ->
1545            let _ , source = term_of_cic_term status t ctx in
1546            let implication =
1547              NCic.Prod("foo",source,target) in
1548            let metasenv,j,_,_ =
1549              NCicMetaSubst.mk_meta
1550                metasenv ctx ~with_type:implication `IsType in
1551            let status = status#set_obj (n,h,metasenv,subst,obj) in
1552            let status = status#set_stack [([1,Open j],[],[],`NoTag)] in
1553            try
1554              let status = NTactics.intro_tac "foo" status in
1555              let status =
1556                NTactics.apply_tac ("",0,Ast.NCic (NCic.Rel 1)) status
1557              in
1558                if (head_goals status#stack = []) then raise Found
1559                else ()
1560            with
1561              | Error _ -> ())
1562         candidates;false
1563     with Found -> debug_print ~depth (lazy "success");true)
1564 ;;
1565
1566 let rec guess_name name ctx =
1567   if name = "_" then guess_name "auto" ctx else
1568   if not (List.mem_assoc name ctx) then name else
1569   guess_name (name^"'") ctx
1570 ;;
1571
1572 let is_prod status =
1573   let _, ctx, gty = current_goal status in
1574   let _, raw_gty = term_of_cic_term status gty ctx in
1575   match raw_gty with
1576     | NCic.Prod (name,_,_) -> Some (guess_name name ctx)
1577     | _ -> None
1578
1579 let intro ~depth status facts name =
1580   let status = NTactics.intro_tac name status in
1581   let _, ctx, ngty = current_goal status in
1582   let t = mk_cic_term ctx (NCic.Rel 1) in
1583   let status, keys = keys_of_term status t in
1584   let facts = List.fold_left (add_to_th t) facts keys in
1585     debug_print ~depth (lazy ("intro: "^ name));
1586   (* unprovability is not stable w.r.t introduction *)
1587   status, facts
1588 ;;
1589
1590 let rec intros_facts ~depth status facts =
1591   match is_prod status with
1592     | Some(name) ->
1593         let status,facts =
1594           intro ~depth status facts name
1595         in intros_facts ~depth status facts
1596     | _ -> status, facts
1597 ;;
1598
1599 let rec intros ~depth status (cache:cache) =
1600     match is_prod status with
1601       | Some _ ->
1602           let status,facts =
1603             intros_facts ~depth status cache.facts
1604           in
1605             (* we reindex the equation from scratch *)
1606           let unit_eq =
1607             index_local_equations status#eq_cache status in
1608             (* under_inspection must be set to empty *)
1609           status, init_cache ~facts ~unit_eq ()
1610       | _ -> status, cache
1611 ;;
1612
1613 let reduce ~depth status g =
1614   let n,h,metasenv,subst,o = status#obj in
1615   let attr, ctx, ty = NCicUtils.lookup_meta g metasenv in
1616   let ty = NCicUntrusted.apply_subst subst ctx ty in
1617   let ty' = NCicReduction.whd ~subst ctx ty in
1618   if ty = ty' then []
1619   else
1620     (debug_print ~depth
1621       (lazy ("reduced to: "^ NCicPp.ppterm ctx subst metasenv ty'));
1622     let metasenv =
1623       (g,(attr,ctx,ty'))::(List.filter (fun (i,_) -> i<>g) metasenv)
1624     in
1625     let status = status#set_obj (n,h,metasenv,subst,o) in
1626     incr candidate_no;
1627     [(!candidate_no,Ast.Ident("__whd",None)),status])
1628 ;;
1629
1630 let do_something signature flags status g depth gty cache =
1631   (* whd *)
1632   let l = reduce ~depth status g in
1633   (* backward aplications *)
1634   let l1 =
1635     List.map
1636       (fun s ->
1637          incr candidate_no;
1638          ((!candidate_no,Ast.Ident("__paramod",None)),s))
1639       (auto_eq_check cache.unit_eq status) in
1640   let l2 =
1641     if (l1 <> []) then []
1642     else applicative_case depth signature status flags gty cache
1643   (* fast paramodulation *)
1644   in
1645   (* states in l1 have have an empty set of subgoals: no point to sort them *)
1646     l1 @ (sort_new_elems (l@l2)), cache
1647 ;;
1648
1649 let pp_goal = function
1650   | (_,Continuationals.Stack.Open i)
1651   | (_,Continuationals.Stack.Closed i) -> string_of_int i
1652 ;;
1653
1654 let pp_goals status l =
1655   String.concat ", "
1656     (List.map
1657        (fun i ->
1658           let gty = get_goalty status i in
1659             NTacStatus.ppterm status gty)
1660        l)
1661 ;;
1662
1663 module M =
1664   struct
1665     type t = int
1666     let compare = Pervasives.compare
1667   end
1668 ;;
1669
1670 module MS = HTopoSort.Make(M)
1671 ;;
1672
1673 let sort_tac status =
1674   let gstatus =
1675     match status#stack with
1676     | [] -> assert false
1677     | (goals, t, k, tag) :: s ->
1678         let g = head_goals status#stack in
1679         let sortedg =
1680           (List.rev (MS.topological_sort g (deps status))) in
1681           debug_print (lazy ("old g = " ^
1682             String.concat "," (List.map string_of_int g)));
1683           debug_print (lazy ("sorted goals = " ^
1684             String.concat "," (List.map string_of_int sortedg)));
1685           let is_it i = function
1686             | (_,Continuationals.Stack.Open j )
1687             | (_,Continuationals.Stack.Closed j ) -> i = j
1688           in
1689           let sorted_goals =
1690             List.map (fun i -> List.find (is_it i) goals) sortedg
1691           in
1692             (sorted_goals, t, k, tag) :: s
1693   in
1694    status#set_stack gstatus
1695 ;;
1696
1697 let clean_up_tac status =
1698   let gstatus =
1699     match status#stack with
1700     | [] -> assert false
1701     | (g, t, k, tag) :: s ->
1702         let is_open = function
1703           | (_,Continuationals.Stack.Open _) -> true
1704           | (_,Continuationals.Stack.Closed _) -> false
1705         in
1706         let g' = List.filter is_open g in
1707           (g', t, k, tag) :: s
1708   in
1709    status#set_stack gstatus
1710 ;;
1711
1712 let focus_tac focus status =
1713   let gstatus =
1714     match status#stack with
1715     | [] -> assert false
1716     | (g, t, k, tag) :: s ->
1717         let in_focus = function
1718           | (_,Continuationals.Stack.Open i)
1719           | (_,Continuationals.Stack.Closed i) -> List.mem i focus
1720         in
1721         let focus,others = List.partition in_focus g
1722         in
1723           (* we need to mark it as a BranchTag, otherwise cannot merge later *)
1724           (focus,[],[],`BranchTag) :: (others, t, k, tag) :: s
1725   in
1726    status#set_stack gstatus
1727 ;;
1728
1729 let rec auto_clusters ?(top=false)
1730     flags signature cache depth status : unit =
1731   debug_print ~depth (lazy "entering auto clusters");
1732   (* ignore(Unix.select [] [] [] 0.01); *)
1733   let status = clean_up_tac status in
1734   let goals = head_goals status#stack in
1735   if goals = [] then raise (Proved status)
1736   else if depth = flags.maxdepth then raise (Gaveup IntSet.empty)
1737   else if List.length goals < 2 then
1738     auto_main flags signature cache depth status
1739   else
1740     debug_print ~depth (lazy ("goals = " ^
1741       String.concat "," (List.map string_of_int goals)));
1742     let classes = HExtlib.clusters (deps status) goals in
1743     let classes = if top then List.rev classes else classes in
1744       debug_print ~depth
1745         (lazy
1746            (String.concat "\n"
1747            (List.map
1748               (fun l ->
1749                  ("cluster:" ^ String.concat "," (List.map string_of_int l)))
1750            classes)));
1751       let status,b =
1752         List.fold_left
1753           (fun (status,b) gl ->
1754              let status = focus_tac gl status in
1755              try
1756                debug_print ~depth (lazy ("focusing on" ^
1757                               String.concat "," (List.map string_of_int gl)));
1758                auto_main flags signature cache depth status; assert false
1759              with
1760                | Proved(status) -> (NTactics.merge_tac status,true)
1761                | Gaveup _ when top -> (NTactics.merge_tac status,b)
1762           )
1763           (status,false) classes
1764       in if b then raise (Proved status) else raise (Gaveup IntSet.empty)
1765
1766 and
1767
1768 (* the goals returned upon failure are an unsatisfiable subset
1769    of the initial head goals in the stack *)
1770
1771 auto_main flags signature (cache:cache) depth status: unit =
1772   debug_print ~depth (lazy "entering auto main");
1773   (* ignore(Unix.select [] [] [] 0.01); *)
1774   let status = sort_tac (clean_up_tac status) in
1775   let goals = head_goals status#stack in
1776   match goals with
1777     | [] -> raise (Proved status)
1778     | orig::_ ->
1779         let ng = List.length goals in
1780         if ng > flags.maxwidth then
1781           (print (lazy "FAIL WIDTH"); raise (Gaveup IntSet.empty))
1782         else let branch = ng>1 in
1783         if depth = flags.maxdepth then raise (Gaveup IntSet.empty)
1784         else
1785         let status =
1786           if branch then NTactics.branch_tac status
1787           else status in
1788         let status, cache = intros ~depth status cache in
1789         let g,gctx, gty = current_goal status in
1790         let ctx,ty = close status g in
1791         let closegty = mk_cic_term ctx ty in
1792         let status, gty = apply_subst status gctx gty in
1793         debug_print ~depth (lazy("Attacking goal " ^ (string_of_int g) ^" : "^ppterm status gty));
1794         if is_subsumed depth status closegty cache.under_inspection then
1795           (debug_print (lazy "SUBSUMED");
1796            raise (Gaveup IntSet.add g IntSet.empty))
1797         else
1798         let alternatives, cache =
1799           do_something signature flags status g depth gty cache in
1800         let loop_cache =
1801           let under_inspection =
1802             add_to_th closegty cache.under_inspection closegty in
1803           {cache with under_inspection = under_inspection} in
1804         let unsat =
1805           List.fold_left
1806             (* the underscore information does not need to be returned
1807                by do_something *)
1808             (fun unsat ((_,t),status) ->
1809                let depth',looping_cache =
1810                  if t=Ast.Ident("__whd",None) then depth,cache
1811                  else depth+1, loop_cache in
1812                debug_print (~depth:depth')
1813                  (lazy ("Case: " ^ CicNotationPp.pp_term t));
1814                let flags' =
1815                  {flags with maxwidth = flags.maxwidth - ng +1} in
1816                try auto_clusters flags' signature loop_cache
1817                  depth' status; unsat
1818                with
1819                  | Proved status ->
1820                      debug_print (~depth:depth') (lazy "proved");
1821                      if branch then
1822                        let status = NTactics.merge_tac status
1823                        in
1824                          (* old cache, here *)
1825                          try auto_clusters flags signature cache
1826                            depth status; assert false
1827                          with Gaveup f ->
1828                            debug_print ~depth
1829                              (lazy ("Unsat1 at depth " ^ (string_of_int depth)
1830                                    ^ ": " ^
1831                                    (pp_goals status (IntSet.elements f))));
1832                         (* TODO: cache failures *)
1833                            IntSet.union f unsat
1834                      else raise (Proved status)
1835                  | Gaveup f ->
1836                      debug_print (~depth:depth')
1837                        (lazy ("Unsat2 at depth " ^ (string_of_int depth')
1838                               ^ ": " ^
1839                               (pp_goals status (IntSet.elements f))));
1840                      (* TODO: cache local failures *)
1841                      unsat)
1842             IntSet.empty alternatives
1843         in
1844           raise (Gaveup IntSet.add orig unsat)
1845 ;;
1846
1847 let int name l def =
1848   try int_of_string (List.assoc name l)
1849   with Failure _ | Not_found -> def
1850 ;;
1851
1852 let auto_tac ~params:(_univ,flags) status =
1853   let oldstatus = status in
1854   let status = (status:> NTacStatus.tac_status) in
1855   let goals = head_goals status#stack in
1856   let status, facts = mk_th_cache status goals in
1857   let unit_eq = index_local_equations status#eq_cache status in
1858   let cache = init_cache ~facts ~unit_eq  () in
1859 (*   pp_th status facts; *)
1860 (*
1861   NDiscriminationTree.DiscriminationTree.iter status#auto_cache (fun p t ->
1862     debug_print (lazy(
1863       NDiscriminationTree.NCicIndexable.string_of_path p ^ " |--> " ^
1864       String.concat "\n    " (List.map (
1865       NCicPp.ppterm ~metasenv:[] ~context:[] ~subst:[])
1866         (NDiscriminationTree.TermSet.elements t))
1867       )));
1868 *)
1869   let depth = int "depth" flags 3 in
1870   let size  = int "size" flags 10 in
1871   let width = int "width" flags 4 (* (3+List.length goals)*) in
1872   (* XXX fix sort *)
1873   let goals = List.map (fun i -> (i,P)) goals in
1874   let signature = () in
1875   let flags = {
1876           maxwidth = width;
1877           maxsize = size;
1878           maxdepth = depth;
1879           timeout = Unix.gettimeofday() +. 3000.;
1880           do_types = false;
1881   } in
1882   let initial_time = Unix.gettimeofday() in
1883   app_counter:= 0;
1884   let rec up_to x y =
1885     if x > y then
1886       (print(lazy
1887         ("TIME ELAPSED:"^string_of_float(Unix.gettimeofday()-.initial_time)));
1888        print(lazy
1889         ("Applicative nodes:"^string_of_int !app_counter));
1890        raise (Error (lazy "auto gave up", None)))
1891     else
1892       let _ = debug_print (lazy("\n\nRound "^string_of_int x^"\n")) in
1893       let flags = { flags with maxdepth = x }
1894       in
1895         try auto_clusters (~top:true) flags signature cache 0 status;assert false
1896         with
1897           | Gaveup _ -> up_to (x+1) y
1898           | Proved s ->
1899               print (lazy ("proved at depth " ^ string_of_int x));
1900               let stack =
1901                 match s#stack with
1902                   | (g,t,k,f) :: rest -> (filter_open g,t,k,f):: rest
1903                   | _ -> assert false
1904               in
1905               let s = s#set_stack stack in
1906                 oldstatus#set_status s
1907   in
1908   let s = up_to depth depth in
1909     print(lazy
1910         ("TIME ELAPSED:"^string_of_float(Unix.gettimeofday()-.initial_time)));
1911     print(lazy
1912         ("Applicative nodes:"^string_of_int !app_counter));
1913     s
1914 ;;
1915