# HG changeset patch # User haftmann # Date 1501757402 -7200 # Node ID dcb3e6bdc00a4fdea1063116df73546a98bfc6a5 # Parent a0369be639486f03c299de21bb491219a36c1ab4 one single plugin for code type declarations avoids problems when bootstrapping new plugins over types which have been both declared concrete and abstract in their code historiy diff -r a0369be63948 -r dcb3e6bdc00a src/HOL/Tools/code_evaluation.ML --- a/src/HOL/Tools/code_evaluation.ML Thu Aug 03 12:50:01 2017 +0200 +++ b/src/HOL/Tools/code_evaluation.ML Thu Aug 03 12:50:02 2017 +0200 @@ -20,8 +20,9 @@ (* formal definition *) -fun add_term_of tyco raw_vs thy = +fun add_term_of_inst tyco thy = let + val ((raw_vs, _), _) = Code.get_type thy tyco; val vs = map (fn (v, _) => (v, @{sort typerep})) raw_vs; val ty = Type (tyco, map TFree vs); val lhs = Const (@{const_name term_of}, ty --> @{typ term}) @@ -39,11 +40,11 @@ |> Class.prove_instantiation_exit (fn ctxt => Class.intro_classes_tac ctxt []) end; -fun ensure_term_of (tyco, (vs, _)) thy = +fun ensure_term_of_inst tyco thy = let val need_inst = not (Sorts.has_instance (Sign.classes_of thy) tyco @{sort term_of}) andalso Sorts.has_instance (Sign.classes_of thy) tyco @{sort typerep}; - in if need_inst then add_term_of tyco vs thy else thy end; + in if need_inst then add_term_of_inst tyco thy else thy end; fun for_term_of_instance tyco vs f thy = let @@ -74,20 +75,19 @@ |> Thm.varifyT_global end; -fun add_term_of_code tyco vs raw_cs thy = +fun add_term_of_code_datatype tyco vs raw_cs thy = let val ty = Type (tyco, map TFree vs); val cs = (map o apsnd o apsnd o map o map_atyps) (fn TFree (v, _) => TFree (v, (the o AList.lookup (op =) vs) v)) raw_cs; - val const = Axclass.param_of_inst thy (@{const_name term_of}, tyco); val eqs = map (mk_term_of_eq thy ty) cs; in thy |> Code.declare_default_eqns_global (map (rpair true) eqs) end; -fun ensure_term_of_code (tyco, (vs, cs)) = - for_term_of_instance tyco vs (fn tyco => fn vs => add_term_of_code tyco vs cs); +fun ensure_term_of_code_datatype (tyco, (vs, cs)) = + for_term_of_instance tyco vs (fn tyco => fn vs => add_term_of_code_datatype tyco vs cs); (* code equations for abstypes *) @@ -105,31 +105,29 @@ |> Thm.varifyT_global end; -fun add_abs_term_of_code tyco vs abs raw_ty_rep proj thy = +fun add_term_of_code_abstype tyco vs abs raw_ty_rep projection thy = let val ty = Type (tyco, map TFree vs); val ty_rep = map_atyps (fn TFree (v, _) => TFree (v, (the o AList.lookup (op =) vs) v)) raw_ty_rep; - val const = Axclass.param_of_inst thy (@{const_name term_of}, tyco); - val eq = mk_abs_term_of_eq thy ty abs ty_rep proj; + val eq = mk_abs_term_of_eq thy ty abs ty_rep projection; in thy |> Code.declare_default_eqns_global [(eq, true)] end; -fun ensure_abs_term_of_code (tyco, (vs, {abstractor = (abs, (_, ty)), +fun ensure_term_of_code_abstype (tyco, (vs, {abstractor = (abs, (_, ty)), projection, ...})) = for_term_of_instance tyco vs - (fn tyco => fn vs => add_abs_term_of_code tyco vs abs ty projection); + (fn tyco => fn vs => add_term_of_code_abstype tyco vs abs ty projection); (* setup *) val _ = Theory.setup - (Code.datatype_interpretation ensure_term_of - #> Code.abstype_interpretation ensure_term_of - #> Code.datatype_interpretation ensure_term_of_code - #> Code.abstype_interpretation ensure_abs_term_of_code); + (Code.type_interpretation ensure_term_of_inst + #> Code.datatype_interpretation ensure_term_of_code_datatype + #> Code.abstype_interpretation ensure_term_of_code_abstype); (** termifying syntax **) diff -r a0369be63948 -r dcb3e6bdc00a src/HOL/Typerep.thy --- a/src/HOL/Typerep.thy Thu Aug 03 12:50:01 2017 +0200 +++ b/src/HOL/Typerep.thy Thu Aug 03 12:50:02 2017 +0200 @@ -72,8 +72,7 @@ add_typerep @{type_name fun} #> Typedef.interpretation (Local_Theory.background_theory o ensure_typerep) -#> Code.datatype_interpretation (ensure_typerep o fst) -#> Code.abstype_interpretation (ensure_typerep o fst) +#> Code.type_interpretation ensure_typerep end \ diff -r a0369be63948 -r dcb3e6bdc00a src/Pure/Isar/code.ML --- a/src/Pure/Isar/code.ML Thu Aug 03 12:50:01 2017 +0200 +++ b/src/Pure/Isar/code.ML Thu Aug 03 12:50:02 2017 +0200 @@ -31,13 +31,14 @@ (*executable code*) type constructors + type abs_type + val type_interpretation: (string -> theory -> theory) -> theory -> theory + val datatype_interpretation: (string * constructors -> theory -> theory) -> theory -> theory + val abstype_interpretation: (string * abs_type -> theory -> theory) -> theory -> theory val declare_datatype_global: (string * typ) list -> theory -> theory val declare_datatype_cmd: string list -> theory -> theory - val datatype_interpretation: (string * constructors -> theory -> theory) -> theory -> theory - type abs_type val declare_abstype: thm -> local_theory -> local_theory val declare_abstype_global: thm -> theory -> theory - val abstype_interpretation: (string * abs_type -> theory -> theory) -> theory -> theory val declare_default_eqns: (thm * bool) list -> local_theory -> local_theory val declare_default_eqns_global: (thm * bool) list -> theory -> theory val declare_eqns: (thm * bool) list -> local_theory -> local_theory @@ -1259,6 +1260,40 @@ (** declaration of executable ingredients **) +(* plugins for dependent applications *) + +structure Codetype_Plugin = Plugin(type T = string); + +val codetype_plugin = Plugin_Name.declare_setup @{binding codetype}; + +fun type_interpretation f = + Codetype_Plugin.interpretation codetype_plugin + (fn tyco => Local_Theory.background_theory + (fn thy => + thy + |> Sign.root_path + |> Sign.add_path (Long_Name.qualifier tyco) + |> f tyco + |> Sign.restore_naming thy)); + +fun datatype_interpretation f = + type_interpretation (fn tyco => fn thy => + case get_type thy tyco of + (spec, false) => f (tyco, spec) thy + | (_, true) => thy + ); + +fun abstype_interpretation f = + type_interpretation (fn tyco => fn thy => + case try (get_abstype_spec thy) tyco of + SOME spec => f (tyco, spec) thy + | NONE => thy + ); + +fun register_tyco_for_plugin tyco = + Named_Target.theory_map (Codetype_Plugin.data_default tyco); + + (* abstract code declarations *) local @@ -1298,22 +1333,6 @@ |> map_types (History.register tyco vs_typ_spec) end; -fun type_interpretation get_spec tyco f = - Local_Theory.background_theory (fn thy => - thy - |> Sign.root_path - |> Sign.add_path (Long_Name.qualifier tyco) - |> f (tyco, get_spec thy tyco) - |> Sign.restore_naming thy); - -structure Datatype_Plugin = Plugin(type T = string); - -val datatype_plugin = Plugin_Name.declare_setup @{binding datatype_code}; - -fun datatype_interpretation f = - Datatype_Plugin.interpretation datatype_plugin - (fn tyco => type_interpretation (fst oo get_type) tyco f); - fun declare_datatype_global proto_constrs thy = let fun unoverload_const_typ (c, ty) = @@ -1324,20 +1343,12 @@ thy |> modify_specs (register_type (tyco, (vs, Constructors {constructors = cos, case_combinators = []}))) - |> Named_Target.theory_map (Datatype_Plugin.data_default tyco) + |> register_tyco_for_plugin tyco end; fun declare_datatype_cmd raw_constrs thy = declare_datatype_global (map (read_bare_const thy) raw_constrs) thy; -structure Abstype_Plugin = Plugin(type T = string); - -val abstype_plugin = Plugin_Name.declare_setup @{binding abstype_code}; - -fun abstype_interpretation f = - Abstype_Plugin.interpretation abstype_plugin - (fn tyco => type_interpretation get_abstype_spec tyco f); - fun generic_declare_abstype strictness proto_thm thy = case check_abstype_cert strictness thy proto_thm of SOME (tyco, (vs, (abstractor as (abs, (_, ty)), (proj, abs_rep)))) => @@ -1346,7 +1357,7 @@ (tyco, (vs, Abstractor {abstractor = abstractor, projection = proj, abs_rep = abs_rep, more_abstract_functions = []})) #> register_fun_spec proj (Proj (Logic.varify_types_global (mk_proj tyco vs ty abs proj), (tyco, abs)))) - |> Named_Target.theory_map (Abstype_Plugin.data_default tyco) + |> register_tyco_for_plugin tyco | NONE => thy; val declare_abstype_global = generic_declare_abstype Strict;