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 ()
18 let debug_do f = if !debug then f () else ()
20 open Continuationals.Stack
22 module Ast = CicNotationPt
24 (* =================================== paramod =========================== *)
25 let auto_paramod ~params:(l,_) status goal =
26 let gty = get_goalty status goal in
27 let n,h,metasenv,subst,o = status#obj in
28 let status,t = term_of_cic_term status gty (ctx_of gty) in
32 let status, t = disambiguate status (ctx_of gty) t None in
33 let status, ty = typeof status (ctx_of t) t in
34 let status, t = term_of_cic_term status t (ctx_of gty) in
35 let status, ty = term_of_cic_term status ty (ctx_of ty) in
36 (status, (t,ty) :: l))
40 NCicParamod.nparamod status metasenv subst (ctx_of gty) (NCic.Rel ~-1,t) l
42 | [] -> raise (Error (lazy "no proof found",None))
43 | (pt, metasenv, subst)::_ ->
44 let status = status#set_obj (n,h,metasenv,subst,o) in
45 instantiate status goal (mk_cic_term (ctx_of gty) pt)
48 let auto_paramod_tac ~params status =
49 NTactics.distribute_tac (auto_paramod ~params) status
52 (* =================================== auto =========================== *)
53 (****************** AUTO ********************
55 let calculate_timeout flags =
56 if flags.timeout = 0. then
57 (debug_print (lazy "AUTO WITH NO TIMEOUT");
58 {flags with timeout = infinity})
62 let is_equational_case goalty flags =
63 let ensure_equational t =
64 if is_an_equational_goal t then true
67 (flags.use_paramod && is_an_equational_goal goalty) ||
68 (flags.use_only_paramod && ensure_equational goalty)
71 type menv = Cic.metasenv
72 type subst = Cic.substitution
73 type goal = ProofEngineTypes.goal * int * AutoTypes.sort
74 let candidate_no = ref 0;;
75 type candidate = int * Cic.term Lazy.t
76 type cache = AutoCache.cache
79 (* the goal (mainly for depth) and key of the goal *)
80 goal * AutoCache.cache_key
82 (* goal has to be proved *)
84 (* goal has to be cached as a success obtained using candidate as the first
86 | S of goal * AutoCache.cache_key * candidate * int
88 (* menv, subst, size, operations done (only S), operations to do, failures to cache if any op fails *)
89 menv * subst * int * op list * op list * fail list
91 (* list of computations that may lead to the solution: all op list will
92 * end with the same (S(g,_)) *)
95 (* menv, subst, alternatives, tables, cache *)
96 | Proved of menv * subst * elem list * AutomationCache.tables * cache
97 | Gaveup of AutomationCache.tables * cache
100 (* the status exported to the external observer *)
102 (* context, (goal,candidate) list, and_list, history *)
103 Cic.context * (int * Cic.term * bool * int * (int * Cic.term Lazy.t) list) list *
104 (int * Cic.term * int) list * Cic.term Lazy.t list
107 let rec aux acc = function
108 | (D g)::tl -> aux (acc@[g]) tl
114 let calculate_goal_ty (goalno,_,_) s m =
116 let _,cc,goalty = CicUtil.lookup_meta goalno m in
117 (* XXX applicare la subst al contesto? *)
118 Some (cc, CicMetaSubst.apply_subst s goalty)
119 with CicUtil.Meta_not_found i when i = goalno -> None
122 let calculate_closed_goal_ty (goalno,_,_) s =
124 let cc,_,goalty = List.assoc goalno s in
125 (* XXX applicare la subst al contesto? *)
126 Some (cc, CicMetaSubst.apply_subst s goalty)
131 let pp_status ctx status =
133 let names = Utils.names_of_context ctx in
136 ProofEngineReduction.replace
137 ~equality:(fun a b -> match b with Cic.Meta _ -> true | _ -> false)
138 ~what:[Cic.Rel 1] ~with_what:[Cic.Implicit None] ~where:x
142 let string_of_do m s (gi,_,_ as g) d =
143 match calculate_goal_ty g s m with
144 | Some (_,gty) -> Printf.sprintf "D(%d, %s, %d)" gi (pp gty) d
145 | None -> Printf.sprintf "D(%d, _, %d)" gi d
147 let string_of_s m su k (ci,ct) gi =
148 Printf.sprintf "S(%d, %s, %s, %d)" gi (pp k) (pp (Lazy.force ct)) ci
150 let string_of_ol m su l =
154 | D (g,d,s) -> string_of_do m su (g,d,s) d
155 | S ((gi,_,_),k,c,_) -> string_of_s m su k c gi)
158 let string_of_fl m s fl =
160 (List.map (fun ((i,_,_),ty) ->
161 Printf.sprintf "(%d, %s)" i (pp ty)) fl)
163 let rec aux = function
165 | (m,s,_,_,ol,fl)::tl ->
166 Printf.eprintf "< [%s] ;;; [%s]>\n"
167 (string_of_ol m s ol) (string_of_fl m s fl);
170 Printf.eprintf "-------------------------- status -------------------\n";
172 Printf.eprintf "-----------------------------------------------------\n";
175 let auto_status = ref [] ;;
176 let auto_context = ref [];;
177 let in_pause = ref false;;
178 let pause b = in_pause := b;;
179 let cond = Condition.create ();;
180 let mutex = Mutex.create ();;
181 let hint = ref None;;
182 let prune_hint = ref [];;
184 let step _ = Condition.signal cond;;
185 let give_hint n = hint := Some n;;
186 let give_prune_hint hint =
187 prune_hint := hint :: !prune_hint
194 Condition.wait cond mutex;
199 let get_auto_status _ =
200 let status = !auto_status in
201 let and_list,elems,last =
204 | (m,s,_,don,gl,fail)::tl ->
207 (fun (id,d,_ as g) ->
208 match calculate_goal_ty g s m with
209 | Some (_,x) -> Some (id,x,d) | None -> None)
213 (* these are the S goalsin the or list *)
216 (fun (m,s,_,don,gl,fail) ->
218 (function S (g,k,c,_) -> Some (g,k,c) | _ -> None)
222 (* this function eats id from a list l::[id,x] returning x, l *)
223 let eat_tail_if_eq id l =
224 let rec aux (s, l) = function
226 | ((id1,_,_),k1,c)::tl when id = id1 ->
228 | None -> aux (Some c,l) tl
229 | Some _ -> assert false)
230 | ((id1,_,_),k1,c as e)::tl -> aux (s, e::l) tl
232 let c, l = aux (None, []) l in
235 let eat_in_parallel id l =
236 let rec aux (b,eaten, new_l as acc) l =
240 match eat_tail_if_eq id l with
241 | None, l -> aux (b@[false], eaten, new_l@[l]) tl
242 | Some t,l -> aux (b@[true],eaten@[t], new_l@[l]) tl
246 let rec eat_all rows l =
250 match List.rev elem with
251 | ((to_eat,depth,_),k,_)::next_lunch ->
252 let b, eaten, l = eat_in_parallel to_eat l in
253 let eaten = HExtlib.list_uniq eaten in
254 let eaten = List.rev eaten in
255 let b = true (* List.hd (List.rev b) *) in
256 let rows = rows @ [to_eat,k,b,depth,eaten] in
258 | [] -> eat_all rows or_list
260 eat_all [] (List.rev orlist)
264 (function (S (_,_,(_,c),_)) -> Some c | _ -> None)
267 (* let rows = List.filter (fun (_,l) -> l <> []) rows in *)
268 and_list, rows, history
270 !auto_context, elems, and_list, last
273 (* Works if there is no dependency over proofs *)
274 let is_a_green_cut goalty =
275 CicUtil.is_meta_closed goalty
277 let rec first_s = function
278 | (D _)::tl -> first_s tl
279 | (S (g,k,c,s))::tl -> Some ((g,k,c,s),tl)
282 let list_union l1 l2 =
283 (* TODO ottimizzare compare *)
284 HExtlib.list_uniq (List.sort compare (l1 @ l1))
286 let rec eq_todo l1 l2 =
288 | (D g1) :: tl1,(D g2) :: tl2 when g1=g2 -> eq_todo tl1 tl2
289 | (S (g1,k1,(c1,lt1),i1)) :: tl1, (S (g2,k2,(c2,lt2),i2)) :: tl2
290 when i1 = i2 && g1 = g2 && k1 = k2 && c1 = c2 ->
291 if Lazy.force lt1 = Lazy.force lt2 then eq_todo tl1 tl2 else false
295 let eat_head todo id fl orlist =
296 let rec aux acc = function
298 | (m, s, _, _, todo1, fl1)::tl as orlist ->
300 match first_s todo1 with
301 | None -> orlist, acc
302 | Some (((gno,_,_),_,_,_), todo11) ->
303 (* TODO confronto tra todo da ottimizzare *)
304 if gno = id && eq_todo todo11 todo then
305 aux (list_union fl1 acc) tl
313 let close_proof p ty menv context =
315 List.map fst (CicUtil.metas_of_term p @ CicUtil.metas_of_term ty)
317 let menv = List.filter (fun (i,_,_) -> List.exists ((=)i) metas) menv in
318 naif_closure p menv context
320 (* XXX capire bene quando aggiungere alla cache *)
321 let add_to_cache_and_del_from_orlist_if_green_cut
322 g s m cache key todo orlist fl ctx size minsize
324 let cache = cache_remove_underinspection cache key in
325 (* prima per fare la irl usavamo il contesto vero e proprio e non quello
327 match calculate_closed_goal_ty g s with
328 | None -> assert false
329 | Some (canonical_ctx , gty) ->
330 let goalno,depth,sort = g in
331 let irl = mk_irl canonical_ctx in
332 let goal = Cic.Meta(goalno, irl) in
333 let proof = CicMetaSubst.apply_subst s goal in
334 let green_proof, closed_proof =
335 let b = is_a_green_cut proof in
337 b, (* close_proof proof gty m ctx *) proof
341 debug_print (lazy ("TENTATIVE CACHE: " ^ CicPp.ppterm key));
342 if is_a_green_cut key then
343 (* if the initia goal was closed, we cut alternatives *)
344 let _ = debug_print (lazy ("MANGIO: " ^ string_of_int goalno)) in
345 let orlist, fl = eat_head todo goalno fl orlist in
347 if size < minsize then
348 (debug_print (lazy ("NO CACHE: 2 (size <= minsize)"));cache)
350 (* if the proof is closed we cache it *)
351 if green_proof then cache_add_success cache key proof
352 else (* cache_add_success cache key closed_proof *)
353 (debug_print (lazy ("NO CACHE: (no gree proof)"));cache)
355 cache, orlist, fl, true
358 debug_print (lazy ("TENTATIVE CACHE: " ^ CicPp.ppterm gty));
359 if size < minsize then
360 (debug_print (lazy ("NO CACHE: (size <= minsize)")); cache) else
361 (* if the substituted goal and the proof are closed we cache it *)
362 if is_a_green_cut gty then
363 if green_proof then cache_add_success cache gty proof
364 else (* cache_add_success cache gty closed_proof *)
365 (debug_print (lazy ("NO CACHE: (no green proof (gty))"));cache)
369 CicTypeChecker.type_of_aux' ~subst:s
370 m ctx closed_proof CicUniv.oblivion_ugraph
372 if is_a_green_cut ty then
373 cache_add_success cache ty closed_proof
376 | CicTypeChecker.TypeCheckerFailure _ ->*)
377 (debug_print (lazy ("NO CACHE: (no green gty )"));cache)
379 cache, orlist, fl, false
381 let close_failures (fl : fail list) (cache : cache) =
383 (fun cache ((gno,depth,_),gty) ->
384 if CicUtil.is_meta_closed gty then
385 ( debug_print (lazy ("FAIL: INDUCED: " ^ string_of_int gno));
386 cache_add_failure cache gty depth)
391 let put_in_subst subst metasenv (goalno,_,_) canonical_ctx t ty =
392 let entry = goalno, (canonical_ctx, t,ty) in
393 assert_subst_are_disjoint subst [entry];
394 let subst = entry :: subst in
396 let metasenv = CicMetaSubst.apply_subst_metasenv subst metasenv in
401 let mk_fake_proof metasenv subst (goalno,_,_) goalty context =
402 None,metasenv,subst ,(lazy (Cic.Meta(goalno,mk_irl context))),goalty, []
406 tables cache depth fake_proof goalno goalty subst context
409 let active,passive,bag = tables in
410 let ppterm = ppterm context in
411 let status = (fake_proof,goalno) in
412 if flags.use_only_paramod then
414 debug_print (lazy ("PARAMODULATION SU: " ^
415 string_of_int goalno ^ " " ^ ppterm goalty ));
416 let goal_steps, saturation_steps, timeout =
417 max_int,max_int,flags.timeout
420 Saturation.given_clause bag status active passive
421 goal_steps saturation_steps timeout
423 | None, active, passive, bag ->
424 [], (active,passive,bag), cache, flags
425 | Some(subst',(_,metasenv,_subst,proof,_, _),open_goals),active,
427 assert_subst_are_disjoint subst subst';
428 let subst = subst@subst' in
430 order_new_goals metasenv subst open_goals ppterm
433 List.map (fun (x,sort) -> x,depth-1,sort) open_goals
436 [(!candidate_no,proof),metasenv,subst,open_goals],
437 (active,passive,bag), cache, flags
441 debug_print (lazy ("NARROWING DEL GOAL: " ^
442 string_of_int goalno ^ " " ^ ppterm goalty ));
443 let goal_steps, saturation_steps, timeout =
447 Saturation.solve_narrowing bag status active passive goal_steps
449 | None, active, passive, bag ->
450 [], (active,passive,bag), cache, flags
451 | Some(subst',(_,metasenv,_subst,proof,_, _),open_goals),active,
453 assert_subst_are_disjoint subst subst';
454 let subst = subst@subst' in
456 order_new_goals metasenv subst open_goals ppterm
459 List.map (fun (x,sort) -> x,depth-1,sort) open_goals
462 [(!candidate_no,proof),metasenv,subst,open_goals],
463 (active,passive,bag), cache, flags
467 let params = ([],["use_context","false"]) in
468 let automation_cache = {
469 AutomationCache.tables = tables ;
470 AutomationCache.univ = Universe.empty; }
473 let ((_,metasenv,subst,_,_,_),open_goals) =
475 solve_rewrite ~params ~automation_cache
478 let proof = lazy (Cic.Meta (-1,[])) in
479 [(!candidate_no,proof),metasenv,subst,[]],tables, cache, flags
480 with ProofEngineTypes.Fail _ -> [], tables, cache, flags
482 let res = Saturation.all_subsumed bag status active passive in
485 (fun (subst',(_,metasenv,_subst,proof,_, _),open_goals) ->
486 assert_subst_are_disjoint subst subst';
487 let subst = subst@subst' in
489 order_new_goals metasenv subst open_goals ppterm
492 List.map (fun (x,sort) -> x,depth-1,sort) open_goals
495 (!candidate_no,proof),metasenv,subst,open_goals)
498 res', (active,passive,bag), cache, flags
505 List.sort (fun (_,_,_,l1) (_,_,_,l2) ->
506 let p1 = List.length (prop_only l1) in
507 let p2 = List.length (prop_only l2) in
508 if p1 = p2 then List.length l1 - List.length l2 else p1-p2)
512 let try_candidate dbd
513 goalty tables subst fake_proof goalno depth context cand
515 let ppterm = ppterm context in
517 let actives, passives, bag = tables in
518 let (_,metasenv,subst,_,_,_), open_goals =
519 ProofEngineTypes.apply_tactic
520 (PrimitiveTactics.apply_tac ~term:cand)
523 let tables = actives, passives,
524 Equality.push_maxmeta bag
525 (max (Equality.maxmeta bag) (CicMkImplicit.new_meta metasenv subst))
527 debug_print (lazy (" OK: " ^ ppterm cand));
528 let metasenv = CicRefine.pack_coercion_metasenv metasenv in
529 let open_goals = order_new_goals metasenv subst open_goals ppterm in
530 let open_goals = List.map (fun (x,sort) -> x,depth-1,sort) open_goals in
532 Some ((!candidate_no,lazy cand),metasenv,subst,open_goals), tables
534 | ProofEngineTypes.Fail s -> None,tables
535 | CicUnification.Uncertain s -> None,tables
538 let applicative_case dbd
539 tables depth subst fake_proof goalno goalty metasenv context
540 signature universe cache flags
544 | Cic.Appl (hd::tl) ->
545 Cic.Appl (hd :: HExtlib.mk_list (Cic.Meta (0,[])) (List.length tl))
548 let goalty_aux = goalty in
550 get_candidates flags.skip_trie_filtering universe cache goalty_aux
552 (* if the goal is an equality we skip the congruence theorems
554 if is_equational_case goalty flags
555 then List.filter not_default_eq_term candidates
558 let candidates = List.filter (only signature context metasenv) candidates
562 (fun (tables,elems) cand ->
564 try_candidate dbd goalty
565 tables subst fake_proof goalno depth context cand
567 | None, tables -> tables, elems
568 | Some x, tables -> tables, x::elems)
569 (tables,[]) candidates
571 let elems = sort_new_elems elems in
575 let try_smart_candidate dbd
576 goalty tables subst fake_proof goalno depth context cand
578 let ppterm = ppterm context in
580 let params = ([],[]) in
581 let automation_cache = {
582 AutomationCache.tables = tables ;
583 AutomationCache.univ = Universe.empty; }
585 debug_print (lazy ("candidato per " ^ string_of_int goalno
586 ^ ": " ^ CicPp.ppterm cand));
588 let (_,metasenv,subst,_,_,_) = fake_proof in
589 prerr_endline ("metasenv:\n" ^ CicMetaSubst.ppmetasenv [] metasenv);
590 prerr_endline ("subst:\n" ^ CicMetaSubst.ppsubst ~metasenv subst);
592 let ((_,metasenv,subst,_,_,_),open_goals) =
593 apply_smart ~dbd ~term:cand ~params ~automation_cache
596 let metasenv = CicRefine.pack_coercion_metasenv metasenv in
597 let open_goals = order_new_goals metasenv subst open_goals ppterm in
598 let open_goals = List.map (fun (x,sort) -> x,depth-1,sort) open_goals in
600 Some ((!candidate_no,lazy cand),metasenv,subst,open_goals), tables
602 | ProofEngineTypes.Fail s -> None,tables
603 | CicUnification.Uncertain s -> None,tables
606 let smart_applicative_case dbd
607 tables depth subst fake_proof goalno goalty metasenv context signature
612 | Cic.Appl (hd::tl) ->
613 Cic.Appl (hd :: HExtlib.mk_list (Cic.Meta (0,[])) (List.length tl))
616 let smart_candidates =
617 get_candidates flags.skip_trie_filtering universe cache goalty_aux
620 get_candidates flags.skip_trie_filtering universe cache goalty
622 let smart_candidates =
624 (fun x -> not(List.mem x candidates)) smart_candidates
627 (lazy ("smart_candidates" ^ " = " ^
628 (String.concat "\n" (List.map CicPp.ppterm smart_candidates)))) in
629 debug_print debug_msg;
630 let candidates = List.filter (only signature context metasenv) candidates in
631 let smart_candidates =
632 List.filter (only signature context metasenv) smart_candidates
635 let penalty cand depth =
636 if only signature context metasenv cand then depth else ((prerr_endline (
637 "penalizzo " ^ CicPp.ppterm cand));depth -1)
642 (fun (tables,elems) cand ->
644 try_candidate dbd goalty
645 tables subst fake_proof goalno depth context cand
648 (* if normal application fails we try to be smart *)
649 (match try_smart_candidate dbd goalty
650 tables subst fake_proof goalno depth context cand
652 | None, tables -> tables, elems
653 | Some x, tables -> tables, x::elems)
654 | Some x, tables -> tables, x::elems)
655 (tables,[]) candidates
657 let tables, smart_elems =
659 (fun (tables,elems) cand ->
661 try_smart_candidate dbd goalty
662 tables subst fake_proof goalno depth context cand
664 | None, tables -> tables, elems
665 | Some x, tables -> tables, x::elems)
666 (tables,[]) smart_candidates
668 let elems = sort_new_elems (elems @ smart_elems) in
672 let equational_and_applicative_case dbd
673 signature universe flags m s g gty tables cache context
675 let goalno, depth, sort = g in
676 let fake_proof = mk_fake_proof m s g gty context in
677 if is_equational_case gty flags then
678 let elems,tables,cache, flags =
679 equational_case tables cache
680 depth fake_proof goalno gty s context flags
682 let more_elems, tables, cache =
683 if flags.use_only_paramod then
687 tables depth s fake_proof goalno
688 gty m context signature universe cache flags
690 elems@more_elems, tables, cache, flags
692 let elems, tables, cache =
693 match LibraryObjects.eq_URI () with
695 smart_applicative_case dbd tables depth s fake_proof goalno
696 gty m context signature universe cache flags
698 applicative_case dbd tables depth s fake_proof goalno
699 gty m context signature universe cache flags
701 elems, tables, cache, flags
703 let rec condition_for_hint i = function
705 | S (_,_,(j,_),_):: tl -> j <> i (* && condition_for_hint i tl *)
706 | _::tl -> condition_for_hint i tl
708 let prunable_for_size flags s m todo =
709 let rec aux b = function
710 | (S _)::tl -> aux b tl
711 | (D (_,_,T))::tl -> aux b tl
713 (match calculate_goal_ty g s m with
715 | Some (canonical_ctx, gty) ->
718 ~consider_metas:false ~count_metas_occurrences:true gty in
719 let newb = b || gsize > flags.maxgoalsizefactor in
726 let prunable ty todo =
727 let rec aux b = function
728 | (S(_,k,_,_))::tl -> aux (b || Equality.meta_convertibility k ty) tl
729 | (D (_,_,T))::tl -> aux b tl
737 let prunable menv subst ty todo =
738 let rec aux = function
739 | (S(_,k,_,_))::tl ->
740 (match Equality.meta_convertibility_subst k ty menv with
743 no_progress variant tl (* || aux tl*))
744 | (D (_,_,T))::tl -> aux tl
746 and no_progress variant = function
747 | [] -> (*prerr_endline "++++++++++++++++++++++++ no_progress";*) true
748 | D ((n,_,P) as g)::tl ->
749 (match calculate_goal_ty g subst menv with
750 | None -> no_progress variant tl
752 (match calculate_goal_ty g variant menv with
753 | None -> assert false
755 if gty = gty' then no_progress variant tl
757 (prerr_endline (string_of_int n);
758 prerr_endline (CicPp.ppterm gty);
759 prerr_endline (CicPp.ppterm gty');
760 prerr_endline "---------- subst";
761 prerr_endline (CicMetaSubst.ppsubst ~metasenv:menv subst);
762 prerr_endline "---------- variant";
763 prerr_endline (CicMetaSubst.ppsubst ~metasenv:menv variant);
764 prerr_endline "---------- menv";
765 prerr_endline (CicMetaSubst.ppmetasenv [] menv);
766 no_progress variant tl) *)
768 | _::tl -> no_progress variant tl
773 let condition_for_prune_hint prune (m, s, size, don, todo, fl) =
775 HExtlib.filter_map (function S (_,_,(c,_),_) -> Some c | _ -> None) todo
777 List.for_all (fun i -> List.for_all (fun j -> i<>j) prune) s
779 let filter_prune_hint c l =
780 let prune = !prune_hint in
781 prune_hint := []; (* possible race... *)
782 if prune = [] then c,l
784 cache_reset_underinspection c,
785 List.filter (condition_for_prune_hint prune) l
791 auto_all_solutions dbd tables universe cache context metasenv gl flags
796 MetadataConstraints.UriManagerSet.union set
797 (MetadataQuery.signature_of metasenv g)
799 MetadataConstraints.UriManagerSet.empty gl
801 let goals = order_new_goals metasenv [] gl CicPp.ppterm in
804 (fun (x,s) -> D (x,flags.maxdepth,s)) goals
806 let elems = [metasenv,[],1,[],goals,[]] in
807 let rec aux tables solutions cache elems flags =
808 match auto_main dbd tables context flags signature universe cache elems with
809 | Gaveup (tables,cache) ->
810 solutions,cache, tables
811 | Proved (metasenv,subst,others,tables,cache) ->
812 if Unix.gettimeofday () > flags.timeout then
813 ((subst,metasenv)::solutions), cache, tables
815 aux tables ((subst,metasenv)::solutions) cache others flags
817 let rc = aux tables [] cache elems flags in
819 | [],cache,tables -> [],cache,tables
820 | solutions, cache,tables ->
823 (fun (subst,newmetasenv) ->
825 ProofEngineHelpers.compare_metasenvs ~oldmetasenv:metasenv ~newmetasenv
827 if opened = [] then Some subst else None)
830 solutions,cache,tables
833 (******************* AUTO ***************)
836 let auto dbd flags metasenv tables universe cache context metasenv gl =
837 let initial_time = Unix.gettimeofday() in
841 MetadataConstraints.UriManagerSet.union set
842 (MetadataQuery.signature_of metasenv g)
844 MetadataConstraints.UriManagerSet.empty gl
846 let goals = order_new_goals metasenv [] gl CicPp.ppterm in
847 let goals = List.map (fun (x,s) -> D(x,flags.maxdepth,s)) goals in
848 let elems = [metasenv,[],1,[],goals,[]] in
849 match auto_main dbd tables context flags signature universe cache elems with
850 | Proved (metasenv,subst,_, tables,cache) ->
852 ("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time)));
853 Some (subst,metasenv), cache
854 | Gaveup (tables,cache) ->
856 ("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time)));
860 let auto_tac ~(dbd:HSql.dbd) ~params:(univ,params) ~automation_cache (proof, goal) =
861 let flags = flags_of_params params () in
862 let use_library = flags.use_library in
863 let universe, tables, cache =
864 init_cache_and_tables
865 ~dbd ~use_library ~use_context:(not flags.skip_context)
866 automation_cache univ (proof, goal)
868 let _,metasenv,subst,_,_, _ = proof in
869 let _,context,goalty = CicUtil.lookup_meta goal metasenv in
870 let signature = MetadataQuery.signature_of metasenv goal in
875 CicTypeChecker.type_of_aux' metasenv context t
876 CicUniv.oblivion_ugraph
878 MetadataConstraints.UriManagerSet.union set
879 (MetadataConstraints.constants_of ty)
884 if flags.close_more then
886 tables context (proof, goal)
887 (auto_all_solutions dbd) signature universe cache
889 let initial_time = Unix.gettimeofday() in
890 let (_,oldmetasenv,_,_,_, _) = proof in
893 metasenv,subst,1,[],[D (goal,flags.maxdepth,P)],[]
895 match auto_main dbd tables context flags signature universe cache [elem] with
896 | Proved (metasenv,subst,_, tables,cache) ->
898 ("TIME:"^string_of_float(Unix.gettimeofday()-.initial_time)));
900 ProofEngineHelpers.subst_meta_and_metasenv_in_proof
901 proof goal subst metasenv
904 ProofEngineHelpers.compare_metasenvs ~oldmetasenv
905 ~newmetasenv:metasenv
908 | Gaveup (tables,cache) ->
911 string_of_float(Unix.gettimeofday()-.initial_time)));
912 raise (ProofEngineTypes.Fail (lazy "Auto gave up"))
917 type th_cache = (NCic.context * InvRelDiscriminationTree.t) list
919 let keys_of_term status t =
920 let status, orig_ty = typeof status (ctx_of t) t in
921 let _, ty, _ = saturate ~delta:max_int status orig_ty in
924 let _, ty = term_of_cic_term status ty (ctx_of ty) in
926 | NCic.Const (NReference.Ref (_,NReference.Def h))
927 | NCic.Appl (NCic.Const(NReference.Ref(_,NReference.Def h))::_)
929 let _,ty,_= saturate status ~delta:(h-1) orig_ty in
936 let mk_th_cache status gl =
938 (fun (status, acc) g ->
939 let gty = get_goalty status g in
940 let ctx = ctx_of gty in
941 debug_print(lazy("th cache for: "^ppterm status gty));
942 debug_print(lazy("th cache in: "^ppcontext status ctx));
943 if List.mem_assq ctx acc then status, acc else
944 let idx = InvRelDiscriminationTree.empty in
947 (fun (status, i, idx) _ ->
948 let t = mk_cic_term ctx (NCic.Rel i) in
949 debug_print(lazy("indexing: "^ppterm status t));
950 let status, keys = keys_of_term status t in
952 List.fold_left (fun idx k ->
953 InvRelDiscriminationTree.index idx k t) idx keys
958 status, (ctx, idx) :: acc)
962 let add_to_th t c ty =
963 let key_c = ctx_of t in
964 if not (List.mem_assq key_c c) then
965 (key_c ,InvRelDiscriminationTree.index
966 InvRelDiscriminationTree.empty ty t ) :: c
968 let rec replace = function
970 | (x, idx) :: tl when x == key_c ->
971 (x, InvRelDiscriminationTree.index idx ty t) :: tl
972 | x :: tl -> x :: replace tl
977 let pp_idx status idx =
978 InvRelDiscriminationTree.iter idx
980 debug_print(lazy("K: " ^ NCicInverseRelIndexable.string_of_path k));
982 (fun t -> debug_print(lazy("\t"^ppterm status t)))
989 debug_print(lazy( "-----------------------------------------------"));
990 debug_print(lazy( (NCicPp.ppcontext ~metasenv:[] ~subst:[] ctx)));
991 debug_print(lazy( "||====> "));
996 let search_in_th gty th =
997 let c = ctx_of gty in
998 let rec aux acc = function
999 | [] -> Ncic_termSet.elements acc
1002 let idx = List.assq k th in
1003 let acc = Ncic_termSet.union acc
1004 (InvRelDiscriminationTree.retrieve_unifiables idx gty)
1007 with Not_found -> aux acc tl
1009 aux Ncic_termSet.empty c
1011 type cache_examination_result =
1014 | `Succeded of NCic.term
1019 type goal = int * sort (* goal, depth, sort *)
1020 type fail = goal * cic_term
1021 type candidate = int * Ast.term (* unique candidate number, candidate *)
1024 (* goal has to be proved *)
1026 (* goal has to be cached as a success obtained using candidate as the first
1028 | S of goal * (#tac_status as 'a)
1029 (* * cic_term * candidate (* int was minsize *) *)
1031 let pp_goal (g,_) = string_of_int g
1032 let pp_item = function
1033 | D g -> "D" ^ pp_goal g
1034 | S (g,_) -> "S" ^ pp_goal g
1037 do_types : bool; (* solve goals in Type *)
1044 type 'a tree_status = #tac_status as 'a * int * int
1045 type 'a tree_item = 'a op
1048 (AndOrTree.andT, 'a tree_status, 'a tree_item) AndOrTree.position
1050 (AndOrTree.orT, 'a tree_status, 'a tree_item) AndOrTree.position
1052 type 'a auto_status = 'a and_pos * th_cache
1054 type 'a auto_result =
1056 | Proved of (#tac_status as 'a) * 'a auto_status option (* alt. proofs *)
1058 let close_failures _ c = c;;
1059 let prunable _ _ _ = false;;
1060 let cache_examine cache gty = `Notfound;;
1061 let put_in_subst s _ _ _ = s;;
1062 let add_to_cache_and_del_from_orlist_if_green_cut _ _ c _ _ o f _ = c, o, f, false ;;
1063 let cache_add_underinspection c _ _ = c;;
1064 let equational_case _ _ _ _ _ _ = [];;
1065 let only _ _ _ = true;;
1067 let candidate_no = ref 0;;
1069 let sort_new_elems l =
1070 List.sort (fun (_,_,_,l1) (_,_,_,l2) -> List.length l1 - List.length l2) l
1073 let try_candidate status t g =
1075 debug_print (lazy (" try " ^ CicNotationPp.pp_term t));
1076 let status = NTactics.focus_tac [g] status in
1077 let status = NTactics.apply_tac ("",0,t) status in
1078 let open_goals = head_goals status#stack in
1080 (lazy (" success: "^String.concat " "(List.map string_of_int open_goals)));
1082 Some ((!candidate_no,t),status,open_goals)
1083 with Error (msg,exn) -> debug_print (lazy " failed"); None
1086 let rec mk_irl n = function
1088 | _ :: tl -> NCic.Rel n :: mk_irl (n+1) tl
1091 let get_candidates status cache_th signature gty =
1092 let universe = status#auto_cache in
1093 let context = ctx_of gty in
1094 let _, raw_gty = term_of_cic_term status gty context in
1096 NDiscriminationTree.DiscriminationTree.retrieve_unifiables universe raw_gty
1099 List.filter (only signature context)
1100 (NDiscriminationTree.TermSet.elements cands)
1103 let _status, t = term_of_cic_term status t context in Ast.NCic t)
1104 (search_in_th gty cache_th)
1106 List.map (function NCic.Const r -> Ast.NRef r | _ -> assert false) cands
1109 let applicative_case signature status flags g gty cache =
1110 let candidates = get_candidates status cache signature gty in
1111 debug_print (lazy ("candidates: " ^ string_of_int (List.length candidates)));
1115 match try_candidate status cand g with
1117 | Some x -> x::elems)
1123 let equational_and_applicative_case
1124 signature flags status g depth gty cache
1127 if false (*is_equational_case gty flags*) then
1130 signature status flags g gty cache
1134 signature status flags g gty cache
1139 (*match LibraryObjects.eq_URI () with
1141 smart_applicative_case dbd tables depth s fake_proof goalno
1142 gty m context signature universe cache flags
1145 signature status flags g gty cache
1150 (* XXX calculate the sort *)
1151 List.map (fun c,s,gl -> c,1,s,List.map (fun i -> i,P) gl) elems
1153 let elems = sort_new_elems elems in
1157 let calculate_goal_ty (goalno,_) status =
1158 try Some (get_goalty status goalno)
1159 with Error _ -> None
1162 let rec aux acc = function
1163 | (D g)::tl -> aux (acc@[g]) tl
1164 | (S _)::tl -> aux acc tl
1170 List.filter (function (_,_,P) -> true | _ -> false) l
1173 let rec guess_name name ctx =
1174 if name = "_" then guess_name "auto" ctx else
1175 if not (List.mem_assoc name ctx) then name else
1176 guess_name (name^"'") ctx
1179 let intro_case status gno gty depth cache name =
1180 let status = NTactics.focus_tac [gno] status in
1181 let status = NTactics.intro_tac (guess_name name (ctx_of gty)) status in
1182 let open_goals = head_goals status#stack in
1183 assert (List.length open_goals = 1);
1184 let open_goal = List.hd open_goals in
1185 let ngty = get_goalty status open_goal in
1186 let ctx = ctx_of ngty in
1187 let t = mk_cic_term ctx (NCic.Rel 1) in
1188 let status, keys = keys_of_term status t in
1189 let cache = List.fold_left (add_to_th t) cache keys in
1190 debug_print (lazy (" intro: "^ string_of_int open_goal));
1191 (* pp_th status cache; *)
1193 (* XXX calculate the sort *)
1194 [(!candidate_no,Ast.Implicit `JustOne),0,status,[open_goal,P]],
1198 let do_something signature flags s gno depth gty cache =
1199 let _s, raw_gty = term_of_cic_term s gty (ctx_of gty) in
1201 | NCic.Prod (name,_,_) -> intro_case s gno gty depth cache name
1203 equational_and_applicative_case signature flags s gno depth gty cache
1207 module Z = AndOrTree
1210 debug_print (lazy("generating a.dot"));
1212 let oc = open_out "/tmp/a.dot" in
1213 let fmt = Format.formatter_of_out_channel oc in
1214 GraphvizPp.Dot.header fmt;
1215 Z.dump pp_item pos fmt;
1216 GraphvizPp.Dot.trailer fmt;
1217 Format.fprintf fmt "@?";
1219 ignore(Sys.command ("dot -Tpng /tmp/a.dot > /tmp/a.png"));
1220 ignore(Sys.command ("gnome-open /tmp/a.png")))
1223 let rightmost_bro pred =
1225 match Z.right pos with
1228 if pred pos then Some pos else fst pos
1234 match Z.getO pos with
1239 let rec next_choice_point (pos : 'a and_pos) : 'a or_pos option =
1240 let rec giveup_right_giveup_up_backtrack_left (pos : 'a and_pos) =
1241 match Z.upA pos with
1244 match rightmost_bro is_not_S alts with
1246 let upalts = Z.upO alts in
1247 let upalts = Z.inject T.Nil upalts in
1248 backtrack_left_giveup_right_giveup_up upalts
1250 and backtrack_left_giveup_right_giveup_up (pos : 'a and_pos) =
1251 let pos = Z.inject T.Nil pos in
1252 let pos = match Z.getA pos with s,D g | s, S (g,_) -> Z.setA s (D g) pos in
1253 match Z.left pos with
1254 | None -> giveup_right_giveup_up_backtrack_left pos
1255 | Some (pos as left_bro) ->
1256 match Z.downA pos with
1257 | Z.Unexplored -> assert false (* we explore left2right *)
1258 | Z.Alternatives alts ->
1259 match rightmost_bro is_not_S alts with
1260 | None -> backtrack_left_giveup_right_giveup_up left_bro
1263 backtrack_left_giveup_right_giveup_up pos
1266 let auto_main flags signature (pos : 'a and_pos) cache =
1267 let solved g depth size s pos =
1268 Z.inject (T.Node(`Or,[D g,T.Node(`And(s,depth,size),[])])) pos
1271 Z.inject (T.Node(`Or,[])) pos
1274 let rec next ~unfocus (pos : 'a and_pos) cache =
1276 match Z.downA pos with
1277 | Z.Unexplored -> attack pos cache (Z.getA pos)
1278 | Z.Alternatives pos -> nextO ~unfocus pos cache
1280 and nextO ~unfocus (pos : 'a or_pos) cache =
1281 match Z.getO pos with
1282 | S _ -> assert false (* XXX set to Nil when backtracking *)
1284 match Z.downO pos with
1285 | Z.Solution (s,_,_) -> move_solution_up ~unfocus s pos cache
1286 | Z.Todo pos -> next ~unfocus:true pos cache
1288 and next_choice (pos : 'a and_pos) cache =
1289 match next_choice_point pos with
1291 | Some pos -> nextO ~unfocus:true pos cache
1293 and move_solution_up
1294 ~unfocus (status : #tac_status as 'a) (pos : 'a or_pos) cache
1296 let pos = (* mark as solved *)
1297 match Z.getO pos with
1298 | S _ -> assert false (* XXX *)
1299 | D g -> Z.setO (S (g,status)) pos
1301 let pos = Z.upO pos in
1302 match Z.getA pos with
1303 | (_, size, depth), S (g,_)
1304 (* S if already solved and then solved again because of a backtrack *)
1305 | (_, size, depth), D g ->
1306 let newg = S (g,status) in(* TODO: cache success g *)
1307 let status = if unfocus then NTactics.unfocus_tac status else status in
1308 let news = status,size,depth in
1309 let pos = Z.setA news newg pos in
1310 match Z.right pos with
1311 | Some pos -> next ~unfocus:true pos cache
1313 match Z.upA pos with
1314 | None -> Proved (status, Some (pos,cache))
1315 | Some pos -> move_solution_up ~unfocus:true status pos cache
1317 and attack pos cache and_item =
1320 | _, S _ -> assert false (* next would close the proof or give a D *)
1321 | _ when Unix.gettimeofday () > flags.timeout ->
1322 debug_print (lazy ("fail timeout"));
1324 | (s, depth, width), D (_, T as g) when not flags.do_types ->
1325 debug_print (lazy "skip goal in Type");
1326 next ~unfocus:true (solved g depth width s pos) cache
1327 | (_,depth,_), D _ when depth > flags.maxdepth ->
1328 debug_print (lazy "fail depth");
1329 next_choice (failed pos) cache
1330 | (_,_,size), D _ when size > flags.maxsize ->
1331 debug_print (lazy "fail size");
1332 next_choice (failed pos) cache
1333 | (s,depth,size), D (gno,_ as g) ->
1334 (* assert unexplored *)
1335 assert (Z.eject pos = ZipTree.Nil);
1336 match calculate_goal_ty g s with
1338 debug_print (lazy ("success side effect: " ^ string_of_int gno));
1339 next ~unfocus:false (solved g depth size s pos) cache
1341 let s, gty = apply_subst s (ctx_of gty) gty in
1342 debug_print (lazy ("EXAMINE: "^ ppterm s gty));
1343 match cache_examine cache gty with
1344 | `Failed_in d when d <= depth ->
1345 debug_print (lazy ("fail depth (c): "^string_of_int gno));
1346 next_choice (failed pos) cache
1347 | `UnderInspection ->
1348 debug_print (lazy ("fail loop: " ^ string_of_int gno));
1349 next_choice (failed pos) cache
1351 debug_print (lazy ("success (c): " ^ string_of_int gno));
1352 let s = put_in_subst s g t gty in
1353 next ~unfocus:true (solved g depth size s pos) cache
1356 (* more depth or is the first time we see the goal *)
1357 if prunable s gty () then
1358 (debug_print (lazy( "fail one father is equal"));
1359 next_choice (failed pos) cache)
1361 let cache = cache_add_underinspection cache gty depth in
1362 debug_print (lazy ("INSPECTING: " ^
1363 string_of_int gno ^ "("^ string_of_int size ^ ") "));
1364 (* pos are possible computations for proving gty *)
1365 let subgoals, cache =
1366 do_something signature flags s gno depth gty cache
1368 if subgoals = [] then (* this goal has failed *)
1369 next_choice (failed pos) cache
1371 let size_gl l = List.length
1372 (List.filter (function (_,P) -> true | _ -> false) l)
1375 List.map (fun (_cand,depth_incr,s,gl) ->
1378 `And (s,depth+depth_incr,size+size_gl gl),
1379 List.map (fun g -> D g,ZipTree.Nil) gl))
1383 (Z.inject (ZipTree.Node (`Or,subtrees)) pos) cache
1385 (next ~unfocus:true pos cache : 'a auto_result)
1388 let int name l def =
1389 try int_of_string (List.assoc name l)
1390 with Failure _ | Not_found -> def
1393 let auto_tac ~params:(_univ,flags) status =
1394 let goals = head_goals status#stack in
1395 let status, cache = mk_th_cache status goals in
1396 (* pp_th status cache; *)
1398 NDiscriminationTree.DiscriminationTree.iter status#auto_cache (fun p t ->
1400 NDiscriminationTree.NCicIndexable.string_of_path p ^ " |--> " ^
1401 String.concat "\n " (List.map (
1402 NCicPp.ppterm ~metasenv:[] ~context:[] ~subst:[])
1403 (NDiscriminationTree.TermSet.elements t))
1406 let depth = int "depth" flags 3 in
1407 let size = int "size" flags 10 in
1408 let width = int "width" flags (3+List.length goals) in
1410 let goals = List.map (fun i -> D(i,P), ZipTree.Nil) goals in
1411 let elems = Z.start (ZipTree.Node (`And(status,0,0),goals)) in
1412 let signature = () in
1417 timeout = Unix.gettimeofday() +. 3000.;
1421 if x > y then raise (Error (lazy "auto gave up", None))
1423 let _ = debug_print (lazy("\n\nRound "^string_of_int x^"\n")) in
1424 let flags = { flags with maxdepth = x } in
1425 match auto_main flags signature elems cache with
1426 | Gaveup -> up_to (x+1) y
1428 HLog.debug ("proved at depth " ^ string_of_int x);
1431 | (g,t,k,f) :: rest -> (filter_open g,t,k,f):: rest
1439 let group_by_tac ~eq_predicate ~action:tactic status =
1440 let goals = head_goals status#stack in
1441 if List.length goals < 2 then tactic status
1443 let eq_predicate = eq_predicate status in
1444 let rec aux classes = function
1448 let c = List.find (fun c -> eq_predicate c g) classes in
1449 let classes = List.filter ((<>) c) classes in
1450 aux ((g::c) :: classes) tl
1451 with Not_found -> aux ([g] :: classes) tl
1453 let classes = aux [] goals in
1456 HLog.debug ("cluster:" ^ String.concat "," (List.map string_of_int l)))
1459 let l2 = HExtlib.list_mapi (fun x i -> x,i+1) l2 in
1460 List.map (fun x -> List.assoc x l2) l1
1462 NTactics.block_tac ([ NTactics.branch_tac ]
1464 HExtlib.list_concat ~sep:[NTactics.shift_tac]
1465 (List.map (fun gl-> [NTactics.pos_tac (pos_of gl goals); tactic]) classes)
1467 [ NTactics.merge_tac ]) status
1470 module IntSet = Set.Make(struct type t = int let compare = compare end)
1472 let type_dependency status gl g =
1473 let rec closure acc = function
1475 | x::l when IntSet.mem x acc -> closure acc l
1477 let acc = IntSet.add x acc in
1478 let gty = get_goalty status x in
1479 let deps = metas_of_term status gty in
1480 closure acc (deps @ l)
1482 not (IntSet.is_empty
1484 (closure IntSet.empty gl)
1485 (closure IntSet.empty [g])))
1488 let auto_tac ~params =
1489 group_by_tac ~eq_predicate:type_dependency ~action:(auto_tac ~params)
1492 (* ========================= dispatching of auto/auto_paramod ============ *)
1493 let auto_tac ~params:(_,flags as params) =
1494 if List.mem_assoc "paramodulation" flags then
1495 auto_paramod_tac ~params