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 facts " ^ 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 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
161 let height_of_ref status (NReference.Ref (uri, x)) =
166 | NReference.CoFix _ ->
167 let _,height,_,_,_ = NCicEnvironment.get_checked_obj status uri in
169 | NReference.Def h -> h
170 | NReference.Fix (_,_,h) -> h
173 (*************************** height functions ********************************)
174 let fast_height_of_term status t =
178 NCic.Meta (_,(_,NCic.Ctx l)) -> List.iter aux l
182 | NCic.Implicit _ -> assert false
185 prerr_endline (status#ppterm ~metasenv:[] ~subst:[]
186 ~context:[] t ^ ":" ^ string_of_int (height_of_ref status nref));
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
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
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);
214 let height_of_goals status =
215 let open_goals = head_goals status#stack in
216 assert (List.length open_goals > 0);
220 h := max !h (height_of_goal open_goal status))
222 noprint (lazy ("altezza sequente: " ^ string_of_int !h));
226 (* =============================== paramod =========================== *)
227 let solve f status eq_cache goal =
230 if fast then NCicParamod.fast_eq_check
231 else NCicParamod.paramod in
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) =
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 *)
249 (status#set_coerc_db NCicCoercion.empty_db)
250 metasenv subst ctx pt (Some gty)
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))
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" ^
268 "\n in the environment\n" ^
269 status#ppmetasenv subst metasenv)); None
270 | Sys.Break as e -> raise e
273 HExtlib.filter_map build_status
274 (f status metasenv subst ctx eq_cache (NCic.Rel ~-1,gty))
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))
283 let dist_fast_eq_check eq_cache s =
284 NTactics.distribute_tac (fast_eq_check eq_cache) s
287 let auto_eq_check eq_cache status =
289 let s = dist_fast_eq_check eq_cache status in
292 | Error _ -> debug_print (lazy ("no paramod proof found"));[]
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
306 let t = NCic.Rel !c in
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)
313 (noprint (lazy ("not a fact: " ^ (status#ppterm ctx subst metasenv 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
441 Sys.Break as e -> raise e
446 let ground_instances status gl =
447 let _,_,metasenv,subst,_ = status#obj in
448 let subset = menv_closure status gl in
449 let submenv = List.filter (fun (x,_) -> IntSet.mem x subset) metasenv in
451 let submenv = metasenv in
453 let subst, objs = close_metasenv status submenv subst in
457 let (_, ctx, t, _) = List.assoc i subst in
458 noprint (lazy (status#ppterm ctx [] [] t));
460 (fun (uri,_,_,_,_) as obj ->
461 NCicEnvironment.invalidate_item (`Obj (uri, obj)))
466 Not_found -> assert false
470 let replace_meta status i args target =
471 let rec aux k = function
472 (* TODO: local context *)
473 | NCic.Meta (j,lc) when i = j ->
477 List.map (NCicSubstitution.subst_meta status lc) args in
478 NCic.Appl(NCic.Rel k::args))
479 | NCic.Meta (j,lc) as m ->
486 aux k (NCicSubstitution.lift status n t)) l))))
487 | t -> NCicUtils.map status (fun _ k -> k+1) k aux t
492 let close_wrt_metasenv status subst =
494 (fun ty (i,(iattr,ctx,mty)) ->
495 let mty = NCicUntrusted.apply_subst status subst ctx mty in
497 NCicUntrusted.apply_subst_context status ~fix_projections:true
499 let cty = close_wrt_context status mty ctx in
500 let name = "foo"^(string_of_int i) in
501 let ty = NCicSubstitution.lift status 1 ty in
502 let args = args_for_context ~k:1 ctx in
503 (* prerr_endline (status#ppterm ctx [] [] iterm); *)
504 let ty = replace_meta status i args ty
506 NCic.Prod(name,cty,ty))
510 let _,_,metasenv,subst,_ = status#obj in
511 let subset = menv_closure status [g] in
512 let subset = IntSet.remove g subset in
513 let elems = IntSet.elements subset in
514 let _, ctx, ty = NCicUtils.lookup_meta g metasenv in
515 let ty = NCicUntrusted.apply_subst status subst ctx ty in
516 noprint (lazy ("metas in " ^ (status#ppterm ctx [] metasenv ty)));
517 noprint (lazy (String.concat ", " (List.map string_of_int elems)));
518 let submenv = List.filter (fun (x,_) -> IntSet.mem x subset) metasenv in
519 let submenv = List.rev (NCicUntrusted.sort_metasenv status subst submenv) in
521 let submenv = metasenv in
523 let ty = close_wrt_metasenv status subst ty submenv in
524 noprint (lazy (status#ppterm ctx [] [] ty));
528 (****************** smart application ********************)
530 let saturate_to_ref status metasenv subst ctx nref ty =
531 let height = height_of_ref status nref in
532 let rec aux metasenv ty args =
533 let ty,metasenv,moreargs =
534 NCicMetaSubst.saturate status ~delta:height metasenv subst ctx ty 0 in
536 | NCic.Const(NReference.Ref (_,NReference.Def _) as nre)
538 let _, _, bo, _, _, _ = NCicEnvironment.get_checked_def status nre in
539 aux metasenv bo (args@moreargs)
540 | NCic.Appl(NCic.Const(NReference.Ref (_,NReference.Def _) as nre)::tl)
542 let _, _, bo, _, _, _ = NCicEnvironment.get_checked_def status nre in
543 aux metasenv (NCic.Appl(bo::tl)) (args@moreargs)
544 | _ -> ty,metasenv,(args@moreargs)
548 let smart_apply t unit_eq status g =
549 let n,h,metasenv,subst,o = status#obj in
550 let gname, ctx, gty = List.assoc g metasenv in
551 (* let ggty = mk_cic_term context gty in *)
552 let status, t = disambiguate status ctx t None in
553 let status,t = term_of_cic_term status t ctx in
554 let _,_,metasenv,subst,_ = status#obj in
555 let ty = NCicTypeChecker.typeof status subst metasenv ctx t in
556 let ty,metasenv,args =
559 | NCic.Appl(NCic.Const(nref)::_) ->
560 saturate_to_ref status metasenv subst ctx nref ty
562 NCicMetaSubst.saturate status metasenv subst ctx ty 0 in
563 let metasenv,j,inst,_ = NCicMetaSubst.mk_meta metasenv ctx `IsTerm in
564 let status = status#set_obj (n,h,metasenv,subst,o) in
565 let pterm = if args=[] then t else
567 | NCic.Appl l -> NCic.Appl(l@args)
568 | _ -> NCic.Appl(t::args)
570 noprint(lazy("pterm " ^ (status#ppterm ctx [] [] pterm)));
571 noprint(lazy("pty " ^ (status#ppterm ctx [] [] ty)));
574 NUri.uri_of_string "cic:/matita/basics/logic/eq_coerc.con" in
575 let ref = NReference.reference_of_spec uri (NReference.Def(2)) in
579 NCic.Appl[eq_coerc;ty;NCic.Implicit `Type;pterm;inst] in
580 let smart = mk_cic_term ctx smart in
582 let status = instantiate status g smart in
583 let _,_,metasenv,subst,_ = status#obj in
584 let _,ctx,jty = List.assoc j metasenv in
585 let jty = NCicUntrusted.apply_subst status subst ctx jty in
586 debug_print(lazy("goal " ^ (status#ppterm ctx [] [] jty)));
587 let res = fast_eq_check unit_eq status j in
588 debug_print(lazy("ritorno da fast_eq_check"));
591 | NCicEnvironment.ObjectNotFound s as e ->
592 raise (Error (lazy "eq_coerc non yet defined",Some e))
593 | Error _ as e -> debug_print (lazy "error"); raise e
596 let compare_statuses ~past ~present =
597 let _,_,past,_,_ = past#obj in
598 let _,_,present,_,_ = present#obj in
599 List.map fst (List.filter (fun (i,_) -> not(List.mem_assoc i past)) present),
600 List.map fst (List.filter (fun (i,_) -> not (List.mem_assoc i present)) past)
603 (* paramodulation has only an implicit knoweledge of the symmetry of equality;
604 hence it is in trouble in proving (a = b) = (b = a) *)
605 let try_sym tac status g =
606 let sym_eq = Ast.Appl [Ast.Ident("sym_eq",None); Ast.Implicit `Vector] in
607 let _,_,metasenv,subst,_ = status#obj in
608 let _, context, gty = List.assoc g metasenv in
610 NCicParamod.is_equation status metasenv subst context gty
615 let new_status = instantiate_with_ast status g ("",0,sym_eq) in
616 let go, _ = compare_statuses ~past:status ~present:new_status in
617 assert (List.length go = 1);
618 let ng = List.hd go in
623 let smart_apply_tac t s =
624 let unit_eq = index_local_equations s#eq_cache s in
625 NTactics.distribute_tac (try_sym (smart_apply t unit_eq)) s
626 (* NTactics.distribute_tac (smart_apply t unit_eq) s *)
628 let smart_apply_auto t eq_cache =
629 NTactics.distribute_tac (try_sym (smart_apply t eq_cache))
630 (* NTactics.distribute_tac (smart_apply t eq_cache) *)
633 (****************** types **************)
636 type th_cache = (NCic.context * InvRelDiscriminationTree.t) list
638 (* cartesian: term set list -> term list set *)
641 [] -> NDiscriminationTree.TermListSet.empty
643 NDiscriminationTree.TermSet.fold
644 (fun x acc -> NDiscriminationTree.TermListSet.add [x] acc) l NDiscriminationTree.TermListSet.empty
646 let rest = cartesian tl in
647 NDiscriminationTree.TermSet.fold
649 NDiscriminationTree.TermListSet.fold (fun l acc' -> NDiscriminationTree.TermListSet.add (x::l) acc') rest acc
650 ) he NDiscriminationTree.TermListSet.empty
653 (* all_keys_of_cic_type: term -> term set *)
654 let all_keys_of_cic_type status metasenv subst context ty =
656 (* Here we are dropping the metasenv, but this should not raise any
657 exception (hopefully...) *)
659 NCicMetaSubst.saturate status ~delta:max_int metasenv subst context ty 0
665 NCic.Appl (he::tl) ->
668 let wty = NCicReduction.whd status ~delta:0 ~subst context ty in
670 NDiscriminationTree.TermSet.add ty (aux ty)
672 NDiscriminationTree.TermSet.union
673 (NDiscriminationTree.TermSet.add ty (aux ty))
674 (NDiscriminationTree.TermSet.add wty (aux wty))
677 NDiscriminationTree.TermListSet.fold
678 (fun l acc -> NDiscriminationTree.TermSet.add (NCic.Appl l) acc)
679 (cartesian ((NDiscriminationTree.TermSet.singleton he)::tl'))
680 NDiscriminationTree.TermSet.empty
681 | _ -> NDiscriminationTree.TermSet.empty
683 let ty,ity = saturate ty in
684 let wty,iwty = saturate (NCicReduction.whd status ~delta:0 ~subst context ty) in
686 [ity, NDiscriminationTree.TermSet.add ty (aux ty)]
688 [ity, NDiscriminationTree.TermSet.add ty (aux ty) ;
689 iwty, NDiscriminationTree.TermSet.add wty (aux wty) ]
692 let all_keys_of_type status t =
693 let _,_,metasenv,subst,_ = status#obj in
694 let context = ctx_of t in
695 let status, t = apply_subst status context t in
697 all_keys_of_cic_type status metasenv subst context
698 (snd (term_of_cic_term status t context))
702 (fun (intros,keys) ->
704 NDiscriminationTree.TermSet.fold
705 (fun t acc -> Ncic_termSet.add (mk_cic_term context t) acc)
706 keys Ncic_termSet.empty
711 let keys_of_type status orig_ty =
712 (* Here we are dropping the metasenv (in the status), but this should not
713 raise any exception (hopefully...) *)
714 let _, ty, _ = saturate ~delta:max_int status orig_ty in
715 let _, ty = apply_subst status (ctx_of ty) ty in
718 let orig_ty' = NCicTacReduction.normalize ~subst context orig_ty in
719 if orig_ty' <> orig_ty then
720 let ty',_,_= NCicMetaSubst.saturate ~delta:0 metasenv subst context orig_ty' 0 in
726 (*CSC: strange: we keep ty, ty normalized and ty ~delta:(h-1) *)
728 let _, ty = term_of_cic_term status ty (ctx_of ty) in
730 | NCic.Const (NReference.Ref (_,(NReference.Def h | NReference.Fix (_,_,h))))
731 | NCic.Appl (NCic.Const(NReference.Ref(_,(NReference.Def h | NReference.Fix (_,_,h))))::_)
733 let _,ty,_= saturate status ~delta:(h-1) orig_ty in
740 let all_keys_of_term status t =
741 let status, orig_ty = typeof status (ctx_of t) t in
742 all_keys_of_type status orig_ty
745 let keys_of_term status t =
746 let status, orig_ty = typeof status (ctx_of t) t in
747 keys_of_type status orig_ty
750 let mk_th_cache status gl =
752 (fun (status, acc) g ->
753 let gty = get_goalty status g in
754 let ctx = ctx_of gty in
755 noprint(lazy("th cache for: "^ppterm status gty));
756 noprint(lazy("th cache in: "^ppcontext status ctx));
757 if List.mem_assq ctx acc then status, acc else
758 let idx = InvRelDiscriminationTree.empty in
761 (fun (status, i, idx) _ ->
762 let t = mk_cic_term ctx (NCic.Rel i) in
763 let status, keys = keys_of_term status t in
764 noprint(lazy("indexing: "^ppterm status t ^ ": " ^ string_of_int (List.length keys)));
766 List.fold_left (fun idx k ->
767 InvRelDiscriminationTree.index idx k t) idx keys
772 status, (ctx, idx) :: acc)
776 let all_elements ctx cache =
777 let dummy = mk_cic_term ctx (NCic.Meta (0,(0, (NCic.Irl 0)))) in
779 let idx = List.assq ctx cache in
780 Ncic_termSet.elements
781 (InvRelDiscriminationTree.retrieve_unifiables idx dummy)
784 let add_to_th t c ty =
785 let key_c = ctx_of t in
786 if not (List.mem_assq key_c c) then
787 (key_c ,InvRelDiscriminationTree.index
788 InvRelDiscriminationTree.empty ty t ) :: c
790 let rec replace = function
792 | (x, idx) :: tl when x == key_c ->
793 (x, InvRelDiscriminationTree.index idx ty t) :: tl
794 | x :: tl -> x :: replace tl
799 let rm_from_th t c ty =
800 let key_c = ctx_of t in
801 if not (List.mem_assq key_c c) then assert false
803 let rec replace = function
805 | (x, idx) :: tl when x == key_c ->
806 (x, InvRelDiscriminationTree.remove_index idx ty t) :: tl
807 | x :: tl -> x :: replace tl
812 let pp_idx status idx =
813 InvRelDiscriminationTree.iter idx
815 noprint(lazy("K: " ^ NCicInverseRelIndexable.string_of_path k));
817 (fun t -> debug_print(lazy("\t"^ppterm status t)))
821 let pp_th (status: #NTacStatus.pstatus) =
824 noprint(lazy( "-----------------------------------------------"));
825 noprint(lazy( (status#ppcontext ~metasenv:[] ~subst:[] ctx)));
826 noprint(lazy( "||====> "));
830 let search_in_th gty th =
831 let c = ctx_of gty in
832 let rec aux acc = function
833 | [] -> (* Ncic_termSet.elements *) acc
836 let idx = List.assoc(*q*) k th in
837 let acc = Ncic_termSet.union acc
838 (InvRelDiscriminationTree.retrieve_unifiables idx gty)
841 with Not_found -> aux acc tl
843 aux Ncic_termSet.empty c
847 do_types : bool; (* solve goals in Type *)
848 last : bool; (* last goal: take first solution only *)
849 candidates: Ast.term list option;
857 {facts : th_cache; (* positive results *)
858 under_inspection : cic_term list * th_cache; (* to prune looping *)
859 failures : th_cache; (* to avoid repetitions *)
860 unit_eq : NCicParamod.state;
864 let add_to_trace status ~depth cache t =
867 debug_print ~depth (lazy ("Adding to trace: " ^ NotationPp.pp_term status t));
868 {cache with trace = t::cache.trace}
869 | Ast.NCic _ (* local candidate *)
870 | _ -> (*not an application *) cache
872 let pptrace status tr =
873 (lazy ("Proof Trace: " ^ (String.concat ";"
874 (List.map (NotationPp.pp_term status) tr))))
876 let remove_from_trace cache t =
879 (match cache.trace with
880 | _::tl -> {cache with trace = tl}
882 | Ast.NCic _ (* local candidate *)
883 | _ -> (*not an application *) cache *)
886 type goal = int * sort (* goal, depth, sort *)
887 type fail = goal * cic_term
888 type candidate = int * Ast.term (* unique candidate number, candidate *)
890 exception Gaveup of th_cache (* failure cache *)
891 exception Proved of NTacStatus.tac_status * Ast.term list
893 (* let close_failures _ c = c;; *)
894 (* let prunable _ _ _ = false;; *)
895 (* let cache_examine cache gty = `Notfound;; *)
896 (* let put_in_subst s _ _ _ = s;; *)
897 (* let add_to_cache_and_del_from_orlist_if_green_cut _ _ c _ _ o f _ = c, o, f, false ;; *)
898 (* let cache_add_underinspection c _ _ = c;; *)
900 let init_cache ?(facts=[]) ?(under_inspection=[],[])
902 ?(unit_eq=NCicParamod.empty_state)
907 under_inspection = under_inspection;
911 let only signature _context candidate = true
913 (* TASSI: nel trie ci mettiamo solo il body, non il ty *)
915 NCicTypeChecker.typeof ~subst:[] ~metasenv:[] [] candidate
917 let height = fast_height_of_term status candidate_ty in
918 let rc = signature >= height in
920 noprint (lazy ("Filtro: " ^ status#ppterm ~context:[] ~subst:[]
921 ~metasenv:[] candidate ^ ": " ^ string_of_int height))
923 noprint (lazy ("Tengo: " ^ status#ppterm ~context:[] ~subst:[]
924 ~metasenv:[] candidate ^ ": " ^ string_of_int height));
929 let candidate_no = ref 0;;
931 let openg_no status = List.length (head_goals status#stack)
933 let sort_candidates status ctx candidates =
934 let _,_,metasenv,subst,_ = status#obj in
936 let status,ct = disambiguate status ctx ("",0,cand) None in
937 let status,t = term_of_cic_term status ct ctx in
938 let ty = NCicTypeChecker.typeof status subst metasenv ctx t in
939 let res = branch status (mk_cic_term ctx ty) in
940 noprint (lazy ("branch factor for: " ^ (ppterm status ct) ^ " = "
941 ^ (string_of_int res)));
944 let candidates = List.map (fun t -> branch t,t) candidates in
946 List.sort (fun (a,_) (b,_) -> a - b) candidates in
947 let candidates = List.map snd candidates in
948 noprint (lazy ("candidates =\n" ^ (String.concat "\n"
949 (List.map (NotationPp.pp_term status) candidates))));
952 let sort_new_elems l =
953 List.sort (fun (_,s1) (_,s2) -> openg_no s1 - openg_no s2) l
955 let rec stack_goals level gs =
960 let is_open = function
961 | (_,Continuationals.Stack.Open i) -> Some i
962 | (_,Continuationals.Stack.Closed _) -> None
964 HExtlib.filter_map is_open g @ stack_goals (level-1) s
967 let open_goals level status = stack_goals level status#stack
970 let try_candidate ?(smart=0) flags depth status eq_cache ctx t =
972 let old_og_no = List.length (open_goals (depth+1) status) in
973 debug_print ~depth (lazy ("try " ^ (string_of_int smart) ^ " : "
974 ^ (NotationPp.pp_term status) t));
976 if smart = 0 then NTactics.apply_tac ("",0,t) status
977 else if smart = 1 then
978 smart_apply_auto ("",0,t) eq_cache status
979 else (* smart = 2: both *)
980 try NTactics.apply_tac ("",0,t) status
982 smart_apply_auto ("",0,t) eq_cache status
984 (* FG: this optimization rules out some applications of
985 * lift_bind (from contribs/lambda_delta/Basic_2/substitution/lift.ma)
987 (* we compare the expected branching with the actual one and
988 prune the candidate when the latter is larger. The optimization
989 is meant to rule out stange applications of flexible terms,
990 such as the application of eq_f that always succeeds.
991 There is some gain but less than expected *)
992 let og_no = List.length (open_goals (depth+1) status) in
993 let status, cict = disambiguate status ctx ("",0,t) None in
994 let status,ct = term_of_cic_term status cict ctx in
995 let _,_,metasenv,subst,_ = status#obj in
996 let ty = NCicTypeChecker.typeof status subst metasenv ctx ct in
997 let res = branch status (mk_cic_term ctx ty) in
998 let diff = og_no - old_og_no in
999 debug_print (lazy ("expected branching: " ^ (string_of_int res)));
1000 debug_print (lazy ("actual: branching" ^ (string_of_int diff)));
1001 (* some flexibility *)
1002 if og_no - old_og_no > res then
1003 (debug_print (lazy ("branch factor for: " ^ (ppterm status cict) ^ " = "
1004 ^ (string_of_int res) ^ " vs. " ^ (string_of_int og_no)));
1005 debug_print ~depth (lazy "strange application"); None)
1007 *) (incr candidate_no; Some ((!candidate_no,t),status))
1008 with Error (msg,exn) -> debug_print ~depth (lazy "failed"); None
1011 let sort_of status subst metasenv ctx t =
1012 let ty = NCicTypeChecker.typeof status subst metasenv ctx t in
1013 let metasenv',ty = NCicUnification.fix_sorts status metasenv subst ty in
1014 assert (metasenv = metasenv');
1015 NCicTypeChecker.typeof status subst metasenv ctx ty
1018 let type0= NUri.uri_of_string ("cic:/matita/pts/Type0.univ")
1021 let perforate_small status subst metasenv context t =
1022 let rec aux = function
1023 | NCic.Appl (hd::tl) ->
1025 let s = sort_of status subst metasenv context t in
1027 | NCic.Sort(NCic.Type [`Type,u])
1028 when u=type0 -> NCic.Meta (0,(0,NCic.Irl 0))
1031 NCic.Appl (hd::List.map map tl)
1037 let get_cands retrieve_for diff empty gty weak_gty =
1038 let cands = retrieve_for gty in
1040 | None -> cands, empty
1042 let more_cands = retrieve_for weak_gty in
1043 cands, diff more_cands cands
1046 let get_candidates ?(smart=true) ~pfailed depth flags status cache signature gty =
1047 let universe = status#auto_cache in
1048 let _,_,metasenv,subst,_ = status#obj in
1049 let context = ctx_of gty in
1050 let _, raw_gty = term_of_cic_term status gty context in
1051 let is_prod, is_eq =
1052 let status, t = term_of_cic_term status gty context in
1053 let t = NCicReduction.whd status subst context t in
1055 | NCic.Prod _ -> true, false
1056 | _ -> false, NCicParamod.is_equation status metasenv subst context t
1058 debug_print ~depth (lazy ("gty:" ^ NTacStatus.ppterm status gty));
1060 NCicParamod.is_equation status metasenv subst context raw_gty
1062 let raw_weak_gty, weak_gty =
1069 perforate_small status subst metasenv context raw_gty in
1070 let weak = mk_cic_term context raw_weak in
1071 noprint ~depth (lazy ("weak_gty:" ^ NTacStatus.ppterm status weak));
1072 Some raw_weak, Some (weak)
1076 (* we now compute global candidates *)
1077 let global_cands, smart_global_cands =
1079 let to_ast = function
1080 | NCic.Const r when true
1081 (*is_relevant statistics r*) -> Some (Ast.NRef r)
1082 (* | NCic.Const _ -> None *)
1083 | _ -> assert false in
1085 to_ast (NDiscriminationTree.TermSet.elements s) in
1088 (NDiscriminationTree.DiscriminationTree.retrieve_unifiables universe)
1089 NDiscriminationTree.TermSet.diff
1090 NDiscriminationTree.TermSet.empty
1091 raw_gty raw_weak_gty in
1093 (* we now compute local candidates *)
1094 let local_cands,smart_local_cands =
1097 let _status, t = term_of_cic_term status t context
1099 List.map to_ast (Ncic_termSet.elements s) in
1102 (fun ty -> search_in_th ty cache)
1103 Ncic_termSet.diff Ncic_termSet.empty gty weak_gty in
1105 (* we now splits candidates in facts or not facts *)
1106 let test = is_a_fact_ast status subst metasenv context in
1107 let by,given_candidates =
1108 match flags.candidates with
1110 | None -> false, [] in
1111 (* we compute candidates to be applied in normal mode, splitted in
1112 facts and not facts *)
1113 let candidates_facts,candidates_other =
1114 let gl1,gl2 = List.partition test global_cands in
1115 let ll1,ll2 = List.partition test local_cands in
1116 (* if the goal is an equation and paramodulation did not fail
1117 we avoid to apply unit equalities; refl is an
1118 exception since it prompts for convertibility *)
1119 let l1 = if is_eq && (not pfailed)
1120 then [Ast.Ident("refl",None)] else gl1@ll1 in
1122 (* if smart given candidates are applied in smart mode *)
1123 if by && smart then ll2
1124 else if by then given_candidates@ll2
1128 (* we now compute candidates to be applied in smart mode, splitted in
1129 facts and not facts *)
1130 let smart_candidates_facts, smart_candidates_other =
1131 if is_prod || not(smart) then [],[]
1133 let sgl1,sgl2 = List.partition test smart_global_cands in
1134 let sll1,sll2 = List.partition test smart_local_cands in
1135 let l1 = if is_eq then [] else sgl1@sll1 in
1137 if by && smart then given_candidates@sll2
1138 else if by then sll2
1143 smart_candidates_facts,
1144 sort_candidates status context (candidates_other),
1145 sort_candidates status context (smart_candidates_other)
1148 let applicative_case ~pfailed depth signature status flags gty cache =
1149 app_counter:= !app_counter+1;
1150 let _,_,metasenv,subst,_ = status#obj in
1151 let context = ctx_of gty in
1152 let tcache = cache.facts in
1153 let is_prod, is_eq =
1154 let status, t = term_of_cic_term status gty context in
1155 let t = NCicReduction.whd status subst context t in
1157 | NCic.Prod _ -> true, false
1158 | _ -> false, NCicParamod.is_equation status metasenv subst context t
1160 debug_print ~depth (lazy (string_of_bool is_eq));
1162 let candidates_facts, smart_candidates_facts,
1163 candidates_other, smart_candidates_other =
1164 get_candidates ~smart:true ~pfailed depth
1165 flags status tcache signature gty
1167 let sm = if is_eq || is_prod then 0 else 2 in
1168 let sm1 = if flags.last then 2 else 0 in
1169 let maxd = (depth + 1 = flags.maxdepth) in
1170 let try_candidates only_one sm acc candidates =
1173 if (only_one && (elems <> [])) then elems
1175 match try_candidate (~smart:sm)
1176 flags depth status cache.unit_eq context cand with
1178 | Some x -> x::elems)
1181 (* if the goal is the last one we stop at the first fact *)
1182 let elems = try_candidates flags.last sm [] candidates_facts in
1183 (* now we add smart_facts *)
1184 let elems = try_candidates flags.last sm elems smart_candidates_facts in
1185 (* if we are at maxdepth and the goal is not a product we are done
1186 similarly, if the goal is the last one and we already found a
1188 if (maxd && not(is_prod)) || (flags.last && elems<>[]) then elems
1190 let elems = try_candidates false 2 elems candidates_other in
1191 debug_print ~depth (lazy ("not facts: try smart application"));
1192 try_candidates false 2 elems smart_candidates_other
1198 (* gty is supposed to be meta-closed *)
1199 let is_subsumed depth filter_depth status gty cache =
1200 if cache=[] then false else (
1201 debug_print ~depth (lazy("Subsuming " ^ (ppterm status gty)));
1202 let n,h,metasenv,subst,obj = status#obj in
1203 let ctx = ctx_of gty in
1204 let _ , raw_gty = term_of_cic_term status gty ctx in
1205 let target = NCicSubstitution.lift status 1 raw_gty in
1206 (* we compute candidates using the perforated type *)
1213 perforate_small status subst metasenv ctx raw_gty in
1214 let weak = mk_cic_term ctx raw_weak in
1215 debug_print ~depth (lazy ("weak_gty:" ^ NTacStatus.ppterm status weak));
1219 (* candidates must only be searched w.r.t the given context *)
1222 let idx = List.assq ctx cache in
1225 Ncic_termSet.elements
1226 (InvRelDiscriminationTree.retrieve_unifiables idx weak)
1228 with Not_found -> []
1230 (* this is a dirty trick: the first argument of an application is used
1231 to remember at which depth a goal failed *)
1233 let ctx = ctx_of t in
1234 let _, src = term_of_cic_term status t ctx in
1236 | NCic.Appl [NCic.Implicit (`Typeof d); t]
1237 when d <= depth -> Some (mk_cic_term ctx t)
1240 if filter_depth then HExtlib.filter_map filter candidates else candidates in
1242 (lazy ("failure candidates: " ^ string_of_int (List.length candidates)));
1246 let _ , source = term_of_cic_term status t ctx in
1248 NCic.Prod("foo",source,target) in
1249 let metasenv,j,_,_ =
1250 NCicMetaSubst.mk_meta
1251 metasenv ctx ~with_type:implication `IsType in
1252 let status = status#set_obj (n,h,metasenv,subst,obj) in
1253 let status = status#set_stack [([1,Open j],[],[],`NoTag)] in
1255 let status = NTactics.intro_tac "foo" status in
1257 NTactics.apply_tac ("",0,Ast.NCic (NCic.Rel 1)) status
1259 if (head_goals status#stack = []) then raise Found
1264 with Found -> debug_print ~depth (lazy "success");true)
1267 let rec guess_name name ctx =
1268 if name = "_" then guess_name "auto" ctx else
1269 if not (List.mem_assoc name ctx) then name else
1270 guess_name (name^"'") ctx
1273 let is_prod status =
1274 let _, ctx, gty = current_goal status in
1275 let status, gty = apply_subst status ctx gty in
1276 let _, raw_gty = term_of_cic_term status gty ctx in
1278 | NCic.Prod (name,src,_) ->
1279 let status, src = whd status ~delta:0 ctx (mk_cic_term ctx src) in
1280 (match snd (term_of_cic_term status src ctx) with
1281 | NCic.Const(NReference.Ref (_,NReference.Ind _) as r)
1282 | NCic.Appl (NCic.Const(NReference.Ref (_,NReference.Ind _) as r)::_) ->
1283 let _,_,itys,_,_ = NCicEnvironment.get_checked_indtys status r in
1285 (* | [_,_,_,[_;_]] con nat va, ovviamente, in loop *)
1287 | [_,_,_,[]] -> `Inductive (guess_name name ctx)
1288 | _ -> `Some (guess_name name ctx))
1289 | _ -> `Some (guess_name name ctx))
1292 let intro ~depth status facts name =
1293 let status = NTactics.intro_tac name status in
1294 let _, ctx, ngty = current_goal status in
1295 let t = mk_cic_term ctx (NCic.Rel 1) in
1296 let status, keys = keys_of_term status t in
1297 let facts = List.fold_left (add_to_th t) facts keys in
1298 debug_print ~depth (lazy ("intro: "^ name));
1299 (* unprovability is not stable w.r.t introduction *)
1303 let rec intros_facts ~depth status facts =
1304 if List.length (head_goals status#stack) <> 1 then status, facts else
1305 match is_prod status with
1309 intro ~depth status facts name
1310 in intros_facts ~depth status facts
1311 (* | `Inductive name ->
1312 let status = NTactics.case1_tac name status in
1313 intros_facts ~depth status facts *)
1314 | _ -> status, facts
1317 let intros ~depth status cache =
1318 match is_prod status with
1321 let trace = cache.trace in
1323 intros_facts ~depth status cache.facts
1325 if head_goals status#stack = [] then
1326 let status = NTactics.merge_tac status in
1327 [(0,Ast.Ident("__intros",None)),status], cache
1329 (* we reindex the equation from scratch *)
1330 let unit_eq = index_local_equations status#eq_cache status in
1331 let status = NTactics.merge_tac status in
1332 [(0,Ast.Ident("__intros",None)),status],
1333 init_cache ~facts ~unit_eq () ~trace
1337 let reduce ~whd ~depth status g =
1338 let n,h,metasenv,subst,o = status#obj in
1339 let attr, ctx, ty = NCicUtils.lookup_meta g metasenv in
1340 let ty = NCicUntrusted.apply_subst status subst ctx ty in
1342 (if whd then NCicReduction.whd else NCicTacReduction.normalize) status ~subst ctx ty
1347 (lazy ("reduced to: "^ status#ppterm ctx subst metasenv ty'));
1349 (g,(attr,ctx,ty'))::(List.filter (fun (i,_) -> i<>g) metasenv)
1351 let status = status#set_obj (n,h,metasenv,subst,o) in
1352 (* we merge to gain a depth level; the previous goal level should
1354 let status = NTactics.merge_tac status in
1356 [(!candidate_no,Ast.Ident("__whd",None)),status])
1359 let is_meta status gty =
1360 let _, ty = term_of_cic_term status gty (ctx_of gty) in
1362 | NCic.Meta _ -> true
1366 let do_something signature flags status g depth gty cache =
1367 (* if the goal is meta we close it with I:True. This should work
1368 thanks to the toplogical sorting of goals. *)
1369 if is_meta status gty then
1370 let t = Ast.Ident("I",None) in
1371 debug_print (lazy ("using default term" ^ (NotationPp.pp_term status) t));
1372 let s = NTactics.apply_tac ("",0,t) status in
1375 let l0, cache = intros ~depth status cache in
1376 if l0 <> [] then l0, cache
1379 let l = reduce ~whd:true ~depth status g in
1380 (* if l <> [] then l,cache else *)
1381 (* backward aplications *)
1386 ((!candidate_no,Ast.Ident("__paramod",None)),s))
1387 (auto_eq_check cache.unit_eq status)
1390 if ((l1 <> []) && flags.last) then [] else
1391 applicative_case ~pfailed:(l1=[]) depth signature status flags gty cache
1395 (fun ((_,t),_) -> toref incr_nominations statistics t) l2;
1396 (* states in l1 have have an empty set of subgoals: no point to sort them *)
1398 (lazy ("alternatives = " ^ (string_of_int (List.length (l1@l@l2)))));
1399 (* we order alternatives w.r.t the number of subgoals they open *)
1400 l1 @ (sort_new_elems l2) @ l, cache
1403 let pp_goal = function
1404 | (_,Continuationals.Stack.Open i)
1405 | (_,Continuationals.Stack.Closed i) -> string_of_int i
1408 let pp_goals status l =
1412 let gty = get_goalty status i in
1413 NTacStatus.ppterm status gty)
1420 let compare = Pervasives.compare
1424 module MS = HTopoSort.Make(M)
1427 let sort_tac status =
1429 match status#stack with
1430 | [] -> assert false
1431 | (goals, t, k, tag) :: s ->
1432 let g = head_goals status#stack in
1434 (List.rev (MS.topological_sort g (deps status))) in
1435 noprint (lazy ("old g = " ^
1436 String.concat "," (List.map string_of_int g)));
1437 noprint (lazy ("sorted goals = " ^
1438 String.concat "," (List.map string_of_int sortedg)));
1439 let is_it i = function
1440 | (_,Continuationals.Stack.Open j )
1441 | (_,Continuationals.Stack.Closed j ) -> i = j
1444 List.map (fun i -> List.find (is_it i) goals) sortedg
1446 (sorted_goals, t, k, tag) :: s
1448 status#set_stack gstatus
1451 let clean_up_tac status =
1453 match status#stack with
1454 | [] -> assert false
1455 | (g, t, k, tag) :: s ->
1456 let is_open = function
1457 | (_,Continuationals.Stack.Open _) -> true
1458 | (_,Continuationals.Stack.Closed _) -> false
1460 let g' = List.filter is_open g in
1461 (g', t, k, tag) :: s
1463 status#set_stack gstatus
1466 let focus_tac focus status =
1468 match status#stack with
1469 | [] -> assert false
1470 | (g, t, k, tag) :: s ->
1471 let in_focus = function
1472 | (_,Continuationals.Stack.Open i)
1473 | (_,Continuationals.Stack.Closed i) -> List.mem i focus
1475 let focus,others = List.partition in_focus g
1477 (* we need to mark it as a BranchTag, otherwise cannot merge later *)
1478 (focus,[],[],`BranchTag) :: (others, t, k, tag) :: s
1480 status#set_stack gstatus
1483 let deep_focus_tac level focus status =
1484 let in_focus = function
1485 | (_,Continuationals.Stack.Open i)
1486 | (_,Continuationals.Stack.Closed i) -> List.mem i focus
1488 let rec slice level gs =
1489 if level = 0 then [],[],gs else
1491 | [] -> assert false
1492 | (g, t, k, tag) :: s ->
1493 let f,o,gs = slice (level-1) s in
1494 let f1,o1 = List.partition in_focus g
1496 (f1,[],[],`BranchTag)::f, (o1, t, k, tag)::o, gs
1499 let f,o,s = slice level status#stack in f@o@s
1501 status#set_stack gstatus
1504 let move_to_side level status =
1505 match status#stack with
1506 | [] -> assert false
1508 let is_open = function
1509 | (_,Continuationals.Stack.Open i) -> Some i
1510 | (_,Continuationals.Stack.Closed _) -> None
1512 let others = menv_closure status (stack_goals (level-1) tl) in
1513 List.for_all (fun i -> IntSet.mem i others)
1514 (HExtlib.filter_map is_open g)
1516 let top_cache ~depth top status cache =
1518 let unit_eq = index_local_equations status#eq_cache status in
1519 {cache with unit_eq = unit_eq}
1522 let rec auto_clusters ?(top=false)
1523 flags signature cache depth status : unit =
1524 debug_print ~depth (lazy ("entering auto clusters at depth " ^
1525 (string_of_int depth)));
1526 debug_print ~depth (pptrace status cache.trace);
1527 (* ignore(Unix.select [] [] [] 0.01); *)
1528 let status = clean_up_tac status in
1529 let goals = head_goals status#stack in
1531 if depth = 0 then raise (Proved (status, cache.trace))
1533 let status = NTactics.merge_tac status in
1535 let l,tree = cache.under_inspection in
1537 | [] -> cache (* possible because of intros that cleans the cache *)
1538 | a::tl -> let tree = rm_from_th a tree a in
1539 {cache with under_inspection = tl,tree}
1541 auto_clusters flags signature cache (depth-1) status
1542 else if List.length goals < 2 then
1543 let cache = top_cache ~depth top status cache in
1544 auto_main flags signature cache depth status
1546 let all_goals = open_goals (depth+1) status in
1547 debug_print ~depth (lazy ("goals = " ^
1548 String.concat "," (List.map string_of_int all_goals)));
1549 let classes = HExtlib.clusters (deps status) all_goals in
1550 (* if any of the classes exceed maxwidth we fail *)
1553 if List.length gl > flags.maxwidth then
1555 debug_print ~depth (lazy "FAIL GLOBAL WIDTH");
1556 HLog.warn (sprintf "global width (%u) exceeded: %u"
1557 flags.maxwidth (List.length gl));
1558 raise (Gaveup cache.failures)
1559 end else ()) classes;
1560 if List.length classes = 1 then
1562 {flags with last = (List.length all_goals = 1)} in
1563 (* no need to cluster *)
1564 let cache = top_cache ~depth top status cache in
1565 auto_main flags signature cache depth status
1567 let classes = if top then List.rev classes else classes in
1573 ("cluster:" ^ String.concat "," (List.map string_of_int l)))
1575 (* we now process each cluster *)
1576 let status,cache,b =
1578 (fun (status,cache,b) gl ->
1580 {flags with last = (List.length gl = 1)} in
1581 let lold = List.length status#stack in
1582 debug_print ~depth (lazy ("stack length = " ^
1583 (string_of_int lold)));
1584 let fstatus = deep_focus_tac (depth+1) gl status in
1585 let cache = top_cache ~depth top fstatus cache in
1587 debug_print ~depth (lazy ("focusing on" ^
1588 String.concat "," (List.map string_of_int gl)));
1589 auto_main flags signature cache depth fstatus; assert false
1591 | Proved(status,trace) ->
1592 let status = NTactics.merge_tac status in
1593 let cache = {cache with trace = trace} in
1594 let lnew = List.length status#stack in
1595 assert (lold = lnew);
1597 | Gaveup failures when top ->
1598 let cache = {cache with failures = failures} in
1601 (status,cache,false) classes
1603 let rec final_merge n s =
1604 if n = 0 then s else final_merge (n-1) (NTactics.merge_tac s)
1605 in let status = final_merge depth status
1606 in if b then raise (Proved(status,cache.trace)) else raise (Gaveup cache.failures)
1610 (* BRAND NEW VERSION *)
1611 auto_main flags signature cache depth status: unit =
1612 debug_print ~depth (lazy "entering auto main");
1613 debug_print ~depth (pptrace status cache.trace);
1614 debug_print ~depth (lazy ("stack length = " ^
1615 (string_of_int (List.length status#stack))));
1616 (* ignore(Unix.select [] [] [] 0.01); *)
1617 let status = sort_tac (clean_up_tac status) in
1618 let goals = head_goals status#stack in
1620 | [] when depth = 0 -> raise (Proved (status,cache.trace))
1622 let status = NTactics.merge_tac status in
1624 let l,tree = cache.under_inspection in
1626 | [] -> cache (* possible because of intros that cleans the cache *)
1627 | a::tl -> let tree = rm_from_th a tree a in
1628 {cache with under_inspection = tl,tree}
1630 auto_clusters flags signature cache (depth-1) status
1632 if depth > 0 && move_to_side depth status
1634 let status = NTactics.merge_tac status in
1636 let l,tree = cache.under_inspection in
1638 | [] -> cache (* possible because of intros that cleans the cache*)
1639 | a::tl -> let tree = rm_from_th a tree a in
1640 {cache with under_inspection = tl,tree}
1642 auto_clusters flags signature cache (depth-1) status
1644 let ng = List.length goals in
1645 (* moved inside auto_clusters *)
1646 if ng > flags.maxwidth then begin
1647 debug_print ~depth (lazy "FAIL LOCAL WIDTH");
1648 HLog.warn (sprintf "local width (%u) exceeded: %u"
1650 raise (Gaveup cache.failures)
1651 end else if depth = flags.maxdepth then
1652 raise (Gaveup cache.failures)
1654 let status = NTactics.branch_tac ~force:true status in
1655 let g,gctx, gty = current_goal status in
1656 let ctx,ty = close status g in
1657 let closegty = mk_cic_term ctx ty in
1658 let status, gty = apply_subst status gctx gty in
1659 debug_print ~depth (lazy("Attacking goal " ^
1660 string_of_int g ^ " : "^ppterm status gty));
1661 debug_print ~depth (lazy ("current failures: " ^
1662 string_of_int (List.length (all_elements ctx cache.failures))));
1664 let _,_,metasenv,subst,_ = status#obj in
1665 NCicParamod.is_equation status metasenv subst ctx ty in
1666 (* if the goal is an equality we artificially raise its depth up to
1667 flags.maxdepth - 1 *)
1668 if (not flags.last && is_eq && (depth < (flags.maxdepth -2))) then
1669 (* for efficiency reasons, in this case we severely cripple the
1671 (debug_print ~depth (lazy ("RAISING DEPTH TO " ^ string_of_int (depth+1)));
1672 auto_main flags signature cache (depth+1) status)
1673 (* check for loops *)
1674 else if is_subsumed depth false status closegty (snd cache.under_inspection) then
1675 (debug_print ~depth (lazy "SUBSUMED");
1676 raise (Gaveup cache.failures))
1677 (* check for failures *)
1678 else if is_subsumed depth true status closegty cache.failures then
1679 (debug_print ~depth (lazy "ALREADY MET");
1680 raise (Gaveup cache.failures))
1682 let new_sig = height_of_goal g status in
1683 if new_sig < signature then
1684 (debug_print ~depth (lazy ("news = " ^ (string_of_int new_sig)));
1685 debug_print ~depth (lazy ("olds = " ^ (string_of_int signature))));
1686 let alternatives, cache =
1687 do_something signature flags status g depth gty cache in
1690 let l,tree = cache.under_inspection in
1691 let l,tree = closegty::l, add_to_th closegty tree closegty in
1692 {cache with under_inspection = l,tree}
1696 (fun allfailures ((_,t),status) ->
1698 (lazy ("(re)considering goal " ^
1699 (string_of_int g) ^" : "^ppterm status gty));
1700 debug_print (~depth:depth)
1701 (lazy ("Case: " ^ NotationPp.pp_term status t));
1703 if t=Ast.Ident("__whd",None) ||
1704 t=Ast.Ident("__intros",None)
1706 else depth+1,loop_cache in
1707 let cache = add_to_trace status ~depth cache t in
1708 let cache = {cache with failures = allfailures} in
1710 auto_clusters flags signature cache depth status;
1713 debug_print ~depth (lazy "Failed");
1715 cache.failures alternatives in
1719 let dty = NCic.Appl [NCic.Implicit (`Typeof depth); ty] in
1722 (*prerr_endline ("FAILURE : " ^ ppterm status gty);*)
1723 add_to_th newfail failures closegty
1725 debug_print ~depth (lazy "no more candidates");
1726 raise (Gaveup failures)
1729 let int name l def =
1730 try int_of_string (List.assoc name l)
1731 with Failure _ | Not_found -> def
1734 module AstSet = Set.Make(struct type t = Ast.term let compare = compare end)
1736 let cleanup_trace s trace =
1737 (* removing duplicates *)
1740 (fun acc t -> AstSet.add t acc)
1741 AstSet.empty trace in
1742 let trace = AstSet.elements trace_set
1743 (* filtering facts *)
1747 | Ast.NRef (NReference.Ref (u,_)) -> not (is_a_fact_obj s u)
1751 let auto_tac ~params:(univ,flags) ?(trace_ref=ref []) status =
1752 let oldstatus = status in
1753 let status = (status:> NTacStatus.tac_status) in
1754 let goals = head_goals status#stack in
1755 let status, facts = mk_th_cache status goals in
1756 (* let unit_eq = index_local_equations status#eq_cache status in *)
1757 let cache = init_cache ~facts () in
1758 (* pp_th status facts; *)
1760 NDiscriminationTree.DiscriminationTree.iter status#auto_cache (fun p t ->
1762 NDiscriminationTree.NCicIndexable.string_of_path p ^ " |--> " ^
1763 String.concat "\n " (List.map (
1764 status#ppterm ~metasenv:[] ~context:[] ~subst:[])
1765 (NDiscriminationTree.TermSet.elements t))
1773 let status, res = disambiguate status [] t None in
1774 let _,res = term_of_cic_term status res (ctx_of res)
1776 in Some (List.map to_Ast l)
1778 let depth = int "depth" flags 3 in
1779 let size = int "size" flags 10 in
1780 let width = int "width" flags 4 (* (3+List.length goals)*) in
1782 (* let goals = List.map (fun i -> (i,P)) goals in *)
1783 let signature = height_of_goals status in
1786 candidates = candidates;
1790 timeout = Unix.gettimeofday() +. 3000.;
1793 let initial_time = Unix.gettimeofday() in
1798 ("TIME ELAPSED:"^string_of_float(Unix.gettimeofday()-.initial_time)));
1800 ("Applicative nodes:"^string_of_int !app_counter));
1801 raise (Error (lazy "auto gave up", None)))
1803 let _ = debug_print (lazy("\n\nRound "^string_of_int x^"\n")) in
1804 let flags = { flags with maxdepth = x }
1806 try auto_clusters (~top:true) flags signature cache 0 status;assert false
1808 try auto_main flags signature cache 0 status;assert false
1811 | Gaveup _ -> up_to (x+1) y
1812 | Proved (s,trace) ->
1813 debug_print (lazy ("proved at depth " ^ string_of_int x));
1814 List.iter (toref incr_uses statistics) trace;
1815 let trace = cleanup_trace s trace in
1816 let _ = debug_print (pptrace status trace) in
1819 | (g,t,k,f) :: rest -> (filter_open g,t,k,f):: rest
1822 let s = s#set_stack stack in
1824 oldstatus#set_status s
1826 let s = up_to depth depth in
1827 debug_print (print_stat status statistics);
1829 ("TIME ELAPSED:"^string_of_float(Unix.gettimeofday()-.initial_time)));
1831 ("Applicative nodes:"^string_of_int !app_counter));
1835 let auto_tac ~params:(_,flags as params) ?trace_ref =
1836 if List.mem_assoc "demod" flags then
1838 else if List.mem_assoc "paramod" flags then
1840 else if List.mem_assoc "fast_paramod" flags then
1841 fast_eq_check_tac ~params
1842 else auto_tac ~params ?trace_ref