Minor cleanup around Term_typing

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

5 files changed, 40 insertions, 71 deletions

diff --git a/kernel/cooking.ml b/kernel/cooking.ml
index e8e35ee85..0ff7d64f0 100644
--- a/kernel/cooking.ml
+++ b/kernel/cooking.ml
@@ -119,6 +119,12 @@ type recipe = {
   d_abstract : named_context;
   d_modlist : work_list }
 
+type inline = bool
+
+type result =
+  constant_def * constant_type * Univ.constraints * inline
+    * Sign.section_context option
+
 let on_body f = function
   | Undef inl -> Undef inl
   | Def cs -> Def (Lazyconstr.from_val (f (Lazyconstr.force cs)))
@@ -151,4 +157,4 @@ let cook_constant env r =
 	let j = make_judge (constr_of_def body) typ in
 	Typeops.make_polymorphic_if_constant_for_ind env j
   in
-  (body, typ, cb.const_constraints, cb.const_inline_code, const_hyps)
+  (body, typ, cb.const_constraints, cb.const_inline_code, Some const_hyps)
diff --git a/kernel/cooking.mli b/kernel/cooking.mli
index 03acb87a9..d6280e119 100644
--- a/kernel/cooking.mli
+++ b/kernel/cooking.mli
@@ -21,9 +21,13 @@ type recipe = {
   d_abstract : Sign.named_context;
   d_modlist : work_list }
 
-val cook_constant :
-  env -> recipe ->
-    constant_def * constant_type * constraints * bool * Sign.section_context
+type inline = bool
+
+type result =
+  constant_def * constant_type * constraints * inline
+    * Sign.section_context option
+
+val cook_constant : env -> recipe -> result
 
 
 (** {6 Utility functions used in module [Discharge]. } *)
diff --git a/kernel/safe_typing.ml b/kernel/safe_typing.ml
index 932e43163..fa565fa34 100644
--- a/kernel/safe_typing.ml
+++ b/kernel/safe_typing.ml
@@ -65,7 +65,6 @@ open Declarations
 open Environ
 open Entries
 open Typeops
-open Term_typing
 open Modops
 open Subtyping
 open Mod_typing
@@ -247,13 +246,13 @@ let safe_push_named (id,_,_ as d) env =
   Environ.push_named d env
 
 let push_named_def (id,b,topt) senv =
-  let (c,typ,cst) = translate_local_def senv.env (b,topt) in
+  let (c,typ,cst) = Term_typing.translate_local_def senv.env (b,topt) in
   let senv' = add_constraints cst senv in
   let env'' = safe_push_named (id,Some c,typ) senv'.env in
   (cst, {senv' with env=env''})
 
 let push_named_assum (id,t) senv =
-  let (t,cst) = translate_local_assum senv.env t in
+  let (t,cst) = Term_typing.translate_local_assum senv.env t in
   let senv' = add_constraints cst senv in
   let env'' = safe_push_named (id,None,t) senv'.env in
   (cst, {senv' with env=env''})
@@ -268,9 +267,9 @@ type global_declaration =
 let add_constant dir l decl senv =
   let kn = make_con senv.modinfo.modpath dir l in
   let cb = match decl with
-    | ConstantEntry ce -> translate_constant senv.env kn ce
+    | ConstantEntry ce -> Term_typing.translate_constant senv.env ce
     | GlobalRecipe r ->
-      let cb = translate_recipe senv.env kn r in
+      let cb = Term_typing.translate_recipe senv.env r in
       if DirPath.is_empty dir then Declareops.hcons_const_body cb else cb
   in
   let senv' = add_field (l,SFBconst cb) (C kn) senv in
@@ -295,7 +294,7 @@ let add_mind dir l mie senv =
     anomaly (Pp.str "the label of inductive packet and its first inductive \
 	     type do not match");
   let kn = make_mind senv.modinfo.modpath dir l in
-  let mib = translate_mind senv.env kn mie in
+  let mib = Term_typing.translate_mind senv.env kn mie in
   let mib = match mib.mind_hyps with [] -> Declareops.hcons_mind mib | _ -> mib
   in
   let senv' = add_field (l,SFBmind mib) (I kn) senv in
diff --git a/kernel/term_typing.ml b/kernel/term_typing.ml
index 3ec0da457..c70a3f2eb 100644
--- a/kernel/term_typing.ml
+++ b/kernel/term_typing.ml
@@ -20,7 +20,6 @@ open Term
 open Declarations
 open Environ
 open Entries
-open Indtypes
 open Typeops
 
 let constrain_type env j cst1 = function
@@ -29,9 +28,9 @@ let constrain_type env j cst1 = function
   | Some t ->
       let (tj,cst2) = infer_type env t in
       let (_,cst3) = judge_of_cast env j DEFAULTcast tj in
-	assert (eq_constr t tj.utj_val);
-	let cstrs = union_constraints (union_constraints cst1 cst2) cst3 in
-	  NonPolymorphicType t, cstrs
+      assert (eq_constr t tj.utj_val);
+      let cstrs = union_constraints (union_constraints cst1 cst2) cst3 in
+      NonPolymorphicType t, cstrs
 
 let local_constrain_type env j cst1 = function
   | None ->
@@ -52,42 +51,10 @@ let translate_local_assum env t =
   let t = Typeops.assumption_of_judgment env j in
     (t,cst)
 
-(*
-
-(* Same as push_named, but check that the variable is not already
-   there. Should *not* be done in Environ because tactics add temporary
-   hypothesis many many times, and the check performed here would
-   cost too much. *)
-let safe_push_named (id,_,_ as d) env =
-  let _ =
-    try
-      let _ = lookup_named id env in
-      error ("Identifier "^Id.to_string id^" already defined.")
-    with Not_found -> () in
-  push_named d env
-
-let push_named_def = push_rel_or_named_def safe_push_named
-let push_rel_def = push_rel_or_named_def push_rel
-
-let push_rel_or_named_assum push (id,t) env =
-  let (j,cst) = safe_infer env t in
-  let t = Typeops.assumption_of_judgment env j in
-  let env' = add_constraints cst env in
-  let env'' = push (id,None,t) env' in
-  (cst,env'')
-
-let push_named_assum = push_rel_or_named_assum push_named
-let push_rel_assum d env = snd (push_rel_or_named_assum push_rel d env)
-
-let push_rels_with_univ vars env =
-  List.fold_left (fun env nvar -> push_rel_assum nvar env) env vars
-*)
-
 
 (* Insertion of constants and parameters in environment. *)
 
-let infer_declaration env dcl =
-  match dcl with
+let infer_declaration env = function
   | DefinitionEntry c ->
       let (j,cst) = infer env c.const_entry_body in
       let j =
@@ -113,7 +80,7 @@ let global_vars_set_constant_type env = function
 	  (fun t c -> Id.Set.union (global_vars_set env t) c))
       ctx ~init:Id.Set.empty
 
-let build_constant_declaration env kn (def,typ,cst,inline_code,ctx) =
+let build_constant_declaration env (def,typ,cst,inline_code,ctx) =
   let hyps = 
     let inferred =
       let ids_typ = global_vars_set_constant_type env typ in
@@ -144,14 +111,12 @@ let build_constant_declaration env kn (def,typ,cst,inline_code,ctx) =
 
 (*s Global and local constant declaration. *)
 
-let translate_constant env kn ce =
-  build_constant_declaration env kn (infer_declaration env ce)
+let translate_constant env ce =
+  build_constant_declaration env (infer_declaration env ce)
 
-let translate_recipe env kn r =
-  build_constant_declaration env kn 
-    (let def,typ,cst,inline,hyps = Cooking.cook_constant env r in
-     def,typ,cst,inline,Some hyps)
+let translate_recipe env r =
+  build_constant_declaration env (Cooking.cook_constant env r)
 
 (* Insertion of inductive types. *)
 
-let translate_mind env kn mie = check_inductive env kn mie
+let translate_mind env kn mie = Indtypes.check_inductive env kn mie
diff --git a/kernel/term_typing.mli b/kernel/term_typing.mli
index d001a258e..cc6025dab 100644
--- a/kernel/term_typing.mli
+++ b/kernel/term_typing.mli
@@ -9,29 +9,24 @@
 open Names
 open Term
 open Univ
-open Declarations
-open Inductive
 open Environ
+open Declarations
 open Entries
-open Typeops
 
 val translate_local_def : env -> constr * types option ->
-  constr * types * Univ.constraints
-
-val translate_local_assum : env -> types ->
-  types * Univ.constraints
-
-val infer_declaration : env -> constant_entry ->
-  constant_def * constant_type * constraints * bool * Sign.section_context option
+  constr * types * constraints
 
-val build_constant_declaration : env -> 'a ->
-  constant_def * constant_type * constraints * bool * Sign.section_context option -> 
-    constant_body
+val translate_local_assum : env -> types -> types * constraints
 
-val translate_constant : env -> constant -> constant_entry -> constant_body
+val translate_constant : env -> constant_entry -> constant_body
 
 val translate_mind :
   env -> mutual_inductive -> mutual_inductive_entry -> mutual_inductive_body
 
-val translate_recipe :
-  env -> constant -> Cooking.recipe -> constant_body
+val translate_recipe : env -> Cooking.recipe -> constant_body
+
+
+(** Internal functions, mentioned here for debug purpose only *)
+
+val infer_declaration : env -> constant_entry -> Cooking.result
+val build_constant_declaration : env -> Cooking.result -> constant_body