# 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
 \<close>
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;