+ and next_choice_point (pos : 'a and_pos) cache =
+
+ let rec global_choice_point (pos : 'a and_pos) : 'a auto_result =
+(* prerr_endline "global"; show pos; *)
+ match Z.upA pos with
+ | None -> Gaveup
+ | Some alts ->
+ let alts = Z.inject T.Nil alts in
+ let alts =
+ match Z.getO alts with
+ | S (s,g) -> Z.setO (L (s,g)) alts
+ | D (g) -> Z.setO (L (g,Obj.magic g)) alts
+ (* L (and other marks) for OR should have no arguments *)
+ | L _ -> assert false
+ in
+ match Z.right alts with
+ | None ->
+ let upalts = Z.upO alts in
+ let upalts = Z.inject T.Nil upalts in
+ let upalts =
+ match Z.getA upalts with
+ | s,S (a,b) -> Z.setA s (L (a,b)) upalts
+ | _,L _ -> assert false
+ | s,D (a) -> Z.setA s (L (a,Obj.magic a)) upalts
+ in
+ backtrack upalts
+ | Some pos ->
+ match Z.downO pos with
+ | Z.Solution (s,_,_) ->
+ move_solution_up ~unfocus:false true s pos cache
+ | Z.Todo pos -> next ~unfocus:true pos cache
+
+ and backtrack (pos : 'a and_pos) : 'a auto_result =
+(* prerr_endline "backtrack"; show pos; *)
+ let pos = Z.inject T.Nil pos in
+ let pos =
+ match Z.getA pos with
+ | s,D g | s, S (g,_) | s,L(g,_) -> Z.setA s (D g) pos
+ in
+ match first_left_mark_L_as_D is_aS pos with
+ | None -> global_choice_point pos
+ | Some pos ->
+ let rec local_choice_point pos =
+(* prerr_endline "local"; show pos; *)
+ match Z.downA pos with
+ | Z.Unexplored -> attack pos cache (Z.getA pos)
+ | Z.Alternatives alts ->
+ match leftmost_bro is_not_oL alts with
+ | None -> assert false (* is not L, thus has alternatives *)
+ | Some pos ->
+ let is_D = is_not_oS pos in
+ match if is_D then Z.downO pos else Z.downOr pos with
+ | Z.Solution (s,_,_) -> assert(is_D);
+ move_solution_up ~unfocus:false true s pos cache
+ | Z.Todo pos when is_D -> attack pos cache (Z.getA pos)
+ | Z.Todo pos ->
+ match first_left_mark_L_as_D is_aS pos with
+ | Some pos -> local_choice_point pos
+ | None -> assert false
+ in
+ local_choice_point pos
+ in
+ backtrack pos
+