From d06211803146dec998b414d215d4d93190e2001f Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Mon, 28 Nov 2016 18:36:10 +0100 Subject: Univs: fix bug #5180 In the kernel's generic conversion, backtrack on UniverseInconsistency for the unfolding heuristic (single backtracking point in reduction). This exception can be raised in the univ_compare structure to produce better error messages when the generic conversion function is called from higher level code in reductionops.ml, which itself is called during unification in evarconv.ml. Inside the kernel, the infer and check variants of conversion never raise UniverseInconsistency though, so this does not change the behavior of the kernel. --- kernel/reduction.mli | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) (limited to 'kernel/reduction.mli') diff --git a/kernel/reduction.mli b/kernel/reduction.mli index 9812c45f7..8a2b2469d 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -36,7 +36,7 @@ type 'a extended_conversion_function = type conv_pb = CONV | CUMUL type 'a universe_compare = - { (* Might raise NotConvertible *) + { (* Might raise NotConvertible or UnivInconsistency *) compare : env -> conv_pb -> sorts -> sorts -> 'a -> 'a; compare_instances: flex:bool -> Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a; @@ -56,9 +56,12 @@ constructors. *) val convert_instances : flex:bool -> Univ.Instance.t -> Univ.Instance.t -> 'a * 'a universe_compare -> 'a * 'a universe_compare +(** These two never raise UnivInconsistency, inferred_universes + just gathers the constraints. *) val checked_universes : UGraph.t universe_compare val inferred_universes : (UGraph.t * Univ.Constraint.t) universe_compare +(** These two functions can only raise NotConvertible *) val conv : constr extended_conversion_function val conv_leq : types extended_conversion_function @@ -70,6 +73,9 @@ val infer_conv : ?l2r:bool -> ?evars:(existential->constr option) -> val infer_conv_leq : ?l2r:bool -> ?evars:(existential->constr option) -> ?ts:Names.transparent_state -> types infer_conversion_function +(** Depending on the universe state functions, this might raise + [UniverseInconsistency] in addition to [NotConvertible] (for better error + messages). *) val generic_conv : conv_pb -> l2r:bool -> (existential->constr option) -> Names.transparent_state -> (constr,'a) generic_conversion_function -- cgit v1.2.3