diff options
Diffstat (limited to 'printing/proof_diffs.ml')
| -rw-r--r-- | printing/proof_diffs.ml | 635 |
1 files changed, 635 insertions, 0 deletions
diff --git a/printing/proof_diffs.ml b/printing/proof_diffs.ml new file mode 100644 index 00000000..0b630b39 --- /dev/null +++ b/printing/proof_diffs.ml @@ -0,0 +1,635 @@ +(************************************************************************) +(* * The Coq Proof Assistant / The Coq Development Team *) +(* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) +(* <O___,, * (see CREDITS file for the list of authors) *) +(* \VV/ **************************************************************) +(* // * This file is distributed under the terms of the *) +(* * GNU Lesser General Public License Version 2.1 *) +(* * (see LICENSE file for the text of the license) *) +(************************************************************************) + +(* +Displays the differences between successive proof steps in coqtop and CoqIDE. +Proof General requires minor changes to make the diffs visible, but this code +shouldn't break the existing version of PG. See pp_diff.ml for details on how +the diff works. + +Diffs are computed for the hypotheses and conclusion of each goal in the new +proof with its matching goal in the old proof. + +Diffs can be enabled in coqtop with 'Set Diffs "on"|"off"|"removed"' or +'-diffs on|off|removed' on the OS command line. In CoqIDE, they can be enabled +from the View menu. The "on" option shows only the new item with added text, +while "removed" shows each modified item twice--once with the old value showing +removed text and once with the new value showing added text. + +In CoqIDE, colors and highlights can be set in the Edit/Preferences/Tags panel. +For coqtop, these can be set through the COQ_COLORS environment variable. + +Limitations/Possible enhancements: + +- coqtop colors were chosen for white text on a black background. They're +not the greatest. I didn't want to change the existing green highlight. +Suggestions welcome. + +- coqtop underlines removed text because (per Wikipedia) the ANSI escape code +for strikeout is not commonly supported (it didn't work on my system). CoqIDE +uses strikeout on removed text. +*) + +open Pp_diff + +let diff_option = ref `OFF + +let read_diffs_option () = match !diff_option with +| `OFF -> "off" +| `ON -> "on" +| `REMOVED -> "removed" + +let write_diffs_option = function +| "off" -> diff_option := `OFF +| "on" -> diff_option := `ON +| "removed" -> diff_option := `REMOVED +| _ -> CErrors.user_err Pp.(str "Diffs option only accepts the following values: \"off\", \"on\", \"removed\".") + +let _ = + Goptions.(declare_string_option { + optdepr = false; + optname = "show diffs in proofs"; + optkey = ["Diffs"]; + optread = read_diffs_option; + optwrite = write_diffs_option + }) + +let show_diffs () = !diff_option <> `OFF;; +let show_removed () = !diff_option = `REMOVED;; + + +(* DEBUG/UNIT TEST *) +let cfprintf oc = Printf.(kfprintf (fun oc -> fprintf oc "") oc) +let log_out_ch = ref stdout +[@@@ocaml.warning "-32"] +let cprintf s = cfprintf !log_out_ch s +[@@@ocaml.warning "+32"] + +module StringMap = Map.Make(String);; + +let tokenize_string s = + (* todo: cLexer changes buff as it proceeds. Seems like that should be saved, too. + But I don't understand how it's used--it looks like things get appended to it but + it never gets cleared. *) + let rec stream_tok acc str = + let e = Stream.next str in + if Tok.(equal e EOI) then + List.rev acc + else + stream_tok ((Tok.extract_string e) :: acc) str + in + let st = CLexer.get_lexer_state () in + try + let istr = Stream.of_string s in + let lex = CLexer.lexer.Plexing.tok_func istr in + let toks = stream_tok [] (fst lex) in + CLexer.set_lexer_state st; + toks + with exn -> + CLexer.set_lexer_state st; + raise (Diff_Failure "Input string is not lexable");; + + +type hyp_info = { + idents: string list; + rhs_pp: Pp.t; + mutable done_: bool; +} + +(* Generate the diffs between the old and new hyps. + This works by matching lines with the hypothesis name and diffing the right-hand side. + Lines that have multiple names such as "n, m : nat" are handled specially to account + for, say, the addition of m to a pre-existing "n : nat". + *) +let diff_hyps o_line_idents o_map n_line_idents n_map = + let rv : Pp.t list ref = ref [] in + + let is_done ident map = (StringMap.find ident map).done_ in + let exists ident map = + try let _ = StringMap.find ident map in true + with Not_found -> false in + let contains l ident = try [List.find (fun x -> x = ident) l] with Not_found -> [] in + + let output old_ids_uo new_ids = + (* use the order from the old line in case it's changed in the new *) + let old_ids = if old_ids_uo = [] then [] else + let orig = (StringMap.find (List.hd old_ids_uo) o_map).idents in + List.concat (List.map (contains orig) old_ids_uo) + in + + let setup ids map = if ids = [] then ("", Pp.mt ()) else + let open Pp in + let rhs_pp = (StringMap.find (List.hd ids) map).rhs_pp in + let pp_ids = List.map (fun x -> str x) ids in + let hyp_pp = List.fold_left (fun l1 l2 -> l1 ++ str ", " ++ l2) (List.hd pp_ids) (List.tl pp_ids) ++ rhs_pp in + (string_of_ppcmds hyp_pp, hyp_pp) + in + + let (o_line, o_pp) = setup old_ids o_map in + let (n_line, n_pp) = setup new_ids n_map in + + let hyp_diffs = diff_str ~tokenize_string o_line n_line in + let (has_added, has_removed) = has_changes hyp_diffs in + if show_removed () && has_removed then begin + let o_entry = StringMap.find (List.hd old_ids) o_map in + o_entry.done_ <- true; + rv := (add_diff_tags `Removed o_pp hyp_diffs) :: !rv; + end; + if n_line <> "" then begin + let n_entry = StringMap.find (List.hd new_ids) n_map in + n_entry.done_ <- true; + rv := (add_diff_tags `Added n_pp hyp_diffs) :: !rv + end + in + + (* process identifier level diff *) + let process_ident_diff diff = + let (dtype, ident) = get_dinfo diff in + match dtype with + | `Removed -> + if dtype = `Removed then begin + let o_idents = (StringMap.find ident o_map).idents in + (* only show lines that have all idents removed here; other removed idents appear later *) + if show_removed () && + List.for_all (fun x -> not (exists x n_map)) o_idents then + output (List.rev o_idents) [] + end + | _ -> begin (* Added or Common case *) + let n_idents = (StringMap.find ident n_map).idents in + + (* Process a new hyp line, possibly splitting it. Duplicates some of + process_ident iteration, but easier to understand this way *) + let process_line ident2 = + if not (is_done ident2 n_map) then begin + let n_ids_list : string list ref = ref [] in + let o_ids_list : string list ref = ref [] in + let fst_omap_idents = ref None in + let add ids id map = + ids := id :: !ids; + (StringMap.find id map).done_ <- true in + + (* get identifiers shared by one old and one new line, plus + other Added in new and other Removed in old *) + let process_split ident3 = + if not (is_done ident3 n_map) then begin + let this_omap_idents = try Some (StringMap.find ident3 o_map).idents + with Not_found -> None in + if !fst_omap_idents = None then + fst_omap_idents := this_omap_idents; + match (!fst_omap_idents, this_omap_idents) with + | (Some fst, Some this) when fst == this -> (* yes, == *) + add n_ids_list ident3 n_map; + (* include, in old order, all undone Removed idents in old *) + List.iter (fun x -> if x = ident3 || not (is_done x o_map) && not (exists x n_map) then + (add o_ids_list x o_map)) fst + | (_, None) -> + add n_ids_list ident3 n_map (* include all undone Added idents in new *) + | _ -> () + end in + List.iter process_split n_idents; + output (List.rev !o_ids_list) (List.rev !n_ids_list) + end in + List.iter process_line n_idents (* O(n^2), so sue me *) + end in + + let cvt s = Array.of_list (List.concat s) in + let ident_diffs = diff_strs (cvt o_line_idents) (cvt n_line_idents) in + List.iter process_ident_diff ident_diffs; + List.rev !rv;; + + +type 'a hyp = (Names.Id.t list * 'a option * 'a) +type 'a reified_goal = { name: string; ty: 'a; hyps: 'a hyp list; env : Environ.env; sigma: Evd.evar_map } + +(* XXX: Port to proofview, one day. *) +(* open Proofview *) +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);; + +(* 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 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 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 = List.map to_tuple hyps in + { name; ty; hyps; env; sigma };; + +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) + +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 diff_concl ?og_s nsigma ng = + let open Evd in + let o_concl_pp = match og_s with + | Some { it=og; sigma=osigma } -> + let (oty, oenv) = process_goal_concl osigma og in + pp_of_type oenv osigma oty + | None -> Pp.mt() + in + let (nty, nenv) = process_goal_concl nsigma ng in + let n_concl_pp = pp_of_type nenv nsigma nty in + + let show_removed = Some (show_removed ()) in + + diff_pp_combined ~tokenize_string ?show_removed o_concl_pp n_concl_pp + +(* fetch info from a goal, returning (idents, map, concl_pp) where +idents is a list with one entry for each hypothesis, in which each entry +is the list of idents on the lhs of the hypothesis. map is a map from +ident to hyp_info reoords. For example: for the hypotheses: + b : bool + n, m : nat + +idents will be [ ["b"]; ["n"; "m"] ] + +map will contain: + "b" -> { ["b"], Pp.t for ": bool"; false } + "n" -> { ["n"; "m"], Pp.t for ": nat"; false } + "m" -> { ["n"; "m"], Pp.t for ": nat"; false } + where the last two entries share the idents list. + +concl_pp is the conclusion as a Pp.t +*) +let goal_info goal sigma = + let map = ref StringMap.empty in + let line_idents = ref [] in + let build_hyp_info env sigma hyp = + let (names, body, ty) = hyp in + let open Pp in + let idents = List.map (fun x -> Names.Id.to_string x) names in + + 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 + str " := " ++ pb + | None -> mt() in + let ts = pp_of_type env sigma ty in + let rhs_pp = mid ++ str " : " ++ ts in + + let make_entry () = { idents; rhs_pp; done_ = false } in + List.iter (fun ident -> map := (StringMap.add ident (make_entry ()) !map); ()) idents + in + + try + let { ty=ty; hyps=hyps; env=env } = process_goal sigma goal in + List.iter (build_hyp_info env sigma) (List.rev hyps); + let concl_pp = pp_of_type env sigma ty in + ( List.rev !line_idents, !map, concl_pp ) + with _ -> ([], !map, Pp.mt ());; + +let diff_goal_info o_info n_info = + let (o_line_idents, o_hyp_map, o_concl_pp) = o_info in + let (n_line_idents, n_hyp_map, n_concl_pp) = n_info in + let show_removed = Some (show_removed ()) in + let concl_pp = diff_pp_combined ~tokenize_string ?show_removed o_concl_pp n_concl_pp in + + let hyp_diffs_list = diff_hyps o_line_idents o_hyp_map n_line_idents n_hyp_map in + (hyp_diffs_list, concl_pp) + +let hyp_list_to_pp hyps = + let open Pp in + match hyps with + | h :: tl -> List.fold_left (fun x y -> x ++ cut () ++ y) h tl + | [] -> mt ();; + +let unwrap g_s = + match g_s with + | Some g_s -> + let goal = Evd.sig_it g_s in + let sigma = Refiner.project g_s in + goal_info goal sigma + | None -> ([], StringMap.empty, Pp.mt ()) + +let diff_goal_ide og_s ng nsigma = + diff_goal_info (unwrap og_s) (goal_info ng nsigma) + +let diff_goal ?og_s ng ns = + let (hyps_pp_list, concl_pp) = diff_goal_info (unwrap og_s) (goal_info ng ns) in + let open Pp in + v 0 ( + (hyp_list_to_pp hyps_pp_list) ++ cut () ++ + str "============================" ++ cut () ++ + concl_pp);; + + +(*** Code to determine which calls to compare between the old and new proofs ***) + +open Constrexpr +open Glob_term +open Names +open CAst + +(* Compare the old and new proof trees to identify the correspondence between +new and old goals. Returns a map from the new evar name to the old, +e.g. "Goal2" -> "Goal1". Assumes that proof steps only rewrite CEvar nodes +and that CEvar nodes cannot contain other CEvar nodes. + +The comparison works this way: +1. Traverse the old and new trees together (ogname = "", ot != nt): +- if the old and new trees both have CEvar nodes, add an entry to the map from + the new evar name to the old evar name. (Position of goals is preserved but + evar names may not be--see below.) +- if the old tree has a CEvar node and the new tree has a different type of node, + we've found a changed goal. Set ogname to the evar name of the old goal and + go to step 2. +- any other mismatch violates the assumptions, raise an exception +2. Traverse the new tree from the point of the difference (ogname <> "", ot = nt). +- if the node is a CEvar, generate a map entry from the new evar name to ogname. + +Goal ids for unchanged goals appear to be preserved across proof steps. +However, the evar name associated with a goal id may change in a proof step +even if that goal is not changed by the tactic. You can see this by enabling +the call to db_goal_map and entering the following: + + Parameter P : nat -> Prop. + Goal (P 1 /\ P 2 /\ P 3) /\ P 4. + split. + Show Proof. + split. + Show Proof. + + Which gives you this summarized output: + + > split. + New Goals: 3 -> Goal 4 -> Goal0 <--- goal 4 is "Goal0" + Old Goals: 1 -> Goal + Goal map: 3 -> 1 4 -> 1 + > Show Proof. + (conj ?Goal ?Goal0) <--- goal 4 is the rightmost goal in the proof + > split. + New Goals: 6 -> Goal0 7 -> Goal1 4 -> Goal <--- goal 4 is now "Goal" + Old Goals: 3 -> Goal 4 -> Goal0 + Goal map: 6 -> 3 7 -> 3 + > Show Proof. + (conj (conj ?Goal0 ?Goal1) ?Goal) <--- goal 4 is still the rightmost goal in the proof + *) +let match_goals ot nt = + let nevar_to_oevar = ref StringMap.empty in + (* ogname is "" when there is no difference on the current path. + It's set to the old goal's evar name once a rewitten goal is found, + at which point the code only searches for the replacing goals + (and ot is set to nt). *) + let rec match_goals_r ogname ot nt = + let constr_expr ogname exp exp2 = + match_goals_r ogname exp.v exp2.v + in + let constr_expr_opt ogname exp exp2 = + 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)") + in + let local_binder_expr ogname exp exp2 = + match exp, exp2 with + | CLocalAssum (nal,bk,ty), CLocalAssum(nal2,bk2,ty2) -> + constr_expr ogname ty ty2 + | CLocalDef (n,c,t), CLocalDef (n2,c2,t2) -> + constr_expr ogname c c2; + constr_expr_opt ogname t t2 + | 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)") + in + let recursion_order_expr ogname exp exp2 = + match exp, exp2 with + | CStructRec, CStructRec -> () + | CWfRec c, CWfRec c2 -> + constr_expr ogname c c2 + | 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)") + in + let fix_expr ogname exp exp2 = + let (l,(lo,ro),lb,ce1,ce2), (l2,(lo2,ro2),lb2,ce12,ce22) = exp,exp2 in + recursion_order_expr ogname ro ro2; + List.iter2 (local_binder_expr ogname) lb lb2; + constr_expr ogname ce1 ce12; + constr_expr ogname ce2 ce22 + in + let cofix_expr ogname exp exp2 = + let (l,lb,ce1,ce2), (l2,lb2,ce12,ce22) = exp,exp2 in + List.iter2 (local_binder_expr ogname) lb lb2; + constr_expr ogname ce1 ce12; + constr_expr ogname ce2 ce22 + in + let case_expr ogname exp exp2 = + let (ce,l,cp), (ce2,l2,cp2) = exp,exp2 in + constr_expr ogname ce ce2 + in + let branch_expr ogname exp exp2 = + let (cpe,ce), (cpe2,ce2) = exp.v,exp2.v in + constr_expr ogname ce ce2 + in + let constr_notation_substitution ogname exp exp2 = + let (ce, cel, cp, lb), (ce2, cel2, cp2, lb2) = exp, exp2 in + List.iter2 (constr_expr ogname) ce ce2; + List.iter2 (fun a a2 -> List.iter2 (constr_expr ogname) a a2) cel cel2; + List.iter2 (fun a a2 -> List.iter2 (local_binder_expr ogname) a a2) lb lb2 + in + begin + match ot, nt with + | CRef (ref,us), CRef (ref2,us2) -> () + | CFix (id,fl), CFix (id2,fl2) -> + List.iter2 (fix_expr ogname) fl fl2 + | CCoFix (id,cfl), CCoFix (id2,cfl2) -> + List.iter2 (cofix_expr ogname) cfl cfl2 + | CProdN (bl,c2), CProdN (bl2,c22) + | CLambdaN (bl,c2), CLambdaN (bl2,c22) -> + List.iter2 (local_binder_expr ogname) bl bl2; + constr_expr ogname c2 c22 + | CLetIn (na,c1,t,c2), CLetIn (na2,c12,t2,c22) -> + constr_expr ogname c1 c12; + constr_expr_opt ogname t t2; + constr_expr ogname c2 c22 + | CAppExpl ((isproj,ref,us),args), CAppExpl ((isproj2,ref2,us2),args2) -> + List.iter2 (constr_expr ogname) args args2 + | CApp ((isproj,f),args), CApp ((isproj2,f2),args2) -> + constr_expr ogname f f2; + List.iter2 (fun a a2 -> let (c, _) = a and (c2, _) = a2 in + constr_expr ogname c c2) args args2 + | CRecord fs, CRecord fs2 -> + List.iter2 (fun a a2 -> let (_, c) = a and (_, c2) = a2 in + constr_expr ogname c c2) fs fs2 + | CCases (sty,rtnpo,tms,eqns), CCases (sty2,rtnpo2,tms2,eqns2) -> + constr_expr_opt ogname rtnpo rtnpo2; + List.iter2 (case_expr ogname) tms tms2; + List.iter2 (branch_expr ogname) eqns eqns2 + | CLetTuple (nal,(na,po),b,c), CLetTuple (nal2,(na2,po2),b2,c2) -> + constr_expr_opt ogname po po2; + constr_expr ogname b b2; + constr_expr ogname c c2 + | CIf (c,(na,po),b1,b2), CIf (c2,(na2,po2),b12,b22) -> + constr_expr ogname c c2; + constr_expr_opt ogname po po2; + constr_expr ogname b1 b12; + constr_expr ogname b2 b22 + | CHole (k,naming,solve), CHole (k2,naming2,solve2) -> () + | CPatVar _, CPatVar _ -> () + | CEvar (n,l), CEvar (n2,l2) -> + let oevar = if ogname = "" then Id.to_string n else ogname in + nevar_to_oevar := StringMap.add (Id.to_string n2) oevar !nevar_to_oevar; + List.iter2 (fun x x2 -> let (_, g) = x and (_, g2) = x2 in constr_expr ogname g g2) l l2 + | CEvar (n,l), nt' -> + (* pass down the old goal evar name *) + match_goals_r (Id.to_string n) nt' nt' + | CSort s, CSort s2 -> () + | CCast (c,c'), CCast (c2,c'2) -> + constr_expr ogname c c2; + (match c', c'2 with + | CastConv a, CastConv a2 + | CastVM a, CastVM a2 + | 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)")) + | CNotation (ntn,args), CNotation (ntn2,args2) -> + constr_notation_substitution ogname args args2 + | CGeneralization (b,a,c), CGeneralization (b2,a2,c2) -> + constr_expr ogname c c2 + | 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)") + end + in + + (match ot with + | Some ot -> match_goals_r "" ot nt + | None -> ()); + !nevar_to_oevar + + +let to_constr p = + let open CAst in + let pprf = Proof.partial_proof p in + (* pprf generally has only one element, but it may have more in the derive plugin *) + let t = List.hd pprf in + let sigma, env = Pfedit.get_current_context ~p () in + let x = Constrextern.extern_constr false env sigma t in (* todo: right options?? *) + x.v + + +module GoalMap = Evar.Map + +let goal_to_evar g sigma = Id.to_string (Termops.pr_evar_suggested_name g sigma) + +[@@@ocaml.warning "-32"] +let db_goal_map op np ng_to_og = + Printf.printf "New Goals: "; + let (ngoals,_,_,_,nsigma) = Proof.proof np in + List.iter (fun ng -> Printf.printf "%d -> %s " (Evar.repr ng) (goal_to_evar ng nsigma)) ngoals; + (match op with + | Some op -> + let (ogoals,_,_,_,osigma) = Proof.proof op in + Printf.printf "\nOld Goals: "; + List.iter (fun og -> Printf.printf "%d -> %s " (Evar.repr og) (goal_to_evar og osigma)) ogoals + | None -> ()); + Printf.printf "\nGoal map: "; + GoalMap.iter (fun og ng -> Printf.printf "%d -> %d " (Evar.repr og) (Evar.repr ng)) 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. + + It proceeds as follows: + 1. Find the goal ids that were removed from the old proof and that were + added in the new proof. If the same goal id is present in both proofs + then conclude the goal is unchanged (assumption). + + 2. The code assumes that proof changes only take the form of replacing + one or more goal symbols (CEvars) with new terms. Therefore: + - if there are no removals, the proofs are the same. + - if there are removals but no additions, then there are no new goals + that aren't the same as their associated old goals. For the both of + these cases, the map is empty because there are no new goals that differ + from their old goals + - if there is only one removal, then any added goals should be mapped to + 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. +*) +let make_goal_map_i op np = + let ng_to_og = ref GoalMap.empty in + match op with + | None -> !ng_to_og + | Some op -> + let open Goal.Set in + let ogs = Proof.all_goals op in + let ngs = Proof.all_goals np in + let rem_gs = diff ogs ngs in + let num_rems = cardinal rem_gs in + let add_gs = diff ngs ogs in + let num_adds = cardinal add_gs in + + if num_rems = 0 then + !ng_to_og (* proofs are the same *) + else if num_adds = 0 then + !ng_to_og (* only removals *) + else if num_rems = 1 then begin + (* only 1 removal, some additions *) + let removed_g = List.hd (elements rem_gs) in + Goal.Set.iter (fun x -> ng_to_og := GoalMap.add x removed_g !ng_to_og) add_gs; + !ng_to_og + end else begin + (* >= 2 removals, >= 1 addition, need to match *) + let nevar_to_oevar = match_goals (Some (to_constr op)) (to_constr np) in + + let oevar_to_og = ref StringMap.empty in + let (_,_,_,_,osigma) = Proof.proof op in + 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)") + end + +let make_goal_map op np = + let ng_to_og = make_goal_map_i op np in + (*db_goal_map op np ng_to_og;*) + ng_to_og |