module Logic

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

9 files changed, 182 insertions, 55 deletions

diff --git a/kernel/environ.ml b/kernel/environ.ml
index f5de3e4e87..e431c1b374 100644
--- a/kernel/environ.ml
+++ b/kernel/environ.ml
@@ -47,6 +47,7 @@ let empty_env = {
 let universes env = env.env_universes
 let context env = env.env_context
 let evar_map env = env.env_evar_map
+let metamap env = failwith "Environ.metamap: TODO: unifier metas et VE"
 
 (* Construction functions. *)
 
diff --git a/kernel/environ.mli b/kernel/environ.mli
index cf89e6dcf7..684758d1e2 100644
--- a/kernel/environ.mli
+++ b/kernel/environ.mli
@@ -24,6 +24,7 @@ val empty_env : unsafe_env
 val universes : unsafe_env -> universes
 val context : unsafe_env -> context
 val evar_map : unsafe_env -> evar_map
+val metamap : unsafe_env -> (int * constr) list
 
 val push_var : identifier * typed_type -> unsafe_env -> unsafe_env
 val push_rel : name * typed_type -> unsafe_env -> unsafe_env
diff --git a/kernel/instantiate.ml b/kernel/instantiate.ml
index e1f9356df8..09265c988f 100644
--- a/kernel/instantiate.ml
+++ b/kernel/instantiate.ml
@@ -7,6 +7,7 @@ open Names
 open Generic
 open Term
 open Sign
+open Evd
 open Constant
 open Inductive
 open Environ
@@ -47,7 +48,7 @@ let constant_value env k =
 	    (ids_of_sign cb.const_hyps) body (Array.to_list args)
       | None -> 
 	  anomalylabstrm "termenv__constant_value"
-	    [< 'sTR "a defined constant as no body." >]
+	    [< 'sTR "a defined constant with no body." >]
   else 
     failwith "opaque"
 
@@ -63,3 +64,22 @@ let mis_lc env mis =
   instantiate_constr (ids_of_sign mis.mis_mib.mind_hyps) mis.mis_mip.mind_lc
     (Array.to_list mis.mis_args)
 
+(* Existentials. *)
+
+let name_of_existential n = id_of_string ("?" ^ string_of_int n)
+
+let existential_type env c =
+  let (n,args) = destEvar c in
+  let info = Evd.map (evar_map env) n in
+  let hyps = info.evar_hyps in
+  instantiate_constr (ids_of_sign hyps) info.evar_concl (Array.to_list args)
+
+let existential_value env c =
+  let (n,args) = destEvar c in
+  let info = Evd.map (evar_map env) n in
+  let hyps = info.evar_hyps in
+  match info.evar_body with
+    | Evar_defined c -> 
+	instantiate_constr (ids_of_sign hyps) c (Array.to_list args)
+    | Evar_empty ->
+	anomaly "a defined existential with no body"
diff --git a/kernel/instantiate.mli b/kernel/instantiate.mli
index cc63b9a547..8ea57f0887 100644
--- a/kernel/instantiate.mli
+++ b/kernel/instantiate.mli
@@ -18,6 +18,9 @@ val instantiate_type :
 val constant_value : unsafe_env -> constr -> constr
 val constant_type : unsafe_env -> constr -> typed_type
 
+val existential_value : unsafe_env -> constr -> constr
+val existential_type : unsafe_env -> constr -> constr
+
 val const_abst_opt_value : unsafe_env -> constr -> constr option
 
 val mis_lc : unsafe_env -> mind_specif -> constr
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 3d67e57d4e..e3b2d9f09f 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -17,8 +17,8 @@ exception Redelimination
 exception Induc
 exception Elimconst
 
-type 'a reduction_function = unsafe_env -> constr -> constr
-type 'a stack_reduction_function = 
+type reduction_function = unsafe_env -> constr -> constr
+type stack_reduction_function = 
     unsafe_env -> constr -> constr list -> constr * constr list
 
 (*************************************)
@@ -739,7 +739,7 @@ let pb_equal = function
   | CONV_LEQ -> CONV
   | CONV -> CONV
 
-type 'a conversion_function = unsafe_env -> constr -> constr -> constraints
+type conversion_function = unsafe_env -> constr -> constr -> constraints
 
 (* Conversion utility functions *)
 
@@ -936,13 +936,40 @@ let is_conv env = test_conversion conv env
 let is_conv_leq env = test_conversion conv_leq env
 
 
+(********************************************************************)
+(*             Special-Purpose Reduction                            *)
+(********************************************************************)
+
+let whd_meta env = function
+  | DOP0(Meta p) as u -> (try List.assoc p (metamap env) with Not_found -> u)
+  | x -> x
+	
+(* Try to replace all metas. Does not replace metas in the metas' values
+ * Differs from (strong whd_meta). *)
+let plain_instance s c = 
+  let rec irec = function
+    | DOP0(Meta p) as u -> (try List.assoc p s with Not_found -> u)
+    | DOP1(oper,c)      -> DOP1(oper, irec c)
+    | DOP2(oper,c1,c2)  -> DOP2(oper, irec c1, irec c2)
+    | DOPN(oper,cl)     -> DOPN(oper, Array.map irec cl)
+    | DOPL(oper,cl)     -> DOPL(oper, List.map irec cl)
+    | DLAM(x,c)         -> DLAM(x, irec c)
+    | DLAMV(x,v)        -> DLAMV(x, Array.map irec v)
+    | u                 -> u
+  in 
+  if s = [] then c else irec c
+    
+(* Pourquoi ne fait-on pas nf_betaiota si s=[] ? *)
+let instance s env c = 
+  if s = [] then c else nf_betaiota env (plain_instance s c)
+
 
 (* pseudo-reduction rule:
  * [hnf_prod_app env s (Prod(_,B)) N --> B[N]
  * with an HNF on the first argument to produce a product.
  * if this does not work, then we use the string S as part of our
- * error message.
- *)
+ * error message. *)
+
 let hnf_prod_app env s t n =
   match whd_betadeltaiota env t with
     | DOP2(Prod,_,b) -> sAPP b n
@@ -1304,6 +1331,56 @@ let poly_args env t =
     | _ -> []
 
 
+(* Expanding existential variables (trad.ml, progmach.ml) *)
+(* 1- whd_ise fails if an existential is undefined *)
+let rec whd_ise env = function
+  | DOPN(Evar sp,_) as k ->
+      let evm = evar_map env in
+      if Evd.in_dom evm sp then
+        if Evd.is_defined evm sp then
+          whd_ise env (constant_value env k)
+        else
+          errorlabstrm "whd_ise"
+            [< 'sTR"There is an unknown subterm I cannot solve" >]
+      else 
+	k
+  | DOP2(Cast,c,_) -> whd_ise env c
+  | DOP0(Sort(Type(_))) -> DOP0(Sort(Type(dummy_univ)))
+  | c -> c
+
+
+(* 2- undefined existentials are left unchanged *)
+let rec whd_ise1 env = function
+  | (DOPN(Evar sp,_) as k) ->
+      let evm = evar_map env in
+      if Evd.in_dom evm sp & Evd.is_defined evm sp then
+        whd_ise1 env (existential_value env k)
+      else 
+	k
+  | DOP2(Cast,c,_) -> whd_ise1 env c
+  | DOP0(Sort(Type _)) -> DOP0(Sort(Type dummy_univ))
+  | c -> c
+
+let nf_ise1 env = strong (whd_ise1 env) env
+
+(* Same as whd_ise1, but replaces the remaining ISEVAR by Metavariables
+ * Similarly we have is_fmachine1_metas and is_resolve1_metas *)
+
+let rec whd_ise1_metas env = function
+  | (DOPN(Evar n,_) as k) ->
+      let evm = evar_map env in
+      if Evd.in_dom evm n then
+	if Evd.is_defined evm n then
+      	  whd_ise1_metas env (existential_value env k)
+	else 
+      	  let m = DOP0(Meta (new_meta())) in
+	  DOP2(Cast,m,existential_type env k)
+      else
+	k
+  | DOP2(Cast,c,_) -> whd_ise1_metas env c
+  | c -> c
+
+
 (* Fonction spéciale qui laisse les cast clés sous les Fix ou les MutCase *)
 
 let under_outer_cast f = function
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index f24431a2f7..771899fad8 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -16,58 +16,58 @@ exception Redelimination
 exception Induc
 exception Elimconst
 
-type 'a reduction_function = unsafe_env -> constr -> constr
+type reduction_function = unsafe_env -> constr -> constr
 
-type 'a stack_reduction_function = 
+type stack_reduction_function = 
     unsafe_env -> constr -> constr list -> constr * constr list
 
-val whd_stack : 'a stack_reduction_function
+val whd_stack : stack_reduction_function
 
 (*s Reduction Function Operators *)
-val under_casts : 'a reduction_function -> 'a reduction_function
-val strong : 'a reduction_function -> 'a reduction_function
-val strong_prodspine : 'a reduction_function -> 'a reduction_function
+val under_casts : reduction_function -> reduction_function
+val strong : reduction_function -> reduction_function
+val strong_prodspine : reduction_function -> reduction_function
 val stack_reduction_of_reduction : 
-  'a reduction_function -> 'a stack_reduction_function
+  reduction_function -> stack_reduction_function
 
 (*s Generic Optimized Reduction Functions using Closures *)
 
 (* 1. lazy strategy *)
-val clos_norm_flags : Closure.flags -> 'a reduction_function
+val clos_norm_flags : Closure.flags -> reduction_function
 (* Same as [(strong whd_beta[delta][iota])], but much faster on big terms *) 
-val nf_beta : 'a reduction_function
-val nf_betaiota : 'a reduction_function
-val nf_betadeltaiota : 'a reduction_function
+val nf_beta : reduction_function
+val nf_betaiota : reduction_function
+val nf_betadeltaiota : reduction_function
 
 (* 2. call by value strategy *)
-val cbv_norm_flags : flags -> 'a reduction_function
-val cbv_beta : 'a reduction_function
-val cbv_betaiota : 'a reduction_function
-val cbv_betadeltaiota : 'a reduction_function
+val cbv_norm_flags : flags -> reduction_function
+val cbv_beta : reduction_function
+val cbv_betaiota : reduction_function
+val cbv_betadeltaiota : reduction_function
 
 (* 3. lazy strategy, weak head reduction *)
-val whd_beta : 'a reduction_function
-val whd_betaiota : 'a reduction_function
-val whd_betadeltaiota : 'a reduction_function
+val whd_beta : reduction_function
+val whd_betaiota : reduction_function
+val whd_betadeltaiota : reduction_function
 
-val whd_beta_stack : 'a stack_reduction_function
-val whd_betaiota_stack : 'a stack_reduction_function
-val whd_betadeltaiota_stack : 'a stack_reduction_function
+val whd_beta_stack : stack_reduction_function
+val whd_betaiota_stack : stack_reduction_function
+val whd_betadeltaiota_stack : stack_reduction_function
 
 
 (*s Head normal forms *)
-val whd_const_stack : section_path list -> 'a stack_reduction_function
-val whd_const : section_path list -> 'a reduction_function
-val whd_delta_stack : 'a stack_reduction_function
-val whd_delta : 'a reduction_function
-val whd_betadelta_stack : 'a stack_reduction_function
-val whd_betadelta : 'a reduction_function
-val whd_betadeltat_stack : 'a stack_reduction_function
-val whd_betadeltat : 'a reduction_function
-val whd_betadeltatiota_stack : 'a stack_reduction_function
-val whd_betadeltatiota : 'a reduction_function
-val whd_betadeltaiotaeta_stack : 'a stack_reduction_function
-val whd_betadeltaiotaeta : 'a reduction_function
+val whd_const_stack : section_path list -> stack_reduction_function
+val whd_const : section_path list -> reduction_function
+val whd_delta_stack : stack_reduction_function
+val whd_delta : reduction_function
+val whd_betadelta_stack : stack_reduction_function
+val whd_betadelta : reduction_function
+val whd_betadeltat_stack : stack_reduction_function
+val whd_betadeltat : reduction_function
+val whd_betadeltatiota_stack : stack_reduction_function
+val whd_betadeltatiota : reduction_function
+val whd_betadeltaiotaeta_stack : stack_reduction_function
+val whd_betadeltaiotaeta : reduction_function
 
 val beta_applist : (constr * constr list) -> constr
 
@@ -98,15 +98,15 @@ val is_info_cast_type : unsafe_env -> constr -> bool
 val contents_of_cast_type : unsafe_env -> constr -> contents
 val poly_args : unsafe_env -> constr -> int list
 
-val whd_programs : 'a reduction_function
+val whd_programs : reduction_function
 
 val unfoldn : 
-  (int list * section_path) list -> 'a reduction_function
-val fold_one_com : constr -> 'a reduction_function
-val fold_commands : constr list -> 'a reduction_function
+  (int list * section_path) list -> reduction_function
+val fold_one_com : constr -> reduction_function
+val fold_commands : constr list -> reduction_function
 val subst_term_occ : int list -> constr -> constr -> constr
-val pattern_occs : (int list * constr * constr) list -> 'a reduction_function
-val compute : 'a reduction_function
+val pattern_occs : (int list * constr * constr) list -> reduction_function
+val compute : reduction_function
 
 
 (*s Conversion Functions (uses closures, lazy strategy) *)
@@ -131,32 +131,45 @@ val convert_or : conversion_test -> conversion_test -> conversion_test
 val convert_forall2 : 
   ('a -> 'b -> conversion_test) -> 'a array -> 'b array -> conversion_test
 
-type 'a conversion_function = unsafe_env -> constr -> constr -> constraints
+type conversion_function = unsafe_env -> constr -> constr -> constraints
 
-val fconv : conv_pb -> 'a conversion_function
+val fconv : conv_pb -> conversion_function
 
 (* [fconv] has 2 instances: [conv = fconv CONV] i.e. conversion test, and
    [conv_leq = fconv CONV_LEQ] i.e. cumulativity test. *)
 
-val conv : 'a conversion_function
-val conv_leq : 'a conversion_function
+val conv : conversion_function
+val conv_leq : conversion_function
 
 val conv_forall2 : 
-  'a conversion_function -> unsafe_env 
-    -> constr array -> constr array -> constraints
+  conversion_function -> unsafe_env -> constr array 
+    -> constr array -> constraints
 
 val conv_forall2_i : 
-  (int -> 'a conversion_function) -> unsafe_env 
+  (int -> conversion_function) -> unsafe_env 
     -> constr array -> constr array -> constraints
 
 val is_conv : unsafe_env -> constr -> constr -> bool
 val is_conv_leq : unsafe_env -> constr -> constr -> bool
 
+
+(*s Special-Purpose Reduction Functions *)
+
+val whd_meta : reduction_function
+val plain_instance : (int * constr) list -> constr -> constr
+val instance : (int * constr) list -> reduction_function
+
+val whd_ise : reduction_function
+val whd_ise1 : reduction_function
+val nf_ise1 : reduction_function
+val whd_ise1_metas : reduction_function
+
+
 (*s Obsolete Reduction Functions *)
 
 val hnf : unsafe_env -> constr -> constr * constr list
-val apprec : 'a stack_reduction_function
-val red_product : 'a reduction_function
+val apprec : stack_reduction_function
+val red_product : reduction_function
 val find_mrectype : unsafe_env -> constr -> constr * constr list
 val find_minductype : unsafe_env -> constr -> constr * constr list
 val find_mcoinductype : unsafe_env -> constr -> constr * constr list
diff --git a/kernel/term.ml b/kernel/term.ml
index a1232ab5a9..5d9817fdef 100644
--- a/kernel/term.ml
+++ b/kernel/term.ml
@@ -353,7 +353,7 @@ let hd_app  = function
 
 (* Destructs a constant *)
 let destConst = function
-  | DOPN (Const  sp, a) -> (sp, a)
+  | DOPN (Const sp, a) -> (sp, a)
   | _ -> invalid_arg "destConst"
 
 let path_of_const = function
@@ -364,6 +364,11 @@ let args_of_const = function
   | DOPN (Const _,args) -> args
   | _ -> anomaly "args_of_const called with bad args"
 
+(* Destructs an existential variable *)
+let destEvar = function
+  | DOPN (Evar n, a) -> (n,a)
+  | _ -> invalid_arg "destEvar"
+
 (* Destructs an abstract term *)
 let destAbst = function
   | DOPN (Abst sp, a) -> (sp, a)
diff --git a/kernel/term.mli b/kernel/term.mli
index 8e16e8fbc3..1fa03507fd 100644
--- a/kernel/term.mli
+++ b/kernel/term.mli
@@ -272,6 +272,9 @@ val destConst : constr -> section_path * constr array
 val path_of_const : constr -> section_path
 val args_of_const : constr -> constr array
 
+(* Destructs an existential variable *)
+val destEvar : constr -> int * constr array
+
 (* Destrucy an abstract term *)
 val destAbst : constr -> section_path * constr array
 val path_of_abst : constr -> section_path
diff --git a/kernel/typeops.mli b/kernel/typeops.mli
index a95b54b66e..0a4419a608 100644
--- a/kernel/typeops.mli
+++ b/kernel/typeops.mli
@@ -33,6 +33,10 @@ val type_of_constructor : unsafe_env -> constr -> constr
 val type_of_case : unsafe_env -> unsafe_judgment -> unsafe_judgment 
   -> unsafe_judgment array -> unsafe_judgment
 
+val type_case_branches :
+  unsafe_env -> constr -> constr -> constr -> constr 
+    -> constr * constr array * constr 
+
 val type_of_prop_or_set : contents -> unsafe_judgment
 
 val type_of_type : universe -> unsafe_judgment * constraints