37 end; |
37 end; |
38 *} |
38 *} |
39 |
39 |
40 setup {* |
40 setup {* |
41 let |
41 let |
42 fun mk thy arities _ = |
42 fun mk arities _ thy = |
43 maps (fn ((tyco, asorts), _) => [(("", []), TypOf.mk_typ_of_def |
43 (maps (fn ((tyco, asorts), _) => [(("", []), TypOf.mk_typ_of_def |
44 (Type (tyco, map TFree (Name.names Name.context "'a" asorts))) |
44 (Type (tyco, map TFree (Name.names Name.context "'a" asorts))))]) arities, thy); |
45 |> tap (writeln o Sign.string_of_term thy))]) arities; |
|
46 fun tac _ = ClassPackage.intro_classes_tac []; |
45 fun tac _ = ClassPackage.intro_classes_tac []; |
47 fun hook specs = |
46 fun hook specs = |
48 DatatypeCodegen.prove_codetypes_arities tac |
47 DatatypeCodegen.prove_codetypes_arities tac |
49 (map (fn (tyco, (is_dt, _)) => (tyco, is_dt)) specs) |
48 (map (fn (tyco, (is_dt, _)) => (tyco, is_dt)) specs) |
50 [TypOf.class_typ_of] mk I |
49 [TypOf.class_typ_of] mk ((K o K) I) |
51 in DatatypeCodegen.add_codetypes_hook_bootstrap hook end |
50 in DatatypeCodegen.add_codetypes_hook_bootstrap hook end |
52 *} |
51 *} |
53 |
52 |
54 |
53 |
55 subsection {* term_of class *} |
54 subsection {* term_of class *} |
88 end; |
87 end; |
89 *} |
88 *} |
90 |
89 |
91 setup {* |
90 setup {* |
92 let |
91 let |
93 fun mk thy arities css = |
92 fun thy_note ((name, atts), thms) = |
|
93 PureThy.add_thmss [((name, thms), atts)] #-> (fn [thms] => pair (name, thms)); |
|
94 fun thy_def ((name, atts), t) = |
|
95 PureThy.add_defs_i false [((name, t), atts)] #-> (fn [thm] => pair (name, thm)); |
|
96 fun mk arities css thy = |
94 let |
97 let |
95 val vs = (Name.names Name.context "'a" o snd o fst o hd) arities; |
98 val vs = (Name.names Name.context "'a" o snd o fst o hd) arities; |
96 val raw_defs = map (TermOf.mk_terms_of_defs vs) css; |
99 val defs = map (TermOf.mk_terms_of_defs vs) css; |
97 fun mk' thy' = map (apfst (rpair [])) ((PrimrecPackage.mk_combdefs thy' o flat) raw_defs) |
100 val defs' = (map (pair ("", []) o ObjectLogic.ensure_propT thy) o flat) defs; |
98 in ClassPackage.assume_arities_thy thy arities mk' end; |
101 in |
|
102 thy |
|
103 |> PrimrecPackage.gen_primrec thy_note thy_def "" defs' |
|
104 |> snd |
|
105 end; |
99 fun tac _ = ClassPackage.intro_classes_tac []; |
106 fun tac _ = ClassPackage.intro_classes_tac []; |
100 fun hook specs = |
107 fun hook specs = |
101 if (fst o hd) specs = (fst o dest_Type) Embed.typ_typ then I |
108 if (fst o hd) specs = (fst o dest_Type) Embed.typ_typ then I |
102 else |
109 else |
103 DatatypeCodegen.prove_codetypes_arities tac |
110 DatatypeCodegen.prove_codetypes_arities tac |
104 (map (fn (tyco, (is_dt, _)) => (tyco, is_dt)) specs) |
111 (map (fn (tyco, (is_dt, _)) => (tyco, is_dt)) specs) |
105 [TermOf.class_term_of] mk I |
112 [TermOf.class_term_of] ((K o K o pair) []) mk |
106 in DatatypeCodegen.add_codetypes_hook_bootstrap hook end |
113 in DatatypeCodegen.add_codetypes_hook_bootstrap hook end |
107 *} |
114 *} |
108 |
115 |
109 |
116 |
110 subsection {* Evaluation infrastructure *} |
117 subsection {* Evaluation infrastructure *} |