aboutsummaryrefslogtreecommitdiffhomepage
diff options
context:
space:
mode:
Diffstat
-rw-r--r--grammar/q_coqast.ml43
-rw-r--r--intf/genredexpr.mli2
-rw-r--r--parsing/g_tactic.ml44
-rw-r--r--pretyping/miscops.ml3
-rw-r--r--printing/pptactic.ml32
-rw-r--r--proofs/redexpr.ml3
-rw-r--r--tactics/coretactics.ml42
-rw-r--r--tactics/tacintern.ml4
-rw-r--r--tactics/tacinterp.ml5
-rw-r--r--tactics/tactics.ml8
10 files changed, 42 insertions, 24 deletions
diff --git a/grammar/q_coqast.ml4 b/grammar/q_coqast.ml4
index d6d13375e..1a11b0028 100644
--- a/grammar/q_coqast.ml4
+++ b/grammar/q_coqast.ml4
@@ -196,7 +196,8 @@ let mlexpr_of_occ_ref_or_constr =
let mlexpr_of_red_expr = function
| Genredexpr.Red b -> <:expr< Genredexpr.Red $mlexpr_of_bool b$ >>
| Genredexpr.Hnf -> <:expr< Genredexpr.Hnf >>
- | Genredexpr.Simpl o -> <:expr< Genredexpr.Simpl $mlexpr_of_option mlexpr_of_occ_ref_or_constr o$ >>
+ | Genredexpr.Simpl (f,o) ->
+ <:expr< Genredexpr.Simpl $mlexpr_of_red_flags f$ $mlexpr_of_option mlexpr_of_occ_ref_or_constr o$ >>
| Genredexpr.Cbv f ->
<:expr< Genredexpr.Cbv $mlexpr_of_red_flags f$ >>
| Genredexpr.Cbn f ->
diff --git a/intf/genredexpr.mli b/intf/genredexpr.mli
index a59278bb0..a9fc47348 100644
--- a/intf/genredexpr.mli
+++ b/intf/genredexpr.mli
@@ -32,7 +32,7 @@ type 'a glob_red_flag = {
type ('a,'b,'c) red_expr_gen =
| Red of bool
| Hnf
- | Simpl of ('b,'c) Util.union Locus.with_occurrences option
+ | Simpl of 'b glob_red_flag*('b,'c) Util.union Locus.with_occurrences option
| Cbv of 'b glob_red_flag
| Cbn of 'b glob_red_flag
| Lazy of 'b glob_red_flag
diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4
index 324efe53e..43d787ba5 100644
--- a/parsing/g_tactic.ml4
+++ b/parsing/g_tactic.ml4
@@ -342,7 +342,7 @@ GEXTEND Gram
red_tactic:
[ [ IDENT "red" -> Red false
| IDENT "hnf" -> Hnf
- | IDENT "simpl"; po = OPT ref_or_pattern_occ -> Simpl po
+ | IDENT "simpl"; d = delta_flag; po = OPT ref_or_pattern_occ -> Simpl (all_with d,po)
| IDENT "cbv"; s = strategy_flag -> Cbv s
| IDENT "cbn"; s = strategy_flag -> Cbn s
| IDENT "lazy"; s = strategy_flag -> Lazy s
@@ -357,7 +357,7 @@ GEXTEND Gram
red_expr:
[ [ IDENT "red" -> Red false
| IDENT "hnf" -> Hnf
- | IDENT "simpl"; po = OPT ref_or_pattern_occ -> Simpl po
+ | IDENT "simpl"; d = delta_flag; po = OPT ref_or_pattern_occ -> Simpl (all_with d,po)
| IDENT "cbv"; s = strategy_flag -> Cbv s
| IDENT "cbn"; s = strategy_flag -> Cbn s
| IDENT "lazy"; s = strategy_flag -> Lazy s
diff --git a/pretyping/miscops.ml b/pretyping/miscops.ml
index 10129306d..9ec031fbb 100644
--- a/pretyping/miscops.ml
+++ b/pretyping/miscops.ml
@@ -49,7 +49,8 @@ let map_occs f (occ,e) = (occ,f e)
let map_red_expr_gen f g h = function
| Fold l -> Fold (List.map f l)
| Pattern occs_l -> Pattern (List.map (map_occs f) occs_l)
- | Simpl occs_o -> Simpl (Option.map (map_occs (map_union g h)) occs_o)
+ | Simpl (flags,occs_o) ->
+ Simpl (map_flags g flags, Option.map (map_occs (map_union g h)) occs_o)
| Unfold occs_l -> Unfold (List.map (map_occs g) occs_l)
| Cbv flags -> Cbv (map_flags g flags)
| Lazy flags -> Lazy (map_flags g flags)
diff --git a/printing/pptactic.ml b/printing/pptactic.ml
index caba9609b..412c1050b 100644
--- a/printing/pptactic.ml
+++ b/printing/pptactic.ml
@@ -118,16 +118,27 @@ module Make
hov 1 (pr c ++ spc () ++ keyword "at" ++ str" - " ++
hov 0 (prlist_with_sep spc (pr_or_var int) nl))
+ exception ComplexRedFlag
+
+ let pr_short_red_flag pr r =
+ if not r.rBeta || not r.rIota || not r.rZeta then raise ComplexRedFlag
+ else if List.is_empty r.rConst then
+ if r.rDelta then mt () else raise ComplexRedFlag
+ else (if r.rDelta then str "-" else mt ()) ++
+ hov 0 (str "[" ++ prlist_with_sep spc pr r.rConst ++ str "]")
+
let pr_red_flag pr r =
- (if r.rBeta then pr_arg str "beta" else mt ()) ++
- (if r.rIota then pr_arg str "iota" else mt ()) ++
- (if r.rZeta then pr_arg str "zeta" else mt ()) ++
- (if List.is_empty r.rConst then
- if r.rDelta then pr_arg str "delta"
- else mt ()
- else
- pr_arg str "delta " ++ (if r.rDelta then str "-" else mt ()) ++
- hov 0 (str "[" ++ prlist_with_sep spc pr r.rConst ++ str "]"))
+ try pr_short_red_flag pr r
+ with complexRedFlags ->
+ (if r.rBeta then pr_arg str "beta" else mt ()) ++
+ (if r.rIota then pr_arg str "iota" else mt ()) ++
+ (if r.rZeta then pr_arg str "zeta" else mt ()) ++
+ (if List.is_empty r.rConst then
+ if r.rDelta then pr_arg str "delta"
+ else mt ()
+ else
+ pr_arg str "delta " ++ (if r.rDelta then str "-" else mt ()) ++
+ hov 0 (str "[" ++ prlist_with_sep spc pr r.rConst ++ str "]"))
let pr_union pr1 pr2 = function
| Inl a -> pr1 a
@@ -136,7 +147,8 @@ module Make
let pr_red_expr (pr_constr,pr_lconstr,pr_ref,pr_pattern) = function
| Red false -> keyword "red"
| Hnf -> keyword "hnf"
- | Simpl o -> keyword "simpl" ++ pr_opt (pr_with_occurrences (pr_union pr_ref pr_pattern)) o
+ | Simpl (f,o) -> keyword "simpl" ++ (pr_short_red_flag pr_ref f)
+ ++ pr_opt (pr_with_occurrences (pr_union pr_ref pr_pattern)) o
| Cbv f ->
if f.rBeta && f.rIota && f.rZeta && f.rDelta && List.is_empty f.rConst then
keyword "compute"
diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml
index 386ad70ec..c07541335 100644
--- a/proofs/redexpr.ml
+++ b/proofs/redexpr.ml
@@ -195,7 +195,8 @@ let reduction_of_red_expr env =
if internal then (e_red try_red_product,DEFAULTcast)
else (e_red red_product,DEFAULTcast)
| Hnf -> (e_red hnf_constr,DEFAULTcast)
- | Simpl o -> (contextualize (if head_style then whd_simpl else simpl) simpl o,DEFAULTcast)
+ | Simpl (_f,o) ->
+ (contextualize (if head_style then whd_simpl else simpl) simpl o,DEFAULTcast)
| Cbv f -> (e_red (cbv_norm_flags (make_flag f)),DEFAULTcast)
| Cbn f ->
let f = strong (fun env evd x -> Stack.zip ~refold:true
diff --git a/tactics/coretactics.ml4 b/tactics/coretactics.ml4
index 93768c10a..4f23e3520 100644
--- a/tactics/coretactics.ml4
+++ b/tactics/coretactics.ml4
@@ -210,7 +210,7 @@ let initial_atomic () =
let () = List.iter iter
[ "red", TacReduce(Red false,nocl);
"hnf", TacReduce(Hnf,nocl);
- "simpl", TacReduce(Simpl None,nocl);
+ "simpl", TacReduce(Simpl (Redops.all_flags,None),nocl);
"compute", TacReduce(Cbv Redops.all_flags,nocl);
"intro", TacIntroMove(None,MoveLast);
"intros", TacIntroPattern [];
diff --git a/tactics/tacintern.ml b/tactics/tacintern.ml
index 48f5c65ff..7d609e1a5 100644
--- a/tactics/tacintern.ml
+++ b/tactics/tacintern.ml
@@ -399,7 +399,9 @@ let intern_red_expr ist = function
| 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_or_ref_with_occurrences ist) o)
+ | Simpl (f,o) ->
+ Simpl (intern_flag ist f,
+ Option.map (intern_typed_pattern_or_ref_with_occurrences ist) o)
| CbvVm o -> CbvVm (Option.map (intern_typed_pattern_or_ref_with_occurrences ist) o)
| CbvNative o -> CbvNative (Option.map (intern_typed_pattern_or_ref_with_occurrences ist) o)
| (Red _ | Hnf | ExtraRedExpr _ as r ) -> r
diff --git a/tactics/tacinterp.ml b/tactics/tacinterp.ml
index c76c28dbf..e774316a6 100644
--- a/tactics/tacinterp.ml
+++ b/tactics/tacinterp.ml
@@ -710,8 +710,9 @@ let interp_red_expr ist env sigma = function
(fun c sigma -> interp_constr_with_occurrences ist env sigma c) l sigma
in
sigma , Pattern l_interp
- | Simpl o ->
- sigma , Simpl (Option.map (interp_closed_typed_pattern_with_occurrences ist env sigma) o)
+ | Simpl (f,o) ->
+ sigma , Simpl (interp_flag ist env sigma f,
+ Option.map (interp_closed_typed_pattern_with_occurrences ist env sigma) o)
| CbvVm o ->
sigma , CbvVm (Option.map (interp_closed_typed_pattern_with_occurrences ist env sigma) o)
| CbvNative o ->
diff --git a/tactics/tactics.ml b/tactics/tactics.ml
index 3a0baf294..40228c4df 100644
--- a/tactics/tactics.ml
+++ b/tactics/tactics.ml
@@ -467,7 +467,7 @@ let bind_red_expr_occurrences occs nbcl redexp =
let has_at_clause = function
| Unfold l -> List.exists (fun (occl,_) -> occl != AllOccurrences) l
| Pattern l -> List.exists (fun (occl,_) -> occl != AllOccurrences) l
- | Simpl (Some (occl,_)) -> occl != AllOccurrences
+ | Simpl (_,Some (occl,_)) -> occl != AllOccurrences
| _ -> false in
if occs == AllOccurrences then
if nbcl > 1 && has_at_clause redexp then
@@ -490,11 +490,11 @@ let bind_red_expr_occurrences occs nbcl redexp =
error_illegal_clause ()
else
Pattern [(occs,c)]
- | Simpl (Some (occl,c)) ->
+ | Simpl (f,Some (occl,c)) ->
if occl != AllOccurrences then
error_illegal_clause ()
else
- Simpl (Some (occs,c))
+ Simpl (f,Some (occs,c))
| CbvVm (Some (occl,c)) ->
if occl != AllOccurrences then
error_illegal_clause ()
@@ -506,7 +506,7 @@ let bind_red_expr_occurrences occs nbcl redexp =
else
CbvNative (Some (occs,c))
| Red _ | Hnf | Cbv _ | Lazy _ | Cbn _
- | ExtraRedExpr _ | Fold _ | Simpl None | CbvVm None | CbvNative None ->
+ | ExtraRedExpr _ | Fold _ | Simpl (_,None) | CbvVm None | CbvNative None ->
error_occurrences_not_unsupported ()
| Unfold [] | Pattern [] ->
assert false
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-11 05:56:20 +0000