diff options
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/dune | 1 | ||||
| -rw-r--r-- | printing/printer.ml | 11 | ||||
| -rw-r--r-- | printing/printer.mli | 15 | ||||
| -rw-r--r-- | printing/proof_diffs.ml | 65 | ||||
| -rw-r--r-- | printing/proof_diffs.mli | 9 |
5 files changed, 49 insertions, 52 deletions
diff --git a/printing/dune b/printing/dune index 837ac48009..3392342165 100644 --- a/printing/dune +++ b/printing/dune @@ -2,6 +2,5 @@ (name printing) (synopsis "Coq's Term Pretty Printing Library") (public_name coq.printing) - (flags :standard -open Gramlib) (wrapped false) (libraries parsing proofs)) diff --git a/printing/printer.ml b/printing/printer.ml index 831008a957..4840577cbf 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -685,10 +685,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 @@ -724,7 +720,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/printer.mli b/printing/printer.mli index 785f452a7b..cefc005c74 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -13,7 +13,6 @@ open Constr open Environ open Pattern open Evd -open Proof_type open Glob_term open Ltac_pretype @@ -144,7 +143,7 @@ val pr_transparent_state : TransparentState.t -> Pp.t records containing the goal and sigma for, respectively, the new and old proof steps, e.g. [{ it = g ; sigma = sigma }]. *) -val pr_goal : ?diffs:bool -> ?og_s:(goal sigma) -> goal sigma -> Pp.t +val pr_goal : ?diffs:bool -> ?og_s:(Goal.goal sigma) -> Goal.goal sigma -> Pp.t (** [pr_subgoals ~pr_first ~diffs ~os_map close_cmd sigma ~seeds ~shelf ~stack ~unfocused ~goals] prints the goals in [goals] followed by the goals in [unfocused] in a compact form @@ -161,17 +160,17 @@ val pr_goal : ?diffs:bool -> ?og_s:(goal sigma) -> goal sigma -> there are non-instantiated existential variables. [stack] is used to print summary info on unfocused goals. *) -val pr_subgoals : ?pr_first:bool -> ?diffs:bool -> ?os_map:(evar_map * Evar.t Evar.Map.t) -> Pp.t option -> evar_map - -> seeds:goal list -> shelf:goal list -> stack:int list - -> unfocused: goal list -> goals:goal list -> Pp.t +val pr_subgoals : ?pr_first:bool -> ?diffs:bool -> ?os_map:(evar_map * Goal.goal Evar.Map.t) -> Pp.t option -> evar_map + -> seeds:Goal.goal list -> shelf:Goal.goal list -> stack:int list + -> unfocused:Goal.goal list -> goals:Goal.goal list -> Pp.t -val pr_subgoal : int -> evar_map -> goal list -> Pp.t +val pr_subgoal : int -> evar_map -> Goal.goal list -> Pp.t (** [pr_concl n ~diffs ~og_s sigma g] prints the conclusion of the goal [g] using [sigma]. The output is labelled "subgoal [n]". If [diffs] is true, highlight the differences between the old conclusion, [og_s], and [g]+[sigma]. [og_s] is a record containing the old goal and sigma, e.g. [{ it = g ; sigma = sigma }]. *) -val pr_concl : int -> ?diffs:bool -> ?og_s:(goal sigma) -> evar_map -> goal -> Pp.t +val pr_concl : int -> ?diffs:bool -> ?og_s:(Goal.goal sigma) -> evar_map -> Goal.goal -> Pp.t (** [pr_open_subgoals_diff ~quiet ~diffs ~oproof proof] shows the context for [proof] as used by, for example, coqtop. The first active goal is printed with all its antecedents and the conclusion. The other active goals only show their @@ -182,7 +181,7 @@ val pr_open_subgoals_diff : ?quiet:bool -> ?diffs:bool -> ?oproof:Proof.t -> Pr val pr_open_subgoals : proof:Proof.t -> Pp.t val pr_nth_open_subgoal : proof:Proof.t -> int -> Pp.t val pr_evar : evar_map -> (Evar.t * evar_info) -> Pp.t -val pr_evars_int : evar_map -> shelf:goal list -> givenup:goal list -> int -> evar_info Evar.Map.t -> Pp.t +val pr_evars_int : evar_map -> shelf:Goal.goal list -> givenup:Goal.goal list -> int -> evar_info Evar.Map.t -> Pp.t val pr_evars : evar_map -> evar_info Evar.Map.t -> Pp.t val pr_ne_evar_set : Pp.t -> Pp.t -> evar_map -> Evar.Set.t -> Pp.t diff --git a/printing/proof_diffs.ml b/printing/proof_diffs.ml index 0b630b39b5..cc1bcc66ae 100644 --- a/printing/proof_diffs.ml +++ b/printing/proof_diffs.ml @@ -88,7 +88,7 @@ let tokenize_string s = 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 lex = CLexer.lexer.Gramlib.Plexing.tok_func istr in let toks = stream_tok [] (fst lex) in CLexer.set_lexer_state st; toks @@ -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/printing/proof_diffs.mli b/printing/proof_diffs.mli index 832393e15f..ce9ee5ae6f 100644 --- a/printing/proof_diffs.mli +++ b/printing/proof_diffs.mli @@ -16,7 +16,6 @@ val write_diffs_option : string -> unit val show_diffs : unit -> bool open Evd -open Proof_type open Environ open Constr @@ -31,7 +30,7 @@ If you want to make your call especially bulletproof, catch these exceptions, print a user-visible message, then recall this routine with the first argument set to None, which will skip the diff. *) -val diff_goal_ide : goal sigma option -> goal -> Evd.evar_map -> Pp.t list * Pp.t +val diff_goal_ide : Goal.goal sigma option -> Goal.goal -> Evd.evar_map -> Pp.t list * Pp.t (** Computes the diff between two goals @@ -43,7 +42,7 @@ If you want to make your call especially bulletproof, catch these exceptions, print a user-visible message, then recall this routine with the first argument set to None, which will skip the diff. *) -val diff_goal : ?og_s:(goal sigma) -> goal -> Evd.evar_map -> Pp.t +val diff_goal : ?og_s:(Goal.goal sigma) -> Goal.goal -> Evd.evar_map -> Pp.t (** Convert a string to a list of token strings using the lexer *) val tokenize_string : string -> string list @@ -53,7 +52,7 @@ val pr_leconstr_core : bool -> Environ.env -> Evd.evar_map -> EConstr.cons val pr_lconstr_env : env -> evar_map -> constr -> Pp.t (** Computes diffs for a single conclusion *) -val diff_concl : ?og_s:goal sigma -> Evd.evar_map -> Goal.goal -> Pp.t +val diff_concl : ?og_s:Goal.goal sigma -> Evd.evar_map -> Goal.goal -> Pp.t (** Generates a map from [np] to [op] that maps changed goals to their prior forms. The map doesn't include entries for unchanged goals; unchanged goals @@ -61,7 +60,7 @@ will have the same goal id in both versions. [op] and [np] must be from the same proof document and [op] must be for a state before [np]. *) -val make_goal_map : Proof.t option -> Proof.t -> Evar.t Evar.Map.t +val make_goal_map : Proof.t option -> Proof.t -> Goal.goal Evar.Map.t (* Exposed for unit test, don't use these otherwise *) (* output channel for the test log file *) |