diff options
Diffstat (limited to 'proofs/proofview.ml')
| -rw-r--r-- | proofs/proofview.ml | 75 |
1 files changed, 49 insertions, 26 deletions
diff --git a/proofs/proofview.ml b/proofs/proofview.ml index 45b7c084d..8a2c7617c 100644 --- a/proofs/proofview.ml +++ b/proofs/proofview.ml @@ -26,7 +26,8 @@ open Util type proofview = { initial : (Term.constr * Term.types) list; solution : Evd.evar_map; - comb : Goal.goal list + comb : Goal.goal list; + side_effects : Declareops.side_effects } let proofview p = @@ -38,7 +39,8 @@ let init = let rec aux = function | [] -> { initial = [] ; solution = Evd.empty ; - comb = [] + comb = []; + side_effects = Declareops.no_seff } | (env,typ)::l -> let { initial = ret ; solution = sol ; comb = comb } = aux l @@ -50,12 +52,15 @@ let init = let gl = Goal.build e in { initial = (econstr,typ)::ret; solution = new_defs ; - comb = gl::comb } + comb = gl::comb; + side_effects = Declareops.no_seff } in fun l -> let v = aux l in (* Marks all the goal unresolvable for typeclasses. *) { v with solution = Typeclasses.mark_unresolvables v.solution } +let initial_goals { initial } = initial + (* Returns whether this proofview is finished or not. That is, if it has empty subgoals in the comb. There could still be unsolved subgoaled, but they would then be out of the view, focused out. *) @@ -64,8 +69,13 @@ let finished = function | _ -> false (* Returns the current value of the proofview partial proofs. *) -let return { initial=init; solution=defs } = - List.map (fun (c,t) -> (Evarutil.nf_evar defs c , t)) init +let return { solution=defs; side_effects=eff } c = Evarutil.nf_evar defs c, eff + +let partial_proof pv = + List.map fst (List.map (return pv) (List.map fst (initial_goals pv))) + +let emit_side_effects eff x = + { x with side_effects = Declareops.union_side_effects eff x.side_effects } (* spiwack: this function should probably go in the Util section, but I'd rather have Util (or a separate module for lists) @@ -356,8 +366,8 @@ let rec catchable_exception = function [s] to each goal successively and applying [k] to each result. *) let list_of_sensitive s k env step = Goal.list_map begin fun defs g -> - let (a,defs) = Goal.eval s env defs g in - (k a) , defs + let (a,defs,effs) = Goal.eval s env defs g in + (k a) , defs, effs end step.comb step.solution (* In form of a tactic *) let list_of_sensitive s k env = @@ -366,8 +376,10 @@ let list_of_sensitive s k env = let (>>) = Inner.seq in Inner.get >>= fun step -> try - let (tacs,defs) = list_of_sensitive s k env step in - Inner.set { step with solution = defs } >> + let (tacs,defs,effs) = list_of_sensitive s k env step in + Inner.set { step with solution = defs; + side_effects = Declareops.union_side_effects step.side_effects + (Declareops.flatten_side_effects effs) } >> Inner.return tacs with e when catchable_exception e -> tclZERO e env @@ -388,19 +400,22 @@ let tclGOALBINDU s k = (* No backtracking can happen here, hence, as opposed to the dispatch tacticals, everything is done in one step. *) let sensitive_on_proofview s env step = - let wrap g ((defs, partial_list) as partial_res) = + let wrap g ((defs, partial_list, partial_eff) as partial_res) = match Goal.advance defs g with - | None ->partial_res + | None -> partial_res | Some g -> - let {Goal.subgoals = sg } , d' = Goal.eval s env defs g in - (d',sg::partial_list) + let { Goal.subgoals = sg } , d', eff = Goal.eval s env defs g in + (d', sg::partial_list, eff::partial_eff) in - let ( new_defs , combed_subgoals ) = - List.fold_right wrap step.comb (step.solution,[]) + let ( new_defs , combed_subgoals, side_effects ) = + List.fold_right wrap step.comb (step.solution,[],[]) in { step with solution = new_defs; - comb = List.flatten combed_subgoals } + comb = List.flatten combed_subgoals; + side_effects = + Declareops.union_side_effects + (Declareops.flatten_side_effects side_effects) step.side_effects } let tclSENSITIVE s env = (* spiwack: convenience notations, waiting for ocaml 3.12 *) let (>>=) = Inner.bind in @@ -440,18 +455,26 @@ module V82 = struct Inner.get >>= fun ps -> try let tac evd gl = - let glsigma = tac { Evd.it = gl ; Evd.sigma = evd } in + let glsigma = + tac { Evd.it = gl ; sigma = evd; eff = Declareops.no_seff } in let sigma = glsigma.Evd.sigma in let g = glsigma.Evd.it in - ( g , sigma ) + ( g, sigma, glsigma.Evd.eff ) in (* Old style tactics expect the goals normalized with respect to evars. *) - let (initgoals,initevd) = - Goal.list_map Goal.V82.nf_evar ps.comb ps.solution + let no_side_eff f x y = + let a, b = f x y in a, b, Declareops.no_seff in + let (initgoals,initevd, eff1) = + Goal.list_map (no_side_eff Goal.V82.nf_evar) ps.comb ps.solution in - let (goalss,evd) = Goal.list_map tac initgoals initevd in + let (goalss,evd,eff2) = Goal.list_map tac initgoals initevd in let sgs = List.flatten goalss in - Inner.set { ps with solution=evd ; comb=sgs } + Inner.set { ps with solution=evd ; comb=sgs; + side_effects = + Declareops.union_side_effects ps.side_effects + (Declareops.union_side_effects + (Declareops.flatten_side_effects eff1) + (Declareops.flatten_side_effects eff2)) } with e when catchable_exception e -> tclZERO e env @@ -471,12 +494,12 @@ module V82 = struct (* Returns the open goals of the proofview together with the evar_map to interprete them. *) - let goals { comb = comb ; solution = solution } = - { Evd.it = comb ; sigma = solution} + let goals { comb = comb ; solution = solution; side_effects=eff } = + { Evd.it = comb ; sigma = solution; eff=eff} - let top_goals { initial=initial ; solution=solution } = + let top_goals { initial=initial ; solution=solution; side_effects=eff } = let goals = List.map (fun (t,_) -> Goal.V82.build (fst (Term.destEvar t))) initial in - { Evd.it = goals ; sigma=solution } + { Evd.it = goals ; sigma=solution; eff=eff } let top_evars { initial=initial } = let evars_of_initial (c,_) = |