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.
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_______________________________________________________________ *)
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
19 open Continuationals.Stack
21 module Ast = NotationPt
23 (* ======================= statistics ========================= *)
25 let app_counter = ref 0
28 type t = NReference.reference
30 let compare = Pervasives.compare
31 let hash = Hashtbl.hash
34 module RefHash = Hashtbl.Make(RHT);;
37 nominations : int ref;
41 let statistics: info RefHash.t = RefHash.create 503
43 let incr_nominations tbl item =
45 let v = RefHash.find tbl item in incr v.nominations
47 RefHash.add tbl item {nominations = ref 1; uses = ref 0}
49 let incr_uses tbl item =
51 let v = RefHash.find tbl item in incr v.uses
52 with Not_found -> assert false
58 | Ast.NCic _ (* local candidate *)
61 let is_relevant tbl item =
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
67 with Not_found -> true
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
76 Filename.chop_extension
77 (Filename.basename (NReference.string_of_reference r))
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))
87 (* ======================= utility functions ========================= *)
88 module IntSet = Set.Make(struct type t = int let compare = compare end)
90 let get_sgoalty status g =
91 let _,_,metasenv,subst,_ = status#obj in
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
98 NTacStatus.mk_cic_term ctx ty
99 with NCicUtils.Meta_not_found _ as exn -> fail ~exn (lazy "get_sgoalty")
103 let gty = get_sgoalty status g in
104 metas_of_term status gty
107 let menv_closure status gl =
108 let rec closure acc = function
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
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 *)
126 let _, m = term_of_cic_term status m (ctx_of m) in
128 | NCic.Meta(i,_) -> IntSet.add i acc
132 (* IntSet.subset menv clos *)
133 IntSet.cardinal(IntSet.diff menv clos)
135 let is_a_fact status ty = branch status ty = 0
137 let is_a_fact_obj s uri =
138 let obj = NCicEnvironment.get_checked_obj s uri in
140 | (_,_,[],[],NCic.Constant(_,_,_,ty,_)) ->
141 is_a_fact s (mk_cic_term [] ty)
142 (* aggiungere i costruttori *)
145 let is_a_fact_ast status subst metasenv ctx cand =
147 (lazy ("------- checking " ^ NotationPp.pp_term status cand));
148 let status, t = disambiguate status ctx ("",0,cand) None 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)
153 let current_goal ?(single_goal=true) status =
154 let open_goals = head_goals status#stack in
156 then assert (List.length open_goals = 1)
157 else assert (List.length open_goals >= 1);
158 let open_goal = List.hd open_goals in
159 let gty = get_goalty status open_goal in
160 let ctx = ctx_of gty in
163 let height_of_ref status (NReference.Ref (uri, x)) =
168 | NReference.CoFix _ ->
169 let _,height,_,_,_ = NCicEnvironment.get_checked_obj status uri in
171 | NReference.Def h -> h
172 | NReference.Fix (_,_,h) -> h
175 (*************************** height functions ********************************)
176 let fast_height_of_term status t =
180 NCic.Meta (_,(_,NCic.Ctx l)) -> List.iter aux l
184 | NCic.Implicit _ -> assert false
187 prerr_endline (status#ppterm ~metasenv:[] ~subst:[]
188 ~context:[] t ^ ":" ^ string_of_int (height_of_ref status nref));
190 h := max !h (height_of_ref status nref)
191 | NCic.Prod (_,t1,t2)
192 | NCic.Lambda (_,t1,t2) -> aux t1; aux t2
193 | NCic.LetIn (_,s,ty,t) -> aux s; aux ty; aux t
194 | NCic.Appl l -> List.iter aux l
195 | NCic.Match (_,outty,t,pl) -> aux outty; aux t; List.iter aux pl
200 let height_of_goal g status =
201 let ty = get_goalty status g in
202 let context = ctx_of ty in
203 let _, ty = term_of_cic_term status ty (ctx_of ty) in
204 let h = ref (fast_height_of_term status ty) in
207 | _, NCic.Decl ty -> h := max !h (fast_height_of_term status ty)
208 | _, NCic.Def (bo,ty) ->
209 h := max !h (fast_height_of_term status ty);
210 h := max !h (fast_height_of_term status bo);
216 let height_of_goals status =
217 let open_goals = head_goals status#stack in
218 assert (List.length open_goals > 0);
222 h := max !h (height_of_goal open_goal status))
224 noprint (lazy ("altezza sequente: " ^ string_of_int !h));
228 (* =============================== paramod =========================== *)
229 let solve f status eq_cache goal =
232 if fast then NCicParamod.fast_eq_check
233 else NCicParamod.paramod in
235 let n,h,metasenv,subst,o = status#obj in
236 let gname, ctx, gty = List.assoc goal metasenv in
237 let gty = NCicUntrusted.apply_subst status subst ctx gty in
238 let build_status (pt, _, metasenv, subst) =
240 noprint (lazy ("refining: "^(status#ppterm ctx subst metasenv pt)));
241 let stamp = Unix.gettimeofday () in
242 let metasenv, subst, pt, pty =
243 (* NCicRefiner.typeof status
244 (* (status#set_coerc_db NCicCoercion.empty_db) *)
245 metasenv subst ctx pt None in
246 debug_print (lazy ("refined: "^(status#ppterm ctx subst metasenv pt)));
247 noprint (lazy ("synt: "^(status#ppterm ctx subst metasenv pty)));
248 let metasenv, subst =
249 NCicUnification.unify status metasenv subst ctx gty pty *)
251 (status#set_coerc_db NCicCoercion.empty_db)
252 metasenv subst ctx pt (Some gty)
254 noprint (lazy (Printf.sprintf "Refined in %fs"
255 (Unix.gettimeofday() -. stamp)));
256 let status = status#set_obj (n,h,metasenv,subst,o) in
257 let metasenv = List.filter (fun j,_ -> j <> goal) metasenv in
258 let subst = (goal,(gname,ctx,pt,pty)) :: subst in
259 Some (status#set_obj (n,h,metasenv,subst,o))
261 NCicRefiner.RefineFailure msg
262 | NCicRefiner.Uncertain msg ->
263 debug_print (lazy ("WARNING: refining in fast_eq_check failed\n" ^
264 snd (Lazy.force msg) ^
265 "\n in the environment\n" ^
266 status#ppmetasenv subst metasenv)); None
267 | NCicRefiner.AssertFailure msg ->
268 debug_print (lazy ("WARNING: refining in fast_eq_check failed" ^
270 "\n in the environment\n" ^
271 status#ppmetasenv subst metasenv)); None
274 HExtlib.filter_map build_status
275 (f status metasenv subst ctx eq_cache (NCic.Rel ~-1,gty))
278 let fast_eq_check eq_cache status (goal:int) =
279 match solve NCicParamod.fast_eq_check status eq_cache goal with
280 | [] -> raise (Error (lazy "no proof found",None))
284 let dist_fast_eq_check eq_cache s =
285 NTactics.distribute_tac (fast_eq_check eq_cache) s
288 let auto_eq_check eq_cache status =
290 let s = dist_fast_eq_check eq_cache status in
293 | Error _ -> debug_print (lazy ("no paramod proof found"));[]
296 let index_local_equations eq_cache status =
297 noprint (lazy "indexing equations");
298 let open_goals = head_goals status#stack in
299 let open_goal = List.hd open_goals in
300 let ngty = get_goalty status open_goal in
301 let ctx = apply_subst_context ~fix_projections:true status (ctx_of ngty) in
306 let t = NCic.Rel !c in
308 let ty = NCicTypeChecker.typeof status [] [] ctx t in
309 if is_a_fact status (mk_cic_term ctx ty) then
310 (noprint(lazy("eq indexing " ^ (status#ppterm ctx [] [] ty)));
311 NCicParamod.forward_infer_step status [] [] ctx eq_cache t ty)
313 (noprint (lazy ("not a fact: " ^ (status#ppterm ctx [] [] ty)));
316 | NCicTypeChecker.TypeCheckerFailure _
317 | NCicTypeChecker.AssertFailure _ -> eq_cache)
321 let fast_eq_check_tac ~params s =
322 let unit_eq = index_local_equations s#eq_cache s in
323 dist_fast_eq_check unit_eq s
326 let paramod eq_cache status goal =
327 match solve NCicParamod.paramod status eq_cache goal with
328 | [] -> raise (Error (lazy "no proof found",None))
332 let paramod_tac ~params s =
333 let unit_eq = index_local_equations s#eq_cache s in
334 NTactics.distribute_tac (paramod unit_eq) s
337 let demod eq_cache status goal =
338 match solve NCicParamod.demod status eq_cache goal with
339 | [] -> raise (Error (lazy "no progress",None))
343 let demod_tac ~params s =
344 let unit_eq = index_local_equations s#eq_cache s in
345 NTactics.distribute_tac (demod unit_eq) s
349 let fast_eq_check_tac_all ~params eq_cache status =
350 let g,_,_ = current_goal status in
351 let allstates = fast_eq_check_all status eq_cache g in
352 let pseudo_low_tac s _ _ = s in
353 let pseudo_low_tactics =
354 List.map pseudo_low_tac allstates
356 List.map (fun f -> NTactics.distribute_tac f status) pseudo_low_tactics
361 let demod status eq_cache goal =
362 let n,h,metasenv,subst,o = status#obj in
363 let gname, ctx, gty = List.assoc goal metasenv in
364 let gty = NCicUntrusted.apply_subst subst ctx gty in
366 let demod_tac ~params s =
367 let unit_eq = index_local_equations s#eq_cache s in
368 dist_fast_eq_check unit_eq s
371 (*************** subsumption ****************)
373 let close_wrt_context status =
377 | name, NCic.Decl t -> NCic.Prod(name,t,ty)
378 | name, NCic.Def(bo, _) -> NCicSubstitution.subst status bo ty)
381 let args_for_context ?(k=1) ctx =
384 (fun (n,l) ctx_entry ->
386 | name, NCic.Decl t -> n+1,NCic.Rel(n)::l
387 | name, NCic.Def(bo, _) -> n+1,l)
391 let constant_for_meta status ctx ty i =
392 let name = "cic:/foo"^(string_of_int i)^".con" in
393 let uri = NUri.uri_of_string name in
394 let ty = close_wrt_context status ty ctx in
395 (* prerr_endline (status#ppterm [] [] [] ty); *)
396 let attr = (`Generated,`Definition,`Local) in
397 let obj = NCic.Constant([],name,None,ty,attr) in
398 (* Constant of relevance * string * term option * term * c_attr *)
402 let refresh metasenv =
404 (fun (metasenv,subst) (i,(iattr,ctx,ty)) ->
405 let ikind = NCicUntrusted.kind_of_meta iattr in
406 let metasenv,j,instance,ty =
407 NCicMetaSubst.mk_meta ~attrs:iattr
408 metasenv ctx ~with_type:ty ikind in
409 let s_entry = i,(iattr, ctx, instance, ty) in
410 let metasenv = List.filter (fun x,_ -> i <> x) metasenv in
411 metasenv,s_entry::subst)
412 (metasenv,[]) metasenv
414 (* close metasenv returns a ground instance of all the metas in the
415 metasenv, insantiatied with axioms, and the list of these axioms *)
416 let close_metasenv status metasenv subst =
418 let metasenv = NCicUntrusted.apply_subst_metasenv subst metasenv in
420 let metasenv = NCicUntrusted.sort_metasenv status subst metasenv in
422 (fun (subst,objs) (i,(iattr,ctx,ty)) ->
423 let ty = NCicUntrusted.apply_subst status subst ctx ty in
425 NCicUntrusted.apply_subst_context status ~fix_projections:true
427 let (uri,_,_,_,obj) as okind =
428 constant_for_meta status ctx ty i in
430 NCicEnvironment.check_and_add_obj status okind;
431 let iref = NReference.reference_of_spec uri NReference.Decl in
433 let args = args_for_context ctx in
434 if args = [] then NCic.Const iref
435 else NCic.Appl(NCic.Const iref::args)
437 (* prerr_endline (status#ppterm ctx [] [] iterm); *)
438 let s_entry = i, ([], ctx, iterm, ty)
439 in s_entry::subst,okind::objs
440 with _ -> assert false)
444 let ground_instances status gl =
445 let _,_,metasenv,subst,_ = status#obj in
446 let subset = menv_closure status gl in
447 let submenv = List.filter (fun (x,_) -> IntSet.mem x subset) metasenv in
449 let submenv = metasenv in
451 let subst, objs = close_metasenv status submenv subst in
455 let (_, ctx, t, _) = List.assoc i subst in
456 noprint (lazy (status#ppterm ctx [] [] t));
458 (fun (uri,_,_,_,_) as obj ->
459 NCicEnvironment.invalidate_item status (`Obj (uri, obj)))
464 Not_found -> assert false
468 let replace_meta status i args target =
469 let rec aux k = function
470 (* TODO: local context *)
471 | NCic.Meta (j,lc) when i = j ->
475 List.map (NCicSubstitution.subst_meta status lc) args in
476 NCic.Appl(NCic.Rel k::args))
477 | NCic.Meta (j,lc) as m ->
484 aux k (NCicSubstitution.lift status n t)) l))))
485 | t -> NCicUtils.map status (fun _ k -> k+1) k aux t
490 let close_wrt_metasenv status subst =
492 (fun ty (i,(iattr,ctx,mty)) ->
493 let mty = NCicUntrusted.apply_subst status subst ctx mty in
495 NCicUntrusted.apply_subst_context status ~fix_projections:true
497 let cty = close_wrt_context status mty ctx in
498 let name = "foo"^(string_of_int i) in
499 let ty = NCicSubstitution.lift status 1 ty in
500 let args = args_for_context ~k:1 ctx in
501 (* prerr_endline (status#ppterm ctx [] [] iterm); *)
502 let ty = replace_meta status i args ty
504 NCic.Prod(name,cty,ty))
508 let _,_,metasenv,subst,_ = status#obj in
509 let subset = menv_closure status [g] in
510 let subset = IntSet.remove g subset in
511 let elems = IntSet.elements subset in
512 let _, ctx, ty = NCicUtils.lookup_meta g metasenv in
513 let ty = NCicUntrusted.apply_subst status subst ctx ty in
514 noprint (lazy ("metas in " ^ (status#ppterm ctx [] metasenv ty)));
515 noprint (lazy (String.concat ", " (List.map string_of_int elems)));
516 let submenv = List.filter (fun (x,_) -> IntSet.mem x subset) metasenv in
517 let submenv = List.rev (NCicUntrusted.sort_metasenv status subst submenv) in
519 let submenv = metasenv in
521 let ty = close_wrt_metasenv status subst ty submenv in
522 noprint (lazy (status#ppterm ctx [] [] ty));
526 (****************** smart application ********************)
528 let saturate_to_ref status metasenv subst ctx nref ty =
529 let height = height_of_ref status nref in
530 let rec aux metasenv ty args =
531 let ty,metasenv,moreargs =
532 NCicMetaSubst.saturate status ~delta:height metasenv subst ctx ty 0 in
534 | NCic.Const(NReference.Ref (_,NReference.Def _) as nre)
536 let _, _, bo, _, _, _ = NCicEnvironment.get_checked_def status nre in
537 aux metasenv bo (args@moreargs)
538 | NCic.Appl(NCic.Const(NReference.Ref (_,NReference.Def _) as nre)::tl)
540 let _, _, bo, _, _, _ = NCicEnvironment.get_checked_def status nre in
541 aux metasenv (NCic.Appl(bo::tl)) (args@moreargs)
542 | _ -> ty,metasenv,(args@moreargs)
546 let smart_apply t unit_eq status g =
547 let n,h,metasenv,subst,o = status#obj in
548 let gname, ctx, gty = List.assoc g metasenv in
549 (* let ggty = mk_cic_term context gty in *)
550 let status, t = disambiguate status ctx t None in
551 let status,t = term_of_cic_term status t ctx in
552 let _,_,metasenv,subst,_ = status#obj in
553 let ty = NCicTypeChecker.typeof status subst metasenv ctx t in
554 let ty,metasenv,args =
557 | NCic.Appl(NCic.Const(nref)::_) ->
558 saturate_to_ref status metasenv subst ctx nref ty
560 NCicMetaSubst.saturate status metasenv subst ctx ty 0 in
561 let metasenv,j,inst,_ = NCicMetaSubst.mk_meta metasenv ctx `IsTerm in
562 let status = status#set_obj (n,h,metasenv,subst,o) in
563 let pterm = if args=[] then t else
565 | NCic.Appl l -> NCic.Appl(l@args)
566 | _ -> NCic.Appl(t::args)
568 noprint(lazy("pterm " ^ (status#ppterm ctx [] [] pterm)));
569 noprint(lazy("pty " ^ (status#ppterm ctx [] [] ty)));
572 NUri.uri_of_string "cic:/matita/basics/logic/eq_coerc.con" in
573 let ref = NReference.reference_of_spec uri (NReference.Def(2)) in
577 NCic.Appl[eq_coerc;ty;NCic.Implicit `Type;pterm;inst] in
578 let smart = mk_cic_term ctx smart in
580 let status = instantiate status g smart in
581 let _,_,metasenv,subst,_ = status#obj in
582 let _,ctx,jty = List.assoc j metasenv in
583 let jty = NCicUntrusted.apply_subst status subst ctx jty in
584 noprint(lazy("goal " ^ (status#ppterm ctx [] [] jty)));
585 fast_eq_check unit_eq status j
587 | NCicEnvironment.ObjectNotFound s as e ->
588 raise (Error (lazy "eq_coerc non yet defined",Some e))
589 | Error _ as e -> debug_print (lazy "error"); raise e
591 let compare_statuses ~past ~present =
592 let _,_,past,_,_ = past#obj in
593 let _,_,present,_,_ = present#obj in
594 List.map fst (List.filter (fun (i,_) -> not(List.mem_assoc i past)) present),
595 List.map fst (List.filter (fun (i,_) -> not (List.mem_assoc i present)) past)
598 (* paramodulation has only an implicit knowledge of the symmetry of equality;
599 hence it is in trouble in proving (a = b) = (b = a) *)
600 let try_sym tac status g =
601 (* put the right uri *)
602 let sym_eq = Ast.Appl [Ast.Ident("sym_eq",`Ambiguous); Ast.Implicit `Vector] in
603 let _,_,metasenv,subst,_ = status#obj in
604 let _, context, gty = List.assoc g metasenv in
606 NCicParamod.is_equation status metasenv subst context gty
611 let new_status = instantiate_with_ast status g ("",0,sym_eq) in
612 let go, _ = compare_statuses ~past:status ~present:new_status in
613 assert (List.length go = 1);
614 let ng = List.hd go in
619 let smart_apply_tac t s =
620 let unit_eq = index_local_equations s#eq_cache s in
621 NTactics.distribute_tac (try_sym (smart_apply t unit_eq)) s
622 (* NTactics.distribute_tac (smart_apply t unit_eq) s *)
624 let smart_apply_auto t eq_cache =
625 NTactics.distribute_tac (try_sym (smart_apply t eq_cache))
626 (* NTactics.distribute_tac (smart_apply t eq_cache) *)
629 (****************** types **************)
632 type th_cache = (NCic.context * InvRelDiscriminationTree.t) list
634 (* cartesian: term set list -> term list set *)
637 [] -> NDiscriminationTree.TermListSet.empty
639 NDiscriminationTree.TermSet.fold
640 (fun x acc -> NDiscriminationTree.TermListSet.add [x] acc) l NDiscriminationTree.TermListSet.empty
642 let rest = cartesian tl in
643 NDiscriminationTree.TermSet.fold
645 NDiscriminationTree.TermListSet.fold (fun l acc' -> NDiscriminationTree.TermListSet.add (x::l) acc') rest acc
646 ) he NDiscriminationTree.TermListSet.empty
649 (* all_keys_of_cic_type: term -> term set *)
650 let all_keys_of_cic_type status metasenv subst context ty =
652 (* Here we are dropping the metasenv, but this should not raise any
653 exception (hopefully...) *)
655 NCicMetaSubst.saturate status ~delta:max_int metasenv subst context ty 0
661 NCic.Appl (he::tl) ->
664 let wty = NCicReduction.whd status ~delta:0 ~subst context ty in
666 NDiscriminationTree.TermSet.add ty (aux ty)
668 NDiscriminationTree.TermSet.union
669 (NDiscriminationTree.TermSet.add ty (aux ty))
670 (NDiscriminationTree.TermSet.add wty (aux wty))
673 NDiscriminationTree.TermListSet.fold
674 (fun l acc -> NDiscriminationTree.TermSet.add (NCic.Appl l) acc)
675 (cartesian ((NDiscriminationTree.TermSet.singleton he)::tl'))
676 NDiscriminationTree.TermSet.empty
677 | _ -> NDiscriminationTree.TermSet.empty
679 let ty,ity = saturate ty in
680 let wty,iwty = saturate (NCicReduction.whd status ~delta:0 ~subst context ty) in
682 [ity, NDiscriminationTree.TermSet.add ty (aux ty)]
684 [ity, NDiscriminationTree.TermSet.add ty (aux ty) ;
685 iwty, NDiscriminationTree.TermSet.add wty (aux wty) ]
688 let all_keys_of_type status t =
689 let _,_,metasenv,subst,_ = status#obj in
690 let context = ctx_of t in
691 let status, t = apply_subst status context t in
693 all_keys_of_cic_type status metasenv subst context
694 (snd (term_of_cic_term status t context))
698 (fun (intros,keys) ->
700 NDiscriminationTree.TermSet.fold
701 (fun t acc -> Ncic_termSet.add (mk_cic_term context t) acc)
702 keys Ncic_termSet.empty
707 let keys_of_type status orig_ty =
708 (* Here we are dropping the metasenv (in the status), but this should not
709 raise any exception (hopefully...) *)
710 let _, ty, _ = saturate ~delta:max_int status orig_ty in
711 let _, ty = apply_subst status (ctx_of ty) ty in
714 let orig_ty' = NCicTacReduction.normalize ~subst context orig_ty in
715 if orig_ty' <> orig_ty then
716 let ty',_,_= NCicMetaSubst.saturate ~delta:0 metasenv subst context orig_ty' 0 in
722 (*CSC: strange: we keep ty, ty normalized and ty ~delta:(h-1) *)
724 let _, ty = term_of_cic_term status ty (ctx_of ty) in
726 | NCic.Const (NReference.Ref (_,(NReference.Def h | NReference.Fix (_,_,h))))
727 | NCic.Appl (NCic.Const(NReference.Ref(_,(NReference.Def h | NReference.Fix (_,_,h))))::_)
729 let _,ty,_= saturate status ~delta:(h-1) orig_ty in
736 let all_keys_of_term status t =
737 let status, orig_ty = typeof status (ctx_of t) t in
738 all_keys_of_type status orig_ty
741 let keys_of_term status t =
742 let status, orig_ty = typeof status (ctx_of t) t in
743 keys_of_type status orig_ty
746 let mk_th_cache status gl =
748 (fun (status, acc) g ->
749 let gty = get_goalty status g in
750 let ctx = ctx_of gty in
751 noprint(lazy("th cache for: "^ppterm status gty));
752 noprint(lazy("th cache in: "^ppcontext status ctx));
753 if List.mem_assq ctx acc then status, acc else
754 let idx = InvRelDiscriminationTree.empty in
757 (fun (status, i, idx) _ ->
758 let t = mk_cic_term ctx (NCic.Rel i) in
759 let status, keys = keys_of_term status t in
760 noprint(lazy("indexing: "^ppterm status t ^ ": " ^ string_of_int (List.length keys)));
762 List.fold_left (fun idx k ->
763 InvRelDiscriminationTree.index idx k t) idx keys
768 status, (ctx, idx) :: acc)
772 let all_elements ctx cache =
773 let dummy = mk_cic_term ctx (NCic.Meta (0,(0, (NCic.Irl 0)))) in
775 let idx = List.assq ctx cache in
776 Ncic_termSet.elements
777 (InvRelDiscriminationTree.retrieve_unifiables idx dummy)
780 let add_to_th t c ty =
781 let key_c = ctx_of t in
782 if not (List.mem_assq key_c c) then
783 (key_c ,InvRelDiscriminationTree.index
784 InvRelDiscriminationTree.empty ty t ) :: c
786 let rec replace = function
788 | (x, idx) :: tl when x == key_c ->
789 (x, InvRelDiscriminationTree.index idx ty t) :: tl
790 | x :: tl -> x :: replace tl
795 let rm_from_th t c ty =
796 let key_c = ctx_of t in
797 if not (List.mem_assq key_c c) then assert false
799 let rec replace = function
801 | (x, idx) :: tl when x == key_c ->
802 (x, InvRelDiscriminationTree.remove_index idx ty t) :: tl
803 | x :: tl -> x :: replace tl
808 let pp_idx status idx =
809 InvRelDiscriminationTree.iter idx
811 noprint(lazy("K: " ^ NCicInverseRelIndexable.string_of_path k));
813 (fun t -> debug_print(lazy("\t"^ppterm status t)))
817 let pp_th (status: #NTacStatus.pstatus) =
820 noprint(lazy( "-----------------------------------------------"));
821 noprint(lazy( (status#ppcontext ~metasenv:[] ~subst:[] ctx)));
822 noprint(lazy( "||====> "));
826 let search_in_th gty th =
827 let c = ctx_of gty in
828 let rec aux acc = function
829 | [] -> (* Ncic_termSet.elements *) acc
832 let idx = List.assoc(*q*) k th in
833 let acc = Ncic_termSet.union acc
834 (InvRelDiscriminationTree.retrieve_unifiables idx gty)
837 with Not_found -> aux acc tl
839 aux Ncic_termSet.empty c
843 do_types : bool; (* solve goals in Type *)
844 last : bool; (* last goal: take first solution only *)
845 candidates: Ast.term list option;
853 {facts : th_cache; (* positive results *)
854 under_inspection : cic_term list * th_cache; (* to prune looping *)
855 failures : th_cache; (* to avoid repetitions *)
856 unit_eq : NCicParamod.state;
860 let add_to_trace status ~depth cache t =
863 print ~depth (lazy ("Adding to trace: " ^ NotationPp.pp_term status t));
864 {cache with trace = t::cache.trace}
865 | Ast.NCic _ (* local candidate *)
866 | _ -> (*not an application *) cache
868 let pptrace status tr =
869 (lazy ("Proof Trace: " ^ (String.concat ";"
870 (List.map (NotationPp.pp_term status) tr))))
872 let remove_from_trace cache t =
875 (match cache.trace with
876 | _::tl -> {cache with trace = tl}
878 | Ast.NCic _ (* local candidate *)
879 | _ -> (*not an application *) cache *)
882 type goal = int * sort (* goal, depth, sort *)
883 type fail = goal * cic_term
884 type candidate = int * Ast.term (* unique candidate number, candidate *)
886 exception Gaveup of th_cache (* failure cache *)
887 exception Proved of NTacStatus.tac_status * Ast.term list
889 (* let close_failures _ c = c;; *)
890 (* let prunable _ _ _ = false;; *)
891 (* let cache_examine cache gty = `Notfound;; *)
892 (* let put_in_subst s _ _ _ = s;; *)
893 (* let add_to_cache_and_del_from_orlist_if_green_cut _ _ c _ _ o f _ = c, o, f, false ;; *)
894 (* let cache_add_underinspection c _ _ = c;; *)
896 let init_cache ?(facts=[]) ?(under_inspection=[],[])
898 ?(unit_eq=NCicParamod.empty_state)
903 under_inspection = under_inspection;
907 let only signature _context candidate = true
909 (* TASSI: nel trie ci mettiamo solo il body, non il ty *)
911 NCicTypeChecker.typeof ~subst:[] ~metasenv:[] [] candidate
913 let height = fast_height_of_term status candidate_ty in
914 let rc = signature >= height in
916 noprint (lazy ("Filtro: " ^ status#ppterm ~context:[] ~subst:[]
917 ~metasenv:[] candidate ^ ": " ^ string_of_int height))
919 noprint (lazy ("Tengo: " ^ status#ppterm ~context:[] ~subst:[]
920 ~metasenv:[] candidate ^ ": " ^ string_of_int height));
925 let candidate_no = ref 0;;
927 let openg_no status = List.length (head_goals status#stack)
929 let sort_candidates status ctx candidates =
930 let _,_,metasenv,subst,_ = status#obj in
932 let status,ct = disambiguate status ctx ("",0,cand) None in
933 let status,t = term_of_cic_term status ct ctx in
934 let ty = NCicTypeChecker.typeof status subst metasenv ctx t in
935 let res = branch status (mk_cic_term ctx ty) in
936 noprint (lazy ("branch factor for: " ^ (ppterm status ct) ^ " = "
937 ^ (string_of_int res)));
940 let candidates = List.map (fun t -> branch t,t) candidates in
942 List.sort (fun (a,_) (b,_) -> a - b) candidates in
943 let candidates = List.map snd candidates in
944 noprint (lazy ("candidates =\n" ^ (String.concat "\n"
945 (List.map (NotationPp.pp_term status) candidates))));
948 let sort_new_elems l =
949 List.sort (fun (_,s1) (_,s2) -> openg_no s1 - openg_no s2) l
951 let rec stack_goals level gs =
956 let is_open = function
957 | (_,Continuationals.Stack.Open i) -> Some i
958 | (_,Continuationals.Stack.Closed _) -> None
960 HExtlib.filter_map is_open g @ stack_goals (level-1) s
963 let open_goals level status = stack_goals level status#stack
966 let try_candidate ?(smart=0) flags depth status eq_cache ctx t =
968 let old_og_no = List.length (open_goals (depth+1) status) in
969 debug_print ~depth (lazy ("try " ^ (NotationPp.pp_term status) t));
971 if smart= 0 then NTactics.apply_tac ("",0,t) status
972 else if smart = 1 then smart_apply_auto ("",0,t) eq_cache status
973 else (* smart = 2: both *)
974 try NTactics.apply_tac ("",0,t) status
976 smart_apply_auto ("",0,t) eq_cache status
978 (* we compare the expected branching with the actual one and
979 prune the candidate when the latter is larger. The optimization
980 is meant to rule out stange applications of flexible terms,
981 such as the application of eq_f that always succeeds.
982 There is some gain but less than expected *)
983 let og_no = List.length (open_goals (depth+1) status) in
984 let status, cict = disambiguate status ctx ("",0,t) None in
985 let status,ct = term_of_cic_term status cict ctx in
986 let _,_,metasenv,subst,_ = status#obj in
987 let ty = NCicTypeChecker.typeof status subst metasenv ctx ct in
988 let res = branch status (mk_cic_term ctx ty) in
989 let diff = og_no - old_og_no in
990 debug_print (lazy ("expected branching: " ^ (string_of_int res)));
991 debug_print (lazy ("actual: branching" ^ (string_of_int diff)));
992 (* some flexibility *)
993 if diff > res && res > 0 (* facts are never pruned *) then
994 (debug_print (lazy ("branch factor for: " ^ (ppterm status cict) ^ " = "
995 ^ (string_of_int res) ^ " vs. " ^ (string_of_int diff)));
996 debug_print ~depth (lazy "strange application"); None)
998 (incr candidate_no; Some ((!candidate_no,t),status))
999 with Error (msg,exn) -> debug_print ~depth (lazy "failed"); None
1002 let sort_of status subst metasenv ctx t =
1003 let ty = NCicTypeChecker.typeof status subst metasenv ctx t in
1004 let metasenv',ty = NCicUnification.fix_sorts status metasenv subst ty in
1005 assert (metasenv = metasenv');
1006 NCicTypeChecker.typeof status subst metasenv ctx ty
1009 let type0= NUri.uri_of_string ("cic:/matita/pts/Type0.univ")
1012 let perforate_small status subst metasenv context t =
1013 let rec aux = function
1014 | NCic.Appl (hd::tl) ->
1016 let s = sort_of status subst metasenv context t in
1018 | NCic.Sort(NCic.Type [`Type,u])
1019 when u=type0 -> NCic.Meta (0,(0,NCic.Irl 0))
1022 NCic.Appl (hd::List.map map tl)
1028 let get_cands retrieve_for diff empty gty weak_gty =
1029 let cands = retrieve_for gty in
1031 | None -> cands, empty
1033 let more_cands = retrieve_for weak_gty in
1034 cands, diff more_cands cands
1037 let get_candidates ?(smart=true) depth flags status cache signature gty =
1038 let universe = status#auto_cache in
1039 let _,_,metasenv,subst,_ = status#obj in
1040 let context = ctx_of gty in
1041 let _, raw_gty = term_of_cic_term status gty context in
1042 let is_prod, is_eq =
1043 let status, t = term_of_cic_term status gty context in
1044 let t = NCicReduction.whd status subst context t in
1046 | NCic.Prod _ -> true, false
1047 | _ -> false, NCicParamod.is_equation status metasenv subst context t
1049 debug_print ~depth (lazy ("gty:" ^ NTacStatus.ppterm status gty));
1051 NCicParamod.is_equation status metasenv subst context raw_gty
1053 let raw_weak_gty, weak_gty =
1060 perforate_small status subst metasenv context raw_gty in
1061 let weak = mk_cic_term context raw_weak in
1062 debug_print ~depth (lazy ("weak_gty:" ^ NTacStatus.ppterm status weak));
1063 Some raw_weak, Some (weak)
1067 (* we now compute global candidates *)
1068 let global_cands, smart_global_cands =
1070 let to_ast = function
1071 | NCic.Const r when true
1072 (*is_relevant statistics r*) -> Some (Ast.NRef r)
1073 (* | NCic.Const _ -> None *)
1074 | _ -> assert false in
1076 to_ast (NDiscriminationTree.TermSet.elements s) in
1079 (NDiscriminationTree.DiscriminationTree.retrieve_unifiables universe)
1080 NDiscriminationTree.TermSet.diff
1081 NDiscriminationTree.TermSet.empty
1082 raw_gty raw_weak_gty in
1084 (* we now compute local candidates *)
1085 let local_cands,smart_local_cands =
1088 let _status, t = term_of_cic_term status t context
1090 List.map to_ast (Ncic_termSet.elements s) in
1093 (fun ty -> search_in_th ty cache)
1094 Ncic_termSet.diff Ncic_termSet.empty gty weak_gty in
1096 (* we now splits candidates in facts or not facts *)
1097 let test = is_a_fact_ast status subst metasenv context in
1098 let by,given_candidates =
1099 match flags.candidates with
1101 | None -> false, [] in
1102 (* we compute candidates to be applied in normal mode, splitted in
1103 facts and not facts *)
1104 let candidates_facts,candidates_other =
1105 let gl1,gl2 = List.partition test global_cands in
1106 let ll1,ll2 = List.partition test local_cands in
1107 (* if the goal is an equation we avoid to apply unit equalities,
1108 since superposition should take care of them; refl is an
1109 exception since it prompts for convertibility *)
1110 let l1 = if is_eq then [Ast.Ident("refl",`Ambiguous)] else gl1@ll1 in
1112 (* if smart given candidates are applied in smart mode *)
1113 if by && smart then ll2
1114 else if by then given_candidates@ll2
1118 (* we now compute candidates to be applied in smart mode, splitted in
1119 facts and not facts *)
1120 let smart_candidates_facts, smart_candidates_other =
1121 if is_prod || not(smart) then [],[]
1123 let sgl1,sgl2 = List.partition test smart_global_cands in
1124 let sll1,sll2 = List.partition test smart_local_cands in
1125 let l1 = if is_eq then [] else sgl1@sll1 in
1127 if by && smart then given_candidates@sll2
1128 else if by then sll2
1133 smart_candidates_facts,
1134 sort_candidates status context (candidates_other),
1135 sort_candidates status context (smart_candidates_other)
1138 let applicative_case depth signature status flags gty cache =
1139 app_counter:= !app_counter+1;
1140 let _,_,metasenv,subst,_ = status#obj in
1141 let context = ctx_of gty in
1142 let tcache = cache.facts in
1143 let is_prod, is_eq =
1144 let status, t = term_of_cic_term status gty context in
1145 let t = NCicReduction.whd status subst context t in
1147 | NCic.Prod _ -> true, false
1148 | _ -> false, NCicParamod.is_equation status metasenv subst context t
1150 debug_print ~depth (lazy (string_of_bool is_eq));
1152 let candidates_facts, smart_candidates_facts,
1153 candidates_other, smart_candidates_other =
1154 get_candidates ~smart:true depth
1155 flags status tcache signature gty
1157 let sm = if is_eq || is_prod then 0 else 2 in
1158 let sm1 = if flags.last then 2 else 0 in
1159 let maxd = (depth + 1 = flags.maxdepth) in
1160 let try_candidates only_one sm acc candidates =
1163 if (only_one && (elems <> [])) then elems
1165 match try_candidate (~smart:sm)
1166 flags depth status cache.unit_eq context cand with
1168 | Some x -> x::elems)
1171 (* if the goal is the last one we stop at the first fact *)
1172 let elems = try_candidates flags.last sm [] candidates_facts in
1173 (* now we add smart_facts *)
1174 let elems = try_candidates flags.last sm elems smart_candidates_facts in
1175 (* if we are at maxdepth and the goal is not a product we are done
1176 similarly, if the goal is the last one and we already found a
1178 if (maxd && not(is_prod)) || (flags.last && elems<>[]) then elems
1180 let elems = try_candidates false 2 elems candidates_other in
1181 debug_print ~depth (lazy ("not facts: try smart application"));
1182 try_candidates false 2 elems smart_candidates_other
1188 (* gty is supposed to be meta-closed *)
1189 let is_subsumed depth filter_depth status gty cache =
1190 if cache=[] then false else (
1191 debug_print ~depth (lazy("Subsuming " ^ (ppterm status gty)));
1192 let n,h,metasenv,subst,obj = status#obj in
1193 let ctx = ctx_of gty in
1194 let _ , raw_gty = term_of_cic_term status gty ctx in
1195 let target = NCicSubstitution.lift status 1 raw_gty in
1196 (* we compute candidates using the perforated type *)
1203 perforate_small status subst metasenv ctx raw_gty in
1204 let weak = mk_cic_term ctx raw_weak in
1205 debug_print ~depth (lazy ("weak_gty:" ^ NTacStatus.ppterm status weak));
1209 (* candidates must only be searched w.r.t the given context *)
1212 let idx = List.assq ctx cache in
1215 Ncic_termSet.elements
1216 (InvRelDiscriminationTree.retrieve_unifiables idx weak)
1218 with Not_found -> []
1220 (* this is a dirty trick: the first argument of an application is used
1221 to remember at which depth a goal failed *)
1223 let ctx = ctx_of t in
1224 let _, src = term_of_cic_term status t ctx in
1226 | NCic.Appl [NCic.Implicit (`Typeof d); t]
1227 when d <= depth -> Some (mk_cic_term ctx t)
1230 if filter_depth then HExtlib.filter_map filter candidates else candidates in
1232 (lazy ("failure candidates: " ^ string_of_int (List.length candidates)));
1236 let _ , source = term_of_cic_term status t ctx in
1238 NCic.Prod("foo",source,target) in
1239 let metasenv,j,_,_ =
1240 NCicMetaSubst.mk_meta
1241 metasenv ctx ~with_type:implication `IsType in
1242 let status = status#set_obj (n,h,metasenv,subst,obj) in
1243 let status = status#set_stack [([1,Open j],[],[],`NoTag)] in
1245 let status = NTactics.intro_tac "foo" status in
1247 NTactics.apply_tac ("",0,Ast.NCic (NCic.Rel 1)) status
1249 if (head_goals status#stack = []) then raise Found
1254 with Found -> debug_print ~depth (lazy "success");true)
1257 let rec guess_name name ctx =
1258 if name = "_" then guess_name "auto" ctx else
1259 if not (List.mem_assoc name ctx) then name else
1260 guess_name (name^"'") ctx
1263 let is_prod status =
1264 let _, ctx, gty = current_goal status in
1265 let status, gty = apply_subst status ctx gty in
1266 let _, raw_gty = term_of_cic_term status gty ctx in
1268 | NCic.Prod (name,src,_) ->
1269 let status, src = whd status ~delta:0 ctx (mk_cic_term ctx src) in
1270 (match snd (term_of_cic_term status src ctx) with
1271 | NCic.Const(NReference.Ref (_,NReference.Ind _) as r)
1272 | NCic.Appl (NCic.Const(NReference.Ref (_,NReference.Ind _) as r)::_) ->
1273 let _,_,itys,_,_ = NCicEnvironment.get_checked_indtys status r in
1275 (* | [_,_,_,[_;_]] con nat va, ovviamente, in loop *)
1277 | [_,_,_,[]] -> `Inductive (guess_name name ctx)
1278 | _ -> `Some (guess_name name ctx))
1279 | _ -> `Some (guess_name name ctx))
1282 let intro ~depth status facts name =
1283 let status = NTactics.intro_tac name status in
1284 let _, ctx, ngty = current_goal status in
1285 let t = mk_cic_term ctx (NCic.Rel 1) in
1286 let status, keys = keys_of_term status t in
1287 let facts = List.fold_left (add_to_th t) facts keys in
1288 debug_print ~depth (lazy ("intro: "^ name));
1289 (* unprovability is not stable w.r.t introduction *)
1293 let rec intros_facts ~depth status facts =
1294 if List.length (head_goals status#stack) <> 1 then status, facts else
1295 match is_prod status with
1299 intro ~depth status facts name
1300 in intros_facts ~depth status facts
1301 (* | `Inductive name ->
1302 let status = NTactics.case1_tac name status in
1303 intros_facts ~depth status facts *)
1304 | _ -> status, facts
1307 let intros ~depth status cache =
1308 match is_prod status with
1311 let trace = cache.trace in
1313 intros_facts ~depth status cache.facts
1315 if head_goals status#stack = [] then
1316 let status = NTactics.merge_tac status in
1317 [(0,Ast.Ident("__intros",`Ambiguous)),status], cache
1319 (* we reindex the equation from scratch *)
1320 let unit_eq = index_local_equations status#eq_cache status in
1321 let status = NTactics.merge_tac status in
1322 [(0,Ast.Ident("__intros",`Ambiguous)),status],
1323 init_cache ~facts ~unit_eq () ~trace
1327 let reduce ~whd ~depth status g =
1328 let n,h,metasenv,subst,o = status#obj in
1329 let attr, ctx, ty = NCicUtils.lookup_meta g metasenv in
1330 let ty = NCicUntrusted.apply_subst status subst ctx ty in
1332 (if whd then NCicReduction.whd else NCicTacReduction.normalize) status ~subst ctx ty
1337 (lazy ("reduced to: "^ status#ppterm ctx subst metasenv ty'));
1339 (g,(attr,ctx,ty'))::(List.filter (fun (i,_) -> i<>g) metasenv)
1341 let status = status#set_obj (n,h,metasenv,subst,o) in
1342 (* we merge to gain a depth level; the previous goal level should
1344 let status = NTactics.merge_tac status in
1346 [(!candidate_no,Ast.Ident("__whd",`Ambiguous)),status])
1349 let do_something signature flags status g depth gty cache =
1350 let l0, cache = intros ~depth status cache in
1351 if l0 <> [] then l0, cache
1354 let l = reduce ~whd:true ~depth status g in
1355 (* if l <> [] then l,cache else *)
1356 (* backward aplications *)
1361 ((!candidate_no,Ast.Ident("__paramod",`Ambiguous)),s))
1362 (auto_eq_check cache.unit_eq status)
1365 if ((l1 <> []) && flags.last) then [] else
1366 applicative_case depth signature status flags gty cache
1370 (fun ((_,t),_) -> toref incr_nominations statistics t) l2;
1371 (* states in l1 have have an empty set of subgoals: no point to sort them *)
1373 (lazy ("alternatives = " ^ (string_of_int (List.length (l1@l@l2)))));
1374 (* we order alternatives w.r.t the number of subgoals they open *)
1375 l1 @ (sort_new_elems l2) @ l, cache
1378 let pp_goal = function
1379 | (_,Continuationals.Stack.Open i)
1380 | (_,Continuationals.Stack.Closed i) -> string_of_int i
1383 let pp_goals status l =
1387 let gty = get_goalty status i in
1388 NTacStatus.ppterm status gty)
1395 let compare = Pervasives.compare
1399 module MS = HTopoSort.Make(M)
1402 let sort_tac status =
1404 match status#stack with
1405 | [] -> assert false
1406 | (goals, t, k, tag) :: s ->
1407 let g = head_goals status#stack in
1409 (List.rev (MS.topological_sort g (deps status))) in
1410 noprint (lazy ("old g = " ^
1411 String.concat "," (List.map string_of_int g)));
1412 noprint (lazy ("sorted goals = " ^
1413 String.concat "," (List.map string_of_int sortedg)));
1414 let is_it i = function
1415 | (_,Continuationals.Stack.Open j )
1416 | (_,Continuationals.Stack.Closed j ) -> i = j
1419 List.map (fun i -> List.find (is_it i) goals) sortedg
1421 (sorted_goals, t, k, tag) :: s
1423 status#set_stack gstatus
1426 let clean_up_tac status =
1428 match status#stack with
1429 | [] -> assert false
1430 | (g, t, k, tag) :: s ->
1431 let is_open = function
1432 | (_,Continuationals.Stack.Open _) -> true
1433 | (_,Continuationals.Stack.Closed _) -> false
1435 let g' = List.filter is_open g in
1436 (g', t, k, tag) :: s
1438 status#set_stack gstatus
1441 let focus_tac focus status =
1443 match status#stack with
1444 | [] -> assert false
1445 | (g, t, k, tag) :: s ->
1446 let in_focus = function
1447 | (_,Continuationals.Stack.Open i)
1448 | (_,Continuationals.Stack.Closed i) -> List.mem i focus
1450 let focus,others = List.partition in_focus g
1452 (* we need to mark it as a BranchTag, otherwise cannot merge later *)
1453 (focus,[],[],`BranchTag) :: (others, t, k, tag) :: s
1455 status#set_stack gstatus
1458 let deep_focus_tac level focus status =
1459 let in_focus = function
1460 | (_,Continuationals.Stack.Open i)
1461 | (_,Continuationals.Stack.Closed i) -> List.mem i focus
1463 let rec slice level gs =
1464 if level = 0 then [],[],gs else
1466 | [] -> assert false
1467 | (g, t, k, tag) :: s ->
1468 let f,o,gs = slice (level-1) s in
1469 let f1,o1 = List.partition in_focus g
1471 (f1,[],[],`BranchTag)::f, (o1, t, k, tag)::o, gs
1474 let f,o,s = slice level status#stack in f@o@s
1476 status#set_stack gstatus
1479 let move_to_side level status =
1480 match status#stack with
1481 | [] -> assert false
1483 let is_open = function
1484 | (_,Continuationals.Stack.Open i) -> Some i
1485 | (_,Continuationals.Stack.Closed _) -> None
1487 let others = menv_closure status (stack_goals (level-1) tl) in
1488 List.for_all (fun i -> IntSet.mem i others)
1489 (HExtlib.filter_map is_open g)
1491 let top_cache ~depth top status cache =
1493 let unit_eq = index_local_equations status#eq_cache status in
1494 {cache with unit_eq = unit_eq}
1497 let rec auto_clusters ?(top=false)
1498 flags signature cache depth status : unit =
1499 debug_print ~depth (lazy ("entering auto clusters at depth " ^
1500 (string_of_int depth)));
1501 debug_print ~depth (pptrace status cache.trace);
1502 (* ignore(Unix.select [] [] [] 0.01); *)
1503 let status = clean_up_tac status in
1504 let goals = head_goals status#stack in
1506 if depth = 0 then raise (Proved (status, cache.trace))
1508 let status = NTactics.merge_tac status in
1510 let l,tree = cache.under_inspection in
1512 | [] -> cache (* possible because of intros that cleans the cache *)
1513 | a::tl -> let tree = rm_from_th a tree a in
1514 {cache with under_inspection = tl,tree}
1516 auto_clusters flags signature cache (depth-1) status
1517 else if List.length goals < 2 then
1518 let cache = top_cache ~depth top status cache in
1519 auto_main flags signature cache depth status
1521 let all_goals = open_goals (depth+1) status in
1522 debug_print ~depth (lazy ("goals = " ^
1523 String.concat "," (List.map string_of_int all_goals)));
1524 let classes = HExtlib.clusters (deps status) all_goals in
1525 (* if any of the classes exceed maxwidth we fail *)
1528 if List.length gl > flags.maxwidth then
1530 debug_print ~depth (lazy "FAIL GLOBAL WIDTH");
1531 HLog.warn (sprintf "global width (%u) exceeded: %u"
1532 flags.maxwidth (List.length gl));
1533 raise (Gaveup cache.failures)
1534 end else ()) classes;
1535 if List.length classes = 1 then
1537 {flags with last = (List.length all_goals = 1)} in
1538 (* no need to cluster *)
1539 let cache = top_cache ~depth top status cache in
1540 auto_main flags signature cache depth status
1542 let classes = if top then List.rev classes else classes in
1548 ("cluster:" ^ String.concat "," (List.map string_of_int l)))
1550 (* we now process each cluster *)
1551 let status,cache,b =
1553 (fun (status,cache,b) gl ->
1555 {flags with last = (List.length gl = 1)} in
1556 let lold = List.length status#stack in
1557 debug_print ~depth (lazy ("stack length = " ^
1558 (string_of_int lold)));
1559 let fstatus = deep_focus_tac (depth+1) gl status in
1560 let cache = top_cache ~depth top fstatus cache in
1562 debug_print ~depth (lazy ("focusing on" ^
1563 String.concat "," (List.map string_of_int gl)));
1564 auto_main flags signature cache depth fstatus; assert false
1566 | Proved(status,trace) ->
1567 let status = NTactics.merge_tac status in
1568 let cache = {cache with trace = trace} in
1569 let lnew = List.length status#stack in
1570 assert (lold = lnew);
1572 | Gaveup failures when top ->
1573 let cache = {cache with failures = failures} in
1576 (status,cache,false) classes
1578 let rec final_merge n s =
1579 if n = 0 then s else final_merge (n-1) (NTactics.merge_tac s)
1580 in let status = final_merge depth status
1581 in if b then raise (Proved(status,cache.trace)) else raise (Gaveup cache.failures)
1585 (* BRAND NEW VERSION *)
1586 auto_main flags signature cache depth status: unit =
1587 debug_print ~depth (lazy "entering auto main");
1588 debug_print ~depth (pptrace status cache.trace);
1589 debug_print ~depth (lazy ("stack length = " ^
1590 (string_of_int (List.length status#stack))));
1591 (* ignore(Unix.select [] [] [] 0.01); *)
1592 let status = sort_tac (clean_up_tac status) in
1593 let goals = head_goals status#stack in
1595 | [] when depth = 0 -> raise (Proved (status,cache.trace))
1597 let status = NTactics.merge_tac status in
1599 let l,tree = cache.under_inspection in
1601 | [] -> cache (* possible because of intros that cleans the cache *)
1602 | a::tl -> let tree = rm_from_th a tree a in
1603 {cache with under_inspection = tl,tree}
1605 auto_clusters flags signature cache (depth-1) status
1607 if depth > 0 && move_to_side depth status
1609 let status = NTactics.merge_tac status in
1611 let l,tree = cache.under_inspection in
1613 | [] -> cache (* possible because of intros that cleans the cache*)
1614 | a::tl -> let tree = rm_from_th a tree a in
1615 {cache with under_inspection = tl,tree}
1617 auto_clusters flags signature cache (depth-1) status
1619 let ng = List.length goals in
1620 (* moved inside auto_clusters *)
1621 if ng > flags.maxwidth then begin
1622 debug_print ~depth (lazy "FAIL LOCAL WIDTH");
1623 HLog.warn (sprintf "local width (%u) exceeded: %u"
1625 raise (Gaveup cache.failures)
1626 end else if depth = flags.maxdepth then
1627 raise (Gaveup cache.failures)
1629 let status = NTactics.branch_tac ~force:true status in
1630 let g,gctx, gty = current_goal status in
1631 let ctx,ty = close status g in
1632 let closegty = mk_cic_term ctx ty in
1633 let status, gty = apply_subst status gctx gty in
1634 debug_print ~depth (lazy("Attacking goal " ^
1635 string_of_int g ^ " : "^ppterm status gty));
1636 debug_print ~depth (lazy ("current failures: " ^
1637 string_of_int (List.length (all_elements ctx cache.failures))));
1639 let _,_,metasenv,subst,_ = status#obj in
1640 NCicParamod.is_equation status metasenv subst ctx ty in
1641 (* if the goal is an equality we artificially raise its depth up to
1642 flags.maxdepth - 1 *)
1643 if (not flags.last && is_eq && (depth < (flags.maxdepth -1))) then
1644 (* for efficiency reasons, in this case we severely cripple the
1646 (debug_print ~depth (lazy ("RAISING DEPTH TO " ^ string_of_int (depth+1)));
1647 auto_main flags signature cache (depth+1) status)
1648 (* check for loops *)
1649 else if is_subsumed depth false status closegty (snd cache.under_inspection) then
1650 (debug_print ~depth (lazy "SUBSUMED");
1651 raise (Gaveup cache.failures))
1652 (* check for failures *)
1653 else if is_subsumed depth true status closegty cache.failures then
1654 (debug_print ~depth (lazy "ALREADY MET");
1655 raise (Gaveup cache.failures))
1657 let new_sig = height_of_goal g status in
1658 if new_sig < signature then
1659 (debug_print ~depth (lazy ("news = " ^ (string_of_int new_sig)));
1660 debug_print ~depth (lazy ("olds = " ^ (string_of_int signature))));
1661 let alternatives, cache =
1662 do_something signature flags status g depth gty cache in
1665 let l,tree = cache.under_inspection in
1666 let l,tree = closegty::l, add_to_th closegty tree closegty in
1667 {cache with under_inspection = l,tree}
1671 (fun allfailures ((_,t),status) ->
1673 (lazy ("(re)considering goal " ^
1674 (string_of_int g) ^" : "^ppterm status gty));
1675 debug_print (~depth:depth)
1676 (lazy ("Case: " ^ NotationPp.pp_term status t));
1678 if t=Ast.Ident("__whd",`Ambiguous) ||
1679 t=Ast.Ident("__intros",`Ambiguous)
1681 else depth+1,loop_cache in
1682 let cache = add_to_trace status ~depth cache t in
1683 let cache = {cache with failures = allfailures} in
1685 auto_clusters flags signature cache depth status;
1688 debug_print ~depth (lazy "Failed");
1690 cache.failures alternatives in
1694 let dty = NCic.Appl [NCic.Implicit (`Typeof depth); ty] in
1697 prerr_endline ("FAILURE : " ^ ppterm status gty);
1698 add_to_th newfail failures closegty
1700 debug_print ~depth (lazy "no more candidates");
1701 raise (Gaveup failures)
1704 let int name l def =
1705 try int_of_string (List.assoc name l)
1706 with Failure _ | Not_found -> def
1709 module AstSet = Set.Make(struct type t = Ast.term let compare = compare end)
1711 let cleanup_trace s trace =
1712 (* removing duplicates *)
1715 (fun acc t -> AstSet.add t acc)
1716 AstSet.empty trace in
1717 let trace = AstSet.elements trace_set
1718 (* filtering facts *)
1722 | Ast.NRef (NReference.Ref (u,_)) -> not (is_a_fact_obj s u)
1726 let auto_tac ~params:(univ,flags) ?(trace_ref=ref []) status =
1727 let oldstatus = status in
1728 let status = (status:> NTacStatus.tac_status) in
1729 let goals = head_goals status#stack in
1730 let status, facts = mk_th_cache status goals in
1731 (* let unit_eq = index_local_equations status#eq_cache status in *)
1732 let cache = init_cache ~facts () in
1733 (* pp_th status facts; *)
1735 NDiscriminationTree.DiscriminationTree.iter status#auto_cache (fun p t ->
1736 (*debug_*)print (lazy(
1737 NDiscriminationTree.NCicIndexable.string_of_path p ^ " |--> " ^
1738 String.concat "\n " (List.map (
1739 status#ppterm ~metasenv:[] ~context:[] ~subst:[])
1740 (NDiscriminationTree.TermSet.elements t))
1743 (* To allow using Rels in the user-specified candidates, we need a context
1744 * but in the case where multiple goals are open, there is no single context
1745 * to type the Rels. At this time, we require that Rels be typed in the
1746 * context of the first selected goal *)
1747 let _,ctx,_ = current_goal ~single_goal:false status in
1748 let status, candidates =
1750 | None -> status, None
1752 let to_Ast (st,l) t =
1753 let st, res = disambiguate st ctx t None in
1754 let st, res = term_of_cic_term st res (ctx_of res)
1755 in (st, Ast.NCic res::l)
1757 let status, l' = List.fold_left to_Ast (status,[]) l in
1760 let depth = int "depth" flags 3 in
1761 let size = int "size" flags 10 in
1762 let width = int "width" flags 4 (* (3+List.length goals)*) in
1764 (* let goals = List.map (fun i -> (i,P)) goals in *)
1765 let signature = height_of_goals status in
1768 candidates = candidates;
1772 timeout = Unix.gettimeofday() +. 3000.;
1775 let initial_time = Unix.gettimeofday() in
1780 ("TIME ELAPSED:"^string_of_float(Unix.gettimeofday()-.initial_time)));
1782 ("Applicative nodes:"^string_of_int !app_counter));
1783 raise (Error (lazy "auto gave up", None)))
1785 let _ = debug_print (lazy("\n\nRound "^string_of_int x^"\n")) in
1786 let flags = { flags with maxdepth = x }
1788 try auto_clusters (~top:true) flags signature cache 0 status;assert false
1790 try auto_main flags signature cache 0 status;assert false
1793 | Gaveup _ -> up_to (x+1) y
1794 | Proved (s,trace) ->
1795 debug_print (lazy ("proved at depth " ^ string_of_int x));
1796 List.iter (toref incr_uses statistics) trace;
1797 let _ = debug_print (pptrace status trace) in
1798 let trace = cleanup_trace s trace in
1799 let _ = debug_print (pptrace status trace) in
1802 | (g,t,k,f) :: rest -> (filter_open g,t,k,f):: rest
1805 let s = s#set_stack stack in
1807 oldstatus#set_status s
1809 let s = up_to depth depth in
1810 debug_print (print_stat status statistics);
1812 ("TIME ELAPSED:"^string_of_float(Unix.gettimeofday()-.initial_time)));
1814 ("Applicative nodes:"^string_of_int !app_counter));
1818 let auto_tac ~params:(_,flags as params) ?trace_ref =
1819 if List.mem_assoc "demod" flags then
1821 else if List.mem_assoc "paramod" flags then
1823 else if List.mem_assoc "fast_paramod" flags then
1824 fast_eq_check_tac ~params
1825 else auto_tac ~params ?trace_ref