Add the ability to give a transparent_state for conversion, to

parameterize what should be unfolded or not, by default unfolding
everything.


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

3 files changed, 40 insertions, 151 deletions

diff --git a/kernel/closure.ml b/kernel/closure.ml
index 2ee2443ff..d29f8b08c 100644
--- a/kernel/closure.ml
+++ b/kernel/closure.ml
@@ -175,137 +175,6 @@ let unfold_red kn =
     | EvalConstRef kn -> fCONST kn in
   mkflags (flag::unfold_side_flags)
 
-(************************* Obsolète
-(* [r_const=(true,cl)] means all constants but those in [cl] *)
-(* [r_const=(false,cl)] means only those in [cl] *)
-type reds = {
-  r_beta : bool;
-  r_const : bool * constant_path list * identifier list;
-  r_zeta : bool;
-  r_evar : bool;
-  r_iota : bool }
-
-let betadeltaiota_red = {
-  r_beta = true;
-  r_const = true,[],[];
-  r_zeta = true;
-  r_evar = true;
-  r_iota = true } 
-
-let betaiota_red = {
-  r_beta = true;
-  r_const = false,[],[];
-  r_zeta = false;
-  r_evar = false;
-  r_iota = true }
-		     
-let beta_red = {
-  r_beta = true;
-  r_const = false,[],[];
-  r_zeta = false;
-  r_evar = false;
-  r_iota = false }
-
-let no_red = {
-  r_beta = false;
-  r_const = false,[],[];
-  r_zeta = false;
-  r_evar = false;
-  r_iota = false }
-
-let betaiotazeta_red = {
-  r_beta = true;
-  r_const = false,[],[];
-  r_zeta = true;
-  r_evar = false;
-  r_iota = true }
-
-let unfold_red kn =
-  let c = match kn with
-    | EvalVarRef id -> false,[],[id]
-    | EvalConstRef kn -> false,[kn],[]
-  in {
-  r_beta = true;
-  r_const = c;
-  r_zeta = true;   (* false for finer behaviour ? *)
-  r_evar = false;
-  r_iota = true }
-
-(* Sets of reduction kinds.
-   Main rule: delta implies all consts (both global (= by
-   kernel_name) and local (= by Rel or Var)), all evars, and zeta (= letin's).
-   Rem: reduction of a Rel/Var bound to a term is Delta, but reduction of 
-   a LetIn expression is Letin reduction *)
-
-type red_kind =
-    BETA | DELTA | ZETA | IOTA
-  | CONST of constant_path list | CONSTBUT of constant_path list
-  | VAR of identifier | VARBUT of identifier
-
-let rec red_add red = function
-  | BETA -> { red with r_beta = true }
-  | DELTA ->
-      (match red.r_const with
-	| _,_::_,[] | _,[],_::_ -> error "Conflict in the reduction flags"
-	| _ -> { red with r_const = true,[],[]; r_zeta = true; r_evar = true })
-  | CONST cl ->
-      (match red.r_const with
-	| true,_,_ -> error "Conflict in the reduction flags"
-	| _,l1,l2 -> { red with r_const = false, list_union cl l1, l2 })
-  | CONSTBUT cl ->
-      (match red.r_const with
-	| false,_::_,_ | false,_,_::_ ->
-			   error "Conflict in the reduction flags"
-	| _,l1,l2 ->
-	    { red with r_const = true, list_union cl l1, l2;
-		r_zeta = true; r_evar = true })
-  | IOTA -> { red with r_iota = true }
-  | ZETA -> { red with r_zeta = true }
-  | VAR id ->
-      (match red.r_const with
-	| true,_,_ -> error "Conflict in the reduction flags"
-	| _,l1,l2 -> { red with r_const = false, l1, list_union [id] l2 })
-  | VARBUT cl ->
-      (match red.r_const with
-	| false,_::_,_ | false,_,_::_ ->
-			   error "Conflict in the reduction flags"
-	| _,l1,l2 ->
-	    { red with r_const = true, l1, list_union [cl] l2;
-		r_zeta = true; r_evar = true })
-
-let red_delta_set red =
-  let b,_,_ = red.r_const in b
-
-let red_local_const = red_delta_set
-
-(* to know if a redex is allowed, only a subset of red_kind is used ... *)
-let red_set red = function
-  | BETA -> incr_cnt red.r_beta beta
-  | CONST [kn] -> 
-      let (b,l,_) = red.r_const in
-      let c = List.mem kn l in
-      incr_cnt ((b & not c) or (c & not b)) delta
-  | VAR id -> (* En attendant d'avoir des kn pour les Var *)
-     let (b,_,l) = red.r_const in
-      let c = List.mem id l in
-      incr_cnt ((b & not c) or (c & not b)) delta
-  | ZETA -> incr_cnt red.r_zeta zeta
-  | EVAR -> incr_cnt red.r_zeta evar
-  | IOTA -> incr_cnt red.r_iota iota
-  | DELTA -> red_delta_set red (*Used for Rel/Var defined in context*)
-  (* Not for internal use *)
-  | CONST _ | CONSTBUT _ | VAR _ | VARBUT _ -> failwith "not implemented"
-
-(* Gives the constant list *)
-let red_get_const red =
-  let b,l1,l2 = red.r_const in
-  let l1' = List.map (fun x -> EvalConstRef x) l1 in
-  let l2' = List.map (fun x -> EvalVarRef x) l2 in
-  b, l1' @ l2'
-fin obsolète **************)
-(* specification of the reduction function *)
-
-
 (* Flags of reduction and cache of constants: 'a is a type that may be
  * mapped to constr. 'a infos implements a cache for constants and
  * abstractions, storing a representation (of type 'a) of the body of
diff --git a/kernel/reduction.ml b/kernel/reduction.ml
index 28176ecc5..7a6c560f8 100644
--- a/kernel/reduction.ml
+++ b/kernel/reduction.ml
@@ -17,6 +17,12 @@ open Environ
 open Closure
 open Esubst
 
+let unfold_reference ((ids, csts), infos) k =
+  match k with
+    | VarKey id when not (Idpred.mem id ids) -> None
+    | ConstKey cst when not (Cpred.mem cst csts) -> None
+    | _ -> unfold_reference infos k
+	  
 let rec is_empty_stack = function
     [] -> true
   | Zupdate _::s -> is_empty_stack s
@@ -117,6 +123,7 @@ let beta_appvect c v =
 
 (* Conversion utility functions *)
 type 'a conversion_function = env -> 'a -> 'a -> Univ.constraints
+type 'a trans_conversion_function = transparent_state -> env -> 'a -> 'a -> Univ.constraints
 
 exception NotConvertible
 exception NotConvertibleVect of int
@@ -171,8 +178,8 @@ let conv_sort_leq env s0 s1 = sort_cmp CUMUL s0 s1 Constraint.empty
 let rec ccnv cv_pb infos lft1 lft2 term1 term2 cuniv = 
   Util.check_for_interrupt ();
   eqappr cv_pb infos
-    (lft1, whd_stack infos term1 [])
-    (lft2, whd_stack infos term2 [])
+    (lft1, whd_stack (snd infos) term1 [])
+    (lft2, whd_stack (snd infos) term2 [])
     cuniv
 
 (* Conversion between [lft1](hd1 v1) and [lft2](hd2 v2) *)
@@ -216,17 +223,17 @@ and eqappr cv_pb infos appr1 appr2 cuniv =
           let (app1,app2) =
             if Conv_oracle.oracle_order fl1 fl2 then
               match unfold_reference infos fl1 with
-                | Some def1 -> ((lft1, whd_stack infos def1 v1), appr2)
+                | Some def1 -> ((lft1, whd_stack (snd infos) def1 v1), appr2)
                 | None ->
                     (match unfold_reference infos fl2 with
-                      | Some def2 -> (appr1, (lft2, whd_stack infos def2 v2))
+                      | Some def2 -> (appr1, (lft2, whd_stack (snd infos) def2 v2))
 		      | None -> raise NotConvertible)
             else
 	      match unfold_reference infos fl2 with
-                | Some def2 -> (appr1, (lft2, whd_stack infos def2 v2))
+                | Some def2 -> (appr1, (lft2, whd_stack (snd infos) def2 v2))
                 | None ->
                     (match unfold_reference infos fl1 with
-                    | Some def1 -> ((lft1, whd_stack infos def1 v1), appr2)
+                    | Some def1 -> ((lft1, whd_stack (snd infos) def1 v1), appr2)
 		    | None -> raise NotConvertible) in
           eqappr cv_pb infos app1 app2 cuniv)
 
@@ -234,12 +241,12 @@ and eqappr cv_pb infos appr1 appr2 cuniv =
     | (FFlex fl1, _)      ->
         (match unfold_reference infos fl1 with
            | Some def1 -> 
-	       eqappr cv_pb infos (lft1, whd_stack infos def1 v1) appr2 cuniv
+	       eqappr cv_pb infos (lft1, whd_stack (snd infos) def1 v1) appr2 cuniv
            | None -> raise NotConvertible)
     | (_, FFlex fl2)      ->
         (match unfold_reference infos fl2 with
-           | Some def2 -> 
-	       eqappr cv_pb infos appr1 (lft2, whd_stack infos def2 v2) cuniv
+           | Some def2 ->
+	       eqappr cv_pb infos appr1 (lft2, whd_stack (snd infos) def2 v2) cuniv
            | None -> raise NotConvertible)
 	
     (* other constructors *)
@@ -258,13 +265,13 @@ and eqappr cv_pb infos appr1 appr2 cuniv =
     (* Inductive types:  MutInd MutConstruct Fix Cofix *)
 
      | (FInd ind1, FInd ind2) ->
-         if mind_equiv_infos infos ind1 ind2
+         if mind_equiv_infos (snd infos) ind1 ind2
 	 then
            convert_stacks infos lft1 lft2 v1 v2 cuniv
          else raise NotConvertible
 
      | (FConstruct (ind1,j1), FConstruct (ind2,j2)) ->
-	 if j1 = j2 && mind_equiv_infos infos ind1 ind2
+	 if j1 = j2 && mind_equiv_infos (snd infos) ind1 ind2
 	 then
            convert_stacks infos lft1 lft2 v1 v2 cuniv
          else raise NotConvertible
@@ -303,11 +310,11 @@ and eqappr cv_pb infos appr1 appr2 cuniv =
        on the other arg and coulb be no more in hnf... *)
     | ( (FLetIn _, _) | (FCases _,_) | (FApp _,_)
       | (FCLOS _, _) | (FLIFT _, _)) ->
-        eqappr cv_pb infos (lft1, whd_stack infos hd1 v1) appr2 cuniv
+        eqappr cv_pb infos (lft1, whd_stack (snd infos) hd1 v1) appr2 cuniv
 
     | ( (_, FLetIn _) | (_,FCases _) | (_,FApp _)
       | (_,FCLOS _) | (_,FLIFT _)) ->
-        eqappr cv_pb infos (lft1, whd_stack infos hd1 v1) appr2 cuniv
+        eqappr cv_pb infos (lft1, whd_stack (snd infos) hd1 v1) appr2 cuniv
 
     (* Should not happen because whd_stack unlocks references *)
     | ((FLOCKED,_) | (_,FLOCKED)) -> assert false
@@ -317,7 +324,7 @@ and eqappr cv_pb infos appr1 appr2 cuniv =
 and convert_stacks infos lft1 lft2 stk1 stk2 cuniv =
   compare_stacks
     (fun (l1,t1) (l2,t2) c -> ccnv CONV infos l1 l2 t1 t2 c)
-    (mind_equiv_infos infos)
+    (mind_equiv_infos (snd infos))
     lft1 stk1 lft2 stk2 cuniv
 
 and convert_vect infos lft1 lft2 v1 v2 cuniv =
@@ -333,13 +340,19 @@ and convert_vect infos lft1 lft2 v1 v2 cuniv =
     fold 0 cuniv
   else raise NotConvertible
 
-let clos_fconv cv_pb env t1 t2 =
-  let infos = create_clos_infos betaiotazeta env in
+let clos_fconv trans cv_pb env t1 t2 =
+  let infos = trans, create_clos_infos betaiotazeta env in
   ccnv cv_pb infos ELID ELID (inject t1) (inject t2) Constraint.empty
 
-let fconv cv_pb env t1 t2 =
+let trans_fconv reds cv_pb env t1 t2 =
   if eq_constr t1 t2 then Constraint.empty
-  else clos_fconv cv_pb env t1 t2
+  else clos_fconv reds cv_pb env t1 t2
+
+let trans_conv_cmp conv reds = trans_fconv reds conv
+let trans_conv reds = trans_fconv reds CONV
+let trans_conv_leq reds = trans_fconv reds CUMUL
+
+let fconv = trans_fconv (Idpred.full, Cpred.full)
 
 let conv_cmp = fconv
 let conv = fconv CONV
@@ -365,7 +378,7 @@ let vm_conv cv_pb env t1 t2 =
     !vm_conv cv_pb env t1 t2
   with Not_found | Invalid_argument _ ->
       (* If compilation fails, fall-back to closure conversion *)
-      clos_fconv cv_pb env t1 t2
+      fconv cv_pb env t1 t2
   
 
 let default_conv = ref fconv 
@@ -377,7 +390,7 @@ let default_conv cv_pb env t1 t2 =
     !default_conv cv_pb env t1 t2
   with Not_found | Invalid_argument _ ->
       (* If compilation fails, fall-back to closure conversion *)
-      clos_fconv cv_pb env t1 t2
+      fconv cv_pb env t1 t2
   
 let default_conv_leq = default_conv CUMUL
 (*
diff --git a/kernel/reduction.mli b/kernel/reduction.mli
index 60cd999d8..663c18e2c 100644
--- a/kernel/reduction.mli
+++ b/kernel/reduction.mli
@@ -11,6 +11,7 @@
 (*i*)
 open Term
 open Environ
+open Closure
 (*i*)
 
 (************************************************************************)
@@ -28,6 +29,7 @@ val nf_betaiota      : constr -> constr
 exception NotConvertible
 exception NotConvertibleVect of int
 type 'a conversion_function = env -> 'a -> 'a -> Univ.constraints
+type 'a trans_conversion_function = Names.transparent_state -> env -> 'a -> 'a -> Univ.constraints
 
 type conv_pb = CONV | CUMUL
 
@@ -37,6 +39,11 @@ val sort_cmp :
 val conv_sort      : sorts conversion_function
 val conv_sort_leq  : sorts conversion_function
 
+val trans_conv_cmp       : conv_pb -> constr trans_conversion_function
+
+val trans_conv           : constr trans_conversion_function
+val trans_conv_leq       : types trans_conversion_function
+
 val conv_cmp       : conv_pb -> constr conversion_function
 
 val conv           : constr conversion_function