aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--ide/idetop.ml11
-rw-r--r--lib/pp_diff.ml2
-rw-r--r--printing/printer.ml11
-rw-r--r--printing/proof_diffs.ml63
-rw-r--r--proofs/proof.ml4
-rw-r--r--test-suite/unit-tests/printing/proof_diffs_test.ml7
6 files changed, 51 insertions, 47 deletions
diff --git a/ide/idetop.ml b/ide/idetop.ml
index 8a221a93e9..8cb02190e6 100644
--- a/ide/idetop.ml
+++ b/ide/idetop.ml
@@ -212,25 +212,20 @@ let goals () =
if Proof_diffs.show_diffs () then begin
let oldp = Stm.get_prev_proof ~doc (Stm.get_current_state ~doc) in
let diff_goal_map = Proof_diffs.make_goal_map oldp newp in
- let map_goal_for_diff ng = (* todo: move to proof_diffs.ml *)
- try Evar.Map.find ng diff_goal_map with Not_found -> ng
- in
let process_goal_diffs nsigma ng =
let open Evd in
- let og = map_goal_for_diff ng in
let og_s = match oldp with
| Some oldp ->
let (_,_,_,_,osigma) = Proof.proof oldp in
- Some { it = og; sigma = osigma }
+ (try Some { it = Evar.Map.find ng diff_goal_map; sigma = osigma }
+ with Not_found -> raise (Pp_diff.Diff_Failure "Unable to match goals between old and new proof states (6)"))
| None -> None
in
let (hyps_pp_list, concl_pp) = Proof_diffs.diff_goal_ide og_s ng nsigma in
{ Interface.goal_hyp = hyps_pp_list; Interface.goal_ccl = concl_pp; Interface.goal_id = Goal.uid ng }
in
- try
- Some (export_pre_goals (Proof.map_structured_proof newp process_goal_diffs))
- with Pp_diff.Diff_Failure _ -> Some (export_pre_goals (Proof.map_structured_proof newp process_goal))
+ Some (export_pre_goals (Proof.map_structured_proof newp process_goal_diffs))
end else
Some (export_pre_goals (Proof.map_structured_proof newp process_goal))
with Proof_global.NoCurrentProof -> None;;
diff --git a/lib/pp_diff.ml b/lib/pp_diff.ml
index 7b4b1eab73..a485bf31c0 100644
--- a/lib/pp_diff.ml
+++ b/lib/pp_diff.ml
@@ -86,7 +86,7 @@ let shorten_diff_span dtype diff_list =
if (get_variant !src) = dtype then begin
if (lt !dst !src) then
dst := !src;
- while (lt !dst len) && (get_variant !dst) <> `Common do
+ while (lt !dst len) && (get_variant !dst) = dtype do
dst := !dst + incr;
done;
if (lt !dst len) && (get_str !src) = (get_str !dst) then begin
diff --git a/printing/printer.ml b/printing/printer.ml
index da364c8b9e..a91ad63ac1 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -674,10 +674,6 @@ let pr_subgoals ?(pr_first=true) ?(diffs=false) ?os_map
| None -> GoalMap.empty
in
- let map_goal_for_diff ng = (* todo: move to proof_diffs.ml *)
- try GoalMap.find ng diff_goal_map with Not_found -> ng
- in
-
(** Printing functions for the extra informations. *)
let rec print_stack a = function
| [] -> Pp.int a
@@ -713,7 +709,12 @@ let pr_subgoals ?(pr_first=true) ?(diffs=false) ?os_map
let get_ogs g =
match os_map with
- | Some (osigma, _) -> Some { it = map_goal_for_diff g; sigma = osigma }
+ | Some (osigma, _) ->
+ (* if Not_found, returning None treats the goal as new and it will be highlighted;
+ returning Some { it = g; sigma = sigma } will compare the new goal
+ to itself and it won't be highlighted *)
+ (try Some { it = GoalMap.find g diff_goal_map; sigma = osigma }
+ with Not_found -> raise (Pp_diff.Diff_Failure "Unable to match goals between old and new proof states (7)"))
| None -> None
in
let rec pr_rec n = function
diff --git a/printing/proof_diffs.ml b/printing/proof_diffs.ml
index 0b630b39b5..a513d0d18e 100644
--- a/printing/proof_diffs.ml
+++ b/printing/proof_diffs.ml
@@ -214,26 +214,22 @@ module CDC = Context.Compacted.Declaration
let to_tuple : Constr.compacted_declaration -> (Names.Id.t list * 'pc option * 'pc) =
let open CDC in function
- | LocalAssum(idl, tm) -> (idl, None, tm)
- | LocalDef(idl,tdef,tm) -> (idl, Some tdef, tm);;
+ | LocalAssum(idl, tm) -> (idl, None, EConstr.of_constr tm)
+ | LocalDef(idl,tdef,tm) -> (idl, Some (EConstr.of_constr tdef), EConstr.of_constr tm);;
(* XXX: Very unfortunately we cannot use the Proofview interface as
Proof is still using the "legacy" one. *)
-let process_goal_concl sigma g : Constr.t * Environ.env =
+let process_goal_concl sigma g : EConstr.t * Environ.env =
let env = Goal.V82.env sigma g in
let ty = Goal.V82.concl sigma g in
- let ty = EConstr.to_constr sigma ty in
(ty, env)
-let process_goal sigma g : Constr.t reified_goal =
+let process_goal sigma g : EConstr.t reified_goal =
let env = Goal.V82.env sigma g in
- let hyps = Goal.V82.hyps sigma g in
let ty = Goal.V82.concl sigma g in
let name = Goal.uid g in
- (* There is a Constr/Econstr mess here... *)
- let ty = EConstr.to_constr sigma ty in
(* compaction is usually desired [eg for better display] *)
- let hyps = Termops.compact_named_context (Environ.named_context_of_val hyps) in
+ let hyps = Termops.compact_named_context (Environ.named_context env) in
let hyps = List.map to_tuple hyps in
{ name; ty; hyps; env; sigma };;
@@ -241,13 +237,15 @@ let pr_letype_core goal_concl_style env sigma t =
Ppconstr.pr_lconstr_expr (Constrextern.extern_type goal_concl_style env sigma t)
let pp_of_type env sigma ty =
- pr_letype_core true env sigma EConstr.(of_constr ty)
+ pr_letype_core true env sigma ty
let pr_leconstr_core goal_concl_style env sigma t =
Ppconstr.pr_lconstr_expr (Constrextern.extern_constr goal_concl_style env sigma t)
let pr_lconstr_env env sigma c = pr_leconstr_core false env sigma (EConstr.of_constr c)
+let pr_lconstr_env_econstr env sigma c = pr_leconstr_core false env sigma c
+
let diff_concl ?og_s nsigma ng =
let open Evd in
let o_concl_pp = match og_s with
@@ -291,8 +289,8 @@ let goal_info goal sigma =
line_idents := idents :: !line_idents;
let mid = match body with
| Some c ->
- let pb = pr_lconstr_env env sigma c in
- let pb = if Constr.isCast c then surround pb else pb in
+ let pb = pr_lconstr_env_econstr env sigma c in
+ let pb = if EConstr.isCast sigma c then surround pb else pb in
str " := " ++ pb
| None -> mt() in
let ts = pp_of_type env sigma ty in
@@ -409,7 +407,7 @@ let match_goals ot nt =
match exp, exp2 with
| Some expa, Some expb -> constr_expr ogname expa expb
| None, None -> ()
- | _, _ -> raise (Diff_Failure "Unable to match goals betwen old and new proof states (1)")
+ | _, _ -> raise (Diff_Failure "Unable to match goals between old and new proof states (1)")
in
let local_binder_expr ogname exp exp2 =
match exp, exp2 with
@@ -421,7 +419,7 @@ let match_goals ot nt =
| CLocalPattern p, CLocalPattern p2 ->
let (p,ty), (p2,ty2) = p.v,p2.v in
constr_expr_opt ogname ty ty2
- | _, _ -> raise (Diff_Failure "Unable to match goals betwen old and new proof states (2)")
+ | _, _ -> raise (Diff_Failure "Unable to match goals between old and new proof states (2)")
in
let recursion_order_expr ogname exp exp2 =
match exp, exp2 with
@@ -431,7 +429,7 @@ let match_goals ot nt =
| CMeasureRec (m,r), CMeasureRec (m2,r2) ->
constr_expr ogname m m2;
constr_expr_opt ogname r r2
- | _, _ -> raise (Diff_Failure "Unable to match goals betwen old and new proof states (3)")
+ | _, _ -> raise (Diff_Failure "Unable to match goals between old and new proof states (3)")
in
let fix_expr ogname exp exp2 =
let (l,(lo,ro),lb,ce1,ce2), (l2,(lo2,ro2),lb2,ce12,ce22) = exp,exp2 in
@@ -515,7 +513,7 @@ let match_goals ot nt =
| CastNative a, CastNative a2 ->
constr_expr ogname a a2
| CastCoerce, CastCoerce -> ()
- | _, _ -> raise (Diff_Failure "Unable to match goals betwen old and new proof states (4)"))
+ | _, _ -> raise (Diff_Failure "Unable to match goals between old and new proof states (4)"))
| CNotation (ntn,args), CNotation (ntn2,args2) ->
constr_notation_substitution ogname args args2
| CGeneralization (b,a,c), CGeneralization (b2,a2,c2) ->
@@ -523,7 +521,7 @@ let match_goals ot nt =
| CPrim p, CPrim p2 -> ()
| CDelimiters (key,e), CDelimiters (key2,e2) ->
constr_expr ogname e e2
- | _, _ -> raise (Diff_Failure "Unable to match goals betwen old and new proof states (5)")
+ | _, _ -> raise (Diff_Failure "Unable to match goals between old and new proof states (5)")
end
in
@@ -563,9 +561,8 @@ let db_goal_map op np ng_to_og =
Printf.printf "\n"
[@@@ocaml.warning "+32"]
-(* Create a map from new goals to old goals for proof diff. The map only
- has entries for new goals that are not the same as the corresponding old
- goal; there are no entries for unchanged goals.
+(* Create a map from new goals to old goals for proof diff. New goals
+ that are evars not appearing in the proof will not have a mapping.
It proceeds as follows:
1. Find the goal ids that were removed from the old proof and that were
@@ -583,7 +580,7 @@ let db_goal_map op np ng_to_og =
the removed goal.
- if there are more than 2 removals and more than one addition, call
match_goals to get a map between old and new evar names, then use this
- to create the map from new goal ids to old goal ids for the differing goals.
+ to create the map from new goal ids to old goal ids.
*)
let make_goal_map_i op np =
let ng_to_og = ref GoalMap.empty in
@@ -598,6 +595,9 @@ let make_goal_map_i op np =
let add_gs = diff ngs ogs in
let num_adds = cardinal add_gs in
+ (* add common goals *)
+ Goal.Set.iter (fun x -> ng_to_og := GoalMap.add x x !ng_to_og) (inter ogs ngs);
+
if num_rems = 0 then
!ng_to_og (* proofs are the same *)
else if num_adds = 0 then
@@ -616,17 +616,16 @@ let make_goal_map_i op np =
List.iter (fun og -> oevar_to_og := StringMap.add (goal_to_evar og osigma) og !oevar_to_og)
(Goal.Set.elements rem_gs);
- try
- let (_,_,_,_,nsigma) = Proof.proof np in
- let get_og ng =
- let nevar = goal_to_evar ng nsigma in
- let oevar = StringMap.find nevar nevar_to_oevar in
- let og = StringMap.find oevar !oevar_to_og in
- og
- in
- Goal.Set.iter (fun ng -> ng_to_og := GoalMap.add ng (get_og ng) !ng_to_og) add_gs;
- !ng_to_og
- with Not_found -> raise (Diff_Failure "Unable to match goals betwen old and new proof states (6)")
+ let (_,_,_,_,nsigma) = Proof.proof np in
+ let get_og ng =
+ let nevar = goal_to_evar ng nsigma in
+ let oevar = StringMap.find nevar nevar_to_oevar in
+ let og = StringMap.find oevar !oevar_to_og in
+ og
+ in
+ Goal.Set.iter (fun ng ->
+ try ng_to_og := GoalMap.add ng (get_og ng) !ng_to_og with Not_found -> ()) add_gs;
+ !ng_to_og
end
let make_goal_map op np =
diff --git a/proofs/proof.ml b/proofs/proof.ml
index 8220949856..352ddcd3c2 100644
--- a/proofs/proof.ml
+++ b/proofs/proof.ml
@@ -491,4 +491,6 @@ let all_goals p =
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
+ let set = add given_up set in
+ let { Evd.it = bgoals ; sigma = bsigma } = V82.background_subgoals p in
+ add bgoals set
diff --git a/test-suite/unit-tests/printing/proof_diffs_test.ml b/test-suite/unit-tests/printing/proof_diffs_test.ml
index 526cefec44..7f9e6cc6e0 100644
--- a/test-suite/unit-tests/printing/proof_diffs_test.ml
+++ b/test-suite/unit-tests/printing/proof_diffs_test.ml
@@ -71,6 +71,13 @@ let _ = add_test "tokenize_string examples" t
open Pp
+(* example that was failing from #8922 *)
+let t () =
+ Proof_diffs.write_diffs_option "removed";
+ ignore (diff_str "X : ?Goal" "X : forall x : ?Goal0, ?Goal1");
+ Proof_diffs.write_diffs_option "on"
+let _ = add_test "shorten_diff_span failure from #8922" t
+
(* note pp_to_string concatenates adjacent strings, could become one token,
e.g. str " a" ++ str "b " will give a token "ab" *)
(* checks background is present and correct *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-01-31 14:09:43 +0000