aboutsummaryrefslogtreecommitdiff
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/cbv.ml6
-rw-r--r--pretyping/evarconv.ml52
-rw-r--r--pretyping/evarconv.mli4
-rw-r--r--pretyping/evarsolve.ml63
-rw-r--r--pretyping/evarsolve.mli28
-rw-r--r--pretyping/globEnv.ml8
-rw-r--r--pretyping/reductionops.ml31
-rw-r--r--pretyping/reductionops.mli10
-rw-r--r--pretyping/tacred.ml19
-rw-r--r--pretyping/typeclasses.ml3
-rw-r--r--pretyping/unification.ml15
-rw-r--r--pretyping/unification.mli6
-rw-r--r--pretyping/vnorm.ml2
13 files changed, 134 insertions, 113 deletions
diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml
index 2c7b689c04..2661000a39 100644
--- a/pretyping/cbv.ml
+++ b/pretyping/cbv.ml
@@ -397,6 +397,10 @@ and apply_env env t =
| _ ->
map_with_binders subs_lift apply_env env t
+let rec strip_app = function
+ | APP (args,st) -> APP (args,strip_app st)
+ | s -> TOP
+
(* The main recursive functions
*
* Go under applications and cases/projections (pushed in the stack),
@@ -442,7 +446,7 @@ let rec norm_head info env t stack =
| Const sp ->
Reductionops.reduction_effect_hook info.env info.sigma
- (fst sp) (lazy (reify_stack t stack));
+ (fst sp) (lazy (reify_stack t (strip_app stack)));
norm_head_ref 0 info env stack (ConstKey sp) t
| LetIn (_, b, _, c) ->
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 2feae8cc25..61453ff214 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -40,7 +40,7 @@ let default_transparent_state env = TransparentState.full
let default_flags_of ?(subterm_ts=TransparentState.empty) ts =
{ modulo_betaiota = true;
open_ts = ts; closed_ts = ts; subterm_ts;
- frozen_evars = Evar.Set.empty; with_cs = true;
+ allowed_evars = AllowedEvars.all; with_cs = true;
allow_K_at_toplevel = true }
let default_flags env =
@@ -118,8 +118,6 @@ type flex_kind_of_term =
| MaybeFlexible of EConstr.t (* reducible but not necessarily reduced *)
| Flexible of EConstr.existential
-let is_frozen flags (evk, _) = Evar.Set.mem evk flags.frozen_evars
-
let flex_kind_of_term flags env evd c sk =
match EConstr.kind evd c with
| LetIn _ | Rel _ | Const _ | Var _ | Proj _ ->
@@ -128,8 +126,7 @@ let flex_kind_of_term flags env evd c sk =
if flags.modulo_betaiota then MaybeFlexible c
else Rigid
| Evar ev ->
- if is_frozen flags ev then Rigid
- else Flexible ev
+ if is_evar_allowed flags (fst ev) then Flexible ev else Rigid
| Lambda _ | Prod _ | Sort _ | Ind _ | Construct _ | CoFix _ | Int _ | Float _ | Array _ -> Rigid
| Meta _ -> Rigid
| Fix _ -> Rigid (* happens when the fixpoint is partially applied *)
@@ -192,11 +189,11 @@ let occur_rigidly flags env evd (evk,_) t =
| Rigid _ as res -> res
| Normal b -> Reducible
| Reducible -> Reducible)
- | Evar (evk',l as ev) ->
+ | Evar (evk',l) ->
if Evar.equal evk evk' then Rigid true
- else if is_frozen flags ev then
- Rigid (List.exists (fun x -> rigid_normal_occ (aux x)) l)
- else Reducible
+ else if is_evar_allowed flags evk' then
+ Reducible
+ else Rigid (List.exists (fun x -> rigid_normal_occ (aux x)) l)
| Cast (p, _, _) -> aux p
| Lambda (na, t, b) -> aux b
| LetIn (na, _, _, b) -> aux b
@@ -458,7 +455,7 @@ let conv_fun f flags on_types =
let typefn env evd pbty term1 term2 =
let flags = { (default_flags env) with
with_cs = flags.with_cs;
- frozen_evars = flags.frozen_evars }
+ allowed_evars = flags.allowed_evars }
in f flags env evd pbty term1 term2
in
let termfn env evd pbty term1 term2 =
@@ -500,7 +497,7 @@ let rec evar_conv_x flags env evd pbty term1 term2 =
(whd_nored_state env evd (term2,Stack.empty))
in
begin match EConstr.kind evd term1, EConstr.kind evd term2 with
- | Evar ev, _ when Evd.is_undefined evd (fst ev) && not (is_frozen flags ev) ->
+ | Evar ev, _ when Evd.is_undefined evd (fst ev) && is_evar_allowed flags (fst ev) ->
(match solve_simple_eqn (conv_fun evar_conv_x) flags env evd
(position_problem true pbty,ev,term2) with
| UnifFailure (_,(OccurCheck _ | NotClean _)) ->
@@ -511,7 +508,7 @@ let rec evar_conv_x flags env evd pbty term1 term2 =
Miller patterns *)
default ()
| x -> x)
- | _, Evar ev when Evd.is_undefined evd (fst ev) && not (is_frozen flags ev) ->
+ | _, Evar ev when Evd.is_undefined evd (fst ev) && is_evar_allowed flags (fst ev) ->
(match solve_simple_eqn (conv_fun evar_conv_x) flags env evd
(position_problem false pbty,ev,term1) with
| UnifFailure (_, (OccurCheck _ | NotClean _)) ->
@@ -1206,14 +1203,14 @@ type occurrences_selection =
let default_occurrence_selection = Unspecified Abstraction.Imitate
-let default_occurrence_test ~frozen_evars ts _ origsigma _ env sigma _ c pat =
- let flags = { (default_flags_of ~subterm_ts:ts ts) with frozen_evars } in
+let default_occurrence_test ~allowed_evars ts _ origsigma _ env sigma _ c pat =
+ let flags = { (default_flags_of ~subterm_ts:ts ts) with allowed_evars } in
match evar_conv_x flags env sigma CONV c pat with
| Success sigma -> true, sigma
| UnifFailure _ -> false, sigma
-let default_occurrences_selection ?(frozen_evars=Evar.Set.empty) ts n =
- (default_occurrence_test ~frozen_evars ts,
+let default_occurrences_selection ?(allowed_evars=AllowedEvars.all) ts n =
+ (default_occurrence_test ~allowed_evars ts,
List.init n (fun _ -> default_occurrence_selection))
let apply_on_subterm env evd fixedref f test c t =
@@ -1352,9 +1349,8 @@ let second_order_matching flags env_rhs evd (evk,args) (test,argoccs) rhs =
(Feedback.msg_debug Pp.(str"env rhs: " ++ Termops.Internal.print_env env_rhs);
Feedback.msg_debug Pp.(str"env evars: " ++ Termops.Internal.print_env env_evar));
let args = List.map (nf_evar evd) args in
- let vars = List.map NamedDecl.get_id ctxt in
- let argsubst = List.map2 (fun id c -> (id, c)) vars args in
- let instance = List.map mkVar vars in
+ let argsubst = List.map2 (fun decl c -> (NamedDecl.get_id decl, c)) ctxt args in
+ let instance = evar_identity_subst evi in
let rhs = nf_evar evd rhs in
if not (noccur_evar env_rhs evd evk rhs) then raise (TypingFailed evd);
(* Ensure that any progress made by Typing.e_solve_evars will not contradict
@@ -1555,7 +1551,7 @@ let second_order_matching_with_args flags env evd with_ho pbty ev l t =
if with_ho then
let evd,ev = evar_absorb_arguments env evd ev (Array.to_list l) in
let argoccs = default_evar_selection flags evd ev in
- let test = default_occurrence_test ~frozen_evars:flags.frozen_evars flags.subterm_ts in
+ let test = default_occurrence_test ~allowed_evars:flags.allowed_evars flags.subterm_ts in
let evd, b =
try second_order_matching flags env evd ev (test,argoccs) t
with PretypeError (_, _, NoOccurrenceFound _) -> evd, false
@@ -1583,8 +1579,8 @@ let apply_conversion_problem_heuristic flags env evd with_ho pbty t1 t2 =
Termops.Internal.print_constr_env env evd t2 ++ cut ())) in
let app_empty = Array.is_empty l1 && Array.is_empty l2 in
match EConstr.kind evd term1, EConstr.kind evd term2 with
- | Evar (evk1,args1 as ev1), (Rel _|Var _) when app_empty
- && not (is_frozen flags ev1)
+ | Evar (evk1,args1), (Rel _|Var _) when app_empty
+ && is_evar_allowed flags evk1
&& List.for_all (fun a -> EConstr.eq_constr evd a term2 || isEvar evd a)
(remove_instance_local_defs evd evk1 args1) ->
(* The typical kind of constraint coming from pattern-matching return
@@ -1594,8 +1590,8 @@ let apply_conversion_problem_heuristic flags env evd with_ho pbty t1 t2 =
| None ->
let reason = ProblemBeyondCapabilities in
UnifFailure (evd, CannotSolveConstraint ((pbty,env,t1,t2),reason)))
- | (Rel _|Var _), Evar (evk2,args2 as ev2) when app_empty
- && not (is_frozen flags ev2)
+ | (Rel _|Var _), Evar (evk2,args2) when app_empty
+ && is_evar_allowed flags evk2
&& List.for_all (fun a -> EConstr.eq_constr evd a term1 || isEvar evd a)
(remove_instance_local_defs evd evk2 args2) ->
(* The typical kind of constraint coming from pattern-matching return
@@ -1621,24 +1617,24 @@ let apply_conversion_problem_heuristic flags env evd with_ho pbty t1 t2 =
(evar_define evar_unify flags ~choose:true)
evar_unify flags env evd
(position_problem true pbty) ev1 ev2)
- | Evar ev1,_ when not (is_frozen flags ev1) && Array.length l1 <= Array.length l2 ->
+ | Evar ev1,_ when is_evar_allowed flags (fst ev1) && Array.length l1 <= Array.length l2 ->
(* On "?n t1 .. tn = u u1 .. u(n+p)", try first-order unification *)
(* and otherwise second-order matching *)
ise_try evd
[(fun evd -> first_order_unification flags env evd (ev1,l1) appr2);
(fun evd ->
second_order_matching_with_args flags env evd with_ho pbty ev1 l1 t2)]
- | _,Evar ev2 when not (is_frozen flags ev2) && Array.length l2 <= Array.length l1 ->
+ | _,Evar ev2 when is_evar_allowed flags (fst ev2) && Array.length l2 <= Array.length l1 ->
(* On "u u1 .. u(n+p) = ?n t1 .. tn", try first-order unification *)
(* and otherwise second-order matching *)
ise_try evd
[(fun evd -> first_order_unification flags env evd (ev2,l2) appr1);
(fun evd ->
second_order_matching_with_args flags env evd with_ho pbty ev2 l2 t1)]
- | Evar ev1,_ when not (is_frozen flags ev1) ->
+ | Evar ev1,_ when is_evar_allowed flags (fst ev1) ->
(* Try second-order pattern-matching *)
second_order_matching_with_args flags env evd with_ho pbty ev1 l1 t2
- | _,Evar ev2 when not (is_frozen flags ev2) ->
+ | _,Evar ev2 when is_evar_allowed flags (fst ev2) ->
(* Try second-order pattern-matching *)
second_order_matching_with_args flags env evd with_ho pbty ev2 l2 t1
| _ ->
diff --git a/pretyping/evarconv.mli b/pretyping/evarconv.mli
index 767a173131..a5a8d1f916 100644
--- a/pretyping/evarconv.mli
+++ b/pretyping/evarconv.mli
@@ -105,11 +105,11 @@ val default_occurrence_selection : occurrence_selection
type occurrences_selection =
occurrence_match_test * occurrence_selection list
-val default_occurrence_test : frozen_evars:Evar.Set.t -> TransparentState.t -> occurrence_match_test
+val default_occurrence_test : allowed_evars:Evarsolve.AllowedEvars.t -> TransparentState.t -> occurrence_match_test
(** [default_occurrence_selection n]
Gives the default test and occurrences for [n] arguments *)
-val default_occurrences_selection : ?frozen_evars:Evar.Set.t (* By default, none *) ->
+val default_occurrences_selection : ?allowed_evars:Evarsolve.AllowedEvars.t (* By default, all *) ->
TransparentState.t -> int -> occurrences_selection
val second_order_matching : unify_flags -> env -> evar_map ->
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 79839099f7..4d5715a391 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -25,14 +25,43 @@ open Reductionops
open Evarutil
open Pretype_errors
+module AllowedEvars = struct
+
+ type t =
+ | AllowAll
+ | AllowFun of (Evar.t -> bool) * Evar.Set.t
+
+ let mem allowed evk =
+ match allowed with
+ | AllowAll -> true
+ | AllowFun (f,except) -> f evk && not (Evar.Set.mem evk except)
+
+ let remove evk = function
+ | AllowAll -> AllowFun ((fun _ -> true), Evar.Set.singleton evk)
+ | AllowFun (f,except) -> AllowFun (f, Evar.Set.add evk except)
+
+ let all = AllowAll
+
+ let except evars =
+ AllowFun ((fun _ -> true), evars)
+
+ let from_pred f =
+ AllowFun (f, Evar.Set.empty)
+
+end
+
type unify_flags = {
modulo_betaiota: bool;
open_ts : TransparentState.t;
closed_ts : TransparentState.t;
subterm_ts : TransparentState.t;
- frozen_evars : Evar.Set.t;
+ allowed_evars : AllowedEvars.t;
allow_K_at_toplevel : bool;
- with_cs : bool }
+ with_cs : bool
+}
+
+let is_evar_allowed flags evk =
+ AllowedEvars.mem flags.allowed_evars evk
type unification_kind =
| TypeUnification
@@ -216,9 +245,6 @@ type 'a update =
| UpdateWith of 'a
| NoUpdate
-open Context.Named.Declaration
-let inst_of_vars sign = List.map (get_id %> mkVar) sign
-
let restrict_evar_key evd evk filter candidates =
match filter, candidates with
| None, NoUpdate -> evd, evk
@@ -701,8 +727,7 @@ let define_evar_from_virtual_equation define_fun env evd src t_in_env ty_t_in_si
let (evd, evk) = new_pure_evar sign evd ty_t_in_sign ~filter ~src in
let t_in_env = whd_evar evd t_in_env in
let evd = define_fun env evd None (evk, inst_in_env) t_in_env in
- let ctxt = named_context_of_val sign in
- let inst_in_sign = inst_of_vars (Filter.filter_list filter ctxt) in
+ let inst_in_sign = evar_identity_subst (Evd.find evd evk) in
let evar_in_sign = mkEvar (evk, inst_in_sign) in
(evd,whd_evar evd evar_in_sign)
@@ -735,9 +760,8 @@ let materialize_evar define_fun env evd k (evk1,args1) ty_in_env =
let sign1 = evar_hyps evi1 in
let filter1 = evar_filter evi1 in
let src = subterm_source evk1 evi1.evar_source in
- let ids1 = List.map get_id (named_context_of_val sign1) in
let avoid = Environ.ids_of_named_context_val sign1 in
- let inst_in_sign = List.map mkVar (Filter.filter_list filter1 ids1) in
+ let inst_in_sign = evar_identity_subst evi1 in
let open Context.Rel.Declaration in
let (sign2,filter2,inst2_in_env,inst2_in_sign,_,evd,_) =
List.fold_right (fun d (sign,filter,inst_in_env,inst_in_sign,env,evd,avoid) ->
@@ -1312,24 +1336,24 @@ let preferred_orientation evd evk1 evk2 =
let solve_evar_evar_aux force f unify flags env evd pbty (evk1,args1 as ev1) (evk2,args2 as ev2) =
let aliases = make_alias_map env evd in
- let frozen_ev1 = Evar.Set.mem evk1 flags.frozen_evars in
- let frozen_ev2 = Evar.Set.mem evk2 flags.frozen_evars in
+ let allowed_ev1 = is_evar_allowed flags evk1 in
+ let allowed_ev2 = is_evar_allowed flags evk2 in
if preferred_orientation evd evk1 evk2 then
- try if not frozen_ev1 then
+ try if allowed_ev1 then
solve_evar_evar_l2r force f unify flags env evd aliases (opp_problem pbty) ev2 ev1
else raise (CannotProject (evd,ev2))
with CannotProject (evd,ev2) ->
- try if not frozen_ev2 then
+ try if allowed_ev2 then
solve_evar_evar_l2r force f unify flags env evd aliases pbty ev1 ev2
else raise (CannotProject (evd,ev1))
with CannotProject (evd,ev1) ->
add_conv_oriented_pb ~tail:true (pbty,env,mkEvar ev1,mkEvar ev2) evd
else
- try if not frozen_ev2 then
+ try if allowed_ev2 then
solve_evar_evar_l2r force f unify flags env evd aliases pbty ev1 ev2
else raise (CannotProject (evd,ev1))
with CannotProject (evd,ev1) ->
- try if not frozen_ev1 then
+ try if allowed_ev1 then
solve_evar_evar_l2r force f unify flags env evd aliases (opp_problem pbty) ev2 ev1
else raise (CannotProject (evd,ev2))
with CannotProject (evd,ev2) ->
@@ -1395,15 +1419,15 @@ let solve_refl ?(can_drop=false) unify flags env evd pbty evk argsv1 argsv2 =
let candidates = filter_candidates evd evk untypedfilter NoUpdate in
let filter = closure_of_filter evd evk untypedfilter in
let evd',ev1 = restrict_applied_evar evd (evk,argsv1) filter candidates in
- let frozen = Evar.Set.mem evk flags.frozen_evars in
- if Evar.equal (fst ev1) evk && (frozen || can_drop) then
+ let allowed = is_evar_allowed flags evk in
+ if Evar.equal (fst ev1) evk && (not allowed || can_drop) then
(* No refinement needed *) evd'
else
(* either progress, or not allowed to drop, e.g. to preserve possibly *)
(* informative equations such as ?e[x:=?y]=?e[x:=?y'] where we don't know *)
(* if e can depend on x until ?y is not resolved, or, conversely, we *)
(* don't know if ?y has to be unified with ?y, until e is resolved *)
- if frozen then
+ if not allowed then
(* We cannot prune a frozen evar *)
add_conv_oriented_pb (pbty,env,mkEvar (evk, argsv1),mkEvar (evk,argsv2)) evd
else
@@ -1460,7 +1484,8 @@ let occur_evar_upto_types sigma n c =
let instantiate_evar unify flags env evd evk body =
(* Check instance freezing the evar to be defined, as
checking could involve the same evar definition problem again otherwise *)
- let flags = { flags with frozen_evars = Evar.Set.add evk flags.frozen_evars } in
+ let allowed_evars = AllowedEvars.remove evk flags.allowed_evars in
+ let flags = { flags with allowed_evars } in
let evd' = check_evar_instance unify flags env evd evk body in
Evd.define evk body evd'
diff --git a/pretyping/evarsolve.mli b/pretyping/evarsolve.mli
index 3fb80432ad..8ff2d7fc63 100644
--- a/pretyping/evarsolve.mli
+++ b/pretyping/evarsolve.mli
@@ -16,6 +16,28 @@ type alias
val of_alias : alias -> EConstr.t
+module AllowedEvars : sig
+
+ type t
+ (** Represents the set of evars that can be defined by the pretyper *)
+
+ val all : t
+ (** All evars can be defined *)
+
+ val mem : t -> Evar.t -> bool
+ (** [mem allowed evk] is true iff evk can be defined *)
+
+ val from_pred : (Evar.t -> bool) -> t
+ (** [from_pred p] means evars satisfying p can be defined *)
+
+ val except : Evar.Set.t -> t
+ (** [except evars] means all evars can be defined except the ones in [evars] *)
+
+ val remove : Evar.t -> t -> t
+ (** [remove evk allowed] removes [evk] from the set of evars allowed by [allowed] *)
+
+end
+
type unify_flags = {
modulo_betaiota : bool;
(* Enable beta-iota reductions during unification *)
@@ -26,8 +48,8 @@ type unify_flags = {
subterm_ts : TransparentState.t;
(* Enable delta reduction according to subterm_ts for selection of subterms during higher-order
unifications. *)
- frozen_evars : Evar.Set.t;
- (* Frozen evars are treated like rigid variables during unification: they can not be instantiated. *)
+ allowed_evars : AllowedEvars.t;
+ (* Disallowed evars are treated like rigid variables during unification: they can not be instantiated. *)
allow_K_at_toplevel : bool;
(* During higher-order unifications, allow to produce K-redexes: i.e. to produce
an abstraction for an unused argument *)
@@ -41,6 +63,8 @@ type unification_result =
val is_success : unification_result -> bool
+val is_evar_allowed : unify_flags -> Evar.t -> bool
+
(** Replace the vars and rels that are aliases to other vars and rels by
their representative that is most ancient in the context *)
val expand_vars_in_term : env -> evar_map -> constr -> constr
diff --git a/pretyping/globEnv.ml b/pretyping/globEnv.ml
index 81a62a7048..34fae613bf 100644
--- a/pretyping/globEnv.ml
+++ b/pretyping/globEnv.ml
@@ -33,8 +33,6 @@ type t = {
(** For locating indices *)
renamed_env : env;
(** For name management *)
- renamed_vars : EConstr.t list Lazy.t;
- (** Identity instance of named_context of renamed_env, to maximize sharing *)
extra : ext_named_context Lazy.t;
(** Delay the computation of the evar extended environment *)
lvar : ltac_var_map;
@@ -45,11 +43,9 @@ let make ~hypnaming env sigma lvar =
let avoid = Environ.ids_of_named_context_val (Environ.named_context_val env) in
Context.Rel.fold_outside (fun d acc -> push_rel_decl_to_named_context ~hypnaming sigma d acc)
(rel_context env) ~init:(empty_csubst, avoid, named_context_val env) in
- let open Context.Named.Declaration in
{
static_env = env;
renamed_env = env;
- renamed_vars = lazy (List.map (get_id %> mkVar) (named_context env));
extra = lazy (get_extra env sigma);
lvar = lvar;
}
@@ -76,7 +72,6 @@ let push_rel ~hypnaming sigma d env =
let env = {
static_env = push_rel d env.static_env;
renamed_env = push_rel d' env.renamed_env;
- renamed_vars = env.renamed_vars;
extra = lazy (push_rel_decl_to_named_context ~hypnaming:hypnaming sigma d' (Lazy.force env.extra));
lvar = env.lvar;
} in
@@ -89,7 +84,6 @@ let push_rel_context ~hypnaming ?(force_names=false) sigma ctx env =
let env = {
static_env = push_rel_context ctx env.static_env;
renamed_env = push_rel_context ctx' env.renamed_env;
- renamed_vars = env.renamed_vars;
extra = lazy (List.fold_right (fun d acc -> push_rel_decl_to_named_context ~hypnaming:hypnaming sigma d acc) ctx' (Lazy.force env.extra));
lvar = env.lvar;
} in
@@ -102,7 +96,7 @@ let push_rec_types ~hypnaming sigma (lna,typarray) env =
Array.map get_annot ctx, env
let new_evar env sigma ?src ?naming typ =
- let lazy inst_vars = env.renamed_vars in
+ let inst_vars = EConstr.identity_subst_val (named_context_val env.renamed_env) in
let rec rel_list n accu =
if n <= 0 then accu
else rel_list (n - 1) (mkRel n :: accu)
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index fdc770dba6..aeb18ec322 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -499,13 +499,6 @@ let beta_applist sigma (c,l) =
(* Iota reduction tools *)
-type 'a miota_args = {
- mP : constr; (* the result type *)
- mconstr : constr; (* the constructor *)
- mci : case_info; (* special info to re-build pattern *)
- mcargs : 'a list; (* the constructor's arguments *)
- mlf : 'a array } (* the branch code vector *)
-
let reducible_mind_case sigma c = match EConstr.kind sigma c with
| Construct _ | CoFix _ -> true
| _ -> false
@@ -514,10 +507,7 @@ let contract_cofix sigma (bodynum,(names,types,bodies as typedbodies)) =
let nbodies = Array.length bodies in
let make_Fi j =
let ind = nbodies-j-1 in
- if Int.equal bodynum ind then mkCoFix (ind,typedbodies)
- else
- let bd = mkCoFix (ind,typedbodies) in
- bd
+ mkCoFix (ind,typedbodies)
in
let closure = List.init nbodies make_Fi in
substl closure bodies.(bodynum)
@@ -530,18 +520,6 @@ let reduce_and_refold_cofix recfun env sigma cofix sk =
(fun _ (t,sk') -> recfun (t,sk'))
[] sigma raw_answer sk
-let reduce_mind_case sigma mia =
- match EConstr.kind sigma mia.mconstr with
- | Construct ((ind_sp,i),u) ->
-(* let ncargs = (fst mia.mci).(i-1) in*)
- let real_cargs = List.skipn mia.mci.ci_npar mia.mcargs in
- applist (mia.mlf.(i-1),real_cargs)
- | CoFix cofix ->
- let cofix_def = contract_cofix sigma cofix in
- (* XXX Is NoInvert OK here? *)
- mkCase (mia.mci, mia.mP, NoInvert, applist(cofix_def,mia.mcargs), mia.mlf)
- | _ -> assert false
-
(* contracts fix==FIX[nl;i](A1...Ak;[F1...Fk]{B1....Bk}) to produce
Bi[Fj --> FIX[nl;j](A1...Ak;[F1...Fk]{B1...Bk})] *)
@@ -549,10 +527,7 @@ let contract_fix sigma ((recindices,bodynum),(names,types,bodies as typedbodies)
let nbodies = Array.length recindices in
let make_Fi j =
let ind = nbodies-j-1 in
- if Int.equal bodynum ind then mkFix ((recindices,ind),typedbodies)
- else
- let bd = mkFix ((recindices,ind),typedbodies) in
- bd
+ mkFix ((recindices,ind),typedbodies)
in
let closure = List.init nbodies make_Fi in
substl closure bodies.(bodynum)
@@ -757,7 +732,7 @@ let rec whd_state_gen flags env sigma =
| None -> fold ())
| Const (c,u as const) ->
reduction_effect_hook env sigma c
- (lazy (EConstr.to_constr sigma (Stack.zip sigma (x,stack))));
+ (lazy (EConstr.to_constr sigma (Stack.zip sigma (x,fst (Stack.strip_app stack)))));
if CClosure.RedFlags.red_set flags (CClosure.RedFlags.fCONST c) then
let u' = EInstance.kind sigma u in
match constant_value_in env (c, u') with
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index 0f288cdd46..d404a7e414 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -217,22 +217,14 @@ val splay_prod_n : env -> evar_map -> int -> constr -> rel_context * constr
val splay_lam_n : env -> evar_map -> int -> constr -> rel_context * constr
(** Raises [Invalid_argument] *)
-
-type 'a miota_args = {
- mP : constr; (** the result type *)
- mconstr : constr; (** the constructor *)
- mci : case_info; (** special info to re-build pattern *)
- mcargs : 'a list; (** the constructor's arguments *)
- mlf : 'a array } (** the branch code vector *)
-
val reducible_mind_case : evar_map -> constr -> bool
-val reduce_mind_case : evar_map -> constr miota_args -> constr
val find_conclusion : env -> evar_map -> constr -> (constr, constr, ESorts.t, EInstance.t) kind_of_term
val is_arity : env -> evar_map -> constr -> bool
val is_sort : env -> evar_map -> types -> bool
val contract_fix : evar_map -> fixpoint -> constr
+val contract_cofix : evar_map -> cofixpoint -> constr
(** {6 Querying the kernel conversion oracle: opaque/transparent constants } *)
val is_transparent : Environ.env -> Constant.t tableKey -> bool
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index e4b5dc1edf..9d15e98373 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -458,6 +458,25 @@ let contract_cofix_use_function env sigma f
substl_checking_arity env (List.rev subbodies)
sigma (nf_beta env sigma bodies.(bodynum))
+type 'a miota_args = {
+ mP : constr; (** the result type *)
+ mconstr : constr; (** the constructor *)
+ mci : case_info; (** special info to re-build pattern *)
+ mcargs : 'a list; (** the constructor's arguments *)
+ mlf : 'a array } (** the branch code vector *)
+
+let reduce_mind_case sigma mia =
+ match EConstr.kind sigma mia.mconstr with
+ | Construct ((ind_sp,i),u) ->
+(* let ncargs = (fst mia.mci).(i-1) in*)
+ let real_cargs = List.skipn mia.mci.ci_npar mia.mcargs in
+ applist (mia.mlf.(i-1),real_cargs)
+ | CoFix cofix ->
+ let cofix_def = contract_cofix sigma cofix in
+ (* XXX Is NoInvert OK here? *)
+ mkCase (mia.mci, mia.mP, NoInvert, applist(cofix_def,mia.mcargs), mia.mlf)
+ | _ -> assert false
+
let reduce_mind_case_use_function func env sigma mia =
match EConstr.kind sigma mia.mconstr with
| Construct ((ind_sp,i),u) ->
diff --git a/pretyping/typeclasses.ml b/pretyping/typeclasses.ml
index d1b65775bd..adb9c5299f 100644
--- a/pretyping/typeclasses.ml
+++ b/pretyping/typeclasses.ml
@@ -68,6 +68,7 @@ type typeclass = {
}
type typeclasses = typeclass GlobRef.Map.t
+(* Invariant: for any pair (gr, tc) in the map, gr and tc.cl_impl are equal *)
type instance = {
is_class: GlobRef.t;
@@ -268,7 +269,7 @@ let instances env sigma r =
let cl = class_info env sigma r in instances_of cl
let is_class gr =
- GlobRef.Map.exists (fun _ v -> GlobRef.equal v.cl_impl gr) !classes
+ GlobRef.Map.mem gr !classes
open Evar_kinds
type evar_filter = Evar.t -> Evar_kinds.t Lazy.t -> bool
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index a26c981cb9..207a03d80f 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -252,10 +252,6 @@ let unify_r2l x = x
let sort_eqns = unify_r2l
*)
-type allowed_evars =
-| AllowAll
-| AllowFun of (Evar.t -> bool)
-
type core_unify_flags = {
modulo_conv_on_closed_terms : TransparentState.t option;
(* What this flag controls was activated with all constants transparent, *)
@@ -289,7 +285,7 @@ type core_unify_flags = {
(* This allowed for instance to unify "forall x:?A, ?B x" with "A' -> B'" *)
(* when ?B is a Meta. *)
- allowed_evars : allowed_evars;
+ allowed_evars : AllowedEvars.t;
(* Evars that are allowed to be instantiated *)
(* Useful e.g. for autorewrite *)
@@ -341,7 +337,7 @@ let default_core_unify_flags () =
check_applied_meta_types = true;
use_pattern_unification = true;
use_meta_bound_pattern_unification = true;
- allowed_evars = AllowAll;
+ allowed_evars = AllowedEvars.all;
restrict_conv_on_strict_subterms = false;
modulo_betaiota = true;
modulo_eta = true;
@@ -421,7 +417,7 @@ let default_no_delta_unify_flags ts =
let allow_new_evars sigma =
let undefined = Evd.undefined_map sigma in
- AllowFun (fun evk -> not (Evar.Map.mem evk undefined))
+ AllowedEvars.from_pred (fun evk -> not (Evar.Map.mem evk undefined))
(* Default flags for looking for subterms in elimination tactics *)
(* Not used in practice at the current date, to the exception of *)
@@ -604,9 +600,8 @@ let do_reduce ts (env, nb) sigma c =
Stack.zip sigma (whd_betaiota_deltazeta_for_iota_state
ts env sigma (c, Stack.empty))
-let is_evar_allowed flags evk = match flags.allowed_evars with
-| AllowAll -> true
-| AllowFun f -> f evk
+let is_evar_allowed flags evk =
+ AllowedEvars.mem flags.allowed_evars evk
let isAllowedEvar sigma flags c = match EConstr.kind sigma c with
| Evar (evk,_) -> is_evar_allowed flags evk
diff --git a/pretyping/unification.mli b/pretyping/unification.mli
index f9a969a253..5462e09359 100644
--- a/pretyping/unification.mli
+++ b/pretyping/unification.mli
@@ -13,10 +13,6 @@ open EConstr
open Environ
open Evd
-type allowed_evars =
-| AllowAll
-| AllowFun of (Evar.t -> bool)
-
type core_unify_flags = {
modulo_conv_on_closed_terms : TransparentState.t option;
use_metas_eagerly_in_conv_on_closed_terms : bool;
@@ -26,7 +22,7 @@ type core_unify_flags = {
check_applied_meta_types : bool;
use_pattern_unification : bool;
use_meta_bound_pattern_unification : bool;
- allowed_evars : allowed_evars;
+ allowed_evars : Evarsolve.AllowedEvars.t;
restrict_conv_on_strict_subterms : bool;
modulo_betaiota : bool;
modulo_eta : bool;
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index e5fa9bada1..900ba0edb9 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -415,7 +415,7 @@ let cbv_vm env sigma c t =
(* This evar-normalizes terms beforehand *)
let c = EConstr.to_constr ~abort_on_undefined_evars:false sigma c in
let t = EConstr.to_constr ~abort_on_undefined_evars:false sigma t in
- let v = Csymtable.val_of_constr env c in
+ let v = Vmsymtable.val_of_constr env c in
EConstr.of_constr (nf_val env sigma v t)
let vm_infer_conv ?(pb=Reduction.CUMUL) env sigma t1 t2 =
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-01 19:14:58 +0000