author | wenzelm |
Wed, 10 Apr 2013 15:30:19 +0200 | |
changeset 51685 | 385ef6706252 |
parent 51551 | 88d1d19fb74f |
child 51717 | 9e7d1c139569 |
permissions | -rw-r--r-- |
33968
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33964
diff
changeset
|
1 |
(* Title: HOL/Tools/Datatype/datatype_codegen.ML |
29265
5b4247055bd7
moved old add_term_vars, add_term_frees etc. to structure OldTerm;
wenzelm
parents:
28965
diff
changeset
|
2 |
Author: Stefan Berghofer and Florian Haftmann, TU Muenchen |
12445 | 3 |
|
25534
d0b74fdd6067
simplified infrastructure for code generator operational equality
haftmann
parents:
25505
diff
changeset
|
4 |
Code generator facilities for inductive datatypes. |
12445 | 5 |
*) |
6 |
||
7 |
signature DATATYPE_CODEGEN = |
|
8 |
sig |
|
18708 | 9 |
val setup: theory -> theory |
12445 | 10 |
end; |
11 |
||
33968
f94fb13ecbb3
modernized structures and tuned headers of datatype package modules; joined former datatype.ML and datatype_rep_proofs.ML
haftmann
parents:
33964
diff
changeset
|
12 |
structure Datatype_Codegen : DATATYPE_CODEGEN = |
12445 | 13 |
struct |
14 |
||
36298
2d55c4aba1dc
swapped generic code generator and SML code generator
haftmann
parents:
35899
diff
changeset
|
15 |
(** generic code generator **) |
2d55c4aba1dc
swapped generic code generator and SML code generator
haftmann
parents:
35899
diff
changeset
|
16 |
|
2d55c4aba1dc
swapped generic code generator and SML code generator
haftmann
parents:
35899
diff
changeset
|
17 |
(* liberal addition of code data for datatypes *) |
2d55c4aba1dc
swapped generic code generator and SML code generator
haftmann
parents:
35899
diff
changeset
|
18 |
|
38538
c87b69396a37
liberal instantiation of class eq; tuned naming scheme
haftmann
parents:
38348
diff
changeset
|
19 |
fun mk_constr_consts thy vs tyco cos = |
36298
2d55c4aba1dc
swapped generic code generator and SML code generator
haftmann
parents:
35899
diff
changeset
|
20 |
let |
38538
c87b69396a37
liberal instantiation of class eq; tuned naming scheme
haftmann
parents:
38348
diff
changeset
|
21 |
val cs = map (fn (c, tys) => (c, tys ---> Type (tyco, map TFree vs))) cos; |
51685
385ef6706252
more standard module name Axclass (according to file name);
wenzelm
parents:
51551
diff
changeset
|
22 |
val cs' = map (fn c_ty as (_, ty) => (Axclass.unoverload_const thy c_ty, ty)) cs; |
45700 | 23 |
in |
24 |
if is_some (try (Code.constrset_of_consts thy) cs') |
|
36298
2d55c4aba1dc
swapped generic code generator and SML code generator
haftmann
parents:
35899
diff
changeset
|
25 |
then SOME cs |
2d55c4aba1dc
swapped generic code generator and SML code generator
haftmann
parents:
35899
diff
changeset
|
26 |
else NONE |
2d55c4aba1dc
swapped generic code generator and SML code generator
haftmann
parents:
35899
diff
changeset
|
27 |
end; |
2d55c4aba1dc
swapped generic code generator and SML code generator
haftmann
parents:
35899
diff
changeset
|
28 |
|
2d55c4aba1dc
swapped generic code generator and SML code generator
haftmann
parents:
35899
diff
changeset
|
29 |
|
2d55c4aba1dc
swapped generic code generator and SML code generator
haftmann
parents:
35899
diff
changeset
|
30 |
(* case certificates *) |
2d55c4aba1dc
swapped generic code generator and SML code generator
haftmann
parents:
35899
diff
changeset
|
31 |
|
2d55c4aba1dc
swapped generic code generator and SML code generator
haftmann
parents:
35899
diff
changeset
|
32 |
fun mk_case_cert thy tyco = |
2d55c4aba1dc
swapped generic code generator and SML code generator
haftmann
parents:
35899
diff
changeset
|
33 |
let |
45700 | 34 |
val raw_thms = #case_rewrites (Datatype_Data.the_info thy tyco); |
36298
2d55c4aba1dc
swapped generic code generator and SML code generator
haftmann
parents:
35899
diff
changeset
|
35 |
val thms as hd_thm :: _ = raw_thms |
2d55c4aba1dc
swapped generic code generator and SML code generator
haftmann
parents:
35899
diff
changeset
|
36 |
|> Conjunction.intr_balanced |
2d55c4aba1dc
swapped generic code generator and SML code generator
haftmann
parents:
35899
diff
changeset
|
37 |
|> Thm.unvarify_global |
2d55c4aba1dc
swapped generic code generator and SML code generator
haftmann
parents:
35899
diff
changeset
|
38 |
|> Conjunction.elim_balanced (length raw_thms) |
2d55c4aba1dc
swapped generic code generator and SML code generator
haftmann
parents:
35899
diff
changeset
|
39 |
|> map Simpdata.mk_meta_eq |
45700 | 40 |
|> map Drule.zero_var_indexes; |
41 |
val params = fold_aterms (fn (Free (v, _)) => insert (op =) v | _ => I) (Thm.prop_of hd_thm) []; |
|
36298
2d55c4aba1dc
swapped generic code generator and SML code generator
haftmann
parents:
35899
diff
changeset
|
42 |
val rhs = hd_thm |
2d55c4aba1dc
swapped generic code generator and SML code generator
haftmann
parents:
35899
diff
changeset
|
43 |
|> Thm.prop_of |
2d55c4aba1dc
swapped generic code generator and SML code generator
haftmann
parents:
35899
diff
changeset
|
44 |
|> Logic.dest_equals |
2d55c4aba1dc
swapped generic code generator and SML code generator
haftmann
parents:
35899
diff
changeset
|
45 |
|> fst |
2d55c4aba1dc
swapped generic code generator and SML code generator
haftmann
parents:
35899
diff
changeset
|
46 |
|> Term.strip_comb |
2d55c4aba1dc
swapped generic code generator and SML code generator
haftmann
parents:
35899
diff
changeset
|
47 |
|> apsnd (fst o split_last) |
2d55c4aba1dc
swapped generic code generator and SML code generator
haftmann
parents:
35899
diff
changeset
|
48 |
|> list_comb; |
43324
2b47822868e4
discontinued Name.variant to emphasize that this is old-style / indirect;
wenzelm
parents:
42411
diff
changeset
|
49 |
val lhs = Free (singleton (Name.variant_list params) "case", Term.fastype_of rhs); |
45700 | 50 |
val asm = Thm.cterm_of thy (Logic.mk_equals (lhs, rhs)); |
36298
2d55c4aba1dc
swapped generic code generator and SML code generator
haftmann
parents:
35899
diff
changeset
|
51 |
in |
2d55c4aba1dc
swapped generic code generator and SML code generator
haftmann
parents:
35899
diff
changeset
|
52 |
thms |
2d55c4aba1dc
swapped generic code generator and SML code generator
haftmann
parents:
35899
diff
changeset
|
53 |
|> Conjunction.intr_balanced |
45700 | 54 |
|> Raw_Simplifier.rewrite_rule [Thm.symmetric (Thm.assume asm)] |
36298
2d55c4aba1dc
swapped generic code generator and SML code generator
haftmann
parents:
35899
diff
changeset
|
55 |
|> Thm.implies_intr asm |
2d55c4aba1dc
swapped generic code generator and SML code generator
haftmann
parents:
35899
diff
changeset
|
56 |
|> Thm.generalize ([], params) 0 |
51685
385ef6706252
more standard module name Axclass (according to file name);
wenzelm
parents:
51551
diff
changeset
|
57 |
|> Axclass.unoverload thy |
36298
2d55c4aba1dc
swapped generic code generator and SML code generator
haftmann
parents:
35899
diff
changeset
|
58 |
|> Thm.varifyT_global |
2d55c4aba1dc
swapped generic code generator and SML code generator
haftmann
parents:
35899
diff
changeset
|
59 |
end; |
2d55c4aba1dc
swapped generic code generator and SML code generator
haftmann
parents:
35899
diff
changeset
|
60 |
|
2d55c4aba1dc
swapped generic code generator and SML code generator
haftmann
parents:
35899
diff
changeset
|
61 |
|
2d55c4aba1dc
swapped generic code generator and SML code generator
haftmann
parents:
35899
diff
changeset
|
62 |
(* equality *) |
2d55c4aba1dc
swapped generic code generator and SML code generator
haftmann
parents:
35899
diff
changeset
|
63 |
|
38538
c87b69396a37
liberal instantiation of class eq; tuned naming scheme
haftmann
parents:
38348
diff
changeset
|
64 |
fun mk_eq_eqns thy tyco = |
36298
2d55c4aba1dc
swapped generic code generator and SML code generator
haftmann
parents:
35899
diff
changeset
|
65 |
let |
38538
c87b69396a37
liberal instantiation of class eq; tuned naming scheme
haftmann
parents:
38348
diff
changeset
|
66 |
val (vs, cos) = Datatype_Data.the_spec thy tyco; |
45700 | 67 |
val {descr, index, inject = inject_thms, distinct = distinct_thms, ...} = |
38538
c87b69396a37
liberal instantiation of class eq; tuned naming scheme
haftmann
parents:
38348
diff
changeset
|
68 |
Datatype_Data.the_info thy tyco; |
c87b69396a37
liberal instantiation of class eq; tuned naming scheme
haftmann
parents:
38348
diff
changeset
|
69 |
val ty = Type (tyco, map TFree vs); |
45700 | 70 |
fun mk_eq (t1, t2) = Const (@{const_name HOL.equal}, ty --> ty --> HOLogic.boolT) $ t1 $ t2; |
45740 | 71 |
fun true_eq t12 = HOLogic.mk_eq (mk_eq t12, @{term True}); |
72 |
fun false_eq t12 = HOLogic.mk_eq (mk_eq t12, @{term False}); |
|
45700 | 73 |
val triv_injects = |
74 |
map_filter |
|
75 |
(fn (c, []) => SOME (HOLogic.mk_Trueprop (true_eq (Const (c, ty), Const (c, ty)))) |
|
76 |
| _ => NONE) cos; |
|
36298
2d55c4aba1dc
swapped generic code generator and SML code generator
haftmann
parents:
35899
diff
changeset
|
77 |
fun prep_inject (trueprop $ (equiv $ (_ $ t1 $ t2) $ rhs)) = |
2d55c4aba1dc
swapped generic code generator and SML code generator
haftmann
parents:
35899
diff
changeset
|
78 |
trueprop $ (equiv $ mk_eq (t1, t2) $ rhs); |
45822 | 79 |
val injects = map prep_inject (nth (Datatype_Prop.make_injs [descr]) index); |
36298
2d55c4aba1dc
swapped generic code generator and SML code generator
haftmann
parents:
35899
diff
changeset
|
80 |
fun prep_distinct (trueprop $ (not $ (_ $ t1 $ t2))) = |
2d55c4aba1dc
swapped generic code generator and SML code generator
haftmann
parents:
35899
diff
changeset
|
81 |
[trueprop $ false_eq (t1, t2), trueprop $ false_eq (t2, t1)]; |
45889 | 82 |
val distincts = maps prep_distinct (nth (Datatype_Prop.make_distincts [descr]) index); |
36298
2d55c4aba1dc
swapped generic code generator and SML code generator
haftmann
parents:
35899
diff
changeset
|
83 |
val refl = HOLogic.mk_Trueprop (true_eq (Free ("x", ty), Free ("x", ty))); |
45700 | 84 |
val simpset = |
85 |
Simplifier.global_context thy |
|
86 |
(HOL_basic_ss addsimps |
|
87 |
(map Simpdata.mk_eq (@{thms equal eq_True} @ inject_thms @ distinct_thms))); |
|
88 |
fun prove prop = |
|
51551 | 89 |
Goal.prove_sorry_global thy [] [] prop (K (ALLGOALS (simp_tac simpset))) |
36298
2d55c4aba1dc
swapped generic code generator and SML code generator
haftmann
parents:
35899
diff
changeset
|
90 |
|> Simpdata.mk_eq; |
2d55c4aba1dc
swapped generic code generator and SML code generator
haftmann
parents:
35899
diff
changeset
|
91 |
in (map prove (triv_injects @ injects @ distincts), prove refl) end; |
2d55c4aba1dc
swapped generic code generator and SML code generator
haftmann
parents:
35899
diff
changeset
|
92 |
|
38538
c87b69396a37
liberal instantiation of class eq; tuned naming scheme
haftmann
parents:
38348
diff
changeset
|
93 |
fun add_equality vs tycos thy = |
36298
2d55c4aba1dc
swapped generic code generator and SML code generator
haftmann
parents:
35899
diff
changeset
|
94 |
let |
38538
c87b69396a37
liberal instantiation of class eq; tuned naming scheme
haftmann
parents:
38348
diff
changeset
|
95 |
fun add_def tyco lthy = |
36298
2d55c4aba1dc
swapped generic code generator and SML code generator
haftmann
parents:
35899
diff
changeset
|
96 |
let |
38538
c87b69396a37
liberal instantiation of class eq; tuned naming scheme
haftmann
parents:
38348
diff
changeset
|
97 |
val ty = Type (tyco, map TFree vs); |
45700 | 98 |
fun mk_side const_name = |
99 |
Const (const_name, ty --> ty --> HOLogic.boolT) $ Free ("x", ty) $ Free ("y", ty); |
|
100 |
val def = |
|
101 |
HOLogic.mk_Trueprop (HOLogic.mk_eq |
|
102 |
(mk_side @{const_name HOL.equal}, mk_side @{const_name HOL.eq})); |
|
36298
2d55c4aba1dc
swapped generic code generator and SML code generator
haftmann
parents:
35899
diff
changeset
|
103 |
val def' = Syntax.check_term lthy def; |
45700 | 104 |
val ((_, (_, thm)), lthy') = |
105 |
Specification.definition (NONE, (Attrib.empty_binding, def')) lthy; |
|
42361 | 106 |
val ctxt_thy = Proof_Context.init_global (Proof_Context.theory_of lthy); |
107 |
val thm' = singleton (Proof_Context.export lthy' ctxt_thy) thm; |
|
36298
2d55c4aba1dc
swapped generic code generator and SML code generator
haftmann
parents:
35899
diff
changeset
|
108 |
in (thm', lthy') end; |
45700 | 109 |
fun tac thms = Class.intro_classes_tac [] THEN ALLGOALS (Proof_Context.fact_tac thms); |
110 |
fun prefix tyco = |
|
111 |
Binding.qualify true (Long_Name.base_name tyco) o Binding.qualify true "eq" o Binding.name; |
|
38538
c87b69396a37
liberal instantiation of class eq; tuned naming scheme
haftmann
parents:
38348
diff
changeset
|
112 |
fun add_eq_thms tyco = |
36298
2d55c4aba1dc
swapped generic code generator and SML code generator
haftmann
parents:
35899
diff
changeset
|
113 |
Theory.checkpoint |
38538
c87b69396a37
liberal instantiation of class eq; tuned naming scheme
haftmann
parents:
38348
diff
changeset
|
114 |
#> `(fn thy => mk_eq_eqns thy tyco) |
45700 | 115 |
#-> (fn (thms, thm) => |
116 |
Global_Theory.note_thmss Thm.lemmaK |
|
38538
c87b69396a37
liberal instantiation of class eq; tuned naming scheme
haftmann
parents:
38348
diff
changeset
|
117 |
[((prefix tyco "refl", [Code.add_nbe_default_eqn_attribute]), [([thm], [])]), |
c87b69396a37
liberal instantiation of class eq; tuned naming scheme
haftmann
parents:
38348
diff
changeset
|
118 |
((prefix tyco "simps", [Code.add_default_eqn_attribute]), [(rev thms, [])])]) |
45700 | 119 |
#> snd; |
36298
2d55c4aba1dc
swapped generic code generator and SML code generator
haftmann
parents:
35899
diff
changeset
|
120 |
in |
2d55c4aba1dc
swapped generic code generator and SML code generator
haftmann
parents:
35899
diff
changeset
|
121 |
thy |
38857
97775f3e8722
renamed class/constant eq to equal; tuned some instantiations
haftmann
parents:
38538
diff
changeset
|
122 |
|> Class.instantiation (tycos, vs, [HOLogic.class_equal]) |
38538
c87b69396a37
liberal instantiation of class eq; tuned naming scheme
haftmann
parents:
38348
diff
changeset
|
123 |
|> fold_map add_def tycos |
36298
2d55c4aba1dc
swapped generic code generator and SML code generator
haftmann
parents:
35899
diff
changeset
|
124 |
|-> (fn def_thms => Class.prove_instantiation_exit_result (map o Morphism.thm) |
2d55c4aba1dc
swapped generic code generator and SML code generator
haftmann
parents:
35899
diff
changeset
|
125 |
(fn _ => fn def_thms => tac def_thms) def_thms) |
2d55c4aba1dc
swapped generic code generator and SML code generator
haftmann
parents:
35899
diff
changeset
|
126 |
|-> (fn def_thms => fold Code.del_eqn def_thms) |
38538
c87b69396a37
liberal instantiation of class eq; tuned naming scheme
haftmann
parents:
38348
diff
changeset
|
127 |
|> fold add_eq_thms tycos |
36298
2d55c4aba1dc
swapped generic code generator and SML code generator
haftmann
parents:
35899
diff
changeset
|
128 |
end; |
2d55c4aba1dc
swapped generic code generator and SML code generator
haftmann
parents:
35899
diff
changeset
|
129 |
|
2d55c4aba1dc
swapped generic code generator and SML code generator
haftmann
parents:
35899
diff
changeset
|
130 |
|
2d55c4aba1dc
swapped generic code generator and SML code generator
haftmann
parents:
35899
diff
changeset
|
131 |
(* register a datatype etc. *) |
2d55c4aba1dc
swapped generic code generator and SML code generator
haftmann
parents:
35899
diff
changeset
|
132 |
|
38538
c87b69396a37
liberal instantiation of class eq; tuned naming scheme
haftmann
parents:
38348
diff
changeset
|
133 |
fun add_all_code config tycos thy = |
36298
2d55c4aba1dc
swapped generic code generator and SML code generator
haftmann
parents:
35899
diff
changeset
|
134 |
let |
45700 | 135 |
val (vs :: _, coss) = split_list (map (Datatype_Data.the_spec thy) tycos); |
38538
c87b69396a37
liberal instantiation of class eq; tuned naming scheme
haftmann
parents:
38348
diff
changeset
|
136 |
val any_css = map2 (mk_constr_consts thy vs) tycos coss; |
45700 | 137 |
val css = if exists is_none any_css then [] else map_filter I any_css; |
38538
c87b69396a37
liberal instantiation of class eq; tuned naming scheme
haftmann
parents:
38348
diff
changeset
|
138 |
val case_rewrites = maps (#case_rewrites o Datatype_Data.the_info thy) tycos; |
c87b69396a37
liberal instantiation of class eq; tuned naming scheme
haftmann
parents:
38348
diff
changeset
|
139 |
val certs = map (mk_case_cert thy) tycos; |
45700 | 140 |
val tycos_eq = |
141 |
filter_out |
|
48272 | 142 |
(fn tyco => Sorts.has_instance (Sign.classes_of thy) tyco [HOLogic.class_equal]) tycos; |
36298
2d55c4aba1dc
swapped generic code generator and SML code generator
haftmann
parents:
35899
diff
changeset
|
143 |
in |
2d55c4aba1dc
swapped generic code generator and SML code generator
haftmann
parents:
35899
diff
changeset
|
144 |
if null css then thy |
45700 | 145 |
else |
146 |
thy |
|
36298
2d55c4aba1dc
swapped generic code generator and SML code generator
haftmann
parents:
35899
diff
changeset
|
147 |
|> tap (fn _ => Datatype_Aux.message config "Registering datatype for code generator ...") |
2d55c4aba1dc
swapped generic code generator and SML code generator
haftmann
parents:
35899
diff
changeset
|
148 |
|> fold Code.add_datatype css |
2d55c4aba1dc
swapped generic code generator and SML code generator
haftmann
parents:
35899
diff
changeset
|
149 |
|> fold_rev Code.add_default_eqn case_rewrites |
2d55c4aba1dc
swapped generic code generator and SML code generator
haftmann
parents:
35899
diff
changeset
|
150 |
|> fold Code.add_case certs |
38538
c87b69396a37
liberal instantiation of class eq; tuned naming scheme
haftmann
parents:
38348
diff
changeset
|
151 |
|> not (null tycos_eq) ? add_equality vs tycos_eq |
36298
2d55c4aba1dc
swapped generic code generator and SML code generator
haftmann
parents:
35899
diff
changeset
|
152 |
end; |
2d55c4aba1dc
swapped generic code generator and SML code generator
haftmann
parents:
35899
diff
changeset
|
153 |
|
2d55c4aba1dc
swapped generic code generator and SML code generator
haftmann
parents:
35899
diff
changeset
|
154 |
|
20426 | 155 |
(** theory setup **) |
156 |
||
45173 | 157 |
val setup = Datatype_Data.interpretation add_all_code; |
20597 | 158 |
|
12445 | 159 |
end; |