--- 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>\<open>The\<close> then
- [{name = "", rough_classification = Spec_Rules.Unknown,
+ [{pos = Position.none, name = "", rough_classification = Spec_Rules.Unknown,
terms = [Logic.varify_global \<^term>\<open>The\<close>],
rules = [@{thm theI_unique}]}]
else if s = \<^const_name>\<open>finite\<close> 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>\<open>finite\<close>],
rules = [Skip_Proof.make_thm thy (Logic.varify_global \<^prop>\<open>finite A = True\<close>)]}]
end
--- 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;
--- 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 _ =
--- 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)
}
}