# HG changeset patch # User wenzelm # Date 1575232148 -3600 # Node ID 8af82f3e03c99a98cda6b3c028cc53a28c3721b0 # Parent 20dce31fe7f40b0ace832f5c4a8e7ea18cf1def3 formal position for spec rule (not significant for equality); diff -r 20dce31fe7f4 -r 8af82f3e03c9 src/HOL/Tools/Nunchaku/nunchaku_collect.ML --- a/src/HOL/Tools/Nunchaku/nunchaku_collect.ML Sun Dec 01 15:38:36 2019 +0100 +++ b/src/HOL/Tools/Nunchaku/nunchaku_collect.ML Sun Dec 01 21:29:08 2019 +0100 @@ -500,7 +500,7 @@ val specs = if s = \<^const_name>\The\ then - [{name = "", rough_classification = Spec_Rules.Unknown, + [{pos = Position.none, name = "", rough_classification = Spec_Rules.Unknown, terms = [Logic.varify_global \<^term>\The\], rules = [@{thm theI_unique}]}] else if s = \<^const_name>\finite\ then @@ -508,7 +508,7 @@ if card = Inf orelse card = Fin_or_Inf then spec_rules () else - [{name = "", rough_classification = Spec_Rules.equational, + [{pos = Position.none, name = "", rough_classification = Spec_Rules.equational, terms = [Logic.varify_global \<^term>\finite\], rules = [Skip_Proof.make_thm thy (Logic.varify_global \<^prop>\finite A = True\)]}] end diff -r 20dce31fe7f4 -r 8af82f3e03c9 src/Pure/Isar/spec_rules.ML --- a/src/Pure/Isar/spec_rules.ML Sun Dec 01 15:38:36 2019 +0100 +++ b/src/Pure/Isar/spec_rules.ML Sun Dec 01 21:29:08 2019 +0100 @@ -28,7 +28,11 @@ val is_unknown: rough_classification -> bool val encode_rough_classification: rough_classification XML.Encode.T type spec = - {name: string, rough_classification: rough_classification, terms: term list, rules: thm list} + {pos: Position.T, + name: string, + rough_classification: rough_classification, + terms: term list, + rules: thm list} val get: Proof.context -> spec list val get_global: theory -> spec list val dest_theory: theory -> spec list @@ -97,7 +101,11 @@ (* rules *) type spec = - {name: string, rough_classification: rough_classification, terms: term list, rules: thm list}; + {pos: Position.T, + name: string, + rough_classification: rough_classification, + terms: term list, + rules: thm list}; fun eq_spec (specs: spec * spec) = (op =) (apply2 #name specs) andalso @@ -105,8 +113,9 @@ eq_list (op aconv) (apply2 #terms specs) andalso eq_list Thm.eq_thm_prop (apply2 #rules specs); -fun map_spec_rules f ({name, rough_classification, terms, rules}: spec) : spec = - {name = name, rough_classification = rough_classification, terms = terms, rules = map f rules}; +fun map_spec_rules f ({pos, name, rough_classification, terms, rules}: spec) : spec = + {pos = pos, name = name, rough_classification = rough_classification, terms = terms, + rules = map f rules}; structure Rules = Generic_Data ( @@ -150,7 +159,10 @@ (* add *) fun add name rough_classification terms rules lthy = - let val thms0 = map Thm.trim_context (map (Drule.mk_term o Thm.cterm_of lthy) terms @ rules) in + let + val pos = Position.thread_data (); + val thms0 = map Thm.trim_context (map (Drule.mk_term o Thm.cterm_of lthy) terms @ rules); + in lthy |> Local_Theory.declaration {syntax = false, pervasive = true} (fn phi => fn context => let @@ -162,14 +174,14 @@ ||> map Thm.trim_context; in context |> (Rules.map o Item_Net.update) - {name = name, rough_classification = rough_classification, + {pos = pos, name = name, rough_classification = rough_classification, terms = terms', rules = rules'} end) end; fun add_global name rough_classification terms rules = (Context.theory_map o Rules.map o Item_Net.update) - {name = name, rough_classification = rough_classification, + {pos = Position.thread_data (), name = name, rough_classification = rough_classification, terms = terms, rules = map Thm.trim_context rules}; end; diff -r 20dce31fe7f4 -r 8af82f3e03c9 src/Pure/Thy/export_theory.ML --- a/src/Pure/Thy/export_theory.ML Sun Dec 01 15:38:36 2019 +0100 +++ b/src/Pure/Thy/export_theory.ML Sun Dec 01 21:29:08 2019 +0100 @@ -402,15 +402,15 @@ (* spec rules *) - fun encode_spec {name, rough_classification, terms, rules} = + fun encode_spec {pos, name, rough_classification, terms, rules} = let val terms' = map Logic.unvarify_global terms; val rules' = map (fn rule => #1 (standard_prop_of (prep_thm rule) NONE)) rules; open XML.Encode; in - pair string (pair Spec_Rules.encode_rough_classification - (pair (list encode_term) (list encode_prop))) - (name, (rough_classification, (terms', rules'))) + pair properties (pair string (pair Spec_Rules.encode_rough_classification + (pair (list encode_term) (list encode_prop)))) + (Position.properties_of pos, (name, (rough_classification, (terms', rules')))) end; val _ = diff -r 20dce31fe7f4 -r 8af82f3e03c9 src/Pure/Thy/export_theory.scala --- a/src/Pure/Thy/export_theory.scala Sun Dec 01 15:38:36 2019 +0100 +++ b/src/Pure/Thy/export_theory.scala Sun Dec 01 21:29:08 2019 +0100 @@ -711,13 +711,17 @@ sealed case class Spec_Rule( + pos: Position.T, name: String, rough_classification: Rough_Classification, terms: List[Term.Term], rules: List[Prop]) { + def id: Option[Long] = Position.Id.unapply(pos) + def cache(cache: Term.Cache): Spec_Rule = Spec_Rule( + cache.position(pos), cache.string(name), rough_classification.cache(cache), terms.map(cache.term(_)), @@ -731,10 +735,11 @@ { import XML.Decode._ import Term_XML.Decode._ - list(pair(string, pair(decode_rough_classification, pair(list(term), list(decode_prop)))))( - body) + list( + pair(properties, pair(string, pair(decode_rough_classification, + pair(list(term), list(decode_prop))))))(body) } - for ((name, (rough_classification, (terms, rules))) <- spec_rules) - yield Spec_Rule(name, rough_classification, terms, rules) + for ((pos, (name, (rough_classification, (terms, rules)))) <- spec_rules) + yield Spec_Rule(pos, name, rough_classification, terms, rules) } }