diff options
| -rw-r--r-- | checker/mod_checking.ml | 8 | ||||
| -rw-r--r-- | checker/subtyping.ml | 17 | ||||
| -rw-r--r-- | kernel/mod_typing.ml | 8 | ||||
| -rw-r--r-- | kernel/subtyping.ml | 36 |
4 files changed, 29 insertions, 40 deletions
diff --git a/checker/mod_checking.ml b/checker/mod_checking.ml index e6582e918..d35dfaff1 100644 --- a/checker/mod_checking.ml +++ b/checker/mod_checking.ml @@ -110,8 +110,11 @@ let check_definition_sub env cb1 cb2 = let typ1 = Typeops.type_of_constant_type env cb1.const_type in let typ2 = Typeops.type_of_constant_type env cb2.const_type in check_type env typ1 typ2; + (* In the spirit of subtyping.check_constant, we accept + any implementations of parameters and opaques terms, + as long as they have the right type *) (match cb2.const_body with - | Undef _ -> () + | Undef _ | OpaqueDef _ -> () | Def lc2 -> (match cb1.const_body with | Def lc1 -> @@ -119,8 +122,7 @@ let check_definition_sub env cb1 cb2 = let c2 = force_constr lc2 in Reduction.conv env c1 c2 (* Coq only places transparent cb in With_definition_body *) - | _ -> assert false) - | _ -> ()) (* Pierre L: shouldn't this case raise an error ? *) + | _ -> assert false)) let lookup_modtype mp env = try Environ.lookup_modtype mp env diff --git a/checker/subtyping.ml b/checker/subtyping.ml index e00671b03..50d27ce2c 100644 --- a/checker/subtyping.ml +++ b/checker/subtyping.ml @@ -243,20 +243,23 @@ let check_constant env mp1 l info1 cb2 spec2 subst1 subst2 = let typ1 = Typeops.type_of_constant_type env cb1.const_type in let typ2 = Typeops.type_of_constant_type env cb2.const_type in check_type env typ1 typ2; - (* Now we check the bodies *) + (* Now we check the bodies: + - A transparent constant can only be implemented by a compatible + transparent constant. + - In the signature, an opaque is handled just as a parameter: + anything of the right type can implement it, even if bodies differ. + *) (match cb2.const_body with - | Undef _ -> () + | Undef _ | OpaqueDef _ -> () | Def lc2 -> - (* Only a transparent cb1 can implement a transparent cb2. - NB: cb1 might have been strengthened and appear as transparent. - Anyway [check_conv] will handle that afterwards. *) (match cb1.const_body with | Undef _ | OpaqueDef _ -> error () | Def lc1 -> + (* NB: cb1 might have been strengthened and appear as transparent. + Anyway [check_conv] will handle that afterwards. *) let c1 = force_constr lc1 in let c2 = force_constr lc2 in - check_conv conv env c1 c2) - | OpaqueDef lc2 -> ()) (* Pierre L. : this looks really strange ?! *) + check_conv conv env c1 c2)) | IndType ((kn,i),mind1) -> ignore (Util.error ( "The kernel does not recognize yet that a parameter can be " ^ diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml index aad541d21..b8162340f 100644 --- a/kernel/mod_typing.ml +++ b/kernel/mod_typing.ml @@ -87,8 +87,11 @@ and check_with_aux_def env sign with_decl mp equiv = | SFBconst cb -> cb | _ -> error_not_a_constant l in + (* In the spirit of subtyping.check_constant, we accept + any implementations of parameters and opaques terms, + as long as they have the right type *) let def,cst = match cb.const_body with - | Undef _ -> + | Undef _ | OpaqueDef _ -> let (j,cst1) = Typeops.infer env' c in let typ = Typeops.type_of_constant_type env' cb.const_type in let cst2 = Reduction.conv_leq env' j.uj_type typ in @@ -104,9 +107,6 @@ and check_with_aux_def env sign with_decl mp equiv = let cst = union_constraints cb.const_constraints cst1 in let def = Def (Declarations.from_val c) in def,cst - | OpaqueDef _ -> - (* We cannot make transparent an opaque field *) - raise Reduction.NotConvertible in let cb' = { cb with diff --git a/kernel/subtyping.ml b/kernel/subtyping.ml index cac55f4be..2430dc6f0 100644 --- a/kernel/subtyping.ml +++ b/kernel/subtyping.ml @@ -260,39 +260,23 @@ let check_constant cst env mp1 l info1 cb2 spec2 subst1 subst2 = let typ1 = Typeops.type_of_constant_type env cb1.const_type in let typ2 = Typeops.type_of_constant_type env cb2.const_type in let cst = check_type cst env typ1 typ2 in - (* Now we check the bodies *) + (* Now we check the bodies: + - A transparent constant can only be implemented by a compatible + transparent constant. + - In the signature, an opaque is handled just as a parameter: + anything of the right type can implement it, even if bodies differ. + *) (match cb2.const_body with - | Undef _ -> cst + | Undef _ | OpaqueDef _ -> cst | Def lc2 -> - (* Only a transparent cb1 can implement a transparent cb2. - NB: cb1 might have been strengthened and appear as transparent. - Anyway [check_conv] will handle that afterwards. *) (match cb1.const_body with | Undef _ | OpaqueDef _ -> error NotConvertibleBodyField | Def lc1 -> + (* NB: cb1 might have been strengthened and appear as transparent. + Anyway [check_conv] will handle that afterwards. *) let c1 = Declarations.force lc1 in let c2 = Declarations.force lc2 in - check_conv NotConvertibleBodyField cst conv env c1 c2) - | OpaqueDef lc2 -> - (* Here cb1 can be either opaque or transparent. We need to - bypass the opacity and possibly do a delta step. *) - (match body_of_constant cb1 with - | None -> error NotConvertibleBodyField - | Some lc1 -> - let c1 = Declarations.force lc1 in - let c2 = Declarations.force_opaque lc2 in - let c1' = match (kind_of_term c1),(kind_of_term c2) with - | Const n1,Const n2 when (eq_constant n1 n2) -> c1 - (* cb1 may have been strengthened, we need to unfold it: *) - | Const n1,_ -> - let cb1' = subst_const_body subst1 (lookup_constant n1 env) - in - (match cb1'.const_body with - | OpaqueDef lc1' -> Declarations.force_opaque lc1' - | _ -> c1) - | _,_ -> c1 - in - check_conv NotConvertibleBodyField cst conv env c1' c2)) + check_conv NotConvertibleBodyField cst conv env c1 c2)) | IndType ((kn,i),mind1) -> ignore (Util.error ( "The kernel does not recognize yet that a parameter can be " ^ |