diff --git a/src/ecCoreSubst.ml b/src/ecCoreSubst.ml index cb99d5b5f..5df52665e 100644 --- a/src/ecCoreSubst.ml +++ b/src/ecCoreSubst.ml @@ -738,4 +738,11 @@ module Tvar = struct let f_subst ~(freshen : bool) (lv : ident list) (lt : ty list) : form -> form = Fsubst.f_subst_tvar ~freshen (init lv lt) + + let sty_subst ~(freshen : bool) (lv : ident list) (lt : ty list) : (ty * form) option -> (ty * form) option = + let tsubst = init lv lt in + Option.map + (fun (ty, f) -> + ( subst tsubst ty, + Fsubst.f_subst_tvar ~freshen tsubst f )) end diff --git a/src/ecCoreSubst.mli b/src/ecCoreSubst.mli index f829b8d38..7743ee452 100644 --- a/src/ecCoreSubst.mli +++ b/src/ecCoreSubst.mli @@ -44,10 +44,11 @@ end (* -------------------------------------------------------------------- *) module Tvar : sig - val init : EcIdent.t list -> ty list -> ty Mid.t - val subst1 : (EcIdent.t * ty) -> ty -> ty - val subst : ty Mid.t -> ty -> ty - val f_subst : freshen:bool -> EcIdent.t list -> ty list -> form -> form + val init : EcIdent.t list -> ty list -> ty Mid.t + val subst1 : (EcIdent.t * ty) -> ty -> ty + val subst : ty Mid.t -> ty -> ty + val f_subst : freshen:bool -> EcIdent.t list -> ty list -> form -> form + val sty_subst : freshen:bool -> EcIdent.t list -> ty list -> (ty * form) option -> (ty * form) option end (* -------------------------------------------------------------------- *) diff --git a/src/ecThCloning.ml b/src/ecThCloning.ml index 121a10858..c84c8ed02 100644 --- a/src/ecThCloning.ml +++ b/src/ecThCloning.ml @@ -15,6 +15,8 @@ type incompatible = | DifferentType of EcTypes.ty * EcTypes.ty | OpBody (* of (EcPath.path * EcDecl.operator) * (EcPath.path * EcDecl.operator) *) | TyBody (* of (EcPath.path * EcDecl.tydecl) * (EcPath.path * EcDecl.tydecl) *) +| SubtypeType of (EcTypes.ty * EcTypes.ty option) +| SubtypePred of (EcAst.form * EcAst.form) type ovkind = | OVK_Type diff --git a/src/ecThCloning.mli b/src/ecThCloning.mli index 4720f2cbc..9b36f6788 100644 --- a/src/ecThCloning.mli +++ b/src/ecThCloning.mli @@ -9,6 +9,8 @@ type incompatible = | DifferentType of EcTypes.ty * EcTypes.ty | OpBody (* of (EcPath.path * EcDecl.operator) * (EcPath.path * EcDecl.operator) *) | TyBody (* of (EcPath.path * EcDecl.tydecl) * (EcPath.path * EcDecl.tydecl) *) +| SubtypeType of (EcTypes.ty * EcTypes.ty option) +| SubtypePred of (EcAst.form * EcAst.form) type ovkind = | OVK_Type diff --git a/src/ecTheoryReplay.ml b/src/ecTheoryReplay.ml index 9d2e25be3..1dd4e9ecc 100644 --- a/src/ecTheoryReplay.ml +++ b/src/ecTheoryReplay.ml @@ -187,12 +187,22 @@ end = struct let tparams = List.map tvar params in let ty_body1 = tyd1.tyd_type in let ty_body2 = EcSubst.open_tydecl tyd2 tparams in + let subtype1 = CS.Tvar.sty_subst ~freshen:false tyd1.tyd_params tparams tyd1.tyd_subtype in + let subtype2 = CS.Tvar.sty_subst ~freshen:false tyd2.tyd_params tparams tyd2.tyd_subtype in let hyps = EcEnv.LDecl.init env params in match ty_body1, ty_body2 with - | Abstract, _ -> () - + | Abstract, _ -> begin + match subtype1, subtype2 with + | Some (ty1, f1), Some (ty2, f2) -> + if not (EcReduction.EqTest.for_type (toenv hyps) ty1 ty2) then + raise (Incompatible (SubtypeType (ty1, Some ty2))); + if not (EcReduction.is_conv ~ri:ri_compatible hyps f1 f2) then + raise (Incompatible (SubtypePred (f1, f2))) + | Some (ty1, _), None -> raise (Incompatible (SubtypeType (ty1, None))) + | _, _ -> () + end | _, _ -> tybody hyps ty_body1 ty_body2 with CoreIncompatible -> raise (Incompatible TyBody) @@ -428,12 +438,18 @@ let rec replay_tyd (ove : _ ovrenv) (subst, ops, proofs, scope) (import, x, otyd nargs in let ue = EcUnify.UniEnv.create (Some nargs) in let ntyd = EcTyping.transty EcTyping.tp_tydecl env ue ntyd in + let subtype = + match ntyd.ty_node with + | Tconstr (p, tys) -> + let reftyd = EcEnv.Ty.by_path p env in + CS.Tvar.sty_subst ~freshen:false reftyd.tyd_params tys reftyd.tyd_subtype + | _ -> None in let decl = { tyd_params = nargs; tyd_type = Concrete ntyd; tyd_loca = otyd.tyd_loca; tyd_clinline = (mode <> `Alias); - tyd_subtype = None; } + tyd_subtype = subtype; } in (decl, ntyd) @@ -459,6 +475,7 @@ let rec replay_tyd (ove : _ ovrenv) (subst, ops, proofs, scope) (import, x, otyd | `Direct ty -> begin assert (List.is_empty otyd.tyd_params); + assert (otyd.tyd_subtype = None); let decl = { tyd_params = []; tyd_type = Concrete ty; diff --git a/src/ecUserMessages.ml b/src/ecUserMessages.ml index dc8e0947d..763bec43a 100644 --- a/src/ecUserMessages.ml +++ b/src/ecUserMessages.ml @@ -839,6 +839,17 @@ end = struct Format.fprintf fmt "incompatible body" | TyBody -> Format.fprintf fmt "incompatible type declaration" + | SubtypeType (ty1, None) -> + Format.fprintf fmt "incompatible type. Not a subtype of %a" + (EcPrinting.pp_type (EcPrinting.PPEnv.ofenv env)) ty1 + | SubtypeType (ty1, Some ty2) -> + Format.fprintf fmt "incompatible type. The type is a subtype of %a instead of %a" + (EcPrinting.pp_type (EcPrinting.PPEnv.ofenv env)) ty2 + (EcPrinting.pp_type (EcPrinting.PPEnv.ofenv env)) ty1 + | SubtypePred (f1, f2) -> + Format.fprintf fmt "incompatible predicate for subtypes. The predicate for the subtype is %a instead of %a" + (EcPrinting.pp_form (EcPrinting.PPEnv.ofenv env)) f2 + (EcPrinting.pp_form (EcPrinting.PPEnv.ofenv env)) f1 let pp_clone_error env fmt error = let msg x = Format.fprintf fmt x in diff --git a/tests/subtype-override.ec b/tests/subtype-override.ec new file mode 100644 index 000000000..f27b7b301 --- /dev/null +++ b/tests/subtype-override.ec @@ -0,0 +1,15 @@ +require Subtype. + +theory T1. + subtype s = {b: bool | b}. + realize inhabited by exists true. +end T1. + +subtype s = {b: bool | !b}. +realize inhabited by exists false. + +fail clone T1 as T2 with +type s <- s, +op insub <- insub, +op val <- val +proof *.