From 952e9aea47d3fad2d0f488d968ff0e90fa403ebc Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Wed, 3 May 2017 11:37:08 +0200 Subject: Adding an even more compact mode for goal display. We want to print variables in vertical boxes as much as possible. The criterion to distinguish "variable" from "hypothesis" is not obvious. We chose this one but may change it in the future: X:T is a variable if T is not of type Prop AND T is "simple" which means T is either id or (t T1 .. Tn) Ti's are sort-typed (typicall Ti:Type, but not Ti:nat). --- printing/printer.ml | 60 ++++++++++++++++++++++++++++++++++++++++++++++------- 1 file changed, 53 insertions(+), 7 deletions(-) (limited to 'printing/printer.ml') diff --git a/printing/printer.ml b/printing/printer.ml index 93d221f03f..0e31a4a042 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -262,6 +262,13 @@ let pr_pattern t = pr_pattern_env (Global.env()) empty_names_context t*) (**********************************************************************) (* Contexts and declarations *) + +(* Flag for compact display of goals *) + +let get_compact_context,set_compact_context = + let compact_context = ref false in + (fun () -> !compact_context),(fun b -> compact_context := b) + let pr_compacted_decl env sigma decl = let ids, pbody, typ = match decl with | CompactedDecl.LocalAssum (ids, typ) -> @@ -342,15 +349,55 @@ let pr_ne_context_of header env sigma = List.is_empty (Environ.named_context env) then (mt ()) else let penv = pr_context_unlimited env sigma in (header ++ penv ++ fnl ()) +(* Heuristic for horizontalizing hypothesis: + Detecting variable which type is a simple id or of the form (t x y ...) + where t is a product or only sorts (typically [Type -> Type -> ...] + and not [nat -> nat -> ...] ). + + Special case for non-Prop dependent terms. *) +let rec should_compact env sigma typ = + get_compact_context() && + match kind_of_term typ with + | Rel _ | Var _ | Sort _ | Const _ | Ind _ -> true + | App (c,args) -> + let _,type_of_c = Typing.type_of env sigma c in + let _,type_of_typ = Typing.type_of env sigma typ in + not (is_Prop type_of_typ) + && (* These two more tests detect rare cases of non-Prop-sorted + dependent hypothesis: *) + let lnamedtyp , _ = decompose_prod type_of_c in + (* c has a non dependent type *) + List.for_all (fun (_,typarg) -> isSort typarg) lnamedtyp + && (* and real arguments are recursively elligible to compaction. *) + Array.for_all (should_compact env sigma) args + | _ -> false + + +(* If option Compact Contexts is set, we pack "simple" hypothesis in a + hov box (with three sapaces as a separator), the global box being a + v box *) let rec bld_sign_env env sigma ctxt pps = match ctxt with | [] -> pps + | CompactedDecl.LocalAssum (ids,typ)::ctxt' when should_compact env sigma typ -> + let pps',ctxt' = bld_sign_env_id env sigma ctxt (mt ()) true in + (* putting simple hyps in a more horizontal flavor *) + bld_sign_env env sigma ctxt' (pps ++ brk (0,0) ++ hov 0 pps') | d:: ctxt' -> - let pidt = pr_var_list_decl env sigma d in - let pps' = pps ++ brk (0,0) ++ pidt in - bld_sign_env env sigma ctxt' pps' + let pidt = pr_var_list_decl env sigma d in + let pps' = pps ++ brk (0,0) ++ pidt in + bld_sign_env env sigma ctxt' pps' +and bld_sign_env_id env sigma ctxt pps is_start = + match ctxt with + | [] -> pps,ctxt + | CompactedDecl.LocalAssum(ids,typ) as d :: ctxt' when should_compact env sigma typ -> + let pidt = pr_var_list_decl env sigma d in + let pps' = pps ++ (if not is_start then brk (3,0) else (mt ())) ++ pidt in + bld_sign_env_id env sigma ctxt' pps' false + | _ -> pps,ctxt +(* compact printing an env (variables and de Bruijn). Separator: three + spaces between simple hyps, and newline otherwise *) let pr_context_limit_compact ?n env sigma = let ctxt = Termops.compact_named_context (named_context env) in let lgth = List.length ctxt in @@ -360,15 +407,14 @@ let pr_context_limit_compact ?n env sigma = | Some n when n > lgth -> lgth | Some n -> n in let ctxt_chopped,ctxt_hidden = Util.List.chop n_capped ctxt in - (* a dot line hinting the number of hiden hyps. *) + (* a dot line hinting the number of hidden hyps. *) let hidden_dots = String.make (List.length ctxt_hidden) '.' in let sign_env = v 0 (str hidden_dots ++ (mt ()) ++ bld_sign_env env sigma (List.rev ctxt_chopped) (mt ())) in let db_env = - fold_rel_context - (fun env d pps -> pps ++ fnl () ++ pr_rel_decl env sigma d) + fold_rel_context (fun env d pps -> pps ++ fnl () ++ pr_rel_decl env sigma d) env ~init:(mt ()) in - (sign_env ++ db_env) + sign_env ++ db_env (* The number of printed hypothesis in a goal *) (* If [None], no limit *) -- cgit v1.2.3 From 1fe73e6af81759fa8b78c8660745492ed886d477 Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Wed, 26 Apr 2017 11:57:58 +0200 Subject: Adding an option "Printing Unfocused". Off by default. + small refactoring of emacs hacks in printer.ml. --- printing/printer.ml | 139 ++++++++++++++++++++++++++++++++++------------------ 1 file changed, 92 insertions(+), 47 deletions(-) (limited to 'printing/printer.ml') diff --git a/printing/printer.ml b/printing/printer.ml index 93d221f03f..3d67e89f51 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -34,6 +34,49 @@ let delayed_emacs_cmd s = let get_current_context () = Pfedit.get_current_context () +let enable_unfocused_goal_printing = ref false +let enable_goal_tags_printing = ref false +let enable_goal_names_printing = ref false + +let should_tag() = !enable_goal_tags_printing +let should_unfoc() = !enable_unfocused_goal_printing +let should_gname() = !enable_goal_names_printing + + +let _ = + let open Goptions in + declare_bool_option + { optsync = true; + optdepr = false; + optname = "printing of unfocused goal"; + optkey = ["Printing";"Unfocused"]; + optread = (fun () -> !enable_unfocused_goal_printing); + optwrite = (fun b -> enable_unfocused_goal_printing:=b) } + +(* This is set on by proofgeneral proof-tree mode. But may be used for + other purposes *) +let _ = + let open Goptions in + declare_bool_option + { optsync = true; + optdepr = false; + optname = "printing of goal tags"; + optkey = ["Printing";"Goal";"Tags"]; + optread = (fun () -> !enable_goal_tags_printing); + optwrite = (fun b -> enable_goal_tags_printing:=b) } + + +let _ = + let open Goptions in + declare_bool_option + { optsync = true; + optdepr = false; + optname = "printing of goal names"; + optkey = ["Printing";"Goal";"Names"]; + optread = (fun () -> !enable_goal_names_printing); + optwrite = (fun b -> enable_goal_names_printing:=b) } + + (**********************************************************************) (** Terms *) @@ -419,23 +462,25 @@ let default_pr_goal gs = (* display a goal tag *) let pr_goal_tag g = let s = " (ID " ^ Goal.uid g ^ ")" in - str (emacs_str s) - -let display_name = false + str s (* display a goal name *) let pr_goal_name sigma g = - if display_name then str " " ++ Pp.surround (pr_existential_key sigma g) + if should_gname() then str " " ++ Pp.surround (pr_existential_key sigma g) else mt () +let pr_goal_header nme sigma g = + let (g,sigma) = Goal.V82.nf_evar sigma g in + str "subgoal " ++ nme ++ (if should_tag() then pr_goal_tag g else str"") + ++ (if should_gname() then str " " ++ Pp.surround (pr_existential_key sigma g) else mt ()) + (* display the conclusion of a goal *) let pr_concl n sigma g = let (g,sigma) = Goal.V82.nf_evar sigma g in let env = Goal.V82.env sigma g in let pc = pr_goal_concl_style_env env sigma (Goal.V82.concl sigma g) in - str (emacs_str "") ++ - str "subgoal " ++ int n ++ pr_goal_tag g ++ pr_goal_name sigma g ++ - str " is:" ++ cut () ++ str" " ++ pc + let header = pr_goal_header (int n) sigma g in + header ++ str " is:" ++ cut () ++ str" " ++ pc (* display evar type: a context and a type *) let pr_evgl_sign sigma evi = @@ -491,8 +536,8 @@ let pr_ne_evar_set hd tl sigma l = let pr_selected_subgoal name sigma g = let pg = default_pr_goal { sigma=sigma ; it=g; } in - v 0 (str "subgoal " ++ name ++ pr_goal_tag g ++ pr_goal_name sigma g - ++ str " is:" ++ cut () ++ pg) + let header = pr_goal_header name sigma g in + v 0 (header ++ str " is:" ++ cut () ++ pg) let default_pr_subgoal n sigma = let rec prrec p = function @@ -585,27 +630,27 @@ let print_dependent_evars gl sigma seeds = end i (str ",") end evars (str "") in - fnl () ++ - str "(dependent evars:" ++ evars ++ str ")" ++ fnl () - else - fnl () ++ - str "(dependent evars: (printing disabled) )" ++ fnl () + cut () ++ cut () ++ + str "(dependent evars:" ++ evars ++ str ")" + else if !Flags.print_emacs then + (* IDEs prefer something dummy instead of nothing *) + cut () ++ cut () ++ str "(dependent evars: (printing disabled) )" + else mt () in - constraints ++ delayed_emacs_cmd evars + constraints ++ evars () (* Print open subgoals. Checks for uninstantiated existential variables *) (* spiwack: [seeds] is for printing dependent evars in emacs mode. *) (* spiwack: [pr_first] is true when the first goal must be singled out and printed in its entirety. *) -(* courtieu: in emacs mode, even less cases where the first goal is printed - in its entirety *) -let default_pr_subgoals ?(pr_first=true) close_cmd sigma seeds shelf stack goals = +let default_pr_subgoals ?(pr_first=true) + close_cmd sigma seeds shelf stack unfocused goals = (** Printing functions for the extra informations. *) let rec print_stack a = function | [] -> Pp.int a | b::l -> Pp.int a ++ str"-" ++ print_stack b l in - let print_unfocused l = + let print_unfocused_nums l = match l with | [] -> None | a::l -> Some (str"unfocused: " ++ print_stack a l) @@ -625,7 +670,7 @@ let default_pr_subgoals ?(pr_first=true) close_cmd sigma seeds shelf stack goals | [] -> Pp.mt () | a::l -> Pp.spc () ++ str"(" ++ print_comma_separated_list a l ++ str")" in - let extra = Option.List.flatten [ print_unfocused stack ; print_shelf shelf ] in + let extra = Option.List.flatten [ print_unfocused_nums stack ; print_shelf shelf ] in let print_extra = print_extra_list extra in let focused_if_needed = let needed = not (CList.is_empty extra) && pr_first in @@ -642,8 +687,9 @@ let default_pr_subgoals ?(pr_first=true) close_cmd sigma seeds shelf stack goals in let print_multiple_goals g l = if pr_first then - default_pr_goal { it = g ; sigma = sigma; } ++ fnl () ++ - pr_rec 2 l + default_pr_goal { it = g ; sigma = sigma; } + ++ (if l=[] then str"" else cut ()) + ++ pr_rec 2 l else pr_rec 1 (g::l) in @@ -658,32 +704,27 @@ let default_pr_subgoals ?(pr_first=true) close_cmd sigma seeds shelf stack goals begin let exl = Evarutil.non_instantiated sigma in if Evar.Map.is_empty exl then - (str"No more subgoals." - ++ print_dependent_evars None sigma seeds) + (str"No more subgoals." ++ print_dependent_evars None sigma seeds) else let pei = pr_evars_int sigma 1 exl in - (str "No more subgoals, but there are non-instantiated existential variables:" - ++ fnl () ++ (hov 0 pei) - ++ print_dependent_evars None sigma seeds ++ fnl () ++ - str "You can use Grab Existential Variables.") + v 0 ((str "No more subgoals," + ++ str " but there are non-instantiated existential variables:" + ++ cut () ++ (hov 0 pei) + ++ print_dependent_evars None sigma seeds + ++ cut () ++ str "You can use Grab Existential Variables.")) end - | [g] when not !Flags.print_emacs && pr_first -> - let pg = default_pr_goal { it = g ; sigma = sigma; } in - v 0 ( - str "1" ++ focused_if_needed ++ str"subgoal" ++ print_extra - ++ pr_goal_tag g ++ pr_goal_name sigma g ++ cut () ++ pg - ++ print_dependent_evars (Some g) sigma seeds - ) | g1::rest -> let goals = print_multiple_goals g1 rest in let ngoals = List.length rest+1 in v 0 ( - int ngoals ++ focused_if_needed ++ str(String.plural ngoals "subgoal") ++ - print_extra ++ - str ((if display_name then (fun x -> x) else emacs_str) ", subgoal 1") - ++ pr_goal_tag g1 - ++ pr_goal_name sigma g1 ++ cut () - ++ goals + int ngoals ++ focused_if_needed ++ str(String.plural ngoals "subgoal") + ++ print_extra + ++ str (if (should_gname()) then ", subgoal 1" else "") + ++ (if should_tag() then pr_goal_tag g1 else str"") + ++ pr_goal_name sigma g1 ++ cut () ++ goals + ++ (if unfocused=[] then str "" + else (cut() ++ cut() ++ str "*** Unfocused goals:" ++ cut() + ++ pr_rec (List.length rest + 2) unfocused)) ++ print_dependent_evars (Some g1) sigma seeds ) @@ -692,7 +733,7 @@ let default_pr_subgoals ?(pr_first=true) close_cmd sigma seeds shelf stack goals type printer_pr = { - pr_subgoals : ?pr_first:bool -> std_ppcmds option -> evar_map -> evar list -> Goal.goal list -> int list -> goal list -> std_ppcmds; + pr_subgoals : ?pr_first:bool -> std_ppcmds option -> evar_map -> evar list -> Goal.goal list -> int list -> goal list -> goal list -> std_ppcmds; pr_subgoal : int -> evar_map -> goal list -> std_ppcmds; pr_goal : goal sigma -> std_ppcmds; } @@ -726,16 +767,16 @@ let pr_open_subgoals ?(proof=Proof_global.give_me_the_proof ()) () = begin match goals with | [] -> let { Evd.it = bgoals ; sigma = bsigma } = Proof.V82.background_subgoals p in begin match bgoals,shelf,given_up with - | [] , [] , [] -> pr_subgoals None sigma seeds shelf stack goals + | [] , [] , [] -> pr_subgoals None sigma seeds shelf stack [] goals | [] , [] , _ -> Feedback.msg_info (str "No more subgoals, but there are some goals you gave up:"); fnl () - ++ pr_subgoals ~pr_first:false None bsigma seeds [] [] given_up + ++ pr_subgoals ~pr_first:false None bsigma seeds [] [] [] given_up ++ fnl () ++ str "You need to go back and solve them." | [] , _ , _ -> Feedback.msg_info (str "All the remaining goals are on the shelf."); fnl () - ++ pr_subgoals ~pr_first:false None bsigma seeds [] [] shelf + ++ pr_subgoals ~pr_first:false None bsigma seeds [] [] [] shelf | _ , _, _ -> let end_cmd = str "This subproof is complete, but there are some unfocused goals." ++ @@ -743,9 +784,13 @@ let pr_open_subgoals ?(proof=Proof_global.give_me_the_proof ()) () = if Pp.ismt s then s else fnl () ++ s) ++ fnl () in - pr_subgoals ~pr_first:false (Some end_cmd) bsigma seeds shelf [] bgoals + pr_subgoals ~pr_first:false (Some end_cmd) bsigma seeds shelf [] [] bgoals end - | _ -> pr_subgoals None sigma seeds shelf stack goals + | _ -> + let { Evd.it = bgoals ; sigma = bsigma } = Proof.V82.background_subgoals p in + let bgoals_focused, bgoals_unfocused = List.partition (fun x -> List.mem x goals) bgoals in + let unfocused_if_needed = if should_unfoc() then bgoals_unfocused else [] in + pr_subgoals ~pr_first:true None bsigma seeds shelf [] unfocused_if_needed bgoals_focused end let pr_nth_open_subgoal n = -- cgit v1.2.3 From 8bcf71360261d789ac3ab919bc49309df678628f Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Tue, 2 May 2017 21:32:26 +0200 Subject: labelizing arguments --- printing/printer.ml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) (limited to 'printing/printer.ml') diff --git a/printing/printer.ml b/printing/printer.ml index 3d67e89f51..1d3e67d9d6 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -688,7 +688,7 @@ let default_pr_subgoals ?(pr_first=true) let print_multiple_goals g l = if pr_first then default_pr_goal { it = g ; sigma = sigma; } - ++ (if l=[] then str"" else cut ()) + ++ (if l=[] then mt () else cut ()) ++ pr_rec 2 l else pr_rec 1 (g::l) -- cgit v1.2.3 From 8bdb00bbea9dce95f7e0bc18250a41545660299d Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Thu, 4 May 2017 11:25:22 +0200 Subject: Warning removed. --- printing/printer.ml | 2 -- 1 file changed, 2 deletions(-) (limited to 'printing/printer.ml') diff --git a/printing/printer.ml b/printing/printer.ml index 1d3e67d9d6..91a7d22899 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -28,8 +28,6 @@ module CompactedDecl = Context.Compacted.Declaration let emacs_str s = if !Flags.print_emacs then s else "" -let delayed_emacs_cmd s = - if !Flags.print_emacs then s () else str "" let get_current_context () = Pfedit.get_current_context () -- cgit v1.2.3 From 91d78c590b35c9edcf9f68c408ba82090f68e156 Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Fri, 5 May 2017 12:59:41 +0200 Subject: Adapted to EConstr. --- printing/printer.ml | 12 ++++++------ 1 file changed, 6 insertions(+), 6 deletions(-) (limited to 'printing/printer.ml') diff --git a/printing/printer.ml b/printing/printer.ml index 0e31a4a042..997d866f92 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -359,14 +359,14 @@ let rec should_compact env sigma typ = match kind_of_term typ with | Rel _ | Var _ | Sort _ | Const _ | Ind _ -> true | App (c,args) -> - let _,type_of_c = Typing.type_of env sigma c in - let _,type_of_typ = Typing.type_of env sigma typ in - not (is_Prop type_of_typ) + let _,type_of_c = Typing.type_of env sigma (EConstr.of_constr c) in + let _,type_of_typ = Typing.type_of env sigma (EConstr.of_constr typ) in + not (is_Prop (EConstr.to_constr sigma type_of_typ)) && (* These two more tests detect rare cases of non-Prop-sorted dependent hypothesis: *) - let lnamedtyp , _ = decompose_prod type_of_c in + let lnamedtyp , _ = EConstr.decompose_prod sigma type_of_c in (* c has a non dependent type *) - List.for_all (fun (_,typarg) -> isSort typarg) lnamedtyp + List.for_all (fun (_,typarg) -> EConstr.isSort sigma typarg) lnamedtyp && (* and real arguments are recursively elligible to compaction. *) Array.for_all (should_compact env sigma) args | _ -> false @@ -389,7 +389,7 @@ let rec bld_sign_env env sigma ctxt pps = and bld_sign_env_id env sigma ctxt pps is_start = match ctxt with | [] -> pps,ctxt - | CompactedDecl.LocalAssum(ids,typ) as d :: ctxt' when should_compact env sigma typ -> + | CompactedDecl.LocalAssum(ids,typ) as d :: ctxt' when should_compact env sigma typ -> let pidt = pr_var_list_decl env sigma d in let pps' = pps ++ (if not is_start then brk (3,0) else (mt ())) ++ pidt in bld_sign_env_id env sigma ctxt' pps' false -- cgit v1.2.3 From 697cd5a8e7927873ed6700c7e906ae3675bd98b1 Mon Sep 17 00:00:00 2001 From: Pierre Courtieu Date: Fri, 12 May 2017 10:30:50 +0200 Subject: Simplified compaction criterion + tests. --- printing/printer.ml | 25 +++++-------------------- 1 file changed, 5 insertions(+), 20 deletions(-) (limited to 'printing/printer.ml') diff --git a/printing/printer.ml b/printing/printer.ml index 997d866f92..3feea65964 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -349,27 +349,12 @@ let pr_ne_context_of header env sigma = List.is_empty (Environ.named_context env) then (mt ()) else let penv = pr_context_unlimited env sigma in (header ++ penv ++ fnl ()) -(* Heuristic for horizontalizing hypothesis: - Detecting variable which type is a simple id or of the form (t x y ...) - where t is a product or only sorts (typically [Type -> Type -> ...] - and not [nat -> nat -> ...] ). - + Special case for non-Prop dependent terms. *) -let rec should_compact env sigma typ = +(* Heuristic for horizontalizing hypothesis that the user probably + considers as "variables": An hypothesis H:T where T:S and S<>Prop. *) +let should_compact env sigma typ = get_compact_context() && - match kind_of_term typ with - | Rel _ | Var _ | Sort _ | Const _ | Ind _ -> true - | App (c,args) -> - let _,type_of_c = Typing.type_of env sigma (EConstr.of_constr c) in - let _,type_of_typ = Typing.type_of env sigma (EConstr.of_constr typ) in - not (is_Prop (EConstr.to_constr sigma type_of_typ)) - && (* These two more tests detect rare cases of non-Prop-sorted - dependent hypothesis: *) - let lnamedtyp , _ = EConstr.decompose_prod sigma type_of_c in - (* c has a non dependent type *) - List.for_all (fun (_,typarg) -> EConstr.isSort sigma typarg) lnamedtyp - && (* and real arguments are recursively elligible to compaction. *) - Array.for_all (should_compact env sigma) args - | _ -> false + let type_of_typ = Retyping.get_type_of env sigma (EConstr.of_constr typ) in + not (is_Prop (EConstr.to_constr sigma type_of_typ)) (* If option Compact Contexts is set, we pack "simple" hypothesis in a -- cgit v1.2.3