aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--pretyping/evarconv.ml30
-rw-r--r--pretyping/evarsolve.ml4
-rw-r--r--pretyping/evarsolve.mli3
-rw-r--r--pretyping/evd.ml2
-rw-r--r--pretyping/reductionops.ml8
-rw-r--r--pretyping/retyping.ml7
-rw-r--r--pretyping/unification.ml81
7 files changed, 90 insertions, 45 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 2db31ccda..694627983 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -34,20 +34,18 @@ let _ = Goptions.declare_bool_option {
}
let unfold_projection env evd ts p c =
- if Projection.unfolded p then assert false
- else
- let cst = Projection.constant p in
- if is_transparent_constant ts cst then
- let unfold_app () =
- let t' = Retyping.expand_projection env evd p c [] in
- Some t'
- in
- (match ReductionBehaviour.get (Globnames.ConstRef cst) with
- | None -> unfold_app ()
- | Some (recargs, nargs, flags) ->
- if (List.mem `ReductionNeverUnfold flags) then None
- else unfold_app ())
- else None
+ let cst = Projection.constant p in
+ if is_transparent_constant ts cst then
+ let unfold_app () =
+ let t' = Retyping.expand_projection env evd p c [] in
+ Some t'
+ in
+ (match ReductionBehaviour.get (Globnames.ConstRef cst) with
+ | None -> unfold_app ()
+ | Some (recargs, nargs, flags) ->
+ if (List.mem `ReductionNeverUnfold flags) then None
+ else unfold_app ())
+ else None
let eval_flexible_term ts env evd c =
match kind_of_term c with
@@ -66,7 +64,9 @@ let eval_flexible_term ts env evd c =
with Not_found -> None)
| LetIn (_,b,_,c) -> Some (subst1 b c)
| Lambda _ -> Some c
- | Proj (p, c) -> unfold_projection env evd ts p c
+ | Proj (p, c) ->
+ if Projection.unfolded p then None
+ else unfold_projection env evd ts p c
| _ -> assert false
type flex_kind_of_term =
diff --git a/pretyping/evarsolve.ml b/pretyping/evarsolve.ml
index a41e0169a..94ec82029 100644
--- a/pretyping/evarsolve.ml
+++ b/pretyping/evarsolve.ml
@@ -101,6 +101,10 @@ let refresh_universes ?(inferred=false) ?(onlyalg=false) pbty env evd t =
in
if !modified then !evdref, t' else !evdref, t
+let get_type_of_refresh ?(polyprop=true) ?(lax=false) env sigma c =
+ let ty = Retyping.get_type_of ~polyprop ~lax env sigma c in
+ refresh_universes (Some false) env sigma ty
+
(************************)
(* Unification results *)
(************************)
diff --git a/pretyping/evarsolve.mli b/pretyping/evarsolve.mli
index 0d0f3c0e5..fc9f25f96 100644
--- a/pretyping/evarsolve.mli
+++ b/pretyping/evarsolve.mli
@@ -69,3 +69,6 @@ val check_evar_instance :
val remove_instance_local_defs :
evar_map -> existential_key -> constr array -> constr list
+
+val get_type_of_refresh :
+ ?polyprop:bool -> ?lax:bool -> env -> evar_map -> constr -> evar_map * types
diff --git a/pretyping/evd.ml b/pretyping/evd.ml
index 826fd59ba..95b7e044b 100644
--- a/pretyping/evd.ml
+++ b/pretyping/evd.ml
@@ -1389,7 +1389,7 @@ let eq_constr_univs evd t u =
let b, c = Universes.eq_constr_univs_infer evd.universes.uctx_universes t u in
if b then
try let evd' = add_universe_constraints evd c in evd', b
- with Univ.UniverseInconsistency _ -> evd, false
+ with Univ.UniverseInconsistency _ | UniversesDiffer -> evd, false
else evd, b
let e_eq_constr_univs evdref t u =
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 8dc46b79b..69f2ba2d0 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -1488,13 +1488,11 @@ let whd_betaiota_deltazeta_for_iota_state ts env sigma csts s =
let (t_o,stack_o),csts_o = whd_state_gen ~csts:csts' false
(Closure.RedFlags.red_add_transparent betadeltaiota ts) env sigma (t,args) in
if isConstruct t_o then whrec csts_o (t_o, stack_o@stack') else s,csts'
- |args, (Stack.Proj (n,m,p,_) :: stack'' as stack') ->
+ |args, (Stack.Proj (n,m,p,_) :: stack'') ->
let (t_o,stack_o),csts_o = whd_state_gen ~csts:csts' false
(Closure.RedFlags.red_add_transparent betadeltaiota ts) env sigma (t,args) in
- if isConstruct t_o then
- if Projection.unfolded p || Closure.is_transparent_constant ts (Projection.constant p)
- then whrec Cst_stack.empty (* csts_o *) (Stack.nth stack_o (n+m), stack'')
- else (* Won't unfold *) (whd_betaiota_state sigma (t_o, stack_o@stack'),csts')
+ if isConstruct t_o && Projection.unfolded p then
+ whrec Cst_stack.empty (Stack.nth stack_o (n+m), stack'')
else s,csts'
|_, ((Stack.App _| Stack.Shift _|Stack.Update _|Stack.Cst _) :: _|[]) -> s,csts'
in whrec csts s
diff --git a/pretyping/retyping.ml b/pretyping/retyping.ml
index 23ad43a1c..653ce3b45 100644
--- a/pretyping/retyping.ml
+++ b/pretyping/retyping.ml
@@ -244,7 +244,10 @@ let sorts_of_context env evc ctxt =
snd (aux ctxt)
let expand_projection env sigma pr c args =
- let ty = get_type_of env sigma c in
- let (i,u), ind_args = Inductiveops.find_mrectype env sigma ty in
+ let ty = get_type_of ~lax:true env sigma c in
+ let (i,u), ind_args =
+ try Inductiveops.find_mrectype env sigma ty
+ with Not_found -> retype_error BadRecursiveType
+ in
mkApp (mkConstU (Projection.constant pr,u),
Array.of_list (ind_args @ (c :: args)))
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 8d0d5394a..0b00b6ee3 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -397,9 +397,13 @@ let unfold_projection env p stk =
let expand_key ts env sigma = function
| Some (IsKey k) -> expand_table_key env k
| Some (IsProj (p, c)) ->
- let red = Stack.zip (fst (whd_betaiota_deltazeta_for_iota_state ts env sigma
- Cst_stack.empty (c, unfold_projection env p [])))
- in if Term.eq_constr (mkProj (p, c)) red then None else Some red
+ if Projection.unfolded p then
+ let red = Stack.zip (fst (whd_betaiota_deltazeta_for_iota_state ts env sigma
+ Cst_stack.empty (c, unfold_projection env (Projection.unfold p) [])))
+ in if Term.eq_constr (mkProj (p, c)) red then None else Some red
+ else
+ (try Some (Retyping.expand_projection env sigma p c [])
+ with RetypeError _ -> None)
| None -> None
let subterm_restriction is_subterm flags =
@@ -442,9 +446,11 @@ let oracle_order env cf1 cf2 =
| Some k2 ->
match k1, k2 with
| IsProj (p, _), IsKey (ConstKey (p',_))
- when eq_constant (Projection.constant p) p' -> Some false
+ when eq_constant (Projection.constant p) p' ->
+ Some (not (Projection.unfolded p))
| IsKey (ConstKey (p,_)), IsProj (p', _)
- when eq_constant p (Projection.constant p') -> Some true
+ when eq_constant p (Projection.constant p') ->
+ Some (Projection.unfolded p')
| _ ->
Some (Conv_oracle.oracle_order (Environ.oracle env) false
(translate_key k1) (translate_key k2))
@@ -618,6 +624,27 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb
| LetIn (_,a,_,c), _ -> unirec_rec curenvnb pb b wt substn (subst1 a c) cN
| _, LetIn (_,a,_,c) -> unirec_rec curenvnb pb b wt substn cM (subst1 a c)
+
+ | Proj (p1,c1), _ when not (Projection.unfolded p1) ->
+ let cM' =
+ try Retyping.expand_projection curenv sigma p1 c1 []
+ with RetypeError _ ->
+ (** Unification can be called on ill-typed terms, due
+ to FO and eta in particular, fail gracefully in that case *)
+ error_cannot_unify (fst curenvnb) sigma (cM,cN)
+ in
+ unirec_rec curenvnb CONV true false substn cM' cN
+
+ | _, Proj (p2,c2) when not (Projection.unfolded p2) ->
+ let cN' =
+ try Retyping.expand_projection curenv sigma p2 c2 []
+ with RetypeError _ ->
+ (** Unification can be called on ill-typed terms, due
+ to FO and eta in particular, fail gracefully in that case *)
+ error_cannot_unify (fst curenvnb) sigma (cM,cN)
+ in
+ unirec_rec curenvnb CONV true false substn cM cN'
+
(* eta-expansion *)
| Lambda (na,t1,c1), _ when flags.modulo_eta ->
unirec_rec (push (na,t1) curenvnb) CONV true wt substn
@@ -661,26 +688,18 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb
try (* Force unification of the types to fill in parameters *)
let ty1 = get_type_of curenv ~lax:true sigma c1 in
let ty2 = get_type_of curenv ~lax:true sigma c2 in
- unify_0_with_initial_metas substn true curenv cv_pb
- { flags with modulo_conv_on_closed_terms = Some full_transparent_state;
- modulo_delta = full_transparent_state;
- modulo_eta = true;
- modulo_betaiota = true }
- ty1 ty2
+ unify_0_with_initial_metas substn true curenv cv_pb
+ { flags with modulo_conv_on_closed_terms = Some full_transparent_state;
+ modulo_delta = full_transparent_state;
+ modulo_eta = true;
+ modulo_betaiota = true }
+ ty1 ty2
with RetypeError _ -> substn
with ex when precatchable_exception ex ->
unify_not_same_head curenvnb pb b wt substn cM cN
else
unify_not_same_head curenvnb pb b wt substn cM cN
- | Proj (p1,c1), _ when not (Projection.unfolded p1) ->
- let cM' = Retyping.expand_projection curenv sigma p1 c1 [] in
- unirec_rec curenvnb CONV true false substn cM' cN
-
- | _, Proj (p2,c2) when not (Projection.unfolded p2) ->
- let cN' = Retyping.expand_projection curenv sigma p2 c2 [] in
- unirec_rec curenvnb CONV true false substn cM cN'
-
| App (f1,l1), _ when
(isMeta f1 && use_metas_pattern_unification flags nb l1
|| use_evars_pattern_unification flags && isAllowedEvar flags f1) ->
@@ -713,11 +732,29 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst) conv_at_top env cv_pb
| _ ->
unify_not_same_head curenvnb pb b wt substn cM cN
- and unify_app curenvnb pb b substn cM f1 l1 cN f2 l2 =
+ and unify_app (curenv, nb as curenvnb) pb b (sigma, metas, evars as substn) cM f1 l1 cN f2 l2 =
try
let (f1,l1,f2,l2) = adjust_app_array_size f1 l1 f2 l2 in
- Array.fold_left2 (unirec_rec curenvnb CONV true false)
- (unirec_rec curenvnb CONV true true substn f1 f2) l1 l2
+ (* let substn = *)
+ (* let sigma, b = Evd.eq_constr_univs sigma f1 f2 in *)
+ (* if b then (sigma,metas,evars) *)
+ (* else if isEvar_or_Meta f1 || isEvar_or_Meta f2 then (sigma,metas,evars) *)
+ (* else *)
+ (* try *)
+ (* let sigma', ty1 = Evarsolve.get_type_of_refresh curenv ~lax:true sigma f1 in *)
+ (* let sigma', ty2 = Evarsolve.get_type_of_refresh curenv ~lax:true sigma f2 in *)
+ (* let substn = unify_0_with_initial_metas (sigma', metas, evars) true curenv CONV *)
+ (* { flags with modulo_conv_on_closed_terms = Some full_transparent_state; *)
+ (* modulo_delta = full_transparent_state; *)
+ (* modulo_eta = true; *)
+ (* modulo_betaiota = true } *)
+ (* ty1 ty2 *)
+ (* in substn *)
+ (* with RetypeError _ -> *)
+ (* error_cannot_unify (fst curenvnb) sigma (cM,cN) *)
+ (* in *)
+ Array.fold_left2 (unirec_rec curenvnb CONV true false)
+ (unirec_rec curenvnb CONV true true substn f1 f2) l1 l2
with ex when precatchable_exception ex ->
try reduce curenvnb pb b false substn cM cN
with ex when precatchable_exception ex ->
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-10 21:09:21 +0000