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
29 let equal = NReference.eq
30 let compare = NReference.compare
31 let hash = NReference.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 Filename.chop_extension
77 (Filename.basename (NReference.string_of_reference r))
80 short_name a ^ ": rel = " ^
81 (string_of_float (relevance v)) ^
82 "; uses = " ^ (string_of_int !(v.uses)) ^
83 "; nom = " ^ (string_of_int !(v.nominations)) in
84 lazy ("\n\nSTATISTICS:\n" ^
85 String.concat "\n" (List.map vstring l))
87 (* ======================= utility functions ========================= *)
88 module IntSet = Set.Make(struct type t = int let compare = compare end)
90 let get_sgoalty status g =
91 let _,_,metasenv,subst,_ = status#obj in
93 let _, ctx, ty = NCicUtils.lookup_meta g metasenv in
94 let ty = NCicUntrusted.apply_subst status subst ctx ty in
95 let ctx = NCicUntrusted.apply_subst_context status
96 ~fix_projections:true subst ctx
98 NTacStatus.mk_cic_term ctx ty
99 with NCicUtils.Meta_not_found _ as exn -> fail ~exn (lazy "get_sgoalty")
103 let gty = get_sgoalty status g in
104 metas_of_term status gty
107 let menv_closure status gl =
108 let rec closure acc = function
110 | x::l when IntSet.mem x acc -> closure acc l
111 | x::l -> closure (IntSet.add x acc) (deps status x @ l)
112 in closure IntSet.empty gl
115 (* we call a "fact" an object whose hypothesis occur in the goal
116 or in types of goal-variables *)
117 let branch status ty =
118 let status, ty, metas = saturate ~delta:0 status ty in
119 noprint (lazy ("saturated ty :" ^ (ppterm status ty)));
120 let g_metas = metas_of_term status ty in
121 let clos = menv_closure status g_metas in
122 (* let _,_,metasenv,_,_ = status#obj in *)
126 let _, m = term_of_cic_term status m (ctx_of m) in
128 | NCic.Meta(i,_) -> IntSet.add i acc
132 (* IntSet.subset menv clos *)
133 IntSet.cardinal(IntSet.diff menv clos)
135 let is_a_fact status ty = branch status ty = 0
137 let is_a_fact_obj s uri =
138 let obj = NCicEnvironment.get_checked_obj s uri in
140 | (_,_,[],[],NCic.Constant(_,_,_,ty,_)) ->
141 is_a_fact s (mk_cic_term [] ty)
142 (* aggiungere i costruttori *)
145 let is_a_fact_ast status subst metasenv ctx cand =
147 (lazy ("checking facts " ^ NotationPp.pp_term status cand));
148 let status, t = disambiguate status ctx ("",0,cand) `XTNone in
149 let status,t = term_of_cic_term status t ctx in
150 let ty = NCicTypeChecker.typeof status subst metasenv ctx t in
151 is_a_fact status (mk_cic_term ctx ty)
153 let current_goal status =
154 let open_goals = head_goals status#stack in
155 assert (List.length open_goals = 1);
156 let open_goal = List.hd open_goals in
157 let gty = get_goalty status open_goal in
158 let ctx = ctx_of gty in
161 let height_of_ref status (NReference.Ref (uri, x)) =
166 | NReference.CoFix _ ->
167 let _,height,_,_,_ = NCicEnvironment.get_checked_obj status uri in
169 | NReference.Def h -> h
170 | NReference.Fix (_,_,h) -> h
173 (*************************** height functions ********************************)
174 let fast_height_of_term status t =
178 NCic.Meta (_,(_,NCic.Ctx l)) -> List.iter aux l
182 | NCic.Implicit _ -> assert false
185 prerr_endline (status#ppterm ~metasenv:[] ~subst:[]
186 ~context:[] t ^ ":" ^ string_of_int (height_of_ref status nref));
188 h := max !h (height_of_ref status nref)
189 | NCic.Prod (_,t1,t2)
190 | NCic.Lambda (_,t1,t2) -> aux t1; aux t2
191 | NCic.LetIn (_,s,ty,t) -> aux s; aux ty; aux t
192 | NCic.Appl l -> List.iter aux l
193 | NCic.Match (_,outty,t,pl) -> aux outty; aux t; List.iter aux pl
198 let height_of_goal g status =
199 let ty = get_goalty status g in
200 let context = ctx_of ty in
201 let _, ty = term_of_cic_term status ty (ctx_of ty) in
202 let h = ref (fast_height_of_term status ty) in
205 | _, NCic.Decl ty -> h := max !h (fast_height_of_term status ty)
206 | _, NCic.Def (bo,ty) ->
207 h := max !h (fast_height_of_term status ty);
208 h := max !h (fast_height_of_term status bo);
214 let height_of_goals status =
215 let open_goals = head_goals status#stack in
216 assert (List.length open_goals > 0);
220 h := max !h (height_of_goal open_goal status))
222 noprint (lazy ("altezza sequente: " ^ string_of_int !h));
226 (* =============================== paramod =========================== *)
227 let solve f status eq_cache goal =
230 if fast then NCicParamod.fast_eq_check
231 else NCicParamod.paramod in
233 let n,h,metasenv,subst,o = status#obj in
234 let gname, ctx, gty = List.assoc goal metasenv in
235 let gty = NCicUntrusted.apply_subst status subst ctx gty in
236 let build_status (pt, _, metasenv, subst) =
238 debug_print (lazy ("refining: "^(status#ppterm ctx subst metasenv pt)));
239 let stamp = Unix.gettimeofday () in
240 let metasenv, subst, pt, pty =
241 (* NCicRefiner.typeof status
242 (* (status#set_coerc_db NCicCoercion.empty_db) *)
243 metasenv subst ctx pt None in
244 debug_print (lazy ("refined: "^(status#ppterm ctx subst metasenv pt)));
245 noprint (lazy ("synt: "^(status#ppterm ctx subst metasenv pty)));
246 let metasenv, subst =
247 NCicUnification.unify status metasenv subst ctx gty pty *)
249 (status#set_coerc_db NCicCoercion.empty_db)
250 metasenv subst ctx pt (`XTSome gty)
252 noprint (lazy (Printf.sprintf "Refined in %fs"
253 (Unix.gettimeofday() -. stamp)));
254 let status = status#set_obj (n,h,metasenv,subst,o) in
255 let metasenv = List.filter (fun j,_ -> j <> goal) metasenv in
256 let subst = (goal,(gname,ctx,pt,pty)) :: subst in
257 Some (status#set_obj (n,h,metasenv,subst,o))
259 NCicRefiner.RefineFailure msg
260 | NCicRefiner.Uncertain msg ->
261 debug_print (lazy ("WARNING U: refining in fast_eq_check failed\n" ^
262 snd (Lazy.force msg) ^
263 "\n in the environment\n" ^
264 status#ppmetasenv subst metasenv)); None
265 | NCicRefiner.AssertFailure msg ->
266 debug_print (lazy ("WARNING F: refining in fast_eq_check failed" ^
268 "\n in the environment\n" ^
269 status#ppmetasenv subst metasenv)); None
270 | Sys.Break as e -> raise e
273 HExtlib.filter_map build_status
274 (f status metasenv subst ctx eq_cache (NCic.Rel ~-1,gty))
277 let fast_eq_check eq_cache status (goal:int) =
278 match solve NCicParamod.fast_eq_check status eq_cache goal with
279 | [] -> raise (Error (lazy "no proof found",None))
283 let dist_fast_eq_check eq_cache s =
284 NTactics.distribute_tac (fast_eq_check eq_cache) s
287 let auto_eq_check eq_cache status =
289 let s = dist_fast_eq_check eq_cache status in
292 | Error _ -> debug_print (lazy ("no paramod proof found"));[]
295 let index_local_equations eq_cache ?(flag=false) status =
297 NCicParamod.empty_state
299 noprint (lazy "indexing equations");
300 let open_goals = head_goals status#stack in
301 let open_goal = List.hd open_goals in
302 let ngty = get_goalty status open_goal in
303 let _,_,metasenv,subst,_ = status#obj in
304 let ctx = apply_subst_context ~fix_projections:true status (ctx_of ngty) in
309 let t = NCic.Rel !c in
311 let ty = NCicTypeChecker.typeof status subst metasenv ctx t in
312 if is_a_fact status (mk_cic_term ctx ty) then
313 (debug_print(lazy("eq indexing " ^ (status#ppterm ctx subst metasenv ty)));
314 NCicParamod.forward_infer_step status metasenv subst ctx eq_cache t ty)
316 (noprint (lazy ("not a fact: " ^ (status#ppterm ctx subst metasenv ty)));
319 | NCicTypeChecker.TypeCheckerFailure _
320 | NCicTypeChecker.AssertFailure _ -> eq_cache)
325 let index_local_equations2 eq_cache status open_goal lemmas ?flag:(_=false) nohyps =
326 noprint (lazy "indexing equations");
327 let eq_cache,lemmas =
330 | Some l -> NCicParamod.empty_state,l
332 let ngty = get_goalty status open_goal in
333 let _,_,metasenv,subst,_ = status#obj in
334 let ctx = apply_subst_context ~fix_projections:true status (ctx_of ngty) in
337 (fun (status,lemmas) l ->
338 let status,l = NTacStatus.disambiguate status ctx l `XTNone in
339 let status,l = NTacStatus.term_of_cic_term status l ctx in
341 (status,[]) lemmas in
342 let local_equations =
343 if nohyps then [] else
344 List.map (fun i -> NCic.Rel (i + 1))
345 (HExtlib.list_seq 1 (List.length ctx)) in
346 let lemmas = lemmas @ local_equations in
350 let ty = NCicTypeChecker.typeof status subst metasenv ctx t in
351 if is_a_fact status (mk_cic_term ctx ty) then
352 (debug_print(lazy("eq indexing " ^ (status#ppterm ctx subst metasenv ty)));
353 NCicParamod.forward_infer_step status metasenv subst ctx eq_cache t ty)
355 (noprint (lazy ("not a fact: " ^ (status#ppterm ctx subst metasenv ty)));
358 | NCicTypeChecker.TypeCheckerFailure _
359 | NCicTypeChecker.AssertFailure _ -> eq_cache)
363 let fast_eq_check_tac ~params:_ s =
364 let unit_eq = index_local_equations s#eq_cache s in
365 dist_fast_eq_check unit_eq s
368 let paramod eq_cache status goal =
369 match solve NCicParamod.paramod status eq_cache goal with
370 | [] -> raise (Error (lazy "no proof found",None))
374 let paramod_tac ~params:_ s =
375 let unit_eq = index_local_equations s#eq_cache s in
376 NTactics.distribute_tac (paramod unit_eq) s
379 let demod eq_cache status goal =
380 match solve NCicParamod.demod status eq_cache goal with
381 | [] -> raise (Error (lazy "no progress",None))
385 let demod_tac ~params s =
387 index_local_equations2 s#eq_cache s i (fst params)
388 (List.mem_assoc "nohyps" (snd params))
390 NTactics.distribute_tac (fun s i -> demod (unit_eq s i) s i) s
394 let fast_eq_check_tac_all ~params eq_cache status =
395 let g,_,_ = current_goal status in
396 let allstates = fast_eq_check_all status eq_cache g in
397 let pseudo_low_tac s _ _ = s in
398 let pseudo_low_tactics =
399 List.map pseudo_low_tac allstates
401 List.map (fun f -> NTactics.distribute_tac f status) pseudo_low_tactics
406 let demod status eq_cache goal =
407 let n,h,metasenv,subst,o = status#obj in
408 let gname, ctx, gty = List.assoc goal metasenv in
409 let gty = NCicUntrusted.apply_subst subst ctx gty in
411 let demod_tac ~params s =
412 let unit_eq = index_local_equations s#eq_cache s in
413 dist_fast_eq_check unit_eq s
416 (*************** subsumption ****************)
418 let close_wrt_context status =
422 | name, NCic.Decl t -> NCic.Prod(name,t,ty)
423 | _name, NCic.Def(bo, _) -> NCicSubstitution.subst status bo ty)
426 let args_for_context ?(k=1) ctx =
429 (fun (n,l) ctx_entry ->
431 | _name, NCic.Decl _t -> n+1,NCic.Rel(n)::l
432 | _name, NCic.Def(_bo, _) -> n+1,l)
436 let constant_for_meta status ctx ty i =
437 let name = "cic:/foo"^(string_of_int i)^".con" in
438 let uri = NUri.uri_of_string name in
439 let ty = close_wrt_context status ty ctx in
440 (* prerr_endline (status#ppterm [] [] [] ty); *)
441 let attr = (`Generated,`Definition,`Local) in
442 let obj = NCic.Constant([],name,None,ty,attr) in
443 (* Constant of relevance * string * term option * term * c_attr *)
447 let refresh metasenv =
449 (fun (metasenv,subst) (i,(iattr,ctx,ty)) ->
450 let ikind = NCicUntrusted.kind_of_meta iattr in
451 let metasenv,_j,instance,ty =
452 NCicMetaSubst.mk_meta ~attrs:iattr
453 metasenv ctx ~with_type:ty ikind in
454 let s_entry = i,(iattr, ctx, instance, ty) in
455 let metasenv = List.filter (fun x,_ -> i <> x) metasenv in
456 metasenv,s_entry::subst)
457 (metasenv,[]) metasenv
459 (* close metasenv returns a ground instance of all the metas in the
460 metasenv, insantiatied with axioms, and the list of these axioms *)
461 let close_metasenv status metasenv subst =
463 let metasenv = NCicUntrusted.apply_subst_metasenv subst metasenv in
465 let metasenv = NCicUntrusted.sort_metasenv status subst metasenv in
467 (fun (subst,objs) (i,(_iattr,ctx,ty)) ->
468 let ty = NCicUntrusted.apply_subst status subst ctx ty in
470 NCicUntrusted.apply_subst_context status ~fix_projections:true
472 let (uri,_,_,_,_obj) as okind =
473 constant_for_meta status ctx ty i in
475 NCicEnvironment.check_and_add_obj status okind;
476 let iref = NReference.reference_of_spec uri NReference.Decl in
478 let args = args_for_context ctx in
479 if args = [] then NCic.Const iref
480 else NCic.Appl(NCic.Const iref::args)
482 (* prerr_endline (status#ppterm ctx [] [] iterm); *)
483 let s_entry = i, ([], ctx, iterm, ty)
484 in s_entry::subst,okind::objs
486 Sys.Break as e -> raise e
491 let ground_instances status gl =
492 let _,_,metasenv,subst,_ = status#obj in
493 let subset = menv_closure status gl in
494 let submenv = List.filter (fun (x,_) -> IntSet.mem x subset) metasenv in
496 let submenv = metasenv in
498 let subst, objs = close_metasenv status submenv subst in
502 let (_, ctx, t, _) = List.assoc i subst in
503 noprint (lazy (status#ppterm ctx [] [] t));
505 (fun (uri,_,_,_,_) as obj ->
506 NCicEnvironment.invalidate_item (`Obj (uri, obj)))
511 Not_found -> assert false
515 let replace_meta status i args target =
516 let rec aux k = function
517 (* TODO: local context *)
518 | NCic.Meta (j,lc) when i = j ->
522 List.map (NCicSubstitution.subst_meta status lc) args in
523 NCic.Appl(NCic.Rel k::args))
524 | NCic.Meta (_j,lc) as m ->
531 aux k (NCicSubstitution.lift status n t)) l))))
532 | t -> NCicUtils.map status (fun _ k -> k+1) k aux t
537 let close_wrt_metasenv status subst =
539 (fun ty (i,(_iattr,ctx,mty)) ->
540 let mty = NCicUntrusted.apply_subst status subst ctx mty in
542 NCicUntrusted.apply_subst_context status ~fix_projections:true
544 let cty = close_wrt_context status mty ctx in
545 let name = "foo"^(string_of_int i) in
546 let ty = NCicSubstitution.lift status 1 ty in
547 let args = args_for_context ~k:1 ctx in
548 (* prerr_endline (status#ppterm ctx [] [] iterm); *)
549 let ty = replace_meta status i args ty
551 NCic.Prod(name,cty,ty))
555 let _,_,metasenv,subst,_ = status#obj in
556 let subset = menv_closure status [g] in
557 let subset = IntSet.remove g subset in
558 let elems = IntSet.elements subset in
559 let _, ctx, ty = NCicUtils.lookup_meta g metasenv in
560 let ty = NCicUntrusted.apply_subst status subst ctx ty in
561 noprint (lazy ("metas in " ^ (status#ppterm ctx [] metasenv ty)));
562 noprint (lazy (String.concat ", " (List.map string_of_int elems)));
563 let submenv = List.filter (fun (x,_) -> IntSet.mem x subset) metasenv in
564 let submenv = List.rev (NCicUntrusted.sort_metasenv status subst submenv) in
566 let submenv = metasenv in
568 let ty = close_wrt_metasenv status subst ty submenv in
569 noprint (lazy (status#ppterm ctx [] [] ty));
573 (****************** smart application ********************)
575 let saturate_to_ref status metasenv subst ctx nref ty =
576 let height = height_of_ref status nref in
577 let rec aux metasenv ty args =
578 let ty,metasenv,moreargs =
579 NCicMetaSubst.saturate status ~delta:height metasenv subst ctx ty 0 in
581 | NCic.Const(NReference.Ref (_,NReference.Def _) as nre)
583 let _, _, bo, _, _, _ = NCicEnvironment.get_checked_def status nre in
584 aux metasenv bo (args@moreargs)
585 | NCic.Appl(NCic.Const(NReference.Ref (_,NReference.Def _) as nre)::tl)
587 let _, _, bo, _, _, _ = NCicEnvironment.get_checked_def status nre in
588 aux metasenv (NCic.Appl(bo::tl)) (args@moreargs)
589 | _ -> ty,metasenv,(args@moreargs)
593 let smart_apply t unit_eq status g =
594 let n,h,metasenv,_subst,o = status#obj in
595 let _gname, ctx, gty = List.assoc g metasenv in
596 (* let ggty = mk_cic_term context gty in *)
597 let status, t = disambiguate status ctx t `XTNone in
598 let status,t = term_of_cic_term status t ctx in
599 let _,_,metasenv,subst,_ = status#obj in
600 let ty = NCicTypeChecker.typeof status subst metasenv ctx t in
601 let ty,metasenv,args =
604 | NCic.Appl(NCic.Const(nref)::_) ->
605 saturate_to_ref status metasenv subst ctx nref ty
607 NCicMetaSubst.saturate status metasenv subst ctx ty 0 in
608 let metasenv,j,inst,_ = NCicMetaSubst.mk_meta metasenv ctx `IsTerm in
609 let status = status#set_obj (n,h,metasenv,subst,o) in
610 let pterm = if args=[] then t else
612 | NCic.Appl l -> NCic.Appl(l@args)
613 | _ -> NCic.Appl(t::args)
615 noprint(lazy("pterm " ^ (status#ppterm ctx [] [] pterm)));
616 noprint(lazy("pty " ^ (status#ppterm ctx [] [] ty)));
619 NUri.uri_of_string "cic:/matita/basics/logic/eq_coerc.con" in
620 let ref = NReference.reference_of_spec uri (NReference.Def(2)) in
624 NCic.Appl[eq_coerc;ty;NCic.Implicit `Type;pterm;inst] in
625 let smart = mk_cic_term ctx smart in
627 let status = instantiate status g smart in
628 let _,_,metasenv,subst,_ = status#obj in
629 let _,ctx,jty = List.assoc j metasenv in
630 let jty = NCicUntrusted.apply_subst status subst ctx jty in
631 debug_print(lazy("goal " ^ (status#ppterm ctx [] [] jty)));
632 let res = fast_eq_check unit_eq status j in
633 debug_print(lazy("ritorno da fast_eq_check"));
636 | NCicEnvironment.ObjectNotFound _s as e ->
637 raise (Error (lazy "eq_coerc non yet defined",Some e))
638 | Error _ as e -> debug_print (lazy "error"); raise e
639 (* FG: for now we catch TypeCheckerFailure; to be understood *)
640 | NCicTypeChecker.TypeCheckerFailure _ ->
641 debug_print (lazy "TypeCheckerFailure");
642 raise (Error (lazy "no proof found",None))
645 let compare_statuses ~past ~present =
646 let _,_,past,_,_ = past#obj in
647 let _,_,present,_,_ = present#obj in
648 List.map fst (List.filter (fun (i,_) -> not(List.mem_assoc i past)) present),
649 List.map fst (List.filter (fun (i,_) -> not (List.mem_assoc i present)) past)
652 (* paramodulation has only an implicit knoweledge of the symmetry of equality;
653 hence it is in trouble in proving (a = b) = (b = a) *)
654 let try_sym tac status g =
655 let sym_eq = Ast.Appl [Ast.Ident("sym_eq",None); Ast.Implicit `Vector] in
656 let _,_,metasenv,subst,_ = status#obj in
657 let _, context, gty = List.assoc g metasenv in
659 NCicParamod.is_equation status metasenv subst context gty
664 let new_status = instantiate_with_ast status g ("",0,sym_eq) in
665 let go, _ = compare_statuses ~past:status ~present:new_status in
666 assert (List.length go = 1);
667 let ng = List.hd go in
672 let smart_apply_tac t s =
673 let unit_eq = index_local_equations s#eq_cache s in
674 NTactics.distribute_tac (try_sym (smart_apply t unit_eq)) s
675 (* NTactics.distribute_tac (smart_apply t unit_eq) s *)
677 let smart_apply_auto t eq_cache =
678 NTactics.distribute_tac (try_sym (smart_apply t eq_cache))
679 (* NTactics.distribute_tac (smart_apply t eq_cache) *)
682 (****************** types **************)
685 type th_cache = (NCic.context * InvRelDiscriminationTree.t) list
687 (* cartesian: term set list -> term list set *)
690 [] -> NDiscriminationTree.TermListSet.empty
692 NDiscriminationTree.TermSet.fold
693 (fun x acc -> NDiscriminationTree.TermListSet.add [x] acc) l NDiscriminationTree.TermListSet.empty
695 let rest = cartesian tl in
696 NDiscriminationTree.TermSet.fold
698 NDiscriminationTree.TermListSet.fold (fun l acc' -> NDiscriminationTree.TermListSet.add (x::l) acc') rest acc
699 ) he NDiscriminationTree.TermListSet.empty
702 (* all_keys_of_cic_type: term -> term set *)
703 let all_keys_of_cic_type status metasenv subst context ty =
705 (* Here we are dropping the metasenv, but this should not raise any
706 exception (hopefully...) *)
708 NCicMetaSubst.saturate status ~delta:max_int metasenv subst context ty 0
714 NCic.Appl (he::tl) ->
717 let wty = NCicReduction.whd status ~delta:0 ~subst context ty in
719 NDiscriminationTree.TermSet.add ty (aux ty)
721 NDiscriminationTree.TermSet.union
722 (NDiscriminationTree.TermSet.add ty (aux ty))
723 (NDiscriminationTree.TermSet.add wty (aux wty))
726 NDiscriminationTree.TermListSet.fold
727 (fun l acc -> NDiscriminationTree.TermSet.add (NCic.Appl l) acc)
728 (cartesian ((NDiscriminationTree.TermSet.singleton he)::tl'))
729 NDiscriminationTree.TermSet.empty
730 | _ -> NDiscriminationTree.TermSet.empty
732 let ty,ity = saturate ty in
733 let wty,iwty = saturate (NCicReduction.whd status ~delta:0 ~subst context ty) in
735 [ity, NDiscriminationTree.TermSet.add ty (aux ty)]
737 [ity, NDiscriminationTree.TermSet.add ty (aux ty) ;
738 iwty, NDiscriminationTree.TermSet.add wty (aux wty) ]
741 let all_keys_of_type status t =
742 let _,_,metasenv,subst,_ = status#obj in
743 let context = ctx_of t in
744 let status, t = apply_subst status context t in
746 all_keys_of_cic_type status metasenv subst context
747 (snd (term_of_cic_term status t context))
751 (fun (intros,keys) ->
753 NDiscriminationTree.TermSet.fold
754 (fun t acc -> Ncic_termSet.add (mk_cic_term context t) acc)
755 keys Ncic_termSet.empty
760 let keys_of_type status orig_ty =
761 (* Here we are dropping the metasenv (in the status), but this should not
762 raise any exception (hopefully...) *)
763 let _, ty, _ = saturate ~delta:max_int status orig_ty in
764 let _, ty = apply_subst status (ctx_of ty) ty in
767 let orig_ty' = NCicTacReduction.normalize ~subst context orig_ty in
768 if orig_ty' <> orig_ty then
769 let ty',_,_= NCicMetaSubst.saturate ~delta:0 metasenv subst context orig_ty' 0 in
775 (*CSC: strange: we keep ty, ty normalized and ty ~delta:(h-1) *)
777 let _, ty = term_of_cic_term status ty (ctx_of ty) in
779 | NCic.Const (NReference.Ref (_,(NReference.Def h | NReference.Fix (_,_,h))))
780 | NCic.Appl (NCic.Const(NReference.Ref(_,(NReference.Def h | NReference.Fix (_,_,h))))::_)
782 let _,ty,_= saturate status ~delta:(h-1) orig_ty in
789 let all_keys_of_term status t =
790 let status, orig_ty = typeof status (ctx_of t) t in
791 all_keys_of_type status orig_ty
794 let keys_of_term status t =
795 let status, orig_ty = typeof status (ctx_of t) t in
796 keys_of_type status orig_ty
799 let mk_th_cache status gl =
801 (fun (status, acc) g ->
802 let gty = get_goalty status g in
803 let ctx = ctx_of gty in
804 noprint(lazy("th cache for: "^ppterm status gty));
805 noprint(lazy("th cache in: "^ppcontext status ctx));
806 if List.mem_assq ctx acc then status, acc else
807 let idx = InvRelDiscriminationTree.empty in
810 (fun (status, i, idx) _ ->
811 let t = mk_cic_term ctx (NCic.Rel i) in
812 let status, keys = keys_of_term status t in
813 noprint(lazy("indexing: "^ppterm status t ^ ": " ^ string_of_int (List.length keys)));
815 List.fold_left (fun idx k ->
816 InvRelDiscriminationTree.index idx k t) idx keys
821 status, (ctx, idx) :: acc)
825 let all_elements ctx cache =
826 let dummy = mk_cic_term ctx (NCic.Meta (0,(0, (NCic.Irl 0)))) in
828 let idx = List.assq ctx cache in
829 Ncic_termSet.elements
830 (InvRelDiscriminationTree.retrieve_unifiables idx dummy)
833 let add_to_th t c ty =
834 let key_c = ctx_of t in
835 if not (List.mem_assq key_c c) then
836 (key_c ,InvRelDiscriminationTree.index
837 InvRelDiscriminationTree.empty ty t ) :: c
839 let rec replace = function
841 | (x, idx) :: tl when x == key_c ->
842 (x, InvRelDiscriminationTree.index idx ty t) :: tl
843 | x :: tl -> x :: replace tl
848 let rm_from_th t c ty =
849 let key_c = ctx_of t in
850 if not (List.mem_assq key_c c) then assert false
852 let rec replace = function
854 | (x, idx) :: tl when x == key_c ->
855 (x, InvRelDiscriminationTree.remove_index idx ty t) :: tl
856 | x :: tl -> x :: replace tl
861 let pp_idx status idx =
862 InvRelDiscriminationTree.iter idx
864 noprint(lazy("K: " ^ NCicInverseRelIndexable.string_of_path k));
866 (fun t -> debug_print(lazy("\t"^ppterm status t)))
870 let pp_th (status: #NTacStatus.pstatus) =
873 noprint(lazy( "-----------------------------------------------"));
874 noprint(lazy( (status#ppcontext ~metasenv:[] ~subst:[] ctx)));
875 noprint(lazy( "||====> "));
879 let search_in_th gty th =
880 let c = ctx_of gty in
881 let rec aux acc = function
882 | [] -> (* Ncic_termSet.elements *) acc
885 let idx = List.assoc(*q*) k th in
886 let acc = Ncic_termSet.union acc
887 (InvRelDiscriminationTree.retrieve_unifiables idx gty)
890 with Not_found -> aux acc tl
892 aux Ncic_termSet.empty c
896 do_types : bool; (* solve goals in Type *)
897 last : bool; (* last goal: take first solution only *)
898 candidates: Ast.term list option;
899 local_candidates: bool;
906 {facts : th_cache; (* positive results *)
907 under_inspection : cic_term list * th_cache; (* to prune looping *)
908 failures : th_cache; (* to avoid repetitions *)
909 unit_eq : NCicParamod.state;
913 let add_to_trace status ~depth cache t =
916 debug_print ~depth (lazy ("Adding to trace: " ^ NotationPp.pp_term status t));
917 {cache with trace = t::cache.trace}
918 | Ast.NCic _ (* local candidate *)
919 | _ -> (*not an application *) cache
921 let pptrace status tr =
922 (lazy ("Proof Trace: " ^ (String.concat ";"
923 (List.map (NotationPp.pp_term status) tr))))
925 let remove_from_trace cache t =
928 (match cache.trace with
929 | _::tl -> {cache with trace = tl}
931 | Ast.NCic _ (* local candidate *)
932 | _ -> (*not an application *) cache *)
935 type goal = int * sort (* goal, depth, sort *)
936 type fail = goal * cic_term
937 type candidate = int * Ast.term (* unique candidate number, candidate *)
939 exception Gaveup of th_cache (* failure cache *)
940 exception Proved of NTacStatus.tac_status * Ast.term list
942 (* let close_failures _ c = c;; *)
943 (* let prunable _ _ _ = false;; *)
944 (* let cache_examine cache gty = `Notfound;; *)
945 (* let put_in_subst s _ _ _ = s;; *)
946 (* let add_to_cache_and_del_from_orlist_if_green_cut _ _ c _ _ o f _ = c, o, f, false ;; *)
947 (* let cache_add_underinspection c _ _ = c;; *)
949 let init_cache ?(facts=[]) ?(under_inspection=[],[])
951 ?(unit_eq=NCicParamod.empty_state)
956 under_inspection = under_inspection;
960 let only _signature _context _candidate = true
962 (* TASSI: nel trie ci mettiamo solo il body, non il ty *)
964 NCicTypeChecker.typeof ~subst:[] ~metasenv:[] [] candidate
966 let height = fast_height_of_term status candidate_ty in
967 let rc = signature >= height in
969 noprint (lazy ("Filtro: " ^ status#ppterm ~context:[] ~subst:[]
970 ~metasenv:[] candidate ^ ": " ^ string_of_int height))
972 noprint (lazy ("Tengo: " ^ status#ppterm ~context:[] ~subst:[]
973 ~metasenv:[] candidate ^ ": " ^ string_of_int height));
978 let candidate_no = ref 0;;
980 let openg_no status = List.length (head_goals status#stack)
982 let sort_candidates status ctx candidates =
983 let _,_,metasenv,subst,_ = status#obj in
985 let status,ct = disambiguate status ctx ("",0,cand) `XTNone in
986 let status,t = term_of_cic_term status ct ctx in
987 let ty = NCicTypeChecker.typeof status subst metasenv ctx t in
988 let res = branch status (mk_cic_term ctx ty) in
989 noprint (lazy ("branch factor for: " ^ (ppterm status ct) ^ " = "
990 ^ (string_of_int res)));
993 let candidates = List.map (fun t -> branch t,t) candidates in
995 List.sort (fun (a,_) (b,_) -> a - b) candidates in
996 let candidates = List.map snd candidates in
997 noprint (lazy ("candidates =\n" ^ (String.concat "\n"
998 (List.map (NotationPp.pp_term status) candidates))));
1001 let sort_new_elems l =
1002 List.sort (fun (_,s1) (_,s2) -> openg_no s1 - openg_no s2) l
1004 let rec stack_goals level gs =
1005 if level = 0 then []
1007 | [] -> assert false
1009 let is_open = function
1010 | (_,Continuationals.Stack.Open i) -> Some i
1011 | (_,Continuationals.Stack.Closed _) -> None
1013 HExtlib.filter_map is_open g @ stack_goals (level-1) s
1016 let open_goals level status = stack_goals level status#stack
1019 let try_candidate ?(smart=0) _flags depth status eq_cache _ctx t =
1021 (*let old_og_no = List.length (open_goals (depth+1) status) in*)
1022 debug_print ~depth (lazy ("try " ^ (string_of_int smart) ^ " : "
1023 ^ (NotationPp.pp_term status) t));
1025 if smart = 0 then NTactics.apply_tac ("",0,t) status
1026 else if smart = 1 then
1027 smart_apply_auto ("",0,t) eq_cache status
1028 else (* smart = 2: both *)
1029 try NTactics.apply_tac ("",0,t) status
1031 smart_apply_auto ("",0,t) eq_cache status
1033 (* FG: this optimization rules out some applications of
1034 * lift_bind (from contribs/lambda_delta/Basic_2/substitution/lift.ma)
1036 (* we compare the expected branching with the actual one and
1037 prune the candidate when the latter is larger. The optimization
1038 is meant to rule out stange applications of flexible terms,
1039 such as the application of eq_f that always succeeds.
1040 There is some gain but less than expected *)
1041 let og_no = List.length (open_goals (depth+1) status) in
1042 let status, cict = disambiguate status ctx ("",0,t) None in
1043 let status,ct = term_of_cic_term status cict ctx in
1044 let _,_,metasenv,subst,_ = status#obj in
1045 let ty = NCicTypeChecker.typeof status subst metasenv ctx ct in
1046 let res = branch status (mk_cic_term ctx ty) in
1047 let diff = og_no - old_og_no in
1048 debug_print (lazy ("expected branching: " ^ (string_of_int res)));
1049 debug_print (lazy ("actual: branching" ^ (string_of_int diff)));
1050 (* some flexibility *)
1051 if og_no - old_og_no > res then
1052 (debug_print (lazy ("branch factor for: " ^ (ppterm status cict) ^ " = "
1053 ^ (string_of_int res) ^ " vs. " ^ (string_of_int og_no)));
1054 debug_print ~depth (lazy "strange application"); None)
1056 *) (incr candidate_no; Some ((!candidate_no,t),status))
1057 with Error _ -> debug_print ~depth (lazy "failed"); None
1060 let sort_of status subst metasenv ctx t =
1061 let ty = NCicTypeChecker.typeof status subst metasenv ctx t in
1062 let metasenv',ty = NCicUnification.fix_sorts status metasenv subst ty in
1063 assert (metasenv = metasenv');
1064 NCicTypeChecker.typeof status subst metasenv ctx ty
1067 let type0= NUri.uri_of_string ("cic:/matita/pts/Type0.univ")
1070 let perforate_small status subst metasenv context t =
1071 let rec aux = function
1072 | NCic.Appl (hd::tl) ->
1074 let s = sort_of status subst metasenv context t in
1076 | NCic.Sort(NCic.Type [`Type,u])
1077 when u=type0 -> NCic.Meta (0,(0,NCic.Irl 0))
1080 NCic.Appl (hd::List.map map tl)
1086 let get_cands retrieve_for diff empty gty weak_gty =
1087 let cands = retrieve_for gty in
1089 | None -> cands, empty
1091 let more_cands = retrieve_for weak_gty in
1092 cands, diff more_cands cands
1095 let is_a_needed_uri s =
1096 s = "cic:/matita/basics/logic/eq.ind" ||
1097 s = "cic:/matita/basics/logic/sym_eq.con" ||
1098 s = "cic:/matita/basics/logic/trans_eq.con" ||
1099 s = "cic:/matita/basics/logic/eq_f3.con" ||
1100 s = "cic:/matita/basics/logic/eq_f2.con" ||
1101 s = "cic:/matita/basics/logic/eq_f.con"
1103 let get_candidates ?(smart=true) ~pfailed depth flags status cache _signature gty =
1104 let universe = status#auto_cache in
1105 let _,_,metasenv,subst,_ = status#obj in
1106 let context = ctx_of gty in
1107 let _, raw_gty = term_of_cic_term status gty context in
1108 let is_prod, _is_eq =
1109 let status, t = term_of_cic_term status gty context in
1110 let t = NCicReduction.whd status subst context t in
1112 | NCic.Prod _ -> true, false
1113 | _ -> false, NCicParamod.is_equation status metasenv subst context t
1115 debug_print ~depth (lazy ("gty:" ^ NTacStatus.ppterm status gty));
1117 NCicParamod.is_equation status metasenv subst context raw_gty
1119 let raw_weak_gty, weak_gty =
1126 perforate_small status subst metasenv context raw_gty in
1127 let weak = mk_cic_term context raw_weak in
1128 noprint ~depth (lazy ("weak_gty:" ^ NTacStatus.ppterm status weak));
1129 Some raw_weak, Some (weak)
1133 (* we now compute global candidates *)
1134 let global_cands, smart_global_cands =
1136 let to_ast = function
1137 | NCic.Const r when true
1138 (*is_relevant statistics r*) -> Some (Ast.NRef r)
1139 (* | NCic.Const _ -> None *)
1140 | _ -> assert false in
1142 to_ast (NDiscriminationTree.TermSet.elements s) in
1145 (NDiscriminationTree.DiscriminationTree.retrieve_unifiables universe)
1146 NDiscriminationTree.TermSet.diff
1147 NDiscriminationTree.TermSet.empty
1148 raw_gty raw_weak_gty in
1151 let global_cands,smart_global_cands =
1152 if flags.local_candidates then global_cands,smart_global_cands
1153 else let filter = List.filter (function Ast.NRef NReference.Ref (uri,_) -> is_a_needed_uri
1156 in filter global_cands,filter smart_global_cands
1158 (* we now compute local candidates *)
1159 let local_cands,smart_local_cands =
1162 let _status, t = term_of_cic_term status t context
1164 List.map to_ast (Ncic_termSet.elements s) in
1167 (fun ty -> search_in_th ty cache)
1168 Ncic_termSet.diff Ncic_termSet.empty gty weak_gty in
1171 let local_cands,smart_local_cands =
1172 if flags.local_candidates then local_cands,smart_local_cands
1173 else let filter = List.filter (function Ast.NRef NReference.Ref (uri,_) -> is_a_needed_uri
1176 in filter local_cands,filter smart_local_cands
1178 (* we now splits candidates in facts or not facts *)
1179 let test = is_a_fact_ast status subst metasenv context in
1180 let by,given_candidates =
1181 match flags.candidates with
1183 | None -> false, [] in
1184 (* we compute candidates to be applied in normal mode, splitted in
1185 facts and not facts *)
1186 let candidates_facts,candidates_other =
1187 let gl1,gl2 = List.partition test global_cands in
1188 let ll1,ll2 = List.partition test local_cands in
1189 (* if the goal is an equation and paramodulation did not fail
1190 we avoid to apply unit equalities; refl is an
1191 exception since it prompts for convertibility *)
1192 let l1 = if is_eq && (not pfailed)
1193 then [Ast.Ident("refl",None)] else gl1@ll1 in
1195 (* if smart given candidates are applied in smart mode *)
1196 if by && smart then ll2
1197 else if by then given_candidates@ll2
1201 (* we now compute candidates to be applied in smart mode, splitted in
1202 facts and not facts *)
1203 let smart_candidates_facts, smart_candidates_other =
1204 if is_prod || not(smart) then [],[]
1206 let sgl1,sgl2 = List.partition test smart_global_cands in
1207 let sll1,sll2 = List.partition test smart_local_cands in
1208 let l1 = if is_eq then [] else sgl1@sll1 in
1210 if by && smart then given_candidates@sll2
1211 else if by then sll2
1216 smart_candidates_facts,
1217 sort_candidates status context (candidates_other),
1218 sort_candidates status context (smart_candidates_other)
1221 let applicative_case ~pfailed depth signature status flags gty cache =
1222 app_counter:= !app_counter+1;
1223 let _,_,metasenv,subst,_ = status#obj in
1224 let context = ctx_of gty in
1225 let tcache = cache.facts in
1226 let is_prod, is_eq =
1227 let status, t = term_of_cic_term status gty context in
1228 let t = NCicReduction.whd status subst context t in
1230 | NCic.Prod _ -> true, false
1231 | _ -> false, NCicParamod.is_equation status metasenv subst context t
1233 debug_print ~depth (lazy (string_of_bool is_eq));
1235 let candidates_facts, smart_candidates_facts,
1236 candidates_other, smart_candidates_other =
1237 get_candidates ~smart:true ~pfailed depth
1238 flags status tcache signature gty
1240 let sm = if is_eq || is_prod then 0 else 2 in
1241 (*let sm1 = if flags.last then 2 else 0 in *)
1242 let maxd = (depth + 1 = flags.maxdepth) in
1243 let try_candidates only_one sm acc candidates =
1246 if (only_one && (elems <> [])) then elems
1248 match try_candidate (~smart:sm)
1249 flags depth status cache.unit_eq context cand with
1251 | Some x -> x::elems)
1254 (* if the goal is the last one we stop at the first fact *)
1255 let elems = try_candidates flags.last sm [] candidates_facts in
1256 (* now we add smart_facts *)
1257 let elems = try_candidates flags.last sm elems smart_candidates_facts in
1258 (* if we are at maxdepth and the goal is not a product we are done
1259 similarly, if the goal is the last one and we already found a
1261 if (maxd && not(is_prod)) || (flags.last && elems<>[]) then elems
1263 let elems = try_candidates false 2 elems candidates_other in
1264 debug_print ~depth (lazy ("not facts: try smart application"));
1265 try_candidates false 2 elems smart_candidates_other
1271 (* gty is supposed to be meta-closed *)
1272 let is_subsumed depth filter_depth status gty cache =
1273 if cache=[] then false else (
1274 debug_print ~depth (lazy("Subsuming " ^ (ppterm status gty)));
1275 let n,h,metasenv,subst,obj = status#obj in
1276 let ctx = ctx_of gty in
1277 let _ , raw_gty = term_of_cic_term status gty ctx in
1278 let target = NCicSubstitution.lift status 1 raw_gty in
1279 (* we compute candidates using the perforated type *)
1286 perforate_small status subst metasenv ctx raw_gty in
1287 let weak = mk_cic_term ctx raw_weak in
1288 debug_print ~depth (lazy ("weak_gty:" ^ NTacStatus.ppterm status weak));
1292 (* candidates must only be searched w.r.t the given context *)
1295 let idx = List.assq ctx cache in
1298 Ncic_termSet.elements
1299 (InvRelDiscriminationTree.retrieve_unifiables idx weak)
1301 with Not_found -> []
1303 (* this is a dirty trick: the first argument of an application is used
1304 to remember at which depth a goal failed *)
1306 let ctx = ctx_of t in
1307 let _, src = term_of_cic_term status t ctx in
1309 | NCic.Appl [NCic.Implicit (`Typeof d); t]
1310 when d <= depth -> Some (mk_cic_term ctx t)
1313 if filter_depth then HExtlib.filter_map filter candidates else candidates in
1315 (lazy ("failure candidates: " ^ string_of_int (List.length candidates)));
1319 let _ , source = term_of_cic_term status t ctx in
1321 NCic.Prod("foo",source,target) in
1322 let metasenv,j,_,_ =
1323 NCicMetaSubst.mk_meta
1324 metasenv ctx ~with_type:implication `IsType in
1325 let status = status#set_obj (n,h,metasenv,subst,obj) in
1326 let status = status#set_stack [([1,Open j],[],[],`NoTag,[])] in
1328 let status = NTactics.intro_tac "foo" status in
1330 NTactics.apply_tac ("",0,Ast.NCic (NCic.Rel 1)) status
1332 if (head_goals status#stack = []) then raise Found
1337 with Found -> debug_print ~depth (lazy "success");true)
1340 let rec guess_name name ctx =
1341 if name = "_" then guess_name "auto" ctx else
1342 if not (List.mem_assoc name ctx) then name else
1343 guess_name (name^"'") ctx
1346 let is_prod status =
1347 let _, ctx, gty = current_goal status in
1348 let status, gty = apply_subst status ctx gty in
1349 let _, raw_gty = term_of_cic_term status gty ctx in
1351 | NCic.Prod (name,src,_) ->
1352 let status, src = whd status ~delta:0 ctx (mk_cic_term ctx src) in
1353 (match snd (term_of_cic_term status src ctx) with
1354 | NCic.Const(NReference.Ref (_,NReference.Ind _) as r)
1355 | NCic.Appl (NCic.Const(NReference.Ref (_,NReference.Ind _) as r)::_) ->
1356 let _,_,itys,_,_ = NCicEnvironment.get_checked_indtys status r in
1358 (* | [_,_,_,[_;_]] con nat va, ovviamente, in loop *)
1360 | [_,_,_,[]] -> `Inductive (guess_name name ctx)
1361 | _ -> `Some (guess_name name ctx))
1362 | _ -> `Some (guess_name name ctx))
1365 let intro ~depth status facts name =
1366 let status = NTactics.intro_tac name status in
1367 let _, ctx, _ngty = current_goal status in
1368 let t = mk_cic_term ctx (NCic.Rel 1) in
1369 let status, keys = keys_of_term status t in
1370 let facts = List.fold_left (add_to_th t) facts keys in
1371 debug_print ~depth (lazy ("intro: "^ name));
1372 (* unprovability is not stable w.r.t introduction *)
1376 let rec intros_facts ~depth status facts =
1377 if List.length (head_goals status#stack) <> 1 then status, facts else
1378 match is_prod status with
1382 intro ~depth status facts name
1383 in intros_facts ~depth status facts
1384 (* | `Inductive name ->
1385 let status = NTactics.case1_tac name status in
1386 intros_facts ~depth status facts *)
1387 | _ -> status, facts
1390 let intros ~depth status ?(use_given_only=false) cache =
1391 match is_prod status with
1394 let trace = cache.trace in
1396 intros_facts ~depth status cache.facts
1398 if head_goals status#stack = [] then
1399 let status = NTactics.merge_tac status in
1400 [(0,Ast.Ident("__intros",None)),status], cache
1402 (* we reindex the equation from scratch *)
1403 let unit_eq = index_local_equations status#eq_cache status ~flag:use_given_only in
1404 let status = NTactics.merge_tac status in
1405 [(0,Ast.Ident("__intros",None)),status],
1406 init_cache ~facts ~unit_eq () ~trace
1410 let reduce ~whd ~depth status g =
1411 let n,h,metasenv,subst,o = status#obj in
1412 let attr, ctx, ty = NCicUtils.lookup_meta g metasenv in
1413 let ty = NCicUntrusted.apply_subst status subst ctx ty in
1415 (if whd then NCicReduction.whd else NCicTacReduction.normalize) status ~subst ctx ty
1420 (lazy ("reduced to: "^ status#ppterm ctx subst metasenv ty'));
1422 (g,(attr,ctx,ty'))::(List.filter (fun (i,_) -> i<>g) metasenv)
1424 let status = status#set_obj (n,h,metasenv,subst,o) in
1425 (* we merge to gain a depth level; the previous goal level should
1427 let status = NTactics.merge_tac status in
1429 [(!candidate_no,Ast.Ident("__whd",None)),status])
1432 let is_meta status gty =
1433 let _, ty = term_of_cic_term status gty (ctx_of gty) in
1435 | NCic.Meta _ -> true
1439 let do_something signature flags status g depth gty ?(use_given_only=false) cache =
1440 (* if the goal is meta we close it with I:True. This should work
1441 thanks to the toplogical sorting of goals. *)
1442 if is_meta status gty then
1443 let t = Ast.Ident("I",None) in
1444 debug_print (lazy ("using default term" ^ (NotationPp.pp_term status) t));
1445 let s = NTactics.apply_tac ("",0,t) status in
1448 let l0, cache = intros ~depth status cache ~use_given_only in
1449 if l0 <> [] then l0, cache
1452 let l = reduce ~whd:true ~depth status g in
1453 (* if l <> [] then l,cache else *)
1454 (* backward aplications *)
1459 ((!candidate_no,Ast.Ident("__paramod",None)),s))
1460 (auto_eq_check cache.unit_eq status)
1463 if ((l1 <> []) && flags.last) then [] else
1464 applicative_case ~pfailed:(l1=[]) depth signature status flags gty cache
1468 (fun ((_,t),_) -> toref incr_nominations statistics t) l2;
1469 (* states in l1 have have an empty set of subgoals: no point to sort them *)
1471 (lazy ("alternatives = " ^ (string_of_int (List.length (l1@l@l2)))));
1472 (* we order alternatives w.r.t the number of subgoals they open *)
1473 l1 @ (sort_new_elems l2) @ l, cache
1476 let pp_goal = function
1477 | (_,Continuationals.Stack.Open i)
1478 | (_,Continuationals.Stack.Closed i) -> string_of_int i
1481 let pp_goals status l =
1485 let gty = get_goalty status i in
1486 NTacStatus.ppterm status gty)
1493 let compare = Pervasives.compare
1497 module MS = HTopoSort.Make(M)
1500 let sort_tac status =
1502 match status#stack with
1503 | [] -> assert false
1504 | (goals, t, k, tag, p) :: s ->
1505 let g = head_goals status#stack in
1507 (List.rev (MS.topological_sort g (deps status))) in
1508 noprint (lazy ("old g = " ^
1509 String.concat "," (List.map string_of_int g)));
1510 noprint (lazy ("sorted goals = " ^
1511 String.concat "," (List.map string_of_int sortedg)));
1512 let is_it i = function
1513 | (_,Continuationals.Stack.Open j )
1514 | (_,Continuationals.Stack.Closed j ) -> i = j
1517 List.map (fun i -> List.find (is_it i) goals) sortedg
1519 (sorted_goals, t, k, tag, p) :: s
1521 status#set_stack gstatus
1524 let clean_up_tac status =
1526 match status#stack with
1527 | [] -> assert false
1528 | (g, t, k, tag, p) :: s ->
1529 let is_open = function
1530 | (_,Continuationals.Stack.Open _) -> true
1531 | (_,Continuationals.Stack.Closed _) -> false
1533 let g' = List.filter is_open g in
1534 (g', t, k, tag, p) :: s
1536 status#set_stack gstatus
1539 let focus_tac focus status =
1541 match status#stack with
1542 | [] -> assert false
1543 | (g, t, k, tag) :: s ->
1544 let in_focus = function
1545 | (_,Continuationals.Stack.Open i)
1546 | (_,Continuationals.Stack.Closed i) -> List.mem i focus
1548 let focus,others = List.partition in_focus g
1550 (* we need to mark it as a BranchTag, otherwise cannot merge later *)
1551 (focus,[],[],`BranchTag) :: (others, t, k, tag) :: s
1553 status#set_stack gstatus
1556 let deep_focus_tac level focus status =
1557 let in_focus = function
1558 | (_,Continuationals.Stack.Open i)
1559 | (_,Continuationals.Stack.Closed i) -> List.mem i focus
1561 let rec slice level gs =
1562 if level = 0 then [],[],gs else
1564 | [] -> assert false
1565 | (g, t, k, tag,p) :: s ->
1566 let f,o,gs = slice (level-1) s in
1567 let f1,o1 = List.partition in_focus g
1569 (f1,[],[],`BranchTag, [])::f, (o1, t, k, tag, p)::o, gs
1572 let f,o,s = slice level status#stack in f@o@s
1574 status#set_stack gstatus
1577 let move_to_side level status =
1578 match status#stack with
1579 | [] -> assert false
1580 | (g,_,_,_,_)::tl ->
1581 let is_open = function
1582 | (_,Continuationals.Stack.Open i) -> Some i
1583 | (_,Continuationals.Stack.Closed _) -> None
1585 let others = menv_closure status (stack_goals (level-1) tl) in
1586 List.for_all (fun i -> IntSet.mem i others)
1587 (HExtlib.filter_map is_open g)
1589 let top_cache ~depth:_ top status ?(use_given_only=false) cache =
1591 let unit_eq = index_local_equations status#eq_cache status ~flag:use_given_only in
1592 {cache with unit_eq = unit_eq}
1595 let rec auto_clusters ?(top=false) flags signature cache depth ?(use_given_only=false) status : unit =
1596 debug_print ~depth (lazy ("entering auto clusters at depth " ^
1597 (string_of_int depth)));
1598 debug_print ~depth (pptrace status cache.trace);
1599 (* ignore(Unix.select [] [] [] 0.01); *)
1600 let status = clean_up_tac status in
1601 let goals = head_goals status#stack in
1603 if depth = 0 then raise (Proved (status, cache.trace))
1605 let status = NTactics.merge_tac status in
1607 let l,tree = cache.under_inspection in
1609 | [] -> cache (* possible because of intros that cleans the cache *)
1610 | a::tl -> let tree = rm_from_th a tree a in
1611 {cache with under_inspection = tl,tree}
1613 auto_clusters flags signature cache (depth-1) status ~use_given_only
1614 else if List.length goals < 2 then
1615 let cache = top_cache ~depth top status cache ~use_given_only in
1616 auto_main flags signature cache depth status ~use_given_only
1618 let all_goals = open_goals (depth+1) status in
1619 debug_print ~depth (lazy ("goals = " ^
1620 String.concat "," (List.map string_of_int all_goals)));
1621 let classes = HExtlib.clusters (deps status) all_goals in
1622 (* if any of the classes exceed maxwidth we fail *)
1625 if List.length gl > flags.maxwidth then
1627 debug_print ~depth (lazy "FAIL GLOBAL WIDTH");
1628 HLog.warn (sprintf "global width (%u) exceeded: %u"
1629 flags.maxwidth (List.length gl));
1630 raise (Gaveup cache.failures)
1631 end else ()) classes;
1632 if List.length classes = 1 then
1634 {flags with last = (List.length all_goals = 1)} in
1635 (* no need to cluster *)
1636 let cache = top_cache ~depth top status cache ~use_given_only in
1637 auto_main flags signature cache depth status ~use_given_only
1639 let classes = if top then List.rev classes else classes in
1645 ("cluster:" ^ String.concat "," (List.map string_of_int l)))
1647 (* we now process each cluster *)
1648 let status,cache,b =
1650 (fun (status,cache,b) gl ->
1652 {flags with last = (List.length gl = 1)} in
1653 let lold = List.length status#stack in
1654 debug_print ~depth (lazy ("stack length = " ^
1655 (string_of_int lold)));
1656 let fstatus = deep_focus_tac (depth+1) gl status in
1657 let cache = top_cache ~depth top fstatus cache ~use_given_only in
1659 debug_print ~depth (lazy ("focusing on" ^
1660 String.concat "," (List.map string_of_int gl)));
1661 auto_main flags signature cache depth fstatus ~use_given_only; assert false
1663 | Proved(status,trace) ->
1664 let status = NTactics.merge_tac status in
1665 let cache = {cache with trace = trace} in
1666 let lnew = List.length status#stack in
1667 assert (lold = lnew);
1669 | Gaveup failures when top ->
1670 let cache = {cache with failures = failures} in
1673 (status,cache,false) classes
1675 let rec final_merge n s =
1676 if n = 0 then s else final_merge (n-1) (NTactics.merge_tac s)
1677 in let status = final_merge depth status
1678 in if b then raise (Proved(status,cache.trace)) else raise (Gaveup cache.failures)
1682 (* BRAND NEW VERSION *)
1683 auto_main flags signature cache depth ?(use_given_only=false) status: unit=
1684 debug_print ~depth (lazy "entering auto main");
1685 debug_print ~depth (pptrace status cache.trace);
1686 debug_print ~depth (lazy ("stack length = " ^
1687 (string_of_int (List.length status#stack))));
1688 (* ignore(Unix.select [] [] [] 0.01); *)
1689 let status = sort_tac (clean_up_tac status) in
1690 let goals = head_goals status#stack in
1692 | [] when depth = 0 -> raise (Proved (status,cache.trace))
1694 let status = NTactics.merge_tac status in
1696 let l,tree = cache.under_inspection in
1698 | [] -> cache (* possible because of intros that cleans the cache *)
1699 | a::tl -> let tree = rm_from_th a tree a in
1700 {cache with under_inspection = tl,tree}
1702 auto_clusters flags signature cache (depth-1) status ~use_given_only
1704 if depth > 0 && move_to_side depth status
1706 let status = NTactics.merge_tac status in
1708 let l,tree = cache.under_inspection in
1710 | [] -> cache (* possible because of intros that cleans the cache*)
1711 | a::tl -> let tree = rm_from_th a tree a in
1712 {cache with under_inspection = tl,tree}
1714 auto_clusters flags signature cache (depth-1) status ~use_given_only
1716 let ng = List.length goals in
1717 (* moved inside auto_clusters *)
1718 if ng > flags.maxwidth then begin
1719 debug_print ~depth (lazy "FAIL LOCAL WIDTH");
1720 HLog.warn (sprintf "local width (%u) exceeded: %u"
1722 raise (Gaveup cache.failures)
1723 end else if depth = flags.maxdepth then
1724 raise (Gaveup cache.failures)
1726 let status = NTactics.branch_tac ~force:true status in
1727 let g,gctx, gty = current_goal status in
1728 let ctx,ty = close status g in
1729 let closegty = mk_cic_term ctx ty in
1730 let status, gty = apply_subst status gctx gty in
1731 debug_print ~depth (lazy("Attacking goal " ^
1732 string_of_int g ^ " : "^ppterm status gty));
1733 debug_print ~depth (lazy ("current failures: " ^
1734 string_of_int (List.length (all_elements ctx cache.failures))));
1736 let _,_,metasenv,subst,_ = status#obj in
1737 NCicParamod.is_equation status metasenv subst ctx ty in
1738 (* if the goal is an equality we artificially raise its depth up to
1739 flags.maxdepth - 1 *)
1740 if (not flags.last && is_eq && (depth < (flags.maxdepth -2))) then
1741 (* for efficiency reasons, in this case we severely cripple the
1743 (debug_print ~depth (lazy ("RAISING DEPTH TO " ^ string_of_int (depth+1)));
1744 auto_main flags signature cache (depth+1) status ~use_given_only)
1745 (* check for loops *)
1746 else if is_subsumed depth false status closegty (snd cache.under_inspection) then
1747 (debug_print ~depth (lazy "SUBSUMED");
1748 raise (Gaveup cache.failures))
1749 (* check for failures *)
1750 else if is_subsumed depth true status closegty cache.failures then
1751 (debug_print ~depth (lazy "ALREADY MET");
1752 raise (Gaveup cache.failures))
1754 let new_sig = height_of_goal g status in
1755 if new_sig < signature then
1756 (debug_print ~depth (lazy ("news = " ^ (string_of_int new_sig)));
1757 debug_print ~depth (lazy ("olds = " ^ (string_of_int signature))));
1758 let alternatives, cache =
1759 do_something signature flags status g depth gty cache ~use_given_only in
1762 let l,tree = cache.under_inspection in
1763 let l,tree = closegty::l, add_to_th closegty tree closegty in
1764 {cache with under_inspection = l,tree}
1768 (fun allfailures ((_,t),status) ->
1770 (lazy ("(re)considering goal " ^
1771 (string_of_int g) ^" : "^ppterm status gty));
1772 debug_print (~depth:depth)
1773 (lazy ("Case: " ^ NotationPp.pp_term status t));
1775 if t=Ast.Ident("__whd",None) ||
1776 t=Ast.Ident("__intros",None)
1778 else depth+1,loop_cache in
1779 let cache = add_to_trace status ~depth cache t in
1780 let cache = {cache with failures = allfailures} in
1782 auto_clusters flags signature cache depth status ~use_given_only;
1785 debug_print ~depth (lazy "Failed");
1787 cache.failures alternatives in
1791 let dty = NCic.Appl [NCic.Implicit (`Typeof depth); ty] in
1794 (*prerr_endline ("FAILURE : " ^ ppterm status gty);*)
1795 add_to_th newfail failures closegty
1797 debug_print ~depth (lazy "no more candidates");
1798 raise (Gaveup failures)
1801 let int name l def =
1802 try int_of_string (List.assoc name l)
1803 with Failure _ | Not_found -> def
1806 module AstSet = Set.Make(struct type t = Ast.term let compare = compare end)
1808 let cleanup_trace s trace =
1809 (* removing duplicates *)
1812 (fun acc t -> AstSet.add t acc)
1813 AstSet.empty trace in
1814 let trace = AstSet.elements trace_set
1815 (* filtering facts *)
1819 | Ast.NRef (NReference.Ref (u,_)) -> not (is_a_fact_obj s u)
1825 - auto_params e' una high tactic che prende in input i parametri e poi li
1826 processa nel contesto vuoto calcolando i candidate
1828 - astrarla su una auto_params' che prende in input gia' i candidate e un
1829 nuovo parametro per evitare il calcolo dei candidate locali che invece
1830 diventano vuoti (ovvero: non usare automaticamente tutte le ipotesi, bensi'
1833 - reimplementi la auto_params chiamando la auto_params' con il flag a
1834 false e il vecchio codice per andare da parametri a candiddati
1835 OVVERO: usa tutti le ipotesi locali + candidati globali
1837 - crei un nuovo entry point lowtac che calcola i candidati usando il contesto
1838 corrente e poi fa exec della auto_params' con i candidati e il flag a true
1839 OVVERO: usa solo candidati globali che comprendono ipotesi locali
1842 type auto_params = NTacStatus.tactic_term list option * (string * string) list
1844 (*let auto_tac ~params:(univ,flags) ?(trace_ref=ref []) status =*)
1845 let auto_tac' candidates ~local_candidates ?(use_given_only=false) flags ?(trace_ref=ref []) status =
1846 let oldstatus = status in
1847 let status = (status:> NTacStatus.tac_status) in
1848 let goals = head_goals status#stack in
1849 let status, facts = mk_th_cache status goals in
1850 (* let unit_eq = index_local_equations status#eq_cache status in *)
1851 let cache = init_cache ~facts () in
1852 (* pp_th status facts; *)
1854 NDiscriminationTree.DiscriminationTree.iter status#auto_cache (fun p t ->
1856 NDiscriminationTree.NCicIndexable.string_of_path p ^ " |--> " ^
1857 String.concat "\n " (List.map (
1858 status#ppterm ~metasenv:[] ~context:[] ~subst:[])
1859 (NDiscriminationTree.TermSet.elements t))
1862 let depth = int "depth" flags 3 in
1863 let size = int "size" flags 10 in
1864 let width = int "width" flags 4 (* (3+List.length goals)*) in
1866 (* let goals = List.map (fun i -> (i,P)) goals in *)
1867 let signature = height_of_goals status in
1870 candidates = candidates;
1871 local_candidates = local_candidates;
1877 let initial_time = Unix.gettimeofday() in
1882 ("TIME ELAPSED:"^string_of_float(Unix.gettimeofday()-.initial_time)));
1884 ("Applicative nodes:"^string_of_int !app_counter));
1885 raise (Error (lazy "auto gave up", None)))
1887 let _ = debug_print (lazy("\n\nRound "^string_of_int x^"\n")) in
1888 let flags = { flags with maxdepth = x }
1890 try auto_clusters (~top:true) flags signature cache 0 status ~use_given_only;assert false
1892 try auto_main flags signature cache 0 status;assert false
1895 | Gaveup _ -> up_to (x+1) y
1896 | Proved (s,trace) ->
1897 debug_print (lazy ("proved at depth " ^ string_of_int x));
1898 List.iter (toref incr_uses statistics) trace;
1899 let trace = cleanup_trace s trace in
1900 let _ = debug_print (pptrace status trace) in
1903 | (g,t,k,f,p) :: rest -> (filter_open g,t,k,f,p):: rest
1906 let s = s#set_stack stack in
1908 oldstatus#set_status s
1910 let s = up_to depth depth in
1911 debug_print (print_stat status statistics);
1913 ("TIME ELAPSED:"^string_of_float(Unix.gettimeofday()-.initial_time)));
1915 ("Applicative nodes:"^string_of_int !app_counter));
1919 let candidates_from_ctx univ ctx status =
1924 (* FG: `XTSort here? *)
1925 let status, res = disambiguate status ctx t `XTNone in
1926 let _,res = term_of_cic_term status res (ctx_of res)
1928 in Some (List.map to_Ast l)
1929 (* FG: adding these lemmas to (List.map to_Ast l) slows auto very much in some cases
1930 @ [Ast.Ident("refl",None); Ast.Ident("sym_eq",None);
1931 Ast.Ident("trans_eq",None); Ast.Ident("eq_f",None);
1932 Ast.Ident("eq_f2",None); Ast.Ident("eq_f3",None);
1933 Ast.Ident("rewrite_r",None); Ast.Ident("rewrite_l",None)
1937 let auto_lowtac ~params:(univ,flags) status goal =
1938 let gty = get_goalty status goal in
1939 let ctx = ctx_of gty in
1940 let candidates = candidates_from_ctx univ ctx status in
1941 auto_tac' candidates ~local_candidates:true ~use_given_only:false flags ~trace_ref:(ref [])
1943 let auto_tac ~params:(univ,flags) ?(trace_ref=ref []) status =
1944 let candidates = candidates_from_ctx univ [] status in
1945 auto_tac' candidates ~local_candidates:true ~use_given_only:false flags ~trace_ref status
1947 let auto_tac ~params:(_,flags as params) ?trace_ref =
1948 if List.mem_assoc "demod" flags then
1950 else if List.mem_assoc "paramod" flags then
1952 else if List.mem_assoc "fast_paramod" flags then
1953 fast_eq_check_tac ~params
1954 else auto_tac ~params ?trace_ref