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).

3 files changed, 75 insertions, 8 deletions

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 *)
diff --git a/printing/printer.mli b/printing/printer.mli
index 504392e35f..9c9f6e766a 100644
--- a/printing/printer.mli
+++ b/printing/printer.mli
@@ -111,6 +111,9 @@ val pr_pconstructor        : env -> pconstructor -> std_ppcmds
 
 
 (** Contexts *)
+(** Display compact contexts of goals (simple hyps on the same line) *)
+val set_compact_context : bool -> unit
+val get_compact_context : unit -> bool
 
 val pr_context_unlimited   : env -> evar_map -> std_ppcmds
 val pr_ne_context_of       : std_ppcmds -> env -> evar_map -> std_ppcmds
@@ -132,7 +135,7 @@ val pr_cpred               : Cpred.t -> std_ppcmds
 val pr_idpred              : Id.Pred.t -> std_ppcmds
 val pr_transparent_state   : transparent_state -> std_ppcmds
 
-(** Proofs *)
+(** Proofs, these functions obey [Hyps Limit] and [Compact contexts]. *)
 
 val pr_goal                : goal sigma -> std_ppcmds
 val pr_subgoals            : ?pr_first:bool -> std_ppcmds option -> evar_map -> evar list -> Goal.goal list -> int list -> goal list -> std_ppcmds
diff --git a/vernac/vernacentries.ml b/vernac/vernacentries.ml
index 2cb6f3918f..40cd1a29c9 100644
--- a/vernac/vernacentries.ml
+++ b/vernac/vernacentries.ml
@@ -1413,6 +1413,24 @@ let _ =
 
 let _ =
   declare_int_option
+    { optsync  = false;
+      optdepr  = false;
+      optname  = "the hypotheses limit";
+      optkey   = ["Hyps";"Limit"];
+      optread  = Flags.print_hyps_limit;
+      optwrite = Flags.set_print_hyps_limit }
+
+let _ =
+  declare_bool_option
+    { optsync  = true;
+      optdepr  = false;
+      optname  = "display compact goal contexts";
+      optkey   = ["Printing";"Compact";"Contexts"];
+      optread  = (fun () -> Printer.get_compact_context());
+      optwrite = (fun b -> Printer.set_compact_context b) }
+
+let _ =
+  declare_int_option
     { optsync  = true;
       optdepr  = false;
       optname  = "the printing depth";