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 (* 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 (* some flexibility *)
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 universe = status#auto_cache in
1037 let _,_,metasenv,subst,_ = status#obj in
1038 let context = ctx_of gty in
1039 let _, raw_gty = term_of_cic_term status gty context in
1040 let is_prod, is_eq =
1041 let status, t = term_of_cic_term status gty context in
1042 let t = NCicReduction.whd status subst context t in
1044 | NCic.Prod _ -> true, false
1045 | _ -> false, NCicParamod.is_equation status metasenv subst context t
1047 debug_print ~depth (lazy ("gty:" ^ NTacStatus.ppterm status gty));
1049 NCicParamod.is_equation status metasenv subst context raw_gty
1051 let raw_weak_gty, weak_gty =
1058 perforate_small status subst metasenv context raw_gty in
1059 let weak = mk_cic_term context raw_weak in
1060 debug_print ~depth (lazy ("weak_gty:" ^ NTacStatus.ppterm status weak));
1061 Some raw_weak, Some (weak)
1065 (* we now compute global candidates *)
1066 let global_cands, smart_global_cands =
1068 let to_ast = function
1069 | NCic.Const r when true
1070 (*is_relevant statistics r*) -> Some (Ast.NRef r)
1071 (* | NCic.Const _ -> None *)
1072 | _ -> assert false in
1074 to_ast (NDiscriminationTree.TermSet.elements s) in
1077 (NDiscriminationTree.DiscriminationTree.retrieve_unifiables universe)
1078 NDiscriminationTree.TermSet.diff
1079 NDiscriminationTree.TermSet.empty
1080 raw_gty raw_weak_gty in
1082 (* we now compute local candidates *)
1083 let local_cands,smart_local_cands =
1086 let _status, t = term_of_cic_term status t context
1088 List.map to_ast (Ncic_termSet.elements s) in
1091 (fun ty -> search_in_th ty cache)
1092 Ncic_termSet.diff Ncic_termSet.empty gty weak_gty in
1094 (* we now splits candidates in facts or not facts *)
1095 let test = is_a_fact_ast status subst metasenv context in
1096 let by,given_candidates =
1097 match flags.candidates with
1099 | None -> false, [] in
1100 (* we compute candidates to be applied in normal mode, splitted in
1101 facts and not facts *)
1102 let candidates_facts,candidates_other =
1103 let gl1,gl2 = List.partition test global_cands in
1104 let ll1,ll2 = List.partition test local_cands in
1105 (* if the goal is an equation we avoid to apply unit equalities,
1106 since superposition should take care of them; refl is an
1107 exception since it prompts for convertibility *)
1108 let l1 = if is_eq then [Ast.Ident("refl",None)] else gl1@ll1 in
1110 (* if smart given candidates are applied in smart mode *)
1111 if by && smart then ll2
1112 else if by then given_candidates@ll2
1116 (* we now compute candidates to be applied in smart mode, splitted in
1117 facts and not facts *)
1118 let smart_candidates_facts, smart_candidates_other =
1119 if is_prod || not(smart) then [],[]
1121 let sgl1,sgl2 = List.partition test smart_global_cands in
1122 let sll1,sll2 = List.partition test smart_local_cands in
1123 let l1 = if is_eq then [] else sgl1@sll1 in
1125 if by && smart then given_candidates@sll2
1126 else if by then sll2
1131 smart_candidates_facts,
1132 sort_candidates status context (candidates_other),
1133 sort_candidates status context (smart_candidates_other)
1136 let applicative_case depth signature status flags gty cache =
1137 app_counter:= !app_counter+1;
1138 let _,_,metasenv,subst,_ = status#obj in
1139 let context = ctx_of gty in
1140 let tcache = cache.facts in
1141 let is_prod, is_eq =
1142 let status, t = term_of_cic_term status gty context in
1143 let t = NCicReduction.whd status subst context t in
1145 | NCic.Prod _ -> true, false
1146 | _ -> false, NCicParamod.is_equation status metasenv subst context t
1148 debug_print ~depth (lazy (string_of_bool is_eq));
1150 let candidates_facts, smart_candidates_facts,
1151 candidates_other, smart_candidates_other =
1152 get_candidates ~smart:true depth
1153 flags status tcache signature gty
1155 let sm = if is_eq || is_prod then 0 else 2 in
1156 let sm1 = if flags.last then 2 else 0 in
1157 let maxd = (depth + 1 = flags.maxdepth) in
1158 let try_candidates only_one sm acc candidates =
1161 if (only_one && (elems <> [])) then elems
1163 match try_candidate (~smart:sm)
1164 flags depth status cache.unit_eq context cand with
1166 | Some x -> x::elems)
1169 (* if the goal is the last one we stop at the first fact *)
1170 let elems = try_candidates flags.last sm [] candidates_facts in
1171 (* now we add smart_facts *)
1172 let elems = try_candidates flags.last sm elems smart_candidates_facts in
1173 (* if we are at maxdepth and the goal is not a product we are done
1174 similarly, if the goal is the last one and we already found a
1176 if (maxd && not(is_prod)) || (flags.last && elems<>[]) then elems
1178 let elems = try_candidates false 2 elems candidates_other in
1179 debug_print ~depth (lazy ("not facts: try smart application"));
1180 try_candidates false 2 elems smart_candidates_other
1187 (* gty is supposed to be meta-closed *)
1188 let is_subsumed depth filter_depth status gty cache =
1189 if cache=[] then false else (
1190 debug_print ~depth (lazy("Subsuming " ^ (ppterm status gty)));
1191 let n,h,metasenv,subst,obj = status#obj in
1192 let ctx = ctx_of gty in
1193 let _ , raw_gty = term_of_cic_term status gty ctx in
1194 let target = NCicSubstitution.lift status 1 raw_gty in
1195 (* we compute candidates using the perforated type *)
1202 perforate_small status subst metasenv ctx raw_gty in
1203 let weak = mk_cic_term ctx raw_weak in
1204 debug_print ~depth (lazy ("weak_gty:" ^ NTacStatus.ppterm status weak));
1208 (* candidates must only be searched w.r.t the given context *)
1211 let idx = List.assq ctx cache in
1214 Ncic_termSet.elements
1215 (InvRelDiscriminationTree.retrieve_unifiables idx weak)
1217 with Not_found -> []
1219 (* this is a dirty trick: the first argument of an application is used
1220 to remember at which depth a goal failed *)
1222 let ctx = ctx_of t in
1223 let _, src = term_of_cic_term status t ctx in
1225 | NCic.Appl [NCic.Implicit (`Typeof d); t]
1226 when d <= depth -> Some (mk_cic_term ctx t)
1229 if filter_depth then HExtlib.filter_map filter candidates else candidates in
1231 (lazy ("failure candidates: " ^ string_of_int (List.length candidates)));
1235 let _ , source = term_of_cic_term status t ctx in
1237 NCic.Prod("foo",source,target) in
1238 let metasenv,j,_,_ =
1239 NCicMetaSubst.mk_meta
1240 metasenv ctx ~with_type:implication `IsType in
1241 let status = status#set_obj (n,h,metasenv,subst,obj) in
1242 let status = status#set_stack [([1,Open j],[],[],`NoTag)] in
1244 let status = NTactics.intro_tac "foo" status in
1246 NTactics.apply_tac ("",0,Ast.NCic (NCic.Rel 1)) status
1248 if (head_goals status#stack = []) then raise Found
1253 with Found -> debug_print ~depth (lazy "success");true)
1256 let rec guess_name name ctx =
1257 if name = "_" then guess_name "auto" ctx else
1258 if not (List.mem_assoc name ctx) then name else
1259 guess_name (name^"'") ctx
1262 let is_prod status =
1263 let _, ctx, gty = current_goal status in
1264 let status, gty = apply_subst status ctx gty in
1265 let _, raw_gty = term_of_cic_term status gty ctx in
1267 | NCic.Prod (name,src,_) ->
1268 let status, src = whd status ~delta:0 ctx (mk_cic_term ctx src) in
1269 (match snd (term_of_cic_term status src ctx) with
1270 | NCic.Const(NReference.Ref (_,NReference.Ind _) as r)
1271 | NCic.Appl (NCic.Const(NReference.Ref (_,NReference.Ind _) as r)::_) ->
1272 let _,_,itys,_,_ = NCicEnvironment.get_checked_indtys status r in
1274 (* | [_,_,_,[_;_]] con nat va, ovviamente, in loop *)
1276 | [_,_,_,[]] -> `Inductive (guess_name name ctx)
1277 | _ -> `Some (guess_name name ctx))
1278 | _ -> `Some (guess_name name ctx))
1281 let intro ~depth status facts name =
1282 let status = NTactics.intro_tac name status in
1283 let _, ctx, ngty = current_goal status in
1284 let t = mk_cic_term ctx (NCic.Rel 1) in
1285 let status, keys = keys_of_term status t in
1286 let facts = List.fold_left (add_to_th t) facts keys in
1287 debug_print ~depth (lazy ("intro: "^ name));
1288 (* unprovability is not stable w.r.t introduction *)
1292 let rec intros_facts ~depth status facts =
1293 if List.length (head_goals status#stack) <> 1 then status, facts else
1294 match is_prod status with
1298 intro ~depth status facts name
1299 in intros_facts ~depth status facts
1300 (* | `Inductive name ->
1301 let status = NTactics.case1_tac name status in
1302 intros_facts ~depth status facts *)
1303 | _ -> status, facts
1306 let intros ~depth status cache =
1307 match is_prod status with
1310 let trace = cache.trace in
1312 intros_facts ~depth status cache.facts
1314 if head_goals status#stack = [] then
1315 let status = NTactics.merge_tac status in
1316 [(0,Ast.Ident("__intros",None)),status], cache
1318 (* we reindex the equation from scratch *)
1319 let unit_eq = index_local_equations status#eq_cache status in
1320 let status = NTactics.merge_tac status in
1321 [(0,Ast.Ident("__intros",None)),status],
1322 init_cache ~facts ~unit_eq () ~trace
1326 let reduce ~whd ~depth status g =
1327 let n,h,metasenv,subst,o = status#obj in
1328 let attr, ctx, ty = NCicUtils.lookup_meta g metasenv in
1329 let ty = NCicUntrusted.apply_subst status subst ctx ty in
1331 (if whd then NCicReduction.whd else NCicTacReduction.normalize) status ~subst ctx ty
1336 (lazy ("reduced to: "^ status#ppterm ctx subst metasenv ty'));
1338 (g,(attr,ctx,ty'))::(List.filter (fun (i,_) -> i<>g) metasenv)
1340 let status = status#set_obj (n,h,metasenv,subst,o) in
1341 (* we merge to gain a depth level; the previous goal level should
1343 let status = NTactics.merge_tac status in
1345 [(!candidate_no,Ast.Ident("__whd",None)),status])
1348 let is_meta status gty =
1349 let _, ty = term_of_cic_term status gty (ctx_of gty) in
1351 | NCic.Meta _ -> true
1355 let do_something signature flags status g depth gty cache =
1356 (* if the goal is meta we close it with I:True. This should work
1357 thnaks to the toplogical sorting of goals. *)
1358 if is_meta status gty then
1359 let t = Ast.Ident("I",None) in
1360 debug_print (lazy ("using default term" ^ (NotationPp.pp_term status) t));
1361 let s = NTactics.apply_tac ("",0,t) status in
1364 let l0, cache = intros ~depth status cache in
1365 if l0 <> [] then l0, cache
1368 let l = reduce ~whd:true ~depth status g in
1369 (* if l <> [] then l,cache else *)
1370 (* backward aplications *)
1375 ((!candidate_no,Ast.Ident("__paramod",None)),s))
1376 (auto_eq_check cache.unit_eq status)
1379 if ((l1 <> []) && flags.last) then [] else
1380 applicative_case depth signature status flags gty cache
1384 (fun ((_,t),_) -> toref incr_nominations statistics t) l2;
1385 (* states in l1 have have an empty set of subgoals: no point to sort them *)
1387 (lazy ("alternatives = " ^ (string_of_int (List.length (l1@l@l2)))));
1388 (* we order alternatives w.r.t the number of subgoals they open *)
1389 l1 @ (sort_new_elems l2) @ l, cache
1392 let pp_goal = function
1393 | (_,Continuationals.Stack.Open i)
1394 | (_,Continuationals.Stack.Closed i) -> string_of_int i
1397 let pp_goals status l =
1401 let gty = get_goalty status i in
1402 NTacStatus.ppterm status gty)
1409 let compare = Pervasives.compare
1413 module MS = HTopoSort.Make(M)
1416 let sort_tac status =
1418 match status#stack with
1419 | [] -> assert false
1420 | (goals, t, k, tag) :: s ->
1421 let g = head_goals status#stack in
1423 (List.rev (MS.topological_sort g (deps status))) in
1424 noprint (lazy ("old g = " ^
1425 String.concat "," (List.map string_of_int g)));
1426 noprint (lazy ("sorted goals = " ^
1427 String.concat "," (List.map string_of_int sortedg)));
1428 let is_it i = function
1429 | (_,Continuationals.Stack.Open j )
1430 | (_,Continuationals.Stack.Closed j ) -> i = j
1433 List.map (fun i -> List.find (is_it i) goals) sortedg
1435 (sorted_goals, t, k, tag) :: s
1437 status#set_stack gstatus
1440 let clean_up_tac status =
1442 match status#stack with
1443 | [] -> assert false
1444 | (g, t, k, tag) :: s ->
1445 let is_open = function
1446 | (_,Continuationals.Stack.Open _) -> true
1447 | (_,Continuationals.Stack.Closed _) -> false
1449 let g' = List.filter is_open g in
1450 (g', t, k, tag) :: s
1452 status#set_stack gstatus
1455 let focus_tac focus status =
1457 match status#stack with
1458 | [] -> assert false
1459 | (g, t, k, tag) :: s ->
1460 let in_focus = function
1461 | (_,Continuationals.Stack.Open i)
1462 | (_,Continuationals.Stack.Closed i) -> List.mem i focus
1464 let focus,others = List.partition in_focus g
1466 (* we need to mark it as a BranchTag, otherwise cannot merge later *)
1467 (focus,[],[],`BranchTag) :: (others, t, k, tag) :: s
1469 status#set_stack gstatus
1472 let deep_focus_tac level focus status =
1473 let in_focus = function
1474 | (_,Continuationals.Stack.Open i)
1475 | (_,Continuationals.Stack.Closed i) -> List.mem i focus
1477 let rec slice level gs =
1478 if level = 0 then [],[],gs else
1480 | [] -> assert false
1481 | (g, t, k, tag) :: s ->
1482 let f,o,gs = slice (level-1) s in
1483 let f1,o1 = List.partition in_focus g
1485 (f1,[],[],`BranchTag)::f, (o1, t, k, tag)::o, gs
1488 let f,o,s = slice level status#stack in f@o@s
1490 status#set_stack gstatus
1493 let move_to_side level status =
1494 match status#stack with
1495 | [] -> assert false
1497 let is_open = function
1498 | (_,Continuationals.Stack.Open i) -> Some i
1499 | (_,Continuationals.Stack.Closed _) -> None
1501 let others = menv_closure status (stack_goals (level-1) tl) in
1502 List.for_all (fun i -> IntSet.mem i others)
1503 (HExtlib.filter_map is_open g)
1505 let top_cache ~depth top status cache =
1507 let unit_eq = index_local_equations status#eq_cache status in
1508 {cache with unit_eq = unit_eq}
1511 let rec auto_clusters ?(top=false)
1512 flags signature cache depth status : unit =
1513 debug_print ~depth (lazy ("entering auto clusters at depth " ^
1514 (string_of_int depth)));
1515 debug_print ~depth (pptrace status cache.trace);
1516 (* ignore(Unix.select [] [] [] 0.01); *)
1517 let status = clean_up_tac status in
1518 let goals = head_goals status#stack in
1520 if depth = 0 then raise (Proved (status, cache.trace))
1522 let status = NTactics.merge_tac status in
1524 let l,tree = cache.under_inspection in
1526 | [] -> cache (* possible because of intros that cleans the cache *)
1527 | a::tl -> let tree = rm_from_th a tree a in
1528 {cache with under_inspection = tl,tree}
1530 auto_clusters flags signature cache (depth-1) status
1531 else if List.length goals < 2 then
1532 let cache = top_cache ~depth top status cache in
1533 auto_main flags signature cache depth status
1535 let all_goals = open_goals (depth+1) status in
1536 debug_print ~depth (lazy ("goals = " ^
1537 String.concat "," (List.map string_of_int all_goals)));
1538 let classes = HExtlib.clusters (deps status) all_goals in
1539 (* if any of the classes exceed maxwidth we fail *)
1542 if List.length gl > flags.maxwidth then
1544 debug_print ~depth (lazy "FAIL GLOBAL WIDTH");
1545 HLog.warn (sprintf "global width (%u) exceeded: %u"
1546 flags.maxwidth (List.length gl));
1547 raise (Gaveup cache.failures)
1548 end else ()) classes;
1549 if List.length classes = 1 then
1551 {flags with last = (List.length all_goals = 1)} in
1552 (* no need to cluster *)
1553 let cache = top_cache ~depth top status cache in
1554 auto_main flags signature cache depth status
1556 let classes = if top then List.rev classes else classes in
1562 ("cluster:" ^ String.concat "," (List.map string_of_int l)))
1564 (* we now process each cluster *)
1565 let status,cache,b =
1567 (fun (status,cache,b) gl ->
1569 {flags with last = (List.length gl = 1)} in
1570 let lold = List.length status#stack in
1571 debug_print ~depth (lazy ("stack length = " ^
1572 (string_of_int lold)));
1573 let fstatus = deep_focus_tac (depth+1) gl status in
1574 let cache = top_cache ~depth top fstatus cache in
1576 debug_print ~depth (lazy ("focusing on" ^
1577 String.concat "," (List.map string_of_int gl)));
1578 auto_main flags signature cache depth fstatus; assert false
1580 | Proved(status,trace) ->
1581 let status = NTactics.merge_tac status in
1582 let cache = {cache with trace = trace} in
1583 let lnew = List.length status#stack in
1584 assert (lold = lnew);
1586 | Gaveup failures when top ->
1587 let cache = {cache with failures = failures} in
1590 (status,cache,false) classes
1592 let rec final_merge n s =
1593 if n = 0 then s else final_merge (n-1) (NTactics.merge_tac s)
1594 in let status = final_merge depth status
1595 in if b then raise (Proved(status,cache.trace)) else raise (Gaveup cache.failures)
1599 (* BRAND NEW VERSION *)
1600 auto_main flags signature cache depth status: unit =
1601 debug_print ~depth (lazy "entering auto main");
1602 debug_print ~depth (pptrace status cache.trace);
1603 debug_print ~depth (lazy ("stack length = " ^
1604 (string_of_int (List.length status#stack))));
1605 (* ignore(Unix.select [] [] [] 0.01); *)
1606 let status = sort_tac (clean_up_tac status) in
1607 let goals = head_goals status#stack in
1609 | [] when depth = 0 -> raise (Proved (status,cache.trace))
1611 let status = NTactics.merge_tac status in
1613 let l,tree = cache.under_inspection in
1615 | [] -> cache (* possible because of intros that cleans the cache *)
1616 | a::tl -> let tree = rm_from_th a tree a in
1617 {cache with under_inspection = tl,tree}
1619 auto_clusters flags signature cache (depth-1) status
1621 if depth > 0 && move_to_side depth status
1623 let status = NTactics.merge_tac status in
1625 let l,tree = cache.under_inspection in
1627 | [] -> cache (* possible because of intros that cleans the cache*)
1628 | a::tl -> let tree = rm_from_th a tree a in
1629 {cache with under_inspection = tl,tree}
1631 auto_clusters flags signature cache (depth-1) status
1633 let ng = List.length goals in
1634 (* moved inside auto_clusters *)
1635 if ng > flags.maxwidth then begin
1636 debug_print ~depth (lazy "FAIL LOCAL WIDTH");
1637 HLog.warn (sprintf "local width (%u) exceeded: %u"
1639 raise (Gaveup cache.failures)
1640 end else if depth = flags.maxdepth then
1641 raise (Gaveup cache.failures)
1643 let status = NTactics.branch_tac ~force:true status in
1644 let g,gctx, gty = current_goal status in
1645 let ctx,ty = close status g in
1646 let closegty = mk_cic_term ctx ty in
1647 let status, gty = apply_subst status gctx gty in
1648 debug_print ~depth (lazy("Attacking goal " ^
1649 string_of_int g ^ " : "^ppterm status gty));
1650 debug_print ~depth (lazy ("current failures: " ^
1651 string_of_int (List.length (all_elements ctx cache.failures))));
1653 let _,_,metasenv,subst,_ = status#obj in
1654 NCicParamod.is_equation status metasenv subst ctx ty in
1655 (* if the goal is an equality we artificially raise its depth up to
1656 flags.maxdepth - 1 *)
1657 if (not flags.last && is_eq && (depth < (flags.maxdepth -2))) then
1658 (* for efficiency reasons, in this case we severely cripple the
1660 (debug_print ~depth (lazy ("RAISING DEPTH TO " ^ string_of_int (depth+1)));
1661 auto_main flags signature cache (depth+1) status)
1662 (* check for loops *)
1663 else if is_subsumed depth false status closegty (snd cache.under_inspection) then
1664 (debug_print ~depth (lazy "SUBSUMED");
1665 raise (Gaveup cache.failures))
1666 (* check for failures *)
1667 else if is_subsumed depth true status closegty cache.failures then
1668 (debug_print ~depth (lazy "ALREADY MET");
1669 raise (Gaveup cache.failures))
1671 let new_sig = height_of_goal g status in
1672 if new_sig < signature then
1673 (debug_print ~depth (lazy ("news = " ^ (string_of_int new_sig)));
1674 debug_print ~depth (lazy ("olds = " ^ (string_of_int signature))));
1675 let alternatives, cache =
1676 do_something signature flags status g depth gty cache in
1679 let l,tree = cache.under_inspection in
1680 let l,tree = closegty::l, add_to_th closegty tree closegty in
1681 {cache with under_inspection = l,tree}
1685 (fun allfailures ((_,t),status) ->
1687 (lazy ("(re)considering goal " ^
1688 (string_of_int g) ^" : "^ppterm status gty));
1689 debug_print (~depth:depth)
1690 (lazy ("Case: " ^ NotationPp.pp_term status t));
1692 if t=Ast.Ident("__whd",None) ||
1693 t=Ast.Ident("__intros",None)
1695 else depth+1,loop_cache in
1696 let cache = add_to_trace status ~depth cache t in
1697 let cache = {cache with failures = allfailures} in
1699 auto_clusters flags signature cache depth status;
1702 debug_print ~depth (lazy "Failed");
1704 cache.failures alternatives in
1708 let dty = NCic.Appl [NCic.Implicit (`Typeof depth); ty] in
1711 (*prerr_endline ("FAILURE : " ^ ppterm status gty);*)
1712 add_to_th newfail failures closegty
1714 debug_print ~depth (lazy "no more candidates");
1715 raise (Gaveup failures)
1718 let int name l def =
1719 try int_of_string (List.assoc name l)
1720 with Failure _ | Not_found -> def
1723 module AstSet = Set.Make(struct type t = Ast.term let compare = compare end)
1725 let cleanup_trace s trace =
1726 (* removing duplicates *)
1729 (fun acc t -> AstSet.add t acc)
1730 AstSet.empty trace in
1731 let trace = AstSet.elements trace_set
1732 (* filtering facts *)
1736 | Ast.NRef (NReference.Ref (u,_)) -> not (is_a_fact_obj s u)
1740 let auto_tac ~params:(univ,flags) ?(trace_ref=ref []) status =
1741 let oldstatus = status in
1742 let status = (status:> NTacStatus.tac_status) in
1743 let goals = head_goals status#stack in
1744 let status, facts = mk_th_cache status goals in
1745 (* let unit_eq = index_local_equations status#eq_cache status in *)
1746 let cache = init_cache ~facts () in
1747 (* pp_th status facts; *)
1749 NDiscriminationTree.DiscriminationTree.iter status#auto_cache (fun p t ->
1751 NDiscriminationTree.NCicIndexable.string_of_path p ^ " |--> " ^
1752 String.concat "\n " (List.map (
1753 status#ppterm ~metasenv:[] ~context:[] ~subst:[])
1754 (NDiscriminationTree.TermSet.elements t))
1762 let status, res = disambiguate status [] t None in
1763 let _,res = term_of_cic_term status res (ctx_of res)
1765 in Some (List.map to_Ast l)
1767 let depth = int "depth" flags 3 in
1768 let size = int "size" flags 10 in
1769 let width = int "width" flags 4 (* (3+List.length goals)*) in
1771 (* let goals = List.map (fun i -> (i,P)) goals in *)
1772 let signature = height_of_goals status in
1775 candidates = candidates;
1779 timeout = Unix.gettimeofday() +. 3000.;
1782 let initial_time = Unix.gettimeofday() in
1787 ("TIME ELAPSED:"^string_of_float(Unix.gettimeofday()-.initial_time)));
1789 ("Applicative nodes:"^string_of_int !app_counter));
1790 raise (Error (lazy "auto gave up", None)))
1792 let _ = debug_print (lazy("\n\nRound "^string_of_int x^"\n")) in
1793 let flags = { flags with maxdepth = x }
1795 try auto_clusters (~top:true) flags signature cache 0 status;assert false
1797 try auto_main flags signature cache 0 status;assert false
1800 | Gaveup _ -> up_to (x+1) y
1801 | Proved (s,trace) ->
1802 debug_print (lazy ("proved at depth " ^ string_of_int x));
1803 List.iter (toref incr_uses statistics) trace;
1804 let trace = cleanup_trace s trace in
1805 let _ = debug_print (pptrace status trace) in
1808 | (g,t,k,f) :: rest -> (filter_open g,t,k,f):: rest
1811 let s = s#set_stack stack in
1813 oldstatus#set_status s
1815 let s = up_to depth depth in
1816 debug_print (print_stat status statistics);
1818 ("TIME ELAPSED:"^string_of_float(Unix.gettimeofday()-.initial_time)));
1820 ("Applicative nodes:"^string_of_int !app_counter));
1824 let auto_tac ~params:(_,flags as params) ?trace_ref =
1825 if List.mem_assoc "demod" flags then
1827 else if List.mem_assoc "paramod" flags then
1829 else if List.mem_assoc "fast_paramod" flags then
1830 fast_eq_check_tac ~params
1831 else auto_tac ~params ?trace_ref