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