nouvel algo de conversion plus uniforme

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

5 files changed, 95 insertions, 105 deletions

diff --git a/pretyping/cbv.ml b/pretyping/cbv.ml
index 96af71ce6..fa1d9fa3a 100644
--- a/pretyping/cbv.ml
+++ b/pretyping/cbv.ml
@@ -91,6 +91,11 @@ let contract_cofixp env (i,(_,_,bds as bodies)) =
   in       
   subst_bodies_from_i 0 env, bds.(i)
 
+let make_constr_ref n = function
+  | FarRelKey p -> mkRel (n+p)
+  | VarKey id -> mkVar id
+  | ConstKey cst -> mkConst cst
+
 
 (* type of terms with a hole. This hole can appear only under App or Case.
  *   TOP means the term is considered without context
@@ -119,27 +124,13 @@ let stack_app appl stack =
     | (_, APP(args,stk)) -> APP(appl@args,stk)
     | _                  -> APP(appl, stack)
 
-(* Tests if we are in a case (modulo some applications) *)
-let under_case_stack = function
-  | (CASE _ | APP(_,CASE _)) -> true
-  | _ -> false
-
-(* Tells if the reduction rk is allowed by flags under a given stack.
- * The stack is useful when flags is (SIMPL,r) because in that case,
- * we perform bdi-reduction under the Case, or r-reduction otherwise
- *)
-let red_allowed flags stack rk =
-  if under_case_stack stack then 
-    red_under flags rk
-  else 
-    red_top flags rk
 
 open RedFlags
 
-let red_allowed_ref flags stack = function
-  | FarRelKey _ -> red_allowed flags stack fDELTA
-  | VarKey id -> red_allowed flags stack (fVAR id)
-  | ConstKey sp -> red_allowed flags stack (fCONST sp)
+let red_set_ref flags = function
+  | FarRelKey _ -> red_set flags fDELTA
+  | VarKey id -> red_set flags (fVAR id)
+  | ConstKey sp -> red_set flags (fCONST sp)
 
 (* Transfer application lists from a value to the stack
  * useful because fixpoints may be totally applied in several times
@@ -152,45 +143,29 @@ let strip_appl head stack =
     | _ -> (head, stack)
 
 
-(* Invariant: if the result of norm_head is CONSTR or (CO)FIXP, its last
- * argument is [].
- * Because we must put all the applied terms in the stack.
- *)
-let reduce_const_body redfun v stk =
-  if under_case_stack stk then strip_appl (redfun v) stk else strip_appl v stk
- 
-
 (* Tests if fixpoint reduction is possible. A reduction function is given as
    argument *)
-let rec check_app_constr redfun = function
+let rec check_app_constr = function
   | ([], _) -> false
   | ((CONSTR _)::_, 0) -> true
-  | (t::_, 0) -> (* TODO: partager ce calcul *)
-      (match redfun t with
-         | CONSTR _ -> true
-         | _ -> false)
-  | (_::l, n) -> check_app_constr redfun (l,(pred n))
+  | (_::l, n) -> check_app_constr (l,(pred n))
 	
-let fixp_reducible redfun flgs ((reci,i),_) stk =
-  if red_allowed flgs stk fIOTA then
+let fixp_reducible flgs ((reci,i),_) stk =
+  if red_set flgs fIOTA then
     match stk with               (* !!! for Acc_rec: reci.(i) = -2 *)
-      | APP(appl,_) -> reci.(i) >=0 & check_app_constr redfun (appl, reci.(i))
+      | APP(appl,_) -> reci.(i) >=0 & check_app_constr (appl, reci.(i))
       | _ -> false
   else 
     false
 
-let cofixp_reducible redfun flgs _ stk =
-  if red_allowed flgs stk fIOTA then
+let cofixp_reducible flgs _ stk =
+  if red_set flgs fIOTA then
     match stk with
       | (CASE _ | APP(_,CASE _)) -> true
       | _ -> false
   else 
     false
 
-let mindsp_nparams env (sp,i) =
-  let mib = lookup_mind sp env in
-  mib.Declarations.mind_packets.(i).Declarations.mind_nparams
-
 (* The main recursive functions
  *
  * Go under applications and cases (pushed in the stack), expand head
@@ -216,28 +191,23 @@ let rec norm_head info env t stack =
   (* constants, axioms
    * the first pattern is CRUCIAL, n=0 happens very often:
    * when reducing closed terms, n is always 0 *)
-  | Rel i -> (match expand_rel i env with
-                | Inl (0,v) ->
-                    reduce_const_body (cbv_norm_more info env) v stack
-                | Inl (n,v) ->
-                    reduce_const_body
-                      (cbv_norm_more info env) (shift_value n v) stack
-                | Inr (n,None) ->
-		    (VAL(0, mkRel n), stack)
-                | Inr (n,Some p) ->
-		    norm_head_ref (n-p) info env stack (FarRelKey p))
+  | Rel i ->
+      (match expand_rel i env with
+        | Inl (0,v)      -> strip_appl v stack
+        | Inl (n,v)      -> strip_appl (shift_value n v) stack
+        | Inr (n,None)   -> (VAL(0, mkRel n), stack)
+        | Inr (n,Some p) -> norm_head_ref (n-p) info env stack (FarRelKey p))
 
   | Var id -> norm_head_ref 0 info env stack (VarKey id)
 
-  | Const sp ->
-      norm_head_ref 0 info env stack (ConstKey sp)
+  | Const sp -> norm_head_ref 0 info env stack (ConstKey sp)
 
   | LetIn (x, b, t, c) ->
       (* zeta means letin are contracted; delta without zeta means we *)
       (* allow substitution but leave let's in place *)
-      let zeta = red_allowed (info_flags info) stack fZETA in
+      let zeta = red_set (info_flags info) fZETA in
       let env' =
-	if zeta or red_allowed (info_flags info) stack fDELTA then 
+	if zeta or red_set (info_flags info) fDELTA then 
 	  subs_cons (cbv_stack_term info TOP env b,env)
 	else
 	  subs_lift env in
@@ -264,17 +234,11 @@ let rec norm_head info env t stack =
 	     stack)
 
 and norm_head_ref k info env stack normt =
-  if red_allowed_ref (info_flags info) stack normt then
+  if red_set_ref (info_flags info) normt then
     match ref_value_cache info normt with
-      | Some body ->
-	  reduce_const_body (cbv_norm_more info env) (shift_value k body) stack
-      | None -> (VAL(0,make_constr_ref k info normt), stack)
-  else (VAL(0,make_constr_ref k info normt), stack)
-
-and make_constr_ref n info = function
-  | FarRelKey p -> mkRel (n+p)
-  | VarKey id -> mkVar id
-  | ConstKey cst -> mkConst cst
+      | Some body -> strip_appl (shift_value k body) stack
+      | None -> (VAL(0,make_constr_ref k normt), stack)
+  else (VAL(0,make_constr_ref k normt), stack)
 
 (* cbv_stack_term performs weak reduction on constr t under the subs
  * env, with context stack, i.e. ([env]t stack).  First computes weak
@@ -286,32 +250,31 @@ and cbv_stack_term info stack env t =
   match norm_head info env t stack with
     (* a lambda meets an application -> BETA *)
     | (LAM (x,a,b,env), APP (arg::args, stk))
-      when red_allowed (info_flags info) stk fBETA ->
+      when red_set (info_flags info) fBETA ->
         let subs = subs_cons (arg,env) in
           cbv_stack_term info (stack_app args stk) subs b
 
     (* a Fix applied enough -> IOTA *)
     | (FIXP(fix,env,_), stk)
-        when fixp_reducible (cbv_norm_more info env) (info_flags info) fix stk ->
+        when fixp_reducible (info_flags info) fix stk ->
         let (envf,redfix) = contract_fixp env fix in
         cbv_stack_term info stk envf redfix
 
     (* constructor guard satisfied or Cofix in a Case -> IOTA *)
     | (COFIXP(cofix,env,_), stk)
-        when cofixp_reducible (cbv_norm_more info env) (info_flags info) cofix stk->
+        when cofixp_reducible (info_flags info) cofix stk->
         let (envf,redfix) = contract_cofixp env cofix in
         cbv_stack_term info stk envf redfix
 
-    (* constructor in a Case -> IOTA
-       (use red_under because we know there is a Case) *)
+    (* constructor in a Case -> IOTA *)
     | (CONSTR((sp,n),_), APP(args,CASE(_,br,ci,env,stk)))
-            when red_under (info_flags info) fIOTA ->
+            when red_set (info_flags info) fIOTA ->
 	let real_args = snd (list_chop ci.ci_npar args) in
         cbv_stack_term info (stack_app real_args stk) env br.(n-1)
          
-    (* constructor of arity 0 in a Case -> IOTA ( "   " )*)
+    (* constructor of arity 0 in a Case -> IOTA *)
     | (CONSTR((_,n),_), CASE(_,br,_,env,stk))
-                  when red_under (info_flags info) fIOTA ->
+            when red_set (info_flags info) fIOTA ->
                     cbv_stack_term info stk env br.(n-1)
 
     (* may be reduced later by application *)  
@@ -324,14 +287,6 @@ and cbv_stack_term info stack env t =
     | (head,stk) -> VAL(0,apply_stack info (cbv_norm_value info head) stk)
 
 
-(* if we are in SIMPL mode, maybe v isn't reduced enough *)
-and cbv_norm_more info env v =
-  match (v, (info_flags info)) with
-    | (VAL(k,t), ((SIMPL|WITHBACK),_)) ->
-        cbv_stack_term (infos_under info) TOP (subs_shft (k,env)) t
-    | _ -> v
-
-
 (* When we are sure t will never produce a redex with its stack, we
  * normalize (even under binders) the applied terms and we build the
  * final term
diff --git a/pretyping/cbv.mli b/pretyping/cbv.mli
index 000ed4e3f..6c9ebde6f 100644
--- a/pretyping/cbv.mli
+++ b/pretyping/cbv.mli
@@ -9,10 +9,8 @@
 (*i $Id$ i*)
 
 (*i*)
-open Pp
 open Names
 open Term
-open Evd
 open Environ
 open Closure
 open Esubst
@@ -23,8 +21,9 @@ open Esubst
 
 (* Entry point for cbv normalization of a constr *)
 type cbv_infos
-val create_cbv_infos : flags -> env -> cbv_infos
-val cbv_norm : cbv_infos -> constr -> constr
+
+val create_cbv_infos : RedFlags.reds -> env -> cbv_infos
+val cbv_norm         : cbv_infos -> constr -> constr
 
 (***********************************************************************)
 (*i This is for cbv debug *)
@@ -43,19 +42,12 @@ type cbv_stack =
   | CASE of constr * constr array * case_info * cbv_value subs * cbv_stack
 
 val stack_app : cbv_value list -> cbv_stack -> cbv_stack
-val under_case_stack : cbv_stack -> bool
 val strip_appl : cbv_value -> cbv_stack -> cbv_value * cbv_stack
 
-open RedFlags
-val red_allowed : flags -> cbv_stack -> red_kind -> bool
-val reduce_const_body :
-  (cbv_value -> cbv_value) -> cbv_value -> cbv_stack -> cbv_value * cbv_stack
-
 (* recursive functions... *)
 val cbv_stack_term : cbv_infos ->
   cbv_stack -> cbv_value subs -> constr -> cbv_value
 val cbv_norm_term : cbv_infos -> cbv_value subs -> constr -> constr
-val cbv_norm_more : cbv_infos -> cbv_value subs -> cbv_value -> cbv_value
 val norm_head : cbv_infos ->
   cbv_value subs -> constr -> cbv_stack -> cbv_value * cbv_stack
 val apply_stack : cbv_infos -> constr -> cbv_stack -> constr
diff --git a/pretyping/reductionops.mli b/pretyping/reductionops.mli
index d545e96cb..a1291284f 100644
--- a/pretyping/reductionops.mli
+++ b/pretyping/reductionops.mli
@@ -56,7 +56,7 @@ val stacklam : (state -> 'a) -> constr list -> constr -> constr stack -> 'a
 
 (*s Generic Optimized Reduction Function using Closures *)
 
-val clos_norm_flags : Closure.flags -> reduction_function
+val clos_norm_flags : Closure.RedFlags.reds -> reduction_function
 (* Same as [(strong whd_beta[delta][iota])], but much faster on big terms *) 
 val nf_beta : local_reduction_function
 val nf_betaiota : local_reduction_function
diff --git a/pretyping/tacred.ml b/pretyping/tacred.ml
index 854a61b26..6c38f6d9a 100644
--- a/pretyping/tacred.ml
+++ b/pretyping/tacred.ml
@@ -14,6 +14,7 @@ open Names
 open Nameops
 open Term
 open Termops
+open Declarations
 open Inductive
 open Environ
 open Reductionops
@@ -24,6 +25,39 @@ open Cbv
 exception Elimconst
 exception Redelimination
 
+let set_opaque_const = Conv_oracle.set_opaque_const
+let set_transparent_const sp =
+  let cb = Global.lookup_constant sp in
+  if cb.const_body <> None & cb.const_opaque then
+    errorlabstrm "set_transparent_const"
+      [< 'sTR "Cannot make"; 'sPC; 
+         Nametab.pr_global_env (Global.env()) (Nametab.ConstRef sp);
+         'sPC; 'sTR "transparent because it was declared opaque." >];
+  Conv_oracle.set_transparent_const sp
+
+let set_opaque_var      = Conv_oracle.set_opaque_var
+let set_transparent_var = Conv_oracle.set_transparent_var
+
+let _ = 
+  Summary.declare_summary "Transparent constants and variables"
+    { Summary.freeze_function = Conv_oracle.freeze;
+      Summary.unfreeze_function = Conv_oracle.unfreeze;
+      Summary.init_function = Conv_oracle.init;
+      Summary.survive_section = false }
+
+let is_evaluable env ref =
+  match ref with
+      EvalConstRef sp ->
+        let (ids,sps) = Conv_oracle.freeze() 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) = Conv_oracle.freeze() in
+        Idpred.mem id ids &
+        let (_,value,_) = Environ.lookup_named id env in
+        value <> None
+
 type evaluable_reference =
   | EvalConst of constant
   | EvalVar of identifier
@@ -37,8 +71,8 @@ let mkEvalRef = function
   | EvalEvar ev -> mkEvar ev
 
 let isEvalRef env c = match kind_of_term c with
-  | Const sp -> Opaque.is_evaluable env (EvalConstRef sp)
-  | Var id -> Opaque.is_evaluable env (EvalVarRef id)
+  | Const sp -> is_evaluable env (EvalConstRef sp)
+  | Var id -> is_evaluable env (EvalVarRef id)
   | Rel _ | Evar _ -> true
   | _ -> false
 
@@ -353,7 +387,7 @@ let special_red_case env whfun (ci, p, c, lf)  =
     let (constr, cargs) = whfun s in 
     match kind_of_term constr with 
       | Const cst -> 
-          (if not (Opaque.is_evaluable env (EvalConstRef cst)) then
+          (if not (is_evaluable env (EvalConstRef cst)) then
             raise Redelimination;
 	  let gvalue = constant_value env cst in
 	  if reducible_mind_case gvalue then
@@ -449,7 +483,7 @@ and construct_const env sigma =
 (* Red reduction tactic: reduction to a product *)
 
 let internal_red_product env sigma c = 
-  let simpfun = clos_norm_flags (UNIFORM,betaiotazeta_red) env sigma in
+  let simpfun = clos_norm_flags betaiotazeta env sigma in
   let rec redrec env x =
     match kind_of_term x with
       | App (f,l) -> 
@@ -660,8 +694,8 @@ let string_of_evaluable_ref = function
   | EvalConstRef sp -> string_of_path sp
 
 let unfold env sigma name =
-  if Opaque.is_evaluable env name then
-    clos_norm_flags (unfold_flags name) env sigma
+  if is_evaluable env name then
+    clos_norm_flags (unfold_red name) env sigma
   else
     error (string_of_evaluable_ref name^" is opaque")
 
@@ -728,8 +762,8 @@ type red_expr =
   | Red of bool
   | Hnf
   | Simpl
-  | Cbv of Closure.flags
-  | Lazy of Closure.flags
+  | Cbv of Closure.RedFlags.reds
+  | Lazy of Closure.RedFlags.reds
   | Unfold of (int list * evaluable_global_reference) list
   | Fold of constr list
   | Pattern of (int list * constr * constr) list
@@ -787,7 +821,7 @@ let one_step_reduce env sigma c =
 
 let reduce_to_ind_gen allow_product env sigma t = 
   let rec elimrec env t l = 
-    let c, _ = whd_stack t in
+    let c, _ = Reductionops.whd_stack t in
     match kind_of_term c with
       | Ind (mind,args) -> ((mind,args),it_mkProd_or_LetIn t l)
       | Prod (n,ty,t') ->
diff --git a/pretyping/tacred.mli b/pretyping/tacred.mli
index 1b87dc712..4100a31ae 100644
--- a/pretyping/tacred.mli
+++ b/pretyping/tacred.mli
@@ -19,6 +19,8 @@ open Closure
 
 (*s Reduction functions associated to tactics. \label{tacred} *)
 
+val is_evaluable : env -> evaluable_global_reference -> bool
+
 exception Redelimination
 
 (* Red (raise Redelimination if nothing reducible) *)
@@ -42,7 +44,7 @@ val pattern_occs : (int list * constr * constr) list ->  reduction_function
 (* Rem: Lazy strategies are defined in Reduction *)
 
 (* Call by value strategy (uses Closures) *)
-val cbv_norm_flags : Closure.flags ->  reduction_function
+val cbv_norm_flags : Closure.RedFlags.reds ->  reduction_function
   val cbv_beta : local_reduction_function
   val cbv_betaiota : local_reduction_function
   val cbv_betadeltaiota :  reduction_function
@@ -62,10 +64,17 @@ type red_expr =
   | Red of bool    (* raise Redelimination if true otherwise UserError *)
   | Hnf
   | Simpl
-  | Cbv of Closure.flags
-  | Lazy of Closure.flags
+  | Cbv of Closure.RedFlags.reds
+  | Lazy of Closure.RedFlags.reds
   | Unfold of (int list * evaluable_global_reference) list
   | Fold of constr list
   | Pattern of (int list * constr * constr) list
 
 val reduction_of_redexp : red_expr ->  reduction_function
+
+(* Opaque and Transparent commands. *)
+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