From fd06eda492de2566ae44777ddbc9cd32744a2633 Mon Sep 17 00:00:00 2001 From: Matthieu Sozeau Date: Fri, 6 Jun 2014 15:59:38 +0200 Subject: Make kernel reduction code parametric over the handling of universes, allowing fast conversion to be used during unification while respecting the semantics of unification w.r.t universes. - Inside kernel, checked_conv is used mainly, it just does checking, while infer_conv is used for module subtyping. - Outside, infer_conv is wrapped in Reductionops to register the right constraints in an evarmap. - In univ, add a flag to universes to cache the fact that they are >= Set, the most common constraints, resulting in an 4x speedup in some cases (e.g. HigmanS). --- kernel/reduction.mli | 24 ++++++++++++++++++------ 1 file changed, 18 insertions(+), 6 deletions(-) (limited to 'kernel/reduction.mli') diff --git a/kernel/reduction.mli b/kernel/reduction.mli index b9bd41f28..b45dca03e 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -26,20 +26,29 @@ val nf_betaiota : env -> constr -> constr exception NotConvertible exception NotConvertibleVect of int -type conv_universes = Univ.universes * Univ.constraints option - type 'a conversion_function = env -> 'a -> 'a -> unit type 'a trans_conversion_function = Names.transparent_state -> 'a conversion_function type 'a universe_conversion_function = env -> Univ.universes -> 'a -> 'a -> unit type 'a trans_universe_conversion_function = Names.transparent_state -> 'a universe_conversion_function -type 'a infer_conversion_function = env -> Univ.universes -> 'a -> 'a -> Univ.constraints - type conv_pb = CONV | CUMUL -val sort_cmp_universes : - conv_pb -> sorts -> sorts -> conv_universes -> conv_universes +type 'a universe_compare = + { (* Might raise NotConvertible *) + compare : conv_pb -> sorts -> sorts -> 'a -> 'a; + compare_instances: bool (* Instance of a flexible constant? *) -> + Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a; + } + +type 'a universe_state = 'a * 'a universe_compare + +type ('a,'b) generic_conversion_function = env -> 'b universe_state -> 'a -> 'a -> 'b + +type 'a infer_conversion_function = env -> Univ.universes -> 'a -> 'a -> Univ.constraints + +val check_sort_cmp_universes : + conv_pb -> sorts -> sorts -> Univ.universes -> unit (* val sort_cmp : *) (* conv_pb -> sorts -> sorts -> Univ.constraints -> Univ.constraints *) @@ -71,6 +80,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 +val generic_conv : conv_pb -> bool -> (existential->constr option) -> + Names.transparent_state -> (constr,'a) generic_conversion_function + (** option for conversion *) val set_vm_conv : (conv_pb -> types conversion_function) -> unit val vm_conv : conv_pb -> types conversion_function -- cgit v1.2.3