aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--dev/ci/user-overlays/07099-ppedrot-unification-returns-option.sh4
-rw-r--r--dev/doc/changes.md4
-rw-r--r--pretyping/evarconv.ml11
-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--proofs/logic.ml7
-rw-r--r--tactics/tactics.ml38
10 files changed, 91 insertions, 80 deletions
diff --git a/dev/ci/user-overlays/07099-ppedrot-unification-returns-option.sh b/dev/ci/user-overlays/07099-ppedrot-unification-returns-option.sh
new file mode 100644
index 000000000..e6c48d10a
--- /dev/null
+++ b/dev/ci/user-overlays/07099-ppedrot-unification-returns-option.sh
@@ -0,0 +1,4 @@
+if [ "$CI_PULL_REQUEST" = "7099" ] || [ "$CI_BRANCH" = "unification-returns-option" ]; then
+ Equations_CI_BRANCH=unification-returns-option
+ Equations_CI_GITURL=https://github.com/ppedrot/Coq-Equations
+fi
diff --git a/dev/doc/changes.md b/dev/doc/changes.md
index 4838dd734..bb8189efc 100644
--- a/dev/doc/changes.md
+++ b/dev/doc/changes.md
@@ -28,6 +28,10 @@ Proof engine
should indicate what the canonical form is. An important change is
the move of `Globnames.global_reference` to `Names.GlobRef.t`.
+- Unification API returns `evar_map option` instead of `bool * evar_map`
+ with the guarantee that the `evar_map` was unchanged if the boolean
+ was false.
+
ML Libraries used by Coq
- Introduction of a "Smart" module for collecting "smart*" functions, e.g.
diff --git a/pretyping/evarconv.ml b/pretyping/evarconv.ml
index 062136ff5..6d08f66c1 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.mli b/pretyping/nativenorm.mli
index 67b7a2a40..4997d0bf0 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 92f87ab95..b2507b5f2 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 6fde86837..7fb1a0a57 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 ad280d9f3..9256fa7ce 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 5f7faa13e..a8a4003dc 100644
--- a/pretyping/unification.ml
+++ b/pretyping/unification.ml
@@ -579,16 +579,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
@@ -623,9 +623,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
@@ -740,11 +740,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) ->
@@ -942,9 +943,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) =
@@ -1001,12 +1002,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
@@ -1109,11 +1111,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) ->
@@ -1603,8 +1607,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
@@ -1921,10 +1927,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/proofs/logic.ml b/proofs/logic.ml
index 218b2671e..95c30d815 100644
--- a/proofs/logic.ml
+++ b/proofs/logic.ml
@@ -309,9 +309,10 @@ let check_meta_variables env sigma c =
let check_conv_leq_goal env sigma arg ty conclty =
if !check then
- let evm, b = Reductionops.infer_conv env sigma (EConstr.of_constr ty) (EConstr.of_constr conclty) in
- if b then evm
- else raise (RefinerError (env, sigma, BadType (arg,ty,conclty)))
+ let ans = Reductionops.infer_conv env sigma (EConstr.of_constr ty) (EConstr.of_constr conclty) in
+ match ans with
+ | Some evm -> evm
+ | None -> raise (RefinerError (env, sigma, BadType (arg,ty,conclty)))
else sigma
exception Stop of EConstr.t list
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 58c62af85..d7888f6ca 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -158,9 +158,9 @@ let convert_concl ?(check=true) ty k =
let sigma =
if check then begin
ignore (Typing.unsafe_type_of env sigma ty);
- let sigma,b = Reductionops.infer_conv env sigma ty conclty in
- if not b then error "Not convertible.";
- sigma
+ match Reductionops.infer_conv env sigma ty conclty with
+ | None -> error "Not convertible."
+ | Some sigma -> sigma
end else sigma in
let (sigma, x) = Evarutil.new_evar env sigma ~principal:true ~store ty in
let ans = if k == DEFAULTcast then x else mkCast(x,k,conclty) in
@@ -186,11 +186,10 @@ let convert_hyp_no_check = convert_hyp ~check:false
let convert_gen pb x y =
Proofview.Goal.enter begin fun gl ->
- try
- let sigma, b = Tacmach.New.pf_apply (Reductionops.infer_conv ~pb) gl x y in
- if b then Proofview.Unsafe.tclEVARS sigma
- else Tacticals.New.tclFAIL 0 (str "Not convertible")
- with (* Reduction.NotConvertible *) _ ->
+ match Tacmach.New.pf_apply (Reductionops.infer_conv ~pb) gl x y with
+ | Some sigma -> Proofview.Unsafe.tclEVARS sigma
+ | None -> Tacticals.New.tclFAIL 0 (str "Not convertible")
+ | exception _ ->
(** FIXME: Sometimes an anomaly is raised from conversion *)
Tacticals.New.tclFAIL 0 (str "Not convertible")
end
@@ -796,15 +795,15 @@ let check_types env sigma mayneedglobalcheck deep newc origc =
let t2 = Retyping.get_type_of env sigma origc in
let sigma, t2 = Evarsolve.refresh_universes
~onlyalg:true (Some false) env sigma t2 in
- let sigma, b = infer_conv ~pb:Reduction.CUMUL env sigma t1 t2 in
- if not b then
+ match infer_conv ~pb:Reduction.CUMUL env sigma t1 t2 with
+ | None ->
if
isSort sigma (whd_all env sigma t1) &&
isSort sigma (whd_all env sigma t2)
then (mayneedglobalcheck := true; sigma)
else
user_err ~hdr:"convert-check-hyp" (str "Types are incompatible.")
- else sigma
+ | Some sigma -> sigma
end
else
if not (isSort sigma (whd_all env sigma t1)) then
@@ -815,9 +814,9 @@ let check_types env sigma mayneedglobalcheck deep newc origc =
let change_and_check cv_pb mayneedglobalcheck deep t env sigma c =
let (sigma, t') = t sigma in
let sigma = check_types env sigma mayneedglobalcheck deep t' c in
- let sigma, b = infer_conv ~pb:cv_pb env sigma t' c in
- if not b then user_err ~hdr:"convert-check-hyp" (str "Not convertible.");
- (sigma, t')
+ match infer_conv ~pb:cv_pb env sigma t' c with
+ | None -> user_err ~hdr:"convert-check-hyp" (str "Not convertible.");
+ | Some sigma -> (sigma, t')
(* Use cumulativity only if changing the conclusion not a subterm *)
let change_on_subterm cv_pb deep t where env sigma c =
@@ -1934,16 +1933,19 @@ let assumption =
let t = NamedDecl.get_type decl in
let concl = Proofview.Goal.concl gl in
let sigma = Tacmach.New.project gl in
- let (sigma, is_same_type) =
- if only_eq then (sigma, EConstr.eq_constr sigma t concl)
+ let ans =
+ if only_eq then
+ if EConstr.eq_constr sigma t concl then Some sigma
+ else None
else
let env = Proofview.Goal.env gl in
infer_conv env sigma t concl
in
- if is_same_type then
+ match ans with
+ | Some sigma ->
(Proofview.Unsafe.tclEVARS sigma) <*>
exact_no_check (mkVar (NamedDecl.get_id decl))
- else arec gl only_eq rest
+ | None -> arec gl only_eq rest
in
let assumption_tac gl =
let hyps = Proofview.Goal.hyps gl in
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-18 03:55:09 +0000