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 status =
150 let open_goals = head_goals status#stack in
151 assert (List.length open_goals = 1);
152 let open_goal = List.hd open_goals in
153 let gty = get_goalty status open_goal in
154 let ctx = ctx_of gty in
157 let height_of_ref status (NReference.Ref (uri, x)) =
162 | NReference.CoFix _ ->
163 let _,height,_,_,_ = NCicEnvironment.get_checked_obj status uri in
165 | NReference.Def h -> h
166 | NReference.Fix (_,_,h) -> h
169 (*************************** height functions ********************************)
170 let fast_height_of_term status t =
174 NCic.Meta (_,(_,NCic.Ctx l)) -> List.iter aux l
178 | NCic.Implicit _ -> assert false
181 prerr_endline (status#ppterm ~metasenv:[] ~subst:[]
182 ~context:[] t ^ ":" ^ string_of_int (height_of_ref status nref));
184 h := max !h (height_of_ref status nref)
185 | NCic.Prod (_,t1,t2)
186 | NCic.Lambda (_,t1,t2) -> aux t1; aux t2
187 | NCic.LetIn (_,s,ty,t) -> aux s; aux ty; aux t
188 | NCic.Appl l -> List.iter aux l
189 | NCic.Match (_,outty,t,pl) -> aux outty; aux t; List.iter aux pl
194 let height_of_goal g status =
195 let ty = get_goalty status g in
196 let context = ctx_of ty in
197 let _, ty = term_of_cic_term status ty (ctx_of ty) in
198 let h = ref (fast_height_of_term status ty) in
201 | _, NCic.Decl ty -> h := max !h (fast_height_of_term status ty)
202 | _, NCic.Def (bo,ty) ->
203 h := max !h (fast_height_of_term status ty);
204 h := max !h (fast_height_of_term status bo);
210 let height_of_goals status =
211 let open_goals = head_goals status#stack in
212 assert (List.length open_goals > 0);
216 h := max !h (height_of_goal open_goal status))
218 noprint (lazy ("altezza sequente: " ^ string_of_int !h));
222 (* =============================== paramod =========================== *)
223 let solve f status eq_cache goal =
226 if fast then NCicParamod.fast_eq_check
227 else NCicParamod.paramod in
229 let n,h,metasenv,subst,o = status#obj in
230 let gname, ctx, gty = List.assoc goal metasenv in
231 let gty = NCicUntrusted.apply_subst status subst ctx gty in
232 let build_status (pt, _, metasenv, subst) =
234 noprint (lazy ("refining: "^(status#ppterm ctx subst metasenv pt)));
235 let stamp = Unix.gettimeofday () in
236 let metasenv, subst, pt, pty =
237 (* NCicRefiner.typeof status
238 (* (status#set_coerc_db NCicCoercion.empty_db) *)
239 metasenv subst ctx pt None in
240 debug_print (lazy ("refined: "^(status#ppterm ctx subst metasenv pt)));
241 noprint (lazy ("synt: "^(status#ppterm ctx subst metasenv pty)));
242 let metasenv, subst =
243 NCicUnification.unify status metasenv subst ctx gty pty *)
245 (status#set_coerc_db NCicCoercion.empty_db)
246 metasenv subst ctx pt (Some gty)
248 noprint (lazy (Printf.sprintf "Refined in %fs"
249 (Unix.gettimeofday() -. stamp)));
250 let status = status#set_obj (n,h,metasenv,subst,o) in
251 let metasenv = List.filter (fun j,_ -> j <> goal) metasenv in
252 let subst = (goal,(gname,ctx,pt,pty)) :: subst in
253 Some (status#set_obj (n,h,metasenv,subst,o))
255 NCicRefiner.RefineFailure msg
256 | NCicRefiner.Uncertain msg ->
257 debug_print (lazy ("WARNING: refining in fast_eq_check failed\n" ^
258 snd (Lazy.force msg) ^
259 "\n in the environment\n" ^
260 status#ppmetasenv subst metasenv)); None
261 | NCicRefiner.AssertFailure msg ->
262 debug_print (lazy ("WARNING: refining in fast_eq_check failed" ^
264 "\n in the environment\n" ^
265 status#ppmetasenv subst metasenv)); None
268 HExtlib.filter_map build_status
269 (f status metasenv subst ctx eq_cache (NCic.Rel ~-1,gty))
272 let fast_eq_check eq_cache status (goal:int) =
273 match solve NCicParamod.fast_eq_check status eq_cache goal with
274 | [] -> raise (Error (lazy "no proof found",None))
278 let dist_fast_eq_check eq_cache s =
279 NTactics.distribute_tac (fast_eq_check eq_cache) s
282 let auto_eq_check eq_cache status =
284 let s = dist_fast_eq_check eq_cache status in
287 | Error _ -> debug_print (lazy ("no paramod proof found"));[]
290 let index_local_equations eq_cache status =
291 noprint (lazy "indexing equations");
292 let open_goals = head_goals status#stack in
293 let open_goal = List.hd open_goals in
294 let ngty = get_goalty status open_goal in
295 let ctx = apply_subst_context ~fix_projections:true status (ctx_of ngty) in
300 let t = NCic.Rel !c in
302 let ty = NCicTypeChecker.typeof status [] [] ctx t in
303 if is_a_fact status (mk_cic_term ctx ty) then
304 (noprint(lazy("eq indexing " ^ (status#ppterm ctx [] [] ty)));
305 NCicParamod.forward_infer_step status [] [] ctx eq_cache t ty)
307 (noprint (lazy ("not a fact: " ^ (status#ppterm ctx [] [] ty)));
310 | NCicTypeChecker.TypeCheckerFailure _
311 | NCicTypeChecker.AssertFailure _ -> eq_cache)
315 let fast_eq_check_tac ~params s =
316 let unit_eq = index_local_equations s#eq_cache s in
317 dist_fast_eq_check unit_eq s
320 let paramod eq_cache status goal =
321 match solve NCicParamod.paramod status eq_cache goal with
322 | [] -> raise (Error (lazy "no proof found",None))
326 let paramod_tac ~params s =
327 let unit_eq = index_local_equations s#eq_cache s in
328 NTactics.distribute_tac (paramod unit_eq) s
331 let demod eq_cache status goal =
332 match solve NCicParamod.demod status eq_cache goal with
333 | [] -> raise (Error (lazy "no progress",None))
337 let demod_tac ~params s =
338 let unit_eq = index_local_equations s#eq_cache s in
339 NTactics.distribute_tac (demod unit_eq) s
343 let fast_eq_check_tac_all ~params eq_cache status =
344 let g,_,_ = current_goal status in
345 let allstates = fast_eq_check_all status eq_cache g in
346 let pseudo_low_tac s _ _ = s in
347 let pseudo_low_tactics =
348 List.map pseudo_low_tac allstates
350 List.map (fun f -> NTactics.distribute_tac f status) pseudo_low_tactics
355 let demod status eq_cache goal =
356 let n,h,metasenv,subst,o = status#obj in
357 let gname, ctx, gty = List.assoc goal metasenv in
358 let gty = NCicUntrusted.apply_subst subst ctx gty in
360 let demod_tac ~params s =
361 let unit_eq = index_local_equations s#eq_cache s in
362 dist_fast_eq_check unit_eq s
365 (*************** subsumption ****************)
367 let close_wrt_context status =
371 | name, NCic.Decl t -> NCic.Prod(name,t,ty)
372 | name, NCic.Def(bo, _) -> NCicSubstitution.subst status bo ty)
375 let args_for_context ?(k=1) ctx =
378 (fun (n,l) ctx_entry ->
380 | name, NCic.Decl t -> n+1,NCic.Rel(n)::l
381 | name, NCic.Def(bo, _) -> n+1,l)
385 let constant_for_meta status ctx ty i =
386 let name = "cic:/foo"^(string_of_int i)^".con" in
387 let uri = NUri.uri_of_string name in
388 let ty = close_wrt_context status ty ctx in
389 (* prerr_endline (status#ppterm [] [] [] ty); *)
390 let attr = (`Generated,`Definition,`Local) in
391 let obj = NCic.Constant([],name,None,ty,attr) in
392 (* Constant of relevance * string * term option * term * c_attr *)
396 let refresh metasenv =
398 (fun (metasenv,subst) (i,(iattr,ctx,ty)) ->
399 let ikind = NCicUntrusted.kind_of_meta iattr in
400 let metasenv,j,instance,ty =
401 NCicMetaSubst.mk_meta ~attrs:iattr
402 metasenv ctx ~with_type:ty ikind in
403 let s_entry = i,(iattr, ctx, instance, ty) in
404 let metasenv = List.filter (fun x,_ -> i <> x) metasenv in
405 metasenv,s_entry::subst)
406 (metasenv,[]) metasenv
408 (* close metasenv returns a ground instance of all the metas in the
409 metasenv, insantiatied with axioms, and the list of these axioms *)
410 let close_metasenv status metasenv subst =
412 let metasenv = NCicUntrusted.apply_subst_metasenv subst metasenv in
414 let metasenv = NCicUntrusted.sort_metasenv status subst metasenv in
416 (fun (subst,objs) (i,(iattr,ctx,ty)) ->
417 let ty = NCicUntrusted.apply_subst status subst ctx ty in
419 NCicUntrusted.apply_subst_context status ~fix_projections:true
421 let (uri,_,_,_,obj) as okind =
422 constant_for_meta status ctx ty i in
424 NCicEnvironment.check_and_add_obj status okind;
425 let iref = NReference.reference_of_spec uri NReference.Decl in
427 let args = args_for_context ctx in
428 if args = [] then NCic.Const iref
429 else NCic.Appl(NCic.Const iref::args)
431 (* prerr_endline (status#ppterm ctx [] [] iterm); *)
432 let s_entry = i, ([], ctx, iterm, ty)
433 in s_entry::subst,okind::objs
434 with _ -> assert false)
438 let ground_instances status gl =
439 let _,_,metasenv,subst,_ = status#obj in
440 let subset = menv_closure status gl in
441 let submenv = List.filter (fun (x,_) -> IntSet.mem x subset) metasenv in
443 let submenv = metasenv in
445 let subst, objs = close_metasenv status submenv subst in
449 let (_, ctx, t, _) = List.assoc i subst in
450 noprint (lazy (status#ppterm ctx [] [] t));
452 (fun (uri,_,_,_,_) as obj ->
453 NCicEnvironment.invalidate_item status (`Obj (uri, obj)))
458 Not_found -> assert false
462 let replace_meta status i args target =
463 let rec aux k = function
464 (* TODO: local context *)
465 | NCic.Meta (j,lc) when i = j ->
469 List.map (NCicSubstitution.subst_meta status lc) args in
470 NCic.Appl(NCic.Rel k::args))
471 | NCic.Meta (j,lc) as m ->
478 aux k (NCicSubstitution.lift status n t)) l))))
479 | t -> NCicUtils.map status (fun _ k -> k+1) k aux t
484 let close_wrt_metasenv status subst =
486 (fun ty (i,(iattr,ctx,mty)) ->
487 let mty = NCicUntrusted.apply_subst status subst ctx mty in
489 NCicUntrusted.apply_subst_context status ~fix_projections:true
491 let cty = close_wrt_context status mty ctx in
492 let name = "foo"^(string_of_int i) in
493 let ty = NCicSubstitution.lift status 1 ty in
494 let args = args_for_context ~k:1 ctx in
495 (* prerr_endline (status#ppterm ctx [] [] iterm); *)
496 let ty = replace_meta status i args ty
498 NCic.Prod(name,cty,ty))
502 let _,_,metasenv,subst,_ = status#obj in
503 let subset = menv_closure status [g] in
504 let subset = IntSet.remove g subset in
505 let elems = IntSet.elements subset in
506 let _, ctx, ty = NCicUtils.lookup_meta g metasenv in
507 let ty = NCicUntrusted.apply_subst status subst ctx ty in
508 noprint (lazy ("metas in " ^ (status#ppterm ctx [] metasenv ty)));
509 noprint (lazy (String.concat ", " (List.map string_of_int elems)));
510 let submenv = List.filter (fun (x,_) -> IntSet.mem x subset) metasenv in
511 let submenv = List.rev (NCicUntrusted.sort_metasenv status subst submenv) in
513 let submenv = metasenv in
515 let ty = close_wrt_metasenv status subst ty submenv in
516 noprint (lazy (status#ppterm ctx [] [] ty));
520 (****************** smart application ********************)
522 let saturate_to_ref status metasenv subst ctx nref ty =
523 let height = height_of_ref status nref in
524 let rec aux metasenv ty args =
525 let ty,metasenv,moreargs =
526 NCicMetaSubst.saturate status ~delta:height metasenv subst ctx ty 0 in
528 | NCic.Const(NReference.Ref (_,NReference.Def _) as nre)
530 let _, _, bo, _, _, _ = NCicEnvironment.get_checked_def status nre in
531 aux metasenv bo (args@moreargs)
532 | NCic.Appl(NCic.Const(NReference.Ref (_,NReference.Def _) as nre)::tl)
534 let _, _, bo, _, _, _ = NCicEnvironment.get_checked_def status nre in
535 aux metasenv (NCic.Appl(bo::tl)) (args@moreargs)
536 | _ -> ty,metasenv,(args@moreargs)
540 let smart_apply t unit_eq status g =
541 let n,h,metasenv,subst,o = status#obj in
542 let gname, ctx, gty = List.assoc g metasenv in
543 (* let ggty = mk_cic_term context gty in *)
544 let status, t = disambiguate status ctx t None in
545 let status,t = term_of_cic_term status t ctx in
546 let _,_,metasenv,subst,_ = status#obj in
547 let ty = NCicTypeChecker.typeof status subst metasenv ctx t in
548 let ty,metasenv,args =
551 | NCic.Appl(NCic.Const(nref)::_) ->
552 saturate_to_ref status metasenv subst ctx nref ty
554 NCicMetaSubst.saturate status metasenv subst ctx ty 0 in
555 let metasenv,j,inst,_ = NCicMetaSubst.mk_meta metasenv ctx `IsTerm in
556 let status = status#set_obj (n,h,metasenv,subst,o) in
557 let pterm = if args=[] then t else
559 | NCic.Appl l -> NCic.Appl(l@args)
560 | _ -> NCic.Appl(t::args)
562 noprint(lazy("pterm " ^ (status#ppterm ctx [] [] pterm)));
563 noprint(lazy("pty " ^ (status#ppterm ctx [] [] ty)));
566 NUri.uri_of_string "cic:/matita/basics/logic/eq_coerc.con" in
567 let ref = NReference.reference_of_spec uri (NReference.Def(2)) in
571 NCic.Appl[eq_coerc;ty;NCic.Implicit `Type;pterm;inst] in
572 let smart = mk_cic_term ctx smart in
574 let status = instantiate status g smart in
575 let _,_,metasenv,subst,_ = status#obj in
576 let _,ctx,jty = List.assoc j metasenv in
577 let jty = NCicUntrusted.apply_subst status subst ctx jty in
578 noprint(lazy("goal " ^ (status#ppterm ctx [] [] jty)));
579 fast_eq_check unit_eq status j
581 | NCicEnvironment.ObjectNotFound s as e ->
582 raise (Error (lazy "eq_coerc non yet defined",Some e))
583 | Error _ as e -> debug_print (lazy "error"); raise e
585 let compare_statuses ~past ~present =
586 let _,_,past,_,_ = past#obj in
587 let _,_,present,_,_ = present#obj in
588 List.map fst (List.filter (fun (i,_) -> not(List.mem_assoc i past)) present),
589 List.map fst (List.filter (fun (i,_) -> not (List.mem_assoc i present)) past)
592 (* paramodulation has only an implicit knoweledge of the symmetry of equality;
593 hence it is in trouble in proving (a = b) = (b = a) *)
594 let try_sym tac status g =
595 (* put the right uri *)
596 let sym_eq = Ast.Appl [Ast.Ident("sym_eq",`Ambiguous); Ast.Implicit `Vector] in
597 let _,_,metasenv,subst,_ = status#obj in
598 let _, context, gty = List.assoc g metasenv in
600 NCicParamod.is_equation status metasenv subst context gty
605 let new_status = instantiate_with_ast status g ("",0,sym_eq) in
606 let go, _ = compare_statuses ~past:status ~present:new_status in
607 assert (List.length go = 1);
608 let ng = List.hd go in
613 let smart_apply_tac t s =
614 let unit_eq = index_local_equations s#eq_cache s in
615 NTactics.distribute_tac (try_sym (smart_apply t unit_eq)) s
616 (* NTactics.distribute_tac (smart_apply t unit_eq) s *)
618 let smart_apply_auto t eq_cache =
619 NTactics.distribute_tac (try_sym (smart_apply t eq_cache))
620 (* NTactics.distribute_tac (smart_apply t eq_cache) *)
623 (****************** types **************)
626 type th_cache = (NCic.context * InvRelDiscriminationTree.t) list
628 (* cartesian: term set list -> term list set *)
631 [] -> NDiscriminationTree.TermListSet.empty
633 NDiscriminationTree.TermSet.fold
634 (fun x acc -> NDiscriminationTree.TermListSet.add [x] acc) l NDiscriminationTree.TermListSet.empty
636 let rest = cartesian tl in
637 NDiscriminationTree.TermSet.fold
639 NDiscriminationTree.TermListSet.fold (fun l acc' -> NDiscriminationTree.TermListSet.add (x::l) acc') rest acc
640 ) he NDiscriminationTree.TermListSet.empty
643 (* all_keys_of_cic_type: term -> term set *)
644 let all_keys_of_cic_type status metasenv subst context ty =
646 (* Here we are dropping the metasenv, but this should not raise any
647 exception (hopefully...) *)
649 NCicMetaSubst.saturate status ~delta:max_int metasenv subst context ty 0
655 NCic.Appl (he::tl) ->
658 let wty = NCicReduction.whd status ~delta:0 ~subst context ty in
660 NDiscriminationTree.TermSet.add ty (aux ty)
662 NDiscriminationTree.TermSet.union
663 (NDiscriminationTree.TermSet.add ty (aux ty))
664 (NDiscriminationTree.TermSet.add wty (aux wty))
667 NDiscriminationTree.TermListSet.fold
668 (fun l acc -> NDiscriminationTree.TermSet.add (NCic.Appl l) acc)
669 (cartesian ((NDiscriminationTree.TermSet.singleton he)::tl'))
670 NDiscriminationTree.TermSet.empty
671 | _ -> NDiscriminationTree.TermSet.empty
673 let ty,ity = saturate ty in
674 let wty,iwty = saturate (NCicReduction.whd status ~delta:0 ~subst context ty) in
676 [ity, NDiscriminationTree.TermSet.add ty (aux ty)]
678 [ity, NDiscriminationTree.TermSet.add ty (aux ty) ;
679 iwty, NDiscriminationTree.TermSet.add wty (aux wty) ]
682 let all_keys_of_type status t =
683 let _,_,metasenv,subst,_ = status#obj in
684 let context = ctx_of t in
685 let status, t = apply_subst status context t in
687 all_keys_of_cic_type status metasenv subst context
688 (snd (term_of_cic_term status t context))
692 (fun (intros,keys) ->
694 NDiscriminationTree.TermSet.fold
695 (fun t acc -> Ncic_termSet.add (mk_cic_term context t) acc)
696 keys Ncic_termSet.empty
701 let keys_of_type status orig_ty =
702 (* Here we are dropping the metasenv (in the status), but this should not
703 raise any exception (hopefully...) *)
704 let _, ty, _ = saturate ~delta:max_int status orig_ty in
705 let _, ty = apply_subst status (ctx_of ty) ty in
708 let orig_ty' = NCicTacReduction.normalize ~subst context orig_ty in
709 if orig_ty' <> orig_ty then
710 let ty',_,_= NCicMetaSubst.saturate ~delta:0 metasenv subst context orig_ty' 0 in
716 (*CSC: strange: we keep ty, ty normalized and ty ~delta:(h-1) *)
718 let _, ty = term_of_cic_term status ty (ctx_of ty) in
720 | NCic.Const (NReference.Ref (_,(NReference.Def h | NReference.Fix (_,_,h))))
721 | NCic.Appl (NCic.Const(NReference.Ref(_,(NReference.Def h | NReference.Fix (_,_,h))))::_)
723 let _,ty,_= saturate status ~delta:(h-1) orig_ty in
730 let all_keys_of_term status t =
731 let status, orig_ty = typeof status (ctx_of t) t in
732 all_keys_of_type status orig_ty
735 let keys_of_term status t =
736 let status, orig_ty = typeof status (ctx_of t) t in
737 keys_of_type status orig_ty
740 let mk_th_cache status gl =
742 (fun (status, acc) g ->
743 let gty = get_goalty status g in
744 let ctx = ctx_of gty in
745 noprint(lazy("th cache for: "^ppterm status gty));
746 noprint(lazy("th cache in: "^ppcontext status ctx));
747 if List.mem_assq ctx acc then status, acc else
748 let idx = InvRelDiscriminationTree.empty in
751 (fun (status, i, idx) _ ->
752 let t = mk_cic_term ctx (NCic.Rel i) in
753 let status, keys = keys_of_term status t in
754 noprint(lazy("indexing: "^ppterm status t ^ ": " ^ string_of_int (List.length keys)));
756 List.fold_left (fun idx k ->
757 InvRelDiscriminationTree.index idx k t) idx keys
762 status, (ctx, idx) :: acc)
766 let all_elements ctx cache =
767 let dummy = mk_cic_term ctx (NCic.Meta (0,(0, (NCic.Irl 0)))) in
769 let idx = List.assq ctx cache in
770 Ncic_termSet.elements
771 (InvRelDiscriminationTree.retrieve_unifiables idx dummy)
774 let add_to_th t c ty =
775 let key_c = ctx_of t in
776 if not (List.mem_assq key_c c) then
777 (key_c ,InvRelDiscriminationTree.index
778 InvRelDiscriminationTree.empty ty t ) :: c
780 let rec replace = function
782 | (x, idx) :: tl when x == key_c ->
783 (x, InvRelDiscriminationTree.index idx ty t) :: tl
784 | x :: tl -> x :: replace tl
789 let rm_from_th t c ty =
790 let key_c = ctx_of t in
791 if not (List.mem_assq key_c c) then assert false
793 let rec replace = function
795 | (x, idx) :: tl when x == key_c ->
796 (x, InvRelDiscriminationTree.remove_index idx ty t) :: tl
797 | x :: tl -> x :: replace tl
802 let pp_idx status idx =
803 InvRelDiscriminationTree.iter idx
805 noprint(lazy("K: " ^ NCicInverseRelIndexable.string_of_path k));
807 (fun t -> debug_print(lazy("\t"^ppterm status t)))
811 let pp_th (status: #NTacStatus.pstatus) =
814 noprint(lazy( "-----------------------------------------------"));
815 noprint(lazy( (status#ppcontext ~metasenv:[] ~subst:[] ctx)));
816 noprint(lazy( "||====> "));
820 let search_in_th gty th =
821 let c = ctx_of gty in
822 let rec aux acc = function
823 | [] -> (* Ncic_termSet.elements *) acc
826 let idx = List.assoc(*q*) k th in
827 let acc = Ncic_termSet.union acc
828 (InvRelDiscriminationTree.retrieve_unifiables idx gty)
831 with Not_found -> aux acc tl
833 aux Ncic_termSet.empty c
837 do_types : bool; (* solve goals in Type *)
838 last : bool; (* last goal: take first solution only *)
839 candidates: Ast.term list option;
847 {facts : th_cache; (* positive results *)
848 under_inspection : cic_term list * th_cache; (* to prune looping *)
849 failures : th_cache; (* to avoid repetitions *)
850 unit_eq : NCicParamod.state;
854 let add_to_trace status ~depth cache t =
857 debug_print ~depth (lazy ("Adding to trace: " ^ NotationPp.pp_term status t));
858 {cache with trace = t::cache.trace}
859 | Ast.NCic _ (* local candidate *)
860 | _ -> (*not an application *) cache
862 let pptrace status tr =
863 (lazy ("Proof Trace: " ^ (String.concat ";"
864 (List.map (NotationPp.pp_term status) tr))))
866 let remove_from_trace cache t =
869 (match cache.trace with
870 | _::tl -> {cache with trace = tl}
872 | Ast.NCic _ (* local candidate *)
873 | _ -> (*not an application *) cache *)
876 type goal = int * sort (* goal, depth, sort *)
877 type fail = goal * cic_term
878 type candidate = int * Ast.term (* unique candidate number, candidate *)
880 exception Gaveup of th_cache (* failure cache *)
881 exception Proved of NTacStatus.tac_status * Ast.term list
883 (* let close_failures _ c = c;; *)
884 (* let prunable _ _ _ = false;; *)
885 (* let cache_examine cache gty = `Notfound;; *)
886 (* let put_in_subst s _ _ _ = s;; *)
887 (* let add_to_cache_and_del_from_orlist_if_green_cut _ _ c _ _ o f _ = c, o, f, false ;; *)
888 (* let cache_add_underinspection c _ _ = c;; *)
890 let init_cache ?(facts=[]) ?(under_inspection=[],[])
892 ?(unit_eq=NCicParamod.empty_state)
897 under_inspection = under_inspection;
901 let only signature _context candidate = true
903 (* TASSI: nel trie ci mettiamo solo il body, non il ty *)
905 NCicTypeChecker.typeof ~subst:[] ~metasenv:[] [] candidate
907 let height = fast_height_of_term status candidate_ty in
908 let rc = signature >= height in
910 noprint (lazy ("Filtro: " ^ status#ppterm ~context:[] ~subst:[]
911 ~metasenv:[] candidate ^ ": " ^ string_of_int height))
913 noprint (lazy ("Tengo: " ^ status#ppterm ~context:[] ~subst:[]
914 ~metasenv:[] candidate ^ ": " ^ string_of_int height));
919 let candidate_no = ref 0;;
921 let openg_no status = List.length (head_goals status#stack)
923 let sort_candidates status ctx candidates =
924 let _,_,metasenv,subst,_ = status#obj in
926 let status,ct = disambiguate status ctx ("",0,cand) None in
927 let status,t = term_of_cic_term status ct ctx in
928 let ty = NCicTypeChecker.typeof status subst metasenv ctx t in
929 let res = branch status (mk_cic_term ctx ty) in
930 noprint (lazy ("branch factor for: " ^ (ppterm status ct) ^ " = "
931 ^ (string_of_int res)));
934 let candidates = List.map (fun t -> branch t,t) candidates in
936 List.sort (fun (a,_) (b,_) -> a - b) candidates in
937 let candidates = List.map snd candidates in
938 noprint (lazy ("candidates =\n" ^ (String.concat "\n"
939 (List.map (NotationPp.pp_term status) candidates))));
942 let sort_new_elems l =
943 List.sort (fun (_,s1) (_,s2) -> openg_no s1 - openg_no s2) l
945 let rec stack_goals level gs =
950 let is_open = function
951 | (_,Continuationals.Stack.Open i) -> Some i
952 | (_,Continuationals.Stack.Closed _) -> None
954 HExtlib.filter_map is_open g @ stack_goals (level-1) s
957 let open_goals level status = stack_goals level status#stack
960 let try_candidate ?(smart=0) flags depth status eq_cache ctx t =
962 let old_og_no = List.length (open_goals (depth+1) status) in
963 debug_print ~depth (lazy ("try " ^ (NotationPp.pp_term status) t));
965 if smart= 0 then NTactics.apply_tac ("",0,t) status
966 else if smart = 1 then smart_apply_auto ("",0,t) eq_cache status
967 else (* smart = 2: both *)
968 try NTactics.apply_tac ("",0,t) status
970 smart_apply_auto ("",0,t) eq_cache status
972 (* we compare the expected branching with the actual one and
973 prune the candidate when the latter is larger. The optimization
974 is meant to rule out stange applications of flexible terms,
975 such as the application of eq_f that always succeeds.
976 There is some gain but less than expected *)
977 let og_no = List.length (open_goals (depth+1) status) in
978 let status, cict = disambiguate status ctx ("",0,t) None in
979 let status,ct = term_of_cic_term status cict ctx in
980 let _,_,metasenv,subst,_ = status#obj in
981 let ty = NCicTypeChecker.typeof status subst metasenv ctx ct in
982 let res = branch status (mk_cic_term ctx ty) in
983 let diff = og_no - old_og_no in
984 debug_print (lazy ("expected branching: " ^ (string_of_int res)));
985 debug_print (lazy ("actual: branching" ^ (string_of_int diff)));
986 (* one goal is closed by the application *)
987 if og_no - old_og_no >= res then
988 (debug_print (lazy ("branch factor for: " ^ (ppterm status cict) ^ " = "
989 ^ (string_of_int res) ^ " vs. " ^ (string_of_int og_no)));
990 debug_print ~depth (lazy "strange application"); None)
992 (incr candidate_no; Some ((!candidate_no,t),status))
993 with Error (msg,exn) -> debug_print ~depth (lazy "failed"); None
996 let sort_of status subst metasenv ctx t =
997 let ty = NCicTypeChecker.typeof status subst metasenv ctx t in
998 let metasenv',ty = NCicUnification.fix_sorts status metasenv subst ty in
999 assert (metasenv = metasenv');
1000 NCicTypeChecker.typeof status subst metasenv ctx ty
1003 let type0= NUri.uri_of_string ("cic:/matita/pts/Type0.univ")
1006 let perforate_small status subst metasenv context t =
1007 let rec aux = function
1008 | NCic.Appl (hd::tl) ->
1010 let s = sort_of status subst metasenv context t in
1012 | NCic.Sort(NCic.Type [`Type,u])
1013 when u=type0 -> NCic.Meta (0,(0,NCic.Irl 0))
1016 NCic.Appl (hd::List.map map tl)
1022 let get_cands retrieve_for diff empty gty weak_gty =
1023 let cands = retrieve_for gty in
1025 | None -> cands, empty
1027 let more_cands = retrieve_for weak_gty in
1028 cands, diff more_cands cands
1031 let get_candidates ?(smart=true) depth flags status cache signature gty =
1032 let maxd = ((depth + 1) = flags.maxdepth) in
1033 let universe = status#auto_cache in
1034 let _,_,metasenv,subst,_ = status#obj in
1035 let context = ctx_of gty in
1036 let _, raw_gty = term_of_cic_term status gty context in
1037 debug_print ~depth (lazy ("gty:" ^ NTacStatus.ppterm status gty));
1038 let raw_weak_gty, weak_gty =
1045 perforate_small status subst metasenv context raw_gty in
1046 let weak = mk_cic_term context raw_weak in
1047 debug_print ~depth (lazy ("weak_gty:" ^ NTacStatus.ppterm status weak));
1048 Some raw_weak, Some (weak)
1052 let global_cands, smart_global_cands =
1053 match flags.candidates with
1054 | Some l when (not maxd) -> l,[]
1058 let to_ast = function
1059 | NCic.Const r when true (*is_relevant statistics r*) -> Some (Ast.NRef r)
1060 (* | NCic.Const _ -> None *)
1061 | _ -> assert false in
1063 to_ast (NDiscriminationTree.TermSet.elements s) in
1066 (NDiscriminationTree.DiscriminationTree.retrieve_unifiables
1068 NDiscriminationTree.TermSet.diff
1069 NDiscriminationTree.TermSet.empty
1070 raw_gty raw_weak_gty in
1072 let local_cands,smart_local_cands =
1075 let _status, t = term_of_cic_term status t context
1077 List.map to_ast (Ncic_termSet.elements s) in
1080 (fun ty -> search_in_th ty cache)
1081 Ncic_termSet.diff Ncic_termSet.empty gty weak_gty in
1083 sort_candidates status context (global_cands@local_cands),
1084 sort_candidates status context (smart_global_cands@smart_local_cands)
1088 let get_candidates ?(smart=true) status cache signature gty =
1089 let universe = status#auto_cache in
1090 let _,_,metasenv,subst,_ = status#obj in
1091 let context = ctx_of gty in
1093 let _status, t = term_of_cic_term status t context
1095 let c_ast = function
1096 | NCic.Const r -> Ast.NRef r | _ -> assert false in
1097 let _, raw_gty = term_of_cic_term status gty context in
1098 let keys = all_keys_of_cic_term metasenv subst context raw_gty in
1099 (* we only keep those keys that do not require any intros for now *)
1100 let no_intros_keys = snd (List.hd keys) in
1102 NDiscriminationTree.TermSet.fold
1104 NDiscriminationTree.TermSet.union acc
1105 (NDiscriminationTree.DiscriminationTree.retrieve_unifiables
1107 ) no_intros_keys NDiscriminationTree.TermSet.empty in
1109 let cands = NDiscriminationTree.DiscriminationTree.retrieve_unifiables
1113 NDiscriminationTree.TermSet.fold
1115 Ncic_termSet.union acc (search_in_th (mk_cic_term context ty) cache)
1116 ) no_intros_keys Ncic_termSet.empty in
1118 let local_cands = search_in_th gty cache in
1120 debug_print (lazy ("candidates for" ^ NTacStatus.ppterm status gty));
1121 debug_print (lazy ("local cands = " ^ (string_of_int (List.length (Ncic_termSet.elements local_cands)))));
1122 let together global local =
1124 (List.filter (only signature context)
1125 (NDiscriminationTree.TermSet.elements global)) @
1126 List.map t_ast (Ncic_termSet.elements local) in
1127 let candidates = together cands local_cands in
1128 let candidates = sort_candidates status context candidates in
1129 let smart_candidates =
1135 let weak_gty = perforate_small status subst metasenv context raw_gty in
1137 NCic.Appl (hd:: HExtlib.mk_list(NCic.Meta (0,(0,NCic.Irl 0)))
1138 (List.length tl)) in *)
1140 NDiscriminationTree.DiscriminationTree.retrieve_unifiables
1144 NDiscriminationTree.TermSet.diff more_cands cands in
1145 let cic_weak_gty = mk_cic_term context weak_gty in
1146 let more_local_cands = search_in_th cic_weak_gty cache in
1147 let smart_local_cands =
1148 Ncic_termSet.diff more_local_cands local_cands in
1149 together smart_cands smart_local_cands
1150 (* together more_cands more_local_cands *)
1154 let smart_candidates = sort_candidates status context smart_candidates in
1155 (* if smart then smart_candidates, []
1156 else candidates, [] *)
1157 candidates, smart_candidates
1160 let get_candidates ?(smart=true) flags status cache signature gty =
1161 match flags.candidates with
1162 | None -> get_candidates ~smart status cache signature gty
1166 let applicative_case depth signature status flags gty cache =
1167 app_counter:= !app_counter+1;
1168 let _,_,metasenv,subst,_ = status#obj in
1169 let context = ctx_of gty in
1170 let tcache = cache.facts in
1171 let is_prod, is_eq =
1172 let status, t = term_of_cic_term status gty context in
1173 let t = NCicReduction.whd status subst context t in
1175 | NCic.Prod _ -> true, false
1176 | _ -> false, NCicParamod.is_equation status metasenv subst context t
1178 debug_print ~depth (lazy (string_of_bool is_eq));
1180 let candidates, smart_candidates =
1181 get_candidates ~smart:true depth
1182 flags status tcache signature gty in
1183 let test = is_a_fact_ast status subst metasenv context in
1184 let candidates_facts,candidates_other =
1185 (* if the goal is an equation we avoid to apply unit equalities,
1186 since superposition should take care of them; refl is an
1187 exception since it prompts for convertibility *)
1188 let l1,l2 = List.partition test candidates in
1189 (* put the right uri *)
1190 if is_eq then [Ast.Ident("refl",`Ambiguous)],l2 else l1,l2
1192 let smart_candidates_facts, smart_candidates_other =
1193 let l1,l2 = List.partition test smart_candidates in
1194 if is_eq then [],l2 else l1,l2
1196 let sm = if is_eq then 0 else 2 in
1197 let sm1 = if flags.last then 2 else 0 in
1198 let maxd = (depth + 1 = flags.maxdepth) in
1199 let try_candidates only_one sm acc candidates =
1202 if (only_one && (elems <> [])) then elems
1204 match try_candidate (~smart:sm)
1205 flags depth status cache.unit_eq context cand with
1207 | Some x -> x::elems)
1210 (* if the goal is the last one we stop at the first fact *)
1211 let elems = try_candidates flags.last sm [] candidates_facts in
1212 (* now we add smart_facts *)
1213 let elems = try_candidates flags.last sm elems smart_candidates_facts in
1214 (* if we are at maxdepth and the goal is not a product we are done
1215 similarly, if the goal is the last one and we already found a
1217 if (maxd && not(is_prod)) || (flags.last && elems<>[]) then elems
1219 let elems = try_candidates false 2 elems candidates_other in
1220 debug_print ~depth (lazy ("not facts: try smart application"));
1221 try_candidates false 2 elems smart_candidates_other
1228 (* gty is supposed to be meta-closed *)
1229 let is_subsumed depth filter_depth status gty cache =
1230 if cache=[] then false else (
1231 debug_print ~depth (lazy("Subsuming " ^ (ppterm status gty)));
1232 let n,h,metasenv,subst,obj = status#obj in
1233 let ctx = ctx_of gty in
1234 let _ , raw_gty = term_of_cic_term status gty ctx in
1235 let target = NCicSubstitution.lift status 1 raw_gty in
1236 (* we compute candidates using the perforated type *)
1243 perforate_small status subst metasenv ctx raw_gty in
1244 let weak = mk_cic_term ctx raw_weak in
1245 debug_print ~depth (lazy ("weak_gty:" ^ NTacStatus.ppterm status weak));
1249 (* candidates must only be searched w.r.t the given context *)
1252 let idx = List.assq ctx cache in
1255 Ncic_termSet.elements
1256 (InvRelDiscriminationTree.retrieve_unifiables idx weak)
1258 with Not_found -> []
1260 (* this is a dirty trick: the first argument of an application is used
1261 to remember at which depth a goal failed *)
1263 let ctx = ctx_of t in
1264 let _, src = term_of_cic_term status t ctx in
1266 | NCic.Appl [NCic.Implicit (`Typeof d); t]
1267 when d <= depth -> Some (mk_cic_term ctx t)
1270 if filter_depth then HExtlib.filter_map filter candidates else candidates in
1272 (lazy ("failure candidates: " ^ string_of_int (List.length candidates)));
1276 let _ , source = term_of_cic_term status t ctx in
1278 NCic.Prod("foo",source,target) in
1279 let metasenv,j,_,_ =
1280 NCicMetaSubst.mk_meta
1281 metasenv ctx ~with_type:implication `IsType in
1282 let status = status#set_obj (n,h,metasenv,subst,obj) in
1283 let status = status#set_stack [([1,Open j],[],[],`NoTag)] in
1285 let status = NTactics.intro_tac "foo" status in
1287 NTactics.apply_tac ("",0,Ast.NCic (NCic.Rel 1)) status
1289 if (head_goals status#stack = []) then raise Found
1294 with Found -> debug_print ~depth (lazy "success");true)
1297 let rec guess_name name ctx =
1298 if name = "_" then guess_name "auto" ctx else
1299 if not (List.mem_assoc name ctx) then name else
1300 guess_name (name^"'") ctx
1303 let is_prod status =
1304 let _, ctx, gty = current_goal status in
1305 let status, gty = apply_subst status ctx gty in
1306 let _, raw_gty = term_of_cic_term status gty ctx in
1308 | NCic.Prod (name,src,_) ->
1309 let status, src = whd status ~delta:0 ctx (mk_cic_term ctx src) in
1310 (match snd (term_of_cic_term status src ctx) with
1311 | NCic.Const(NReference.Ref (_,NReference.Ind _) as r)
1312 | NCic.Appl (NCic.Const(NReference.Ref (_,NReference.Ind _) as r)::_) ->
1313 let _,_,itys,_,_ = NCicEnvironment.get_checked_indtys status r in
1315 (* | [_,_,_,[_;_]] con nat va, ovviamente, in loop *)
1317 | [_,_,_,[]] -> `Inductive (guess_name name ctx)
1318 | _ -> `Some (guess_name name ctx))
1319 | _ -> `Some (guess_name name ctx))
1322 let intro ~depth status facts name =
1323 let status = NTactics.intro_tac name status in
1324 let _, ctx, ngty = current_goal status in
1325 let t = mk_cic_term ctx (NCic.Rel 1) in
1326 let status, keys = keys_of_term status t in
1327 let facts = List.fold_left (add_to_th t) facts keys in
1328 debug_print ~depth (lazy ("intro: "^ name));
1329 (* unprovability is not stable w.r.t introduction *)
1333 let rec intros_facts ~depth status facts =
1334 if List.length (head_goals status#stack) <> 1 then status, facts else
1335 match is_prod status with
1339 intro ~depth status facts name
1340 in intros_facts ~depth status facts
1341 (* | `Inductive name ->
1342 let status = NTactics.case1_tac name status in
1343 intros_facts ~depth status facts *)
1344 | _ -> status, facts
1347 let intros ~depth status cache =
1348 match is_prod status with
1351 let trace = cache.trace in
1353 intros_facts ~depth status cache.facts
1355 if head_goals status#stack = [] then
1356 let status = NTactics.merge_tac status in
1357 [(0,Ast.Ident("__intros",`Ambiguous)),status], cache
1359 (* we reindex the equation from scratch *)
1360 let unit_eq = index_local_equations status#eq_cache status in
1361 let status = NTactics.merge_tac status in
1362 [(0,Ast.Ident("__intros",`Ambiguous)),status],
1363 init_cache ~facts ~unit_eq () ~trace
1367 let reduce ~whd ~depth status g =
1368 let n,h,metasenv,subst,o = status#obj in
1369 let attr, ctx, ty = NCicUtils.lookup_meta g metasenv in
1370 let ty = NCicUntrusted.apply_subst status subst ctx ty in
1372 (if whd then NCicReduction.whd else NCicTacReduction.normalize) status ~subst ctx ty
1377 (lazy ("reduced to: "^ status#ppterm ctx subst metasenv ty'));
1379 (g,(attr,ctx,ty'))::(List.filter (fun (i,_) -> i<>g) metasenv)
1381 let status = status#set_obj (n,h,metasenv,subst,o) in
1382 (* we merge to gain a depth level; the previous goal level should
1384 let status = NTactics.merge_tac status in
1386 [(!candidate_no,Ast.Ident("__whd",`Ambiguous)),status])
1389 let do_something signature flags status g depth gty cache =
1390 let l0, cache = intros ~depth status cache in
1391 if l0 <> [] then l0, cache
1394 let l = reduce ~whd:true ~depth status g in
1395 (* if l <> [] then l,cache else *)
1396 (* backward aplications *)
1401 ((!candidate_no,Ast.Ident("__paramod",`Ambiguous)),s))
1402 (auto_eq_check cache.unit_eq status)
1405 if ((l1 <> []) && flags.last) then [] else
1406 applicative_case depth signature status flags gty cache
1410 (fun ((_,t),_) -> toref incr_nominations statistics t) l2;
1411 (* states in l1 have have an empty set of subgoals: no point to sort them *)
1413 (lazy ("alternatives = " ^ (string_of_int (List.length (l1@l@l2)))));
1414 (* we order alternatives w.r.t the number of subgoals they open *)
1415 l1 @ (sort_new_elems l2) @ l, cache
1418 let pp_goal = function
1419 | (_,Continuationals.Stack.Open i)
1420 | (_,Continuationals.Stack.Closed i) -> string_of_int i
1423 let pp_goals status l =
1427 let gty = get_goalty status i in
1428 NTacStatus.ppterm status gty)
1435 let compare = Pervasives.compare
1439 module MS = HTopoSort.Make(M)
1442 let sort_tac status =
1444 match status#stack with
1445 | [] -> assert false
1446 | (goals, t, k, tag) :: s ->
1447 let g = head_goals status#stack in
1449 (List.rev (MS.topological_sort g (deps status))) in
1450 noprint (lazy ("old g = " ^
1451 String.concat "," (List.map string_of_int g)));
1452 noprint (lazy ("sorted goals = " ^
1453 String.concat "," (List.map string_of_int sortedg)));
1454 let is_it i = function
1455 | (_,Continuationals.Stack.Open j )
1456 | (_,Continuationals.Stack.Closed j ) -> i = j
1459 List.map (fun i -> List.find (is_it i) goals) sortedg
1461 (sorted_goals, t, k, tag) :: s
1463 status#set_stack gstatus
1466 let clean_up_tac status =
1468 match status#stack with
1469 | [] -> assert false
1470 | (g, t, k, tag) :: s ->
1471 let is_open = function
1472 | (_,Continuationals.Stack.Open _) -> true
1473 | (_,Continuationals.Stack.Closed _) -> false
1475 let g' = List.filter is_open g in
1476 (g', t, k, tag) :: s
1478 status#set_stack gstatus
1481 let focus_tac focus status =
1483 match status#stack with
1484 | [] -> assert false
1485 | (g, t, k, tag) :: s ->
1486 let in_focus = function
1487 | (_,Continuationals.Stack.Open i)
1488 | (_,Continuationals.Stack.Closed i) -> List.mem i focus
1490 let focus,others = List.partition in_focus g
1492 (* we need to mark it as a BranchTag, otherwise cannot merge later *)
1493 (focus,[],[],`BranchTag) :: (others, t, k, tag) :: s
1495 status#set_stack gstatus
1498 let deep_focus_tac level focus status =
1499 let in_focus = function
1500 | (_,Continuationals.Stack.Open i)
1501 | (_,Continuationals.Stack.Closed i) -> List.mem i focus
1503 let rec slice level gs =
1504 if level = 0 then [],[],gs else
1506 | [] -> assert false
1507 | (g, t, k, tag) :: s ->
1508 let f,o,gs = slice (level-1) s in
1509 let f1,o1 = List.partition in_focus g
1511 (f1,[],[],`BranchTag)::f, (o1, t, k, tag)::o, gs
1514 let f,o,s = slice level status#stack in f@o@s
1516 status#set_stack gstatus
1519 let move_to_side level status =
1520 match status#stack with
1521 | [] -> assert false
1523 let is_open = function
1524 | (_,Continuationals.Stack.Open i) -> Some i
1525 | (_,Continuationals.Stack.Closed _) -> None
1527 let others = menv_closure status (stack_goals (level-1) tl) in
1528 List.for_all (fun i -> IntSet.mem i others)
1529 (HExtlib.filter_map is_open g)
1531 let top_cache ~depth top status cache =
1533 let unit_eq = index_local_equations status#eq_cache status in
1534 {cache with unit_eq = unit_eq}
1537 let rec auto_clusters ?(top=false)
1538 flags signature cache depth status : unit =
1539 debug_print ~depth (lazy ("entering auto clusters at depth " ^
1540 (string_of_int depth)));
1541 debug_print ~depth (pptrace status cache.trace);
1542 (* ignore(Unix.select [] [] [] 0.01); *)
1543 let status = clean_up_tac status in
1544 let goals = head_goals status#stack in
1546 if depth = 0 then raise (Proved (status, cache.trace))
1548 let status = NTactics.merge_tac status in
1550 let l,tree = cache.under_inspection in
1552 | [] -> cache (* possible because of intros that cleans the cache *)
1553 | a::tl -> let tree = rm_from_th a tree a in
1554 {cache with under_inspection = tl,tree}
1556 auto_clusters flags signature cache (depth-1) status
1557 else if List.length goals < 2 then
1558 let cache = top_cache ~depth top status cache in
1559 auto_main flags signature cache depth status
1561 let all_goals = open_goals (depth+1) status in
1562 debug_print ~depth (lazy ("goals = " ^
1563 String.concat "," (List.map string_of_int all_goals)));
1564 let classes = HExtlib.clusters (deps status) all_goals in
1565 (* if any of the classes exceed maxwidth we fail *)
1568 if List.length gl > flags.maxwidth then
1570 debug_print ~depth (lazy "FAIL GLOBAL WIDTH");
1571 HLog.warn (sprintf "global width (%u) exceeded: %u"
1572 flags.maxwidth (List.length gl));
1573 raise (Gaveup cache.failures)
1574 end else ()) classes;
1575 if List.length classes = 1 then
1577 {flags with last = (List.length all_goals = 1)} in
1578 (* no need to cluster *)
1579 let cache = top_cache ~depth top status cache in
1580 auto_main flags signature cache depth status
1582 let classes = if top then List.rev classes else classes in
1588 ("cluster:" ^ String.concat "," (List.map string_of_int l)))
1590 (* we now process each cluster *)
1591 let status,cache,b =
1593 (fun (status,cache,b) gl ->
1595 {flags with last = (List.length gl = 1)} in
1596 let lold = List.length status#stack in
1597 debug_print ~depth (lazy ("stack length = " ^
1598 (string_of_int lold)));
1599 let fstatus = deep_focus_tac (depth+1) gl status in
1600 let cache = top_cache ~depth top fstatus cache in
1602 debug_print ~depth (lazy ("focusing on" ^
1603 String.concat "," (List.map string_of_int gl)));
1604 auto_main flags signature cache depth fstatus; assert false
1606 | Proved(status,trace) ->
1607 let status = NTactics.merge_tac status in
1608 let cache = {cache with trace = trace} in
1609 let lnew = List.length status#stack in
1610 assert (lold = lnew);
1612 | Gaveup failures when top ->
1613 let cache = {cache with failures = failures} in
1616 (status,cache,false) classes
1618 let rec final_merge n s =
1619 if n = 0 then s else final_merge (n-1) (NTactics.merge_tac s)
1620 in let status = final_merge depth status
1621 in if b then raise (Proved(status,cache.trace)) else raise (Gaveup cache.failures)
1625 (* BRAND NEW VERSION *)
1626 auto_main flags signature cache depth status: unit =
1627 debug_print ~depth (lazy "entering auto main");
1628 debug_print ~depth (pptrace status cache.trace);
1629 debug_print ~depth (lazy ("stack length = " ^
1630 (string_of_int (List.length status#stack))));
1631 (* ignore(Unix.select [] [] [] 0.01); *)
1632 let status = sort_tac (clean_up_tac status) in
1633 let goals = head_goals status#stack in
1635 | [] when depth = 0 -> raise (Proved (status,cache.trace))
1637 let status = NTactics.merge_tac status in
1639 let l,tree = cache.under_inspection in
1641 | [] -> cache (* possible because of intros that cleans the cache *)
1642 | a::tl -> let tree = rm_from_th a tree a in
1643 {cache with under_inspection = tl,tree}
1645 auto_clusters flags signature cache (depth-1) status
1647 if depth > 0 && move_to_side depth status
1649 let status = NTactics.merge_tac status in
1651 let l,tree = cache.under_inspection in
1653 | [] -> cache (* possible because of intros that cleans the cache*)
1654 | a::tl -> let tree = rm_from_th a tree a in
1655 {cache with under_inspection = tl,tree}
1657 auto_clusters flags signature cache (depth-1) status
1659 let ng = List.length goals in
1660 (* moved inside auto_clusters *)
1661 if ng > flags.maxwidth then begin
1662 debug_print ~depth (lazy "FAIL LOCAL WIDTH");
1663 HLog.warn (sprintf "local width (%u) exceeded: %u"
1665 raise (Gaveup cache.failures)
1666 end else if depth = flags.maxdepth then
1667 raise (Gaveup cache.failures)
1669 let status = NTactics.branch_tac ~force:true status in
1670 let g,gctx, gty = current_goal status in
1671 let ctx,ty = close status g in
1672 let closegty = mk_cic_term ctx ty in
1673 let status, gty = apply_subst status gctx gty in
1674 debug_print ~depth (lazy("Attacking goal " ^
1675 string_of_int g ^ " : "^ppterm status gty));
1676 debug_print ~depth (lazy ("current failures: " ^
1677 string_of_int (List.length (all_elements ctx cache.failures))));
1679 let _,_,metasenv,subst,_ = status#obj in
1680 NCicParamod.is_equation status metasenv subst ctx ty in
1681 (* if the goal is an equality we artificially raise its depth up to
1682 flags.maxdepth - 1 *)
1683 if (not flags.last && is_eq && (depth < (flags.maxdepth -1))) then
1684 (* for efficiency reasons, in this case we severely cripple the
1686 (debug_print ~depth (lazy ("RAISING DEPTH TO " ^ string_of_int (depth+1)));
1687 auto_main flags signature cache (depth+1) status)
1688 (* check for loops *)
1689 else if is_subsumed depth false status closegty (snd cache.under_inspection) then
1690 (debug_print ~depth (lazy "SUBSUMED");
1691 raise (Gaveup cache.failures))
1692 (* check for failures *)
1693 else if is_subsumed depth true status closegty cache.failures then
1694 (debug_print ~depth (lazy "ALREADY MET");
1695 raise (Gaveup cache.failures))
1697 let new_sig = height_of_goal g status in
1698 if new_sig < signature then
1699 (debug_print ~depth (lazy ("news = " ^ (string_of_int new_sig)));
1700 debug_print ~depth (lazy ("olds = " ^ (string_of_int signature))));
1701 let alternatives, cache =
1702 do_something signature flags status g depth gty cache in
1705 let l,tree = cache.under_inspection in
1706 let l,tree = closegty::l, add_to_th closegty tree closegty in
1707 {cache with under_inspection = l,tree}
1711 (fun allfailures ((_,t),status) ->
1713 (lazy ("(re)considering goal " ^
1714 (string_of_int g) ^" : "^ppterm status gty));
1715 debug_print (~depth:depth)
1716 (lazy ("Case: " ^ NotationPp.pp_term status t));
1718 if t=Ast.Ident("__whd",`Ambiguous) ||
1719 t=Ast.Ident("__intros",`Ambiguous)
1721 else depth+1,loop_cache in
1722 let cache = add_to_trace status ~depth cache t in
1723 let cache = {cache with failures = allfailures} in
1725 auto_clusters flags signature cache depth status;
1728 debug_print ~depth (lazy "Failed");
1730 cache.failures alternatives in
1734 let dty = NCic.Appl [NCic.Implicit (`Typeof depth); ty] in
1737 prerr_endline ("FAILURE : " ^ ppterm status gty);
1738 add_to_th newfail failures closegty
1740 debug_print ~depth (lazy "no more candidates");
1741 raise (Gaveup failures)
1744 let int name l def =
1745 try int_of_string (List.assoc name l)
1746 with Failure _ | Not_found -> def
1749 module AstSet = Set.Make(struct type t = Ast.term let compare = compare end)
1751 let cleanup_trace s trace =
1752 (* removing duplicates *)
1755 (fun acc t -> AstSet.add t acc)
1756 AstSet.empty trace in
1757 let trace = AstSet.elements trace_set
1758 (* filtering facts *)
1762 | Ast.NRef (NReference.Ref (u,_)) -> not (is_a_fact_obj s u)
1766 let auto_tac ~params:(univ,flags) ?(trace_ref=ref []) status =
1767 let oldstatus = status in
1768 let status = (status:> NTacStatus.tac_status) in
1769 let goals = head_goals status#stack in
1770 let status, facts = mk_th_cache status goals in
1771 (* let unit_eq = index_local_equations status#eq_cache status in *)
1772 let cache = init_cache ~facts () in
1773 (* pp_th status facts; *)
1775 NDiscriminationTree.DiscriminationTree.iter status#auto_cache (fun p t ->
1777 NDiscriminationTree.NCicIndexable.string_of_path p ^ " |--> " ^
1778 String.concat "\n " (List.map (
1779 status#ppterm ~metasenv:[] ~context:[] ~subst:[])
1780 (NDiscriminationTree.TermSet.elements t))
1788 let status, res = disambiguate status [] t None in
1789 let _,res = term_of_cic_term status res (ctx_of res)
1791 in Some (List.map to_Ast l)
1793 let depth = int "depth" flags 3 in
1794 let size = int "size" flags 10 in
1795 let width = int "width" flags 4 (* (3+List.length goals)*) in
1797 (* let goals = List.map (fun i -> (i,P)) goals in *)
1798 let signature = height_of_goals status in
1801 candidates = candidates;
1805 timeout = Unix.gettimeofday() +. 3000.;
1808 let initial_time = Unix.gettimeofday() in
1813 ("TIME ELAPSED:"^string_of_float(Unix.gettimeofday()-.initial_time)));
1815 ("Applicative nodes:"^string_of_int !app_counter));
1816 raise (Error (lazy "auto gave up", None)))
1818 let _ = debug_print (lazy("\n\nRound "^string_of_int x^"\n")) in
1819 let flags = { flags with maxdepth = x }
1821 try auto_clusters (~top:true) flags signature cache 0 status;assert false
1823 try auto_main flags signature cache 0 status;assert false
1826 | Gaveup _ -> up_to (x+1) y
1827 | Proved (s,trace) ->
1828 debug_print (lazy ("proved at depth " ^ string_of_int x));
1829 List.iter (toref incr_uses statistics) trace;
1830 let trace = cleanup_trace s trace in
1831 let _ = debug_print (pptrace status trace) in
1834 | (g,t,k,f) :: rest -> (filter_open g,t,k,f):: rest
1837 let s = s#set_stack stack in
1839 oldstatus#set_status s
1841 let s = up_to depth depth in
1842 debug_print (print_stat status statistics);
1844 ("TIME ELAPSED:"^string_of_float(Unix.gettimeofday()-.initial_time)));
1846 ("Applicative nodes:"^string_of_int !app_counter));
1850 let auto_tac ~params:(_,flags as params) ?trace_ref =
1851 if List.mem_assoc "demod" flags then
1853 else if List.mem_assoc "paramod" flags then
1855 else if List.mem_assoc "fast_paramod" flags then
1856 fast_eq_check_tac ~params
1857 else auto_tac ~params ?trace_ref