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