diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/g_ltac2.ml4 | 37 | ||||
| -rw-r--r-- | src/tac2core.ml | 1 | ||||
| -rw-r--r-- | src/tac2entries.ml | 1 | ||||
| -rw-r--r-- | src/tac2entries.mli | 1 | ||||
| -rw-r--r-- | src/tac2qexpr.mli | 14 | ||||
| -rw-r--r-- | src/tac2quote.ml | 50 | ||||
| -rw-r--r-- | src/tac2quote.mli | 2 |
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 |