- let loop_cache =
- let under_inspection =
- add_to_th closegty cache.under_inspection closegty in
- {cache with under_inspection = under_inspection} in
- let unsat =
- List.fold_left
- (* the underscore information does not need to be returned
- by do_something *)
- (fun unsat ((_,t),status) ->
- let depth',looping_cache =
- if t=Ast.Ident("__whd",None) then depth,cache
- else depth+1, loop_cache in
- debug_print (~depth:depth')
- (lazy ("Case: " ^ CicNotationPp.pp_term t));
- let flags' =
- {flags with maxwidth = flags.maxwidth - ng +1} in
- (* sistemare *)
- let flags' =
- {flags' with last = flags'.last && (not branch)} in
- debug_print
- (lazy ("auto last: " ^ (string_of_bool flags'.last)));
- try auto_clusters flags' signature loop_cache
- depth' status; unsat
- with
- | Proved status ->
- debug_print (~depth:depth') (lazy "proved");
- if branch then
- let status = NTactics.merge_tac status
- in
- (* old cache, here *)
- let flags =
- {flags with maxwidth = flags.maxwidth - 1} in
- try auto_clusters flags signature cache
- depth status; assert false
- with Gaveup f ->
- debug_print ~depth
- (lazy ("Unsat1 at depth " ^ (string_of_int depth)
- ^ ": " ^
- (pp_goals status (IntSet.elements f))));
- (* TODO: cache failures *)
- IntSet.union f unsat
- else raise (Proved status)
- | Gaveup f ->
- debug_print (~depth:depth')
- (lazy ("Unsat2 at depth " ^ (string_of_int depth')
- ^ ": " ^
- (pp_goals status (IntSet.elements f))));
- (* TODO: cache local failures *)
- unsat)
- IntSet.empty alternatives
- in
- raise (Gaveup IntSet.add orig unsat)
-;;
-
+ let loop_cache =
+ let l,tree = cache.under_inspection in
+ let l,tree = closegty::l, add_to_th closegty tree closegty in
+ {cache with under_inspection = l,tree} in
+ List.iter
+ (fun ((_,t),status) ->
+ debug_print ~depth
+ (lazy("(re)considering goal " ^
+ (string_of_int g) ^" : "^ppterm status gty));
+ debug_print (~depth:depth)
+ (lazy ("Case: " ^ CicNotationPp.pp_term t));
+ let depth,cache =
+ if t=Ast.Ident("__whd",None) then depth, cache
+ else depth+1,loop_cache in
+ try
+ auto_clusters flags signature (cache:cache) depth status
+ with Gaveup _ ->
+ debug_print ~depth (lazy "Failed");())
+ alternatives;
+ raise (Gaveup IntSet.empty)
+;;
+