let cond = Condition.create ();;
let mutex = Mutex.create ();;
let hint = ref None;;
+let prune_hint = ref [];;
let step _ = Condition.signal cond;;
let give_hint n = hint := Some n;;
+let give_prune_hint hint =
+ prune_hint := hint :: !prune_hint
+;;
let check_pause _ =
if !in_pause then
let prunable menv subst ty todo =
let rec aux = function
| (S(_,k,_,_))::tl ->
- (match Equality.meta_convertibility_subst k ty menv with
+ (match Equality.meta_convertibility_subst k ty menv with
| None -> aux tl
- | Some variant -> no_progress variant tl (* || aux tl)*) )
+ | Some variant ->
+ no_progress variant tl (* || aux tl*))
| (D (_,_,T))::tl -> aux tl
| _ -> false
and no_progress variant = function
| [] -> prerr_endline "++++++++++++++++++++++++ no_progress"; true
| D ((n,_,P) as g)::tl ->
(match calculate_goal_ty g subst menv with
- | None -> no_progress subst tl
+ | None -> no_progress variant tl
| Some (_, gty) ->
(match calculate_goal_ty g variant menv with
| None -> assert false
- | Some (_, gty') ->
+ | Some (_, gty') ->
if gty = gty' then
- no_progress variant tl
+ no_progress variant tl
else false))
- | _::tl -> no_progress subst tl
+ | _::tl -> no_progress variant tl
in
aux todo
;;
-
+let condition_for_prune_hint prune (m, s, size, don, todo, fl) =
+ let s =
+ HExtlib.filter_map (function S (_,_,(c,_),_) -> Some c | _ -> None) todo
+ in
+ List.for_all (fun i -> List.for_all (fun j -> i<>j) prune) s
+;;
+let filter_prune_hint l =
+ let prune = !prune_hint in
+ prune_hint := []; (* possible race... *)
+ if prune = [] then l
+ else List.filter (condition_for_prune_hint prune) l
+;;
let auto_main tables maxm context flags universe cache elems =
auto_context := context;
let rec aux tables maxm flags cache (elems : status) =
(* pp_status context elems; *)
+(* DEBUGGING CODE: uncomment these two lines to stop execution at each iteration
+ auto_status := elems;
+ check_pause ();
+*)
+ let elems = filter_prune_hint elems in
match elems with
+ | (m, s, size, don, todo, fl)::orlist when !hint <> None ->
+ (match !hint with
+ | Some i when condition_for_hint i todo ->
+ aux tables maxm flags cache orlist
+ | _ ->
+ hint := None;
+ aux tables maxm flags cache elems)
| [] ->
(* complete failure *)
Gaveup (tables, cache, maxm)
aux tables maxm flags cache ((m, s, size, don,todo, fl)::orlist)
| Notfound
| Failed_in _ when depth > 0 ->
- (match !hint with
- | Some i when condition_for_hint i todo ->
- aux tables maxm flags cache orlist
- | _ -> hint := None;
- (* more depth or is the first time we see the goal *)
+ ( (* more depth or is the first time we see the goal *)
if prunable m s gty todo then
(debug_print (lazy(
"FAIL: LOOP: one father is equal"));
let pp_proofterm = Equality.pp_proofterm;;
let revision = "$Revision$";;
+let size_and_depth context metasenv t = 100, 100