aboutsummaryrefslogtreecommitdiff
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/cases.ml2
-rw-r--r--pretyping/evarconv.ml15
-rw-r--r--pretyping/evarconv.mli17
-rw-r--r--pretyping/evarsolve.ml6
-rw-r--r--pretyping/heads.ml29
-rw-r--r--pretyping/inferCumulativity.ml4
-rw-r--r--pretyping/pretyping.ml15
-rw-r--r--pretyping/pretyping.mli3
-rw-r--r--pretyping/recordops.ml12
-rw-r--r--pretyping/recordops.mli2
-rw-r--r--pretyping/reductionops.ml35
-rw-r--r--pretyping/reductionops.mli17
-rw-r--r--pretyping/tacred.ml2
-rw-r--r--pretyping/typeclasses.mli4
-rw-r--r--pretyping/unification.ml60
-rw-r--r--pretyping/unification.mli9
16 files changed, 96 insertions, 136 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 164f5ab96d..e02fb33276 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1698,7 +1698,7 @@ let abstract_tycon ?loc env sigma subst tycon extenv t =
try list_assoc_in_triple i subst0 with Not_found -> mkRel i)
1 (rel_context !!env) in
let sigma, ev' = Evarutil.new_evar ~src ~typeclass_candidate:false !!env sigma ty in
- begin match solve_simple_eqn (evar_conv_x full_transparent_state) !!env sigma (None,ev,substl inst ev') with
+ begin match solve_simple_eqn (evar_conv_x TransparentState.full) !!env sigma (None,ev,substl inst ev') with
| Success evd -> evdref := evd
| UnifFailure _ -> assert false
end;
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 6a75be352b..f370ad7ae2 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -16,7 +16,6 @@ open Termops
open Environ
open EConstr
open Vars
-open CClosure
open Reduction
open Reductionops
open Recordops
@@ -30,7 +29,7 @@ open Context.Named.Declaration
module RelDecl = Context.Rel.Declaration
module NamedDecl = Context.Named.Declaration
-type unify_fun = transparent_state ->
+type unify_fun = TransparentState.t ->
env -> evar_map -> conv_pb -> EConstr.constr -> EConstr.constr -> Evarsolve.unification_result
let debug_unification = ref (false)
@@ -74,14 +73,14 @@ let coq_unit_judge =
let unfold_projection env evd ts p c =
let cst = Projection.constant p in
- if is_transparent_constant ts cst then
+ if TransparentState.is_transparent_constant ts cst then
Some (mkProj (Projection.unfold p, c))
else None
let eval_flexible_term ts env evd c =
match EConstr.kind evd c with
| Const (c, u) ->
- if is_transparent_constant ts c
+ if TransparentState.is_transparent_constant ts c
then Option.map EConstr.of_constr (constant_opt_value_in env (c, EInstance.kind evd u))
else None
| Rel n ->
@@ -91,7 +90,7 @@ let eval_flexible_term ts env evd c =
with Not_found -> None)
| Var id ->
(try
- if is_transparent_variable ts id then
+ if TransparentState.is_transparent_variable ts id then
env |> lookup_named id |> NamedDecl.get_value
else None
with Not_found -> None)
@@ -1211,7 +1210,7 @@ let second_order_matching ts env_rhs evd (evk,args) argoccs rhs =
| [] ->
let evd =
try Evarsolve.check_evar_instance evd evk rhs
- (evar_conv_x full_transparent_state)
+ (evar_conv_x TransparentState.full)
with IllTypedInstance _ -> raise (TypingFailed evd)
in
Evd.define evk rhs evd
@@ -1354,7 +1353,7 @@ let solve_unconstrained_impossible_cases env evd =
let j, ctx = coq_unit_judge env in
let evd' = Evd.merge_context_set Evd.univ_flexible_alg ?loc evd' ctx in
let ty = j_type j in
- let conv_algo = evar_conv_x full_transparent_state in
+ let conv_algo = evar_conv_x TransparentState.full in
let evd' = check_evar_instance evd' evk ty conv_algo in
Evd.define evk ty evd'
| _ -> evd') evd evd
@@ -1393,7 +1392,7 @@ let solve_unif_constraints_with_heuristics env
exception UnableToUnify of evar_map * unification_error
-let default_transparent_state env = full_transparent_state
+let default_transparent_state env = TransparentState.full
(* Conv_oracle.get_transp_state (Environ.oracle env) *)
let the_conv_x env ?(ts=default_transparent_state env) t1 t2 evd =
diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli
index 350dece28a..4585fac252 100644
--- a/pretyping/evarconv.mli
+++ b/pretyping/evarconv.mli
@@ -8,7 +8,6 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
-open Names
open EConstr
open Environ
open Reductionops
@@ -22,20 +21,20 @@ exception UnableToUnify of evar_map * Pretype_errors.unification_error
(** {6 Main unification algorithm for type inference. } *)
(** returns exception NotUnifiable with best known evar_map if not unifiable *)
-val the_conv_x : env -> ?ts:transparent_state -> constr -> constr -> evar_map -> evar_map
-val the_conv_x_leq : env -> ?ts:transparent_state -> constr -> constr -> evar_map -> evar_map
+val the_conv_x : env -> ?ts:TransparentState.t -> constr -> constr -> evar_map -> evar_map
+val the_conv_x_leq : env -> ?ts:TransparentState.t -> constr -> constr -> evar_map -> evar_map
(** The same function resolving evars by side-effect and
catching the exception *)
-val conv : env -> ?ts:transparent_state -> evar_map -> constr -> constr -> evar_map option
-val cumul : env -> ?ts:transparent_state -> evar_map -> constr -> constr -> evar_map option
+val conv : env -> ?ts:TransparentState.t -> evar_map -> constr -> constr -> evar_map option
+val cumul : env -> ?ts:TransparentState.t -> evar_map -> constr -> constr -> evar_map option
(** {6 Unification heuristics. } *)
(** Try heuristics to solve pending unification problems and to solve
evars with candidates *)
-val solve_unif_constraints_with_heuristics : env -> ?ts:transparent_state -> evar_map -> evar_map
+val solve_unif_constraints_with_heuristics : env -> ?ts:TransparentState.t -> evar_map -> evar_map
(** Check all pending unification problems are solved and raise an
error otherwise *)
@@ -55,14 +54,14 @@ val check_conv_record : env -> evar_map ->
(** Try to solve problems of the form ?x[args] = c by second-order
matching, using typing to select occurrences *)
-val second_order_matching : transparent_state -> env -> evar_map ->
+val second_order_matching : TransparentState.t -> env -> evar_map ->
EConstr.existential -> occurrences option list -> constr -> evar_map * bool
(** Declare function to enforce evars resolution by using typing constraints *)
val set_solve_evars : (env -> evar_map -> constr -> evar_map * constr) -> unit
-type unify_fun = transparent_state ->
+type unify_fun = TransparentState.t ->
env -> evar_map -> conv_pb -> constr -> constr -> Evarsolve.unification_result
(** Override default [evar_conv_x] algorithm. *)
@@ -73,7 +72,7 @@ val evar_conv_x : unify_fun
(**/**)
(* For debugging *)
-val evar_eqappr_x : ?rhs_is_already_stuck:bool -> transparent_state * bool ->
+val evar_eqappr_x : ?rhs_is_already_stuck:bool -> TransparentState.t * bool ->
env -> evar_map ->
conv_pb -> state * Cst_stack.t -> state * Cst_stack.t ->
Evarsolve.unification_result
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 96213af9c6..4692fe0057 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -66,9 +66,9 @@ let refresh_universes ?(status=univ_rigid) ?(onlyalg=false) ?(refreshset=false)
if not onlyalg then refresh_sort status ~direction s
else t
| UnivFlexible alg ->
- if onlyalg && alg then
- (evdref := Evd.make_flexible_variable !evdref ~algebraic:false l; t)
- else t))
+ (if alg then
+ evdref := Evd.make_nonalgebraic_variable !evdref l);
+ t))
| Set when refreshset && not direction ->
(* Cannot make a universe "lower" than "Set",
only refreshing when we want higher universes. *)
diff --git a/pretyping/heads.ml b/pretyping/heads.ml
index a3e4eb8971..e533930267 100644
--- a/pretyping/heads.ml
+++ b/pretyping/heads.ml
@@ -26,9 +26,8 @@ open Context.Named.Declaration
the evaluation of [phi(0)] and the head of [h] is declared unknown). *)
type rigid_head_kind =
-| RigidParameter of Constant.t (* a Const without body *)
-| RigidVar of variable (* a Var without body *)
-| RigidType (* an inductive, a product or a sort *)
+| RigidParameter of Constant.t (* a Const without body. Module substitution may instantiate it with something else. *)
+| RigidOther (* a Var without body, inductive, product, sort, projection *)
type head_approximation =
| RigidHead of rigid_head_kind
@@ -77,7 +76,7 @@ let kind_of_head env t =
str "."))
| Construct _ | CoFix _ ->
if b then NotImmediatelyComputableHead else ConstructorHead
- | Sort _ | Ind _ | Prod _ -> RigidHead RigidType
+ | Sort _ | Ind _ | Prod _ -> RigidHead RigidOther
| Cast (c,_,_) -> aux k l c b
| Lambda (_,_,c) ->
begin match l with
@@ -89,9 +88,7 @@ let kind_of_head env t =
| LetIn _ -> assert false
| Meta _ | Evar _ -> NotImmediatelyComputableHead
| App (c,al) -> aux k (Array.to_list al @ l) c b
- | Proj (p,c) ->
- (try on_subterm k (c :: l) b (constant_head (Projection.constant p))
- with Not_found -> assert false)
+ | Proj (p,c) -> RigidHead RigidOther
| Case (_,_,c,_) -> aux k [] c true
| Fix ((i,j),_) ->
@@ -124,22 +121,16 @@ let kind_of_head env t =
(* FIXME: maybe change interface here *)
let compute_head = function
| EvalConstRef cst ->
- let env = Global.env() in
- let cb = Environ.lookup_constant cst env in
- let is_Def = function Declarations.Def _ -> true | _ -> false in
- let body =
- if not (Recordops.is_primitive_projection cst) && is_Def cb.Declarations.const_body
- then Global.body_of_constant cst else None
- in
- (match body with
- | None -> RigidHead (RigidParameter cst)
- | Some (c, _) -> kind_of_head env c)
+ let env = Global.env() in
+ let body = Environ.constant_opt_value_in env (cst,Univ.Instance.empty) in
+ (match body with
+ | None -> RigidHead (RigidParameter cst)
+ | Some c -> kind_of_head env c)
| EvalVarRef id ->
(match Global.lookup_named id with
| LocalDef (_,c,_) when not (Decls.variable_opacity id) ->
kind_of_head (Global.env()) c
- | _ ->
- RigidHead (RigidVar id))
+ | _ -> RigidHead RigidOther)
let is_rigid env t =
match kind_of_head env t with
diff --git a/pretyping/inferCumulativity.ml b/pretyping/inferCumulativity.ml
index 422a05c19a..9762d0f1d9 100644
--- a/pretyping/inferCumulativity.ml
+++ b/pretyping/inferCumulativity.ml
@@ -188,7 +188,7 @@ let infer_inductive env mie =
match mie.mind_entry_universes with
| Monomorphic_ind_entry _
| Polymorphic_ind_entry _ as univs -> univs
- | Cumulative_ind_entry cumi ->
+ | Cumulative_ind_entry (nas, cumi) ->
let uctx = CumulativityInfo.univ_context cumi in
let uarray = Instance.to_array @@ UContext.instance uctx in
let env = Environ.push_context uctx env in
@@ -207,6 +207,6 @@ let infer_inductive env mie =
entries
in
let variances = Array.map (fun u -> LMap.find u variances) uarray in
- Cumulative_ind_entry (CumulativityInfo.make (uctx, variances))
+ Cumulative_ind_entry (nas, CumulativityInfo.make (uctx, variances))
in
{ mie with mind_entry_universes = univs }
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index cba1533da5..8c57fc2375 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -193,7 +193,6 @@ type inference_hook = env -> evar_map -> Evar.t -> evar_map * constr
type inference_flags = {
use_typeclasses : bool;
solve_unification_constraints : bool;
- use_hook : inference_hook option;
fail_evar : bool;
expand_evars : bool
}
@@ -247,14 +246,14 @@ let apply_typeclasses env sigma frozen fail_evar =
else sigma in
sigma
-let apply_inference_hook hook sigma frozen = match frozen with
+let apply_inference_hook hook env sigma frozen = match frozen with
| FrozenId _ -> sigma
| FrozenProgress (lazy (_, pending)) ->
Evar.Set.fold (fun evk sigma ->
if Evd.is_undefined sigma evk (* in particular not defined by side-effect *)
then
try
- let sigma, c = hook sigma evk in
+ let sigma, c = hook env sigma evk in
Evd.define evk c sigma
with Exit ->
sigma
@@ -307,16 +306,16 @@ let check_evars_are_solved env sigma frozen =
(* Try typeclasses, hooks, unification heuristics ... *)
-let solve_remaining_evars flags env sigma init_sigma =
+let solve_remaining_evars ?hook flags env sigma init_sigma =
let frozen = frozen_and_pending_holes (init_sigma, sigma) in
let sigma =
if flags.use_typeclasses
then apply_typeclasses env sigma frozen false
else sigma
in
- let sigma = if Option.has_some flags.use_hook
- then apply_inference_hook (Option.get flags.use_hook env) sigma frozen
- else sigma
+ let sigma = match hook with
+ | None -> sigma
+ | Some hook -> apply_inference_hook hook env sigma frozen
in
let sigma = if flags.solve_unification_constraints
then apply_heuristics env sigma false
@@ -1075,14 +1074,12 @@ let ise_pretype_gen flags env sigma lvar kind c =
let default_inference_flags fail = {
use_typeclasses = true;
solve_unification_constraints = true;
- use_hook = None;
fail_evar = fail;
expand_evars = true }
let no_classes_no_fail_inference_flags = {
use_typeclasses = false;
solve_unification_constraints = true;
- use_hook = None;
fail_evar = false;
expand_evars = true }
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 0f95d27528..2eaa77b822 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -35,7 +35,6 @@ type inference_hook = env -> evar_map -> Evar.t -> evar_map * constr
type inference_flags = {
use_typeclasses : bool;
solve_unification_constraints : bool;
- use_hook : inference_hook option;
fail_evar : bool;
expand_evars : bool
}
@@ -95,7 +94,7 @@ val understand : ?flags:inference_flags -> ?expected_type:typing_constraint ->
with candidate and no other conversion problems that the one in
[pending], however, it can contain more evars than the pending ones. *)
-val solve_remaining_evars : inference_flags ->
+val solve_remaining_evars : ?hook:inference_hook -> inference_flags ->
env -> (* current map *) evar_map -> (* initial map *) evar_map -> evar_map
(** Checking evars and pending conversion problems are all solved,
diff --git a/pretyping/recordops.ml b/pretyping/recordops.ml
index 4faa753dfb..fe9b69dbbc 100644
--- a/pretyping/recordops.ml
+++ b/pretyping/recordops.ml
@@ -106,16 +106,16 @@ let find_projection = function
let prim_table =
Summary.ref (Cmap_env.empty : Projection.Repr.t Cmap_env.t) ~name:"record-prim-projs"
-let load_prim i (_,p) =
- prim_table := Cmap_env.add (Projection.Repr.constant p) p !prim_table
+let load_prim i (_,(p,c)) =
+ prim_table := Cmap_env.add c p !prim_table
let cache_prim p = load_prim 1 p
-let subst_prim (subst,p) = subst_proj_repr subst p
+let subst_prim (subst,(p,c)) = subst_proj_repr subst p, subst_constant subst c
-let discharge_prim (_,p) = Some (Lib.discharge_proj_repr p)
+let discharge_prim (_,(p,c)) = Some (Lib.discharge_proj_repr p, c)
-let inPrim : Projection.Repr.t -> obj =
+let inPrim : (Projection.Repr.t * Constant.t) -> obj =
declare_object {
(default_object "PRIMPROJS") with
cache_function = cache_prim ;
@@ -124,7 +124,7 @@ let inPrim : Projection.Repr.t -> obj =
classify_function = (fun x -> Substitute x);
discharge_function = discharge_prim }
-let declare_primitive_projection p = Lib.add_anonymous_leaf (inPrim p)
+let declare_primitive_projection p c = Lib.add_anonymous_leaf (inPrim (p,c))
let is_primitive_projection c = Cmap_env.mem c !prim_table
diff --git a/pretyping/recordops.mli b/pretyping/recordops.mli
index 415b964168..3e43372b65 100644
--- a/pretyping/recordops.mli
+++ b/pretyping/recordops.mli
@@ -45,7 +45,7 @@ val find_projection_nparams : GlobRef.t -> int
val find_projection : GlobRef.t -> struc_typ
(** Sets up the mapping from constants to primitive projections *)
-val declare_primitive_projection : Projection.Repr.t -> unit
+val declare_primitive_projection : Projection.Repr.t -> Constant.t -> unit
val is_primitive_projection : Constant.t -> bool
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 17003cd1dd..e632976ae5 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -675,10 +675,6 @@ let apply_subst recfun env sigma refold cst_l t stack =
let stacklam recfun env sigma t stack =
apply_subst (fun _ _ s -> recfun s) env sigma false Cst_stack.empty t stack
-let beta_app sigma (c,l) =
- let zip s = Stack.zip sigma s in
- stacklam zip [] sigma c (Stack.append_app l Stack.empty)
-
let beta_applist sigma (c,l) =
let zip s = Stack.zip sigma s in
stacklam zip [] sigma c (Stack.append_app_list l Stack.empty)
@@ -1305,13 +1301,13 @@ let test_trans_conversion (f: constr Reduction.extended_conversion_function) red
with Reduction.NotConvertible -> false
| e when is_anomaly e -> report_anomaly e
-let is_conv ?(reds=full_transparent_state) env sigma = test_trans_conversion f_conv reds env sigma
-let is_conv_leq ?(reds=full_transparent_state) env sigma = test_trans_conversion f_conv_leq reds env sigma
-let is_fconv ?(reds=full_transparent_state) = function
+let is_conv ?(reds=TransparentState.full) env sigma = test_trans_conversion f_conv reds env sigma
+let is_conv_leq ?(reds=TransparentState.full) env sigma = test_trans_conversion f_conv_leq reds env sigma
+let is_fconv ?(reds=TransparentState.full) = function
| Reduction.CONV -> is_conv ~reds
| Reduction.CUMUL -> is_conv_leq ~reds
-let check_conv ?(pb=Reduction.CUMUL) ?(ts=full_transparent_state) env sigma x y =
+let check_conv ?(pb=Reduction.CUMUL) ?(ts=TransparentState.full) env sigma x y =
let f = match pb with
| Reduction.CONV -> f_conv
| Reduction.CUMUL -> f_conv_leq
@@ -1345,7 +1341,7 @@ let sigma_univ_state =
compare_cumul_instances = sigma_check_inductive_instances; }
let infer_conv_gen conv_fun ?(catch_incon=true) ?(pb=Reduction.CUMUL)
- ?(ts=full_transparent_state) env sigma x y =
+ ?(ts=TransparentState.full) env sigma x y =
(** FIXME *)
try
let ans = match pb with
@@ -1378,7 +1374,7 @@ let infer_conv = infer_conv_gen (fun pb ~l2r sigma ->
Reduction.generic_conv pb ~l2r (safe_evar_value sigma))
(* This reference avoids always having to link C code with the kernel *)
-let vm_infer_conv = ref (infer_conv ~catch_incon:true ~ts:full_transparent_state)
+let vm_infer_conv = ref (infer_conv ~catch_incon:true ~ts:TransparentState.full)
let set_vm_infer_conv f = vm_infer_conv := f
let vm_infer_conv ?(pb=Reduction.CUMUL) env t1 t2 =
!vm_infer_conv ~pb env t1 t2
@@ -1681,25 +1677,6 @@ let meta_reducible_instance evd b =
if Metaset.is_empty fm then (* nf_betaiota? *) b.rebus
else irec b.rebus
-
-let head_unfold_under_prod ts env sigma c =
- let unfold (cst,u) =
- let cstu = (cst, EInstance.kind sigma u) in
- if Cpred.mem cst (snd ts) then
- match constant_opt_value_in env cstu with
- | Some c -> EConstr.of_constr c
- | None -> mkConstU (cst, u)
- else mkConstU (cst, u) in
- let rec aux c =
- match EConstr.kind sigma c with
- | Prod (n,t,c) -> mkProd (n,aux t, aux c)
- | _ ->
- let (h,l) = decompose_app_vect sigma c in
- match EConstr.kind sigma h with
- | Const cst -> beta_app sigma (unfold cst, l)
- | _ -> c in
- aux c
-
let betazetaevar_applist sigma n c l =
let rec stacklam n env t stack =
if Int.equal n 0 then applist (substl env t, stack) else
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 41de779414..088e898a99 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -266,21 +266,21 @@ type conversion_test = Constraint.t -> Constraint.t
val pb_is_equal : conv_pb -> bool
val pb_equal : conv_pb -> conv_pb
-val is_conv : ?reds:transparent_state -> env -> evar_map -> constr -> constr -> bool
-val is_conv_leq : ?reds:transparent_state -> env -> evar_map -> constr -> constr -> bool
-val is_fconv : ?reds:transparent_state -> conv_pb -> env -> evar_map -> constr -> constr -> bool
+val is_conv : ?reds:TransparentState.t -> env -> evar_map -> constr -> constr -> bool
+val is_conv_leq : ?reds:TransparentState.t -> env -> evar_map -> constr -> constr -> bool
+val is_fconv : ?reds:TransparentState.t -> conv_pb -> env -> evar_map -> constr -> constr -> bool
(** [check_conv] Checks universe constraints only.
pb defaults to CUMUL and ts to a full transparent state.
*)
-val check_conv : ?pb:conv_pb -> ?ts:transparent_state -> env -> evar_map -> constr -> constr -> bool
+val check_conv : ?pb:conv_pb -> ?ts:TransparentState.t -> env -> evar_map -> constr -> constr -> bool
(** [infer_conv] Adds necessary universe constraints to the evar map.
pb defaults to CUMUL and ts to a full transparent state.
@raise UniverseInconsistency iff catch_incon is set to false,
otherwise returns false in that case.
*)
-val infer_conv : ?catch_incon:bool -> ?pb:conv_pb -> ?ts:transparent_state ->
+val infer_conv : ?catch_incon:bool -> ?pb:conv_pb -> ?ts:TransparentState.t ->
env -> evar_map -> constr -> constr -> evar_map option
(** Conversion with inference of universe constraints *)
@@ -292,9 +292,9 @@ val vm_infer_conv : ?pb:conv_pb -> env -> evar_map -> constr -> constr ->
(** [infer_conv_gen] behaves like [infer_conv] but is parametrized by a
conversion function. Used to pretype vm and native casts. *)
-val infer_conv_gen : (conv_pb -> l2r:bool -> evar_map -> transparent_state ->
+val infer_conv_gen : (conv_pb -> l2r:bool -> evar_map -> TransparentState.t ->
(Constr.constr, evar_map) Reduction.generic_conversion_function) ->
- ?catch_incon:bool -> ?pb:conv_pb -> ?ts:transparent_state -> env ->
+ ?catch_incon:bool -> ?pb:conv_pb -> ?ts:TransparentState.t -> env ->
evar_map -> constr -> constr -> evar_map option
(** {6 Special-Purpose Reduction Functions } *)
@@ -302,13 +302,12 @@ val infer_conv_gen : (conv_pb -> l2r:bool -> evar_map -> transparent_state ->
val whd_meta : local_reduction_function
val plain_instance : evar_map -> constr Metamap.t -> constr -> constr
val instance : evar_map -> constr Metamap.t -> constr -> constr
-val head_unfold_under_prod : transparent_state -> reduction_function
val betazetaevar_applist : evar_map -> int -> constr -> constr list -> constr
(** {6 Heuristic for Conversion with Evar } *)
val whd_betaiota_deltazeta_for_iota_state :
- transparent_state -> Environ.env -> Evd.evar_map -> Cst_stack.t -> state ->
+ TransparentState.t -> Environ.env -> Evd.evar_map -> Cst_stack.t -> state ->
state * Cst_stack.t
(** {6 Meta-related reduction functions } *)
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 4ec8569dd8..d9df8c8cf8 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -638,7 +638,7 @@ let whd_nothing_for_iota env sigma s =
| Meta ev ->
(try whrec (Evd.meta_value sigma ev, stack)
with Not_found -> s)
- | Const (const, u) when is_transparent_constant full_transparent_state const ->
+ | Const (const, u) ->
let u = EInstance.kind sigma u in
(match constant_opt_value_in env (const, u) with
| Some body -> whrec (EConstr.of_constr body, stack)
diff --git a/pretyping/typeclasses.mli b/pretyping/typeclasses.mli
index ee9c83dad3..8bdac0a575 100644
--- a/pretyping/typeclasses.mli
+++ b/pretyping/typeclasses.mli
@@ -119,8 +119,8 @@ val resolve_one_typeclass : ?unique:bool -> env -> evar_map -> EConstr.types ->
val set_typeclass_transparency_hook : (evaluable_global_reference -> bool (*local?*) -> bool -> unit) Hook.t
val set_typeclass_transparency : evaluable_global_reference -> bool -> bool -> unit
-val classes_transparent_state_hook : (unit -> transparent_state) Hook.t
-val classes_transparent_state : unit -> transparent_state
+val classes_transparent_state_hook : (unit -> TransparentState.t) Hook.t
+val classes_transparent_state : unit -> TransparentState.t
val add_instance_hint_hook :
(global_reference_or_constr -> GlobRef.t list ->
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index e3b942b610..490d58fa52 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -149,7 +149,7 @@ let abstract_list_all_with_dependencies env evd typ c l =
let n = List.length l in
let argoccs = set_occurrences_of_last_arg (Array.sub (snd ev') 0 n) in
let evd,b =
- Evarconv.second_order_matching empty_transparent_state
+ Evarconv.second_order_matching TransparentState.empty
env evd ev' argoccs c in
if b then
let p = nf_evar evd ev in
@@ -247,7 +247,7 @@ let sort_eqns = unify_r2l
*)
type core_unify_flags = {
- modulo_conv_on_closed_terms : Names.transparent_state option;
+ modulo_conv_on_closed_terms : TransparentState.t option;
(* What this flag controls was activated with all constants transparent, *)
(* even for auto, since Coq V5.10 *)
@@ -257,11 +257,11 @@ type core_unify_flags = {
use_evars_eagerly_in_conv_on_closed_terms : bool;
- modulo_delta : Names.transparent_state;
+ modulo_delta : TransparentState.t;
(* This controls which constants are unfoldable; this is on for apply *)
(* (but not simple apply) since Feb 2008 for 8.2 *)
- modulo_delta_types : Names.transparent_state;
+ modulo_delta_types : TransparentState.t;
check_applied_meta_types : bool;
(* This controls whether meta's applied to arguments have their *)
@@ -322,7 +322,7 @@ type unify_flags = {
(* Default flag for unifying a type against a type (e.g. apply) *)
(* We set all conversion flags (no flag should be modified anymore) *)
let default_core_unify_flags () =
- let ts = Names.full_transparent_state in {
+ let ts = TransparentState.full in {
modulo_conv_on_closed_terms = Some ts;
use_metas_eagerly_in_conv_on_closed_terms = true;
use_evars_eagerly_in_conv_on_closed_terms = false;
@@ -344,14 +344,14 @@ let default_unify_flags () =
let flags = default_core_unify_flags () in {
core_unify_flags = flags;
merge_unify_flags = flags;
- subterm_unify_flags = { flags with modulo_delta = var_full_transparent_state };
+ subterm_unify_flags = { flags with modulo_delta = TransparentState.var_full };
allow_K_in_toplevel_higher_order_unification = false; (* Why not? *)
resolve_evars = false
}
let set_no_delta_core_flags flags = { flags with
modulo_conv_on_closed_terms = None;
- modulo_delta = empty_transparent_state;
+ modulo_delta = TransparentState.empty;
check_applied_meta_types = false;
use_pattern_unification = false;
use_meta_bound_pattern_unification = true;
@@ -370,7 +370,7 @@ let set_no_delta_flags flags = {
(* For the first phase of keyed unification, restrict
to conversion (including beta-iota) only on closed terms *)
let set_no_delta_open_core_flags flags = { flags with
- modulo_delta = empty_transparent_state;
+ modulo_delta = TransparentState.empty;
modulo_betaiota = false;
}
@@ -388,7 +388,7 @@ let set_no_delta_open_flags flags = {
(* We set only the flags available at the time the new "apply" extended *)
(* out of "simple apply" *)
let default_no_delta_core_unify_flags () = { (default_core_unify_flags ()) with
- modulo_delta = empty_transparent_state;
+ modulo_delta = TransparentState.empty;
check_applied_meta_types = false;
use_pattern_unification = false;
use_meta_bound_pattern_unification = true;
@@ -425,7 +425,7 @@ let elim_flags_evars sigma =
let flags = elim_core_flags sigma in {
core_unify_flags = flags;
merge_unify_flags = flags;
- subterm_unify_flags = { flags with modulo_delta = empty_transparent_state };
+ subterm_unify_flags = { flags with modulo_delta = TransparentState.empty };
allow_K_in_toplevel_higher_order_unification = true;
resolve_evars = false
}
@@ -433,7 +433,7 @@ let elim_flags_evars sigma =
let elim_flags () = elim_flags_evars Evd.empty
let elim_no_delta_core_flags () = { (elim_core_flags Evd.empty) with
- modulo_delta = empty_transparent_state;
+ modulo_delta = TransparentState.empty;
check_applied_meta_types = false;
use_pattern_unification = false;
modulo_betaiota = false;
@@ -504,16 +504,16 @@ let key_of env sigma b flags f =
if subterm_restriction b flags then None else
match EConstr.kind sigma f with
| Const (cst, u) when is_transparent env (ConstKey cst) &&
- (Cpred.mem cst (snd flags.modulo_delta)
+ (TransparentState.is_transparent_constant flags.modulo_delta cst
|| Recordops.is_primitive_projection cst) ->
let u = EInstance.kind sigma u in
Some (IsKey (ConstKey (cst, u)))
| Var id when is_transparent env (VarKey id) &&
- Id.Pred.mem id (fst flags.modulo_delta) ->
+ TransparentState.is_transparent_variable flags.modulo_delta id ->
Some (IsKey (VarKey id))
| Proj (p, c) when Projection.unfolded p
|| (is_transparent env (ConstKey (Projection.constant p)) &&
- (Cpred.mem (Projection.constant p) (snd flags.modulo_delta))) ->
+ (TransparentState.is_transparent_constant flags.modulo_delta (Projection.constant p))) ->
Some (IsProj (p, c))
| _ -> None
@@ -550,7 +550,7 @@ let oracle_order env cf1 cf2 =
let is_rigid_head sigma flags t =
match EConstr.kind sigma t with
- | Const (cst,u) -> not (Cpred.mem cst (snd flags.modulo_delta))
+ | Const (cst,u) -> not (TransparentState.is_transparent_constant flags.modulo_delta cst)
| Ind (i,u) -> true
| Construct _ -> true
| Fix _ | CoFix _ -> true
@@ -633,11 +633,11 @@ let rec is_neutral env sigma ts t =
| Const (c, u) ->
not (Environ.evaluable_constant c env) ||
not (is_transparent env (ConstKey c)) ||
- not (Cpred.mem c (snd ts))
+ not (TransparentState.is_transparent_constant ts c)
| Var id ->
not (Environ.evaluable_named id env) ||
not (is_transparent env (VarKey id)) ||
- not (Id.Pred.mem id (fst ts))
+ not (TransparentState.is_transparent_variable ts id)
| Rel n -> true
| Evar _ | Meta _ -> true
| Case (_, p, c, cl) -> is_neutral env sigma ts c
@@ -935,8 +935,8 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
let ty1 = get_type_of curenv ~lax:true sigma c1 in
let ty2 = get_type_of curenv ~lax:true sigma c2 in
unify_0_with_initial_metas substn true curenv cv_pb
- { flags with modulo_conv_on_closed_terms = Some full_transparent_state;
- modulo_delta = full_transparent_state;
+ { flags with modulo_conv_on_closed_terms = Some TransparentState.full;
+ modulo_delta = TransparentState.full;
modulo_eta = true;
modulo_betaiota = true }
ty1 ty2
@@ -1120,10 +1120,10 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
| Some sigma -> ans
| None ->
if (match flags.modulo_conv_on_closed_terms, flags.modulo_delta with
- | Some (cv_id, cv_k), (dl_id, dl_k) ->
- Id.Pred.subset dl_id cv_id && Cpred.subset dl_k cv_k
- | None,(dl_id, dl_k) ->
- Id.Pred.is_empty dl_id && Cpred.is_empty dl_k)
+ | Some cv, dl ->
+ let open TransparentState in
+ Id.Pred.subset dl.tr_var cv.tr_var && Cpred.subset dl.tr_cst cv.tr_cst
+ | None, dl -> TransparentState.is_empty dl)
then error_cannot_unify env sigma (m, n) else None
in
let a = match res with
@@ -1263,8 +1263,8 @@ let applyHead env evd n c =
let is_mimick_head sigma ts f =
match EConstr.kind sigma f with
- | Const (c,u) -> not (CClosure.is_transparent_constant ts c)
- | Var id -> not (CClosure.is_transparent_variable ts id)
+ | Const (c,u) -> not (TransparentState.is_transparent_constant ts c)
+ | Var id -> not (TransparentState.is_transparent_variable ts id)
| (Rel _|Construct _|Ind _) -> true
| _ -> false
@@ -1534,11 +1534,11 @@ let finish_evar_resolution ?(flags=Pretyping.all_and_fail_flags) env current_sig
(sigma, nf_evar sigma c)
let default_matching_core_flags sigma =
- let ts = Names.full_transparent_state in {
- modulo_conv_on_closed_terms = Some empty_transparent_state;
+ let ts = TransparentState.full in {
+ modulo_conv_on_closed_terms = Some TransparentState.empty;
use_metas_eagerly_in_conv_on_closed_terms = false;
use_evars_eagerly_in_conv_on_closed_terms = false;
- modulo_delta = empty_transparent_state;
+ modulo_delta = TransparentState.empty;
modulo_delta_types = ts;
check_applied_meta_types = true;
use_pattern_unification = false;
@@ -1550,7 +1550,7 @@ let default_matching_core_flags sigma =
}
let default_matching_merge_flags sigma =
- let ts = Names.full_transparent_state in
+ let ts = TransparentState.full in
let flags = default_matching_core_flags sigma in {
flags with
modulo_conv_on_closed_terms = Some ts;
@@ -1580,7 +1580,7 @@ let make_pattern_test from_prefix_of_ind is_correct_type env sigma (pending,c) =
if from_prefix_of_ind then
let flags = default_matching_flags pending in
{ flags with core_unify_flags = { flags.core_unify_flags with
- modulo_conv_on_closed_terms = Some Names.full_transparent_state;
+ modulo_conv_on_closed_terms = Some TransparentState.full;
restrict_conv_on_strict_subterms = true } }
else default_matching_flags pending in
let n = Array.length (snd (decompose_app_vect sigma c)) in
diff --git a/pretyping/unification.mli b/pretyping/unification.mli
index e2e261ae7a..a45b8f1dd8 100644
--- a/pretyping/unification.mli
+++ b/pretyping/unification.mli
@@ -8,18 +8,17 @@
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
-open Names
open Constr
open EConstr
open Environ
open Evd
type core_unify_flags = {
- modulo_conv_on_closed_terms : Names.transparent_state option;
+ modulo_conv_on_closed_terms : TransparentState.t option;
use_metas_eagerly_in_conv_on_closed_terms : bool;
use_evars_eagerly_in_conv_on_closed_terms : bool;
- modulo_delta : Names.transparent_state;
- modulo_delta_types : Names.transparent_state;
+ modulo_delta : TransparentState.t;
+ modulo_delta_types : TransparentState.t;
check_applied_meta_types : bool;
use_pattern_unification : bool;
use_meta_bound_pattern_unification : bool;
@@ -41,7 +40,7 @@ val default_core_unify_flags : unit -> core_unify_flags
val default_no_delta_core_unify_flags : unit -> core_unify_flags
val default_unify_flags : unit -> unify_flags
-val default_no_delta_unify_flags : transparent_state -> unify_flags
+val default_no_delta_unify_flags : TransparentState.t -> unify_flags
val elim_flags : unit -> unify_flags
val elim_no_delta_flags : unit -> unify_flags
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 16:54:51 +0000