diff options
Diffstat (limited to 'printing')
| -rw-r--r-- | printing/genprint.ml | 4 | ||||
| -rw-r--r-- | printing/genprint.mli | 11 | ||||
| -rw-r--r-- | printing/miscprint.ml | 74 | ||||
| -rw-r--r-- | printing/miscprint.mli | 37 | ||||
| -rw-r--r-- | printing/ppconstr.ml | 17 | ||||
| -rw-r--r-- | printing/ppconstr.mli | 69 | ||||
| -rw-r--r-- | printing/pputils.ml | 2 | ||||
| -rw-r--r-- | printing/pputils.mli | 25 | ||||
| -rw-r--r-- | printing/ppvernac.ml | 30 | ||||
| -rw-r--r-- | printing/ppvernac.mli | 8 | ||||
| -rw-r--r-- | printing/prettyp.ml | 88 | ||||
| -rw-r--r-- | printing/prettyp.mli | 79 | ||||
| -rw-r--r-- | printing/printer.ml | 71 | ||||
| -rw-r--r-- | printing/printer.mli | 187 | ||||
| -rw-r--r-- | printing/printmod.ml | 65 | ||||
| -rw-r--r-- | printing/printmod.mli | 9 |
16 files changed, 369 insertions, 407 deletions
diff --git a/printing/genprint.ml b/printing/genprint.ml index 6505a8f826..543b05024d 100644 --- a/printing/genprint.ml +++ b/printing/genprint.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -9,7 +9,7 @@ open Pp open Genarg -type 'a printer = 'a -> std_ppcmds +type 'a printer = 'a -> Pp.t type ('raw, 'glb, 'top) genprinter = { raw : 'raw printer; diff --git a/printing/genprint.mli b/printing/genprint.mli index 5381fc5bdb..130a89c929 100644 --- a/printing/genprint.mli +++ b/printing/genprint.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -8,18 +8,17 @@ (** Entry point for generic printers *) -open Pp open Genarg -type 'a printer = 'a -> std_ppcmds +type 'a printer = 'a -> Pp.t -val raw_print : ('raw, 'glb, 'top) genarg_type -> 'raw -> std_ppcmds +val raw_print : ('raw, 'glb, 'top) genarg_type -> 'raw -> Pp.t (** Printer for raw level generic arguments. *) -val glb_print : ('raw, 'glb, 'top) genarg_type -> 'glb -> std_ppcmds +val glb_print : ('raw, 'glb, 'top) genarg_type -> 'glb -> Pp.t (** Printer for glob level generic arguments. *) -val top_print : ('raw, 'glb, 'top) genarg_type -> 'top -> std_ppcmds +val top_print : ('raw, 'glb, 'top) genarg_type -> 'top -> Pp.t (** Printer for top level generic arguments. *) val generic_raw_print : rlevel generic_argument printer diff --git a/printing/miscprint.ml b/printing/miscprint.ml deleted file mode 100644 index a4ecbdf5e5..0000000000 --- a/printing/miscprint.ml +++ /dev/null @@ -1,74 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -open Misctypes -open Pp - -(** Printing of [intro_pattern] *) - -let rec pr_intro_pattern prc (_,pat) = match pat with - | IntroForthcoming true -> str "*" - | IntroForthcoming false -> str "**" - | IntroNaming p -> pr_intro_pattern_naming p - | IntroAction p -> pr_intro_pattern_action prc p - -and pr_intro_pattern_naming = function - | IntroIdentifier id -> Nameops.pr_id id - | IntroFresh id -> str "?" ++ Nameops.pr_id id - | IntroAnonymous -> str "?" - -and pr_intro_pattern_action prc = function - | IntroWildcard -> str "_" - | IntroOrAndPattern pll -> pr_or_and_intro_pattern prc pll - | IntroInjection pl -> - str "[=" ++ hv 0 (prlist_with_sep spc (pr_intro_pattern prc) pl) ++ - str "]" - | IntroApplyOn ((_,c),pat) -> pr_intro_pattern prc pat ++ str "%" ++ prc c - | IntroRewrite true -> str "->" - | IntroRewrite false -> str "<-" - -and pr_or_and_intro_pattern prc = function - | IntroAndPattern pl -> - str "(" ++ hv 0 (prlist_with_sep pr_comma (pr_intro_pattern prc) pl) ++ str ")" - | IntroOrPattern pll -> - str "[" ++ - hv 0 (prlist_with_sep pr_bar (prlist_with_sep spc (pr_intro_pattern prc)) pll) - ++ str "]" - -(** Printing of [move_location] *) - -let pr_move_location pr_id = function - | MoveAfter id -> brk(1,1) ++ str "after " ++ pr_id id - | MoveBefore id -> brk(1,1) ++ str "before " ++ pr_id id - | MoveFirst -> str " at top" - | MoveLast -> str " at bottom" - -(** Printing of bindings *) -let pr_binding prc = function - | loc, (NamedHyp id, c) -> hov 1 (Names.Id.print id ++ str " := " ++ cut () ++ prc c) - | loc, (AnonHyp n, c) -> hov 1 (int n ++ str " := " ++ cut () ++ prc c) - -let pr_bindings prc prlc = function - | ImplicitBindings l -> - brk (1,1) ++ str "with" ++ brk (1,1) ++ - pr_sequence prc l - | ExplicitBindings l -> - brk (1,1) ++ str "with" ++ brk (1,1) ++ - pr_sequence (fun b -> str"(" ++ pr_binding prlc b ++ str")") l - | NoBindings -> mt () - -let pr_bindings_no_with prc prlc = function - | ImplicitBindings l -> - brk (0,1) ++ prlist_with_sep spc prc l - | ExplicitBindings l -> - brk (0,1) ++ prlist_with_sep spc (fun b -> str"(" ++ pr_binding prlc b ++ str")") l - | NoBindings -> mt () - -let pr_with_bindings prc prlc (c,bl) = - hov 1 (prc c ++ pr_bindings prc prlc bl) - diff --git a/printing/miscprint.mli b/printing/miscprint.mli deleted file mode 100644 index dbbe3dcfd8..0000000000 --- a/printing/miscprint.mli +++ /dev/null @@ -1,37 +0,0 @@ -(************************************************************************) -(* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) -(* \VV/ **************************************************************) -(* // * This file is distributed under the terms of the *) -(* * GNU Lesser General Public License Version 2.1 *) -(************************************************************************) - -open Misctypes - -(** Printing of [intro_pattern] *) - -val pr_intro_pattern : - ('a -> Pp.std_ppcmds) -> 'a intro_pattern_expr Loc.located -> Pp.std_ppcmds - -val pr_or_and_intro_pattern : - ('a -> Pp.std_ppcmds) -> 'a or_and_intro_pattern_expr -> Pp.std_ppcmds - -val pr_intro_pattern_naming : intro_pattern_naming_expr -> Pp.std_ppcmds - -(** Printing of [move_location] *) - -val pr_move_location : - ('a -> Pp.std_ppcmds) -> 'a move_location -> Pp.std_ppcmds - -val pr_bindings : - ('a -> Pp.std_ppcmds) -> - ('a -> Pp.std_ppcmds) -> 'a bindings -> Pp.std_ppcmds - -val pr_bindings_no_with : - ('a -> Pp.std_ppcmds) -> - ('a -> Pp.std_ppcmds) -> 'a bindings -> Pp.std_ppcmds - -val pr_with_bindings : - ('a -> Pp.std_ppcmds) -> - ('a -> Pp.std_ppcmds) -> 'a * 'a bindings -> Pp.std_ppcmds - diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml index 49eedb767b..37204c2134 100644 --- a/printing/ppconstr.ml +++ b/printing/ppconstr.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -15,6 +15,7 @@ open Nameops open Libnames open Pputils open Ppextend +open Notation_term open Constrexpr open Constrexpr_ops open Decl_kinds @@ -379,9 +380,9 @@ let tag_var = tag Tag.variable match bl with | [CLocalAssum (nal,k,t)] -> kw n ++ pr_binder false pr_c (nal,k,t) - | (CLocalAssum _ | CLocalPattern _) :: _ as bdl -> + | (CLocalAssum _ | CLocalPattern _ | CLocalDef _) :: _ as bdl -> kw n ++ pr_undelimited_binders sep pr_c bdl - | _ -> assert false + | [] -> assert false let pr_binders_gen pr_c sep is_open = if is_open then pr_delimited_binders pr_com_at sep pr_c @@ -731,13 +732,13 @@ let tag_var = tag Tag.variable (sep() ++ if prec_less prec inherited then strm else surround strm) type term_pr = { - pr_constr_expr : constr_expr -> std_ppcmds; - pr_lconstr_expr : constr_expr -> std_ppcmds; - pr_constr_pattern_expr : constr_pattern_expr -> std_ppcmds; - pr_lconstr_pattern_expr : constr_pattern_expr -> std_ppcmds + pr_constr_expr : constr_expr -> Pp.t; + pr_lconstr_expr : constr_expr -> Pp.t; + pr_constr_pattern_expr : constr_pattern_expr -> Pp.t; + pr_lconstr_pattern_expr : constr_pattern_expr -> Pp.t } - type precedence = Ppextend.precedence * Ppextend.parenRelation + type precedence = Notation_term.precedence * Notation_term.parenRelation let modular_constr_pr = pr let rec fix rf x = rf (fix rf) x let pr = fix modular_constr_pr mt diff --git a/printing/ppconstr.mli b/printing/ppconstr.mli index 482c994c25..7546c748d8 100644 --- a/printing/ppconstr.mli +++ b/printing/ppconstr.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -9,14 +9,13 @@ (** This module implements pretty-printers for constr_expr syntactic objects and their subcomponents. *) -(** The default pretty-printers produce {!Pp.std_ppcmds} that are - interpreted as raw strings. *) +(** The default pretty-printers produce pretty-printing commands ({!Pp.t}). *) open Loc -open Pp open Libnames open Constrexpr open Names open Misctypes +open Notation_term val extract_lam_binders : constr_expr -> local_binder_expr list * constr_expr @@ -26,47 +25,47 @@ val split_fix : int -> constr_expr -> constr_expr -> local_binder_expr list * constr_expr * constr_expr -val prec_less : int -> int * Ppextend.parenRelation -> bool +val prec_less : precedence -> tolerability -> bool -val pr_tight_coma : unit -> std_ppcmds +val pr_tight_coma : unit -> Pp.t -val pr_or_var : ('a -> std_ppcmds) -> 'a or_var -> std_ppcmds +val pr_or_var : ('a -> Pp.t) -> 'a or_var -> Pp.t -val pr_lident : Id.t located -> std_ppcmds -val pr_lname : Name.t located -> std_ppcmds +val pr_lident : Id.t located -> Pp.t +val pr_lname : Name.t located -> Pp.t -val pr_with_comments : ?loc:Loc.t -> std_ppcmds -> std_ppcmds -val pr_com_at : int -> std_ppcmds +val pr_with_comments : ?loc:Loc.t -> Pp.t -> Pp.t +val pr_com_at : int -> Pp.t val pr_sep_com : - (unit -> std_ppcmds) -> - (constr_expr -> std_ppcmds) -> - constr_expr -> std_ppcmds + (unit -> Pp.t) -> + (constr_expr -> Pp.t) -> + constr_expr -> Pp.t -val pr_id : Id.t -> std_ppcmds -val pr_name : Name.t -> std_ppcmds -val pr_qualid : qualid -> std_ppcmds -val pr_patvar : patvar -> std_ppcmds +val pr_id : Id.t -> Pp.t +val pr_name : Name.t -> Pp.t +val pr_qualid : qualid -> Pp.t +val pr_patvar : patvar -> Pp.t -val pr_glob_level : glob_level -> std_ppcmds -val pr_glob_sort : glob_sort -> std_ppcmds -val pr_guard_annot : (constr_expr -> std_ppcmds) -> +val pr_glob_level : glob_level -> Pp.t +val pr_glob_sort : glob_sort -> Pp.t +val pr_guard_annot : (constr_expr -> Pp.t) -> local_binder_expr list -> ('a * Names.Id.t) option * recursion_order_expr -> - std_ppcmds + Pp.t -val pr_record_body : (reference * constr_expr) list -> std_ppcmds -val pr_binders : local_binder_expr list -> std_ppcmds -val pr_constr_pattern_expr : constr_pattern_expr -> std_ppcmds -val pr_lconstr_pattern_expr : constr_pattern_expr -> std_ppcmds -val pr_constr_expr : constr_expr -> std_ppcmds -val pr_lconstr_expr : constr_expr -> std_ppcmds -val pr_cases_pattern_expr : cases_pattern_expr -> std_ppcmds +val pr_record_body : (reference * constr_expr) list -> Pp.t +val pr_binders : local_binder_expr list -> Pp.t +val pr_constr_pattern_expr : constr_pattern_expr -> Pp.t +val pr_lconstr_pattern_expr : constr_pattern_expr -> Pp.t +val pr_constr_expr : constr_expr -> Pp.t +val pr_lconstr_expr : constr_expr -> Pp.t +val pr_cases_pattern_expr : cases_pattern_expr -> Pp.t type term_pr = { - pr_constr_expr : constr_expr -> std_ppcmds; - pr_lconstr_expr : constr_expr -> std_ppcmds; - pr_constr_pattern_expr : constr_pattern_expr -> std_ppcmds; - pr_lconstr_pattern_expr : constr_pattern_expr -> std_ppcmds + pr_constr_expr : constr_expr -> Pp.t; + pr_lconstr_expr : constr_expr -> Pp.t; + pr_constr_pattern_expr : constr_pattern_expr -> Pp.t; + pr_lconstr_pattern_expr : constr_pattern_expr -> Pp.t } val set_term_pr : term_pr -> unit @@ -91,5 +90,5 @@ type precedence val lsimpleconstr : precedence val ltop : precedence val modular_constr_pr : - ((unit->std_ppcmds) -> precedence -> constr_expr -> std_ppcmds) -> - (unit->std_ppcmds) -> precedence -> constr_expr -> std_ppcmds + ((unit->Pp.t) -> precedence -> constr_expr -> Pp.t) -> + (unit->Pp.t) -> precedence -> constr_expr -> Pp.t diff --git a/printing/pputils.ml b/printing/pputils.ml index 99d07601c4..9ef9162aee 100644 --- a/printing/pputils.ml +++ b/printing/pputils.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) diff --git a/printing/pputils.mli b/printing/pputils.mli index b236fed702..1f4fa1390d 100644 --- a/printing/pputils.mli +++ b/printing/pputils.mli @@ -1,31 +1,30 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Pp open Genarg open Misctypes open Locus open Genredexpr -val pr_located : ('a -> std_ppcmds) -> 'a Loc.located -> std_ppcmds +val pr_located : ('a -> Pp.t) -> 'a Loc.located -> Pp.t (** Prints an object surrounded by its commented location *) -val pr_or_var : ('a -> std_ppcmds) -> 'a or_var -> std_ppcmds -val pr_or_by_notation : ('a -> std_ppcmds) -> 'a or_by_notation -> std_ppcmds +val pr_or_var : ('a -> Pp.t) -> 'a or_var -> Pp.t +val pr_or_by_notation : ('a -> Pp.t) -> 'a or_by_notation -> Pp.t val pr_with_occurrences : - ('a -> std_ppcmds) -> (string -> std_ppcmds) -> 'a with_occurrences -> std_ppcmds + ('a -> Pp.t) -> (string -> Pp.t) -> 'a with_occurrences -> Pp.t -val pr_short_red_flag : ('a -> std_ppcmds) -> 'a glob_red_flag -> std_ppcmds -val pr_red_flag : ('a -> std_ppcmds) -> 'a glob_red_flag -> std_ppcmds +val pr_short_red_flag : ('a -> Pp.t) -> 'a glob_red_flag -> Pp.t +val pr_red_flag : ('a -> Pp.t) -> 'a glob_red_flag -> Pp.t val pr_red_expr : - ('a -> std_ppcmds) * ('a -> std_ppcmds) * ('b -> std_ppcmds) * ('c -> std_ppcmds) -> - (string -> std_ppcmds) -> - ('a,'b,'c) red_expr_gen -> std_ppcmds + ('a -> Pp.t) * ('a -> Pp.t) * ('b -> Pp.t) * ('c -> Pp.t) -> + (string -> Pp.t) -> + ('a,'b,'c) red_expr_gen -> Pp.t -val pr_raw_generic : Environ.env -> rlevel generic_argument -> std_ppcmds -val pr_glb_generic : Environ.env -> glevel generic_argument -> std_ppcmds +val pr_raw_generic : Environ.env -> rlevel generic_argument -> Pp.t +val pr_glb_generic : Environ.env -> glevel generic_argument -> Pp.t diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml index 9d28bc4f84..4c50c2f368 100644 --- a/printing/ppvernac.ml +++ b/printing/ppvernac.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -105,7 +105,7 @@ open Decl_kinds | SearchString (s,sc) -> qs s ++ pr_opt (fun sc -> str "%" ++ str sc) sc let pr_search a gopt b pr_p = - pr_opt (fun g -> Proof_global.pr_goal_selector g ++ str ":"++ spc()) gopt + pr_opt (fun g -> Proof_bullet.pr_goal_selector g ++ str ":"++ spc()) gopt ++ match a with | SearchHead c -> keyword "SearchHead" ++ spc() ++ pr_p c ++ pr_in_out_modules b @@ -490,7 +490,7 @@ open Decl_kinds | PrintVisibility s -> keyword "Print Visibility" ++ pr_opt str s | PrintAbout (qid,gopt) -> - pr_opt (fun g -> Proof_global.pr_goal_selector g ++ str ":"++ spc()) gopt + pr_opt (fun g -> Proof_bullet.pr_goal_selector g ++ str ":"++ spc()) gopt ++ keyword "About" ++ spc() ++ pr_smart_global qid | PrintImplicit qid -> keyword "Print Implicit" ++ spc() ++ pr_smart_global qid @@ -698,7 +698,7 @@ open Decl_kinds | Some cc -> str" :=" ++ spc() ++ cc)) ) - | VernacStartTheoremProof (ki,l,_) -> + | VernacStartTheoremProof (ki,l) -> return ( hov 1 (pr_statement (pr_thm_token ki) (List.hd l) ++ prlist (pr_statement (spc () ++ keyword "with")) (List.tl l)) @@ -727,7 +727,7 @@ open Decl_kinds let assumptions = prlist_with_sep spc (fun p -> hov 1 (str "(" ++ pr_params p ++ str ")")) l in return (hov 2 (pr_assumption_token (n > 1) stre ++ pr_non_empty_arg pr_assumption_inline t ++ spc() ++ assumptions)) - | VernacInductive (p,f,l) -> + | VernacInductive (cum, p,f,l) -> let pr_constructor (coe,(id,c)) = hov 2 (pr_lident id ++ str" " ++ (if coe then str":>" else str":") ++ @@ -754,13 +754,23 @@ open Decl_kinds in let key = let (_,_,_,k,_),_ = List.hd l in - match k with Record -> "Record" | Structure -> "Structure" - | Inductive_kw -> "Inductive" | CoInductive -> "CoInductive" - | Class _ -> "Class" | Variant -> "Variant" + let kind = + match k with Record -> "Record" | Structure -> "Structure" + | Inductive_kw -> "Inductive" | CoInductive -> "CoInductive" + | Class _ -> "Class" | Variant -> "Variant" + in + if p then + let cm = + match cum with + | GlobalCumulativity | LocalCumulativity -> "Cumulative" + | GlobalNonCumulativity | LocalNonCumulativity -> "NonCumulative" + in + cm ^ " " ^ kind + else kind in return ( hov 1 (pr_oneind key (List.hd l)) ++ - (prlist (fun ind -> fnl() ++ hov 1 (pr_oneind "with" ind)) (List.tl l)) + (prlist (fun ind -> fnl() ++ hov 1 (pr_oneind "with" ind)) (List.tl l)) ) | VernacFixpoint (local, recs) -> @@ -1126,7 +1136,7 @@ open Decl_kinds | None -> hov 2 (keyword "Check" ++ spc() ++ pr_lconstr c) in let pr_i = match io with None -> mt () - | Some i -> Proof_global.pr_goal_selector i ++ str ": " in + | Some i -> Proof_bullet.pr_goal_selector i ++ str ": " in return (pr_i ++ pr_mayeval r c) | VernacGlobalCheck c -> return (hov 2 (keyword "Type" ++ pr_constrarg c)) diff --git a/printing/ppvernac.mli b/printing/ppvernac.mli index 836b05e0e4..b88eed4843 100644 --- a/printing/ppvernac.mli +++ b/printing/ppvernac.mli @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -10,10 +10,10 @@ objects and their subcomponents. *) (** Prints a fixpoint body *) -val pr_rec_definition : (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) -> Pp.std_ppcmds +val pr_rec_definition : (Vernacexpr.fixpoint_expr * Vernacexpr.decl_notation list) -> Pp.t (** Prints a vernac expression *) -val pr_vernac_body : Vernacexpr.vernac_expr -> Pp.std_ppcmds +val pr_vernac_body : Vernacexpr.vernac_expr -> Pp.t (** Prints a vernac expression and closes it with a dot. *) -val pr_vernac : Vernacexpr.vernac_expr -> Pp.std_ppcmds +val pr_vernac : Vernacexpr.vernac_expr -> Pp.t diff --git a/printing/prettyp.ml b/printing/prettyp.ml index 3ae7da8fc1..09859157c3 100644 --- a/printing/prettyp.ml +++ b/printing/prettyp.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -33,17 +33,17 @@ open Context.Rel.Declaration module NamedDecl = Context.Named.Declaration type object_pr = { - print_inductive : mutual_inductive -> std_ppcmds; - print_constant_with_infos : constant -> std_ppcmds; - print_section_variable : variable -> std_ppcmds; - print_syntactic_def : kernel_name -> std_ppcmds; - print_module : bool -> Names.module_path -> std_ppcmds; - print_modtype : module_path -> std_ppcmds; - print_named_decl : Context.Named.Declaration.t -> std_ppcmds; - print_library_entry : bool -> (object_name * Lib.node) -> std_ppcmds option; - print_context : bool -> int option -> Lib.library_segment -> std_ppcmds; - print_typed_value_in_env : Environ.env -> Evd.evar_map -> EConstr.constr * EConstr.types -> Pp.std_ppcmds; - print_eval : Reductionops.reduction_function -> env -> Evd.evar_map -> Constrexpr.constr_expr -> EConstr.unsafe_judgment -> std_ppcmds; + print_inductive : mutual_inductive -> Pp.t; + print_constant_with_infos : constant -> Pp.t; + print_section_variable : variable -> Pp.t; + print_syntactic_def : kernel_name -> Pp.t; + print_module : bool -> Names.module_path -> Pp.t; + print_modtype : module_path -> Pp.t; + print_named_decl : Context.Named.Declaration.t -> Pp.t; + print_library_entry : bool -> (object_name * Lib.node) -> Pp.t option; + print_context : bool -> int option -> Lib.library_segment -> Pp.t; + print_typed_value_in_env : Environ.env -> Evd.evar_map -> EConstr.constr * EConstr.types -> Pp.t; + print_eval : Reductionops.reduction_function -> env -> Evd.evar_map -> Constrexpr.constr_expr -> EConstr.unsafe_judgment -> Pp.t; } let gallina_print_module = print_module @@ -70,7 +70,8 @@ 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 = - let typ = Global.type_of_global_unsafe ref in + let typ, ctx = Global.type_of_global_in_context (Global.env ()) ref in + let typ = Vars.subst_instance_constr (Univ.AUContext.instance ctx) typ in let typ = EConstr.of_constr typ in let typ = if reduce then @@ -78,6 +79,8 @@ let print_ref reduce ref = in EConstr.it_mkProd_or_LetIn ccl ctx else typ in let univs = Global.universes_of_global ref in + let inst = Univ.AUContext.instance univs in + let univs = Univ.UContext.make (inst, Univ.AUContext.instantiate inst univs) in let env = Global.env () in let bl = Universes.universe_binders_of_global ref in let sigma = Evd.from_ctx (Evd.evar_universe_context_of_binders bl) in @@ -135,7 +138,7 @@ let print_renames_list prefix l = hv 2 (prlist_with_sep pr_comma (fun x -> x) (List.map Name.print l))] let need_expansion impl ref = - let typ = Global.type_of_global_unsafe ref in + let typ, _ = Global.type_of_global_in_context (Global.env ()) ref in let ctx = prod_assum typ in let nprods = List.count is_local_assum ctx in not (List.is_empty impl) && List.length impl >= nprods && @@ -498,21 +501,45 @@ let print_body env evd = function let print_typed_body env evd (val_0,typ) = (print_body env evd val_0 ++ fnl () ++ str " : " ++ pr_ltype_env env evd typ) -let ungeneralized_type_of_constant_type t = - Typeops.type_of_constant_type (Global.env ()) t - let print_instance sigma cb = - if cb.const_polymorphic then - pr_universe_instance sigma cb.const_universes + if Declareops.constant_is_polymorphic cb then + let univs = Declareops.constant_polymorphic_context cb in + let inst = Univ.AUContext.instance univs in + let univs = Univ.UContext.make (inst, Univ.AUContext.instantiate inst univs) in + pr_universe_instance sigma univs else mt() let print_constant with_values sep sp = let cb = Global.lookup_constant sp in let val_0 = Global.body_of_constant_body cb in - let typ = Declareops.type_of_constant cb in - let typ = ungeneralized_type_of_constant_type typ in - let univs = Univ.instantiate_univ_context - (Global.universes_of_constant_body cb) + let typ = + match cb.const_universes with + | Monomorphic_const _ -> cb.const_type + | Polymorphic_const univs -> + let inst = Univ.AUContext.instance univs in + Vars.subst_instance_constr inst cb.const_type + in + let univs = + let otab = Global.opaque_tables () in + match cb.const_body with + | Undef _ | Def _ -> + begin + match cb.const_universes with + | Monomorphic_const ctx -> ctx + | Polymorphic_const ctx -> + let inst = Univ.AUContext.instance ctx in + Univ.UContext.make (inst, Univ.AUContext.instantiate inst ctx) + end + | OpaqueDef o -> + let body_uctxs = Opaqueproof.force_constraints otab o in + match cb.const_universes with + | Monomorphic_const ctx -> + let uctxs = Univ.ContextSet.of_context ctx in + Univ.ContextSet.to_context (Univ.ContextSet.union body_uctxs uctxs) + | Polymorphic_const ctx -> + assert(Univ.ContextSet.is_empty body_uctxs); + let inst = Univ.AUContext.instance ctx in + Univ.UContext.make (inst, Univ.AUContext.instantiate inst ctx) in let ctx = Evd.evar_universe_context_of_binders @@ -520,16 +547,17 @@ let print_constant with_values sep sp = in let env = Global.env () and sigma = Evd.from_ctx ctx in let pr_ltype = pr_ltype_env env sigma in - hov 0 (pr_polymorphic cb.const_polymorphic ++ + hov 0 (pr_polymorphic (Declareops.constant_is_polymorphic cb) ++ match val_0 with | None -> str"*** [ " ++ print_basename sp ++ print_instance sigma cb ++ str " : " ++ cut () ++ pr_ltype typ ++ str" ]" ++ Printer.pr_universe_ctx sigma univs - | _ -> + | Some (c, ctx) -> + let c = Vars.subst_instance_constr (Univ.AUContext.instance ctx) c in print_basename sp ++ print_instance sigma cb ++ str sep ++ cut () ++ - (if with_values then print_typed_body env sigma (val_0,typ) else pr_ltype typ)++ + (if with_values then print_typed_body env sigma (Some c,typ) else pr_ltype typ)++ Printer.pr_universe_ctx sigma univs) let gallina_print_constant_with_infos sp = @@ -663,7 +691,7 @@ let print_full_pure_context () = | "CONSTANT" -> let con = Global.constant_of_delta_kn kn in let cb = Global.lookup_constant con in - let typ = ungeneralized_type_of_constant_type cb.const_type in + let typ = cb.const_type in hov 0 ( match cb.const_body with | Undef _ -> @@ -767,9 +795,11 @@ let print_opaque_name qid = | IndRef (sp,_) -> print_inductive sp | ConstructRef cstr as gr -> - let open EConstr in - let ty = Universes.unsafe_type_of_global gr in + let ty, ctx = Global.type_of_global_in_context env gr in + let inst = Univ.AUContext.instance ctx in + let ty = Vars.subst_instance_constr inst ty in let ty = EConstr.of_constr ty in + let open EConstr in print_typed_value (mkConstruct cstr, ty) | VarRef id -> env |> lookup_named id |> NamedDecl.set_id id |> print_named_decl diff --git a/printing/prettyp.mli b/printing/prettyp.mli index 6841781ccd..f4277b6c50 100644 --- a/printing/prettyp.mli +++ b/printing/prettyp.mli @@ -1,12 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Pp open Names open Environ open Reductionops @@ -19,57 +18,57 @@ open Misctypes val assumptions_for_print : Name.t list -> Termops.names_context val print_closed_sections : bool ref -val print_context : bool -> int option -> Lib.library_segment -> std_ppcmds -val print_library_entry : bool -> (object_name * Lib.node) -> std_ppcmds option -val print_full_context : unit -> std_ppcmds -val print_full_context_typ : unit -> std_ppcmds -val print_full_pure_context : unit -> std_ppcmds -val print_sec_context : reference -> std_ppcmds -val print_sec_context_typ : reference -> std_ppcmds -val print_judgment : env -> Evd.evar_map -> EConstr.unsafe_judgment -> std_ppcmds -val print_safe_judgment : env -> Evd.evar_map -> Safe_typing.judgment -> std_ppcmds +val print_context : bool -> int option -> Lib.library_segment -> Pp.t +val print_library_entry : bool -> (object_name * Lib.node) -> Pp.t option +val print_full_context : unit -> Pp.t +val print_full_context_typ : unit -> Pp.t +val print_full_pure_context : unit -> Pp.t +val print_sec_context : reference -> Pp.t +val print_sec_context_typ : reference -> Pp.t +val print_judgment : env -> Evd.evar_map -> EConstr.unsafe_judgment -> Pp.t +val print_safe_judgment : env -> Evd.evar_map -> Safe_typing.judgment -> Pp.t val print_eval : reduction_function -> env -> Evd.evar_map -> - Constrexpr.constr_expr -> EConstr.unsafe_judgment -> std_ppcmds + Constrexpr.constr_expr -> EConstr.unsafe_judgment -> Pp.t -val print_name : reference or_by_notation -> std_ppcmds -val print_opaque_name : reference -> std_ppcmds -val print_about : reference or_by_notation -> std_ppcmds -val print_impargs : reference or_by_notation -> std_ppcmds +val print_name : reference or_by_notation -> Pp.t +val print_opaque_name : reference -> Pp.t +val print_about : reference or_by_notation -> Pp.t +val print_impargs : reference or_by_notation -> Pp.t (** Pretty-printing functions for classes and coercions *) -val print_graph : unit -> std_ppcmds -val print_classes : unit -> std_ppcmds -val print_coercions : unit -> std_ppcmds -val print_path_between : Classops.cl_typ -> Classops.cl_typ -> std_ppcmds -val print_canonical_projections : unit -> std_ppcmds +val print_graph : unit -> Pp.t +val print_classes : unit -> Pp.t +val print_coercions : unit -> Pp.t +val print_path_between : Classops.cl_typ -> Classops.cl_typ -> Pp.t +val print_canonical_projections : unit -> Pp.t (** Pretty-printing functions for type classes and instances *) -val print_typeclasses : unit -> std_ppcmds -val print_instances : global_reference -> std_ppcmds -val print_all_instances : unit -> std_ppcmds +val print_typeclasses : unit -> Pp.t +val print_instances : global_reference -> Pp.t +val print_all_instances : unit -> Pp.t -val inspect : int -> std_ppcmds +val inspect : int -> Pp.t (** Locate *) -val print_located_qualid : reference -> std_ppcmds -val print_located_term : reference -> std_ppcmds -val print_located_tactic : reference -> std_ppcmds -val print_located_module : reference -> std_ppcmds +val print_located_qualid : reference -> Pp.t +val print_located_term : reference -> Pp.t +val print_located_tactic : reference -> Pp.t +val print_located_module : reference -> Pp.t type object_pr = { - print_inductive : mutual_inductive -> std_ppcmds; - print_constant_with_infos : constant -> std_ppcmds; - print_section_variable : variable -> std_ppcmds; - print_syntactic_def : kernel_name -> std_ppcmds; - print_module : bool -> Names.module_path -> std_ppcmds; - print_modtype : module_path -> std_ppcmds; - print_named_decl : Context.Named.Declaration.t -> std_ppcmds; - print_library_entry : bool -> (object_name * Lib.node) -> std_ppcmds option; - print_context : bool -> int option -> Lib.library_segment -> std_ppcmds; - print_typed_value_in_env : Environ.env -> Evd.evar_map -> EConstr.constr * EConstr.types -> Pp.std_ppcmds; - print_eval : reduction_function -> env -> Evd.evar_map -> Constrexpr.constr_expr -> EConstr.unsafe_judgment -> std_ppcmds + print_inductive : mutual_inductive -> Pp.t; + print_constant_with_infos : constant -> Pp.t; + print_section_variable : variable -> Pp.t; + print_syntactic_def : kernel_name -> Pp.t; + print_module : bool -> Names.module_path -> Pp.t; + print_modtype : module_path -> Pp.t; + print_named_decl : Context.Named.Declaration.t -> Pp.t; + print_library_entry : bool -> (object_name * Lib.node) -> Pp.t option; + print_context : bool -> int option -> Lib.library_segment -> Pp.t; + print_typed_value_in_env : Environ.env -> Evd.evar_map -> EConstr.constr * EConstr.types -> Pp.t; + print_eval : reduction_function -> env -> Evd.evar_map -> Constrexpr.constr_expr -> EConstr.unsafe_judgment -> Pp.t } val set_object_pr : object_pr -> unit diff --git a/printing/printer.ml b/printing/printer.ml index d6f0778f75..28b10c7812 100644 --- a/printing/printer.ml +++ b/printing/printer.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -79,23 +79,23 @@ let _ = and only names of goal/section variables and rel names that do _not_ occur in the scope of the binder to be printed are avoided. *) -let pr_constr_core goal_concl_style env sigma t = +let pr_econstr_core goal_concl_style env sigma t = pr_constr_expr (extern_constr goal_concl_style env sigma t) -let pr_lconstr_core goal_concl_style env sigma t = +let pr_leconstr_core goal_concl_style env sigma t = pr_lconstr_expr (extern_constr goal_concl_style env sigma t) -let pr_lconstr_env env = pr_lconstr_core false env -let pr_constr_env env = pr_constr_core false env +let pr_lconstr_env env sigma c = pr_leconstr_core false env sigma (EConstr.of_constr c) +let pr_constr_env env sigma c = pr_econstr_core false env sigma (EConstr.of_constr c) let _ = Hook.set Refine.pr_constr pr_constr_env -let pr_lconstr_goal_style_env env = pr_lconstr_core true env -let pr_constr_goal_style_env env = pr_constr_core true env +let pr_lconstr_goal_style_env env sigma c = pr_leconstr_core true env sigma (EConstr.of_constr c) +let pr_constr_goal_style_env env sigma c = pr_econstr_core true env sigma (EConstr.of_constr c) let pr_open_lconstr_env env sigma (_,c) = pr_lconstr_env env sigma c let pr_open_constr_env env sigma (_,c) = pr_constr_env env sigma c -let pr_leconstr_env env sigma c = pr_lconstr_env env sigma (EConstr.to_constr sigma c) -let pr_econstr_env env sigma c = pr_constr_env env sigma (EConstr.to_constr sigma c) +let pr_leconstr_env env sigma c = pr_leconstr_core false env sigma c +let pr_econstr_env env sigma c = pr_econstr_core false env sigma c (* NB do not remove the eta-redexes! Global.env() has side-effects... *) let pr_lconstr t = @@ -128,13 +128,13 @@ let pr_lconstr_under_binders c = let (sigma, env) = get_current_context () in pr_lconstr_under_binders_env env sigma c -let pr_type_core goal_concl_style env sigma t = +let pr_etype_core goal_concl_style env sigma t = pr_constr_expr (extern_type goal_concl_style env sigma t) -let pr_ltype_core goal_concl_style env sigma t = +let pr_letype_core goal_concl_style env sigma t = pr_lconstr_expr (extern_type goal_concl_style env sigma t) -let pr_ltype_env env = pr_ltype_core false env -let pr_type_env env = pr_type_core false env +let pr_ltype_env env sigma c = pr_letype_core false env sigma (EConstr.of_constr c) +let pr_type_env env sigma c = pr_etype_core false env sigma (EConstr.of_constr c) let pr_ltype t = let (sigma, env) = get_current_context () in @@ -143,10 +143,9 @@ let pr_type t = let (sigma, env) = get_current_context () in pr_type_env env sigma t -let pr_etype_env env sigma c = pr_type_env env sigma (EConstr.to_constr sigma c) -let pr_letype_env env sigma c = pr_ltype_env env sigma (EConstr.to_constr sigma c) -let pr_goal_concl_style_env env sigma c = - pr_ltype_core true env sigma (EConstr.to_constr sigma c) +let pr_etype_env env sigma c = pr_etype_core false env sigma c +let pr_letype_env env sigma c = pr_letype_core false env sigma c +let pr_goal_concl_style_env env sigma c = pr_letype_core true env sigma c let pr_ljudge_env env sigma j = (pr_leconstr_env env sigma j.uj_val, pr_leconstr_env env sigma j.uj_type) @@ -191,7 +190,7 @@ let pr_constr_pattern t = let pr_sort sigma s = pr_glob_sort (extern_sort sigma s) let _ = Termops.set_print_constr - (fun env sigma t -> pr_lconstr_expr (extern_constr ~lax:true false env sigma (EConstr.Unsafe.to_constr t))) + (fun env sigma t -> pr_lconstr_expr (extern_constr ~lax:true false env sigma t)) let pr_in_comment pr x = str "(* " ++ pr x ++ str " *)" @@ -261,6 +260,14 @@ let pr_universe_ctx sigma c = else mt() +let pr_cumulativity_info sigma cumi = + if !Detyping.print_universes + && not (Univ.UContext.is_empty (Univ.CumulativityInfo.univ_context cumi)) then + fnl()++pr_in_comment (fun uii -> v 0 + (Univ.pr_cumulativity_info (Termops.pr_evd_level sigma) uii)) cumi + else + mt() + (**********************************************************************) (* Global references *) @@ -356,6 +363,7 @@ let pr_named_context env sigma ne_context = ne_context ~init:(mt ())) let pr_rel_context env sigma rel_context = + let rel_context = List.map (fun d -> Termops.map_rel_decl EConstr.of_constr d) rel_context in pr_binders (extern_rel_context None env sigma rel_context) let pr_rel_context_of env sigma = @@ -471,7 +479,8 @@ let pr_transparent_state (ids, csts) = (* display complete goal *) let default_pr_goal gs = - let (g,sigma) = Goal.V82.nf_evar (project gs) (sig_it gs) in + let g = sig_it gs in + let sigma = project gs in let env = Goal.V82.env sigma g in let concl = Goal.V82.concl sigma g in let goal = @@ -719,7 +728,7 @@ let default_pr_subgoals ?(pr_first=true) match goals with | [] -> begin - let exl = Evarutil.non_instantiated sigma in + let exl = Evd.undefined_map sigma in if Evar.Map.is_empty exl then (str"No more subgoals." ++ print_dependent_evars None sigma seeds) else @@ -750,9 +759,9 @@ let default_pr_subgoals ?(pr_first=true) type printer_pr = { - 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; + pr_subgoals : ?pr_first:bool -> Pp.t option -> evar_map -> evar list -> Goal.goal list -> int list -> goal list -> goal list -> Pp.t; + pr_subgoal : int -> evar_map -> goal list -> Pp.t; + pr_goal : goal sigma -> Pp.t; } let default_printer_pr = { @@ -797,7 +806,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 + (let s = Proof_bullet.suggest p in if Pp.ismt s then s else fnl () ++ s) ++ fnl () in @@ -837,15 +846,6 @@ let pr_goal_by_uid uid = (* Elementary tactics *) let pr_prim_rule = function - | Cut (b,replace,id,t) -> - if b then - (* TODO: express "replace" *) - (str"assert " ++ str"(" ++ pr_id id ++ str":" ++ pr_lconstr t ++ str")") - else - let cl = if replace then str"clear " ++ pr_id id ++ str"; " else mt() in - (str"cut " ++ pr_constr t ++ - str ";[" ++ cl ++ str"intro " ++ pr_id id ++ str"|idtac]") - | Refine c -> (** FIXME *) str(if Termops.occur_meta Evd.empty (EConstr.of_constr c) then "refine " else "exact ") ++ @@ -991,6 +991,11 @@ let pr_assumptionset env s = let xor a b = (a && not b) || (not a && b) +let pr_cumulative poly cum = + if poly then + if cum then str "Cumulative " else str "NonCumulative " + else mt () + let pr_polymorphic b = let print = xor (Flags.is_universe_polymorphism ()) b in if print then diff --git a/printing/printer.mli b/printing/printer.mli index 3fce065613..2c9a4d70e6 100644 --- a/printing/printer.mli +++ b/printing/printer.mli @@ -1,12 +1,11 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Pp open Names open Globnames open Term @@ -25,94 +24,96 @@ val enable_goal_names_printing : bool ref (** Terms *) -val pr_lconstr_env : env -> evar_map -> constr -> std_ppcmds -val pr_lconstr : constr -> std_ppcmds -val pr_lconstr_goal_style_env : env -> evar_map -> constr -> std_ppcmds +val pr_lconstr_env : env -> evar_map -> constr -> Pp.t +val pr_lconstr : constr -> Pp.t +val pr_lconstr_goal_style_env : env -> evar_map -> constr -> Pp.t -val pr_constr_env : env -> evar_map -> constr -> std_ppcmds -val pr_constr : constr -> std_ppcmds -val pr_constr_goal_style_env : env -> evar_map -> constr -> std_ppcmds +val pr_constr_env : env -> evar_map -> constr -> Pp.t +val pr_constr : constr -> Pp.t +val pr_constr_goal_style_env : env -> evar_map -> constr -> Pp.t (** Same, but resilient to [Nametab] errors. Prints fully-qualified names when [shortest_qualid_of_global] has failed. Prints "??" in case of remaining issues (such as reference not in env). *) -val safe_pr_lconstr_env : env -> evar_map -> constr -> std_ppcmds -val safe_pr_lconstr : constr -> std_ppcmds +val safe_pr_lconstr_env : env -> evar_map -> constr -> Pp.t +val safe_pr_lconstr : constr -> Pp.t -val safe_pr_constr_env : env -> evar_map -> constr -> std_ppcmds -val safe_pr_constr : constr -> std_ppcmds +val safe_pr_constr_env : env -> evar_map -> constr -> Pp.t +val safe_pr_constr : constr -> Pp.t -val pr_econstr_env : env -> evar_map -> EConstr.t -> std_ppcmds -val pr_econstr : EConstr.t -> std_ppcmds -val pr_leconstr_env : env -> evar_map -> EConstr.t -> std_ppcmds -val pr_leconstr : EConstr.t -> std_ppcmds +val pr_econstr_env : env -> evar_map -> EConstr.t -> Pp.t +val pr_econstr : EConstr.t -> Pp.t +val pr_leconstr_env : env -> evar_map -> EConstr.t -> Pp.t +val pr_leconstr : EConstr.t -> Pp.t -val pr_etype_env : env -> evar_map -> EConstr.types -> std_ppcmds -val pr_letype_env : env -> evar_map -> EConstr.types -> std_ppcmds +val pr_etype_env : env -> evar_map -> EConstr.types -> Pp.t +val pr_letype_env : env -> evar_map -> EConstr.types -> Pp.t -val pr_open_constr_env : env -> evar_map -> open_constr -> std_ppcmds -val pr_open_constr : open_constr -> std_ppcmds +val pr_open_constr_env : env -> evar_map -> open_constr -> Pp.t +val pr_open_constr : open_constr -> Pp.t -val pr_open_lconstr_env : env -> evar_map -> open_constr -> std_ppcmds -val pr_open_lconstr : open_constr -> std_ppcmds +val pr_open_lconstr_env : env -> evar_map -> open_constr -> Pp.t +val pr_open_lconstr : open_constr -> Pp.t -val pr_constr_under_binders_env : env -> evar_map -> constr_under_binders -> std_ppcmds -val pr_constr_under_binders : constr_under_binders -> std_ppcmds +val pr_constr_under_binders_env : env -> evar_map -> constr_under_binders -> Pp.t +val pr_constr_under_binders : constr_under_binders -> Pp.t -val pr_lconstr_under_binders_env : env -> evar_map -> constr_under_binders -> std_ppcmds -val pr_lconstr_under_binders : constr_under_binders -> std_ppcmds +val pr_lconstr_under_binders_env : env -> evar_map -> constr_under_binders -> Pp.t +val pr_lconstr_under_binders : constr_under_binders -> Pp.t -val pr_goal_concl_style_env : env -> evar_map -> EConstr.types -> std_ppcmds -val pr_ltype_env : env -> evar_map -> types -> std_ppcmds -val pr_ltype : types -> std_ppcmds +val pr_goal_concl_style_env : env -> evar_map -> EConstr.types -> Pp.t +val pr_ltype_env : env -> evar_map -> types -> Pp.t +val pr_ltype : types -> Pp.t -val pr_type_env : env -> evar_map -> types -> std_ppcmds -val pr_type : types -> std_ppcmds +val pr_type_env : env -> evar_map -> types -> Pp.t +val pr_type : types -> Pp.t -val pr_closed_glob_env : env -> evar_map -> closed_glob_constr -> std_ppcmds -val pr_closed_glob : closed_glob_constr -> std_ppcmds +val pr_closed_glob_env : env -> evar_map -> closed_glob_constr -> Pp.t +val pr_closed_glob : closed_glob_constr -> Pp.t -val pr_ljudge_env : env -> evar_map -> EConstr.unsafe_judgment -> std_ppcmds * std_ppcmds -val pr_ljudge : EConstr.unsafe_judgment -> std_ppcmds * std_ppcmds +val pr_ljudge_env : env -> evar_map -> EConstr.unsafe_judgment -> Pp.t * Pp.t +val pr_ljudge : EConstr.unsafe_judgment -> Pp.t * Pp.t -val pr_lglob_constr_env : env -> glob_constr -> std_ppcmds -val pr_lglob_constr : glob_constr -> std_ppcmds +val pr_lglob_constr_env : env -> glob_constr -> Pp.t +val pr_lglob_constr : glob_constr -> Pp.t -val pr_glob_constr_env : env -> glob_constr -> std_ppcmds -val pr_glob_constr : glob_constr -> std_ppcmds +val pr_glob_constr_env : env -> glob_constr -> Pp.t +val pr_glob_constr : glob_constr -> Pp.t -val pr_lconstr_pattern_env : env -> evar_map -> constr_pattern -> std_ppcmds -val pr_lconstr_pattern : constr_pattern -> std_ppcmds +val pr_lconstr_pattern_env : env -> evar_map -> constr_pattern -> Pp.t +val pr_lconstr_pattern : constr_pattern -> Pp.t -val pr_constr_pattern_env : env -> evar_map -> constr_pattern -> std_ppcmds -val pr_constr_pattern : constr_pattern -> std_ppcmds +val pr_constr_pattern_env : env -> evar_map -> constr_pattern -> Pp.t +val pr_constr_pattern : constr_pattern -> Pp.t -val pr_cases_pattern : cases_pattern -> std_ppcmds +val pr_cases_pattern : cases_pattern -> Pp.t -val pr_sort : evar_map -> sorts -> std_ppcmds +val pr_sort : evar_map -> sorts -> Pp.t (** Universe constraints *) -val pr_polymorphic : bool -> std_ppcmds -val pr_universe_instance : evar_map -> Univ.universe_context -> std_ppcmds -val pr_universe_ctx : evar_map -> Univ.universe_context -> std_ppcmds +val pr_polymorphic : bool -> Pp.t +val pr_cumulative : bool -> bool -> Pp.t +val pr_universe_instance : evar_map -> Univ.universe_context -> Pp.t +val pr_universe_ctx : evar_map -> Univ.universe_context -> Pp.t +val pr_cumulativity_info : evar_map -> Univ.cumulativity_info -> Pp.t (** Printing global references using names as short as possible *) -val pr_global_env : Id.Set.t -> global_reference -> std_ppcmds -val pr_global : global_reference -> std_ppcmds +val pr_global_env : Id.Set.t -> global_reference -> Pp.t +val pr_global : global_reference -> Pp.t -val pr_constant : env -> constant -> std_ppcmds -val pr_existential_key : evar_map -> existential_key -> std_ppcmds -val pr_existential : env -> evar_map -> existential -> std_ppcmds -val pr_constructor : env -> constructor -> std_ppcmds -val pr_inductive : env -> inductive -> std_ppcmds -val pr_evaluable_reference : evaluable_global_reference -> std_ppcmds +val pr_constant : env -> constant -> Pp.t +val pr_existential_key : evar_map -> existential_key -> Pp.t +val pr_existential : env -> evar_map -> existential -> Pp.t +val pr_constructor : env -> constructor -> Pp.t +val pr_inductive : env -> inductive -> Pp.t +val pr_evaluable_reference : evaluable_global_reference -> Pp.t -val pr_pconstant : env -> pconstant -> std_ppcmds -val pr_pinductive : env -> pinductive -> std_ppcmds -val pr_pconstructor : env -> pconstructor -> std_ppcmds +val pr_pconstant : env -> pconstant -> Pp.t +val pr_pinductive : env -> pinductive -> Pp.t +val pr_pconstructor : env -> pconstructor -> Pp.t (** Contexts *) @@ -120,29 +121,29 @@ val pr_pconstructor : env -> pconstructor -> std_ppcmds 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 +val pr_context_unlimited : env -> evar_map -> Pp.t +val pr_ne_context_of : Pp.t -> env -> evar_map -> Pp.t -val pr_named_decl : env -> evar_map -> Context.Named.Declaration.t -> std_ppcmds -val pr_compacted_decl : env -> evar_map -> Context.Compacted.Declaration.t -> std_ppcmds -val pr_rel_decl : env -> evar_map -> Context.Rel.Declaration.t -> std_ppcmds +val pr_named_decl : env -> evar_map -> Context.Named.Declaration.t -> Pp.t +val pr_compacted_decl : env -> evar_map -> Context.Compacted.Declaration.t -> Pp.t +val pr_rel_decl : env -> evar_map -> Context.Rel.Declaration.t -> Pp.t -val pr_named_context : env -> evar_map -> Context.Named.t -> std_ppcmds -val pr_named_context_of : env -> evar_map -> std_ppcmds -val pr_rel_context : env -> evar_map -> Context.Rel.t -> std_ppcmds -val pr_rel_context_of : env -> evar_map -> std_ppcmds -val pr_context_of : env -> evar_map -> std_ppcmds +val pr_named_context : env -> evar_map -> Context.Named.t -> Pp.t +val pr_named_context_of : env -> evar_map -> Pp.t +val pr_rel_context : env -> evar_map -> Context.Rel.t -> Pp.t +val pr_rel_context_of : env -> evar_map -> Pp.t +val pr_context_of : env -> evar_map -> Pp.t (** Predicates *) -val pr_predicate : ('a -> std_ppcmds) -> (bool * 'a list) -> std_ppcmds -val pr_cpred : Cpred.t -> std_ppcmds -val pr_idpred : Id.Pred.t -> std_ppcmds -val pr_transparent_state : transparent_state -> std_ppcmds +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 (** Proofs, these functions obey [Hyps Limit] and [Compact contexts]. *) -val pr_goal : goal sigma -> std_ppcmds +val pr_goal : goal sigma -> Pp.t (** [pr_subgoals ~pr_first pp sigma seeds shelf focus_stack unfocused goals] prints the goals of the list [goals] followed by the goals in @@ -153,25 +154,25 @@ val pr_goal : goal sigma -> std_ppcmds focused goals unless the conrresponding option [enable_unfocused_goal_printing] is set. [seeds] is for printing dependent evars (mainly for emacs proof tree mode). *) -val pr_subgoals : ?pr_first:bool -> std_ppcmds option -> evar_map -> evar list -> Goal.goal list -> int list - -> goal list -> goal list -> std_ppcmds +val pr_subgoals : ?pr_first:bool -> Pp.t option -> evar_map -> evar list -> Goal.goal list -> int list + -> goal list -> goal list -> Pp.t -val pr_subgoal : int -> evar_map -> goal list -> std_ppcmds -val pr_concl : int -> evar_map -> goal -> std_ppcmds +val pr_subgoal : int -> evar_map -> goal list -> Pp.t +val pr_concl : int -> evar_map -> goal -> Pp.t -val pr_open_subgoals : ?proof:Proof.proof -> unit -> std_ppcmds -val pr_nth_open_subgoal : int -> std_ppcmds -val pr_evar : evar_map -> (evar * evar_info) -> std_ppcmds -val pr_evars_int : evar_map -> int -> evar_info Evar.Map.t -> std_ppcmds -val pr_evars : evar_map -> evar_info Evar.Map.t -> std_ppcmds -val pr_ne_evar_set : std_ppcmds -> std_ppcmds -> evar_map -> - Evar.Set.t -> std_ppcmds +val pr_open_subgoals : ?proof:Proof.proof -> unit -> Pp.t +val pr_nth_open_subgoal : int -> Pp.t +val pr_evar : evar_map -> (evar * evar_info) -> Pp.t +val pr_evars_int : evar_map -> 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 -val pr_prim_rule : prim_rule -> std_ppcmds +val pr_prim_rule : prim_rule -> Pp.t (** Backwards compatibility *) -val prterm : constr -> std_ppcmds (** = pr_lconstr *) +val prterm : constr -> Pp.t (** = pr_lconstr *) (** Declarations for the "Print Assumption" command *) @@ -191,15 +192,15 @@ module ContextObjectMap : CMap.ExtS with type key = context_object and module Set := ContextObjectSet val pr_assumptionset : - env -> Term.types ContextObjectMap.t -> std_ppcmds + env -> Term.types ContextObjectMap.t -> Pp.t -val pr_goal_by_id : Id.t -> std_ppcmds -val pr_goal_by_uid : string -> std_ppcmds +val pr_goal_by_id : Id.t -> Pp.t +val pr_goal_by_uid : string -> Pp.t type printer_pr = { - 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; + pr_subgoals : ?pr_first:bool -> Pp.t option -> evar_map -> evar list -> Goal.goal list -> int list -> goal list -> goal list -> Pp.t; + pr_subgoal : int -> evar_map -> goal list -> Pp.t; + pr_goal : goal sigma -> Pp.t; };; val set_printer_pr : printer_pr -> unit diff --git a/printing/printmod.ml b/printing/printmod.ml index c4affd4acd..219eafda4c 100644 --- a/printing/printmod.ml +++ b/printing/printmod.ml @@ -1,6 +1,6 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) @@ -88,8 +88,8 @@ let build_ind_type env mip = Inductive.type_of_inductive env mip let print_one_inductive env sigma mib ((_,i) as ind) = - let u = if mib.mind_polymorphic then - Univ.UContext.instance mib.mind_universes + let u = if Declareops.inductive_is_polymorphic mib then + Univ.AUContext.instance (Declareops.inductive_polymorphic_context mib) else Univ.Instance.empty in let mip = mib.mind_packets.(i) in let params = Inductive.inductive_paramdecls (mib,u) in @@ -99,8 +99,10 @@ let print_one_inductive env sigma mib ((_,i) as ind) = let cstrtypes = Array.map (fun c -> hnf_prod_applist env c args) cstrtypes in let envpar = push_rel_context params env in let inst = - if mib.mind_polymorphic then - Printer.pr_universe_instance sigma mib.mind_universes + if Declareops.inductive_is_polymorphic mib then + let ctx = Declareops.inductive_polymorphic_context mib in + let ctx = Univ.UContext.make (u, Univ.AUContext.instantiate u ctx) in + Printer.pr_universe_instance sigma ctx else mt () in hov 0 ( @@ -108,6 +110,17 @@ let print_one_inductive env sigma mib ((_,i) as ind) = str ": " ++ Printer.pr_lconstr_env envpar sigma arity ++ str " :=") ++ brk(0,2) ++ print_constructors envpar sigma mip.mind_consnames cstrtypes +let instantiate_cumulativity_info cumi = + let open Univ in + let univs = ACumulativityInfo.univ_context cumi in + let subtyp = ACumulativityInfo.subtyp_context cumi in + let expose ctx = + let inst = AUContext.instance ctx in + let cst = AUContext.instantiate inst ctx in + UContext.make (inst, cst) + in + CumulativityInfo.make (expose univs, expose subtyp) + let print_mutual_inductive env mind mib = let inds = List.init (Array.length mib.mind_packets) (fun x -> (mind, x)) in @@ -120,11 +133,18 @@ let print_mutual_inductive env mind mib = in let bl = Universes.universe_binders_of_global (IndRef (mind, 0)) in let sigma = Evd.from_ctx (Evd.evar_universe_context_of_binders bl) in - hov 0 (Printer.pr_polymorphic mib.mind_polymorphic ++ - def keyword ++ spc () ++ - prlist_with_sep (fun () -> fnl () ++ str" with ") - (print_one_inductive env sigma mib) inds ++ - Printer.pr_universe_ctx sigma (Univ.instantiate_univ_context mib.mind_universes)) + hov 0 (Printer.pr_polymorphic (Declareops.inductive_is_polymorphic mib) ++ + Printer.pr_cumulative + (Declareops.inductive_is_polymorphic mib) + (Declareops.inductive_is_cumulative mib) ++ + def keyword ++ spc () ++ + prlist_with_sep (fun () -> fnl () ++ str" with ") + (print_one_inductive env sigma mib) inds ++ + match mib.mind_universes with + | Monomorphic_ind _ | Polymorphic_ind _ -> str "" + | Cumulative_ind cumi -> + Printer.pr_cumulativity_info + sigma (instantiate_cumulativity_info cumi)) let get_fields = let rec prodec_rec l subst c = @@ -141,8 +161,8 @@ let get_fields = let print_record env mind mib = let u = - if mib.mind_polymorphic then - Univ.UContext.instance mib.mind_universes + if Declareops.inductive_is_polymorphic mib then + Univ.AUContext.instance (Declareops.inductive_polymorphic_context mib) else Univ.Instance.empty in let mip = mib.mind_packets.(0) in @@ -164,7 +184,10 @@ let print_record env mind mib = in hov 0 ( hov 0 ( - Printer.pr_polymorphic mib.mind_polymorphic ++ + Printer.pr_polymorphic (Declareops.inductive_is_polymorphic mib) ++ + Printer.pr_cumulative + (Declareops.inductive_is_polymorphic mib) + (Declareops.inductive_is_cumulative mib) ++ def keyword ++ spc () ++ pr_id mip.mind_typename ++ brk(1,4) ++ print_params env sigma params ++ str ": " ++ Printer.pr_lconstr_env envpar sigma arity ++ brk(1,2) ++ @@ -175,7 +198,12 @@ let print_record env mind mib = (fun (id,b,c) -> pr_id id ++ str (if b then " : " else " := ") ++ Printer.pr_lconstr_env envpar sigma c) fields) ++ str" }" ++ - Printer.pr_universe_ctx sigma (Univ.instantiate_univ_context mib.mind_universes)) + match mib.mind_universes with + | Monomorphic_ind _ | Polymorphic_ind _ -> str "" + | Cumulative_ind cumi -> + Printer.pr_cumulativity_info + sigma (instantiate_cumulativity_info cumi) + ) let pr_mutual_inductive_body env mind mib = if mib.mind_record <> None && not !Flags.raw_print then @@ -277,10 +305,13 @@ let print_body is_impl env mp (l,body) = | SFBmodule _ -> keyword "Module" ++ spc () ++ name | SFBmodtype _ -> keyword "Module Type" ++ spc () ++ name | SFBconst cb -> + let ctx = Declareops.constant_polymorphic_context cb in let u = - if cb.const_polymorphic then Univ.UContext.instance cb.const_universes + if Declareops.constant_is_polymorphic cb then + Univ.AUContext.instance ctx else Univ.Instance.empty in + let ctx = Univ.UContext.make (u, Univ.AUContext.instantiate u ctx) in let sigma = Evd.empty in (match cb.const_body with | Def _ -> def "Definition" ++ spc () @@ -292,7 +323,7 @@ let print_body is_impl env mp (l,body) = str " :" ++ spc () ++ hov 0 (Printer.pr_ltype_env env sigma (Vars.subst_instance_constr u - (Typeops.type_of_constant_type env cb.const_type))) ++ + cb.const_type)) ++ (match cb.const_body with | Def l when is_impl -> spc () ++ @@ -300,7 +331,7 @@ let print_body is_impl env mp (l,body) = Printer.pr_lconstr_env env sigma (Vars.subst_instance_constr u (Mod_subst.force_constr l))) | _ -> mt ()) ++ str "." ++ - Printer.pr_universe_ctx sigma (Univ.instantiate_univ_context cb.const_universes)) + Printer.pr_universe_ctx sigma ctx) | SFBmind mib -> try let env = Option.get env in diff --git a/printing/printmod.mli b/printing/printmod.mli index f3079d5b6b..8c3f0149e6 100644 --- a/printing/printmod.mli +++ b/printing/printmod.mli @@ -1,17 +1,16 @@ (************************************************************************) (* v * The Coq Proof Assistant / The Coq Development Team *) -(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2016 *) +(* <O___,, * INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2017 *) (* \VV/ **************************************************************) (* // * This file is distributed under the terms of the *) (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Pp open Names (** false iff the module is an element of an open module type *) val printable_body : DirPath.t -> bool -val pr_mutual_inductive_body : Environ.env -> mutual_inductive -> Declarations.mutual_inductive_body -> std_ppcmds -val print_module : bool -> module_path -> std_ppcmds -val print_modtype : module_path -> std_ppcmds +val pr_mutual_inductive_body : Environ.env -> mutual_inductive -> Declarations.mutual_inductive_body -> Pp.t +val print_module : bool -> module_path -> Pp.t +val print_modtype : module_path -> Pp.t |