Have a more useful Environ.set_qualities

Author: yannl35133

dev/top_printers.dbg

@@ -88,6 +88,7 @@ install_printer Top_printers.ppqconstraints
 install_printer Top_printers.ppuniverseconstraints
 install_printer Top_printers.ppuniverse_context_future
 install_printer Top_printers.ppuniverses
+install_printer Top_printers.ppqualities
 install_printer Top_printers.pp_partialfsubst
 install_printer Top_printers.pp_partialsubst
 install_printer Top_printers.ppnamedcontextval

dev/top_printers.ml

@@ -295,6 +295,7 @@ let ppuniverse_context_future c =
   let ctx = Future.force c in
     ppuniverse_context ctx
 let ppuniverses u = pp (UGraph.pr_universes Level.raw_pr (UGraph.repr u))
+let ppqualities q = pp (QGraph.pr_qualities Quality.raw_pr q)
 let ppnamedcontextval e =
   let env = Global.env () in
   let sigma = Evd.from_env env in

dev/top_printers.mli

@@ -167,6 +167,7 @@ val ppqconstraints : Sorts.ElimConstraints.t -> unit
 val ppuniverseconstraints : UnivProblem.Set.t -> unit
 val ppuniverse_context_future : UVars.UContext.t Future.computation -> unit
 val ppuniverses : UGraph.t -> unit
+val ppqualities : QGraph.t -> unit
 
 val pp_partialfsubst : (CClosure.fconstr, Sorts.Quality.t, Univ.Universe.t) Partial_subst.t -> unit
 val pp_partialsubst : (EConstr.constr, Sorts.Quality.t, Univ.Universe.t) Partial_subst.t -> unit

kernel/environ.ml

@@ -494,7 +494,7 @@ let push_qualities qs env =
             (fun v -> QGraph.add_quality (Sorts.Quality.QVar v)) qs env.env_qualities in
   set_qualities g env
 
-let set_qualities qs env =
+let set_qvars qs env =
   let g = QGraph.initial_graph in
   let g = Sorts.QVar.Set.fold (fun v -> QGraph.add_quality (Sorts.Quality.QVar v)) qs g in
   { env with env_qualities = g }

kernel/environ.mli

@@ -74,10 +74,11 @@ val named_context : env -> Constr.named_context
 val named_context_val : env -> named_context_val
 
 val set_universes : UGraph.t -> env -> env
+val set_qualities : QGraph.t -> env -> env
+val set_qvars : Sorts.QVar.Set.t -> env -> env
 
 val qualities : env -> QGraph.t
 val qvars : env -> Sorts.QVar.Set.t
-val set_qualities : Sorts.QVar.Set.t -> env -> env
 
 val typing_flags    : env -> typing_flags
 val is_impredicative_set : env -> bool

kernel/qGraph.ml

@@ -275,6 +275,32 @@ let qvar_domain g =
 
 let is_empty g = QVar.Set.is_empty (qvar_domain g)
 
+(* Pretty printing *)
+
+let pr_pmap sep pr map =
+  let cmp (u,_) (v,_) = Quality.compare u v in
+  Pp.prlist_with_sep sep pr (List.sort cmp (Quality.Map.bindings map))
+
+let pr_arc prq =
+  let open Pp in
+  function
+  | u, G.Node ltle ->
+    if Quality.Map.is_empty ltle then mt ()
+    else
+      prq u ++ str " " ++
+      v 0
+        (pr_pmap spc (fun (v, strict) ->
+              (if strict then str "< " else str "<= ") ++ prq v)
+            ltle) ++
+      fnl ()
+  | u, G.Alias v ->
+    prq u  ++ str " = " ++ prq v ++ fnl ()
+
+
+let repr g = G.repr g.graph
+
+let pr_qualities prq g = pr_pmap Pp.mt (pr_arc prq) (repr g)
+
 let explain_quality_inconsistency prv r =
   let open Pp in
   let pr_cst = function

kernel/qGraph.mli

@@ -99,4 +99,6 @@ val qvar_domain : t -> QVar.Set.t
 
 val is_empty : t -> bool
 
+val pr_qualities : (Quality.t -> Pp.t) -> t -> Pp.t
+
 val explain_quality_inconsistency : (QVar.t -> Pp.t) -> explanation option -> Pp.t

kernel/safe_typing.ml

@@ -1392,7 +1392,7 @@ let end_module l restype senv =
   let mbids = List.rev_map fst params in
   let mb = build_module_body params restype senv in
   let newenv = Environ.set_universes (Environ.universes senv.env) oldsenv.env in
-  let newenv = Environ.set_qualities (Environ.qvars senv.env) newenv in
+  let newenv = Environ.set_qualities (Environ.qualities senv.env) newenv in
   let newenv = if Environ.rewrite_rules_allowed senv.env then Environ.allow_rewrite_rules newenv else newenv in
   let newenv = Environ.set_vm_library (Environ.vm_library senv.env) newenv in
   let senv' = propagate_loads { senv with env = newenv } in

pretyping/reductionops.ml

@@ -1336,6 +1336,7 @@ let infer_conv_gen conv_fun ?(catch_incon=true) ?(pb=Conversion.CUMUL)
       | None ->
         let x = EConstr.Unsafe.to_constr x in
         let y = EConstr.Unsafe.to_constr y in
+        let env = Environ.set_qualities (Evd.elim_graph sigma) env in
         let env = Environ.set_universes (Evd.universes sigma) env in
         (* First try conversion with postponed universe problems as a kind of FO
            approximation. This may result in unsatisfiable constraints even if

vernac/himsg.ml

@@ -251,7 +251,7 @@ let explain_elim_arity env sigma ind c okinds =
         if ppunivs then Flags.with_option Constrextern.print_universes pp ()
         else pp ()
       in
-      let env = Environ.set_qualities (QGraph.qvar_domain @@ Evd.elim_graph sigma) env in
+      let env = Environ.set_qualities (Evd.elim_graph sigma) env in
       let squash = Option.get (Inductive.is_squashed env (specif, snd ind)) in
       match squash with
       | SquashToSet ->