diff options
Diffstat (limited to 'printing/printer.ml')
| -rw-r--r-- | printing/printer.ml | 125 |
1 files changed, 67 insertions, 58 deletions
diff --git a/printing/printer.ml b/printing/printer.ml index 04337f6be8..5e7e9ce548 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -22,6 +22,10 @@ open Constrextern open Ppconstr open Declarations +module RelDecl = Context.Rel.Declaration +module NamedDecl = Context.Named.Declaration +module CompactedDecl = Context.Compacted.Declaration + let emacs_str s = if !Flags.print_emacs then s else "" let delayed_emacs_cmd s = @@ -248,31 +252,30 @@ let pr_pattern t = pr_pattern_env (Global.env()) empty_names_context t*) (**********************************************************************) (* Contexts and declarations *) -let pr_var_decl_skel pr_id env sigma (id,c,typ) = - let pbody = match c with - | None -> (mt ()) - | Some c -> - (* Force evaluation *) - let pb = pr_lconstr_env env sigma c in - let pb = if isCast c then surround pb else pb in - (str" := " ++ pb ++ cut () ) in +let pr_compacted_decl env sigma decl = + let ids, pbody, typ = match decl with + | CompactedDecl.LocalAssum (ids, typ) -> + ids, mt (), typ + | CompactedDecl.LocalDef (ids,c,typ) -> + (* Force evaluation *) + let pb = pr_lconstr_env env sigma c in + let pb = if isCast c then surround pb else pb in + ids, (str" := " ++ pb ++ cut ()), typ + in + let pids = prlist_with_sep pr_comma pr_id ids in let pt = pr_ltype_env env sigma typ in let ptyp = (str" : " ++ pt) in - (pr_id id ++ hov 0 (pbody ++ ptyp)) - -let pr_var_decl env sigma d = - pr_var_decl_skel pr_id env sigma (Context.Named.Declaration.to_tuple d) + hov 0 (pids ++ pbody ++ ptyp) -let pr_var_list_decl env sigma (l,c,typ) = - hov 0 (pr_var_decl_skel (fun ids -> prlist_with_sep pr_comma pr_id ids) env sigma (l,c,typ)) +let pr_named_decl env sigma decl = + decl |> CompactedDecl.of_named_decl |> pr_compacted_decl env sigma let pr_rel_decl env sigma decl = - let open Context.Rel.Declaration in - let na = get_name decl in - let typ = get_type decl in + let na = RelDecl.get_name decl in + let typ = RelDecl.get_type decl in let pbody = match decl with - | LocalAssum _ -> mt () - | LocalDef (_,c,_) -> + | RelDecl.LocalAssum _ -> mt () + | RelDecl.LocalDef (_,c,_) -> (* Force evaluation *) let pb = pr_lconstr_env env sigma c in let pb = if isCast c then surround pb else pb in @@ -289,13 +292,16 @@ let pr_rel_decl env sigma decl = (* Prints a signature, all declarations on the same line if possible *) let pr_named_context_of env sigma = - let make_decl_list env d pps = pr_var_decl env sigma d :: pps in + let make_decl_list env d pps = pr_named_decl env sigma d :: pps in let psl = List.rev (fold_named_context make_decl_list env ~init:[]) in hv 0 (prlist_with_sep (fun _ -> ws 2) (fun x -> x) psl) +let pr_var_list_decl env sigma decl = + hov 0 (pr_compacted_decl env sigma decl) + let pr_named_context env sigma ne_context = hv 0 (Context.Named.fold_outside - (fun d pps -> pps ++ ws 2 ++ pr_var_decl env sigma d) + (fun d pps -> pps ++ ws 2 ++ pr_named_decl env sigma d) ne_context ~init:(mt ())) let pr_rel_context env sigma rel_context = @@ -307,9 +313,9 @@ let pr_rel_context_of env sigma = (* Prints an env (variables and de Bruijn). Separator: newline *) let pr_context_unlimited env sigma = let sign_env = - Context.NamedList.fold + Context.Compacted.fold (fun d pps -> - let pidt = pr_var_list_decl env sigma d in + let pidt = pr_compacted_decl env sigma d in (pps ++ fnl () ++ pidt)) (Termops.compact_named_context (named_context env)) ~init:(mt ()) in @@ -326,39 +332,43 @@ 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 ()) -let pr_context_limit n env sigma = - let named_context = Environ.named_context env in - let lgsign = List.length named_context in - if n >= lgsign then - pr_context_unlimited env sigma - else - let k = lgsign-n in - let _,sign_env = - Context.NamedList.fold - (fun d (i,pps) -> - if i < k then - (i+1, (pps ++str ".")) - else - let pidt = pr_var_list_decl env sigma d in - (i+1, (pps ++ fnl () ++ - str (emacs_str "") ++ - pidt))) - (Termops.compact_named_context (Environ.named_context env)) ~init:(0,(mt ())) - in - let db_env = - fold_rel_context - (fun env d pps -> - let pnat = pr_rel_decl env sigma d in - (pps ++ fnl () ++ - str (emacs_str "") ++ - pnat)) - env ~init:(mt ()) - in - (sign_env ++ db_env) +let rec bld_sign_env env sigma ctxt pps = + match ctxt with + | [] -> 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 pr_context_limit_compact ?n env sigma = + let ctxt = Termops.compact_named_context (named_context env) in + let lgth = List.length ctxt in + let n_capped = + match n with + | None -> lgth + | 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. *) + 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) + env ~init:(mt ()) in + (sign_env ++ db_env) + +(* compact printing an env (variables and de Bruijn). Separator: three + spaces between simple hyps, and newline otherwise *) +let pr_context_unlimited_compact env sigma = + pr_context_limit_compact env sigma -let pr_context_of env sigma = match Flags.print_hyps_limit () with - | None -> hv 0 (pr_context_unlimited env sigma) - | Some n -> hv 0 (pr_context_limit n env sigma) +let pr_context_of env sigma = + match Flags.print_hyps_limit () with + | None -> hv 0 (pr_context_limit_compact env sigma) + | Some n -> hv 0 (pr_context_limit_compact ~n env sigma) (* display goal parts (Proof mode) *) @@ -417,8 +427,7 @@ let pr_evgl_sign sigma evi = | None -> [], [] | Some f -> List.filter2 (fun b c -> not b) f (evar_context evi) in - let open Context.Named.Declaration in - let ids = List.rev_map get_id l in + let ids = List.rev_map NamedDecl.get_id l in let warn = if List.is_empty ids then mt () else (str "(" ++ prlist_with_sep pr_comma pr_id ids ++ str " cannot be used)") @@ -713,7 +722,7 @@ let pr_open_subgoals ?(proof=Proof_global.give_me_the_proof ()) () = let end_cmd = str "This subproof is complete, but there are some unfocused goals." ++ (let s = Proof_global.Bullet.suggest p in - if Pp.is_empty s then s else fnl () ++ s) ++ + if Pp.ismt s then s else fnl () ++ s) ++ fnl () in pr_subgoals ~pr_first:false (Some end_cmd) bsigma seeds shelf [] bgoals |