diff options
author | 2016-10-12 17:43:51 +0200 | |
---|---|---|
committer | 2016-10-12 17:44:34 +0200 | |
commit | 112e974ec90b2afc51a7cffeba49e5777f3ea80f (patch) | |
tree | 1bf579fca94adea5ee4a423c0a96c8832e68861e /engine | |
parent | 8b2a08ecd123515778584596918666e5f49076f7 (diff) | |
parent | 6d55121c90ec50319a3de6a6907726fbcdc2f835 (diff) |
Merge branch 'v8.5' into v8.6
Diffstat (limited to 'engine')
-rw-r--r-- | engine/ftactic.ml | 23 | ||||
-rw-r--r-- | engine/proofview.ml | 6 | ||||
-rw-r--r-- | engine/proofview.mli | 7 |
3 files changed, 32 insertions, 4 deletions
diff --git a/engine/ftactic.ml b/engine/ftactic.ml index 588709873..aeaaea7e4 100644 --- a/engine/ftactic.ml +++ b/engine/ftactic.ml @@ -29,13 +29,28 @@ let bind (type a) (type b) (m : a t) (f : a -> b t) : b t = m >>= function | Uniform x -> (** We dispatch the uniform result on each goal under focus, as we know that the [m] argument was actually dependent. *) - Proofview.Goal.goals >>= fun l -> - let ans = List.map (fun _ -> x) l in + Proofview.Goal.goals >>= fun goals -> + let ans = List.map (fun g -> (g,x)) goals in Proofview.tclUNIT ans - | Depends l -> Proofview.tclUNIT l + | Depends l -> + Proofview.Goal.goals >>= fun goals -> + Proofview.tclUNIT (List.combine goals l) + in + (* After the tactic has run, some goals which were previously + produced may have been solved by side effects. The values + attached to such goals must be discarded, otherwise the list of + result would not have the same length as the list of focused + goals, which is an invariant of the [Ftactic] module. It is the + reason why a goal is attached to each result above. *) + let filter (g,x) = + g >>= fun g -> + Proofview.Goal.unsolved g >>= function + | true -> Proofview.tclUNIT (Some x) + | false -> Proofview.tclUNIT None in Proofview.tclDISPATCHL (List.map f l) >>= fun l -> - Proofview.tclUNIT (Depends (List.concat l)) + Proofview.Monad.List.map_filter filter (List.concat l) >>= fun filtered -> + Proofview.tclUNIT (Depends filtered) let goals = Proofview.Goal.goals >>= fun l -> Proofview.tclUNIT (Depends l) let set_sigma r = diff --git a/engine/proofview.ml b/engine/proofview.ml index a2838a2de..f2f400515 100644 --- a/engine/proofview.ml +++ b/engine/proofview.ml @@ -929,6 +929,8 @@ module Unsafe = struct { step with comb = step.comb @ gls } end + let tclSETENV = Env.set + let tclGETGOALS = Comb.get let tclSETGOALS = Comb.set @@ -1129,6 +1131,10 @@ module Goal = struct in tclUNIT (CList.map_filter map step.comb) + let unsolved { self=self } = + tclEVARMAP >>= fun sigma -> + tclUNIT (not (Option.is_empty (advance sigma self))) + (* compatibility *) let goal { self=self } = self diff --git a/engine/proofview.mli b/engine/proofview.mli index bc68f11ff..fae75f825 100644 --- a/engine/proofview.mli +++ b/engine/proofview.mli @@ -409,6 +409,9 @@ module Unsafe : sig (** Like {!tclEVARS} but also checks whether goals have been solved. *) val tclEVARSADVANCE : Evd.evar_map -> unit tactic + (** Set the global environment of the tactic *) + val tclSETENV : Environ.env -> unit tactic + (** [tclNEWGOALS gls] adds the goals [gls] to the ones currently being proved, appending them to the list of focused goals. If a goal is already solved, it is not added. *) @@ -518,6 +521,10 @@ module Goal : sig FIXME: encapsulate the level in an existential type. *) val goals : ([ `LZ ], 'r) t tactic list tactic + (** [unsolved g] is [true] if [g] is still unsolved in the current + proof state. *) + val unsolved : ('a, 'r) t -> bool tactic + (** Compatibility: avoid if possible *) val goal : ([ `NF ], 'r) t -> Evar.t |