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 NotationPp.pp_term status (Ast.NCic (NCic.Const a)) ^ ": rel = " ^
77 (string_of_float (relevance v)) ^
78 "; uses = " ^ (string_of_int !(v.uses)) ^
79 "; nom = " ^ (string_of_int !(v.nominations)) in
80 lazy ("\n\nSTATISTICS:\n" ^
81 String.concat "\n" (List.map vstring l))
83 (* ======================= utility functions ========================= *)
84 module IntSet = Set.Make(struct type t = int let compare = compare end)
86 let get_sgoalty status g =
87 let _,_,metasenv,subst,_ = status#obj in
89 let _, ctx, ty = NCicUtils.lookup_meta g metasenv in
90 let ty = NCicUntrusted.apply_subst status subst ctx ty in
91 let ctx = NCicUntrusted.apply_subst_context status
92 ~fix_projections:true subst ctx
94 NTacStatus.mk_cic_term ctx ty
95 with NCicUtils.Meta_not_found _ as exn -> fail ~exn (lazy "get_sgoalty")
99 let gty = get_sgoalty status g in
100 metas_of_term status gty
103 let menv_closure status gl =
104 let rec closure acc = function
106 | x::l when IntSet.mem x acc -> closure acc l
107 | x::l -> closure (IntSet.add x acc) (deps status x @ l)
108 in closure IntSet.empty gl
111 (* we call a "fact" an object whose hypothesis occur in the goal
112 or in types of goal-variables *)
113 let branch status ty =
114 let status, ty, metas = saturate ~delta:0 status ty in
115 noprint (lazy ("saturated ty :" ^ (ppterm status ty)));
116 let g_metas = metas_of_term status ty in
117 let clos = menv_closure status g_metas in
118 (* let _,_,metasenv,_,_ = status#obj in *)
122 let _, m = term_of_cic_term status m (ctx_of m) in
124 | NCic.Meta(i,_) -> IntSet.add i acc
128 (* IntSet.subset menv clos *)
129 IntSet.cardinal(IntSet.diff menv clos)
131 let is_a_fact status ty = branch status ty = 0
133 let is_a_fact_obj s uri =
134 let obj = NCicEnvironment.get_checked_obj s uri in
136 | (_,_,[],[],NCic.Constant(_,_,_,ty,_)) ->
137 is_a_fact s (mk_cic_term [] ty)
138 (* aggiungere i costruttori *)
141 let is_a_fact_ast status subst metasenv ctx cand =
143 (lazy ("------- checking " ^ NotationPp.pp_term status cand));
144 let status, t = disambiguate status ctx ("",0,cand) None in
145 let status,t = term_of_cic_term status t ctx in
146 let ty = NCicTypeChecker.typeof status subst metasenv ctx t in
147 is_a_fact status (mk_cic_term ctx ty)
149 let current_goal status =
150 let open_goals = head_goals status#stack in
151 assert (List.length open_goals = 1);
152 let open_goal = List.hd open_goals in
153 let gty = get_goalty status open_goal in
154 let ctx = ctx_of gty in
157 let height_of_ref status (NReference.Ref (uri, x)) =
162 | NReference.CoFix _ ->
163 let _,height,_,_,_ = NCicEnvironment.get_checked_obj status uri in
165 | NReference.Def h -> h
166 | NReference.Fix (_,_,h) -> h
169 (*************************** height functions ********************************)
170 let fast_height_of_term status t =
174 NCic.Meta (_,(_,NCic.Ctx l)) -> List.iter aux l
178 | NCic.Implicit _ -> assert false
181 prerr_endline (status#ppterm ~metasenv:[] ~subst:[]
182 ~context:[] t ^ ":" ^ string_of_int (height_of_ref status nref));
184 h := max !h (height_of_ref status nref)
185 | NCic.Prod (_,t1,t2)
186 | NCic.Lambda (_,t1,t2) -> aux t1; aux t2
187 | NCic.LetIn (_,s,ty,t) -> aux s; aux ty; aux t
188 | NCic.Appl l -> List.iter aux l
189 | NCic.Match (_,outty,t,pl) -> aux outty; aux t; List.iter aux pl
194 let height_of_goal g status =
195 let ty = get_goalty status g in
196 let context = ctx_of ty in
197 let _, ty = term_of_cic_term status ty (ctx_of ty) in
198 let h = ref (fast_height_of_term status ty) in
201 | _, NCic.Decl ty -> h := max !h (fast_height_of_term status ty)
202 | _, NCic.Def (bo,ty) ->
203 h := max !h (fast_height_of_term status ty);
204 h := max !h (fast_height_of_term status bo);
210 let height_of_goals status =
211 let open_goals = head_goals status#stack in
212 assert (List.length open_goals > 0);
216 h := max !h (height_of_goal open_goal status))
218 noprint (lazy ("altezza sequente: " ^ string_of_int !h));
222 (* =============================== paramod =========================== *)
223 let solve f status eq_cache goal =
226 if fast then NCicParamod.fast_eq_check
227 else NCicParamod.paramod in
229 let n,h,metasenv,subst,o = status#obj in
230 let gname, ctx, gty = List.assoc goal metasenv in
231 let gty = NCicUntrusted.apply_subst status subst ctx gty in
232 let build_status (pt, _, metasenv, subst) =
234 noprint (lazy ("refining: "^(status#ppterm ctx subst metasenv pt)));
235 let stamp = Unix.gettimeofday () in
236 let metasenv, subst, pt, pty =
237 (* NCicRefiner.typeof status
238 (* (status#set_coerc_db NCicCoercion.empty_db) *)
239 metasenv subst ctx pt None in
240 debug_print (lazy ("refined: "^(status#ppterm ctx subst metasenv pt)));
241 noprint (lazy ("synt: "^(status#ppterm ctx subst metasenv pty)));
242 let metasenv, subst =
243 NCicUnification.unify status metasenv subst ctx gty pty *)
245 (status#set_coerc_db NCicCoercion.empty_db)
246 metasenv subst ctx pt (Some gty)
248 noprint (lazy (Printf.sprintf "Refined in %fs"
249 (Unix.gettimeofday() -. stamp)));
250 let status = status#set_obj (n,h,metasenv,subst,o) in
251 let metasenv = List.filter (fun j,_ -> j <> goal) metasenv in
252 let subst = (goal,(gname,ctx,pt,pty)) :: subst in
253 Some (status#set_obj (n,h,metasenv,subst,o))
255 NCicRefiner.RefineFailure msg
256 | NCicRefiner.Uncertain msg ->
257 debug_print (lazy ("WARNING: refining in fast_eq_check failed\n" ^
258 snd (Lazy.force msg) ^
259 "\n in the environment\n" ^
260 status#ppmetasenv subst metasenv)); None
261 | NCicRefiner.AssertFailure msg ->
262 debug_print (lazy ("WARNING: refining in fast_eq_check failed" ^
264 "\n in the environment\n" ^
265 status#ppmetasenv subst metasenv)); None
268 HExtlib.filter_map build_status
269 (f status metasenv subst ctx eq_cache (NCic.Rel ~-1,gty))
272 let fast_eq_check eq_cache status (goal:int) =
273 match solve NCicParamod.fast_eq_check status eq_cache goal with
274 | [] -> raise (Error (lazy "no proof found",None))
278 let dist_fast_eq_check eq_cache s =
279 NTactics.distribute_tac (fast_eq_check eq_cache) s
282 let auto_eq_check eq_cache status =
284 let s = dist_fast_eq_check eq_cache status in
287 | Error _ -> debug_print (lazy ("no paramod proof found"));[]
290 let index_local_equations eq_cache status =
291 noprint (lazy "indexing equations");
292 let open_goals = head_goals status#stack in
293 let open_goal = List.hd open_goals in
294 let ngty = get_goalty status open_goal in
295 let ctx = apply_subst_context ~fix_projections:true status (ctx_of ngty) in
300 let t = NCic.Rel !c in
302 let ty = NCicTypeChecker.typeof status [] [] ctx t in
303 if is_a_fact status (mk_cic_term ctx ty) then
304 (noprint(lazy("eq indexing " ^ (status#ppterm ctx [] [] ty)));
305 NCicParamod.forward_infer_step status [] [] ctx eq_cache t ty)
307 (noprint (lazy ("not a fact: " ^ (status#ppterm ctx [] [] ty)));
310 | NCicTypeChecker.TypeCheckerFailure _
311 | NCicTypeChecker.AssertFailure _ -> eq_cache)
315 let fast_eq_check_tac ~params s =
316 let unit_eq = index_local_equations s#eq_cache s in
317 dist_fast_eq_check unit_eq s
320 let paramod eq_cache status goal =
321 match solve NCicParamod.paramod status eq_cache goal with
322 | [] -> raise (Error (lazy "no proof found",None))
326 let paramod_tac ~params s =
327 let unit_eq = index_local_equations s#eq_cache s in
328 NTactics.distribute_tac (paramod unit_eq) s
331 let demod eq_cache status goal =
332 match solve NCicParamod.demod status eq_cache goal with
333 | [] -> raise (Error (lazy "no progress",None))
337 let demod_tac ~params s =
338 let unit_eq = index_local_equations s#eq_cache s in
339 NTactics.distribute_tac (demod unit_eq) s
343 let fast_eq_check_tac_all ~params eq_cache status =
344 let g,_,_ = current_goal status in
345 let allstates = fast_eq_check_all status eq_cache g in
346 let pseudo_low_tac s _ _ = s in
347 let pseudo_low_tactics =
348 List.map pseudo_low_tac allstates
350 List.map (fun f -> NTactics.distribute_tac f status) pseudo_low_tactics
355 let demod status eq_cache goal =
356 let n,h,metasenv,subst,o = status#obj in
357 let gname, ctx, gty = List.assoc goal metasenv in
358 let gty = NCicUntrusted.apply_subst subst ctx gty in
360 let demod_tac ~params s =
361 let unit_eq = index_local_equations s#eq_cache s in
362 dist_fast_eq_check unit_eq s
365 (*************** subsumption ****************)
367 let close_wrt_context status =
371 | name, NCic.Decl t -> NCic.Prod(name,t,ty)
372 | name, NCic.Def(bo, _) -> NCicSubstitution.subst status bo ty)
375 let args_for_context ?(k=1) ctx =
378 (fun (n,l) ctx_entry ->
380 | name, NCic.Decl t -> n+1,NCic.Rel(n)::l
381 | name, NCic.Def(bo, _) -> n+1,l)
385 let constant_for_meta status ctx ty i =
386 let name = "cic:/foo"^(string_of_int i)^".con" in
387 let uri = NUri.uri_of_string name in
388 let ty = close_wrt_context status ty ctx in
389 (* prerr_endline (status#ppterm [] [] [] ty); *)
390 let attr = (`Generated,`Definition,`Local) in
391 let obj = NCic.Constant([],name,None,ty,attr) in
392 (* Constant of relevance * string * term option * term * c_attr *)
396 let refresh metasenv =
398 (fun (metasenv,subst) (i,(iattr,ctx,ty)) ->
399 let ikind = NCicUntrusted.kind_of_meta iattr in
400 let metasenv,j,instance,ty =
401 NCicMetaSubst.mk_meta ~attrs:iattr
402 metasenv ctx ~with_type:ty ikind in
403 let s_entry = i,(iattr, ctx, instance, ty) in
404 let metasenv = List.filter (fun x,_ -> i <> x) metasenv in
405 metasenv,s_entry::subst)
406 (metasenv,[]) metasenv
408 (* close metasenv returns a ground instance of all the metas in the
409 metasenv, insantiatied with axioms, and the list of these axioms *)
410 let close_metasenv status metasenv subst =
412 let metasenv = NCicUntrusted.apply_subst_metasenv subst metasenv in
414 let metasenv = NCicUntrusted.sort_metasenv status subst metasenv in
416 (fun (subst,objs) (i,(iattr,ctx,ty)) ->
417 let ty = NCicUntrusted.apply_subst status subst ctx ty in
419 NCicUntrusted.apply_subst_context status ~fix_projections:true
421 let (uri,_,_,_,obj) as okind =
422 constant_for_meta status ctx ty i in
424 NCicEnvironment.check_and_add_obj status okind;
425 let iref = NReference.reference_of_spec uri NReference.Decl in
427 let args = args_for_context ctx in
428 if args = [] then NCic.Const iref
429 else NCic.Appl(NCic.Const iref::args)
431 (* prerr_endline (status#ppterm ctx [] [] iterm); *)
432 let s_entry = i, ([], ctx, iterm, ty)
433 in s_entry::subst,okind::objs
434 with _ -> assert false)
438 let ground_instances status gl =
439 let _,_,metasenv,subst,_ = status#obj in
440 let subset = menv_closure status gl in
441 let submenv = List.filter (fun (x,_) -> IntSet.mem x subset) metasenv in
443 let submenv = metasenv in
445 let subst, objs = close_metasenv status submenv subst in
449 let (_, ctx, t, _) = List.assoc i subst in
450 noprint (lazy (status#ppterm ctx [] [] t));
452 (fun (uri,_,_,_,_) as obj ->
453 NCicEnvironment.invalidate_item status (`Obj (uri, obj)))
458 Not_found -> assert false
462 let replace_meta status i args target =
463 let rec aux k = function
464 (* TODO: local context *)
465 | NCic.Meta (j,lc) when i = j ->
469 List.map (NCicSubstitution.subst_meta status lc) args in
470 NCic.Appl(NCic.Rel k::args))
471 | NCic.Meta (j,lc) as m ->
478 aux k (NCicSubstitution.lift status n t)) l))))
479 | t -> NCicUtils.map status (fun _ k -> k+1) k aux t
484 let close_wrt_metasenv status subst =
486 (fun ty (i,(iattr,ctx,mty)) ->
487 let mty = NCicUntrusted.apply_subst status subst ctx mty in
489 NCicUntrusted.apply_subst_context status ~fix_projections:true
491 let cty = close_wrt_context status mty ctx in
492 let name = "foo"^(string_of_int i) in
493 let ty = NCicSubstitution.lift status 1 ty in
494 let args = args_for_context ~k:1 ctx in
495 (* prerr_endline (status#ppterm ctx [] [] iterm); *)
496 let ty = replace_meta status i args ty
498 NCic.Prod(name,cty,ty))
502 let _,_,metasenv,subst,_ = status#obj in
503 let subset = menv_closure status [g] in
504 let subset = IntSet.remove g subset in
505 let elems = IntSet.elements subset in
506 let _, ctx, ty = NCicUtils.lookup_meta g metasenv in
507 let ty = NCicUntrusted.apply_subst status subst ctx ty in
508 noprint (lazy ("metas in " ^ (status#ppterm ctx [] metasenv ty)));
509 noprint (lazy (String.concat ", " (List.map string_of_int elems)));
510 let submenv = List.filter (fun (x,_) -> IntSet.mem x subset) metasenv in
511 let submenv = List.rev (NCicUntrusted.sort_metasenv status subst submenv) in
513 let submenv = metasenv in
515 let ty = close_wrt_metasenv status subst ty submenv in
516 noprint (lazy (status#ppterm ctx [] [] ty));
520 (****************** smart application ********************)
522 let saturate_to_ref status metasenv subst ctx nref ty =
523 let height = height_of_ref status nref in
524 let rec aux metasenv ty args =
525 let ty,metasenv,moreargs =
526 NCicMetaSubst.saturate status ~delta:height metasenv subst ctx ty 0 in
528 | NCic.Const(NReference.Ref (_,NReference.Def _) as nre)
530 let _, _, bo, _, _, _ = NCicEnvironment.get_checked_def status nre in
531 aux metasenv bo (args@moreargs)
532 | NCic.Appl(NCic.Const(NReference.Ref (_,NReference.Def _) as nre)::tl)
534 let _, _, bo, _, _, _ = NCicEnvironment.get_checked_def status nre in
535 aux metasenv (NCic.Appl(bo::tl)) (args@moreargs)
536 | _ -> ty,metasenv,(args@moreargs)
540 let smart_apply t unit_eq status g =
541 let n,h,metasenv,subst,o = status#obj in
542 let gname, ctx, gty = List.assoc g metasenv in
543 (* let ggty = mk_cic_term context gty in *)
544 let status, t = disambiguate status ctx t None in
545 let status,t = term_of_cic_term status t ctx in
546 let _,_,metasenv,subst,_ = status#obj in
547 let ty = NCicTypeChecker.typeof status subst metasenv ctx t in
548 let ty,metasenv,args =
551 | NCic.Appl(NCic.Const(nref)::_) ->
552 saturate_to_ref status metasenv subst ctx nref ty
554 NCicMetaSubst.saturate status metasenv subst ctx ty 0 in
555 let metasenv,j,inst,_ = NCicMetaSubst.mk_meta metasenv ctx `IsTerm in
556 let status = status#set_obj (n,h,metasenv,subst,o) in
557 let pterm = if args=[] then t else
559 | NCic.Appl l -> NCic.Appl(l@args)
560 | _ -> NCic.Appl(t::args)
562 noprint(lazy("pterm " ^ (status#ppterm ctx [] [] pterm)));
563 noprint(lazy("pty " ^ (status#ppterm ctx [] [] ty)));
566 NUri.uri_of_string "cic:/matita/basics/logic/eq_coerc.con" in
567 let ref = NReference.reference_of_spec uri (NReference.Def(2)) in
571 NCic.Appl[eq_coerc;ty;NCic.Implicit `Type;pterm;inst] in
572 let smart = mk_cic_term ctx smart in
574 let status = instantiate status g smart in
575 let _,_,metasenv,subst,_ = status#obj in
576 let _,ctx,jty = List.assoc j metasenv in
577 let jty = NCicUntrusted.apply_subst status subst ctx jty in
578 noprint(lazy("goal " ^ (status#ppterm ctx [] [] jty)));
579 fast_eq_check unit_eq status j
581 | NCicEnvironment.ObjectNotFound s as e ->
582 raise (Error (lazy "eq_coerc non yet defined",Some e))
583 | Error _ as e -> debug_print (lazy "error"); raise e
585 let compare_statuses ~past ~present =
586 let _,_,past,_,_ = past#obj in
587 let _,_,present,_,_ = present#obj in
588 List.map fst (List.filter (fun (i,_) -> not(List.mem_assoc i past)) present),
589 List.map fst (List.filter (fun (i,_) -> not (List.mem_assoc i present)) past)
592 (* paramodulation has only an implicit knoweledge of the symmetry of equality;
593 hence it is in trouble in proving (a = b) = (b = a) *)
594 let try_sym tac status g =
595 (* put the right uri *)
596 let sym_eq = Ast.Appl [Ast.Ident("sym_eq",`Ambiguous); Ast.Implicit `Vector] in
597 let _,_,metasenv,subst,_ = status#obj in
598 let _, context, gty = List.assoc g metasenv in
600 NCicParamod.is_equation status metasenv subst context gty
605 let new_status = instantiate_with_ast status g ("",0,sym_eq) in
606 let go, _ = compare_statuses ~past:status ~present:new_status in
607 assert (List.length go = 1);
608 let ng = List.hd go in
613 let smart_apply_tac t s =
614 let unit_eq = index_local_equations s#eq_cache s in
615 NTactics.distribute_tac (try_sym (smart_apply t unit_eq)) s
616 (* NTactics.distribute_tac (smart_apply t unit_eq) s *)
618 let smart_apply_auto t eq_cache =
619 NTactics.distribute_tac (try_sym (smart_apply t eq_cache))
620 (* NTactics.distribute_tac (smart_apply t eq_cache) *)
623 (****************** types **************)
626 type th_cache = (NCic.context * InvRelDiscriminationTree.t) list
628 (* cartesian: term set list -> term list set *)
631 [] -> NDiscriminationTree.TermListSet.empty
633 NDiscriminationTree.TermSet.fold
634 (fun x acc -> NDiscriminationTree.TermListSet.add [x] acc) l NDiscriminationTree.TermListSet.empty
636 let rest = cartesian tl in
637 NDiscriminationTree.TermSet.fold
639 NDiscriminationTree.TermListSet.fold (fun l acc' -> NDiscriminationTree.TermListSet.add (x::l) acc') rest acc
640 ) he NDiscriminationTree.TermListSet.empty
643 (* all_keys_of_cic_type: term -> term set *)
644 let all_keys_of_cic_type status metasenv subst context ty =
646 (* Here we are dropping the metasenv, but this should not raise any
647 exception (hopefully...) *)
649 NCicMetaSubst.saturate status ~delta:max_int metasenv subst context ty 0
655 NCic.Appl (he::tl) ->
658 let wty = NCicReduction.whd status ~delta:0 ~subst context ty in
660 NDiscriminationTree.TermSet.add ty (aux ty)
662 NDiscriminationTree.TermSet.union
663 (NDiscriminationTree.TermSet.add ty (aux ty))
664 (NDiscriminationTree.TermSet.add wty (aux wty))
667 NDiscriminationTree.TermListSet.fold
668 (fun l acc -> NDiscriminationTree.TermSet.add (NCic.Appl l) acc)
669 (cartesian ((NDiscriminationTree.TermSet.singleton he)::tl'))
670 NDiscriminationTree.TermSet.empty
671 | _ -> NDiscriminationTree.TermSet.empty
673 let ty,ity = saturate ty in
674 let wty,iwty = saturate (NCicReduction.whd status ~delta:0 ~subst context ty) in
676 [ity, NDiscriminationTree.TermSet.add ty (aux ty)]
678 [ity, NDiscriminationTree.TermSet.add ty (aux ty) ;
679 iwty, NDiscriminationTree.TermSet.add wty (aux wty) ]
682 let all_keys_of_type status t =
683 let _,_,metasenv,subst,_ = status#obj in
684 let context = ctx_of t in
685 let status, t = apply_subst status context t in
687 all_keys_of_cic_type status metasenv subst context
688 (snd (term_of_cic_term status t context))
692 (fun (intros,keys) ->
694 NDiscriminationTree.TermSet.fold
695 (fun t acc -> Ncic_termSet.add (mk_cic_term context t) acc)
696 keys Ncic_termSet.empty
701 let keys_of_type status orig_ty =
702 (* Here we are dropping the metasenv (in the status), but this should not
703 raise any exception (hopefully...) *)
704 let _, ty, _ = saturate ~delta:max_int status orig_ty in
705 let _, ty = apply_subst status (ctx_of ty) ty in
708 let orig_ty' = NCicTacReduction.normalize ~subst context orig_ty in
709 if orig_ty' <> orig_ty then
710 let ty',_,_= NCicMetaSubst.saturate ~delta:0 metasenv subst context orig_ty' 0 in
716 (*CSC: strange: we keep ty, ty normalized and ty ~delta:(h-1) *)
718 let _, ty = term_of_cic_term status ty (ctx_of ty) in
720 | NCic.Const (NReference.Ref (_,(NReference.Def h | NReference.Fix (_,_,h))))
721 | NCic.Appl (NCic.Const(NReference.Ref(_,(NReference.Def h | NReference.Fix (_,_,h))))::_)
723 let _,ty,_= saturate status ~delta:(h-1) orig_ty in
730 let all_keys_of_term status t =
731 let status, orig_ty = typeof status (ctx_of t) t in
732 all_keys_of_type status orig_ty
735 let keys_of_term status t =
736 let status, orig_ty = typeof status (ctx_of t) t in
737 keys_of_type status orig_ty
740 let mk_th_cache status gl =
742 (fun (status, acc) g ->
743 let gty = get_goalty status g in
744 let ctx = ctx_of gty in
745 noprint(lazy("th cache for: "^ppterm status gty));
746 noprint(lazy("th cache in: "^ppcontext status ctx));
747 if List.mem_assq ctx acc then status, acc else
748 let idx = InvRelDiscriminationTree.empty in
751 (fun (status, i, idx) _ ->
752 let t = mk_cic_term ctx (NCic.Rel i) in
753 let status, keys = keys_of_term status t in
754 noprint(lazy("indexing: "^ppterm status t ^ ": " ^ string_of_int (List.length keys)));
756 List.fold_left (fun idx k ->
757 InvRelDiscriminationTree.index idx k t) idx keys
762 status, (ctx, idx) :: acc)
766 let all_elements ctx cache =
767 let dummy = mk_cic_term ctx (NCic.Meta (0,(0, (NCic.Irl 0)))) in
769 let idx = List.assq ctx cache in
770 Ncic_termSet.elements
771 (InvRelDiscriminationTree.retrieve_unifiables idx dummy)
774 let add_to_th t c ty =
775 let key_c = ctx_of t in
776 if not (List.mem_assq key_c c) then
777 (key_c ,InvRelDiscriminationTree.index
778 InvRelDiscriminationTree.empty ty t ) :: c
780 let rec replace = function
782 | (x, idx) :: tl when x == key_c ->
783 (x, InvRelDiscriminationTree.index idx ty t) :: tl
784 | x :: tl -> x :: replace tl
789 let rm_from_th t c ty =
790 let key_c = ctx_of t in
791 if not (List.mem_assq key_c c) then assert false
793 let rec replace = function
795 | (x, idx) :: tl when x == key_c ->
796 (x, InvRelDiscriminationTree.remove_index idx ty t) :: tl
797 | x :: tl -> x :: replace tl
802 let pp_idx status idx =
803 InvRelDiscriminationTree.iter idx
805 noprint(lazy("K: " ^ NCicInverseRelIndexable.string_of_path k));
807 (fun t -> debug_print(lazy("\t"^ppterm status t)))
811 let pp_th (status: #NTacStatus.pstatus) =
814 noprint(lazy( "-----------------------------------------------"));
815 noprint(lazy( (status#ppcontext ~metasenv:[] ~subst:[] ctx)));
816 noprint(lazy( "||====> "));
820 let search_in_th gty th =
821 let c = ctx_of gty in
822 let rec aux acc = function
823 | [] -> (* Ncic_termSet.elements *) acc
826 let idx = List.assoc(*q*) k th in
827 let acc = Ncic_termSet.union acc
828 (InvRelDiscriminationTree.retrieve_unifiables idx gty)
831 with Not_found -> aux acc tl
833 aux Ncic_termSet.empty c
837 do_types : bool; (* solve goals in Type *)
838 last : bool; (* last goal: take first solution only *)
839 candidates: Ast.term list option;
847 {facts : th_cache; (* positive results *)
848 under_inspection : cic_term list * th_cache; (* to prune looping *)
849 failures : th_cache; (* to avoid repetitions *)
850 unit_eq : NCicParamod.state;
854 let add_to_trace status ~depth cache t =
857 debug_print ~depth (lazy ("Adding to trace: " ^ NotationPp.pp_term status t));
858 {cache with trace = t::cache.trace}
859 | Ast.NCic _ (* local candidate *)
860 | _ -> (*not an application *) cache
862 let pptrace status tr =
863 (lazy ("Proof Trace: " ^ (String.concat ";"
864 (List.map (NotationPp.pp_term status) tr))))
866 let remove_from_trace cache t =
869 (match cache.trace with
870 | _::tl -> {cache with trace = tl}
872 | Ast.NCic _ (* local candidate *)
873 | _ -> (*not an application *) cache *)
876 type goal = int * sort (* goal, depth, sort *)
877 type fail = goal * cic_term
878 type candidate = int * Ast.term (* unique candidate number, candidate *)
880 exception Gaveup of th_cache (* failure cache *)
881 exception Proved of NTacStatus.tac_status * Ast.term list
883 (* let close_failures _ c = c;; *)
884 (* let prunable _ _ _ = false;; *)
885 (* let cache_examine cache gty = `Notfound;; *)
886 (* let put_in_subst s _ _ _ = s;; *)
887 (* let add_to_cache_and_del_from_orlist_if_green_cut _ _ c _ _ o f _ = c, o, f, false ;; *)
888 (* let cache_add_underinspection c _ _ = c;; *)
890 let init_cache ?(facts=[]) ?(under_inspection=[],[])
892 ?(unit_eq=NCicParamod.empty_state)
897 under_inspection = under_inspection;
901 let only signature _context candidate = true
903 (* TASSI: nel trie ci mettiamo solo il body, non il ty *)
905 NCicTypeChecker.typeof ~subst:[] ~metasenv:[] [] candidate
907 let height = fast_height_of_term status candidate_ty in
908 let rc = signature >= height in
910 noprint (lazy ("Filtro: " ^ status#ppterm ~context:[] ~subst:[]
911 ~metasenv:[] candidate ^ ": " ^ string_of_int height))
913 noprint (lazy ("Tengo: " ^ status#ppterm ~context:[] ~subst:[]
914 ~metasenv:[] candidate ^ ": " ^ string_of_int height));
919 let candidate_no = ref 0;;
921 let openg_no status = List.length (head_goals status#stack)
923 let sort_candidates status ctx candidates =
924 let _,_,metasenv,subst,_ = status#obj in
926 let status,ct = disambiguate status ctx ("",0,cand) None in
927 let status,t = term_of_cic_term status ct ctx in
928 let ty = NCicTypeChecker.typeof status subst metasenv ctx t in
929 let res = branch status (mk_cic_term ctx ty) in
930 noprint (lazy ("branch factor for: " ^ (ppterm status ct) ^ " = "
931 ^ (string_of_int res)));
934 let candidates = List.map (fun t -> branch t,t) candidates in
936 List.sort (fun (a,_) (b,_) -> a - b) candidates in
937 let candidates = List.map snd candidates in
938 noprint (lazy ("candidates =\n" ^ (String.concat "\n"
939 (List.map (NotationPp.pp_term status) candidates))));
942 let sort_new_elems l =
943 List.sort (fun (_,s1) (_,s2) -> openg_no s1 - openg_no s2) l
945 let rec stack_goals level gs =
950 let is_open = function
951 | (_,Continuationals.Stack.Open i) -> Some i
952 | (_,Continuationals.Stack.Closed _) -> None
954 HExtlib.filter_map is_open g @ stack_goals (level-1) s
957 let open_goals level status = stack_goals level status#stack
960 let try_candidate ?(smart=0) flags depth status eq_cache ctx t =
962 let old_og_no = List.length (open_goals (depth+1) status) in
963 debug_print ~depth (lazy ("try " ^ (NotationPp.pp_term status) t));
965 if smart= 0 then NTactics.apply_tac ("",0,t) status
966 else if smart = 1 then smart_apply_auto ("",0,t) eq_cache status
967 else (* smart = 2: both *)
968 try NTactics.apply_tac ("",0,t) status
970 smart_apply_auto ("",0,t) eq_cache status
972 (* we compare the expected branching with the actual one and
973 prune the candidate when the latter is larger. The optimization
974 is meant to rule out stange applications of flexible terms,
975 such as the application of eq_f that always succeeds.
976 There is some gain but less than expected *)
977 let og_no = List.length (open_goals (depth+1) status) in
978 let status, cict = disambiguate status ctx ("",0,t) None in
979 let status,ct = term_of_cic_term status cict ctx in
980 let _,_,metasenv,subst,_ = status#obj in
981 let ty = NCicTypeChecker.typeof status subst metasenv ctx ct in
982 let res = branch status (mk_cic_term ctx ty) in
983 let diff = og_no - old_og_no in
984 debug_print (lazy ("expected branching: " ^ (string_of_int res)));
985 debug_print (lazy ("actual: branching" ^ (string_of_int diff)));
986 (* one goal is closed by the application *)
987 if og_no - old_og_no >= res then
988 (debug_print (lazy ("branch factor for: " ^ (ppterm status cict) ^ " = "
989 ^ (string_of_int res) ^ " vs. " ^ (string_of_int og_no)));
990 debug_print ~depth (lazy "strange application"); None)
992 (incr candidate_no; Some ((!candidate_no,t),status))
993 with Error (msg,exn) -> debug_print ~depth (lazy "failed"); None
996 let sort_of status subst metasenv ctx t =
997 let ty = NCicTypeChecker.typeof status subst metasenv ctx t in
998 let metasenv',ty = NCicUnification.fix_sorts status metasenv subst ty in
999 assert (metasenv = metasenv');
1000 NCicTypeChecker.typeof status subst metasenv ctx ty
1003 let type0= NUri.uri_of_string ("cic:/matita/pts/Type0.univ")
1006 let perforate_small status subst metasenv context t =
1007 let rec aux = function
1008 | NCic.Appl (hd::tl) ->
1010 let s = sort_of status subst metasenv context t in
1012 | NCic.Sort(NCic.Type [`Type,u])
1013 when u=type0 -> NCic.Meta (0,(0,NCic.Irl 0))
1016 NCic.Appl (hd::List.map map tl)
1022 let get_cands retrieve_for diff empty gty weak_gty =
1023 let cands = retrieve_for gty in
1025 | None -> cands, empty
1027 let more_cands = retrieve_for weak_gty in
1028 cands, diff more_cands cands
1031 let get_candidates ?(smart=true) depth flags status cache signature gty =
1032 let universe = status#auto_cache in
1033 let _,_,metasenv,subst,_ = status#obj in
1034 let context = ctx_of gty in
1035 let _, raw_gty = term_of_cic_term status gty context in
1036 let is_prod, is_eq =
1037 let status, t = term_of_cic_term status gty context in
1038 let t = NCicReduction.whd status subst context t in
1040 | NCic.Prod _ -> true, false
1041 | _ -> false, NCicParamod.is_equation status metasenv subst context t
1043 debug_print ~depth (lazy ("gty:" ^ NTacStatus.ppterm status gty));
1045 NCicParamod.is_equation status metasenv subst context raw_gty
1047 let raw_weak_gty, weak_gty =
1054 perforate_small status subst metasenv context raw_gty in
1055 let weak = mk_cic_term context raw_weak in
1056 debug_print ~depth (lazy ("weak_gty:" ^ NTacStatus.ppterm status weak));
1057 Some raw_weak, Some (weak)
1061 (* we now compute global candidates *)
1062 let global_cands, smart_global_cands =
1064 let to_ast = function
1065 | NCic.Const r when true
1066 (*is_relevant statistics r*) -> Some (Ast.NRef r)
1067 (* | NCic.Const _ -> None *)
1068 | _ -> assert false in
1070 to_ast (NDiscriminationTree.TermSet.elements s) in
1073 (NDiscriminationTree.DiscriminationTree.retrieve_unifiables universe)
1074 NDiscriminationTree.TermSet.diff
1075 NDiscriminationTree.TermSet.empty
1076 raw_gty raw_weak_gty in
1078 (* we now compute local candidates *)
1079 let local_cands,smart_local_cands =
1082 let _status, t = term_of_cic_term status t context
1084 List.map to_ast (Ncic_termSet.elements s) in
1087 (fun ty -> search_in_th ty cache)
1088 Ncic_termSet.diff Ncic_termSet.empty gty weak_gty in
1090 (* we now splits candidates in facts or not facts *)
1091 let test = is_a_fact_ast status subst metasenv context in
1092 let by,given_candidates =
1093 match flags.candidates with
1095 | None -> false, [] in
1096 (* we compute candidates to be applied in normal mode, splitted in
1097 facts and not facts *)
1098 let candidates_facts,candidates_other =
1099 (* warning : the order between global_cands and local_cand is
1100 relevant. In this way we process first local cands *)
1101 let l1,l2 = List.partition test (global_cands@local_cands) in
1102 (* if the goal is an equation we avoid to apply unit equalities,
1103 since superposition should take care of them; refl is an
1104 exception since it prompts for convertibility *)
1105 let l1 = if is_eq then [Ast.Ident("refl",`Ambiguous)] else l1 in
1107 (* if smart given candidates are applied in smart mode *)
1108 if by && smart then []
1109 else if by then given_candidates
1113 (* we now compute candidates to be applied in smart mode, splitted in
1114 facts and not facts *)
1115 let smart_candidates_facts, smart_candidates_other =
1116 if is_prod || not(smart) then [],[]
1118 let l1,l2 = List.partition test (smart_local_cands@smart_global_cands) in
1119 let l1 = if is_eq then [] else l1 in
1120 let l2 = if by then given_candidates else l2
1125 smart_candidates_facts,
1126 sort_candidates status context (candidates_other),
1127 sort_candidates status context (smart_candidates_other)
1130 let applicative_case depth signature status flags gty cache =
1131 app_counter:= !app_counter+1;
1132 let _,_,metasenv,subst,_ = status#obj in
1133 let context = ctx_of gty in
1134 let tcache = cache.facts in
1135 let is_prod, is_eq =
1136 let status, t = term_of_cic_term status gty context in
1137 let t = NCicReduction.whd status subst context t in
1139 | NCic.Prod _ -> true, false
1140 | _ -> false, NCicParamod.is_equation status metasenv subst context t
1142 debug_print ~depth (lazy (string_of_bool is_eq));
1144 let candidates_facts, smart_candidates_facts,
1145 candidates_other, smart_candidates_other =
1146 get_candidates ~smart:true depth
1147 flags status tcache signature gty
1149 let sm = if is_eq || is_prod then 0 else 2 in
1150 let sm1 = if flags.last then 2 else 0 in
1151 let maxd = (depth + 1 = flags.maxdepth) in
1152 let try_candidates only_one sm acc candidates =
1155 if (only_one && (elems <> [])) then elems
1157 match try_candidate (~smart:sm)
1158 flags depth status cache.unit_eq context cand with
1160 | Some x -> x::elems)
1163 (* if the goal is the last one we stop at the first fact *)
1164 let elems = try_candidates flags.last sm [] candidates_facts in
1165 (* now we add smart_facts *)
1166 let elems = try_candidates flags.last sm elems smart_candidates_facts in
1167 (* if we are at maxdepth and the goal is not a product we are done
1168 similarly, if the goal is the last one and we already found a
1170 if (maxd && not(is_prod)) || (flags.last && elems<>[]) then elems
1172 let elems = try_candidates false 2 elems candidates_other in
1173 debug_print ~depth (lazy ("not facts: try smart application"));
1174 try_candidates false 2 elems smart_candidates_other
1180 (* gty is supposed to be meta-closed *)
1181 let is_subsumed depth filter_depth status gty cache =
1182 if cache=[] then false else (
1183 debug_print ~depth (lazy("Subsuming " ^ (ppterm status gty)));
1184 let n,h,metasenv,subst,obj = status#obj in
1185 let ctx = ctx_of gty in
1186 let _ , raw_gty = term_of_cic_term status gty ctx in
1187 let target = NCicSubstitution.lift status 1 raw_gty in
1188 (* we compute candidates using the perforated type *)
1195 perforate_small status subst metasenv ctx raw_gty in
1196 let weak = mk_cic_term ctx raw_weak in
1197 debug_print ~depth (lazy ("weak_gty:" ^ NTacStatus.ppterm status weak));
1201 (* candidates must only be searched w.r.t the given context *)
1204 let idx = List.assq ctx cache in
1207 Ncic_termSet.elements
1208 (InvRelDiscriminationTree.retrieve_unifiables idx weak)
1210 with Not_found -> []
1212 (* this is a dirty trick: the first argument of an application is used
1213 to remember at which depth a goal failed *)
1215 let ctx = ctx_of t in
1216 let _, src = term_of_cic_term status t ctx in
1218 | NCic.Appl [NCic.Implicit (`Typeof d); t]
1219 when d <= depth -> Some (mk_cic_term ctx t)
1222 if filter_depth then HExtlib.filter_map filter candidates else candidates in
1224 (lazy ("failure candidates: " ^ string_of_int (List.length candidates)));
1228 let _ , source = term_of_cic_term status t ctx in
1230 NCic.Prod("foo",source,target) in
1231 let metasenv,j,_,_ =
1232 NCicMetaSubst.mk_meta
1233 metasenv ctx ~with_type:implication `IsType in
1234 let status = status#set_obj (n,h,metasenv,subst,obj) in
1235 let status = status#set_stack [([1,Open j],[],[],`NoTag)] in
1237 let status = NTactics.intro_tac "foo" status in
1239 NTactics.apply_tac ("",0,Ast.NCic (NCic.Rel 1)) status
1241 if (head_goals status#stack = []) then raise Found
1246 with Found -> debug_print ~depth (lazy "success");true)
1249 let rec guess_name name ctx =
1250 if name = "_" then guess_name "auto" ctx else
1251 if not (List.mem_assoc name ctx) then name else
1252 guess_name (name^"'") ctx
1255 let is_prod status =
1256 let _, ctx, gty = current_goal status in
1257 let status, gty = apply_subst status ctx gty in
1258 let _, raw_gty = term_of_cic_term status gty ctx in
1260 | NCic.Prod (name,src,_) ->
1261 let status, src = whd status ~delta:0 ctx (mk_cic_term ctx src) in
1262 (match snd (term_of_cic_term status src ctx) with
1263 | NCic.Const(NReference.Ref (_,NReference.Ind _) as r)
1264 | NCic.Appl (NCic.Const(NReference.Ref (_,NReference.Ind _) as r)::_) ->
1265 let _,_,itys,_,_ = NCicEnvironment.get_checked_indtys status r in
1267 (* | [_,_,_,[_;_]] con nat va, ovviamente, in loop *)
1269 | [_,_,_,[]] -> `Inductive (guess_name name ctx)
1270 | _ -> `Some (guess_name name ctx))
1271 | _ -> `Some (guess_name name ctx))
1274 let intro ~depth status facts name =
1275 let status = NTactics.intro_tac name status in
1276 let _, ctx, ngty = current_goal status in
1277 let t = mk_cic_term ctx (NCic.Rel 1) in
1278 let status, keys = keys_of_term status t in
1279 let facts = List.fold_left (add_to_th t) facts keys in
1280 debug_print ~depth (lazy ("intro: "^ name));
1281 (* unprovability is not stable w.r.t introduction *)
1285 let rec intros_facts ~depth status facts =
1286 if List.length (head_goals status#stack) <> 1 then status, facts else
1287 match is_prod status with
1291 intro ~depth status facts name
1292 in intros_facts ~depth status facts
1293 (* | `Inductive name ->
1294 let status = NTactics.case1_tac name status in
1295 intros_facts ~depth status facts *)
1296 | _ -> status, facts
1299 let intros ~depth status cache =
1300 match is_prod status with
1303 let trace = cache.trace in
1305 intros_facts ~depth status cache.facts
1307 if head_goals status#stack = [] then
1308 let status = NTactics.merge_tac status in
1309 [(0,Ast.Ident("__intros",`Ambiguous)),status], cache
1311 (* we reindex the equation from scratch *)
1312 let unit_eq = index_local_equations status#eq_cache status in
1313 let status = NTactics.merge_tac status in
1314 [(0,Ast.Ident("__intros",`Ambiguous)),status],
1315 init_cache ~facts ~unit_eq () ~trace
1319 let reduce ~whd ~depth status g =
1320 let n,h,metasenv,subst,o = status#obj in
1321 let attr, ctx, ty = NCicUtils.lookup_meta g metasenv in
1322 let ty = NCicUntrusted.apply_subst status subst ctx ty in
1324 (if whd then NCicReduction.whd else NCicTacReduction.normalize) status ~subst ctx ty
1329 (lazy ("reduced to: "^ status#ppterm ctx subst metasenv ty'));
1331 (g,(attr,ctx,ty'))::(List.filter (fun (i,_) -> i<>g) metasenv)
1333 let status = status#set_obj (n,h,metasenv,subst,o) in
1334 (* we merge to gain a depth level; the previous goal level should
1336 let status = NTactics.merge_tac status in
1338 [(!candidate_no,Ast.Ident("__whd",`Ambiguous)),status])
1341 let do_something signature flags status g depth gty cache =
1342 let l0, cache = intros ~depth status cache in
1343 if l0 <> [] then l0, cache
1346 let l = reduce ~whd:true ~depth status g in
1347 (* if l <> [] then l,cache else *)
1348 (* backward aplications *)
1353 ((!candidate_no,Ast.Ident("__paramod",`Ambiguous)),s))
1354 (auto_eq_check cache.unit_eq status)
1357 if ((l1 <> []) && flags.last) then [] else
1358 applicative_case depth signature status flags gty cache
1362 (fun ((_,t),_) -> toref incr_nominations statistics t) l2;
1363 (* states in l1 have have an empty set of subgoals: no point to sort them *)
1365 (lazy ("alternatives = " ^ (string_of_int (List.length (l1@l@l2)))));
1366 (* we order alternatives w.r.t the number of subgoals they open *)
1367 l1 @ (sort_new_elems l2) @ l, cache
1370 let pp_goal = function
1371 | (_,Continuationals.Stack.Open i)
1372 | (_,Continuationals.Stack.Closed i) -> string_of_int i
1375 let pp_goals status l =
1379 let gty = get_goalty status i in
1380 NTacStatus.ppterm status gty)
1387 let compare = Pervasives.compare
1391 module MS = HTopoSort.Make(M)
1394 let sort_tac status =
1396 match status#stack with
1397 | [] -> assert false
1398 | (goals, t, k, tag) :: s ->
1399 let g = head_goals status#stack in
1401 (List.rev (MS.topological_sort g (deps status))) in
1402 noprint (lazy ("old g = " ^
1403 String.concat "," (List.map string_of_int g)));
1404 noprint (lazy ("sorted goals = " ^
1405 String.concat "," (List.map string_of_int sortedg)));
1406 let is_it i = function
1407 | (_,Continuationals.Stack.Open j )
1408 | (_,Continuationals.Stack.Closed j ) -> i = j
1411 List.map (fun i -> List.find (is_it i) goals) sortedg
1413 (sorted_goals, t, k, tag) :: s
1415 status#set_stack gstatus
1418 let clean_up_tac status =
1420 match status#stack with
1421 | [] -> assert false
1422 | (g, t, k, tag) :: s ->
1423 let is_open = function
1424 | (_,Continuationals.Stack.Open _) -> true
1425 | (_,Continuationals.Stack.Closed _) -> false
1427 let g' = List.filter is_open g in
1428 (g', t, k, tag) :: s
1430 status#set_stack gstatus
1433 let focus_tac focus status =
1435 match status#stack with
1436 | [] -> assert false
1437 | (g, t, k, tag) :: s ->
1438 let in_focus = function
1439 | (_,Continuationals.Stack.Open i)
1440 | (_,Continuationals.Stack.Closed i) -> List.mem i focus
1442 let focus,others = List.partition in_focus g
1444 (* we need to mark it as a BranchTag, otherwise cannot merge later *)
1445 (focus,[],[],`BranchTag) :: (others, t, k, tag) :: s
1447 status#set_stack gstatus
1450 let deep_focus_tac level focus status =
1451 let in_focus = function
1452 | (_,Continuationals.Stack.Open i)
1453 | (_,Continuationals.Stack.Closed i) -> List.mem i focus
1455 let rec slice level gs =
1456 if level = 0 then [],[],gs else
1458 | [] -> assert false
1459 | (g, t, k, tag) :: s ->
1460 let f,o,gs = slice (level-1) s in
1461 let f1,o1 = List.partition in_focus g
1463 (f1,[],[],`BranchTag)::f, (o1, t, k, tag)::o, gs
1466 let f,o,s = slice level status#stack in f@o@s
1468 status#set_stack gstatus
1471 let move_to_side level status =
1472 match status#stack with
1473 | [] -> assert false
1475 let is_open = function
1476 | (_,Continuationals.Stack.Open i) -> Some i
1477 | (_,Continuationals.Stack.Closed _) -> None
1479 let others = menv_closure status (stack_goals (level-1) tl) in
1480 List.for_all (fun i -> IntSet.mem i others)
1481 (HExtlib.filter_map is_open g)
1483 let top_cache ~depth top status cache =
1485 let unit_eq = index_local_equations status#eq_cache status in
1486 {cache with unit_eq = unit_eq}
1489 let rec auto_clusters ?(top=false)
1490 flags signature cache depth status : unit =
1491 debug_print ~depth (lazy ("entering auto clusters at depth " ^
1492 (string_of_int depth)));
1493 debug_print ~depth (pptrace status cache.trace);
1494 (* ignore(Unix.select [] [] [] 0.01); *)
1495 let status = clean_up_tac status in
1496 let goals = head_goals status#stack in
1498 if depth = 0 then raise (Proved (status, cache.trace))
1500 let status = NTactics.merge_tac status in
1502 let l,tree = cache.under_inspection in
1504 | [] -> cache (* possible because of intros that cleans the cache *)
1505 | a::tl -> let tree = rm_from_th a tree a in
1506 {cache with under_inspection = tl,tree}
1508 auto_clusters flags signature cache (depth-1) status
1509 else if List.length goals < 2 then
1510 let cache = top_cache ~depth top status cache in
1511 auto_main flags signature cache depth status
1513 let all_goals = open_goals (depth+1) status in
1514 debug_print ~depth (lazy ("goals = " ^
1515 String.concat "," (List.map string_of_int all_goals)));
1516 let classes = HExtlib.clusters (deps status) all_goals in
1517 (* if any of the classes exceed maxwidth we fail *)
1520 if List.length gl > flags.maxwidth then
1522 debug_print ~depth (lazy "FAIL GLOBAL WIDTH");
1523 HLog.warn (sprintf "global width (%u) exceeded: %u"
1524 flags.maxwidth (List.length gl));
1525 raise (Gaveup cache.failures)
1526 end else ()) classes;
1527 if List.length classes = 1 then
1529 {flags with last = (List.length all_goals = 1)} in
1530 (* no need to cluster *)
1531 let cache = top_cache ~depth top status cache in
1532 auto_main flags signature cache depth status
1534 let classes = if top then List.rev classes else classes in
1540 ("cluster:" ^ String.concat "," (List.map string_of_int l)))
1542 (* we now process each cluster *)
1543 let status,cache,b =
1545 (fun (status,cache,b) gl ->
1547 {flags with last = (List.length gl = 1)} in
1548 let lold = List.length status#stack in
1549 debug_print ~depth (lazy ("stack length = " ^
1550 (string_of_int lold)));
1551 let fstatus = deep_focus_tac (depth+1) gl status in
1552 let cache = top_cache ~depth top fstatus cache in
1554 debug_print ~depth (lazy ("focusing on" ^
1555 String.concat "," (List.map string_of_int gl)));
1556 auto_main flags signature cache depth fstatus; assert false
1558 | Proved(status,trace) ->
1559 let status = NTactics.merge_tac status in
1560 let cache = {cache with trace = trace} in
1561 let lnew = List.length status#stack in
1562 assert (lold = lnew);
1564 | Gaveup failures when top ->
1565 let cache = {cache with failures = failures} in
1568 (status,cache,false) classes
1570 let rec final_merge n s =
1571 if n = 0 then s else final_merge (n-1) (NTactics.merge_tac s)
1572 in let status = final_merge depth status
1573 in if b then raise (Proved(status,cache.trace)) else raise (Gaveup cache.failures)
1577 (* BRAND NEW VERSION *)
1578 auto_main flags signature cache depth status: unit =
1579 debug_print ~depth (lazy "entering auto main");
1580 debug_print ~depth (pptrace status cache.trace);
1581 debug_print ~depth (lazy ("stack length = " ^
1582 (string_of_int (List.length status#stack))));
1583 (* ignore(Unix.select [] [] [] 0.01); *)
1584 let status = sort_tac (clean_up_tac status) in
1585 let goals = head_goals status#stack in
1587 | [] when depth = 0 -> raise (Proved (status,cache.trace))
1589 let status = NTactics.merge_tac status in
1591 let l,tree = cache.under_inspection in
1593 | [] -> cache (* possible because of intros that cleans the cache *)
1594 | a::tl -> let tree = rm_from_th a tree a in
1595 {cache with under_inspection = tl,tree}
1597 auto_clusters flags signature cache (depth-1) status
1599 if depth > 0 && move_to_side depth status
1601 let status = NTactics.merge_tac status in
1603 let l,tree = cache.under_inspection in
1605 | [] -> cache (* possible because of intros that cleans the cache*)
1606 | a::tl -> let tree = rm_from_th a tree a in
1607 {cache with under_inspection = tl,tree}
1609 auto_clusters flags signature cache (depth-1) status
1611 let ng = List.length goals in
1612 (* moved inside auto_clusters *)
1613 if ng > flags.maxwidth then begin
1614 debug_print ~depth (lazy "FAIL LOCAL WIDTH");
1615 HLog.warn (sprintf "local width (%u) exceeded: %u"
1617 raise (Gaveup cache.failures)
1618 end else if depth = flags.maxdepth then
1619 raise (Gaveup cache.failures)
1621 let status = NTactics.branch_tac ~force:true status in
1622 let g,gctx, gty = current_goal status in
1623 let ctx,ty = close status g in
1624 let closegty = mk_cic_term ctx ty in
1625 let status, gty = apply_subst status gctx gty in
1626 debug_print ~depth (lazy("Attacking goal " ^
1627 string_of_int g ^ " : "^ppterm status gty));
1628 debug_print ~depth (lazy ("current failures: " ^
1629 string_of_int (List.length (all_elements ctx cache.failures))));
1631 let _,_,metasenv,subst,_ = status#obj in
1632 NCicParamod.is_equation status metasenv subst ctx ty in
1633 (* if the goal is an equality we artificially raise its depth up to
1634 flags.maxdepth - 1 *)
1635 if (not flags.last && is_eq && (depth < (flags.maxdepth -1))) then
1636 (* for efficiency reasons, in this case we severely cripple the
1638 (debug_print ~depth (lazy ("RAISING DEPTH TO " ^ string_of_int (depth+1)));
1639 auto_main flags signature cache (depth+1) status)
1640 (* check for loops *)
1641 else if is_subsumed depth false status closegty (snd cache.under_inspection) then
1642 (debug_print ~depth (lazy "SUBSUMED");
1643 raise (Gaveup cache.failures))
1644 (* check for failures *)
1645 else if is_subsumed depth true status closegty cache.failures then
1646 (debug_print ~depth (lazy "ALREADY MET");
1647 raise (Gaveup cache.failures))
1649 let new_sig = height_of_goal g status in
1650 if new_sig < signature then
1651 (debug_print ~depth (lazy ("news = " ^ (string_of_int new_sig)));
1652 debug_print ~depth (lazy ("olds = " ^ (string_of_int signature))));
1653 let alternatives, cache =
1654 do_something signature flags status g depth gty cache in
1657 let l,tree = cache.under_inspection in
1658 let l,tree = closegty::l, add_to_th closegty tree closegty in
1659 {cache with under_inspection = l,tree}
1663 (fun allfailures ((_,t),status) ->
1665 (lazy ("(re)considering goal " ^
1666 (string_of_int g) ^" : "^ppterm status gty));
1667 debug_print (~depth:depth)
1668 (lazy ("Case: " ^ NotationPp.pp_term status t));
1670 if t=Ast.Ident("__whd",`Ambiguous) ||
1671 t=Ast.Ident("__intros",`Ambiguous)
1673 else depth+1,loop_cache in
1674 let cache = add_to_trace status ~depth cache t in
1675 let cache = {cache with failures = allfailures} in
1677 auto_clusters flags signature cache depth status;
1680 debug_print ~depth (lazy "Failed");
1682 cache.failures alternatives in
1686 let dty = NCic.Appl [NCic.Implicit (`Typeof depth); ty] in
1689 prerr_endline ("FAILURE : " ^ ppterm status gty);
1690 add_to_th newfail failures closegty
1692 debug_print ~depth (lazy "no more candidates");
1693 raise (Gaveup failures)
1696 let int name l def =
1697 try int_of_string (List.assoc name l)
1698 with Failure _ | Not_found -> def
1701 module AstSet = Set.Make(struct type t = Ast.term let compare = compare end)
1703 let cleanup_trace s trace =
1704 (* removing duplicates *)
1707 (fun acc t -> AstSet.add t acc)
1708 AstSet.empty trace in
1709 let trace = AstSet.elements trace_set
1710 (* filtering facts *)
1714 | Ast.NRef (NReference.Ref (u,_)) -> not (is_a_fact_obj s u)
1718 let auto_tac ~params:(univ,flags) ?(trace_ref=ref []) status =
1719 let oldstatus = status in
1720 let status = (status:> NTacStatus.tac_status) in
1721 let goals = head_goals status#stack in
1722 let status, facts = mk_th_cache status goals in
1723 (* let unit_eq = index_local_equations status#eq_cache status in *)
1724 let cache = init_cache ~facts () in
1725 (* pp_th status facts; *)
1727 NDiscriminationTree.DiscriminationTree.iter status#auto_cache (fun p t ->
1729 NDiscriminationTree.NCicIndexable.string_of_path p ^ " |--> " ^
1730 String.concat "\n " (List.map (
1731 status#ppterm ~metasenv:[] ~context:[] ~subst:[])
1732 (NDiscriminationTree.TermSet.elements t))
1740 let status, res = disambiguate status [] t None in
1741 let _,res = term_of_cic_term status res (ctx_of res)
1743 in Some (List.map to_Ast l)
1745 let depth = int "depth" flags 3 in
1746 let size = int "size" flags 10 in
1747 let width = int "width" flags 4 (* (3+List.length goals)*) in
1749 (* let goals = List.map (fun i -> (i,P)) goals in *)
1750 let signature = height_of_goals status in
1753 candidates = candidates;
1757 timeout = Unix.gettimeofday() +. 3000.;
1760 let initial_time = Unix.gettimeofday() in
1765 ("TIME ELAPSED:"^string_of_float(Unix.gettimeofday()-.initial_time)));
1767 ("Applicative nodes:"^string_of_int !app_counter));
1768 raise (Error (lazy "auto gave up", None)))
1770 let _ = debug_print (lazy("\n\nRound "^string_of_int x^"\n")) in
1771 let flags = { flags with maxdepth = x }
1773 try auto_clusters (~top:true) flags signature cache 0 status;assert false
1775 try auto_main flags signature cache 0 status;assert false
1778 | Gaveup _ -> up_to (x+1) y
1779 | Proved (s,trace) ->
1780 debug_print (lazy ("proved at depth " ^ string_of_int x));
1781 List.iter (toref incr_uses statistics) trace;
1782 let trace = cleanup_trace s trace in
1783 let _ = debug_print (pptrace status trace) in
1786 | (g,t,k,f) :: rest -> (filter_open g,t,k,f):: rest
1789 let s = s#set_stack stack in
1791 oldstatus#set_status s
1793 let s = up_to depth depth in
1794 debug_print (print_stat status statistics);
1796 ("TIME ELAPSED:"^string_of_float(Unix.gettimeofday()-.initial_time)));
1798 ("Applicative nodes:"^string_of_int !app_counter));
1802 let auto_tac ~params:(_,flags as params) ?trace_ref =
1803 if List.mem_assoc "demod" flags then
1805 else if List.mem_assoc "paramod" flags then
1807 else if List.mem_assoc "fast_paramod" flags then
1808 fast_eq_check_tac ~params
1809 else auto_tac ~params ?trace_ref