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 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 noprint (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 noprint (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 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 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 (* we compare the expected branching with the actual one and
977 prune the candidate when the latter is larger. The optimization
978 is meant to rule out stange applications of flexible terms,
979 such as the application of eq_f that always succeeds.
980 There is some gain but less than expected *)
981 let og_no = List.length (open_goals (depth+1) status) in
982 let status, cict = disambiguate status ctx ("",0,t) None in
983 let status,ct = term_of_cic_term status cict ctx in
984 let _,_,metasenv,subst,_ = status#obj in
985 let ty = NCicTypeChecker.typeof status subst metasenv ctx ct in
986 let res = branch status (mk_cic_term ctx ty) in
987 let diff = og_no - old_og_no in
988 debug_print (lazy ("expected branching: " ^ (string_of_int res)));
989 debug_print (lazy ("actual: branching" ^ (string_of_int diff)));
990 (* one goal is closed by the application *)
991 if og_no - old_og_no >= res then
992 (debug_print (lazy ("branch factor for: " ^ (ppterm status cict) ^ " = "
993 ^ (string_of_int res) ^ " vs. " ^ (string_of_int og_no)));
994 debug_print ~depth (lazy "strange application"); None)
996 (incr candidate_no; Some ((!candidate_no,t),status))
997 with Error (msg,exn) -> debug_print ~depth (lazy "failed"); None
1000 let sort_of status subst metasenv ctx t =
1001 let ty = NCicTypeChecker.typeof status subst metasenv ctx t in
1002 let metasenv',ty = NCicUnification.fix_sorts status metasenv subst ty in
1003 assert (metasenv = metasenv');
1004 NCicTypeChecker.typeof status subst metasenv ctx ty
1007 let type0= NUri.uri_of_string ("cic:/matita/pts/Type0.univ")
1010 let perforate_small status subst metasenv context t =
1011 let rec aux = function
1012 | NCic.Appl (hd::tl) ->
1014 let s = sort_of status subst metasenv context t in
1016 | NCic.Sort(NCic.Type [`Type,u])
1017 when u=type0 -> NCic.Meta (0,(0,NCic.Irl 0))
1020 NCic.Appl (hd::List.map map tl)
1026 let get_cands retrieve_for diff empty gty weak_gty =
1027 let cands = retrieve_for gty in
1029 | None -> cands, empty
1031 let more_cands = retrieve_for weak_gty in
1032 cands, diff more_cands cands
1035 let get_candidates ?(smart=true) depth flags status cache signature gty =
1036 let maxd = ((depth + 1) = flags.maxdepth) in
1037 let universe = status#auto_cache in
1038 let _,_,metasenv,subst,_ = status#obj in
1039 let context = ctx_of gty in
1040 let _, raw_gty = term_of_cic_term status gty context in
1041 debug_print ~depth (lazy ("gty:" ^ NTacStatus.ppterm status gty));
1042 let raw_weak_gty, weak_gty =
1049 perforate_small status subst metasenv context raw_gty in
1050 let weak = mk_cic_term context raw_weak in
1051 debug_print ~depth (lazy ("weak_gty:" ^ NTacStatus.ppterm status weak));
1052 Some raw_weak, Some (weak)
1056 let global_cands, smart_global_cands =
1057 match flags.candidates with
1058 | Some l when (not maxd) -> l,[]
1062 let to_ast = function
1063 | NCic.Const r when true (*is_relevant statistics r*) -> Some (Ast.NRef r)
1064 (* | NCic.Const _ -> None *)
1065 | _ -> assert false in
1067 to_ast (NDiscriminationTree.TermSet.elements s) in
1070 (NDiscriminationTree.DiscriminationTree.retrieve_unifiables
1072 NDiscriminationTree.TermSet.diff
1073 NDiscriminationTree.TermSet.empty
1074 raw_gty raw_weak_gty in
1076 let local_cands,smart_local_cands =
1079 let _status, t = term_of_cic_term status t context
1081 List.map to_ast (Ncic_termSet.elements s) in
1084 (fun ty -> search_in_th ty cache)
1085 Ncic_termSet.diff Ncic_termSet.empty gty weak_gty in
1087 sort_candidates status context (global_cands@local_cands),
1088 sort_candidates status context (smart_global_cands@smart_local_cands)
1092 let get_candidates ?(smart=true) status cache signature gty =
1093 let universe = status#auto_cache in
1094 let _,_,metasenv,subst,_ = status#obj in
1095 let context = ctx_of gty in
1097 let _status, t = term_of_cic_term status t context
1099 let c_ast = function
1100 | NCic.Const r -> Ast.NRef r | _ -> assert false in
1101 let _, raw_gty = term_of_cic_term status gty context in
1102 let keys = all_keys_of_cic_term metasenv subst context raw_gty in
1103 (* we only keep those keys that do not require any intros for now *)
1104 let no_intros_keys = snd (List.hd keys) in
1106 NDiscriminationTree.TermSet.fold
1108 NDiscriminationTree.TermSet.union acc
1109 (NDiscriminationTree.DiscriminationTree.retrieve_unifiables
1111 ) no_intros_keys NDiscriminationTree.TermSet.empty in
1113 let cands = NDiscriminationTree.DiscriminationTree.retrieve_unifiables
1117 NDiscriminationTree.TermSet.fold
1119 Ncic_termSet.union acc (search_in_th (mk_cic_term context ty) cache)
1120 ) no_intros_keys Ncic_termSet.empty in
1122 let local_cands = search_in_th gty cache in
1124 debug_print (lazy ("candidates for" ^ NTacStatus.ppterm status gty));
1125 debug_print (lazy ("local cands = " ^ (string_of_int (List.length (Ncic_termSet.elements local_cands)))));
1126 let together global local =
1128 (List.filter (only signature context)
1129 (NDiscriminationTree.TermSet.elements global)) @
1130 List.map t_ast (Ncic_termSet.elements local) in
1131 let candidates = together cands local_cands in
1132 let candidates = sort_candidates status context candidates in
1133 let smart_candidates =
1139 let weak_gty = perforate_small status subst metasenv context raw_gty in
1141 NCic.Appl (hd:: HExtlib.mk_list(NCic.Meta (0,(0,NCic.Irl 0)))
1142 (List.length tl)) in *)
1144 NDiscriminationTree.DiscriminationTree.retrieve_unifiables
1148 NDiscriminationTree.TermSet.diff more_cands cands in
1149 let cic_weak_gty = mk_cic_term context weak_gty in
1150 let more_local_cands = search_in_th cic_weak_gty cache in
1151 let smart_local_cands =
1152 Ncic_termSet.diff more_local_cands local_cands in
1153 together smart_cands smart_local_cands
1154 (* together more_cands more_local_cands *)
1158 let smart_candidates = sort_candidates status context smart_candidates in
1159 (* if smart then smart_candidates, []
1160 else candidates, [] *)
1161 candidates, smart_candidates
1164 let get_candidates ?(smart=true) flags status cache signature gty =
1165 match flags.candidates with
1166 | None -> get_candidates ~smart status cache signature gty
1172 let applicative_case depth signature status flags gty cache =
1173 app_counter:= !app_counter+1;
1174 let _,_,metasenv,subst,_ = status#obj in
1175 let context = ctx_of gty in
1176 let tcache = cache.facts in
1177 let is_prod, is_eq =
1178 let status, t = term_of_cic_term status gty context in
1179 let t = NCicReduction.whd status subst context t in
1181 | NCic.Prod _ -> true, false
1182 | _ -> false, NCicParamod.is_equation status metasenv subst context t
1184 debug_print ~depth (lazy (string_of_bool is_eq));
1186 let candidates, smart_candidates =
1187 get_candidates ~smart:true depth
1188 flags status tcache signature gty in
1189 let test = is_a_fact_ast status subst metasenv context in
1190 let candidates_facts,candidates_other =
1191 (* if the goal is an equation we avoid to apply unit equalities,
1192 since superposition should take care of them; refl is an
1193 exception since it prompts for convertibility *)
1194 let l1,l2 = List.partition test candidates in
1195 if is_eq then [Ast.Ident("refl",None)],l2 else l1,l2
1197 let smart_candidates_facts, smart_candidates_other =
1198 if is_prod then [],[]
1200 let l1,l2 = List.partition test smart_candidates in
1201 if is_eq then [],l2 else l1,l2
1203 let sm = if is_eq || is_prod then 0 else 2 in
1204 let sm1 = if flags.last then 2 else 0 in
1205 let maxd = (depth + 1 = flags.maxdepth) in
1206 let try_candidates only_one sm acc candidates =
1209 if (only_one && (elems <> [])) then elems
1211 match try_candidate (~smart:sm)
1212 flags depth status cache.unit_eq context cand with
1214 | Some x -> x::elems)
1217 (* if the goal is the last one we stop at the first fact *)
1218 let elems = try_candidates flags.last sm [] candidates_facts in
1219 (* now we add smart_facts *)
1220 let elems = try_candidates flags.last sm elems smart_candidates_facts in
1221 (* if we are at maxdepth and the goal is not a product we are done
1222 similarly, if the goal is the last one and we already found a
1224 if (maxd && not(is_prod)) || (flags.last && elems<>[]) then elems
1226 let elems = try_candidates false 2 elems candidates_other in
1227 debug_print ~depth (lazy ("not facts: try smart application"));
1228 try_candidates false 2 elems smart_candidates_other
1235 (* gty is supposed to be meta-closed *)
1236 let is_subsumed depth filter_depth status gty cache =
1237 if cache=[] then false else (
1238 debug_print ~depth (lazy("Subsuming " ^ (ppterm status gty)));
1239 let n,h,metasenv,subst,obj = status#obj in
1240 let ctx = ctx_of gty in
1241 let _ , raw_gty = term_of_cic_term status gty ctx in
1242 let target = NCicSubstitution.lift status 1 raw_gty in
1243 (* we compute candidates using the perforated type *)
1250 perforate_small status subst metasenv ctx raw_gty in
1251 let weak = mk_cic_term ctx raw_weak in
1252 debug_print ~depth (lazy ("weak_gty:" ^ NTacStatus.ppterm status weak));
1256 (* candidates must only be searched w.r.t the given context *)
1259 let idx = List.assq ctx cache in
1262 Ncic_termSet.elements
1263 (InvRelDiscriminationTree.retrieve_unifiables idx weak)
1265 with Not_found -> []
1267 (* this is a dirty trick: the first argument of an application is used
1268 to remember at which depth a goal failed *)
1270 let ctx = ctx_of t in
1271 let _, src = term_of_cic_term status t ctx in
1273 | NCic.Appl [NCic.Implicit (`Typeof d); t]
1274 when d <= depth -> Some (mk_cic_term ctx t)
1277 if filter_depth then HExtlib.filter_map filter candidates else candidates in
1279 (lazy ("failure candidates: " ^ string_of_int (List.length candidates)));
1283 let _ , source = term_of_cic_term status t ctx in
1285 NCic.Prod("foo",source,target) in
1286 let metasenv,j,_,_ =
1287 NCicMetaSubst.mk_meta
1288 metasenv ctx ~with_type:implication `IsType in
1289 let status = status#set_obj (n,h,metasenv,subst,obj) in
1290 let status = status#set_stack [([1,Open j],[],[],`NoTag)] in
1292 let status = NTactics.intro_tac "foo" status in
1294 NTactics.apply_tac ("",0,Ast.NCic (NCic.Rel 1)) status
1296 if (head_goals status#stack = []) then raise Found
1301 with Found -> debug_print ~depth (lazy "success");true)
1304 let rec guess_name name ctx =
1305 if name = "_" then guess_name "auto" ctx else
1306 if not (List.mem_assoc name ctx) then name else
1307 guess_name (name^"'") ctx
1310 let is_prod status =
1311 let _, ctx, gty = current_goal status in
1312 let status, gty = apply_subst status ctx gty in
1313 let _, raw_gty = term_of_cic_term status gty ctx in
1315 | NCic.Prod (name,src,_) ->
1316 let status, src = whd status ~delta:0 ctx (mk_cic_term ctx src) in
1317 (match snd (term_of_cic_term status src ctx) with
1318 | NCic.Const(NReference.Ref (_,NReference.Ind _) as r)
1319 | NCic.Appl (NCic.Const(NReference.Ref (_,NReference.Ind _) as r)::_) ->
1320 let _,_,itys,_,_ = NCicEnvironment.get_checked_indtys status r in
1322 (* | [_,_,_,[_;_]] con nat va, ovviamente, in loop *)
1324 | [_,_,_,[]] -> `Inductive (guess_name name ctx)
1325 | _ -> `Some (guess_name name ctx))
1326 | _ -> `Some (guess_name name ctx))
1329 let intro ~depth status facts name =
1330 let status = NTactics.intro_tac name status in
1331 let _, ctx, ngty = current_goal status in
1332 let t = mk_cic_term ctx (NCic.Rel 1) in
1333 let status, keys = keys_of_term status t in
1334 let facts = List.fold_left (add_to_th t) facts keys in
1335 debug_print ~depth (lazy ("intro: "^ name));
1336 (* unprovability is not stable w.r.t introduction *)
1340 let rec intros_facts ~depth status facts =
1341 if List.length (head_goals status#stack) <> 1 then status, facts else
1342 match is_prod status with
1346 intro ~depth status facts name
1347 in intros_facts ~depth status facts
1348 (* | `Inductive name ->
1349 let status = NTactics.case1_tac name status in
1350 intros_facts ~depth status facts *)
1351 | _ -> status, facts
1354 let intros ~depth status cache =
1355 match is_prod status with
1358 let trace = cache.trace in
1360 intros_facts ~depth status cache.facts
1362 if head_goals status#stack = [] then
1363 let status = NTactics.merge_tac status in
1364 [(0,Ast.Ident("__intros",None)),status], cache
1366 (* we reindex the equation from scratch *)
1367 let unit_eq = index_local_equations status#eq_cache status in
1368 let status = NTactics.merge_tac status in
1369 [(0,Ast.Ident("__intros",None)),status],
1370 init_cache ~facts ~unit_eq () ~trace
1374 let reduce ~whd ~depth status g =
1375 let n,h,metasenv,subst,o = status#obj in
1376 let attr, ctx, ty = NCicUtils.lookup_meta g metasenv in
1377 let ty = NCicUntrusted.apply_subst status subst ctx ty in
1379 (if whd then NCicReduction.whd else NCicTacReduction.normalize) status ~subst ctx ty
1384 (lazy ("reduced to: "^ status#ppterm ctx subst metasenv ty'));
1386 (g,(attr,ctx,ty'))::(List.filter (fun (i,_) -> i<>g) metasenv)
1388 let status = status#set_obj (n,h,metasenv,subst,o) in
1389 (* we merge to gain a depth level; the previous goal level should
1391 let status = NTactics.merge_tac status in
1393 [(!candidate_no,Ast.Ident("__whd",None)),status])
1396 let is_meta status gty =
1397 let _, ty = term_of_cic_term status gty (ctx_of gty) in
1399 | NCic.Meta _ -> true
1403 let do_something signature flags status g depth gty cache =
1404 (* if the goal is meta we close it with I:True. This should work
1405 thnaks to the toplogical sorting of goals. *)
1406 if is_meta status gty then
1407 let t = Ast.Ident("I",None) in
1408 debug_print (lazy ("using default term" ^ (NotationPp.pp_term status) t));
1409 let s = NTactics.apply_tac ("",0,t) status in
1412 let l0, cache = intros ~depth status cache in
1413 if l0 <> [] then l0, cache
1416 let l = reduce ~whd:true ~depth status g in
1417 (* if l <> [] then l,cache else *)
1418 (* backward aplications *)
1423 ((!candidate_no,Ast.Ident("__paramod",None)),s))
1424 (auto_eq_check cache.unit_eq status)
1427 if ((l1 <> []) && flags.last) then [] else
1428 applicative_case depth signature status flags gty cache
1432 (fun ((_,t),_) -> toref incr_nominations statistics t) l2;
1433 (* states in l1 have have an empty set of subgoals: no point to sort them *)
1435 (lazy ("alternatives = " ^ (string_of_int (List.length (l1@l@l2)))));
1436 (* we order alternatives w.r.t the number of subgoals they open *)
1437 l1 @ (sort_new_elems l2) @ l, cache
1440 let pp_goal = function
1441 | (_,Continuationals.Stack.Open i)
1442 | (_,Continuationals.Stack.Closed i) -> string_of_int i
1445 let pp_goals status l =
1449 let gty = get_goalty status i in
1450 NTacStatus.ppterm status gty)
1457 let compare = Pervasives.compare
1461 module MS = HTopoSort.Make(M)
1464 let sort_tac status =
1466 match status#stack with
1467 | [] -> assert false
1468 | (goals, t, k, tag) :: s ->
1469 let g = head_goals status#stack in
1471 (List.rev (MS.topological_sort g (deps status))) in
1472 noprint (lazy ("old g = " ^
1473 String.concat "," (List.map string_of_int g)));
1474 noprint (lazy ("sorted goals = " ^
1475 String.concat "," (List.map string_of_int sortedg)));
1476 let is_it i = function
1477 | (_,Continuationals.Stack.Open j )
1478 | (_,Continuationals.Stack.Closed j ) -> i = j
1481 List.map (fun i -> List.find (is_it i) goals) sortedg
1483 (sorted_goals, t, k, tag) :: s
1485 status#set_stack gstatus
1488 let clean_up_tac status =
1490 match status#stack with
1491 | [] -> assert false
1492 | (g, t, k, tag) :: s ->
1493 let is_open = function
1494 | (_,Continuationals.Stack.Open _) -> true
1495 | (_,Continuationals.Stack.Closed _) -> false
1497 let g' = List.filter is_open g in
1498 (g', t, k, tag) :: s
1500 status#set_stack gstatus
1503 let focus_tac focus status =
1505 match status#stack with
1506 | [] -> assert false
1507 | (g, t, k, tag) :: s ->
1508 let in_focus = function
1509 | (_,Continuationals.Stack.Open i)
1510 | (_,Continuationals.Stack.Closed i) -> List.mem i focus
1512 let focus,others = List.partition in_focus g
1514 (* we need to mark it as a BranchTag, otherwise cannot merge later *)
1515 (focus,[],[],`BranchTag) :: (others, t, k, tag) :: s
1517 status#set_stack gstatus
1520 let deep_focus_tac level focus status =
1521 let in_focus = function
1522 | (_,Continuationals.Stack.Open i)
1523 | (_,Continuationals.Stack.Closed i) -> List.mem i focus
1525 let rec slice level gs =
1526 if level = 0 then [],[],gs else
1528 | [] -> assert false
1529 | (g, t, k, tag) :: s ->
1530 let f,o,gs = slice (level-1) s in
1531 let f1,o1 = List.partition in_focus g
1533 (f1,[],[],`BranchTag)::f, (o1, t, k, tag)::o, gs
1536 let f,o,s = slice level status#stack in f@o@s
1538 status#set_stack gstatus
1541 let move_to_side level status =
1542 match status#stack with
1543 | [] -> assert false
1545 let is_open = function
1546 | (_,Continuationals.Stack.Open i) -> Some i
1547 | (_,Continuationals.Stack.Closed _) -> None
1549 let others = menv_closure status (stack_goals (level-1) tl) in
1550 List.for_all (fun i -> IntSet.mem i others)
1551 (HExtlib.filter_map is_open g)
1553 let rec auto_clusters ?(top=false)
1554 flags signature cache depth status : unit =
1555 debug_print ~depth (lazy ("entering auto clusters at depth " ^
1556 (string_of_int depth)));
1557 debug_print ~depth (pptrace status cache.trace);
1558 (* ignore(Unix.select [] [] [] 0.01); *)
1559 let status = clean_up_tac status in
1560 let goals = head_goals status#stack in
1562 if depth = 0 then raise (Proved (status, cache.trace))
1564 let status = NTactics.merge_tac status in
1566 let l,tree = cache.under_inspection in
1568 | [] -> cache (* possible because of intros that cleans the cache *)
1569 | a::tl -> let tree = rm_from_th a tree a in
1570 {cache with under_inspection = tl,tree}
1572 auto_clusters flags signature cache (depth-1) status
1573 else if List.length goals < 2 then
1574 auto_main flags signature cache depth status
1576 let all_goals = open_goals (depth+1) status in
1577 debug_print ~depth (lazy ("goals = " ^
1578 String.concat "," (List.map string_of_int all_goals)));
1579 let classes = HExtlib.clusters (deps status) all_goals in
1580 (* if any of the classes exceed maxwidth we fail *)
1583 if List.length gl > flags.maxwidth then
1585 debug_print ~depth (lazy "FAIL GLOBAL WIDTH");
1586 HLog.warn (sprintf "global width (%u) exceeded: %u"
1587 flags.maxwidth (List.length gl));
1588 raise (Gaveup cache.failures)
1589 end else ()) classes;
1590 if List.length classes = 1 then
1592 {flags with last = (List.length all_goals = 1)} in
1593 (* no need to cluster *)
1594 auto_main flags signature cache depth status
1596 let classes = if top then List.rev classes else classes in
1602 ("cluster:" ^ String.concat "," (List.map string_of_int l)))
1604 (* we now process each cluster *)
1605 let status,cache,b =
1607 (fun (status,cache,b) gl ->
1609 {flags with last = (List.length gl = 1)} in
1610 let lold = List.length status#stack in
1611 debug_print ~depth (lazy ("stack length = " ^
1612 (string_of_int lold)));
1613 let fstatus = deep_focus_tac (depth+1) gl status in
1615 debug_print ~depth (lazy ("focusing on" ^
1616 String.concat "," (List.map string_of_int gl)));
1617 auto_main flags signature cache depth fstatus; assert false
1619 | Proved(status,trace) ->
1620 let status = NTactics.merge_tac status in
1621 let cache = {cache with trace = trace} in
1622 let lnew = List.length status#stack in
1623 assert (lold = lnew);
1625 | Gaveup failures when top ->
1626 let cache = {cache with failures = failures} in
1629 (status,cache,false) classes
1631 let rec final_merge n s =
1632 if n = 0 then s else final_merge (n-1) (NTactics.merge_tac s)
1633 in let status = final_merge depth status
1634 in if b then raise (Proved(status,cache.trace)) else raise (Gaveup cache.failures)
1638 (* BRAND NEW VERSION *)
1639 auto_main flags signature cache depth status: unit =
1640 debug_print ~depth (lazy "entering auto main");
1641 debug_print ~depth (pptrace status cache.trace);
1642 debug_print ~depth (lazy ("stack length = " ^
1643 (string_of_int (List.length status#stack))));
1644 (* ignore(Unix.select [] [] [] 0.01); *)
1645 let status = sort_tac (clean_up_tac status) in
1646 let goals = head_goals status#stack in
1648 | [] when depth = 0 -> raise (Proved (status,cache.trace))
1650 let status = NTactics.merge_tac status in
1652 let l,tree = cache.under_inspection in
1654 | [] -> cache (* possible because of intros that cleans the cache *)
1655 | a::tl -> let tree = rm_from_th a tree a in
1656 {cache with under_inspection = tl,tree}
1658 auto_clusters flags signature cache (depth-1) status
1660 if depth > 0 && move_to_side depth status
1662 let status = NTactics.merge_tac status in
1664 let l,tree = cache.under_inspection in
1666 | [] -> cache (* possible because of intros that cleans the cache*)
1667 | a::tl -> let tree = rm_from_th a tree a in
1668 {cache with under_inspection = tl,tree}
1670 auto_clusters flags signature cache (depth-1) status
1672 let ng = List.length goals in
1673 (* moved inside auto_clusters *)
1674 if ng > flags.maxwidth then begin
1675 debug_print ~depth (lazy "FAIL LOCAL WIDTH");
1676 HLog.warn (sprintf "local width (%u) exceeded: %u"
1678 raise (Gaveup cache.failures)
1679 end else if depth = flags.maxdepth then
1680 raise (Gaveup cache.failures)
1682 let status = NTactics.branch_tac ~force:true status in
1683 let g,gctx, gty = current_goal status in
1684 let ctx,ty = close status g in
1685 let closegty = mk_cic_term ctx ty in
1686 let status, gty = apply_subst status gctx gty in
1687 debug_print ~depth (lazy("Attacking goal " ^
1688 string_of_int g ^ " : "^ppterm status gty));
1689 debug_print ~depth (lazy ("current failures: " ^
1690 string_of_int (List.length (all_elements ctx cache.failures))));
1692 let _,_,metasenv,subst,_ = status#obj in
1693 NCicParamod.is_equation status metasenv subst ctx ty in
1694 (* if the goal is an equality we artificially raise its depth up to
1695 flags.maxdepth - 1 *)
1696 if (not flags.last && is_eq && (depth < (flags.maxdepth -2))) then
1697 (* for efficiency reasons, in this case we severely cripple the
1699 (debug_print ~depth (lazy ("RAISING DEPTH TO " ^ string_of_int (depth+1)));
1700 auto_main flags signature cache (depth+1) status)
1701 (* check for loops *)
1702 else if is_subsumed depth false status closegty (snd cache.under_inspection) then
1703 (debug_print ~depth (lazy "SUBSUMED");
1704 raise (Gaveup cache.failures))
1705 (* check for failures *)
1706 else if is_subsumed depth true status closegty cache.failures then
1707 (debug_print ~depth (lazy "ALREADY MET");
1708 raise (Gaveup cache.failures))
1710 let new_sig = height_of_goal g status in
1711 if new_sig < signature then
1712 (debug_print ~depth (lazy ("news = " ^ (string_of_int new_sig)));
1713 debug_print ~depth (lazy ("olds = " ^ (string_of_int signature))));
1714 let alternatives, cache =
1715 do_something signature flags status g depth gty cache in
1718 let l,tree = cache.under_inspection in
1719 let l,tree = closegty::l, add_to_th closegty tree closegty in
1720 {cache with under_inspection = l,tree}
1724 (fun allfailures ((_,t),status) ->
1726 (lazy ("(re)considering goal " ^
1727 (string_of_int g) ^" : "^ppterm status gty));
1728 debug_print (~depth:depth)
1729 (lazy ("Case: " ^ NotationPp.pp_term status t));
1731 if t=Ast.Ident("__whd",None) ||
1732 t=Ast.Ident("__intros",None)
1734 else depth+1,loop_cache in
1735 let cache = add_to_trace status ~depth cache t in
1736 let cache = {cache with failures = allfailures} in
1738 auto_clusters flags signature cache depth status;
1741 debug_print ~depth (lazy "Failed");
1743 cache.failures alternatives in
1747 let dty = NCic.Appl [NCic.Implicit (`Typeof depth); ty] in
1750 (*prerr_endline ("FAILURE : " ^ ppterm status gty);*)
1751 add_to_th newfail failures closegty
1753 debug_print ~depth (lazy "no more candidates");
1754 raise (Gaveup failures)
1757 let int name l def =
1758 try int_of_string (List.assoc name l)
1759 with Failure _ | Not_found -> def
1762 module AstSet = Set.Make(struct type t = Ast.term let compare = compare end)
1764 let cleanup_trace s trace =
1765 (* removing duplicates *)
1768 (fun acc t -> AstSet.add t acc)
1769 AstSet.empty trace in
1770 let trace = AstSet.elements trace_set
1771 (* filtering facts *)
1775 | Ast.NRef (NReference.Ref (u,_)) -> not (is_a_fact_obj s u)
1779 let auto_tac ~params:(univ,flags) ?(trace_ref=ref []) status =
1780 let oldstatus = status in
1781 let status = (status:> NTacStatus.tac_status) in
1782 let goals = head_goals status#stack in
1783 let status, facts = mk_th_cache status goals in
1784 let unit_eq = index_local_equations status#eq_cache status in
1785 let cache = init_cache ~facts ~unit_eq () in
1786 (* pp_th status facts; *)
1788 NDiscriminationTree.DiscriminationTree.iter status#auto_cache (fun p t ->
1790 NDiscriminationTree.NCicIndexable.string_of_path p ^ " |--> " ^
1791 String.concat "\n " (List.map (
1792 status#ppterm ~metasenv:[] ~context:[] ~subst:[])
1793 (NDiscriminationTree.TermSet.elements t))
1801 let status, res = disambiguate status [] t None in
1802 let _,res = term_of_cic_term status res (ctx_of res)
1804 in Some (List.map to_Ast l)
1806 let depth = int "depth" flags 3 in
1807 let size = int "size" flags 10 in
1808 let width = int "width" flags 4 (* (3+List.length goals)*) in
1810 (* let goals = List.map (fun i -> (i,P)) goals in *)
1811 let signature = height_of_goals status in
1814 candidates = candidates;
1818 timeout = Unix.gettimeofday() +. 3000.;
1821 let initial_time = Unix.gettimeofday() in
1826 ("TIME ELAPSED:"^string_of_float(Unix.gettimeofday()-.initial_time)));
1828 ("Applicative nodes:"^string_of_int !app_counter));
1829 raise (Error (lazy "auto gave up", None)))
1831 let _ = debug_print (lazy("\n\nRound "^string_of_int x^"\n")) in
1832 let flags = { flags with maxdepth = x }
1834 try auto_clusters (~top:true) flags signature cache 0 status;assert false
1836 try auto_main flags signature cache 0 status;assert false
1839 | Gaveup _ -> up_to (x+1) y
1840 | Proved (s,trace) ->
1841 debug_print (lazy ("proved at depth " ^ string_of_int x));
1842 List.iter (toref incr_uses statistics) trace;
1843 let trace = cleanup_trace s trace in
1844 let _ = debug_print (pptrace status trace) in
1847 | (g,t,k,f) :: rest -> (filter_open g,t,k,f):: rest
1850 let s = s#set_stack stack in
1852 oldstatus#set_status s
1854 let s = up_to depth depth in
1855 debug_print (print_stat status statistics);
1857 ("TIME ELAPSED:"^string_of_float(Unix.gettimeofday()-.initial_time)));
1859 ("Applicative nodes:"^string_of_int !app_counter));
1863 let auto_tac ~params:(_,flags as params) ?trace_ref =
1864 if List.mem_assoc "demod" flags then
1866 else if List.mem_assoc "paramod" flags then
1868 else if List.mem_assoc "fast_paramod" flags then
1869 fast_eq_check_tac ~params
1870 else auto_tac ~params ?trace_ref