diff options
author | 2014-10-21 12:25:11 +0200 | |
---|---|---|
committer | 2014-10-22 07:31:45 +0200 | |
commit | 328c775067b045b851ec48b97f0507afcc4bb768 (patch) | |
tree | 0fe3cdf8dfecc09cffc1da721d91e97d1ec7c77c /proofs/proofview.ml | |
parent | e87a491d724c83fe1bc98dfb94c665e8ba7f56a1 (diff) |
Proofview: use an iter-like combinator rather than a fold_left-like one for dispatch.
Leads to clearer an more efficient code.
Diffstat (limited to 'proofs/proofview.ml')
-rw-r--r-- | proofs/proofview.ml | 25 |
1 files changed, 12 insertions, 13 deletions
diff --git a/proofs/proofview.ml b/proofs/proofview.ml index 94a89aca3..3f94dbadf 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -433,26 +433,25 @@ let on_advance g ~solved ~adv = | None -> solved (* If [first] has been solved by side effect: do nothing. *) | Some g -> adv g -(* A variant of [Monad.List.fold_left] where we iter over the focused list of +(* A variant of [Monad.List.iter] where we iter over the focused list of goals. The argument tactic is executed in a focus comprising only of the current goal, a goal which has been solved by side effect is skipped. The generated subgoals are concatenated in order. *) -let fold_left_goal i s = +let iter_goal i = (* spiwack: convenience notations, waiting for ocaml 3.12 *) let (>>=) = Proof.bind in let (>>) = Proof.seq in Pv.get >>= fun initial -> - Monad.List.fold_left begin fun ((r,subgoals) as cur) goal -> + Monad.List.fold_left begin fun (subgoals as cur) goal -> on_advance goal ~solved: ( Proof.ret cur ) ~adv: begin fun goal -> Comb.set [goal] >> - i goal r >>= fun r -> - Proof.map (fun step -> (r, step.comb :: subgoals)) Pv.get + i goal >> + Proof.map (fun step -> step.comb :: subgoals) Pv.get end - end (s,[]) initial.comb >>= fun (r,subgoals) -> - Comb.set (List.flatten (List.rev subgoals)) >> - Proof.ret r + end [] initial.comb >>= fun subgoals -> + Comb.set (List.flatten (List.rev subgoals)) (* A variant of [Monad.List.fold_left2] where the first list is the list of focused goals. The argument tactic is executed in a focus @@ -560,7 +559,7 @@ let tclINDEPENDENT tac = match initial.comb with | [] -> tclUNIT () | [_] -> tac - | _ -> fold_left_goal (fun _ () -> tac) () + | _ -> iter_goal (fun _ -> tac) (* Equality function on goals *) let goal_equal evars1 gl1 evars2 gl2 = @@ -848,7 +847,7 @@ module Goal = struct gmake_with info env sigma goal , sigma let nf_enter f = - fold_left_goal begin fun goal () -> + iter_goal begin fun goal -> Env.get >>= fun env -> tclEVARMAP >>= fun sigma -> try @@ -857,7 +856,7 @@ module Goal = struct with e when catchable_exception e -> let e = Errors.push e in tclZERO e - end () + end let normalize { self } = Env.get >>= fun env -> @@ -870,14 +869,14 @@ module Goal = struct gmake_with info env sigma goal let enter f = - fold_left_goal begin fun goal () -> + iter_goal begin fun goal -> Env.get >>= fun env -> tclEVARMAP >>= fun sigma -> try f (gmake env sigma goal) with e when catchable_exception e -> let e = Errors.push e in tclZERO e - end () + end let goals = Env.get >>= fun env -> |