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 =
16 if !debug then prerr_endline (String.make depth '\t'^Lazy.force s) else ()
17 (* let print= debug_print *)
18 let print ?(depth=0) s =
19 prerr_endline (String.make depth '\t'^Lazy.force s)
21 let debug_do f = if !debug then f () else ()
23 open Continuationals.Stack
25 module Ast = CicNotationPt
26 let app_counter = ref 0
28 (* =================================== paramod =========================== *)
29 let auto_paramod ~params:(l,_) status goal =
30 let gty = get_goalty status goal in
31 let n,h,metasenv,subst,o = status#obj in
32 let status,t = term_of_cic_term status gty (ctx_of gty) in
36 let status, t = disambiguate status (ctx_of gty) t None in
37 let status, ty = typeof status (ctx_of t) t in
38 let status, t = term_of_cic_term status t (ctx_of gty) in
39 let status, ty = term_of_cic_term status ty (ctx_of ty) in
40 (status, (t,ty) :: l))
44 NCicParamod.nparamod status metasenv subst (ctx_of gty) (NCic.Rel ~-1,t) l
46 | [] -> raise (Error (lazy "no proof found",None))
47 | (pt, metasenv, subst)::_ ->
48 let status = status#set_obj (n,h,metasenv,subst,o) in
49 instantiate status goal (mk_cic_term (ctx_of gty) pt)
52 let auto_paramod_tac ~params status =
53 NTactics.distribute_tac (auto_paramod ~params) status
56 (*************** subsumption ****************)
57 module IntSet = Set.Make(struct type t = int let compare = compare end)
60 let get_sgoalty status g =
61 let _,_,metasenv,subst,_ = status#obj in
63 let _, ctx, ty = NCicUtils.lookup_meta g metasenv in
64 let ty = NCicUntrusted.apply_subst subst ctx ty in
65 let ctx = NCicUntrusted.apply_subst_context
66 ~fix_projections:true subst ctx
68 NTacStatus.mk_cic_term ctx ty
69 with NCicUtils.Meta_not_found _ as exn -> fail ~exn (lazy "get_sgoalty")
73 let gty = get_sgoalty status g in
74 metas_of_term status gty
77 let menv_closure status gl =
78 let rec closure acc = function
80 | x::l when IntSet.mem x acc -> closure acc l
81 | x::l -> closure (IntSet.add x acc) (deps status x @ l)
82 in closure IntSet.empty gl
85 let close_wrt_context =
89 | name, NCic.Decl t -> NCic.Prod(name,t,ty)
90 | name, NCic.Def(bo, _) -> NCicSubstitution.subst bo ty)
93 let args_for_context ?(k=1) ctx =
96 (fun (n,l) ctx_entry ->
98 | name, NCic.Decl t -> n+1,NCic.Rel(n)::l
99 | name, NCic.Def(bo, _) -> n+1,l)
103 let constant_for_meta ctx ty i =
104 let name = "cic:/foo"^(string_of_int i)^".con" in
105 let uri = NUri.uri_of_string name in
106 let ty = close_wrt_context ty ctx in
107 (* prerr_endline (NCicPp.ppterm [] [] [] ty); *)
108 let attr = (`Generated,`Definition,`Local) in
109 let obj = NCic.Constant([],name,None,ty,attr) in
110 (* Constant of relevance * string * term option * term * c_attr *)
114 let refresh metasenv =
116 (fun (metasenv,subst) (i,(iattr,ctx,ty)) ->
117 let ikind = NCicUntrusted.kind_of_meta iattr in
118 let metasenv,j,instance,ty =
119 NCicMetaSubst.mk_meta ~attrs:iattr
120 metasenv ctx ~with_type:ty ikind in
121 let s_entry = i,(iattr, ctx, instance, ty) in
122 let metasenv = List.filter (fun x,_ -> i <> x) metasenv in
123 metasenv,s_entry::subst)
124 (metasenv,[]) metasenv
126 (* close metasenv returns a ground instance of all the metas in the
127 metasenv, insantiatied with axioms, and the list of these axioms *)
128 let close_metasenv metasenv subst =
130 let metasenv = NCicUntrusted.apply_subst_metasenv subst metasenv in
132 let metasenv = NCicUntrusted.sort_metasenv subst metasenv in
134 (fun (subst,objs) (i,(iattr,ctx,ty)) ->
135 let ty = NCicUntrusted.apply_subst subst ctx ty in
137 NCicUntrusted.apply_subst_context ~fix_projections:true
139 let (uri,_,_,_,obj) as okind =
140 constant_for_meta ctx ty i in
142 NCicEnvironment.check_and_add_obj okind;
143 let iref = NReference.reference_of_spec uri NReference.Decl in
145 let args = args_for_context ctx in
146 if args = [] then NCic.Const iref
147 else NCic.Appl(NCic.Const iref::args)
149 (* prerr_endline (NCicPp.ppterm ctx [] [] iterm); *)
150 let s_entry = i, ([], ctx, iterm, ty)
151 in s_entry::subst,okind::objs
152 with _ -> assert false)
156 let ground_instances status gl =
157 let _,_,metasenv,subst,_ = status#obj in
158 let subset = menv_closure status gl in
159 let submenv = List.filter (fun (x,_) -> IntSet.mem x subset) metasenv in
161 let submenv = metasenv in
163 let subst, objs = close_metasenv submenv subst in
167 let (_, ctx, t, _) = List.assoc i subst in
168 debug_print (lazy (NCicPp.ppterm ctx [] [] t));
170 (fun (uri,_,_,_,_) as obj ->
171 NCicEnvironment.invalidate_item (`Obj (uri, obj)))
176 Not_found -> assert false
180 let replace_meta i args target =
181 let rec aux k = function
182 (* TODO: local context *)
183 | NCic.Meta (j,lc) when i = j ->
187 List.map (NCicSubstitution.subst_meta lc) args in
188 NCic.Appl(NCic.Rel k::args))
189 | NCic.Meta (j,lc) as m ->
196 aux k (NCicSubstitution.lift n t)) l))))
197 | t -> NCicUtils.map (fun _ k -> k+1) k aux t
202 let close_wrt_metasenv subst =
204 (fun ty (i,(iattr,ctx,mty)) ->
205 let mty = NCicUntrusted.apply_subst subst ctx mty in
207 NCicUntrusted.apply_subst_context ~fix_projections:true
209 let cty = close_wrt_context mty ctx in
210 let name = "foo"^(string_of_int i) in
211 let ty = NCicSubstitution.lift 1 ty in
212 let args = args_for_context ~k:1 ctx in
213 (* prerr_endline (NCicPp.ppterm ctx [] [] iterm); *)
214 let ty = replace_meta i args ty
216 NCic.Prod(name,cty,ty))
220 let _,_,metasenv,subst,_ = status#obj in
221 let subset = menv_closure status [g] in
222 let subset = IntSet.remove g subset in
223 let elems = IntSet.elements subset in
224 let _, ctx, ty = NCicUtils.lookup_meta g metasenv in
225 let ty = NCicUntrusted.apply_subst subst ctx ty in
226 print (lazy ("Elements for " ^ (NCicPp.ppterm ctx [] metasenv ty)));
227 print (lazy (String.concat ", " (List.map string_of_int elems)));
228 let submenv = List.filter (fun (x,_) -> IntSet.mem x subset) metasenv in
229 let submenv = List.rev (NCicUntrusted.sort_metasenv subst submenv) in
231 let submenv = metasenv in
233 let ty = close_wrt_metasenv subst ty submenv in
234 print (lazy (NCicPp.ppterm ctx [] [] ty));
240 (* =================================== auto =========================== *)
241 (****************** AUTO ********************
243 let calculate_timeout flags =
244 if flags.timeout = 0. then
245 (debug_print (lazy "AUTO WITH NO TIMEOUT");
246 {flags with timeout = infinity})
250 let is_equational_case goalty flags =
251 let ensure_equational t =
252 if is_an_equational_goal t then true
255 (flags.use_paramod && is_an_equational_goal goalty) ||
256 (flags.use_only_paramod && ensure_equational goalty)
259 type menv = Cic.metasenv
260 type subst = Cic.substitution
261 type goal = ProofEngineTypes.goal * int * AutoTypes.sort
262 let candidate_no = ref 0;;
263 type candidate = int * Cic.term Lazy.t
264 type cache = AutoCache.cache
267 (* the goal (mainly for depth) and key of the goal *)
268 goal * AutoCache.cache_key
270 (* goal has to be proved *)
272 (* goal has to be cached as a success obtained using candidate as the first
274 | S of goal * AutoCache.cache_key * candidate * int
276 (* menv, subst, size, operations done (only S), operations to do, failures to cache if any op fails *)
277 menv * subst * int * op list * op list * fail list
279 (* list of computations that may lead to the solution: all op list will
280 * end with the same (S(g,_)) *)
283 (* menv, subst, alternatives, tables, cache *)
284 | Proved of menv * subst * elem list * AutomationCache.tables * cache
285 | Gaveup of AutomationCache.tables * cache
288 (* the status exported to the external observer *)
290 (* context, (goal,candidate) list, and_list, history *)
291 Cic.context * (int * Cic.term * bool * int * (int * Cic.term Lazy.t) list) list *
292 (int * Cic.term * int) list * Cic.term Lazy.t list
295 let rec aux acc = function
296 | (D g)::tl -> aux (acc@[g]) tl
302 let calculate_goal_ty (goalno,_,_) s m =
304 let _,cc,goalty = CicUtil.lookup_meta goalno m in
305 (* XXX applicare la subst al contesto? *)
306 Some (cc, CicMetaSubst.apply_subst s goalty)
307 with CicUtil.Meta_not_found i when i = goalno -> None
310 let calculate_closed_goal_ty (goalno,_,_) s =
312 let cc,_,goalty = List.assoc goalno s in
313 (* XXX applicare la subst al contesto? *)
314 Some (cc, CicMetaSubst.apply_subst s goalty)
319 let pp_status ctx status =
321 let names = Utils.names_of_context ctx in
324 ProofEngineReduction.replace
325 ~equality:(fun a b -> match b with Cic.Meta _ -> true | _ -> false)
326 ~what:[Cic.Rel 1] ~with_what:[Cic.Implicit None] ~where:x
330 let string_of_do m s (gi,_,_ as g) d =
331 match calculate_goal_ty g s m with
332 | Some (_,gty) -> Printf.sprintf "D(%d, %s, %d)" gi (pp gty) d
333 | None -> Printf.sprintf "D(%d, _, %d)" gi d
335 let string_of_s m su k (ci,ct) gi =
336 Printf.sprintf "S(%d, %s, %s, %d)" gi (pp k) (pp (Lazy.force ct)) ci
338 let string_of_ol m su l =
342 | D (g,d,s) -> string_of_do m su (g,d,s) d
343 | S ((gi,_,_),k,c,_) -> string_of_s m su k c gi)
346 let string_of_fl m s fl =
348 (List.map (fun ((i,_,_),ty) ->
349 Printf.sprintf "(%d, %s)" i (pp ty)) fl)
351 let rec aux = function
353 | (m,s,_,_,ol,fl)::tl ->
354 Printf.eprintf "< [%s] ;;; [%s]>\n"
355 (string_of_ol m s ol) (string_of_fl m s fl);
358 Printf.eprintf "-------------------------- status -------------------\n";
360 Printf.eprintf "-----------------------------------------------------\n";
363 let auto_status = ref [] ;;
364 let auto_context = ref [];;
365 let in_pause = ref false;;
366 let pause b = in_pause := b;;
367 let cond = Condition.create ();;
368 let mutex = Mutex.create ();;
369 let hint = ref None;;
370 let prune_hint = ref [];;
372 let step _ = Condition.signal cond;;
373 let give_hint n = hint := Some n;;
374 let give_prune_hint hint =
375 prune_hint := hint :: !prune_hint
382 Condition.wait cond mutex;
387 let get_auto_status _ =
388 let status = !auto_status in
389 let and_list,elems,last =
392 | (m,s,_,don,gl,fail)::tl ->
395 (fun (id,d,_ as g) ->
396 match calculate_goal_ty g s m with
397 | Some (_,x) -> Some (id,x,d) | None -> None)
401 (* these are the S goalsin the or list *)
404 (fun (m,s,_,don,gl,fail) ->
406 (function S (g,k,c,_) -> Some (g,k,c) | _ -> None)
410 (* this function eats id from a list l::[id,x] returning x, l *)
411 let eat_tail_if_eq id l =
412 let rec aux (s, l) = function
414 | ((id1,_,_),k1,c)::tl when id = id1 ->
416 | None -> aux (Some c,l) tl
417 | Some _ -> assert false)
418 | ((id1,_,_),k1,c as e)::tl -> aux (s, e::l) tl
420 let c, l = aux (None, []) l in
423 let eat_in_parallel id l =
424 let rec aux (b,eaten, new_l as acc) l =
428 match eat_tail_if_eq id l with
429 | None, l -> aux (b@[false], eaten, new_l@[l]) tl
430 | Some t,l -> aux (b@[true],eaten@[t], new_l@[l]) tl
434 let rec eat_all rows l =
438 match List.rev elem with
439 | ((to_eat,depth,_),k,_)::next_lunch ->
440 let b, eaten, l = eat_in_parallel to_eat l in
441 let eaten = HExtlib.list_uniq eaten in
442 let eaten = List.rev eaten in
443 let b = true (* List.hd (List.rev b) *) in
444 let rows = rows @ [to_eat,k,b,depth,eaten] in
446 | [] -> eat_all rows or_list
448 eat_all [] (List.rev orlist)
452 (function (S (_,_,(_,c),_)) -> Some c | _ -> None)
455 (* let rows = List.filter (fun (_,l) -> l <> []) rows in *)
456 and_list, rows, history
458 !auto_context, elems, and_list, last
461 (* Works if there is no dependency over proofs *)
462 let is_a_green_cut goalty =
463 CicUtil.is_meta_closed goalty
465 let rec first_s = function
466 | (D _)::tl -> first_s tl
467 | (S (g,k,c,s))::tl -> Some ((g,k,c,s),tl)
470 let list_union l1 l2 =
471 (* TODO ottimizzare compare *)
472 HExtlib.list_uniq (List.sort compare (l1 @ l1))
474 let rec eq_todo l1 l2 =
476 | (D g1) :: tl1,(D g2) :: tl2 when g1=g2 -> eq_todo tl1 tl2
477 | (S (g1,k1,(c1,lt1),i1)) :: tl1, (S (g2,k2,(c2,lt2),i2)) :: tl2
478 when i1 = i2 && g1 = g2 && k1 = k2 && c1 = c2 ->
479 if Lazy.force lt1 = Lazy.force lt2 then eq_todo tl1 tl2 else false
483 let eat_head todo id fl orlist =
484 let rec aux acc = function
486 | (m, s, _, _, todo1, fl1)::tl as orlist ->
488 match first_s todo1 with
489 | None -> orlist, acc
490 | Some (((gno,_,_),_,_,_), todo11) ->
491 (* TODO confronto tra todo da ottimizzare *)
492 if gno = id && eq_todo todo11 todo then
493 aux (list_union fl1 acc) tl
501 let close_proof p ty menv context =
503 List.map fst (CicUtil.metas_of_term p @ CicUtil.metas_of_term ty)
505 let menv = List.filter (fun (i,_,_) -> List.exists ((=)i) metas) menv in
506 naif_closure p menv context
508 (* XXX capire bene quando aggiungere alla cache *)
509 let add_to_cache_and_del_from_orlist_if_green_cut
510 g s m cache key todo orlist fl ctx size minsize
512 let cache = cache_remove_underinspection cache key in
513 (* prima per fare la irl usavamo il contesto vero e proprio e non quello
515 match calculate_closed_goal_ty g s with
516 | None -> assert false
517 | Some (canonical_ctx , gty) ->
518 let goalno,depth,sort = g in
519 let irl = mk_irl canonical_ctx in
520 let goal = Cic.Meta(goalno, irl) in
521 let proof = CicMetaSubst.apply_subst s goal in
522 let green_proof, closed_proof =
523 let b = is_a_green_cut proof in
525 b, (* close_proof proof gty m ctx *) proof
529 debug_print (lazy ("TENTATIVE CACHE: " ^ CicPp.ppterm key));
530 if is_a_green_cut key then
531 (* if the initia goal was closed, we cut alternatives *)
532 let _ = debug_print (lazy ("MANGIO: " ^ string_of_int goalno)) in
533 let orlist, fl = eat_head todo goalno fl orlist in
535 if size < minsize then
536 (debug_print (lazy ("NO CACHE: 2 (size <= minsize)"));cache)
538 (* if the proof is closed we cache it *)
539 if green_proof then cache_add_success cache key proof
540 else (* cache_add_success cache key closed_proof *)
541 (debug_print (lazy ("NO CACHE: (no gree proof)"));cache)
543 cache, orlist, fl, true
546 debug_print (lazy ("TENTATIVE CACHE: " ^ CicPp.ppterm gty));
547 if size < minsize then
548 (debug_print (lazy ("NO CACHE: (size <= minsize)")); cache) else
549 (* if the substituted goal and the proof are closed we cache it *)
550 if is_a_green_cut gty then
551 if green_proof then cache_add_success cache gty proof
552 else (* cache_add_success cache gty closed_proof *)
553 (debug_print (lazy ("NO CACHE: (no green proof (gty))"));cache)
557 CicTypeChecker.type_of_aux' ~subst:s
558 m ctx closed_proof CicUniv.oblivion_ugraph
560 if is_a_green_cut ty then
561 cache_add_success cache ty closed_proof
564 | CicTypeChecker.TypeCheckerFailure _ ->*)
565 (debug_print (lazy ("NO CACHE: (no green gty )"));cache)
567 cache, orlist, fl, false
569 let close_failures (fl : fail list) (cache : cache) =
571 (fun cache ((gno,depth,_),gty) ->
572 if CicUtil.is_meta_closed gty then
573 ( debug_print (lazy ("FAIL: INDUCED: " ^ string_of_int gno));
574 cache_add_failure cache gty depth)
579 let put_in_subst subst metasenv (goalno,_,_) canonical_ctx t ty =
580 let entry = goalno, (canonical_ctx, t,ty) in
581 assert_subst_are_disjoint subst [entry];
582 let subst = entry :: subst in
584 let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
589 let mk_fake_proof metasenv subst (goalno,_,_) goalty context =
590 None,metasenv,subst ,(lazy (Cic.Meta(goalno,mk_irl context))),goalty, []
594 tables cache depth fake_proof goalno goalty subst context
597 let active,passive,bag = tables in
598 let ppterm = ppterm context in
599 let status = (fake_proof,goalno) in
600 if flags.use_only_paramod then
602 debug_print (lazy ("PARAMODULATION SU: " ^
603 string_of_int goalno ^ " " ^ ppterm goalty ));
604 let goal_steps, saturation_steps, timeout =
605 max_int,max_int,flags.timeout
608 Saturation.given_clause bag status active passive
609 goal_steps saturation_steps timeout
611 | None, active, passive, bag ->
612 [], (active,passive,bag), cache, flags
613 | Some(subst',(_,metasenv,_subst,proof,_, _),open_goals),active,
615 assert_subst_are_disjoint subst subst';
616 let subst = subst@subst' in
618 order_new_goals metasenv subst open_goals ppterm
621 List.map (fun (x,sort) -> x,depth-1,sort) open_goals
624 [(!candidate_no,proof),metasenv,subst,open_goals],
625 (active,passive,bag), cache, flags
629 debug_print (lazy ("NARROWING DEL GOAL: " ^
630 string_of_int goalno ^ " " ^ ppterm goalty ));
631 let goal_steps, saturation_steps, timeout =
635 Saturation.solve_narrowing bag status active passive goal_steps
637 | None, active, passive, bag ->
638 [], (active,passive,bag), cache, flags
639 | Some(subst',(_,metasenv,_subst,proof,_, _),open_goals),active,
641 assert_subst_are_disjoint subst subst';
642 let subst = subst@subst' in
644 order_new_goals metasenv subst open_goals ppterm
647 List.map (fun (x,sort) -> x,depth-1,sort) open_goals
650 [(!candidate_no,proof),metasenv,subst,open_goals],
651 (active,passive,bag), cache, flags
655 let params = ([],["use_context","false"]) in
656 let automation_cache = {
657 AutomationCache.tables = tables ;
658 AutomationCache.univ = Universe.empty; }
661 let ((_,metasenv,subst,_,_,_),open_goals) =
663 solve_rewrite ~params ~automation_cache
666 let proof = lazy (Cic.Meta (-1,[])) in
667 [(!candidate_no,proof),metasenv,subst,[]],tables, cache, flags
668 with ProofEngineTypes.Fail _ -> [], tables, cache, flags
670 let res = Saturation.all_subsumed bag status active passive in
673 (fun (subst',(_,metasenv,_subst,proof,_, _),open_goals) ->
674 assert_subst_are_disjoint subst subst';
675 let subst = subst@subst' in
677 order_new_goals metasenv subst open_goals ppterm
680 List.map (fun (x,sort) -> x,depth-1,sort) open_goals
683 (!candidate_no,proof),metasenv,subst,open_goals)
686 res', (active,passive,bag), cache, flags
693 List.sort (fun (_,_,_,l1) (_,_,_,l2) ->
694 let p1 = List.length (prop_only l1) in
695 let p2 = List.length (prop_only l2) in
696 if p1 = p2 then List.length l1 - List.length l2 else p1-p2)
700 let try_candidate dbd
701 goalty tables subst fake_proof goalno depth context cand
703 let ppterm = ppterm context in
705 let actives, passives, bag = tables in
706 let (_,metasenv,subst,_,_,_), open_goals =
707 ProofEngineTypes.apply_tactic
708 (PrimitiveTactics.apply_tac ~term:cand)
711 let tables = actives, passives,
712 Equality.push_maxmeta bag
713 (max (Equality.maxmeta bag) (CicMkImplicit.new_meta metasenv subst))
715 debug_print (lazy (" OK: " ^ ppterm cand));
716 let metasenv = CicRefine.pack_coercion_metasenv metasenv in
717 let open_goals = order_new_goals metasenv subst open_goals ppterm in
718 let open_goals = List.map (fun (x,sort) -> x,depth-1,sort) open_goals in
720 Some ((!candidate_no,lazy cand),metasenv,subst,open_goals), tables
722 | ProofEngineTypes.Fail s -> None,tables
723 | CicUnification.Uncertain s -> None,tables
726 let applicative_case dbd
727 tables depth subst fake_proof goalno goalty metasenv context
728 signature universe cache flags
732 | Cic.Appl (hd::tl) ->
733 Cic.Appl (hd :: HExtlib.mk_list (Cic.Meta (0,[])) (List.length tl))
736 let goalty_aux = goalty in
738 get_candidates flags.skip_trie_filtering universe cache goalty_aux
740 (* if the goal is an equality we skip the congruence theorems
742 if is_equational_case goalty flags
743 then List.filter not_default_eq_term candidates
746 let candidates = List.filter (only signature context metasenv) candidates
750 (fun (tables,elems) cand ->
752 try_candidate dbd goalty
753 tables subst fake_proof goalno depth context cand
755 | None, tables -> tables, elems
756 | Some x, tables -> tables, x::elems)
757 (tables,[]) candidates
759 let elems = sort_new_elems elems in
763 let try_smart_candidate dbd
764 goalty tables subst fake_proof goalno depth context cand
766 let ppterm = ppterm context in
768 let params = ([],[]) in
769 let automation_cache = {
770 AutomationCache.tables = tables ;
771 AutomationCache.univ = Universe.empty; }
773 debug_print (lazy ("candidato per " ^ string_of_int goalno
774 ^ ": " ^ CicPp.ppterm cand));
776 let (_,metasenv,subst,_,_,_) = fake_proof in
777 prerr_endline ("metasenv:\n" ^ CicMetaSubst.ppmetasenv [] metasenv);
778 prerr_endline ("subst:\n" ^ CicMetaSubst.ppsubst ~metasenv subst);
780 let ((_,metasenv,subst,_,_,_),open_goals) =
781 apply_smart ~dbd ~term:cand ~params ~automation_cache
784 let metasenv = CicRefine.pack_coercion_metasenv metasenv in
785 let open_goals = order_new_goals metasenv subst open_goals ppterm in
786 let open_goals = List.map (fun (x,sort) -> x,depth-1,sort) open_goals in
788 Some ((!candidate_no,lazy cand),metasenv,subst,open_goals), tables
790 | ProofEngineTypes.Fail s -> None,tables
791 | CicUnification.Uncertain s -> None,tables
794 let smart_applicative_case dbd
795 tables depth subst fake_proof goalno goalty metasenv context signature
800 | Cic.Appl (hd::tl) ->
801 Cic.Appl (hd :: HExtlib.mk_list (Cic.Meta (0,[])) (List.length tl))
804 let smart_candidates =
805 get_candidates flags.skip_trie_filtering universe cache goalty_aux
808 get_candidates flags.skip_trie_filtering universe cache goalty
810 let smart_candidates =
812 (fun x -> not(List.mem x candidates)) smart_candidates
815 (lazy ("smart_candidates" ^ " = " ^
816 (String.concat "\n" (List.map CicPp.ppterm smart_candidates)))) in
817 debug_print debug_msg;
818 let candidates = List.filter (only signature context metasenv) candidates in
819 let smart_candidates =
820 List.filter (only signature context metasenv) smart_candidates
823 let penalty cand depth =
824 if only signature context metasenv cand then depth else ((prerr_endline (
825 "penalizzo " ^ CicPp.ppterm cand));depth -1)
830 (fun (tables,elems) cand ->
832 try_candidate dbd goalty
833 tables subst fake_proof goalno depth context cand
836 (* if normal application fails we try to be smart *)
837 (match try_smart_candidate dbd goalty
838 tables subst fake_proof goalno depth context cand
840 | None, tables -> tables, elems
841 | Some x, tables -> tables, x::elems)
842 | Some x, tables -> tables, x::elems)
843 (tables,[]) candidates
845 let tables, smart_elems =
847 (fun (tables,elems) cand ->
849 try_smart_candidate dbd goalty
850 tables subst fake_proof goalno depth context cand
852 | None, tables -> tables, elems
853 | Some x, tables -> tables, x::elems)
854 (tables,[]) smart_candidates
856 let elems = sort_new_elems (elems @ smart_elems) in
860 let equational_and_applicative_case dbd
861 signature universe flags m s g gty tables cache context
863 let goalno, depth, sort = g in
864 let fake_proof = mk_fake_proof m s g gty context in
865 if is_equational_case gty flags then
866 let elems,tables,cache, flags =
867 equational_case tables cache
868 depth fake_proof goalno gty s context flags
870 let more_elems, tables, cache =
871 if flags.use_only_paramod then
875 tables depth s fake_proof goalno
876 gty m context signature universe cache flags
878 elems@more_elems, tables, cache, flags
880 let elems, tables, cache =
881 match LibraryObjects.eq_URI () with
883 smart_applicative_case dbd tables depth s fake_proof goalno
884 gty m context signature universe cache flags
886 applicative_case dbd tables depth s fake_proof goalno
887 gty m context signature universe cache flags
889 elems, tables, cache, flags
891 let rec condition_for_hint i = function
893 | S (_,_,(j,_),_):: tl -> j <> i (* && condition_for_hint i tl *)
894 | _::tl -> condition_for_hint i tl
896 let prunable_for_size flags s m todo =
897 let rec aux b = function
898 | (S _)::tl -> aux b tl
899 | (D (_,_,T))::tl -> aux b tl
901 (match calculate_goal_ty g s m with
903 | Some (canonical_ctx, gty) ->
906 ~consider_metas:false ~count_metas_occurrences:true gty in
907 let newb = b || gsize > flags.maxgoalsizefactor in
914 let prunable ty todo =
915 let rec aux b = function
916 | (S(_,k,_,_))::tl -> aux (b || Equality.meta_convertibility k ty) tl
917 | (D (_,_,T))::tl -> aux b tl
925 let prunable menv subst ty todo =
926 let rec aux = function
927 | (S(_,k,_,_))::tl ->
928 (match Equality.meta_convertibility_subst k ty menv with
931 no_progress variant tl (* || aux tl*))
932 | (D (_,_,T))::tl -> aux tl
934 and no_progress variant = function
935 | [] -> (*prerr_endline "++++++++++++++++++++++++ no_progress";*) true
936 | D ((n,_,P) as g)::tl ->
937 (match calculate_goal_ty g subst menv with
938 | None -> no_progress variant tl
940 (match calculate_goal_ty g variant menv with
941 | None -> assert false
943 if gty = gty' then no_progress variant tl
945 (prerr_endline (string_of_int n);
946 prerr_endline (CicPp.ppterm gty);
947 prerr_endline (CicPp.ppterm gty');
948 prerr_endline "---------- subst";
949 prerr_endline (CicMetaSubst.ppsubst ~metasenv:menv subst);
950 prerr_endline "---------- variant";
951 prerr_endline (CicMetaSubst.ppsubst ~metasenv:menv variant);
952 prerr_endline "---------- menv";
953 prerr_endline (CicMetaSubst.ppmetasenv [] menv);
954 no_progress variant tl) *)
956 | _::tl -> no_progress variant tl
961 let condition_for_prune_hint prune (m, s, size, don, todo, fl) =
963 HExtlib.filter_map (function S (_,_,(c,_),_) -> Some c | _ -> None) todo
965 List.for_all (fun i -> List.for_all (fun j -> i<>j) prune) s
967 let filter_prune_hint c l =
968 let prune = !prune_hint in
969 prune_hint := []; (* possible race... *)
970 if prune = [] then c,l
972 cache_reset_underinspection c,
973 List.filter (condition_for_prune_hint prune) l
979 auto_all_solutions dbd tables universe cache context metasenv gl flags
984 MetadataConstraints.UriManagerSet.union set
985 (MetadataQuery.signature_of metasenv g)
987 MetadataConstraints.UriManagerSet.empty gl
989 let goals = order_new_goals metasenv [] gl CicPp.ppterm in
992 (fun (x,s) -> D (x,flags.maxdepth,s)) goals
994 let elems = [metasenv,[],1,[],goals,[]] in
995 let rec aux tables solutions cache elems flags =
996 match auto_main dbd tables context flags signature universe cache elems with
997 | Gaveup (tables,cache) ->
998 solutions,cache, tables
999 | Proved (metasenv,subst,others,tables,cache) ->
1000 if Unix.gettimeofday () > flags.timeout then
1001 ((subst,metasenv)::solutions), cache, tables
1003 aux tables ((subst,metasenv)::solutions) cache others flags
1005 let rc = aux tables [] cache elems flags in
1007 | [],cache,tables -> [],cache,tables
1008 | solutions, cache,tables ->
1011 (fun (subst,newmetasenv) ->
1013 ProofEngineHelpers.compare_metasenvs ~oldmetasenv:metasenv ~newmetasenv
1015 if opened = [] then Some subst else None)
1018 solutions,cache,tables
1021 (******************* AUTO ***************)
1024 let auto dbd flags metasenv tables universe cache context metasenv gl =
1025 let initial_time = Unix.gettimeofday() in
1029 MetadataConstraints.UriManagerSet.union set
1030 (MetadataQuery.signature_of metasenv g)
1032 MetadataConstraints.UriManagerSet.empty gl
1034 let goals = order_new_goals metasenv [] gl CicPp.ppterm in
1035 let goals = List.map (fun (x,s) -> D(x,flags.maxdepth,s)) goals in
1036 let elems = [metasenv,[],1,[],goals,[]] in
1037 match auto_main dbd tables context flags signature universe cache elems with
1038 | Proved (metasenv,subst,_, tables,cache) ->
1040 ("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time)));
1041 Some (subst,metasenv), cache
1042 | Gaveup (tables,cache) ->
1044 ("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time)));
1048 let auto_tac ~(dbd:HSql.dbd) ~params:(univ,params) ~automation_cache (proof, goal) =
1049 let flags = flags_of_params params () in
1050 let use_library = flags.use_library in
1051 let universe, tables, cache =
1052 init_cache_and_tables
1053 ~dbd ~use_library ~use_context:(not flags.skip_context)
1054 automation_cache univ (proof, goal)
1056 let _,metasenv,subst,_,_, _ = proof in
1057 let _,context,goalty = CicUtil.lookup_meta goal metasenv in
1058 let signature = MetadataQuery.signature_of metasenv goal in
1063 CicTypeChecker.type_of_aux' metasenv context t
1064 CicUniv.oblivion_ugraph
1066 MetadataConstraints.UriManagerSet.union set
1067 (MetadataConstraints.constants_of ty)
1072 if flags.close_more then
1074 tables context (proof, goal)
1075 (auto_all_solutions dbd) signature universe cache
1076 else tables,cache in
1077 let initial_time = Unix.gettimeofday() in
1078 let (_,oldmetasenv,_,_,_, _) = proof in
1081 metasenv,subst,1,[],[D (goal,flags.maxdepth,P)],[]
1083 match auto_main dbd tables context flags signature universe cache [elem] with
1084 | Proved (metasenv,subst,_, tables,cache) ->
1086 ("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time)));
1087 let proof,metasenv =
1088 ProofEngineHelpers.subst_meta_and_metasenv_in_proof
1089 proof goal subst metasenv
1092 ProofEngineHelpers.compare_metasenvs ~oldmetasenv
1093 ~newmetasenv:metasenv
1096 | Gaveup (tables,cache) ->
1099 string_of_float(Unix.gettimeofday()-.initial_time)));
1100 raise (ProofEngineTypes.Fail (lazy "Auto gave up"))
1104 (****************** types **************)
1105 type th_cache = (NCic.context * InvRelDiscriminationTree.t) list
1107 let keys_of_term status t =
1108 let status, orig_ty = typeof status (ctx_of t) t in
1109 let _, ty, _ = saturate ~delta:max_int status orig_ty in
1112 let _, ty = term_of_cic_term status ty (ctx_of ty) in
1114 | NCic.Const (NReference.Ref (_,NReference.Def h))
1115 | NCic.Appl (NCic.Const(NReference.Ref(_,NReference.Def h))::_)
1117 let _,ty,_= saturate status ~delta:(h-1) orig_ty in
1124 let mk_th_cache status gl =
1126 (fun (status, acc) g ->
1127 let gty = get_goalty status g in
1128 let ctx = ctx_of gty in
1129 debug_print(lazy("th cache for: "^ppterm status gty));
1130 debug_print(lazy("th cache in: "^ppcontext status ctx));
1131 if List.mem_assq ctx acc then status, acc else
1132 let idx = InvRelDiscriminationTree.empty in
1135 (fun (status, i, idx) _ ->
1136 let t = mk_cic_term ctx (NCic.Rel i) in
1137 debug_print(lazy("indexing: "^ppterm status t));
1138 let status, keys = keys_of_term status t in
1140 List.fold_left (fun idx k ->
1141 InvRelDiscriminationTree.index idx k t) idx keys
1144 (status, 1, idx) ctx
1146 status, (ctx, idx) :: acc)
1150 let add_to_th t c ty =
1151 let key_c = ctx_of t in
1152 if not (List.mem_assq key_c c) then
1153 (key_c ,InvRelDiscriminationTree.index
1154 InvRelDiscriminationTree.empty ty t ) :: c
1156 let rec replace = function
1158 | (x, idx) :: tl when x == key_c ->
1159 (x, InvRelDiscriminationTree.index idx ty t) :: tl
1160 | x :: tl -> x :: replace tl
1165 let pp_idx status idx =
1166 InvRelDiscriminationTree.iter idx
1168 debug_print(lazy("K: " ^ NCicInverseRelIndexable.string_of_path k));
1170 (fun t -> debug_print(lazy("\t"^ppterm status t)))
1177 debug_print(lazy( "-----------------------------------------------"));
1178 debug_print(lazy( (NCicPp.ppcontext ~metasenv:[] ~subst:[] ctx)));
1179 debug_print(lazy( "||====> "));
1184 let search_in_th gty th =
1185 let c = ctx_of gty in
1186 let rec aux acc = function
1187 | [] -> Ncic_termSet.elements acc
1190 let idx = List.assq k th in
1191 let acc = Ncic_termSet.union acc
1192 (InvRelDiscriminationTree.retrieve_unifiables idx gty)
1195 with Not_found -> aux acc tl
1197 aux Ncic_termSet.empty c
1201 do_types : bool; (* solve goals in Type *)
1209 type goal = int * sort (* goal, depth, sort *)
1210 type fail = goal * cic_term
1211 type candidate = int * Ast.term (* unique candidate number, candidate *)
1213 exception Gaveup of IntSet.t (* a sublist of unprovable conjunctive
1214 atoms of the input goals *)
1215 exception Proved of #NTacStatus.tac_status
1217 let close_failures _ c = c;;
1218 let prunable _ _ _ = false;;
1219 let cache_examine cache gty = `Notfound;;
1220 let put_in_subst s _ _ _ = s;;
1221 let add_to_cache_and_del_from_orlist_if_green_cut _ _ c _ _ o f _ = c, o, f, false ;;
1222 let cache_add_underinspection c _ _ = c;;
1223 let equational_case _ _ _ _ _ _ = [];;
1224 let only _ _ _ = true;;
1226 let candidate_no = ref 0;;
1228 let sort_new_elems l =
1229 List.sort (fun (_,_,_,_,l1) (_,_,_,_,l2) -> List.length l1 - List.length l2) l
1232 let try_candidate flags depth status t g =
1234 debug_print ~depth (lazy ("try " ^ CicNotationPp.pp_term t));
1235 (* let status = NTactics.focus_tac [g] status in *)
1236 let status = NTactics.apply_tac ("",0,t) status in
1237 let open_goals = head_goals status#stack in
1239 (lazy ("success: "^String.concat " "(List.map string_of_int open_goals)));
1240 if List.length open_goals > flags.maxwidth ||
1241 (depth = flags.maxdepth && open_goals <> []) then
1242 (debug_print ~depth (lazy "pruned immediately"); None)
1245 Some ((!candidate_no,t),status,open_goals))
1246 with Error (msg,exn) -> debug_print ~depth (lazy "failed"); None
1249 let get_candidates status cache_th signature gty =
1250 let universe = status#auto_cache in
1251 let context = ctx_of gty in
1252 let _, raw_gty = term_of_cic_term status gty context in
1254 NDiscriminationTree.DiscriminationTree.retrieve_unifiables universe raw_gty
1257 List.filter (only signature context)
1258 (NDiscriminationTree.TermSet.elements cands)
1261 let _status, t = term_of_cic_term status t context in Ast.NCic t)
1262 (search_in_th gty cache_th)
1264 List.map (function NCic.Const r -> Ast.NRef r | _ -> assert false) cands
1267 let applicative_case depth signature status flags g gty cache =
1268 app_counter:= !app_counter+1;
1269 let candidates = get_candidates status cache signature gty in
1271 (lazy ("candidates: " ^ string_of_int (List.length candidates)));
1275 match try_candidate flags depth status cand g with
1277 | Some x -> x::elems)
1283 let equational_and_applicative_case
1284 signature flags status g depth gty cache
1287 if false (*is_equational_case gty flags*) then
1290 signature status flags g gty cache
1293 applicative_case depth
1294 signature status flags g gty cache
1299 (*match LibraryObjects.eq_URI () with
1301 smart_applicative_case dbd tables depth s fake_proof goalno
1302 gty m context signature universe cache flags
1304 applicative_case depth
1305 signature status flags g gty cache
1310 List.map (fun c,s,gl ->
1311 c,1,1,s,List.map (fun i ->
1313 let gty = get_goalty s i in
1314 let _, sort = typeof s (ctx_of gty) gty in
1315 match term_of_cic_term s sort (ctx_of sort) with
1316 | _, NCic.Sort NCic.Prop -> P
1321 let elems = sort_new_elems elems in
1325 let rec guess_name name ctx =
1326 if name = "_" then guess_name "auto" ctx else
1327 if not (List.mem_assoc name ctx) then name else
1328 guess_name (name^"'") ctx
1331 let intro_case status gno gty depth cache name =
1332 (* let status = NTactics.focus_tac [gno] status in *)
1333 let status = NTactics.intro_tac (guess_name name (ctx_of gty)) status in
1334 let open_goals = head_goals status#stack in
1335 assert (List.length open_goals = 1);
1336 let open_goal = List.hd open_goals in
1337 let ngty = get_goalty status open_goal in
1338 let ctx = ctx_of ngty in
1339 let t = mk_cic_term ctx (NCic.Rel 1) in
1340 let status, keys = keys_of_term status t in
1341 let cache = List.fold_left (add_to_th t) cache keys in
1342 debug_print ~depth (lazy ("intro: "^ string_of_int open_goal));
1344 (* XXX compute the sort *)
1345 [(!candidate_no,Ast.Implicit `JustOne),0,0,status,[open_goal,P]],
1349 let pp_goal = function
1350 | (_,Continuationals.Stack.Open i)
1351 | (_,Continuationals.Stack.Closed i) -> string_of_int i
1354 let pp_goals status l =
1358 let gty = get_goalty status i in
1359 NTacStatus.ppterm status gty)
1363 let do_something signature flags s gno depth gty cache =
1364 let _s, raw_gty = term_of_cic_term s gty (ctx_of gty) in
1366 | NCic.Prod (name,_,_) -> intro_case s gno gty depth cache name
1368 equational_and_applicative_case signature flags s gno depth gty cache
1374 let compare = Pervasives.compare
1378 module MS = HTopoSort.Make(M)
1381 let sort_tac status =
1383 match status#stack with
1384 | [] -> assert false
1385 | (goals, t, k, tag) :: s ->
1386 let g = head_goals status#stack in
1388 (List.rev (MS.topological_sort g (deps status))) in
1389 debug_print (lazy ("old g = " ^
1390 String.concat "," (List.map string_of_int g)));
1391 debug_print (lazy ("sorted goals = " ^
1392 String.concat "," (List.map string_of_int sortedg)));
1393 let is_it i = function
1394 | (_,Continuationals.Stack.Open j )
1395 | (_,Continuationals.Stack.Closed j ) -> i = j
1398 List.map (fun i -> List.find (is_it i) goals) sortedg
1400 (sorted_goals, t, k, tag) :: s
1402 status#set_stack gstatus
1405 let clean_up_tac status =
1407 match status#stack with
1408 | [] -> assert false
1409 | (g, t, k, tag) :: s ->
1410 let is_open = function
1411 | (_,Continuationals.Stack.Open _) -> true
1412 | (_,Continuationals.Stack.Closed _) -> false
1414 let g' = List.filter is_open g in
1415 (g', t, k, tag) :: s
1417 status#set_stack gstatus
1420 let focus_tac focus status =
1422 match status#stack with
1423 | [] -> assert false
1424 | (g, t, k, tag) :: s ->
1425 let in_focus = function
1426 | (_,Continuationals.Stack.Open i)
1427 | (_,Continuationals.Stack.Closed i) -> List.mem i focus
1429 let focus,others = List.partition in_focus g
1431 (* we need to mark it as a BranchTag, otherwise cannot merge later *)
1432 (focus,[],[],`BranchTag) :: (others, t, k, tag) :: s
1434 status#set_stack gstatus
1437 let rec auto_clusters
1438 flags signature cache depth status : unit =
1439 debug_print ~depth (lazy "entering auto clusters");
1440 (* ignore(Unix.select [] [] [] 0.01); *)
1441 let status = clean_up_tac status in
1442 let goals = head_goals status#stack in
1443 if goals = [] then raise (Proved status)
1444 else if depth = flags.maxdepth then raise (Gaveup IntSet.empty)
1445 else if List.length goals < 2 then
1446 auto_main flags signature cache depth status
1448 debug_print ~depth (lazy ("goals = " ^
1449 String.concat "," (List.map string_of_int goals)));
1450 let classes = HExtlib.clusters (deps status) goals in
1456 ("cluster:" ^ String.concat "," (List.map string_of_int l)))
1461 let status = focus_tac gl status in
1463 debug_print ~depth (lazy ("focusing on" ^
1464 String.concat "," (List.map string_of_int gl)));
1465 auto_main flags signature cache depth status; status
1466 with Proved(status) -> NTactics.merge_tac status)
1468 in raise (Proved status)
1472 (* The pair solved,init_status is used for chaching purposes.
1473 solved is the list of goals in init_status already proved.
1474 Initially, init_status=status and k is set to [] *)
1475 (* let rec auto_main flags signature cache status k depth = *)
1477 auto_main flags signature cache depth status: unit =
1478 debug_print ~depth (lazy "entering auto main");
1479 (* ignore(Unix.select [] [] [] 0.01); *)
1480 let status = sort_tac (clean_up_tac status) in
1481 let goals = head_goals status#stack in
1483 | [] -> raise (Proved status)
1485 if depth = flags.maxdepth then raise (Gaveup IntSet.empty)
1488 if tlg=[] then status
1489 else NTactics.branch_tac status in
1490 let gty = get_goalty status g in
1491 let status, gty = apply_subst status (ctx_of gty) gty in
1492 debug_print ~depth (lazy("Depth = " ^ (string_of_int depth)));
1493 debug_print ~depth (lazy("Attacking goal " ^ (string_of_int g) ^" : "^ppterm status gty));
1495 (* let closed = metas_of_term status gty = [] in *)
1496 let alternatives, cache =
1497 do_something signature flags status g depth gty cache in
1500 (* the underscore information does not need to be returned
1502 (fun unsat ((_,t),_,_,status,_) ->
1504 if t=(Ast.Implicit `JustOne) then depth else depth+1 in
1505 debug_print (~depth:depth')
1506 (lazy ("Case: " ^ CicNotationPp.pp_term t));
1507 try auto_clusters flags signature cache
1508 depth' status; unsat
1511 debug_print (~depth:depth') (lazy "proved");
1512 if tlg=[] then raise (Proved status)
1514 let status = NTactics.merge_tac status
1516 (try auto_clusters flags signature cache
1520 (lazy ("Unsat1 at depth " ^ (string_of_int depth)
1522 (pp_goals status (IntSet.elements f))));
1523 (* TODO: cache failures *)
1524 IntSet.union f unsat)
1526 debug_print (~depth:depth')
1527 (lazy ("Unsat2 at depth " ^ (string_of_int depth')
1529 (pp_goals status (IntSet.elements f))));
1530 (* TODO: cache local failures *)
1532 IntSet.empty alternatives
1534 raise (Gaveup IntSet.add g unsat)
1537 let int name l def =
1538 try int_of_string (List.assoc name l)
1539 with Failure _ | Not_found -> def
1542 let auto_tac ~params:(_univ,flags) status =
1543 let goals = head_goals status#stack in
1544 let status, cache = mk_th_cache status goals in
1545 (* pp_th status cache; *)
1547 NDiscriminationTree.DiscriminationTree.iter status#auto_cache (fun p t ->
1549 NDiscriminationTree.NCicIndexable.string_of_path p ^ " |--> " ^
1550 String.concat "\n " (List.map (
1551 NCicPp.ppterm ~metasenv:[] ~context:[] ~subst:[])
1552 (NDiscriminationTree.TermSet.elements t))
1555 let depth = int "depth" flags 3 in
1556 let size = int "size" flags 10 in
1557 let width = int "width" flags (3+List.length goals) in
1559 let goals = List.map (fun i -> (i,P)) goals in
1560 let signature = () in
1565 timeout = Unix.gettimeofday() +. 3000.;
1568 let initial_time = Unix.gettimeofday() in
1571 if x > y then raise (Error (lazy "auto gave up", None))
1573 let _ = debug_print (lazy("\n\nRound "^string_of_int x^"\n")) in
1574 let flags = { flags with maxdepth = x }
1576 try auto_clusters flags signature cache 0 status;status
1578 | Gaveup _ -> up_to (x+1) y
1580 HLog.debug ("proved at depth " ^ string_of_int x);
1583 | (g,t,k,f) :: rest -> (filter_open g,t,k,f):: rest
1588 let s = up_to depth depth in
1590 ("TIME ELAPSED:"^string_of_float(Unix.gettimeofday()-.initial_time)));
1592 ("Applicative nodes:"^string_of_int !app_counter));