aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--doc/refman/RefMan-ext.tex8
-rw-r--r--kernel/univ.ml154
-rw-r--r--kernel/univ.mli2
-rw-r--r--parsing/g_vernac.ml43
-rw-r--r--parsing/ppvernac.ml2
-rw-r--r--test-suite/success/PrintSortedUniverses.v2
-rw-r--r--toplevel/vernacentries.ml16
-rw-r--r--toplevel/vernacexpr.ml2
8 files changed, 180 insertions, 9 deletions
diff --git a/doc/refman/RefMan-ext.tex b/doc/refman/RefMan-ext.tex
index 7a56426c4..942530c3b 100644
--- a/doc/refman/RefMan-ext.tex
+++ b/doc/refman/RefMan-ext.tex
@@ -1750,16 +1750,20 @@ of the occurrences of {\Type}, use
\end{quote}
\comindex{Print Universes}
+\comindex{Print Sorted Universes}
The constraints on the internal level of the occurrences of {\Type}
(see Section~\ref{Sorts}) can be printed using the command
\begin{quote}
-{\tt Print Universes.}
+{\tt Print [Sorted] Universes.}
\end{quote}
+If the optional {\tt Sorted} option is given, each universe will be
+made equivalent to a numbered label reflecting its level (with a
+linear ordering) in the universe hierarchy.
This command also accepts an optional output filename:
\begin{quote}
-\tt Print Universes {\str}.
+\tt Print [Sorted] Universes {\str}.
\end{quote}
If {\str} ends in \texttt{.dot} or \texttt{.gv}, the constraints are
printed in the DOT language, and can be processed by Graphviz
diff --git a/kernel/univ.ml b/kernel/univ.ml
index db5b07131..227fe0417 100644
--- a/kernel/univ.ml
+++ b/kernel/univ.ml
@@ -494,6 +494,160 @@ let enforce_eq u v c =
let merge_constraints c g =
Constraint.fold enforce_constraint c g
+(* Normalization *)
+
+module UniverseLSet =
+ Set.Make (struct type t = universe_level let compare = cmp_univ_level end)
+
+let lookup_level u g =
+ try Some (UniverseLMap.find u g) with Not_found -> None
+
+(** [normalize_universes g] returns a graph where all edges point
+ directly to the canonical representent of their target. The output
+ graph should be equivalent to the input graph from a logical point
+ of view, but optimized. We maintain the invariant that the key of
+ a [Canonical] element is its own name, by keeping [Equiv] edges
+ (see the assertion)... I (Stéphane Glondu) am not sure if this
+ plays a role in the rest of the module. *)
+let normalize_universes g =
+ let rec visit u arc cache = match lookup_level u cache with
+ | Some x -> x, cache
+ | None -> match Lazy.force arc with
+ | None ->
+ u, UniverseLMap.add u u cache
+ | Some (Canonical {univ=v; lt=_; le=_}) ->
+ v, UniverseLMap.add u v cache
+ | Some (Equiv v) ->
+ let v, cache = visit v (lazy (lookup_level v g)) cache in
+ v, UniverseLMap.add u v cache
+ in
+ let cache = UniverseLMap.fold
+ (fun u arc cache -> snd (visit u (Lazy.lazy_from_val (Some arc)) cache))
+ g UniverseLMap.empty
+ in
+ let repr x = UniverseLMap.find x cache in
+ let lrepr us = List.fold_left
+ (fun e x -> UniverseLSet.add (repr x) e) UniverseLSet.empty us
+ in
+ let canonicalize u = function
+ | Equiv _ -> Equiv (repr u)
+ | Canonical {univ=v; lt=lt; le=le} ->
+ assert (u == v);
+ (* avoid duplicates and self-loops *)
+ let lt = lrepr lt and le = lrepr le in
+ let le = UniverseLSet.filter
+ (fun x -> x != u && not (UniverseLSet.mem x lt)) le
+ in
+ UniverseLSet.iter (fun x -> assert (x != u)) lt;
+ Canonical {
+ univ = v;
+ lt = UniverseLSet.elements lt;
+ le = UniverseLSet.elements le;
+ }
+ in
+ UniverseLMap.mapi canonicalize g
+
+(** [check_sorted g sorted]: [g] being a universe graph, [sorted]
+ being a map to [Equiv Type.n] (with [n] being a natural number),
+ checks that all constraints in [g] are satisfied in [sorted]. *)
+let check_sorted g sorted =
+ let get u = match UniverseLMap.find u sorted with
+ | Equiv x -> x
+ | Canonical _ -> assert false
+ in
+ UniverseLMap.iter (fun u arc -> let repr_u = get u in match arc with
+ | Equiv v -> assert (get v == repr_u)
+ | Canonical {univ=u'; lt=lt; le=le} ->
+ assert (u == u');
+ List.iter (fun v -> assert (cmp_univ_level repr_u (get v) <= 0)) le;
+ List.iter (fun v -> assert (cmp_univ_level repr_u (get v) < 0)) lt) g
+
+(** [sort_universes g] builds a map from universes in [g] to natural
+ numbers. It outputs a graph containing equivalence edges from each
+ level appearing in [g] to [Type.n], and [lt] edges between the
+ [Type.n]s. The output graph should imply the input graph (and the
+ implication will be strict most of the time), but is not
+ necessarily minimal. Note: the result is unspecified if the input
+ graph already contains [Type.n] nodes (calling a module Type is
+ probably a bad idea anyway). *)
+let sort_universes orig_g =
+ (* basically a topological sort with grouping, le and lt nodes are
+ treated the same way *)
+ let mp = Names.make_dirpath [Names.id_of_string "Type"] in
+ let g = normalize_universes orig_g in
+ let degs = (* map from canonical nodes to incoming degrees *)
+ UniverseLMap.fold
+ (fun u arc res -> match arc with
+ | Equiv _ -> res
+ | Canonical {univ=_; lt=lt; le=le} ->
+ let res =
+ try let _ = UniverseLMap.find u res in res
+ with Not_found -> UniverseLMap.add u 0 res
+ in
+ let cumul res u =
+ let x = try UniverseLMap.find u res with Not_found -> 0 in
+ UniverseLMap.add u (x+1) res
+ in
+ List.fold_left cumul (List.fold_left cumul res lt) le)
+ g UniverseLMap.empty
+ in
+ let init = (* canonical nodes with zero incoming edges *)
+ UniverseLMap.fold
+ (fun u deg res -> if deg = 0 then u::res else res) degs []
+ in
+ (* [init] should contain at least [Set] *)
+ assert (List.mem Set init);
+ let make_level n = Level (mp, n) in
+ let rec reduce level_map degs n level us =
+ (* preconditions: [us] is the list of nodes for universe number
+ [n], supposed non-empty, and [level] is the [universe_level]
+ corresponding to [n] *)
+ assert (us <> [] && level = make_level n);
+ let edge = Equiv level in
+ let visit (level_map, degs, next) u =
+ let level_map = UniverseLMap.add u edge level_map in
+ match lookup_level u g with
+ | None -> level_map, degs, next
+ | Some (Equiv _) -> assert false
+ | Some (Canonical {univ=_; lt=lt; le=le}) ->
+ (* virtually remove [u] from the graph, decrement incoming
+ edge counts in [degs], and collect nodes for the next
+ level (i.e. nodes for which the edge count reached
+ zero) *)
+ let cumul (degs, next) u =
+ let x = UniverseLMap.find u degs - 1 in
+ assert (x >= 0);
+ let degs = UniverseLMap.add u x degs in
+ if x = 0 then degs, u::next else degs, next
+ in
+ let z = List.fold_left cumul (degs, next) lt in
+ let degs, next = List.fold_left cumul z le in
+ level_map, degs, next
+ in
+ let level_map, degs, next =
+ List.fold_left visit (level_map, degs, []) us
+ in
+ if next = [] then
+ let () = UniverseLMap.iter (fun _ x -> assert (x = 0)) degs in
+ level_map
+ else
+ (* we create [next_level] here to keep physical equality of all
+ [Type.n]s *)
+ let next_level = make_level (n+1) in
+ let level_map = UniverseLMap.add level
+ (Canonical {univ=level; lt=[next_level]; le=[]}) level_map
+ in
+ reduce level_map degs (n+1) next_level next
+ in
+ let level_map = reduce UniverseLMap.empty degs 0 (make_level 0) init in
+ let level_map = UniverseLMap.fold (fun u arc res -> match arc with
+ | Equiv v -> UniverseLMap.add u (UniverseLMap.find v res) res
+ | Canonical _ -> res) g level_map
+ in
+ (* defensively check that the result makes sense *)
+ check_sorted orig_g level_map;
+ level_map
+
(**********************************************************************)
(* Tools for sort-polymorphic inductive types *)
diff --git a/kernel/univ.mli b/kernel/univ.mli
index 83c69da99..e19a4c43a 100644
--- a/kernel/univ.mli
+++ b/kernel/univ.mli
@@ -63,6 +63,8 @@ type constraint_type = Lt | Le | Eq
exception UniverseInconsistency of constraint_type * universe * universe
val merge_constraints : constraints -> universes -> universes
+val normalize_universes : universes -> universes
+val sort_universes : universes -> universes
(** {6 Support for sort-polymorphic inductive types } *)
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index 5ff8e06a6..4abc2e5eb 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -755,7 +755,8 @@ GEXTEND Gram
| IDENT "Scope"; s = IDENT -> PrintScope s
| IDENT "Visibility"; s = OPT [x = IDENT -> x ] -> PrintVisibility s
| IDENT "Implicit"; qid = smart_global -> PrintImplicit qid
- | IDENT "Universes"; fopt = OPT ne_string -> PrintUniverses fopt
+ | IDENT "Universes"; fopt = OPT ne_string -> PrintUniverses (false, fopt)
+ | IDENT "Sorted"; IDENT "Universes"; fopt = OPT ne_string -> PrintUniverses (true, fopt)
| IDENT "Assumptions"; qid = smart_global -> PrintAssumptions (false, qid)
| IDENT "Opaque"; IDENT "Dependencies"; qid = smart_global -> PrintAssumptions (true, qid) ] ]
;
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index 8d74fd1f8..0583403df 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -878,7 +878,7 @@ let rec pr_vernac = function
| PrintHintDb -> str"Print Hint *"
| PrintHintDbName s -> str"Print HintDb" ++ spc() ++ str s
| PrintRewriteHintDbName s -> str"Print Rewrite HintDb" ++ spc() ++ str s
- | PrintUniverses fopt -> str"Print Universes" ++ pr_opt str fopt
+ | PrintUniverses (b, fopt) -> Printf.ksprintf str "Print %sUniverses" (if b then "Sorted " else "") ++ pr_opt str fopt
| PrintName qid -> str"Print" ++ spc() ++ pr_smart_global qid
| PrintModuleType qid -> str"Print Module Type" ++ spc() ++ pr_reference qid
| PrintModule qid -> str"Print Module" ++ spc() ++ pr_reference qid
diff --git a/test-suite/success/PrintSortedUniverses.v b/test-suite/success/PrintSortedUniverses.v
new file mode 100644
index 000000000..813265808
--- /dev/null
+++ b/test-suite/success/PrintSortedUniverses.v
@@ -0,0 +1,2 @@
+Require Reals.
+Print Sorted Universes.
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 367f0ef00..16817143d 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -202,7 +202,7 @@ let print_modtype r =
with
Not_found -> msgnl (str"Unknown Module Type " ++ pr_qualid qid)
-let dump_universes s =
+let dump_universes_gen g s =
let output = open_out s in
let output_constraint, close =
if Filename.check_suffix s ".dot" || Filename.check_suffix s ".gv" then begin
@@ -232,12 +232,17 @@ let dump_universes s =
end
in
try
- Univ.dump_universes output_constraint (Global.universes ());
+ Univ.dump_universes output_constraint g;
close ();
msgnl (str ("Universes written to file \""^s^"\"."))
with
e -> close (); raise e
+let dump_universes sorted s =
+ let g = Global.universes () in
+ let g = if sorted then Univ.sort_universes g else g in
+ dump_universes_gen g s
+
(*********************)
(* "Locate" commands *)
@@ -1112,8 +1117,11 @@ let vernac_print = function
| PrintCoercionPaths (cls,clt) ->
ppnl (Prettyp.print_path_between (cl_of_qualid cls) (cl_of_qualid clt))
| PrintCanonicalConversions -> ppnl (Prettyp.print_canonical_projections ())
- | PrintUniverses None -> pp (Univ.pr_universes (Global.universes ()))
- | PrintUniverses (Some s) -> dump_universes s
+ | PrintUniverses (b, None) ->
+ let univ = Global.universes () in
+ let univ = if b then Univ.sort_universes univ else univ in
+ pp (Univ.pr_universes univ)
+ | PrintUniverses (b, Some s) -> dump_universes b s
| PrintHint r -> Auto.print_hint_ref (smart_global r)
| PrintHintGoal -> Auto.print_applicable_hint ()
| PrintHintDbName s -> Auto.print_hint_db_by_name s
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 9af222461..72c9b1fe8 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -51,7 +51,7 @@ type printable =
| PrintCoercions
| PrintCoercionPaths of class_rawexpr * class_rawexpr
| PrintCanonicalConversions
- | PrintUniverses of string option
+ | PrintUniverses of bool * string option
| PrintHint of reference or_by_notation
| PrintHintGoal
| PrintHintDbName of string
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-02 13:32:34 +0000