aboutsummaryrefslogtreecommitdiff
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/cases.ml100
-rw-r--r--pretyping/pretyping.ml6
-rw-r--r--pretyping/pretyping.mli4
-rw-r--r--pretyping/reductionops.ml7
-rw-r--r--pretyping/unification.ml9
-rw-r--r--pretyping/vnorm.ml6
6 files changed, 71 insertions, 61 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index fe2b0a5a1a..e89c3ea719 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1870,16 +1870,22 @@ 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 subst, len =
+ let (rel_subst,var_subst), len =
List.fold_right2 (fun (tm, tmtype) sign (subst, len) ->
let signlen = List.length sign in
match kind_of_term tm with
- | Rel n when dependent tm c
+ | Rel _ | Var _ when dependent tm c
&& Int.equal signlen 1 (* The term to match is not of a dependent type itself *) ->
- ((n, len) :: subst, len - signlen)
- | Rel n when signlen > 1 (* The term is of a dependent type,
+ (add_subst tm len subst, len - signlen)
+ | Rel _ | Var _ 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)
@@ -1888,28 +1894,36 @@ 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 n when dependent arg c ->
- ((n, len) :: subst, pred len)
+ | Rel _ | Var _ when dependent arg c ->
+ (add_subst arg len subst, pred len)
| _ -> (subst, pred len))
(subst, len) realargs
in
let subst =
- if dependent tm c && List.for_all isRel realargs
- then (n, len) :: subst else subst
+ if dependent tm c && List.for_all (fun c -> isRel c || isVar c) realargs
+ then add_subst tm 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) subst in
+ let idx = Int.List.assoc (n - lift) rel_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
@@ -1925,46 +1939,44 @@ 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 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.
+ * Each matched term is independently considered dependent or not.
*)
let prepare_predicate loc typing_fun env sigma tomatchs arsign tycon pred =
let preds =
- match pred, tycon with
+ match pred with
(* No return clause *)
- | 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
- (* 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 *)
+ | 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
- (* 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]
+ (* 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 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
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/reductionops.ml b/pretyping/reductionops.ml
index 4ccbc81b47..332d4e0b26 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -166,9 +166,6 @@ module Cst_stack = struct
let empty = []
let is_empty = CList.is_empty
- let sanity x y =
- assert(Term.eq_constr x y)
-
let drop_useless = function
| _ :: ((_,_,[])::_ as q) -> q
| l -> l
@@ -177,9 +174,9 @@ module Cst_stack = struct
let append2cst = function
| (c,params,[]) -> (c, h::params, [])
| (c,params,((i,t)::q)) when i = pred (Array.length t) ->
- let () = sanity h t.(i) in (c, params, q)
+ (c, params, q)
| (c,params,(i,t)::q) ->
- let () = sanity h t.(i) in (c, params, (succ i,t)::q)
+ (c, params, (succ i,t)::q)
in
drop_useless (List.map append2cst cst_l)
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index bc888b8973..6573bd238c 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -1599,14 +1599,7 @@ let make_abstraction_core name (test,out) env sigma c ty occs check_occs concl =
let hyp = get_id d in
match occurrences_of_hyp hyp occs with
| NoOccurrences, InHyp ->
- if indirectly_dependent c d depdecls then
- (* Told explicitly not to abstract over [d], but it is dependent *)
- let id' = indirect_dependency d depdecls in
- errorlabstrm "" (str "Cannot abstract over " ++ Nameops.pr_id id'
- ++ str " without also abstracting or erasing " ++ Nameops.pr_id hyp
- ++ str ".")
- else
- (push_named_context_val d sign,depdecls)
+ (push_named_context_val d sign,depdecls)
| AllOccurrences, InHyp as occ ->
let occ = if likefirst then LikeFirst else AtOccs occ in
let newdecl = replace_term_occ_decl_modulo occ test mkvarid d in
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index c396f593bb..e281f22df6 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -46,7 +46,11 @@ let invert_tag cst tag reloc_tbl =
with Find_at j -> (j+1)
(* Argggg, ces constructeurs de ... qui commencent a 1*)
-let find_rectype_a env c = Inductiveops.find_mrectype_vect env Evd.empty c
+let find_rectype_a env c =
+ let (t, l) = decompose_appvect (whd_all env c) in
+ match kind_of_term t with
+ | Ind ind -> (ind, l)
+ | _ -> assert false
(* Instantiate inductives and parameters in constructor type *)
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-04 10:32:09 +0000