aboutsummaryrefslogtreecommitdiff
path: root/proofs
diff options
context:
space:
mode:
Diffstat (limited to 'proofs')
-rw-r--r--proofs/logic.ml50
-rw-r--r--proofs/logic.mli2
-rw-r--r--proofs/pfedit.ml4
-rw-r--r--proofs/proof.ml72
-rw-r--r--proofs/proof.mli49
-rw-r--r--proofs/proof_global.ml2
-rw-r--r--proofs/tacmach.ml4
-rw-r--r--proofs/tacmach.mli2
8 files changed, 48 insertions, 137 deletions
diff --git a/proofs/logic.ml b/proofs/logic.ml
index a01ddf2388..b79e1e6024 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -78,14 +78,6 @@ let error_no_such_hypothesis env sigma id = raise (RefinerError (env, sigma, NoS
let check = ref false
let with_check = Flags.with_option check
-(* [apply_to_hyp sign id f] splits [sign] into [tail::[id,_,_]::head] and
- returns [tail::(f head (id,_,_) (rev tail))] *)
-let apply_to_hyp env sigma check sign id f =
- try apply_to_hyp sign id f
- with Hyp_not_found ->
- if check then error_no_such_hypothesis env sigma id
- else sign
-
let check_typability env sigma c =
if !check then let _ = unsafe_type_of env sigma (EConstr.of_constr c) in ()
@@ -161,12 +153,14 @@ let reorder_context env sigma sign ord =
step ord ords sign mt_q []
let reorder_val_context env sigma sign ord =
+match ord with
+| [] | [_] ->
+ (* Single variable-free definitions need not be reordered *)
+ sign
+| _ :: _ :: _ ->
let open EConstr in
val_of_named_context (reorder_context env sigma (named_context_of_val sign) ord)
-
-
-
let check_decl_position env sigma sign d =
let open EConstr in
let x = NamedDecl.get_id d in
@@ -556,25 +550,25 @@ and treat_case sigma goal ci lbrty lf acc' =
(lacc,sigma,fi::bacc))
(acc',sigma,[]) lbrty lf ci.ci_pp_info.cstr_tags
-let convert_hyp check sign sigma d =
+let convert_hyp ~check ~reorder env sigma d =
let id = NamedDecl.get_id d in
let b = NamedDecl.get_value d in
- let env = Global.env () in
- let reorder = ref [] in
- let sign' =
- apply_to_hyp env sigma check sign id
- (fun _ d' _ ->
- let c = Option.map EConstr.of_constr (NamedDecl.get_value d') in
- let env = Global.env_of_context sign in
- if check && not (is_conv env sigma (NamedDecl.get_type d) (EConstr.of_constr (NamedDecl.get_type d'))) then
- user_err ~hdr:"Logic.convert_hyp"
- (str "Incorrect change of the type of " ++ Id.print id ++ str ".");
- if check && not (Option.equal (is_conv env sigma) b c) then
- user_err ~hdr:"Logic.convert_hyp"
- (str "Incorrect change of the body of "++ Id.print id ++ str ".");
- if check then reorder := check_decl_position env sigma sign d;
- map_named_decl EConstr.Unsafe.to_constr d) in
- reorder_val_context env sigma sign' !reorder
+ let sign = Environ.named_context_val env in
+ match lookup_named_ctxt id sign with
+ | exception Not_found ->
+ if check then error_no_such_hypothesis env sigma id
+ else sign
+ | d' ->
+ let c = Option.map EConstr.of_constr (NamedDecl.get_value d') in
+ if check && not (is_conv env sigma (NamedDecl.get_type d) (EConstr.of_constr (NamedDecl.get_type d'))) then
+ user_err ~hdr:"Logic.convert_hyp"
+ (str "Incorrect change of the type of " ++ Id.print id ++ str ".");
+ if check && not (Option.equal (is_conv env sigma) b c) then
+ user_err ~hdr:"Logic.convert_hyp"
+ (str "Incorrect change of the body of "++ Id.print id ++ str ".");
+ let sign' = apply_to_hyp sign id (fun _ _ _ -> EConstr.Unsafe.to_named_decl d) in
+ if reorder then reorder_val_context env sigma sign' (check_decl_position env sigma sign d)
+ else sign'
(************************************************************************)
(************************************************************************)
diff --git a/proofs/logic.mli b/proofs/logic.mli
index f99076db23..406fe57985 100644
--- a/proofs/logic.mli
+++ b/proofs/logic.mli
@@ -62,7 +62,7 @@ type 'id move_location =
val pr_move_location :
('a -> Pp.t) -> 'a move_location -> Pp.t
-val convert_hyp : bool -> Environ.named_context_val -> evar_map ->
+val convert_hyp : check:bool -> reorder:bool -> Environ.env -> evar_map ->
EConstr.named_declaration -> Environ.named_context_val
val move_hyp_in_named_context : Environ.env -> Evd.evar_map -> Id.t -> Id.t move_location ->
diff --git a/proofs/pfedit.ml b/proofs/pfedit.ml
index 4f36354f79..52e15f466f 100644
--- a/proofs/pfedit.ml
+++ b/proofs/pfedit.ml
@@ -98,7 +98,7 @@ let solve ?with_end_tac gi info_lvl tac pr =
else tac
in
let env = Global.env () in
- let (p,(status,info)) = Proof.run_tactic env tac pr in
+ let (p,(status,info),()) = Proof.run_tactic env tac pr in
let env = Global.env () in
let sigma = Evd.from_env env in
let () =
@@ -161,7 +161,7 @@ let refine_by_tactic ~name ~poly env sigma ty tac =
let prev_future_goals = save_future_goals sigma in
(* Start a proof *)
let prf = Proof.start ~name ~poly sigma [env, ty] in
- let (prf, _) =
+ let (prf, _, ()) =
try Proof.run_tactic env tac prf
with Logic_monad.TacticFailure e as src ->
(* Catch the inner error of the monad tactic *)
diff --git a/proofs/proof.ml b/proofs/proof.ml
index 978b1f6f78..09e4e898fe 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -126,9 +126,6 @@ type t =
(** Locality, polymorphism, and "kind" [Coercion, Definition, etc...] *)
}
-let initial_goals pf = Proofview.initial_goals pf.entry
-let initial_euctx pf = pf.initial_euctx
-
(*** General proof functions ***)
let proof p =
@@ -147,33 +144,6 @@ let proof p =
let given_up = p.given_up in
(goals,stack,shelf,given_up,sigma)
-type 'a pre_goals = {
- fg_goals : 'a list;
- (** List of the focussed goals *)
- bg_goals : ('a list * 'a list) list;
- (** Zipper representing the unfocussed background goals *)
- shelved_goals : 'a list;
- (** List of the goals on the shelf. *)
- given_up_goals : 'a list;
- (** List of the goals that have been given up *)
-}
-
-let map_structured_proof pfts process_goal: 'a pre_goals =
- let (goals, zipper, shelf, given_up, sigma) = proof pfts in
- let fg = List.map (process_goal sigma) goals in
- let map_zip (lg, rg) =
- let lg = List.map (process_goal sigma) lg in
- let rg = List.map (process_goal sigma) rg in
- (lg, rg)
- in
- let bg = List.map map_zip zipper in
- let shelf = List.map (process_goal sigma) shelf in
- let given_up = List.map (process_goal sigma) given_up in
- { fg_goals = fg;
- bg_goals = bg;
- shelved_goals = shelf;
- given_up_goals = given_up; }
-
let rec unroll_focus pv = function
| (_,_,ctx)::stk -> unroll_focus (Proofview.unfocus ctx pv) stk
| [] -> pv
@@ -402,7 +372,7 @@ let run_tactic env tac pr =
let sp = pr.proofview in
let undef sigma l = List.filter (fun g -> Evd.is_undefined sigma g) l in
let tac =
- tac >>= fun () ->
+ tac >>= fun result ->
Proofview.tclEVARMAP >>= fun sigma ->
(* Already solved goals are not to be counted as shelved. Nor are
they to be marked as unresolvable. *)
@@ -413,10 +383,10 @@ let run_tactic env tac pr =
CErrors.anomaly Pp.(str "Evars generated outside of proof engine (e.g. V82, clear, ...) are not supposed to be explicitly given up.");
let sigma = Proofview.Unsafe.mark_as_goals sigma retrieved in
Proofview.Unsafe.tclEVARS sigma >>= fun () ->
- Proofview.tclUNIT retrieved
+ Proofview.tclUNIT (result,retrieved)
in
let { name; poly } = pr in
- let (retrieved,proofview,(status,to_shelve,give_up),info_trace) =
+ let ((result,retrieved),proofview,(status,to_shelve,give_up),info_trace) =
Proofview.apply ~name ~poly env tac sp
in
let sigma = Proofview.return proofview in
@@ -430,7 +400,7 @@ let run_tactic env tac pr =
in
let given_up = pr.given_up@give_up in
let proofview = Proofview.Unsafe.reset_future_goals proofview in
- { pr with proofview ; shelf ; given_up },(status,info_trace)
+ { pr with proofview ; shelf ; given_up },(status,info_trace),result
(*** Commands ***)
@@ -441,22 +411,6 @@ let in_proof p k = k (Proofview.return p.proofview)
let unshelve p =
{ p with proofview = Proofview.unshelve (p.shelf) (p.proofview) ; shelf = [] }
-let pr_proof p =
- let p = map_structured_proof p (fun _sigma g -> g) in
- Pp.(
- let pr_goal_list = prlist_with_sep spc Goal.pr_goal in
- let rec aux acc = function
- | [] -> acc
- | (before,after)::stack ->
- aux (pr_goal_list before ++ spc () ++ str "{" ++ acc ++ str "}" ++ spc () ++
- pr_goal_list after) stack in
- str "[" ++ str "focus structure: " ++
- aux (pr_goal_list p.fg_goals) p.bg_goals ++ str ";" ++ spc () ++
- str "shelved: " ++ pr_goal_list p.shelved_goals ++ str ";" ++ spc () ++
- str "given up: " ++ pr_goal_list p.given_up_goals ++
- str "]"
- )
-
(*** Compatibility layer with <=v8.2 ***)
module V82 = struct
@@ -471,7 +425,7 @@ module V82 = struct
{ Evd.it=List.hd gls ; sigma=sigma; }
let top_evars p =
- Proofview.V82.top_evars p.entry
+ Proofview.V82.top_evars p.entry p.proofview
let grab_evars p =
if not (is_done p) then
@@ -554,3 +508,19 @@ let data { proofview; focus_stack; entry; shelf; given_up; initial_euctx; name;
let stack =
map_minus_one (fun (_,_,c) -> Proofview.focus_context c) focus_stack in
{ sigma; goals; entry; stack; shelf; given_up; initial_euctx; name; poly }
+
+let pr_proof p =
+ let { goals=fg_goals; stack=bg_goals; shelf; given_up; _ } = data p in
+ Pp.(
+ let pr_goal_list = prlist_with_sep spc Goal.pr_goal in
+ let rec aux acc = function
+ | [] -> acc
+ | (before,after)::stack ->
+ aux (pr_goal_list before ++ spc () ++ str "{" ++ acc ++ str "}" ++ spc () ++
+ pr_goal_list after) stack in
+ str "[" ++ str "focus structure: " ++
+ aux (pr_goal_list fg_goals) bg_goals ++ str ";" ++ spc () ++
+ str "shelved: " ++ pr_goal_list shelf ++ str ";" ++ spc () ++
+ str "given up: " ++ pr_goal_list given_up ++
+ str "]"
+ )
diff --git a/proofs/proof.mli b/proofs/proof.mli
index defef57a8d..248b9d921e 100644
--- a/proofs/proof.mli
+++ b/proofs/proof.mli
@@ -34,30 +34,6 @@
(* Type of a proof. *)
type t
-(* Returns a stylised view of a proof for use by, for instance,
- ide-s. *)
-(* spiwack: the type of [proof] will change as we push more refined
- functions to ide-s. This would be better than spawning a new nearly
- identical function everytime. Hence the generic name. *)
-(* In this version: returns the focused goals, a representation of the
- focus stack (the goals at each level), a representation of the
- shelf (the list of goals on the shelf), a representation of the
- given up goals (the list of the given up goals) and the underlying
- evar_map *)
-val proof : t ->
- Goal.goal list
- * (Goal.goal list * Goal.goal list) list
- * Goal.goal list
- * Goal.goal list
- * Evd.evar_map
-[@@ocaml.deprecated "use [Proof.data]"]
-
-val initial_goals : t -> (EConstr.constr * EConstr.types) list
-[@@ocaml.deprecated "use [Proof.data]"]
-
-val initial_euctx : t -> UState.t
-[@@ocaml.deprecated "use [Proof.data]"]
-
type data =
{ sigma : Evd.evar_map
(** A representation of the evar_map [EJGA wouldn't it better to just return the proofview?] *)
@@ -81,29 +57,6 @@ type data =
val data : t -> data
-(* Generic records structured like the return type of proof *)
-type 'a pre_goals = {
- fg_goals : 'a list;
- [@ocaml.deprecated "use [Proof.data]"]
- (** List of the focussed goals *)
- bg_goals : ('a list * 'a list) list;
- [@ocaml.deprecated "use [Proof.data]"]
- (** Zipper representing the unfocussed background goals *)
- shelved_goals : 'a list;
- [@ocaml.deprecated "use [Proof.data]"]
- (** List of the goals on the shelf. *)
- given_up_goals : 'a list;
- [@ocaml.deprecated "use [Proof.data]"]
- (** List of the goals that have been given up *)
-}
-[@@ocaml.deprecated "use [Proof.data]"]
-
-(* needed in OCaml 4.05.0, not needed in newer ones *)
-[@@@ocaml.warning "-3"]
-val map_structured_proof : t -> (Evd.evar_map -> Goal.goal -> 'a) -> ('a pre_goals) [@ocaml.warning "-3"]
-[@@ocaml.deprecated "use [Proof.data]"]
-[@@@ocaml.warning "+3"]
-
(*** General proof functions ***)
val start
: name:Names.Id.t
@@ -219,7 +172,7 @@ val no_focused_goal : t -> bool
used. In which case it is [false]. *)
val run_tactic
: Environ.env
- -> unit Proofview.tactic -> t -> t * (bool*Proofview_monad.Info.tree)
+ -> 'a Proofview.tactic -> t -> t * (bool*Proofview_monad.Info.tree) * 'a
val maximal_unfocus : 'a focus_kind -> t -> t
diff --git a/proofs/proof_global.ml b/proofs/proof_global.ml
index 08b98d702a..40ae4acc88 100644
--- a/proofs/proof_global.ml
+++ b/proofs/proof_global.ml
@@ -345,6 +345,6 @@ let update_global_env (pf : t) =
with_current_proof (fun _ p ->
Proof.in_proof p (fun sigma ->
let tac = Proofview.Unsafe.tclEVARS (Evd.update_sigma_env sigma (Global.env ())) in
- let (p,(status,info)) = Proof.run_tactic (Global.env ()) tac p in
+ let (p,(status,info),()) = Proof.run_tactic (Global.env ()) tac p in
(p, ()))) pf
in res
diff --git a/proofs/tacmach.ml b/proofs/tacmach.ml
index 7b3d9e534b..93031c2202 100644
--- a/proofs/tacmach.ml
+++ b/proofs/tacmach.ml
@@ -104,10 +104,6 @@ let db_pr_goal sigma g =
let pr_gls gls =
hov 0 (pr_evar_map (Some 2) (pf_env gls) (sig_sig gls) ++ fnl () ++ db_pr_goal (project gls) (sig_it gls))
-let pr_glls glls =
- hov 0 (pr_evar_map (Some 2) (Global.env()) (sig_sig glls) ++ fnl () ++
- prlist_with_sep fnl (db_pr_goal (project glls)) (sig_it glls))
-
(* Variants of [Tacmach] functions built with the new proof engine *)
module New = struct
diff --git a/proofs/tacmach.mli b/proofs/tacmach.mli
index 218011c316..23e1e6f566 100644
--- a/proofs/tacmach.mli
+++ b/proofs/tacmach.mli
@@ -68,8 +68,6 @@ val pf_conv_x_leq : Goal.goal sigma -> constr -> constr -> bool
(** {6 Pretty-printing functions (debug only). } *)
val pr_gls : Goal.goal sigma -> Pp.t
-val pr_glls : Goal.goal list sigma -> Pp.t
-[@@ocaml.deprecated "Please move to \"new\" proof engine"]
(** Variants of [Tacmach] functions built with the new proof engine *)
module New : sig
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-01 22:00:04 +0000