modules Instantiate, Constant et Inductive

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

17 files changed, 495 insertions, 113 deletions

diff --git a/kernel/abstraction.mli b/kernel/abstraction.mli
new file mode 100644
index 0000000000..5d71a13192
--- /dev/null
+++ b/kernel/abstraction.mli
@@ -0,0 +1,11 @@
+
+(* $Id$ *)
+
+open Names
+open Term
+
+type abstraction_body = { 
+  abs_kind : path_kind;
+  abs_arity : int array;
+  abs_rhs : constr }
+
diff --git a/kernel/closure.ml b/kernel/closure.ml
index f4cee1c83a..f84b231d10 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -6,7 +6,9 @@ open Pp
 open Term
 open Generic
 open Names
+open Inductive
 open Environ
+open Instantiate
 open Univ
 open Evd
 
@@ -130,11 +132,12 @@ let red_under (md,r) rk =
  * after a Reset.  * This type is not exported. Only its two
  * instantiations (cbv or lazy) are.
  *)
+
 type ('a, 'b) infos = {
   i_flags : flags;
   i_repr : ('a, 'b) infos -> constr -> 'a;
-  i_env   : 'b unsafe_env;
-  i_tab   : (constr, 'a) Hashtbl.t }
+  i_env : 'b unsafe_env;
+  i_tab : (constr, 'a) Hashtbl.t }
 
 let const_value_cache info c =
   try  
@@ -302,6 +305,9 @@ let fixp_reducible redfun flgs op stk =
   else 
     false
 
+let mindsp_nparams env sp =
+  let mib = lookup_mind sp env in mib.mind_nparams
+
 (* The main recursive functions
  *
  * Go under applications and cases (pushed in the stack), expand head
@@ -311,8 +317,8 @@ let fixp_reducible redfun flgs op stk =
  * the function returns the pair of a cbv_value and its stack.  *
  * Invariant: if the result of norm_head is CONSTR or FIXP, it last
  * argument is [].  Because we must put all the applied terms in the
- * stack.
- *)
+ * stack. *)
+
 let rec norm_head info env t stack =
   (* no reduction under binders *)
   match t with
@@ -488,8 +494,10 @@ let cbv_norm infos constr =
  * between 2 lifted copies of a given term FFROZEN is a delayed
  * substitution applied to a constr
  *)
-type 'oper freeze =
-    { mutable norm: bool; mutable term: 'oper frterm }
+
+type 'oper freeze = { 
+  mutable norm: bool; 
+  mutable term: 'oper frterm }
 
 and 'oper frterm =
   | FRel of int
@@ -513,8 +521,8 @@ let is_val v = v.norm
  * interpretation of v1.
  *
  * The implementation without side effect, but losing sharing,
- * simply returns v2.
- *)
+ * simply returns v2. *)
+
 let freeze_assign v1 v2 =
   if !share then begin
       v1.norm <- v2.norm;
@@ -527,8 +535,8 @@ let freeze_assign v1 v2 =
  * resulting term takes advantage of any reduction performed in v.
  * i.e.: if (lift_frterm n v) yields w, reductions in w are reported
  * in w.term (yes: w.term, not only in w) The lifts are collapsed,
- * because we often insert lifts of 0. 
- *)
+ * because we often insert lifts of 0. *)
+
 let rec lift_frterm n v =
   match v.term with
     | FLIFT (k,f) -> lift_frterm (k+n) f
@@ -540,8 +548,7 @@ let rec lift_frterm n v =
 (* lift a freeze, keep sharing, but spare records when possible (case
  * n=0 ... ) The difference with lift_frterm is that reductions in v
  * are reported only in w, and not necessarily in w.term (with
- * notations above). 
- *)
+ * notations above). *)
 let lift_freeze n v =
   match (n, v.term) with
     | (0, _) | (_, (FOP0 _ | FVAR _)) -> v   (* identity lift or closed term *)
@@ -553,8 +560,8 @@ let freeze_vect env v = Array.map (freeze env) v
 let freeze_list env l = List.map (freeze env) l
 
 (* pourrait peut-etre remplacer freeze ?! (et alors FFROZEN
- * deviendrait inutile)
- *)
+ * deviendrait inutile) *)
+
 let rec traverse_term env t =
   match t with
     | Rel i -> (match expand_rel i env with
diff --git a/kernel/constant.ml b/kernel/constant.ml
new file mode 100644
index 0000000000..0b52af6956
--- /dev/null
+++ b/kernel/constant.ml
@@ -0,0 +1,33 @@
+
+(* $Id$ *)
+
+open Names
+open Generic
+open Term
+open Sign
+
+type discharge_recipe = {
+  d_expand : section_path list;
+  d_modify : (sorts oper * sorts oper modification) list;
+  d_abstract : identifier list;
+  d_from : section_path }
+
+type recipe =
+  | Cooked of constr
+  | Recipe of discharge_recipe
+
+type constant_body = {
+  const_kind : path_kind;
+  const_body : recipe ref option;
+  const_type : typed_type;
+  const_hyps : context;
+  mutable const_opaque : bool;
+  mutable const_eval : ((int * constr) list * int * bool) option option;
+}
+
+type constant_entry = section_path * constant_body
+
+let is_defined cb = 
+  match cb.const_body with Some _ -> true | _ -> false
+
+let is_opaque cb = cb.const_opaque
diff --git a/kernel/constant.mli b/kernel/constant.mli
index 7f52f94d46..60607cef25 100644
--- a/kernel/constant.mli
+++ b/kernel/constant.mli
@@ -16,7 +16,13 @@ type constant_body = {
   const_body : recipe ref option;
   const_type : typed_type;
   const_hyps : context;
+  mutable const_opaque : bool;
   mutable const_eval : ((int * constr) list * int * bool) option option;
 }
 
 type constant_entry = section_path * constant_body
+
+val is_defined : constant_body -> bool
+
+val is_opaque : constant_body -> bool
+
diff --git a/kernel/environ.ml b/kernel/environ.ml
index adf7cc9ff5..7086432acc 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -1,52 +1,223 @@
 
 (* $Id$ *)
 
+open Util
 open Names
 open Sign
 open Univ
+open Generic
 open Term
+open Evd
+open Constant
+open Inductive
+open Abstraction
+
+(* The type of environments. *)
+
+type globals = {
+  env_constants : constant_body Spmap.t;
+  env_inductives : mutual_inductive_body Spmap.t;
+  env_abstractions : abstraction_body Spmap.t }
 
 type 'a unsafe_env = {
-  context : environment;
-  inf_context : environment option;
-  sigma : 'a evar_map;
-  metamap : (int * constr) list;
-  constraints : universes
-}
+  env_context : environment;
+  env_globals : globals;
+  env_sigma : 'a evar_map;
+  env_metamap : (int * constr) list;
+  env_universes : universes }
+
+let universes env = env.env_universes
+let metamap env = env.env_metamap
+let evar_map env = env.env_sigma
+let context env = env.env_context
+
+(* Construction functions. *)
+
+let push_var idvar env =
+  { env with env_context = add_glob idvar env.env_context }
+
+let push_rel idrel env =
+  { env with env_context = add_rel idrel env.env_context }
+
+let set_universes g env =
+  if env.env_universes == g then env else { env with env_universes = g }
+
+let add_constant (sp,cb) env =
+  let new_constants = Spmap.add sp cb env.env_globals.env_constants in
+  let new_globals = { env.env_globals with env_constants = new_constants } in
+  { env with env_globals = new_globals }
+
+let add_mind (sp,mib) env =
+  let new_inds = Spmap.add sp mib env.env_globals.env_inductives in
+  let new_globals = { env.env_globals with env_inductives = new_inds } in
+  { env with env_globals = new_globals }
+  
+let new_meta = 
+  let meta_ctr = ref 0 in
+  fun () -> (incr meta_ctr; !meta_ctr)
+
+(* Access functions. *)
   
+let lookup_var id env =
+  let (_,var) = lookup_glob id env.env_context in
+  (Name id, var)
+
+let lookup_rel n env =
+  Sign.lookup_rel n env.env_context
+
+let lookup_constant sp env =
+  Spmap.find sp env.env_globals.env_constants
+
+let lookup_mind sp env =
+  Spmap.find sp env.env_globals.env_inductives
+
+let lookup_mind_specif i env =
+  match i with
+    | DOPN (MutInd (sp,tyi), args) ->
+	let mib = lookup_mind sp env in
+	{ mis_sp = sp; mis_mib = mib; mis_tyi = tyi; mis_args = args;
+	  mis_mip = mind_nth_type_packet mib tyi }
+    | _ -> invalid_arg "lookup_mind_specif"
+
+let mind_nparams env i =
+  let mis = lookup_mind_specif i env in mis.mis_mib.mind_nparams
+
+let lookup_meta n env =
+  List.assoc n env.env_metamap
+
+let lookup_abst sp env =
+  Spmap.find sp env.env_globals.env_abstractions
+
 (* First character of a constr *)
 
 let lowercase_first_char id = String.lowercase (first_char id)
 
-let rec hdchar = function
-  | DOP2(Prod,_,DLAM(_,c))     -> hdchar c
-  | DOP2(Cast,c,_)             -> hdchar c
-  | DOPN(AppL,cl)              -> hdchar (array_hd cl)
-  | DOP2(Lambda,_,DLAM(_,c))   -> hdchar c
-  | DOPN(Const _,_) as x ->
-      let c = lowercase_first_char (basename (path_of_const x)) in
-      if c = "?" then "y" else c
-  | DOPN(Abst _,_) as x ->
-      lowercase_first_char (basename (path_of_abst x))
-  | DOPN(MutInd (sp,i) as x,_) ->
-      if i=0 then 
-	lowercase_first_char (basename sp)
+(* id_of_global gives the name of the given sort oper *)
+let id_of_global env = function
+  | Const sp -> basename sp
+  | MutInd (sp,tyi) -> 
+      (* Does not work with extracted inductive types when the first 
+	 inductive is logic : if tyi=0 then basename sp else *)
+      let mib = lookup_mind sp env in
+      let mip = mind_nth_type_packet mib tyi in
+      mip.mind_typename
+  | MutConstruct ((sp,tyi),i) ->
+      let mib = lookup_mind sp env in
+      let mip = mind_nth_type_packet mib tyi in
+      if i <= Array.length mip.mind_consnames & i > 0 then
+        mip.mind_consnames.(i-1)
       else 
-	let na = id_of_global x in lowercase_first_char na
-  | DOPN(MutConstruct(sp,i) as x,_) ->
-      let na = id_of_global x  in String.lowercase(List.hd(explode_id na))
-  | VAR id  -> lowercase_first_char id
-  | DOP0(Sort s) -> sort_hdchar s
-  | _ -> "y"
-
-let id_of_name_using_hdchar a = function
-  | Anonymous -> id_of_string (hdchar a) 
+	failwith "id_of_global"
+  | _ -> assert false
+
+let hdchar env c = 
+  let rec hdrec = function
+    | DOP2(Prod,_,DLAM(_,c))     -> hdrec c
+    | DOP2(Cast,c,_)             -> hdrec c
+    | DOPN(AppL,cl)              -> hdrec (array_hd cl)
+    | DOP2(Lambda,_,DLAM(_,c))   -> hdrec c
+    | DOPN(Const _,_) as x ->
+	let c = lowercase_first_char (basename (path_of_const x)) in
+	if c = "?" then "y" else c
+    | DOPN(Abst _,_) as x ->
+	lowercase_first_char (basename (path_of_abst x))
+    | DOPN(MutInd (sp,i) as x,_) ->
+	if i=0 then 
+	  lowercase_first_char (basename sp)
+	else 
+	  let na = id_of_global env x in lowercase_first_char na
+    | DOPN(MutConstruct(sp,i) as x,_) ->
+	let na = id_of_global env x in String.lowercase(List.hd(explode_id na))
+    | VAR id  -> lowercase_first_char id
+    | DOP0(Sort s) -> sort_hdchar s
+    | _ -> "y"
+  in 
+  hdrec c
+
+let id_of_name_using_hdchar env a = function
+  | Anonymous -> id_of_string (hdchar env a) 
   | Name id   -> id
 
-let named_hd a = function
-  | Anonymous -> Name (id_of_string (hdchar a)) 
+let named_hd env a = function
+  | Anonymous -> Name (id_of_string (hdchar env a)) 
   | x         -> x
 
+let prod_name env (n,a,b) = mkProd (named_hd env a n) a b
+
+(* Abstractions. *)
+
+let evaluable_abst env = function
+  | DOPN (Abst _,_) -> true
+  | _ -> invalid_arg "evaluable_abst"
+
+let translucent_abst env = function
+  | DOPN (Abst _,_) -> false
+  | _ -> invalid_arg "translucent_abst"
+
+let abst_value env = function
+  | DOPN(Abst sp, args) ->
+    let ab = lookup_abst sp env in
+    if array_for_all2 (fun c i -> (count_dlam c) = i) args ab.abs_arity then
+      (* Sosub.soexecute (Array.fold_left sAPP ab.abs_rhs args) *)
+      failwith "todo: abstractions"
+    else 
+      failwith "contract_abstraction"
+  | _ -> invalid_arg "contract_abstraction"
+
+let defined_constant env = function
+  | DOPN (Const sp, _) ->
+      Constant.is_defined (lookup_constant sp env)
+  | _ -> invalid_arg "defined_constant"
+
+(* A constant is an existential if its name has the existential id prefix *)
+let existential_id_prefix = "?"
+
+let is_existential_id id =
+  atompart_of_id id = existential_id_prefix
+
+let is_existential_oper = function
+  | Const sp -> is_existential_id (basename sp)
+  | _ -> false
+
+let is_existential = function
+  | DOPN (oper, _) -> is_existential_oper oper
+  | _ -> false
+
+let defined_existential env = function
+  | DOPN (Const sp, _) -> 
+      Evd.is_defined env.env_sigma sp
+  | _ -> invalid_arg "defined_existential"
+
+let defined_const env c =
+  (defined_constant env c) || 
+  ((is_existential c) && (defined_existential env c))
+
+let translucent_const env c =
+  (is_existential c) && (defined_existential env c)
+
+(* A const is opaque if it is a non-defined existential or
+   a non-existential opaque constant *)
+
+let opaque_constant env = function
+  | DOPN (Const sp, _) -> 
+      Constant.is_opaque (lookup_constant sp env)
+  | _ -> invalid_arg "opaque_constant"
+
+let opaque_const env = function
+  | DOPN(Const sp,_) as k ->
+      if is_existential k then
+        not (defined_existential env k)
+      else 
+	opaque_constant env k
+  | _ -> invalid_arg "opaque_const"
+
+(* A const is evaluable if it is defined and not opaque *)
+let evaluable_const env k =
+  try 
+    defined_const env k && not (opaque_const env k)
+  with Not_found -> 
+    false
+
 (* Judgments. *)
 
 type unsafe_judgment = { 
diff --git a/kernel/environ.mli b/kernel/environ.mli
index 60006e82f8..686e871795 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -19,7 +19,6 @@ val context : 'a unsafe_env -> environment
 val push_var : identifier * typed_type -> 'a unsafe_env -> 'a unsafe_env
 val push_rel : name * typed_type -> 'a unsafe_env -> 'a unsafe_env
 val set_universes : universes -> 'a unsafe_env -> 'a unsafe_env
-
 val add_constant : constant_entry -> 'a unsafe_env -> 'a unsafe_env
 val add_mind : mutual_inductive_entry -> 'a unsafe_env -> 'a unsafe_env
 
@@ -27,15 +26,15 @@ val new_meta : unit -> int
 
 val lookup_var : identifier -> 'a unsafe_env -> name * typed_type
 val lookup_rel : int -> 'a unsafe_env -> name * typed_type
-val lookup_constant : section_path -> 'a unsafe_env -> constant_entry
-val lookup_mind : section_path -> 'a unsafe_env -> mutual_inductive_entry
+val lookup_constant : section_path -> 'a unsafe_env -> constant_body
+val lookup_mind : section_path -> 'a unsafe_env -> mutual_inductive_body
 val lookup_mind_specif : constr -> 'a unsafe_env -> mind_specif
 val lookup_meta : int -> 'a unsafe_env -> constr
 
 val id_of_global : 'a unsafe_env -> sorts oper -> identifier
 val id_of_name_using_hdchar : 'a unsafe_env -> constr -> name -> identifier
 val named_hd : 'a unsafe_env -> constr -> name -> name
-val prod_name : name * constr * constr -> constr
+val prod_name : 'a unsafe_env -> name * constr * constr -> constr
 
 val translucent_abst : 'a unsafe_env -> constr -> bool
 val evaluable_abst : 'a unsafe_env -> constr -> bool
@@ -44,18 +43,10 @@ val abst_value : 'a unsafe_env -> constr -> constr
 val defined_const : 'a unsafe_env -> constr -> bool
 val translucent_const : 'a unsafe_env -> constr -> bool
 val evaluable_const : 'a unsafe_env -> constr -> bool
-val const_value : 'a unsafe_env -> constr -> constr
-val const_type : 'a unsafe_env -> constr -> constr
-val const_of_path : 'a unsafe_env -> section_path -> constant_entry
 
 val is_existential : constr -> bool
 
-val const_abst_opt_value : 'a unsafe_env -> constr -> constr option
-
-val mind_of_path : section_path -> mutual_inductive_entry
-val mind_path : constr -> section_path
 val mind_nparams : 'a unsafe_env -> constr -> int
-val mindsp_nparams : 'a unsafe_env -> section_path -> int
 
 type unsafe_judgment = { 
   uj_val : constr;
diff --git a/kernel/evd.ml b/kernel/evd.ml
index 5b870d87af..24a50afa80 100644
--- a/kernel/evd.ml
+++ b/kernel/evd.ml
@@ -9,7 +9,8 @@ open Sign
 (* The type of mappings for existential variables *)
 
 type evar_body =
-    EVAR_EMPTY | EVAR_DEFINED of constr
+  | EVAR_EMPTY 
+  | EVAR_DEFINED of constr
 
 type 'a evar_info = {
   evar_concl : typed_type;        (* the type of the evar ...          *)
@@ -62,3 +63,6 @@ let non_instantiated sigma =
     [] listsp
     
 let is_evar sigma sp = in_dom sigma sp
+
+let is_defined sigma sp =
+  let info = map sigma sp in not (info.evar_body = EVAR_EMPTY)
diff --git a/kernel/evd.mli b/kernel/evd.mli
index bdbd759156..899abb2034 100644
--- a/kernel/evd.mli
+++ b/kernel/evd.mli
@@ -42,3 +42,6 @@ val define : 'a evar_map -> section_path -> constr -> 'a evar_map
 
 val non_instantiated : 'a evar_map -> (section_path * 'a evar_info) list
 val is_evar : 'a evar_map -> section_path -> bool
+
+val is_defined : 'a evar_map -> section_path -> bool
+
diff --git a/kernel/generic.ml b/kernel/generic.ml
index 9adc53ce68..3e33dca7b7 100644
--- a/kernel/generic.ml
+++ b/kernel/generic.ml
@@ -570,6 +570,9 @@ let rel_list n m =
   in 
   reln [] 1
 
+let rec count_dlam = function
+  | DLAM (_,c) -> 1 + (count_dlam c)
+  | _ -> 0
 
 (* Hash-consing *)
 let comp_term t1 t2 =
diff --git a/kernel/generic.mli b/kernel/generic.mli
index 20b24c68a9..40006fdf9d 100644
--- a/kernel/generic.mli
+++ b/kernel/generic.mli
@@ -113,6 +113,8 @@ val put_DLAMSV_subst : identifier list -> 'a term array -> 'a term
 val rel_vect : int -> int -> 'a term array
 val rel_list : int -> int -> 'a term list
 
+val count_dlam : 'a term -> int
+
 (* For hash-consing use *)
 val hash_term :
   ('a term -> 'a term)
diff --git a/kernel/inductive.ml b/kernel/inductive.ml
new file mode 100644
index 0000000000..2aedc8dfd0
--- /dev/null
+++ b/kernel/inductive.ml
@@ -0,0 +1,53 @@
+
+(* $Id$ *)
+
+open Names
+open Term
+open Sign
+
+type recarg = 
+  | Param of int 
+  | Norec 
+  | Mrec of int 
+  | Imbr of section_path * int * (recarg list)
+
+type mutual_inductive_packet = {
+  mind_consnames : identifier array;
+  mind_typename : identifier;
+  mind_lc : constr;
+  mind_stamp : name;
+  mind_arity : typed_type;
+  mind_lamexp : constr option;
+  mind_kd : sorts list;
+  mind_kn : sorts list;
+  mind_listrec : (recarg list) array;
+  mind_finite : bool }
+
+type mutual_inductive_body = {
+  mind_kind : path_kind;
+  mind_ntypes : int;
+  mind_hyps : typed_type signature;
+  mind_packets : mutual_inductive_packet array;
+  mind_singl : constr option;
+  mind_nparams : int }
+
+type mutual_inductive_entry = section_path * mutual_inductive_body
+
+let mind_type_finite mib i = mib.mind_packets.(i).mind_finite
+
+type mind_specif = {
+  mis_sp : section_path;
+  mis_mib : mutual_inductive_body;
+  mis_tyi : int;
+  mis_args : constr array;
+  mis_mip : mutual_inductive_packet }
+
+let mis_ntypes mis = mis.mis_mib.mind_ntypes
+let mis_nconstr mis = Array.length (mis.mis_mip.mind_consnames)
+let mis_nparams mis = mis.mis_mib.mind_nparams
+let mis_kd mis = mis.mis_mip.mind_kd
+let mis_kn mis = mis.mis_mip.mind_kn
+let mis_recargs mis =
+  Array.map (fun mip -> mip.mind_listrec) mis.mis_mib.mind_packets
+
+let mind_nth_type_packet mib n = mib.mind_packets.(n)
diff --git a/kernel/inductive.mli b/kernel/inductive.mli
index d3022c5697..7f2887f200 100644
--- a/kernel/inductive.mli
+++ b/kernel/inductive.mli
@@ -49,3 +49,5 @@ val mis_kd : mind_specif -> sorts list
 val mis_kn : mind_specif -> sorts list
 val mis_recargs : mind_specif -> (recarg list) array array
 
+val mind_nth_type_packet : 
+  mutual_inductive_body -> int -> mutual_inductive_packet
diff --git a/kernel/instantiate.ml b/kernel/instantiate.ml
new file mode 100644
index 0000000000..6302badc22
--- /dev/null
+++ b/kernel/instantiate.ml
@@ -0,0 +1,103 @@
+
+(* $Id$ *)
+
+open Pp
+open Util
+open Names
+open Generic
+open Term
+open Sign
+open Constant
+open Evd
+open Environ
+
+let is_id_inst ids args =
+  let is_id id = function
+    | VAR id' -> id = id'
+    | _ -> false
+  in
+  List.for_all2 is_id ids args
+
+let instantiate_constr ids c args =
+  if is_id_inst ids args then
+    c
+  else
+    replace_vars (List.combine ids (List.map make_substituend args)) c
+
+let instantiate_type ids tty args =
+  { body = instantiate_constr ids tty.body args;
+    typ = tty.typ }
+
+(* Constants. *)
+
+(* constant_type gives the type of a constant *)
+let constant_type env k =
+  let (sp,args) = destConst k in
+  let cb = lookup_constant sp env in
+  instantiate_type 
+    (ids_of_sign cb.const_hyps) cb.const_type (Array.to_list args)
+
+let constant_value env k =
+  let (sp,args) = destConst k in
+  let cb = lookup_constant sp env in
+  if not cb.const_opaque & defined_const env k then
+    match cb.const_body with
+      Some { contents = Cooked body } -> 
+        instantiate_constr 
+	  (ids_of_sign cb.const_hyps) body (Array.to_list args)
+    | Some { contents = Recipe _ } ->
+        anomalylabstrm "termenv__constant_value"
+          [< 'sTR "a transparent constant which was not cooked" >]
+    | None -> anomalylabstrm "termenv__constant_value"
+          [< 'sTR "a defined constant as no body." >]
+  else failwith "opaque"
+
+
+(* existential_type gives the type of an existential *)
+let existential_type env k = 
+  let (sp,args) = destConst k in
+  let evd = Evd.map (evar_map env) sp in
+  instantiate_constr 
+    (ids_of_sign evd.evar_hyps) evd.evar_concl.body (Array.to_list args)
+
+(* existential_value gives the value of a defined existential *)
+let existential_value env k =
+  let (sp,args) = destConst k in
+  if defined_const env k then
+    let evd = Evd.map (evar_map env) sp in
+    match evd.evar_body with
+      | EVAR_DEFINED c ->
+ 	  instantiate_constr (ids_of_sign evd.evar_hyps) c (Array.to_list args)
+      | _ -> anomalylabstrm "termenv__existential_value"
+            [< 'sTR"The existential variable code just registered a" ;
+               'sPC ; 'sTR"grave internal error." >]
+  else 
+    failwith "undefined existential"
+
+(* Constants or existentials. *)
+
+(* gives the value of a const *)
+let const_or_ex_value env = function
+  | DOPN (Const sp, _) as k -> 
+      if is_existential k then
+        existential_value env k
+      else 
+	constant_value env k
+  | _ -> invalid_arg "const_or_ex_value"
+
+(* gives the type of a const *)
+let const_or_ex_type env = function
+  | DOPN (Const sp, _) as k -> 
+      if is_existential k then
+	existential_type env k
+      else 
+	(constant_type env k).body
+  | _ -> invalid_arg "const_or_ex_type"
+
+let const_abst_opt_value env c =
+  match c with
+    | DOPN(Const sp,_) ->
+	if evaluable_const env c then Some (const_or_ex_value env c) else None
+    | DOPN(Abst sp,_) ->
+	if evaluable_abst env c then Some (abst_value env c) else None
+    | _ -> invalid_arg "const_abst_opt_value"
diff --git a/kernel/instantiate.mli b/kernel/instantiate.mli
new file mode 100644
index 0000000000..e0279abb1a
--- /dev/null
+++ b/kernel/instantiate.mli
@@ -0,0 +1,19 @@
+
+(* $Id$ *)
+
+open Names
+open Term
+open Environ
+
+val instantiate_constr : 
+  identifier list -> constr -> constr list -> constr
+val instantiate_type : 
+  identifier list -> typed_type -> constr list -> typed_type
+
+val constant_value : 'a unsafe_env -> constr -> constr
+val constant_type : 'a unsafe_env -> constr -> typed_type
+
+val const_or_ex_value : 'a unsafe_env -> constr -> constr
+val const_or_ex_type : 'a unsafe_env -> constr -> constr
+
+val const_abst_opt_value : 'a unsafe_env -> constr -> constr option
diff --git a/kernel/machops.ml b/kernel/machops.ml
index 8d79cac17f..afeb7f3fad 100644
--- a/kernel/machops.ml
+++ b/kernel/machops.ml
@@ -13,6 +13,7 @@ open Inductive
 open Sign
 open Environ
 open Reduction
+open Instantiate
 open Himsg
 
 type information = Logic | Inf of unsafe_judgment
@@ -90,32 +91,9 @@ let check_hyps id env hyps =
 
 (* Instantiation of terms on real arguments. *)
 
-let is_id_inst ids args =
-  let is_id id = function
-    | VAR id' -> id = id'
-    | _ -> false
-  in
-  List.for_all2 is_id ids args
-
-let instantiate_constr ids c args =
-  if is_id_inst ids args then
-    c
-  else
-    replace_vars (List.combine ids (List.map make_substituend args)) c
-
-let instantiate_type ids tty args =
-  { body = instantiate_constr ids tty.body args;
-    typ = tty.typ }
-
-(* Constants. *)
-
-let constant_reference env sp =
-  let (_,cb) = lookup_constant sp env in
-  (Const sp, construct_reference (basename sp) env cb.const_hyps)
-
 let type_of_constant env c =
   let (sp,args) = destConst c in
-  let (_,cb) = lookup_constant sp env in
+  let cb = lookup_constant sp env in
   let hyps = cb.const_hyps in
   check_hyps (basename sp) env hyps;
   instantiate_type (ids_of_sign hyps) cb.const_type (Array.to_list args)
@@ -204,7 +182,7 @@ let make_arity_dep env k =
   let rec mrec c m = match whd_betadeltaiota env c with 
     | DOP0(Sort _) -> mkArrow m k
     | DOP2(Prod,b,DLAM(n,c_0)) ->
-        prod_name (n,b,mrec c_0 (applist(lift 1 m,[Rel 1])))
+        prod_name env (n,b,mrec c_0 (applist(lift 1 m,[Rel 1])))
     | _ -> invalid_arg "make_arity_dep"
   in 
   mrec
@@ -274,7 +252,7 @@ let find_case_dep_nparams env (c,p) (mind,largs) typP =
 let type_one_branch_dep (env,nparams,globargs,p) co t = 
   let rec typrec n c =
     match whd_betadeltaiota env c with
-      | DOP2(Prod,a1,DLAM(x,a2)) -> prod_name (x,a1,typrec (n+1) a2)
+      | DOP2(Prod,a1,DLAM(x,a2)) -> prod_name env (x,a1,typrec (n+1) a2)
       | x -> let lAV = destAppL (ensure_appl x) in
              let (_,vargs) = array_chop (nparams+1) lAV in
              applist 
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index b78dab085e..f1eb159981 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -11,6 +11,7 @@ open Evd
 open Constant
 open Inductive
 open Environ
+open Instantiate
 open Closure
 
 let mt_evd = Evd.mt_evd
@@ -100,7 +101,7 @@ let red_product env c =
     match x with
       | DOPN(AppL,cl) -> 
 	  DOPN(AppL,Array.append [|redrec (array_hd cl)|] (array_tl cl))
-      | DOPN(Const _,_) when evaluable_const env x -> const_value env x
+      | DOPN(Const _,_) when evaluable_const env x -> const_or_ex_value env x
       | DOPN(Abst _,_) when evaluable_abst env x -> abst_value env x 
       | DOP2(Cast,c,_) -> redrec c
       | DOP2(Prod,a,DLAM(x,b)) -> DOP2(Prod, a, DLAM(x, redrec b))  
@@ -185,7 +186,7 @@ let rec substlin env name n ol c =
         if (path_of_const c)=name then
           if (List.hd ol)=n then
             if evaluable_const env c then 
-	      ((n+1),(List.tl ol), const_value env c)
+	      ((n+1),(List.tl ol), const_or_ex_value env c)
             else
               errorlabstrm "substlin"
                 [< 'sTR(string_of_path sp);
@@ -366,7 +367,7 @@ let whd_const_stack namelist env =
       | DOPN(Const sp,_) as c ->
 	  if List.mem sp namelist then
             if evaluable_const env c then
-              whrec (const_value env c) l
+              whrec (const_or_ex_value env c) l
             else 
 	      error "whd_const_stack"
 	  else 
@@ -394,7 +395,7 @@ let whd_delta_stack env =
     match x with
       | DOPN(Const _,_) as c ->
 	  if evaluable_const env c then
-            whrec (const_value env c) l
+            whrec (const_or_ex_value env c) l
 	  else 
 	    x,l
       | (DOPN(Abst _,_)) as c ->
@@ -416,7 +417,7 @@ let whd_betadelta_stack env =
     match x with
       | DOPN(Const _,_) ->
           if evaluable_const env x then 
-	    whrec (const_value env x) l
+	    whrec (const_or_ex_value env x) l
           else 
 	    (x,l)
       | DOPN(Abst _,_) ->
@@ -442,7 +443,7 @@ let whd_betadeltat_stack env =
     match x with
       | DOPN(Const _,_) ->
           if translucent_const env x then 
-	    whrec (const_value env x) l
+	    whrec (const_or_ex_value env x) l
           else 
 	    (x,l)
       | DOPN(Abst _,_) ->
@@ -467,7 +468,7 @@ let whd_betadeltaeta_stack env =
     match x with
       | DOPN(Const _,_) ->
           if evaluable_const env x then
-	    whrec (const_value env x) stack
+	    whrec (const_or_ex_value env x) stack
           else 
 	    (x,stack)
       | DOPN(Abst _,_) ->
@@ -525,7 +526,7 @@ let reduce_mind_case env mia =
   match mia.mconstr with 
     | DOPN(MutConstruct((indsp,tyindx),i),_) ->
 	let ind = DOPN(MutInd(indsp,tyindx),args_of_mconstr mia.mconstr) in
-	let nparams    = mind_nparams env ind in
+	let nparams = mind_nparams env ind in
 	let real_cargs = snd (list_chop nparams mia.mcargs) in
         applist (mia.mlf.(i-1),real_cargs)
     | DOPN(CoFix _,_) as cofix ->
@@ -607,7 +608,7 @@ let whd_betadeltatiota_stack env =
     match x with
       | DOPN(Const _,_) ->
           if translucent_const env x then
-            whrec (const_value env x) stack
+            whrec (const_or_ex_value env x) stack
           else 
 	    (x,stack)
       | DOPN(Abst _,_) ->
@@ -643,7 +644,7 @@ let whd_betadeltaiota_stack env =
     match x with
       | DOPN(Const _,_) ->
           if evaluable_const env x then
-	    bdi_rec (const_value env x) stack
+	    bdi_rec (const_or_ex_value env x) stack
           else 
 	    (x,stack)
       | DOPN(Abst _,_) ->
@@ -680,7 +681,7 @@ let whd_betadeltaiotaeta_stack env =
     match x with
       | DOPN(Const _,_) ->
           if evaluable_const env x then 
-	    whrec (const_value env x) stack
+	    whrec (const_or_ex_value env x) stack
           else 
 	    (x,stack)
       | DOPN(Abst _,_) ->
@@ -1067,7 +1068,7 @@ let reduce_mind_case_use_function env f mia =
   match mia.mconstr with 
     | DOPN(MutConstruct((indsp,tyindx),i),_) ->
 	let ind = DOPN(MutInd(indsp,tyindx),args_of_mconstr mia.mconstr) in
-	let nparams    = mind_nparams env ind in
+	let nparams = mind_nparams env ind in
 	let real_cargs = snd(list_chop nparams mia.mcargs) in
 	applist (mia.mlf.(i-1),real_cargs)
     | DOPN(CoFix _,_) as cofix ->
@@ -1081,7 +1082,7 @@ let special_red_case env whfun p c ci lf  =
     match constr with 
       | DOPN(Const _,_) as g -> 
           if (evaluable_const env g) then
-            let gvalue = (const_value env g) in
+            let gvalue = (const_or_ex_value env g) in
             if reducible_mind_case  gvalue then
               reduce_mind_case_use_function env g
                 {mP=p; mconstr=gvalue; mcargs=cargs; mci=ci; mlf=lf}
@@ -1173,7 +1174,7 @@ let is_elim env c =
   let (sp, cl) = destConst c in
   if evaluable_const env c && defined_const env c && (not (is_existential c))
   then
-    let (_,cb) = const_of_path env sp in 
+    let cb = lookup_constant sp env in 
     begin match cb.const_eval with
       | Some _ -> ()
       | None -> 
@@ -1238,7 +1239,7 @@ let make_elim_fun env f largs =
 let rec red_elim_const env k largs =
   if not(evaluable_const env k) then raise Redelimination else
     let f = make_elim_fun env k largs in
-    match whd_betadeltaeta_stack env (const_value env k) largs with
+    match whd_betadeltaeta_stack env (const_or_ex_value env k) largs with
       | (DOPN(MutCase _,_) as mc,lrest) ->
           let (ci,p,c,lf) = destCase mc in
           (special_red_case env (construct_const env) p c ci lf, lrest)
@@ -1259,7 +1260,7 @@ and construct_const env c stack =
            with 
 	     | Redelimination ->
 		 if evaluable_const env k then
-		   let cval = const_value env k in
+		   let cval = const_or_ex_value env k in
 		   (match cval with
 		      | DOPN (CoFix _,_) -> (k,stack)
                       | _                -> hnfstack cval stack) 
@@ -1303,7 +1304,7 @@ let hnf_constr env c =
              redrec c' lrest
            with Redelimination ->
              if evaluable_const env x then
-               let c = const_value env x in
+               let c = const_or_ex_value env x in
                match c with 
                  | DOPN(CoFix _,_) -> x
                  | _ ->  redrec c largs
@@ -1403,7 +1404,7 @@ let one_step_reduce env =
              applistc c' l
            with Redelimination ->
 	     if evaluable_const env x then
-	       applistc (const_value env x) largs
+	       applistc (const_or_ex_value env x) largs
 	     else 
 	       error "Not reductible 1")
       | DOPN(Abst _,_) ->
@@ -1523,10 +1524,6 @@ let reduce_to_mind env t =
   in 
   elimrec t []
     
-let reduce_to_ind env t =
-  let (mind,redt,c) = reduce_to_mind env t in
-  (mind_path mind, redt, c)
-
 let find_mrectype env c =
   let (t,l) = whd_betadeltaiota_stack env c [] in
   match t with
@@ -1537,14 +1534,14 @@ let find_minductype env c =
   let (t,l) = whd_betadeltaiota_stack env c [] in
   match t with
     | DOPN(MutInd (sp,i),_)
-        when mind_type_finite (snd (mind_of_path sp)) i -> (t,l)
+        when mind_type_finite (lookup_mind sp env) i -> (t,l)
     | _ -> raise Induc
 
 let find_mcoinductype env c =
   let (t,l) = whd_betadeltaiota_stack env c [] in
   match t with
     | DOPN(MutInd (sp,i),_)
-        when not (mind_type_finite (snd (mind_of_path sp)) i) -> (t,l)
+        when not (mind_type_finite (lookup_mind sp env) i) -> (t,l)
     | _ -> raise Induc
 
 let minductype_spec env c = 
@@ -1654,7 +1651,7 @@ let rec whd_ise env = function
   | DOPN(Const sp,_) as k ->
       if Evd.in_dom (evar_map env) sp then
         if defined_const env k then
-          whd_ise env (const_value env k)
+          whd_ise env (const_or_ex_value env k)
         else
           errorlabstrm "whd_ise"
             [< 'sTR"There is an unknown subterm I cannot solve" >]
@@ -1669,7 +1666,7 @@ let rec whd_ise env = function
 let rec whd_ise1 env = function
   | (DOPN(Const sp,_) as k) ->
       if Evd.in_dom (evar_map env) sp & defined_const env k then
-        whd_ise1 env (const_value env k)
+        whd_ise1 env (const_or_ex_value env k)
       else 
 	k
   | DOP2(Cast,c,_) -> whd_ise1 env c
@@ -1685,10 +1682,10 @@ let rec whd_ise1_metas env = function
   | (DOPN(Const sp,_) as k) ->
       if Evd.in_dom (evar_map env) sp then
 	if defined_const env k then
-      	  whd_ise1_metas env (const_value env k)
+      	  whd_ise1_metas env (const_or_ex_value env k)
 	else 
       	  let m = DOP0(Meta (new_meta())) in
-	  DOP2(Cast,m,const_type env k)
+	  DOP2(Cast,m,const_or_ex_type env k)
       else
 	k
   | DOP2(Cast,c,_) -> whd_ise1_metas env c
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index 7d3dd44b7a..cc5bfba3ea 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -110,8 +110,7 @@ val is_info_cast_type : 'c unsafe_env -> constr -> bool
 val contents_of_cast_type : 'c unsafe_env -> constr -> contents
 val poly_args : 'a unsafe_env -> constr -> int list
 val reduce_to_mind : 'c unsafe_env -> constr -> constr * constr * constr
-val reduce_to_ind  : 'c unsafe_env -> constr -> 
-                                section_path*constr*constr
+
 
 val whd_programs : 'a reduction_function