aboutsummaryrefslogtreecommitdiff
path: root/printing
diff options
context:
space:
mode:
Diffstat (limited to 'printing')
-rw-r--r--printing/ppconstr.ml61
-rw-r--r--printing/ppconstrsig.mli1
-rw-r--r--printing/pptactic.ml65
-rw-r--r--printing/pptacticsig.mli3
-rw-r--r--printing/pputils.ml8
-rw-r--r--printing/ppvernac.ml87
-rw-r--r--printing/prettyp.ml16
-rw-r--r--printing/printer.ml94
-rw-r--r--printing/printmod.ml25
9 files changed, 250 insertions, 110 deletions
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index eead3a6840..aa94fb7be3 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -7,7 +7,7 @@
(************************************************************************)
(*i*)
-open Errors
+open CErrors
open Util
open Pp
open Names
@@ -129,7 +129,7 @@ end) = struct
str "`" ++ str hd ++ c ++ str tl
let pr_com_at n =
- if Flags.do_beautify() && not (Int.equal n 0) then comment n
+ if !Flags.beautify && not (Int.equal n 0) then comment (CLexer.extract_comments n)
else mt()
let pr_with_comments loc pp = pr_located (fun x -> x) (loc,pp)
@@ -149,6 +149,12 @@ end) = struct
| GType [] -> tag_type (str "Type")
| GType u -> hov 0 (tag_type (str "Type") ++ pr_univ_annot pr_univ u)
+ let pr_glob_level = function
+ | GProp -> tag_type (str "Prop")
+ | GSet -> tag_type (str "Set")
+ | GType None -> tag_type (str "Type")
+ | GType (Some (_, u)) -> tag_type (str u)
+
let pr_qualid sp =
let (sl, id) = repr_qualid sp in
let id = tag_ref (pr_id id) in
@@ -279,6 +285,8 @@ end) = struct
| CPatDelimiters (_,k,p) ->
pr_delimiters k (pr_patt mt lsimplepatt p), 1
+ | CPatCast _ ->
+ assert false
in
let loc = cases_pattern_expr_loc p in
pr_with_comments loc
@@ -298,6 +306,7 @@ end) = struct
let begin_of_binder = function
LocalRawDef((loc,_),_) -> fst (Loc.unloc loc)
| LocalRawAssum((loc,_)::_,_,_) -> fst (Loc.unloc loc)
+ | LocalPattern(loc,_,_) -> fst (Loc.unloc loc)
| _ -> assert false
let begin_of_binders = function
@@ -346,6 +355,13 @@ end) = struct
| _ -> c, CHole (Loc.ghost, None, Misctypes.IntroAnonymous, None) in
surround (pr_lname na ++ pr_opt_type pr_c topt ++
str":=" ++ cut() ++ pr_c c)
+ | LocalPattern (loc,p,tyo) ->
+ let p = pr_patt lsimplepatt p in
+ match tyo with
+ | None ->
+ str "'" ++ p
+ | Some ty ->
+ str "'" ++ surround (p ++ spc () ++ str ":" ++ ws 1 ++ pr_c ty)
let pr_undelimited_binders sep pr_c =
prlist_with_sep sep (pr_binder_among_many pr_c)
@@ -354,13 +370,13 @@ end) = struct
let n = begin_of_binders bl in
match bl with
| [LocalRawAssum (nal,k,t)] ->
- pr_com_at n ++ kw() ++ pr_binder false pr_c (nal,k,t)
- | LocalRawAssum _ :: _ as bdl ->
- pr_com_at n ++ kw() ++ pr_undelimited_binders sep pr_c bdl
+ kw n ++ pr_binder false pr_c (nal,k,t)
+ | (LocalRawAssum _ | LocalPattern _) :: _ as bdl ->
+ kw n ++ pr_undelimited_binders sep pr_c bdl
| _ -> assert false
let pr_binders_gen pr_c sep is_open =
- if is_open then pr_delimited_binders mt sep pr_c
+ if is_open then pr_delimited_binders pr_com_at sep pr_c
else pr_undelimited_binders sep pr_c
let rec extract_prod_binders = function
@@ -369,6 +385,11 @@ end) = struct
if bl = [] then [], x else LocalRawDef (na,b) :: bl, c*)
| CProdN (loc,[],c) ->
extract_prod_binders c
+ | CProdN (loc,[[_,Name id],bk,t],
+ CCases (_,LetPatternStyle,None, [CRef (Ident (_,id'),None),None,None],[(_,[_,[p]],b)]))
+ when Id.equal id id' && not (Id.Set.mem id (Topconstr.free_vars_of_constr_expr b)) ->
+ let bl,c = extract_prod_binders b in
+ LocalPattern (loc,p,None) :: bl, c
| CProdN (loc,(nal,bk,t)::bl,c) ->
let bl,c = extract_prod_binders (CProdN(loc,bl,c)) in
LocalRawAssum (nal,bk,t) :: bl, c
@@ -380,6 +401,11 @@ end) = struct
if bl = [] then [], x else LocalRawDef (na,b) :: bl, c*)
| CLambdaN (loc,[],c) ->
extract_lam_binders c
+ | CLambdaN (loc,[[_,Name id],bk,t],
+ CCases (_,LetPatternStyle,None, [CRef (Ident (_,id'),None),None,None],[(_,[_,[p]],b)]))
+ when Id.equal id id' && not (Id.Set.mem id (Topconstr.free_vars_of_constr_expr b)) ->
+ let bl,c = extract_lam_binders b in
+ LocalPattern (loc,p,None) :: bl, c
| CLambdaN (loc,(nal,bk,t)::bl,c) ->
let bl,c = extract_lam_binders (CLambdaN(loc,bl,c)) in
LocalRawAssum (nal,bk,t) :: bl, c
@@ -430,6 +456,7 @@ end) = struct
let names_of_binder = function
| LocalRawAssum (nal,_,_) -> nal
| LocalRawDef (_,_) -> []
+ | LocalPattern _ -> assert false
in let ids = List.flatten (List.map names_of_binder bl) in
if List.length ids > 1 then
spc() ++ str "{" ++ keyword "struct" ++ spc () ++ pr_id id ++ str"}"
@@ -498,9 +525,9 @@ end) = struct
prlist_with_sep pr_semicolon
(fun (id, c) -> h 1 (pr_reference id ++ spc () ++ str":=" ++ pr ltop c)) l
- let pr_forall () = keyword "forall" ++ spc ()
+ let pr_forall n = keyword "forall" ++ pr_com_at n ++ spc ()
- let pr_fun () = keyword "fun" ++ spc ()
+ let pr_fun n = keyword "fun" ++ pr_com_at n ++ spc ()
let pr_fun_sep = spc () ++ str "=>"
@@ -772,6 +799,22 @@ end
let do_not_tag _ x = x
+let split_token tag s =
+ let len = String.length s in
+ let rec parse_string off i =
+ if Int.equal i len then
+ if Int.equal off i then mt () else tag (str (String.sub s off (i - off)))
+ else if s.[i] == ' ' then
+ if Int.equal off i then parse_space 1 (succ i)
+ else tag (str (String.sub s off (i - off))) ++ parse_space 1 (succ i)
+ else parse_string off (succ i)
+ and parse_space spc i =
+ if Int.equal i len then str (String.make spc ' ')
+ else if s.[i] == ' ' then parse_space (succ spc) (succ i)
+ else str (String.make spc ' ') ++ parse_string i (succ i)
+ in
+ parse_string 0 0
+
(** Instantiating Make with tagging functions that only add style
information. *)
include Make (struct
@@ -780,7 +823,7 @@ include Make (struct
let tag_evar = tag Tag.evar
let tag_type = tag Tag.univ
let tag_unparsing = function
- | UnpTerminal s -> tag Tag.notation
+ | UnpTerminal s -> fun _ -> split_token (fun pp -> tag Tag.notation pp) s
| _ -> do_not_tag ()
let tag_constr_expr = do_not_tag
let tag_path = tag Tag.path
diff --git a/printing/ppconstrsig.mli b/printing/ppconstrsig.mli
index a59fc6d67d..3de0d805c4 100644
--- a/printing/ppconstrsig.mli
+++ b/printing/ppconstrsig.mli
@@ -44,6 +44,7 @@ module type Pp = sig
val pr_qualid : qualid -> std_ppcmds
val pr_patvar : patvar -> std_ppcmds
+ val pr_glob_level : glob_level -> std_ppcmds
val pr_glob_sort : glob_sort -> std_ppcmds
val pr_guard_annot : (constr_expr -> std_ppcmds) ->
local_binder list ->
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index b6e4c8011c..1e618b59eb 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -9,7 +9,7 @@
open Pp
open Names
open Namegen
-open Errors
+open CErrors
open Util
open Constrexpr
open Tacexpr
@@ -151,7 +151,8 @@ module Make
exception ComplexRedFlag
let pr_short_red_flag pr r =
- if not r.rBeta || not r.rIota || not r.rZeta then raise ComplexRedFlag
+ if not r.rBeta || not r.rMatch || not r.rFix || not r.rCofix || not r.rZeta then
+ raise ComplexRedFlag
else if List.is_empty r.rConst then
if r.rDelta then mt () else raise ComplexRedFlag
else (if r.rDelta then str "-" else mt ()) ++
@@ -161,9 +162,12 @@ module Make
try pr_short_red_flag pr r
with complexRedFlags ->
(if r.rBeta then pr_arg str "beta" else mt ()) ++
- (if r.rIota then pr_arg str "iota" else mt ()) ++
- (if r.rZeta then pr_arg str "zeta" else mt ()) ++
- (if List.is_empty r.rConst then
+ (if r.rMatch && r.rFix && r.rCofix then pr_arg str "iota" else
+ (if r.rMatch then pr_arg str "match" else mt ()) ++
+ (if r.rFix then pr_arg str "fix" else mt ()) ++
+ (if r.rCofix then pr_arg str "cofix" else mt ())) ++
+ (if r.rZeta then pr_arg str "zeta" else mt ()) ++
+ (if List.is_empty r.rConst then
if r.rDelta then pr_arg str "delta"
else mt ()
else
@@ -180,7 +184,8 @@ module Make
| Simpl (f,o) -> keyword "simpl" ++ (pr_short_red_flag pr_ref f)
++ pr_opt (pr_with_occurrences (pr_union pr_ref pr_pattern)) o
| Cbv f ->
- if f.rBeta && f.rIota && f.rZeta && f.rDelta && List.is_empty f.rConst then
+ if f.rBeta && f.rMatch && f.rFix && f.rCofix &&
+ f.rZeta && f.rDelta && List.is_empty f.rConst then
keyword "compute"
else
hov 1 (keyword "cbv" ++ pr_red_flag pr_ref f)
@@ -368,20 +373,25 @@ module Make
in
str "<" ++ name ++ str ">" ++ args
+ let rec pr_user_symbol = function
+ | Extend.Ulist1 tkn -> "ne_" ^ pr_user_symbol tkn ^ "_list"
+ | Extend.Ulist1sep (tkn, _) -> "ne_" ^ pr_user_symbol tkn ^ "_list"
+ | Extend.Ulist0 tkn -> pr_user_symbol tkn ^ "_list"
+ | Extend.Ulist0sep (tkn, _) -> pr_user_symbol tkn ^ "_list"
+ | Extend.Uopt tkn -> pr_user_symbol tkn ^ "_opt"
+ | Extend.Uentry tag ->
+ let ArgT.Any tag = tag in
+ ArgT.repr tag
+ | Extend.Uentryl (tkn, lvl) -> "tactic" ^ string_of_int lvl
+
let pr_alias_key key =
try
let prods = (KNmap.find key !prnotation_tab).pptac_prods in
- (* First printing strategy: only the head symbol *)
- match prods with
- | TacTerm s :: prods -> str s
- | _ ->
- (* Second printing strategy; if ever Tactic Notation is eventually *)
- (* accepting notations not starting with an identifier *)
let rec pr = function
- | [] -> []
- | TacTerm s :: prods -> s :: pr prods
- | TacNonTerm (_,_,id) :: prods -> ".." :: pr prods in
- str (String.concat " " (pr prods))
+ | TacTerm s -> primitive s
+ | TacNonTerm (_, symb, _) -> str (Printf.sprintf "(%s)" (pr_user_symbol symb))
+ in
+ pr_sequence pr prods
with Not_found ->
KerName.print key
@@ -573,13 +583,13 @@ module Make
| None -> mt()
let pr_hyp_location pr_id = function
- | occs, InHyp -> spc () ++ pr_with_occurrences pr_id occs
+ | occs, InHyp -> pr_with_occurrences pr_id occs
| occs, InHypTypeOnly ->
- spc () ++ pr_with_occurrences (fun id ->
+ pr_with_occurrences (fun id ->
str "(" ++ keyword "type of" ++ spc () ++ pr_id id ++ str ")"
) occs
| occs, InHypValueOnly ->
- spc () ++ pr_with_occurrences (fun id ->
+ pr_with_occurrences (fun id ->
str "(" ++ keyword "value of" ++ spc () ++ pr_id id ++ str ")"
) occs
@@ -593,6 +603,17 @@ module Make
| None -> mt ()
| Some (id,ipat) -> pr_in (spc () ++ pr_id id) ++ pr_as_ipat prc ipat
+ let pr_in_clause pr_id = function
+ | { onhyps=None; concl_occs=NoOccurrences } ->
+ (str "* |-")
+ | { onhyps=None; concl_occs=occs } ->
+ (pr_with_occurrences (fun () -> str "*") (occs,()))
+ | { onhyps=Some l; concl_occs=NoOccurrences } ->
+ prlist_with_sep (fun () -> str ", ") (pr_hyp_location pr_id) l
+ | { onhyps=Some l; concl_occs=occs } ->
+ let pr_occs = pr_with_occurrences (fun () -> str" |- *") (occs,()) in
+ (prlist_with_sep (fun () -> str", ") (pr_hyp_location pr_id) l ++ pr_occs)
+
let pr_clauses default_is_concl pr_id = function
| { onhyps=Some []; concl_occs=occs }
when (match default_is_concl with Some true -> true | _ -> false) ->
@@ -609,7 +630,7 @@ module Make
| _ -> pr_with_occurrences (fun () -> str" |- *") (occs,())
in
pr_in
- (prlist_with_sep (fun () -> str",") (pr_hyp_location pr_id) l ++ pr_occs)
+ (prlist_with_sep (fun () -> str", ") (pr_hyp_location pr_id) l ++ pr_occs)
let pr_orient b = if b then mt () else str "<- "
@@ -792,7 +813,7 @@ module Make
let pr_with_bindings_arg = pr_with_bindings_arg pr.pr_constr pr.pr_lconstr in
let pr_red_expr = pr_red_expr (pr.pr_constr,pr.pr_lconstr,pr.pr_constant,pr.pr_pattern) in
- let pr_constrarg c = spc () ++ pr.pr_constr c in
+ let _pr_constrarg c = spc () ++ pr.pr_constr c in
let pr_lconstrarg c = spc () ++ pr.pr_lconstr c in
let pr_intarg n = spc () ++ int n in
@@ -840,7 +861,7 @@ module Make
prlist pr_binder_fix bll ++ annot ++ str" :" ++
pr_lconstrarg ty ++ str")") in
(* spc() ++
- hov 0 (pr_id id ++ pr_intarg n ++ str":" ++ pr_constrarg
+ hov 0 (pr_id id ++ pr_intarg n ++ str":" ++ _pr_constrarg
c)
*)
let pr_cofix_tac (id,c) =
diff --git a/printing/pptacticsig.mli b/printing/pptacticsig.mli
index c08d6044db..665e055f23 100644
--- a/printing/pptacticsig.mli
+++ b/printing/pptacticsig.mli
@@ -29,6 +29,9 @@ module type Pp = sig
val pr_and_short_name : ('a -> std_ppcmds) -> 'a and_short_name -> std_ppcmds
val pr_or_by_notation : ('a -> std_ppcmds) -> 'a or_by_notation -> std_ppcmds
+ val pr_in_clause :
+ ('a -> Pp.std_ppcmds) -> 'a Locus.clause_expr -> Pp.std_ppcmds
+
val pr_clauses : bool option ->
('a -> Pp.std_ppcmds) -> 'a Locus.clause_expr -> Pp.std_ppcmds
diff --git a/printing/pputils.ml b/printing/pputils.ml
index 906b463a85..50ce56fb02 100644
--- a/printing/pputils.ml
+++ b/printing/pputils.ml
@@ -9,7 +9,11 @@
open Pp
let pr_located pr (loc, x) =
- if Flags.do_beautify () && loc <> Loc.ghost then
+ if !Flags.beautify && loc <> Loc.ghost then
let (b, e) = Loc.unloc loc in
- Pp.comment b ++ pr x ++ Pp.comment e
+ (* Side-effect: order matters *)
+ let before = Pp.comment (CLexer.extract_comments b) in
+ let x = pr x in
+ let after = Pp.comment (CLexer.extract_comments e) in
+ before ++ x ++ after
else pr x
diff --git a/printing/ppvernac.ml b/printing/ppvernac.ml
index 5b73b054dd..3494ad006f 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -9,7 +9,7 @@
open Pp
open Names
-open Errors
+open CErrors
open Util
open Extend
open Vernacexpr
@@ -166,14 +166,17 @@ module Make
| ModeNoHeadEvar -> str"!"
| ModeOutput -> str"-"
+ let pr_hint_info pr_pat { hint_priority = pri; hint_pattern = pat } =
+ pr_opt (fun x -> str"|" ++ int x) pri ++
+ pr_opt (fun y -> (if Option.is_empty pri then str"| " else mt()) ++ pr_pat y) pat
+
let pr_hints db h pr_c pr_pat =
let opth = pr_opt_hintbases db in
let pph =
match h with
| HintsResolve l ->
keyword "Resolve " ++ prlist_with_sep sep
- (fun (pri, _, c) -> pr_reference_or_constr pr_c c ++
- match pri with Some x -> spc () ++ str"(" ++ int x ++ str")" | None -> mt ())
+ (fun (info, _, c) -> pr_reference_or_constr pr_c c ++ pr_hint_info pr_pat info)
l
| HintsImmediate l ->
keyword "Immediate" ++ spc() ++
@@ -263,7 +266,7 @@ module Make
let pr_decl_notation prc ((loc,ntn),c,scopt) =
fnl () ++ keyword "where " ++ qs ntn ++ str " := "
- ++ Flags.without_option Flags.beautify_file prc c ++
+ ++ Flags.without_option Flags.beautify prc c ++
pr_opt (fun sc -> str ": " ++ str sc) scopt
let pr_binders_arg =
@@ -367,8 +370,8 @@ module Make
| SetAssoc NonA -> keyword "no associativity"
| SetEntryType (x,typ) -> str x ++ spc() ++ pr_set_entry_type typ
| SetOnlyPrinting -> keyword "only printing"
- | SetOnlyParsing Flags.Current -> keyword "only parsing"
- | SetOnlyParsing v -> keyword("compat \"" ^ Flags.pr_version v ^ "\"")
+ | SetOnlyParsing -> keyword "only parsing"
+ | SetCompatVersion v -> keyword("compat \"" ^ Flags.pr_version v ^ "\"")
| SetFormat("text",s) -> keyword "format " ++ pr_located qs s
| SetFormat(k,s) -> keyword "format " ++ qs k ++ spc() ++ pr_located qs s
@@ -383,7 +386,7 @@ module Make
| Some pl -> str"@{" ++ prlist_with_sep spc pr_lident pl ++ str"}"
let pr_rec_definition ((((loc,id),pl),ro,bl,type_,def),ntn) =
- let pr_pure_lconstr c = Flags.without_option Flags.beautify_file pr_lconstr c in
+ let pr_pure_lconstr c = Flags.without_option Flags.beautify pr_lconstr c in
let annot = pr_guard_annot pr_lconstr_expr bl ro in
pr_id id ++ pr_univs pl ++ pr_binders_arg bl ++ annot
++ pr_type_option (fun c -> spc() ++ pr_lconstr_expr c) type_
@@ -591,7 +594,7 @@ module Make
| ShowTree -> keyword "Show Tree"
| ShowProofNames -> keyword "Show Conjectures"
| ShowIntros b -> keyword "Show " ++ (if b then keyword "Intros" else keyword "Intro")
- | ShowMatch id -> keyword "Show Match " ++ pr_lident id
+ | ShowMatch id -> keyword "Show Match " ++ pr_reference id
| ShowThesis -> keyword "Show Thesis"
in
return (pr_showable s)
@@ -678,7 +681,7 @@ module Make
| VernacNotation (_,c,((_,s),l),opt) ->
return (
hov 2 (keyword "Notation" ++ spc() ++ qs s ++
- str " :=" ++ Flags.without_option Flags.beautify_file pr_constrarg c ++ pr_syntax_modifiers l ++
+ str " :=" ++ Flags.without_option Flags.beautify pr_constrarg c ++ pr_syntax_modifiers l ++
(match opt with
| None -> mt()
| Some sc -> str" :" ++ spc() ++ str sc))
@@ -760,7 +763,7 @@ module Make
let pr_constructor (coe,(id,c)) =
hov 2 (pr_lident id ++ str" " ++
(if coe then str":>" else str":") ++
- Flags.without_option Flags.beautify_file pr_spc_lconstr c)
+ Flags.without_option Flags.beautify pr_spc_lconstr c)
in
let pr_constructor_list b l = match l with
| Constructors [] -> mt()
@@ -838,7 +841,8 @@ module Make
)
| VernacConstraint v ->
let pr_uconstraint (l, d, r) =
- pr_lident l ++ spc () ++ Univ.pr_constraint_type d ++ spc () ++ pr_lident r
+ pr_glob_level l ++ spc () ++ Univ.pr_constraint_type d ++ spc () ++
+ pr_glob_level r
in
return (
hov 2 (keyword "Constraint" ++ spc () ++
@@ -887,7 +891,7 @@ module Make
spc() ++ pr_class_rawexpr c2)
)
- | VernacInstance (abst, sup, (instid, bk, cl), props, pri) ->
+ | VernacInstance (abst, sup, (instid, bk, cl), props, info) ->
return (
hov 1 (
(if abst then keyword "Declare" ++ spc () else mt ()) ++
@@ -898,7 +902,7 @@ module Make
pr_and_type_binders_arg sup ++
str":" ++ spc () ++
(match bk with Implicit -> str "! " | Explicit -> mt ()) ++
- pr_constr cl ++ pr_priority pri ++
+ pr_constr cl ++ pr_hint_info pr_constr_pattern_expr info ++
(match props with
| Some (true,CRecord (_,l)) -> spc () ++ str":=" ++ spc () ++ str"{" ++ pr_record_body l ++ str "}"
| Some (true,_) -> assert false
@@ -912,11 +916,14 @@ module Make
keyword "Context" ++ spc () ++ pr_and_type_binders_arg l)
)
- | VernacDeclareInstances (ids, pri) ->
- return (
+ | VernacDeclareInstances insts ->
+ let pr_inst (id, info) =
+ pr_reference id ++ pr_hint_info pr_constr_pattern_expr info
+ in
+ return (
hov 1 (keyword "Existing" ++ spc () ++
- keyword(String.plural (List.length ids) "Instance") ++
- spc () ++ prlist_with_sep spc pr_reference ids ++ pr_priority pri)
+ keyword(String.plural (List.length insts) "Instance") ++
+ spc () ++ prlist_with_sep (fun () -> str", ") pr_inst insts)
)
| VernacDeclareClass id ->
@@ -1002,13 +1009,13 @@ module Make
)
| VernacHints (_, dbnames,h) ->
return (pr_hints dbnames h pr_constr pr_constr_pattern_expr)
- | VernacSyntacticDefinition (id,(ids,c),_,onlyparsing) ->
+ | VernacSyntacticDefinition (id,(ids,c),_,compat) ->
return (
hov 2
(keyword "Notation" ++ spc () ++ pr_lident id ++ spc () ++
prlist_with_sep spc pr_id ids ++ str":=" ++ pr_constrarg c ++
pr_syntax_modifiers
- (match onlyparsing with None -> [] | Some v -> [SetOnlyParsing v]))
+ (match compat with None -> [] | Some v -> [SetCompatVersion v]))
)
| VernacDeclareImplicits (q,[]) ->
return (
@@ -1022,25 +1029,36 @@ module Make
str"[" ++ prlist_with_sep sep pr_explanation imps ++ str"]")
impls)
)
- | VernacArguments (q, impl, nargs, mods) ->
+ | VernacArguments (q, args, more_implicits, nargs, mods) ->
return (
hov 2 (
keyword "Arguments" ++ spc() ++
pr_smart_global q ++
let pr_s = function None -> str"" | Some (_,s) -> str "%" ++ str s in
let pr_if b x = if b then x else str "" in
- let pr_br imp max x = match imp, max with
- | true, false -> str "[" ++ x ++ str "]"
- | true, true -> str "{" ++ x ++ str "}"
- | _ -> x in
- let rec aux n l =
+ let pr_br imp x = match imp with
+ | Vernacexpr.Implicit -> str "[" ++ x ++ str "]"
+ | Vernacexpr.MaximallyImplicit -> str "{" ++ x ++ str "}"
+ | Vernacexpr.NotImplicit -> x in
+ let rec print_arguments n l =
match n, l with
- | 0, l -> spc () ++ str"/" ++ aux ~-1 l
+ | Some 0, l -> spc () ++ str"/" ++ print_arguments None l
| _, [] -> mt()
- | n, (id,k,s,imp,max) :: tl ->
- spc() ++ pr_br imp max (pr_if k (str"!") ++ pr_name id ++ pr_s s) ++
- aux (n-1) tl in
- prlist_with_sep (fun () -> str", ") (aux nargs) impl ++
+ | n, { name = id; recarg_like = k;
+ notation_scope = s;
+ implicit_status = imp } :: tl ->
+ spc() ++ pr_br imp (pr_if k (str"!") ++ pr_name id ++ pr_s s) ++
+ print_arguments (Option.map pred n) tl
+ in
+ let rec print_implicits = function
+ | [] -> mt ()
+ | (name, impl) :: rest ->
+ spc() ++ pr_br impl (pr_name name) ++ print_implicits rest
+ in
+ print_arguments nargs args ++
+ if not (List.is_empty more_implicits) then
+ str ", " ++ prlist_with_sep (fun () -> str", ") print_implicits more_implicits
+ else (mt ()) ++
(if not (List.is_empty mods) then str" : " else str"") ++
prlist_with_sep (fun () -> str", " ++ spc()) (function
| `ReductionDontExposeCase -> keyword "simpl nomatch"
@@ -1082,7 +1100,7 @@ module Make
)
| VernacSetOpacity _ ->
return (
- Errors.anomaly (keyword "VernacSetOpacity used to set something else")
+ CErrors.anomaly (keyword "VernacSetOpacity used to set something else")
)
| VernacSetStrategy l ->
let pr_lev = function
@@ -1107,6 +1125,11 @@ module Make
return (
hov 2 (keyword "Set" ++ spc() ++ pr_set_option na v)
)
+ | VernacSetAppendOption (na,v) ->
+ return (
+ hov 2 (keyword "Set" ++ spc() ++ pr_printoption na None ++
+ spc() ++ keyword "Append" ++ spc() ++ str v)
+ )
| VernacAddOption (na,l) ->
return (
hov 2 (keyword "Add" ++ spc() ++ pr_printoption na (Some l))
@@ -1219,7 +1242,7 @@ module Make
let pr_vernac v =
try pr_vernac_body v ++ sep_end v
- with e -> Errors.print e
+ with e -> CErrors.print e
end
diff --git a/printing/prettyp.ml b/printing/prettyp.ml
index ad67becd01..e117f1dcb0 100644
--- a/printing/prettyp.ml
+++ b/printing/prettyp.ml
@@ -11,7 +11,7 @@
*)
open Pp
-open Errors
+open CErrors
open Util
open Names
open Nameops
@@ -224,12 +224,12 @@ let print_type_in_type ref =
let print_primitive_record recflag mipv = function
| Some (Some (_, ps,_)) ->
let eta = match recflag with
- | Decl_kinds.CoFinite | Decl_kinds.Finite -> mt ()
- | Decl_kinds.BiFinite -> str " and has eta conversion"
+ | Decl_kinds.CoFinite | Decl_kinds.Finite -> str" without eta conversion"
+ | Decl_kinds.BiFinite -> str " with eta conversion"
in
- [pr_id mipv.(0).mind_typename ++ str" is primitive" ++ eta ++ str"."]
+ [pr_id mipv.(0).mind_typename ++ str" has primitive projections" ++ eta ++ str"."]
| _ -> []
-
+
let print_primitive ref =
match ref with
| IndRef ind ->
@@ -241,7 +241,7 @@ let print_name_infos ref =
let impls = implicits_of_global ref in
let scopes = Notation.find_arguments_scope ref in
let renames =
- try List.hd (Arguments_renaming.arguments_names ref) with Not_found -> [] in
+ try Arguments_renaming.arguments_names ref with Not_found -> [] in
let type_info_for_implicit =
if need_expansion (select_impargs_size 0 impls) ref then
(* Need to reduce since implicits are computed with products flattened *)
@@ -281,7 +281,7 @@ let print_inductive_implicit_args =
let print_inductive_renames =
print_args_data_of_inductive_ids
(fun r ->
- try List.hd (Arguments_renaming.arguments_names r) with Not_found -> [])
+ try Arguments_renaming.arguments_names r with Not_found -> [])
((!=) Anonymous)
print_renames_list
@@ -872,7 +872,7 @@ let pr_instance env i =
(* gallina_print_constant_with_infos i.is_impl *)
(* lighter *)
print_ref false (instance_impl i) ++
- begin match instance_priority i with
+ begin match hint_priority i with
| None -> mt ()
| Some i -> spc () ++ str "|" ++ spc () ++ int i
end
diff --git a/printing/printer.ml b/printing/printer.ml
index 8af2af98a5..04337f6be8 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -7,7 +7,7 @@
(************************************************************************)
open Pp
-open Errors
+open CErrors
open Util
open Names
open Term
@@ -184,7 +184,7 @@ let safe_gen f env sigma c =
let orig_extern_ref = Constrextern.get_extern_reference () in
let extern_ref loc vars r =
try orig_extern_ref loc vars r
- with e when Errors.noncritical e ->
+ with e when CErrors.noncritical e ->
Libnames.Qualid (loc, qualid_of_global env r)
in
Constrextern.set_extern_reference extern_ref;
@@ -192,7 +192,7 @@ let safe_gen f env sigma c =
let p = f env sigma c in
Constrextern.set_extern_reference orig_extern_ref;
p
- with e when Errors.noncritical e ->
+ with e when CErrors.noncritical e ->
Constrextern.set_extern_reference orig_extern_ref;
str "??"
@@ -424,7 +424,16 @@ let pr_evgl_sign sigma evi =
(str "(" ++ prlist_with_sep pr_comma pr_id ids ++ str " cannot be used)")
in
let pc = pr_lconstr_env env sigma evi.evar_concl in
- hov 0 (str"[" ++ ps ++ spc () ++ str"|- " ++ pc ++ str"]" ++ spc () ++ warn)
+ let candidates =
+ match evi.evar_body, evi.evar_candidates with
+ | Evar_empty, Some l ->
+ spc () ++ str "= {" ++
+ prlist_with_sep (fun () -> str "|") (pr_lconstr_env env sigma) l ++ str "}"
+ | _ ->
+ mt ()
+ in
+ hov 0 (str"[" ++ ps ++ spc () ++ str"|- " ++ pc ++ str"]" ++
+ candidates ++ spc () ++ warn)
(* Print an existential variable *)
@@ -471,7 +480,7 @@ let default_pr_subgoal n sigma =
let pr_internal_existential_key ev = str (string_of_existential ev)
-let print_evar_constraints gl sigma cstrs =
+let print_evar_constraints gl sigma =
let pr_env =
match gl with
| None -> fun e' -> pr_context_of e' sigma
@@ -487,6 +496,14 @@ let print_evar_constraints gl sigma cstrs =
let pr_evconstr (pbty,env,t1,t2) =
let t1 = Evarutil.nf_evar sigma t1
and t2 = Evarutil.nf_evar sigma t2 in
+ let env =
+ (** We currently allow evar instances to refer to anonymous de Bruijn
+ indices, so we protect the error printing code in this case by giving
+ names to every de Bruijn variable in the rel_context of the conversion
+ problem. MS: we should rather stop depending on anonymous variables, they
+ can be used to indicate independency. Also, this depends on a strategy for
+ naming/renaming *)
+ Namegen.make_all_name_different env in
str" " ++
hov 2 (pr_env env ++ pr_lconstr_env env sigma t1 ++ spc () ++
str (match pbty with
@@ -494,31 +511,58 @@ let print_evar_constraints gl sigma cstrs =
| Reduction.CUMUL -> "<=") ++
spc () ++ pr_lconstr_env env sigma t2)
in
- prlist_with_sep fnl pr_evconstr cstrs
-
-let print_dependent_evars gl sigma seeds =
+ let pr_candidate ev evi (candidates,acc) =
+ if Option.has_some evi.evar_candidates then
+ (succ candidates, acc ++ pr_evar sigma (ev,evi) ++ fnl ())
+ else (candidates, acc)
+ in
let constraints =
let _, cstrs = Evd.extract_all_conv_pbs sigma in
if List.is_empty cstrs then mt ()
else fnl () ++ str (String.plural (List.length cstrs) "unification constraint")
- ++ str":" ++ fnl () ++ hov 0 (print_evar_constraints gl sigma cstrs)
+ ++ str":" ++ fnl () ++ hov 0 (prlist_with_sep fnl pr_evconstr cstrs)
in
+ let candidates, ppcandidates = Evd.fold_undefined pr_candidate sigma (0,mt ()) in
+ constraints ++
+ if candidates > 0 then
+ fnl () ++ str (String.plural candidates "existential") ++
+ str" with candidates:" ++ fnl () ++ hov 0 ppcandidates
+ else mt ()
+
+let should_print_dependent_evars = ref false
+
+let _ =
+ let open Goptions in
+ declare_bool_option
+ { optsync = true;
+ optdepr = false;
+ optname = "Printing Dependent Evars Line";
+ optkey = ["Printing";"Dependent";"Evars";"Line"];
+ optread = (fun () -> !should_print_dependent_evars);
+ optwrite = (fun v -> should_print_dependent_evars := v) }
+
+let print_dependent_evars gl sigma seeds =
+ let constraints = print_evar_constraints gl sigma in
let evars () =
- let evars = Evarutil.gather_dependent_evars sigma seeds in
- let evars =
- Evar.Map.fold begin fun e i s ->
- let e' = pr_internal_existential_key e in
- match i with
- | None -> s ++ str" " ++ e' ++ str " open,"
- | Some i ->
- s ++ str " " ++ e' ++ str " using " ++
- Evar.Set.fold begin fun d s ->
- pr_internal_existential_key d ++ str " " ++ s
- end i (str ",")
- end evars (str "")
+ if !should_print_dependent_evars then
+ let evars = Evarutil.gather_dependent_evars sigma seeds in
+ let evars =
+ Evar.Map.fold begin fun e i s ->
+ let e' = pr_internal_existential_key e in
+ match i with
+ | None -> s ++ str" " ++ e' ++ str " open,"
+ | Some i ->
+ s ++ str " " ++ e' ++ str " using " ++
+ Evar.Set.fold begin fun d s ->
+ pr_internal_existential_key d ++ str " " ++ s
+ end i (str ",")
+ end evars (str "")
in
fnl () ++
str "(dependent evars:" ++ evars ++ str ")" ++ fnl ()
+ else
+ fnl () ++
+ str "(dependent evars: (printing disabled) )" ++ fnl ()
in
constraints ++ delayed_emacs_cmd evars
@@ -717,9 +761,6 @@ let pr_prim_rule = function
str(if Termops.occur_meta c then "refine " else "exact ") ++
Constrextern.with_meta_as_hole pr_constr c
- | Move (id1,id2) ->
- (str"move " ++ pr_id id1 ++ Miscprint.pr_move_location pr_id id2)
-
(* Backwards compatibility *)
let prterm = pr_lconstr
@@ -786,13 +827,13 @@ let pr_assumptionset env s =
in
let safe_pr_ltype typ =
try str " : " ++ pr_ltype typ
- with e when Errors.noncritical e -> mt ()
+ with e when CErrors.noncritical e -> mt ()
in
let safe_pr_ltype_relctx (rctx, typ) =
let sigma, env = get_current_context () in
let env = Environ.push_rel_context rctx env in
try str " " ++ pr_ltype_env env sigma typ
- with e when Errors.noncritical e -> mt ()
+ with e when CErrors.noncritical e -> mt ()
in
let pr_axiom env ax typ =
match ax with
@@ -869,4 +910,3 @@ let pr_polymorphic b =
let pr_universe_instance evd ctx =
let inst = Univ.UContext.instance ctx in
str"@{" ++ Univ.Instance.pr (Evd.pr_evd_level evd) inst ++ str"}"
-
diff --git a/printing/printmod.ml b/printing/printmod.ml
index 5f98eeeab9..dfa66d4376 100644
--- a/printing/printmod.ml
+++ b/printing/printmod.ml
@@ -247,19 +247,24 @@ let get_typ_expr_alg mtb = match mtb.mod_type_alg with
| _ -> raise Not_found
let nametab_register_modparam mbid mtb =
+ let id = MBId.to_id mbid in
match mtb.mod_type with
- | MoreFunctor _ -> () (* functorial param : nothing to register *)
+ | MoreFunctor _ -> id (* functorial param : nothing to register *)
| NoFunctor struc ->
(* We first try to use the algebraic type expression if any,
via a Declaremods function that converts back to module entries *)
try
- Declaremods.process_module_binding mbid (get_typ_expr_alg mtb)
- with e when Errors.noncritical e ->
+ let () = Declaremods.process_module_binding mbid (get_typ_expr_alg mtb) in
+ id
+ with e when CErrors.noncritical e ->
(* Otherwise, we try to play with the nametab ourselves *)
let mp = MPbound mbid in
- let dir = DirPath.make [MBId.to_id mbid] in
+ let check id = Nametab.exists_dir (DirPath.make [id]) in
+ let id = Namegen.next_ident_away_from id check in
+ let dir = DirPath.make [id] in
nametab_register_dir mp;
- List.iter (nametab_register_body mp dir) struc
+ List.iter (nametab_register_body mp dir) struc;
+ id
let print_body is_impl env mp (l,body) =
let name = pr_label l in
@@ -295,7 +300,7 @@ let print_body is_impl env mp (l,body) =
try
let env = Option.get env in
pr_mutual_inductive_body env (MutInd.make2 mp l) mib
- with e when Errors.noncritical e ->
+ with e when CErrors.noncritical e ->
let keyword =
let open Decl_kinds in
match mib.mind_finite with
@@ -353,7 +358,7 @@ let print_mod_expr env mp locals = function
let rec print_functor fty fatom is_type env mp locals = function
|NoFunctor me -> fatom is_type env mp locals me
|MoreFunctor (mbid,mtb1,me2) ->
- nametab_register_modparam mbid mtb1;
+ let id = nametab_register_modparam mbid mtb1 in
let mp1 = MPbound mbid in
let pr_mtb1 = fty env mp1 locals mtb1 in
let env' = Option.map (Modops.add_module_type mp1 mtb1) env in
@@ -361,7 +366,7 @@ let rec print_functor fty fatom is_type env mp locals = function
let kwd = if is_type then "Funsig" else "Functor" in
hov 2
(keyword kwd ++ spc () ++
- str "(" ++ pr_id (MBId.to_id mbid) ++ str ":" ++ pr_mtb1 ++ str ")" ++
+ str "(" ++ pr_id id ++ str ":" ++ pr_mtb1 ++ str ")" ++
spc() ++ print_functor fty fatom is_type env' mp locals' me2)
let rec print_expression x =
@@ -422,7 +427,7 @@ let print_module with_body mp =
try
if !short then raise ShortPrinting;
unsafe_print_module (Some (Global.env ())) mp with_body me ++ fnl ()
- with e when Errors.noncritical e ->
+ with e when CErrors.noncritical e ->
unsafe_print_module None mp with_body me ++ fnl ()
let print_modtype kn =
@@ -433,7 +438,7 @@ let print_modtype kn =
(try
if !short then raise ShortPrinting;
print_signature' true (Some (Global.env ())) kn mtb.mod_type
- with e when Errors.noncritical e ->
+ with e when CErrors.noncritical e ->
print_signature' true None kn mtb.mod_type))
end
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 15:04:56 +0000