# HG changeset patch # User wenzelm # Date 1697915942 -7200 # Node ID d769a183d51dec02ff1d06b7f0d322ba04d6dccd # Parent d3328c562307f6ced82cd26704756645664bebf1 simprocs may be distinguished via 'identifier': only works for ML antiquotation (see also 13252110a6fe); diff -r d3328c562307 -r d769a183d51d NEWS --- a/NEWS Sat Oct 21 14:36:47 2023 +0200 +++ b/NEWS Sat Oct 21 21:19:02 2023 +0200 @@ -40,6 +40,22 @@ val eq_simproc = \<^simproc_setup>\eq ("r = s") = \K eq_proc\\; +* Simplification procedures may be distinguished via characteristic +theorems that are specified as 'identifier' in ML antiquotation +"simproc_setup" (but not in the corresponding Isar command). This allows +to work with several versions of the simproc, e.g. due to locale +interpretations. For example: + + locale test = fixes x y :: 'a assumes eq: "x = y" + begin + + ML \ + \<^simproc_setup>\foo (x) = \fn _ => fn _ => fn _ => SOME @{thm eq}\ + identifier test_axioms\ + \ + + end + * Isabelle/ML explicitly rejects 'handle' with catch-all patterns. INCOMPATIBILITY, better use \<^try>\...\ with 'catch' or 'finally', or as last resort declare [[ML_catch_all]] within the theory context. diff -r d3328c562307 -r d769a183d51d src/HOL/Nominal/nominal_inductive.ML --- a/src/HOL/Nominal/nominal_inductive.ML Sat Oct 21 14:36:47 2023 +0200 +++ b/src/HOL/Nominal/nominal_inductive.ML Sat Oct 21 21:19:02 2023 +0200 @@ -40,14 +40,16 @@ th RS infer_instantiate ctxt [(#1 (dest_Var (Thm.term_of perm_boolI_pi)), pi)] perm_boolI; fun mk_perm_bool_simproc names = - Simplifier.make_simproc \<^context> "perm_bool" - {lhss = [\<^term>\perm pi x\], + Simplifier.make_simproc \<^context> + {name = "perm_bool", + lhss = [\<^term>\perm pi x\], proc = fn _ => fn _ => fn ct => (case Thm.term_of ct of Const (\<^const_name>\Nominal.perm\, _) $ _ $ t => if member (op =) names (the_default "" (try (head_of #> dest_Const #> fst) t)) then SOME perm_bool else NONE - | _ => NONE)}; + | _ => NONE), + identifier = []}; fun transp ([] :: _) = [] | transp xs = map hd xs :: transp (map tl xs); diff -r d3328c562307 -r d769a183d51d src/HOL/Nominal/nominal_inductive2.ML --- a/src/HOL/Nominal/nominal_inductive2.ML Sat Oct 21 14:36:47 2023 +0200 +++ b/src/HOL/Nominal/nominal_inductive2.ML Sat Oct 21 21:19:02 2023 +0200 @@ -44,14 +44,16 @@ th RS infer_instantiate ctxt [(#1 (dest_Var (Thm.term_of perm_boolI_pi)), pi)] perm_boolI; fun mk_perm_bool_simproc names = - Simplifier.make_simproc \<^context> "perm_bool" - {lhss = [\<^term>\perm pi x\], + Simplifier.make_simproc \<^context> + {name = "perm_bool", + lhss = [\<^term>\perm pi x\], proc = fn _ => fn _ => fn ct => (case Thm.term_of ct of Const (\<^const_name>\Nominal.perm\, _) $ _ $ t => if member (op =) names (the_default "" (try (head_of #> dest_Const #> fst) t)) then SOME perm_bool else NONE - | _ => NONE)}; + | _ => NONE), + identifier = []}; fun transp ([] :: _) = [] | transp xs = map hd xs :: transp (map tl xs); diff -r d3328c562307 -r d769a183d51d src/HOL/Statespace/distinct_tree_prover.ML --- a/src/HOL/Statespace/distinct_tree_prover.ML Sat Oct 21 14:36:47 2023 +0200 +++ b/src/HOL/Statespace/distinct_tree_prover.ML Sat Oct 21 21:19:02 2023 +0200 @@ -364,14 +364,16 @@ mk_solver "distinctFieldSolver" (distinctTree_tac names); fun distinct_simproc names = - Simplifier.make_simproc \<^context> "DistinctTreeProver.distinct_simproc" - {lhss = [\<^term>\x = y\], + Simplifier.make_simproc \<^context> + {name = "DistinctTreeProver.distinct_simproc", + lhss = [\<^term>\x = y\], proc = fn _ => fn ctxt => fn ct => (case Thm.term_of ct of Const (\<^const_name>\HOL.eq\, _) $ x $ y => Option.map (fn neq => @{thm neq_to_eq_False} OF [neq]) (get_fst_success (neq_x_y ctxt x y) names) - | _ => NONE)}; + | _ => NONE), + identifier = []}; end; diff -r d3328c562307 -r d769a183d51d src/HOL/Tools/groebner.ML --- a/src/HOL/Tools/groebner.ML Sat Oct 21 14:36:47 2023 +0200 +++ b/src/HOL/Tools/groebner.ML Sat Oct 21 21:19:02 2023 +0200 @@ -779,9 +779,11 @@ let val th = poly_eq_conv ct in if Thm.is_reflexive th then NONE else SOME th end in - Simplifier.cert_simproc (Thm.theory_of_thm idl_sub) "poly_eq_simproc" - {lhss = [Thm.term_of (Thm.lhs_of idl_sub)], - proc = Morphism.entity (fn _ => fn _ => proc)} + Simplifier.cert_simproc (Thm.theory_of_thm idl_sub) + {name = "poly_eq_simproc", + lhss = [Thm.term_of (Thm.lhs_of idl_sub)], + proc = Morphism.entity (fn _ => fn _ => proc), + identifier = []} end; val poly_eq_ss = diff -r d3328c562307 -r d769a183d51d src/HOL/Tools/inductive_set.ML --- a/src/HOL/Tools/inductive_set.ML Sat Oct 21 14:36:47 2023 +0200 +++ b/src/HOL/Tools/inductive_set.ML Sat Oct 21 21:19:02 2023 +0200 @@ -38,8 +38,9 @@ val anyt = Free ("t", TFree ("'t", [])); fun strong_ind_simproc tab = - Simplifier.make_simproc \<^context> "strong_ind" - {lhss = [\<^term>\x::'a::{}\], + Simplifier.make_simproc \<^context> + {name = "strong_ind", + lhss = [\<^term>\x::'a::{}\], proc = fn _ => fn ctxt => fn ct => let fun close p t f = @@ -102,7 +103,8 @@ end else NONE | _ => NONE) - end}; + end, + identifier = []}; (* only eta contract terms occurring as arguments of functions satisfying p *) fun eta_contract p = @@ -318,11 +320,13 @@ fun to_pred_simproc rules = let val rules' = map mk_meta_eq rules in - Simplifier.make_simproc \<^context> "to_pred" - {lhss = [anyt], + Simplifier.make_simproc \<^context> + {name = "to_pred", + lhss = [anyt], proc = fn _ => fn ctxt => fn ct => lookup_rule (Proof_Context.theory_of ctxt) - (Thm.prop_of #> Logic.dest_equals) rules' (Thm.term_of ct)} + (Thm.prop_of #> Logic.dest_equals) rules' (Thm.term_of ct), + identifier = []} end; fun to_pred_proc thy rules t = diff -r d3328c562307 -r d769a183d51d src/HOL/Tools/record.ML --- a/src/HOL/Tools/record.ML Sat Oct 21 14:36:47 2023 +0200 +++ b/src/HOL/Tools/record.ML Sat Oct 21 21:19:02 2023 +0200 @@ -1322,8 +1322,9 @@ P t = ~1: completely split P t > 0: split up to given bound of record extensions.*) fun split_simproc P = - Simplifier.make_simproc \<^context> "record_split" - {lhss = [\<^term>\x::'a::{}\], + Simplifier.make_simproc \<^context> + {name = "record_split", + lhss = [\<^term>\x::'a::{}\], proc = fn _ => fn ctxt => fn ct => (case Thm.term_of ct of Const (quantifier, Type (_, [Type (_, [T, _]), _])) $ _ => @@ -1348,7 +1349,8 @@ else NONE end) else NONE - | _ => NONE)}; + | _ => NONE), + identifier = []}; fun ex_sel_eq_proc ctxt ct = let diff -r d3328c562307 -r d769a183d51d src/Pure/ML/ml_thms.ML --- a/src/Pure/ML/ml_thms.ML Sat Oct 21 14:36:47 2023 +0200 +++ b/src/Pure/ML/ml_thms.ML Sat Oct 21 21:19:02 2023 +0200 @@ -8,6 +8,8 @@ sig val the_attributes: Proof.context -> int -> Token.src list val the_thmss: Proof.context -> thm list list + val thm_binding: string -> bool -> thm list -> Proof.context -> + (Proof.context -> string * string) * Proof.context val embedded_lemma: (Proof.context -> thm list * (term list * Proof.context)) parser val get_stored_thms: unit -> thm list val get_stored_thm: unit -> thm diff -r d3328c562307 -r d769a183d51d src/Pure/Pure.thy --- a/src/Pure/Pure.thy Sat Oct 21 14:36:47 2023 +0200 +++ b/src/Pure/Pure.thy Sat Oct 21 21:19:02 2023 +0200 @@ -7,7 +7,7 @@ theory Pure keywords "!!" "!" "+" ":" ";" "<" "<=" "==" "=>" "?" "[" "\" "\" "\" "\" "\" - "\" "]" "binder" "by" "in" "infix" "infixl" "infixr" "is" "open" "output" + "\" "]" "binder" "by" "identifier" "in" "infix" "infixl" "infixr" "is" "open" "output" "overloaded" "passive" "pervasive" "premises" "structure" "unchecked" and "private" "qualified" :: before_command and "assumes" "constrains" "defines" "fixes" "for" "if" "includes" "notes" "rewrites" diff -r d3328c562307 -r d769a183d51d src/Pure/ROOT.ML --- a/src/Pure/ROOT.ML Sat Oct 21 14:36:47 2023 +0200 +++ b/src/Pure/ROOT.ML Sat Oct 21 21:19:02 2023 +0200 @@ -277,6 +277,7 @@ ML_file "Isar/class_declaration.ML"; ML_file "Isar/target_context.ML"; ML_file "Isar/experiment.ML"; +ML_file "ML/ml_thms.ML"; ML_file "simplifier.ML"; ML_file "Tools/plugin.ML"; @@ -327,7 +328,6 @@ (*ML add-ons*) ML_file "ML/ml_pp.ML"; -ML_file "ML/ml_thms.ML"; ML_file "ML/ml_instantiate.ML"; ML_file "ML/ml_file.ML"; ML_file "ML/ml_pid.ML"; diff -r d3328c562307 -r d769a183d51d src/Pure/raw_simplifier.ML --- a/src/Pure/raw_simplifier.ML Sat Oct 21 14:36:47 2023 +0200 +++ b/src/Pure/raw_simplifier.ML Sat Oct 21 21:19:02 2023 +0200 @@ -36,8 +36,8 @@ safe_solvers: string list} val dest_simps: simpset -> thm list type simproc - val eq_simproc: simproc * simproc -> bool - val cert_simproc: theory -> string -> {lhss: term list, proc: proc Morphism.entity} -> simproc + val cert_simproc: theory -> + {name: string, lhss: term list, proc: proc Morphism.entity, identifier: thm list} -> simproc val transform_simproc: morphism -> simproc -> simproc val trim_context_simproc: simproc -> simproc val simpset_of: Proof.context -> simpset @@ -215,10 +215,12 @@ {name: string, lhs: term, proc: proc Morphism.entity, - stamp: stamp}; + id: stamp * thm list}; -fun eq_simproc0 (Simproc0 {stamp = stamp1, ...}, Simproc0 {stamp = stamp2, ...}) = - stamp1 = stamp2; +fun eq_simproc_id ((s1: stamp, ths1: thm list), (s2, ths2)) = + s1 = s2 andalso eq_list Thm.eq_thm_prop (ths1, ths2); + +fun eq_simproc0 (Simproc0 a, Simproc0 b) = eq_simproc_id (#id a, #id b); (* solvers *) @@ -291,8 +293,8 @@ {simps = Net.entries rules |> map (fn {name, thm, ...} => (name, thm)), procs = Net.entries procs - |> map (fn Simproc0 {name, lhs, stamp, ...} => ((name, lhs), stamp)) - |> partition_eq (eq_snd op =) + |> map (fn Simproc0 {name, lhs, id, ...} => ((name, lhs), id)) + |> partition_eq (eq_snd eq_simproc_id) |> map (fn ps => (fst (fst (hd ps)), map (snd o fst) ps)), congs = congs |> fst |> Congtab.dest, weak_congs = congs |> snd, @@ -719,26 +721,28 @@ {name: string, lhss: term list, proc: proc Morphism.entity, - stamp: stamp}; - -fun eq_simproc (Simproc {stamp = stamp1, ...}, Simproc {stamp = stamp2, ...}) = stamp1 = stamp2; + id: stamp * thm list}; -fun cert_simproc thy name {lhss, proc} = - Simproc {name = name, lhss = map (Sign.cert_term thy) lhss, proc = proc, stamp = stamp ()}; +fun cert_simproc thy {name, lhss, proc, identifier} = + Simproc + {name = name, + lhss = map (Sign.cert_term thy) lhss, + proc = proc, + id = (stamp (), map (Thm.transfer thy) identifier)}; -fun transform_simproc phi (Simproc {name, lhss, proc, stamp}) = +fun transform_simproc phi (Simproc {name, lhss, proc, id = (stamp, identifier)}) = Simproc {name = name, lhss = map (Morphism.term phi) lhss, proc = Morphism.transform phi proc, - stamp = stamp}; + id = (stamp, Morphism.fact phi identifier)}; -fun trim_context_simproc (Simproc {name, lhss, proc, stamp}) = +fun trim_context_simproc (Simproc {name, lhss, proc, id = (stamp, identifier)}) = Simproc {name = name, lhss = lhss, proc = Morphism.entity_reset_context proc, - stamp = stamp}; + id = (stamp, map Thm.trim_context identifier)}; local @@ -762,8 +766,8 @@ (cond_warning ctxt (fn () => "Simplification procedure " ^ quote name ^ " not in simpset"); ctxt); -fun prep_procs (Simproc {name, lhss, proc, stamp}) = - lhss |> map (fn lhs => Simproc0 {name = name, lhs = lhs, proc = proc, stamp = stamp}); +fun prep_procs (Simproc {name, lhss, proc, id}) = + lhss |> map (fn lhs => Simproc0 {name = name, lhs = lhs, proc = proc, id = id}); in diff -r d3328c562307 -r d769a183d51d src/Pure/simplifier.ML --- a/src/Pure/simplifier.ML Sat Oct 21 14:36:47 2023 +0200 +++ b/src/Pure/simplifier.ML Sat Oct 21 21:19:02 2023 +0200 @@ -37,14 +37,16 @@ val cong_del: attribute val check_simproc: Proof.context -> xstring * Position.T -> string * simproc val the_simproc: Proof.context -> string -> simproc - val make_simproc: Proof.context -> string -> - {lhss: term list, proc: morphism -> proc} -> simproc - type ('a, 'b) simproc_spec = {passive: bool, name: binding, lhss: 'a list, proc: 'b} - val read_simproc_spec: Proof.context -> (string, 'a) simproc_spec -> (term, 'a) simproc_spec - val define_simproc: (term, morphism -> proc) simproc_spec -> local_theory -> + val make_simproc: Proof.context -> + {name: string, lhss: term list, proc: morphism -> proc, identifier: thm list} -> simproc + type ('a, 'b, 'c) simproc_spec = + {passive: bool, name: binding, lhss: 'a list, proc: 'b, identifier: 'c} + val read_simproc_spec: Proof.context -> + (string, 'b, 'c) simproc_spec -> (term, 'b, 'c) simproc_spec + val define_simproc: (term, morphism -> proc, thm list) simproc_spec -> local_theory -> simproc * local_theory - val simproc_setup: (term, morphism -> proc) simproc_spec -> simproc - val simproc_setup_cmd: (string, morphism -> proc) simproc_spec -> simproc + val simproc_setup: (term, morphism -> proc, thm list) simproc_spec -> simproc + val simproc_setup_cmd: (string, morphism -> proc, thm list) simproc_spec -> simproc val simproc_setup_command: (local_theory -> local_theory) parser val pretty_simpset: bool -> Proof.context -> Pretty.T val default_mk_sym: Proof.context -> thm -> thm option @@ -125,28 +127,30 @@ (* define simprocs *) -fun make_simproc ctxt name {lhss, proc} = +fun make_simproc ctxt {name, lhss, proc, identifier} = let val ctxt' = fold Proof_Context.augment lhss ctxt; val lhss' = Variable.export_terms ctxt' ctxt lhss; in - cert_simproc (Proof_Context.theory_of ctxt) name - {lhss = lhss', proc = Morphism.entity proc} + cert_simproc (Proof_Context.theory_of ctxt) + {name = name, lhss = lhss', proc = Morphism.entity proc, identifier = identifier} end; -type ('a, 'b) simproc_spec = {passive: bool, name: binding, lhss: 'a list, proc: 'b}; +type ('a, 'b, 'c) simproc_spec = + {passive: bool, name: binding, lhss: 'a list, proc: 'b, identifier: 'c}; -fun read_simproc_spec ctxt {passive, name, lhss, proc} : (term, 'a) simproc_spec = +fun read_simproc_spec ctxt {passive, name, lhss, proc, identifier} = let val lhss' = Syntax.read_terms ctxt lhss handle ERROR msg => error (msg ^ Position.here_list (map Syntax.read_input_pos lhss)); - in {passive = passive, name = name, lhss = lhss', proc = proc} end; + in {passive = passive, name = name, lhss = lhss', proc = proc, identifier = identifier} end; -fun define_simproc {passive, name, lhss, proc} lthy = +fun define_simproc {passive, name, lhss, proc, identifier} lthy = let val simproc0 = - make_simproc lthy (Local_Theory.full_name lthy name) {lhss = lhss, proc = proc}; + make_simproc lthy + {name = Local_Theory.full_name lthy name, lhss = lhss, proc = proc, identifier = identifier}; in lthy |> Local_Theory.declaration {syntax = false, pervasive = false, pos = Binding.pos_of name} (fn phi => fn context => @@ -171,12 +175,14 @@ Named_Target.setup_result Raw_Simplifier.transform_simproc (fn lthy => lthy |> define_simproc (read_simproc_spec lthy args)); -val simproc_setup_parser = + +val parse_simproc_spec = Scan.optional (Parse.$$$ "passive" >> K true) false -- Parse.binding -- (Parse.$$$ "(" |-- Parse.enum1 "|" Parse.term --| Parse.$$$ ")") -- - (Parse.$$$ "=" |-- Parse.ML_source) - >> (fn (((a, b), c), d) => {passive = a, name = b, lhss = c, proc = d}); + (Parse.$$$ "=" |-- Parse.ML_source) -- + Scan.option ((Parse.position (Parse.$$$ "identifier") >> #2) -- Parse.thms1) + >> (fn ((((a, b), c), d), e) => {passive = a, name = b, lhss = c, proc = d, identifier = e}); val _ = Theory.setup (ML_Context.add_antiquotation_embedded \<^binding>\simproc_setup\ @@ -184,31 +190,44 @@ let val ml = ML_Lex.tokenize_no_range; - val {passive, name, lhss, proc} = input - |> Parse.read_embedded ctxt (Thy_Header.get_keywords' ctxt) simproc_setup_parser + val {passive, name, lhss, proc, identifier} = input + |> Parse.read_embedded ctxt (Thy_Header.get_keywords' ctxt) parse_simproc_spec |> read_simproc_spec ctxt; - val (decl, ctxt') = ML_Context.read_antiquotes proc ctxt; - fun decl' ctxt'' = + val (decl1, ctxt1) = ML_Context.read_antiquotes proc ctxt; + val (decl2, ctxt2) = + (case identifier of + NONE => (K ("", "[]"), ctxt1) + | SOME (_, thms) => ML_Thms.thm_binding "thms" false (Attrib.eval_thms ctxt1 thms) ctxt1); + + fun decl' ctxt' = let - val (ml_env, ml_body) = decl ctxt''; + val (ml_env1, ml_body1) = decl1 ctxt'; + val (ml_env2, ml_body2) = decl2 ctxt' |> apply2 ml; val ml_body' = ml "Simplifier.simproc_setup {passive = " @ ml (Bool.toString passive) @ ml ", name = " @ ml (ML_Syntax.make_binding (Binding.name_of name, Binding.pos_of name)) @ ml ", lhss = " @ ml (ML_Syntax.print_list ML_Syntax.print_term lhss) @ - ml ", proc = (" @ ml_body @ ml ")}"; - in (ml_env, ml_body') end; - in (decl', ctxt') end)); + ml ", proc = (" @ ml_body1 @ ml ")" @ + ml ", identifier = (" @ ml_body2 @ ml ")}"; + in (ml_env1 @ ml_env2, ml_body') end; + in (decl', ctxt2) end)); val simproc_setup_command = - simproc_setup_parser >> (fn {passive, name, lhss, proc} => - Context.proof_map - (ML_Context.expression (Input.pos_of proc) - (ML_Lex.read - ("Simplifier.simproc_setup_cmd {passive = " ^ Bool.toString passive ^ - ", name = " ^ ML_Syntax.make_binding (Binding.name_of name, Binding.pos_of name) ^ - ", lhss = " ^ ML_Syntax.print_strings lhss ^ - ", proc = (") @ ML_Lex.read_source proc @ ML_Lex.read ")}"))); + parse_simproc_spec >> (fn {passive, name, lhss, proc, identifier} => + (case identifier of + NONE => + Context.proof_map + (ML_Context.expression (Input.pos_of proc) + (ML_Lex.read + ("Simplifier.simproc_setup_cmd {passive = " ^ Bool.toString passive ^ + ", name = " ^ ML_Syntax.make_binding (Binding.name_of name, Binding.pos_of name) ^ + ", lhss = " ^ ML_Syntax.print_strings lhss ^ + ", proc = (") @ ML_Lex.read_source proc @ ML_Lex.read "), identifier = []}")) + | SOME (pos, _) => + error ("Bad command " ^ Markup.markup Markup.keyword1 "simproc_setup" ^ + " with " ^ Markup.markup Markup.keyword2 "identifier" ^ + ": this is only supported in\nML antiquotation \<^simproc_setup>\...\" ^ Position.here pos)));