aboutsummaryrefslogtreecommitdiff
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/cases.ml118
-rw-r--r--pretyping/evarconv.ml17
-rw-r--r--pretyping/evarsolve.ml10
-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, 88 insertions, 84 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index e89c3ea719..5c9ce2624c 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -62,13 +62,14 @@ let error_wrong_numarg_constructor_loc loc env c n =
let error_wrong_numarg_inductive_loc loc env c n =
raise_pattern_matching_error (loc, env, Evd.empty, WrongNumargInductive(c,n))
-let rec list_try_compile f = function
- | [a] -> f a
- | [] -> anomaly (str "try_find_f")
+let list_try_compile f l =
+ let rec aux errors = function
+ | [] -> if errors = [] then anomaly (str "try_find_f") else raise (List.last errors)
| h::t ->
try f h
- with UserError _ | TypeError _ | PretypeError _ | PatternMatchingError _ ->
- list_try_compile f t
+ with UserError _ | TypeError _ | PretypeError _ | PatternMatchingError _ as e ->
+ aux (e::errors) t in
+ aux [] l
let force_name =
let nx = Name default_dependent_ident in function Anonymous -> nx | na -> na
@@ -1870,22 +1871,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 +1889,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
@@ -1939,44 +1926,46 @@ let prepare_predicate_from_arsign_tycon env sigma loc tomatchs arsign c =
* type and 1 assumption for each term not _syntactically_ in an
* inductive type.
- * Each matched term is independently considered dependent or not.
+ * Each matched terms are independently considered dependent or not.
+
+ * A type constraint but no annotation case: we try to specialize the
+ * tycon to make the predicate if it is not closed.
*)
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 *)
- 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 =
+ | 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 abstract the tycon wrt to the dependencies *)
+ let p1 =
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])
+ (* Second strategy: we build an "inversion" predicate *)
+ let sigma2,pred2 = build_inversion_problem loc env sigma tomatchs t in
+ (match p1 with
+ | Some (sigma1,pred1) -> [sigma1, pred1; sigma2, pred2]
+ | None -> [sigma2, pred2])
+ | 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 directly use the evar 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 +2566,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 +2579,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..3680cd777a 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 =
@@ -102,19 +97,19 @@ let position_problem l2r = function
| CONV -> None
| CUMUL -> Some l2r
-let occur_rigidly ev evd t =
+let occur_rigidly (evk,_ as ev) evd t =
let rec aux t =
match kind_of_term (whd_evar evd t) with
| App (f, c) -> if aux f then Array.exists aux c else false
| Construct _ | Ind _ | Sort _ | Meta _ | Fix _ | CoFix _ -> true
| Proj (p, c) -> not (aux c)
- | Evar (ev',_) -> if Evar.equal ev ev' then raise Occur else false
+ | Evar (evk',_) -> if Evar.equal evk evk' then raise Occur else false
| Cast (p, _, _) -> aux p
| Lambda _ | LetIn _ -> false
| Const _ -> false
| Prod (_, b, t) -> ignore(aux b || aux t); true
| Rel _ | Var _ -> false
- | Case _ -> false
+ | Case (_,_,c,_) -> if eq_constr (mkEvar ev) c then raise Occur else false
in try ignore(aux t); false with Occur -> true
(* [check_conv_record env sigma (t1,stack1) (t2,stack2)] tries to decompose
@@ -483,7 +478,7 @@ and evar_eqappr_x ?(rhs_is_already_stuck = false) ts env evd pbty
ise_try evd
[eta;(* Postpone the use of an heuristic *)
(fun i ->
- if not (occur_rigidly (fst ev) i tR) then
+ if not (occur_rigidly ev i tR) then
let i,tF =
if isRel tR || isVar tR then
(* Optimization so as to generate candidates *)
@@ -1152,7 +1147,7 @@ let apply_conversion_problem_heuristic ts env evd pbty t1 t2 =
let f env evd pbty x y = is_fconv ~reds:ts pbty env evd x y in
Success (solve_refl ~can_drop:true f env evd
(position_problem true pbty) evk1 args1 args2)
- | Evar ev1, Evar ev2 ->
+ | Evar ev1, Evar ev2 when app_empty ->
Success (solve_evar_evar ~force:true
(evar_define (evar_conv_x ts) ~choose:true) (evar_conv_x ts) env evd
(position_problem true pbty) ev1 ev2)
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index 6c8677855a..d695d4537b 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -613,7 +613,13 @@ let define_evar_from_virtual_equation define_fun env evd src t_in_env ty_t_in_si
* substitution u1..uq.
*)
+exception MorePreciseOccurCheckNeeeded
+
let materialize_evar define_fun env evd k (evk1,args1) ty_in_env =
+ if Evd.is_defined evd evk1 then
+ (* Some circularity somewhere (see e.g. #3209) *)
+ raise MorePreciseOccurCheckNeeeded;
+ let (evk1,args1) = destEvar (whd_evar evd (mkEvar (evk1,args1))) in
let evi1 = Evd.find_undefined evd evk1 in
let env1,rel_sign = env_rel_context_chop k env in
let sign1 = evar_hyps evi1 in
@@ -1553,6 +1559,8 @@ and evar_define conv_algo ?(choose=false) env evd pbty (evk,argsv as ev) rhs =
postpone_non_unique_projection env evd pbty ev sols rhs
| NotEnoughInformationEvarEvar t ->
add_conv_oriented_pb (pbty,env,mkEvar ev,t) evd
+ | MorePreciseOccurCheckNeeeded ->
+ add_conv_oriented_pb (pbty,env,mkEvar ev,rhs) evd
| NotInvertibleUsingOurAlgorithm _ | MetaOccurInBodyInternal as e ->
raise e
| OccurCheckIn (evd,rhs) ->
@@ -1591,6 +1599,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-02 19:14:17 +0000