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