aboutsummaryrefslogtreecommitdiff
path: root/printing
diff options
context:
space:
mode:
Diffstat (limited to 'printing')
-rw-r--r--printing/ppconstr.ml18
-rw-r--r--printing/ppconstrsig.mli1
-rw-r--r--printing/pptactic.ml19
-rw-r--r--printing/pptacticsig.mli3
-rw-r--r--printing/pputils.ml8
-rw-r--r--printing/ppvernac.ml38
-rw-r--r--printing/printer.ml46
-rw-r--r--printing/printmod.ml17
8 files changed, 108 insertions, 42 deletions
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index a00e4bab30..aa94fb7be3 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -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
@@ -364,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)
+ kw n ++ pr_binder false pr_c (nal,k,t)
| (LocalRawAssum _ | LocalPattern _) :: _ as bdl ->
- pr_com_at n ++ kw() ++ pr_undelimited_binders sep pr_c 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
@@ -519,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 "=>"
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 f3117db170..1e618b59eb 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -583,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
@@ -603,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) ->
@@ -619,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 "<- "
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 40ce28dc0c..cfb4e79f03 100644
--- a/printing/ppvernac.ml
+++ b/printing/ppvernac.ml
@@ -263,7 +263,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 +367,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 +383,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_
@@ -678,7 +678,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 +760,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 +838,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 () ++
@@ -1002,13 +1003,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 (
@@ -1029,16 +1030,18 @@ module Make
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 pr_br imp x = match imp with
+ | `Implicit -> str "[" ++ x ++ str "]"
+ | `MaximallyImplicit -> str "{" ++ x ++ str "}"
+ | `NotImplicit -> x in
let rec aux n l =
match n, l with
| 0, l -> spc () ++ str"/" ++ aux ~-1 l
| _, [] -> mt()
- | n, (id,k,s,imp,max) :: tl ->
- spc() ++ pr_br imp max (pr_if k (str"!") ++ pr_name id ++ pr_s s) ++
+ | 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) ++
aux (n-1) tl in
prlist_with_sep (fun () -> str", ") (aux nargs) impl ++
(if not (List.is_empty mods) then str" : " else str"") ++
@@ -1107,6 +1110,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))
diff --git a/printing/printer.ml b/printing/printer.ml
index 6d54a5b3d5..608bca62ac 100644
--- a/printing/printer.ml
+++ b/printing/printer.ml
@@ -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,7 +511,23 @@ 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 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 (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 true
@@ -509,12 +542,7 @@ let _ =
optwrite = (fun v -> should_print_dependent_evars := v) }
let print_dependent_evars gl sigma seeds =
- 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)
- in
+ let constraints = print_evar_constraints gl sigma in
let evars () =
if !should_print_dependent_evars then
let evars = Evarutil.gather_dependent_evars sigma seeds in
diff --git a/printing/printmod.ml b/printing/printmod.ml
index c939f54e80..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)
+ 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
@@ -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 =
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 20:45:15 +0000