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_______________________________________________________________ *)
12 (* $Id: nCic.ml 9058 2008-10-13 17:42:30Z tassi $ *)
17 let debug_print s = if debug then prerr_endline (Lazy.force s) else ()
19 open Continuationals.Stack
21 module Ast = CicNotationPt
23 (* =================================== paramod =========================== *)
24 let auto_paramod ~params:(l,_) status goal =
25 let gty = get_goalty status goal in
26 let n,h,metasenv,subst,o = status#obj in
27 let status,t = term_of_cic_term status gty (ctx_of gty) in
31 let status, t = disambiguate status t None (ctx_of gty) in
32 let status, ty = typeof status (ctx_of t) t in
33 let status, t = term_of_cic_term status t (ctx_of gty) in
34 let status, ty = term_of_cic_term status ty (ctx_of ty) in
35 (status, (t,ty) :: l))
39 NCicParamod.nparamod status metasenv subst (ctx_of gty) (NCic.Rel ~-1,t) l
41 | [] -> raise (NTacStatus.Error (lazy "no proof found",None))
42 | (pt, metasenv, subst)::_ ->
43 let status = status#set_obj (n,h,metasenv,subst,o) in
44 instantiate status goal (NTacStatus.mk_cic_term (ctx_of gty) pt)
47 let auto_paramod_tac ~params status =
48 NTactics.distribute_tac (auto_paramod ~params) status
51 (* =================================== auto =========================== *)
52 (****************** AUTO ********************
54 let calculate_timeout flags =
55 if flags.timeout = 0. then
56 (debug_print (lazy "AUTO WITH NO TIMEOUT");
57 {flags with timeout = infinity})
61 let is_equational_case goalty flags =
62 let ensure_equational t =
63 if is_an_equational_goal t then true
66 (flags.use_paramod && is_an_equational_goal goalty) ||
67 (flags.use_only_paramod && ensure_equational goalty)
70 type menv = Cic.metasenv
71 type subst = Cic.substitution
72 type goal = ProofEngineTypes.goal * int * AutoTypes.sort
73 let candidate_no = ref 0;;
74 type candidate = int * Cic.term Lazy.t
75 type cache = AutoCache.cache
78 (* the goal (mainly for depth) and key of the goal *)
79 goal * AutoCache.cache_key
81 (* goal has to be proved *)
83 (* goal has to be cached as a success obtained using candidate as the first
85 | S of goal * AutoCache.cache_key * candidate * int
87 (* menv, subst, size, operations done (only S), operations to do, failures to cache if any op fails *)
88 menv * subst * int * op list * op list * fail list
90 (* list of computations that may lead to the solution: all op list will
91 * end with the same (S(g,_)) *)
94 (* menv, subst, alternatives, tables, cache *)
95 | Proved of menv * subst * elem list * AutomationCache.tables * cache
96 | Gaveup of AutomationCache.tables * cache
99 (* the status exported to the external observer *)
101 (* context, (goal,candidate) list, and_list, history *)
102 Cic.context * (int * Cic.term * bool * int * (int * Cic.term Lazy.t) list) list *
103 (int * Cic.term * int) list * Cic.term Lazy.t list
106 let rec aux acc = function
107 | (D g)::tl -> aux (acc@[g]) tl
113 let calculate_goal_ty (goalno,_,_) s m =
115 let _,cc,goalty = CicUtil.lookup_meta goalno m in
116 (* XXX applicare la subst al contesto? *)
117 Some (cc, CicMetaSubst.apply_subst s goalty)
118 with CicUtil.Meta_not_found i when i = goalno -> None
121 let calculate_closed_goal_ty (goalno,_,_) s =
123 let cc,_,goalty = List.assoc goalno s in
124 (* XXX applicare la subst al contesto? *)
125 Some (cc, CicMetaSubst.apply_subst s goalty)
130 let pp_status ctx status =
132 let names = Utils.names_of_context ctx in
135 ProofEngineReduction.replace
136 ~equality:(fun a b -> match b with Cic.Meta _ -> true | _ -> false)
137 ~what:[Cic.Rel 1] ~with_what:[Cic.Implicit None] ~where:x
141 let string_of_do m s (gi,_,_ as g) d =
142 match calculate_goal_ty g s m with
143 | Some (_,gty) -> Printf.sprintf "D(%d, %s, %d)" gi (pp gty) d
144 | None -> Printf.sprintf "D(%d, _, %d)" gi d
146 let string_of_s m su k (ci,ct) gi =
147 Printf.sprintf "S(%d, %s, %s, %d)" gi (pp k) (pp (Lazy.force ct)) ci
149 let string_of_ol m su l =
153 | D (g,d,s) -> string_of_do m su (g,d,s) d
154 | S ((gi,_,_),k,c,_) -> string_of_s m su k c gi)
157 let string_of_fl m s fl =
159 (List.map (fun ((i,_,_),ty) ->
160 Printf.sprintf "(%d, %s)" i (pp ty)) fl)
162 let rec aux = function
164 | (m,s,_,_,ol,fl)::tl ->
165 Printf.eprintf "< [%s] ;;; [%s]>\n"
166 (string_of_ol m s ol) (string_of_fl m s fl);
169 Printf.eprintf "-------------------------- status -------------------\n";
171 Printf.eprintf "-----------------------------------------------------\n";
174 let auto_status = ref [] ;;
175 let auto_context = ref [];;
176 let in_pause = ref false;;
177 let pause b = in_pause := b;;
178 let cond = Condition.create ();;
179 let mutex = Mutex.create ();;
180 let hint = ref None;;
181 let prune_hint = ref [];;
183 let step _ = Condition.signal cond;;
184 let give_hint n = hint := Some n;;
185 let give_prune_hint hint =
186 prune_hint := hint :: !prune_hint
193 Condition.wait cond mutex;
198 let get_auto_status _ =
199 let status = !auto_status in
200 let and_list,elems,last =
203 | (m,s,_,don,gl,fail)::tl ->
206 (fun (id,d,_ as g) ->
207 match calculate_goal_ty g s m with
208 | Some (_,x) -> Some (id,x,d) | None -> None)
212 (* these are the S goalsin the or list *)
215 (fun (m,s,_,don,gl,fail) ->
217 (function S (g,k,c,_) -> Some (g,k,c) | _ -> None)
221 (* this function eats id from a list l::[id,x] returning x, l *)
222 let eat_tail_if_eq id l =
223 let rec aux (s, l) = function
225 | ((id1,_,_),k1,c)::tl when id = id1 ->
227 | None -> aux (Some c,l) tl
228 | Some _ -> assert false)
229 | ((id1,_,_),k1,c as e)::tl -> aux (s, e::l) tl
231 let c, l = aux (None, []) l in
234 let eat_in_parallel id l =
235 let rec aux (b,eaten, new_l as acc) l =
239 match eat_tail_if_eq id l with
240 | None, l -> aux (b@[false], eaten, new_l@[l]) tl
241 | Some t,l -> aux (b@[true],eaten@[t], new_l@[l]) tl
245 let rec eat_all rows l =
249 match List.rev elem with
250 | ((to_eat,depth,_),k,_)::next_lunch ->
251 let b, eaten, l = eat_in_parallel to_eat l in
252 let eaten = HExtlib.list_uniq eaten in
253 let eaten = List.rev eaten in
254 let b = true (* List.hd (List.rev b) *) in
255 let rows = rows @ [to_eat,k,b,depth,eaten] in
257 | [] -> eat_all rows or_list
259 eat_all [] (List.rev orlist)
263 (function (S (_,_,(_,c),_)) -> Some c | _ -> None)
266 (* let rows = List.filter (fun (_,l) -> l <> []) rows in *)
267 and_list, rows, history
269 !auto_context, elems, and_list, last
272 (* Works if there is no dependency over proofs *)
273 let is_a_green_cut goalty =
274 CicUtil.is_meta_closed goalty
276 let rec first_s = function
277 | (D _)::tl -> first_s tl
278 | (S (g,k,c,s))::tl -> Some ((g,k,c,s),tl)
281 let list_union l1 l2 =
282 (* TODO ottimizzare compare *)
283 HExtlib.list_uniq (List.sort compare (l1 @ l1))
285 let rec eq_todo l1 l2 =
287 | (D g1) :: tl1,(D g2) :: tl2 when g1=g2 -> eq_todo tl1 tl2
288 | (S (g1,k1,(c1,lt1),i1)) :: tl1, (S (g2,k2,(c2,lt2),i2)) :: tl2
289 when i1 = i2 && g1 = g2 && k1 = k2 && c1 = c2 ->
290 if Lazy.force lt1 = Lazy.force lt2 then eq_todo tl1 tl2 else false
294 let eat_head todo id fl orlist =
295 let rec aux acc = function
297 | (m, s, _, _, todo1, fl1)::tl as orlist ->
299 match first_s todo1 with
300 | None -> orlist, acc
301 | Some (((gno,_,_),_,_,_), todo11) ->
302 (* TODO confronto tra todo da ottimizzare *)
303 if gno = id && eq_todo todo11 todo then
304 aux (list_union fl1 acc) tl
312 let close_proof p ty menv context =
314 List.map fst (CicUtil.metas_of_term p @ CicUtil.metas_of_term ty)
316 let menv = List.filter (fun (i,_,_) -> List.exists ((=)i) metas) menv in
317 naif_closure p menv context
319 (* XXX capire bene quando aggiungere alla cache *)
320 let add_to_cache_and_del_from_orlist_if_green_cut
321 g s m cache key todo orlist fl ctx size minsize
323 let cache = cache_remove_underinspection cache key in
324 (* prima per fare la irl usavamo il contesto vero e proprio e non quello
326 match calculate_closed_goal_ty g s with
327 | None -> assert false
328 | Some (canonical_ctx , gty) ->
329 let goalno,depth,sort = g in
330 let irl = mk_irl canonical_ctx in
331 let goal = Cic.Meta(goalno, irl) in
332 let proof = CicMetaSubst.apply_subst s goal in
333 let green_proof, closed_proof =
334 let b = is_a_green_cut proof in
336 b, (* close_proof proof gty m ctx *) proof
340 debug_print (lazy ("TENTATIVE CACHE: " ^ CicPp.ppterm key));
341 if is_a_green_cut key then
342 (* if the initia goal was closed, we cut alternatives *)
343 let _ = debug_print (lazy ("MANGIO: " ^ string_of_int goalno)) in
344 let orlist, fl = eat_head todo goalno fl orlist in
346 if size < minsize then
347 (debug_print (lazy ("NO CACHE: 2 (size <= minsize)"));cache)
349 (* if the proof is closed we cache it *)
350 if green_proof then cache_add_success cache key proof
351 else (* cache_add_success cache key closed_proof *)
352 (debug_print (lazy ("NO CACHE: (no gree proof)"));cache)
354 cache, orlist, fl, true
357 debug_print (lazy ("TENTATIVE CACHE: " ^ CicPp.ppterm gty));
358 if size < minsize then
359 (debug_print (lazy ("NO CACHE: (size <= minsize)")); cache) else
360 (* if the substituted goal and the proof are closed we cache it *)
361 if is_a_green_cut gty then
362 if green_proof then cache_add_success cache gty proof
363 else (* cache_add_success cache gty closed_proof *)
364 (debug_print (lazy ("NO CACHE: (no green proof (gty))"));cache)
368 CicTypeChecker.type_of_aux' ~subst:s
369 m ctx closed_proof CicUniv.oblivion_ugraph
371 if is_a_green_cut ty then
372 cache_add_success cache ty closed_proof
375 | CicTypeChecker.TypeCheckerFailure _ ->*)
376 (debug_print (lazy ("NO CACHE: (no green gty )"));cache)
378 cache, orlist, fl, false
380 let close_failures (fl : fail list) (cache : cache) =
382 (fun cache ((gno,depth,_),gty) ->
383 if CicUtil.is_meta_closed gty then
384 ( debug_print (lazy ("FAIL: INDUCED: " ^ string_of_int gno));
385 cache_add_failure cache gty depth)
390 let put_in_subst subst metasenv (goalno,_,_) canonical_ctx t ty =
391 let entry = goalno, (canonical_ctx, t,ty) in
392 assert_subst_are_disjoint subst [entry];
393 let subst = entry :: subst in
395 let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
400 let mk_fake_proof metasenv subst (goalno,_,_) goalty context =
401 None,metasenv,subst ,(lazy (Cic.Meta(goalno,mk_irl context))),goalty, []
405 tables cache depth fake_proof goalno goalty subst context
408 let active,passive,bag = tables in
409 let ppterm = ppterm context in
410 let status = (fake_proof,goalno) in
411 if flags.use_only_paramod then
413 debug_print (lazy ("PARAMODULATION SU: " ^
414 string_of_int goalno ^ " " ^ ppterm goalty ));
415 let goal_steps, saturation_steps, timeout =
416 max_int,max_int,flags.timeout
419 Saturation.given_clause bag status active passive
420 goal_steps saturation_steps timeout
422 | None, active, passive, bag ->
423 [], (active,passive,bag), cache, flags
424 | Some(subst',(_,metasenv,_subst,proof,_, _),open_goals),active,
426 assert_subst_are_disjoint subst subst';
427 let subst = subst@subst' in
429 order_new_goals metasenv subst open_goals ppterm
432 List.map (fun (x,sort) -> x,depth-1,sort) open_goals
435 [(!candidate_no,proof),metasenv,subst,open_goals],
436 (active,passive,bag), cache, flags
440 debug_print (lazy ("NARROWING DEL GOAL: " ^
441 string_of_int goalno ^ " " ^ ppterm goalty ));
442 let goal_steps, saturation_steps, timeout =
446 Saturation.solve_narrowing bag status active passive goal_steps
448 | None, active, passive, bag ->
449 [], (active,passive,bag), cache, flags
450 | Some(subst',(_,metasenv,_subst,proof,_, _),open_goals),active,
452 assert_subst_are_disjoint subst subst';
453 let subst = subst@subst' in
455 order_new_goals metasenv subst open_goals ppterm
458 List.map (fun (x,sort) -> x,depth-1,sort) open_goals
461 [(!candidate_no,proof),metasenv,subst,open_goals],
462 (active,passive,bag), cache, flags
466 let params = ([],["use_context","false"]) in
467 let automation_cache = {
468 AutomationCache.tables = tables ;
469 AutomationCache.univ = Universe.empty; }
472 let ((_,metasenv,subst,_,_,_),open_goals) =
474 solve_rewrite ~params ~automation_cache
477 let proof = lazy (Cic.Meta (-1,[])) in
478 [(!candidate_no,proof),metasenv,subst,[]],tables, cache, flags
479 with ProofEngineTypes.Fail _ -> [], tables, cache, flags
481 let res = Saturation.all_subsumed bag status active passive in
484 (fun (subst',(_,metasenv,_subst,proof,_, _),open_goals) ->
485 assert_subst_are_disjoint subst subst';
486 let subst = subst@subst' in
488 order_new_goals metasenv subst open_goals ppterm
491 List.map (fun (x,sort) -> x,depth-1,sort) open_goals
494 (!candidate_no,proof),metasenv,subst,open_goals)
497 res', (active,passive,bag), cache, flags
504 List.sort (fun (_,_,_,l1) (_,_,_,l2) ->
505 let p1 = List.length (prop_only l1) in
506 let p2 = List.length (prop_only l2) in
507 if p1 = p2 then List.length l1 - List.length l2 else p1-p2)
511 let try_candidate dbd
512 goalty tables subst fake_proof goalno depth context cand
514 let ppterm = ppterm context in
516 let actives, passives, bag = tables in
517 let (_,metasenv,subst,_,_,_), open_goals =
518 ProofEngineTypes.apply_tactic
519 (PrimitiveTactics.apply_tac ~term:cand)
522 let tables = actives, passives,
523 Equality.push_maxmeta bag
524 (max (Equality.maxmeta bag) (CicMkImplicit.new_meta metasenv subst))
526 debug_print (lazy (" OK: " ^ ppterm cand));
527 let metasenv = CicRefine.pack_coercion_metasenv metasenv in
528 let open_goals = order_new_goals metasenv subst open_goals ppterm in
529 let open_goals = List.map (fun (x,sort) -> x,depth-1,sort) open_goals in
531 Some ((!candidate_no,lazy cand),metasenv,subst,open_goals), tables
533 | ProofEngineTypes.Fail s -> None,tables
534 | CicUnification.Uncertain s -> None,tables
537 let applicative_case dbd
538 tables depth subst fake_proof goalno goalty metasenv context
539 signature universe cache flags
543 | Cic.Appl (hd::tl) ->
544 Cic.Appl (hd :: HExtlib.mk_list (Cic.Meta (0,[])) (List.length tl))
547 let goalty_aux = goalty in
549 get_candidates flags.skip_trie_filtering universe cache goalty_aux
551 (* if the goal is an equality we skip the congruence theorems
553 if is_equational_case goalty flags
554 then List.filter not_default_eq_term candidates
557 let candidates = List.filter (only signature context metasenv) candidates
561 (fun (tables,elems) cand ->
563 try_candidate dbd goalty
564 tables subst fake_proof goalno depth context cand
566 | None, tables -> tables, elems
567 | Some x, tables -> tables, x::elems)
568 (tables,[]) candidates
570 let elems = sort_new_elems elems in
574 let try_smart_candidate dbd
575 goalty tables subst fake_proof goalno depth context cand
577 let ppterm = ppterm context in
579 let params = ([],[]) in
580 let automation_cache = {
581 AutomationCache.tables = tables ;
582 AutomationCache.univ = Universe.empty; }
584 debug_print (lazy ("candidato per " ^ string_of_int goalno
585 ^ ": " ^ CicPp.ppterm cand));
587 let (_,metasenv,subst,_,_,_) = fake_proof in
588 prerr_endline ("metasenv:\n" ^ CicMetaSubst.ppmetasenv [] metasenv);
589 prerr_endline ("subst:\n" ^ CicMetaSubst.ppsubst ~metasenv subst);
591 let ((_,metasenv,subst,_,_,_),open_goals) =
592 apply_smart ~dbd ~term:cand ~params ~automation_cache
595 let metasenv = CicRefine.pack_coercion_metasenv metasenv in
596 let open_goals = order_new_goals metasenv subst open_goals ppterm in
597 let open_goals = List.map (fun (x,sort) -> x,depth-1,sort) open_goals in
599 Some ((!candidate_no,lazy cand),metasenv,subst,open_goals), tables
601 | ProofEngineTypes.Fail s -> None,tables
602 | CicUnification.Uncertain s -> None,tables
605 let smart_applicative_case dbd
606 tables depth subst fake_proof goalno goalty metasenv context signature
611 | Cic.Appl (hd::tl) ->
612 Cic.Appl (hd :: HExtlib.mk_list (Cic.Meta (0,[])) (List.length tl))
615 let smart_candidates =
616 get_candidates flags.skip_trie_filtering universe cache goalty_aux
619 get_candidates flags.skip_trie_filtering universe cache goalty
621 let smart_candidates =
623 (fun x -> not(List.mem x candidates)) smart_candidates
626 (lazy ("smart_candidates" ^ " = " ^
627 (String.concat "\n" (List.map CicPp.ppterm smart_candidates)))) in
628 debug_print debug_msg;
629 let candidates = List.filter (only signature context metasenv) candidates in
630 let smart_candidates =
631 List.filter (only signature context metasenv) smart_candidates
634 let penalty cand depth =
635 if only signature context metasenv cand then depth else ((prerr_endline (
636 "penalizzo " ^ CicPp.ppterm cand));depth -1)
641 (fun (tables,elems) cand ->
643 try_candidate dbd goalty
644 tables subst fake_proof goalno depth context cand
647 (* if normal application fails we try to be smart *)
648 (match try_smart_candidate dbd goalty
649 tables subst fake_proof goalno depth context cand
651 | None, tables -> tables, elems
652 | Some x, tables -> tables, x::elems)
653 | Some x, tables -> tables, x::elems)
654 (tables,[]) candidates
656 let tables, smart_elems =
658 (fun (tables,elems) cand ->
660 try_smart_candidate dbd goalty
661 tables subst fake_proof goalno depth context cand
663 | None, tables -> tables, elems
664 | Some x, tables -> tables, x::elems)
665 (tables,[]) smart_candidates
667 let elems = sort_new_elems (elems @ smart_elems) in
671 let equational_and_applicative_case dbd
672 signature universe flags m s g gty tables cache context
674 let goalno, depth, sort = g in
675 let fake_proof = mk_fake_proof m s g gty context in
676 if is_equational_case gty flags then
677 let elems,tables,cache, flags =
678 equational_case tables cache
679 depth fake_proof goalno gty s context flags
681 let more_elems, tables, cache =
682 if flags.use_only_paramod then
686 tables depth s fake_proof goalno
687 gty m context signature universe cache flags
689 elems@more_elems, tables, cache, flags
691 let elems, tables, cache =
692 match LibraryObjects.eq_URI () with
694 smart_applicative_case dbd tables depth s fake_proof goalno
695 gty m context signature universe cache flags
697 applicative_case dbd tables depth s fake_proof goalno
698 gty m context signature universe cache flags
700 elems, tables, cache, flags
702 let rec condition_for_hint i = function
704 | S (_,_,(j,_),_):: tl -> j <> i (* && condition_for_hint i tl *)
705 | _::tl -> condition_for_hint i tl
707 let prunable_for_size flags s m todo =
708 let rec aux b = function
709 | (S _)::tl -> aux b tl
710 | (D (_,_,T))::tl -> aux b tl
712 (match calculate_goal_ty g s m with
714 | Some (canonical_ctx, gty) ->
717 ~consider_metas:false ~count_metas_occurrences:true gty in
718 let newb = b || gsize > flags.maxgoalsizefactor in
725 let prunable ty todo =
726 let rec aux b = function
727 | (S(_,k,_,_))::tl -> aux (b || Equality.meta_convertibility k ty) tl
728 | (D (_,_,T))::tl -> aux b tl
736 let prunable menv subst ty todo =
737 let rec aux = function
738 | (S(_,k,_,_))::tl ->
739 (match Equality.meta_convertibility_subst k ty menv with
742 no_progress variant tl (* || aux tl*))
743 | (D (_,_,T))::tl -> aux tl
745 and no_progress variant = function
746 | [] -> (*prerr_endline "++++++++++++++++++++++++ no_progress";*) true
747 | D ((n,_,P) as g)::tl ->
748 (match calculate_goal_ty g subst menv with
749 | None -> no_progress variant tl
751 (match calculate_goal_ty g variant menv with
752 | None -> assert false
754 if gty = gty' then no_progress variant tl
756 (prerr_endline (string_of_int n);
757 prerr_endline (CicPp.ppterm gty);
758 prerr_endline (CicPp.ppterm gty');
759 prerr_endline "---------- subst";
760 prerr_endline (CicMetaSubst.ppsubst ~metasenv:menv subst);
761 prerr_endline "---------- variant";
762 prerr_endline (CicMetaSubst.ppsubst ~metasenv:menv variant);
763 prerr_endline "---------- menv";
764 prerr_endline (CicMetaSubst.ppmetasenv [] menv);
765 no_progress variant tl) *)
767 | _::tl -> no_progress variant tl
772 let condition_for_prune_hint prune (m, s, size, don, todo, fl) =
774 HExtlib.filter_map (function S (_,_,(c,_),_) -> Some c | _ -> None) todo
776 List.for_all (fun i -> List.for_all (fun j -> i<>j) prune) s
778 let filter_prune_hint c l =
779 let prune = !prune_hint in
780 prune_hint := []; (* possible race... *)
781 if prune = [] then c,l
783 cache_reset_underinspection c,
784 List.filter (condition_for_prune_hint prune) l
790 auto_all_solutions dbd tables universe cache context metasenv gl flags
795 MetadataConstraints.UriManagerSet.union set
796 (MetadataQuery.signature_of metasenv g)
798 MetadataConstraints.UriManagerSet.empty gl
800 let goals = order_new_goals metasenv [] gl CicPp.ppterm in
803 (fun (x,s) -> D (x,flags.maxdepth,s)) goals
805 let elems = [metasenv,[],1,[],goals,[]] in
806 let rec aux tables solutions cache elems flags =
807 match auto_main dbd tables context flags signature universe cache elems with
808 | Gaveup (tables,cache) ->
809 solutions,cache, tables
810 | Proved (metasenv,subst,others,tables,cache) ->
811 if Unix.gettimeofday () > flags.timeout then
812 ((subst,metasenv)::solutions), cache, tables
814 aux tables ((subst,metasenv)::solutions) cache others flags
816 let rc = aux tables [] cache elems flags in
818 | [],cache,tables -> [],cache,tables
819 | solutions, cache,tables ->
822 (fun (subst,newmetasenv) ->
824 ProofEngineHelpers.compare_metasenvs ~oldmetasenv:metasenv ~newmetasenv
826 if opened = [] then Some subst else None)
829 solutions,cache,tables
832 (******************* AUTO ***************)
835 let auto dbd flags metasenv tables universe cache context metasenv gl =
836 let initial_time = Unix.gettimeofday() in
840 MetadataConstraints.UriManagerSet.union set
841 (MetadataQuery.signature_of metasenv g)
843 MetadataConstraints.UriManagerSet.empty gl
845 let goals = order_new_goals metasenv [] gl CicPp.ppterm in
846 let goals = List.map (fun (x,s) -> D(x,flags.maxdepth,s)) goals in
847 let elems = [metasenv,[],1,[],goals,[]] in
848 match auto_main dbd tables context flags signature universe cache elems with
849 | Proved (metasenv,subst,_, tables,cache) ->
851 ("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time)));
852 Some (subst,metasenv), cache
853 | Gaveup (tables,cache) ->
855 ("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time)));
859 let auto_tac ~(dbd:HSql.dbd) ~params:(univ,params) ~automation_cache (proof, goal) =
860 let flags = flags_of_params params () in
861 let use_library = flags.use_library in
862 let universe, tables, cache =
863 init_cache_and_tables
864 ~dbd ~use_library ~use_context:(not flags.skip_context)
865 automation_cache univ (proof, goal)
867 let _,metasenv,subst,_,_, _ = proof in
868 let _,context,goalty = CicUtil.lookup_meta goal metasenv in
869 let signature = MetadataQuery.signature_of metasenv goal in
874 CicTypeChecker.type_of_aux' metasenv context t
875 CicUniv.oblivion_ugraph
877 MetadataConstraints.UriManagerSet.union set
878 (MetadataConstraints.constants_of ty)
883 if flags.close_more then
885 tables context (proof, goal)
886 (auto_all_solutions dbd) signature universe cache
888 let initial_time = Unix.gettimeofday() in
889 let (_,oldmetasenv,_,_,_, _) = proof in
892 metasenv,subst,1,[],[D (goal,flags.maxdepth,P)],[]
894 match auto_main dbd tables context flags signature universe cache [elem] with
895 | Proved (metasenv,subst,_, tables,cache) ->
897 ("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time)));
899 ProofEngineHelpers.subst_meta_and_metasenv_in_proof
900 proof goal subst metasenv
903 ProofEngineHelpers.compare_metasenvs ~oldmetasenv
904 ~newmetasenv:metasenv
907 | Gaveup (tables,cache) ->
910 string_of_float(Unix.gettimeofday()-.initial_time)));
911 raise (ProofEngineTypes.Fail (lazy "Auto gave up"))
915 module CacheElem : Set.OrderedType =
918 | Failed_in of int * NCic.term (* depth, goal type *)
919 | Succeded of Cic.term * Cic.term (* proof, proof type *)
920 | UnderInspection of Cic.term (* avoid looping *)
922 let compare = Pervasives.compare
925 module CacheSet = Set.Make(CacheElem)
927 Discrimination_tree.Make(NDiscriminationTree.NCicIndexable)(CacheSet)
929 type cache_examination_result =
932 | `Succeded of NCic.term
937 type goal = int * int * sort
938 type fail = goal * NCic.term
939 type candidate = NCic.term
940 type menv = NCic.metasenv
941 type subst = NCic.substitution
944 (* goal has to be proved *)
946 (* goal has to be cached as a success obtained using candidate as the first
948 | S of goal * Cache.input * candidate (* int was minsize *)
950 (* menv, subst, size, operations done (only S), operations to do,
951 * failures to cache if any op fails *)
952 menv * subst * int * op list * op list * fail list
955 (* list of computations that may lead to the solution: all op list will
956 * end with the same (S(g,_)) *)
961 | Proved of menv * subst * auto_status (* the alternative proofs *)
964 do_types : bool; (* solve goals in Type *)
970 let close_failures _ = assert false;;
971 let equational_and_applicative_case _ = assert false;;
972 let prunable _ = assert false;;
973 let cache_examine _ = assert false;;
974 let put_in_subst _ = assert false;;
975 let calculate_goal_ty _ = assert false;;
976 let add_to_cache_and_del_from_orlist_if_green_cut _ = assert false;;
977 let cache_add_underinspection _ = assert false;;
980 let rec aux acc = function
981 | (D g)::tl -> aux (acc@[g]) tl
982 | (S _)::tl -> aux acc tl
988 List.filter (function (_,_,P) -> true | _ -> false) l
990 let remove_s_from_fl (id,_,_) (fl : fail list) =
991 let rec aux = function
993 | ((id1,_,_),_)::tl when id = id1 -> tl
994 | hd::tl -> hd :: aux tl
999 let auto_main status context flags signature elems cache =
1000 let rec aux (elems, cache : auto_status) =
1001 (* processa le hint dell'utente *)
1002 (* let cache, elems = filter_prune_hint cache elems in *)
1005 | (m, s, size, don, todo, fl)::orlist when !hint <> None ->
1006 debug_print (lazy "skip");
1008 | Some i when condition_for_hint i todo ->
1009 aux tables flags cache orlist
1012 aux tables flags cache elems)
1015 (* complete failure *)
1016 debug_print (lazy "gave up");
1018 | (m, s, _, _, [],_)::orlist ->
1019 (* complete success *)
1020 debug_print (lazy "success");
1021 Proved (m, s, (orlist, cache))
1022 | (m, s, size, don, (D (_,_,T))::todo, fl)::orlist
1023 when not flags.do_types ->
1024 (* skip since not Prop, don't even check if closed by side-effect *)
1025 debug_print (lazy "skip goal in Type");
1026 aux ((m, s, size, don, todo, fl)::orlist, cache)
1027 | (m, s, size, don, (S(g, key, c) as op)::todo, fl)::orlist ->
1028 (* partial success, cache g and go on *)
1029 let cache, orlist, fl, sibling_pruned =
1030 add_to_cache_and_del_from_orlist_if_green_cut
1031 g s m cache key todo orlist fl context size
1033 let fl = remove_s_from_fl g fl in
1034 let don = if sibling_pruned then don else op::don in
1035 aux ((m, s, size, don, todo, fl)::orlist, cache)
1036 | (m, s, size, don, todo, fl)::orlist
1037 when List.length(prop_only (d_goals todo)) > flags.maxwidth ->
1038 debug_print (lazy ("FAIL: WIDTH"));
1040 | (m, s, size, don, todo, fl)::orlist when size > flags.maxsize ->
1041 debug_print (lazy ("FAIL: SIZE: "^string_of_int size ^
1042 " > " ^ string_of_int flags.maxsize ));
1044 | _ when Unix.gettimeofday () > flags.timeout ->
1045 debug_print (lazy ("FAIL: TIMEOUT"));
1047 | (m, s, size, don, (D (gno,depth,_ as g))::todo, fl)::orlist as status ->
1048 debug_print (lazy "attack goal");
1049 match calculate_goal_ty g s m with
1051 debug_print (lazy ("SUCCESS: SIDE EFFECT: " ^ string_of_int gno));
1052 aux ((m,s,size,don,todo, fl)::orlist, cache)
1053 | Some (canonical_ctx, gty) ->
1054 debug_print (lazy ("EXAMINE: "^
1055 NCicPp.ppterm ~metasenv:m ~subst:s ~context gty));
1056 match cache_examine cache gty with
1057 | `Failed_in d when d >= depth ->
1058 debug_print (lazy ("FAIL: DEPTH (cache): "^string_of_int gno));
1059 let cache = close_failures fl cache in
1061 | `UnderInspection ->
1062 debug_print (lazy ("FAIL: LOOP: " ^ string_of_int gno));
1063 let cache = close_failures fl cache in
1066 debug_print (lazy ("SUCCESS: CACHE HIT: " ^ string_of_int gno));
1067 let s, m = put_in_subst s m g canonical_ctx t gty in
1068 aux ((m, s, size, don,todo, fl)::orlist, cache)
1070 | `Failed_in _ when depth > 0 ->
1071 ( (* more depth or is the first time we see the goal *)
1072 if prunable m s gty todo then
1073 (debug_print (lazy( "FAIL: LOOP: one father is equal"));
1074 let cache = close_failures fl cache in
1077 let cache = cache_add_underinspection cache gty depth in
1078 debug_print (lazy ("INSPECTING: " ^
1079 string_of_int gno ^ "("^ string_of_int size ^ "): "^
1080 NCicPp.ppterm ~metasenv:m ~subst:s ~context gty));
1081 (* elems are possible computations for proving gty *)
1083 equational_and_applicative_case
1084 signature status flags m s g gty cache context
1087 (* this goal has failed *)
1088 let cache = close_failures ((g,gty)::fl) cache in
1091 let size_gl l = List.length
1092 (List.filter (function (_,_,P) -> true | _ -> false) l)
1095 let inj_gl gl = List.map (fun g -> D g) gl in
1096 let rec map = function
1097 | [] -> assert false
1098 | (cand,m,s,gl)::[] ->
1100 inj_gl gl @ (S(g,gty,cand))::todo
1102 (* we are the last in OR, we fail on g and
1103 * also on all failures implied by g *)
1104 (m,s, size + size_gl gl, don, todo, (g,gty)::fl)
1106 | (cand,m,s,gl)::tl ->
1108 inj_gl gl @ (S(g,gty,cand))::todo
1110 (m,s, size + size_gl gl, don, todo, []) :: map tl
1116 debug_print (lazy ("FAIL: DEPTH: " ^ string_of_int gno));
1117 let cache = close_failures fl cache in
1120 (aux (elems, cache) : auto_result)
1123 let auto_tac ~params status =
1124 prerr_endline "I teoremi noti sono";
1125 NDiscriminationTree.DiscriminationTree.iter status#auto_cache
1129 (NCicPp.ppterm ~metasenv:[] ~subst:[] ~context:[] t))
1130 (NDiscriminationTree.TermSet.elements t));
1135 (* ========================= dispatching of auto/auto_paramod ============ *)
1136 let auto_tac ~params:(_,flags as params) =
1137 if List.mem_assoc "paramodulation" flags then
1138 auto_paramod_tac ~params