From 5113afbb6e8c1f9122b37c37b0561c529c406256 Mon Sep 17 00:00:00 2001
From: letouzey
Date: Tue, 12 Apr 2011 22:31:42 +0000
Subject: Subtyping: align coqtop behavior concerning opaque csts on coqchk's
 one

 After discussion with Bruno and Hugo, coqtop now accepts that an opaque
 constant in a module type could be implemented by anything of
 the right type, even if bodies differ. Said otherwise, with respect
 to subtyping, an opaque constant behaves just as a parameter.
 This was already the case in coqchk, and a footnote in documentation
 is advertising for quite some time that:

   "Opaque definitions are processed as assumptions."

 Truly, it might seem awkward that "Definition x:=3" can implement
 "Lemma x:nat. Proof 2. Qed." but the opacity ensures that nothing
 can go wrong afterwards, since Coq is forced to ignore that the x
 in signature has body "2".

 Similarly, "T with Definition x := c" is now legal when T contains
 an opaque x, even when this x isn't convertible with c.

 By avoiding accesses to opaque bodies, we also achieve some speedup
 (less delayed load of .vo final sections containing opaque terms).

 Nota: the extraction will have to be adapted, since for the moment it
 might access the body of opaque constants: the warning emitted when
 doing that should become an error.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@13987 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 kernel/mod_typing.ml |  8 ++++----
 kernel/subtyping.ml  | 36 ++++++++++--------------------------
 2 files changed, 14 insertions(+), 30 deletions(-)

(limited to 'kernel')

diff --git a/kernel/mod_typing.ml b/kernel/mod_typing.ml
index aad541d218..b8162340f7 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 cac55f4be6..2430dc6f0f 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 " ^
-- 
cgit v1.2.3