kernel/declarations becomes a pure mli

 - constr_substituted and lazy_constr are now in a dedicated kernel/lazyconstr.ml
 - the functions that were in declarations.ml (mostly substitution utilities
   and hashcons) are now in kernel/declareops.ml

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

9 files changed, 39 insertions, 29 deletions

diff --git a/plugins/extraction/extract_env.ml b/plugins/extraction/extract_env.ml
index 5aee45dcc..ae60259e9 100644
--- a/plugins/extraction/extract_env.ml
+++ b/plugins/extraction/extract_env.ml
@@ -136,7 +136,7 @@ let check_arity env cb =
 let check_fix env cb i =
   match cb.const_body with
     | Def lbody ->
-	(match kind_of_term (Declarations.force lbody) with
+	(match kind_of_term (Lazyconstr.force lbody) with
 	  | Fix ((_,j),recd) when i=j -> check_arity env cb; (true,recd)
 	  | CoFix (j,recd) when i=j -> check_arity env cb; (false,recd)
 	  | _ -> raise Impossible)
diff --git a/plugins/extraction/extraction.ml b/plugins/extraction/extraction.ml
index c8f376565..035f8e3bb 100644
--- a/plugins/extraction/extraction.ml
+++ b/plugins/extraction/extraction.ml
@@ -11,6 +11,7 @@ open Util
 open Names
 open Term
 open Declarations
+open Declareops
 open Environ
 open Reduction
 open Reductionops
@@ -277,7 +278,7 @@ let rec extract_type env db j c args =
 		  | Undef _ | OpaqueDef _ -> mlt
 		  | Def _ when is_custom r -> mlt
 		  | Def lbody ->
-		      let newc = applist (Declarations.force lbody, args) in
+		      let newc = applist (Lazyconstr.force lbody, args) in
 		      let mlt' = extract_type env db j newc [] in
 		      (* ML type abbreviations interact badly with Coq *)
 		      (* reduction, so [mlt] and [mlt'] might be different: *)
@@ -291,7 +292,7 @@ let rec extract_type env db j c args =
 		  | Undef _  | OpaqueDef _ -> Tunknown (* Brutal approx ... *)
 		  | Def lbody ->
 		      (* We try to reduce. *)
-		      let newc = applist (Declarations.force lbody, args) in
+		      let newc = applist (Lazyconstr.force lbody, args) in
 		      extract_type env db j newc []))
     | Ind (kn,i) ->
 	let s = (extract_ind env kn).ind_packets.(i).ip_sign in
@@ -515,7 +516,7 @@ and mlt_env env r = match r with
 	   | Def l_body ->
 	       (match flag_of_type env typ with
 		  | Info,TypeScheme ->
-		      let body = Declarations.force l_body in
+		      let body = Lazyconstr.force l_body in
 		      let s,vl = type_sign_vl env typ in
 		      let db = db_from_sign s in
 		      let t = extract_type_scheme env db body (List.length s)
@@ -986,17 +987,21 @@ let extract_constant env kn cb =
     | (Info,TypeScheme) ->
         (match cb.const_body with
 	  | Undef _ -> warn_info (); mk_typ_ax ()
-	  | Def c -> mk_typ (force c)
+	  | Def c -> mk_typ (Lazyconstr.force c)
 	  | OpaqueDef c ->
 	    add_opaque r;
-	    if access_opaque () then mk_typ (force_opaque c) else mk_typ_ax ())
+	    if access_opaque () then
+              mk_typ (Lazyconstr.force_opaque c)
+            else mk_typ_ax ())
     | (Info,Default) ->
         (match cb.const_body with
 	  | Undef _ -> warn_info (); mk_ax ()
-	  | Def c -> mk_def (force c)
+	  | Def c -> mk_def (Lazyconstr.force c)
 	  | OpaqueDef c ->
 	    add_opaque r;
-	    if access_opaque () then mk_def (force_opaque c) else mk_ax ())
+	    if access_opaque () then
+              mk_def (Lazyconstr.force_opaque c)
+            else mk_ax ())
 
 let extract_constant_spec env kn cb =
   let r = ConstRef kn in
@@ -1010,7 +1015,8 @@ let extract_constant_spec env kn cb =
 	  | Undef _ | OpaqueDef _ -> Stype (r, vl, None)
 	  | Def body ->
 	      let db = db_from_sign s in
-	      let t = extract_type_scheme env db (force body) (List.length s)
+              let body = Lazyconstr.force body in
+	      let t = extract_type_scheme env db body (List.length s)
 	      in Stype (r, vl, Some t))
     | (Info, Default) ->
 	let t = snd (record_constant_type env kn (Some typ)) in
@@ -1023,7 +1029,7 @@ let extract_with_type env cb =
 	let s,vl = type_sign_vl env typ in
 	let db = db_from_sign s in
 	let c = match cb.const_body with
-	  | Def body -> force body
+	  | Def body -> Lazyconstr.force body
 	  (* A "with Definition ..." is necessarily transparent *)
 	  | Undef _ | OpaqueDef _ -> assert false
 	in
diff --git a/plugins/extraction/mlutil.ml b/plugins/extraction/mlutil.ml
index 8ecd8cd7c..4407c6798 100644
--- a/plugins/extraction/mlutil.ml
+++ b/plugins/extraction/mlutil.ml
@@ -1289,6 +1289,7 @@ let is_not_strict t =
 *)
 
 open Declarations
+open Declareops
 
 let inline_test r t =
   if not (auto_inline ()) then false
diff --git a/plugins/funind/functional_principles_proofs.ml b/plugins/funind/functional_principles_proofs.ml
index 450b3ef40..3c92bb5bd 100644
--- a/plugins/funind/functional_principles_proofs.ml
+++ b/plugins/funind/functional_principles_proofs.ml
@@ -5,6 +5,7 @@ open Term
 open Namegen
 open Names
 open Declarations
+open Declareops
 open Pp
 open Hiddentac
 open Tacmach
@@ -947,7 +948,7 @@ let generate_equation_lemma fnames f fun_num nb_params nb_args rec_args_num =
   let f_def = Global.lookup_constant (destConst f) in
   let eq_lhs = mkApp(f,Array.init (nb_params + nb_args) (fun i -> mkRel(nb_params + nb_args - i))) in
   let f_body =
-    force (Option.get (body_of_constant f_def))
+    Lazyconstr.force (Option.get (body_of_constant f_def))
   in
   let params,f_body_with_params = decompose_lam_n nb_params f_body in
   let (_,num),(_,_,bodies) = destFix f_body_with_params in
@@ -1065,7 +1066,7 @@ let prove_princ_for_struct interactive_proof fun_num fnames all_funs _nparams :
     let get_body const =
       match body_of_constant (Global.lookup_constant const) with
 	| Some b ->
-	     let body = force b in
+	     let body = Lazyconstr.force b in
 	     Tacred.cbv_norm_flags
 	       (Closure.RedFlags.mkflags [Closure.RedFlags.fZETA])
 	       (Global.env ())
diff --git a/plugins/funind/functional_principles_types.ml b/plugins/funind/functional_principles_types.ml
index 9916ed95a..debf96345 100644
--- a/plugins/funind/functional_principles_types.ml
+++ b/plugins/funind/functional_principles_types.ml
@@ -5,6 +5,7 @@ open Term
 open Namegen
 open Names
 open Declarations
+open Declareops
 open Pp
 open Entries
 open Tactics
@@ -404,7 +405,7 @@ let get_funs_constant mp dp =
     let find_constant_body const =
       match body_of_constant (Global.lookup_constant const) with
 	| Some b ->
-	    let body = force b in
+	    let body = Lazyconstr.force b in
 	    let body = Tacred.cbv_norm_flags
 	      (Closure.RedFlags.mkflags [Closure.RedFlags.fZETA])
 	      (Global.env ())
@@ -539,7 +540,7 @@ let make_scheme (fas : (constant*glob_sort) list) : Entries.definition_entry lis
     let finfos = find_Function_infos this_block_funs.(0) in
     try
       let equation =  Option.get finfos.equation_lemma in
-      Declarations.is_opaque (Global.lookup_constant equation)
+      Declareops.is_opaque (Global.lookup_constant equation)
     with Option.IsNone -> (* non recursive definition *)
       false
   in
diff --git a/plugins/funind/indfun.ml b/plugins/funind/indfun.ml
index 99bf66d1f..fd4e23de7 100644
--- a/plugins/funind/indfun.ml
+++ b/plugins/funind/indfun.ml
@@ -8,6 +8,7 @@ open Libnames
 open Globnames
 open Glob_term
 open Declarations
+open Declareops
 open Misctypes
 open Decl_kinds
 
@@ -770,7 +771,7 @@ let make_graph (f_ref:global_reference) =
      | None -> error "Cannot build a graph over an axiom !"
      | Some b ->
 	 let env = Global.env () in
-	 let body = (force b) in
+	 let body = Lazyconstr.force b in
 	 let extern_body,extern_type =
 	   with_full_print
 	     (fun () ->
diff --git a/plugins/funind/indfun_common.ml b/plugins/funind/indfun_common.ml
index 92d2fe680..9879f08a0 100644
--- a/plugins/funind/indfun_common.ml
+++ b/plugins/funind/indfun_common.ml
@@ -121,8 +121,8 @@ let const_of_id id =
 let def_of_const t =
    match (Term.kind_of_term t) with
     Term.Const sp ->
-      (try (match Declarations.body_of_constant (Global.lookup_constant sp) with
-             | Some c -> Declarations.force c
+      (try (match Declareops.body_of_constant (Global.lookup_constant sp) with
+             | Some c -> Lazyconstr.force c
 	     | _ -> assert false)
        with _ -> assert false)
     |_ -> assert false
diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml
index d5e1ee53a..bea019259 100644
--- a/plugins/funind/recdef.ml
+++ b/plugins/funind/recdef.ml
@@ -10,6 +10,7 @@ open Term
 open Namegen
 open Environ
 open Declarations
+open Declareops
 open Entries
 open Pp
 open Names
@@ -68,7 +69,7 @@ let def_of_const t =
    match (kind_of_term t) with
     Const sp ->
       (try (match body_of_constant (Global.lookup_constant sp) with
-             | Some c -> Declarations.force c
+             | Some c -> Lazyconstr.force c
 	     | _ -> assert false)
        with _ ->
 	 anomaly (str "Cannot find definition of constant " ++
diff --git a/plugins/xml/xmlcommand.ml b/plugins/xml/xmlcommand.ml
index 033c84691..4d9541ebc 100644
--- a/plugins/xml/xmlcommand.ml
+++ b/plugins/xml/xmlcommand.ml
@@ -229,12 +229,11 @@ let mk_constant_obj id bo ty variables hyps =
       Acic.Constant (Names.Id.to_string id,None,ty,params)
    | Some c ->
       Acic.Constant
-       (Names.Id.to_string id, Some (Unshare.unshare (Declarations.force c)),
+       (Names.Id.to_string id, Some (Unshare.unshare (Lazyconstr.force c)),
          ty,params)
 ;;
 
 let mk_inductive_obj sp mib packs variables nparams hyps finite =
- let module D = Declarations in
   let hyps = string_list_of_named_context_list hyps in
   let params = filter_params variables hyps in
 (*  let nparams = extract_nparams packs in *)
@@ -243,8 +242,8 @@ let mk_inductive_obj sp mib packs variables nparams hyps finite =
     Array.fold_right
      (fun p i ->
        decr tyno ;
-       let {D.mind_consnames=consnames ;
-            D.mind_typename=typename } = p
+       let {Declarations.mind_consnames=consnames ;
+            Declarations.mind_typename=typename } = p
        in
         let arity = Inductive.type_of_inductive (Global.env()) (mib,p) in
         let lc = Inductiveops.arities_of_constructors (Global.env ()) (sp,!tyno) in
@@ -368,7 +367,7 @@ let print_object_kind uri (xmltag,variation) =
 (*       form of the definition (all the parameters are                   *)
 (*       lambda-abstracted, but the object can still refer to variables)  *)
 let print internal glob_ref kind xml_library_root =
- let module D = Declarations in
+ let module D = Declareops in
  let module De = Declare in
  let module G = Global in
  let module N = Names in
@@ -392,16 +391,16 @@ let print internal glob_ref kind xml_library_root =
        let id = N.Label.to_id (N.con_label kn) in
        let cb = G.lookup_constant kn in
        let val0 = D.body_of_constant cb in
-       let typ = cb.D.const_type in
-       let hyps = cb.D.const_hyps in
+       let typ = cb.Declarations.const_type in
+       let hyps = cb.Declarations.const_hyps in
        let typ = Typeops.type_of_constant_type (Global.env()) typ in
         Cic2acic.Constant kn,mk_constant_obj id val0 typ variables hyps
     | Gn.IndRef (kn,_) ->
        let mib = G.lookup_mind kn in
-       let {D.mind_nparams=nparams;
-	    D.mind_packets=packs ;
-            D.mind_hyps=hyps;
-            D.mind_finite=finite} = mib in
+       let {Declarations.mind_nparams=nparams;
+	    Declarations.mind_packets=packs ;
+            Declarations.mind_hyps=hyps;
+            Declarations.mind_finite=finite} = mib in
           Cic2acic.Inductive kn,mk_inductive_obj kn mib packs variables nparams hyps finite
     | Gn.ConstructRef _ ->
        Errors.error ("a single constructor cannot be printed in XML")