Optionally list opaque constants in addition to axions/variables in

assumptions. Feel free to rename "Print Opaque Dependencies" to
something better.


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

8 files changed, 60 insertions, 30 deletions

diff --git a/kernel/environ.ml b/kernel/environ.ml
index c43b633709..4fb5a2b1a0 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -554,7 +554,7 @@ fun env field value ->
 type context_object =
   | Variable of identifier (* A section variable or a Let definition *)
   | Axiom of constant      (* An axiom or a constant. *)
-
+  | Opaque of constant     (* An opaque constant. *)
 
 (* Defines a set of [assumption] *)
 module OrderedContextObject = 
@@ -566,15 +566,19 @@ struct
       | Axiom k1 , Axiom k2 -> Pervasives.compare k1 k2
 	          (* spiwack: it would probably be cleaner
 		     to provide a [kn_ord] function *)
+      | Opaque k1 , Opaque k2 -> Pervasives.compare k1 k2
       | Variable _ , Axiom _ -> -1
       | Axiom _ , Variable _ -> 1
+      | Opaque _ , _ -> -1
+      | _, Opaque _ -> 1
 end
 
 module ContextObjectSet = Set.Make (OrderedContextObject)
 module ContextObjectMap = Map.Make (OrderedContextObject)
 
 
-let assumptions (* t env *) =   
+let assumptions ?(add_opaque=false) st (* t env *) =
+  let (idts,knst) = st in
   (* Infix definition for chaining function that accumulate
      on a and a ContextObjectSet, ContextObjectMap.  *)
   let ( ** ) f1 f2 s m = let (s',m') = f1 s m in f2 s' m' in
@@ -650,16 +654,26 @@ let assumptions (* t env *) =
 
   and add_kn kn env s acc =
     let cb = lookup_constant kn env in
-    match cb.Declarations.const_body with
-    | None -> 
-	let ctype = 
-	  match cb.Declarations.const_type with
-	  | PolymorphicArity (ctx,a) -> mkArity (ctx, Type a.poly_level)
-	  | NonPolymorphicType t -> t
-	in
-	(s,ContextObjectMap.add (Axiom kn) ctype acc)
-    | Some body -> aux (Declarations.force body) env s acc
-
+    let do_type cst =
+      let ctype =
+	match cb.Declarations.const_type with
+	| PolymorphicArity (ctx,a) -> mkArity (ctx, Type a.poly_level)
+	| NonPolymorphicType t -> t
+      in
+	(s,ContextObjectMap.add cst ctype acc)
+    in
+    let (s,acc) =
+      if cb.Declarations.const_body <> None
+	&& (cb.Declarations.const_opaque || not (Cpred.mem kn knst))
+	&& add_opaque 
+      then
+	do_type (Opaque kn)
+      else (s,acc)
+    in
+      match cb.Declarations.const_body with
+      | None -> do_type (Axiom kn)
+      | Some body -> aux (Declarations.force body) env s acc
+	  
   and aux_memoize_kn kn env =
     try_and_go (Axiom kn) (add_kn kn env)
  in
diff --git a/kernel/environ.mli b/kernel/environ.mli
index b0dc2846f9..9e1afdf19b 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -244,13 +244,14 @@ val register : env -> field -> Retroknowledge.entry -> env
 type context_object =
   | Variable of identifier (* A section variable or a Let definition *)
   | Axiom of constant      (* An axiom or a constant. *)
+  | Opaque of constant     (* An opaque constant. *)
 
 (* AssumptionSet.t is a set of [assumption] *)
 module OrderedContextObject :  Set.OrderedType with type t = context_object
 module ContextObjectMap : Map.S with type key = context_object
 
-(* collects all the assumptions on which a term relies (together with
-   their type *)
-val assumptions : constr -> env -> Term.types ContextObjectMap.t
+(* collects all the assumptions (optionally including opaque definitions) 
+   on which a term relies (together with their type) *)
+val assumptions : ?add_opaque:bool -> transparent_state -> constr -> env -> Term.types ContextObjectMap.t
 
 
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 09b2f918f0..7469e12181 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -114,7 +114,7 @@ let add_constraints cst senv =
 (* terms which are closed under the environnement env, i.e
    terms which only depends on constant who are themselves closed *)
 let closed env term = 
-  ContextObjectMap.is_empty (assumptions env term)
+  ContextObjectMap.is_empty (assumptions full_transparent_state env term)
 
 (* the set of safe terms in an environement any recursive set of
    terms who are known not to prove inconsistent statement. It should
diff --git a/parsing/g_vernac.ml4 b/parsing/g_vernac.ml4
index dfe79a2543..ec1e7415bc 100644
--- a/parsing/g_vernac.ml4
+++ b/parsing/g_vernac.ml4
@@ -703,7 +703,8 @@ GEXTEND Gram
       | IDENT "Visibility"; s = OPT IDENT -> PrintVisibility s
       | IDENT "Implicit"; qid = global -> PrintImplicit qid
       | IDENT "Universes"; fopt = OPT ne_string -> PrintUniverses fopt
-      | IDENT "Assumptions"; qid = global -> PrintAssumptions qid ] ]
+      | IDENT "Assumptions"; qid = global -> PrintAssumptions (false, qid)
+      | IDENT "Opaque"; IDENT "Dependencies"; qid = global -> PrintAssumptions (true, qid) ] ]
   ;
   class_rawexpr:
     [ [ IDENT "Funclass" -> FunClass
diff --git a/parsing/ppvernac.ml b/parsing/ppvernac.ml
index b86f5ce660..4eb8ae9386 100644
--- a/parsing/ppvernac.ml
+++ b/parsing/ppvernac.ml
@@ -910,7 +910,8 @@ let rec pr_vernac = function
 	| PrintImplicit qid -> str"Print Implicit" ++ spc()  ++ pr_reference qid
 (* spiwack: command printing all the axioms and section variables used in a 
          term *)
-	| PrintAssumptions qid -> str"Print Assumptions"++spc()++pr_reference qid
+	| PrintAssumptions (b,qid) -> (if b then str"Print Assumptions" else str"Print Opaque Dependencies")
+	    ++spc()++pr_reference qid
       in pr_printable p
   | VernacSearch (sea,sea_r) -> pr_search sea sea_r pr_constr_pattern_expr
   | VernacLocate loc -> 
diff --git a/parsing/printer.ml b/parsing/printer.ml
index e2150fcbf8..f26d4d9cfc 100644
--- a/parsing/printer.ml
+++ b/parsing/printer.ml
@@ -498,10 +498,10 @@ let pr_assumptionset env s =
   if (Environ.ContextObjectMap.is_empty s) then
     str "Closed under the global context"
   else
-    let (vars,axioms) =
-      Environ.ContextObjectMap.fold (fun o typ r ->
-	let (v,a) = r in
-	match o with
+    let (vars,axioms,opaque) =
+      Environ.ContextObjectMap.fold (fun t typ r ->
+	let (v,a,o) = r in
+	match t with
 	| Variable id -> (  Some (
 	                      Option.default (fnl ()) v 
 			   ++ str (string_of_id id)
@@ -510,7 +510,7 @@ let pr_assumptionset env s =
 	                   ++ fnl ()
 			    )
 	                 ,
-	                   a )
+	                   a, o)
 	| Axiom kn    -> ( v ,
 			     Some (
 			      Option.default (fnl ()) a
@@ -519,16 +519,28 @@ let pr_assumptionset env s =
 	                   ++ pr_ltype typ
 	                   ++ fnl ()
 			     )
+			 , o
 			 )
-	)
-	s (None,None)
+	| Opaque kn    -> ( v , a ,
+			     Some (
+			      Option.default (fnl ()) o
+			   ++ (pr_constant env kn)
+	                   ++ str " : "
+	                   ++ pr_ltype typ
+	                   ++ fnl ()
+			     )
+			 )
+      )
+	s (None,None,None)
     in
-    let (vars,axioms) = 
+    let (vars,axioms,opaque) = 
       ( Option.map (fun p -> str "Section Variables:" ++ p) vars ,
-	Option.map (fun p -> str "Axioms:" ++ p) axioms 
+	Option.map (fun p -> str "Axioms:" ++ p) axioms ,
+	Option.map (fun p -> str "Opaque constants:" ++ p) opaque
       )
     in
     (Option.default (mt ()) vars) ++ (Option.default (mt ()) axioms)
+      ++ (Option.default (mt ()) opaque)
 
 let cmap_to_list m = Cmap.fold (fun k v acc -> v :: acc) m []
 
diff --git a/toplevel/vernacentries.ml b/toplevel/vernacentries.ml
index 4e9edd90a4..b146e0c506 100644
--- a/toplevel/vernacentries.ml
+++ b/toplevel/vernacentries.ml
@@ -1100,9 +1100,10 @@ let vernac_print = function
   | PrintAbout qid -> msgnl (print_about qid)
   | PrintImplicit qid -> msg (print_impargs qid)
 (*spiwack: prints all the axioms and section variables used by a term *)
-  | PrintAssumptions r ->
+  | PrintAssumptions (o,r) ->
       let cstr = constr_of_global (global_with_alias r) in
-      let nassumptions = Environ.assumptions cstr (Global.env ()) in
+      let nassumptions = Environ.assumptions (Conv_oracle.get_transp_state ())
+	~add_opaque:o cstr (Global.env ()) in
       msg (Printer.pr_assumptionset (Global.env ()) nassumptions)
 
 let global_module r =
diff --git a/toplevel/vernacexpr.ml b/toplevel/vernacexpr.ml
index 7a9e2b5a65..94ebce9ea7 100644
--- a/toplevel/vernacexpr.ml
+++ b/toplevel/vernacexpr.ml
@@ -65,7 +65,7 @@ type printable =
   | PrintVisibility of string option
   | PrintAbout of reference
   | PrintImplicit of reference
-  | PrintAssumptions of reference
+  | PrintAssumptions of bool * reference
 
 type search_about_item =
   | SearchSubPattern of constr_pattern_expr