diff options
Diffstat (limited to 'kernel/reduction.mli')
| -rw-r--r-- | kernel/reduction.mli | 30 |
1 files changed, 19 insertions, 11 deletions
diff --git a/kernel/reduction.mli b/kernel/reduction.mli index 253c0874f2..6f7e3f8f8f 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -6,7 +6,7 @@ (* * GNU Lesser General Public License Version 2.1 *) (************************************************************************) -open Term +open Constr open Environ (*********************************************************************** @@ -35,23 +35,25 @@ type 'a extended_conversion_function = type conv_pb = CONV | CUMUL -type 'a universe_compare = +type 'a universe_compare = { (* Might raise NotConvertible *) - compare : env -> conv_pb -> sorts -> sorts -> 'a -> 'a; + compare_sorts : env -> conv_pb -> Sorts.t -> Sorts.t -> 'a -> 'a; compare_instances: flex:bool -> Univ.Instance.t -> Univ.Instance.t -> 'a -> 'a; - conv_inductives : conv_pb -> (Declarations.mutual_inductive_body * int) -> Univ.Instance.t -> int -> - Univ.Instance.t -> int -> 'a -> 'a; - conv_constructors : (Declarations.mutual_inductive_body * int * int) -> - Univ.Instance.t -> int -> Univ.Instance.t -> int -> 'a -> 'a; - } + compare_cumul_instances : Univ.Constraint.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 -> UGraph.t -> 'a -> 'a -> Univ.constraints +type 'a infer_conversion_function = env -> UGraph.t -> 'a -> 'a -> Univ.Constraint.t -val sort_cmp_universes : env -> conv_pb -> sorts -> sorts -> +val get_cumulativity_constraints : conv_pb -> Univ.ACumulativityInfo.t -> + Univ.Instance.t -> Univ.Instance.t -> Univ.Constraint.t + +val inductive_cumulativity_arguments : (Declarations.mutual_inductive_body * int) -> int +val constructor_cumulativity_arguments : (Declarations.mutual_inductive_body * int * int) -> int + +val sort_cmp_universes : env -> conv_pb -> Sorts.t -> Sorts.t -> 'a * 'a universe_compare -> 'a * 'a universe_compare (* [flex] should be true for constants, false for inductive types and @@ -103,6 +105,12 @@ val beta_app : constr -> constr -> constr (** Pseudo-reduction rule Prod(x,A,B) a --> B[x\a] *) val hnf_prod_applist : env -> types -> constr list -> types +(** In [hnf_prod_applist_assum n c args], [c] is supposed to (whd-)reduce to + the form [∀Γ.t] with [Γ] of length [n] and possibly with let-ins; it + returns [t] with the assumptions of [Γ] instantiated by [args] and + the local definitions of [Γ] expanded. *) +val hnf_prod_applist_assum : env -> int -> types -> constr list -> types + (** Compatibility alias for Term.lambda_appvect_assum *) val betazeta_appvect : int -> constr -> constr array -> constr @@ -115,7 +123,7 @@ val dest_lam_assum : env -> types -> Context.Rel.t * types exception NotArity -val dest_arity : env -> types -> arity (* raises NotArity if not an arity *) +val dest_arity : env -> types -> Term.arity (* raises NotArity if not an arity *) val is_arity : env -> types -> bool val warn_bytecode_compiler_failed : ?loc:Loc.t -> unit -> unit |