isabelle: src/HOL/Tools/Old_Datatype/old_datatype_codegen.ML@c6a7de505796 (annotated)

58112 8081087096ad renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place blanchet parents: 55401 diff changeset	1	(* Title: HOL/Tools/Old_Datatype/old_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 f17eb90bfd16 Code generator for datatypes. berghofe parents: diff changeset	3
25534 d0b74fdd6067 simplified infrastructure for code generator operational equality haftmann parents: 25505 diff changeset	4	Code generator facilities for inductive datatypes.
12445 f17eb90bfd16 Code generator for datatypes. berghofe parents: diff changeset	5	*)
f17eb90bfd16 Code generator for datatypes. berghofe parents: diff changeset	6
58112 8081087096ad renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place blanchet parents: 55401 diff changeset	7	signature OLD_DATATYPE_CODEGEN =
12445 f17eb90bfd16 Code generator for datatypes. berghofe parents: diff changeset	8	sig
f17eb90bfd16 Code generator for datatypes. berghofe parents: diff changeset	9	end;
f17eb90bfd16 Code generator for datatypes. berghofe parents: diff changeset	10
58112 8081087096ad renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place blanchet parents: 55401 diff changeset	11	structure Old_Datatype_Codegen : OLD_DATATYPE_CODEGEN =
12445 f17eb90bfd16 Code generator for datatypes. berghofe parents: diff changeset	12	struct
f17eb90bfd16 Code generator for datatypes. berghofe parents: diff changeset	13
54615 62fb5af93fe2 generalized datatype code generation code so that it works with old-style and new-style (co)datatypes (as long as they are not local) blanchet parents: 52788 diff changeset	14	fun add_code_for_datatype fcT_name thy =
36298 2d55c4aba1dc swapped generic code generator and SML code generator haftmann parents: 35899 diff changeset	15	let
55401 f33536723999 more 'ctr_sugar' modernization blanchet parents: 54615 diff changeset	16	val ctxt = Proof_Context.init_global thy
f33536723999 more 'ctr_sugar' modernization blanchet parents: 54615 diff changeset	17	val SOME {ctrs, injects, distincts, case_thms, ...} = Ctr_Sugar.ctr_sugar_of ctxt fcT_name
f33536723999 more 'ctr_sugar' modernization blanchet parents: 54615 diff changeset	18	val Type (_, As) = body_type (fastype_of (hd ctrs))
36298 2d55c4aba1dc swapped generic code generator and SML code generator haftmann parents: 35899 diff changeset	19	in
55401 f33536723999 more 'ctr_sugar' modernization blanchet parents: 54615 diff changeset	20	Ctr_Sugar_Code.add_ctr_code fcT_name As (map dest_Const ctrs) injects distincts case_thms thy
36298 2d55c4aba1dc swapped generic code generator and SML code generator haftmann parents: 35899 diff changeset	21	end;
2d55c4aba1dc swapped generic code generator and SML code generator haftmann parents: 35899 diff changeset	22
58112 8081087096ad renamed modules defining old datatypes, as a step towards having 'datatype_new' take 'datatype's place blanchet parents: 55401 diff changeset	23	val _ = Theory.setup (Old_Datatype_Data.interpretation (K (fold add_code_for_datatype)));
20597 65fe827aa595 code generation 2 adjustments haftmann parents: 20439 diff changeset	24
12445 f17eb90bfd16 Code generator for datatypes. berghofe parents: diff changeset	25	end;

author	haftmann
	Mon, 06 Feb 2017 20:56:34 +0100
changeset 64990	c6a7de505796
parent 58112	8081087096ad
permissions	-rw-r--r--