helm/software/components/ng_tactics/nAuto.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 (* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
  13
  14 open Printf
  15
  16 let debug = ref false
  17 let debug_print s = if !debug then prerr_endline (Lazy.force s) else ()
  18
  19 open Continuationals.Stack
  20 open NTacStatus
  21 module Ast = CicNotationPt
  22
  23 (* =================================== paramod =========================== *)
  24 let auto_paramod ~params:(l,_) status goal =
  25   let gty = get_goalty status goal in
  26   let n,h,metasenv,subst,o = status#obj in
  27   let status,t = term_of_cic_term status gty (ctx_of gty) in
  28   let status, l =
  29     List.fold_left
  30       (fun (status, l) t ->
  31         let status, t = disambiguate status (ctx_of gty) t None in
  32         let status, ty = typeof status (ctx_of t) t in
  33         let status, t =  term_of_cic_term status t (ctx_of gty) in
  34         let status, ty = term_of_cic_term status ty (ctx_of ty) in
  35         (status, (t,ty) :: l))
  36       (status,[]) l
  37   in
  38   match
  39     NCicParamod.nparamod status metasenv subst (ctx_of gty) (NCic.Rel ~-1,t) l
  40   with
  41   | [] -> raise (Error (lazy "no proof found",None))
  42   | (pt, metasenv, subst)::_ ->
  43       let status = status#set_obj (n,h,metasenv,subst,o) in
  44       instantiate status goal (mk_cic_term (ctx_of gty) pt)
  45 ;;
  46
  47 let auto_paramod_tac ~params status =
  48   NTactics.distribute_tac (auto_paramod ~params) status
  49 ;;
  50
  51 (* =================================== auto =========================== *)
  52 (****************** AUTO ********************
  53
  54 let calculate_timeout flags =
  55     if flags.timeout = 0. then
  56       (debug_print (lazy "AUTO WITH NO TIMEOUT");
  57        {flags with timeout = infinity})
  58     else
  59       flags
  60 ;;
  61 let is_equational_case goalty flags =
  62   let ensure_equational t =
  63     if is_an_equational_goal t then true
  64     else false
  65   in
  66   (flags.use_paramod && is_an_equational_goal goalty) ||
  67   (flags.use_only_paramod && ensure_equational goalty)
  68 ;;
  69
  70 type menv = Cic.metasenv
  71 type subst = Cic.substitution
  72 type goal = ProofEngineTypes.goal * int * AutoTypes.sort
  73 let candidate_no = ref 0;;
  74 type candidate = int * Cic.term Lazy.t
  75 type cache = AutoCache.cache
  76
  77 type fail =
  78   (* the goal (mainly for depth) and key of the goal *)
  79   goal * AutoCache.cache_key
  80 type op =
  81   (* goal has to be proved *)
  82   | D of goal
  83   (* goal has to be cached as a success obtained using candidate as the first
  84    * step *)
  85   | S of goal * AutoCache.cache_key * candidate * int
  86 type elem =
  87   (* menv, subst, size, operations done (only S), operations to do, failures to cache if any op fails *)
  88   menv * subst * int * op list * op list * fail list
  89 type status =
  90   (* list of computations that may lead to the solution: all op list will
  91    * end with the same (S(g,_)) *)
  92   elem list
  93 type auto_result =
  94   (* menv, subst, alternatives, tables, cache *)
  95   | Proved of menv * subst * elem list * AutomationCache.tables * cache
  96   | Gaveup of AutomationCache.tables * cache
  97
  98
  99 (* the status exported to the external observer *)
 100 type auto_status =
 101   (* context, (goal,candidate) list, and_list, history *)
 102   Cic.context * (int * Cic.term * bool * int * (int * Cic.term Lazy.t) list) list *
 103   (int * Cic.term * int) list * Cic.term Lazy.t list
 104
 105 let d_prefix l =
 106   let rec aux acc = function
 107     | (D g)::tl -> aux (acc@[g]) tl
 108     | _ -> acc
 109   in
 110     aux [] l
 111 ;;
 112
 113 let calculate_goal_ty (goalno,_,_) s m =
 114   try
 115     let _,cc,goalty = CicUtil.lookup_meta goalno m in
 116     (* XXX applicare la subst al contesto? *)
 117     Some (cc, CicMetaSubst.apply_subst s goalty)
 118   with CicUtil.Meta_not_found i when i = goalno -> None
 119 ;;
 120
 121 let calculate_closed_goal_ty (goalno,_,_) s =
 122   try
 123     let cc,_,goalty = List.assoc goalno s in
 124     (* XXX applicare la subst al contesto? *)
 125     Some (cc, CicMetaSubst.apply_subst s goalty)
 126   with Not_found ->
 127     None
 128 ;;
 129
 130 let pp_status ctx status =
 131   if debug then
 132   let names = Utils.names_of_context ctx in
 133   let pp x =
 134     let x =
 135       ProofEngineReduction.replace
 136         ~equality:(fun a b -> match b with Cic.Meta _ -> true | _ -> false)
 137           ~what:[Cic.Rel 1] ~with_what:[Cic.Implicit None] ~where:x
 138     in
 139     CicPp.pp x names
 140   in
 141   let string_of_do m s (gi,_,_ as g) d =
 142     match calculate_goal_ty g s m with
 143     | Some (_,gty) -> Printf.sprintf "D(%d, %s, %d)" gi (pp gty) d
 144     | None -> Printf.sprintf "D(%d, _, %d)" gi d
 145   in
 146   let string_of_s m su k (ci,ct) gi =
 147     Printf.sprintf "S(%d, %s, %s, %d)" gi (pp k) (pp (Lazy.force ct)) ci
 148   in
 149   let string_of_ol m su l =
 150     String.concat " | "
 151       (List.map
 152         (function
 153           | D (g,d,s) -> string_of_do m su (g,d,s) d
 154           | S ((gi,_,_),k,c,_) -> string_of_s m su k c gi)
 155         l)
 156   in
 157   let string_of_fl m s fl =
 158     String.concat " | "
 159       (List.map (fun ((i,_,_),ty) ->
 160          Printf.sprintf "(%d, %s)" i (pp ty)) fl)
 161   in
 162   let rec aux = function
 163     | [] -> ()
 164     | (m,s,_,_,ol,fl)::tl ->
 165         Printf.eprintf "< [%s] ;;; [%s]>\n"
 166           (string_of_ol m s ol) (string_of_fl m s fl);
 167         aux tl
 168   in
 169     Printf.eprintf "-------------------------- status -------------------\n";
 170     aux status;
 171     Printf.eprintf "-----------------------------------------------------\n";
 172 ;;
 173
 174 let auto_status = ref [] ;;
 175 let auto_context = ref [];;
 176 let in_pause = ref false;;
 177 let pause b = in_pause := b;;
 178 let cond = Condition.create ();;
 179 let mutex = Mutex.create ();;
 180 let hint = ref None;;
 181 let prune_hint = ref [];;
 182
 183 let step _ = Condition.signal cond;;
 184 let give_hint n = hint := Some n;;
 185 let give_prune_hint hint =
 186   prune_hint := hint :: !prune_hint
 187 ;;
 188
 189 let check_pause _ =
 190   if !in_pause then
 191     begin
 192       Mutex.lock mutex;
 193       Condition.wait cond mutex;
 194       Mutex.unlock mutex
 195     end
 196 ;;
 197
 198 let get_auto_status _ =
 199   let status = !auto_status in
 200   let and_list,elems,last =
 201     match status with
 202     | [] -> [],[],[]
 203     | (m,s,_,don,gl,fail)::tl ->
 204         let and_list =
 205           HExtlib.filter_map
 206             (fun (id,d,_ as g) ->
 207               match calculate_goal_ty g s m with
 208               | Some (_,x) -> Some (id,x,d) | None -> None)
 209             (d_goals gl)
 210         in
 211         let rows =
 212           (* these are the S goalsin the or list *)
 213           let orlist =
 214             List.map
 215               (fun (m,s,_,don,gl,fail) ->
 216                 HExtlib.filter_map
 217                   (function S (g,k,c,_) -> Some (g,k,c) | _ -> None)
 218                   (List.rev don @ gl))
 219               status
 220           in
 221           (* this function eats id from a list l::[id,x] returning x, l *)
 222           let eat_tail_if_eq id l =
 223             let rec aux (s, l) = function
 224               | [] -> s, l
 225               | ((id1,_,_),k1,c)::tl when id = id1 ->
 226                   (match s with
 227                   | None -> aux (Some c,l) tl
 228                   | Some _ -> assert false)
 229               | ((id1,_,_),k1,c as e)::tl -> aux (s, e::l) tl
 230             in
 231             let c, l = aux (None, []) l in
 232             c, List.rev l
 233           in
 234           let eat_in_parallel id l =
 235             let rec aux (b,eaten, new_l as acc) l =
 236               match l with
 237               | [] -> acc
 238               | l::tl ->
 239                   match eat_tail_if_eq id l with
 240                   | None, l -> aux (b@[false], eaten, new_l@[l]) tl
 241                   | Some t,l -> aux (b@[true],eaten@[t], new_l@[l]) tl
 242             in
 243             aux ([],[],[]) l
 244           in
 245           let rec eat_all rows l =
 246             match l with
 247             | [] -> rows
 248             | elem::or_list ->
 249                 match List.rev elem with
 250                 | ((to_eat,depth,_),k,_)::next_lunch ->
 251                     let b, eaten, l = eat_in_parallel to_eat l in
 252                     let eaten = HExtlib.list_uniq eaten in
 253                     let eaten = List.rev eaten in
 254                     let b = true (* List.hd (List.rev b) *) in
 255                     let rows = rows @ [to_eat,k,b,depth,eaten] in
 256                     eat_all rows l
 257                 | [] -> eat_all rows or_list
 258           in
 259           eat_all [] (List.rev orlist)
 260         in
 261         let history =
 262           HExtlib.filter_map
 263             (function (S (_,_,(_,c),_)) -> Some c | _ -> None)
 264             gl
 265         in
 266 (*         let rows = List.filter (fun (_,l) -> l <> []) rows in *)
 267         and_list, rows, history
 268   in
 269   !auto_context, elems, and_list, last
 270 ;;
 271
 272 (* Works if there is no dependency over proofs *)
 273 let is_a_green_cut goalty =
 274   CicUtil.is_meta_closed goalty
 275 ;;
 276 let rec first_s = function
 277   | (D _)::tl -> first_s tl
 278   | (S (g,k,c,s))::tl -> Some ((g,k,c,s),tl)
 279   | [] -> None
 280 ;;
 281 let list_union l1 l2 =
 282   (* TODO ottimizzare compare *)
 283   HExtlib.list_uniq (List.sort compare (l1 @ l1))
 284 ;;
 285 let rec eq_todo l1 l2 =
 286   match l1,l2 with
 287   | (D g1) :: tl1,(D g2) :: tl2 when g1=g2 -> eq_todo tl1 tl2
 288   | (S (g1,k1,(c1,lt1),i1)) :: tl1, (S (g2,k2,(c2,lt2),i2)) :: tl2
 289     when i1 = i2 && g1 = g2 && k1 = k2 && c1 = c2 ->
 290       if Lazy.force lt1 = Lazy.force lt2 then eq_todo tl1 tl2 else false
 291   | [],[] -> true
 292   | _ -> false
 293 ;;
 294 let eat_head todo id fl orlist =
 295   let rec aux acc = function
 296   | [] -> [], acc
 297   | (m, s, _, _, todo1, fl1)::tl as orlist ->
 298       let rec aux1 todo1 =
 299         match first_s todo1 with
 300         | None -> orlist, acc
 301         | Some (((gno,_,_),_,_,_), todo11) ->
 302             (* TODO confronto tra todo da ottimizzare *)
 303             if gno = id && eq_todo todo11 todo then
 304               aux (list_union fl1 acc) tl
 305             else
 306               aux1 todo11
 307       in
 308        aux1 todo1
 309   in
 310     aux fl orlist
 311 ;;
 312 let close_proof p ty menv context =
 313   let metas =
 314     List.map fst (CicUtil.metas_of_term p @ CicUtil.metas_of_term ty)
 315   in
 316   let menv = List.filter (fun (i,_,_) -> List.exists ((=)i) metas) menv in
 317   naif_closure p menv context
 318 ;;
 319 (* XXX capire bene quando aggiungere alla cache *)
 320 let add_to_cache_and_del_from_orlist_if_green_cut
 321   g s m cache key todo orlist fl ctx size minsize
 322 =
 323   let cache = cache_remove_underinspection cache key in
 324   (* prima per fare la irl usavamo il contesto vero e proprio e non quello
 325    * canonico! XXX *)
 326   match calculate_closed_goal_ty g s with
 327   | None -> assert false
 328   | Some (canonical_ctx , gty) ->
 329       let goalno,depth,sort = g in
 330       let irl = mk_irl canonical_ctx in
 331       let goal = Cic.Meta(goalno, irl) in
 332       let proof = CicMetaSubst.apply_subst s goal in
 333       let green_proof, closed_proof =
 334         let b = is_a_green_cut proof in
 335         if not b then
 336           b, (* close_proof proof gty m ctx *) proof
 337         else
 338           b, proof
 339       in
 340       debug_print (lazy ("TENTATIVE CACHE: " ^ CicPp.ppterm key));
 341       if is_a_green_cut key then
 342         (* if the initia goal was closed, we cut alternatives *)
 343         let _ = debug_print (lazy ("MANGIO: " ^ string_of_int goalno)) in
 344         let orlist, fl = eat_head todo goalno fl orlist in
 345         let cache =
 346           if size < minsize then
 347             (debug_print (lazy ("NO CACHE: 2 (size <= minsize)"));cache)
 348           else
 349           (* if the proof is closed we cache it *)
 350           if green_proof then cache_add_success cache key proof
 351           else (* cache_add_success cache key closed_proof *)
 352             (debug_print (lazy ("NO CACHE: (no gree proof)"));cache)
 353         in
 354         cache, orlist, fl, true
 355       else
 356         let cache =
 357           debug_print (lazy ("TENTATIVE CACHE: " ^ CicPp.ppterm gty));
 358           if size < minsize then
 359             (debug_print (lazy ("NO CACHE: (size <= minsize)")); cache) else
 360           (* if the substituted goal and the proof are closed we cache it *)
 361           if is_a_green_cut gty then
 362             if green_proof then cache_add_success cache gty proof
 363             else (* cache_add_success cache gty closed_proof *)
 364               (debug_print (lazy ("NO CACHE: (no green proof (gty))"));cache)
 365           else (*
 366             try
 367               let ty, _ =
 368                 CicTypeChecker.type_of_aux' ~subst:s
 369                   m ctx closed_proof CicUniv.oblivion_ugraph
 370               in
 371               if is_a_green_cut ty then
 372                 cache_add_success cache ty closed_proof
 373               else cache
 374             with
 375             | CicTypeChecker.TypeCheckerFailure _ ->*)
 376           (debug_print (lazy ("NO CACHE: (no green gty )"));cache)
 377         in
 378         cache, orlist, fl, false
 379 ;;
 380 let close_failures (fl : fail list) (cache : cache) =
 381   List.fold_left
 382     (fun cache ((gno,depth,_),gty) ->
 383       if CicUtil.is_meta_closed gty then
 384        ( debug_print (lazy ("FAIL: INDUCED: " ^ string_of_int gno));
 385          cache_add_failure cache gty depth)
 386       else
 387          cache)
 388     cache fl
 389 ;;
 390 let put_in_subst subst metasenv  (goalno,_,_) canonical_ctx t ty =
 391   let entry = goalno, (canonical_ctx, t,ty) in
 392   assert_subst_are_disjoint subst [entry];
 393   let subst = entry :: subst in
 394
 395   let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
 396
 397   subst, metasenv
 398 ;;
 399
 400 let mk_fake_proof metasenv subst (goalno,_,_) goalty context =
 401   None,metasenv,subst ,(lazy (Cic.Meta(goalno,mk_irl context))),goalty, []
 402 ;;
 403
 404 let equational_case
 405   tables cache depth fake_proof goalno goalty subst context
 406     flags
 407 =
 408   let active,passive,bag = tables in
 409   let ppterm = ppterm context in
 410   let status = (fake_proof,goalno) in
 411     if flags.use_only_paramod then
 412       begin
 413         debug_print (lazy ("PARAMODULATION SU: " ^
 414                          string_of_int goalno ^ " " ^ ppterm goalty ));
 415         let goal_steps, saturation_steps, timeout =
 416           max_int,max_int,flags.timeout
 417         in
 418         match
 419           Saturation.given_clause bag status active passive
 420             goal_steps saturation_steps timeout
 421         with
 422           | None, active, passive, bag ->
 423               [], (active,passive,bag), cache, flags
 424           | Some(subst',(_,metasenv,_subst,proof,_, _),open_goals),active,
 425             passive,bag ->
 426               assert_subst_are_disjoint subst subst';
 427               let subst = subst@subst' in
 428               let open_goals =
 429                 order_new_goals metasenv subst open_goals ppterm
 430               in
 431               let open_goals =
 432                 List.map (fun (x,sort) -> x,depth-1,sort) open_goals
 433               in
 434               incr candidate_no;
 435               [(!candidate_no,proof),metasenv,subst,open_goals],
 436                 (active,passive,bag), cache, flags
 437       end
 438     else
 439       begin
 440         debug_print (lazy ("NARROWING DEL GOAL: " ^
 441                          string_of_int goalno ^ " " ^ ppterm goalty ));
 442         let goal_steps, saturation_steps, timeout =
 443           1,0,flags.timeout
 444         in
 445         match
 446           Saturation.solve_narrowing bag status active passive goal_steps
 447         with
 448           | None, active, passive, bag ->
 449               [], (active,passive,bag), cache, flags
 450           | Some(subst',(_,metasenv,_subst,proof,_, _),open_goals),active,
 451             passive,bag ->
 452               assert_subst_are_disjoint subst subst';
 453               let subst = subst@subst' in
 454               let open_goals =
 455                 order_new_goals metasenv subst open_goals ppterm
 456               in
 457               let open_goals =
 458                 List.map (fun (x,sort) -> x,depth-1,sort) open_goals
 459               in
 460               incr candidate_no;
 461               [(!candidate_no,proof),metasenv,subst,open_goals],
 462                 (active,passive,bag), cache, flags
 463       end
 464 (*
 465       begin
 466         let params = ([],["use_context","false"]) in
 467         let automation_cache = {
 468               AutomationCache.tables = tables ;
 469               AutomationCache.univ = Universe.empty; }
 470         in
 471         try
 472           let ((_,metasenv,subst,_,_,_),open_goals) =
 473
 474             solve_rewrite ~params ~automation_cache
 475               (fake_proof, goalno)
 476           in
 477           let proof = lazy (Cic.Meta (-1,[])) in
 478           [(!candidate_no,proof),metasenv,subst,[]],tables, cache, flags
 479         with ProofEngineTypes.Fail _ -> [], tables, cache, flags
 480 (*
 481         let res = Saturation.all_subsumed bag status active passive in
 482         let res' =
 483           List.map
 484             (fun (subst',(_,metasenv,_subst,proof,_, _),open_goals) ->
 485                assert_subst_are_disjoint subst subst';
 486                let subst = subst@subst' in
 487                let open_goals =
 488                  order_new_goals metasenv subst open_goals ppterm
 489                in
 490                let open_goals =
 491                  List.map (fun (x,sort) -> x,depth-1,sort) open_goals
 492                in
 493                incr candidate_no;
 494                  (!candidate_no,proof),metasenv,subst,open_goals)
 495             res
 496           in
 497           res', (active,passive,bag), cache, flags
 498 *)
 499       end
 500 *)
 501 ;;
 502
 503 let sort_new_elems =
 504  List.sort (fun (_,_,_,l1) (_,_,_,l2) ->
 505          let p1 = List.length (prop_only l1) in
 506          let p2 = List.length (prop_only l2) in
 507          if p1 = p2 then List.length l1 - List.length l2 else p1-p2)
 508 ;;
 509
 510
 511 let try_candidate dbd
 512   goalty tables subst fake_proof goalno depth context cand
 513 =
 514   let ppterm = ppterm context in
 515   try
 516     let actives, passives, bag = tables in
 517     let (_,metasenv,subst,_,_,_), open_goals =
 518        ProofEngineTypes.apply_tactic
 519         (PrimitiveTactics.apply_tac ~term:cand)
 520         (fake_proof,goalno)
 521     in
 522     let tables = actives, passives,
 523       Equality.push_maxmeta bag
 524         (max (Equality.maxmeta bag) (CicMkImplicit.new_meta metasenv subst))
 525     in
 526     debug_print (lazy ("   OK: " ^ ppterm cand));
 527     let metasenv = CicRefine.pack_coercion_metasenv metasenv in
 528     let open_goals = order_new_goals metasenv subst open_goals ppterm in
 529     let open_goals = List.map (fun (x,sort) -> x,depth-1,sort) open_goals in
 530     incr candidate_no;
 531     Some ((!candidate_no,lazy cand),metasenv,subst,open_goals), tables
 532   with
 533     | ProofEngineTypes.Fail s -> None,tables
 534     | CicUnification.Uncertain s ->  None,tables
 535 ;;
 536
 537 let applicative_case dbd
 538   tables depth subst fake_proof goalno goalty metasenv context
 539   signature universe cache flags
 540 =
 541   (* let goalty_aux =
 542     match goalty with
 543     | Cic.Appl (hd::tl) ->
 544         Cic.Appl (hd :: HExtlib.mk_list (Cic.Meta (0,[])) (List.length tl))
 545     | _ -> goalty
 546   in *)
 547   let goalty_aux = goalty in
 548   let candidates =
 549     get_candidates flags.skip_trie_filtering universe cache goalty_aux
 550   in
 551   (* if the goal is an equality we skip the congruence theorems
 552   let candidates =
 553     if is_equational_case goalty flags
 554     then List.filter not_default_eq_term candidates
 555     else candidates
 556   in *)
 557   let candidates = List.filter (only signature context metasenv) candidates
 558   in
 559   let tables, elems =
 560     List.fold_left
 561       (fun (tables,elems) cand ->
 562         match
 563           try_candidate dbd goalty
 564             tables subst fake_proof goalno depth context cand
 565         with
 566         | None, tables -> tables, elems
 567         | Some x, tables -> tables, x::elems)
 568       (tables,[]) candidates
 569   in
 570   let elems = sort_new_elems elems in
 571   elems, tables, cache
 572 ;;
 573
 574 let try_smart_candidate dbd
 575   goalty tables subst fake_proof goalno depth context cand
 576 =
 577   let ppterm = ppterm context in
 578   try
 579     let params = ([],[]) in
 580     let automation_cache = {
 581           AutomationCache.tables = tables ;
 582           AutomationCache.univ = Universe.empty; }
 583     in
 584     debug_print (lazy ("candidato per " ^ string_of_int goalno
 585       ^ ": " ^ CicPp.ppterm cand));
 586 (*
 587     let (_,metasenv,subst,_,_,_) = fake_proof in
 588     prerr_endline ("metasenv:\n" ^ CicMetaSubst.ppmetasenv [] metasenv);
 589     prerr_endline ("subst:\n" ^ CicMetaSubst.ppsubst ~metasenv subst);
 590 *)
 591     let ((_,metasenv,subst,_,_,_),open_goals) =
 592       apply_smart ~dbd ~term:cand ~params ~automation_cache
 593         (fake_proof, goalno)
 594     in
 595     let metasenv = CicRefine.pack_coercion_metasenv metasenv in
 596     let open_goals = order_new_goals metasenv subst open_goals ppterm in
 597     let open_goals = List.map (fun (x,sort) -> x,depth-1,sort) open_goals in
 598     incr candidate_no;
 599     Some ((!candidate_no,lazy cand),metasenv,subst,open_goals), tables
 600   with
 601   | ProofEngineTypes.Fail s -> None,tables
 602   | CicUnification.Uncertain s ->  None,tables
 603 ;;
 604
 605 let smart_applicative_case dbd
 606   tables depth subst fake_proof goalno goalty metasenv context signature
 607   universe cache flags
 608 =
 609   let goalty_aux =
 610     match goalty with
 611     | Cic.Appl (hd::tl) ->
 612         Cic.Appl (hd :: HExtlib.mk_list (Cic.Meta (0,[])) (List.length tl))
 613     | _ -> goalty
 614   in
 615   let smart_candidates =
 616     get_candidates flags.skip_trie_filtering universe cache goalty_aux
 617   in
 618   let candidates =
 619     get_candidates flags.skip_trie_filtering universe cache goalty
 620   in
 621   let smart_candidates =
 622     List.filter
 623       (fun x -> not(List.mem x candidates)) smart_candidates
 624   in
 625   let debug_msg =
 626     (lazy ("smart_candidates" ^ " = " ^
 627              (String.concat "\n" (List.map CicPp.ppterm smart_candidates)))) in
 628   debug_print debug_msg;
 629   let candidates = List.filter (only signature context metasenv) candidates in
 630   let smart_candidates =
 631     List.filter (only signature context metasenv) smart_candidates
 632   in
 633 (*
 634   let penalty cand depth =
 635     if only signature context metasenv cand then depth else ((prerr_endline (
 636     "penalizzo " ^ CicPp.ppterm cand));depth -1)
 637   in
 638 *)
 639   let tables, elems =
 640     List.fold_left
 641       (fun (tables,elems) cand ->
 642         match
 643           try_candidate dbd goalty
 644             tables subst fake_proof goalno depth context cand
 645         with
 646         | None, tables ->
 647             (* if normal application fails we try to be smart *)
 648             (match try_smart_candidate dbd goalty
 649                tables subst fake_proof goalno depth context cand
 650              with
 651                | None, tables -> tables, elems
 652                | Some x, tables -> tables, x::elems)
 653         | Some x, tables -> tables, x::elems)
 654       (tables,[]) candidates
 655   in
 656   let tables, smart_elems =
 657       List.fold_left
 658         (fun (tables,elems) cand ->
 659           match
 660             try_smart_candidate dbd goalty
 661               tables subst fake_proof goalno depth context cand
 662           with
 663           | None, tables -> tables, elems
 664           | Some x, tables -> tables, x::elems)
 665         (tables,[]) smart_candidates
 666   in
 667   let elems = sort_new_elems (elems @ smart_elems) in
 668   elems, tables, cache
 669 ;;
 670
 671 let equational_and_applicative_case dbd
 672   signature universe flags m s g gty tables cache context
 673 =
 674   let goalno, depth, sort = g in
 675   let fake_proof = mk_fake_proof m s g gty context in
 676   if is_equational_case gty flags then
 677     let elems,tables,cache, flags =
 678       equational_case tables cache
 679         depth fake_proof goalno gty s context flags
 680     in
 681     let more_elems, tables, cache =
 682       if flags.use_only_paramod then
 683         [],tables, cache
 684       else
 685         applicative_case dbd
 686           tables depth s fake_proof goalno
 687             gty m context signature universe cache flags
 688     in
 689       elems@more_elems, tables, cache, flags
 690   else
 691     let elems, tables, cache =
 692       match LibraryObjects.eq_URI () with
 693       | Some _ ->
 694          smart_applicative_case dbd tables depth s fake_proof goalno
 695            gty m context signature universe cache flags
 696       | None ->
 697          applicative_case dbd tables depth s fake_proof goalno
 698            gty m context signature universe cache flags
 699     in
 700       elems, tables, cache, flags
 701 ;;
 702 let rec condition_for_hint i = function
 703   | [] -> false
 704   | S (_,_,(j,_),_):: tl -> j <> i (* && condition_for_hint i tl *)
 705   | _::tl -> condition_for_hint i tl
 706 ;;
 707 let prunable_for_size flags s m todo =
 708   let rec aux b = function
 709     | (S _)::tl -> aux b tl
 710     | (D (_,_,T))::tl -> aux b tl
 711     | (D g)::tl ->
 712         (match calculate_goal_ty g s m with
 713           | None -> aux b tl
 714           | Some (canonical_ctx, gty) ->
 715             let gsize, _ =
 716               Utils.weight_of_term
 717                 ~consider_metas:false ~count_metas_occurrences:true gty in
 718             let newb = b || gsize > flags.maxgoalsizefactor in
 719             aux newb tl)
 720     | [] -> b
 721   in
 722     aux false todo
 723
 724 (*
 725 let prunable ty todo =
 726   let rec aux b = function
 727     | (S(_,k,_,_))::tl -> aux (b || Equality.meta_convertibility k ty) tl
 728     | (D (_,_,T))::tl -> aux b tl
 729     | D _::_ -> false
 730     | [] -> b
 731   in
 732     aux false todo
 733 ;;
 734 *)
 735
 736 let prunable menv subst ty todo =
 737   let rec aux = function
 738     | (S(_,k,_,_))::tl ->
 739          (match Equality.meta_convertibility_subst k ty menv with
 740           | None -> aux tl
 741           | Some variant ->
 742                no_progress variant tl (* || aux tl*))
 743     | (D (_,_,T))::tl -> aux tl
 744     | _ -> false
 745   and no_progress variant = function
 746     | [] -> (*prerr_endline "++++++++++++++++++++++++ no_progress";*) true
 747     | D ((n,_,P) as g)::tl ->
 748         (match calculate_goal_ty g subst menv with
 749            | None -> no_progress variant tl
 750            | Some (_, gty) ->
 751                (match calculate_goal_ty g variant menv with
 752                   | None -> assert false
 753                   | Some (_, gty') ->
 754                       if gty = gty' then no_progress variant tl
 755 (*
 756 (prerr_endline (string_of_int n);
 757  prerr_endline (CicPp.ppterm gty);
 758  prerr_endline (CicPp.ppterm gty');
 759  prerr_endline "---------- subst";
 760  prerr_endline (CicMetaSubst.ppsubst ~metasenv:menv subst);
 761  prerr_endline "---------- variant";
 762  prerr_endline (CicMetaSubst.ppsubst ~metasenv:menv variant);
 763  prerr_endline "---------- menv";
 764  prerr_endline (CicMetaSubst.ppmetasenv [] menv);
 765                          no_progress variant tl) *)
 766                       else false))
 767     | _::tl -> no_progress variant tl
 768   in
 769     aux todo
 770
 771 ;;
 772 let condition_for_prune_hint prune (m, s, size, don, todo, fl) =
 773   let s =
 774     HExtlib.filter_map (function S (_,_,(c,_),_) -> Some c | _ -> None) todo
 775   in
 776   List.for_all (fun i -> List.for_all (fun j -> i<>j) prune) s
 777 ;;
 778 let filter_prune_hint c l =
 779   let prune = !prune_hint in
 780   prune_hint := []; (* possible race... *)
 781   if prune = [] then c,l
 782   else
 783     cache_reset_underinspection c,
 784     List.filter (condition_for_prune_hint prune) l
 785 ;;
 786
 787
 788
 789 let
 790   auto_all_solutions dbd tables universe cache context metasenv gl flags
 791 =
 792   let signature =
 793     List.fold_left
 794       (fun set g ->
 795          MetadataConstraints.UriManagerSet.union set
 796              (MetadataQuery.signature_of metasenv g)
 797        )
 798       MetadataConstraints.UriManagerSet.empty gl
 799   in
 800   let goals = order_new_goals metasenv [] gl CicPp.ppterm in
 801   let goals =
 802     List.map
 803       (fun (x,s) -> D (x,flags.maxdepth,s)) goals
 804   in
 805   let elems = [metasenv,[],1,[],goals,[]] in
 806   let rec aux tables solutions cache elems flags =
 807     match auto_main dbd tables context flags signature universe cache elems with
 808     | Gaveup (tables,cache) ->
 809         solutions,cache, tables
 810     | Proved (metasenv,subst,others,tables,cache) ->
 811         if Unix.gettimeofday () > flags.timeout then
 812           ((subst,metasenv)::solutions), cache, tables
 813         else
 814           aux tables ((subst,metasenv)::solutions) cache others flags
 815   in
 816   let rc = aux tables [] cache elems flags in
 817     match rc with
 818     | [],cache,tables -> [],cache,tables
 819     | solutions, cache,tables ->
 820         let solutions =
 821           HExtlib.filter_map
 822             (fun (subst,newmetasenv) ->
 823               let opened =
 824                 ProofEngineHelpers.compare_metasenvs ~oldmetasenv:metasenv ~newmetasenv
 825               in
 826               if opened = [] then Some subst else None)
 827             solutions
 828         in
 829          solutions,cache,tables
 830 ;;
 831
 832 (******************* AUTO ***************)
 833
 834
 835 let auto dbd flags metasenv tables universe cache context metasenv gl =
 836   let initial_time = Unix.gettimeofday() in
 837   let signature =
 838     List.fold_left
 839       (fun set g ->
 840          MetadataConstraints.UriManagerSet.union set
 841              (MetadataQuery.signature_of metasenv g)
 842        )
 843       MetadataConstraints.UriManagerSet.empty gl
 844   in
 845   let goals = order_new_goals metasenv [] gl CicPp.ppterm in
 846   let goals = List.map (fun (x,s) -> D(x,flags.maxdepth,s)) goals in
 847   let elems = [metasenv,[],1,[],goals,[]] in
 848   match auto_main dbd tables context flags signature universe cache elems with
 849   | Proved (metasenv,subst,_, tables,cache) ->
 850       debug_print(lazy
 851         ("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time)));
 852       Some (subst,metasenv), cache
 853   | Gaveup (tables,cache) ->
 854       debug_print(lazy
 855         ("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time)));
 856       None,cache
 857 ;;
 858
 859 let auto_tac ~(dbd:HSql.dbd) ~params:(univ,params) ~automation_cache (proof, goal) =
 860   let flags = flags_of_params params () in
 861   let use_library = flags.use_library in
 862   let universe, tables, cache =
 863     init_cache_and_tables
 864      ~dbd ~use_library ~use_context:(not flags.skip_context)
 865      automation_cache univ (proof, goal)
 866   in
 867   let _,metasenv,subst,_,_, _ = proof in
 868   let _,context,goalty = CicUtil.lookup_meta goal metasenv in
 869   let signature = MetadataQuery.signature_of metasenv goal in
 870   let signature =
 871     List.fold_left
 872       (fun set t ->
 873          let ty, _ =
 874            CicTypeChecker.type_of_aux' metasenv context t
 875              CicUniv.oblivion_ugraph
 876          in
 877          MetadataConstraints.UriManagerSet.union set
 878            (MetadataConstraints.constants_of ty)
 879        )
 880       signature univ
 881   in
 882   let tables,cache =
 883     if flags.close_more then
 884       close_more
 885         tables context (proof, goal)
 886           (auto_all_solutions dbd) signature universe cache
 887     else tables,cache in
 888   let initial_time = Unix.gettimeofday() in
 889   let (_,oldmetasenv,_,_,_, _) = proof in
 890     hint := None;
 891   let elem =
 892     metasenv,subst,1,[],[D (goal,flags.maxdepth,P)],[]
 893   in
 894   match auto_main dbd tables context flags signature universe cache [elem] with
 895     | Proved (metasenv,subst,_, tables,cache) ->
 896         debug_print (lazy
 897           ("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time)));
 898         let proof,metasenv =
 899         ProofEngineHelpers.subst_meta_and_metasenv_in_proof
 900           proof goal subst metasenv
 901         in
 902         let opened =
 903           ProofEngineHelpers.compare_metasenvs ~oldmetasenv
 904             ~newmetasenv:metasenv
 905         in
 906           proof,opened
 907     | Gaveup (tables,cache) ->
 908         debug_print
 909           (lazy ("TIME:"^
 910             string_of_float(Unix.gettimeofday()-.initial_time)));
 911         raise (ProofEngineTypes.Fail (lazy "Auto gave up"))
 912 ;;
 913 *)
 914
 915
 916 type th_cache = (NCic.context * InvRelDiscriminationTree.t) list
 917
 918 let mk_th_cache status gl =
 919   List.fold_left
 920     (fun (status, acc) g ->
 921        let gty = get_goalty status g in
 922        let ctx = ctx_of gty in
 923        if List.mem_assq ctx acc then status, acc else
 924          let idx = InvRelDiscriminationTree.empty in
 925          let status,_,idx =
 926            List.fold_left (fun (status, i, idx) _ ->
 927               let t = mk_cic_term ctx (NCic.Rel i) in
 928               let status, orig_ty = typeof status ctx t in
 929               let _, ty, _ = saturate ~delta:max_int status orig_ty in
 930               let idx = InvRelDiscriminationTree.index idx ty t in
 931               let idx =
 932                 let _, ty = term_of_cic_term status ty (ctx_of ty) in
 933                 match ty with
 934                 | NCic.Const (NReference.Ref (_,NReference.Def h))
 935                 | NCic.Appl (NCic.Const(NReference.Ref(_,NReference.Def h))::_)
 936                    when h > 0 ->
 937                      let _,ty,_= saturate status ~delta:(h-1) orig_ty in
 938                      InvRelDiscriminationTree.index idx ty t
 939                 | _ -> idx
 940               in
 941               status, i+1, idx)
 942              (status, 1, idx) ctx
 943           in
 944          status, (ctx, idx) :: acc)
 945     (status,[]) gl
 946 ;;
 947
 948 let add_to_th t ty c =
 949   let key_c = ctx_of t in
 950   if not (List.mem_assq key_c c) then
 951       (key_c ,InvRelDiscriminationTree.index
 952                InvRelDiscriminationTree.empty ty t ) :: c
 953   else
 954     let rec replace = function
 955       | [] -> []
 956       | (x, idx) :: tl when x == key_c ->
 957           (x, InvRelDiscriminationTree.index idx ty t) :: tl
 958       | x :: tl -> x :: replace tl
 959     in
 960       replace c
 961 ;;
 962
 963 let search_in_th gty th =
 964   let c = ctx_of gty in
 965   let rec aux acc = function
 966    | [] -> Ncic_termSet.elements acc
 967    | (_::tl) as k ->
 968        try
 969          let idx = List.assq k th in
 970          let acc = Ncic_termSet.union acc
 971            (InvRelDiscriminationTree.retrieve_unifiables idx gty)
 972          in
 973          aux acc tl
 974        with Not_found -> aux acc tl
 975   in
 976     aux Ncic_termSet.empty c
 977 ;;
 978
 979 let pp_th status =
 980   List.iter
 981     (fun ctx, idx ->
 982        prerr_endline "-----------------------------------------------";
 983        prerr_endline (NCicPp.ppcontext ~metasenv:[] ~subst:[] ctx);
 984        prerr_endline "||====>  ";
 985        InvRelDiscriminationTree.iter idx
 986           (fun k set ->
 987              prerr_endline ("K: " ^ NCicInverseRelIndexable.string_of_path k);
 988              Ncic_termSet.iter
 989              (fun t -> prerr_endline ("\t"^ppterm status t)) set))
 990 ;;
 991
 992 type cache_examination_result =
 993   [ `Failed_in of int
 994   | `UnderInspection
 995   | `Succeded of NCic.term
 996   | `NotFound
 997   ]
 998
 999 type sort = T | P
1000 type goal = int * int * sort (* goal, depth, sort *)
1001 type fail = goal * cic_term
1002 type candidate = int * Ast.term (* unique candidate number, candidate *)
1003
1004 type op =
1005   (* goal has to be proved *)
1006   | D of goal
1007   (* goal has to be cached as a success obtained using candidate as the first
1008    * step *)
1009   | S of goal * cic_term * candidate (* int was minsize *)
1010 type 'a elem =
1011   (* menv, subst, size, operations done (only S), operations to do,
1012    * failures to cache if any op fails *)
1013   (#tac_status as 'a) * int * op list * op list * fail list
1014
1015 type 'a auto_status =
1016   (* list of computations that may lead to the solution: all op list will
1017    * end with the same (S(g,_)) *)
1018   'a elem list * th_cache
1019
1020 type 'a auto_result =
1021   | Gaveup
1022   | Proved of (#tac_status as 'a) * 'a auto_status (* alt. proofs *)
1023
1024 type flags = {
1025         do_types : bool; (* solve goals in Type *)
1026         maxwidth : int;
1027         maxsize  : int;
1028         timeout  : float;
1029 }
1030
1031 let close_failures _ c = c;;
1032 let prunable _ _ _ = false;;
1033 let cache_examine cache gty = `Notfound;;
1034 let put_in_subst s _ _ _  = s;;
1035 let add_to_cache_and_del_from_orlist_if_green_cut _ _ c _ _ o f _ = c, o, f, false ;;
1036 let cache_add_underinspection c _ _ = c;;
1037 let equational_case _ _ _ _ _ _ = [];;
1038 let only _ _ _ = true;;
1039
1040 let candidate_no = ref 0;;
1041
1042 let sort_new_elems l =
1043   List.sort (fun (_,_,l1) (_,_,l2) -> List.length l1 - List.length l2) l
1044 ;;
1045
1046 let try_candidate status t g =
1047  try
1048    debug_print (lazy (" try " ^ CicNotationPp.pp_term t));
1049    let status = NTactics.focus_tac [g] status in
1050    let status = NTactics.apply_tac ("",0,t) status in
1051    let open_goals = head_goals status#stack in
1052    debug_print
1053      (lazy (" success: "^String.concat " "(List.map string_of_int open_goals)));
1054    incr candidate_no;
1055    Some ((!candidate_no,t),status,open_goals)
1056  with Error (msg,exn) -> debug_print (lazy " failed"); None
1057 ;;
1058
1059 let rec mk_irl n = function
1060   | [] -> []
1061   | _ :: tl -> NCic.Rel n :: mk_irl (n+1) tl
1062 ;;
1063
1064 let get_candidates status cache_th signature gty =
1065   let universe = status#auto_cache in
1066   let context = ctx_of gty in
1067   let _, raw_gty = term_of_cic_term status gty context in
1068   let cands =
1069     NDiscriminationTree.DiscriminationTree.retrieve_unifiables universe raw_gty
1070   in
1071   let cands =
1072     List.filter (only signature context)
1073       (NDiscriminationTree.TermSet.elements cands)
1074   in
1075   List.map (fun t ->
1076      let _status, t = term_of_cic_term status t context in Ast.NCic t)
1077      (search_in_th gty cache_th)
1078   @
1079   List.map (function NCic.Const r -> Ast.NRef r | _ -> assert false) cands
1080 ;;
1081
1082 let applicative_case signature status flags g gty cache =
1083   let candidates = get_candidates status cache signature gty in
1084   debug_print (lazy ("candidates: " ^ string_of_int (List.length candidates)));
1085   let elems =
1086     List.fold_left
1087       (fun elems cand ->
1088         match try_candidate status cand g with
1089         | None -> elems
1090         | Some x -> x::elems)
1091       [] candidates
1092   in
1093   elems
1094 ;;
1095
1096 let equational_and_applicative_case
1097   signature flags status g depth gty cache
1098 =
1099  let elems =
1100   if false (*is_equational_case gty flags*) then
1101     let elems =
1102       equational_case
1103         signature status flags g gty cache
1104     in
1105     let more_elems =
1106         applicative_case
1107           signature status flags g gty cache
1108     in
1109       elems@more_elems
1110   else
1111     let elems =
1112       (*match LibraryObjects.eq_URI () with
1113       | Some _ ->
1114          smart_applicative_case dbd tables depth s fake_proof goalno
1115            gty m context signature universe cache flags
1116       | None -> *)
1117          applicative_case
1118           signature status flags g gty cache
1119     in
1120       elems
1121  in
1122  let elems =
1123     (* XXX calculate the sort *)
1124    List.map (fun c,s,gl -> c,s,List.map (fun i -> i,depth-1,P) gl) elems
1125  in
1126  let elems = sort_new_elems elems in
1127  elems, cache
1128 ;;
1129
1130 let calculate_goal_ty (goalno,_,_) status =
1131   try Some (get_goalty status goalno)
1132   with Error _ -> None
1133 ;;
1134 let d_goals l =
1135   let rec aux acc = function
1136     | (D g)::tl -> aux (acc@[g]) tl
1137     | (S _)::tl -> aux acc tl
1138     | [] -> acc
1139   in
1140     aux [] l
1141 ;;
1142 let prop_only l =
1143   List.filter (function (_,_,P) -> true | _ -> false) l
1144 ;;
1145 let remove_s_from_fl (id,_,_) (fl : fail list) =
1146   let rec aux = function
1147     | [] -> []
1148     | ((id1,_,_),_)::tl when id = id1 -> tl
1149     | hd::tl ->  hd :: aux tl
1150   in
1151     aux fl
1152 ;;
1153
1154 let rec guess_name name ctx =
1155   if name = "_" then guess_name "auto" ctx else
1156   if not (List.mem_assoc name ctx) then name else
1157   guess_name (name^"'") ctx
1158 ;;
1159
1160 let intro_case status gno gty depth cache name =
1161    let status = NTactics.focus_tac [gno] status in
1162    let status = NTactics.intro_tac (guess_name name (ctx_of gty)) status in
1163    let open_goals = head_goals status#stack in
1164    assert (List.length open_goals  = 1);
1165    let open_goal = List.hd open_goals in
1166    let status, cache =
1167      let ngty = get_goalty status open_goal in
1168      let ctx = ctx_of ngty in
1169      let t = mk_cic_term ctx (NCic.Rel 1) in
1170      let status, ty = typeof status ctx t in
1171      let _status, ty, _args = saturate status ty in
1172      status, add_to_th t ty cache
1173    in
1174    debug_print (lazy (" intro: "^ string_of_int open_goal));
1175 (*    pp_th status cache; *)
1176    incr candidate_no;
1177     (* XXX calculate the sort *)
1178    [(!candidate_no,Ast.Implicit `JustOne),status,[open_goal,depth,P]],
1179    cache
1180 ;;
1181
1182 let do_something signature flags s gno depth gty cache =
1183   let _s, raw_gty = term_of_cic_term s gty (ctx_of gty) in
1184   match raw_gty with
1185   | NCic.Prod (name,_,_) -> intro_case s gno gty depth cache name
1186   | _ ->
1187       equational_and_applicative_case signature flags s gno depth gty cache
1188 ;;
1189
1190 let auto_main flags signature elems cache =
1191   let rec aux (elems, cache : 'a auto_status) =
1192 (* processa le hint dell'utente *)
1193 (*     let cache, elems = filter_prune_hint cache elems in *)
1194     match elems with
1195 (* USER HINT
1196     | (m, s, size, don, todo, fl)::orlist when !hint <> None ->
1197         debug_print (lazy "skip");
1198         (match !hint with
1199         | Some i when condition_for_hint i todo ->
1200             aux tables flags cache orlist
1201         | _ ->
1202           hint := None;
1203           aux tables flags cache elems)
1204 *)
1205     | [] ->
1206         debug_print (lazy "gave up");
1207         Gaveup
1208     | (s, _, _, [],_)::orlist ->
1209         debug_print (lazy "success");
1210         Proved (s, (orlist, cache))
1211     | (s, size, don, (D (_,_,T))::todo, fl)::orlist
1212       when not flags.do_types ->
1213         debug_print (lazy "skip goal in Type");
1214         aux ((s, size, don, todo, fl)::orlist, cache)
1215     | (s, size, don, (S(g, key, c) as op)::todo, fl)::orlist ->
1216         let cache, orlist, fl, sibling_pruned =
1217           add_to_cache_and_del_from_orlist_if_green_cut
1218             g s cache key todo orlist fl size
1219         in
1220         let fl = remove_s_from_fl g fl in
1221         let don = if sibling_pruned then don else op::don in
1222         let s = NTactics.unfocus_tac s in
1223         aux ((s, size, don, todo, fl)::orlist, cache)
1224     | (s, size, don, todo, fl)::orlist
1225       when List.length(prop_only (d_goals todo)) > flags.maxwidth ->
1226         debug_print (lazy ("FAIL: WIDTH"));
1227         aux (orlist, cache)
1228     | (s, size, don, todo, fl)::orlist when size > flags.maxsize ->
1229         debug_print (lazy ("FAIL: SIZE: "^string_of_int size ^
1230             " > " ^ string_of_int flags.maxsize ));
1231         aux (orlist, cache)
1232     | _ when Unix.gettimeofday () > flags.timeout ->
1233         debug_print (lazy ("FAIL: TIMEOUT"));
1234         Gaveup
1235     | (s, size, don, (D (gno,depth,_ as g))::todo, fl)::orlist ->
1236         debug_print (lazy "attack goal");
1237         match calculate_goal_ty g s with
1238         | None ->
1239             debug_print (lazy ("SUCCESS: SIDE EFFECT: " ^ string_of_int gno));
1240             aux ((s,size,don,todo, fl)::orlist, cache)
1241         | Some gty ->
1242             let s, gty = apply_subst s (ctx_of gty) gty in
1243             debug_print (lazy ("EXAMINE: "^ ppterm s gty));
1244             match cache_examine cache gty with
1245             | `Failed_in d when d >= depth ->
1246                 debug_print (lazy ("FAIL: DEPTH (cache): "^string_of_int gno));
1247                 let cache = close_failures fl cache in
1248                 aux (orlist, cache)
1249             | `UnderInspection ->
1250                 debug_print (lazy ("FAIL: LOOP: " ^ string_of_int gno));
1251                 let cache = close_failures fl cache in
1252                 aux (orlist,cache)
1253             | `Succeded t ->
1254                 debug_print (lazy ("SUCCESS: CACHE HIT: " ^ string_of_int gno));
1255                 let s = put_in_subst s g t gty in
1256                 aux ((s, size, don,todo, fl)::orlist, cache)
1257             | `Notfound
1258             | `Failed_in _ when depth > 0 ->
1259                 ( (* more depth or is the first time we see the goal *)
1260                     if prunable s gty todo then
1261                       (debug_print (lazy( "FAIL: LOOP: one father is equal"));
1262                        let cache = close_failures fl cache in
1263                        aux (orlist,cache))
1264                     else
1265                     let cache = cache_add_underinspection cache gty depth in
1266                     debug_print (lazy ("INSPECTING: " ^
1267                         string_of_int gno ^ "("^ string_of_int size ^ "): "^
1268                         ppterm s gty));
1269                     (* elems are possible computations for proving gty *)
1270                     let elems, cache =
1271                       do_something signature flags s gno depth gty cache
1272                     in
1273                     if elems = [] then
1274                       (* this goal has failed *)
1275                       let cache = close_failures ((g,gty)::fl) cache in
1276                       aux (orlist, cache)
1277                     else
1278                       let size_gl l = List.length
1279                         (List.filter (function (_,_,P) -> true | _ -> false) l)
1280                       in
1281                       let elems =
1282                         let inj_gl gl = List.map (fun g -> D g) gl in
1283                         let rec map = function
1284                           | [] -> assert false
1285                           | (cand,s,gl)::[] ->
1286                               let todo =
1287                                 inj_gl gl @ (S(g,gty,cand))::todo
1288                               in
1289                               (* we are the last in OR, we fail on g and
1290                                * also on all failures implied by g *)
1291                               (s, size + size_gl gl, don, todo, (g,gty)::fl)
1292                               :: orlist
1293                           | (cand,s,gl)::tl ->
1294                               let todo =
1295                                 inj_gl gl @ (S(g,gty,cand))::todo
1296                               in
1297                               (s, size + size_gl gl, don, todo, []) :: map tl
1298                         in
1299                           map elems
1300                       in
1301                         aux (elems, cache))
1302             | _ ->
1303                 debug_print (lazy ("FAIL: DEPTH: " ^ string_of_int gno));
1304                 let cache = close_failures fl cache in
1305                 aux (orlist, cache)
1306   in
1307     (aux (elems, cache) : 'a auto_result)
1308 ;;
1309
1310 let int name l def =
1311   try int_of_string (List.assoc name l)
1312   with Failure _ | Not_found -> def
1313 ;;
1314
1315 let auto_tac ~params:(_univ,flags) status =
1316   let goals = head_goals status#stack in
1317   let status, cache = mk_th_cache status goals in
1318   let depth = int "depth" flags 3 in
1319   (* XXX fix sort *)
1320   let goals = List.map (fun i -> D(i,depth,P)) goals in
1321   let elems = [status,0,[],goals,[]] in
1322   let signature = () in
1323   let flags = {
1324           maxwidth = 3 + List.length goals;
1325           maxsize = 10;
1326           timeout = Unix.gettimeofday() +. 3000.;
1327           do_types = false;
1328   } in
1329   match auto_main flags signature elems cache with
1330   | Gaveup -> raise (Error (lazy "auto gave up", None))
1331   | Proved (s, (_orlist, _cache)) ->
1332       let stack =
1333         match s#stack with
1334         | (g,t,k,f) :: rest -> (filter_open g,t,k,f):: rest
1335         | _ -> assert false
1336       in
1337       s#set_stack stack
1338 ;;
1339
1340
1341 (* ========================= dispatching of auto/auto_paramod ============ *)
1342 let auto_tac ~params:(_,flags as params) =
1343   if List.mem_assoc "paramodulation" flags then
1344     auto_paramod_tac ~params
1345   else
1346     auto_tac ~params
1347 ;;
1348
1349 (* EOF *)