(************************************************************************) (* * The Coq Proof Assistant / The Coq Development Team *) (* v * INRIA, CNRS and contributors - Copyright 1999-2018 *) (* "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