diff options
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/dune | 1 | ||||
| -rw-r--r-- | printing/prettyp.ml | 11 | ||||
| -rw-r--r-- | printing/printer.ml | 30 | ||||
| -rw-r--r-- | printing/printer.mli | 18 | ||||
| -rw-r--r-- | printing/printmod.ml | 10 | ||||
| -rw-r--r-- | printing/proof_diffs.ml | 65 | ||||
| -rw-r--r-- | printing/proof_diffs.mli | 9 |
7 files changed, 78 insertions, 66 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/prettyp.ml b/printing/prettyp.ml index e698ba9f8f..712eb21ee6 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -71,27 +71,26 @@ let int_or_no n = if Int.equal n 0 then str "no" else int n let print_basename sp = pr_global (ConstRef sp) let print_ref reduce ref udecl = - let typ, univs = Typeops.type_of_global_in_context (Global.env ()) ref in + let env = Global.env () in + let typ, univs = Typeops.type_of_global_in_context env ref in let inst = Univ.make_abstract_instance univs in - let bl = UnivNames.universe_binders_with_opt_names ref udecl in + let bl = UnivNames.universe_binders_with_opt_names (Environ.universes_of_global env ref) udecl in let sigma = Evd.from_ctx (UState.of_binders bl) in let typ = EConstr.of_constr typ in let typ = if reduce then - let env = Global.env () in let ctx,ccl = Reductionops.splay_prod_assum env sigma typ in EConstr.it_mkProd_or_LetIn ccl ctx else typ in let variance = match ref with | VarRef _ | ConstRef _ -> None | IndRef (ind,_) | ConstructRef ((ind,_),_) -> - let mind = Environ.lookup_mind ind (Global.env ()) in + let mind = Environ.lookup_mind ind env in begin match mind.Declarations.mind_universes with | Declarations.Monomorphic_ind _ | Declarations.Polymorphic_ind _ -> None | Declarations.Cumulative_ind cumi -> Some (Univ.ACumulativityInfo.variance cumi) end in - let env = Global.env () in let inst = if Global.is_polymorphic ref then Printer.pr_universe_instance sigma inst @@ -571,7 +570,7 @@ let print_constant with_values sep sp udecl = in let ctx = UState.of_binders - (UnivNames.universe_binders_with_opt_names (ConstRef sp) udecl) + (UnivNames.universe_binders_with_opt_names (Declareops.constant_polymorphic_context cb) udecl) in let env = Global.env () and sigma = Evd.from_ctx ctx in let pr_ltype = pr_ltype_env env sigma in diff --git a/printing/printer.ml b/printing/printer.ml index da364c8b9e..4840577cbf 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -244,8 +244,19 @@ let pr_abstract_cumulativity_info sigma cumi = let pr_global_env = Nametab.pr_global_env let pr_global = pr_global_env Id.Set.empty +let pr_universe_instance_constraints evd inst csts = + let open Univ in + let prlev = Termops.pr_evd_level evd in + let pcsts = if Constraint.is_empty csts then mt() + else str " |= " ++ + prlist_with_sep (fun () -> str "," ++ spc()) + (fun (u,d,v) -> hov 0 (prlev u ++ pr_constraint_type d ++ prlev v)) + (Constraint.elements csts) + in + str"@{" ++ Instance.pr prlev inst ++ pcsts ++ str"}" + let pr_universe_instance evd inst = - str"@{" ++ Univ.Instance.pr (Termops.pr_evd_level evd) inst ++ str"}" + pr_universe_instance_constraints evd inst Univ.Constraint.empty let pr_puniverses f env sigma (c,u) = if !Constrextern.print_universes @@ -445,9 +456,9 @@ let pr_predicate pr_elt (b, elts) = let pr_cpred p = pr_predicate (pr_constant (Global.env())) (Cpred.elements p) let pr_idpred p = pr_predicate Id.print (Id.Pred.elements p) -let pr_transparent_state (ids, csts) = - hv 0 (str"VARIABLES: " ++ pr_idpred ids ++ fnl () ++ - str"CONSTANTS: " ++ pr_cpred csts ++ fnl ()) +let pr_transparent_state ts = + hv 0 (str"VARIABLES: " ++ pr_idpred ts.TransparentState.tr_var ++ fnl () ++ + str"CONSTANTS: " ++ pr_cpred ts.TransparentState.tr_cst ++ fnl ()) (* display complete goal og_s has goal+sigma on the previous proof step for diffs @@ -674,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 @@ -713,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 f9d1a62895..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 @@ -85,6 +84,7 @@ val pr_sort : evar_map -> Sorts.t -> Pp.t val pr_polymorphic : bool -> Pp.t val pr_cumulative : bool -> bool -> Pp.t val pr_universe_instance : evar_map -> Univ.Instance.t -> Pp.t +val pr_universe_instance_constraints : evar_map -> Univ.Instance.t -> Univ.Constraint.t -> Pp.t val pr_universe_ctx : evar_map -> ?variance:Univ.Variance.t array -> Univ.UContext.t -> Pp.t val pr_abstract_universe_ctx : evar_map -> ?variance:Univ.Variance.t array -> @@ -134,7 +134,7 @@ val pr_context_of : env -> evar_map -> Pp.t val pr_predicate : ('a -> Pp.t) -> (bool * 'a list) -> Pp.t val pr_cpred : Cpred.t -> Pp.t val pr_idpred : Id.Pred.t -> Pp.t -val pr_transparent_state : transparent_state -> Pp.t +val pr_transparent_state : TransparentState.t -> Pp.t (** Proofs, these functions obey [Hyps Limit] and [Compact contexts]. *) @@ -143,7 +143,7 @@ val pr_transparent_state : transparent_state -> 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 @@ -160,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 @@ -181,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/printmod.ml b/printing/printmod.ml index cc40c74998..2c3ab46670 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -119,7 +119,9 @@ let print_mutual_inductive env mind mib udecl = | BiFinite -> "Variant" | CoFinite -> "CoInductive" in - let bl = UnivNames.universe_binders_with_opt_names (IndRef (mind, 0)) udecl in + let bl = UnivNames.universe_binders_with_opt_names + (Declareops.inductive_polymorphic_context mib) udecl + in let sigma = Evd.from_ctx (UState.of_binders bl) in hov 0 (Printer.pr_polymorphic (Declareops.inductive_is_polymorphic mib) ++ Printer.pr_cumulative @@ -157,7 +159,9 @@ let print_record env mind mib udecl = let cstrtype = hnf_prod_applist_assum env nparamdecls cstrtypes.(0) args in let fields = get_fields cstrtype in let envpar = push_rel_context params env in - let bl = UnivNames.universe_binders_with_opt_names (IndRef (mind,0)) udecl in + let bl = UnivNames.universe_binders_with_opt_names (Declareops.inductive_polymorphic_context mib) + udecl + in let sigma = Evd.from_ctx (UState.of_binders bl) in let keyword = let open Declarations in @@ -296,7 +300,7 @@ let print_body is_impl extent env mp (l,body) = (match extent with | OnlyNames -> mt () | WithContents -> - let bl = UnivNames.universe_binders_with_opt_names (ConstRef (Constant.make2 mp l)) None in + let bl = UnivNames.universe_binders_with_opt_names ctx None in let sigma = Evd.from_ctx (UState.of_binders bl) in str " :" ++ spc () ++ hov 0 (Printer.pr_ltype_env env sigma cb.const_type) ++ 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 *) |