# HG changeset patch # User wenzelm # Date 1575658605 -3600 # Node ID a9ad4a954cb7f73e529b9a893afca810c93510a0 # Parent 38457af660bc89eee6ff1585de640db7f86ac1d5# Parent a624319011409e2fbf31532508dde07ef0438a34 merged diff -r 38457af660bc -r a9ad4a954cb7 src/HOL/Number_Theory/Residues.thy --- 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 \ 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) diff -r 38457af660bc -r a9ad4a954cb7 src/HOL/Tools/BNF/bnf_fp_util.ML --- 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; diff -r 38457af660bc -r a9ad4a954cb7 src/HOL/Tools/BNF/bnf_gfp.ML --- 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>\codatatype\ "define coinductive datatypes" (parse_co_datatype_cmd Greatest_FP construct_gfp); -val _ = Theory.setup (fp_antiquote_setup \<^binding>\codatatype\); - end; diff -r 38457af660bc -r a9ad4a954cb7 src/HOL/Tools/BNF/bnf_lfp.ML --- 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>\datatype\ "define inductive datatypes" (parse_co_datatype_cmd Least_FP construct_lfp); -val _ = Theory.setup (fp_antiquote_setup \<^binding>\datatype\); - end; diff -r 38457af660bc -r a9ad4a954cb7 src/HOL/Tools/Ctr_Sugar/ctr_sugar.ML --- 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>\datatype\ false #> + antiquote_setup \<^binding>\codatatype\ 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; diff -r 38457af660bc -r a9ad4a954cb7 src/Pure/Concurrent/par_exn.ML --- 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 diff -r 38457af660bc -r a9ad4a954cb7 src/Pure/ML/exn_properties.ML --- 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 = diff -r 38457af660bc -r a9ad4a954cb7 src/Pure/Thy/export_theory.ML --- 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 = diff -r 38457af660bc -r a9ad4a954cb7 src/Pure/Thy/export_theory.scala --- 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 diff -r 38457af660bc -r a9ad4a954cb7 src/Pure/Thy/thy_info.ML --- 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;