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_______________________________________________________________ *)
15 let debug_print ?(depth=0) s =
17 if !debug then prerr_endline (String.make depth '\t'^Lazy.force s) else ()
19 (* let print = debug_print *)
20 let print ?(depth=0) s = ()
22 prerr_endline (String.make depth '\t'^Lazy.force s)
25 let debug_do f = if !debug then f () else ()
27 open Continuationals.Stack
29 module Ast = CicNotationPt
30 let app_counter = ref 0
32 (* ======================= utility functions ========================= *)
33 module IntSet = Set.Make(struct type t = int let compare = compare end)
35 let get_sgoalty status g =
36 let _,_,metasenv,subst,_ = status#obj in
38 let _, ctx, ty = NCicUtils.lookup_meta g metasenv in
39 let ty = NCicUntrusted.apply_subst subst ctx ty in
40 let ctx = NCicUntrusted.apply_subst_context
41 ~fix_projections:true subst ctx
43 NTacStatus.mk_cic_term ctx ty
44 with NCicUtils.Meta_not_found _ as exn -> fail ~exn (lazy "get_sgoalty")
48 let gty = get_sgoalty status g in
49 metas_of_term status gty
52 let menv_closure status gl =
53 let rec closure acc = function
55 | x::l when IntSet.mem x acc -> closure acc l
56 | x::l -> closure (IntSet.add x acc) (deps status x @ l)
57 in closure IntSet.empty gl
60 (* we call a "fact" an object whose hypothesis occur in the goal
61 or in types of goal-variables *)
62 let is_a_fact status ty =
63 let status, ty, metas = saturate ~delta:0 status ty in
64 debug_print (lazy ("saturated ty :" ^ (ppterm status ty)));
65 let g_metas = metas_of_term status ty in
66 let clos = menv_closure status g_metas in
67 (* let _,_,metasenv,_,_ = status#obj in *)
71 let _, m = term_of_cic_term status m (ctx_of m) in
73 | NCic.Meta(i,_) -> IntSet.add i acc
76 in IntSet.subset menv clos;;
78 let is_a_fact_obj s uri =
79 let obj = NCicEnvironment.get_checked_obj uri in
81 | (_,_,[],[],NCic.Constant(_,_,Some(t),ty,_)) ->
82 is_a_fact s (mk_cic_term [] ty)
83 (* aggiungere i costruttori *)
86 let is_a_fact_ast status subst metasenv ctx cand =
88 (lazy ("------- checking " ^ CicNotationPp.pp_term cand));
89 let status, t = disambiguate status ctx ("",0,cand) None in
90 let status,t = term_of_cic_term status t ctx in
91 let ty = NCicTypeChecker.typeof subst metasenv ctx t in
92 is_a_fact status (mk_cic_term ctx ty)
94 let current_goal status =
95 let open_goals = head_goals status#stack in
96 assert (List.length open_goals = 1);
97 let open_goal = List.hd open_goals in
98 let gty = get_goalty status open_goal in
99 let ctx = ctx_of gty in
103 (* =============================== paramod =========================== *)
104 let solve fast status eq_cache goal =
106 if fast then NCicParamod.fast_eq_check
107 else NCicParamod.paramod in
108 let n,h,metasenv,subst,o = status#obj in
109 let gname, ctx, gty = List.assoc goal metasenv in
110 let gty = NCicUntrusted.apply_subst subst ctx gty in
111 let build_status (pt, _, metasenv, subst) =
113 debug_print (lazy ("refining: "^(NCicPp.ppterm ctx subst metasenv pt)));
114 let stamp = Unix.gettimeofday () in
115 let metasenv, subst, pt, pty =
116 NCicRefiner.typeof status
117 (* (status#set_coerc_db NCicCoercion.empty_db) *)
118 metasenv subst ctx pt None in
119 debug_print (lazy ("refined: "^(NCicPp.ppterm ctx subst metasenv pt)));
120 debug_print (lazy ("synt: "^(NCicPp.ppterm ctx subst metasenv pty)));
121 let metasenv, subst =
122 NCicUnification.unify status metasenv subst ctx gty pty
123 (* the previous code is much less expensive than directly refining
124 pt with expected type pty
126 prerr_endline ("exp: "^(NCicPp.ppterm ctx subst metasenv gty));
128 (status#set_coerc_db NCicCoercion.empty_db)
129 metasenv subst ctx pt (Some gty) *)
131 debug_print (lazy (Printf.sprintf "Refined in %fs"
132 (Unix.gettimeofday() -. stamp)));
133 let status = status#set_obj (n,h,metasenv,subst,o) in
134 let metasenv = List.filter (fun j,_ -> j <> goal) metasenv in
135 let subst = (goal,(gname,ctx,pt,pty)) :: subst in
136 Some (status#set_obj (n,h,metasenv,subst,o))
138 NCicRefiner.RefineFailure msg
139 | NCicRefiner.Uncertain msg ->
140 debug_print (lazy ("WARNING: refining in fast_eq_check failed" ^
141 snd (Lazy.force msg))); None
142 | NCicRefiner.AssertFailure msg ->
143 debug_print (lazy ("WARNING: refining in fast_eq_check failed" ^
144 Lazy.force msg)); None
147 HExtlib.filter_map build_status
148 (f status metasenv subst ctx eq_cache (NCic.Rel ~-1,gty))
151 let fast_eq_check eq_cache status goal =
152 match solve true status eq_cache goal with
153 | [] -> raise (Error (lazy "no proof found",None))
157 let dist_fast_eq_check eq_cache s =
158 NTactics.distribute_tac (fast_eq_check eq_cache) s
161 let auto_eq_check eq_cache status =
163 let s = dist_fast_eq_check eq_cache status in
169 (* warning: ctx is supposed to be already instantiated w.r.t subst *)
170 let index_local_equations eq_cache status =
171 let open_goals = head_goals status#stack in
172 let open_goal = List.hd open_goals in
173 let ngty = get_goalty status open_goal in
174 let ctx = ctx_of ngty in
179 let t = NCic.Rel !c in
181 let ty = NCicTypeChecker.typeof [] [] ctx t in
182 if is_a_fact status (mk_cic_term ctx ty) then
183 (debug_print(lazy("eq indexing " ^ (NCicPp.ppterm ctx [] [] ty)));
184 NCicParamod.forward_infer_step eq_cache t ty)
186 (debug_print (lazy ("not a fact: " ^ (NCicPp.ppterm ctx [] [] ty)));
189 | NCicTypeChecker.TypeCheckerFailure _
190 | NCicTypeChecker.AssertFailure _ -> eq_cache)
194 let fast_eq_check_tac ~params s =
195 let unit_eq = index_local_equations s#eq_cache s in
196 dist_fast_eq_check unit_eq s
199 let paramod eq_cache status goal =
200 match solve false status eq_cache goal with
201 | [] -> raise (Error (lazy "no proof found",None))
205 let paramod_tac ~params s =
206 let unit_eq = index_local_equations s#eq_cache s in
207 NTactics.distribute_tac (paramod unit_eq) s
211 let fast_eq_check_tac_all ~params eq_cache status =
212 let g,_,_ = current_goal status in
213 let allstates = fast_eq_check_all status eq_cache g in
214 let pseudo_low_tac s _ _ = s in
215 let pseudo_low_tactics =
216 List.map pseudo_low_tac allstates
218 List.map (fun f -> NTactics.distribute_tac f status) pseudo_low_tactics
223 let demod status eq_cache goal =
224 let n,h,metasenv,subst,o = status#obj in
225 let gname, ctx, gty = List.assoc goal metasenv in
226 let gty = NCicUntrusted.apply_subst subst ctx gty in
228 let demod_tac ~params s =
229 let unit_eq = index_local_equations s#eq_cache s in
230 dist_fast_eq_check unit_eq s
233 (*************** subsumption ****************)
235 let close_wrt_context =
239 | name, NCic.Decl t -> NCic.Prod(name,t,ty)
240 | name, NCic.Def(bo, _) -> NCicSubstitution.subst bo ty)
243 let args_for_context ?(k=1) ctx =
246 (fun (n,l) ctx_entry ->
248 | name, NCic.Decl t -> n+1,NCic.Rel(n)::l
249 | name, NCic.Def(bo, _) -> n+1,l)
253 let constant_for_meta ctx ty i =
254 let name = "cic:/foo"^(string_of_int i)^".con" in
255 let uri = NUri.uri_of_string name in
256 let ty = close_wrt_context ty ctx in
257 (* prerr_endline (NCicPp.ppterm [] [] [] ty); *)
258 let attr = (`Generated,`Definition,`Local) in
259 let obj = NCic.Constant([],name,None,ty,attr) in
260 (* Constant of relevance * string * term option * term * c_attr *)
264 let refresh metasenv =
266 (fun (metasenv,subst) (i,(iattr,ctx,ty)) ->
267 let ikind = NCicUntrusted.kind_of_meta iattr in
268 let metasenv,j,instance,ty =
269 NCicMetaSubst.mk_meta ~attrs:iattr
270 metasenv ctx ~with_type:ty ikind in
271 let s_entry = i,(iattr, ctx, instance, ty) in
272 let metasenv = List.filter (fun x,_ -> i <> x) metasenv in
273 metasenv,s_entry::subst)
274 (metasenv,[]) metasenv
276 (* close metasenv returns a ground instance of all the metas in the
277 metasenv, insantiatied with axioms, and the list of these axioms *)
278 let close_metasenv metasenv subst =
280 let metasenv = NCicUntrusted.apply_subst_metasenv subst metasenv in
282 let metasenv = NCicUntrusted.sort_metasenv subst metasenv in
284 (fun (subst,objs) (i,(iattr,ctx,ty)) ->
285 let ty = NCicUntrusted.apply_subst subst ctx ty in
287 NCicUntrusted.apply_subst_context ~fix_projections:true
289 let (uri,_,_,_,obj) as okind =
290 constant_for_meta ctx ty i in
292 NCicEnvironment.check_and_add_obj okind;
293 let iref = NReference.reference_of_spec uri NReference.Decl in
295 let args = args_for_context ctx in
296 if args = [] then NCic.Const iref
297 else NCic.Appl(NCic.Const iref::args)
299 (* prerr_endline (NCicPp.ppterm ctx [] [] iterm); *)
300 let s_entry = i, ([], ctx, iterm, ty)
301 in s_entry::subst,okind::objs
302 with _ -> assert false)
306 let ground_instances status gl =
307 let _,_,metasenv,subst,_ = status#obj in
308 let subset = menv_closure status gl in
309 let submenv = List.filter (fun (x,_) -> IntSet.mem x subset) metasenv in
311 let submenv = metasenv in
313 let subst, objs = close_metasenv submenv subst in
317 let (_, ctx, t, _) = List.assoc i subst in
318 debug_print (lazy (NCicPp.ppterm ctx [] [] t));
320 (fun (uri,_,_,_,_) as obj ->
321 NCicEnvironment.invalidate_item (`Obj (uri, obj)))
326 Not_found -> assert false
330 let replace_meta i args target =
331 let rec aux k = function
332 (* TODO: local context *)
333 | NCic.Meta (j,lc) when i = j ->
337 List.map (NCicSubstitution.subst_meta lc) args in
338 NCic.Appl(NCic.Rel k::args))
339 | NCic.Meta (j,lc) as m ->
346 aux k (NCicSubstitution.lift n t)) l))))
347 | t -> NCicUtils.map (fun _ k -> k+1) k aux t
352 let close_wrt_metasenv subst =
354 (fun ty (i,(iattr,ctx,mty)) ->
355 let mty = NCicUntrusted.apply_subst subst ctx mty in
357 NCicUntrusted.apply_subst_context ~fix_projections:true
359 let cty = close_wrt_context mty ctx in
360 let name = "foo"^(string_of_int i) in
361 let ty = NCicSubstitution.lift 1 ty in
362 let args = args_for_context ~k:1 ctx in
363 (* prerr_endline (NCicPp.ppterm ctx [] [] iterm); *)
364 let ty = replace_meta i args ty
366 NCic.Prod(name,cty,ty))
370 let _,_,metasenv,subst,_ = status#obj in
371 let subset = menv_closure status [g] in
372 let subset = IntSet.remove g subset in
373 let elems = IntSet.elements subset in
374 let _, ctx, ty = NCicUtils.lookup_meta g metasenv in
375 let ty = NCicUntrusted.apply_subst subst ctx ty in
376 debug_print (lazy ("metas in " ^ (NCicPp.ppterm ctx [] metasenv ty)));
377 debug_print (lazy (String.concat ", " (List.map string_of_int elems)));
378 let submenv = List.filter (fun (x,_) -> IntSet.mem x subset) metasenv in
379 let submenv = List.rev (NCicUntrusted.sort_metasenv subst submenv) in
381 let submenv = metasenv in
383 let ty = close_wrt_metasenv subst ty submenv in
384 debug_print (lazy (NCicPp.ppterm ctx [] [] ty));
390 (* =================================== auto =========================== *)
391 (****************** AUTO ********************
393 let calculate_timeout flags =
394 if flags.timeout = 0. then
395 (debug_print (lazy "AUTO WITH NO TIMEOUT");
396 {flags with timeout = infinity})
400 let is_equational_case goalty flags =
401 let ensure_equational t =
402 if is_an_equational_goal t then true
405 (flags.use_paramod && is_an_equational_goal goalty) ||
406 (flags.use_only_paramod && ensure_equational goalty)
409 type menv = Cic.metasenv
410 type subst = Cic.substitution
411 type goal = ProofEngineTypes.goal * int * AutoTypes.sort
412 let candidate_no = ref 0;;
413 type candidate = int * Cic.term Lazy.t
414 type cache = AutoCache.cache
417 (* the goal (mainly for depth) and key of the goal *)
418 goal * AutoCache.cache_key
420 (* goal has to be proved *)
422 (* goal has to be cached as a success obtained using candidate as the first
424 | S of goal * AutoCache.cache_key * candidate * int
426 (* menv, subst, size, operations done (only S), operations to do, failures to cache if any op fails *)
427 menv * subst * int * op list * op list * fail list
429 (* list of computations that may lead to the solution: all op list will
430 * end with the same (S(g,_)) *)
433 (* menv, subst, alternatives, tables, cache *)
434 | Proved of menv * subst * elem list * AutomationCache.tables * cache
435 | Gaveup of AutomationCache.tables * cache
438 (* the status exported to the external observer *)
440 (* context, (goal,candidate) list, and_list, history *)
441 Cic.context * (int * Cic.term * bool * int * (int * Cic.term Lazy.t) list) list *
442 (int * Cic.term * int) list * Cic.term Lazy.t list
445 let rec aux acc = function
446 | (D g)::tl -> aux (acc@[g]) tl
452 let calculate_goal_ty (goalno,_,_) s m =
454 let _,cc,goalty = CicUtil.lookup_meta goalno m in
455 (* XXX applicare la subst al contesto? *)
456 Some (cc, CicMetaSubst.apply_subst s goalty)
457 with CicUtil.Meta_not_found i when i = goalno -> None
460 let calculate_closed_goal_ty (goalno,_,_) s =
462 let cc,_,goalty = List.assoc goalno s in
463 (* XXX applicare la subst al contesto? *)
464 Some (cc, CicMetaSubst.apply_subst s goalty)
469 let pp_status ctx status =
471 let names = Utils.names_of_context ctx in
474 ProofEngineReduction.replace
475 ~equality:(fun a b -> match b with Cic.Meta _ -> true | _ -> false)
476 ~what:[Cic.Rel 1] ~with_what:[Cic.Implicit None] ~where:x
480 let string_of_do m s (gi,_,_ as g) d =
481 match calculate_goal_ty g s m with
482 | Some (_,gty) -> Printf.sprintf "D(%d, %s, %d)" gi (pp gty) d
483 | None -> Printf.sprintf "D(%d, _, %d)" gi d
485 let string_of_s m su k (ci,ct) gi =
486 Printf.sprintf "S(%d, %s, %s, %d)" gi (pp k) (pp (Lazy.force ct)) ci
488 let string_of_ol m su l =
492 | D (g,d,s) -> string_of_do m su (g,d,s) d
493 | S ((gi,_,_),k,c,_) -> string_of_s m su k c gi)
496 let string_of_fl m s fl =
498 (List.map (fun ((i,_,_),ty) ->
499 Printf.sprintf "(%d, %s)" i (pp ty)) fl)
501 let rec aux = function
503 | (m,s,_,_,ol,fl)::tl ->
504 Printf.eprintf "< [%s] ;;; [%s]>\n"
505 (string_of_ol m s ol) (string_of_fl m s fl);
508 Printf.eprintf "-------------------------- status -------------------\n";
510 Printf.eprintf "-----------------------------------------------------\n";
513 let auto_status = ref [] ;;
514 let auto_context = ref [];;
515 let in_pause = ref false;;
516 let pause b = in_pause := b;;
517 let cond = Condition.create ();;
518 let mutex = Mutex.create ();;
519 let hint = ref None;;
520 let prune_hint = ref [];;
522 let step _ = Condition.signal cond;;
523 let give_hint n = hint := Some n;;
524 let give_prune_hint hint =
525 prune_hint := hint :: !prune_hint
532 Condition.wait cond mutex;
537 let get_auto_status _ =
538 let status = !auto_status in
539 let and_list,elems,last =
542 | (m,s,_,don,gl,fail)::tl ->
545 (fun (id,d,_ as g) ->
546 match calculate_goal_ty g s m with
547 | Some (_,x) -> Some (id,x,d) | None -> None)
551 (* these are the S goalsin the or list *)
554 (fun (m,s,_,don,gl,fail) ->
556 (function S (g,k,c,_) -> Some (g,k,c) | _ -> None)
560 (* this function eats id from a list l::[id,x] returning x, l *)
561 let eat_tail_if_eq id l =
562 let rec aux (s, l) = function
564 | ((id1,_,_),k1,c)::tl when id = id1 ->
566 | None -> aux (Some c,l) tl
567 | Some _ -> assert false)
568 | ((id1,_,_),k1,c as e)::tl -> aux (s, e::l) tl
570 let c, l = aux (None, []) l in
573 let eat_in_parallel id l =
574 let rec aux (b,eaten, new_l as acc) l =
578 match eat_tail_if_eq id l with
579 | None, l -> aux (b@[false], eaten, new_l@[l]) tl
580 | Some t,l -> aux (b@[true],eaten@[t], new_l@[l]) tl
584 let rec eat_all rows l =
588 match List.rev elem with
589 | ((to_eat,depth,_),k,_)::next_lunch ->
590 let b, eaten, l = eat_in_parallel to_eat l in
591 let eaten = HExtlib.list_uniq eaten in
592 let eaten = List.rev eaten in
593 let b = true (* List.hd (List.rev b) *) in
594 let rows = rows @ [to_eat,k,b,depth,eaten] in
596 | [] -> eat_all rows or_list
598 eat_all [] (List.rev orlist)
602 (function (S (_,_,(_,c),_)) -> Some c | _ -> None)
605 (* let rows = List.filter (fun (_,l) -> l <> []) rows in *)
606 and_list, rows, history
608 !auto_context, elems, and_list, last
611 (* Works if there is no dependency over proofs *)
612 let is_a_green_cut goalty =
613 CicUtil.is_meta_closed goalty
615 let rec first_s = function
616 | (D _)::tl -> first_s tl
617 | (S (g,k,c,s))::tl -> Some ((g,k,c,s),tl)
620 let list_union l1 l2 =
621 (* TODO ottimizzare compare *)
622 HExtlib.list_uniq (List.sort compare (l1 @ l1))
624 let rec eq_todo l1 l2 =
626 | (D g1) :: tl1,(D g2) :: tl2 when g1=g2 -> eq_todo tl1 tl2
627 | (S (g1,k1,(c1,lt1),i1)) :: tl1, (S (g2,k2,(c2,lt2),i2)) :: tl2
628 when i1 = i2 && g1 = g2 && k1 = k2 && c1 = c2 ->
629 if Lazy.force lt1 = Lazy.force lt2 then eq_todo tl1 tl2 else false
633 let eat_head todo id fl orlist =
634 let rec aux acc = function
636 | (m, s, _, _, todo1, fl1)::tl as orlist ->
638 match first_s todo1 with
639 | None -> orlist, acc
640 | Some (((gno,_,_),_,_,_), todo11) ->
641 (* TODO confronto tra todo da ottimizzare *)
642 if gno = id && eq_todo todo11 todo then
643 aux (list_union fl1 acc) tl
651 let close_proof p ty menv context =
653 List.map fst (CicUtil.metas_of_term p @ CicUtil.metas_of_term ty)
655 let menv = List.filter (fun (i,_,_) -> List.exists ((=)i) metas) menv in
656 naif_closure p menv context
658 (* XXX capire bene quando aggiungere alla cache *)
659 let add_to_cache_and_del_from_orlist_if_green_cut
660 g s m cache key todo orlist fl ctx size minsize
662 let cache = cache_remove_underinspection cache key in
663 (* prima per fare la irl usavamo il contesto vero e proprio e non quello
665 match calculate_closed_goal_ty g s with
666 | None -> assert false
667 | Some (canonical_ctx , gty) ->
668 let goalno,depth,sort = g in
669 let irl = mk_irl canonical_ctx in
670 let goal = Cic.Meta(goalno, irl) in
671 let proof = CicMetaSubst.apply_subst s goal in
672 let green_proof, closed_proof =
673 let b = is_a_green_cut proof in
675 b, (* close_proof proof gty m ctx *) proof
679 debug_print (lazy ("TENTATIVE CACHE: " ^ CicPp.ppterm key));
680 if is_a_green_cut key then
681 (* if the initia goal was closed, we cut alternatives *)
682 let _ = debug_print (lazy ("MANGIO: " ^ string_of_int goalno)) in
683 let orlist, fl = eat_head todo goalno fl orlist in
685 if size < minsize then
686 (debug_print (lazy ("NO CACHE: 2 (size <= minsize)"));cache)
688 (* if the proof is closed we cache it *)
689 if green_proof then cache_add_success cache key proof
690 else (* cache_add_success cache key closed_proof *)
691 (debug_print (lazy ("NO CACHE: (no gree proof)"));cache)
693 cache, orlist, fl, true
696 debug_print (lazy ("TENTATIVE CACHE: " ^ CicPp.ppterm gty));
697 if size < minsize then
698 (debug_print (lazy ("NO CACHE: (size <= minsize)")); cache) else
699 (* if the substituted goal and the proof are closed we cache it *)
700 if is_a_green_cut gty then
701 if green_proof then cache_add_success cache gty proof
702 else (* cache_add_success cache gty closed_proof *)
703 (debug_print (lazy ("NO CACHE: (no green proof (gty))"));cache)
707 CicTypeChecker.type_of_aux' ~subst:s
708 m ctx closed_proof CicUniv.oblivion_ugraph
710 if is_a_green_cut ty then
711 cache_add_success cache ty closed_proof
714 | CicTypeChecker.TypeCheckerFailure _ ->*)
715 (debug_print (lazy ("NO CACHE: (no green gty )"));cache)
717 cache, orlist, fl, false
719 let close_failures (fl : fail list) (cache : cache) =
721 (fun cache ((gno,depth,_),gty) ->
722 if CicUtil.is_meta_closed gty then
723 ( debug_print (lazy ("FAIL: INDUCED: " ^ string_of_int gno));
724 cache_add_failure cache gty depth)
729 let put_in_subst subst metasenv (goalno,_,_) canonical_ctx t ty =
730 let entry = goalno, (canonical_ctx, t,ty) in
731 assert_subst_are_disjoint subst [entry];
732 let subst = entry :: subst in
734 let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
739 let mk_fake_proof metasenv subst (goalno,_,_) goalty context =
740 None,metasenv,subst ,(lazy (Cic.Meta(goalno,mk_irl context))),goalty, []
744 tables cache depth fake_proof goalno goalty subst context
747 let active,passive,bag = tables in
748 let ppterm = ppterm context in
749 let status = (fake_proof,goalno) in
750 if flags.use_only_paramod then
752 debug_print (lazy ("PARAMODULATION SU: " ^
753 string_of_int goalno ^ " " ^ ppterm goalty ));
754 let goal_steps, saturation_steps, timeout =
755 max_int,max_int,flags.timeout
758 Saturation.given_clause bag status active passive
759 goal_steps saturation_steps timeout
761 | None, active, passive, bag ->
762 [], (active,passive,bag), cache, flags
763 | Some(subst',(_,metasenv,_subst,proof,_, _),open_goals),active,
765 assert_subst_are_disjoint subst subst';
766 let subst = subst@subst' in
768 order_new_goals metasenv subst open_goals ppterm
771 List.map (fun (x,sort) -> x,depth-1,sort) open_goals
774 [(!candidate_no,proof),metasenv,subst,open_goals],
775 (active,passive,bag), cache, flags
779 debug_print (lazy ("NARROWING DEL GOAL: " ^
780 string_of_int goalno ^ " " ^ ppterm goalty ));
781 let goal_steps, saturation_steps, timeout =
785 Saturation.solve_narrowing bag status active passive goal_steps
787 | None, active, passive, bag ->
788 [], (active,passive,bag), cache, flags
789 | Some(subst',(_,metasenv,_subst,proof,_, _),open_goals),active,
791 assert_subst_are_disjoint subst subst';
792 let subst = subst@subst' in
794 order_new_goals metasenv subst open_goals ppterm
797 List.map (fun (x,sort) -> x,depth-1,sort) open_goals
800 [(!candidate_no,proof),metasenv,subst,open_goals],
801 (active,passive,bag), cache, flags
805 let params = ([],["use_context","false"]) in
806 let automation_cache = {
807 AutomationCache.tables = tables ;
808 AutomationCache.univ = Universe.empty; }
811 let ((_,metasenv,subst,_,_,_),open_goals) =
813 solve_rewrite ~params ~automation_cache
816 let proof = lazy (Cic.Meta (-1,[])) in
817 [(!candidate_no,proof),metasenv,subst,[]],tables, cache, flags
818 with ProofEngineTypes.Fail _ -> [], tables, cache, flags
820 let res = Saturation.all_subsumed bag status active passive in
823 (fun (subst',(_,metasenv,_subst,proof,_, _),open_goals) ->
824 assert_subst_are_disjoint subst subst';
825 let subst = subst@subst' in
827 order_new_goals metasenv subst open_goals ppterm
830 List.map (fun (x,sort) -> x,depth-1,sort) open_goals
833 (!candidate_no,proof),metasenv,subst,open_goals)
836 res', (active,passive,bag), cache, flags
843 List.sort (fun (_,_,_,l1) (_,_,_,l2) ->
844 let p1 = List.length (prop_only l1) in
845 let p2 = List.length (prop_only l2) in
846 if p1 = p2 then List.length l1 - List.length l2 else p1-p2)
850 let try_candidate dbd
851 goalty tables subst fake_proof goalno depth context cand
853 let ppterm = ppterm context in
855 let actives, passives, bag = tables in
856 let (_,metasenv,subst,_,_,_), open_goals =
857 ProofEngineTypes.apply_tactic
858 (PrimitiveTactics.apply_tac ~term:cand)
861 let tables = actives, passives,
862 Equality.push_maxmeta bag
863 (max (Equality.maxmeta bag) (CicMkImplicit.new_meta metasenv subst))
865 debug_print (lazy (" OK: " ^ ppterm cand));
866 let metasenv = CicRefine.pack_coercion_metasenv metasenv in
867 let open_goals = order_new_goals metasenv subst open_goals ppterm in
868 let open_goals = List.map (fun (x,sort) -> x,depth-1,sort) open_goals in
870 Some ((!candidate_no,lazy cand),metasenv,subst,open_goals), tables
872 | ProofEngineTypes.Fail s -> None,tables
873 | CicUnification.Uncertain s -> None,tables
876 let applicative_case dbd
877 tables depth subst fake_proof goalno goalty metasenv context
878 signature universe cache flags
882 | Cic.Appl (hd::tl) ->
883 Cic.Appl (hd :: HExtlib.mk_list (Cic.Meta (0,[])) (List.length tl))
886 let goalty_aux = goalty in
888 get_candidates flags.skip_trie_filtering universe cache goalty_aux
890 (* if the goal is an equality we skip the congruence theorems
892 if is_equational_case goalty flags
893 then List.filter not_default_eq_term candidates
896 let candidates = List.filter (only signature context metasenv) candidates
900 (fun (tables,elems) cand ->
902 try_candidate dbd goalty
903 tables subst fake_proof goalno depth context cand
905 | None, tables -> tables, elems
906 | Some x, tables -> tables, x::elems)
907 (tables,[]) candidates
909 let elems = sort_new_elems elems in
913 let try_smart_candidate dbd
914 goalty tables subst fake_proof goalno depth context cand
916 let ppterm = ppterm context in
918 let params = ([],[]) in
919 let automation_cache = {
920 AutomationCache.tables = tables ;
921 AutomationCache.univ = Universe.empty; }
923 debug_print (lazy ("candidato per " ^ string_of_int goalno
924 ^ ": " ^ CicPp.ppterm cand));
926 let (_,metasenv,subst,_,_,_) = fake_proof in
927 prerr_endline ("metasenv:\n" ^ CicMetaSubst.ppmetasenv [] metasenv);
928 prerr_endline ("subst:\n" ^ CicMetaSubst.ppsubst ~metasenv subst);
930 let ((_,metasenv,subst,_,_,_),open_goals) =
931 apply_smart ~dbd ~term:cand ~params ~automation_cache
934 let metasenv = CicRefine.pack_coercion_metasenv metasenv in
935 let open_goals = order_new_goals metasenv subst open_goals ppterm in
936 let open_goals = List.map (fun (x,sort) -> x,depth-1,sort) open_goals in
938 Some ((!candidate_no,lazy cand),metasenv,subst,open_goals), tables
940 | ProofEngineTypes.Fail s -> None,tables
941 | CicUnification.Uncertain s -> None,tables
944 let smart_applicative_case dbd
945 tables depth subst fake_proof goalno goalty metasenv context signature
950 | Cic.Appl (hd::tl) ->
951 Cic.Appl (hd :: HExtlib.mk_list (Cic.Meta (0,[])) (List.length tl))
954 let smart_candidates =
955 get_candidates flags.skip_trie_filtering universe cache goalty_aux
958 get_candidates flags.skip_trie_filtering universe cache goalty
960 let smart_candidates =
962 (fun x -> not(List.mem x candidates)) smart_candidates
965 (lazy ("smart_candidates" ^ " = " ^
966 (String.concat "\n" (List.map CicPp.ppterm smart_candidates)))) in
967 debug_print debug_msg;
968 let candidates = List.filter (only signature context metasenv) candidates in
969 let smart_candidates =
970 List.filter (only signature context metasenv) smart_candidates
973 let penalty cand depth =
974 if only signature context metasenv cand then depth else ((prerr_endline (
975 "penalizzo " ^ CicPp.ppterm cand));depth -1)
980 (fun (tables,elems) cand ->
982 try_candidate dbd goalty
983 tables subst fake_proof goalno depth context cand
986 (* if normal application fails we try to be smart *)
987 (match try_smart_candidate dbd goalty
988 tables subst fake_proof goalno depth context cand
990 | None, tables -> tables, elems
991 | Some x, tables -> tables, x::elems)
992 | Some x, tables -> tables, x::elems)
993 (tables,[]) candidates
995 let tables, smart_elems =
997 (fun (tables,elems) cand ->
999 try_smart_candidate dbd goalty
1000 tables subst fake_proof goalno depth context cand
1002 | None, tables -> tables, elems
1003 | Some x, tables -> tables, x::elems)
1004 (tables,[]) smart_candidates
1006 let elems = sort_new_elems (elems @ smart_elems) in
1007 elems, tables, cache
1010 let equational_and_applicative_case dbd
1011 signature universe flags m s g gty tables cache context
1013 let goalno, depth, sort = g in
1014 let fake_proof = mk_fake_proof m s g gty context in
1015 if is_equational_case gty flags then
1016 let elems,tables,cache, flags =
1017 equational_case tables cache
1018 depth fake_proof goalno gty s context flags
1020 let more_elems, tables, cache =
1021 if flags.use_only_paramod then
1024 applicative_case dbd
1025 tables depth s fake_proof goalno
1026 gty m context signature universe cache flags
1028 elems@more_elems, tables, cache, flags
1030 let elems, tables, cache =
1031 match LibraryObjects.eq_URI () with
1033 smart_applicative_case dbd tables depth s fake_proof goalno
1034 gty m context signature universe cache flags
1036 applicative_case dbd tables depth s fake_proof goalno
1037 gty m context signature universe cache flags
1039 elems, tables, cache, flags
1041 let rec condition_for_hint i = function
1043 | S (_,_,(j,_),_):: tl -> j <> i (* && condition_for_hint i tl *)
1044 | _::tl -> condition_for_hint i tl
1046 let prunable_for_size flags s m todo =
1047 let rec aux b = function
1048 | (S _)::tl -> aux b tl
1049 | (D (_,_,T))::tl -> aux b tl
1051 (match calculate_goal_ty g s m with
1053 | Some (canonical_ctx, gty) ->
1055 Utils.weight_of_term
1056 ~consider_metas:false ~count_metas_occurrences:true gty in
1057 let newb = b || gsize > flags.maxgoalsizefactor in
1064 let prunable ty todo =
1065 let rec aux b = function
1066 | (S(_,k,_,_))::tl -> aux (b || Equality.meta_convertibility k ty) tl
1067 | (D (_,_,T))::tl -> aux b tl
1075 let prunable menv subst ty todo =
1076 let rec aux = function
1077 | (S(_,k,_,_))::tl ->
1078 (match Equality.meta_convertibility_subst k ty menv with
1081 no_progress variant tl (* || aux tl*))
1082 | (D (_,_,T))::tl -> aux tl
1084 and no_progress variant = function
1085 | [] -> (*prerr_endline "++++++++++++++++++++++++ no_progress";*) true
1086 | D ((n,_,P) as g)::tl ->
1087 (match calculate_goal_ty g subst menv with
1088 | None -> no_progress variant tl
1090 (match calculate_goal_ty g variant menv with
1091 | None -> assert false
1093 if gty = gty' then no_progress variant tl
1095 (prerr_endline (string_of_int n);
1096 prerr_endline (CicPp.ppterm gty);
1097 prerr_endline (CicPp.ppterm gty');
1098 prerr_endline "---------- subst";
1099 prerr_endline (CicMetaSubst.ppsubst ~metasenv:menv subst);
1100 prerr_endline "---------- variant";
1101 prerr_endline (CicMetaSubst.ppsubst ~metasenv:menv variant);
1102 prerr_endline "---------- menv";
1103 prerr_endline (CicMetaSubst.ppmetasenv [] menv);
1104 no_progress variant tl) *)
1106 | _::tl -> no_progress variant tl
1111 let condition_for_prune_hint prune (m, s, size, don, todo, fl) =
1113 HExtlib.filter_map (function S (_,_,(c,_),_) -> Some c | _ -> None) todo
1115 List.for_all (fun i -> List.for_all (fun j -> i<>j) prune) s
1117 let filter_prune_hint c l =
1118 let prune = !prune_hint in
1119 prune_hint := []; (* possible race... *)
1120 if prune = [] then c,l
1122 cache_reset_underinspection c,
1123 List.filter (condition_for_prune_hint prune) l
1129 auto_all_solutions dbd tables universe cache context metasenv gl flags
1134 MetadataConstraints.UriManagerSet.union set
1135 (MetadataQuery.signature_of metasenv g)
1137 MetadataConstraints.UriManagerSet.empty gl
1139 let goals = order_new_goals metasenv [] gl CicPp.ppterm in
1142 (fun (x,s) -> D (x,flags.maxdepth,s)) goals
1144 let elems = [metasenv,[],1,[],goals,[]] in
1145 let rec aux tables solutions cache elems flags =
1146 match auto_main dbd tables context flags signature universe cache elems with
1147 | Gaveup (tables,cache) ->
1148 solutions,cache, tables
1149 | Proved (metasenv,subst,others,tables,cache) ->
1150 if Unix.gettimeofday () > flags.timeout then
1151 ((subst,metasenv)::solutions), cache, tables
1153 aux tables ((subst,metasenv)::solutions) cache others flags
1155 let rc = aux tables [] cache elems flags in
1157 | [],cache,tables -> [],cache,tables
1158 | solutions, cache,tables ->
1161 (fun (subst,newmetasenv) ->
1163 ProofEngineHelpers.compare_metasenvs ~oldmetasenv:metasenv ~newmetasenv
1165 if opened = [] then Some subst else None)
1168 solutions,cache,tables
1171 (******************* AUTO ***************)
1174 let auto dbd flags metasenv tables universe cache context metasenv gl =
1175 let initial_time = Unix.gettimeofday() in
1179 MetadataConstraints.UriManagerSet.union set
1180 (MetadataQuery.signature_of metasenv g)
1182 MetadataConstraints.UriManagerSet.empty gl
1184 let goals = order_new_goals metasenv [] gl CicPp.ppterm in
1185 let goals = List.map (fun (x,s) -> D(x,flags.maxdepth,s)) goals in
1186 let elems = [metasenv,[],1,[],goals,[]] in
1187 match auto_main dbd tables context flags signature universe cache elems with
1188 | Proved (metasenv,subst,_, tables,cache) ->
1190 ("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time)));
1191 Some (subst,metasenv), cache
1192 | Gaveup (tables,cache) ->
1194 ("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time)));
1198 let auto_tac ~(dbd:HSql.dbd) ~params:(univ,params) ~automation_cache (proof, goal) =
1199 let flags = flags_of_params params () in
1200 let use_library = flags.use_library in
1201 let universe, tables, cache =
1202 init_cache_and_tables
1203 ~dbd ~use_library ~use_context:(not flags.skip_context)
1204 automation_cache univ (proof, goal)
1206 let _,metasenv,subst,_,_, _ = proof in
1207 let _,context,goalty = CicUtil.lookup_meta goal metasenv in
1208 let signature = MetadataQuery.signature_of metasenv goal in
1213 CicTypeChecker.type_of_aux' metasenv context t
1214 CicUniv.oblivion_ugraph
1216 MetadataConstraints.UriManagerSet.union set
1217 (MetadataConstraints.constants_of ty)
1222 if flags.close_more then
1224 tables context (proof, goal)
1225 (auto_all_solutions dbd) signature universe cache
1226 else tables,cache in
1227 let initial_time = Unix.gettimeofday() in
1228 let (_,oldmetasenv,_,_,_, _) = proof in
1231 metasenv,subst,1,[],[D (goal,flags.maxdepth,P)],[]
1233 match auto_main dbd tables context flags signature universe cache [elem] with
1234 | Proved (metasenv,subst,_, tables,cache) ->
1236 ("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time)));
1237 let proof,metasenv =
1238 ProofEngineHelpers.subst_meta_and_metasenv_in_proof
1239 proof goal subst metasenv
1242 ProofEngineHelpers.compare_metasenvs ~oldmetasenv
1243 ~newmetasenv:metasenv
1246 | Gaveup (tables,cache) ->
1249 string_of_float(Unix.gettimeofday()-.initial_time)));
1250 raise (ProofEngineTypes.Fail (lazy "Auto gave up"))
1254 (****************** smart application ********************)
1257 let smart_apply t unit_eq status g =
1258 let n,h,metasenv,subst,o = status#obj in
1259 let gname, ctx, gty = List.assoc g metasenv in
1260 (* let ggty = mk_cic_term context gty in *)
1261 let status, t = disambiguate status ctx t None in
1262 let status,t = term_of_cic_term status t ctx in
1263 let ty = NCicTypeChecker.typeof subst metasenv ctx t in
1264 let ty,metasenv,args = NCicMetaSubst.saturate metasenv subst ctx ty 0 in
1265 let metasenv,j,inst,_ = NCicMetaSubst.mk_meta metasenv ctx `IsTerm in
1266 let status = status#set_obj (n,h,metasenv,subst,o) in
1267 let pterm = if args=[] then t else NCic.Appl(t::args) in
1270 NUri.uri_of_string "cic:/matita/ng/Plogic/equality/eq_coerc.con" in
1271 let ref = NReference.reference_of_spec uri (NReference.Def(2)) in
1275 NCic.Appl[eq_coerc;ty;NCic.Implicit `Type;pterm;inst] in
1276 let smart = mk_cic_term ctx smart in
1278 let status = instantiate status g smart in
1279 let _,_,metasenv,subst,_ = status#obj in
1280 let _,ctx,jty = List.assoc j metasenv in
1281 let jty = NCicUntrusted.apply_subst subst ctx jty in
1282 debug_print(lazy("goal " ^ (NCicPp.ppterm ctx [] [] jty)));
1283 fast_eq_check unit_eq status j
1285 | Error _ as e -> debug_print (lazy "error"); raise e
1287 let smart_apply_tac t s =
1288 let unit_eq = index_local_equations s#eq_cache s in
1289 NTactics.distribute_tac (smart_apply t unit_eq) s
1291 let smart_apply_auto t eq_cache =
1292 NTactics.distribute_tac (smart_apply t eq_cache)
1295 (****************** types **************)
1298 type th_cache = (NCic.context * InvRelDiscriminationTree.t) list
1300 let keys_of_term status t =
1301 let status, orig_ty = typeof status (ctx_of t) t in
1302 let _, ty, _ = saturate ~delta:max_int status orig_ty in
1305 let _, ty = term_of_cic_term status ty (ctx_of ty) in
1307 | NCic.Const (NReference.Ref (_,(NReference.Def h | NReference.Fix (_,_,h))))
1308 | NCic.Appl (NCic.Const(NReference.Ref(_,(NReference.Def h | NReference.Fix (_,_,h))))::_)
1310 let _,ty,_= saturate status ~delta:(h-1) orig_ty in
1317 let mk_th_cache status gl =
1319 (fun (status, acc) g ->
1320 let gty = get_goalty status g in
1321 let ctx = ctx_of gty in
1322 debug_print(lazy("th cache for: "^ppterm status gty));
1323 debug_print(lazy("th cache in: "^ppcontext status ctx));
1324 if List.mem_assq ctx acc then status, acc else
1325 let idx = InvRelDiscriminationTree.empty in
1328 (fun (status, i, idx) _ ->
1329 let t = mk_cic_term ctx (NCic.Rel i) in
1330 let status, keys = keys_of_term status t in
1331 debug_print(lazy("indexing: "^ppterm status t ^ ": " ^ string_of_int (List.length keys)));
1333 List.fold_left (fun idx k ->
1334 InvRelDiscriminationTree.index idx k t) idx keys
1337 (status, 1, idx) ctx
1339 status, (ctx, idx) :: acc)
1343 let add_to_th t c ty =
1344 let key_c = ctx_of t in
1345 if not (List.mem_assq key_c c) then
1346 (key_c ,InvRelDiscriminationTree.index
1347 InvRelDiscriminationTree.empty ty t ) :: c
1349 let rec replace = function
1351 | (x, idx) :: tl when x == key_c ->
1352 (x, InvRelDiscriminationTree.index idx ty t) :: tl
1353 | x :: tl -> x :: replace tl
1358 let pp_idx status idx =
1359 InvRelDiscriminationTree.iter idx
1361 debug_print(lazy("K: " ^ NCicInverseRelIndexable.string_of_path k));
1363 (fun t -> debug_print(lazy("\t"^ppterm status t)))
1370 debug_print(lazy( "-----------------------------------------------"));
1371 debug_print(lazy( (NCicPp.ppcontext ~metasenv:[] ~subst:[] ctx)));
1372 debug_print(lazy( "||====> "));
1376 let search_in_th gty th =
1377 let c = ctx_of gty in
1378 let rec aux acc = function
1379 | [] -> (* Ncic_termSet.elements *) acc
1382 let idx = List.assq k th in
1383 let acc = Ncic_termSet.union acc
1384 (InvRelDiscriminationTree.retrieve_unifiables idx gty)
1387 with Not_found -> aux acc tl
1389 aux Ncic_termSet.empty c
1393 do_types : bool; (* solve goals in Type *)
1394 last : bool; (* last goal: take first solution only *)
1402 {facts : th_cache; (* positive results *)
1403 under_inspection : th_cache; (* to prune looping *)
1404 unit_eq : NCicParamod.state
1408 type goal = int * sort (* goal, depth, sort *)
1409 type fail = goal * cic_term
1410 type candidate = int * Ast.term (* unique candidate number, candidate *)
1412 exception Gaveup of IntSet.t (* a sublist of unprovable conjunctive
1413 atoms of the input goals *)
1414 exception Proved of NTacStatus.tac_status
1416 let height_of_ref (NReference.Ref (uri, x)) =
1421 | NReference.CoFix _ ->
1422 let _,height,_,_,_ = NCicEnvironment.get_checked_obj uri in
1424 | NReference.Def h -> h
1425 | NReference.Fix (_,_,h) -> h
1428 let fast_height_of_term t =
1432 NCic.Meta (_,(_,NCic.Ctx l)) -> List.iter aux l
1436 | NCic.Implicit _ -> assert false
1437 | NCic.Const nref as t ->
1439 prerr_endline (NCicPp.ppterm ~metasenv:[] ~subst:[]
1440 ~context:[] t ^ ":" ^ string_of_int (height_of_ref nref));
1442 h := max !h (height_of_ref nref)
1443 | NCic.Prod (_,t1,t2)
1444 | NCic.Lambda (_,t1,t2) -> aux t1; aux t2
1445 | NCic.LetIn (_,s,ty,t) -> aux s; aux ty; aux t
1446 | NCic.Appl l -> List.iter aux l
1447 | NCic.Match (_,outty,t,pl) -> aux outty; aux t; List.iter aux pl
1452 let height_of_goals status =
1453 let open_goals = head_goals status#stack in
1454 assert (List.length open_goals > 0);
1458 let ty = get_goalty status open_goal in
1459 let context = ctx_of ty in
1460 let _, ty = term_of_cic_term status ty (ctx_of ty) in
1461 h := max !h (fast_height_of_term ty);
1464 | _, NCic.Decl ty -> h := max !h (fast_height_of_term ty)
1465 | _, NCic.Def (bo,ty) ->
1466 h := max !h (fast_height_of_term ty);
1467 h := max !h (fast_height_of_term bo);
1471 prerr_endline ("altezza sequente: " ^ string_of_int !h);
1475 (* let close_failures _ c = c;; *)
1476 (* let prunable _ _ _ = false;; *)
1477 (* let cache_examine cache gty = `Notfound;; *)
1478 (* let put_in_subst s _ _ _ = s;; *)
1479 (* let add_to_cache_and_del_from_orlist_if_green_cut _ _ c _ _ o f _ = c, o, f, false ;; *)
1480 (* let cache_add_underinspection c _ _ = c;; *)
1482 let init_cache ?(facts=[]) ?(under_inspection=[])
1483 ?(unit_eq=NCicParamod.empty_state) _ =
1485 under_inspection = under_inspection;
1489 let only signature _context candidate =
1490 (* TASSI: nel trie ci mettiamo solo il body, non il ty *)
1492 NCicTypeChecker.typeof ~subst:[] ~metasenv:[] [] candidate
1494 let height = fast_height_of_term candidate_ty in
1495 let rc = signature >= height in
1497 prerr_endline ("Filtro: " ^ NCicPp.ppterm ~context:[] ~subst:[]
1498 ~metasenv:[] candidate ^ ": " ^ string_of_int height)
1500 prerr_endline ("Tengo: " ^ NCicPp.ppterm ~context:[] ~subst:[]
1501 ~metasenv:[] candidate ^ ": " ^ string_of_int height);
1506 let candidate_no = ref 0;;
1508 let openg_no status = List.length (head_goals status#stack)
1510 let sort_new_elems l =
1511 List.sort (fun (_,s1) (_,s2) -> openg_no s1 - openg_no s2) l
1513 let try_candidate ?(smart=0) flags depth status eq_cache t =
1515 debug_print ~depth (lazy ("------------ try " ^ CicNotationPp.pp_term t));
1517 if smart= 0 then NTactics.apply_tac ("",0,t) status
1518 else if smart = 1 then smart_apply_auto ("",0,t) eq_cache status
1519 else (* smart = 2: both *)
1520 try NTactics.apply_tac ("",0,t) status
1522 smart_apply_auto ("",0,t) eq_cache status in
1523 let og_no = openg_no status in
1524 if (* og_no > flags.maxwidth || *)
1525 ((depth + 1) = flags.maxdepth && og_no <> 0) then
1526 (debug_print ~depth (lazy "pruned immediately"); None)
1529 Some ((!candidate_no,t),status))
1530 with Error (msg,exn) -> debug_print ~depth (lazy "failed"); None
1533 let get_candidates ?(smart=true) status cache signature gty =
1534 let universe = status#auto_cache in
1535 let context = ctx_of gty in
1537 let _status, t = term_of_cic_term status t context
1539 let c_ast = function
1540 | NCic.Const r -> Ast.NRef r | _ -> assert false in
1541 let _, raw_gty = term_of_cic_term status gty context in
1542 let cands = NDiscriminationTree.DiscriminationTree.retrieve_unifiables
1544 let local_cands = search_in_th gty cache in
1545 let together global local =
1547 (List.filter (only signature context)
1548 (NDiscriminationTree.TermSet.elements global)) @
1549 List.map t_ast (Ncic_termSet.elements local) in
1550 let candidates = together cands local_cands in
1551 let smart_candidates =
1554 | NCic.Appl (hd::tl) ->
1556 NCic.Appl (hd:: HExtlib.mk_list(NCic.Meta (0,(0,NCic.Irl 0)))
1557 (List.length tl)) in
1559 NDiscriminationTree.DiscriminationTree.retrieve_unifiables
1560 universe weak_gty in
1562 NDiscriminationTree.TermSet.diff more_cands cands in
1563 let cic_weak_gty = mk_cic_term context weak_gty in
1564 let more_local_cands = search_in_th cic_weak_gty cache in
1565 let smart_local_cands =
1566 Ncic_termSet.diff more_local_cands local_cands in
1567 together smart_cands smart_local_cands
1571 candidates, smart_candidates
1574 let applicative_case depth signature status flags gty (cache:cache) =
1575 app_counter:= !app_counter+1;
1576 let _,_,metasenv,subst,_ = status#obj in
1577 let context = ctx_of gty in
1578 let tcache = cache.facts in
1580 let status, t = term_of_cic_term status gty context in
1581 NCicParamod.is_equation metasenv subst context t
1583 debug_print(lazy (string_of_bool is_eq));
1584 let candidates, smart_candidates =
1585 get_candidates ~smart:(not is_eq) status tcache signature gty in
1587 (lazy ("candidates: " ^ string_of_int (List.length candidates)));
1589 (lazy ("smart candidates: " ^
1590 string_of_int (List.length smart_candidates)));
1593 let smart_candidates = [] in *)
1594 let sm = if is_eq then 0 else 2 in
1595 let maxd = ((depth + 1) = flags.maxdepth) in
1596 let only_one = flags.last && maxd in
1597 debug_print (lazy ("only_one: " ^ (string_of_bool only_one)));
1598 debug_print (lazy ("maxd: " ^ (string_of_bool maxd)));
1602 if (only_one && (elems <> [])) then elems
1604 if (maxd && not(is_a_fact_ast status subst metasenv context cand))
1605 then (debug_print (lazy "pruned: not a fact"); elems)
1607 match try_candidate (~smart:sm)
1608 flags depth status cache.unit_eq cand with
1610 | Some x -> x::elems)
1614 if only_one && elems <> [] then elems
1618 if (only_one && (elems <> [])) then elems
1620 if (maxd && not(is_a_fact_ast status subst metasenv context cand))
1621 then (debug_print (lazy "pruned: not a fact"); elems)
1623 match try_candidate (~smart:1)
1624 flags depth status cache.unit_eq cand with
1626 | Some x -> x::elems)
1635 (* gty is supposed to be meta-closed *)
1636 let is_subsumed depth status gty cache =
1637 if cache=[] then false else (
1638 debug_print ~depth (lazy("Subsuming " ^ (ppterm status gty)));
1639 let n,h,metasenv,subst,obj = status#obj in
1640 let ctx = ctx_of gty in
1641 let _ , target = term_of_cic_term status gty ctx in
1642 let target = NCicSubstitution.lift 1 target in
1643 (* candidates must only be searched w.r.t the given context *)
1646 let idx = List.assq ctx cache in
1647 Ncic_termSet.elements
1648 (InvRelDiscriminationTree.retrieve_generalizations idx gty)
1649 with Not_found -> []
1652 (lazy ("failure candidates: " ^ string_of_int (List.length candidates)));
1656 let _ , source = term_of_cic_term status t ctx in
1658 NCic.Prod("foo",source,target) in
1659 let metasenv,j,_,_ =
1660 NCicMetaSubst.mk_meta
1661 metasenv ctx ~with_type:implication `IsType in
1662 let status = status#set_obj (n,h,metasenv,subst,obj) in
1663 let status = status#set_stack [([1,Open j],[],[],`NoTag)] in
1665 let status = NTactics.intro_tac "foo" status in
1667 NTactics.apply_tac ("",0,Ast.NCic (NCic.Rel 1)) status
1669 if (head_goals status#stack = []) then raise Found
1674 with Found -> debug_print ~depth (lazy "success");true)
1677 let rec guess_name name ctx =
1678 if name = "_" then guess_name "auto" ctx else
1679 if not (List.mem_assoc name ctx) then name else
1680 guess_name (name^"'") ctx
1683 let is_prod status =
1684 let _, ctx, gty = current_goal status in
1685 let _, raw_gty = term_of_cic_term status gty ctx in
1687 | NCic.Prod (name,_,_) -> Some (guess_name name ctx)
1690 let intro ~depth status facts name =
1691 let status = NTactics.intro_tac name status in
1692 let _, ctx, ngty = current_goal status in
1693 let t = mk_cic_term ctx (NCic.Rel 1) in
1694 let status, keys = keys_of_term status t in
1695 let facts = List.fold_left (add_to_th t) facts keys in
1696 debug_print ~depth (lazy ("intro: "^ name));
1697 (* unprovability is not stable w.r.t introduction *)
1701 let rec intros_facts ~depth status facts =
1702 match is_prod status with
1705 intro ~depth status facts name
1706 in intros_facts ~depth status facts
1707 | _ -> status, facts
1710 let rec intros ~depth status (cache:cache) =
1711 match is_prod status with
1714 intros_facts ~depth status cache.facts
1716 (* we reindex the equation from scratch *)
1718 index_local_equations status#eq_cache status in
1719 (* under_inspection must be set to empty *)
1720 status, init_cache ~facts ~unit_eq ()
1721 | _ -> status, cache
1724 let reduce ~depth status g =
1725 let n,h,metasenv,subst,o = status#obj in
1726 let attr, ctx, ty = NCicUtils.lookup_meta g metasenv in
1727 let ty = NCicUntrusted.apply_subst subst ctx ty in
1728 let ty' = NCicReduction.whd ~subst ctx ty in
1732 (lazy ("reduced to: "^ NCicPp.ppterm ctx subst metasenv ty'));
1734 (g,(attr,ctx,ty'))::(List.filter (fun (i,_) -> i<>g) metasenv)
1736 let status = status#set_obj (n,h,metasenv,subst,o) in
1738 [(!candidate_no,Ast.Ident("__whd",None)),status])
1741 let do_something signature flags status g depth gty cache =
1743 let l = reduce ~depth status g in
1744 (* backward aplications *)
1749 ((!candidate_no,Ast.Ident("__paramod",None)),s))
1750 (auto_eq_check cache.unit_eq status) in
1752 if (l1 <> []) then []
1753 else applicative_case depth signature status flags gty cache
1754 (* fast paramodulation *)
1756 (* states in l1 have have an empty set of subgoals: no point to sort them *)
1757 l1 @ (sort_new_elems (l@l2)), cache
1760 let pp_goal = function
1761 | (_,Continuationals.Stack.Open i)
1762 | (_,Continuationals.Stack.Closed i) -> string_of_int i
1765 let pp_goals status l =
1769 let gty = get_goalty status i in
1770 NTacStatus.ppterm status gty)
1777 let compare = Pervasives.compare
1781 module MS = HTopoSort.Make(M)
1784 let sort_tac status =
1786 match status#stack with
1787 | [] -> assert false
1788 | (goals, t, k, tag) :: s ->
1789 let g = head_goals status#stack in
1791 (List.rev (MS.topological_sort g (deps status))) in
1792 debug_print (lazy ("old g = " ^
1793 String.concat "," (List.map string_of_int g)));
1794 debug_print (lazy ("sorted goals = " ^
1795 String.concat "," (List.map string_of_int sortedg)));
1796 let is_it i = function
1797 | (_,Continuationals.Stack.Open j )
1798 | (_,Continuationals.Stack.Closed j ) -> i = j
1801 List.map (fun i -> List.find (is_it i) goals) sortedg
1803 (sorted_goals, t, k, tag) :: s
1805 status#set_stack gstatus
1808 let clean_up_tac status =
1810 match status#stack with
1811 | [] -> assert false
1812 | (g, t, k, tag) :: s ->
1813 let is_open = function
1814 | (_,Continuationals.Stack.Open _) -> true
1815 | (_,Continuationals.Stack.Closed _) -> false
1817 let g' = List.filter is_open g in
1818 (g', t, k, tag) :: s
1820 status#set_stack gstatus
1823 let focus_tac focus status =
1825 match status#stack with
1826 | [] -> assert false
1827 | (g, t, k, tag) :: s ->
1828 let in_focus = function
1829 | (_,Continuationals.Stack.Open i)
1830 | (_,Continuationals.Stack.Closed i) -> List.mem i focus
1832 let focus,others = List.partition in_focus g
1834 (* we need to mark it as a BranchTag, otherwise cannot merge later *)
1835 (focus,[],[],`BranchTag) :: (others, t, k, tag) :: s
1837 status#set_stack gstatus
1840 let rec auto_clusters ?(top=false)
1841 flags signature cache depth status : unit =
1842 debug_print ~depth (lazy "entering auto clusters");
1843 (* ignore(Unix.select [] [] [] 0.01); *)
1844 let status = clean_up_tac status in
1845 let goals = head_goals status#stack in
1846 if goals = [] then raise (Proved status)
1847 else if depth = flags.maxdepth then raise (Gaveup IntSet.empty)
1848 else if List.length goals < 2 then
1849 auto_main flags signature cache depth status
1851 debug_print ~depth (lazy ("goals = " ^
1852 String.concat "," (List.map string_of_int goals)));
1853 let classes = HExtlib.clusters (deps status) goals in
1854 let classes = if top then List.rev classes else classes in
1860 ("cluster:" ^ String.concat "," (List.map string_of_int l)))
1864 (fun (status,b) gl ->
1865 let status = focus_tac gl status in
1867 debug_print ~depth (lazy ("focusing on" ^
1868 String.concat "," (List.map string_of_int gl)));
1869 auto_main flags signature cache depth status; assert false
1871 | Proved(status) -> (NTactics.merge_tac status,true)
1872 | Gaveup _ when top -> (NTactics.merge_tac status,b)
1874 (status,false) classes
1875 in if b then raise (Proved status) else raise (Gaveup IntSet.empty)
1879 (* the goals returned upon failure are an unsatisfiable subset
1880 of the initial head goals in the stack *)
1882 auto_main flags signature (cache:cache) depth status: unit =
1883 debug_print ~depth (lazy "entering auto main");
1884 (* ignore(Unix.select [] [] [] 0.01); *)
1885 let status = sort_tac (clean_up_tac status) in
1886 let goals = head_goals status#stack in
1888 | [] -> raise (Proved status)
1890 let ng = List.length goals in
1891 if ng > flags.maxwidth then
1892 (debug_print (lazy "FAIL WIDTH"); raise (Gaveup IntSet.empty))
1893 else let branch = ng>1 in
1894 if depth = flags.maxdepth then raise (Gaveup IntSet.empty)
1897 if branch then NTactics.branch_tac status
1899 let status, cache = intros ~depth status cache in
1900 let g,gctx, gty = current_goal status in
1901 let ctx,ty = close status g in
1902 let closegty = mk_cic_term ctx ty in
1903 let status, gty = apply_subst status gctx gty in
1904 debug_print ~depth (lazy("Attacking goal " ^ (string_of_int g) ^" : "^ppterm status gty));
1905 if is_subsumed depth status closegty cache.under_inspection then
1906 (debug_print (lazy "SUBSUMED");
1907 raise (Gaveup IntSet.add g IntSet.empty))
1910 {flags with last = flags.last && (not branch)} in
1911 let alternatives, cache =
1912 do_something signature do_flags status g depth gty cache in
1914 let under_inspection =
1915 add_to_th closegty cache.under_inspection closegty in
1916 {cache with under_inspection = under_inspection} in
1919 (* the underscore information does not need to be returned
1921 (fun unsat ((_,t),status) ->
1922 let depth',looping_cache =
1923 if t=Ast.Ident("__whd",None) then depth,cache
1924 else depth+1, loop_cache in
1925 debug_print (~depth:depth')
1926 (lazy ("Case: " ^ CicNotationPp.pp_term t));
1928 {flags with maxwidth = flags.maxwidth - ng +1} in
1931 {flags' with last = flags'.last && (not branch)} in
1933 (lazy ("auto last: " ^ (string_of_bool flags'.last)));
1934 try auto_clusters flags' signature loop_cache
1935 depth' status; unsat
1938 debug_print (~depth:depth') (lazy "proved");
1940 let status = NTactics.merge_tac status
1942 (* old cache, here *)
1944 {flags with maxwidth = flags.maxwidth - 1} in
1945 try auto_clusters flags signature cache
1946 depth status; assert false
1949 (lazy ("Unsat1 at depth " ^ (string_of_int depth)
1951 (pp_goals status (IntSet.elements f))));
1952 (* TODO: cache failures *)
1953 IntSet.union f unsat
1954 else raise (Proved status)
1956 debug_print (~depth:depth')
1957 (lazy ("Unsat2 at depth " ^ (string_of_int depth')
1959 (pp_goals status (IntSet.elements f))));
1960 (* TODO: cache local failures *)
1962 IntSet.empty alternatives
1964 raise (Gaveup IntSet.add orig unsat)
1967 let int name l def =
1968 try int_of_string (List.assoc name l)
1969 with Failure _ | Not_found -> def
1972 let auto_tac ~params:(_univ,flags) status =
1973 let oldstatus = status in
1974 let status = (status:> NTacStatus.tac_status) in
1975 let goals = head_goals status#stack in
1976 let status, facts = mk_th_cache status goals in
1977 let unit_eq = index_local_equations status#eq_cache status in
1978 let cache = init_cache ~facts ~unit_eq () in
1979 (* pp_th status facts; *)
1981 NDiscriminationTree.DiscriminationTree.iter status#auto_cache (fun p t ->
1983 NDiscriminationTree.NCicIndexable.string_of_path p ^ " |--> " ^
1984 String.concat "\n " (List.map (
1985 NCicPp.ppterm ~metasenv:[] ~context:[] ~subst:[])
1986 (NDiscriminationTree.TermSet.elements t))
1989 let depth = int "depth" flags 3 in
1990 let size = int "size" flags 10 in
1991 let width = int "width" flags 4 (* (3+List.length goals)*) in
1993 (* let goals = List.map (fun i -> (i,P)) goals in *)
1994 let signature = height_of_goals status in
2000 timeout = Unix.gettimeofday() +. 3000.;
2003 let initial_time = Unix.gettimeofday() in
2008 ("TIME ELAPSED:"^string_of_float(Unix.gettimeofday()-.initial_time)));
2010 ("Applicative nodes:"^string_of_int !app_counter));
2011 raise (Error (lazy "auto gave up", None)))
2013 let _ = debug_print (lazy("\n\nRound "^string_of_int x^"\n")) in
2014 let flags = { flags with maxdepth = x }
2016 try auto_clusters (~top:true) flags signature cache 0 status;assert false
2018 | Gaveup _ -> up_to (x+1) y
2020 debug_print (lazy ("proved at depth " ^ string_of_int x));
2023 | (g,t,k,f) :: rest -> (filter_open g,t,k,f):: rest
2026 let s = s#set_stack stack in
2027 oldstatus#set_status s
2029 let s = up_to depth depth in
2031 ("TIME ELAPSED:"^string_of_float(Unix.gettimeofday()-.initial_time)));
2033 ("Applicative nodes:"^string_of_int !app_counter));