Transparent

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

6 files changed, 118 insertions, 37 deletions

diff --git a/library/declare.ml b/library/declare.ml
index d2e451dd9..b10658466 100644
--- a/library/declare.ml
+++ b/library/declare.ml
@@ -63,20 +63,19 @@ let make_strength_2 () =
   if depth > 2 then DischargeAt (list_firstn (List.length cwd -2) cwd, depth-2)
   else NeverDischarge
 
+
 (* Section variables. *)
 
 type section_variable_entry =
   | SectionLocalDef of constr
   | SectionLocalAssum of constr
 
-type sticky = bool
-
-type variable_declaration = section_variable_entry * strength * sticky
+type variable_declaration = section_variable_entry * strength
 
 type checked_section_variable = constr option * types * Univ.constraints
 
 type checked_variable_declaration =
-    checked_section_variable * strength * sticky
+    checked_section_variable * strength
 
 let vartab =
   ref ((Spmap.empty, []) :
@@ -91,7 +90,7 @@ let _ = Summary.declare_summary "VARIABLE"
 	    Summary.init_function = (fun () -> vartab := (Spmap.empty, []));
 	    Summary.survive_section = false }
 
-let cache_variable (sp,(id,(d,str,sticky))) =
+let cache_variable (sp,(id,(d,str))) =
   (* Constr raisonne sur les noms courts *)
   if List.mem_assoc id (current_section_context ()) then
     errorlabstrm "cache_variable"
@@ -101,7 +100,7 @@ let cache_variable (sp,(id,(d,str,sticky))) =
     | SectionLocalDef c -> Global.push_named_def (id,c)
   in
   Nametab.push 0 (restrict_path 0 sp) (VarRef sp);
-  vartab := let (m,l) = !vartab in (Spmap.add sp (id,(vd,str,sticky)) m, sp::l)
+  vartab := let (m,l) = !vartab in (Spmap.add sp (id,(vd,str)) m, sp::l)
 
 let (in_variable, out_variable) =
   let od = {
@@ -160,9 +159,7 @@ type constant_declaration_type =
   | ConstantEntry  of constant_entry
   | ConstantRecipe of Cooking.recipe
 
-type opacity = bool
-
-type constant_declaration = constant_declaration_type * strength * opacity
+type constant_declaration = constant_declaration_type * strength
 
 let csttab = ref (Spmap.empty : strength Spmap.t)
 
@@ -172,7 +169,7 @@ let _ = Summary.declare_summary "CONSTANT"
 	    Summary.init_function = (fun () -> csttab := Spmap.empty);
 	    Summary.survive_section = false }
 
-let cache_constant (sp,(cdt,stre,op)) =
+let cache_constant (sp,(cdt,stre)) =
   if Nametab.exists_cci sp then
     errorlabstrm "cache_constant"
       [< pr_id (basename sp); 'sTR " already exists" >] ;
@@ -190,12 +187,11 @@ let cache_constant (sp,(cdt,stre,op)) =
         (* All qualifications of Theorem, Lemma & Definition are visible *)
         Nametab.push 0 sp (ConstRef sp)
     | NotDeclare -> assert false);
-  if op then Global.set_opaque sp;
   csttab := Spmap.add sp stre !csttab
 
 (* At load-time, the segment starting from the module name to the discharge *)
 (* section (if Remark or Fact) is needed to access a construction *)
-let load_constant (sp,(ce,stre,op)) =
+let load_constant (sp,(ce,stre)) =
   if Nametab.exists_cci sp then
     errorlabstrm "cache_constant"
       [< pr_id (basename sp); 'sTR " already exists" >] ;
@@ -203,16 +199,17 @@ let load_constant (sp,(ce,stre,op)) =
   Nametab.push (depth_of_strength stre + 1) sp (ConstRef sp)
 
 (* Opening means making the name without its module qualification available *)
-let open_constant (sp,(_,stre,_)) =
+let open_constant (sp,(_,stre)) =
   let n = depth_of_strength stre in
   Nametab.push n (restrict_path n sp) (ConstRef sp)
 
 (* Hack to reduce the size of .vo: we keep only what load/open needs *)
 let dummy_constant_entry = ConstantEntry { 
   const_entry_body = mkProp;
-  const_entry_type = None }
+  const_entry_type = None;
+  const_entry_opaque = false }
 
-let export_constant (ce,stre,op) = Some (dummy_constant_entry,stre,op)
+let export_constant (ce,stre) = Some (dummy_constant_entry,stre)
 
 let (in_constant, out_constant) =
   let od = {
@@ -227,7 +224,8 @@ let hcons_constant_declaration = function
   | (ConstantEntry ce, stre) ->
       (ConstantEntry 
 	 { const_entry_body = hcons1_constr ce.const_entry_body;
-	   const_entry_type = option_app hcons1_constr ce.const_entry_type },
+	   const_entry_type = option_app hcons1_constr ce.const_entry_type;
+           const_entry_opaque = ce.const_entry_opaque },
 	 stre)
   | cd -> cd
 
@@ -328,17 +326,17 @@ let constant_or_parameter_strength sp =
   try constant_strength sp with Not_found -> NeverDischarge
 
 let get_variable sp = 
-  let (id,((c,ty,cst),str,sticky)) = Spmap.find sp (fst !vartab) in
+  let (id,((c,ty,cst),str)) = Spmap.find sp (fst !vartab) in
 (*  let (c,ty) = Global.lookup_named id in*)
-  ((id,c,ty),str,sticky)
+  ((id,c,ty),str)
 
 let get_variable_with_constraints sp = 
-  let (id,((c,ty,cst),str,sticky)) = Spmap.find sp (fst !vartab) in
+  let (id,((c,ty,cst),str)) = Spmap.find sp (fst !vartab) in
 (*  let (c,ty) = Global.lookup_named id in*)
-  ((id,c,ty),cst,str,sticky)
+  ((id,c,ty),cst,str)
 
 let variable_strength sp =
-  let _,(_,str,_) = Spmap.find sp (fst !vartab) in str
+  let _,(_,str) = Spmap.find sp (fst !vartab) in str
 
 (* Global references. *)
 
@@ -570,8 +568,11 @@ let declare_one_elimination mispec =
     let c = instantiate_inductive_section_params c (fst (mis_inductive mispec))
     in
     let _ = declare_constant (id_of_string na)
-      (ConstantEntry { const_entry_body = c; const_entry_type = None }, 
-       NeverDischarge,false) in
+      (ConstantEntry
+        { const_entry_body = c;
+          const_entry_type = None;
+          const_entry_opaque = false }, 
+       NeverDischarge) in
     Options.if_verbose pPNL [< 'sTR na; 'sTR " is defined" >]
   in
   let env = Global.env () in
diff --git a/library/declare.mli b/library/declare.mli
index 8d5744ad2..5563ebe9e 100644
--- a/library/declare.mli
+++ b/library/declare.mli
@@ -33,9 +33,7 @@ type section_variable_entry =
   | SectionLocalDef of constr
   | SectionLocalAssum of constr
 
-type sticky = bool
-
-type variable_declaration = section_variable_entry * strength * sticky
+type variable_declaration = section_variable_entry * strength
 
 val declare_variable : identifier -> variable_declaration -> variable_path
 
@@ -43,9 +41,7 @@ type constant_declaration_type =
   | ConstantEntry  of constant_entry
   | ConstantRecipe of Cooking.recipe
 
-type opacity = bool
-
-type constant_declaration = constant_declaration_type * strength * opacity
+type constant_declaration = constant_declaration_type * strength
 
 (* [declare_constant id cd] declares a global declaration
    (constant/parameter) with name [id] in the current section; it returns
@@ -78,9 +74,9 @@ val constant_strength : constant_path -> strength
 val constant_or_parameter_strength : constant_path -> strength
 
 val out_variable : Libobject.obj -> identifier * variable_declaration
-val get_variable : variable_path -> named_declaration * strength * sticky
+val get_variable : variable_path -> named_declaration * strength
 val get_variable_with_constraints : 
-  variable_path -> named_declaration * Univ.constraints * strength * sticky
+  variable_path -> named_declaration * Univ.constraints * strength
 val variable_strength : variable_path -> strength
 val find_section_variable : identifier -> variable_path
 val last_section_hyps : dir_path -> identifier list
diff --git a/library/global.ml b/library/global.ml
index 9dc5cdcd7..1f509bcde 100644
--- a/library/global.ml
+++ b/library/global.ml
@@ -61,9 +61,6 @@ let lookup_constant sp = lookup_constant sp !global_env
 let lookup_mind sp = lookup_mind sp !global_env
 let lookup_mind_specif c = lookup_mind_specif c !global_env
 
-let set_opaque sp = set_opaque !global_env sp
-let set_transparent sp = set_transparent !global_env sp
-
 let export s = export !global_env s
 let import cenv = global_env := import cenv !global_env
 
diff --git a/library/global.mli b/library/global.mli
index 0d0db36ce..a9cda1289 100644
--- a/library/global.mli
+++ b/library/global.mli
@@ -48,9 +48,6 @@ val lookup_constant : section_path -> constant_body
 val lookup_mind : section_path -> mutual_inductive_body
 val lookup_mind_specif : inductive -> inductive_instance
 
-val set_opaque : section_path -> unit
-val set_transparent : section_path -> unit
-
 val export : dir_path -> compiled_env
 val import : compiled_env -> unit
 
diff --git a/library/opaque.ml b/library/opaque.ml
new file mode 100644
index 000000000..26d2798b1
--- /dev/null
+++ b/library/opaque.ml
@@ -0,0 +1,60 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(*i $Id$ *)
+
+(*i*)
+open Util
+open Names
+open Closure
+open Summary
+open Term
+open Declarations
+(*i*)
+
+let tr_state = ref all_transparent
+
+let state () = !tr_state
+
+let _ = 
+  declare_summary "Transparent constants and variables"
+    { freeze_function = state;
+      unfreeze_function = (fun ts -> tr_state := ts);
+      init_function = (fun () -> tr_state := all_transparent);
+      survive_section = false }
+
+let is_evaluable env ref =
+  match ref with
+      EvalConstRef sp ->
+        let (ids,sps) = !tr_state in
+        Sppred.mem sp sps &
+        let cb = Environ.lookup_constant sp env in
+        cb.const_body <> None & not cb.const_opaque
+    | EvalVarRef id ->
+        let (ids,sps) = !tr_state in
+        Idpred.mem id ids &
+        Environ.lookup_named_value id env <> None
+
+(* Modifying this state *)
+let set_opaque_const sp =
+  let (ids,sps) = !tr_state in
+  tr_state := (ids, Sppred.remove sp sps)
+let set_transparent_const sp =
+  let (ids,sps) = !tr_state in
+  let cb = Global.lookup_constant sp in
+  if cb.const_body <> None & cb.const_opaque then
+    error ("Cannot make "^Global.string_of_global (ConstRef sp)^
+           " transparent because it was declared opaque.");
+  tr_state := (ids, Sppred.add sp sps)
+
+let set_opaque_var id =
+  let (ids,sps) = !tr_state in
+  tr_state := (Idpred.remove id ids, sps)
+let set_transparent_var id =
+  let (ids,sps) = !tr_state in
+  tr_state := (Idpred.add id ids, sps)
diff --git a/library/opaque.mli b/library/opaque.mli
new file mode 100644
index 000000000..47427a67b
--- /dev/null
+++ b/library/opaque.mli
@@ -0,0 +1,30 @@
+(***********************************************************************)
+(*  v      *   The Coq Proof Assistant  /  The Coq Development Team    *)
+(* <O___,, *        INRIA-Rocquencourt  &  LRI-CNRS-Orsay              *)
+(*   \VV/  *************************************************************)
+(*    //   *      This file is distributed under the terms of the      *)
+(*         *       GNU Lesser General Public License Version 2.1       *)
+(***********************************************************************)
+
+(*i $Id$ *)
+
+(*i*)
+open Names
+open Closure
+open Safe_typing
+open Environ
+(*i*)
+
+(* The current set of transparent constants and variables *)
+val state : unit -> transparent_state
+
+(* returns true if the global reference has a definition and that is
+   has not been set opaque *)
+val is_evaluable : env -> evaluable_global_reference -> bool
+
+(* Modifying this state *)
+val set_opaque_const : section_path -> unit
+val set_transparent_const : section_path -> unit
+
+val set_opaque_var : identifier -> unit
+val set_transparent_var : identifier -> unit