From d4cdb7e41844e1bb77bac9a7b9df423364b996e2 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Fri, 27 May 2016 14:02:39 +0200 Subject: Univs: add source locations of levels For better error messages. The API change is backwards compatible, using a new optional argument. --- engine/evd.ml | 1 + engine/evd.mli | 5 +++-- engine/uState.ml | 23 +++++++++++++++-------- 3 files changed, 19 insertions(+), 10 deletions(-) (limited to 'engine') diff --git a/engine/evd.ml b/engine/evd.ml index b883db615e..1276c5994e 100644 --- a/engine/evd.ml +++ b/engine/evd.ml @@ -252,6 +252,7 @@ let instantiate_evar_array info c args = | _ -> replace_vars inst c type evar_universe_context = UState.t + type 'a in_evar_universe_context = 'a * evar_universe_context let empty_evar_universe_context = UState.empty diff --git a/engine/evd.mli b/engine/evd.mli index df491c27b4..d6cf83525c 100644 --- a/engine/evd.mli +++ b/engine/evd.mli @@ -511,6 +511,7 @@ val normalize_evar_universe_context : evar_universe_context -> val new_univ_level_variable : ?loc:Loc.t -> ?name:string -> ?predicative:bool -> rigid -> evar_map -> evar_map * Univ.universe_level val new_univ_variable : ?loc:Loc.t -> ?name:string -> ?predicative:bool -> rigid -> evar_map -> evar_map * Univ.universe val new_sort_variable : ?loc:Loc.t -> ?name:string -> ?predicative:bool -> rigid -> evar_map -> evar_map * sorts + val add_global_univ : evar_map -> Univ.Level.t -> evar_map val make_flexible_variable : evar_map -> bool -> Univ.universe_level -> evar_map @@ -568,8 +569,8 @@ val fresh_constant_instance : ?loc:Loc.t -> env -> evar_map -> constant -> evar_ val fresh_inductive_instance : ?loc:Loc.t -> env -> evar_map -> inductive -> evar_map * pinductive val fresh_constructor_instance : ?loc:Loc.t -> env -> evar_map -> constructor -> evar_map * pconstructor -val fresh_global : ?loc:Loc.t -> ?rigid:rigid -> ?names:Univ.Instance.t -> env -> evar_map -> - Globnames.global_reference -> evar_map * constr +val fresh_global : ?loc:Loc.t -> ?rigid:rigid -> ?names:Univ.Instance.t -> env -> + evar_map -> Globnames.global_reference -> evar_map * constr (******************************************************************** Conversion w.r.t. an evar map, not unifying universes. See diff --git a/engine/uState.ml b/engine/uState.ml index 8aa9a61ab9..73b2318515 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -49,7 +49,7 @@ let empty = uctx_univ_variables = Univ.LMap.empty; uctx_univ_algebraic = Univ.LSet.empty; uctx_universes = UGraph.initial_universes; - uctx_initial_universes = UGraph.initial_universes } + uctx_initial_universes = UGraph.initial_universes; } let make u = { empty with @@ -83,7 +83,7 @@ let union ctx ctx' = if local == ctx.uctx_local then ctx.uctx_universes else let cstrsr = Univ.ContextSet.constraints ctx'.uctx_local in - UGraph.merge_constraints cstrsr (declarenew ctx.uctx_universes) } + UGraph.merge_constraints cstrsr (declarenew ctx.uctx_universes) } let context_set ctx = ctx.uctx_local @@ -263,13 +263,19 @@ let universe_context ?names ctx = if not (Univ.LSet.is_empty left) then let n = Univ.LSet.cardinal left in let loc = - let get_loc u = try (Univ.LMap.find u (snd ctx.uctx_names)).uloc with Not_found -> None in - try List.find_map get_loc (Univ.LSet.elements left) with Not_found -> Loc.ghost + if n == 1 then + try + let info = + Univ.LMap.find (Univ.LSet.choose left) (snd ctx.uctx_names) in + Option.default Loc.ghost info.uloc + with Not_found -> Loc.ghost + else Loc.ghost in user_err_loc (loc, "universe_context", - (str(CString.plural n "Universe") ++ spc () ++ - Univ.LSet.pr (pr_uctx_level ctx) left ++ - spc () ++ str (CString.conjugate_verb_to_be n) ++ str" unbound.")) + (str(CString.plural n "Universe") ++ spc () ++ + Univ.LSet.pr (pr_uctx_level ctx) left ++ + spc () ++ str (CString.conjugate_verb_to_be n) ++ + str" unbound.")) else let inst = Univ.Instance.of_array (Array.of_list newinst) in let ctx = Univ.UContext.make (inst, @@ -329,7 +335,8 @@ let merge ?loc sideff rigid uctx ctx' = let initial = declare uctx.uctx_initial_universes in let univs = declare uctx.uctx_universes in let uctx_universes = UGraph.merge_constraints (ContextSet.constraints ctx') univs in - { uctx with uctx_names; uctx_local; uctx_universes; uctx_initial_universes = initial } + { uctx with uctx_names; uctx_local; uctx_universes; + uctx_initial_universes = initial } let merge_subst uctx s = { uctx with uctx_univ_variables = Univ.LMap.subst_union uctx.uctx_univ_variables s } -- cgit v1.2.3 From 40ee96a0392fbc0945c48b5b134aa1be36f86225 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Fri, 27 May 2016 14:10:20 +0200 Subject: Univ: Use loc even if there are more unbound levels --- engine/uState.ml | 12 +++++------- 1 file changed, 5 insertions(+), 7 deletions(-) (limited to 'engine') diff --git a/engine/uState.ml b/engine/uState.ml index 73b2318515..2fb64cd6e5 100644 --- a/engine/uState.ml +++ b/engine/uState.ml @@ -263,13 +263,11 @@ let universe_context ?names ctx = if not (Univ.LSet.is_empty left) then let n = Univ.LSet.cardinal left in let loc = - if n == 1 then - try - let info = - Univ.LMap.find (Univ.LSet.choose left) (snd ctx.uctx_names) in - Option.default Loc.ghost info.uloc - with Not_found -> Loc.ghost - else Loc.ghost + try + let info = + Univ.LMap.find (Univ.LSet.choose left) (snd ctx.uctx_names) in + Option.default Loc.ghost info.uloc + with Not_found -> Loc.ghost in user_err_loc (loc, "universe_context", (str(CString.plural n "Universe") ++ spc () ++ -- cgit v1.2.3