in
aux fl
;;
+
+let prunable_for_size flags s m todo =
+ let rec aux b = function
+ | (S _)::tl -> aux b tl
+ | (D (_,_,T))::tl -> aux b tl
+ | (D g)::tl ->
+ (match calculate_goal_ty g s m with
+ | None -> aux b tl
+ | Some (canonical_ctx, gty) ->
+ let gsize, _ =
+ Utils.weight_of_term
+ ~consider_metas:false ~count_metas_occurrences:true gty in
+ let newb = b || gsize > flags.maxgoalsizefactor in
+ aux newb tl)
+ | [] -> b
+ in
+ aux false todo
+
+(*
let prunable ty todo =
let rec aux b = function
| (S(_,k,_,_))::tl -> aux (b || Equality.meta_convertibility k ty) tl
in
aux false todo
;;
+*)
+
+let prunable menv subst ty todo =
+ let rec aux = function
+ | (S(_,k,_,_))::tl ->
+ (match Equality.meta_convertibility_subst k ty menv with
+ | None -> 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
+ | Some (_, gty) ->
+ (match calculate_goal_ty g variant menv with
+ | None -> assert false
+ | Some (_, gty') ->
+ if gty = gty' then
+ no_progress variant tl
+ else false))
+ | _::tl -> no_progress subst tl
+ in
+ aux todo
+
+;;
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 ();
+*)
match elems with
+ | (m, s, size, don, todo, fl)::orlist as status 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)
| Some (canonical_ctx, gty) ->
let gsize, _ =
- Utils.weight_of_term ~count_metas_occurrences:true gty
+ Utils.weight_of_term ~consider_metas:false ~count_metas_occurrences:true gty
in
if gsize > flags.maxgoalsizefactor then
- (debug_print (lazy ("FAIL: SIZE: goal: "^string_of_int size));
+ (debug_print (lazy ("FAIL: SIZE: goal: "^string_of_int gsize));
aux tables maxm flags cache orlist)
- else
+ else if prunable_for_size flags s m todo then
+ (prerr_endline ("POTO at depth: "^(string_of_int depth));
+ aux tables maxm flags cache orlist)
+ else
(* still to be proved *)
(debug_print (lazy ("EXAMINE: "^CicPp.ppterm gty));
match cache_examine cache gty with
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 *)
- if prunable gty todo then
+ ( (* 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"));
aux tables maxm flags cache orlist)