CLEANUP: in the Reduction module

4 files changed, 35 insertions, 39 deletions

diff --git a/kernel/nativeconv.mli b/kernel/nativeconv.mli
index 4dddb9fd3..abc9e3a3c 100644
--- a/kernel/nativeconv.mli
+++ b/kernel/nativeconv.mli
@@ -11,7 +11,7 @@ open Nativelambda
 
 (** This module implements the conversion test by compiling to OCaml code *)
 
-val native_conv : conv_pb -> evars -> types conversion_function
+val native_conv : conv_pb -> evars -> types kernel_conversion_function
 
 (** A conversion function parametrized by a universe comparator. Used outside of
     the kernel. *)
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 8c9be0edd..95bea9292 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -125,11 +125,15 @@ let whd_betadeltaiota_nolet env t =
 (********************************************************************)
 
 (* Conversion utility functions *)
-type 'a conversion_function = env -> 'a -> 'a -> unit
-type 'a trans_conversion_function = ?reds:Names.transparent_state -> 'a conversion_function
-type 'a universe_conversion_function = env -> UGraph.t -> 'a -> 'a -> unit
-type 'a trans_universe_conversion_function = 
-  Names.transparent_state -> 'a universe_conversion_function
+
+(* functions of this type are called from the kernel *)
+type 'a kernel_conversion_function = env -> 'a -> 'a -> unit
+
+(* functions of this type can be called from outside the kernel *)
+type 'a extended_conversion_function =
+  ?l2r:bool -> ?reds:Names.transparent_state -> env ->
+  ?evars:((existential->constr option) * UGraph.t) ->
+  'a -> 'a -> unit
 
 exception NotConvertible
 exception NotConvertibleVect of int
@@ -616,7 +620,7 @@ let inferred_universes : (UGraph.t * Univ.Constraint.t) universe_compare =
   { compare = infer_cmp_universes;
     compare_instances = infer_convert_instances }
 
-let fconv_universes reds cv_pb l2r evars env univs t1 t2 =
+let fconv cv_pb l2r reds env evars univs t1 t2 =
   let b = 
     if cv_pb = CUMUL then leq_constr_univs univs t1 t2 
     else eq_constr_univs univs t1 t2
@@ -627,22 +631,16 @@ let fconv_universes reds cv_pb l2r evars env univs t1 t2 =
 	()
 
 (* Profiling *)
-let fconv_universes = 
+let fconv cv_pb ?(l2r=false) ?(reds=full_transparent_state) env ?(evars=(fun _->None), universes env) =
+  let evars, univs = evars in
   if Flags.profile then
     let fconv_universes_key = Profile.declare_profile "trans_fconv_universes" in
-      Profile.profile8 fconv_universes_key fconv_universes
-  else fconv_universes
+      Profile.profile8 fconv_universes_key fconv cv_pb l2r reds env evars univs
+  else fconv cv_pb l2r reds env evars univs
 
-let fconv ?(reds=full_transparent_state) cv_pb l2r evars env = 
-  fconv_universes reds cv_pb l2r evars env (universes env)
+let conv = fconv CONV
 
-let conv ?(l2r=false) ?(evars=fun _->None) ?(reds=full_transparent_state) =
-  fconv ~reds CONV l2r evars
-
-let conv_universes ?(l2r=false) ?(evars=fun _->None) reds =
-  fconv_universes reds CONV l2r evars
-let conv_leq_universes ?(l2r=false) ?(evars=fun _->None) reds = 
-  fconv_universes reds CUMUL l2r evars
+let conv_leq = fconv CUMUL
 
 let generic_conv cv_pb ~l2r evars reds env univs t1 t2 =
   let (s, _) = 
@@ -676,17 +674,19 @@ let infer_conv_leq ?(l2r=false) ?(evars=fun _ -> None) ?(ts=full_transparent_sta
   infer_conv_universes CUMUL l2r evars ts env univs t1 t2
 
 (* This reference avoids always having to link C code with the kernel *)
-let vm_conv = ref (fun cv_pb -> fconv cv_pb false (fun _->None))
-let set_vm_conv f = vm_conv := f
+let vm_conv = ref (fun cv_pb env ->
+		   fconv cv_pb env ~evars:((fun _->None), universes env))
+
+let set_vm_conv (f:conv_pb -> Term.types kernel_conversion_function) = vm_conv := f
 let vm_conv cv_pb env t1 t2 =
   try
     !vm_conv cv_pb env t1 t2
   with Not_found | Invalid_argument _ ->
     Pp.msg_warning (Pp.str "Bytecode compilation failed, falling back to standard conversion");
-    fconv cv_pb false (fun _->None) env t1 t2
+    fconv cv_pb env t1 t2
 
 let default_conv cv_pb ?(l2r=false) env t1 t2 =
-    fconv cv_pb false (fun _ -> None) env t1 t2
+    fconv cv_pb env t1 t2
 
 let default_conv_leq = default_conv CUMUL
 (*
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index 304046a1d..f7a8d88c2 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -26,11 +26,11 @@ val nf_betaiota      : env -> constr -> constr
 exception NotConvertible
 exception NotConvertibleVect of int
 
-type 'a conversion_function = env -> 'a -> 'a -> unit
-type 'a trans_conversion_function = ?reds:Names.transparent_state -> 'a conversion_function
-type 'a universe_conversion_function = env -> UGraph.t -> 'a -> 'a -> unit
-type 'a trans_universe_conversion_function = 
-  Names.transparent_state -> 'a universe_conversion_function
+type 'a kernel_conversion_function = env -> 'a -> 'a -> unit
+type 'a extended_conversion_function = 
+  ?l2r:bool -> ?reds:Names.transparent_state -> env ->
+  ?evars:((existential->constr option) * UGraph.t) ->
+  'a -> 'a -> unit
 
 type conv_pb = CONV | CUMUL
 
@@ -58,13 +58,9 @@ val convert_instances : flex:bool -> Univ.Instance.t -> Univ.Instance.t ->
 val checked_universes : UGraph.t universe_compare
 val inferred_universes : (UGraph.t * Univ.Constraint.t) universe_compare
 
-val conv :
-  ?l2r:bool -> ?evars:(existential->constr option) -> constr trans_conversion_function
+val conv : constr extended_conversion_function
 
-val conv_universes :
-  ?l2r:bool -> ?evars:(existential->constr option) -> constr trans_universe_conversion_function
-val conv_leq_universes :
-  ?l2r:bool -> ?evars:(existential->constr option) -> types trans_universe_conversion_function
+val conv_leq : types extended_conversion_function
 
 (** These conversion functions are used by module subtyping, which needs to infer
     universe constraints inside the kernel *)
@@ -77,11 +73,11 @@ val generic_conv : conv_pb -> l2r: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
+val set_vm_conv : (conv_pb -> types kernel_conversion_function) -> unit
+val vm_conv : conv_pb -> types kernel_conversion_function
 
-val default_conv     : conv_pb -> ?l2r:bool -> types conversion_function
-val default_conv_leq : ?l2r:bool -> types conversion_function
+val default_conv     : conv_pb -> ?l2r:bool -> types kernel_conversion_function
+val default_conv_leq : ?l2r:bool -> types kernel_conversion_function
 
 (************************************************************************)
 
diff --git a/kernel/vconv.mli b/kernel/vconv.mli
index 49e5d23e6..acf4c408f 100644
--- a/kernel/vconv.mli
+++ b/kernel/vconv.mli
@@ -12,7 +12,7 @@ open Reduction
 
 (**********************************************************************
   s conversion functions *)
-val vm_conv : conv_pb -> types conversion_function
+val vm_conv : conv_pb -> types kernel_conversion_function
 
 (** A conversion function parametrized by a universe comparator. Used outside of
     the kernel. *)