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
272 HExtlib.filter_map build_status
273 (f status metasenv subst ctx eq_cache (NCic.Rel ~-1,gty))
276 let fast_eq_check eq_cache status (goal:int) =
277 match solve NCicParamod.fast_eq_check status eq_cache goal with
278 | [] -> raise (Error (lazy "no proof found",None))
282 let dist_fast_eq_check eq_cache s =
283 NTactics.distribute_tac (fast_eq_check eq_cache) s
286 let auto_eq_check eq_cache status =
288 let s = dist_fast_eq_check eq_cache status in
291 | Error _ -> debug_print (lazy ("no paramod proof found"));[]
294 let index_local_equations eq_cache status =
295 noprint (lazy "indexing equations");
296 let open_goals = head_goals status#stack in
297 let open_goal = List.hd open_goals in
298 let ngty = get_goalty status open_goal in
299 let _,_,metasenv,subst,_ = status#obj in
300 let ctx = apply_subst_context ~fix_projections:true status (ctx_of ngty) in
305 let t = NCic.Rel !c in
307 let ty = NCicTypeChecker.typeof status subst metasenv ctx t in
308 if is_a_fact status (mk_cic_term ctx ty) then
309 (noprint(lazy("eq indexing " ^ (status#ppterm ctx subst metasenv ty)));
310 NCicParamod.forward_infer_step status metasenv subst ctx eq_cache t ty)
312 (noprint (lazy ("not a fact: " ^ (status#ppterm ctx subst metasenv ty)));
315 | NCicTypeChecker.TypeCheckerFailure _
316 | NCicTypeChecker.AssertFailure _ -> eq_cache)
320 let fast_eq_check_tac ~params s =
321 let unit_eq = index_local_equations s#eq_cache s in
322 dist_fast_eq_check unit_eq s
325 let paramod eq_cache status goal =
326 match solve NCicParamod.paramod status eq_cache goal with
327 | [] -> raise (Error (lazy "no proof found",None))
331 let paramod_tac ~params s =
332 let unit_eq = index_local_equations s#eq_cache s in
333 NTactics.distribute_tac (paramod unit_eq) s
336 let demod eq_cache status goal =
337 match solve NCicParamod.demod status eq_cache goal with
338 | [] -> raise (Error (lazy "no progress",None))
342 let demod_tac ~params s =
343 let unit_eq = index_local_equations s#eq_cache s in
344 NTactics.distribute_tac (demod unit_eq) s
348 let fast_eq_check_tac_all ~params eq_cache status =
349 let g,_,_ = current_goal status in
350 let allstates = fast_eq_check_all status eq_cache g in
351 let pseudo_low_tac s _ _ = s in
352 let pseudo_low_tactics =
353 List.map pseudo_low_tac allstates
355 List.map (fun f -> NTactics.distribute_tac f status) pseudo_low_tactics
360 let demod status eq_cache goal =
361 let n,h,metasenv,subst,o = status#obj in
362 let gname, ctx, gty = List.assoc goal metasenv in
363 let gty = NCicUntrusted.apply_subst subst ctx gty in
365 let demod_tac ~params s =
366 let unit_eq = index_local_equations s#eq_cache s in
367 dist_fast_eq_check unit_eq s
370 (*************** subsumption ****************)
372 let close_wrt_context status =
376 | name, NCic.Decl t -> NCic.Prod(name,t,ty)
377 | name, NCic.Def(bo, _) -> NCicSubstitution.subst status bo ty)
380 let args_for_context ?(k=1) ctx =
383 (fun (n,l) ctx_entry ->
385 | name, NCic.Decl t -> n+1,NCic.Rel(n)::l
386 | name, NCic.Def(bo, _) -> n+1,l)
390 let constant_for_meta status ctx ty i =
391 let name = "cic:/foo"^(string_of_int i)^".con" in
392 let uri = NUri.uri_of_string name in
393 let ty = close_wrt_context status ty ctx in
394 (* prerr_endline (status#ppterm [] [] [] ty); *)
395 let attr = (`Generated,`Definition,`Local) in
396 let obj = NCic.Constant([],name,None,ty,attr) in
397 (* Constant of relevance * string * term option * term * c_attr *)
401 let refresh metasenv =
403 (fun (metasenv,subst) (i,(iattr,ctx,ty)) ->
404 let ikind = NCicUntrusted.kind_of_meta iattr in
405 let metasenv,j,instance,ty =
406 NCicMetaSubst.mk_meta ~attrs:iattr
407 metasenv ctx ~with_type:ty ikind in
408 let s_entry = i,(iattr, ctx, instance, ty) in
409 let metasenv = List.filter (fun x,_ -> i <> x) metasenv in
410 metasenv,s_entry::subst)
411 (metasenv,[]) metasenv
413 (* close metasenv returns a ground instance of all the metas in the
414 metasenv, insantiatied with axioms, and the list of these axioms *)
415 let close_metasenv status metasenv subst =
417 let metasenv = NCicUntrusted.apply_subst_metasenv subst metasenv in
419 let metasenv = NCicUntrusted.sort_metasenv status subst metasenv in
421 (fun (subst,objs) (i,(iattr,ctx,ty)) ->
422 let ty = NCicUntrusted.apply_subst status subst ctx ty in
424 NCicUntrusted.apply_subst_context status ~fix_projections:true
426 let (uri,_,_,_,obj) as okind =
427 constant_for_meta status ctx ty i in
429 NCicEnvironment.check_and_add_obj status okind;
430 let iref = NReference.reference_of_spec uri NReference.Decl in
432 let args = args_for_context ctx in
433 if args = [] then NCic.Const iref
434 else NCic.Appl(NCic.Const iref::args)
436 (* prerr_endline (status#ppterm ctx [] [] iterm); *)
437 let s_entry = i, ([], ctx, iterm, ty)
438 in s_entry::subst,okind::objs
439 with _ -> assert false)
443 let ground_instances status gl =
444 let _,_,metasenv,subst,_ = status#obj in
445 let subset = menv_closure status gl in
446 let submenv = List.filter (fun (x,_) -> IntSet.mem x subset) metasenv in
448 let submenv = metasenv in
450 let subst, objs = close_metasenv status submenv subst in
454 let (_, ctx, t, _) = List.assoc i subst in
455 noprint (lazy (status#ppterm ctx [] [] t));
457 (fun (uri,_,_,_,_) as obj ->
458 NCicEnvironment.invalidate_item (`Obj (uri, obj)))
463 Not_found -> assert false
467 let replace_meta status i args target =
468 let rec aux k = function
469 (* TODO: local context *)
470 | NCic.Meta (j,lc) when i = j ->
474 List.map (NCicSubstitution.subst_meta status lc) args in
475 NCic.Appl(NCic.Rel k::args))
476 | NCic.Meta (j,lc) as m ->
483 aux k (NCicSubstitution.lift status n t)) l))))
484 | t -> NCicUtils.map status (fun _ k -> k+1) k aux t
489 let close_wrt_metasenv status subst =
491 (fun ty (i,(iattr,ctx,mty)) ->
492 let mty = NCicUntrusted.apply_subst status subst ctx mty in
494 NCicUntrusted.apply_subst_context status ~fix_projections:true
496 let cty = close_wrt_context status mty ctx in
497 let name = "foo"^(string_of_int i) in
498 let ty = NCicSubstitution.lift status 1 ty in
499 let args = args_for_context ~k:1 ctx in
500 (* prerr_endline (status#ppterm ctx [] [] iterm); *)
501 let ty = replace_meta status i args ty
503 NCic.Prod(name,cty,ty))
507 let _,_,metasenv,subst,_ = status#obj in
508 let subset = menv_closure status [g] in
509 let subset = IntSet.remove g subset in
510 let elems = IntSet.elements subset in
511 let _, ctx, ty = NCicUtils.lookup_meta g metasenv in
512 let ty = NCicUntrusted.apply_subst status subst ctx ty in
513 noprint (lazy ("metas in " ^ (status#ppterm ctx [] metasenv ty)));
514 noprint (lazy (String.concat ", " (List.map string_of_int elems)));
515 let submenv = List.filter (fun (x,_) -> IntSet.mem x subset) metasenv in
516 let submenv = List.rev (NCicUntrusted.sort_metasenv status subst submenv) in
518 let submenv = metasenv in
520 let ty = close_wrt_metasenv status subst ty submenv in
521 noprint (lazy (status#ppterm ctx [] [] ty));
525 (****************** smart application ********************)
527 let saturate_to_ref status metasenv subst ctx nref ty =
528 let height = height_of_ref status nref in
529 let rec aux metasenv ty args =
530 let ty,metasenv,moreargs =
531 NCicMetaSubst.saturate status ~delta:height metasenv subst ctx ty 0 in
533 | NCic.Const(NReference.Ref (_,NReference.Def _) as nre)
535 let _, _, bo, _, _, _ = NCicEnvironment.get_checked_def status nre in
536 aux metasenv bo (args@moreargs)
537 | NCic.Appl(NCic.Const(NReference.Ref (_,NReference.Def _) as nre)::tl)
539 let _, _, bo, _, _, _ = NCicEnvironment.get_checked_def status nre in
540 aux metasenv (NCic.Appl(bo::tl)) (args@moreargs)
541 | _ -> ty,metasenv,(args@moreargs)
545 let smart_apply t unit_eq status g =
546 let n,h,metasenv,subst,o = status#obj in
547 let gname, ctx, gty = List.assoc g metasenv in
548 (* let ggty = mk_cic_term context gty in *)
549 let status, t = disambiguate status ctx t None in
550 let status,t = term_of_cic_term status t ctx in
551 let _,_,metasenv,subst,_ = status#obj in
552 let ty = NCicTypeChecker.typeof status subst metasenv ctx t in
553 let ty,metasenv,args =
556 | NCic.Appl(NCic.Const(nref)::_) ->
557 saturate_to_ref status metasenv subst ctx nref ty
559 NCicMetaSubst.saturate status metasenv subst ctx ty 0 in
560 let metasenv,j,inst,_ = NCicMetaSubst.mk_meta metasenv ctx `IsTerm in
561 let status = status#set_obj (n,h,metasenv,subst,o) in
562 let pterm = if args=[] then t else
564 | NCic.Appl l -> NCic.Appl(l@args)
565 | _ -> NCic.Appl(t::args)
567 noprint(lazy("pterm " ^ (status#ppterm ctx [] [] pterm)));
568 noprint(lazy("pty " ^ (status#ppterm ctx [] [] ty)));
571 NUri.uri_of_string "cic:/matita/basics/logic/eq_coerc.con" in
572 let ref = NReference.reference_of_spec uri (NReference.Def(2)) in
576 NCic.Appl[eq_coerc;ty;NCic.Implicit `Type;pterm;inst] in
577 let smart = mk_cic_term ctx smart in
579 let status = instantiate status g smart in
580 let _,_,metasenv,subst,_ = status#obj in
581 let _,ctx,jty = List.assoc j metasenv in
582 let jty = NCicUntrusted.apply_subst status subst ctx jty in
583 debug_print(lazy("goal " ^ (status#ppterm ctx [] [] jty)));
584 let res = fast_eq_check unit_eq status j in
585 debug_print(lazy("ritorno da fast_eq_check"));
588 | NCicEnvironment.ObjectNotFound s as e ->
589 raise (Error (lazy "eq_coerc non yet defined",Some e))
590 | Error _ as e -> debug_print (lazy "error"); raise e
593 let compare_statuses ~past ~present =
594 let _,_,past,_,_ = past#obj in
595 let _,_,present,_,_ = present#obj in
596 List.map fst (List.filter (fun (i,_) -> not(List.mem_assoc i past)) present),
597 List.map fst (List.filter (fun (i,_) -> not (List.mem_assoc i present)) past)
600 (* paramodulation has only an implicit knoweledge of the symmetry of equality;
601 hence it is in trouble in proving (a = b) = (b = a) *)
602 let try_sym tac status g =
603 let sym_eq = Ast.Appl [Ast.Ident("sym_eq",None); Ast.Implicit `Vector] in
604 let _,_,metasenv,subst,_ = status#obj in
605 let _, context, gty = List.assoc g metasenv in
607 NCicParamod.is_equation status metasenv subst context gty
612 let new_status = instantiate_with_ast status g ("",0,sym_eq) in
613 let go, _ = compare_statuses ~past:status ~present:new_status in
614 assert (List.length go = 1);
615 let ng = List.hd go in
620 let smart_apply_tac t s =
621 let unit_eq = index_local_equations s#eq_cache s in
622 NTactics.distribute_tac (try_sym (smart_apply t unit_eq)) s
623 (* NTactics.distribute_tac (smart_apply t unit_eq) s *)
625 let smart_apply_auto t eq_cache =
626 NTactics.distribute_tac (try_sym (smart_apply t eq_cache))
627 (* NTactics.distribute_tac (smart_apply t eq_cache) *)
630 (****************** types **************)
633 type th_cache = (NCic.context * InvRelDiscriminationTree.t) list
635 (* cartesian: term set list -> term list set *)
638 [] -> NDiscriminationTree.TermListSet.empty
640 NDiscriminationTree.TermSet.fold
641 (fun x acc -> NDiscriminationTree.TermListSet.add [x] acc) l NDiscriminationTree.TermListSet.empty
643 let rest = cartesian tl in
644 NDiscriminationTree.TermSet.fold
646 NDiscriminationTree.TermListSet.fold (fun l acc' -> NDiscriminationTree.TermListSet.add (x::l) acc') rest acc
647 ) he NDiscriminationTree.TermListSet.empty
650 (* all_keys_of_cic_type: term -> term set *)
651 let all_keys_of_cic_type status metasenv subst context ty =
653 (* Here we are dropping the metasenv, but this should not raise any
654 exception (hopefully...) *)
656 NCicMetaSubst.saturate status ~delta:max_int metasenv subst context ty 0
662 NCic.Appl (he::tl) ->
665 let wty = NCicReduction.whd status ~delta:0 ~subst context ty in
667 NDiscriminationTree.TermSet.add ty (aux ty)
669 NDiscriminationTree.TermSet.union
670 (NDiscriminationTree.TermSet.add ty (aux ty))
671 (NDiscriminationTree.TermSet.add wty (aux wty))
674 NDiscriminationTree.TermListSet.fold
675 (fun l acc -> NDiscriminationTree.TermSet.add (NCic.Appl l) acc)
676 (cartesian ((NDiscriminationTree.TermSet.singleton he)::tl'))
677 NDiscriminationTree.TermSet.empty
678 | _ -> NDiscriminationTree.TermSet.empty
680 let ty,ity = saturate ty in
681 let wty,iwty = saturate (NCicReduction.whd status ~delta:0 ~subst context ty) in
683 [ity, NDiscriminationTree.TermSet.add ty (aux ty)]
685 [ity, NDiscriminationTree.TermSet.add ty (aux ty) ;
686 iwty, NDiscriminationTree.TermSet.add wty (aux wty) ]
689 let all_keys_of_type status t =
690 let _,_,metasenv,subst,_ = status#obj in
691 let context = ctx_of t in
692 let status, t = apply_subst status context t in
694 all_keys_of_cic_type status metasenv subst context
695 (snd (term_of_cic_term status t context))
699 (fun (intros,keys) ->
701 NDiscriminationTree.TermSet.fold
702 (fun t acc -> Ncic_termSet.add (mk_cic_term context t) acc)
703 keys Ncic_termSet.empty
708 let keys_of_type status orig_ty =
709 (* Here we are dropping the metasenv (in the status), but this should not
710 raise any exception (hopefully...) *)
711 let _, ty, _ = saturate ~delta:max_int status orig_ty in
712 let _, ty = apply_subst status (ctx_of ty) ty in
715 let orig_ty' = NCicTacReduction.normalize ~subst context orig_ty in
716 if orig_ty' <> orig_ty then
717 let ty',_,_= NCicMetaSubst.saturate ~delta:0 metasenv subst context orig_ty' 0 in
723 (*CSC: strange: we keep ty, ty normalized and ty ~delta:(h-1) *)
725 let _, ty = term_of_cic_term status ty (ctx_of ty) in
727 | NCic.Const (NReference.Ref (_,(NReference.Def h | NReference.Fix (_,_,h))))
728 | NCic.Appl (NCic.Const(NReference.Ref(_,(NReference.Def h | NReference.Fix (_,_,h))))::_)
730 let _,ty,_= saturate status ~delta:(h-1) orig_ty in
737 let all_keys_of_term status t =
738 let status, orig_ty = typeof status (ctx_of t) t in
739 all_keys_of_type status orig_ty
742 let keys_of_term status t =
743 let status, orig_ty = typeof status (ctx_of t) t in
744 keys_of_type status orig_ty
747 let mk_th_cache status gl =
749 (fun (status, acc) g ->
750 let gty = get_goalty status g in
751 let ctx = ctx_of gty in
752 noprint(lazy("th cache for: "^ppterm status gty));
753 noprint(lazy("th cache in: "^ppcontext status ctx));
754 if List.mem_assq ctx acc then status, acc else
755 let idx = InvRelDiscriminationTree.empty in
758 (fun (status, i, idx) _ ->
759 let t = mk_cic_term ctx (NCic.Rel i) in
760 let status, keys = keys_of_term status t in
761 noprint(lazy("indexing: "^ppterm status t ^ ": " ^ string_of_int (List.length keys)));
763 List.fold_left (fun idx k ->
764 InvRelDiscriminationTree.index idx k t) idx keys
769 status, (ctx, idx) :: acc)
773 let all_elements ctx cache =
774 let dummy = mk_cic_term ctx (NCic.Meta (0,(0, (NCic.Irl 0)))) in
776 let idx = List.assq ctx cache in
777 Ncic_termSet.elements
778 (InvRelDiscriminationTree.retrieve_unifiables idx dummy)
781 let add_to_th t c ty =
782 let key_c = ctx_of t in
783 if not (List.mem_assq key_c c) then
784 (key_c ,InvRelDiscriminationTree.index
785 InvRelDiscriminationTree.empty ty t ) :: c
787 let rec replace = function
789 | (x, idx) :: tl when x == key_c ->
790 (x, InvRelDiscriminationTree.index idx ty t) :: tl
791 | x :: tl -> x :: replace tl
796 let rm_from_th t c ty =
797 let key_c = ctx_of t in
798 if not (List.mem_assq key_c c) then assert false
800 let rec replace = function
802 | (x, idx) :: tl when x == key_c ->
803 (x, InvRelDiscriminationTree.remove_index idx ty t) :: tl
804 | x :: tl -> x :: replace tl
809 let pp_idx status idx =
810 InvRelDiscriminationTree.iter idx
812 noprint(lazy("K: " ^ NCicInverseRelIndexable.string_of_path k));
814 (fun t -> debug_print(lazy("\t"^ppterm status t)))
818 let pp_th (status: #NTacStatus.pstatus) =
821 noprint(lazy( "-----------------------------------------------"));
822 noprint(lazy( (status#ppcontext ~metasenv:[] ~subst:[] ctx)));
823 noprint(lazy( "||====> "));
827 let search_in_th gty th =
828 let c = ctx_of gty in
829 let rec aux acc = function
830 | [] -> (* Ncic_termSet.elements *) acc
833 let idx = List.assoc(*q*) k th in
834 let acc = Ncic_termSet.union acc
835 (InvRelDiscriminationTree.retrieve_unifiables idx gty)
838 with Not_found -> aux acc tl
840 aux Ncic_termSet.empty c
844 do_types : bool; (* solve goals in Type *)
845 last : bool; (* last goal: take first solution only *)
846 candidates: Ast.term list option;
854 {facts : th_cache; (* positive results *)
855 under_inspection : cic_term list * th_cache; (* to prune looping *)
856 failures : th_cache; (* to avoid repetitions *)
857 unit_eq : NCicParamod.state;
861 let add_to_trace status ~depth cache t =
864 debug_print ~depth (lazy ("Adding to trace: " ^ NotationPp.pp_term status t));
865 {cache with trace = t::cache.trace}
866 | Ast.NCic _ (* local candidate *)
867 | _ -> (*not an application *) cache
869 let pptrace status tr =
870 (lazy ("Proof Trace: " ^ (String.concat ";"
871 (List.map (NotationPp.pp_term status) tr))))
873 let remove_from_trace cache t =
876 (match cache.trace with
877 | _::tl -> {cache with trace = tl}
879 | Ast.NCic _ (* local candidate *)
880 | _ -> (*not an application *) cache *)
883 type goal = int * sort (* goal, depth, sort *)
884 type fail = goal * cic_term
885 type candidate = int * Ast.term (* unique candidate number, candidate *)
887 exception Gaveup of th_cache (* failure cache *)
888 exception Proved of NTacStatus.tac_status * Ast.term list
890 (* let close_failures _ c = c;; *)
891 (* let prunable _ _ _ = false;; *)
892 (* let cache_examine cache gty = `Notfound;; *)
893 (* let put_in_subst s _ _ _ = s;; *)
894 (* let add_to_cache_and_del_from_orlist_if_green_cut _ _ c _ _ o f _ = c, o, f, false ;; *)
895 (* let cache_add_underinspection c _ _ = c;; *)
897 let init_cache ?(facts=[]) ?(under_inspection=[],[])
899 ?(unit_eq=NCicParamod.empty_state)
904 under_inspection = under_inspection;
908 let only signature _context candidate = true
910 (* TASSI: nel trie ci mettiamo solo il body, non il ty *)
912 NCicTypeChecker.typeof ~subst:[] ~metasenv:[] [] candidate
914 let height = fast_height_of_term status candidate_ty in
915 let rc = signature >= height in
917 noprint (lazy ("Filtro: " ^ status#ppterm ~context:[] ~subst:[]
918 ~metasenv:[] candidate ^ ": " ^ string_of_int height))
920 noprint (lazy ("Tengo: " ^ status#ppterm ~context:[] ~subst:[]
921 ~metasenv:[] candidate ^ ": " ^ string_of_int height));
926 let candidate_no = ref 0;;
928 let openg_no status = List.length (head_goals status#stack)
930 let sort_candidates status ctx candidates =
931 let _,_,metasenv,subst,_ = status#obj in
933 let status,ct = disambiguate status ctx ("",0,cand) None in
934 let status,t = term_of_cic_term status ct ctx in
935 let ty = NCicTypeChecker.typeof status subst metasenv ctx t in
936 let res = branch status (mk_cic_term ctx ty) in
937 noprint (lazy ("branch factor for: " ^ (ppterm status ct) ^ " = "
938 ^ (string_of_int res)));
941 let candidates = List.map (fun t -> branch t,t) candidates in
943 List.sort (fun (a,_) (b,_) -> a - b) candidates in
944 let candidates = List.map snd candidates in
945 noprint (lazy ("candidates =\n" ^ (String.concat "\n"
946 (List.map (NotationPp.pp_term status) candidates))));
949 let sort_new_elems l =
950 List.sort (fun (_,s1) (_,s2) -> openg_no s1 - openg_no s2) l
952 let rec stack_goals level gs =
957 let is_open = function
958 | (_,Continuationals.Stack.Open i) -> Some i
959 | (_,Continuationals.Stack.Closed _) -> None
961 HExtlib.filter_map is_open g @ stack_goals (level-1) s
964 let open_goals level status = stack_goals level status#stack
967 let try_candidate ?(smart=0) flags depth status eq_cache ctx t =
969 let old_og_no = List.length (open_goals (depth+1) status) in
970 debug_print ~depth (lazy ("try " ^ (string_of_int smart) ^ " : "
971 ^ (NotationPp.pp_term status) t));
973 if smart = 0 then NTactics.apply_tac ("",0,t) status
974 else if smart = 1 then
975 smart_apply_auto ("",0,t) eq_cache status
976 else (* smart = 2: both *)
977 try NTactics.apply_tac ("",0,t) status
979 smart_apply_auto ("",0,t) eq_cache status
981 (* FG: this optimization rules out some applications of
982 * lift_bind (from contribs/lambda_delta/Basic_2/substitution/lift.ma)
984 (* we compare the expected branching with the actual one and
985 prune the candidate when the latter is larger. The optimization
986 is meant to rule out stange applications of flexible terms,
987 such as the application of eq_f that always succeeds.
988 There is some gain but less than expected *)
989 let og_no = List.length (open_goals (depth+1) status) in
990 let status, cict = disambiguate status ctx ("",0,t) None in
991 let status,ct = term_of_cic_term status cict ctx in
992 let _,_,metasenv,subst,_ = status#obj in
993 let ty = NCicTypeChecker.typeof status subst metasenv ctx ct in
994 let res = branch status (mk_cic_term ctx ty) in
995 let diff = og_no - old_og_no in
996 debug_print (lazy ("expected branching: " ^ (string_of_int res)));
997 debug_print (lazy ("actual: branching" ^ (string_of_int diff)));
998 (* some flexibility *)
999 if og_no - old_og_no > res then
1000 (debug_print (lazy ("branch factor for: " ^ (ppterm status cict) ^ " = "
1001 ^ (string_of_int res) ^ " vs. " ^ (string_of_int og_no)));
1002 debug_print ~depth (lazy "strange application"); None)
1004 *) (incr candidate_no; Some ((!candidate_no,t),status))
1005 with Error (msg,exn) -> debug_print ~depth (lazy "failed"); None
1008 let sort_of status subst metasenv ctx t =
1009 let ty = NCicTypeChecker.typeof status subst metasenv ctx t in
1010 let metasenv',ty = NCicUnification.fix_sorts status metasenv subst ty in
1011 assert (metasenv = metasenv');
1012 NCicTypeChecker.typeof status subst metasenv ctx ty
1015 let type0= NUri.uri_of_string ("cic:/matita/pts/Type0.univ")
1018 let perforate_small status subst metasenv context t =
1019 let rec aux = function
1020 | NCic.Appl (hd::tl) ->
1022 let s = sort_of status subst metasenv context t in
1024 | NCic.Sort(NCic.Type [`Type,u])
1025 when u=type0 -> NCic.Meta (0,(0,NCic.Irl 0))
1028 NCic.Appl (hd::List.map map tl)
1034 let get_cands retrieve_for diff empty gty weak_gty =
1035 let cands = retrieve_for gty in
1037 | None -> cands, empty
1039 let more_cands = retrieve_for weak_gty in
1040 cands, diff more_cands cands
1043 let get_candidates ?(smart=true) depth flags status cache signature gty =
1044 let universe = status#auto_cache in
1045 let _,_,metasenv,subst,_ = status#obj in
1046 let context = ctx_of gty in
1047 let _, raw_gty = term_of_cic_term status gty context in
1048 let is_prod, is_eq =
1049 let status, t = term_of_cic_term status gty context in
1050 let t = NCicReduction.whd status subst context t in
1052 | NCic.Prod _ -> true, false
1053 | _ -> false, NCicParamod.is_equation status metasenv subst context t
1055 debug_print ~depth (lazy ("gty:" ^ NTacStatus.ppterm status gty));
1057 NCicParamod.is_equation status metasenv subst context raw_gty
1059 let raw_weak_gty, weak_gty =
1066 perforate_small status subst metasenv context raw_gty in
1067 let weak = mk_cic_term context raw_weak in
1068 noprint ~depth (lazy ("weak_gty:" ^ NTacStatus.ppterm status weak));
1069 Some raw_weak, Some (weak)
1073 (* we now compute global candidates *)
1074 let global_cands, smart_global_cands =
1076 let to_ast = function
1077 | NCic.Const r when true
1078 (*is_relevant statistics r*) -> Some (Ast.NRef r)
1079 (* | NCic.Const _ -> None *)
1080 | _ -> assert false in
1082 to_ast (NDiscriminationTree.TermSet.elements s) in
1085 (NDiscriminationTree.DiscriminationTree.retrieve_unifiables universe)
1086 NDiscriminationTree.TermSet.diff
1087 NDiscriminationTree.TermSet.empty
1088 raw_gty raw_weak_gty in
1090 (* we now compute local candidates *)
1091 let local_cands,smart_local_cands =
1094 let _status, t = term_of_cic_term status t context
1096 List.map to_ast (Ncic_termSet.elements s) in
1099 (fun ty -> search_in_th ty cache)
1100 Ncic_termSet.diff Ncic_termSet.empty gty weak_gty in
1102 (* we now splits candidates in facts or not facts *)
1103 let test = is_a_fact_ast status subst metasenv context in
1104 let by,given_candidates =
1105 match flags.candidates with
1107 | None -> false, [] in
1108 (* we compute candidates to be applied in normal mode, splitted in
1109 facts and not facts *)
1110 let candidates_facts,candidates_other =
1111 let gl1,gl2 = List.partition test global_cands in
1112 let ll1,ll2 = List.partition test local_cands in
1113 (* if the goal is an equation we avoid to apply unit equalities,
1114 since superposition should take care of them; refl is an
1115 exception since it prompts for convertibility *)
1116 let l1 = if is_eq then [Ast.Ident("refl",None)] else gl1@ll1 in
1118 (* if smart given candidates are applied in smart mode *)
1119 if by && smart then ll2
1120 else if by then given_candidates@ll2
1124 (* we now compute candidates to be applied in smart mode, splitted in
1125 facts and not facts *)
1126 let smart_candidates_facts, smart_candidates_other =
1127 if is_prod || not(smart) then [],[]
1129 let sgl1,sgl2 = List.partition test smart_global_cands in
1130 let sll1,sll2 = List.partition test smart_local_cands in
1131 let l1 = if is_eq then [] else sgl1@sll1 in
1133 if by && smart then given_candidates@sll2
1134 else if by then sll2
1139 smart_candidates_facts,
1140 sort_candidates status context (candidates_other),
1141 sort_candidates status context (smart_candidates_other)
1144 let applicative_case depth signature status flags gty cache =
1145 app_counter:= !app_counter+1;
1146 let _,_,metasenv,subst,_ = status#obj in
1147 let context = ctx_of gty in
1148 let tcache = cache.facts in
1149 let is_prod, is_eq =
1150 let status, t = term_of_cic_term status gty context in
1151 let t = NCicReduction.whd status subst context t in
1153 | NCic.Prod _ -> true, false
1154 | _ -> false, NCicParamod.is_equation status metasenv subst context t
1156 debug_print ~depth (lazy (string_of_bool is_eq));
1158 let candidates_facts, smart_candidates_facts,
1159 candidates_other, smart_candidates_other =
1160 get_candidates ~smart:true depth
1161 flags status tcache signature gty
1163 let sm = if is_eq || is_prod then 0 else 2 in
1164 let sm1 = if flags.last then 2 else 0 in
1165 let maxd = (depth + 1 = flags.maxdepth) in
1166 let try_candidates only_one sm acc candidates =
1169 if (only_one && (elems <> [])) then elems
1171 match try_candidate (~smart:sm)
1172 flags depth status cache.unit_eq context cand with
1174 | Some x -> x::elems)
1177 (* if the goal is the last one we stop at the first fact *)
1178 let elems = try_candidates flags.last sm [] candidates_facts in
1179 (* now we add smart_facts *)
1180 let elems = try_candidates flags.last sm elems smart_candidates_facts in
1181 (* if we are at maxdepth and the goal is not a product we are done
1182 similarly, if the goal is the last one and we already found a
1184 if (maxd && not(is_prod)) || (flags.last && elems<>[]) then elems
1186 let elems = try_candidates false 2 elems candidates_other in
1187 debug_print ~depth (lazy ("not facts: try smart application"));
1188 try_candidates false 2 elems smart_candidates_other
1194 (* gty is supposed to be meta-closed *)
1195 let is_subsumed depth filter_depth status gty cache =
1196 if cache=[] then false else (
1197 debug_print ~depth (lazy("Subsuming " ^ (ppterm status gty)));
1198 let n,h,metasenv,subst,obj = status#obj in
1199 let ctx = ctx_of gty in
1200 let _ , raw_gty = term_of_cic_term status gty ctx in
1201 let target = NCicSubstitution.lift status 1 raw_gty in
1202 (* we compute candidates using the perforated type *)
1209 perforate_small status subst metasenv ctx raw_gty in
1210 let weak = mk_cic_term ctx raw_weak in
1211 debug_print ~depth (lazy ("weak_gty:" ^ NTacStatus.ppterm status weak));
1215 (* candidates must only be searched w.r.t the given context *)
1218 let idx = List.assq ctx cache in
1221 Ncic_termSet.elements
1222 (InvRelDiscriminationTree.retrieve_unifiables idx weak)
1224 with Not_found -> []
1226 (* this is a dirty trick: the first argument of an application is used
1227 to remember at which depth a goal failed *)
1229 let ctx = ctx_of t in
1230 let _, src = term_of_cic_term status t ctx in
1232 | NCic.Appl [NCic.Implicit (`Typeof d); t]
1233 when d <= depth -> Some (mk_cic_term ctx t)
1236 if filter_depth then HExtlib.filter_map filter candidates else candidates in
1238 (lazy ("failure candidates: " ^ string_of_int (List.length candidates)));
1242 let _ , source = term_of_cic_term status t ctx in
1244 NCic.Prod("foo",source,target) in
1245 let metasenv,j,_,_ =
1246 NCicMetaSubst.mk_meta
1247 metasenv ctx ~with_type:implication `IsType in
1248 let status = status#set_obj (n,h,metasenv,subst,obj) in
1249 let status = status#set_stack [([1,Open j],[],[],`NoTag)] in
1251 let status = NTactics.intro_tac "foo" status in
1253 NTactics.apply_tac ("",0,Ast.NCic (NCic.Rel 1)) status
1255 if (head_goals status#stack = []) then raise Found
1260 with Found -> debug_print ~depth (lazy "success");true)
1263 let rec guess_name name ctx =
1264 if name = "_" then guess_name "auto" ctx else
1265 if not (List.mem_assoc name ctx) then name else
1266 guess_name (name^"'") ctx
1269 let is_prod status =
1270 let _, ctx, gty = current_goal status in
1271 let status, gty = apply_subst status ctx gty in
1272 let _, raw_gty = term_of_cic_term status gty ctx in
1274 | NCic.Prod (name,src,_) ->
1275 let status, src = whd status ~delta:0 ctx (mk_cic_term ctx src) in
1276 (match snd (term_of_cic_term status src ctx) with
1277 | NCic.Const(NReference.Ref (_,NReference.Ind _) as r)
1278 | NCic.Appl (NCic.Const(NReference.Ref (_,NReference.Ind _) as r)::_) ->
1279 let _,_,itys,_,_ = NCicEnvironment.get_checked_indtys status r in
1281 (* | [_,_,_,[_;_]] con nat va, ovviamente, in loop *)
1283 | [_,_,_,[]] -> `Inductive (guess_name name ctx)
1284 | _ -> `Some (guess_name name ctx))
1285 | _ -> `Some (guess_name name ctx))
1288 let intro ~depth status facts name =
1289 let status = NTactics.intro_tac name status in
1290 let _, ctx, ngty = current_goal status in
1291 let t = mk_cic_term ctx (NCic.Rel 1) in
1292 let status, keys = keys_of_term status t in
1293 let facts = List.fold_left (add_to_th t) facts keys in
1294 debug_print ~depth (lazy ("intro: "^ name));
1295 (* unprovability is not stable w.r.t introduction *)
1299 let rec intros_facts ~depth status facts =
1300 if List.length (head_goals status#stack) <> 1 then status, facts else
1301 match is_prod status with
1305 intro ~depth status facts name
1306 in intros_facts ~depth status facts
1307 (* | `Inductive name ->
1308 let status = NTactics.case1_tac name status in
1309 intros_facts ~depth status facts *)
1310 | _ -> status, facts
1313 let intros ~depth status cache =
1314 match is_prod status with
1317 let trace = cache.trace in
1319 intros_facts ~depth status cache.facts
1321 if head_goals status#stack = [] then
1322 let status = NTactics.merge_tac status in
1323 [(0,Ast.Ident("__intros",None)),status], cache
1325 (* we reindex the equation from scratch *)
1326 let unit_eq = index_local_equations status#eq_cache status in
1327 let status = NTactics.merge_tac status in
1328 [(0,Ast.Ident("__intros",None)),status],
1329 init_cache ~facts ~unit_eq () ~trace
1333 let reduce ~whd ~depth status g =
1334 let n,h,metasenv,subst,o = status#obj in
1335 let attr, ctx, ty = NCicUtils.lookup_meta g metasenv in
1336 let ty = NCicUntrusted.apply_subst status subst ctx ty in
1338 (if whd then NCicReduction.whd else NCicTacReduction.normalize) status ~subst ctx ty
1343 (lazy ("reduced to: "^ status#ppterm ctx subst metasenv ty'));
1345 (g,(attr,ctx,ty'))::(List.filter (fun (i,_) -> i<>g) metasenv)
1347 let status = status#set_obj (n,h,metasenv,subst,o) in
1348 (* we merge to gain a depth level; the previous goal level should
1350 let status = NTactics.merge_tac status in
1352 [(!candidate_no,Ast.Ident("__whd",None)),status])
1355 let is_meta status gty =
1356 let _, ty = term_of_cic_term status gty (ctx_of gty) in
1358 | NCic.Meta _ -> true
1362 let do_something signature flags status g depth gty cache =
1363 (* if the goal is meta we close it with I:True. This should work
1364 thnaks to the toplogical sorting of goals. *)
1365 if is_meta status gty then
1366 let t = Ast.Ident("I",None) in
1367 debug_print (lazy ("using default term" ^ (NotationPp.pp_term status) t));
1368 let s = NTactics.apply_tac ("",0,t) status in
1371 let l0, cache = intros ~depth status cache in
1372 if l0 <> [] then l0, cache
1375 let l = reduce ~whd:true ~depth status g in
1376 (* if l <> [] then l,cache else *)
1377 (* backward aplications *)
1382 ((!candidate_no,Ast.Ident("__paramod",None)),s))
1383 (auto_eq_check cache.unit_eq status)
1386 if ((l1 <> []) && flags.last) then [] else
1387 applicative_case depth signature status flags gty cache
1391 (fun ((_,t),_) -> toref incr_nominations statistics t) l2;
1392 (* states in l1 have have an empty set of subgoals: no point to sort them *)
1394 (lazy ("alternatives = " ^ (string_of_int (List.length (l1@l@l2)))));
1395 (* we order alternatives w.r.t the number of subgoals they open *)
1396 l1 @ (sort_new_elems l2) @ l, cache
1399 let pp_goal = function
1400 | (_,Continuationals.Stack.Open i)
1401 | (_,Continuationals.Stack.Closed i) -> string_of_int i
1404 let pp_goals status l =
1408 let gty = get_goalty status i in
1409 NTacStatus.ppterm status gty)
1416 let compare = Pervasives.compare
1420 module MS = HTopoSort.Make(M)
1423 let sort_tac status =
1425 match status#stack with
1426 | [] -> assert false
1427 | (goals, t, k, tag) :: s ->
1428 let g = head_goals status#stack in
1430 (List.rev (MS.topological_sort g (deps status))) in
1431 noprint (lazy ("old g = " ^
1432 String.concat "," (List.map string_of_int g)));
1433 noprint (lazy ("sorted goals = " ^
1434 String.concat "," (List.map string_of_int sortedg)));
1435 let is_it i = function
1436 | (_,Continuationals.Stack.Open j )
1437 | (_,Continuationals.Stack.Closed j ) -> i = j
1440 List.map (fun i -> List.find (is_it i) goals) sortedg
1442 (sorted_goals, t, k, tag) :: s
1444 status#set_stack gstatus
1447 let clean_up_tac status =
1449 match status#stack with
1450 | [] -> assert false
1451 | (g, t, k, tag) :: s ->
1452 let is_open = function
1453 | (_,Continuationals.Stack.Open _) -> true
1454 | (_,Continuationals.Stack.Closed _) -> false
1456 let g' = List.filter is_open g in
1457 (g', t, k, tag) :: s
1459 status#set_stack gstatus
1462 let focus_tac focus status =
1464 match status#stack with
1465 | [] -> assert false
1466 | (g, t, k, tag) :: s ->
1467 let in_focus = function
1468 | (_,Continuationals.Stack.Open i)
1469 | (_,Continuationals.Stack.Closed i) -> List.mem i focus
1471 let focus,others = List.partition in_focus g
1473 (* we need to mark it as a BranchTag, otherwise cannot merge later *)
1474 (focus,[],[],`BranchTag) :: (others, t, k, tag) :: s
1476 status#set_stack gstatus
1479 let deep_focus_tac level focus status =
1480 let in_focus = function
1481 | (_,Continuationals.Stack.Open i)
1482 | (_,Continuationals.Stack.Closed i) -> List.mem i focus
1484 let rec slice level gs =
1485 if level = 0 then [],[],gs else
1487 | [] -> assert false
1488 | (g, t, k, tag) :: s ->
1489 let f,o,gs = slice (level-1) s in
1490 let f1,o1 = List.partition in_focus g
1492 (f1,[],[],`BranchTag)::f, (o1, t, k, tag)::o, gs
1495 let f,o,s = slice level status#stack in f@o@s
1497 status#set_stack gstatus
1500 let move_to_side level status =
1501 match status#stack with
1502 | [] -> assert false
1504 let is_open = function
1505 | (_,Continuationals.Stack.Open i) -> Some i
1506 | (_,Continuationals.Stack.Closed _) -> None
1508 let others = menv_closure status (stack_goals (level-1) tl) in
1509 List.for_all (fun i -> IntSet.mem i others)
1510 (HExtlib.filter_map is_open g)
1512 let top_cache ~depth top status cache =
1514 let unit_eq = index_local_equations status#eq_cache status in
1515 {cache with unit_eq = unit_eq}
1518 let rec auto_clusters ?(top=false)
1519 flags signature cache depth status : unit =
1520 debug_print ~depth (lazy ("entering auto clusters at depth " ^
1521 (string_of_int depth)));
1522 debug_print ~depth (pptrace status cache.trace);
1523 (* ignore(Unix.select [] [] [] 0.01); *)
1524 let status = clean_up_tac status in
1525 let goals = head_goals status#stack in
1527 if depth = 0 then raise (Proved (status, cache.trace))
1529 let status = NTactics.merge_tac status in
1531 let l,tree = cache.under_inspection in
1533 | [] -> cache (* possible because of intros that cleans the cache *)
1534 | a::tl -> let tree = rm_from_th a tree a in
1535 {cache with under_inspection = tl,tree}
1537 auto_clusters flags signature cache (depth-1) status
1538 else if List.length goals < 2 then
1539 let cache = top_cache ~depth top status cache in
1540 auto_main flags signature cache depth status
1542 let all_goals = open_goals (depth+1) status in
1543 debug_print ~depth (lazy ("goals = " ^
1544 String.concat "," (List.map string_of_int all_goals)));
1545 let classes = HExtlib.clusters (deps status) all_goals in
1546 (* if any of the classes exceed maxwidth we fail *)
1549 if List.length gl > flags.maxwidth then
1551 debug_print ~depth (lazy "FAIL GLOBAL WIDTH");
1552 HLog.warn (sprintf "global width (%u) exceeded: %u"
1553 flags.maxwidth (List.length gl));
1554 raise (Gaveup cache.failures)
1555 end else ()) classes;
1556 if List.length classes = 1 then
1558 {flags with last = (List.length all_goals = 1)} in
1559 (* no need to cluster *)
1560 let cache = top_cache ~depth top status cache in
1561 auto_main flags signature cache depth status
1563 let classes = if top then List.rev classes else classes in
1569 ("cluster:" ^ String.concat "," (List.map string_of_int l)))
1571 (* we now process each cluster *)
1572 let status,cache,b =
1574 (fun (status,cache,b) gl ->
1576 {flags with last = (List.length gl = 1)} in
1577 let lold = List.length status#stack in
1578 debug_print ~depth (lazy ("stack length = " ^
1579 (string_of_int lold)));
1580 let fstatus = deep_focus_tac (depth+1) gl status in
1581 let cache = top_cache ~depth top fstatus cache in
1583 debug_print ~depth (lazy ("focusing on" ^
1584 String.concat "," (List.map string_of_int gl)));
1585 auto_main flags signature cache depth fstatus; assert false
1587 | Proved(status,trace) ->
1588 let status = NTactics.merge_tac status in
1589 let cache = {cache with trace = trace} in
1590 let lnew = List.length status#stack in
1591 assert (lold = lnew);
1593 | Gaveup failures when top ->
1594 let cache = {cache with failures = failures} in
1597 (status,cache,false) classes
1599 let rec final_merge n s =
1600 if n = 0 then s else final_merge (n-1) (NTactics.merge_tac s)
1601 in let status = final_merge depth status
1602 in if b then raise (Proved(status,cache.trace)) else raise (Gaveup cache.failures)
1606 (* BRAND NEW VERSION *)
1607 auto_main flags signature cache depth status: unit =
1608 debug_print ~depth (lazy "entering auto main");
1609 debug_print ~depth (pptrace status cache.trace);
1610 debug_print ~depth (lazy ("stack length = " ^
1611 (string_of_int (List.length status#stack))));
1612 (* ignore(Unix.select [] [] [] 0.01); *)
1613 let status = sort_tac (clean_up_tac status) in
1614 let goals = head_goals status#stack in
1616 | [] when depth = 0 -> raise (Proved (status,cache.trace))
1618 let status = NTactics.merge_tac status in
1620 let l,tree = cache.under_inspection in
1622 | [] -> cache (* possible because of intros that cleans the cache *)
1623 | a::tl -> let tree = rm_from_th a tree a in
1624 {cache with under_inspection = tl,tree}
1626 auto_clusters flags signature cache (depth-1) status
1628 if depth > 0 && move_to_side depth status
1630 let status = NTactics.merge_tac status in
1632 let l,tree = cache.under_inspection in
1634 | [] -> cache (* possible because of intros that cleans the cache*)
1635 | a::tl -> let tree = rm_from_th a tree a in
1636 {cache with under_inspection = tl,tree}
1638 auto_clusters flags signature cache (depth-1) status
1640 let ng = List.length goals in
1641 (* moved inside auto_clusters *)
1642 if ng > flags.maxwidth then begin
1643 debug_print ~depth (lazy "FAIL LOCAL WIDTH");
1644 HLog.warn (sprintf "local width (%u) exceeded: %u"
1646 raise (Gaveup cache.failures)
1647 end else if depth = flags.maxdepth then
1648 raise (Gaveup cache.failures)
1650 let status = NTactics.branch_tac ~force:true status in
1651 let g,gctx, gty = current_goal status in
1652 let ctx,ty = close status g in
1653 let closegty = mk_cic_term ctx ty in
1654 let status, gty = apply_subst status gctx gty in
1655 debug_print ~depth (lazy("Attacking goal " ^
1656 string_of_int g ^ " : "^ppterm status gty));
1657 debug_print ~depth (lazy ("current failures: " ^
1658 string_of_int (List.length (all_elements ctx cache.failures))));
1660 let _,_,metasenv,subst,_ = status#obj in
1661 NCicParamod.is_equation status metasenv subst ctx ty in
1662 (* if the goal is an equality we artificially raise its depth up to
1663 flags.maxdepth - 1 *)
1664 if (not flags.last && is_eq && (depth < (flags.maxdepth -2))) then
1665 (* for efficiency reasons, in this case we severely cripple the
1667 (debug_print ~depth (lazy ("RAISING DEPTH TO " ^ string_of_int (depth+1)));
1668 auto_main flags signature cache (depth+1) status)
1669 (* check for loops *)
1670 else if is_subsumed depth false status closegty (snd cache.under_inspection) then
1671 (debug_print ~depth (lazy "SUBSUMED");
1672 raise (Gaveup cache.failures))
1673 (* check for failures *)
1674 else if is_subsumed depth true status closegty cache.failures then
1675 (debug_print ~depth (lazy "ALREADY MET");
1676 raise (Gaveup cache.failures))
1678 let new_sig = height_of_goal g status in
1679 if new_sig < signature then
1680 (debug_print ~depth (lazy ("news = " ^ (string_of_int new_sig)));
1681 debug_print ~depth (lazy ("olds = " ^ (string_of_int signature))));
1682 let alternatives, cache =
1683 do_something signature flags status g depth gty cache in
1686 let l,tree = cache.under_inspection in
1687 let l,tree = closegty::l, add_to_th closegty tree closegty in
1688 {cache with under_inspection = l,tree}
1692 (fun allfailures ((_,t),status) ->
1694 (lazy ("(re)considering goal " ^
1695 (string_of_int g) ^" : "^ppterm status gty));
1696 debug_print (~depth:depth)
1697 (lazy ("Case: " ^ NotationPp.pp_term status t));
1699 if t=Ast.Ident("__whd",None) ||
1700 t=Ast.Ident("__intros",None)
1702 else depth+1,loop_cache in
1703 let cache = add_to_trace status ~depth cache t in
1704 let cache = {cache with failures = allfailures} in
1706 auto_clusters flags signature cache depth status;
1709 debug_print ~depth (lazy "Failed");
1711 cache.failures alternatives in
1715 let dty = NCic.Appl [NCic.Implicit (`Typeof depth); ty] in
1718 (*prerr_endline ("FAILURE : " ^ ppterm status gty);*)
1719 add_to_th newfail failures closegty
1721 debug_print ~depth (lazy "no more candidates");
1722 raise (Gaveup failures)
1725 let int name l def =
1726 try int_of_string (List.assoc name l)
1727 with Failure _ | Not_found -> def
1730 module AstSet = Set.Make(struct type t = Ast.term let compare = compare end)
1732 let cleanup_trace s trace =
1733 (* removing duplicates *)
1736 (fun acc t -> AstSet.add t acc)
1737 AstSet.empty trace in
1738 let trace = AstSet.elements trace_set
1739 (* filtering facts *)
1743 | Ast.NRef (NReference.Ref (u,_)) -> not (is_a_fact_obj s u)
1747 let auto_tac ~params:(univ,flags) ?(trace_ref=ref []) status =
1748 let oldstatus = status in
1749 let status = (status:> NTacStatus.tac_status) in
1750 let goals = head_goals status#stack in
1751 let status, facts = mk_th_cache status goals in
1752 (* let unit_eq = index_local_equations status#eq_cache status in *)
1753 let cache = init_cache ~facts () in
1754 (* pp_th status facts; *)
1756 NDiscriminationTree.DiscriminationTree.iter status#auto_cache (fun p t ->
1758 NDiscriminationTree.NCicIndexable.string_of_path p ^ " |--> " ^
1759 String.concat "\n " (List.map (
1760 status#ppterm ~metasenv:[] ~context:[] ~subst:[])
1761 (NDiscriminationTree.TermSet.elements t))
1769 let status, res = disambiguate status [] t None in
1770 let _,res = term_of_cic_term status res (ctx_of res)
1772 in Some (List.map to_Ast l)
1774 let depth = int "depth" flags 3 in
1775 let size = int "size" flags 10 in
1776 let width = int "width" flags 4 (* (3+List.length goals)*) in
1778 (* let goals = List.map (fun i -> (i,P)) goals in *)
1779 let signature = height_of_goals status in
1782 candidates = candidates;
1786 timeout = Unix.gettimeofday() +. 3000.;
1789 let initial_time = Unix.gettimeofday() in
1794 ("TIME ELAPSED:"^string_of_float(Unix.gettimeofday()-.initial_time)));
1796 ("Applicative nodes:"^string_of_int !app_counter));
1797 raise (Error (lazy "auto gave up", None)))
1799 let _ = debug_print (lazy("\n\nRound "^string_of_int x^"\n")) in
1800 let flags = { flags with maxdepth = x }
1802 try auto_clusters (~top:true) flags signature cache 0 status;assert false
1804 try auto_main flags signature cache 0 status;assert false
1807 | Gaveup _ -> up_to (x+1) y
1808 | Proved (s,trace) ->
1809 debug_print (lazy ("proved at depth " ^ string_of_int x));
1810 List.iter (toref incr_uses statistics) trace;
1811 let trace = cleanup_trace s trace in
1812 let _ = debug_print (pptrace status trace) in
1815 | (g,t,k,f) :: rest -> (filter_open g,t,k,f):: rest
1818 let s = s#set_stack stack in
1820 oldstatus#set_status s
1822 let s = up_to depth depth in
1823 debug_print (print_stat status statistics);
1825 ("TIME ELAPSED:"^string_of_float(Unix.gettimeofday()-.initial_time)));
1827 ("Applicative nodes:"^string_of_int !app_counter));
1831 let auto_tac ~params:(_,flags as params) ?trace_ref =
1832 if List.mem_assoc "demod" flags then
1834 else if List.mem_assoc "paramod" flags then
1836 else if List.mem_assoc "fast_paramod" flags then
1837 fast_eq_check_tac ~params
1838 else auto_tac ~params ?trace_ref