diff options
author | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-09-29 15:37:51 +0200 |
---|---|---|
committer | Gaëtan Gilbert <gaetan.gilbert@skyskimmer.net> | 2017-09-29 20:30:43 +0200 |
commit | 423ee45f91a88582983d0cc1928708dba5391ca7 (patch) | |
tree | 2b7d16f54c94f61a511321153ffcd0e9b99034c5 | |
parent | ef04917cb7b0a867aef13d2135f57f746600b664 (diff) |
Cleanup suggest_bullet
-rw-r--r-- | proofs/proof_bullet.ml | 40 |
1 files changed, 18 insertions, 22 deletions
diff --git a/proofs/proof_bullet.ml b/proofs/proof_bullet.ml index f80cb7cc6..4f575ab4b 100644 --- a/proofs/proof_bullet.ml +++ b/proofs/proof_bullet.ml @@ -110,10 +110,6 @@ module Strict = struct let push (b:t) pr = focus bullet_cond (b::get_bullets pr) 1 pr - (* Used only in the next function. - TODO: use a recursive function instead? *) - exception SuggestFound of t - let suggest_bullet (prf : proof): suggestion = if is_done prf then ProofFinished else if not (no_focused_goal prf) @@ -122,24 +118,24 @@ module Strict = struct | b::_ -> Unfinished b | _ -> NoBulletInUse else (* There is no goal under focus but some are unfocussed, - let us look at the bullet needed. If no *) - let pcobaye = ref prf in - try - while true do - let pcobaye', b = pop !pcobaye in - (* pop went well, this means that there are no more goals - *under this* bullet b, see if a new b can be pushed. *) - (try let _ = push b pcobaye' in (* push didn't fail so a new b can be pushed. *) - raise (SuggestFound b) - with SuggestFound _ as e -> raise e - | _ -> ()); (* b could not be pushed, so we must look for a outer bullet *) - pcobaye := pcobaye' - done; - assert false - with SuggestFound b -> Suggest b - | _ -> NeedClosingBrace (* No push was possible, but there are still - subgoals somewhere: there must be a "}" to use. *) - + let us look at the bullet needed. *) + let rec loop prf = + match pop prf with + | prf, b -> + (* pop went well, this means that there are no more goals + *under this* bullet b, see if a new b can be pushed. *) + begin + try ignore (push b prf); Suggest b + with _ -> + (* b could not be pushed, so we must look for a outer bullet *) + loop prf + end + | exception _ -> + (* No pop was possible, but there are still + subgoals somewhere: there must be a "}" to use. *) + NeedClosingBrace + in + loop prf let rec pop_until (prf : proof) bul : proof = let prf', b = pop prf in |