First attempt at making Print Assumption compatible with opaque modules (fix #2168)

 We replace Global.lookup_constant by our own code that looks for a module
 and enters its implementation. This is still preliminary work, I would prefer
 to understand more completely the part about module substitutions when
 entering an applied functor. But this code already appears to work quite well.
 Anyway, since we only search for constants, we don't need to reconstitute a
 100% accurate environment, as long as the same objects are in it.

 Note:

  - Digging inside module structures is slower than just using
    Global.lookup_constant. Hence we try to avoid it as long as we could.
    Only in front of axioms (or in front of constant unknown to Global)
    do we check whether we have an inner-module implementation for this
    constant. There is some memoization of the search for internal
    structure_body out of a module_path.

  - In case of inner-module axioms, we might not be able to print
    its type, but only its long name.

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14600 85f007b7-540e-0410-9357-904b9bb8a0f7

2 files changed, 114 insertions, 0 deletions

diff --git a/test-suite/output/PrintAssumptions.out b/test-suite/output/PrintAssumptions.out
new file mode 100644
index 0000000000..23f33081b4
--- /dev/null
+++ b/test-suite/output/PrintAssumptions.out
@@ -0,0 +1,18 @@
+Axioms:
+foo : nat
+Axioms:
+foo : nat
+Axioms:
+extensionality : forall (P Q : Type) (f g : P -> Q),
+                 (forall x : P, f x = g x) -> f = g
+Axioms:
+extensionality : forall (P Q : Type) (f g : P -> Q),
+                 (forall x : P, f x = g x) -> f = g
+Axioms:
+extensionality : forall (P Q : Type) (f g : P -> Q),
+                 (forall x : P, f x = g x) -> f = g
+Axioms:
+extensionality : forall (P Q : Type) (f g : P -> Q),
+                 (forall x : P, f x = g x) -> f = g
+Closed under the global context
+Closed under the global context
diff --git a/test-suite/output/PrintAssumptions.v b/test-suite/output/PrintAssumptions.v
new file mode 100644
index 0000000000..f23bc49808
--- /dev/null
+++ b/test-suite/output/PrintAssumptions.v
@@ -0,0 +1,96 @@
+
+(** Print Assumption and opaque modules :
+
+  Print Assumption used to consider as axioms the modular fields
+  unexported by their signature, cf bug report #2186. This should
+  now be fixed, let's test this here. *)
+
+(* First, a minimal test-case *)
+
+Axiom foo : nat.
+
+Module Type T.
+ Parameter bar : nat.
+End T.
+
+Module M : T.
+  Module Hide. (* An entire sub-module could be hidden *)
+  Definition x := foo.
+  End Hide.
+  Definition bar := Hide.x.
+End M.
+
+Module N (X:T) : T.
+  Definition y := X.bar. (* A non-exported field *)
+  Definition bar := y.
+End N.
+
+Module P := N M.
+
+Print Assumptions M.bar. (* Should answer: foo *)
+Print Assumptions P.bar. (* Should answer: foo *)
+
+
+(* The original test-case of the bug-report *)
+
+Require Import Arith.
+
+Axiom extensionality : forall P Q (f g:P -> Q),
+  (forall x, f x = g x) -> f = g.
+
+Module Type ADD_COMM_EXT.
+  Axiom add_comm_ext : forall n, (fun x => x + n) = (fun x => n + x).
+End ADD_COMM_EXT.
+
+Module AddCommExt_Opaque : ADD_COMM_EXT.
+  Lemma add_comm_ext : forall n, (fun x => x + n) = (fun x => n + x).
+  Proof.
+    intro n; apply extensionality; auto with arith.
+  Qed.
+End AddCommExt_Opaque.
+
+Module AddCommExt_Transparent <: ADD_COMM_EXT.
+  Lemma add_comm_ext : forall n, (fun x => x + n) = (fun x => n + x).
+  Proof.
+    intro n; apply extensionality; auto with arith.
+  Qed.
+End AddCommExt_Transparent.
+
+Print Assumptions AddCommExt_Opaque.add_comm_ext.
+(* Should answer: extensionality *)
+
+Print Assumptions AddCommExt_Transparent.add_comm_ext.
+(* Should answer: extensionality *)
+
+Lemma add1_comm_ext_opaque :
+  (fun x => x + 1) = (fun x => 1 + x).
+Proof (AddCommExt_Opaque.add_comm_ext 1).
+
+Lemma add1_comm_ext_transparent :
+  (fun x => x + 1) = (fun x => 1 + x).
+Proof (AddCommExt_Transparent.add_comm_ext 1).
+
+Print Assumptions add1_comm_ext_opaque.
+(* Should answer: extensionality *)
+
+Print Assumptions add1_comm_ext_transparent.
+(* Should answer: extensionality *)
+
+Module Type FALSE_POSITIVE.
+  Axiom add_comm : forall n x, x + n = n + x.
+End FALSE_POSITIVE.
+
+Module false_positive : FALSE_POSITIVE.
+  Lemma add_comm : forall n x, x + n = n + x.
+  Proof. auto with arith. Qed.
+
+  Print Assumptions add_comm.
+  (* Should answer : Closed under the global context *)
+End false_positive.
+
+Lemma comm_plus5 : forall x,
+  x + 5 = 5 + x.
+Proof (false_positive.add_comm 5).
+
+Print Assumptions comm_plus5.
+(* Should answer : Closed under the global context *)