--- a/src/HOL/Number_Theory/Residues.thy Fri Dec 06 17:03:58 2019 +0100
+++ b/src/HOL/Number_Theory/Residues.thy Fri Dec 06 19:56:45 2019 +0100
@@ -465,7 +465,6 @@
shows "card A \<le> n"
proof -
define R where "R = residue_ring (int p)"
- term monom
from assms(1) interpret residues_prime p R
by unfold_locales (simp_all add: R_def)
interpret R: UP_domain R "UP R" by (unfold_locales)
--- a/src/HOL/Tools/BNF/bnf_fp_util.ML Fri Dec 06 17:03:58 2019 +0100
+++ b/src/HOL/Tools/BNF/bnf_fp_util.ML Fri Dec 06 19:56:45 2019 +0100
@@ -213,7 +213,6 @@
binding list -> (string * sort) list -> (string * sort) list -> (string * sort) list ->
typ list -> BNF_Comp.comp_cache -> local_theory ->
((BNF_Def.bnf list * BNF_Comp.absT_info list) * BNF_Comp.comp_cache) * 'a
- val fp_antiquote_setup: binding -> theory -> theory
end;
structure BNF_FP_Util : BNF_FP_UTIL =
@@ -982,27 +981,4 @@
(((pre_bnfs, absT_infos), comp_cache'), res)
end;
-fun fp_antiquote_setup binding =
- Thy_Output.antiquotation_pretty_source_embedded binding
- (Args.type_name {proper = true, strict = true})
- (fn ctxt => fn fcT_name =>
- (case Ctr_Sugar.ctr_sugar_of ctxt fcT_name of
- NONE => error ("Not a known freely generated type name: " ^ quote fcT_name)
- | SOME {T = T0, ctrs = ctrs0, ...} =>
- let
- val freezeT = Term.map_atyps (fn TVar ((s, _), S) => TFree (s, S) | T => T);
-
- val T = freezeT T0;
- val ctrs = map (Term.map_types freezeT) ctrs0;
-
- val pretty_typ_bracket = Syntax.pretty_typ (Config.put pretty_priority 1001 ctxt);
- fun pretty_ctr ctr =
- Pretty.block (Pretty.breaks (Syntax.pretty_term ctxt ctr ::
- map pretty_typ_bracket (binder_types (fastype_of ctr))));
- in
- Pretty.block (Pretty.keyword1 (Binding.name_of binding) :: Pretty.brk 1 ::
- Syntax.pretty_typ ctxt T :: Pretty.str " =" :: Pretty.brk 1 ::
- flat (separate [Pretty.brk 1, Pretty.str "| "] (map (single o pretty_ctr) ctrs)))
- end));
-
end;
--- a/src/HOL/Tools/BNF/bnf_gfp.ML Fri Dec 06 17:03:58 2019 +0100
+++ b/src/HOL/Tools/BNF/bnf_gfp.ML Fri Dec 06 19:56:45 2019 +0100
@@ -2606,6 +2606,4 @@
Outer_Syntax.local_theory \<^command_keyword>\<open>codatatype\<close> "define coinductive datatypes"
(parse_co_datatype_cmd Greatest_FP construct_gfp);
-val _ = Theory.setup (fp_antiquote_setup \<^binding>\<open>codatatype\<close>);
-
end;
--- a/src/HOL/Tools/BNF/bnf_lfp.ML Fri Dec 06 17:03:58 2019 +0100
+++ b/src/HOL/Tools/BNF/bnf_lfp.ML Fri Dec 06 19:56:45 2019 +0100
@@ -1870,6 +1870,4 @@
Outer_Syntax.local_theory \<^command_keyword>\<open>datatype\<close> "define inductive datatypes"
(parse_co_datatype_cmd Least_FP construct_lfp);
-val _ = Theory.setup (fp_antiquote_setup \<^binding>\<open>datatype\<close>);
-
end;
--- a/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Fri Dec 06 17:03:58 2019 +0100
+++ b/src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML Fri Dec 06 19:56:45 2019 +0100
@@ -177,17 +177,17 @@
structure Data = Generic_Data
(
- type T = ctr_sugar Symtab.table;
+ type T = (Position.T * ctr_sugar) Symtab.table;
val empty = Symtab.empty;
val extend = I;
fun merge data : T = Symtab.merge (K true) data;
);
fun ctr_sugar_of_generic context =
- Option.map (transfer_ctr_sugar (Context.theory_of context)) o Symtab.lookup (Data.get context);
+ Option.map (transfer_ctr_sugar (Context.theory_of context) o #2) o Symtab.lookup (Data.get context);
fun ctr_sugars_of_generic context =
- Symtab.fold (cons o transfer_ctr_sugar (Context.theory_of context) o snd) (Data.get context) [];
+ Symtab.fold (cons o transfer_ctr_sugar (Context.theory_of context) o #2 o #2) (Data.get context) [];
fun ctr_sugar_of_case_generic context s =
find_first (fn {casex = Const (s', _), ...} => s' = s | _ => false)
@@ -210,20 +210,24 @@
val interpret_ctr_sugar = Ctr_Sugar_Plugin.data;
-fun register_ctr_sugar_raw (ctr_sugar as {T = Type (s, _), ...}) =
+fun register_ctr_sugar_raw (ctr_sugar as {T = Type (name, _), ...}) =
Local_Theory.declaration {syntax = false, pervasive = true}
- (fn phi => Data.map (Symtab.update (s, morph_ctr_sugar phi ctr_sugar)));
+ (fn phi => fn context =>
+ let val pos = Position.thread_data ()
+ in Data.map (Symtab.update (name, (pos, morph_ctr_sugar phi ctr_sugar))) context end);
fun register_ctr_sugar plugins ctr_sugar =
register_ctr_sugar_raw ctr_sugar #> interpret_ctr_sugar plugins ctr_sugar;
-fun default_register_ctr_sugar_global plugins (ctr_sugar as {T = Type (s, _), ...}) thy =
- let val tab = Data.get (Context.Theory thy) in
- if Symtab.defined tab s then
- thy
+fun default_register_ctr_sugar_global plugins (ctr_sugar as {T = Type (name, _), ...}) thy =
+ let
+ val tab = Data.get (Context.Theory thy);
+ val pos = Position.thread_data ();
+ in
+ if Symtab.defined tab name then thy
else
thy
- |> Context.theory_map (Data.put (Symtab.update_new (s, ctr_sugar) tab))
+ |> Context.theory_map (Data.put (Symtab.update_new (name, (pos, ctr_sugar)) tab))
|> Named_Target.theory_map (Ctr_Sugar_Plugin.data plugins ctr_sugar)
end;
@@ -1187,4 +1191,80 @@
-- parse_sel_default_eqs
>> free_constructors_cmd Unknown);
+
+
+(** external views **)
+
+(* document antiquotations *)
+
+local
+
+fun antiquote_setup binding co =
+ Thy_Output.antiquotation_pretty_source_embedded binding
+ ((Scan.ahead (Scan.lift Parse.not_eof) >> Token.pos_of) --
+ Args.type_name {proper = true, strict = true})
+ (fn ctxt => fn (pos, type_name) =>
+ let
+ fun err () =
+ error ("Bad " ^ Binding.name_of binding ^ ": " ^ quote type_name ^ Position.here pos);
+ in
+ (case ctr_sugar_of ctxt type_name of
+ NONE => err ()
+ | SOME {kind, T = T0, ctrs = ctrs0, ...} =>
+ let
+ val _ = if co = (kind = Codatatype) then () else err ();
+
+ val T = Logic.unvarifyT_global T0;
+ val ctrs = map Logic.unvarify_global ctrs0;
+
+ val pretty_typ_bracket = Syntax.pretty_typ (Config.put pretty_priority 1001 ctxt);
+ fun pretty_ctr ctr =
+ Pretty.block (Pretty.breaks (Syntax.pretty_term ctxt ctr ::
+ map pretty_typ_bracket (binder_types (fastype_of ctr))));
+ in
+ Pretty.block (Pretty.keyword1 (Binding.name_of binding) :: Pretty.brk 1 ::
+ Syntax.pretty_typ ctxt T :: Pretty.str " =" :: Pretty.brk 1 ::
+ flat (separate [Pretty.brk 1, Pretty.str "| "] (map (single o pretty_ctr) ctrs)))
+ end)
+ end);
+
+in
+
+val _ =
+ Theory.setup
+ (antiquote_setup \<^binding>\<open>datatype\<close> false #>
+ antiquote_setup \<^binding>\<open>codatatype\<close> true);
+
end;
+
+
+(* theory export *)
+
+val _ = Export_Theory.setup_presentation (fn context => fn thy =>
+ let
+ val parents = map (Data.get o Context.Theory) (Theory.parents_of thy);
+ val datatypes =
+ (Data.get (Context.Theory thy), []) |-> Symtab.fold
+ (fn (name, (pos, {kind, T, ctrs, ...})) =>
+ if kind = Record orelse exists (fn tab => Symtab.defined tab name) parents then I
+ else
+ let
+ val pos_properties = Thy_Info.adjust_pos_properties context pos;
+ val typ = Logic.unvarifyT_global T;
+ val constrs = map Logic.unvarify_global ctrs;
+ val typargs = rev (fold Term.add_tfrees (Logic.mk_type typ :: constrs) []);
+ val constructors = map (fn t => (t, Term.type_of t)) constrs;
+ in
+ cons (pos_properties, (name, (kind = Codatatype, (typargs, (typ, constructors)))))
+ end);
+ in
+ if null datatypes then ()
+ else
+ Export_Theory.export_body thy "datatypes"
+ let open XML.Encode Term_XML.Encode in
+ list (pair properties (pair string (pair bool (pair (list (pair string sort))
+ (pair typ (list (pair (term (Sign.consts_of thy)) typ))))))) datatypes
+ end
+ end);
+
+end;
--- a/src/Pure/Concurrent/par_exn.ML Fri Dec 06 17:03:58 2019 +0100
+++ b/src/Pure/Concurrent/par_exn.ML Fri Dec 06 19:56:45 2019 +0100
@@ -7,7 +7,7 @@
signature PAR_EXN =
sig
- val identify: Properties.entry list -> exn -> exn
+ val identify: Properties.T -> exn -> exn
val the_serial: exn -> int
val make: exn list -> exn
val dest: exn -> exn list option
--- a/src/Pure/ML/exn_properties.ML Fri Dec 06 17:03:58 2019 +0100
+++ b/src/Pure/ML/exn_properties.ML Fri Dec 06 19:56:45 2019 +0100
@@ -9,7 +9,7 @@
val position_of_polyml_location: ML_Compiler0.polyml_location -> Position.T
val position: exn -> Position.T
val get: exn -> Properties.T
- val update: Properties.entry list -> exn -> exn
+ val update: Properties.T -> exn -> exn
end;
structure Exn_Properties: EXN_PROPERTIES =
--- a/src/Pure/Thy/export_theory.ML Fri Dec 06 17:03:58 2019 +0100
+++ b/src/Pure/Thy/export_theory.ML Fri Dec 06 19:56:45 2019 +0100
@@ -121,19 +121,18 @@
(* presentation *)
-val _ = setup_presentation (fn {adjust_pos, ...} => fn thy =>
+val _ = setup_presentation (fn context => fn thy =>
let
val parents = Theory.parents_of thy;
val rep_tsig = Type.rep_tsig (Sign.tsig_of thy);
val thy_ctxt = Proof_Context.init_global thy;
+ val pos_properties = Thy_Info.adjust_pos_properties context;
+
(* spec rules *)
- fun position_properties pos =
- Position.offset_properties_of (adjust_pos pos) @ Position.id_properties_of pos;
-
fun spec_rule_content {pos, name, rough_classification, terms, rules} =
let
val spec =
@@ -141,7 +140,7 @@
|> Term_Subst.zero_var_indexes_list
|> map Logic.unvarify_global;
in
- {props = position_properties pos,
+ {props = pos_properties pos,
name = name,
rough_classification = rough_classification,
typargs = rev (fold Term.add_tfrees spec []),
@@ -154,7 +153,7 @@
(* entities *)
fun make_entity_markup name xname pos serial =
- let val props = position_properties pos @ Markup.serial_properties serial;
+ let val props = pos_properties pos @ Markup.serial_properties serial;
in (Markup.entityN, (Markup.nameN, name) :: (Markup.xnameN, xname) :: props) end;
fun entity_markup space name =
--- a/src/Pure/Thy/export_theory.scala Fri Dec 06 17:03:58 2019 +0100
+++ b/src/Pure/Thy/export_theory.scala Fri Dec 06 19:56:45 2019 +0100
@@ -31,18 +31,6 @@
sessions_structure: Sessions.Structure,
session_name: String,
progress: Progress = No_Progress,
- types: Boolean = true,
- consts: Boolean = true,
- axioms: Boolean = true,
- thms: Boolean = true,
- classes: Boolean = true,
- locales: Boolean = true,
- locale_dependencies: Boolean = true,
- classrel: Boolean = true,
- arities: Boolean = true,
- constdefs: Boolean = true,
- typedefs: Boolean = true,
- spec_rules: Boolean = true,
cache: Term.Cache = Term.make_cache()): Session =
{
val thys =
@@ -54,11 +42,7 @@
yield {
progress.echo("Reading theory " + theory)
read_theory(Export.Provider.database(db, session, theory),
- session, theory, types = types, consts = consts,
- axioms = axioms, thms = thms, classes = classes, locales = locales,
- locale_dependencies = locale_dependencies, classrel = classrel, arities = arities,
- constdefs = constdefs, typedefs = typedefs,
- spec_rules = spec_rules, cache = Some(cache))
+ session, theory, cache = Some(cache))
}
}
}))
@@ -93,6 +77,7 @@
arities: List[Arity],
constdefs: List[Constdef],
typedefs: List[Typedef],
+ datatypes: List[Datatype],
spec_rules: List[Spec_Rule])
{
override def toString: String = name
@@ -120,22 +105,11 @@
arities.map(_.cache(cache)),
constdefs.map(_.cache(cache)),
typedefs.map(_.cache(cache)),
+ datatypes.map(_.cache(cache)),
spec_rules.map(_.cache(cache)))
}
def read_theory(provider: Export.Provider, session_name: String, theory_name: String,
- types: Boolean = true,
- consts: Boolean = true,
- axioms: Boolean = true,
- thms: Boolean = true,
- classes: Boolean = true,
- locales: Boolean = true,
- locale_dependencies: Boolean = true,
- classrel: Boolean = true,
- arities: Boolean = true,
- constdefs: Boolean = true,
- typedefs: Boolean = true,
- spec_rules: Boolean = true,
cache: Option[Term.Cache] = None): Theory =
{
val parents =
@@ -150,18 +124,19 @@
}
val theory =
Theory(theory_name, parents,
- if (types) read_types(provider) else Nil,
- if (consts) read_consts(provider) else Nil,
- if (axioms) read_axioms(provider) else Nil,
- if (thms) read_thms(provider) else Nil,
- if (classes) read_classes(provider) else Nil,
- if (locales) read_locales(provider) else Nil,
- if (locale_dependencies) read_locale_dependencies(provider) else Nil,
- if (classrel) read_classrel(provider) else Nil,
- if (arities) read_arities(provider) else Nil,
- if (constdefs) read_constdefs(provider) else Nil,
- if (typedefs) read_typedefs(provider) else Nil,
- if (spec_rules) read_spec_rules(provider) else Nil)
+ read_types(provider),
+ read_consts(provider),
+ read_axioms(provider),
+ read_thms(provider),
+ read_classes(provider),
+ read_locales(provider),
+ read_locale_dependencies(provider),
+ read_classrel(provider),
+ read_arities(provider),
+ read_constdefs(provider),
+ read_typedefs(provider),
+ read_datatypes(provider),
+ read_spec_rules(provider))
if (cache.isDefined) theory.cache(cache.get) else theory
}
@@ -646,6 +621,43 @@
}
+ /* HOL datatypes */
+
+ sealed case class Datatype(
+ pos: Position.T,
+ name: String,
+ co: Boolean,
+ typargs: List[(String, Term.Sort)],
+ typ: Term.Typ,
+ constructors: List[(Term.Term, Term.Typ)])
+ {
+ def id: Option[Long] = Position.Id.unapply(pos)
+
+ def cache(cache: Term.Cache): Datatype =
+ Datatype(
+ cache.position(pos),
+ cache.string(name),
+ co,
+ typargs.map({ case (name, sort) => (cache.string(name), cache.sort(sort)) }),
+ cache.typ(typ),
+ constructors.map({ case (term, typ) => (cache.term(term), cache.typ(typ)) }))
+ }
+
+ def read_datatypes(provider: Export.Provider): List[Datatype] =
+ {
+ val body = provider.uncompressed_yxml(export_prefix + "datatypes")
+ val datatypes =
+ {
+ import XML.Decode._
+ import Term_XML.Decode._
+ list(pair(properties, pair(string, pair(bool, pair(list(pair(string, sort)),
+ pair(typ, list(pair(term, typ))))))))(body)
+ }
+ for ((pos, (name, (co, (typargs, (typ, constructors))))) <- datatypes)
+ yield Datatype(pos, name, co, typargs, typ, constructors)
+ }
+
+
/* Pure spec rules */
sealed abstract class Recursion
--- a/src/Pure/Thy/thy_info.ML Fri Dec 06 17:03:58 2019 +0100
+++ b/src/Pure/Thy/thy_info.ML Fri Dec 06 19:56:45 2019 +0100
@@ -10,6 +10,7 @@
type presentation_context =
{options: Options.T, file_pos: Position.T, adjust_pos: Position.T -> Position.T,
segments: Thy_Output.segment list}
+ val adjust_pos_properties: presentation_context -> Position.T -> Properties.T
val apply_presentation: presentation_context -> theory -> unit
val add_presentation: (presentation_context -> theory -> unit) -> theory -> theory
val get_names: unit -> string list
@@ -38,6 +39,9 @@
{options: Options.T, file_pos: Position.T, adjust_pos: Position.T -> Position.T,
segments: Thy_Output.segment list};
+fun adjust_pos_properties (context: presentation_context) pos =
+ Position.offset_properties_of (#adjust_pos context pos) @ Position.id_properties_of pos;
+
structure Presentation = Theory_Data
(
type T = ((presentation_context -> theory -> unit) * stamp) list;