]> matita.cs.unibo.it Git - helm.git/blob - matita/components/ng_tactics/nnAuto.ml
several dialog boxes no longer used removed
[helm.git] / matita / 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 print ?(depth=0) s = 
15   prerr_endline (String.make (2*depth) ' '^Lazy.force s) 
16 let noprint ?(depth=0) _ = () 
17 let debug_print = noprint
18
19 open Continuationals.Stack
20 open NTacStatus
21 module Ast = NotationPt
22
23 (* ======================= statistics  ========================= *)
24
25 let app_counter = ref 0
26
27 module RHT = struct
28   type t = NReference.reference
29   let equal = NReference.eq
30   let compare = NReference.compare
31   let hash = NReference.hash
32 end;;
33
34 module RefHash = Hashtbl.Make(RHT);;
35
36 type info = {
37   nominations : int ref;
38   uses: int ref;
39 }
40
41 let statistics: info RefHash.t = RefHash.create 503
42
43 let incr_nominations tbl item =
44   try
45     let v = RefHash.find tbl item in incr v.nominations
46   with Not_found ->
47     RefHash.add tbl item {nominations = ref 1; uses = ref 0}
48
49 let incr_uses tbl item =
50   try
51     let v = RefHash.find tbl item in incr v.uses
52   with Not_found -> assert false
53
54 let toref f tbl t =
55   match t with
56     | Ast.NRef n -> 
57         f tbl n
58     | Ast.NCic _  (* local candidate *)
59     | _  ->  ()
60
61 let is_relevant tbl item =
62   try
63     let v = RefHash.find tbl item in
64       if !(v.nominations) < 60 then true (* not enough info *)
65       else if !(v.uses) = 0 then false
66       else true
67   with Not_found -> true
68
69 let print_stat status tbl =
70   let l = RefHash.fold (fun a v l -> (a,v)::l) tbl [] in
71   let relevance v = float !(v.uses) /. float !(v.nominations) in
72   let vcompare (_,v1) (_,v2) =
73     Pervasives.compare (relevance v1) (relevance v2) in
74   let l = List.sort vcompare l in
75   let short_name r = 
76     Filename.chop_extension 
77       (Filename.basename (NReference.string_of_reference r))
78   in
79   let vstring (a,v)=
80       short_name a ^ ": rel = " ^
81       (string_of_float (relevance v)) ^
82       "; uses = " ^ (string_of_int !(v.uses)) ^
83       "; nom = " ^ (string_of_int !(v.nominations)) in
84   lazy ("\n\nSTATISTICS:\n" ^
85           String.concat "\n" (List.map vstring l)) 
86
87 (* ======================= utility functions ========================= *)
88 module IntSet = Set.Make(struct type t = int let compare = compare end)
89
90 let get_sgoalty status g =
91  let _,_,metasenv,subst,_ = status#obj in
92  try
93    let _, ctx, ty = NCicUtils.lookup_meta g metasenv in
94    let ty = NCicUntrusted.apply_subst status subst ctx ty in
95    let ctx = NCicUntrusted.apply_subst_context status
96      ~fix_projections:true subst ctx
97    in
98      NTacStatus.mk_cic_term ctx ty
99  with NCicUtils.Meta_not_found _ as exn -> fail ~exn (lazy "get_sgoalty")
100 ;;
101
102 let deps status g =
103   let gty = get_sgoalty status g in
104   metas_of_term status gty
105 ;;
106
107 let menv_closure status gl = 
108   let rec closure acc = function
109     | [] -> acc
110     | x::l when IntSet.mem x acc -> closure acc l
111     | x::l -> closure (IntSet.add x acc) (deps status x @ l)
112   in closure IntSet.empty gl
113 ;;
114
115 (* we call a "fact" an object whose hypothesis occur in the goal 
116    or in types of goal-variables *)
117 let branch status ty =  
118   let status, ty, metas = saturate ~delta:0 status ty in
119   noprint (lazy ("saturated ty :" ^ (ppterm status ty)));
120   let g_metas = metas_of_term status ty in
121   let clos = menv_closure status g_metas in
122   (* let _,_,metasenv,_,_ = status#obj in *)
123   let menv = 
124     List.fold_left
125       (fun acc m ->
126          let _, m = term_of_cic_term status m (ctx_of m) in
127          match m with 
128          | NCic.Meta(i,_) -> IntSet.add i acc
129          | _ -> assert false)
130       IntSet.empty metas
131   in 
132   (* IntSet.subset menv clos *)
133   IntSet.cardinal(IntSet.diff menv clos)
134
135 let is_a_fact status ty = branch status ty = 0
136
137 let is_a_fact_obj s uri = 
138   let obj = NCicEnvironment.get_checked_obj s uri in
139   match obj with
140     | (_,_,[],[],NCic.Constant(_,_,_,ty,_)) ->
141         is_a_fact s (mk_cic_term [] ty)
142 (* aggiungere i costruttori *)
143     | _ -> false
144
145 let is_a_fact_ast status subst metasenv ctx cand = 
146  noprint ~depth:0 
147    (lazy ("checking facts " ^ NotationPp.pp_term status cand)); 
148  let status, t = disambiguate status ctx ("",0,cand) `XTNone in
149  let status,t = term_of_cic_term status t ctx in
150  let ty = NCicTypeChecker.typeof status subst metasenv ctx t in
151    is_a_fact status (mk_cic_term ctx ty)
152
153 let current_goal status = 
154   let open_goals = head_goals status#stack in
155   assert (List.length open_goals  = 1);
156   let open_goal = List.hd open_goals in
157   let gty = get_goalty status open_goal in
158   let ctx = ctx_of gty in
159     open_goal, ctx, gty
160
161 let height_of_ref status (NReference.Ref (uri, x)) = 
162   match x with
163   | NReference.Decl 
164   | NReference.Ind _ 
165   | NReference.Con _
166   | NReference.CoFix _ -> 
167       let _,height,_,_,_ = NCicEnvironment.get_checked_obj status uri in
168       height 
169   | NReference.Def h -> h 
170   | NReference.Fix (_,_,h) -> h 
171 ;;
172
173 (*************************** height functions ********************************)
174 let fast_height_of_term status t =
175  let h = ref 0 in
176  let rec aux =
177   function
178      NCic.Meta (_,(_,NCic.Ctx l)) -> List.iter aux l
179    | NCic.Meta _ -> ()
180    | NCic.Rel _
181    | NCic.Sort _ -> ()
182    | NCic.Implicit _ -> assert false
183    | NCic.Const nref -> 
184 (*
185                    prerr_endline (status#ppterm ~metasenv:[] ~subst:[]
186                    ~context:[] t ^ ":" ^ string_of_int (height_of_ref status nref));            
187 *)
188        h := max !h (height_of_ref status nref)
189    | NCic.Prod (_,t1,t2)
190    | NCic.Lambda (_,t1,t2) -> aux t1; aux t2
191    | NCic.LetIn (_,s,ty,t) -> aux s; aux ty; aux t
192    | NCic.Appl l -> List.iter aux l
193    | NCic.Match (_,outty,t,pl) -> aux outty; aux t; List.iter aux pl
194  in
195   aux t; !h
196 ;;
197
198 let height_of_goal g status = 
199   let ty = get_goalty status g in
200   let context = ctx_of ty in
201   let _, ty = term_of_cic_term status ty (ctx_of ty) in
202   let h = ref (fast_height_of_term status ty) in
203   List.iter 
204     (function 
205        | _, NCic.Decl ty -> h := max !h (fast_height_of_term status ty)
206        | _, NCic.Def (bo,ty) -> 
207            h := max !h (fast_height_of_term status ty);
208            h := max !h (fast_height_of_term status bo);
209     )
210     context;
211   !h
212 ;;      
213
214 let height_of_goals status = 
215   let open_goals = head_goals status#stack in
216   assert (List.length open_goals > 0);
217   let h = ref 1 in
218   List.iter 
219     (fun open_goal ->
220        h := max !h (height_of_goal open_goal status))
221      open_goals;
222   noprint (lazy ("altezza sequente: " ^ string_of_int !h));
223   !h
224 ;;
225
226 (* =============================== paramod =========================== *)
227 let solve f status eq_cache goal =
228 (*
229   let f = 
230     if fast then NCicParamod.fast_eq_check
231     else NCicParamod.paramod in
232 *)
233   let n,h,metasenv,subst,o = status#obj in
234   let gname, ctx, gty = List.assoc goal metasenv in
235   let gty = NCicUntrusted.apply_subst status subst ctx gty in
236   let build_status (pt, _, metasenv, subst) =
237     try
238       debug_print (lazy ("refining: "^(status#ppterm ctx subst metasenv pt)));
239       let stamp = Unix.gettimeofday () in 
240       let metasenv, subst, pt, pty =
241         (* NCicRefiner.typeof status
242           (* (status#set_coerc_db NCicCoercion.empty_db) *)
243           metasenv subst ctx pt None in
244           debug_print (lazy ("refined: "^(status#ppterm ctx subst metasenv pt)));
245           noprint (lazy ("synt: "^(status#ppterm ctx subst metasenv pty)));
246           let metasenv, subst =
247             NCicUnification.unify status metasenv subst ctx gty pty *)
248         NCicRefiner.typeof 
249           (status#set_coerc_db NCicCoercion.empty_db) 
250           metasenv subst ctx pt (`XTSome gty) 
251         in 
252           noprint (lazy (Printf.sprintf "Refined in %fs"
253                      (Unix.gettimeofday() -. stamp))); 
254           let status = status#set_obj (n,h,metasenv,subst,o) in
255           let metasenv = List.filter (fun j,_ -> j <> goal) metasenv in
256           let subst = (goal,(gname,ctx,pt,pty)) :: subst in
257             Some (status#set_obj (n,h,metasenv,subst,o))
258     with 
259         NCicRefiner.RefineFailure msg 
260       | NCicRefiner.Uncertain msg ->
261           debug_print (lazy ("WARNING U: refining in fast_eq_check failed\n" ^
262                         snd (Lazy.force msg) ^  
263                         "\n in the environment\n" ^ 
264                         status#ppmetasenv subst metasenv)); None
265       | NCicRefiner.AssertFailure msg -> 
266           debug_print (lazy ("WARNING F: refining in fast_eq_check failed" ^
267                         Lazy.force msg ^
268                         "\n in the environment\n" ^ 
269                         status#ppmetasenv subst metasenv)); None
270       | Sys.Break as e -> raise e
271       | _ -> None
272     in
273     HExtlib.filter_map build_status
274       (f status metasenv subst ctx eq_cache (NCic.Rel ~-1,gty))
275 ;;
276
277 let fast_eq_check eq_cache status (goal:int) =
278   match solve NCicParamod.fast_eq_check status eq_cache goal with
279   | [] -> raise (Error (lazy "no proof found",None))
280   | s::_ -> s
281 ;;
282
283 let dist_fast_eq_check eq_cache s = 
284   NTactics.distribute_tac (fast_eq_check eq_cache) s
285 ;;
286
287 let auto_eq_check eq_cache status =
288   try 
289     let s = dist_fast_eq_check eq_cache status in
290       [s]
291   with
292     | Error _ -> debug_print (lazy ("no paramod proof found"));[]
293 ;;
294
295 let index_local_equations eq_cache status =
296   noprint (lazy "indexing equations");
297   let open_goals = head_goals status#stack in
298   let open_goal = List.hd open_goals in
299   let ngty = get_goalty status open_goal in
300   let _,_,metasenv,subst,_ = status#obj in
301   let ctx = apply_subst_context ~fix_projections:true status (ctx_of ngty) in
302   let c = ref 0 in
303   List.fold_left 
304     (fun eq_cache _ ->
305        c:= !c+1;
306        let t = NCic.Rel !c in
307          try
308            let ty = NCicTypeChecker.typeof status subst metasenv ctx t in
309            if is_a_fact status (mk_cic_term ctx ty) then
310              (debug_print(lazy("eq indexing " ^ (status#ppterm ctx subst metasenv ty)));
311               NCicParamod.forward_infer_step status metasenv subst ctx eq_cache t ty)
312            else 
313              (noprint (lazy ("not a fact: " ^ (status#ppterm ctx subst metasenv ty)));
314               eq_cache)
315          with 
316            | NCicTypeChecker.TypeCheckerFailure _
317            | NCicTypeChecker.AssertFailure _ -> eq_cache) 
318     eq_cache ctx
319 ;;
320
321 let index_local_equations2 eq_cache status open_goal lemmas nohyps =
322   noprint (lazy "indexing equations");
323   let eq_cache,lemmas =
324    match lemmas with
325       None -> eq_cache,[]
326     | Some l -> NCicParamod.empty_state,l
327   in
328   let ngty = get_goalty status open_goal in
329   let _,_,metasenv,subst,_ = status#obj in
330   let ctx = apply_subst_context ~fix_projections:true status (ctx_of ngty) in
331   let status,lemmas =
332    List.fold_left
333     (fun (status,lemmas) l ->
334       let status,l = NTacStatus.disambiguate status ctx l `XTNone in
335       let status,l = NTacStatus.term_of_cic_term status l ctx in
336        status,l::lemmas)
337     (status,[]) lemmas in
338   let local_equations =
339    if nohyps then [] else
340     List.map (fun i -> NCic.Rel (i + 1))
341      (HExtlib.list_seq 1 (List.length ctx)) in
342   let lemmas = lemmas @ local_equations in
343   List.fold_left 
344     (fun eq_cache t ->
345          try
346            let ty = NCicTypeChecker.typeof status subst metasenv ctx t in
347            if is_a_fact status (mk_cic_term ctx ty) then
348              (debug_print(lazy("eq indexing " ^ (status#ppterm ctx subst metasenv ty)));
349               NCicParamod.forward_infer_step status metasenv subst ctx eq_cache t ty)
350            else 
351              (noprint (lazy ("not a fact: " ^ (status#ppterm ctx subst metasenv ty)));
352               eq_cache)
353          with 
354            | NCicTypeChecker.TypeCheckerFailure _
355            | NCicTypeChecker.AssertFailure _ -> eq_cache)
356     eq_cache lemmas
357 ;;
358
359 let fast_eq_check_tac ~params s = 
360   let unit_eq = index_local_equations s#eq_cache s in   
361   dist_fast_eq_check unit_eq s
362 ;;
363
364 let paramod eq_cache status goal =
365   match solve NCicParamod.paramod status eq_cache goal with
366   | [] -> raise (Error (lazy "no proof found",None))
367   | s::_ -> s
368 ;;
369
370 let paramod_tac ~params s = 
371   let unit_eq = index_local_equations s#eq_cache s in   
372   NTactics.distribute_tac (paramod unit_eq) s
373 ;;
374
375 let demod eq_cache status goal =
376   match solve NCicParamod.demod status eq_cache goal with
377   | [] -> raise (Error (lazy "no progress",None))
378   | s::_ -> s
379 ;;
380
381 let demod_tac ~params s = 
382   let unit_eq s i =
383    index_local_equations2 s#eq_cache s i (fst params)
384     (List.mem_assoc "nohyps" (snd params))
385   in   
386    NTactics.distribute_tac (fun s i -> demod (unit_eq s i) s i) s
387 ;;
388
389 (*
390 let fast_eq_check_tac_all  ~params eq_cache status = 
391   let g,_,_ = current_goal status in
392   let allstates = fast_eq_check_all status eq_cache g in
393   let pseudo_low_tac s _ _ = s in
394   let pseudo_low_tactics = 
395     List.map pseudo_low_tac allstates 
396   in
397     List.map (fun f -> NTactics.distribute_tac f status) pseudo_low_tactics
398 ;;
399 *)
400
401 (*
402 let demod status eq_cache goal =
403   let n,h,metasenv,subst,o = status#obj in
404   let gname, ctx, gty = List.assoc goal metasenv in
405   let gty = NCicUntrusted.apply_subst subst ctx gty in
406
407 let demod_tac ~params s = 
408   let unit_eq = index_local_equations s#eq_cache s in   
409   dist_fast_eq_check unit_eq s
410 *)
411
412 (*************** subsumption ****************)
413
414 let close_wrt_context status =
415   List.fold_left 
416     (fun ty ctx_entry -> 
417         match ctx_entry with 
418        | name, NCic.Decl t -> NCic.Prod(name,t,ty)
419        | name, NCic.Def(bo, _) -> NCicSubstitution.subst status bo ty)
420 ;;
421
422 let args_for_context ?(k=1) ctx =
423   let _,args =
424     List.fold_left 
425       (fun (n,l) ctx_entry -> 
426          match ctx_entry with 
427            | name, NCic.Decl t -> n+1,NCic.Rel(n)::l
428            | name, NCic.Def(bo, _) -> n+1,l)
429       (k,[]) ctx in
430     args
431
432 let constant_for_meta status ctx ty i =
433   let name = "cic:/foo"^(string_of_int i)^".con" in
434   let uri = NUri.uri_of_string name in
435   let ty = close_wrt_context status ty ctx in
436   (* prerr_endline (status#ppterm [] [] [] ty); *)
437   let attr = (`Generated,`Definition,`Local) in
438   let obj = NCic.Constant([],name,None,ty,attr) in
439     (* Constant  of relevance * string * term option * term * c_attr *)
440     (uri,0,[],[],obj)
441
442 (* not used *)
443 let refresh metasenv =
444   List.fold_left 
445     (fun (metasenv,subst) (i,(iattr,ctx,ty)) ->
446        let ikind = NCicUntrusted.kind_of_meta iattr in
447        let metasenv,j,instance,ty = 
448          NCicMetaSubst.mk_meta ~attrs:iattr 
449            metasenv ctx ~with_type:ty ikind in
450        let s_entry = i,(iattr, ctx, instance, ty) in
451        let metasenv = List.filter (fun x,_ -> i <> x) metasenv in
452          metasenv,s_entry::subst) 
453       (metasenv,[]) metasenv
454
455 (* close metasenv returns a ground instance of all the metas in the
456 metasenv, insantiatied with axioms, and the list of these axioms *)
457 let close_metasenv status metasenv subst = 
458   (*
459   let metasenv = NCicUntrusted.apply_subst_metasenv subst metasenv in
460   *)
461   let metasenv = NCicUntrusted.sort_metasenv status subst metasenv in 
462     List.fold_left 
463       (fun (subst,objs) (i,(iattr,ctx,ty)) ->
464          let ty = NCicUntrusted.apply_subst status subst ctx ty in
465          let ctx = 
466            NCicUntrusted.apply_subst_context status ~fix_projections:true 
467              subst ctx in
468          let (uri,_,_,_,obj) as okind = 
469            constant_for_meta status ctx ty i in
470          try
471            NCicEnvironment.check_and_add_obj status okind;
472            let iref = NReference.reference_of_spec uri NReference.Decl in
473            let iterm =
474              let args = args_for_context ctx in
475                if args = [] then NCic.Const iref 
476                else NCic.Appl(NCic.Const iref::args)
477            in
478            (* prerr_endline (status#ppterm ctx [] [] iterm); *)
479            let s_entry = i, ([], ctx, iterm, ty)
480            in s_entry::subst,okind::objs
481          with
482             Sys.Break as e -> raise e
483           | _ -> assert false)
484       (subst,[]) metasenv
485 ;;
486
487 let ground_instances status gl =
488   let _,_,metasenv,subst,_ = status#obj in
489   let subset = menv_closure status gl in
490   let submenv = List.filter (fun (x,_) -> IntSet.mem x subset) metasenv in
491 (*
492   let submenv = metasenv in
493 *)
494   let subst, objs = close_metasenv status submenv subst in
495   try
496     List.iter
497       (fun i -> 
498          let (_, ctx, t, _) = List.assoc i subst in
499            noprint (lazy (status#ppterm ctx [] [] t));
500            List.iter 
501              (fun (uri,_,_,_,_) as obj -> 
502                 NCicEnvironment.invalidate_item (`Obj (uri, obj))) 
503              objs;
504            ())
505       gl
506   with
507       Not_found -> assert false 
508   (* (ctx,t) *)
509 ;;
510
511 let replace_meta status i args target = 
512   let rec aux k = function
513     (* TODO: local context *)
514     | NCic.Meta (j,lc) when i = j ->
515         (match args with
516            | [] -> NCic.Rel 1
517            | _ -> let args = 
518                List.map (NCicSubstitution.subst_meta status lc) args in
519                NCic.Appl(NCic.Rel k::args))
520     | NCic.Meta (j,lc) as m ->
521         (match lc with
522            _,NCic.Irl _ -> m
523          | n,NCic.Ctx l ->
524             NCic.Meta
525              (i,(0,NCic.Ctx
526                  (List.map (fun t ->
527                    aux k (NCicSubstitution.lift status n t)) l))))
528     | t -> NCicUtils.map status (fun _ k -> k+1) k aux t
529  in
530    aux 1 target
531 ;;
532
533 let close_wrt_metasenv status subst =
534   List.fold_left 
535     (fun ty (i,(iattr,ctx,mty)) ->
536        let mty = NCicUntrusted.apply_subst status subst ctx mty in
537        let ctx = 
538          NCicUntrusted.apply_subst_context status ~fix_projections:true 
539            subst ctx in
540        let cty = close_wrt_context status mty ctx in
541        let name = "foo"^(string_of_int i) in
542        let ty = NCicSubstitution.lift status 1 ty in
543        let args = args_for_context ~k:1 ctx in
544          (* prerr_endline (status#ppterm ctx [] [] iterm); *)
545        let ty = replace_meta status i args ty
546        in
547        NCic.Prod(name,cty,ty))
548 ;;
549
550 let close status g =
551   let _,_,metasenv,subst,_ = status#obj in
552   let subset = menv_closure status [g] in
553   let subset = IntSet.remove g subset in
554   let elems = IntSet.elements subset in 
555   let _, ctx, ty = NCicUtils.lookup_meta g metasenv in
556   let ty = NCicUntrusted.apply_subst status subst ctx ty in
557   noprint (lazy ("metas in " ^ (status#ppterm ctx [] metasenv ty)));
558   noprint (lazy (String.concat ", " (List.map string_of_int elems)));
559   let submenv = List.filter (fun (x,_) -> IntSet.mem x subset) metasenv in
560   let submenv = List.rev (NCicUntrusted.sort_metasenv status subst submenv) in 
561 (*  
562     let submenv = metasenv in
563 *)
564   let ty = close_wrt_metasenv status subst ty submenv in
565     noprint (lazy (status#ppterm ctx [] [] ty));
566     ctx,ty
567 ;;
568
569 (****************** smart application ********************)
570
571 let saturate_to_ref status metasenv subst ctx nref ty =
572   let height = height_of_ref status nref in
573   let rec aux metasenv ty args = 
574     let ty,metasenv,moreargs =  
575       NCicMetaSubst.saturate status ~delta:height metasenv subst ctx ty 0 in 
576     match ty with
577       | NCic.Const(NReference.Ref (_,NReference.Def _) as nre) 
578           when nre<>nref ->
579           let _, _, bo, _, _, _ = NCicEnvironment.get_checked_def status nre in 
580             aux metasenv bo (args@moreargs)
581       | NCic.Appl(NCic.Const(NReference.Ref (_,NReference.Def _) as nre)::tl) 
582           when nre<>nref ->
583           let _, _, bo, _, _, _ = NCicEnvironment.get_checked_def status nre in
584             aux metasenv (NCic.Appl(bo::tl)) (args@moreargs) 
585     | _ -> ty,metasenv,(args@moreargs)
586   in
587     aux metasenv ty []
588
589 let smart_apply t unit_eq status g = 
590   let n,h,metasenv,subst,o = status#obj in
591   let gname, ctx, gty = List.assoc g metasenv in
592   (* let ggty = mk_cic_term context gty in *)
593   let status, t = disambiguate status ctx t `XTNone in
594   let status,t = term_of_cic_term status t ctx in
595   let _,_,metasenv,subst,_ = status#obj in
596   let ty = NCicTypeChecker.typeof status subst metasenv ctx t in
597   let ty,metasenv,args = 
598     match gty with
599       | NCic.Const(nref)
600       | NCic.Appl(NCic.Const(nref)::_) -> 
601           saturate_to_ref status metasenv subst ctx nref ty
602       | _ -> 
603           NCicMetaSubst.saturate status metasenv subst ctx ty 0 in
604   let metasenv,j,inst,_ = NCicMetaSubst.mk_meta metasenv ctx `IsTerm in
605   let status = status#set_obj (n,h,metasenv,subst,o) in
606   let pterm = if args=[] then t else 
607     match t with
608       | NCic.Appl l -> NCic.Appl(l@args) 
609       | _ -> NCic.Appl(t::args) 
610   in
611   noprint(lazy("pterm " ^ (status#ppterm ctx [] [] pterm)));
612   noprint(lazy("pty " ^ (status#ppterm ctx [] [] ty)));
613   let eq_coerc =       
614     let uri = 
615       NUri.uri_of_string "cic:/matita/basics/logic/eq_coerc.con" in
616     let ref = NReference.reference_of_spec uri (NReference.Def(2)) in
617       NCic.Const ref
618   in
619   let smart = 
620     NCic.Appl[eq_coerc;ty;NCic.Implicit `Type;pterm;inst] in
621   let smart = mk_cic_term ctx smart in 
622     try
623       let status = instantiate status g smart in
624       let _,_,metasenv,subst,_ = status#obj in
625       let _,ctx,jty = List.assoc j metasenv in
626       let jty = NCicUntrusted.apply_subst status subst ctx jty in
627         debug_print(lazy("goal " ^ (status#ppterm ctx [] [] jty)));
628         let res = fast_eq_check unit_eq status j in
629         debug_print(lazy("ritorno da fast_eq_check"));
630         res
631     with
632       | NCicEnvironment.ObjectNotFound s as e ->
633           raise (Error (lazy "eq_coerc non yet defined",Some e))
634       | Error _ as e -> debug_print (lazy "error"); raise e
635 (* FG: for now we catch TypeCheckerFailure; to be understood *)  
636       | NCicTypeChecker.TypeCheckerFailure _ ->
637           debug_print (lazy "TypeCheckerFailure");
638           raise (Error (lazy "no proof found",None))
639 ;;
640
641 let compare_statuses ~past ~present =
642  let _,_,past,_,_ = past#obj in 
643  let _,_,present,_,_ = present#obj in 
644  List.map fst (List.filter (fun (i,_) -> not(List.mem_assoc i past)) present),
645  List.map fst (List.filter (fun (i,_) -> not (List.mem_assoc i present)) past)
646 ;;
647
648 (* paramodulation has only an implicit knoweledge of the symmetry of equality;
649    hence it is in trouble in proving (a = b) = (b = a) *) 
650 let try_sym tac status g =
651   let sym_eq = Ast.Appl [Ast.Ident("sym_eq",None); Ast.Implicit `Vector] in
652   let _,_,metasenv,subst,_ = status#obj in
653   let _, context, gty = List.assoc g metasenv in
654   let is_eq = 
655     NCicParamod.is_equation status metasenv subst context gty 
656   in
657   if is_eq then
658     try tac status g
659     with Error _ ->
660       let new_status = instantiate_with_ast status g ("",0,sym_eq) in 
661       let go, _ = compare_statuses ~past:status ~present:new_status in
662       assert (List.length go  = 1);
663       let ng = List.hd go in
664       tac new_status ng
665    else tac status g
666 ;;
667
668 let smart_apply_tac t s =
669   let unit_eq = index_local_equations s#eq_cache s in   
670   NTactics.distribute_tac (try_sym (smart_apply t unit_eq)) s 
671   (* NTactics.distribute_tac (smart_apply t unit_eq) s *)
672
673 let smart_apply_auto t eq_cache =
674   NTactics.distribute_tac (try_sym (smart_apply t eq_cache)) 
675   (* NTactics.distribute_tac (smart_apply t eq_cache) *)
676
677
678 (****************** types **************)
679
680
681 type th_cache = (NCic.context * InvRelDiscriminationTree.t) list
682
683 (* cartesian: term set list -> term list set *)
684 let rec cartesian =
685  function
686     [] -> NDiscriminationTree.TermListSet.empty
687   | [l] ->
688      NDiscriminationTree.TermSet.fold
689       (fun x acc -> NDiscriminationTree.TermListSet.add [x] acc) l NDiscriminationTree.TermListSet.empty
690   | he::tl ->
691      let rest = cartesian tl in
692       NDiscriminationTree.TermSet.fold
693        (fun x acc ->
694          NDiscriminationTree.TermListSet.fold (fun l acc' -> NDiscriminationTree.TermListSet.add (x::l) acc') rest acc
695        ) he NDiscriminationTree.TermListSet.empty
696 ;;
697
698 (* all_keys_of_cic_type: term -> term set *)
699 let all_keys_of_cic_type status metasenv subst context ty =
700  let saturate ty =
701   (* Here we are dropping the metasenv, but this should not raise any
702      exception (hopefully...) *)
703   let ty,_,hyps =
704    NCicMetaSubst.saturate status ~delta:max_int metasenv subst context ty 0
705   in
706    ty,List.length hyps
707  in
708  let rec aux ty =
709   match ty with
710      NCic.Appl (he::tl) ->
711       let tl' =
712        List.map (fun ty ->
713         let wty = NCicReduction.whd status ~delta:0 ~subst context ty in
714          if ty = wty then
715           NDiscriminationTree.TermSet.add ty (aux ty)
716          else
717           NDiscriminationTree.TermSet.union
718            (NDiscriminationTree.TermSet.add  ty (aux  ty))
719            (NDiscriminationTree.TermSet.add wty (aux wty))
720         ) tl
721       in
722        NDiscriminationTree.TermListSet.fold
723         (fun l acc -> NDiscriminationTree.TermSet.add (NCic.Appl l) acc)
724         (cartesian ((NDiscriminationTree.TermSet.singleton he)::tl'))
725         NDiscriminationTree.TermSet.empty
726    | _ -> NDiscriminationTree.TermSet.empty
727  in
728   let ty,ity = saturate ty in
729   let wty,iwty = saturate (NCicReduction.whd status ~delta:0 ~subst context ty) in
730    if ty = wty then
731     [ity, NDiscriminationTree.TermSet.add ty (aux ty)]
732    else
733     [ity,  NDiscriminationTree.TermSet.add  ty (aux  ty) ;
734      iwty, NDiscriminationTree.TermSet.add wty (aux wty) ]
735 ;;
736
737 let all_keys_of_type status t =
738  let _,_,metasenv,subst,_ = status#obj in
739  let context = ctx_of t in
740  let status, t = apply_subst status context t in
741  let keys =
742   all_keys_of_cic_type status metasenv subst context
743    (snd (term_of_cic_term status t context))
744  in
745   status,
746    List.map
747     (fun (intros,keys) ->
748       intros,
749        NDiscriminationTree.TermSet.fold
750         (fun t acc -> Ncic_termSet.add (mk_cic_term context t) acc)
751         keys Ncic_termSet.empty
752     ) keys
753 ;;
754
755
756 let keys_of_type status orig_ty =
757   (* Here we are dropping the metasenv (in the status), but this should not
758      raise any exception (hopefully...) *)
759   let _, ty, _ = saturate ~delta:max_int status orig_ty in
760   let _, ty = apply_subst status (ctx_of ty) ty in
761   let keys =
762 (*
763     let orig_ty' = NCicTacReduction.normalize ~subst context orig_ty in
764     if orig_ty' <> orig_ty then
765      let ty',_,_= NCicMetaSubst.saturate ~delta:0 metasenv subst context orig_ty' 0 in
766       [ty;ty']
767     else
768      [ty]
769 *)
770    [ty] in
771 (*CSC: strange: we keep ty, ty normalized and ty ~delta:(h-1) *)
772   let keys = 
773     let _, ty = term_of_cic_term status ty (ctx_of ty) in
774     match ty with
775     | NCic.Const (NReference.Ref (_,(NReference.Def h | NReference.Fix (_,_,h)))) 
776     | NCic.Appl (NCic.Const(NReference.Ref(_,(NReference.Def h | NReference.Fix (_,_,h))))::_) 
777        when h > 0 ->
778          let _,ty,_= saturate status ~delta:(h-1) orig_ty in
779          ty::keys
780     | _ -> keys
781   in
782   status, keys
783 ;;
784
785 let all_keys_of_term status t =
786  let status, orig_ty = typeof status (ctx_of t) t in
787   all_keys_of_type status orig_ty
788 ;;
789
790 let keys_of_term status t =
791   let status, orig_ty = typeof status (ctx_of t) t in
792     keys_of_type status orig_ty
793 ;;
794
795 let mk_th_cache status gl = 
796   List.fold_left 
797     (fun (status, acc) g ->
798        let gty = get_goalty status g in
799        let ctx = ctx_of gty in
800        noprint(lazy("th cache for: "^ppterm status gty));
801        noprint(lazy("th cache in: "^ppcontext status ctx));
802        if List.mem_assq ctx acc then status, acc else
803          let idx = InvRelDiscriminationTree.empty in
804          let status,_,idx = 
805            List.fold_left 
806              (fun (status, i, idx) _ -> 
807                 let t = mk_cic_term ctx (NCic.Rel i) in
808                 let status, keys = keys_of_term status t in
809                 noprint(lazy("indexing: "^ppterm status t ^ ": " ^ string_of_int (List.length keys)));
810                 let idx =
811                   List.fold_left (fun idx k -> 
812                     InvRelDiscriminationTree.index idx k t) idx keys
813                 in
814                 status, i+1, idx)
815              (status, 1, idx) ctx
816           in
817          status, (ctx, idx) :: acc)
818     (status,[]) gl
819 ;;
820
821 let all_elements ctx cache =
822   let dummy = mk_cic_term ctx (NCic.Meta (0,(0, (NCic.Irl 0)))) in
823     try
824       let idx = List.assq ctx cache in
825       Ncic_termSet.elements 
826         (InvRelDiscriminationTree.retrieve_unifiables idx dummy)
827     with Not_found -> []
828
829 let add_to_th t c ty = 
830   let key_c = ctx_of t in
831   if not (List.mem_assq key_c c) then
832       (key_c ,InvRelDiscriminationTree.index 
833                InvRelDiscriminationTree.empty ty t ) :: c 
834   else
835     let rec replace = function
836       | [] -> []
837       | (x, idx) :: tl when x == key_c -> 
838           (x, InvRelDiscriminationTree.index idx ty t) :: tl
839       | x :: tl -> x :: replace tl
840     in 
841       replace c
842 ;;
843
844 let rm_from_th t c ty = 
845   let key_c = ctx_of t in
846   if not (List.mem_assq key_c c) then assert false
847   else
848     let rec replace = function
849       | [] -> []
850       | (x, idx) :: tl when x == key_c -> 
851           (x, InvRelDiscriminationTree.remove_index idx ty t) :: tl
852       | x :: tl -> x :: replace tl
853     in 
854       replace c
855 ;;
856
857 let pp_idx status idx =
858    InvRelDiscriminationTree.iter idx
859       (fun k set ->
860          noprint(lazy("K: " ^ NCicInverseRelIndexable.string_of_path k));
861          Ncic_termSet.iter 
862            (fun t -> debug_print(lazy("\t"^ppterm status t))) 
863            set)
864 ;;
865
866 let pp_th (status: #NTacStatus.pstatus) = 
867   List.iter 
868     (fun ctx, idx ->
869        noprint(lazy( "-----------------------------------------------"));
870        noprint(lazy( (status#ppcontext ~metasenv:[] ~subst:[] ctx)));
871        noprint(lazy( "||====>  "));
872        pp_idx status idx)
873 ;;
874
875 let search_in_th gty th = 
876   let c = ctx_of gty in
877   let rec aux acc = function
878    | [] -> (* Ncic_termSet.elements *) acc
879    | (_::tl) as k ->
880        try 
881          let idx = List.assoc(*q*) k th in
882          let acc = Ncic_termSet.union acc 
883            (InvRelDiscriminationTree.retrieve_unifiables idx gty)
884          in
885          aux acc tl
886        with Not_found -> aux acc tl
887   in
888     aux Ncic_termSet.empty c
889 ;;
890
891 type flags = {
892         do_types : bool; (* solve goals in Type *)
893         last : bool; (* last goal: take first solution only  *)
894         candidates: Ast.term list option;
895         maxwidth : int;
896         maxsize  : int;
897         maxdepth : int;
898 }
899
900 type cache =
901     {facts : th_cache; (* positive results *)
902      under_inspection : cic_term list * th_cache; (* to prune looping *)
903      failures : th_cache; (* to avoid repetitions *)
904      unit_eq : NCicParamod.state;
905      trace: Ast.term list
906     }
907
908 let add_to_trace status ~depth cache t =
909   match t with
910     | Ast.NRef _ -> 
911         debug_print ~depth (lazy ("Adding to trace: " ^ NotationPp.pp_term status t));
912         {cache with trace = t::cache.trace}
913     | Ast.NCic _  (* local candidate *)
914     | _  -> (*not an application *) cache 
915
916 let pptrace status tr = 
917   (lazy ("Proof Trace: " ^ (String.concat ";" 
918                               (List.map (NotationPp.pp_term status) tr))))
919 (* not used
920 let remove_from_trace cache t =
921   match t with
922     | Ast.NRef _ -> 
923         (match cache.trace with 
924            |  _::tl -> {cache with trace = tl}
925            | _ -> assert false)
926     | Ast.NCic _  (* local candidate *)
927     |  _  -> (*not an application *) cache *)
928
929 type sort = T | P
930 type goal = int * sort (* goal, depth, sort *)
931 type fail = goal * cic_term
932 type candidate = int * Ast.term (* unique candidate number, candidate *)
933
934 exception Gaveup of th_cache (* failure cache *)
935 exception Proved of NTacStatus.tac_status * Ast.term list
936
937 (* let close_failures _ c = c;; *)
938 (* let prunable _ _ _ = false;; *)
939 (* let cache_examine cache gty = `Notfound;; *)
940 (* let put_in_subst s _ _ _  = s;; *)
941 (* let add_to_cache_and_del_from_orlist_if_green_cut _ _ c _ _ o f _ = c, o, f, false ;; *)
942 (* let cache_add_underinspection c _ _ = c;; *)
943
944 let init_cache ?(facts=[]) ?(under_inspection=[],[])
945     ?(failures=[])
946     ?(unit_eq=NCicParamod.empty_state) 
947     ?(trace=[]) 
948     _ = 
949     {facts = facts;
950      failures = failures;
951      under_inspection = under_inspection;
952      unit_eq = unit_eq;
953      trace = trace}
954
955 let only signature _context candidate = true
956 (*
957         (* TASSI: nel trie ci mettiamo solo il body, non il ty *)
958   let candidate_ty = 
959    NCicTypeChecker.typeof ~subst:[] ~metasenv:[] [] candidate
960   in
961   let height = fast_height_of_term status candidate_ty in
962   let rc = signature >= height in
963   if rc = false then
964     noprint (lazy ("Filtro: " ^ status#ppterm ~context:[] ~subst:[]
965           ~metasenv:[] candidate ^ ": " ^ string_of_int height))
966   else 
967     noprint (lazy ("Tengo: " ^ status#ppterm ~context:[] ~subst:[]
968           ~metasenv:[] candidate ^ ": " ^ string_of_int height));
969
970   rc *)
971 ;; 
972
973 let candidate_no = ref 0;;
974
975 let openg_no status = List.length (head_goals status#stack)
976
977 let sort_candidates status ctx candidates =
978  let _,_,metasenv,subst,_ = status#obj in
979   let branch cand =
980     let status,ct = disambiguate status ctx ("",0,cand) `XTNone in
981     let status,t = term_of_cic_term status ct ctx in
982     let ty = NCicTypeChecker.typeof status subst metasenv ctx t in
983     let res = branch status (mk_cic_term ctx ty) in
984     noprint (lazy ("branch factor for: " ^ (ppterm status ct) ^ " = " 
985                       ^ (string_of_int res)));
986       res
987   in 
988   let candidates = List.map (fun t -> branch t,t) candidates in
989   let candidates = 
990      List.sort (fun (a,_) (b,_) -> a - b) candidates in 
991   let candidates = List.map snd candidates in
992     noprint (lazy ("candidates =\n" ^ (String.concat "\n" 
993         (List.map (NotationPp.pp_term status) candidates))));
994     candidates
995
996 let sort_new_elems l =
997   List.sort (fun (_,s1) (_,s2) -> openg_no s1 - openg_no s2) l
998
999 let rec stack_goals level gs = 
1000   if level = 0 then []
1001   else match gs with 
1002     | [] -> assert false
1003     | (g,_,_,_)::s -> 
1004         let is_open = function
1005           | (_,Continuationals.Stack.Open i) -> Some i
1006           | (_,Continuationals.Stack.Closed _) -> None
1007         in
1008           HExtlib.filter_map is_open g @ stack_goals (level-1) s
1009 ;;
1010
1011 let open_goals level status = stack_goals level status#stack
1012 ;;
1013
1014 let try_candidate ?(smart=0) flags depth status eq_cache ctx t =
1015   try
1016     let old_og_no = List.length (open_goals (depth+1) status) in
1017     debug_print ~depth (lazy ("try " ^ (string_of_int smart) ^ " : "
1018       ^ (NotationPp.pp_term status) t));
1019     let status = 
1020       if smart = 0 then NTactics.apply_tac ("",0,t) status
1021       else if smart = 1 then  
1022         smart_apply_auto ("",0,t) eq_cache status 
1023       else (* smart = 2: both *)
1024         try NTactics.apply_tac ("",0,t) status
1025         with Error _ -> 
1026           smart_apply_auto ("",0,t) eq_cache status 
1027     in
1028 (* FG: this optimization rules out some applications of
1029  * lift_bind (from contribs/lambda_delta/Basic_2/substitution/lift.ma)
1030  *
1031     (* we compare the expected branching with the actual one and
1032        prune the candidate when the latter is larger. The optimization
1033        is meant to rule out stange applications of flexible terms,
1034        such as the application of eq_f that always succeeds.  
1035        There is some gain but less than expected *)
1036     let og_no = List.length (open_goals (depth+1) status) in
1037     let status, cict = disambiguate status ctx ("",0,t) None in
1038     let status,ct = term_of_cic_term status cict ctx in
1039     let _,_,metasenv,subst,_ = status#obj in
1040     let ty = NCicTypeChecker.typeof status subst metasenv ctx ct in
1041     let res = branch status (mk_cic_term ctx ty) in
1042     let diff = og_no - old_og_no in
1043     debug_print (lazy ("expected branching: " ^ (string_of_int res)));
1044     debug_print (lazy ("actual: branching" ^ (string_of_int diff))); 
1045     (* some flexibility *)
1046     if og_no - old_og_no > res then 
1047       (debug_print (lazy ("branch factor for: " ^ (ppterm status cict) ^ " = " 
1048                     ^ (string_of_int res) ^ " vs. " ^ (string_of_int og_no)));
1049        debug_print ~depth (lazy "strange application"); None)
1050     else 
1051 *)      (incr candidate_no; Some ((!candidate_no,t),status))
1052    with Error (msg,exn) -> debug_print ~depth (lazy "failed"); None
1053 ;;
1054
1055 let sort_of status subst metasenv ctx t =
1056   let ty = NCicTypeChecker.typeof status subst metasenv ctx t in
1057   let metasenv',ty = NCicUnification.fix_sorts status metasenv subst ty in
1058    assert (metasenv = metasenv');
1059    NCicTypeChecker.typeof status subst metasenv ctx ty
1060 ;;
1061   
1062 let type0= NUri.uri_of_string ("cic:/matita/pts/Type0.univ")
1063 ;;
1064
1065 let perforate_small status subst metasenv context t =
1066   let rec aux = function
1067     | NCic.Appl (hd::tl) ->
1068         let map t =
1069             let s = sort_of status subst metasenv context t in
1070             match s with
1071               | NCic.Sort(NCic.Type [`Type,u])
1072                   when u=type0 -> NCic.Meta (0,(0,NCic.Irl 0))
1073               | _ -> aux t
1074         in
1075           NCic.Appl (hd::List.map map tl)
1076     | t -> t
1077   in 
1078     aux t
1079 ;;
1080
1081 let get_cands retrieve_for diff empty gty weak_gty =
1082   let cands = retrieve_for gty in
1083     match weak_gty with
1084       | None -> cands, empty
1085       | Some weak_gty ->
1086           let more_cands =  retrieve_for weak_gty in
1087             cands, diff more_cands cands
1088 ;;
1089
1090 let get_candidates ?(smart=true) ~pfailed depth flags status cache signature gty =
1091   let universe = status#auto_cache in
1092   let _,_,metasenv,subst,_ = status#obj in
1093   let context = ctx_of gty in
1094   let _, raw_gty = term_of_cic_term status gty context in
1095   let is_prod, is_eq =   
1096   let status, t = term_of_cic_term status gty context  in 
1097   let t = NCicReduction.whd status subst context t in
1098     match t with
1099       | NCic.Prod _ -> true, false
1100       | _ -> false, NCicParamod.is_equation status metasenv subst context t 
1101   in
1102   debug_print ~depth (lazy ("gty:" ^ NTacStatus.ppterm status gty));
1103   let is_eq = 
1104     NCicParamod.is_equation status metasenv subst context raw_gty 
1105   in
1106   let raw_weak_gty, weak_gty  =
1107     if smart then
1108       match raw_gty with
1109         | NCic.Appl _ 
1110         | NCic.Const _ 
1111         | NCic.Rel _ -> 
1112             let raw_weak = 
1113               perforate_small status subst metasenv context raw_gty in
1114             let weak = mk_cic_term context raw_weak in
1115             noprint ~depth (lazy ("weak_gty:" ^ NTacStatus.ppterm status weak));
1116               Some raw_weak, Some (weak)
1117         | _ -> None,None
1118     else None,None
1119   in
1120   (* we now compute global candidates *)
1121   let global_cands, smart_global_cands =
1122     let mapf s = 
1123       let to_ast = function 
1124         | NCic.Const r when true 
1125              (*is_relevant statistics r*) -> Some (Ast.NRef r)
1126      (* | NCic.Const _ -> None  *)
1127         | _ -> assert false in
1128           HExtlib.filter_map 
1129             to_ast (NDiscriminationTree.TermSet.elements s) in
1130       let g,l = 
1131         get_cands
1132           (NDiscriminationTree.DiscriminationTree.retrieve_unifiables universe)
1133           NDiscriminationTree.TermSet.diff 
1134           NDiscriminationTree.TermSet.empty
1135           raw_gty raw_weak_gty in
1136       mapf g, mapf l in
1137   (* we now compute local candidates *)
1138   let local_cands,smart_local_cands = 
1139     let mapf s = 
1140       let to_ast t =
1141         let _status, t = term_of_cic_term status t context 
1142         in Ast.NCic t in
1143         List.map to_ast (Ncic_termSet.elements s) in
1144     let g,l = 
1145       get_cands
1146         (fun ty -> search_in_th ty cache)
1147         Ncic_termSet.diff  Ncic_termSet.empty gty weak_gty in
1148       mapf g, mapf l in
1149   (* we now splits candidates in facts or not facts *)
1150   let test = is_a_fact_ast status subst metasenv context in
1151   let by,given_candidates =
1152     match flags.candidates with
1153     | Some l -> true, l
1154     | None -> false, [] in
1155 (* we compute candidates to be applied in normal mode, splitted in
1156      facts and not facts *)
1157   let candidates_facts,candidates_other =
1158     let gl1,gl2 = List.partition test global_cands in
1159     let ll1,ll2 = List.partition test local_cands in
1160     (* if the goal is an equation and paramodulation did not fail
1161      we avoid to apply unit equalities; refl is an
1162      exception since it prompts for convertibility *)
1163     let l1 = if is_eq && (not pfailed) 
1164       then [Ast.Ident("refl",None)] else gl1@ll1 in 
1165     let l2 = 
1166       (* if smart given candidates are applied in smart mode *)
1167       if by && smart then ll2
1168       else if by then given_candidates@ll2 
1169       else gl2@ll2
1170     in l1,l2
1171   in
1172   (* we now compute candidates to be applied in smart mode, splitted in
1173      facts and not facts *) 
1174   let smart_candidates_facts, smart_candidates_other =
1175     if is_prod || not(smart) then [],[] 
1176     else 
1177     let sgl1,sgl2 = List.partition test smart_global_cands in
1178     let sll1,sll2 = List.partition test smart_local_cands in
1179     let l1 = if is_eq then [] else sgl1@sll1 in
1180     let l2 = 
1181       if by && smart then given_candidates@sll2 
1182       else if by then sll2
1183       else sgl2@sll2
1184     in l1,l2
1185   in
1186   candidates_facts,
1187   smart_candidates_facts,
1188   sort_candidates status context (candidates_other),
1189   sort_candidates status context (smart_candidates_other)
1190 ;;
1191
1192 let applicative_case ~pfailed depth signature status flags gty cache =
1193   app_counter:= !app_counter+1; 
1194   let _,_,metasenv,subst,_ = status#obj in
1195   let context = ctx_of gty in
1196   let tcache = cache.facts in
1197   let is_prod, is_eq =   
1198     let status, t = term_of_cic_term status gty context  in 
1199     let t = NCicReduction.whd status subst context t in
1200       match t with
1201         | NCic.Prod _ -> true, false
1202         | _ -> false, NCicParamod.is_equation status metasenv subst context t 
1203   in
1204   debug_print ~depth (lazy (string_of_bool is_eq)); 
1205   (* new *)
1206   let candidates_facts, smart_candidates_facts, 
1207       candidates_other, smart_candidates_other = 
1208     get_candidates ~smart:true ~pfailed depth 
1209       flags status tcache signature gty 
1210   in
1211   let sm = if is_eq || is_prod then 0 else 2 in
1212   let sm1 = if flags.last then 2 else 0 in 
1213   let maxd = (depth + 1 = flags.maxdepth) in 
1214   let try_candidates only_one sm acc candidates =
1215     List.fold_left 
1216       (fun elems cand ->
1217          if (only_one && (elems <> [])) then elems 
1218          else
1219            match try_candidate (~smart:sm) 
1220              flags depth status cache.unit_eq context cand with
1221                | None -> elems
1222                | Some x -> x::elems)
1223       acc candidates
1224   in 
1225   (* if the goal is the last one we stop at the first fact *)
1226   let elems = try_candidates flags.last sm [] candidates_facts in
1227   (* now we add smart_facts *)
1228   let elems = try_candidates flags.last sm elems smart_candidates_facts in
1229   (* if we are at maxdepth and the goal is not a product we are done 
1230      similarly, if the goal is the last one and we already found a
1231      solution *)
1232   if (maxd && not(is_prod)) || (flags.last && elems<>[]) then elems
1233   else
1234     let elems = try_candidates false 2 elems candidates_other in
1235     debug_print ~depth (lazy ("not facts: try smart application"));
1236     try_candidates false 2 elems smart_candidates_other
1237 ;;
1238
1239 exception Found
1240 ;;
1241
1242 (* gty is supposed to be meta-closed *)
1243 let is_subsumed depth filter_depth status gty cache =
1244   if cache=[] then false else (
1245   debug_print ~depth (lazy("Subsuming " ^ (ppterm status gty))); 
1246   let n,h,metasenv,subst,obj = status#obj in
1247   let ctx = ctx_of gty in
1248   let _ , raw_gty = term_of_cic_term status gty ctx in
1249   let target = NCicSubstitution.lift status 1 raw_gty in 
1250   (* we compute candidates using the perforated type *)
1251   let weak_gty  =
1252     match target with
1253       | NCic.Appl _ 
1254       | NCic.Const _ 
1255       | NCic.Rel _ -> 
1256           let raw_weak = 
1257             perforate_small status subst metasenv ctx raw_gty in
1258           let weak = mk_cic_term ctx raw_weak in
1259           debug_print ~depth (lazy ("weak_gty:" ^ NTacStatus.ppterm status weak));
1260           Some (weak)
1261       | _ -> None
1262   in
1263   (* candidates must only be searched w.r.t the given context *)
1264   let candidates = 
1265     try
1266     let idx = List.assq ctx cache in
1267     match weak_gty with
1268       | Some weak ->
1269           Ncic_termSet.elements 
1270             (InvRelDiscriminationTree.retrieve_unifiables idx weak)
1271       |None -> []
1272     with Not_found -> []
1273   in
1274   (* this is a dirty trick: the first argument of an application is used
1275      to remember at which depth a goal failed *)
1276   let filter t = 
1277     let ctx = ctx_of t in 
1278     let _, src = term_of_cic_term status t ctx in 
1279     match src with 
1280      | NCic.Appl [NCic.Implicit (`Typeof d); t] 
1281        when d <= depth -> Some (mk_cic_term ctx t)
1282      | _ -> None in
1283   let candidates = 
1284     if filter_depth then HExtlib.filter_map filter candidates else candidates in  
1285   debug_print ~depth
1286     (lazy ("failure candidates: " ^ string_of_int (List.length candidates)));
1287     try
1288       List.iter
1289         (fun t ->
1290            let _ , source = term_of_cic_term status t ctx in
1291            let implication = 
1292              NCic.Prod("foo",source,target) in
1293            let metasenv,j,_,_ = 
1294              NCicMetaSubst.mk_meta  
1295                metasenv ctx ~with_type:implication `IsType in
1296            let status = status#set_obj (n,h,metasenv,subst,obj) in
1297            let status = status#set_stack [([1,Open j],[],[],`NoTag)] in 
1298            try
1299              let status = NTactics.intro_tac "foo" status in
1300              let status =
1301                NTactics.apply_tac ("",0,Ast.NCic (NCic.Rel 1)) status
1302              in 
1303                if (head_goals status#stack = []) then raise Found
1304                else ()
1305            with
1306              | Error _ -> ())
1307         candidates;false
1308     with Found -> debug_print ~depth (lazy "success");true)
1309 ;;
1310
1311 let rec guess_name name ctx = 
1312   if name = "_" then guess_name "auto" ctx else
1313   if not (List.mem_assoc name ctx) then name else
1314   guess_name (name^"'") ctx
1315 ;;
1316
1317 let is_prod status = 
1318   let _, ctx, gty = current_goal status in
1319   let status, gty = apply_subst status ctx gty in
1320   let _, raw_gty = term_of_cic_term status gty ctx in
1321   match raw_gty with
1322     | NCic.Prod (name,src,_) ->
1323         let status, src = whd status ~delta:0 ctx (mk_cic_term ctx src) in 
1324         (match snd (term_of_cic_term status src ctx) with
1325         | NCic.Const(NReference.Ref (_,NReference.Ind _) as r) 
1326         | NCic.Appl (NCic.Const(NReference.Ref (_,NReference.Ind _) as r)::_) ->
1327             let _,_,itys,_,_ = NCicEnvironment.get_checked_indtys status r in
1328             (match itys with
1329             (* | [_,_,_,[_;_]]  con nat va, ovviamente, in loop *)
1330             | [_,_,_,[_]] 
1331             | [_,_,_,[]] -> `Inductive (guess_name name ctx)         
1332             | _ -> `Some (guess_name name ctx))
1333         | _ -> `Some (guess_name name ctx))
1334     | _ -> `None
1335
1336 let intro ~depth status facts name =
1337   let status = NTactics.intro_tac name status in
1338   let _, ctx, ngty = current_goal status in
1339   let t = mk_cic_term ctx (NCic.Rel 1) in
1340   let status, keys = keys_of_term status t in
1341   let facts = List.fold_left (add_to_th t) facts keys in
1342     debug_print ~depth (lazy ("intro: "^ name));
1343   (* unprovability is not stable w.r.t introduction *)
1344   status, facts
1345 ;;
1346
1347 let rec intros_facts ~depth status facts =
1348   if List.length (head_goals status#stack) <> 1 then status, facts else
1349   match is_prod status with
1350     | `Inductive name 
1351     | `Some(name) ->
1352         let status,facts =
1353           intro ~depth status facts name
1354         in intros_facts ~depth status facts
1355 (*    | `Inductive name ->
1356           let status = NTactics.case1_tac name status in
1357           intros_facts ~depth status facts *)
1358     | _ -> status, facts
1359 ;; 
1360
1361 let intros ~depth status cache =
1362     match is_prod status with
1363       | `Inductive _
1364       | `Some _ ->
1365           let trace = cache.trace in
1366           let status,facts =
1367             intros_facts ~depth status cache.facts 
1368           in 
1369           if head_goals status#stack = [] then 
1370             let status = NTactics.merge_tac status in
1371             [(0,Ast.Ident("__intros",None)),status], cache
1372           else
1373             (* we reindex the equation from scratch *)
1374             let unit_eq = index_local_equations status#eq_cache status in
1375             let status = NTactics.merge_tac status in
1376             [(0,Ast.Ident("__intros",None)),status], 
1377             init_cache ~facts ~unit_eq () ~trace
1378       | _ -> [],cache
1379 ;;
1380
1381 let reduce ~whd ~depth status g = 
1382   let n,h,metasenv,subst,o = status#obj in 
1383   let attr, ctx, ty = NCicUtils.lookup_meta g metasenv in
1384   let ty = NCicUntrusted.apply_subst status subst ctx ty in
1385   let ty' =
1386    (if whd then NCicReduction.whd else NCicTacReduction.normalize) status ~subst ctx ty
1387   in
1388   if ty = ty' then []
1389   else
1390     (debug_print ~depth 
1391       (lazy ("reduced to: "^ status#ppterm ctx subst metasenv ty'));
1392     let metasenv = 
1393       (g,(attr,ctx,ty'))::(List.filter (fun (i,_) -> i<>g) metasenv) 
1394     in
1395     let status = status#set_obj (n,h,metasenv,subst,o) in
1396     (* we merge to gain a depth level; the previous goal level should
1397        be empty *)
1398     let status = NTactics.merge_tac status in
1399     incr candidate_no;
1400     [(!candidate_no,Ast.Ident("__whd",None)),status])
1401 ;;
1402
1403 let is_meta status gty =
1404   let _, ty = term_of_cic_term status gty (ctx_of gty) in
1405   match ty with
1406   | NCic.Meta _ -> true
1407   | _ -> false 
1408 ;;
1409
1410 let do_something signature flags status g depth gty cache =
1411   (* if the goal is meta we close it with I:True. This should work
1412     thanks to the toplogical sorting of goals. *)
1413   if is_meta status gty then
1414     let t = Ast.Ident("I",None) in
1415     debug_print (lazy ("using default term" ^ (NotationPp.pp_term status) t));
1416     let s = NTactics.apply_tac ("",0,t) status in
1417     [(0,t),s], cache
1418   else 
1419   let l0, cache = intros ~depth status cache in
1420   if l0 <> [] then l0, cache
1421   else
1422   (* whd *)
1423   let l = reduce ~whd:true ~depth status g in
1424   (* if l <> [] then l,cache else *)
1425   (* backward aplications *)
1426   let l1 = 
1427     List.map 
1428       (fun s ->
1429          incr candidate_no;
1430          ((!candidate_no,Ast.Ident("__paramod",None)),s))
1431       (auto_eq_check cache.unit_eq status) 
1432   in
1433   let l2 = 
1434     if ((l1 <> []) && flags.last) then [] else
1435     applicative_case ~pfailed:(l1=[]) depth signature status flags gty cache 
1436   in
1437   (* statistics *)
1438   List.iter 
1439     (fun ((_,t),_) -> toref incr_nominations statistics t) l2;
1440   (* states in l1 have have an empty set of subgoals: no point to sort them *)
1441   debug_print ~depth 
1442     (lazy ("alternatives = " ^ (string_of_int (List.length (l1@l@l2)))));
1443     (* we order alternatives w.r.t the number of subgoals they open *)
1444     l1 @ (sort_new_elems l2) @ l, cache 
1445 ;;
1446
1447 let pp_goal = function
1448   | (_,Continuationals.Stack.Open i) 
1449   | (_,Continuationals.Stack.Closed i) -> string_of_int i 
1450 ;;
1451
1452 let pp_goals status l =
1453   String.concat ", " 
1454     (List.map 
1455        (fun i -> 
1456           let gty = get_goalty status i in
1457             NTacStatus.ppterm status gty)
1458        l)
1459 ;;
1460
1461 module M = 
1462   struct 
1463     type t = int
1464     let compare = Pervasives.compare
1465   end
1466 ;;
1467
1468 module MS = HTopoSort.Make(M)
1469 ;;
1470
1471 let sort_tac status =
1472   let gstatus = 
1473     match status#stack with
1474     | [] -> assert false
1475     | (goals, t, k, tag) :: s ->
1476         let g = head_goals status#stack in
1477         let sortedg = 
1478           (List.rev (MS.topological_sort g (deps status))) in
1479           noprint (lazy ("old g = " ^ 
1480             String.concat "," (List.map string_of_int g)));
1481           noprint (lazy ("sorted goals = " ^ 
1482             String.concat "," (List.map string_of_int sortedg)));
1483           let is_it i = function
1484             | (_,Continuationals.Stack.Open j ) 
1485             | (_,Continuationals.Stack.Closed j ) -> i = j
1486           in 
1487           let sorted_goals = 
1488             List.map (fun i -> List.find (is_it i) goals) sortedg
1489           in
1490             (sorted_goals, t, k, tag) :: s
1491   in
1492    status#set_stack gstatus
1493 ;;
1494   
1495 let clean_up_tac status =
1496   let gstatus = 
1497     match status#stack with
1498     | [] -> assert false
1499     | (g, t, k, tag) :: s ->
1500         let is_open = function
1501           | (_,Continuationals.Stack.Open _) -> true
1502           | (_,Continuationals.Stack.Closed _) -> false
1503         in
1504         let g' = List.filter is_open g in
1505           (g', t, k, tag) :: s
1506   in
1507    status#set_stack gstatus
1508 ;;
1509
1510 let focus_tac focus status =
1511   let gstatus = 
1512     match status#stack with
1513     | [] -> assert false
1514     | (g, t, k, tag) :: s ->
1515         let in_focus = function
1516           | (_,Continuationals.Stack.Open i) 
1517           | (_,Continuationals.Stack.Closed i) -> List.mem i focus
1518         in
1519         let focus,others = List.partition in_focus g
1520         in
1521           (* we need to mark it as a BranchTag, otherwise cannot merge later *)
1522           (focus,[],[],`BranchTag) :: (others, t, k, tag) :: s
1523   in
1524    status#set_stack gstatus
1525 ;;
1526
1527 let deep_focus_tac level focus status =
1528   let in_focus = function
1529     | (_,Continuationals.Stack.Open i) 
1530     | (_,Continuationals.Stack.Closed i) -> List.mem i focus
1531   in
1532   let rec slice level gs = 
1533     if level = 0 then [],[],gs else
1534       match gs with 
1535         | [] -> assert false
1536         | (g, t, k, tag) :: s ->
1537             let f,o,gs = slice (level-1) s in           
1538             let f1,o1 = List.partition in_focus g
1539             in
1540             (f1,[],[],`BranchTag)::f, (o1, t, k, tag)::o, gs
1541   in
1542   let gstatus = 
1543     let f,o,s = slice level status#stack in f@o@s
1544   in
1545    status#set_stack gstatus
1546 ;;
1547
1548 let move_to_side level status =
1549 match status#stack with
1550   | [] -> assert false
1551   | (g,_,_,_)::tl ->
1552       let is_open = function
1553           | (_,Continuationals.Stack.Open i) -> Some i
1554           | (_,Continuationals.Stack.Closed _) -> None
1555         in 
1556       let others = menv_closure status (stack_goals (level-1) tl) in
1557       List.for_all (fun i -> IntSet.mem i others) 
1558         (HExtlib.filter_map is_open g)
1559
1560 let top_cache ~depth top status cache =
1561   if top then
1562     let unit_eq = index_local_equations status#eq_cache status in 
1563     {cache with unit_eq = unit_eq}
1564   else cache
1565
1566 let rec auto_clusters ?(top=false)  
1567     flags signature cache depth status : unit =
1568   debug_print ~depth (lazy ("entering auto clusters at depth " ^
1569                            (string_of_int depth)));
1570   debug_print ~depth (pptrace status cache.trace);
1571   (* ignore(Unix.select [] [] [] 0.01); *)
1572   let status = clean_up_tac status in
1573   let goals = head_goals status#stack in
1574   if goals = [] then 
1575     if depth = 0 then raise (Proved (status, cache.trace))
1576     else 
1577       let status = NTactics.merge_tac status in
1578         let cache =
1579         let l,tree = cache.under_inspection in
1580           match l with 
1581             | [] -> cache (* possible because of intros that cleans the cache *)
1582             | a::tl -> let tree = rm_from_th a tree a in
1583               {cache with under_inspection = tl,tree} 
1584         in 
1585          auto_clusters flags signature cache (depth-1) status
1586   else if List.length goals < 2 then
1587     let cache = top_cache ~depth top status cache in
1588     auto_main flags signature cache depth status
1589   else
1590     let all_goals = open_goals (depth+1) status in
1591     debug_print ~depth (lazy ("goals = " ^ 
1592       String.concat "," (List.map string_of_int all_goals)));
1593     let classes = HExtlib.clusters (deps status) all_goals in
1594     (* if any of the classes exceed maxwidth we fail *)
1595     List.iter
1596       (fun gl ->
1597          if List.length gl > flags.maxwidth then 
1598            begin
1599              debug_print ~depth (lazy "FAIL GLOBAL WIDTH"); 
1600              HLog.warn (sprintf "global width (%u) exceeded: %u"
1601                flags.maxwidth (List.length gl));
1602              raise (Gaveup cache.failures)
1603            end else ()) classes;
1604     if List.length classes = 1 then
1605       let flags = 
1606         {flags with last = (List.length all_goals = 1)} in 
1607         (* no need to cluster *)
1608       let cache = top_cache ~depth top status cache in
1609         auto_main flags signature cache depth status 
1610     else
1611       let classes = if top then List.rev classes else classes in
1612       debug_print ~depth
1613         (lazy 
1614            (String.concat "\n" 
1615            (List.map
1616              (fun l -> 
1617                ("cluster:" ^ String.concat "," (List.map string_of_int l)))
1618            classes)));
1619       (* we now process each cluster *)
1620       let status,cache,b = 
1621         List.fold_left
1622           (fun (status,cache,b) gl ->
1623              let flags = 
1624                {flags with last = (List.length gl = 1)} in 
1625              let lold = List.length status#stack in 
1626               debug_print ~depth (lazy ("stack length = " ^ 
1627                         (string_of_int lold)));
1628              let fstatus = deep_focus_tac (depth+1) gl status in
1629              let cache = top_cache ~depth top fstatus cache in
1630              try 
1631                debug_print ~depth (lazy ("focusing on" ^ 
1632                               String.concat "," (List.map string_of_int gl)));
1633                auto_main flags signature cache depth fstatus; assert false
1634              with 
1635                | Proved(status,trace) -> 
1636                    let status = NTactics.merge_tac status in
1637                    let cache = {cache with trace = trace} in
1638                    let lnew = List.length status#stack in 
1639                      assert (lold = lnew);
1640                    (status,cache,true)
1641                | Gaveup failures when top ->
1642                    let cache = {cache with failures = failures} in
1643                    (status,cache,b)
1644           )
1645           (status,cache,false) classes
1646       in
1647       let rec final_merge n s =
1648         if n = 0 then s else final_merge (n-1) (NTactics.merge_tac s)
1649       in let status = final_merge depth status 
1650       in if b then raise (Proved(status,cache.trace)) else raise (Gaveup cache.failures)
1651
1652 and
1653         
1654 (* BRAND NEW VERSION *)         
1655 auto_main flags signature cache depth status: unit =
1656   debug_print ~depth (lazy "entering auto main");
1657   debug_print ~depth (pptrace status cache.trace);
1658   debug_print ~depth (lazy ("stack length = " ^ 
1659                         (string_of_int (List.length status#stack))));
1660   (* ignore(Unix.select [] [] [] 0.01); *)
1661   let status = sort_tac (clean_up_tac status) in
1662   let goals = head_goals status#stack in
1663   match goals with
1664     | [] when depth = 0 -> raise (Proved (status,cache.trace))
1665     | []  -> 
1666         let status = NTactics.merge_tac status in
1667         let cache =
1668           let l,tree = cache.under_inspection in
1669             match l with 
1670               | [] -> cache (* possible because of intros that cleans the cache *)
1671               | a::tl -> let tree = rm_from_th a tree a in
1672                   {cache with under_inspection = tl,tree} 
1673         in 
1674           auto_clusters flags signature cache (depth-1) status
1675     | orig::_ ->
1676         if depth > 0 && move_to_side depth status
1677         then 
1678           let status = NTactics.merge_tac status in
1679           let cache =
1680             let l,tree = cache.under_inspection in
1681               match l with 
1682                 | [] -> cache (* possible because of intros that cleans the cache*)
1683                 | a::tl -> let tree = rm_from_th a tree a in
1684                     {cache with under_inspection = tl,tree} 
1685           in 
1686             auto_clusters flags signature cache (depth-1) status 
1687         else
1688         let ng = List.length goals in
1689         (* moved inside auto_clusters *)
1690         if ng > flags.maxwidth then begin 
1691           debug_print ~depth (lazy "FAIL LOCAL WIDTH");
1692           HLog.warn (sprintf "local width (%u) exceeded: %u"
1693              flags.maxwidth ng);
1694           raise (Gaveup cache.failures)
1695         end else if depth = flags.maxdepth then
1696           raise (Gaveup cache.failures)
1697         else 
1698         let status = NTactics.branch_tac ~force:true status in
1699         let g,gctx, gty = current_goal status in
1700         let ctx,ty = close status g in
1701         let closegty = mk_cic_term ctx ty in
1702         let status, gty = apply_subst status gctx gty in
1703         debug_print ~depth (lazy("Attacking goal " ^ 
1704           string_of_int g ^ " : "^ppterm status gty));
1705         debug_print ~depth (lazy ("current failures: " ^ 
1706           string_of_int (List.length (all_elements ctx cache.failures))));
1707         let is_eq =
1708            let _,_,metasenv,subst,_ = status#obj in
1709            NCicParamod.is_equation status metasenv subst ctx ty in
1710         (* if the goal is an equality we artificially raise its depth up to
1711            flags.maxdepth - 1 *)
1712         if (not flags.last && is_eq && (depth < (flags.maxdepth -2))) then
1713         (* for efficiency reasons, in this case we severely cripple the
1714            search depth *)
1715           (debug_print ~depth (lazy ("RAISING DEPTH TO " ^ string_of_int (depth+1)));
1716            auto_main flags signature cache (depth+1) status)
1717         (* check for loops *)
1718         else if is_subsumed depth false status closegty (snd cache.under_inspection) then 
1719           (debug_print ~depth (lazy "SUBSUMED");
1720            raise (Gaveup cache.failures))
1721         (* check for failures *)
1722         else if is_subsumed depth true status closegty cache.failures then 
1723           (debug_print ~depth (lazy "ALREADY MET");
1724            raise (Gaveup cache.failures))
1725         else
1726         let new_sig = height_of_goal g status in
1727         if new_sig < signature then 
1728           (debug_print  ~depth (lazy ("news = " ^ (string_of_int new_sig)));
1729            debug_print  ~depth (lazy ("olds = " ^ (string_of_int signature)))); 
1730         let alternatives, cache = 
1731           do_something signature flags status g depth gty cache in
1732         let loop_cache =
1733           if flags.last then
1734             let l,tree = cache.under_inspection in
1735             let l,tree = closegty::l, add_to_th closegty tree closegty in
1736             {cache with under_inspection = l,tree}
1737           else cache in 
1738         let failures =
1739           List.fold_left  
1740           (fun allfailures ((_,t),status) ->
1741              debug_print ~depth 
1742                (lazy ("(re)considering goal " ^ 
1743                        (string_of_int g) ^" : "^ppterm status gty)); 
1744              debug_print (~depth:depth) 
1745                (lazy ("Case: " ^ NotationPp.pp_term status t));
1746              let depth,cache =
1747                if t=Ast.Ident("__whd",None) || 
1748                   t=Ast.Ident("__intros",None) 
1749                then depth, cache 
1750                else depth+1,loop_cache in 
1751              let cache = add_to_trace status ~depth cache t in
1752              let cache = {cache with failures = allfailures} in
1753              try
1754                auto_clusters flags signature cache depth status;
1755                assert false;
1756              with Gaveup fail ->
1757                debug_print ~depth (lazy "Failed");
1758                fail)
1759           cache.failures alternatives in
1760         let failures =
1761           if flags.last then 
1762             let newfail =
1763               let dty = NCic.Appl [NCic.Implicit (`Typeof depth); ty] in
1764               mk_cic_term ctx dty 
1765             in 
1766             (*prerr_endline ("FAILURE : " ^ ppterm status gty);*)
1767             add_to_th newfail failures closegty
1768           else failures in
1769         debug_print ~depth (lazy "no more candidates");
1770         raise (Gaveup failures)
1771 ;;
1772
1773 let int name l def = 
1774   try int_of_string (List.assoc name l)
1775   with Failure _ | Not_found -> def
1776 ;;
1777
1778 module AstSet = Set.Make(struct type t = Ast.term let compare = compare end)
1779
1780 let cleanup_trace s trace =
1781   (* removing duplicates *)
1782   let trace_set = 
1783     List.fold_left 
1784       (fun acc t -> AstSet.add t acc)
1785       AstSet.empty trace in
1786   let trace = AstSet.elements trace_set
1787     (* filtering facts *)
1788   in List.filter 
1789        (fun t -> 
1790           match t with
1791             | Ast.NRef (NReference.Ref (u,_)) -> not (is_a_fact_obj s u)
1792             | _ -> false) trace
1793 ;;
1794
1795 let auto_tac ~params:(univ,flags) ?(trace_ref=ref []) status =
1796   let oldstatus = status in
1797   let status = (status:> NTacStatus.tac_status) in
1798   let goals = head_goals status#stack in
1799   let status, facts = mk_th_cache status goals in
1800 (*  let unit_eq = index_local_equations status#eq_cache status in *)
1801   let cache = init_cache ~facts () in 
1802 (*   pp_th status facts; *)
1803 (*
1804   NDiscriminationTree.DiscriminationTree.iter status#auto_cache (fun p t -> 
1805     debug_print (lazy(
1806       NDiscriminationTree.NCicIndexable.string_of_path p ^ " |--> " ^
1807       String.concat "\n    " (List.map (
1808       status#ppterm ~metasenv:[] ~context:[] ~subst:[])
1809         (NDiscriminationTree.TermSet.elements t))
1810       )));
1811 *)
1812   let candidates = 
1813     match univ with
1814       | None -> None 
1815       | Some l -> 
1816           let to_Ast t =
1817 (* FG: `XTSort here? *)   
1818             let status, res = disambiguate status [] t `XTNone in 
1819             let _,res = term_of_cic_term status res (ctx_of res) 
1820             in Ast.NCic res 
1821           in Some (List.map to_Ast l) 
1822   in
1823   let depth = int "depth" flags 3 in 
1824   let size  = int "size" flags 10 in 
1825   let width = int "width" flags 4 (* (3+List.length goals)*) in 
1826   (* XXX fix sort *)
1827 (*   let goals = List.map (fun i -> (i,P)) goals in *)
1828   let signature = height_of_goals status in 
1829   let flags = { 
1830           last = true;
1831           candidates = candidates;
1832           maxwidth = width;
1833           maxsize = size;
1834           maxdepth = depth;
1835           do_types = false; 
1836   } in
1837   let initial_time = Unix.gettimeofday() in
1838   app_counter:= 0;
1839   let rec up_to x y =
1840     if x > y then
1841       (debug_print(lazy
1842         ("TIME ELAPSED:"^string_of_float(Unix.gettimeofday()-.initial_time)));
1843        debug_print(lazy
1844         ("Applicative nodes:"^string_of_int !app_counter)); 
1845        raise (Error (lazy "auto gave up", None)))
1846     else
1847       let _ = debug_print (lazy("\n\nRound "^string_of_int x^"\n")) in
1848       let flags = { flags with maxdepth = x } 
1849       in 
1850         try auto_clusters (~top:true) flags signature cache 0 status;assert false 
1851 (*
1852         try auto_main flags signature cache 0 status;assert false
1853 *)
1854         with
1855           | Gaveup _ -> up_to (x+1) y
1856           | Proved (s,trace) -> 
1857               debug_print (lazy ("proved at depth " ^ string_of_int x));
1858               List.iter (toref incr_uses statistics) trace;
1859               let trace = cleanup_trace s trace in
1860               let _ = debug_print (pptrace status trace) in
1861               let stack = 
1862                 match s#stack with
1863                   | (g,t,k,f) :: rest -> (filter_open g,t,k,f):: rest
1864                   | _ -> assert false
1865               in
1866               let s = s#set_stack stack in
1867                 trace_ref := trace;
1868                 oldstatus#set_status s 
1869   in
1870   let s = up_to depth depth in
1871     debug_print (print_stat status statistics);
1872     debug_print(lazy
1873         ("TIME ELAPSED:"^string_of_float(Unix.gettimeofday()-.initial_time)));
1874     debug_print(lazy
1875         ("Applicative nodes:"^string_of_int !app_counter));
1876     s
1877 ;;
1878
1879 let auto_tac ~params:(_,flags as params) ?trace_ref =
1880   if List.mem_assoc "demod" flags then 
1881     demod_tac ~params 
1882   else if List.mem_assoc "paramod" flags then 
1883     paramod_tac ~params 
1884   else if List.mem_assoc "fast_paramod" flags then 
1885     fast_eq_check_tac ~params  
1886   else auto_tac ~params ?trace_ref
1887 ;;