diff options
| -rw-r--r-- | dev/doc/changes.txt | 3 | ||||
| -rw-r--r-- | doc/refman/RefMan-tac.tex | 6 | ||||
| -rw-r--r-- | intf/genredexpr.mli | 8 | ||||
| -rw-r--r-- | parsing/g_tactic.ml4 | 17 | ||||
| -rw-r--r-- | plugins/funind/recdef.ml | 2 | ||||
| -rw-r--r-- | pretyping/redops.ml | 10 | ||||
| -rw-r--r-- | printing/pptactic.ml | 15 | ||||
| -rw-r--r-- | proofs/redexpr.ml | 7 | ||||
| -rw-r--r-- | tactics/tactics.ml | 2 |
9 files changed, 45 insertions, 25 deletions
diff --git a/dev/doc/changes.txt b/dev/doc/changes.txt index dd0a81603c..4ce1338443 100644 --- a/dev/doc/changes.txt +++ b/dev/doc/changes.txt @@ -48,6 +48,9 @@ Reductionops.whd_betadeltaiotaeta_stack Reductionops.whd_betadeltaiotaeta_state Reductionops.whd_betadeltaiotaeta +In intf/genredexpr.mli, fIota was replaced by FMatch, FFix and +FCofix. Similarly, rIota was replaced by rMatch, rFix and rCofix. + ** Notation_ops ** Use Glob_ops.glob_constr_eq instead of Notation_ops.eq_glob_constr. diff --git a/doc/refman/RefMan-tac.tex b/doc/refman/RefMan-tac.tex index 2d9cc12fd7..21b72b8eff 100644 --- a/doc/refman/RefMan-tac.tex +++ b/doc/refman/RefMan-tac.tex @@ -3033,8 +3033,10 @@ $\beta$ (reduction of functional application), $\delta$ (unfolding of transparent constants, see \ref{Transparent}), $\iota$ (reduction of pattern-matching over a constructed term, and unfolding of {\tt fix} and {\tt cofix} expressions) and $\zeta$ (contraction of local -definitions), the flag are either {\tt beta}, {\tt delta}, {\tt iota} -or {\tt zeta}. The {\tt delta} flag itself can be refined into {\tt +definitions), the flags are either {\tt beta}, {\tt delta}, +{\tt match}, {\tt fix}, {\tt cofix}, {\tt iota} or {\tt zeta}. +The {\tt iota} flag is a shorthand for {\tt match}, {\tt fix} and {\tt cofix}. +The {\tt delta} flag itself can be refined into {\tt delta [\qualid$_1$\ldots\qualid$_k$]} or {\tt delta -[\qualid$_1$\ldots\qualid$_k$]}, restricting in the first case the constants to unfold to the constants listed, and restricting in the diff --git a/intf/genredexpr.mli b/intf/genredexpr.mli index ff036a13f2..2df79673ad 100644 --- a/intf/genredexpr.mli +++ b/intf/genredexpr.mli @@ -12,7 +12,9 @@ type 'a red_atom = | FBeta - | FIota + | FMatch + | FFix + | FCofix | FZeta | FConst of 'a list | FDeltaBut of 'a list @@ -21,7 +23,9 @@ type 'a red_atom = type 'a glob_red_flag = { rBeta : bool; - rIota : bool; + rMatch : bool; + rFix : bool; + rCofix : bool; rZeta : bool; rDelta : bool; (** true = delta all but rConst; false = delta only on rConst*) rConst : 'a list diff --git a/parsing/g_tactic.ml4 b/parsing/g_tactic.ml4 index 8a83bc2d1d..33ca9158cd 100644 --- a/parsing/g_tactic.ml4 +++ b/parsing/g_tactic.ml4 @@ -22,7 +22,7 @@ open Decl_kinds open Pcoq -let all_with delta = Redops.make_red_flag [FBeta;FIota;FZeta;delta] +let all_with delta = Redops.make_red_flag [FBeta;FMatch;FFix;FCofix;FZeta;delta] let tactic_kw = [ "->"; "<-" ; "by" ] let _ = List.iter CLexer.add_keyword tactic_kw @@ -348,11 +348,14 @@ GEXTEND Gram with_bindings: [ [ "with"; bl = bindings -> bl | -> NoBindings ] ] ; - red_flag: - [ [ IDENT "beta" -> FBeta - | IDENT "iota" -> FIota - | IDENT "zeta" -> FZeta - | IDENT "delta"; d = delta_flag -> d + red_flags: + [ [ IDENT "beta" -> [FBeta] + | IDENT "iota" -> [FMatch;FFix;FCofix] + | IDENT "match" -> [FMatch] + | IDENT "fix" -> [FFix] + | IDENT "cofix" -> [FCofix] + | IDENT "zeta" -> [FZeta] + | IDENT "delta"; d = delta_flag -> [d] ] ] ; delta_flag: @@ -362,7 +365,7 @@ GEXTEND Gram ] ] ; strategy_flag: - [ [ s = LIST1 red_flag -> Redops.make_red_flag s + [ [ s = LIST1 red_flags -> Redops.make_red_flag (List.flatten s) | d = delta_flag -> all_with d ] ] ; diff --git a/plugins/funind/recdef.ml b/plugins/funind/recdef.ml index e742f7b80d..ceea4fa535 100644 --- a/plugins/funind/recdef.ml +++ b/plugins/funind/recdef.ml @@ -161,7 +161,7 @@ let rec n_x_id ids n = let simpl_iter clause = reduce (Lazy - {rBeta=true;rIota=true;rZeta= true; rDelta=false; + {rBeta=true;rMatch=true;rFix=true;rCofix=true;rZeta=true;rDelta=false; rConst = [ EvalConstRef (const_of_ref (delayed_force iter_ref))]}) clause diff --git a/pretyping/redops.ml b/pretyping/redops.ml index c188995a84..db5879174d 100644 --- a/pretyping/redops.ml +++ b/pretyping/redops.ml @@ -14,7 +14,9 @@ let make_red_flag l = let rec add_flag red = function | [] -> red | FBeta :: lf -> add_flag { red with rBeta = true } lf - | FIota :: lf -> add_flag { red with rIota = true } lf + | FMatch :: lf -> add_flag { red with rMatch = true } lf + | FFix :: lf -> add_flag { red with rFix = true } lf + | FCofix :: lf -> add_flag { red with rCofix = true } lf | FZeta :: lf -> add_flag { red with rZeta = true } lf | FConst l :: lf -> if red.rDelta then @@ -30,9 +32,11 @@ let make_red_flag l = lf in add_flag - {rBeta = false; rIota = false; rZeta = false; rDelta = false; rConst = []} + {rBeta = false; rMatch = false; rFix = false; rCofix = false; + rZeta = false; rDelta = false; rConst = []} l let all_flags = - {rBeta = true; rIota = true; rZeta = true; rDelta = true; rConst = []} + {rBeta = true; rMatch = true; rFix = true; rCofix = true; + rZeta = true; rDelta = true; rConst = []} diff --git a/printing/pptactic.ml b/printing/pptactic.ml index b6e4c8011c..0ab1349ecf 100644 --- a/printing/pptactic.ml +++ b/printing/pptactic.ml @@ -151,7 +151,8 @@ module Make exception ComplexRedFlag let pr_short_red_flag pr r = - if not r.rBeta || not r.rIota || not r.rZeta then raise ComplexRedFlag + if not r.rBeta || not r.rMatch || not r.rFix || not r.rCofix || 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 ()) ++ @@ -161,9 +162,12 @@ module Make 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.rMatch && r.rFix && r.rCofix then pr_arg str "iota" else + (if r.rMatch then pr_arg str "match" else mt ()) ++ + (if r.rFix then pr_arg str "fix" else mt ()) ++ + (if r.rCofix then pr_arg str "cofix" 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 @@ -180,7 +184,8 @@ module Make | 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 + if f.rBeta && f.rMatch && f.rFix && f.rCofix && + f.rZeta && f.rDelta && List.is_empty f.rConst then keyword "compute" else hov 1 (keyword "cbv" ++ pr_red_flag pr_ref f) diff --git a/proofs/redexpr.ml b/proofs/redexpr.ml index 55dfb88b46..d5e3f30af3 100644 --- a/proofs/redexpr.ml +++ b/proofs/redexpr.ml @@ -146,10 +146,9 @@ let make_flag_constant = function let make_flag env f = let red = no_red in let red = if f.rBeta then red_add red fBETA else red in - let red = - if f.rIota then (red_add (red_add (red_add red fMATCH) fFIX) fCOFIX) - else red - in + let red = if f.rMatch then red_add red fMATCH else red in + let red = if f.rFix then red_add red fFIX else red in + let red = if f.rCofix then red_add red fCOFIX else red in let red = if f.rZeta then red_add red fZETA else red in let red = if f.rDelta then (* All but rConst *) diff --git a/tactics/tactics.ml b/tactics/tactics.ml index 9a39773a84..61aaef871d 100644 --- a/tactics/tactics.ml +++ b/tactics/tactics.ml @@ -4944,7 +4944,7 @@ module New = struct let reduce_after_refine = reduce - (Lazy {rBeta=true;rIota=true;rZeta=false;rDelta=false;rConst=[]}) + (Lazy {rBeta=true;rMatch=true;rFix=true;rCofix=true;rZeta=false;rDelta=false;rConst=[]}) {onhyps=None; concl_occs=AllOccurrences } let refine ?unsafe c = |