aboutsummaryrefslogtreecommitdiff
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/constr_matching.ml2
-rw-r--r--pretyping/evarsolve.ml35
-rw-r--r--pretyping/nativenorm.ml8
-rw-r--r--pretyping/patternops.ml25
-rw-r--r--pretyping/patternops.mli2
-rw-r--r--pretyping/pretyping.ml9
-rw-r--r--pretyping/tacred.ml2
-rw-r--r--pretyping/unification.ml4
8 files changed, 74 insertions, 13 deletions
diff --git a/pretyping/constr_matching.ml b/pretyping/constr_matching.ml
index 9128d4042b..ddef1cee96 100644
--- a/pretyping/constr_matching.ml
+++ b/pretyping/constr_matching.ml
@@ -213,7 +213,7 @@ let matches_core env sigma convert allow_partial_app allow_bound_rels
let open EConstr in
let convref ref c =
match ref, EConstr.kind sigma c with
- | VarRef id, Var id' -> Names.id_eq id id'
+ | VarRef id, Var id' -> Names.Id.equal id id'
| ConstRef c, Const (c',_) -> Names.eq_constant c c'
| IndRef i, Ind (i', _) -> Names.eq_ind i i'
| ConstructRef c, Construct (c',u) -> Names.eq_constructor c c'
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index ad1409f5b1..b906c3b597 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -842,6 +842,25 @@ let rec find_solution_type evarenv = function
| (id,ProjectEvar _)::l -> find_solution_type evarenv l
| [] -> assert false
+let is_preferred_projection_over sign (id,p) (id',p') =
+ (* We give priority to projection of variables over instantiation of
+ an evar considering that the latter is a stronger decision which
+ may even procude an incorrect (ill-typed) solution *)
+ match p, p' with
+ | ProjectEvar _, ProjectVar -> false
+ | ProjectVar, ProjectEvar _ -> true
+ | _, _ ->
+ List.index Id.equal id sign < List.index Id.equal id' sign
+
+let choose_projection evi sols =
+ let sign = List.map get_id (evar_filtered_context evi) in
+ match sols with
+ | y::l ->
+ List.fold_right (fun (id,p as x) (id',_ as y) ->
+ if is_preferred_projection_over sign x y then x else y)
+ l y
+ | _ -> assert false
+
(* In case the solution to a projection problem requires the instantiation of
* subsidiary evars, [do_projection_effects] performs them; it
* also try to instantiate the type of those subsidiary evars if their
@@ -1002,7 +1021,7 @@ let closure_of_filter evd evk = function
| Some filter ->
let evi = Evd.find_undefined evd evk in
let vars = collect_vars evd (EConstr.of_constr (evar_concl evi)) in
- let test b decl = b || Idset.mem (get_id decl) vars ||
+ let test b decl = b || Id.Set.mem (get_id decl) vars ||
match decl with
| LocalAssum _ ->
false
@@ -1429,8 +1448,12 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs =
let c, p = match sols with
| [] -> raise Not_found
| [id,p] -> (mkVar id, p)
- | (id,p)::_::_ ->
- if choose then (mkVar id, p) else raise (NotUniqueInType sols)
+ | _ ->
+ if choose then
+ let (id,p) = choose_projection evi sols in
+ (mkVar id, p)
+ else
+ raise (NotUniqueInType sols)
in
let ty = lazy (Retyping.get_type_of env !evdref (of_alias t)) in
let evd = do_projection_effects (evar_define conv_algo ~choose) env ty !evdref p in
@@ -1551,19 +1574,19 @@ let rec invert_definition conv_algo choose env evd pbty (evk,argsv as ev) rhs =
let rhs = whd_beta evd rhs (* heuristic *) in
let fast rhs =
let filter_ctxt = evar_filtered_context evi in
- let names = ref Idset.empty in
+ let names = ref Id.Set.empty in
let rec is_id_subst ctxt s =
match ctxt, s with
| (decl :: ctxt'), (c :: s') ->
let id = get_id decl in
- names := Idset.add id !names;
+ names := Id.Set.add id !names;
isVarId evd id c && is_id_subst ctxt' s'
| [], [] -> true
| _ -> false
in
is_id_subst filter_ctxt (Array.to_list argsv) &&
closed0 evd rhs &&
- Idset.subset (collect_vars evd rhs) !names
+ Id.Set.subset (collect_vars evd rhs) !names
in
let body =
if fast rhs then EConstr.of_constr (EConstr.to_constr evd rhs) (** FIXME? *)
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index 1038945c18..fe134f5126 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -88,7 +88,7 @@ let invert_tag cst tag reloc_tbl =
let decompose_prod env t =
let (name,dom,codom as res) = destProd (whd_all env t) in
match name with
- | Anonymous -> (Name (id_of_string "x"),dom,codom)
+ | Anonymous -> (Name (Id.of_string "x"),dom,codom)
| _ -> res
let app_type env c =
@@ -321,7 +321,7 @@ and nf_atom_type env sigma atom =
mkCase(ci, p, a, branchs), tcase
| Afix(tt,ft,rp,s) ->
let tt = Array.map (fun t -> nf_type env sigma t) tt in
- let name = Array.map (fun _ -> (Name (id_of_string "Ffix"))) tt in
+ let name = Array.map (fun _ -> (Name (Id.of_string "Ffix"))) tt in
let lvl = nb_rel env in
let nbfix = Array.length ft in
let fargs = mk_rels_accu lvl (Array.length ft) in
@@ -334,7 +334,7 @@ and nf_atom_type env sigma atom =
mkFix((rp,s),(name,tt,ft)), tt.(s)
| Acofix(tt,ft,s,_) | Acofixe(tt,ft,s,_) ->
let tt = Array.map (nf_type env sigma) tt in
- let name = Array.map (fun _ -> (Name (id_of_string "Fcofix"))) tt in
+ let name = Array.map (fun _ -> (Name (Id.of_string "Fcofix"))) tt in
let lvl = nb_rel env in
let fargs = mk_rels_accu lvl (Array.length ft) in
let env = push_rec_types (name,tt,[||]) env in
@@ -376,7 +376,7 @@ and nf_predicate env sigma ind mip params v pT =
| Vfun f, _ ->
let k = nb_rel env in
let vb = f (mk_rel_accu k) in
- let name = Name (id_of_string "c") in
+ let name = Name (Id.of_string "c") in
let n = mip.mind_nrealargs in
let rargs = Array.init n (fun i -> mkRel (n-i)) in
let params = if Int.equal n 0 then params else Array.map (lift n) params in
diff --git a/pretyping/patternops.ml b/pretyping/patternops.ml
index 3b3ad021e4..aaa9467068 100644
--- a/pretyping/patternops.ml
+++ b/pretyping/patternops.ml
@@ -96,6 +96,31 @@ let rec occur_meta_pattern = function
| PMeta _ | PSoApp _ -> true
| PEvar _ | PVar _ | PRef _ | PRel _ | PSort _ | PFix _ | PCoFix _ -> false
+let rec occurn_pattern n = function
+ | PRel p -> Int.equal n p
+ | PApp (f,args) ->
+ (occurn_pattern n f) || (Array.exists (occurn_pattern n) args)
+ | PProj (_,arg) -> occurn_pattern n arg
+ | PLambda (na,t,c) -> (occurn_pattern n t) || (occurn_pattern (n+1) c)
+ | PProd (na,t,c) -> (occurn_pattern n t) || (occurn_pattern (n+1) c)
+ | PLetIn (na,b,t,c) ->
+ Option.fold_left (fun b t -> b || occurn_pattern n t) (occurn_pattern n b) t ||
+ (occurn_pattern (n+1) c)
+ | PIf (c,c1,c2) ->
+ (occurn_pattern n c) ||
+ (occurn_pattern n c1) || (occurn_pattern n c2)
+ | PCase(_,p,c,br) ->
+ (occurn_pattern n p) ||
+ (occurn_pattern n c) ||
+ (List.exists (fun (_,_,p) -> occurn_pattern n p) br)
+ | PMeta _ | PSoApp _ -> true
+ | PEvar (_,args) -> Array.exists (occurn_pattern n) args
+ | PVar _ | PRef _ | PSort _ -> false
+ | PFix fix -> not (noccurn n (mkFix fix))
+ | PCoFix cofix -> not (noccurn n (mkCoFix cofix))
+
+let noccurn_pattern n c = not (occurn_pattern n c)
+
exception BoundPattern;;
let rec head_pattern_bound t =
diff --git a/pretyping/patternops.mli b/pretyping/patternops.mli
index ffe0186af0..2d1ce1dbc9 100644
--- a/pretyping/patternops.mli
+++ b/pretyping/patternops.mli
@@ -22,6 +22,8 @@ val occur_meta_pattern : constr_pattern -> bool
val subst_pattern : substitution -> constr_pattern -> constr_pattern
+val noccurn_pattern : int -> constr_pattern -> bool
+
exception BoundPattern
(** [head_pattern_bound t] extracts the head variable/constant of the
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 30783bfad5..b2b583ba74 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -202,7 +202,7 @@ let interp_universe_level_name ~anon_rigidity evd (loc, s) =
with Not_found ->
try
let id = try Id.of_string s with _ -> raise Not_found in
- evd, snd (Idmap.find id names)
+ evd, snd (Id.Map.find id names)
with Not_found ->
if not (is_strict_universe_declarations ()) then
new_univ_level_variable ?loc ~name:s univ_rigid evd
@@ -888,6 +888,9 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
| [], [] -> []
| _ -> assert false
in aux 1 1 (List.rev nal) cs.cs_args, true in
+ let fsign = if Flags.version_strictly_greater Flags.V8_6 || Flags.version_less_or_equal Flags.VOld
+ then Context.Rel.map (whd_betaiota !evdref) fsign
+ else fsign (* beta-iota-normalization regression in 8.5 and 8.6 *) in
let obj ind p v f =
if not record then
let nal = List.map (fun na -> ltac_interp_name lvar na) nal in
@@ -997,6 +1000,10 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
let pi = lift n pred in (* liftn n 2 pred ? *)
let pi = beta_applist !evdref (pi, [EConstr.of_constr (build_dependent_constructor cs)]) in
let cs_args = List.map (fun d -> map_rel_decl EConstr.of_constr d) cs.cs_args in
+ let cs_args =
+ if Flags.version_strictly_greater Flags.V8_6 || Flags.version_less_or_equal Flags.VOld
+ then Context.Rel.map (whd_betaiota !evdref) cs_args
+ else cs_args (* beta-iota-normalization regression in 8.5 and 8.6 *) in
let csgn =
List.map (set_name Anonymous) cs_args
in
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 708788ab87..9451b0f868 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -1051,7 +1051,7 @@ let contextually byhead occs f env sigma t =
let match_constr_evaluable_ref sigma c evref =
match EConstr.kind sigma c, evref with
| Const (c,u), EvalConstRef c' when eq_constant c c' -> Some u
- | Var id, EvalVarRef id' when id_eq id id' -> Some EInstance.empty
+ | Var id, EvalVarRef id' when Id.equal id id' -> Some EInstance.empty
| _, _ -> None
let substlin env sigma evalref n (nowhere_except_in,locs) c =
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index e8f7e2bbaf..86ebc1f01f 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -194,6 +194,10 @@ let pose_all_metas_as_evars env evd t =
let {rebus=ty;freemetas=mvs} = Evd.meta_ftype evd mv in
let ty = EConstr.of_constr ty in
let ty = if Evd.Metaset.is_empty mvs then ty else aux ty in
+ let ty =
+ if Flags.version_strictly_greater Flags.V8_6 || Flags.version_less_or_equal Flags.VOld
+ then nf_betaiota evd ty (* How it was in Coq <= 8.4 (but done in logic.ml at this time) *)
+ else ty (* some beta-iota-normalization "regression" in 8.5 and 8.6 *) in
let src = Evd.evar_source_of_meta mv !evdref in
let ev = Evarutil.e_new_evar env evdref ~src ty in
evdref := meta_assign mv (EConstr.Unsafe.to_constr ev,(Conv,TypeNotProcessed)) !evdref;
generated by cgit v1.2.3 (git 2.25.1) at 2026-04-29 12:02:14 +0000