aboutsummaryrefslogtreecommitdiff
path: root/pretyping
diff options
context:
space:
mode:
Diffstat (limited to 'pretyping')
-rw-r--r--pretyping/evarconv.ml11
-rw-r--r--pretyping/nativenorm.ml28
-rw-r--r--pretyping/nativenorm.mli2
-rw-r--r--pretyping/pretyping.ml12
-rw-r--r--pretyping/reductionops.ml20
-rw-r--r--pretyping/reductionops.mli8
-rw-r--r--pretyping/unification.ml65
-rw-r--r--pretyping/vnorm.ml20
8 files changed, 89 insertions, 77 deletions
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 062136ff52..6d08f66c1b 100644
--- a/pretyping/evarconv.ml
+++ b/pretyping/evarconv.ml
@@ -366,13 +366,10 @@ let rec evar_conv_x ts env evd pbty term1 term2 =
let ground_test =
if is_ground_term evd term1 && is_ground_term evd term2 then (
let e =
- try
- let evd, b = infer_conv ~catch_incon:false ~pb:pbty ~ts:(fst ts)
- env evd term1 term2
- in
- if b then Success evd
- else UnifFailure (evd, ConversionFailed (env,term1,term2))
- with Univ.UniverseInconsistency e -> UnifFailure (evd, UnifUnivInconsistency e)
+ match infer_conv ~catch_incon:false ~pb:pbty ~ts:(fst ts) env evd term1 term2 with
+ | Some evd -> Success evd
+ | None -> UnifFailure (evd, ConversionFailed (env,term1,term2))
+ | exception Univ.UniverseInconsistency e -> UnifFailure (evd, UnifUnivInconsistency e)
in
match e with
| UnifFailure (evd, e) when not (is_ground_env evd env) -> None
diff --git a/pretyping/nativenorm.ml b/pretyping/nativenorm.ml
index 978ceed1ea..3fce2f3c63 100644
--- a/pretyping/nativenorm.ml
+++ b/pretyping/nativenorm.ml
@@ -303,10 +303,10 @@ and nf_atom_type env sigma atom =
let (mib,mip) = Inductive.lookup_mind_specif env (fst ind) in
let nparams = mib.mind_nparams in
let params,realargs = Array.chop nparams allargs in
+ let nparamdecls = Context.Rel.length (Inductive.inductive_paramdecls (mib,u)) in
let pT =
- hnf_prod_applist env
+ hnf_prod_applist_assum env nparamdecls
(Inductiveops.type_of_inductive env ind) (Array.to_list params) in
- let pT = whd_all env pT in
let dep, p = nf_predicate env sigma ind mip params p pT in
(* Calcul du type des branches *)
let btypes = build_branches_type env sigma (fst ind) mib mip u params dep p in
@@ -362,20 +362,24 @@ and nf_atom_type env sigma atom =
and nf_predicate env sigma ind mip params v pT =
- match kind_of_value v, kind pT with
- | Vfun f, Prod _ ->
+ match kind (whd_allnolet env pT) with
+ | LetIn (name,b,t,pT) ->
+ let dep,body =
+ nf_predicate (push_rel (LocalDef (name,b,t)) env) sigma ind mip params v pT in
+ dep, mkLetIn (name,b,t,body)
+ | Prod (name,dom,codom) -> begin
+ match kind_of_value v with
+ | Vfun f ->
let k = nb_rel env in
let vb = f (mk_rel_accu k) in
- let name,dom,codom =
- try decompose_prod env pT with
- DestKO ->
- CErrors.anomaly
- (Pp.strbrk "Returned a functional value in a type not recognized as a product type.")
- in
let dep,body =
nf_predicate (push_rel (LocalAssum (name,dom)) env) sigma ind mip params vb codom in
dep, mkLambda(name,dom,body)
- | Vfun f, _ ->
+ | _ -> false, nf_type env sigma v
+ end
+ | _ ->
+ match kind_of_value v with
+ | Vfun f ->
let k = nb_rel env in
let vb = f (mk_rel_accu k) in
let name = Name (Id.of_string "c") in
@@ -385,7 +389,7 @@ and nf_predicate env sigma ind mip params v pT =
let dom = mkApp(mkIndU ind,Array.append params rargs) in
let body = nf_type (push_rel (LocalAssum (name,dom)) env) sigma vb in
true, mkLambda(name,dom,body)
- | _, _ -> false, nf_type env sigma v
+ | _ -> false, nf_type env sigma v
and nf_evar env sigma evk ty args =
let evi = try Evd.find sigma evk with Not_found -> assert false in
diff --git a/pretyping/nativenorm.mli b/pretyping/nativenorm.mli
index 67b7a2a405..4997d0bf0d 100644
--- a/pretyping/nativenorm.mli
+++ b/pretyping/nativenorm.mli
@@ -25,4 +25,4 @@ val native_norm : env -> evar_map -> constr -> types -> constr
(** Conversion with inference of universe constraints *)
val native_infer_conv : ?pb:conv_pb -> env -> evar_map -> constr -> constr ->
- evar_map * bool
+ evar_map option
diff --git a/pretyping/pretyping.ml b/pretyping/pretyping.ml
index 92f87ab95a..b2507b5f26 100644
--- a/pretyping/pretyping.ml
+++ b/pretyping/pretyping.ml
@@ -1082,9 +1082,9 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
let cj = pretype empty_tycon env evdref lvar c in
let cty = nf_evar !evdref cj.uj_type and tval = nf_evar !evdref tval in
if not (occur_existential !evdref cty || occur_existential !evdref tval) then
- let (evd,b) = Reductionops.vm_infer_conv env.ExtraEnv.env !evdref cty tval in
- if b then (evdref := evd; cj, tval)
- else
+ match Reductionops.vm_infer_conv env.ExtraEnv.env !evdref cty tval with
+ | Some evd -> (evdref := evd; cj, tval)
+ | None ->
error_actual_type ?loc env.ExtraEnv.env !evdref cj tval
(ConversionFailed (env.ExtraEnv.env,cty,tval))
else user_err ?loc (str "Cannot check cast with vm: " ++
@@ -1093,9 +1093,9 @@ let rec pretype k0 resolve_tc (tycon : type_constraint) (env : ExtraEnv.t) evdre
let cj = pretype empty_tycon env evdref lvar c in
let cty = nf_evar !evdref cj.uj_type and tval = nf_evar !evdref tval in
begin
- let (evd,b) = Nativenorm.native_infer_conv env.ExtraEnv.env !evdref cty tval in
- if b then (evdref := evd; cj, tval)
- else
+ match Nativenorm.native_infer_conv env.ExtraEnv.env !evdref cty tval with
+ | Some evd -> (evdref := evd; cj, tval)
+ | None ->
error_actual_type ?loc env.ExtraEnv.env !evdref cj tval
(ConversionFailed (env.ExtraEnv.env,cty,tval))
end
diff --git a/pretyping/reductionops.ml b/pretyping/reductionops.ml
index 6fde868370..7fb1a0a578 100644
--- a/pretyping/reductionops.ml
+++ b/pretyping/reductionops.ml
@@ -1348,11 +1348,10 @@ let infer_conv_gen conv_fun ?(catch_incon=true) ?(pb=Reduction.CUMUL)
?(ts=full_transparent_state) env sigma x y =
(** FIXME *)
try
- let b, sigma =
- let ans =
- if pb == Reduction.CUMUL then
+ let ans = match pb with
+ | Reduction.CUMUL ->
EConstr.leq_constr_universes env sigma x y
- else
+ | Reduction.CONV ->
EConstr.eq_constr_universes env sigma x y
in
let ans = match ans with
@@ -1362,20 +1361,17 @@ let infer_conv_gen conv_fun ?(catch_incon=true) ?(pb=Reduction.CUMUL)
with Univ.UniverseInconsistency _ | Evd.UniversesDiffer -> None
in
match ans with
- | None -> false, sigma
- | Some sigma -> true, sigma
- in
- if b then sigma, true
- else
+ | Some sigma -> ans
+ | None ->
let x = EConstr.Unsafe.to_constr x in
let y = EConstr.Unsafe.to_constr y in
let sigma' =
conv_fun pb ~l2r:false sigma ts
env (sigma, sigma_univ_state) x y in
- sigma', true
+ Some sigma'
with
- | Reduction.NotConvertible -> sigma, false
- | Univ.UniverseInconsistency _ when catch_incon -> sigma, false
+ | Reduction.NotConvertible -> None
+ | Univ.UniverseInconsistency _ when catch_incon -> None
| e when is_anomaly e -> report_anomaly e
let infer_conv = infer_conv_gen (fun pb ~l2r sigma ->
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index ad280d9f37..9256fa7ce6 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -277,13 +277,13 @@ val check_conv : ?pb:conv_pb -> ?ts:transparent_state -> env -> evar_map -> con
otherwise returns false in that case.
*)
val infer_conv : ?catch_incon:bool -> ?pb:conv_pb -> ?ts:transparent_state ->
- env -> evar_map -> constr -> constr -> evar_map * bool
+ env -> evar_map -> constr -> constr -> evar_map option
(** Conversion with inference of universe constraints *)
val set_vm_infer_conv : (?pb:conv_pb -> env -> evar_map -> constr -> constr ->
- evar_map * bool) -> unit
+ evar_map option) -> unit
val vm_infer_conv : ?pb:conv_pb -> env -> evar_map -> constr -> constr ->
- evar_map * bool
+ evar_map option
(** [infer_conv_gen] behaves like [infer_conv] but is parametrized by a
@@ -291,7 +291,7 @@ conversion function. Used to pretype vm and native casts. *)
val infer_conv_gen : (conv_pb -> l2r:bool -> evar_map -> transparent_state ->
(Constr.constr, evar_map) Reduction.generic_conversion_function) ->
?catch_incon:bool -> ?pb:conv_pb -> ?ts:transparent_state -> env ->
- evar_map -> constr -> constr -> evar_map * bool
+ evar_map -> constr -> constr -> evar_map option
(** {6 Special-Purpose Reduction Functions } *)
diff --git a/pretyping/unification.ml b/pretyping/unification.ml
index 4c788abdb4..5cf6e4b262 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -584,16 +584,16 @@ let constr_cmp pb env sigma flags t u =
in
match cstrs with
| Some cstrs ->
- begin try Evd.add_universe_constraints sigma cstrs, true
- with Univ.UniverseInconsistency _ -> sigma, false
+ begin try Some (Evd.add_universe_constraints sigma cstrs)
+ with Univ.UniverseInconsistency _ -> None
| Evd.UniversesDiffer ->
if is_rigid_head sigma flags t then
- try Evd.add_universe_constraints sigma (force_eqs cstrs), true
- with Univ.UniverseInconsistency _ -> sigma, false
- else sigma, false
+ try Some (Evd.add_universe_constraints sigma (force_eqs cstrs))
+ with Univ.UniverseInconsistency _ -> None
+ else None
end
| None ->
- sigma, false
+ None
let do_reduce ts (env, nb) sigma c =
Stack.zip sigma (fst (whd_betaiota_deltazeta_for_iota_state
@@ -628,9 +628,9 @@ let check_compatibility env pbty flags (sigma,metasubst,evarsubst : subst0) tyM
| None -> sigma
| Some n ->
if is_ground_term sigma m && is_ground_term sigma n then
- let sigma, b = infer_conv ~pb:pbty ~ts:flags.modulo_delta_types env sigma m n in
- if b then sigma
- else error_cannot_unify env sigma (m,n)
+ match infer_conv ~pb:pbty ~ts:flags.modulo_delta_types env sigma m n with
+ | Some sigma -> sigma
+ | None -> error_cannot_unify env sigma (m,n)
else sigma
@@ -745,11 +745,12 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
| Evar (evk,_ as ev), Evar (evk',_)
when not (Evar.Set.mem evk flags.frozen_evars)
&& Evar.equal evk evk' ->
- let sigma',b = constr_cmp cv_pb env sigma flags cM cN in
- if b then
- sigma',metasubst,evarsubst
- else
+ begin match constr_cmp cv_pb env sigma flags cM cN with
+ | Some sigma ->
+ sigma, metasubst, evarsubst
+ | None ->
sigma,metasubst,((curenv,ev,cN)::evarsubst)
+ end
| Evar (evk,_ as ev), _
when not (Evar.Set.mem evk flags.frozen_evars)
&& not (occur_evar sigma evk cN) ->
@@ -947,9 +948,9 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
and unify_not_same_head curenvnb pb opt (sigma, metas, evars as substn : subst0) cM cN =
try canonical_projections curenvnb pb opt cM cN substn
with ex when precatchable_exception ex ->
- let sigma', b = constr_cmp cv_pb env sigma flags cM cN in
- if b then (sigma', metas, evars)
- else
+ match constr_cmp cv_pb env sigma flags cM cN with
+ | Some sigma -> (sigma, metas, evars)
+ | None ->
try reduce curenvnb pb opt substn cM cN
with ex when precatchable_exception ex ->
let (f1,l1) =
@@ -1006,12 +1007,13 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
(* Renounce, maybe metas/evars prevents typing *) sigma
else sigma
in
- let sigma, b = infer_conv ~pb ~ts:convflags curenv sigma m1 n1 in
- if b then Some (sigma, metasubst, evarsubst)
- else
- if is_ground_term sigma m1 && is_ground_term sigma n1 then
- error_cannot_unify curenv sigma (cM,cN)
- else None
+ match infer_conv ~pb ~ts:convflags curenv sigma m1 n1 with
+ | Some sigma ->
+ Some (sigma, metasubst, evarsubst)
+ | None ->
+ if is_ground_term sigma m1 && is_ground_term sigma n1 then
+ error_cannot_unify curenv sigma (cM,cN)
+ else None
in
match res with
| Some substn -> substn
@@ -1114,11 +1116,13 @@ let rec unify_0_with_initial_metas (sigma,ms,es as subst : subst0) conv_at_top e
then
None
else
- let sigma, b = match flags.modulo_conv_on_closed_terms with
+ let ans = match flags.modulo_conv_on_closed_terms with
| Some convflags -> infer_conv ~pb:cv_pb ~ts:convflags env sigma m n
| _ -> constr_cmp cv_pb env sigma flags m n in
- if b then Some sigma
- else if (match flags.modulo_conv_on_closed_terms, flags.modulo_delta with
+ match ans with
+ | Some sigma -> ans
+ | None ->
+ if (match flags.modulo_conv_on_closed_terms, flags.modulo_delta with
| Some (cv_id, cv_k), (dl_id, dl_k) ->
Id.Pred.subset dl_id cv_id && Cpred.subset dl_k cv_k
| None,(dl_id, dl_k) ->
@@ -1608,8 +1612,10 @@ let make_pattern_test from_prefix_of_ind is_correct_type env sigma (pending,c) =
let merge_fun c1 c2 =
match c1, c2 with
| Some (evd,c1,x), Some (_,c2,_) ->
- let (evd,b) = infer_conv ~pb:CONV env evd c1 c2 in
- if b then Some (evd, c1, x) else raise (NotUnifiable None)
+ begin match infer_conv ~pb:CONV env evd c1 c2 with
+ | Some evd -> Some (evd, c1, x)
+ | None -> raise (NotUnifiable None)
+ end
| Some _, None -> c1
| None, Some _ -> c2
| None, None -> None in
@@ -1926,10 +1932,11 @@ let secondOrderAbstraction env evd flags typ (p, oplist) =
let (evd',cllist) = w_unify_to_subterm_list env evd flags p oplist typ in
let typp = Typing.meta_type evd' p in
let evd',(pred,predtyp) = abstract_list_all env evd' typp typ cllist in
- let evd', b = infer_conv ~pb:CUMUL env evd' predtyp typp in
- if not b then
+ match infer_conv ~pb:CUMUL env evd' predtyp typp with
+ | None ->
error_wrong_abstraction_type env evd'
(Evd.meta_name evd p) pred typp predtyp;
+ | Some evd' ->
w_merge env false flags.merge_unify_flags
(evd',[p,pred,(Conv,TypeProcessed)],[])
diff --git a/pretyping/vnorm.ml b/pretyping/vnorm.ml
index a1ba4a6a98..14c9f49b12 100644
--- a/pretyping/vnorm.ml
+++ b/pretyping/vnorm.ml
@@ -266,7 +266,6 @@ and nf_stk ?from:(from=0) env sigma c t stk =
let nparamdecls = Context.Rel.length (Inductive.inductive_paramdecls (mib,u)) in
let pT =
hnf_prod_applist_assum env nparamdecls (type_of_ind env (ind,u)) (Array.to_list params) in
- let pT = whd_all env pT in
let dep, p = nf_predicate env sigma (ind,u) mip params (type_of_switch sw) pT in
(* Calcul du type des branches *)
let btypes = build_branches_type env sigma ind mib mip u params dep p in
@@ -288,15 +287,24 @@ and nf_stk ?from:(from=0) env sigma c t stk =
nf_stk env sigma (mkProj(p',c)) ty stk
and nf_predicate env sigma ind mip params v pT =
- match whd_val v, kind pT with
- | Vfun f, Prod _ ->
+ match kind (whd_allnolet env pT) with
+ | LetIn (name,b,t,pT) ->
+ let dep,body =
+ nf_predicate (push_rel (LocalDef (name,b,t)) env) sigma ind mip params v pT in
+ dep, mkLetIn (name,b,t,body)
+ | Prod (name,dom,codom) -> begin
+ match whd_val v with
+ | Vfun f ->
let k = nb_rel env in
let vb = reduce_fun k f in
- let name,dom,codom = decompose_prod env pT in
let dep,body =
nf_predicate (push_rel (LocalAssum (name,dom)) env) sigma ind mip params vb codom in
dep, mkLambda(name,dom,body)
- | Vfun f, _ ->
+ | _ -> assert false
+ end
+ | _ ->
+ match whd_val v with
+ | Vfun f ->
let k = nb_rel env in
let vb = reduce_fun k f in
let name = Name (Id.of_string "c") in
@@ -306,7 +314,7 @@ and nf_predicate env sigma ind mip params v pT =
let dom = mkApp(mkIndU ind,Array.append params rargs) in
let body = nf_vtype (push_rel (LocalAssum (name,dom)) env) sigma vb in
true, mkLambda(name,dom,body)
- | _, _ -> false, nf_val env sigma v crazy_type
+ | _ -> false, nf_val env sigma v crazy_type
and nf_args env sigma vargs ?from:(f=0) t =
let t = ref t in
generated by cgit v1.2.3 (git 2.25.1) at 2026-05-03 18:30:09 +0000