# HG changeset patch
# User Gerwin Klein <gerwin.klein@nicta.com.au>
# Date 1335788319 -36000
# Node ID bfc08ce7b7b949838cf5598c6ac9045dda4feac2
# Parent  179b5e7c980300f0d5710a14c2e05302678c46cc
provide [[record_codegen]] option for skipping codegen setup for records

diff -r 179b5e7c9803 -r bfc08ce7b7b9 NEWS
--- a/NEWS	Mon Apr 30 12:14:53 2012 +0200
+++ b/NEWS	Mon Apr 30 22:18:39 2012 +1000
@@ -180,6 +180,9 @@
 * Code generation by default implements sets as container type rather
 than predicates.  INCOMPATIBILITY.
 
+* Records: code generation can be switched off manually with 
+declare [[record_coden = false]]. Default remains true.
+
 * HOL-Import: Re-implementation from scratch is faster, simpler, and
 more scalable.  Requires a proof bundle, which is available as an
 external component.  Discontinued old (and mostly dead) Importer for
diff -r 179b5e7c9803 -r bfc08ce7b7b9 src/HOL/Tools/record.ML
--- a/src/HOL/Tools/record.ML	Mon Apr 30 12:14:53 2012 +0200
+++ b/src/HOL/Tools/record.ML	Mon Apr 30 22:18:39 2012 +1000
@@ -46,6 +46,7 @@
   val split_simp_tac: thm list -> (term -> int) -> int -> tactic
   val split_wrapper: string * (Proof.context -> wrapper)
 
+  val codegen: bool Config.T
   val updateN: string
   val ext_typeN: string
   val extN: string
@@ -209,6 +210,7 @@
 val updacc_cong_triv = @{thm update_accessor_cong_assist_triv};
 val updacc_cong_from_eq = @{thm iso_tuple_update_accessor_cong_from_eq};
 
+val codegen = Attrib.setup_config_bool @{binding record_codegen} (K true);
 
 
 (** name components **)
@@ -1732,43 +1734,45 @@
   end;
 
 fun add_code ext_tyco vs extT ext simps inject thy =
-  let
-    val eq =
-      HOLogic.mk_Trueprop (HOLogic.mk_eq
-        (Const (@{const_name HOL.equal}, extT --> extT --> HOLogic.boolT),
-         Const (@{const_name HOL.eq}, extT --> extT --> HOLogic.boolT)));
-    fun tac eq_def =
-      Class.intro_classes_tac []
-      THEN rewrite_goals_tac [Simpdata.mk_eq eq_def]
-      THEN ALLGOALS (rtac @{thm refl});
-    fun mk_eq thy eq_def =
-      Simplifier.rewrite_rule
-        [AxClass.unoverload thy (Thm.symmetric (Simpdata.mk_eq eq_def))] inject;
-    fun mk_eq_refl thy =
-      @{thm equal_refl}
-      |> Thm.instantiate
-        ([pairself (ctyp_of thy) (TVar (("'a", 0), @{sort equal}), Logic.varifyT_global extT)], [])
-      |> AxClass.unoverload thy;
-    val ensure_random_record = ensure_sort_record (@{sort random}, mk_random_eq);
-    val ensure_exhaustive_record =
-      ensure_sort_record (@{sort full_exhaustive}, mk_full_exhaustive_eq);
-  in
-    thy
-    |> Code.add_datatype [ext]
-    |> fold Code.add_default_eqn simps
-    |> Class.instantiation ([ext_tyco], vs, [HOLogic.class_equal])
-    |> `(fn lthy => Syntax.check_term lthy eq)
-    |-> (fn eq => Specification.definition
-          (NONE, (Attrib.empty_binding, eq)))
-    |-> (fn (_, (_, eq_def)) =>
-       Class.prove_instantiation_exit_result Morphism.thm
-          (fn _ => fn eq_def => tac eq_def) eq_def)
-    |-> (fn eq_def => fn thy =>
-          thy |> Code.del_eqn eq_def |> Code.add_default_eqn (mk_eq thy eq_def))
-    |> (fn thy => Code.add_nbe_default_eqn (mk_eq_refl thy) thy)
-    |> ensure_random_record ext_tyco vs (fst ext) (binder_types (snd ext))
-    |> ensure_exhaustive_record ext_tyco vs (fst ext) (binder_types (snd ext))
-  end;
+  if Config.get_global thy codegen then
+    let
+      val eq =
+        HOLogic.mk_Trueprop (HOLogic.mk_eq
+          (Const (@{const_name HOL.equal}, extT --> extT --> HOLogic.boolT),
+           Const (@{const_name HOL.eq}, extT --> extT --> HOLogic.boolT)));
+      fun tac eq_def =
+        Class.intro_classes_tac []
+        THEN rewrite_goals_tac [Simpdata.mk_eq eq_def]
+        THEN ALLGOALS (rtac @{thm refl});
+      fun mk_eq thy eq_def =
+        Simplifier.rewrite_rule
+          [AxClass.unoverload thy (Thm.symmetric (Simpdata.mk_eq eq_def))] inject;
+      fun mk_eq_refl thy =
+        @{thm equal_refl}
+        |> Thm.instantiate
+          ([pairself (ctyp_of thy) (TVar (("'a", 0), @{sort equal}), Logic.varifyT_global extT)], [])
+        |> AxClass.unoverload thy;
+      val ensure_random_record = ensure_sort_record (@{sort random}, mk_random_eq);
+      val ensure_exhaustive_record =
+        ensure_sort_record (@{sort full_exhaustive}, mk_full_exhaustive_eq);
+    in
+      thy
+      |> Code.add_datatype [ext]
+      |> fold Code.add_default_eqn simps
+      |> Class.instantiation ([ext_tyco], vs, [HOLogic.class_equal])
+      |> `(fn lthy => Syntax.check_term lthy eq)
+      |-> (fn eq => Specification.definition
+            (NONE, (Attrib.empty_binding, eq)))
+      |-> (fn (_, (_, eq_def)) =>
+         Class.prove_instantiation_exit_result Morphism.thm
+            (fn _ => fn eq_def => tac eq_def) eq_def)
+      |-> (fn eq_def => fn thy =>
+            thy |> Code.del_eqn eq_def |> Code.add_default_eqn (mk_eq thy eq_def))
+      |> (fn thy => Code.add_nbe_default_eqn (mk_eq_refl thy) thy)
+      |> ensure_random_record ext_tyco vs (fst ext) (binder_types (snd ext))
+      |> ensure_exhaustive_record ext_tyco vs (fst ext) (binder_types (snd ext))
+    end
+  else thy;
 
 
 (* definition *)
diff -r 179b5e7c9803 -r bfc08ce7b7b9 src/HOL/ex/Records.thy
--- a/src/HOL/ex/Records.thy	Mon Apr 30 12:14:53 2012 +0200
+++ b/src/HOL/ex/Records.thy	Mon Apr 30 22:18:39 2012 +1000
@@ -324,4 +324,16 @@
 
 export_code foo1 foo3 foo5 foo10 checking SML
 
+text {*
+  Code generation can also be switched off, for instance for very large records
+*}
+
+declare [[record_codegen = false]]
+
+record not_so_large_record =
+  bar520 :: nat
+  bar521 :: "nat * nat"
+
+declare [[record_codegen = true]]
+
 end