diff options
Diffstat (limited to 'printing/proof_diffs.ml')
| -rw-r--r-- | printing/proof_diffs.ml | 392 |
1 files changed, 341 insertions, 51 deletions
diff --git a/printing/proof_diffs.ml b/printing/proof_diffs.ml index 3a81e908a7..5bb1053645 100644 --- a/printing/proof_diffs.ml +++ b/printing/proof_diffs.ml @@ -14,39 +14,26 @@ 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 the first goal between -the old and new proofs. +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 with the Coq commmand "Set Diffs on|off|removed." or -'-diffs "on"|"off"|"removed"' on the OS command line. 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. +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: -- If you go back to a prior proof step, diffs are not shown on the new current -step. Diffs will be shown again once you do another proof step. - -- Diffs are done between the first active goal in the old and new proofs. -If, for example, the proof step completed a goal, then the new goal is a -different goal, not a transformation of the old goal, so a diff is probably -not appropriate. (There's currently no way to tell when this happens or to -accurately match goals across old and new proofs. -See https://github.com/coq/coq/issues/7653) This is also why only the -first goal is diffed. - -- "Set Diffs "xx"." should reprint the current goal using the new option. - - 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 mine). CoqIDE +for strikeout is not commonly supported (it didn't work on my system). CoqIDE uses strikeout on removed text. *) @@ -54,8 +41,6 @@ open Pp_diff let diff_option = ref `OFF -(* todo: Is there a way to persist the setting between sessions? - Eg if the user wants this as a permanent config setting? *) let read_diffs_option () = match !diff_option with | `OFF -> "off" | `ON -> "on" @@ -136,7 +121,8 @@ let diff_hyps o_line_idents o_map n_line_idents n_map = (* 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 + List.concat (List.map (contains orig) old_ids_uo) + in let setup ids map = if ids = [] then ("", Pp.mt ()) else let open Pp in @@ -233,6 +219,12 @@ let to_tuple : Constr.compacted_declaration -> (Names.Id.t list * 'pc option * ' (* 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 @@ -256,14 +248,29 @@ let pr_leconstr_core 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, 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: +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 -list will be [ ["b"]; ["n"; "m"] ] +idents will be [ ["b"]; ["n"; "m"] ] map will contain: "b" -> { ["b"], Pp.t for ": bool"; false } @@ -317,31 +324,314 @@ let hyp_list_to_pp hyps = | h :: tl -> List.fold_left (fun x y -> x ++ cut () ++ y) h tl | [] -> mt ();; -(* Special purpuse, use only for the IDE interface, *) -let diff_first_goal o_proof n_proof = - let first_goal_info proof = - match proof with - | None -> ([], StringMap.empty, Pp.mt ()) - | Some proof2 -> - let (goals,_,_,_,sigma) = Proof.proof proof2 in - match goals with - | hd :: tl -> goal_info hd sigma; - | _ -> ([], StringMap.empty, Pp.mt ()) - in - diff_goal_info (first_goal_info o_proof) (first_goal_info n_proof);; - -let diff_goals ?prev_gs n_gs = - let unwrap gs = - match gs with - | Some gs -> - let goal = Evd.sig_it gs in - let sigma = Refiner.project gs in - goal_info goal sigma - | None -> ([], StringMap.empty, Pp.mt ()) - in - let (hyps_pp_list, concl_pp) = diff_goal_info (unwrap prev_gs) (unwrap n_gs) in +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 + | CProj (pr,c), CProj (pr2,c2) -> + constr_expr ogname c c2 + | _, _ -> 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 |