summaryrefslogtreecommitdiff
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/cases.ml2
-rw-r--r--pretyping/detyping.ml2
-rw-r--r--pretyping/evarutil.ml42
-rw-r--r--pretyping/glob_term.ml34
-rw-r--r--pretyping/typing.ml9
-rw-r--r--pretyping/unification.ml56
-rw-r--r--pretyping/unification.mli1
7 files changed, 90 insertions, 56 deletions
diff --git a/pretyping/cases.ml b/pretyping/cases.ml
index 1819dc52..38355cf1 100644
--- a/pretyping/cases.ml
+++ b/pretyping/cases.ml
@@ -1763,7 +1763,7 @@ let prepare_predicate loc typing_fun sigma env tomatchs arsign tycon pred =
(* 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 arsign) t in
+ let pred2 = lift (List.length (List.flatten arsign)) t in
[sigma1, pred1; sigma, pred2]
(* Some type annotation *)
| Some rtntyp, _ ->
diff --git a/pretyping/detyping.ml b/pretyping/detyping.ml
index 69ff2af9..a74e4cb4 100644
--- a/pretyping/detyping.ml
+++ b/pretyping/detyping.ml
@@ -389,6 +389,8 @@ let rec detype (isgoal:bool) avoid env t =
with _ ->
GVar (dl, id))
| Sort s -> GSort (dl,detype_sort s)
+ | Cast (c1,REVERTcast,c2) when not !Flags.raw_print ->
+ detype isgoal avoid env c1
| Cast (c1,k,c2) ->
GCast(dl,detype isgoal avoid env c1, CastConv (k, detype isgoal avoid env c2))
| Prod (na,ty,c) -> detype_binder isgoal BProd avoid env na ty c
diff --git a/pretyping/evarutil.ml b/pretyping/evarutil.ml
index fa29243a..b0248a84 100644
--- a/pretyping/evarutil.ml
+++ b/pretyping/evarutil.ml
@@ -135,15 +135,20 @@ let whd_head_evar_stack sigma c =
let whd_head_evar sigma c = applist (whd_head_evar_stack sigma c)
-let noccur_evar evd evk c =
- let rec occur_rec c = match kind_of_term c with
- | Evar (evk',_ as ev') ->
+let noccur_evar env evd evk c =
+ let rec occur_rec k c = match kind_of_term c with
+ | Evar (evk',args' as ev') ->
(match safe_evar_value evd ev' with
- | Some c -> occur_rec c
- | None -> if evk = evk' then raise Occur)
- | _ -> iter_constr occur_rec c
+ | Some c -> occur_rec k c
+ | None ->
+ if evk = evk' then raise Occur else Array.iter (occur_rec k) args')
+ | Rel i when i > k ->
+ (match pi2 (Environ.lookup_rel (i-k) env) with
+ | None -> ()
+ | Some b -> occur_rec k (lift i b))
+ | _ -> iter_constr_with_binders succ occur_rec k c
in
- try occur_rec c; true with Occur -> false
+ try occur_rec 0 c; true with Occur -> false
let normalize_evar evd ev =
match kind_of_term (whd_evar evd (mkEvar ev)) with
@@ -741,7 +746,8 @@ let is_unification_pattern_meta env nb m l t =
None
let is_unification_pattern_evar env evd (evk,args) l t =
- if List.for_all (fun x -> isRel x || isVar x) l & noccur_evar evd evk t then
+ if List.for_all (fun x -> isRel x || isVar x) l & noccur_evar env evd evk t
+ then
let args = remove_instance_local_defs evd evk (Array.to_list args) in
let n = List.length args in
match find_unification_pattern_args env (args @ l) t with
@@ -1112,10 +1118,11 @@ let invert_arg_from_subst evd aliases k0 subst_in_env_extended_with_k_binders c_
| Not_found -> CannotInvert
| NotUnique -> Invertible NoUniqueProjection
-let invert_arg evd aliases k evk subst_in_env_extended_with_k_binders c_in_env_extended_with_k_binders =
+let invert_arg fullenv evd aliases k evk subst_in_env_extended_with_k_binders c_in_env_extended_with_k_binders =
let res = invert_arg_from_subst evd aliases k subst_in_env_extended_with_k_binders c_in_env_extended_with_k_binders in
match res with
- | Invertible (UniqueProjection (c,_)) when not (noccur_evar evd evk c) ->
+ | Invertible (UniqueProjection (c,_)) when not (noccur_evar fullenv evd evk c)
+ ->
CannotInvert
| _ ->
res
@@ -1153,10 +1160,11 @@ let extract_candidates sols =
let filter_of_projection = function Invertible _ -> true | _ -> false
-let invert_invertible_arg evd aliases k (evk,argsv) args' =
+let invert_invertible_arg fullenv evd aliases k (evk,argsv) args' =
let evi = Evd.find_undefined evd evk in
let subst,_ = make_projectable_subst aliases evd evi argsv in
- let projs = array_map_to_list (invert_arg evd aliases k evk subst) args' in
+ let projs =
+ array_map_to_list (invert_arg fullenv evd aliases k evk subst) args' in
Array.of_list (extract_unique_projections projs)
(* Redefines an evar with a smaller context (i.e. it may depend on less
@@ -1364,12 +1372,14 @@ let has_constrainable_free_vars evd aliases k ev (fv_rels,fv_ids as fvs) t =
let ensure_evar_independent g env evd (evk1,argsv1 as ev1) (evk2,argsv2 as ev2)=
let filter1 =
- restrict_upon_filter evd evk1 (noccur_evar evd evk2) (Array.to_list argsv1)
+ restrict_upon_filter evd evk1 (noccur_evar env evd evk2)
+ (Array.to_list argsv1)
in
let candidates1 = restrict_candidates g env evd filter1 ev1 ev2 in
let evd,(evk1,_ as ev1) = do_restrict_hyps evd ev1 filter1 candidates1 in
let filter2 =
- restrict_upon_filter evd evk2 (noccur_evar evd evk1) (Array.to_list argsv2)
+ restrict_upon_filter evd evk2 (noccur_evar env evd evk1)
+ (Array.to_list argsv2)
in
let candidates2 = restrict_candidates g env evd filter2 ev2 ev1 in
let evd,ev2 = do_restrict_hyps evd ev2 filter2 candidates2 in
@@ -1389,7 +1399,7 @@ let project_evar_on_evar g env evd aliases k2 (evk1,argsv1 as ev1) (evk2,argsv2
try
let candidates1 = restrict_candidates g env evd filter1 ev1 ev2 in
let evd,(evk1',args1) = do_restrict_hyps evd ev1 filter1 candidates1 in
- evd,mkEvar (evk1',invert_invertible_arg evd aliases k2 ev2 args1)
+ evd,mkEvar (evk1',invert_invertible_arg env evd aliases k2 ev2 args1)
with
| EvarSolvedWhileRestricting (evd,ev1) ->
raise (EvarSolvedOnTheFly (evd,ev1))
@@ -1585,7 +1595,7 @@ let rec invert_definition conv_algo choose env evd (evk,argsv as ev) rhs =
let aliases = lift_aliases k aliases in
(try
let ev = (evk,Array.map (lift k) argsv) in
- let evd,body = project_evar_on_evar conv_algo env !evdref aliases k ev' ev in
+ let evd,body = project_evar_on_evar conv_algo env' !evdref aliases k ev' ev in
evdref := evd;
body
with
diff --git a/pretyping/glob_term.ml b/pretyping/glob_term.ml
index 24c5ba5b..8e4b211f 100644
--- a/pretyping/glob_term.ml
+++ b/pretyping/glob_term.ml
@@ -346,8 +346,38 @@ let rec cases_pattern_of_glob_constr na = function
| GHole (loc,_) -> PatVar (loc,na)
| GRef (loc,ConstructRef cstr) ->
PatCstr (loc,cstr,[],na)
- | GApp (loc,GRef (_,ConstructRef cstr),l) ->
- PatCstr (loc,cstr,List.map (cases_pattern_of_glob_constr Anonymous) l,na)
+ | GApp (loc,GRef (_,ConstructRef (ind,_ as cstr)),args) ->
+ let mib,_ = Global.lookup_inductive ind in
+ let nparams = mib.Declarations.mind_nparams in
+ if nparams > List.length args then
+ user_err_loc (loc,"",Pp.str "Invalid notation for pattern.");
+ let params,args = list_chop nparams args in
+ List.iter (function GHole _ -> ()
+ | _ -> user_err_loc (loc,"",Pp.str"Invalid notation for pattern."))
+ params;
+ let args = List.map (cases_pattern_of_glob_constr Anonymous) args in
+ PatCstr (loc,cstr,args,na)
+ | _ -> raise Not_found
+
+let rec cases_pattern_of_glob_constr na = function
+ | GVar (loc,id) when na<>Anonymous ->
+ (* Unable to manage the presence of both an alias and a variable *)
+ raise Not_found
+ | GVar (loc,id) -> PatVar (loc,Name id)
+ | GHole (loc,_) -> PatVar (loc,na)
+ | GRef (loc,ConstructRef cstr) ->
+ PatCstr (loc,cstr,[],na)
+ | GApp (loc,GRef (_,ConstructRef (ind,_ as cstr)),args) ->
+ let mib,_ = Global.lookup_inductive ind in
+ let nparams = mib.Declarations.mind_nparams in
+ if nparams > List.length args then
+ user_err_loc (loc,"",Pp.str "Invalid notation for pattern.");
+ let params,args = list_chop nparams args in
+ List.iter (function GHole _ -> ()
+ | _ -> user_err_loc (loc,"",Pp.str"Invalid notation for pattern."))
+ params;
+ let args = List.map (cases_pattern_of_glob_constr Anonymous) args in
+ PatCstr (loc,cstr,args,na)
| _ -> raise Not_found
(* Turn a closed cases pattern into a glob_constr *)
diff --git a/pretyping/typing.ml b/pretyping/typing.ml
index 665491e7..22aacb29 100644
--- a/pretyping/typing.ml
+++ b/pretyping/typing.ml
@@ -42,6 +42,11 @@ let e_type_judgment env evdref j =
evdref := evd; { utj_val = j.uj_val; utj_type = s }
| _ -> error_not_type env j
+let e_assumption_of_judgment env evdref j =
+ try (e_type_judgment env evdref j).utj_val
+ with TypeError _ ->
+ error_assumption env j
+
let e_judge_of_apply env evdref funj argjv =
let rec apply_rec n typ = function
| [] ->
@@ -150,7 +155,7 @@ let rec execute env evdref cstr =
| Evar ev ->
let ty = Evd.existential_type !evdref ev in
let jty = execute env evdref (whd_evar !evdref ty) in
- let jty = assumption_of_judgment env jty in
+ let jty = e_assumption_of_judgment env evdref jty in
{ uj_val = cstr; uj_type = jty }
| Rel n ->
@@ -243,7 +248,7 @@ let rec execute env evdref cstr =
and execute_recdef env evdref (names,lar,vdef) =
let larj = execute_array env evdref lar in
- let lara = Array.map (assumption_of_judgment env) larj in
+ let lara = Array.map (e_assumption_of_judgment env evdref) larj in
let env1 = push_rec_types (names,lara,vdef) env in
let vdefj = execute_array env1 evdref vdef in
let vdefv = Array.map j_val vdefj in
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index c92c183d..63cdb378 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -198,11 +198,18 @@ type unify_flags = {
(* (and activated for apply, rewrite but not auto since Feb 2008 for 8.2) *)
modulo_delta : Names.transparent_state;
- (* This controls which constant are unfoldable; this is on for apply *)
+ (* This controls which constants are unfoldable; this is on for apply *)
(* (but not simple apply) since Feb 2008 for 8.2 *)
modulo_delta_types : Names.transparent_state;
+ modulo_delta_in_merge : Names.transparent_state option;
+ (* This controls whether unfoldability is different when trying to unify *)
+ (* several instances of the same metavariable *)
+ (* Typical situation is when we give a pattern to be matched *)
+ (* syntactically against a subterm but we want the metas of the *)
+ (* pattern to be modulo convertibility *)
+
check_applied_meta_types : bool;
(* This controls whether meta's applied to arguments have their *)
(* type unified with the type of their instance *)
@@ -240,12 +247,13 @@ type unify_flags = {
}
(* Default flag for unifying a type against a type (e.g. apply) *)
-(* We set all conversion flags *)
+(* We set all conversion flags (no flag should be modified anymore) *)
let default_unify_flags = {
modulo_conv_on_closed_terms = Some full_transparent_state;
use_metas_eagerly_in_conv_on_closed_terms = true;
modulo_delta = full_transparent_state;
modulo_delta_types = full_transparent_state;
+ modulo_delta_in_merge = None;
check_applied_meta_types = true;
resolve_evars = false;
use_pattern_unification = true;
@@ -258,24 +266,22 @@ let default_unify_flags = {
(* in fact useless when not used in w_unify_to_subterm_list *)
}
+let set_merge_flags flags =
+ match flags.modulo_delta_in_merge with
+ | None -> flags
+ | Some ts ->
+ { flags with modulo_delta = ts; modulo_conv_on_closed_terms = Some ts }
+
(* Default flag for the "simple apply" version of unification of a *)
(* type against a type (e.g. apply) *)
(* We set only the flags available at the time the new "apply" extends *)
(* out of "simple apply" *)
-let default_no_delta_unify_flags = {
- modulo_conv_on_closed_terms = Some full_transparent_state;
- use_metas_eagerly_in_conv_on_closed_terms = true;
+let default_no_delta_unify_flags = { default_unify_flags with
modulo_delta = empty_transparent_state;
- modulo_delta_types = full_transparent_state;
check_applied_meta_types = false;
- resolve_evars = false;
use_pattern_unification = false;
use_meta_bound_pattern_unification = true;
- frozen_evars = ExistentialSet.empty;
- restrict_conv_on_strict_subterms = false;
modulo_betaiota = false;
- modulo_eta = true;
- allow_K_in_toplevel_higher_order_unification = false
}
(* Default flags for looking for subterms in elimination tactics *)
@@ -283,36 +289,16 @@ let default_no_delta_unify_flags = {
(* allow_K) because only closed terms are involved in *)
(* induction/destruct/case/elim and w_unify_to_subterm_list does not *)
(* call w_unify for induction/destruct/case/elim (13/6/2011) *)
-let elim_flags = {
- modulo_conv_on_closed_terms = Some full_transparent_state;
- use_metas_eagerly_in_conv_on_closed_terms = true;
- modulo_delta = full_transparent_state;
- modulo_delta_types = full_transparent_state;
- check_applied_meta_types = true;
- resolve_evars = false;
- use_pattern_unification = true;
- use_meta_bound_pattern_unification = true;
- frozen_evars = ExistentialSet.empty;
+let elim_flags = { default_unify_flags with
restrict_conv_on_strict_subterms = false; (* ? *)
modulo_betaiota = false;
- modulo_eta = true;
allow_K_in_toplevel_higher_order_unification = true
}
-let elim_no_delta_flags = {
- modulo_conv_on_closed_terms = Some full_transparent_state;
- use_metas_eagerly_in_conv_on_closed_terms = true;
+let elim_no_delta_flags = { elim_flags with
modulo_delta = empty_transparent_state;
- modulo_delta_types = full_transparent_state;
check_applied_meta_types = false;
- resolve_evars = false;
use_pattern_unification = false;
- use_meta_bound_pattern_unification = true;
- frozen_evars = ExistentialSet.empty;
- restrict_conv_on_strict_subterms = false; (* ? *)
- modulo_betaiota = false;
- modulo_eta = true;
- allow_K_in_toplevel_higher_order_unification = true
}
let set_no_head_reduction flags =
@@ -865,7 +851,7 @@ let w_merge env with_types flags (evd,metas,evars) =
if Evd.is_defined evd evk then
let v = Evd.existential_value evd ev in
let (evd,metas',evars'') =
- unify_0 curenv evd CONV flags rhs v in
+ unify_0 curenv evd CONV (set_merge_flags flags) rhs v in
w_merge_rec evd (metas'@metas) (evars''@evars') eqns
else begin
(* This can make rhs' ill-typed if metas are *)
@@ -943,7 +929,7 @@ let w_merge env with_types flags (evd,metas,evars) =
let sp_env = Global.env_of_context ev.evar_hyps in
let (evd', c) = applyHead sp_env evd nargs hdc in
let (evd'',mc,ec) =
- unify_0 sp_env evd' CUMUL flags
+ unify_0 sp_env evd' CUMUL (set_merge_flags flags)
(get_type_of sp_env evd' c) ev.evar_concl in
let evd''' = w_merge_rec evd'' mc ec [] in
if evd' == evd'''
diff --git a/pretyping/unification.mli b/pretyping/unification.mli
index e3fd46af..1ec5c1a2 100644
--- a/pretyping/unification.mli
+++ b/pretyping/unification.mli
@@ -15,6 +15,7 @@ type unify_flags = {
use_metas_eagerly_in_conv_on_closed_terms : bool;
modulo_delta : Names.transparent_state;
modulo_delta_types : Names.transparent_state;
+ modulo_delta_in_merge : Names.transparent_state option;
check_applied_meta_types : bool;
resolve_evars : bool;
use_pattern_unification : bool;
generated by cgit v1.2.3 (git 2.39.1) at 2024-11-02 08:47:12 +0000