Adding a scope for reduction flags.

7 files changed, 105 insertions, 1 deletions

diff --git a/src/g_ltac2.ml4 b/src/g_ltac2.ml4
index c70f1e882d..ef3615db89 100644
--- a/src/g_ltac2.ml4
+++ b/src/g_ltac2.ml4
@@ -317,7 +317,7 @@ let loc_of_ne_list l = Loc.merge_opt (fst (List.hd l)) (fst (List.last l))
 
 GEXTEND Gram
   GLOBAL: q_ident q_bindings q_intropattern q_intropatterns q_induction_clause
-          q_rewriting q_clause q_dispatch q_occurrences;
+          q_rewriting q_clause q_dispatch q_occurrences q_strategy_flag;
   anti:
     [ [ "$"; id = Prim.ident -> QAnti (Loc.tag ~loc:!@loc id) ] ]
   ;
@@ -568,6 +568,41 @@ GEXTEND Gram
   q_occurrences:
     [ [ occs = occs -> occs ] ]
   ;
+  red_flag:
+    [ [ IDENT "beta" -> Loc.tag ~loc:!@loc @@ QBeta
+      | IDENT "iota" -> Loc.tag ~loc:!@loc @@ QIota
+      | IDENT "match" -> Loc.tag ~loc:!@loc @@ QMatch
+      | IDENT "fix" -> Loc.tag ~loc:!@loc @@ QFix
+      | IDENT "cofix" -> Loc.tag ~loc:!@loc @@ QCofix
+      | IDENT "zeta" -> Loc.tag ~loc:!@loc @@ QZeta
+      | IDENT "delta"; d = delta_flag -> d
+    ] ]
+  ;
+  refglobal:
+    [ [ "&"; id = Prim.ident -> QExpr (Libnames.Ident (Loc.tag ~loc:!@loc id))
+      | qid = Prim.qualid -> QExpr (Libnames.Qualid qid)
+      | "$"; id = Prim.ident -> QAnti (Loc.tag ~loc:!@loc id)
+    ] ]
+  ;
+  refglobals:
+    [ [ gl = LIST1 refglobal -> Loc.tag ~loc:!@loc gl ] ]
+  ;
+  delta_flag:
+    [ [ "-"; "["; idl = refglobals; "]" -> Loc.tag ~loc:!@loc @@ QDeltaBut idl
+      | "["; idl = refglobals; "]" -> Loc.tag ~loc:!@loc @@ QConst idl
+      | -> Loc.tag ~loc:!@loc @@ QDeltaBut (Loc.tag ~loc:!@loc [])
+    ] ]
+  ;
+  strategy_flag:
+    [ [ s = LIST1 red_flag -> Loc.tag ~loc:!@loc s
+      | d = delta_flag ->
+        Loc.tag ~loc:!@loc
+          [Loc.tag ~loc:!@loc QBeta; Loc.tag ~loc:!@loc QIota; Loc.tag ~loc:!@loc QZeta; d]
+    ] ]
+  ;
+  q_strategy_flag:
+    [ [ flag = strategy_flag -> flag ] ]
+  ;
 END
 
 (** Extension of constr syntax *)
diff --git a/src/tac2core.ml b/src/tac2core.ml
index 303d62a30d..196755346d 100644
--- a/src/tac2core.ml
+++ b/src/tac2core.ml
@@ -930,6 +930,7 @@ let () = add_expr_scope "rewriting" q_rewriting Tac2quote.of_rewriting
 let () = add_expr_scope "clause" q_clause Tac2quote.of_clause
 let () = add_expr_scope "occurrences" q_occurrences Tac2quote.of_occurrences
 let () = add_expr_scope "dispatch" q_dispatch Tac2quote.of_dispatch
+let () = add_expr_scope "strategy" q_strategy_flag Tac2quote.of_strategy_flag
 
 let () = add_generic_scope "constr" Pcoq.Constr.constr Stdarg.wit_constr
 let () = add_generic_scope "open_constr" Pcoq.Constr.constr Stdarg.wit_open_constr
diff --git a/src/tac2entries.ml b/src/tac2entries.ml
index 2490f6534b..a6c0e21ac5 100644
--- a/src/tac2entries.ml
+++ b/src/tac2entries.ml
@@ -33,6 +33,7 @@ let q_rewriting = Pcoq.Gram.entry_create "tactic:q_rewriting"
 let q_clause = Pcoq.Gram.entry_create "tactic:q_clause"
 let q_dispatch = Pcoq.Gram.entry_create "tactic:q_dispatch"
 let q_occurrences = Pcoq.Gram.entry_create "tactic:q_occurrences"
+let q_strategy_flag = Pcoq.Gram.entry_create "tactic:q_strategy_flag"
 end
 
 (** Tactic definition *)
diff --git a/src/tac2entries.mli b/src/tac2entries.mli
index 667378030a..645d37a8c6 100644
--- a/src/tac2entries.mli
+++ b/src/tac2entries.mli
@@ -68,4 +68,5 @@ val q_rewriting : rewriting Pcoq.Gram.entry
 val q_clause : clause Pcoq.Gram.entry
 val q_dispatch : dispatch Pcoq.Gram.entry
 val q_occurrences : occurrences Pcoq.Gram.entry
+val q_strategy_flag : strategy_flag Pcoq.Gram.entry
 end
diff --git a/src/tac2qexpr.mli b/src/tac2qexpr.mli
index 2e7fc7b44a..7c774a5c80 100644
--- a/src/tac2qexpr.mli
+++ b/src/tac2qexpr.mli
@@ -101,3 +101,17 @@ type rewriting = rewriting_r located
 type dispatch_r = raw_tacexpr option list * (raw_tacexpr option * raw_tacexpr option list) option
 
 type dispatch = dispatch_r located
+
+type red_flag_r =
+| QBeta
+| QIota
+| QMatch
+| QFix
+| QCofix
+| QZeta
+| QConst of Libnames.reference or_anti list located
+| QDeltaBut of Libnames.reference or_anti list located
+
+type red_flag = red_flag_r located
+
+type strategy_flag = red_flag list located
diff --git a/src/tac2quote.ml b/src/tac2quote.ml
index 8adeb15d20..4fcbcb5424 100644
--- a/src/tac2quote.ml
+++ b/src/tac2quote.ml
@@ -236,3 +236,53 @@ let of_dispatch tacs =
   in
   let map e = of_pair default (fun l -> of_list ~loc default l) (Loc.tag ~loc e) in
   of_pair (fun l -> of_list ~loc default l) (fun r -> of_option ~loc map r) tacs
+
+let make_red_flag l =
+  let open Genredexpr in
+  let rec add_flag red = function
+  | [] -> red
+  | (_, flag) :: lf ->
+    let red = match flag with
+    | QBeta -> { red with rBeta = true }
+    | QMatch -> { red with rMatch = true }
+    | QFix -> { red with rFix = true }
+    | QCofix -> { red with rCofix = true }
+    | QZeta -> { red with rZeta = true }
+    | QConst (loc, l) ->
+        if red.rDelta then
+          CErrors.user_err ?loc Pp.(str
+            "Cannot set both constants to unfold and constants not to unfold");
+        { red with rConst = red.rConst @ l }
+    | QDeltaBut (loc, l) ->
+        if red.rConst <> [] && not red.rDelta then
+          CErrors.user_err ?loc Pp.(str
+            "Cannot set both constants to unfold and constants not to unfold");
+        { red with rConst = red.rConst @ l; rDelta = true }
+    | QIota ->
+      { red with rMatch = true; rFix = true; rCofix = true }
+    in
+    add_flag red lf
+  in
+  add_flag
+    {rBeta = false; rMatch = false; rFix = false; rCofix = false;
+     rZeta = false; rDelta = false; rConst = []}
+    l
+
+let of_strategy_flag (loc, flag) =
+  let open Genredexpr in
+  let loc = Option.default dummy_loc loc in
+  let flag = make_red_flag flag in
+  let of_reference ref =
+    let loc = Libnames.loc_of_reference ref in
+    inj_wit ?loc Tac2env.wit_reference ref
+  in
+  let of_ref r = of_anti of_reference r in
+  CTacRec (loc, [
+    std_proj "rBeta", of_bool ~loc flag.rBeta;
+    std_proj "rMatch", of_bool ~loc flag.rMatch;
+    std_proj "rFix", of_bool ~loc flag.rFix;
+    std_proj "rCofix", of_bool ~loc flag.rCofix;
+    std_proj "rZeta", of_bool ~loc flag.rZeta;
+    std_proj "rDelta", of_bool ~loc flag.rDelta;
+    std_proj "rConst", of_list ~loc of_ref flag.rConst;
+  ])
diff --git a/src/tac2quote.mli b/src/tac2quote.mli
index 456d1fa97d..730324d051 100644
--- a/src/tac2quote.mli
+++ b/src/tac2quote.mli
@@ -55,3 +55,5 @@ val of_exact_hyp : ?loc:Loc.t -> Id.t located -> raw_tacexpr
 (** id ↦ 'Control.refine (fun () => Control.hyp @id') *)
 
 val of_dispatch : dispatch -> raw_tacexpr
+
+val of_strategy_flag : strategy_flag -> raw_tacexpr