Yet a new reduction tactic in Coq : cbn

It is supposed to become the next generation of the simpl tactics (it "refolds" constant)
but
1/it is a bit more aggresive than the old simpl
2/it cannot be customized as simpl start to be
3/(for now)it does not refold in reccursive calls constant such as
compare x y := compare_cont x y Eq := (fix compare_cont x y s := ...) x y Eq

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

9 files changed, 13 insertions, 1 deletions

diff --git a/grammar/q_coqast.ml4 b/grammar/q_coqast.ml4
index 738c3e1f18..ec14717305 100644
--- a/grammar/q_coqast.ml4
+++ b/grammar/q_coqast.ml4
@@ -182,6 +182,8 @@ let mlexpr_of_red_expr = function
   | Genredexpr.Simpl o -> <:expr< Genredexpr.Simpl $mlexpr_of_option mlexpr_of_occ_constr o$ >>
   | Genredexpr.Cbv f ->
       <:expr< Genredexpr.Cbv $mlexpr_of_red_flags f$ >>
+  | Genredexpr.Cbn f ->
+      <:expr< Genredexpr.Cbn $mlexpr_of_red_flags f$ >>
   | Genredexpr.Lazy f ->
       <:expr< Genredexpr.Lazy $mlexpr_of_red_flags f$ >>
   | Genredexpr.Unfold l ->
diff --git a/intf/genredexpr.mli b/intf/genredexpr.mli
index 833d32545d..97f9b04848 100644
--- a/intf/genredexpr.mli
+++ b/intf/genredexpr.mli
@@ -34,6 +34,7 @@ type ('a,'b,'c) red_expr_gen =
   | Hnf
   | Simpl of 'c Locus.with_occurrences option
   | Cbv of 'b glob_red_flag
+  | Cbn of 'b glob_red_flag
   | Lazy of 'b glob_red_flag
   | Unfold of 'b Locus.with_occurrences list
   | Fold of 'a list
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index b77c85bf77..0f256749c6 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -342,6 +342,7 @@ GEXTEND Gram
       | IDENT "hnf" -> Hnf
       | IDENT "simpl"; po = OPT pattern_occ -> Simpl po
       | IDENT "cbv"; s = strategy_flag -> Cbv s
+      | IDENT "cbn"; s = strategy_flag -> Cbn s
       | IDENT "lazy"; s = strategy_flag -> Lazy s
       | IDENT "compute"; delta = delta_flag -> Cbv (all_with delta)
       | IDENT "vm_compute"; po = OPT pattern_occ -> CbvVm po
diff --git a/printing/ppconstr.ml b/printing/ppconstr.ml
index 6d34b10bc9..e7f4a0b245 100644
--- a/printing/ppconstr.ml
+++ b/printing/ppconstr.ml
@@ -624,6 +624,8 @@ let pr_red_expr (pr_constr,pr_lconstr,pr_ref,pr_pattern) = function
 	hov 1 (str "cbv" ++ pr_red_flag pr_ref f)
   | Lazy f ->
       hov 1 (str "lazy" ++ pr_red_flag pr_ref f)
+  | Cbn f ->
+      hov 1 (str "cbn" ++ pr_red_flag pr_ref f)
   | Unfold l ->
       hov 1 (str "unfold" ++ spc() ++
              prlist_with_sep pr_comma (pr_with_occurrences pr_ref) l)
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index be0cba3a12..c4c821a9e5 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -183,6 +183,9 @@ let rec reduction_of_red_expr = function
       (fun _ -> simpl),DEFAULTcast)
   | Simpl None -> (simpl,DEFAULTcast)
   | Cbv f -> (cbv_norm_flags (make_flag f),DEFAULTcast)
+  | Cbn f ->
+    (strong (fun env evd x -> zip ~refold:true
+      (whd_state_gen ~refold:true (make_flag f) env evd (x, []))),DEFAULTcast)
   | Lazy f -> (clos_norm_flags (make_flag f),DEFAULTcast)
   | Unfold ubinds -> (unfoldn (List.map out_with_occurrences ubinds),DEFAULTcast)
   | Fold cl -> (fold_commands cl,DEFAULTcast)
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index 93b39583be..89cca15c8a 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -455,6 +455,7 @@ let intern_red_expr ist = function
   | Unfold l -> Unfold (List.map (intern_unfold ist) l)
   | Fold l -> Fold (List.map (intern_constr ist) l)
   | Cbv f -> Cbv (intern_flag ist f)
+  | Cbn f -> Cbn (intern_flag ist f)
   | Lazy f -> Lazy (intern_flag ist f)
   | Pattern l -> Pattern (List.map (intern_constr_with_occurrences ist) l)
   | Simpl o -> Simpl (Option.map (intern_typed_pattern_with_occurrences ist) o)
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index 3db2328e2c..96634f963e 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -577,6 +577,7 @@ let interp_red_expr ist sigma env = function
     let (sigma,l_interp) = interp_constr_list ist env sigma l in
     sigma , Fold l_interp
   | Cbv f -> sigma , Cbv (interp_flag ist env f)
+  | Cbn f -> sigma , Cbn (interp_flag ist env f)
   | Lazy f -> sigma , Lazy (interp_flag ist env f)
   | Pattern l ->
     let (sigma,l_interp) =
diff --git a/tactics/tacsubst.ml b/tactics/tacsubst.ml
index bbf4089eda..007ec9c6fa 100644
--- a/tactics/tacsubst.ml
+++ b/tactics/tacsubst.ml
@@ -117,6 +117,7 @@ let subst_redexp subst = function
   | Unfold l -> Unfold (List.map (subst_unfold subst) l)
   | Fold l -> Fold (List.map (subst_glob_constr subst) l)
   | Cbv f -> Cbv (subst_flag subst f)
+  | Cbn f -> Cbn (subst_flag subst f)
   | Lazy f -> Lazy (subst_flag subst f)
   | Pattern l -> Pattern (List.map (subst_constr_with_occurrences subst) l)
   | Simpl o -> Simpl (Option.map (subst_pattern_with_occurrences subst) o)
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index abafaa0597..0f0e43021d 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -262,7 +262,7 @@ let bind_red_expr_occurrences occs nbcl redexp =
           error_illegal_clause ()
         else
           CbvVm (Some (occs,c))
-    | Red _ | Hnf | Cbv _ | Lazy _
+    | Red _ | Hnf | Cbv _ | Lazy _ | Cbn _
     | ExtraRedExpr _ | Fold _ | Simpl None | CbvVm None ->
 	error_occurrences_not_unsupported ()
     | Unfold [] | Pattern [] ->