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) =
auto_status := elems;
check_pause ();
*)
+ let elems = filter_prune_hint elems in
match elems with
- | (m, s, size, don, todo, fl)::orlist as status when !hint <> None ->
+ | (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
let pp_proofterm = Equality.pp_proofterm;;
let revision = "$Revision$";;
+let size_and_depth context metasenv t = 100, 100