aboutsummaryrefslogtreecommitdiff
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/cases.ml94
-rw-r--r--pretyping/evarconv.ml7
-rw-r--r--pretyping/evarsolve.ml2
-rw-r--r--pretyping/pretyping.ml6
-rw-r--r--pretyping/pretyping.mli4
-rw-r--r--pretyping/program.ml6
-rw-r--r--pretyping/retyping.mli2
-rw-r--r--pretyping/unification.ml9
8 files changed, 61 insertions, 69 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index e89c3ea719..98d3000885 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1870,22 +1870,16 @@ let inh_conv_coerce_to_tycon loc env evdref j tycon =
(* We put the tycon inside the arity signature, possibly discovering dependencies. *)
-let add_subst c len (rel_subst,var_subst) =
- match kind_of_term c with
- | Rel n -> (n,len) :: rel_subst, var_subst
- | Var id -> rel_subst, (id,len) :: var_subst
- | _ -> assert false
-
let prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign c =
let nar = List.fold_left (fun n sign -> Context.Rel.nhyps sign + n) 0 arsign in
- let (rel_subst,var_subst), len =
+ let subst, len =
List.fold_right2 (fun (tm, tmtype) sign (subst, len) ->
let signlen = List.length sign in
match kind_of_term tm with
- | Rel _ | Var _ when dependent tm c
+ | Rel n when dependent tm c
&& Int.equal signlen 1 (* The term to match is not of a dependent type itself *) ->
- (add_subst tm len subst, len - signlen)
- | Rel _ | Var _ when signlen > 1 (* The term is of a dependent type,
+ ((n, len) :: subst, len - signlen)
+ | Rel n when signlen > 1 (* The term is of a dependent type,
maybe some variable in its type appears in the tycon. *) ->
(match tmtype with
NotInd _ -> (subst, len - signlen)
@@ -1894,36 +1888,28 @@ let prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign c =
List.fold_left
(fun (subst, len) arg ->
match kind_of_term arg with
- | Rel _ | Var _ when dependent arg c ->
- (add_subst arg len subst, pred len)
+ | Rel n when dependent arg c ->
+ ((n, len) :: subst, pred len)
| _ -> (subst, pred len))
(subst, len) realargs
in
let subst =
- if dependent tm c && List.for_all (fun c -> isRel c || isVar c) realargs
- then add_subst tm len subst else subst
+ if dependent tm c && List.for_all isRel realargs
+ then (n, len) :: subst else subst
in (subst, pred len))
| _ -> (subst, len - signlen))
- (List.rev tomatchs) arsign (([],[]), nar)
+ (List.rev tomatchs) arsign ([], nar)
in
let rec predicate lift c =
match kind_of_term c with
| Rel n when n > lift ->
(try
(* Make the predicate dependent on the matched variable *)
- let idx = Int.List.assoc (n - lift) rel_subst in
+ let idx = Int.List.assoc (n - lift) subst in
mkRel (idx + lift)
with Not_found ->
- (* A variable that is not matched, lift over the arsign *)
+ (* A variable that is not matched, lift over the arsign. *)
mkRel (n + nar))
- | Var id ->
- (try
- (* Make the predicate dependent on the matched variable *)
- let idx = Id.List.assoc id var_subst in
- mkRel (idx + lift)
- with Not_found ->
- (* A variable that is not matched *)
- c)
| _ ->
map_constr_with_binders succ predicate lift c
in
@@ -1944,39 +1930,38 @@ let prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign c =
let prepare_predicate loc typing_fun env sigma tomatchs arsign tycon pred =
let preds =
- match pred with
+ match pred, tycon with
(* No return clause *)
- | None ->
- let sigma,t =
- match tycon with
- | Some t -> sigma, t
- | None ->
- (* No type constraint: we first create a generic evar type constraint *)
- let src = (loc, Evar_kinds.CasesType false) in
- let sigma = Sigma.Unsafe.of_evar_map sigma in
- let Sigma ((t, _), sigma, _) = new_type_evar env sigma univ_flexible_alg ~src in
- let sigma = Sigma.to_evar_map sigma in
- sigma, t in
- (* First strategy: we build an "inversion" predicate, also replacing the *)
- (* dependencies with existential variables *)
+ | None, Some t when not (noccur_with_meta 0 max_int t) ->
+ (* If the tycon is not closed w.r.t real variables, we try *)
+ (* two different strategies *)
+ (* First strategy: we build an "inversion" predicate *)
let sigma1,pred1 = build_inversion_problem loc env sigma tomatchs t in
(* Optional second strategy: we abstract the tycon wrt to the dependencies *)
let p2 =
prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign t in
- (* Third strategy: we take the type constraint as it is; of course we could *)
- (* need something inbetween, abstracting some but not all of the dependencies *)
- (* the "inversion" strategy deals with that but unification may not be *)
- (* powerful enough so strategy 2 and 3 helps; moreover, inverting does not *)
- (* work (yet) when a constructor has a type not precise enough for the inversion *)
- (* see log message for details *)
- let pred3 = lift (List.length (List.flatten arsign)) t in
(match p2 with
- | Some (sigma2,pred2) when not (Constr.equal pred2 pred3) ->
- [sigma1, pred1; sigma2, pred2; sigma, pred3]
- | _ ->
- [sigma1, pred1; sigma, pred3])
+ | Some (sigma2,pred2) -> [sigma1, pred1; sigma2, pred2]
+ | None -> [sigma1, pred1])
+ | None, _ ->
+ (* No dependent type constraint, or no constraints at all: *)
+ (* we use two strategies *)
+ let sigma,t = match tycon with
+ | Some t -> sigma,t
+ | None ->
+ let sigma = Sigma.Unsafe.of_evar_map sigma in
+ let Sigma ((t, _), sigma, _) =
+ new_type_evar env sigma univ_flexible_alg ~src:(loc, Evar_kinds.CasesType false) in
+ let sigma = Sigma.to_evar_map sigma in
+ sigma, t
+ in
+ (* First strategy: we build an "inversion" predicate *)
+ let sigma1,pred1 = build_inversion_problem loc env sigma tomatchs t in
+ (* Second strategy: we use the evar or tycon as a non dependent pred *)
+ let pred2 = lift (List.length (List.flatten arsign)) t in
+ [sigma1, pred1; sigma, pred2]
(* Some type annotation *)
- | Some rtntyp ->
+ | Some rtntyp, _ ->
(* We extract the signature of the arity *)
let envar = List.fold_right push_rel_context arsign env in
let sigma, newt = new_sort_variable univ_flexible_alg sigma in
@@ -2577,6 +2562,9 @@ let compile_cases loc style (typing_fun, evdref) tycon env (predopt, tomatchl, e
typing_function = typing_fun } in
let j = compile pb in
+
+ (* We coerce to the tycon (if an elim predicate was provided) *)
+ let j = inh_conv_coerce_to_tycon loc env myevdref j tycon in
evdref := !myevdref;
j in
@@ -2587,6 +2575,4 @@ let compile_cases loc style (typing_fun, evdref) tycon env (predopt, tomatchl, e
(* We check for unused patterns *)
List.iter (check_unused_pattern env) matx;
- (* We coerce to the tycon (if an elim predicate was provided) *)
- inh_conv_coerce_to_tycon loc env evdref j tycon
-
+ j
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index b033f5a395..b7e0535dad 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -42,12 +42,7 @@ let _ = Goptions.declare_bool_option {
let unfold_projection env evd ts p c =
let cst = Projection.constant p in
if is_transparent_constant ts cst then
- let c' = Some (mkProj (Projection.make cst true, c)) in
- match ReductionBehaviour.get (Globnames.ConstRef cst) with
- | None -> c'
- | Some (recargs, nargs, flags) ->
- if (List.mem `ReductionNeverUnfold flags) then None
- else c'
+ Some (mkProj (Projection.make cst true, c))
else None
let eval_flexible_term ts env evd c =
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 6c8677855a..a97e248aee 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -1591,6 +1591,8 @@ and evar_define conv_algo ?(choose=false) env evd pbty (evk,argsv as ev) rhs =
* ass.
*)
+(* This criterion relies on the fact that we postpone only problems of the form:
+?x [?x1 ... ?xn] = t or the symmetric case. *)
let status_changed lev (pbty,_,t1,t2) =
(try Evar.Set.mem (head_evar t1) lev with NoHeadEvar -> false) ||
(try Evar.Set.mem (head_evar t2) lev with NoHeadEvar -> false)
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 46f0219f91..48bf9149d0 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -239,10 +239,12 @@ let interp_elimination_sort = function
| GSet -> InSet
| GType _ -> InType
+type inference_hook = env -> evar_map -> evar -> evar_map * constr
+
type inference_flags = {
use_typeclasses : bool;
use_unif_heuristics : bool;
- use_hook : (env -> evar_map -> evar -> constr) option;
+ use_hook : inference_hook option;
fail_evar : bool;
expand_evars : bool
}
@@ -272,7 +274,7 @@ let apply_inference_hook hook evdref pending =
if Evd.is_undefined sigma evk (* in particular not defined by side-effect *)
then
try
- let c = hook sigma evk in
+ let sigma, c = hook sigma evk in
Evd.define evk c sigma
with Exit ->
sigma
diff --git a/pretyping/pretyping.mli b/pretyping/pretyping.mli
index 824bb11aa4..eead48a549 100644
--- a/pretyping/pretyping.mli
+++ b/pretyping/pretyping.mli
@@ -47,10 +47,12 @@ val empty_lvar : ltac_var_map
type glob_constr_ltac_closure = ltac_var_map * glob_constr
type pure_open_constr = evar_map * constr
+type inference_hook = env -> evar_map -> evar -> evar_map * constr
+
type inference_flags = {
use_typeclasses : bool;
use_unif_heuristics : bool;
- use_hook : (env -> evar_map -> evar -> constr) option;
+ use_hook : inference_hook option;
fail_evar : bool;
expand_evars : bool
}
diff --git a/pretyping/program.ml b/pretyping/program.ml
index b4333847b7..62aedcfbf6 100644
--- a/pretyping/program.ml
+++ b/pretyping/program.ml
@@ -15,10 +15,12 @@ open Term
let make_dir l = DirPath.make (List.rev_map Id.of_string l)
let find_reference locstr dir s =
- let sp = Libnames.make_path (make_dir dir) (Id.of_string s) in
+ let dp = make_dir dir in
+ let sp = Libnames.make_path dp (Id.of_string s) in
try Nametab.global_of_path sp
with Not_found ->
- anomaly ~label:locstr (Pp.str "cannot find" ++ spc () ++ Libnames.pr_path sp)
+ user_err_loc (Loc.ghost, "", str "Library " ++ Libnames.pr_dirpath dp ++
+ str " has to be required first.")
let coq_reference locstr dir s = find_reference locstr ("Coq"::dir) s
let coq_constant locstr dir s = Universes.constr_of_global (coq_reference locstr dir s)
diff --git a/pretyping/retyping.mli b/pretyping/retyping.mli
index e4cca2679c..8ca40f829f 100644
--- a/pretyping/retyping.mli
+++ b/pretyping/retyping.mli
@@ -46,3 +46,5 @@ val type_of_global_reference_knowing_conclusion :
val sorts_of_context : env -> evar_map -> Context.Rel.t -> sorts list
val expand_projection : env -> evar_map -> Names.projection -> constr -> constr list -> constr
+
+val print_retype_error : retype_error -> Pp.std_ppcmds
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 6573bd238c..531b615539 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1269,8 +1269,7 @@ let solve_simple_evar_eqn ts env evd ev rhs =
match solve_simple_eqn (Evarconv.evar_conv_x ts) env evd (None,ev,rhs) with
| UnifFailure (evd,reason) ->
error_cannot_unify env evd ~reason (mkEvar ev,rhs);
- | Success evd ->
- Evarconv.consider_remaining_unif_problems env evd
+ | Success evd -> evd
(* [w_merge env sigma b metas evars] merges common instances in metas
or in evars, possibly generating new unification problems; if [b]
@@ -1389,7 +1388,9 @@ let w_merge env with_types flags (evd,metas,evars) =
in w_merge_rec evd [] [] eqns
in
let res = (* merge constraints *)
- w_merge_rec evd (order_metas metas) (List.rev evars) []
+ w_merge_rec evd (order_metas metas)
+ (* Assign evars in the order of assignments during unification *)
+ (List.rev evars) []
in
if with_types then check_types res
else res
@@ -1587,7 +1588,7 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl =
let x = id_of_name_using_hdchar (Global.env()) t name in
let ids = ids_of_named_context (named_context env) in
if name == Anonymous then next_ident_away_in_goal x ids else
- if mem_named_context x (named_context env) then
+ if mem_named_context_val x (named_context_val env) then
errorlabstrm "Unification.make_abstraction_core"
(str "The variable " ++ Nameops.pr_id x ++ str " is already declared.")
else
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 12:46:20 +0000