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 facts " ^ 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 debug_print (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 U: 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 F: 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 let open_goals = head_goals status#stack in
292 let open_goal = List.hd open_goals in
293 debug_print (lazy ("indexing equations for " ^ string_of_int open_goal));
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 (debug_print(lazy("eq indexing " ^ (status#ppterm ctx [] [] ty)));
305 NCicParamod.forward_infer_step 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 (`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 debug_print(lazy("goal " ^ (status#ppterm ctx [] [] jty)));
579 let res = fast_eq_check unit_eq status j in
580 debug_print(lazy("ritorno da fast_eq_check"));
583 | NCicEnvironment.ObjectNotFound s as e ->
584 raise (Error (lazy "eq_coerc non yet defined",Some e))
585 | Error _ as e -> debug_print (lazy "error"); raise e
588 let compare_statuses ~past ~present =
589 let _,_,past,_,_ = past#obj in
590 let _,_,present,_,_ = present#obj in
591 List.map fst (List.filter (fun (i,_) -> not(List.mem_assoc i past)) present),
592 List.map fst (List.filter (fun (i,_) -> not (List.mem_assoc i present)) past)
595 (* paramodulation has only an implicit knoweledge of the symmetry of equality;
596 hence it is in trouble in proving (a = b) = (b = a) *)
597 let try_sym tac status g =
598 let sym_eq = Ast.Appl [Ast.Ident("sym_eq",None); Ast.Implicit `Vector] in
599 let _,_,metasenv,subst,_ = status#obj in
600 let _, context, gty = List.assoc g metasenv in
602 NCicParamod.is_equation status metasenv subst context gty
607 let new_status = instantiate_with_ast status g ("",0,sym_eq) in
608 let go, _ = compare_statuses ~past:status ~present:new_status in
609 assert (List.length go = 1);
610 let ng = List.hd go in
615 let smart_apply_tac t s =
616 let unit_eq = index_local_equations s#eq_cache s in
617 NTactics.distribute_tac (try_sym (smart_apply t unit_eq)) s
618 (* NTactics.distribute_tac (smart_apply t unit_eq) s *)
620 let smart_apply_auto t eq_cache =
621 NTactics.distribute_tac (try_sym (smart_apply t eq_cache))
622 (* NTactics.distribute_tac (smart_apply t eq_cache) *)
625 (****************** types **************)
628 type th_cache = (NCic.context * InvRelDiscriminationTree.t) list
630 (* cartesian: term set list -> term list set *)
633 [] -> NDiscriminationTree.TermListSet.empty
635 NDiscriminationTree.TermSet.fold
636 (fun x acc -> NDiscriminationTree.TermListSet.add [x] acc) l NDiscriminationTree.TermListSet.empty
638 let rest = cartesian tl in
639 NDiscriminationTree.TermSet.fold
641 NDiscriminationTree.TermListSet.fold (fun l acc' -> NDiscriminationTree.TermListSet.add (x::l) acc') rest acc
642 ) he NDiscriminationTree.TermListSet.empty
645 (* all_keys_of_cic_type: term -> term set *)
646 let all_keys_of_cic_type status metasenv subst context ty =
648 (* Here we are dropping the metasenv, but this should not raise any
649 exception (hopefully...) *)
651 NCicMetaSubst.saturate status ~delta:max_int metasenv subst context ty 0
657 NCic.Appl (he::tl) ->
660 let wty = NCicReduction.whd status ~delta:0 ~subst context ty in
662 NDiscriminationTree.TermSet.add ty (aux ty)
664 NDiscriminationTree.TermSet.union
665 (NDiscriminationTree.TermSet.add ty (aux ty))
666 (NDiscriminationTree.TermSet.add wty (aux wty))
669 NDiscriminationTree.TermListSet.fold
670 (fun l acc -> NDiscriminationTree.TermSet.add (NCic.Appl l) acc)
671 (cartesian ((NDiscriminationTree.TermSet.singleton he)::tl'))
672 NDiscriminationTree.TermSet.empty
673 | _ -> NDiscriminationTree.TermSet.empty
675 let ty,ity = saturate ty in
676 let wty,iwty = saturate (NCicReduction.whd status ~delta:0 ~subst context ty) in
678 [ity, NDiscriminationTree.TermSet.add ty (aux ty)]
680 [ity, NDiscriminationTree.TermSet.add ty (aux ty) ;
681 iwty, NDiscriminationTree.TermSet.add wty (aux wty) ]
684 let all_keys_of_type status t =
685 let _,_,metasenv,subst,_ = status#obj in
686 let context = ctx_of t in
687 let status, t = apply_subst status context t in
689 all_keys_of_cic_type status metasenv subst context
690 (snd (term_of_cic_term status t context))
694 (fun (intros,keys) ->
696 NDiscriminationTree.TermSet.fold
697 (fun t acc -> Ncic_termSet.add (mk_cic_term context t) acc)
698 keys Ncic_termSet.empty
703 let keys_of_type status orig_ty =
704 (* Here we are dropping the metasenv (in the status), but this should not
705 raise any exception (hopefully...) *)
706 let _, ty, _ = saturate ~delta:max_int status orig_ty in
707 let _, ty = apply_subst status (ctx_of ty) ty in
710 let orig_ty' = NCicTacReduction.normalize ~subst context orig_ty in
711 if orig_ty' <> orig_ty then
712 let ty',_,_= NCicMetaSubst.saturate ~delta:0 metasenv subst context orig_ty' 0 in
718 (*CSC: strange: we keep ty, ty normalized and ty ~delta:(h-1) *)
720 let _, ty = term_of_cic_term status ty (ctx_of ty) in
722 | NCic.Const (NReference.Ref (_,(NReference.Def h | NReference.Fix (_,_,h))))
723 | NCic.Appl (NCic.Const(NReference.Ref(_,(NReference.Def h | NReference.Fix (_,_,h))))::_)
725 let _,ty,_= saturate status ~delta:(h-1) orig_ty in
732 let all_keys_of_term status t =
733 let status, orig_ty = typeof status (ctx_of t) t in
734 all_keys_of_type status orig_ty
737 let keys_of_term status t =
738 let status, orig_ty = typeof status (ctx_of t) t in
739 keys_of_type status orig_ty
742 let mk_th_cache status gl =
744 (fun (status, acc) g ->
745 let gty = get_goalty status g in
746 let ctx = ctx_of gty in
747 noprint(lazy("th cache for: "^ppterm status gty));
748 noprint(lazy("th cache in: "^ppcontext status ctx));
749 if List.mem_assq ctx acc then status, acc else
750 let idx = InvRelDiscriminationTree.empty in
753 (fun (status, i, idx) _ ->
754 let t = mk_cic_term ctx (NCic.Rel i) in
755 let status, keys = keys_of_term status t in
756 noprint(lazy("indexing: "^ppterm status t ^ ": " ^ string_of_int (List.length keys)));
758 List.fold_left (fun idx k ->
759 InvRelDiscriminationTree.index idx k t) idx keys
764 status, (ctx, idx) :: acc)
768 let all_elements ctx cache =
769 let dummy = mk_cic_term ctx (NCic.Meta (0,(0, (NCic.Irl 0)))) in
771 let idx = List.assq ctx cache in
772 Ncic_termSet.elements
773 (InvRelDiscriminationTree.retrieve_unifiables idx dummy)
776 let add_to_th t c ty =
777 let key_c = ctx_of t in
778 if not (List.mem_assq key_c c) then
779 (key_c ,InvRelDiscriminationTree.index
780 InvRelDiscriminationTree.empty ty t ) :: c
782 let rec replace = function
784 | (x, idx) :: tl when x == key_c ->
785 (x, InvRelDiscriminationTree.index idx ty t) :: tl
786 | x :: tl -> x :: replace tl
791 let rm_from_th t c ty =
792 let key_c = ctx_of t in
793 if not (List.mem_assq key_c c) then assert false
795 let rec replace = function
797 | (x, idx) :: tl when x == key_c ->
798 (x, InvRelDiscriminationTree.remove_index idx ty t) :: tl
799 | x :: tl -> x :: replace tl
804 let pp_idx status idx =
805 InvRelDiscriminationTree.iter idx
807 noprint(lazy("K: " ^ NCicInverseRelIndexable.string_of_path k));
809 (fun t -> debug_print(lazy("\t"^ppterm status t)))
813 let pp_th (status: #NTacStatus.pstatus) =
816 noprint(lazy( "-----------------------------------------------"));
817 noprint(lazy( (status#ppcontext ~metasenv:[] ~subst:[] ctx)));
818 noprint(lazy( "||====> "));
822 let search_in_th gty th =
823 let c = ctx_of gty in
824 let rec aux acc = function
825 | [] -> (* Ncic_termSet.elements *) acc
828 let idx = List.assoc(*q*) k th in
829 let acc = Ncic_termSet.union acc
830 (InvRelDiscriminationTree.retrieve_unifiables idx gty)
833 with Not_found -> aux acc tl
835 aux Ncic_termSet.empty c
839 do_types : bool; (* solve goals in Type *)
840 last : bool; (* last goal: take first solution only *)
841 candidates: Ast.term list option;
849 {facts : th_cache; (* positive results *)
850 under_inspection : cic_term list * th_cache; (* to prune looping *)
851 failures : th_cache; (* to avoid repetitions *)
852 unit_eq : NCicParamod.state;
856 let add_to_trace status ~depth cache t =
859 debug_print ~depth (lazy ("Adding to trace: " ^ NotationPp.pp_term status t));
860 {cache with trace = t::cache.trace}
861 | Ast.NCic _ (* local candidate *)
862 | _ -> (*not an application *) cache
864 let pptrace status tr =
865 (lazy ("Proof Trace: " ^ (String.concat ";"
866 (List.map (NotationPp.pp_term status) tr))))
868 let remove_from_trace cache t =
871 (match cache.trace with
872 | _::tl -> {cache with trace = tl}
874 | Ast.NCic _ (* local candidate *)
875 | _ -> (*not an application *) cache *)
878 type goal = int * sort (* goal, depth, sort *)
879 type fail = goal * cic_term
880 type candidate = int * Ast.term (* unique candidate number, candidate *)
882 exception Gaveup of th_cache (* failure cache *)
883 exception Proved of NTacStatus.tac_status * Ast.term list
885 (* let close_failures _ c = c;; *)
886 (* let prunable _ _ _ = false;; *)
887 (* let cache_examine cache gty = `Notfound;; *)
888 (* let put_in_subst s _ _ _ = s;; *)
889 (* let add_to_cache_and_del_from_orlist_if_green_cut _ _ c _ _ o f _ = c, o, f, false ;; *)
890 (* let cache_add_underinspection c _ _ = c;; *)
892 let init_cache ?(facts=[]) ?(under_inspection=[],[])
894 ?(unit_eq=NCicParamod.empty_state)
899 under_inspection = under_inspection;
903 let only signature _context candidate = true
905 (* TASSI: nel trie ci mettiamo solo il body, non il ty *)
907 NCicTypeChecker.typeof ~subst:[] ~metasenv:[] [] candidate
909 let height = fast_height_of_term status candidate_ty in
910 let rc = signature >= height in
912 noprint (lazy ("Filtro: " ^ status#ppterm ~context:[] ~subst:[]
913 ~metasenv:[] candidate ^ ": " ^ string_of_int height))
915 noprint (lazy ("Tengo: " ^ status#ppterm ~context:[] ~subst:[]
916 ~metasenv:[] candidate ^ ": " ^ string_of_int height));
921 let candidate_no = ref 0;;
923 let openg_no status = List.length (head_goals status#stack)
925 let sort_candidates status ctx candidates =
926 let _,_,metasenv,subst,_ = status#obj in
928 let status,ct = disambiguate status ctx ("",0,cand) None in
929 let status,t = term_of_cic_term status ct ctx in
930 let ty = NCicTypeChecker.typeof status subst metasenv ctx t in
931 let res = branch status (mk_cic_term ctx ty) in
932 noprint (lazy ("branch factor for: " ^ (ppterm status ct) ^ " = "
933 ^ (string_of_int res)));
936 let candidates = List.map (fun t -> branch t,t) candidates in
938 List.sort (fun (a,_) (b,_) -> a - b) candidates in
939 let candidates = List.map snd candidates in
940 noprint (lazy ("candidates =\n" ^ (String.concat "\n"
941 (List.map (NotationPp.pp_term status) candidates))));
944 let sort_new_elems l =
945 List.sort (fun (_,s1) (_,s2) -> openg_no s1 - openg_no s2) l
947 let rec stack_goals level gs =
952 let is_open = function
953 | (_,Continuationals.Stack.Open i) -> Some i
954 | (_,Continuationals.Stack.Closed _) -> None
956 HExtlib.filter_map is_open g @ stack_goals (level-1) s
959 let open_goals level status = stack_goals level status#stack
962 let try_candidate ?(smart=0) flags depth status eq_cache ctx t =
964 let old_og_no = List.length (open_goals (depth+1) status) in
965 debug_print ~depth (lazy ("try " ^ (string_of_int smart) ^ " : "
966 ^ (NotationPp.pp_term status) t));
968 if smart = 0 then NTactics.apply_tac ("",0,t) status
969 else if smart = 1 then
970 smart_apply_auto ("",0,t) eq_cache status
971 else (* smart = 2: both *)
972 try NTactics.apply_tac ("",0,t) status
974 smart_apply_auto ("",0,t) eq_cache status
976 (* FG: this optimization rules out some applications of
977 * lift_bind (from contribs/lambda_delta/Basic_2/substitution/lift.ma)
979 (* we compare the expected branching with the actual one and
980 prune the candidate when the latter is larger. The optimization
981 is meant to rule out stange applications of flexible terms,
982 such as the application of eq_f that always succeeds.
983 There is some gain but less than expected *)
984 let og_no = List.length (open_goals (depth+1) status) in
985 let status, cict = disambiguate status ctx ("",0,t) None in
986 let status,ct = term_of_cic_term status cict ctx in
987 let _,_,metasenv,subst,_ = status#obj in
988 let ty = NCicTypeChecker.typeof status subst metasenv ctx ct in
989 let res = branch status (mk_cic_term ctx ty) in
990 let diff = og_no - old_og_no in
991 debug_print (lazy ("expected branching: " ^ (string_of_int res)));
992 debug_print (lazy ("actual: branching" ^ (string_of_int diff)));
993 (* some flexibility *)
994 if og_no - old_og_no > res then
995 (debug_print (lazy ("branch factor for: " ^ (ppterm status cict) ^ " = "
996 ^ (string_of_int res) ^ " vs. " ^ (string_of_int og_no)));
997 debug_print ~depth (lazy "strange application"); None)
999 *) (incr candidate_no; Some ((!candidate_no,t),status))
1000 with Error (msg,exn) -> debug_print ~depth (lazy "failed"); None
1003 let sort_of status subst metasenv ctx t =
1004 let ty = NCicTypeChecker.typeof status subst metasenv ctx t in
1005 let metasenv',ty = NCicUnification.fix_sorts status metasenv subst ty in
1006 assert (metasenv = metasenv');
1007 NCicTypeChecker.typeof status subst metasenv ctx ty
1010 let type0= NUri.uri_of_string ("cic:/matita/pts/Type0.univ")
1013 let perforate_small status subst metasenv context t =
1014 let rec aux = function
1015 | NCic.Appl (hd::tl) ->
1017 let s = sort_of status subst metasenv context t in
1019 | NCic.Sort(NCic.Type [`Type,u])
1020 when u=type0 -> NCic.Meta (0,(0,NCic.Irl 0))
1023 NCic.Appl (hd::List.map map tl)
1029 let get_cands retrieve_for diff empty gty weak_gty =
1030 let cands = retrieve_for gty in
1032 | None -> cands, empty
1034 let more_cands = retrieve_for weak_gty in
1035 cands, diff more_cands cands
1038 let get_candidates ?(smart=true) depth flags status cache signature gty =
1039 let universe = status#auto_cache in
1040 let _,_,metasenv,subst,_ = status#obj in
1041 let context = ctx_of gty in
1042 let _, raw_gty = term_of_cic_term status gty context in
1043 let is_prod, is_eq =
1044 let status, t = term_of_cic_term status gty context in
1045 let t = NCicReduction.whd status subst context t in
1047 | NCic.Prod _ -> true, false
1048 | _ -> false, NCicParamod.is_equation status metasenv subst context t
1050 debug_print ~depth (lazy ("gty:" ^ NTacStatus.ppterm status gty));
1052 NCicParamod.is_equation status metasenv subst context raw_gty
1054 let raw_weak_gty, weak_gty =
1061 perforate_small status subst metasenv context raw_gty in
1062 let weak = mk_cic_term context raw_weak in
1063 debug_print ~depth (lazy ("weak_gty:" ^ NTacStatus.ppterm status weak));
1064 Some raw_weak, Some (weak)
1068 (* we now compute global candidates *)
1069 let global_cands, smart_global_cands =
1071 let to_ast = function
1072 | NCic.Const r when true
1073 (*is_relevant statistics r*) -> Some (Ast.NRef r)
1074 (* | NCic.Const _ -> None *)
1075 | _ -> assert false in
1077 to_ast (NDiscriminationTree.TermSet.elements s) in
1080 (NDiscriminationTree.DiscriminationTree.retrieve_unifiables universe)
1081 NDiscriminationTree.TermSet.diff
1082 NDiscriminationTree.TermSet.empty
1083 raw_gty raw_weak_gty in
1085 (* we now compute local candidates *)
1086 let local_cands,smart_local_cands =
1089 let _status, t = term_of_cic_term status t context
1091 List.map to_ast (Ncic_termSet.elements s) in
1094 (fun ty -> search_in_th ty cache)
1095 Ncic_termSet.diff Ncic_termSet.empty gty weak_gty in
1097 (* we now splits candidates in facts or not facts *)
1098 let test = is_a_fact_ast status subst metasenv context in
1099 let by,given_candidates =
1100 match flags.candidates with
1102 | None -> false, [] in
1103 (* we compute candidates to be applied in normal mode, splitted in
1104 facts and not facts *)
1105 let candidates_facts,candidates_other =
1106 let gl1,gl2 = List.partition test global_cands in
1107 let ll1,ll2 = List.partition test local_cands in
1108 (* if the goal is an equation we avoid to apply unit equalities,
1109 since superposition should take care of them; refl is an
1110 exception since it prompts for convertibility *)
1111 let l1 = if is_eq then [Ast.Ident("refl",None)] else gl1@ll1 in
1113 (* if smart given candidates are applied in smart mode *)
1114 if by && smart then ll2
1115 else if by then given_candidates@ll2
1119 (* we now compute candidates to be applied in smart mode, splitted in
1120 facts and not facts *)
1121 let smart_candidates_facts, smart_candidates_other =
1122 if is_prod || not(smart) then [],[]
1124 let sgl1,sgl2 = List.partition test smart_global_cands in
1125 let sll1,sll2 = List.partition test smart_local_cands in
1126 let l1 = if is_eq then [] else sgl1@sll1 in
1128 if by && smart then given_candidates@sll2
1129 else if by then sll2
1134 smart_candidates_facts,
1135 sort_candidates status context (candidates_other),
1136 sort_candidates status context (smart_candidates_other)
1139 let applicative_case depth signature status flags gty cache =
1140 app_counter:= !app_counter+1;
1141 let _,_,metasenv,subst,_ = status#obj in
1142 let context = ctx_of gty in
1143 let tcache = cache.facts in
1144 let is_prod, is_eq =
1145 let status, t = term_of_cic_term status gty context in
1146 let t = NCicReduction.whd status subst context t in
1148 | NCic.Prod _ -> true, false
1149 | _ -> false, NCicParamod.is_equation status metasenv subst context t
1151 debug_print ~depth (lazy (string_of_bool is_eq));
1153 let candidates_facts, smart_candidates_facts,
1154 candidates_other, smart_candidates_other =
1155 get_candidates ~smart:true depth
1156 flags status tcache signature gty
1158 let sm = if is_eq || is_prod then 0 else 2 in
1159 let sm1 = if flags.last then 2 else 0 in
1160 let maxd = (depth + 1 = flags.maxdepth) in
1161 let try_candidates only_one sm acc candidates =
1164 if (only_one && (elems <> [])) then elems
1166 match try_candidate (~smart:sm)
1167 flags depth status cache.unit_eq context cand with
1169 | Some x -> x::elems)
1172 (* if the goal is the last one we stop at the first fact *)
1173 let elems = try_candidates flags.last sm [] candidates_facts in
1174 (* now we add smart_facts *)
1175 let elems = try_candidates flags.last sm elems smart_candidates_facts in
1176 (* if we are at maxdepth and the goal is not a product we are done
1177 similarly, if the goal is the last one and we already found a
1179 if (maxd && not(is_prod)) || (flags.last && elems<>[]) then elems
1181 let elems = try_candidates false 2 elems candidates_other in
1182 debug_print ~depth (lazy ("not facts: try smart application"));
1183 try_candidates false 2 elems smart_candidates_other
1190 (* gty is supposed to be meta-closed *)
1191 let is_subsumed depth filter_depth status gty cache =
1192 if cache=[] then false else (
1193 debug_print ~depth (lazy("Subsuming " ^ (ppterm status gty)));
1194 let n,h,metasenv,subst,obj = status#obj in
1195 let ctx = ctx_of gty in
1196 let _ , raw_gty = term_of_cic_term status gty ctx in
1197 let target = NCicSubstitution.lift status 1 raw_gty in
1198 (* we compute candidates using the perforated type *)
1205 perforate_small status subst metasenv ctx raw_gty in
1206 let weak = mk_cic_term ctx raw_weak in
1207 debug_print ~depth (lazy ("weak_gty:" ^ NTacStatus.ppterm status weak));
1211 (* candidates must only be searched w.r.t the given context *)
1214 let idx = List.assq ctx cache in
1217 Ncic_termSet.elements
1218 (InvRelDiscriminationTree.retrieve_unifiables idx weak)
1220 with Not_found -> []
1222 (* this is a dirty trick: the first argument of an application is used
1223 to remember at which depth a goal failed *)
1225 let ctx = ctx_of t in
1226 let _, src = term_of_cic_term status t ctx in
1228 | NCic.Appl [NCic.Implicit (`Typeof d); t]
1229 when d <= depth -> Some (mk_cic_term ctx t)
1232 if filter_depth then HExtlib.filter_map filter candidates else candidates in
1234 (lazy ("failure candidates: " ^ string_of_int (List.length candidates)));
1238 let _ , source = term_of_cic_term status t ctx in
1240 NCic.Prod("foo",source,target) in
1241 let metasenv,j,_,_ =
1242 NCicMetaSubst.mk_meta
1243 metasenv ctx ~with_type:implication `IsType in
1244 let status = status#set_obj (n,h,metasenv,subst,obj) in
1245 let status = status#set_stack [([1,Open j],[],[],`NoTag)] in
1247 let status = NTactics.intro_tac "foo" status in
1249 NTactics.apply_tac ("",0,Ast.NCic (NCic.Rel 1)) status
1251 if (head_goals status#stack = []) then raise Found
1256 with Found -> debug_print ~depth (lazy "success");true)
1259 let rec guess_name name ctx =
1260 if name = "_" then guess_name "auto" ctx else
1261 if not (List.mem_assoc name ctx) then name else
1262 guess_name (name^"'") ctx
1265 let is_prod status =
1266 let _, ctx, gty = current_goal status in
1267 let status, gty = apply_subst status ctx gty in
1268 let _, raw_gty = term_of_cic_term status gty ctx in
1270 | NCic.Prod (name,src,_) ->
1271 let status, src = whd status ~delta:0 ctx (mk_cic_term ctx src) in
1272 (match snd (term_of_cic_term status src ctx) with
1273 | NCic.Const(NReference.Ref (_,NReference.Ind _) as r)
1274 | NCic.Appl (NCic.Const(NReference.Ref (_,NReference.Ind _) as r)::_) ->
1275 let _,_,itys,_,_ = NCicEnvironment.get_checked_indtys status r in
1277 (* | [_,_,_,[_;_]] con nat va, ovviamente, in loop *)
1279 | [_,_,_,[]] -> `Inductive (guess_name name ctx)
1280 | _ -> `Some (guess_name name ctx))
1281 | _ -> `Some (guess_name name ctx))
1284 let intro ~depth status facts name =
1285 let status = NTactics.intro_tac name status in
1286 let _, ctx, ngty = current_goal status in
1287 let t = mk_cic_term ctx (NCic.Rel 1) in
1288 let status, keys = keys_of_term status t in
1289 let facts = List.fold_left (add_to_th t) facts keys in
1290 debug_print ~depth (lazy ("intro: "^ name));
1291 (* unprovability is not stable w.r.t introduction *)
1295 let rec intros_facts ~depth status facts =
1296 if List.length (head_goals status#stack) <> 1 then status, facts else
1297 match is_prod status with
1301 intro ~depth status facts name
1302 in intros_facts ~depth status facts
1303 (* | `Inductive name ->
1304 let status = NTactics.case1_tac name status in
1305 intros_facts ~depth status facts *)
1306 | _ -> status, facts
1309 let intros ~depth status cache =
1310 match is_prod status with
1313 let trace = cache.trace in
1315 intros_facts ~depth status cache.facts
1317 if head_goals status#stack = [] then
1318 let status = NTactics.merge_tac status in
1319 [(0,Ast.Ident("__intros",None)),status], cache
1321 (* we reindex the equation from scratch *)
1322 let unit_eq = index_local_equations status#eq_cache status in
1323 let status = NTactics.merge_tac status in
1324 [(0,Ast.Ident("__intros",None)),status],
1325 init_cache ~facts ~unit_eq () ~trace
1329 let reduce ~whd ~depth status g =
1330 let n,h,metasenv,subst,o = status#obj in
1331 let attr, ctx, ty = NCicUtils.lookup_meta g metasenv in
1332 let ty = NCicUntrusted.apply_subst status subst ctx ty in
1334 (if whd then NCicReduction.whd else NCicTacReduction.normalize) status ~subst ctx ty
1339 (lazy ("reduced to: "^ status#ppterm ctx subst metasenv ty'));
1341 (g,(attr,ctx,ty'))::(List.filter (fun (i,_) -> i<>g) metasenv)
1343 let status = status#set_obj (n,h,metasenv,subst,o) in
1344 (* we merge to gain a depth level; the previous goal level should
1346 let status = NTactics.merge_tac status in
1348 [(!candidate_no,Ast.Ident("__whd",None)),status])
1351 let is_meta status gty =
1352 let _, ty = term_of_cic_term status gty (ctx_of gty) in
1354 | NCic.Meta _ -> true
1358 let do_something signature flags status g depth gty cache =
1359 (* if the goal is meta we close it with I:True. This should work
1360 thnaks to the toplogical sorting of goals. *)
1361 if is_meta status gty then
1362 let t = Ast.Ident("I",None) in
1363 debug_print (lazy ("using default term" ^ (NotationPp.pp_term status) t));
1364 let s = NTactics.apply_tac ("",0,t) status in
1367 let l0, cache = intros ~depth status cache in
1368 if l0 <> [] then l0, cache
1371 let l = reduce ~whd:true ~depth status g in
1372 (* if l <> [] then l,cache else *)
1373 (* backward aplications *)
1378 ((!candidate_no,Ast.Ident("__paramod",None)),s))
1379 (auto_eq_check cache.unit_eq status)
1382 if ((l1 <> []) && flags.last) then [] else
1383 applicative_case depth signature status flags gty cache
1387 (fun ((_,t),_) -> toref incr_nominations statistics t) l2;
1388 (* states in l1 have have an empty set of subgoals: no point to sort them *)
1390 (lazy ("alternatives = " ^ (string_of_int (List.length (l1@l@l2)))));
1391 (* we order alternatives w.r.t the number of subgoals they open *)
1392 l1 @ (sort_new_elems l2) @ l, cache
1395 let pp_goal = function
1396 | (_,Continuationals.Stack.Open i)
1397 | (_,Continuationals.Stack.Closed i) -> string_of_int i
1400 let pp_goals status l =
1404 let gty = get_goalty status i in
1405 NTacStatus.ppterm status gty)
1412 let compare = Pervasives.compare
1416 module MS = HTopoSort.Make(M)
1419 let sort_tac status =
1421 match status#stack with
1422 | [] -> assert false
1423 | (goals, t, k, tag) :: s ->
1424 let g = head_goals status#stack in
1426 (List.rev (MS.topological_sort g (deps status))) in
1427 noprint (lazy ("old g = " ^
1428 String.concat "," (List.map string_of_int g)));
1429 noprint (lazy ("sorted goals = " ^
1430 String.concat "," (List.map string_of_int sortedg)));
1431 let is_it i = function
1432 | (_,Continuationals.Stack.Open j )
1433 | (_,Continuationals.Stack.Closed j ) -> i = j
1436 List.map (fun i -> List.find (is_it i) goals) sortedg
1438 (sorted_goals, t, k, tag) :: s
1440 status#set_stack gstatus
1443 let clean_up_tac status =
1445 match status#stack with
1446 | [] -> assert false
1447 | (g, t, k, tag) :: s ->
1448 let is_open = function
1449 | (_,Continuationals.Stack.Open _) -> true
1450 | (_,Continuationals.Stack.Closed _) -> false
1452 let g' = List.filter is_open g in
1453 (g', t, k, tag) :: s
1455 status#set_stack gstatus
1458 let focus_tac focus status =
1460 match status#stack with
1461 | [] -> assert false
1462 | (g, t, k, tag) :: s ->
1463 let in_focus = function
1464 | (_,Continuationals.Stack.Open i)
1465 | (_,Continuationals.Stack.Closed i) -> List.mem i focus
1467 let focus,others = List.partition in_focus g
1469 (* we need to mark it as a BranchTag, otherwise cannot merge later *)
1470 (focus,[],[],`BranchTag) :: (others, t, k, tag) :: s
1472 status#set_stack gstatus
1475 let deep_focus_tac level focus status =
1476 let in_focus = function
1477 | (_,Continuationals.Stack.Open i)
1478 | (_,Continuationals.Stack.Closed i) -> List.mem i focus
1480 let rec slice level gs =
1481 if level = 0 then [],[],gs else
1483 | [] -> assert false
1484 | (g, t, k, tag) :: s ->
1485 let f,o,gs = slice (level-1) s in
1486 let f1,o1 = List.partition in_focus g
1488 (f1,[],[],`BranchTag)::f, (o1, t, k, tag)::o, gs
1491 let f,o,s = slice level status#stack in f@o@s
1493 status#set_stack gstatus
1496 let move_to_side level status =
1497 match status#stack with
1498 | [] -> assert false
1500 let is_open = function
1501 | (_,Continuationals.Stack.Open i) -> Some i
1502 | (_,Continuationals.Stack.Closed _) -> None
1504 let others = menv_closure status (stack_goals (level-1) tl) in
1505 List.for_all (fun i -> IntSet.mem i others)
1506 (HExtlib.filter_map is_open g)
1508 let top_cache ~depth top status cache =
1510 let unit_eq = index_local_equations status#eq_cache status in
1511 {cache with unit_eq = unit_eq}
1514 let rec auto_clusters ?(top=false)
1515 flags signature cache depth status : unit =
1516 debug_print ~depth (lazy ("entering auto clusters at depth " ^
1517 (string_of_int depth)));
1518 debug_print ~depth (pptrace status cache.trace);
1519 (* ignore(Unix.select [] [] [] 0.01); *)
1520 let status = clean_up_tac status in
1521 let goals = head_goals status#stack in
1523 if depth = 0 then raise (Proved (status, cache.trace))
1525 let status = NTactics.merge_tac status in
1527 let l,tree = cache.under_inspection in
1529 | [] -> cache (* possible because of intros that cleans the cache *)
1530 | a::tl -> let tree = rm_from_th a tree a in
1531 {cache with under_inspection = tl,tree}
1533 auto_clusters flags signature cache (depth-1) status
1534 else if List.length goals < 2 then
1535 let cache = top_cache ~depth top status cache in
1536 auto_main flags signature cache depth status
1538 let all_goals = open_goals (depth+1) status in
1539 debug_print ~depth (lazy ("goals = " ^
1540 String.concat "," (List.map string_of_int all_goals)));
1541 let classes = HExtlib.clusters (deps status) all_goals in
1542 (* if any of the classes exceed maxwidth we fail *)
1545 if List.length gl > flags.maxwidth then
1547 debug_print ~depth (lazy "FAIL GLOBAL WIDTH");
1548 HLog.warn (sprintf "global width (%u) exceeded: %u"
1549 flags.maxwidth (List.length gl));
1550 raise (Gaveup cache.failures)
1551 end else ()) classes;
1552 if List.length classes = 1 then
1554 {flags with last = (List.length all_goals = 1)} in
1555 (* no need to cluster *)
1556 let cache = top_cache ~depth top status cache in
1557 auto_main flags signature cache depth status
1559 let classes = if top then List.rev classes else classes in
1565 ("cluster:" ^ String.concat "," (List.map string_of_int l)))
1567 (* we now process each cluster *)
1568 let status,cache,b =
1570 (fun (status,cache,b) gl ->
1572 {flags with last = (List.length gl = 1)} in
1573 let lold = List.length status#stack in
1574 debug_print ~depth (lazy ("stack length = " ^
1575 (string_of_int lold)));
1576 let fstatus = deep_focus_tac (depth+1) gl status in
1577 let cache = top_cache ~depth top fstatus cache in
1579 debug_print ~depth (lazy ("focusing on" ^
1580 String.concat "," (List.map string_of_int gl)));
1581 auto_main flags signature cache depth fstatus; assert false
1583 | Proved(status,trace) ->
1584 let status = NTactics.merge_tac status in
1585 let cache = {cache with trace = trace} in
1586 let lnew = List.length status#stack in
1587 assert (lold = lnew);
1589 | Gaveup failures when top ->
1590 let cache = {cache with failures = failures} in
1593 (status,cache,false) classes
1595 let rec final_merge n s =
1596 if n = 0 then s else final_merge (n-1) (NTactics.merge_tac s)
1597 in let status = final_merge depth status
1598 in if b then raise (Proved(status,cache.trace)) else raise (Gaveup cache.failures)
1602 (* BRAND NEW VERSION *)
1603 auto_main flags signature cache depth status: unit =
1604 debug_print ~depth (lazy "entering auto main");
1605 debug_print ~depth (pptrace status cache.trace);
1606 debug_print ~depth (lazy ("stack length = " ^
1607 (string_of_int (List.length status#stack))));
1608 (* ignore(Unix.select [] [] [] 0.01); *)
1609 let status = sort_tac (clean_up_tac status) in
1610 let goals = head_goals status#stack in
1612 | [] when depth = 0 -> raise (Proved (status,cache.trace))
1614 let status = NTactics.merge_tac status in
1616 let l,tree = cache.under_inspection in
1618 | [] -> cache (* possible because of intros that cleans the cache *)
1619 | a::tl -> let tree = rm_from_th a tree a in
1620 {cache with under_inspection = tl,tree}
1622 auto_clusters flags signature cache (depth-1) status
1624 if depth > 0 && move_to_side depth status
1626 let status = NTactics.merge_tac status in
1628 let l,tree = cache.under_inspection in
1630 | [] -> cache (* possible because of intros that cleans the cache*)
1631 | a::tl -> let tree = rm_from_th a tree a in
1632 {cache with under_inspection = tl,tree}
1634 auto_clusters flags signature cache (depth-1) status
1636 let ng = List.length goals in
1637 (* moved inside auto_clusters *)
1638 if ng > flags.maxwidth then begin
1639 debug_print ~depth (lazy "FAIL LOCAL WIDTH");
1640 HLog.warn (sprintf "local width (%u) exceeded: %u"
1642 raise (Gaveup cache.failures)
1643 end else if depth = flags.maxdepth then
1644 raise (Gaveup cache.failures)
1646 let status = NTactics.branch_tac ~force:true status in
1647 let g,gctx, gty = current_goal status in
1648 let ctx,ty = close status g in
1649 let closegty = mk_cic_term ctx ty in
1650 let status, gty = apply_subst status gctx gty in
1651 debug_print ~depth (lazy("Attacking goal " ^
1652 string_of_int g ^ " : "^ppterm status gty));
1653 debug_print ~depth (lazy ("current failures: " ^
1654 string_of_int (List.length (all_elements ctx cache.failures))));
1656 let _,_,metasenv,subst,_ = status#obj in
1657 NCicParamod.is_equation status metasenv subst ctx ty in
1658 (* if the goal is an equality we artificially raise its depth up to
1659 flags.maxdepth - 1 *)
1660 if (not flags.last && is_eq && (depth < (flags.maxdepth -2))) then
1661 (* for efficiency reasons, in this case we severely cripple the
1663 (debug_print ~depth (lazy ("RAISING DEPTH TO " ^ string_of_int (depth+1)));
1664 auto_main flags signature cache (depth+1) status)
1665 (* check for loops *)
1666 else if is_subsumed depth false status closegty (snd cache.under_inspection) then
1667 (debug_print ~depth (lazy "SUBSUMED");
1668 raise (Gaveup cache.failures))
1669 (* check for failures *)
1670 else if is_subsumed depth true status closegty cache.failures then
1671 (debug_print ~depth (lazy "ALREADY MET");
1672 raise (Gaveup cache.failures))
1674 let new_sig = height_of_goal g status in
1675 if new_sig < signature then
1676 (debug_print ~depth (lazy ("news = " ^ (string_of_int new_sig)));
1677 debug_print ~depth (lazy ("olds = " ^ (string_of_int signature))));
1678 let alternatives, cache =
1679 do_something signature flags status g depth gty cache in
1682 let l,tree = cache.under_inspection in
1683 let l,tree = closegty::l, add_to_th closegty tree closegty in
1684 {cache with under_inspection = l,tree}
1688 (fun allfailures ((_,t),status) ->
1690 (lazy ("(re)considering goal " ^
1691 (string_of_int g) ^" : "^ppterm status gty));
1692 debug_print (~depth:depth)
1693 (lazy ("Case: " ^ NotationPp.pp_term status t));
1695 if t=Ast.Ident("__whd",None) ||
1696 t=Ast.Ident("__intros",None)
1698 else depth+1,loop_cache in
1699 let cache = add_to_trace status ~depth cache t in
1700 let cache = {cache with failures = allfailures} in
1702 auto_clusters flags signature cache depth status;
1705 debug_print ~depth (lazy "Failed");
1707 cache.failures alternatives in
1711 let dty = NCic.Appl [NCic.Implicit (`Typeof depth); ty] in
1714 (*prerr_endline ("FAILURE : " ^ ppterm status gty);*)
1715 add_to_th newfail failures closegty
1717 debug_print ~depth (lazy "no more candidates");
1718 raise (Gaveup failures)
1721 let int name l def =
1722 try int_of_string (List.assoc name l)
1723 with Failure _ | Not_found -> def
1726 module AstSet = Set.Make(struct type t = Ast.term let compare = compare end)
1728 let cleanup_trace s trace =
1729 (* removing duplicates *)
1732 (fun acc t -> AstSet.add t acc)
1733 AstSet.empty trace in
1734 let trace = AstSet.elements trace_set
1735 (* filtering facts *)
1739 | Ast.NRef (NReference.Ref (u,_)) -> not (is_a_fact_obj s u)
1743 let auto_tac ~params:(univ,flags) ?(trace_ref=ref []) status =
1744 let oldstatus = status in
1745 let status = (status:> NTacStatus.tac_status) in
1746 let goals = head_goals status#stack in
1747 let status, facts = mk_th_cache status goals in
1748 (* let unit_eq = index_local_equations status#eq_cache status in *)
1749 let cache = init_cache ~facts () in
1750 (* pp_th status facts; *)
1752 NDiscriminationTree.DiscriminationTree.iter status#auto_cache (fun p t ->
1754 NDiscriminationTree.NCicIndexable.string_of_path p ^ " |--> " ^
1755 String.concat "\n " (List.map (
1756 status#ppterm ~metasenv:[] ~context:[] ~subst:[])
1757 (NDiscriminationTree.TermSet.elements t))
1765 let status, res = disambiguate status [] t None in
1766 let _,res = term_of_cic_term status res (ctx_of res)
1768 in Some (List.map to_Ast l)
1770 let depth = int "depth" flags 3 in
1771 let size = int "size" flags 10 in
1772 let width = int "width" flags 4 (* (3+List.length goals)*) in
1774 (* let goals = List.map (fun i -> (i,P)) goals in *)
1775 let signature = height_of_goals status in
1778 candidates = candidates;
1782 timeout = Unix.gettimeofday() +. 3000.;
1785 let initial_time = Unix.gettimeofday() in
1790 ("TIME ELAPSED:"^string_of_float(Unix.gettimeofday()-.initial_time)));
1792 ("Applicative nodes:"^string_of_int !app_counter));
1793 raise (Error (lazy "auto gave up", None)))
1795 let _ = debug_print (lazy("\n\nRound "^string_of_int x^"\n")) in
1796 let flags = { flags with maxdepth = x }
1798 try auto_clusters (~top:true) flags signature cache 0 status;assert false
1800 try auto_main flags signature cache 0 status;assert false
1803 | Gaveup _ -> up_to (x+1) y
1804 | Proved (s,trace) ->
1805 debug_print (lazy ("proved at depth " ^ string_of_int x));
1806 List.iter (toref incr_uses statistics) trace;
1807 let trace = cleanup_trace s trace in
1808 let _ = debug_print (pptrace status trace) in
1811 | (g,t,k,f) :: rest -> (filter_open g,t,k,f):: rest
1814 let s = s#set_stack stack in
1816 oldstatus#set_status s
1818 let s = up_to depth depth in
1819 debug_print (print_stat status statistics);
1821 ("TIME ELAPSED:"^string_of_float(Unix.gettimeofday()-.initial_time)));
1823 ("Applicative nodes:"^string_of_int !app_counter));
1827 let auto_tac ~params:(_,flags as params) ?trace_ref =
1828 if List.mem_assoc "demod" flags then
1830 else if List.mem_assoc "paramod" flags then
1832 else if List.mem_assoc "fast_paramod" flags then
1833 fast_eq_check_tac ~params
1834 else auto_tac ~params ?trace_ref