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 = print
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 (* one goal is closed by the application *)
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 (* warning : the order between global_cands and local_cand is
1102 relevant. In this way we process first local cands *)
1103 let l1,l2 = List.partition test (global_cands@local_cands) in
1104 (* if the goal is an equation we avoid to apply unit equalities,
1105 since superposition should take care of them; refl is an
1106 exception since it prompts for convertibility *)
1107 let l1 = if is_eq then [Ast.Ident("refl",`Ambiguous)] else l1 in
1109 (* if smart given candidates are applied in smart mode *)
1110 if by && smart then []
1111 else if by then given_candidates
1115 (* we now compute candidates to be applied in smart mode, splitted in
1116 facts and not facts *)
1117 let smart_candidates_facts, smart_candidates_other =
1118 if is_prod || not(smart) then [],[]
1120 let l1,l2 = List.partition test (smart_local_cands@smart_global_cands) in
1121 let l1 = if is_eq then [] else l1 in
1122 let l2 = if by then given_candidates else l2
1127 smart_candidates_facts,
1128 sort_candidates status context (candidates_other),
1129 sort_candidates status context (smart_candidates_other)
1132 let applicative_case depth signature status flags gty cache =
1133 app_counter:= !app_counter+1;
1134 let _,_,metasenv,subst,_ = status#obj in
1135 let context = ctx_of gty in
1136 let tcache = cache.facts in
1137 let is_prod, is_eq =
1138 let status, t = term_of_cic_term status gty context in
1139 let t = NCicReduction.whd status subst context t in
1141 | NCic.Prod _ -> true, false
1142 | _ -> false, NCicParamod.is_equation status metasenv subst context t
1144 debug_print ~depth (lazy (string_of_bool is_eq));
1146 let candidates_facts, smart_candidates_facts,
1147 candidates_other, smart_candidates_other =
1148 get_candidates ~smart:true depth
1149 flags status tcache signature gty
1151 let sm = if is_eq || is_prod then 0 else 2 in
1152 let sm1 = if flags.last then 2 else 0 in
1153 let maxd = (depth + 1 = flags.maxdepth) in
1154 let try_candidates only_one sm acc candidates =
1157 if (only_one && (elems <> [])) then elems
1159 match try_candidate (~smart:sm)
1160 flags depth status cache.unit_eq context cand with
1162 | Some x -> x::elems)
1165 (* if the goal is the last one we stop at the first fact *)
1166 let elems = try_candidates flags.last sm [] candidates_facts in
1167 (* now we add smart_facts *)
1168 let elems = try_candidates flags.last sm elems smart_candidates_facts in
1169 (* if we are at maxdepth and the goal is not a product we are done
1170 similarly, if the goal is the last one and we already found a
1172 if (maxd && not(is_prod)) || (flags.last && elems<>[]) then elems
1174 let elems = try_candidates false 2 elems candidates_other in
1175 debug_print ~depth (lazy ("not facts: try smart application"));
1176 try_candidates false 2 elems smart_candidates_other
1182 (* gty is supposed to be meta-closed *)
1183 let is_subsumed depth filter_depth status gty cache =
1184 if cache=[] then false else (
1185 debug_print ~depth (lazy("Subsuming " ^ (ppterm status gty)));
1186 let n,h,metasenv,subst,obj = status#obj in
1187 let ctx = ctx_of gty in
1188 let _ , raw_gty = term_of_cic_term status gty ctx in
1189 let target = NCicSubstitution.lift status 1 raw_gty in
1190 (* we compute candidates using the perforated type *)
1197 perforate_small status subst metasenv ctx raw_gty in
1198 let weak = mk_cic_term ctx raw_weak in
1199 debug_print ~depth (lazy ("weak_gty:" ^ NTacStatus.ppterm status weak));
1203 (* candidates must only be searched w.r.t the given context *)
1206 let idx = List.assq ctx cache in
1209 Ncic_termSet.elements
1210 (InvRelDiscriminationTree.retrieve_unifiables idx weak)
1212 with Not_found -> []
1214 (* this is a dirty trick: the first argument of an application is used
1215 to remember at which depth a goal failed *)
1217 let ctx = ctx_of t in
1218 let _, src = term_of_cic_term status t ctx in
1220 | NCic.Appl [NCic.Implicit (`Typeof d); t]
1221 when d <= depth -> Some (mk_cic_term ctx t)
1224 if filter_depth then HExtlib.filter_map filter candidates else candidates in
1226 (lazy ("failure candidates: " ^ string_of_int (List.length candidates)));
1230 let _ , source = term_of_cic_term status t ctx in
1232 NCic.Prod("foo",source,target) in
1233 let metasenv,j,_,_ =
1234 NCicMetaSubst.mk_meta
1235 metasenv ctx ~with_type:implication `IsType in
1236 let status = status#set_obj (n,h,metasenv,subst,obj) in
1237 let status = status#set_stack [([1,Open j],[],[],`NoTag)] in
1239 let status = NTactics.intro_tac "foo" status in
1241 NTactics.apply_tac ("",0,Ast.NCic (NCic.Rel 1)) status
1243 if (head_goals status#stack = []) then raise Found
1248 with Found -> debug_print ~depth (lazy "success");true)
1251 let rec guess_name name ctx =
1252 if name = "_" then guess_name "auto" ctx else
1253 if not (List.mem_assoc name ctx) then name else
1254 guess_name (name^"'") ctx
1257 let is_prod status =
1258 let _, ctx, gty = current_goal status in
1259 let status, gty = apply_subst status ctx gty in
1260 let _, raw_gty = term_of_cic_term status gty ctx in
1262 | NCic.Prod (name,src,_) ->
1263 let status, src = whd status ~delta:0 ctx (mk_cic_term ctx src) in
1264 (match snd (term_of_cic_term status src ctx) with
1265 | NCic.Const(NReference.Ref (_,NReference.Ind _) as r)
1266 | NCic.Appl (NCic.Const(NReference.Ref (_,NReference.Ind _) as r)::_) ->
1267 let _,_,itys,_,_ = NCicEnvironment.get_checked_indtys status r in
1269 (* | [_,_,_,[_;_]] con nat va, ovviamente, in loop *)
1271 | [_,_,_,[]] -> `Inductive (guess_name name ctx)
1272 | _ -> `Some (guess_name name ctx))
1273 | _ -> `Some (guess_name name ctx))
1276 let intro ~depth status facts name =
1277 let status = NTactics.intro_tac name status in
1278 let _, ctx, ngty = current_goal status in
1279 let t = mk_cic_term ctx (NCic.Rel 1) in
1280 let status, keys = keys_of_term status t in
1281 let facts = List.fold_left (add_to_th t) facts keys in
1282 debug_print ~depth (lazy ("intro: "^ name));
1283 (* unprovability is not stable w.r.t introduction *)
1287 let rec intros_facts ~depth status facts =
1288 if List.length (head_goals status#stack) <> 1 then status, facts else
1289 match is_prod status with
1293 intro ~depth status facts name
1294 in intros_facts ~depth status facts
1295 (* | `Inductive name ->
1296 let status = NTactics.case1_tac name status in
1297 intros_facts ~depth status facts *)
1298 | _ -> status, facts
1301 let intros ~depth status cache =
1302 match is_prod status with
1305 let trace = cache.trace in
1307 intros_facts ~depth status cache.facts
1309 if head_goals status#stack = [] then
1310 let status = NTactics.merge_tac status in
1311 [(0,Ast.Ident("__intros",`Ambiguous)),status], cache
1313 (* we reindex the equation from scratch *)
1314 let unit_eq = index_local_equations status#eq_cache status in
1315 let status = NTactics.merge_tac status in
1316 [(0,Ast.Ident("__intros",`Ambiguous)),status],
1317 init_cache ~facts ~unit_eq () ~trace
1321 let reduce ~whd ~depth status g =
1322 let n,h,metasenv,subst,o = status#obj in
1323 let attr, ctx, ty = NCicUtils.lookup_meta g metasenv in
1324 let ty = NCicUntrusted.apply_subst status subst ctx ty in
1326 (if whd then NCicReduction.whd else NCicTacReduction.normalize) status ~subst ctx ty
1331 (lazy ("reduced to: "^ status#ppterm ctx subst metasenv ty'));
1333 (g,(attr,ctx,ty'))::(List.filter (fun (i,_) -> i<>g) metasenv)
1335 let status = status#set_obj (n,h,metasenv,subst,o) in
1336 (* we merge to gain a depth level; the previous goal level should
1338 let status = NTactics.merge_tac status in
1340 [(!candidate_no,Ast.Ident("__whd",`Ambiguous)),status])
1343 let do_something signature flags status g depth gty cache =
1344 let l0, cache = intros ~depth status cache in
1345 if l0 <> [] then l0, cache
1348 let l = reduce ~whd:true ~depth status g in
1349 (* if l <> [] then l,cache else *)
1350 (* backward aplications *)
1355 ((!candidate_no,Ast.Ident("__paramod",`Ambiguous)),s))
1356 (auto_eq_check cache.unit_eq status)
1359 if ((l1 <> []) && flags.last) then [] else
1360 applicative_case depth signature status flags gty cache
1364 (fun ((_,t),_) -> toref incr_nominations statistics t) l2;
1365 (* states in l1 have have an empty set of subgoals: no point to sort them *)
1367 (lazy ("alternatives = " ^ (string_of_int (List.length (l1@l@l2)))));
1368 (* we order alternatives w.r.t the number of subgoals they open *)
1369 l1 @ (sort_new_elems l2) @ l, cache
1372 let pp_goal = function
1373 | (_,Continuationals.Stack.Open i)
1374 | (_,Continuationals.Stack.Closed i) -> string_of_int i
1377 let pp_goals status l =
1381 let gty = get_goalty status i in
1382 NTacStatus.ppterm status gty)
1389 let compare = Pervasives.compare
1393 module MS = HTopoSort.Make(M)
1396 let sort_tac status =
1398 match status#stack with
1399 | [] -> assert false
1400 | (goals, t, k, tag) :: s ->
1401 let g = head_goals status#stack in
1403 (List.rev (MS.topological_sort g (deps status))) in
1404 noprint (lazy ("old g = " ^
1405 String.concat "," (List.map string_of_int g)));
1406 noprint (lazy ("sorted goals = " ^
1407 String.concat "," (List.map string_of_int sortedg)));
1408 let is_it i = function
1409 | (_,Continuationals.Stack.Open j )
1410 | (_,Continuationals.Stack.Closed j ) -> i = j
1413 List.map (fun i -> List.find (is_it i) goals) sortedg
1415 (sorted_goals, t, k, tag) :: s
1417 status#set_stack gstatus
1420 let clean_up_tac status =
1422 match status#stack with
1423 | [] -> assert false
1424 | (g, t, k, tag) :: s ->
1425 let is_open = function
1426 | (_,Continuationals.Stack.Open _) -> true
1427 | (_,Continuationals.Stack.Closed _) -> false
1429 let g' = List.filter is_open g in
1430 (g', t, k, tag) :: s
1432 status#set_stack gstatus
1435 let focus_tac focus status =
1437 match status#stack with
1438 | [] -> assert false
1439 | (g, t, k, tag) :: s ->
1440 let in_focus = function
1441 | (_,Continuationals.Stack.Open i)
1442 | (_,Continuationals.Stack.Closed i) -> List.mem i focus
1444 let focus,others = List.partition in_focus g
1446 (* we need to mark it as a BranchTag, otherwise cannot merge later *)
1447 (focus,[],[],`BranchTag) :: (others, t, k, tag) :: s
1449 status#set_stack gstatus
1452 let deep_focus_tac level focus status =
1453 let in_focus = function
1454 | (_,Continuationals.Stack.Open i)
1455 | (_,Continuationals.Stack.Closed i) -> List.mem i focus
1457 let rec slice level gs =
1458 if level = 0 then [],[],gs else
1460 | [] -> assert false
1461 | (g, t, k, tag) :: s ->
1462 let f,o,gs = slice (level-1) s in
1463 let f1,o1 = List.partition in_focus g
1465 (f1,[],[],`BranchTag)::f, (o1, t, k, tag)::o, gs
1468 let f,o,s = slice level status#stack in f@o@s
1470 status#set_stack gstatus
1473 let move_to_side level status =
1474 match status#stack with
1475 | [] -> assert false
1477 let is_open = function
1478 | (_,Continuationals.Stack.Open i) -> Some i
1479 | (_,Continuationals.Stack.Closed _) -> None
1481 let others = menv_closure status (stack_goals (level-1) tl) in
1482 List.for_all (fun i -> IntSet.mem i others)
1483 (HExtlib.filter_map is_open g)
1485 let top_cache ~depth top status cache =
1487 let unit_eq = index_local_equations status#eq_cache status in
1488 {cache with unit_eq = unit_eq}
1491 let rec auto_clusters ?(top=false)
1492 flags signature cache depth status : unit =
1493 debug_print ~depth (lazy ("entering auto clusters at depth " ^
1494 (string_of_int depth)));
1495 debug_print ~depth (pptrace status cache.trace);
1496 (* ignore(Unix.select [] [] [] 0.01); *)
1497 let status = clean_up_tac status in
1498 let goals = head_goals status#stack in
1500 if depth = 0 then raise (Proved (status, cache.trace))
1502 let status = NTactics.merge_tac status in
1504 let l,tree = cache.under_inspection in
1506 | [] -> cache (* possible because of intros that cleans the cache *)
1507 | a::tl -> let tree = rm_from_th a tree a in
1508 {cache with under_inspection = tl,tree}
1510 auto_clusters flags signature cache (depth-1) status
1511 else if List.length goals < 2 then
1512 let cache = top_cache ~depth top status cache in
1513 auto_main flags signature cache depth status
1515 let all_goals = open_goals (depth+1) status in
1516 debug_print ~depth (lazy ("goals = " ^
1517 String.concat "," (List.map string_of_int all_goals)));
1518 let classes = HExtlib.clusters (deps status) all_goals in
1519 (* if any of the classes exceed maxwidth we fail *)
1522 if List.length gl > flags.maxwidth then
1524 debug_print ~depth (lazy "FAIL GLOBAL WIDTH");
1525 HLog.warn (sprintf "global width (%u) exceeded: %u"
1526 flags.maxwidth (List.length gl));
1527 raise (Gaveup cache.failures)
1528 end else ()) classes;
1529 if List.length classes = 1 then
1531 {flags with last = (List.length all_goals = 1)} in
1532 (* no need to cluster *)
1533 let cache = top_cache ~depth top status cache in
1534 auto_main flags signature cache depth status
1536 let classes = if top then List.rev classes else classes in
1542 ("cluster:" ^ String.concat "," (List.map string_of_int l)))
1544 (* we now process each cluster *)
1545 let status,cache,b =
1547 (fun (status,cache,b) gl ->
1549 {flags with last = (List.length gl = 1)} in
1550 let lold = List.length status#stack in
1551 debug_print ~depth (lazy ("stack length = " ^
1552 (string_of_int lold)));
1553 let fstatus = deep_focus_tac (depth+1) gl status in
1554 let cache = top_cache ~depth top fstatus cache in
1556 debug_print ~depth (lazy ("focusing on" ^
1557 String.concat "," (List.map string_of_int gl)));
1558 auto_main flags signature cache depth fstatus; assert false
1560 | Proved(status,trace) ->
1561 let status = NTactics.merge_tac status in
1562 let cache = {cache with trace = trace} in
1563 let lnew = List.length status#stack in
1564 assert (lold = lnew);
1566 | Gaveup failures when top ->
1567 let cache = {cache with failures = failures} in
1570 (status,cache,false) classes
1572 let rec final_merge n s =
1573 if n = 0 then s else final_merge (n-1) (NTactics.merge_tac s)
1574 in let status = final_merge depth status
1575 in if b then raise (Proved(status,cache.trace)) else raise (Gaveup cache.failures)
1579 (* BRAND NEW VERSION *)
1580 auto_main flags signature cache depth status: unit =
1581 debug_print ~depth (lazy "entering auto main");
1582 debug_print ~depth (pptrace status cache.trace);
1583 debug_print ~depth (lazy ("stack length = " ^
1584 (string_of_int (List.length status#stack))));
1585 (* ignore(Unix.select [] [] [] 0.01); *)
1586 let status = sort_tac (clean_up_tac status) in
1587 let goals = head_goals status#stack in
1589 | [] when depth = 0 -> raise (Proved (status,cache.trace))
1591 let status = NTactics.merge_tac status in
1593 let l,tree = cache.under_inspection in
1595 | [] -> cache (* possible because of intros that cleans the cache *)
1596 | a::tl -> let tree = rm_from_th a tree a in
1597 {cache with under_inspection = tl,tree}
1599 auto_clusters flags signature cache (depth-1) status
1601 if depth > 0 && move_to_side depth status
1603 let status = NTactics.merge_tac status in
1605 let l,tree = cache.under_inspection in
1607 | [] -> cache (* possible because of intros that cleans the cache*)
1608 | a::tl -> let tree = rm_from_th a tree a in
1609 {cache with under_inspection = tl,tree}
1611 auto_clusters flags signature cache (depth-1) status
1613 let ng = List.length goals in
1614 (* moved inside auto_clusters *)
1615 if ng > flags.maxwidth then begin
1616 debug_print ~depth (lazy "FAIL LOCAL WIDTH");
1617 HLog.warn (sprintf "local width (%u) exceeded: %u"
1619 raise (Gaveup cache.failures)
1620 end else if depth = flags.maxdepth then
1621 raise (Gaveup cache.failures)
1623 let status = NTactics.branch_tac ~force:true status in
1624 let g,gctx, gty = current_goal status in
1625 let ctx,ty = close status g in
1626 let closegty = mk_cic_term ctx ty in
1627 let status, gty = apply_subst status gctx gty in
1628 debug_print ~depth (lazy("Attacking goal " ^
1629 string_of_int g ^ " : "^ppterm status gty));
1630 debug_print ~depth (lazy ("current failures: " ^
1631 string_of_int (List.length (all_elements ctx cache.failures))));
1633 let _,_,metasenv,subst,_ = status#obj in
1634 NCicParamod.is_equation status metasenv subst ctx ty in
1635 (* if the goal is an equality we artificially raise its depth up to
1636 flags.maxdepth - 1 *)
1637 if (not flags.last && is_eq && (depth < (flags.maxdepth -1))) then
1638 (* for efficiency reasons, in this case we severely cripple the
1640 (debug_print ~depth (lazy ("RAISING DEPTH TO " ^ string_of_int (depth+1)));
1641 auto_main flags signature cache (depth+1) status)
1642 (* check for loops *)
1643 else if is_subsumed depth false status closegty (snd cache.under_inspection) then
1644 (debug_print ~depth (lazy "SUBSUMED");
1645 raise (Gaveup cache.failures))
1646 (* check for failures *)
1647 else if is_subsumed depth true status closegty cache.failures then
1648 (debug_print ~depth (lazy "ALREADY MET");
1649 raise (Gaveup cache.failures))
1651 let new_sig = height_of_goal g status in
1652 if new_sig < signature then
1653 (debug_print ~depth (lazy ("news = " ^ (string_of_int new_sig)));
1654 debug_print ~depth (lazy ("olds = " ^ (string_of_int signature))));
1655 let alternatives, cache =
1656 do_something signature flags status g depth gty cache in
1659 let l,tree = cache.under_inspection in
1660 let l,tree = closegty::l, add_to_th closegty tree closegty in
1661 {cache with under_inspection = l,tree}
1665 (fun allfailures ((_,t),status) ->
1667 (lazy ("(re)considering goal " ^
1668 (string_of_int g) ^" : "^ppterm status gty));
1669 debug_print (~depth:depth)
1670 (lazy ("Case: " ^ NotationPp.pp_term status t));
1672 if t=Ast.Ident("__whd",`Ambiguous) ||
1673 t=Ast.Ident("__intros",`Ambiguous)
1675 else depth+1,loop_cache in
1676 let cache = add_to_trace status ~depth cache t in
1677 let cache = {cache with failures = allfailures} in
1679 auto_clusters flags signature cache depth status;
1682 debug_print ~depth (lazy "Failed");
1684 cache.failures alternatives in
1688 let dty = NCic.Appl [NCic.Implicit (`Typeof depth); ty] in
1691 prerr_endline ("FAILURE : " ^ ppterm status gty);
1692 add_to_th newfail failures closegty
1694 debug_print ~depth (lazy "no more candidates");
1695 raise (Gaveup failures)
1698 let int name l def =
1699 try int_of_string (List.assoc name l)
1700 with Failure _ | Not_found -> def
1703 module AstSet = Set.Make(struct type t = Ast.term let compare = compare end)
1705 let cleanup_trace s trace =
1706 (* removing duplicates *)
1709 (fun acc t -> AstSet.add t acc)
1710 AstSet.empty trace in
1711 let trace = AstSet.elements trace_set
1712 (* filtering facts *)
1716 | Ast.NRef (NReference.Ref (u,_)) -> not (is_a_fact_obj s u)
1720 let auto_tac ~params:(univ,flags) ?(trace_ref=ref []) status =
1721 let oldstatus = status in
1722 let status = (status:> NTacStatus.tac_status) in
1723 let goals = head_goals status#stack in
1724 let status, facts = mk_th_cache status goals in
1725 (* let unit_eq = index_local_equations status#eq_cache status in *)
1726 let cache = init_cache ~facts () in
1727 (* pp_th status facts; *)
1729 NDiscriminationTree.DiscriminationTree.iter status#auto_cache (fun p t ->
1731 NDiscriminationTree.NCicIndexable.string_of_path p ^ " |--> " ^
1732 String.concat "\n " (List.map (
1733 status#ppterm ~metasenv:[] ~context:[] ~subst:[])
1734 (NDiscriminationTree.TermSet.elements t))
1737 (* To allow using Rels in the user-specified candidates, we need a context
1738 * but in the case where multiple goals are open, there is no single context
1739 * to type the Rels. At this time, we require that Rels be typed in the
1740 * context of the first selected goal *)
1741 let _,ctx,_ = current_goal ~single_goal:false status in
1742 let status, candidates =
1744 | None -> status, None
1746 let to_Ast (st,l) t =
1747 let st, res = disambiguate st ctx t None in
1748 let st, res = term_of_cic_term st res (ctx_of res)
1749 in (st, Ast.NCic res::l)
1751 let status, l' = List.fold_left to_Ast (status,[]) l in
1754 let depth = int "depth" flags 3 in
1755 let size = int "size" flags 10 in
1756 let width = int "width" flags 4 (* (3+List.length goals)*) in
1758 (* let goals = List.map (fun i -> (i,P)) goals in *)
1759 let signature = height_of_goals status in
1762 candidates = candidates;
1766 timeout = Unix.gettimeofday() +. 3000.;
1769 let initial_time = Unix.gettimeofday() in
1774 ("TIME ELAPSED:"^string_of_float(Unix.gettimeofday()-.initial_time)));
1776 ("Applicative nodes:"^string_of_int !app_counter));
1777 raise (Error (lazy "auto gave up", None)))
1779 let _ = debug_print (lazy("\n\nRound "^string_of_int x^"\n")) in
1780 let flags = { flags with maxdepth = x }
1782 try auto_clusters (~top:true) flags signature cache 0 status;assert false
1784 try auto_main flags signature cache 0 status;assert false
1787 | Gaveup _ -> up_to (x+1) y
1788 | Proved (s,trace) ->
1789 debug_print (lazy ("proved at depth " ^ string_of_int x));
1790 List.iter (toref incr_uses statistics) trace;
1791 let _ = debug_print (pptrace status trace) in
1792 let trace = cleanup_trace s trace in
1793 let _ = debug_print (pptrace status trace) in
1796 | (g,t,k,f) :: rest -> (filter_open g,t,k,f):: rest
1799 let s = s#set_stack stack in
1801 oldstatus#set_status s
1803 let s = up_to depth depth in
1804 debug_print (print_stat status statistics);
1806 ("TIME ELAPSED:"^string_of_float(Unix.gettimeofday()-.initial_time)));
1808 ("Applicative nodes:"^string_of_int !app_counter));
1812 let auto_tac ~params:(_,flags as params) ?trace_ref =
1813 if List.mem_assoc "demod" flags then
1815 else if List.mem_assoc "paramod" flags then
1817 else if List.mem_assoc "fast_paramod" flags then
1818 fast_eq_check_tac ~params
1819 else auto_tac ~params ?trace_ref