From 260fdcc8b5855230f357673e0ea0c1cea47d49cf Mon Sep 17 00:00:00 2001 From: Enrico Tassi Date: Wed, 28 Oct 2009 13:37:07 +0000 Subject: [PATCH] better indentation --- helm/software/components/ng_tactics/nAuto.ml | 126 +++++++++---------- 1 file changed, 63 insertions(+), 63 deletions(-) diff --git a/helm/software/components/ng_tactics/nAuto.ml b/helm/software/components/ng_tactics/nAuto.ml index fe45320dd..2d460ff00 100644 --- a/helm/software/components/ng_tactics/nAuto.ml +++ b/helm/software/components/ng_tactics/nAuto.ml @@ -1320,69 +1320,69 @@ let auto_main flags signature (pos : 'a and_pos) cache = | Some pos -> move_solution_up ~unfocus:true status pos cache and attack pos cache and_item = - (* show pos; *) (* uncomment to show the tree *) - match and_item with - | _, S _ -> assert false (* next would close the proof or give a D *) - | (_, depth, _),_ when Unix.gettimeofday () > flags.timeout -> - debug_print ~depth (lazy ("fail timeout")); - Gaveup - | (s, depth, width), D (_, T as g) when not flags.do_types -> - debug_print ~depth (lazy "skip goal in Type"); - next ~unfocus:true (solved g depth width s pos) cache - | (_,depth,_), D _ when depth > flags.maxdepth -> - debug_print ~depth (lazy "fail depth"); - next_choice (failed pos) cache - | (_,depth,size), D _ when size > flags.maxsize -> - debug_print ~depth (lazy "fail size"); - next_choice (failed pos) cache - | (s,depth,size), D (gno,_ as g) -> - assert (Z.eject pos = T.Nil); (*subtree must be unexplored *) - match calculate_goal_ty g s with - | None -> - debug_print - ~depth (lazy ("success side effect: " ^ string_of_int gno)); - next ~unfocus:false (solved g depth size s pos) cache - | Some gty -> - let s, gty = apply_subst s (ctx_of gty) gty in - debug_print ~depth (lazy ("EXAMINE: "^ ppterm s gty)); - match cache_examine cache gty with - | `Failed_in d when d <= depth -> - debug_print ~depth(lazy("fail depth (c): "^string_of_int gno)); - next_choice (failed pos) cache - | `UnderInspection -> - debug_print ~depth (lazy("fail loop: "^string_of_int gno)); - next_choice (failed pos) cache - | `Succeded t -> - debug_print ~depth (lazy("success (c): "^string_of_int gno)); - let s = put_in_subst s g t gty in - next ~unfocus:true (solved g depth size s pos) cache - | `Notfound - | `Failed_in _ -> - (* more depth than before or first time we see the goal *) - if prunable s gty () then - (debug_print ~depth (lazy( "fail one father is equal")); - next_choice (failed pos) cache) - else - let cache = cache_add_underinspection cache gty depth in - debug_print ~depth (lazy ("INSPECTING: " ^ - string_of_int gno ^ "("^ string_of_int size ^ ") ")); - let subgoals, cache = - do_something signature flags s gno depth gty cache - in - if subgoals = [] then (* this goal has failed *) - next_choice (failed pos) cache - else - let size_gl l = List.length (prop_only l) in - let subtrees = - List.map - (fun (_cand,depth_incr,s,gl) -> - D(gno,P), - T.Node (`And (s,depth+depth_incr,size+size_gl gl), - List.map (fun g -> D g,T.Nil) gl)) - subgoals - in - next ~unfocus:true - (Z.inject (T.Node (`Or,subtrees)) pos) cache + (* show pos; *) (* uncomment to show the tree *) + match and_item with + | _, S _ -> assert false (* next would close the proof or give a D *) + | (_, depth, _),_ when Unix.gettimeofday () > flags.timeout -> + debug_print ~depth (lazy ("fail timeout")); + Gaveup + | (s, depth, width), D (_, T as g) when not flags.do_types -> + debug_print ~depth (lazy "skip goal in Type"); + next ~unfocus:true (solved g depth width s pos) cache + | (_,depth,_), D _ when depth > flags.maxdepth -> + debug_print ~depth (lazy "fail depth"); + next_choice (failed pos) cache + | (_,depth,size), D _ when size > flags.maxsize -> + debug_print ~depth (lazy "fail size"); + next_choice (failed pos) cache + | (s,depth,size), D (gno,_ as g) -> + assert (Z.eject pos = T.Nil); (*subtree must be unexplored *) + match calculate_goal_ty g s with + | None -> + debug_print + ~depth (lazy ("success side effect: " ^ string_of_int gno)); + next ~unfocus:false (solved g depth size s pos) cache + | Some gty -> + let s, gty = apply_subst s (ctx_of gty) gty in + debug_print ~depth (lazy ("EXAMINE: "^ ppterm s gty)); + match cache_examine cache gty with + | `Failed_in d when d <= depth -> + debug_print ~depth(lazy("fail depth (c): "^string_of_int gno)); + next_choice (failed pos) cache + | `UnderInspection -> + debug_print ~depth (lazy("fail loop: "^string_of_int gno)); + next_choice (failed pos) cache + | `Succeded t -> + debug_print ~depth (lazy("success (c): "^string_of_int gno)); + let s = put_in_subst s g t gty in + next ~unfocus:true (solved g depth size s pos) cache + | `Notfound + | `Failed_in _ -> + (* more depth than before or first time we see the goal *) + if prunable s gty () then + (debug_print ~depth (lazy( "fail one father is equal")); + next_choice (failed pos) cache) + else + let cache = cache_add_underinspection cache gty depth in + debug_print ~depth (lazy ("INSPECTING: " ^ + string_of_int gno ^ "("^ string_of_int size ^ ") ")); + let subgoals, cache = + do_something signature flags s gno depth gty cache + in + if subgoals = [] then (* this goal has failed *) + next_choice (failed pos) cache + else + let size_gl l = List.length (prop_only l) in + let subtrees = + List.map + (fun (_cand,depth_incr,s,gl) -> + D(gno,P), + T.Node (`And (s,depth+depth_incr,size+size_gl gl), + List.map (fun g -> D g,T.Nil) gl)) + subgoals + in + next ~unfocus:true + (Z.inject (T.Node (`Or,subtrees)) pos) cache in (next ~unfocus:true pos cache : 'a auto_result) ;; -- 2.39.2