1.1 --- a/NEWS Mon Apr 30 12:14:53 2012 +0200
1.2 +++ b/NEWS Mon Apr 30 22:18:39 2012 +1000
1.3 @@ -180,6 +180,9 @@
1.4 * Code generation by default implements sets as container type rather
1.5 than predicates. INCOMPATIBILITY.
1.6
1.7 +* Records: code generation can be switched off manually with
1.8 +declare [[record_coden = false]]. Default remains true.
1.9 +
1.10 * HOL-Import: Re-implementation from scratch is faster, simpler, and
1.11 more scalable. Requires a proof bundle, which is available as an
1.12 external component. Discontinued old (and mostly dead) Importer for
2.1 --- a/src/HOL/Tools/record.ML Mon Apr 30 12:14:53 2012 +0200
2.2 +++ b/src/HOL/Tools/record.ML Mon Apr 30 22:18:39 2012 +1000
2.3 @@ -46,6 +46,7 @@
2.4 val split_simp_tac: thm list -> (term -> int) -> int -> tactic
2.5 val split_wrapper: string * (Proof.context -> wrapper)
2.6
2.7 + val codegen: bool Config.T
2.8 val updateN: string
2.9 val ext_typeN: string
2.10 val extN: string
2.11 @@ -209,6 +210,7 @@
2.12 val updacc_cong_triv = @{thm update_accessor_cong_assist_triv};
2.13 val updacc_cong_from_eq = @{thm iso_tuple_update_accessor_cong_from_eq};
2.14
2.15 +val codegen = Attrib.setup_config_bool @{binding record_codegen} (K true);
2.16
2.17
2.18 (** name components **)
2.19 @@ -1732,43 +1734,45 @@
2.20 end;
2.21
2.22 fun add_code ext_tyco vs extT ext simps inject thy =
2.23 - let
2.24 - val eq =
2.25 - HOLogic.mk_Trueprop (HOLogic.mk_eq
2.26 - (Const (@{const_name HOL.equal}, extT --> extT --> HOLogic.boolT),
2.27 - Const (@{const_name HOL.eq}, extT --> extT --> HOLogic.boolT)));
2.28 - fun tac eq_def =
2.29 - Class.intro_classes_tac []
2.30 - THEN rewrite_goals_tac [Simpdata.mk_eq eq_def]
2.31 - THEN ALLGOALS (rtac @{thm refl});
2.32 - fun mk_eq thy eq_def =
2.33 - Simplifier.rewrite_rule
2.34 - [AxClass.unoverload thy (Thm.symmetric (Simpdata.mk_eq eq_def))] inject;
2.35 - fun mk_eq_refl thy =
2.36 - @{thm equal_refl}
2.37 - |> Thm.instantiate
2.38 - ([pairself (ctyp_of thy) (TVar (("'a", 0), @{sort equal}), Logic.varifyT_global extT)], [])
2.39 - |> AxClass.unoverload thy;
2.40 - val ensure_random_record = ensure_sort_record (@{sort random}, mk_random_eq);
2.41 - val ensure_exhaustive_record =
2.42 - ensure_sort_record (@{sort full_exhaustive}, mk_full_exhaustive_eq);
2.43 - in
2.44 - thy
2.45 - |> Code.add_datatype [ext]
2.46 - |> fold Code.add_default_eqn simps
2.47 - |> Class.instantiation ([ext_tyco], vs, [HOLogic.class_equal])
2.48 - |> `(fn lthy => Syntax.check_term lthy eq)
2.49 - |-> (fn eq => Specification.definition
2.50 - (NONE, (Attrib.empty_binding, eq)))
2.51 - |-> (fn (_, (_, eq_def)) =>
2.52 - Class.prove_instantiation_exit_result Morphism.thm
2.53 - (fn _ => fn eq_def => tac eq_def) eq_def)
2.54 - |-> (fn eq_def => fn thy =>
2.55 - thy |> Code.del_eqn eq_def |> Code.add_default_eqn (mk_eq thy eq_def))
2.56 - |> (fn thy => Code.add_nbe_default_eqn (mk_eq_refl thy) thy)
2.57 - |> ensure_random_record ext_tyco vs (fst ext) (binder_types (snd ext))
2.58 - |> ensure_exhaustive_record ext_tyco vs (fst ext) (binder_types (snd ext))
2.59 - end;
2.60 + if Config.get_global thy codegen then
2.61 + let
2.62 + val eq =
2.63 + HOLogic.mk_Trueprop (HOLogic.mk_eq
2.64 + (Const (@{const_name HOL.equal}, extT --> extT --> HOLogic.boolT),
2.65 + Const (@{const_name HOL.eq}, extT --> extT --> HOLogic.boolT)));
2.66 + fun tac eq_def =
2.67 + Class.intro_classes_tac []
2.68 + THEN rewrite_goals_tac [Simpdata.mk_eq eq_def]
2.69 + THEN ALLGOALS (rtac @{thm refl});
2.70 + fun mk_eq thy eq_def =
2.71 + Simplifier.rewrite_rule
2.72 + [AxClass.unoverload thy (Thm.symmetric (Simpdata.mk_eq eq_def))] inject;
2.73 + fun mk_eq_refl thy =
2.74 + @{thm equal_refl}
2.75 + |> Thm.instantiate
2.76 + ([pairself (ctyp_of thy) (TVar (("'a", 0), @{sort equal}), Logic.varifyT_global extT)], [])
2.77 + |> AxClass.unoverload thy;
2.78 + val ensure_random_record = ensure_sort_record (@{sort random}, mk_random_eq);
2.79 + val ensure_exhaustive_record =
2.80 + ensure_sort_record (@{sort full_exhaustive}, mk_full_exhaustive_eq);
2.81 + in
2.82 + thy
2.83 + |> Code.add_datatype [ext]
2.84 + |> fold Code.add_default_eqn simps
2.85 + |> Class.instantiation ([ext_tyco], vs, [HOLogic.class_equal])
2.86 + |> `(fn lthy => Syntax.check_term lthy eq)
2.87 + |-> (fn eq => Specification.definition
2.88 + (NONE, (Attrib.empty_binding, eq)))
2.89 + |-> (fn (_, (_, eq_def)) =>
2.90 + Class.prove_instantiation_exit_result Morphism.thm
2.91 + (fn _ => fn eq_def => tac eq_def) eq_def)
2.92 + |-> (fn eq_def => fn thy =>
2.93 + thy |> Code.del_eqn eq_def |> Code.add_default_eqn (mk_eq thy eq_def))
2.94 + |> (fn thy => Code.add_nbe_default_eqn (mk_eq_refl thy) thy)
2.95 + |> ensure_random_record ext_tyco vs (fst ext) (binder_types (snd ext))
2.96 + |> ensure_exhaustive_record ext_tyco vs (fst ext) (binder_types (snd ext))
2.97 + end
2.98 + else thy;
2.99
2.100
2.101 (* definition *)
3.1 --- a/src/HOL/ex/Records.thy Mon Apr 30 12:14:53 2012 +0200
3.2 +++ b/src/HOL/ex/Records.thy Mon Apr 30 22:18:39 2012 +1000
3.3 @@ -324,4 +324,16 @@
3.4
3.5 export_code foo1 foo3 foo5 foo10 checking SML
3.6
3.7 +text {*
3.8 + Code generation can also be switched off, for instance for very large records
3.9 +*}
3.10 +
3.11 +declare [[record_codegen = false]]
3.12 +
3.13 +record not_so_large_record =
3.14 + bar520 :: nat
3.15 + bar521 :: "nat * nat"
3.16 +
3.17 +declare [[record_codegen = true]]
3.18 +
3.19 end