2 ||M|| This file is part of HELM, an Hypertextual, Electronic
3 ||A|| Library of Mathematics, developed at the Computer Science
4 ||T|| Department, University of Bologna, Italy.
6 ||T|| HELM is free software; you can redistribute it and/or
7 ||A|| modify it under the terms of the GNU General Public License
8 \ / version 2 or (at your option) any later version.
9 \ / This software is distributed as is, NO WARRANTY.
10 V_______________________________________________________________ *)
14 let print ?(depth=0) s =
15 prerr_endline (String.make (2*depth) ' '^Lazy.force s)
16 let noprint ?(depth=0) _ = ()
17 let debug_print = noprint
19 open Continuationals.Stack
21 module Ast = NotationPt
23 (* ======================= statistics ========================= *)
25 let app_counter = ref 0
28 type t = NReference.reference
30 let compare = Pervasives.compare
31 let hash = Hashtbl.hash
34 module RefHash = Hashtbl.Make(RHT);;
37 nominations : int ref;
41 let statistics: info RefHash.t = RefHash.create 503
43 let incr_nominations tbl item =
45 let v = RefHash.find tbl item in incr v.nominations
47 RefHash.add tbl item {nominations = ref 1; uses = ref 0}
49 let incr_uses tbl item =
51 let v = RefHash.find tbl item in incr v.uses
52 with Not_found -> assert false
58 | Ast.NCic _ (* local candidate *)
61 let is_relevant tbl item =
63 let v = RefHash.find tbl item in
64 if !(v.nominations) < 60 then true (* not enough info *)
65 else if !(v.uses) = 0 then false
67 with Not_found -> true
69 let print_stat status tbl =
70 let l = RefHash.fold (fun a v l -> (a,v)::l) tbl [] in
71 let relevance v = float !(v.uses) /. float !(v.nominations) in
72 let vcompare (_,v1) (_,v2) =
73 Pervasives.compare (relevance v1) (relevance v2) in
74 let l = List.sort vcompare l in
76 NotationPp.pp_term status (Ast.NCic (NCic.Const a)) ^ ": rel = " ^
77 (string_of_float (relevance v)) ^
78 "; uses = " ^ (string_of_int !(v.uses)) ^
79 "; nom = " ^ (string_of_int !(v.nominations)) in
80 lazy ("\n\nSTATISTICS:\n" ^
81 String.concat "\n" (List.map vstring l))
83 (* ======================= utility functions ========================= *)
84 module IntSet = Set.Make(struct type t = int let compare = compare end)
86 let get_sgoalty status g =
87 let _,_,metasenv,subst,_ = status#obj in
89 let _, ctx, ty = NCicUtils.lookup_meta g metasenv in
90 let ty = NCicUntrusted.apply_subst status subst ctx ty in
91 let ctx = NCicUntrusted.apply_subst_context status
92 ~fix_projections:true subst ctx
94 NTacStatus.mk_cic_term ctx ty
95 with NCicUtils.Meta_not_found _ as exn -> fail ~exn (lazy "get_sgoalty")
99 let gty = get_sgoalty status g in
100 metas_of_term status gty
103 let menv_closure status gl =
104 let rec closure acc = function
106 | x::l when IntSet.mem x acc -> closure acc l
107 | x::l -> closure (IntSet.add x acc) (deps status x @ l)
108 in closure IntSet.empty gl
111 (* we call a "fact" an object whose hypothesis occur in the goal
112 or in types of goal-variables *)
113 let branch status ty =
114 let status, ty, metas = saturate ~delta:0 status ty in
115 noprint (lazy ("saturated ty :" ^ (ppterm status ty)));
116 let g_metas = metas_of_term status ty in
117 let clos = menv_closure status g_metas in
118 (* let _,_,metasenv,_,_ = status#obj in *)
122 let _, m = term_of_cic_term status m (ctx_of m) in
124 | NCic.Meta(i,_) -> IntSet.add i acc
128 (* IntSet.subset menv clos *)
129 IntSet.cardinal(IntSet.diff menv clos)
131 let is_a_fact status ty = branch status ty = 0
133 let is_a_fact_obj s uri =
134 let obj = NCicEnvironment.get_checked_obj s uri in
136 | (_,_,[],[],NCic.Constant(_,_,_,ty,_)) ->
137 is_a_fact s (mk_cic_term [] ty)
138 (* aggiungere i costruttori *)
141 let is_a_fact_ast status subst metasenv ctx cand =
143 (lazy ("------- checking " ^ NotationPp.pp_term status cand));
144 let status, t = disambiguate status ctx ("",0,cand) None in
145 let status,t = term_of_cic_term status t ctx in
146 let ty = NCicTypeChecker.typeof status subst metasenv ctx t in
147 is_a_fact status (mk_cic_term ctx ty)
149 let current_goal ?(single_goal=true) status =
150 let open_goals = head_goals status#stack in
152 then assert (List.length open_goals = 1)
153 else assert (List.length open_goals >= 1);
154 let open_goal = List.hd open_goals in
155 let gty = get_goalty status open_goal in
156 let ctx = ctx_of gty in
159 let height_of_ref status (NReference.Ref (uri, x)) =
164 | NReference.CoFix _ ->
165 let _,height,_,_,_ = NCicEnvironment.get_checked_obj status uri in
167 | NReference.Def h -> h
168 | NReference.Fix (_,_,h) -> h
171 (*************************** height functions ********************************)
172 let fast_height_of_term status t =
176 NCic.Meta (_,(_,NCic.Ctx l)) -> List.iter aux l
180 | NCic.Implicit _ -> assert false
183 prerr_endline (status#ppterm ~metasenv:[] ~subst:[]
184 ~context:[] t ^ ":" ^ string_of_int (height_of_ref status nref));
186 h := max !h (height_of_ref status nref)
187 | NCic.Prod (_,t1,t2)
188 | NCic.Lambda (_,t1,t2) -> aux t1; aux t2
189 | NCic.LetIn (_,s,ty,t) -> aux s; aux ty; aux t
190 | NCic.Appl l -> List.iter aux l
191 | NCic.Match (_,outty,t,pl) -> aux outty; aux t; List.iter aux pl
196 let height_of_goal g status =
197 let ty = get_goalty status g in
198 let context = ctx_of ty in
199 let _, ty = term_of_cic_term status ty (ctx_of ty) in
200 let h = ref (fast_height_of_term status ty) in
203 | _, NCic.Decl ty -> h := max !h (fast_height_of_term status ty)
204 | _, NCic.Def (bo,ty) ->
205 h := max !h (fast_height_of_term status ty);
206 h := max !h (fast_height_of_term status bo);
212 let height_of_goals status =
213 let open_goals = head_goals status#stack in
214 assert (List.length open_goals > 0);
218 h := max !h (height_of_goal open_goal status))
220 noprint (lazy ("altezza sequente: " ^ string_of_int !h));
224 (* =============================== paramod =========================== *)
225 let solve f status eq_cache goal =
228 if fast then NCicParamod.fast_eq_check
229 else NCicParamod.paramod in
231 let n,h,metasenv,subst,o = status#obj in
232 let gname, ctx, gty = List.assoc goal metasenv in
233 let gty = NCicUntrusted.apply_subst status subst ctx gty in
234 let build_status (pt, _, metasenv, subst) =
236 noprint (lazy ("refining: "^(status#ppterm ctx subst metasenv pt)));
237 let stamp = Unix.gettimeofday () in
238 let metasenv, subst, pt, pty =
239 (* NCicRefiner.typeof status
240 (* (status#set_coerc_db NCicCoercion.empty_db) *)
241 metasenv subst ctx pt None in
242 debug_print (lazy ("refined: "^(status#ppterm ctx subst metasenv pt)));
243 noprint (lazy ("synt: "^(status#ppterm ctx subst metasenv pty)));
244 let metasenv, subst =
245 NCicUnification.unify status metasenv subst ctx gty pty *)
247 (status#set_coerc_db NCicCoercion.empty_db)
248 metasenv subst ctx pt (Some gty)
250 noprint (lazy (Printf.sprintf "Refined in %fs"
251 (Unix.gettimeofday() -. stamp)));
252 let status = status#set_obj (n,h,metasenv,subst,o) in
253 let metasenv = List.filter (fun j,_ -> j <> goal) metasenv in
254 let subst = (goal,(gname,ctx,pt,pty)) :: subst in
255 Some (status#set_obj (n,h,metasenv,subst,o))
257 NCicRefiner.RefineFailure msg
258 | NCicRefiner.Uncertain msg ->
259 debug_print (lazy ("WARNING: refining in fast_eq_check failed\n" ^
260 snd (Lazy.force msg) ^
261 "\n in the environment\n" ^
262 status#ppmetasenv subst metasenv)); None
263 | NCicRefiner.AssertFailure msg ->
264 debug_print (lazy ("WARNING: refining in fast_eq_check failed" ^
266 "\n in the environment\n" ^
267 status#ppmetasenv subst metasenv)); None
270 HExtlib.filter_map build_status
271 (f status metasenv subst ctx eq_cache (NCic.Rel ~-1,gty))
274 let fast_eq_check eq_cache status (goal:int) =
275 match solve NCicParamod.fast_eq_check status eq_cache goal with
276 | [] -> raise (Error (lazy "no proof found",None))
280 let dist_fast_eq_check eq_cache s =
281 NTactics.distribute_tac (fast_eq_check eq_cache) s
284 let auto_eq_check eq_cache status =
286 let s = dist_fast_eq_check eq_cache status in
289 | Error _ -> debug_print (lazy ("no paramod proof found"));[]
292 let index_local_equations eq_cache status =
293 noprint (lazy "indexing equations");
294 let open_goals = head_goals status#stack in
295 let open_goal = List.hd open_goals in
296 let ngty = get_goalty status open_goal in
297 let ctx = apply_subst_context ~fix_projections:true status (ctx_of ngty) in
302 let t = NCic.Rel !c in
304 let ty = NCicTypeChecker.typeof status [] [] ctx t in
305 if is_a_fact status (mk_cic_term ctx ty) then
306 (noprint(lazy("eq indexing " ^ (status#ppterm ctx [] [] ty)));
307 NCicParamod.forward_infer_step status [] [] ctx eq_cache t ty)
309 (noprint (lazy ("not a fact: " ^ (status#ppterm ctx [] [] ty)));
312 | NCicTypeChecker.TypeCheckerFailure _
313 | NCicTypeChecker.AssertFailure _ -> eq_cache)
317 let fast_eq_check_tac ~params s =
318 let unit_eq = index_local_equations s#eq_cache s in
319 dist_fast_eq_check unit_eq s
322 let paramod eq_cache status goal =
323 match solve NCicParamod.paramod status eq_cache goal with
324 | [] -> raise (Error (lazy "no proof found",None))
328 let paramod_tac ~params s =
329 let unit_eq = index_local_equations s#eq_cache s in
330 NTactics.distribute_tac (paramod unit_eq) s
333 let demod eq_cache status goal =
334 match solve NCicParamod.demod status eq_cache goal with
335 | [] -> raise (Error (lazy "no progress",None))
339 let demod_tac ~params s =
340 let unit_eq = index_local_equations s#eq_cache s in
341 NTactics.distribute_tac (demod unit_eq) s
345 let fast_eq_check_tac_all ~params eq_cache status =
346 let g,_,_ = current_goal status in
347 let allstates = fast_eq_check_all status eq_cache g in
348 let pseudo_low_tac s _ _ = s in
349 let pseudo_low_tactics =
350 List.map pseudo_low_tac allstates
352 List.map (fun f -> NTactics.distribute_tac f status) pseudo_low_tactics
357 let demod status eq_cache goal =
358 let n,h,metasenv,subst,o = status#obj in
359 let gname, ctx, gty = List.assoc goal metasenv in
360 let gty = NCicUntrusted.apply_subst subst ctx gty in
362 let demod_tac ~params s =
363 let unit_eq = index_local_equations s#eq_cache s in
364 dist_fast_eq_check unit_eq s
367 (*************** subsumption ****************)
369 let close_wrt_context status =
373 | name, NCic.Decl t -> NCic.Prod(name,t,ty)
374 | name, NCic.Def(bo, _) -> NCicSubstitution.subst status bo ty)
377 let args_for_context ?(k=1) ctx =
380 (fun (n,l) ctx_entry ->
382 | name, NCic.Decl t -> n+1,NCic.Rel(n)::l
383 | name, NCic.Def(bo, _) -> n+1,l)
387 let constant_for_meta status ctx ty i =
388 let name = "cic:/foo"^(string_of_int i)^".con" in
389 let uri = NUri.uri_of_string name in
390 let ty = close_wrt_context status ty ctx in
391 (* prerr_endline (status#ppterm [] [] [] ty); *)
392 let attr = (`Generated,`Definition,`Local) in
393 let obj = NCic.Constant([],name,None,ty,attr) in
394 (* Constant of relevance * string * term option * term * c_attr *)
398 let refresh metasenv =
400 (fun (metasenv,subst) (i,(iattr,ctx,ty)) ->
401 let ikind = NCicUntrusted.kind_of_meta iattr in
402 let metasenv,j,instance,ty =
403 NCicMetaSubst.mk_meta ~attrs:iattr
404 metasenv ctx ~with_type:ty ikind in
405 let s_entry = i,(iattr, ctx, instance, ty) in
406 let metasenv = List.filter (fun x,_ -> i <> x) metasenv in
407 metasenv,s_entry::subst)
408 (metasenv,[]) metasenv
410 (* close metasenv returns a ground instance of all the metas in the
411 metasenv, insantiatied with axioms, and the list of these axioms *)
412 let close_metasenv status metasenv subst =
414 let metasenv = NCicUntrusted.apply_subst_metasenv subst metasenv in
416 let metasenv = NCicUntrusted.sort_metasenv status subst metasenv in
418 (fun (subst,objs) (i,(iattr,ctx,ty)) ->
419 let ty = NCicUntrusted.apply_subst status subst ctx ty in
421 NCicUntrusted.apply_subst_context status ~fix_projections:true
423 let (uri,_,_,_,obj) as okind =
424 constant_for_meta status ctx ty i in
426 NCicEnvironment.check_and_add_obj status okind;
427 let iref = NReference.reference_of_spec uri NReference.Decl in
429 let args = args_for_context ctx in
430 if args = [] then NCic.Const iref
431 else NCic.Appl(NCic.Const iref::args)
433 (* prerr_endline (status#ppterm ctx [] [] iterm); *)
434 let s_entry = i, ([], ctx, iterm, ty)
435 in s_entry::subst,okind::objs
436 with _ -> assert false)
440 let ground_instances status gl =
441 let _,_,metasenv,subst,_ = status#obj in
442 let subset = menv_closure status gl in
443 let submenv = List.filter (fun (x,_) -> IntSet.mem x subset) metasenv in
445 let submenv = metasenv in
447 let subst, objs = close_metasenv status submenv subst in
451 let (_, ctx, t, _) = List.assoc i subst in
452 noprint (lazy (status#ppterm ctx [] [] t));
454 (fun (uri,_,_,_,_) as obj ->
455 NCicEnvironment.invalidate_item status (`Obj (uri, obj)))
460 Not_found -> assert false
464 let replace_meta status i args target =
465 let rec aux k = function
466 (* TODO: local context *)
467 | NCic.Meta (j,lc) when i = j ->
471 List.map (NCicSubstitution.subst_meta status lc) args in
472 NCic.Appl(NCic.Rel k::args))
473 | NCic.Meta (j,lc) as m ->
480 aux k (NCicSubstitution.lift status n t)) l))))
481 | t -> NCicUtils.map status (fun _ k -> k+1) k aux t
486 let close_wrt_metasenv status subst =
488 (fun ty (i,(iattr,ctx,mty)) ->
489 let mty = NCicUntrusted.apply_subst status subst ctx mty in
491 NCicUntrusted.apply_subst_context status ~fix_projections:true
493 let cty = close_wrt_context status mty ctx in
494 let name = "foo"^(string_of_int i) in
495 let ty = NCicSubstitution.lift status 1 ty in
496 let args = args_for_context ~k:1 ctx in
497 (* prerr_endline (status#ppterm ctx [] [] iterm); *)
498 let ty = replace_meta status i args ty
500 NCic.Prod(name,cty,ty))
504 let _,_,metasenv,subst,_ = status#obj in
505 let subset = menv_closure status [g] in
506 let subset = IntSet.remove g subset in
507 let elems = IntSet.elements subset in
508 let _, ctx, ty = NCicUtils.lookup_meta g metasenv in
509 let ty = NCicUntrusted.apply_subst status subst ctx ty in
510 noprint (lazy ("metas in " ^ (status#ppterm ctx [] metasenv ty)));
511 noprint (lazy (String.concat ", " (List.map string_of_int elems)));
512 let submenv = List.filter (fun (x,_) -> IntSet.mem x subset) metasenv in
513 let submenv = List.rev (NCicUntrusted.sort_metasenv status subst submenv) in
515 let submenv = metasenv in
517 let ty = close_wrt_metasenv status subst ty submenv in
518 noprint (lazy (status#ppterm ctx [] [] ty));
522 (****************** smart application ********************)
524 let saturate_to_ref status metasenv subst ctx nref ty =
525 let height = height_of_ref status nref in
526 let rec aux metasenv ty args =
527 let ty,metasenv,moreargs =
528 NCicMetaSubst.saturate status ~delta:height metasenv subst ctx ty 0 in
530 | NCic.Const(NReference.Ref (_,NReference.Def _) as nre)
532 let _, _, bo, _, _, _ = NCicEnvironment.get_checked_def status nre in
533 aux metasenv bo (args@moreargs)
534 | NCic.Appl(NCic.Const(NReference.Ref (_,NReference.Def _) as nre)::tl)
536 let _, _, bo, _, _, _ = NCicEnvironment.get_checked_def status nre in
537 aux metasenv (NCic.Appl(bo::tl)) (args@moreargs)
538 | _ -> ty,metasenv,(args@moreargs)
542 let smart_apply t unit_eq status g =
543 let n,h,metasenv,subst,o = status#obj in
544 let gname, ctx, gty = List.assoc g metasenv in
545 (* let ggty = mk_cic_term context gty in *)
546 let status, t = disambiguate status ctx t None in
547 let status,t = term_of_cic_term status t ctx in
548 let _,_,metasenv,subst,_ = status#obj in
549 let ty = NCicTypeChecker.typeof status subst metasenv ctx t in
550 let ty,metasenv,args =
553 | NCic.Appl(NCic.Const(nref)::_) ->
554 saturate_to_ref status metasenv subst ctx nref ty
556 NCicMetaSubst.saturate status metasenv subst ctx ty 0 in
557 let metasenv,j,inst,_ = NCicMetaSubst.mk_meta metasenv ctx `IsTerm in
558 let status = status#set_obj (n,h,metasenv,subst,o) in
559 let pterm = if args=[] then t else
561 | NCic.Appl l -> NCic.Appl(l@args)
562 | _ -> NCic.Appl(t::args)
564 noprint(lazy("pterm " ^ (status#ppterm ctx [] [] pterm)));
565 noprint(lazy("pty " ^ (status#ppterm ctx [] [] ty)));
568 NUri.uri_of_string "cic:/matita/basics/logic/eq_coerc.con" in
569 let ref = NReference.reference_of_spec uri (NReference.Def(2)) in
573 NCic.Appl[eq_coerc;ty;NCic.Implicit `Type;pterm;inst] in
574 let smart = mk_cic_term ctx smart in
576 let status = instantiate status g smart in
577 let _,_,metasenv,subst,_ = status#obj in
578 let _,ctx,jty = List.assoc j metasenv in
579 let jty = NCicUntrusted.apply_subst status subst ctx jty in
580 noprint(lazy("goal " ^ (status#ppterm ctx [] [] jty)));
581 fast_eq_check unit_eq status j
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
587 let compare_statuses ~past ~present =
588 let _,_,past,_,_ = past#obj in
589 let _,_,present,_,_ = present#obj in
590 List.map fst (List.filter (fun (i,_) -> not(List.mem_assoc i past)) present),
591 List.map fst (List.filter (fun (i,_) -> not (List.mem_assoc i present)) past)
594 (* paramodulation has only an implicit knoweledge of the symmetry of equality;
595 hence it is in trouble in proving (a = b) = (b = a) *)
596 let try_sym tac status g =
597 (* put the right uri *)
598 let sym_eq = Ast.Appl [Ast.Ident("sym_eq",`Ambiguous); 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 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 " ^ (NotationPp.pp_term status) t));
967 if smart= 0 then NTactics.apply_tac ("",0,t) status
968 else if smart = 1 then smart_apply_auto ("",0,t) eq_cache status
969 else (* smart = 2: both *)
970 try NTactics.apply_tac ("",0,t) status
972 smart_apply_auto ("",0,t) eq_cache status
974 (* we compare the expected branching with the actual one and
975 prune the candidate when the latter is larger. The optimization
976 is meant to rule out stange applications of flexible terms,
977 such as the application of eq_f that always succeeds.
978 There is some gain but less than expected *)
979 let og_no = List.length (open_goals (depth+1) status) in
980 let status, cict = disambiguate status ctx ("",0,t) None in
981 let status,ct = term_of_cic_term status cict ctx in
982 let _,_,metasenv,subst,_ = status#obj in
983 let ty = NCicTypeChecker.typeof status subst metasenv ctx ct in
984 let res = branch status (mk_cic_term ctx ty) in
985 let diff = og_no - old_og_no in
986 debug_print (lazy ("expected branching: " ^ (string_of_int res)));
987 debug_print (lazy ("actual: branching" ^ (string_of_int diff)));
988 (* some flexibility *)
989 if og_no - old_og_no > res then
990 (debug_print (lazy ("branch factor for: " ^ (ppterm status cict) ^ " = "
991 ^ (string_of_int res) ^ " vs. " ^ (string_of_int og_no)));
992 debug_print ~depth (lazy "strange application"); None)
994 (incr candidate_no; Some ((!candidate_no,t),status))
995 with Error (msg,exn) -> debug_print ~depth (lazy "failed"); None
998 let sort_of status subst metasenv ctx t =
999 let ty = NCicTypeChecker.typeof status subst metasenv ctx t in
1000 let metasenv',ty = NCicUnification.fix_sorts status metasenv subst ty in
1001 assert (metasenv = metasenv');
1002 NCicTypeChecker.typeof status subst metasenv ctx ty
1005 let type0= NUri.uri_of_string ("cic:/matita/pts/Type0.univ")
1008 let perforate_small status subst metasenv context t =
1009 let rec aux = function
1010 | NCic.Appl (hd::tl) ->
1012 let s = sort_of status subst metasenv context t in
1014 | NCic.Sort(NCic.Type [`Type,u])
1015 when u=type0 -> NCic.Meta (0,(0,NCic.Irl 0))
1018 NCic.Appl (hd::List.map map tl)
1024 let get_cands retrieve_for diff empty gty weak_gty =
1025 let cands = retrieve_for gty in
1027 | None -> cands, empty
1029 let more_cands = retrieve_for weak_gty in
1030 cands, diff more_cands cands
1033 let get_candidates ?(smart=true) depth flags status cache signature gty =
1034 let universe = status#auto_cache in
1035 let _,_,metasenv,subst,_ = status#obj in
1036 let context = ctx_of gty in
1037 let _, raw_gty = term_of_cic_term status gty context in
1038 let is_prod, is_eq =
1039 let status, t = term_of_cic_term status gty context in
1040 let t = NCicReduction.whd status subst context t in
1042 | NCic.Prod _ -> true, false
1043 | _ -> false, NCicParamod.is_equation status metasenv subst context t
1045 debug_print ~depth (lazy ("gty:" ^ NTacStatus.ppterm status gty));
1047 NCicParamod.is_equation status metasenv subst context raw_gty
1049 let raw_weak_gty, weak_gty =
1056 perforate_small status subst metasenv context raw_gty in
1057 let weak = mk_cic_term context raw_weak in
1058 debug_print ~depth (lazy ("weak_gty:" ^ NTacStatus.ppterm status weak));
1059 Some raw_weak, Some (weak)
1063 (* we now compute global candidates *)
1064 let global_cands, smart_global_cands =
1066 let to_ast = function
1067 | NCic.Const r when true
1068 (*is_relevant statistics r*) -> Some (Ast.NRef r)
1069 (* | NCic.Const _ -> None *)
1070 | _ -> assert false in
1072 to_ast (NDiscriminationTree.TermSet.elements s) in
1075 (NDiscriminationTree.DiscriminationTree.retrieve_unifiables universe)
1076 NDiscriminationTree.TermSet.diff
1077 NDiscriminationTree.TermSet.empty
1078 raw_gty raw_weak_gty in
1080 (* we now compute local candidates *)
1081 let local_cands,smart_local_cands =
1084 let _status, t = term_of_cic_term status t context
1086 List.map to_ast (Ncic_termSet.elements s) in
1089 (fun ty -> search_in_th ty cache)
1090 Ncic_termSet.diff Ncic_termSet.empty gty weak_gty in
1092 (* we now splits candidates in facts or not facts *)
1093 let test = is_a_fact_ast status subst metasenv context in
1094 let by,given_candidates =
1095 match flags.candidates with
1097 | None -> false, [] in
1098 (* we compute candidates to be applied in normal mode, splitted in
1099 facts and not facts *)
1100 let candidates_facts,candidates_other =
1101 let gl1,gl2 = List.partition test global_cands in
1102 let ll1,ll2 = List.partition test local_cands in
1103 (* if the goal is an equation we avoid to apply unit equalities,
1104 since superposition should take care of them; refl is an
1105 exception since it prompts for convertibility *)
1106 let l1 = if is_eq then [Ast.Ident("refl",`Ambiguous)] else gl1@ll1 in
1108 (* if smart given candidates are applied in smart mode *)
1109 if by && smart then ll2
1110 else if by then given_candidates@ll2
1114 (* we now compute candidates to be applied in smart mode, splitted in
1115 facts and not facts *)
1116 let smart_candidates_facts, smart_candidates_other =
1117 if is_prod || not(smart) then [],[]
1119 let sgl1,sgl2 = List.partition test smart_global_cands in
1120 let sll1,sll2 = List.partition test smart_local_cands in
1121 let l1 = if is_eq then [] else sgl1@sll1 in
1123 if by && smart then given_candidates@sll2
1124 else if by then sll2
1129 smart_candidates_facts,
1130 sort_candidates status context (candidates_other),
1131 sort_candidates status context (smart_candidates_other)
1134 let applicative_case depth signature status flags gty cache =
1135 app_counter:= !app_counter+1;
1136 let _,_,metasenv,subst,_ = status#obj in
1137 let context = ctx_of gty in
1138 let tcache = cache.facts in
1139 let is_prod, is_eq =
1140 let status, t = term_of_cic_term status gty context in
1141 let t = NCicReduction.whd status subst context t in
1143 | NCic.Prod _ -> true, false
1144 | _ -> false, NCicParamod.is_equation status metasenv subst context t
1146 debug_print ~depth (lazy (string_of_bool is_eq));
1148 let candidates_facts, smart_candidates_facts,
1149 candidates_other, smart_candidates_other =
1150 get_candidates ~smart:true depth
1151 flags status tcache signature gty
1153 let sm = if is_eq || is_prod then 0 else 2 in
1154 let sm1 = if flags.last then 2 else 0 in
1155 let maxd = (depth + 1 = flags.maxdepth) in
1156 let try_candidates only_one sm acc candidates =
1159 if (only_one && (elems <> [])) then elems
1161 match try_candidate (~smart:sm)
1162 flags depth status cache.unit_eq context cand with
1164 | Some x -> x::elems)
1167 (* if the goal is the last one we stop at the first fact *)
1168 let elems = try_candidates flags.last sm [] candidates_facts in
1169 (* now we add smart_facts *)
1170 let elems = try_candidates flags.last sm elems smart_candidates_facts in
1171 (* if we are at maxdepth and the goal is not a product we are done
1172 similarly, if the goal is the last one and we already found a
1174 if (maxd && not(is_prod)) || (flags.last && elems<>[]) then elems
1176 let elems = try_candidates false 2 elems candidates_other in
1177 debug_print ~depth (lazy ("not facts: try smart application"));
1178 try_candidates false 2 elems smart_candidates_other
1184 (* gty is supposed to be meta-closed *)
1185 let is_subsumed depth filter_depth status gty cache =
1186 if cache=[] then false else (
1187 debug_print ~depth (lazy("Subsuming " ^ (ppterm status gty)));
1188 let n,h,metasenv,subst,obj = status#obj in
1189 let ctx = ctx_of gty in
1190 let _ , raw_gty = term_of_cic_term status gty ctx in
1191 let target = NCicSubstitution.lift status 1 raw_gty in
1192 (* we compute candidates using the perforated type *)
1199 perforate_small status subst metasenv ctx raw_gty in
1200 let weak = mk_cic_term ctx raw_weak in
1201 debug_print ~depth (lazy ("weak_gty:" ^ NTacStatus.ppterm status weak));
1205 (* candidates must only be searched w.r.t the given context *)
1208 let idx = List.assq ctx cache in
1211 Ncic_termSet.elements
1212 (InvRelDiscriminationTree.retrieve_unifiables idx weak)
1214 with Not_found -> []
1216 (* this is a dirty trick: the first argument of an application is used
1217 to remember at which depth a goal failed *)
1219 let ctx = ctx_of t in
1220 let _, src = term_of_cic_term status t ctx in
1222 | NCic.Appl [NCic.Implicit (`Typeof d); t]
1223 when d <= depth -> Some (mk_cic_term ctx t)
1226 if filter_depth then HExtlib.filter_map filter candidates else candidates in
1228 (lazy ("failure candidates: " ^ string_of_int (List.length candidates)));
1232 let _ , source = term_of_cic_term status t ctx in
1234 NCic.Prod("foo",source,target) in
1235 let metasenv,j,_,_ =
1236 NCicMetaSubst.mk_meta
1237 metasenv ctx ~with_type:implication `IsType in
1238 let status = status#set_obj (n,h,metasenv,subst,obj) in
1239 let status = status#set_stack [([1,Open j],[],[],`NoTag)] in
1241 let status = NTactics.intro_tac "foo" status in
1243 NTactics.apply_tac ("",0,Ast.NCic (NCic.Rel 1)) status
1245 if (head_goals status#stack = []) then raise Found
1250 with Found -> debug_print ~depth (lazy "success");true)
1253 let rec guess_name name ctx =
1254 if name = "_" then guess_name "auto" ctx else
1255 if not (List.mem_assoc name ctx) then name else
1256 guess_name (name^"'") ctx
1259 let is_prod status =
1260 let _, ctx, gty = current_goal status in
1261 let status, gty = apply_subst status ctx gty in
1262 let _, raw_gty = term_of_cic_term status gty ctx in
1264 | NCic.Prod (name,src,_) ->
1265 let status, src = whd status ~delta:0 ctx (mk_cic_term ctx src) in
1266 (match snd (term_of_cic_term status src ctx) with
1267 | NCic.Const(NReference.Ref (_,NReference.Ind _) as r)
1268 | NCic.Appl (NCic.Const(NReference.Ref (_,NReference.Ind _) as r)::_) ->
1269 let _,_,itys,_,_ = NCicEnvironment.get_checked_indtys status r in
1271 (* | [_,_,_,[_;_]] con nat va, ovviamente, in loop *)
1273 | [_,_,_,[]] -> `Inductive (guess_name name ctx)
1274 | _ -> `Some (guess_name name ctx))
1275 | _ -> `Some (guess_name name ctx))
1278 let intro ~depth status facts name =
1279 let status = NTactics.intro_tac name status in
1280 let _, ctx, ngty = current_goal status in
1281 let t = mk_cic_term ctx (NCic.Rel 1) in
1282 let status, keys = keys_of_term status t in
1283 let facts = List.fold_left (add_to_th t) facts keys in
1284 debug_print ~depth (lazy ("intro: "^ name));
1285 (* unprovability is not stable w.r.t introduction *)
1289 let rec intros_facts ~depth status facts =
1290 if List.length (head_goals status#stack) <> 1 then status, facts else
1291 match is_prod status with
1295 intro ~depth status facts name
1296 in intros_facts ~depth status facts
1297 (* | `Inductive name ->
1298 let status = NTactics.case1_tac name status in
1299 intros_facts ~depth status facts *)
1300 | _ -> status, facts
1303 let intros ~depth status cache =
1304 match is_prod status with
1307 let trace = cache.trace in
1309 intros_facts ~depth status cache.facts
1311 if head_goals status#stack = [] then
1312 let status = NTactics.merge_tac status in
1313 [(0,Ast.Ident("__intros",`Ambiguous)),status], cache
1315 (* we reindex the equation from scratch *)
1316 let unit_eq = index_local_equations status#eq_cache status in
1317 let status = NTactics.merge_tac status in
1318 [(0,Ast.Ident("__intros",`Ambiguous)),status],
1319 init_cache ~facts ~unit_eq () ~trace
1323 let reduce ~whd ~depth status g =
1324 let n,h,metasenv,subst,o = status#obj in
1325 let attr, ctx, ty = NCicUtils.lookup_meta g metasenv in
1326 let ty = NCicUntrusted.apply_subst status subst ctx ty in
1328 (if whd then NCicReduction.whd else NCicTacReduction.normalize) status ~subst ctx ty
1333 (lazy ("reduced to: "^ status#ppterm ctx subst metasenv ty'));
1335 (g,(attr,ctx,ty'))::(List.filter (fun (i,_) -> i<>g) metasenv)
1337 let status = status#set_obj (n,h,metasenv,subst,o) in
1338 (* we merge to gain a depth level; the previous goal level should
1340 let status = NTactics.merge_tac status in
1342 [(!candidate_no,Ast.Ident("__whd",`Ambiguous)),status])
1345 let do_something signature flags status g depth gty cache =
1346 let l0, cache = intros ~depth status cache in
1347 if l0 <> [] then l0, cache
1350 let l = reduce ~whd:true ~depth status g in
1351 (* if l <> [] then l,cache else *)
1352 (* backward aplications *)
1357 ((!candidate_no,Ast.Ident("__paramod",`Ambiguous)),s))
1358 (auto_eq_check cache.unit_eq status)
1361 if ((l1 <> []) && flags.last) then [] else
1362 applicative_case depth signature status flags gty cache
1366 (fun ((_,t),_) -> toref incr_nominations statistics t) l2;
1367 (* states in l1 have have an empty set of subgoals: no point to sort them *)
1369 (lazy ("alternatives = " ^ (string_of_int (List.length (l1@l@l2)))));
1370 (* we order alternatives w.r.t the number of subgoals they open *)
1371 l1 @ (sort_new_elems l2) @ l, cache
1374 let pp_goal = function
1375 | (_,Continuationals.Stack.Open i)
1376 | (_,Continuationals.Stack.Closed i) -> string_of_int i
1379 let pp_goals status l =
1383 let gty = get_goalty status i in
1384 NTacStatus.ppterm status gty)
1391 let compare = Pervasives.compare
1395 module MS = HTopoSort.Make(M)
1398 let sort_tac status =
1400 match status#stack with
1401 | [] -> assert false
1402 | (goals, t, k, tag) :: s ->
1403 let g = head_goals status#stack in
1405 (List.rev (MS.topological_sort g (deps status))) in
1406 noprint (lazy ("old g = " ^
1407 String.concat "," (List.map string_of_int g)));
1408 noprint (lazy ("sorted goals = " ^
1409 String.concat "," (List.map string_of_int sortedg)));
1410 let is_it i = function
1411 | (_,Continuationals.Stack.Open j )
1412 | (_,Continuationals.Stack.Closed j ) -> i = j
1415 List.map (fun i -> List.find (is_it i) goals) sortedg
1417 (sorted_goals, t, k, tag) :: s
1419 status#set_stack gstatus
1422 let clean_up_tac status =
1424 match status#stack with
1425 | [] -> assert false
1426 | (g, t, k, tag) :: s ->
1427 let is_open = function
1428 | (_,Continuationals.Stack.Open _) -> true
1429 | (_,Continuationals.Stack.Closed _) -> false
1431 let g' = List.filter is_open g in
1432 (g', t, k, tag) :: s
1434 status#set_stack gstatus
1437 let focus_tac focus status =
1439 match status#stack with
1440 | [] -> assert false
1441 | (g, t, k, tag) :: s ->
1442 let in_focus = function
1443 | (_,Continuationals.Stack.Open i)
1444 | (_,Continuationals.Stack.Closed i) -> List.mem i focus
1446 let focus,others = List.partition in_focus g
1448 (* we need to mark it as a BranchTag, otherwise cannot merge later *)
1449 (focus,[],[],`BranchTag) :: (others, t, k, tag) :: s
1451 status#set_stack gstatus
1454 let deep_focus_tac level focus status =
1455 let in_focus = function
1456 | (_,Continuationals.Stack.Open i)
1457 | (_,Continuationals.Stack.Closed i) -> List.mem i focus
1459 let rec slice level gs =
1460 if level = 0 then [],[],gs else
1462 | [] -> assert false
1463 | (g, t, k, tag) :: s ->
1464 let f,o,gs = slice (level-1) s in
1465 let f1,o1 = List.partition in_focus g
1467 (f1,[],[],`BranchTag)::f, (o1, t, k, tag)::o, gs
1470 let f,o,s = slice level status#stack in f@o@s
1472 status#set_stack gstatus
1475 let move_to_side level status =
1476 match status#stack with
1477 | [] -> assert false
1479 let is_open = function
1480 | (_,Continuationals.Stack.Open i) -> Some i
1481 | (_,Continuationals.Stack.Closed _) -> None
1483 let others = menv_closure status (stack_goals (level-1) tl) in
1484 List.for_all (fun i -> IntSet.mem i others)
1485 (HExtlib.filter_map is_open g)
1487 let top_cache ~depth top status cache =
1489 let unit_eq = index_local_equations status#eq_cache status in
1490 {cache with unit_eq = unit_eq}
1493 let rec auto_clusters ?(top=false)
1494 flags signature cache depth status : unit =
1495 debug_print ~depth (lazy ("entering auto clusters at depth " ^
1496 (string_of_int depth)));
1497 debug_print ~depth (pptrace status cache.trace);
1498 (* ignore(Unix.select [] [] [] 0.01); *)
1499 let status = clean_up_tac status in
1500 let goals = head_goals status#stack in
1502 if depth = 0 then raise (Proved (status, cache.trace))
1504 let status = NTactics.merge_tac status in
1506 let l,tree = cache.under_inspection in
1508 | [] -> cache (* possible because of intros that cleans the cache *)
1509 | a::tl -> let tree = rm_from_th a tree a in
1510 {cache with under_inspection = tl,tree}
1512 auto_clusters flags signature cache (depth-1) status
1513 else if List.length goals < 2 then
1514 let cache = top_cache ~depth top status cache in
1515 auto_main flags signature cache depth status
1517 let all_goals = open_goals (depth+1) status in
1518 debug_print ~depth (lazy ("goals = " ^
1519 String.concat "," (List.map string_of_int all_goals)));
1520 let classes = HExtlib.clusters (deps status) all_goals in
1521 (* if any of the classes exceed maxwidth we fail *)
1524 if List.length gl > flags.maxwidth then
1526 debug_print ~depth (lazy "FAIL GLOBAL WIDTH");
1527 HLog.warn (sprintf "global width (%u) exceeded: %u"
1528 flags.maxwidth (List.length gl));
1529 raise (Gaveup cache.failures)
1530 end else ()) classes;
1531 if List.length classes = 1 then
1533 {flags with last = (List.length all_goals = 1)} in
1534 (* no need to cluster *)
1535 let cache = top_cache ~depth top status cache in
1536 auto_main flags signature cache depth status
1538 let classes = if top then List.rev classes else classes in
1544 ("cluster:" ^ String.concat "," (List.map string_of_int l)))
1546 (* we now process each cluster *)
1547 let status,cache,b =
1549 (fun (status,cache,b) gl ->
1551 {flags with last = (List.length gl = 1)} in
1552 let lold = List.length status#stack in
1553 debug_print ~depth (lazy ("stack length = " ^
1554 (string_of_int lold)));
1555 let fstatus = deep_focus_tac (depth+1) gl status in
1556 let cache = top_cache ~depth top fstatus cache in
1558 debug_print ~depth (lazy ("focusing on" ^
1559 String.concat "," (List.map string_of_int gl)));
1560 auto_main flags signature cache depth fstatus; assert false
1562 | Proved(status,trace) ->
1563 let status = NTactics.merge_tac status in
1564 let cache = {cache with trace = trace} in
1565 let lnew = List.length status#stack in
1566 assert (lold = lnew);
1568 | Gaveup failures when top ->
1569 let cache = {cache with failures = failures} in
1572 (status,cache,false) classes
1574 let rec final_merge n s =
1575 if n = 0 then s else final_merge (n-1) (NTactics.merge_tac s)
1576 in let status = final_merge depth status
1577 in if b then raise (Proved(status,cache.trace)) else raise (Gaveup cache.failures)
1581 (* BRAND NEW VERSION *)
1582 auto_main flags signature cache depth status: unit =
1583 debug_print ~depth (lazy "entering auto main");
1584 debug_print ~depth (pptrace status cache.trace);
1585 debug_print ~depth (lazy ("stack length = " ^
1586 (string_of_int (List.length status#stack))));
1587 (* ignore(Unix.select [] [] [] 0.01); *)
1588 let status = sort_tac (clean_up_tac status) in
1589 let goals = head_goals status#stack in
1591 | [] when depth = 0 -> raise (Proved (status,cache.trace))
1593 let status = NTactics.merge_tac status in
1595 let l,tree = cache.under_inspection in
1597 | [] -> cache (* possible because of intros that cleans the cache *)
1598 | a::tl -> let tree = rm_from_th a tree a in
1599 {cache with under_inspection = tl,tree}
1601 auto_clusters flags signature cache (depth-1) status
1603 if depth > 0 && move_to_side depth status
1605 let status = NTactics.merge_tac status in
1607 let l,tree = cache.under_inspection in
1609 | [] -> cache (* possible because of intros that cleans the cache*)
1610 | a::tl -> let tree = rm_from_th a tree a in
1611 {cache with under_inspection = tl,tree}
1613 auto_clusters flags signature cache (depth-1) status
1615 let ng = List.length goals in
1616 (* moved inside auto_clusters *)
1617 if ng > flags.maxwidth then begin
1618 debug_print ~depth (lazy "FAIL LOCAL WIDTH");
1619 HLog.warn (sprintf "local width (%u) exceeded: %u"
1621 raise (Gaveup cache.failures)
1622 end else if depth = flags.maxdepth then
1623 raise (Gaveup cache.failures)
1625 let status = NTactics.branch_tac ~force:true status in
1626 let g,gctx, gty = current_goal status in
1627 let ctx,ty = close status g in
1628 let closegty = mk_cic_term ctx ty in
1629 let status, gty = apply_subst status gctx gty in
1630 debug_print ~depth (lazy("Attacking goal " ^
1631 string_of_int g ^ " : "^ppterm status gty));
1632 debug_print ~depth (lazy ("current failures: " ^
1633 string_of_int (List.length (all_elements ctx cache.failures))));
1635 let _,_,metasenv,subst,_ = status#obj in
1636 NCicParamod.is_equation status metasenv subst ctx ty in
1637 (* if the goal is an equality we artificially raise its depth up to
1638 flags.maxdepth - 1 *)
1639 if (not flags.last && is_eq && (depth < (flags.maxdepth -1))) then
1640 (* for efficiency reasons, in this case we severely cripple the
1642 (debug_print ~depth (lazy ("RAISING DEPTH TO " ^ string_of_int (depth+1)));
1643 auto_main flags signature cache (depth+1) status)
1644 (* check for loops *)
1645 else if is_subsumed depth false status closegty (snd cache.under_inspection) then
1646 (debug_print ~depth (lazy "SUBSUMED");
1647 raise (Gaveup cache.failures))
1648 (* check for failures *)
1649 else if is_subsumed depth true status closegty cache.failures then
1650 (debug_print ~depth (lazy "ALREADY MET");
1651 raise (Gaveup cache.failures))
1653 let new_sig = height_of_goal g status in
1654 if new_sig < signature then
1655 (debug_print ~depth (lazy ("news = " ^ (string_of_int new_sig)));
1656 debug_print ~depth (lazy ("olds = " ^ (string_of_int signature))));
1657 let alternatives, cache =
1658 do_something signature flags status g depth gty cache in
1661 let l,tree = cache.under_inspection in
1662 let l,tree = closegty::l, add_to_th closegty tree closegty in
1663 {cache with under_inspection = l,tree}
1667 (fun allfailures ((_,t),status) ->
1669 (lazy ("(re)considering goal " ^
1670 (string_of_int g) ^" : "^ppterm status gty));
1671 debug_print (~depth:depth)
1672 (lazy ("Case: " ^ NotationPp.pp_term status t));
1674 if t=Ast.Ident("__whd",`Ambiguous) ||
1675 t=Ast.Ident("__intros",`Ambiguous)
1677 else depth+1,loop_cache in
1678 let cache = add_to_trace status ~depth cache t in
1679 let cache = {cache with failures = allfailures} in
1681 auto_clusters flags signature cache depth status;
1684 debug_print ~depth (lazy "Failed");
1686 cache.failures alternatives in
1690 let dty = NCic.Appl [NCic.Implicit (`Typeof depth); ty] in
1693 prerr_endline ("FAILURE : " ^ ppterm status gty);
1694 add_to_th newfail failures closegty
1696 debug_print ~depth (lazy "no more candidates");
1697 raise (Gaveup failures)
1700 let int name l def =
1701 try int_of_string (List.assoc name l)
1702 with Failure _ | Not_found -> def
1705 module AstSet = Set.Make(struct type t = Ast.term let compare = compare end)
1707 let cleanup_trace s trace =
1708 (* removing duplicates *)
1711 (fun acc t -> AstSet.add t acc)
1712 AstSet.empty trace in
1713 let trace = AstSet.elements trace_set
1714 (* filtering facts *)
1718 | Ast.NRef (NReference.Ref (u,_)) -> not (is_a_fact_obj s u)
1722 let auto_tac ~params:(univ,flags) ?(trace_ref=ref []) status =
1723 let oldstatus = status in
1724 let status = (status:> NTacStatus.tac_status) in
1725 let goals = head_goals status#stack in
1726 let status, facts = mk_th_cache status goals in
1727 (* let unit_eq = index_local_equations status#eq_cache status in *)
1728 let cache = init_cache ~facts () in
1729 (* pp_th status facts; *)
1731 NDiscriminationTree.DiscriminationTree.iter status#auto_cache (fun p t ->
1733 NDiscriminationTree.NCicIndexable.string_of_path p ^ " |--> " ^
1734 String.concat "\n " (List.map (
1735 status#ppterm ~metasenv:[] ~context:[] ~subst:[])
1736 (NDiscriminationTree.TermSet.elements t))
1739 (* To allow using Rels in the user-specified candidates, we need a context
1740 * but in the case where multiple goals are open, there is no single context
1741 * to type the Rels. At this time, we require that Rels be typed in the
1742 * context of the first selected goal *)
1743 let _,ctx,_ = current_goal ~single_goal:false status in
1744 let status, candidates =
1746 | None -> status, None
1748 let to_Ast (st,l) t =
1749 let st, res = disambiguate st ctx t None in
1750 let st, res = term_of_cic_term st res (ctx_of res)
1751 in (st, Ast.NCic res::l)
1753 let status, l' = List.fold_left to_Ast (status,[]) l in
1756 let depth = int "depth" flags 3 in
1757 let size = int "size" flags 10 in
1758 let width = int "width" flags 4 (* (3+List.length goals)*) in
1760 (* let goals = List.map (fun i -> (i,P)) goals in *)
1761 let signature = height_of_goals status in
1764 candidates = candidates;
1768 timeout = Unix.gettimeofday() +. 3000.;
1771 let initial_time = Unix.gettimeofday() in
1776 ("TIME ELAPSED:"^string_of_float(Unix.gettimeofday()-.initial_time)));
1778 ("Applicative nodes:"^string_of_int !app_counter));
1779 raise (Error (lazy "auto gave up", None)))
1781 let _ = debug_print (lazy("\n\nRound "^string_of_int x^"\n")) in
1782 let flags = { flags with maxdepth = x }
1784 try auto_clusters (~top:true) flags signature cache 0 status;assert false
1786 try auto_main flags signature cache 0 status;assert false
1789 | Gaveup _ -> up_to (x+1) y
1790 | Proved (s,trace) ->
1791 debug_print (lazy ("proved at depth " ^ string_of_int x));
1792 List.iter (toref incr_uses statistics) trace;
1793 let _ = debug_print (pptrace status trace) in
1794 let trace = cleanup_trace s trace in
1795 let _ = debug_print (pptrace status trace) in
1798 | (g,t,k,f) :: rest -> (filter_open g,t,k,f):: rest
1801 let s = s#set_stack stack in
1803 oldstatus#set_status s
1805 let s = up_to depth depth in
1806 debug_print (print_stat status statistics);
1808 ("TIME ELAPSED:"^string_of_float(Unix.gettimeofday()-.initial_time)));
1810 ("Applicative nodes:"^string_of_int !app_counter));
1814 let auto_tac ~params:(_,flags as params) ?trace_ref =
1815 if List.mem_assoc "demod" flags then
1817 else if List.mem_assoc "paramod" flags then
1819 else if List.mem_assoc "fast_paramod" flags then
1820 fast_eq_check_tac ~params
1821 else auto_tac ~params ?trace_ref