diff options
Diffstat (limited to 'kernel')
| -rw-r--r-- | kernel/uGraph.ml | 35 |
1 files changed, 33 insertions, 2 deletions
diff --git a/kernel/uGraph.ml b/kernel/uGraph.ml index 096e458ec4..5d7cc92181 100644 --- a/kernel/uGraph.ml +++ b/kernel/uGraph.ml @@ -222,11 +222,42 @@ let choose p g u = if Level.is_sprop u then if p u then Some u else None else G.choose p g.graph u -let dump_universes f g = G.dump f g.graph +(* Dumping constraints to a file *) + +let dump_universes output g = + let dump_arc u = function + | G.Node ltle -> + LMap.iter (fun v strict -> + let typ = if strict then Lt else Le in + output typ u v) ltle; + | G.Alias v -> + output Eq u v + in + LMap.iter dump_arc (G.repr g.graph) let check_universes_invariants g = G.check_invariants ~required_canonical:Level.is_small g.graph -let pr_universes prl g = G.pr prl g.graph +(** Pretty-printing *) + +let pr_pmap sep pr map = + let cmp (u,_) (v,_) = Level.compare u v in + Pp.prlist_with_sep sep pr (List.sort cmp (LMap.bindings map)) + +let pr_arc prl = let open Pp in + function + | u, G.Node ltle -> + if LMap.is_empty ltle then mt () + else + prl u ++ str " " ++ + v 0 + (pr_pmap spc (fun (v, strict) -> + (if strict then str "< " else str "<= ") ++ prl v) + ltle) ++ + fnl () + | u, G.Alias v -> + prl u ++ str " = " ++ prl v ++ fnl () + +let pr_universes prl g = pr_pmap Pp.mt (pr_arc prl) (G.repr g.graph) let dummy_mp = Names.DirPath.make [Names.Id.of_string "Type"] let make_dummy i = Level.(make (UGlobal.make dummy_mp i)) |