author | blanchet |
Mon, 02 Dec 2013 20:31:54 +0100 | |
changeset 55988 | 62fb5af93fe2 |
parent 53925 | da1fdbfebd39 |
child 56743 | f33536723999 |
permissions | -rw-r--r-- |
haftmann@33967 | 1 |
(* Title: HOL/Tools/Datatype/datatype_codegen.ML |
wenzelm@29265 | 2 |
Author: Stefan Berghofer and Florian Haftmann, TU Muenchen |
berghofe@12445 | 3 |
|
haftmann@25534 | 4 |
Code generator facilities for inductive datatypes. |
berghofe@12445 | 5 |
*) |
berghofe@12445 | 6 |
|
berghofe@12445 | 7 |
signature DATATYPE_CODEGEN = |
berghofe@12445 | 8 |
sig |
berghofe@12445 | 9 |
end; |
berghofe@12445 | 10 |
|
haftmann@33967 | 11 |
structure Datatype_Codegen : DATATYPE_CODEGEN = |
berghofe@12445 | 12 |
struct |
berghofe@12445 | 13 |
|
blanchet@55988 | 14 |
fun add_code_for_datatype fcT_name thy = |
blanchet@55988 | 15 |
let |
blanchet@55988 | 16 |
val (As', ctr_specs) = Datatype_Data.the_spec thy fcT_name; |
blanchet@55988 | 17 |
val {inject = inject_thms, distinct = distinct_thms, case_rewrites = case_thms, ...} = |
blanchet@55988 | 18 |
Datatype_Data.the_info thy fcT_name; |
haftmann@36296 | 19 |
|
blanchet@55988 | 20 |
val As = map TFree As'; |
blanchet@55988 | 21 |
val fcT = Type (fcT_name, As); |
blanchet@55988 | 22 |
val ctrs = map (fn (c, arg_Ts) => (c, arg_Ts ---> fcT)) ctr_specs; |
wenzelm@46571 | 23 |
in |
blanchet@55988 | 24 |
Ctr_Sugar_Code.add_ctr_code fcT_name As ctrs inject_thms distinct_thms case_thms thy |
haftmann@36296 | 25 |
end; |
haftmann@36296 | 26 |
|
blanchet@55988 | 27 |
val _ = Theory.setup (Datatype_Data.interpretation (K (fold add_code_for_datatype))); |
haftmann@20597 | 28 |
|
berghofe@12445 | 29 |
end; |