|
(************************************************************************)
(* * The Rocq Prover / The Rocq Development Team *)
(* v * Copyright INRIA, CNRS and contributors *)
(* <O___,, * (see version control and CREDITS file for authors & dates) *)
(* \VV/ **************************************************************)
(* // * This file is distributed under the terms of the *)
(* * GNU Lesser General Public License Version 2.1 *)
(* * (see LICENSE file for the text of the license) *)
(************************************************************************)
(* Syntax for rewriting with strategies *)
{
open Names
open Locus
open Constrexpr
open Glob_term
open Genintern
open Geninterp
open Extraargs
open Rewrite
open ComRewrite
open Stdarg
open Tactypes
open Procq.Prim
open Procq.Constr
open Pvernac.Vernac_
open Pltac
open Vernacextend
}
DECLARE PLUGIN "rocq-runtime.plugins.ltac"
{
type constr_expr_with_bindings = constr_expr with_bindings
type glob_constr_with_bindings = glob_constr_and_expr with_bindings
type glob_constr_with_bindings_sign = interp_sign * glob_constr_and_expr with_bindings
let pr_glob_constr_with_bindings_sign env sigma _ _ _ (ge : glob_constr_with_bindings_sign) =
Printer.pr_glob_constr_env env sigma (fst (fst (snd ge)))
let pr_glob_constr_with_bindings env sigma _ _ _ (ge : glob_constr_with_bindings) =
Printer.pr_glob_constr_env env sigma (fst (fst ge))
let pr_constr_expr_with_bindings env sigma prc _ _ (ge : constr_expr_with_bindings) = prc env sigma (fst ge)
let interp_glob_constr_with_bindings ist _ _ c = (ist, c)
let glob_glob_constr_with_bindings ist l = Tacintern.intern_constr_with_bindings ist l
let subst_glob_constr_with_bindings s c =
Tacsubst.subst_glob_with_bindings s c
}
ARGUMENT EXTEND glob_constr_with_bindings
PRINTED BY { pr_glob_constr_with_bindings_sign env sigma }
INTERPRETED BY { interp_glob_constr_with_bindings }
GLOBALIZED BY { glob_glob_constr_with_bindings }
SUBSTITUTED BY { subst_glob_constr_with_bindings }
RAW_PRINTED BY { pr_constr_expr_with_bindings env sigma }
GLOB_PRINTED BY { pr_glob_constr_with_bindings env sigma }
| [ constr_with_bindings(bl) ] -> { bl }
END
{
let subst_strategy sub = map_strategy
(Tacsubst.subst_glob_constr_and_expr sub)
(Tacsubst.subst_glob_red_expr sub)
(fun x -> x)
let pr_strategy _ _ _ (s : strategy) = Pp.str "<strategy>"
let pr_raw_strategy env sigma prc prlc _ (s : Tacexpr.raw_strategy) =
let prr = Pptactic.pr_red_expr env sigma (prc, prlc, Pputils.pr_or_by_notation Libnames.pr_qualid, prc,Pputils.pr_or_var Pp.int) in
Rewrite.pr_strategy (prc env sigma) prr Pputils.pr_lident s
let pr_glob_strategy env sigma prc prlc _ (s : Tacexpr.glob_strategy) =
let prcst = Pputils.pr_or_var Pptactic.(pr_and_short_name (pr_evaluable_reference_env env)) in
let prr = Pptactic.pr_red_expr env sigma (prc, prlc, prcst, prc, Pputils.pr_or_var Pp.int) in
Rewrite.pr_strategy (prc env sigma) prr Id.print s
}
ARGUMENT EXTEND rewstrategy
PRINTED BY { pr_strategy }
INTERPRETED BY { Tacinterp.interp_strategy }
GLOBALIZED BY { Tacintern.intern_strategy }
SUBSTITUTED BY { subst_strategy }
RAW_PRINTED BY { pr_raw_strategy env sigma }
GLOB_PRINTED BY { pr_glob_strategy env sigma }
END
GRAMMAR EXTEND Gram
GLOBAL: rewstrategy;
rewstrategy:
[ NONA
[ IDENT "fix"; id = identref; ":="; s = rewstrategy1 -> { StratFix (id, s) }
| h = ne_rewstrategy1_list_sep_semicolon -> { h } ] ]
;
ne_rewstrategy1_list_sep_semicolon:
[ LEFTA
[ h = SELF; ";"; h' = rewstrategy1 -> { StratBinary (Compose, h, h') }
| h = rewstrategy1 -> { h } ] ]
;
rewstrategy1:
[ RIGHTA
[ "<-"; c = constr -> { StratConstr (c, false) }
| IDENT "subterms"; h = SELF -> { StratUnary (Subterms, h) }
| IDENT "subterm"; h = SELF -> { StratUnary (Subterm, h) }
| IDENT "innermost"; h = SELF -> { StratUnary(Innermost, h) }
| IDENT "outermost"; h = SELF -> { StratUnary(Outermost, h) }
| IDENT "bottomup"; h = SELF -> { StratUnary(Bottomup, h) }
| IDENT "topdown"; h = SELF -> { StratUnary(Topdown, h) }
| IDENT "progress"; h = SELF -> { StratUnary (Progress, h) }
| IDENT "try"; h = SELF -> { StratUnary (Try, h) }
| IDENT "any"; h = SELF -> { StratUnary (Any, h) }
| IDENT "repeat"; h = SELF -> { StratUnary (Repeat, h) }
| IDENT "choice"; h = LIST1 rewstrategy0 -> { StratNAry (Choice, h) }
| IDENT "old_hints"; h = preident -> { StratHints (true, h) }
| IDENT "hints"; h = preident -> { StratHints (false, h) }
| IDENT "terms"; h = LIST0 constr -> { StratTerms h }
| IDENT "eval"; r = red_expr -> { StratEval r }
| IDENT "fold"; c = constr -> { StratFold c }
| h = rewstrategy0 -> { h } ] ]
;
rewstrategy0:
[ NONA
[ c = constr -> { StratConstr (c, true) }
| IDENT "id" -> { StratId }
| IDENT "fail" -> { StratFail }
| IDENT "refl" -> { StratRefl }
| "("; h = rewstrategy; ")" -> { h } ] ]
;
END
(* By default the strategy for "rewrite_db" is top-down *)
{
let db_strat db = StratUnary (Topdown, StratHints (false, db))
let cl_rewrite_clause_db ist db = cl_rewrite_clause_strat (strategy_of_ast (db_strat db))
let cl_rewrite_clause (ist, c) b occ cl =
let c env sigma = Tacinterp.interp_open_constr_with_bindings ist env sigma c in
cl_rewrite_clause c b occ cl
}
TACTIC EXTEND rewrite_strat
| [ "rewrite_strat" rewstrategy(s) "in" hyp(id) ] -> { cl_rewrite_clause_strat s (Some id) }
| [ "rewrite_strat" rewstrategy(s) ] -> { cl_rewrite_clause_strat s None }
| [ "rewrite_db" preident(db) "in" hyp(id) ] -> { cl_rewrite_clause_db ist db (Some id) }
| [ "rewrite_db" preident(db) ] -> { cl_rewrite_clause_db ist db None }
END
{
let clsubstitute o c =
Proofview.Goal.enter begin fun gl ->
let is_tac id = match DAst.get (fst (fst (snd c))) with GVar id' when Id.equal id' id -> true | _ -> false in
let hyps = Tacmach.pf_ids_of_hyps gl in
Tacticals.tclMAP
(fun cl ->
match cl with
| Some id when is_tac id -> Tacticals.tclIDTAC
| _ -> cl_rewrite_clause c o AllOccurrences cl)
(None :: List.map (fun id -> Some id) hyps)
end
}
TACTIC EXTEND substitute
| [ "substitute" orient(o) glob_constr_with_bindings(c) ] -> { clsubstitute o c }
END
(* Compatibility with old Setoids *)
TACTIC EXTEND setoid_rewrite
| [ "setoid_rewrite" orient(o) glob_constr_with_bindings(c) ]
-> { cl_rewrite_clause c o AllOccurrences None }
| [ "setoid_rewrite" orient(o) glob_constr_with_bindings(c) "in" hyp(id) ] ->
{ cl_rewrite_clause c o AllOccurrences (Some id) }
| [ "setoid_rewrite" orient(o) glob_constr_with_bindings(c) "at" occurrences(occ) ] ->
{ cl_rewrite_clause c o (occurrences_of occ) None }
| [ "setoid_rewrite" orient(o) glob_constr_with_bindings(c) "at" occurrences(occ) "in" hyp(id)] ->
{ cl_rewrite_clause c o (occurrences_of occ) (Some id) }
| [ "setoid_rewrite" orient(o) glob_constr_with_bindings(c) "in" hyp(id) "at" occurrences(occ)] ->
{ cl_rewrite_clause c o (occurrences_of occ) (Some id) }
END
VERNAC COMMAND EXTEND AddRelation CLASSIFIED AS SIDEFF
| #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
"symmetry" "proved" "by" constr(lemma2) "as" identref(n) ] ->
{ declare_relation atts a aeq n (Some lemma1) (Some lemma2) None }
| #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
"as" identref(n) ] ->
{ declare_relation atts a aeq n (Some lemma1) None None }
| #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "as" identref(n) ] ->
{ declare_relation atts a aeq n None None None }
END
VERNAC COMMAND EXTEND AddRelation2 CLASSIFIED AS SIDEFF
| #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2)
"as" identref(n) ] ->
{ declare_relation atts a aeq n None (Some lemma2) None }
| #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3) "as" identref(n) ] ->
{ declare_relation atts a aeq n None (Some lemma2) (Some lemma3) }
END
VERNAC COMMAND EXTEND AddRelation3 CLASSIFIED AS SIDEFF
| #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
"transitivity" "proved" "by" constr(lemma3) "as" identref(n) ] ->
{ declare_relation atts a aeq n (Some lemma1) None (Some lemma3) }
| #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
"symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3)
"as" identref(n) ] ->
{ declare_relation atts a aeq n (Some lemma1) (Some lemma2) (Some lemma3) }
| #[ atts = rewrite_attributes; ] [ "Add" "Relation" constr(a) constr(aeq) "transitivity" "proved" "by" constr(lemma3)
"as" identref(n) ] ->
{ declare_relation atts a aeq n None None (Some lemma3) }
END
{
type binders_argtype = local_binder_expr list
let wit_binders =
(Genarg.create_arg "binders" : binders_argtype Genarg.vernac_genarg_type)
let binders = Procq.create_generic_entry2 "binders" (Genarg.rawwit wit_binders)
let () =
let raw_printer l = Genprint.PrinterBasic (fun env sigma -> Pp.pr_non_empty_arg (Ppconstr.pr_binders env sigma) l) in
Genprint.register_vernac_print0 wit_binders raw_printer
}
GRAMMAR EXTEND Gram
GLOBAL: binders;
binders:
[ [ b = Procq.Constr.binders -> { b } ] ];
END
VERNAC COMMAND EXTEND AddParametricRelation CLASSIFIED AS SIDEFF
| #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq)
"reflexivity" "proved" "by" constr(lemma1)
"symmetry" "proved" "by" constr(lemma2) "as" identref(n) ] ->
{ declare_relation atts ~binders:b a aeq n (Some lemma1) (Some lemma2) None }
| #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq)
"reflexivity" "proved" "by" constr(lemma1)
"as" identref(n) ] ->
{ declare_relation atts ~binders:b a aeq n (Some lemma1) None None }
| #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "as" identref(n) ] ->
{ declare_relation atts ~binders:b a aeq n None None None }
END
VERNAC COMMAND EXTEND AddParametricRelation2 CLASSIFIED AS SIDEFF
| #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2)
"as" identref(n) ] ->
{ declare_relation atts ~binders:b a aeq n None (Some lemma2) None }
| #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3) "as" identref(n) ] ->
{ declare_relation atts ~binders:b a aeq n None (Some lemma2) (Some lemma3) }
END
VERNAC COMMAND EXTEND AddParametricRelation3 CLASSIFIED AS SIDEFF
| #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
"transitivity" "proved" "by" constr(lemma3) "as" identref(n) ] ->
{ declare_relation atts ~binders:b a aeq n (Some lemma1) None (Some lemma3) }
| #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "reflexivity" "proved" "by" constr(lemma1)
"symmetry" "proved" "by" constr(lemma2) "transitivity" "proved" "by" constr(lemma3)
"as" identref(n) ] ->
{ declare_relation atts ~binders:b a aeq n (Some lemma1) (Some lemma2) (Some lemma3) }
| #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Relation" binders(b) ":" constr(a) constr(aeq) "transitivity" "proved" "by" constr(lemma3)
"as" identref(n) ] ->
{ declare_relation atts ~binders:b a aeq n None None (Some lemma3) }
END
{
let morphism_tactic =
let open Tacexpr in
let name = "Corelib.Classes.SetoidTactics.add_morphism_tactic" in
let tacqid = Libnames.qualid_of_string name in
let tac = CAst.make @@ TacArg (TacCall (CAst.make (tacqid, []))) in
Tacinterp.interp tac
}
VERNAC COMMAND EXTEND AddSetoid1 CLASSIFIED AS SIDEFF
| #[ atts = rewrite_attributes; ] [ "Add" "Setoid" constr(a) constr(aeq) constr(t) "as" identref(n) ] ->
{
add_setoid atts [] a aeq t n
}
| #[ atts = rewrite_attributes; ] [ "Add" "Parametric" "Setoid" binders(binders) ":" constr(a) constr(aeq) constr(t) "as" identref(n) ] ->
{
add_setoid atts binders a aeq t n
}
| #[ atts = rewrite_attributes; ] ![ open_proof ] [ "Add" "Morphism" constr(m) ":" identref(n) ]
=> { VtStartProof(GuaranteesOpacity, [n.CAst.v]) }
-> { if Lib.is_modtype () then
CErrors.user_err Pp.(str "Add Morphism cannot be used in a module type. Use Parameter Morphism instead.");
add_morphism_interactive atts ~tactic:morphism_tactic m n }
| #[ atts = rewrite_attributes; ] [ "Declare" "Morphism" constr(m) ":" identref(n) ]
=> { VtSideff([n.CAst.v], VtLater) }
-> { add_morphism_as_parameter atts m n }
| #[ atts = rewrite_attributes; ] ![ open_proof ] [ "Add" "Morphism" constr(m) "with" "signature" lconstr(s) "as" identref(n) ]
=> { VtStartProof(GuaranteesOpacity,[n.CAst.v]) }
-> { add_morphism atts ~tactic:morphism_tactic [] m s n }
| #[ atts = rewrite_attributes; ] ![ open_proof ] [ "Add" "Parametric" "Morphism" binders(binders) ":" constr(m)
"with" "signature" lconstr(s) "as" identref(n) ]
=> { VtStartProof(GuaranteesOpacity,[n.CAst.v]) }
-> { add_morphism atts ~tactic:morphism_tactic binders m s n }
END
TACTIC EXTEND setoid_symmetry
| [ "setoid_symmetry" ] -> { setoid_symmetry }
| [ "setoid_symmetry" "in" hyp(n) ] -> { setoid_symmetry_in n }
END
TACTIC EXTEND setoid_reflexivity
| [ "setoid_reflexivity" ] -> { setoid_reflexivity }
END
TACTIC EXTEND setoid_transitivity
| [ "setoid_transitivity" constr(t) ] -> { setoid_transitivity (Some t) }
| [ "setoid_etransitivity" ] -> { setoid_transitivity None }
END
VERNAC COMMAND EXTEND PrintRewriteHintDb CLASSIFIED AS QUERY
| [ "Print" "Rewrite" "HintDb" preident(s) ] ->
{ Feedback.msg_notice (Autorewrite.print_rewrite_hintdb s) }
END
[ Dauer der Verarbeitung: 0.22 Sekunden
(vorverarbeitet)
]
|
