diff options
Diffstat (limited to 'kernel/reduction.mli')
| -rw-r--r-- | kernel/reduction.mli | 75 |
1 files changed, 37 insertions, 38 deletions
diff --git a/kernel/reduction.mli b/kernel/reduction.mli index 9a83ca70..8a2b2469 100644 --- a/kernel/reduction.mli +++ b/kernel/reduction.mli @@ -7,15 +7,16 @@ (************************************************************************) open Term -open Context open Environ (*********************************************************************** s Reduction functions *) +(* None of these functions do eta reduction *) + val whd_betaiotazeta : env -> constr -> constr -val whd_betadeltaiota : env -> constr -> constr -val whd_betadeltaiota_nolet : env -> constr -> constr +val whd_all : env -> constr -> constr +val whd_allnolet : env -> constr -> constr val whd_betaiota : env -> constr -> constr val nf_betaiota : env -> constr -> constr @@ -26,16 +27,16 @@ 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 = 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 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 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; @@ -45,7 +46,7 @@ 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 +type 'a infer_conversion_function = env -> UGraph.t -> 'a -> 'a -> Univ.constraints val sort_cmp_universes : env -> conv_pb -> sorts -> sorts -> 'a * 'a universe_compare -> 'a * 'a universe_compare @@ -55,27 +56,15 @@ constructors. *) val convert_instances : flex:bool -> Univ.Instance.t -> Univ.Instance.t -> 'a * 'a universe_compare -> 'a * 'a universe_compare -val checked_universes : Univ.universes universe_compare -val inferred_universes : (Univ.universes * Univ.Constraint.t) universe_compare - -val trans_conv_cmp : ?l2r:bool -> conv_pb -> constr trans_conversion_function -val trans_conv : - ?l2r:bool -> ?evars:(existential->constr option) -> constr trans_conversion_function -val trans_conv_leq : - ?l2r:bool -> ?evars:(existential->constr option) -> types trans_conversion_function +(** 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 -val trans_conv_universes : - ?l2r:bool -> ?evars:(existential->constr option) -> constr trans_universe_conversion_function -val trans_conv_leq_universes : - ?l2r:bool -> ?evars:(existential->constr option) -> types trans_universe_conversion_function +(** These two functions can only raise NotConvertible *) +val conv : constr extended_conversion_function -val conv_cmp : ?l2r:bool -> conv_pb -> constr conversion_function -val conv : - ?l2r:bool -> ?evars:(existential->constr option) -> constr conversion_function -val conv_leq : - ?l2r:bool -> ?evars:(existential->constr option) -> types conversion_function -val conv_leq_vecti : - ?l2r:bool -> ?evars:(existential->constr option) -> types array 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 *) @@ -84,36 +73,46 @@ 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 (** 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 (************************************************************************) (** Builds an application node, reducing beta redexes it may produce. *) +val beta_applist : constr -> constr list -> constr + +(** Builds an application node, reducing beta redexes it may produce. *) val beta_appvect : constr -> constr array -> constr -(** Builds an application node, reducing the [n] first beta-zeta redexes. *) -val betazeta_appvect : int -> constr -> constr array -> constr +(** Builds an application node, reducing beta redexe it may produce. *) +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 +(** Compatibility alias for Term.lambda_appvect_assum *) +val betazeta_appvect : int -> constr -> constr array -> constr (*********************************************************************** s Recognizing products and arities modulo reduction *) -val dest_prod : env -> types -> rel_context * types -val dest_prod_assum : env -> types -> rel_context * types -val dest_lam_assum : env -> types -> rel_context * types +val dest_prod : env -> types -> Context.Rel.t * types +val dest_prod_assum : env -> types -> Context.Rel.t * types +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 is_arity : env -> types -> bool + +val warn_bytecode_compiler_failed : ?loc:Loc.t -> unit -> unit |