aboutsummaryrefslogtreecommitdiff
path: root/proofs
diff options
context:
space:
mode:
Diffstat (limited to 'proofs')
-rw-r--r--proofs/dune6
-rw-r--r--proofs/goal.ml2
-rw-r--r--proofs/goal.mli2
-rw-r--r--proofs/logic.ml1
-rw-r--r--proofs/pfedit.ml25
-rw-r--r--proofs/pfedit.mli2
-rw-r--r--proofs/proof.ml45
-rw-r--r--proofs/proof.mli6
-rw-r--r--proofs/redexpr.ml2
-rw-r--r--proofs/refine.ml18
10 files changed, 84 insertions, 25 deletions
diff --git a/proofs/dune b/proofs/dune
new file mode 100644
index 0000000000..679c45f6bf
--- /dev/null
+++ b/proofs/dune
@@ -0,0 +1,6 @@
+(library
+ (name proofs)
+ (synopsis "Coq's Higher-level Refinement Proof Engine and Top-level Proof Structure")
+ (public_name coq.proofs)
+ (wrapped false)
+ (libraries interp))
diff --git a/proofs/goal.ml b/proofs/goal.ml
index 1440d1636b..c14c0a8a77 100644
--- a/proofs/goal.ml
+++ b/proofs/goal.ml
@@ -143,3 +143,5 @@ module V82 = struct
) ~init:(concl sigma gl) env
end
+
+module Set = Set.Make(struct type t = goal let compare = Evar.compare end)
diff --git a/proofs/goal.mli b/proofs/goal.mli
index b8c979ad7a..a033d6daab 100644
--- a/proofs/goal.mli
+++ b/proofs/goal.mli
@@ -71,3 +71,5 @@ module V82 : sig
val abstract_type : Evd.evar_map -> goal -> EConstr.types
end
+
+module Set : sig include Set.S with type elt = goal end
diff --git a/proofs/logic.ml b/proofs/logic.ml
index e8ca719932..613581ade7 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -62,6 +62,7 @@ let is_unification_error = function
let catchable_exception = function
| CErrors.UserError _ | TypeError _
+ | Notation.NumeralNotationError _
| RefinerError _ | Indrec.RecursionSchemeError _
| Nametab.GlobalizationError _
(* reduction errors *)
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 678c3ea3f7..e6507332b1 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -51,23 +51,22 @@ let _ = CErrors.register_handler begin function
| _ -> raise CErrors.Unhandled
end
-let get_nth_V82_goal i =
- let p = Proof_global.give_me_the_proof () in
+let get_nth_V82_goal p i =
let goals,_,_,_,sigma = Proof.proof p in
try { it = List.nth goals (i-1) ; sigma }
with Failure _ -> raise NoSuchGoal
-let get_goal_context_gen i =
- let { it=goal ; sigma=sigma; } = get_nth_V82_goal i in
+let get_goal_context_gen p i =
+ let { it=goal ; sigma=sigma; } = get_nth_V82_goal p i in
(sigma, Refiner.pf_env { it=goal ; sigma=sigma; })
let get_goal_context i =
- try get_goal_context_gen i
+ try get_goal_context_gen (Proof_global.give_me_the_proof ()) i
with Proof_global.NoCurrentProof -> CErrors.user_err Pp.(str "No focused proof.")
| NoSuchGoal -> CErrors.user_err Pp.(str "No such goal.")
let get_current_goal_context () =
- try get_goal_context_gen 1
+ try get_goal_context_gen (Proof_global.give_me_the_proof ()) 1
with Proof_global.NoCurrentProof -> CErrors.user_err Pp.(str "No focused proof.")
| NoSuchGoal ->
(* spiwack: returning empty evar_map, since if there is no goal, under focus,
@@ -75,14 +74,18 @@ let get_current_goal_context () =
let env = Global.env () in
(Evd.from_env env, env)
-let get_current_context () =
- try get_goal_context_gen 1
+let get_current_context ?p () =
+ let current_proof_by_default = function
+ | Some p -> p
+ | None -> Proof_global.give_me_the_proof ()
+ in
+ try get_goal_context_gen (current_proof_by_default p) 1
with Proof_global.NoCurrentProof ->
let env = Global.env () in
(Evd.from_env env, env)
| NoSuchGoal ->
(* No more focused goals ? *)
- let p = Proof_global.give_me_the_proof () in
+ let p = (current_proof_by_default p) in
let evd = Proof.in_proof p (fun x -> x) in
(evd, Global.env ())
@@ -173,8 +176,8 @@ let build_by_tactic ?(side_eff=true) env sigma ?(poly=false) typ tac =
const_entry_body = Future.chain ce.const_entry_body
(fun (pt, _) -> pt, ()) } in
let (cb, ctx), () = Future.force ce.const_entry_body in
- let univs' = Evd.merge_context_set Evd.univ_rigid (Evd.from_ctx univs) ctx in
- cb, status, Evd.evar_universe_context univs'
+ let univs = UState.merge ~sideff:side_eff ~extend:true Evd.univ_rigid univs ctx in
+ cb, status, univs
let refine_by_tactic env sigma ty tac =
(** Save the initial side-effects to restore them afterwards. We set the
diff --git a/proofs/pfedit.mli b/proofs/pfedit.mli
index e02b5ab956..5feb5bd645 100644
--- a/proofs/pfedit.mli
+++ b/proofs/pfedit.mli
@@ -60,7 +60,7 @@ val get_current_goal_context : unit -> Evd.evar_map * env
If there is no pending proof then it returns the current global
environment and empty evar_map. *)
-val get_current_context : unit -> Evd.evar_map * env
+val get_current_context : ?p:Proof.t -> unit -> Evd.evar_map * env
(** [current_proof_statement] *)
diff --git a/proofs/proof.ml b/proofs/proof.ml
index 51e0a1d614..8bbd82bb0a 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -63,6 +63,7 @@ exception CannotUnfocusThisWay
(* Cannot focus on non-existing subgoals *)
exception NoSuchGoals of int * int
+exception NoSuchGoal of Names.Id.t
exception FullyUnfocused
@@ -75,6 +76,10 @@ let _ = CErrors.register_handler begin function
CErrors.user_err ~hdr:"Focus" Pp.(
str"Not every goal in range ["++ int i ++ str","++int j++str"] exist."
)
+ | NoSuchGoal id ->
+ CErrors.user_err
+ ~hdr:"Focus"
+ Pp.(str "No such goal: " ++ str (Names.Id.to_string id) ++ str ".")
| FullyUnfocused -> CErrors.user_err Pp.(str "The proof is not focused")
| _ -> raise CErrors.Unhandled
end
@@ -230,6 +235,37 @@ let focus cond inf i pr =
try _focus cond (Obj.repr inf) i i pr
with CList.IndexOutOfRange -> raise (NoSuchGoals (i,i))
+(* Focus on the goal named id *)
+let focus_id cond inf id pr =
+ let (focused_goals, evar_map) = Proofview.proofview pr.proofview in
+ begin match try Some (Evd.evar_key id evar_map) with Not_found -> None with
+ | Some ev ->
+ begin match CList.safe_index Evar.equal ev focused_goals with
+ | Some i ->
+ (* goal is already under focus *)
+ _focus cond (Obj.repr inf) i i pr
+ | None ->
+ if CList.mem_f Evar.equal ev pr.shelf then
+ (* goal is on the shelf, put it in focus *)
+ let proofview = Proofview.unshelve [ev] pr.proofview in
+ let shelf =
+ CList.filter (fun ev' -> Evar.equal ev ev' |> not) pr.shelf
+ in
+ let pr = { pr with proofview; shelf } in
+ let (focused_goals, _) = Proofview.proofview pr.proofview in
+ let i =
+ (* Now we know that this will succeed *)
+ try CList.index Evar.equal ev focused_goals
+ with Not_found -> assert false
+ in
+ _focus cond (Obj.repr inf) i i pr
+ else
+ raise CannotUnfocusThisWay
+ end
+ | None ->
+ raise (NoSuchGoal id)
+ end
+
let rec unfocus kind pr () =
let cond = cond_of_focus pr in
match test_cond cond kind pr.proofview with
@@ -452,3 +488,12 @@ module V82 = struct
{ pr with proofview ; shelf }
end
+
+let all_goals p =
+ let add gs set =
+ List.fold_left (fun s g -> Goal.Set.add g s) set gs in
+ let (goals,stack,shelf,given_up,_) = proof p in
+ let set = add goals Goal.Set.empty in
+ let set = List.fold_left (fun s gs -> let (g1, g2) = gs in add g1 (add g2 set)) set stack in
+ let set = add shelf set in
+ add given_up set
diff --git a/proofs/proof.mli b/proofs/proof.mli
index c0e832fb8c..511dcc2e00 100644
--- a/proofs/proof.mli
+++ b/proofs/proof.mli
@@ -137,6 +137,9 @@ val done_cond : ?loose_end:bool -> 'a focus_kind -> 'a focus_condition
a need for it? *)
val focus : 'a focus_condition -> 'a -> int -> t -> t
+(* focus on goal named id *)
+val focus_id : 'aa focus_condition -> 'a -> Names.Id.t -> t -> t
+
exception FullyUnfocused
exception CannotUnfocusThisWay
@@ -207,3 +210,6 @@ module V82 : sig
(* Implements the Existential command *)
val instantiate_evar : int -> Constrexpr.constr_expr -> t -> t
end
+
+(* returns the set of all goals in the proof *)
+val all_goals : t -> Goal.Set.t
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index 629b77be2a..44685d2bbd 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -52,7 +52,7 @@ let whd_cbn flags env sigma t =
Reductionops.Stack.zip ~refold:true sigma state
let strong_cbn flags =
- strong (whd_cbn flags)
+ strong_with_flags whd_cbn flags
let simplIsCbn = ref (false)
let _ = Goptions.declare_bool_option {
diff --git a/proofs/refine.ml b/proofs/refine.ml
index b64e7a2e5e..198e057ebc 100644
--- a/proofs/refine.ml
+++ b/proofs/refine.ml
@@ -49,20 +49,14 @@ let (pr_constrv,pr_constr) =
(* Get the side-effect's constant declarations to update the monad's
* environmnent *)
-let add_if_undefined kn cb env =
- try ignore(Environ.lookup_constant kn env); env
- with Not_found -> Environ.add_constant kn cb env
+let add_if_undefined env eff =
+ let open Entries in
+ try ignore(Environ.lookup_constant eff.seff_constant env); env
+ with Not_found -> Environ.add_constant eff.seff_constant eff.seff_body env
(* Add the side effects to the monad's environment, if not already done. *)
-let add_side_effect env = function
- | { Entries.eff = Entries.SEsubproof (kn, cb, eff_env) } ->
- add_if_undefined kn cb env
- | { Entries.eff = Entries.SEscheme (l,_) } ->
- List.fold_left (fun env (_,kn,cb,eff_env) ->
- add_if_undefined kn cb env) env l
-
-let add_side_effects env effects =
- List.fold_left (fun env eff -> add_side_effect env eff) env effects
+let add_side_effects env eff =
+ List.fold_left add_if_undefined env eff
let generic_refine ~typecheck f gl =
let sigma = Proofview.Goal.sigma gl in
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 23:18:27 +0000