From dfa7719a3c73c2dd79a444e8b8c5306661005538 Mon Sep 17 00:00:00 2001 From: Pierre-Marie Pédrot Date: Wed, 28 Mar 2018 13:48:19 +0200 Subject: Stronger invariants in unification signature. We use an option type instead of returning a pair with a boolean. Indeed, the boolean being true was always indicating that the returned value was unchanged. The previous API was somewhat error-prone, and I don't understand why it was designed this way in the first place. --- pretyping/evarconv.ml | 11 +++----- pretyping/nativenorm.mli | 2 +- pretyping/pretyping.ml | 12 ++++----- pretyping/reductionops.ml | 20 ++++++-------- pretyping/reductionops.mli | 8 +++--- pretyping/unification.ml | 65 +++++++++++++++++++++++++--------------------- 6 files changed, 59 insertions(+), 59 deletions(-) (limited to 'pretyping') 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)],[]) -- cgit v1.2.3