nominal2: Nominal/nominal_dt_data.ML@01ff621599bc (annotated)

2890 503630c553a8 added file Christian Urban <urbanc@in.tum.de> parents: diff changeset	1	(* Author: Christian Urban
503630c553a8 added file Christian Urban <urbanc@in.tum.de> parents: diff changeset	2
503630c553a8 added file Christian Urban <urbanc@in.tum.de> parents: diff changeset	3	data about nominal datatypes
503630c553a8 added file Christian Urban <urbanc@in.tum.de> parents: diff changeset	4	*)
503630c553a8 added file Christian Urban <urbanc@in.tum.de> parents: diff changeset	5
503630c553a8 added file Christian Urban <urbanc@in.tum.de> parents: diff changeset	6	signature NOMINAL_DT_DATA =
503630c553a8 added file Christian Urban <urbanc@in.tum.de> parents: diff changeset	7	sig
2957 01ff621599bc code refactoring; introduced a record for raw_dt_info Christian Urban <urbanc@in.tum.de> parents: 2927 diff changeset	8	(* info of raw datatypes *)
01ff621599bc code refactoring; introduced a record for raw_dt_info Christian Urban <urbanc@in.tum.de> parents: 2927 diff changeset	9	type dt_info = (string list * binding * mixfix * ((binding * typ list * mixfix) list)) list
01ff621599bc code refactoring; introduced a record for raw_dt_info Christian Urban <urbanc@in.tum.de> parents: 2927 diff changeset	10
01ff621599bc code refactoring; introduced a record for raw_dt_info Christian Urban <urbanc@in.tum.de> parents: 2927 diff changeset	11	(* info of raw binding functions *)
01ff621599bc code refactoring; introduced a record for raw_dt_info Christian Urban <urbanc@in.tum.de> parents: 2927 diff changeset	12	type bn_info = term * int * (int * term option) list list
01ff621599bc code refactoring; introduced a record for raw_dt_info Christian Urban <urbanc@in.tum.de> parents: 2927 diff changeset	13
01ff621599bc code refactoring; introduced a record for raw_dt_info Christian Urban <urbanc@in.tum.de> parents: 2927 diff changeset	14	(* binding modes and binding clauses *)
01ff621599bc code refactoring; introduced a record for raw_dt_info Christian Urban <urbanc@in.tum.de> parents: 2927 diff changeset	15	datatype bmode = Lst \| Res \| Set
01ff621599bc code refactoring; introduced a record for raw_dt_info Christian Urban <urbanc@in.tum.de> parents: 2927 diff changeset	16	datatype bclause = BC of bmode * (term option * int) list * int list
01ff621599bc code refactoring; introduced a record for raw_dt_info Christian Urban <urbanc@in.tum.de> parents: 2927 diff changeset	17
2890 503630c553a8 added file Christian Urban <urbanc@in.tum.de> parents: diff changeset	18	type info =
2957 01ff621599bc code refactoring; introduced a record for raw_dt_info Christian Urban <urbanc@in.tum.de> parents: 2927 diff changeset	19	{inject : thm list,
01ff621599bc code refactoring; introduced a record for raw_dt_info Christian Urban <urbanc@in.tum.de> parents: 2927 diff changeset	20	distinct : thm list,
01ff621599bc code refactoring; introduced a record for raw_dt_info Christian Urban <urbanc@in.tum.de> parents: 2927 diff changeset	21	strong_inducts : thm list,
01ff621599bc code refactoring; introduced a record for raw_dt_info Christian Urban <urbanc@in.tum.de> parents: 2927 diff changeset	22	strong_exhaust : thm list}
2890 503630c553a8 added file Christian Urban <urbanc@in.tum.de> parents: diff changeset	23
503630c553a8 added file Christian Urban <urbanc@in.tum.de> parents: diff changeset	24	val get_all_info: Proof.context -> (string * info) list
503630c553a8 added file Christian Urban <urbanc@in.tum.de> parents: diff changeset	25	val get_info: Proof.context -> string -> info option
503630c553a8 added file Christian Urban <urbanc@in.tum.de> parents: diff changeset	26	val the_info: Proof.context -> string -> info
503630c553a8 added file Christian Urban <urbanc@in.tum.de> parents: diff changeset	27	val register_info: (string * info) -> Context.generic -> Context.generic
503630c553a8 added file Christian Urban <urbanc@in.tum.de> parents: diff changeset	28	val mk_infos: string list -> thm list -> thm list -> thm list -> thm list -> (string * info) list
2927 116f9ba4f59f combined distributed data for alpha in alpha_result (partially done) Christian Urban <urbanc@in.tum.de> parents: 2890 diff changeset	29
2957 01ff621599bc code refactoring; introduced a record for raw_dt_info Christian Urban <urbanc@in.tum.de> parents: 2927 diff changeset	30	datatype raw_dt_info = RawDtInfo of
01ff621599bc code refactoring; introduced a record for raw_dt_info Christian Urban <urbanc@in.tum.de> parents: 2927 diff changeset	31	{raw_dt_names : string list,
01ff621599bc code refactoring; introduced a record for raw_dt_info Christian Urban <urbanc@in.tum.de> parents: 2927 diff changeset	32	raw_dts : dt_info,
01ff621599bc code refactoring; introduced a record for raw_dt_info Christian Urban <urbanc@in.tum.de> parents: 2927 diff changeset	33	raw_tys : typ list,
01ff621599bc code refactoring; introduced a record for raw_dt_info Christian Urban <urbanc@in.tum.de> parents: 2927 diff changeset	34	raw_ty_args : (string * sort) list,
01ff621599bc code refactoring; introduced a record for raw_dt_info Christian Urban <urbanc@in.tum.de> parents: 2927 diff changeset	35	raw_cns_info : cns_info list,
01ff621599bc code refactoring; introduced a record for raw_dt_info Christian Urban <urbanc@in.tum.de> parents: 2927 diff changeset	36	raw_all_cns : term list list,
01ff621599bc code refactoring; introduced a record for raw_dt_info Christian Urban <urbanc@in.tum.de> parents: 2927 diff changeset	37	raw_inject_thms : thm list,
01ff621599bc code refactoring; introduced a record for raw_dt_info Christian Urban <urbanc@in.tum.de> parents: 2927 diff changeset	38	raw_distinct_thms : thm list,
01ff621599bc code refactoring; introduced a record for raw_dt_info Christian Urban <urbanc@in.tum.de> parents: 2927 diff changeset	39	raw_induct_thm : thm,
01ff621599bc code refactoring; introduced a record for raw_dt_info Christian Urban <urbanc@in.tum.de> parents: 2927 diff changeset	40	raw_induct_thms : thm list,
01ff621599bc code refactoring; introduced a record for raw_dt_info Christian Urban <urbanc@in.tum.de> parents: 2927 diff changeset	41	raw_exhaust_thms : thm list,
01ff621599bc code refactoring; introduced a record for raw_dt_info Christian Urban <urbanc@in.tum.de> parents: 2927 diff changeset	42	raw_size_trms : term list,
01ff621599bc code refactoring; introduced a record for raw_dt_info Christian Urban <urbanc@in.tum.de> parents: 2927 diff changeset	43	raw_size_thms : thm list}
01ff621599bc code refactoring; introduced a record for raw_dt_info Christian Urban <urbanc@in.tum.de> parents: 2927 diff changeset	44
2927 116f9ba4f59f combined distributed data for alpha in alpha_result (partially done) Christian Urban <urbanc@in.tum.de> parents: 2890 diff changeset	45	datatype alpha_result = AlphaResult of
116f9ba4f59f combined distributed data for alpha in alpha_result (partially done) Christian Urban <urbanc@in.tum.de> parents: 2890 diff changeset	46	{alpha_names : string list,
116f9ba4f59f combined distributed data for alpha in alpha_result (partially done) Christian Urban <urbanc@in.tum.de> parents: 2890 diff changeset	47	alpha_trms : term list,
116f9ba4f59f combined distributed data for alpha in alpha_result (partially done) Christian Urban <urbanc@in.tum.de> parents: 2890 diff changeset	48	alpha_tys : typ list,
116f9ba4f59f combined distributed data for alpha in alpha_result (partially done) Christian Urban <urbanc@in.tum.de> parents: 2890 diff changeset	49	alpha_bn_names : string list,
116f9ba4f59f combined distributed data for alpha in alpha_result (partially done) Christian Urban <urbanc@in.tum.de> parents: 2890 diff changeset	50	alpha_bn_trms : term list,
116f9ba4f59f combined distributed data for alpha in alpha_result (partially done) Christian Urban <urbanc@in.tum.de> parents: 2890 diff changeset	51	alpha_bn_tys : typ list,
116f9ba4f59f combined distributed data for alpha in alpha_result (partially done) Christian Urban <urbanc@in.tum.de> parents: 2890 diff changeset	52	alpha_intros : thm list,
116f9ba4f59f combined distributed data for alpha in alpha_result (partially done) Christian Urban <urbanc@in.tum.de> parents: 2890 diff changeset	53	alpha_cases : thm list,
116f9ba4f59f combined distributed data for alpha in alpha_result (partially done) Christian Urban <urbanc@in.tum.de> parents: 2890 diff changeset	54	alpha_raw_induct : thm}
116f9ba4f59f combined distributed data for alpha in alpha_result (partially done) Christian Urban <urbanc@in.tum.de> parents: 2890 diff changeset	55
2890 503630c553a8 added file Christian Urban <urbanc@in.tum.de> parents: diff changeset	56	end
503630c553a8 added file Christian Urban <urbanc@in.tum.de> parents: diff changeset	57
503630c553a8 added file Christian Urban <urbanc@in.tum.de> parents: diff changeset	58	structure Nominal_Dt_Data: NOMINAL_DT_DATA =
503630c553a8 added file Christian Urban <urbanc@in.tum.de> parents: diff changeset	59	struct
503630c553a8 added file Christian Urban <urbanc@in.tum.de> parents: diff changeset	60
2957 01ff621599bc code refactoring; introduced a record for raw_dt_info Christian Urban <urbanc@in.tum.de> parents: 2927 diff changeset	61	(* string list - type variables of a datatype
01ff621599bc code refactoring; introduced a record for raw_dt_info Christian Urban <urbanc@in.tum.de> parents: 2927 diff changeset	62	binding - name of the datatype
01ff621599bc code refactoring; introduced a record for raw_dt_info Christian Urban <urbanc@in.tum.de> parents: 2927 diff changeset	63	mixfix - its mixfix
01ff621599bc code refactoring; introduced a record for raw_dt_info Christian Urban <urbanc@in.tum.de> parents: 2927 diff changeset	64	(binding * typ list * mixfix) list - datatype constructors of the type
01ff621599bc code refactoring; introduced a record for raw_dt_info Christian Urban <urbanc@in.tum.de> parents: 2927 diff changeset	65	*)
01ff621599bc code refactoring; introduced a record for raw_dt_info Christian Urban <urbanc@in.tum.de> parents: 2927 diff changeset	66	type dt_info = (string list * binding * mixfix * ((binding * typ list * mixfix) list)) list
01ff621599bc code refactoring; introduced a record for raw_dt_info Christian Urban <urbanc@in.tum.de> parents: 2927 diff changeset	67
01ff621599bc code refactoring; introduced a record for raw_dt_info Christian Urban <urbanc@in.tum.de> parents: 2927 diff changeset	68
01ff621599bc code refactoring; introduced a record for raw_dt_info Christian Urban <urbanc@in.tum.de> parents: 2927 diff changeset	69	(* term - is constant of the bn-function
01ff621599bc code refactoring; introduced a record for raw_dt_info Christian Urban <urbanc@in.tum.de> parents: 2927 diff changeset	70	int - is datatype number over which the bn-function is defined
01ff621599bc code refactoring; introduced a record for raw_dt_info Christian Urban <urbanc@in.tum.de> parents: 2927 diff changeset	71	int * term option - is number of the corresponding argument with possibly
01ff621599bc code refactoring; introduced a record for raw_dt_info Christian Urban <urbanc@in.tum.de> parents: 2927 diff changeset	72	recursive call with bn-function term
01ff621599bc code refactoring; introduced a record for raw_dt_info Christian Urban <urbanc@in.tum.de> parents: 2927 diff changeset	73	*)
01ff621599bc code refactoring; introduced a record for raw_dt_info Christian Urban <urbanc@in.tum.de> parents: 2927 diff changeset	74	type bn_info = term * int * (int * term option) list list
01ff621599bc code refactoring; introduced a record for raw_dt_info Christian Urban <urbanc@in.tum.de> parents: 2927 diff changeset	75
01ff621599bc code refactoring; introduced a record for raw_dt_info Christian Urban <urbanc@in.tum.de> parents: 2927 diff changeset	76	datatype bmode = Lst \| Res \| Set
01ff621599bc code refactoring; introduced a record for raw_dt_info Christian Urban <urbanc@in.tum.de> parents: 2927 diff changeset	77	datatype bclause = BC of bmode * (term option * int) list * int list
01ff621599bc code refactoring; introduced a record for raw_dt_info Christian Urban <urbanc@in.tum.de> parents: 2927 diff changeset	78
2927 116f9ba4f59f combined distributed data for alpha in alpha_result (partially done) Christian Urban <urbanc@in.tum.de> parents: 2890 diff changeset	79
2890 503630c553a8 added file Christian Urban <urbanc@in.tum.de> parents: diff changeset	80	(* information generated by nominal_datatype *)
503630c553a8 added file Christian Urban <urbanc@in.tum.de> parents: diff changeset	81	type info =
503630c553a8 added file Christian Urban <urbanc@in.tum.de> parents: diff changeset	82	{inject : thm list,
503630c553a8 added file Christian Urban <urbanc@in.tum.de> parents: diff changeset	83	distinct : thm list,
503630c553a8 added file Christian Urban <urbanc@in.tum.de> parents: diff changeset	84	strong_inducts : thm list,
503630c553a8 added file Christian Urban <urbanc@in.tum.de> parents: diff changeset	85	strong_exhaust : thm list}
503630c553a8 added file Christian Urban <urbanc@in.tum.de> parents: diff changeset	86
503630c553a8 added file Christian Urban <urbanc@in.tum.de> parents: diff changeset	87	structure NominalData = Generic_Data
503630c553a8 added file Christian Urban <urbanc@in.tum.de> parents: diff changeset	88	(type T = info Symtab.table
503630c553a8 added file Christian Urban <urbanc@in.tum.de> parents: diff changeset	89	val empty = Symtab.empty
503630c553a8 added file Christian Urban <urbanc@in.tum.de> parents: diff changeset	90	val extend = I
503630c553a8 added file Christian Urban <urbanc@in.tum.de> parents: diff changeset	91	val merge = Symtab.merge (K true))
503630c553a8 added file Christian Urban <urbanc@in.tum.de> parents: diff changeset	92
503630c553a8 added file Christian Urban <urbanc@in.tum.de> parents: diff changeset	93	val get_all_info = Symtab.dest o NominalData.get o Context.Proof
503630c553a8 added file Christian Urban <urbanc@in.tum.de> parents: diff changeset	94	val get_info = Symtab.lookup o NominalData.get o Context.Proof
503630c553a8 added file Christian Urban <urbanc@in.tum.de> parents: diff changeset	95	val register_info = NominalData.map o Symtab.update
503630c553a8 added file Christian Urban <urbanc@in.tum.de> parents: diff changeset	96
503630c553a8 added file Christian Urban <urbanc@in.tum.de> parents: diff changeset	97	fun the_info thy name =
503630c553a8 added file Christian Urban <urbanc@in.tum.de> parents: diff changeset	98	(case get_info thy name of
503630c553a8 added file Christian Urban <urbanc@in.tum.de> parents: diff changeset	99	SOME info => info
503630c553a8 added file Christian Urban <urbanc@in.tum.de> parents: diff changeset	100	\| NONE => error ("Unknown nominal datatype " ^ quote name))
503630c553a8 added file Christian Urban <urbanc@in.tum.de> parents: diff changeset	101
503630c553a8 added file Christian Urban <urbanc@in.tum.de> parents: diff changeset	102	fun mk_infos ty_names inject distinct strong_inducts strong_exhaust =
503630c553a8 added file Christian Urban <urbanc@in.tum.de> parents: diff changeset	103	let
503630c553a8 added file Christian Urban <urbanc@in.tum.de> parents: diff changeset	104	fun aux ty_name =
503630c553a8 added file Christian Urban <urbanc@in.tum.de> parents: diff changeset	105	(ty_name, {inject = inject,
503630c553a8 added file Christian Urban <urbanc@in.tum.de> parents: diff changeset	106	distinct = distinct,
503630c553a8 added file Christian Urban <urbanc@in.tum.de> parents: diff changeset	107	strong_inducts = strong_inducts,
503630c553a8 added file Christian Urban <urbanc@in.tum.de> parents: diff changeset	108	strong_exhaust = strong_exhaust
503630c553a8 added file Christian Urban <urbanc@in.tum.de> parents: diff changeset	109	})
503630c553a8 added file Christian Urban <urbanc@in.tum.de> parents: diff changeset	110	in
503630c553a8 added file Christian Urban <urbanc@in.tum.de> parents: diff changeset	111	map aux ty_names
503630c553a8 added file Christian Urban <urbanc@in.tum.de> parents: diff changeset	112	end
503630c553a8 added file Christian Urban <urbanc@in.tum.de> parents: diff changeset	113
2957 01ff621599bc code refactoring; introduced a record for raw_dt_info Christian Urban <urbanc@in.tum.de> parents: 2927 diff changeset	114
01ff621599bc code refactoring; introduced a record for raw_dt_info Christian Urban <urbanc@in.tum.de> parents: 2927 diff changeset	115	datatype raw_dt_info = RawDtInfo of
01ff621599bc code refactoring; introduced a record for raw_dt_info Christian Urban <urbanc@in.tum.de> parents: 2927 diff changeset	116	{raw_dt_names : string list,
01ff621599bc code refactoring; introduced a record for raw_dt_info Christian Urban <urbanc@in.tum.de> parents: 2927 diff changeset	117	raw_dts : dt_info,
01ff621599bc code refactoring; introduced a record for raw_dt_info Christian Urban <urbanc@in.tum.de> parents: 2927 diff changeset	118	raw_tys : typ list,
01ff621599bc code refactoring; introduced a record for raw_dt_info Christian Urban <urbanc@in.tum.de> parents: 2927 diff changeset	119	raw_ty_args : (string * sort) list,
01ff621599bc code refactoring; introduced a record for raw_dt_info Christian Urban <urbanc@in.tum.de> parents: 2927 diff changeset	120	raw_cns_info : cns_info list,
01ff621599bc code refactoring; introduced a record for raw_dt_info Christian Urban <urbanc@in.tum.de> parents: 2927 diff changeset	121	raw_all_cns : term list list,
01ff621599bc code refactoring; introduced a record for raw_dt_info Christian Urban <urbanc@in.tum.de> parents: 2927 diff changeset	122	raw_inject_thms : thm list,
01ff621599bc code refactoring; introduced a record for raw_dt_info Christian Urban <urbanc@in.tum.de> parents: 2927 diff changeset	123	raw_distinct_thms : thm list,
01ff621599bc code refactoring; introduced a record for raw_dt_info Christian Urban <urbanc@in.tum.de> parents: 2927 diff changeset	124	raw_induct_thm : thm,
01ff621599bc code refactoring; introduced a record for raw_dt_info Christian Urban <urbanc@in.tum.de> parents: 2927 diff changeset	125	raw_induct_thms : thm list,
01ff621599bc code refactoring; introduced a record for raw_dt_info Christian Urban <urbanc@in.tum.de> parents: 2927 diff changeset	126	raw_exhaust_thms : thm list,
01ff621599bc code refactoring; introduced a record for raw_dt_info Christian Urban <urbanc@in.tum.de> parents: 2927 diff changeset	127	raw_size_trms : term list,
01ff621599bc code refactoring; introduced a record for raw_dt_info Christian Urban <urbanc@in.tum.de> parents: 2927 diff changeset	128	raw_size_thms : thm list}
01ff621599bc code refactoring; introduced a record for raw_dt_info Christian Urban <urbanc@in.tum.de> parents: 2927 diff changeset	129
2927 116f9ba4f59f combined distributed data for alpha in alpha_result (partially done) Christian Urban <urbanc@in.tum.de> parents: 2890 diff changeset	130	datatype alpha_result = AlphaResult of
116f9ba4f59f combined distributed data for alpha in alpha_result (partially done) Christian Urban <urbanc@in.tum.de> parents: 2890 diff changeset	131	{alpha_names : string list,
116f9ba4f59f combined distributed data for alpha in alpha_result (partially done) Christian Urban <urbanc@in.tum.de> parents: 2890 diff changeset	132	alpha_trms : term list,
116f9ba4f59f combined distributed data for alpha in alpha_result (partially done) Christian Urban <urbanc@in.tum.de> parents: 2890 diff changeset	133	alpha_tys : typ list,
116f9ba4f59f combined distributed data for alpha in alpha_result (partially done) Christian Urban <urbanc@in.tum.de> parents: 2890 diff changeset	134	alpha_bn_names : string list,
116f9ba4f59f combined distributed data for alpha in alpha_result (partially done) Christian Urban <urbanc@in.tum.de> parents: 2890 diff changeset	135	alpha_bn_trms : term list,
116f9ba4f59f combined distributed data for alpha in alpha_result (partially done) Christian Urban <urbanc@in.tum.de> parents: 2890 diff changeset	136	alpha_bn_tys : typ list,
116f9ba4f59f combined distributed data for alpha in alpha_result (partially done) Christian Urban <urbanc@in.tum.de> parents: 2890 diff changeset	137	alpha_intros : thm list,
116f9ba4f59f combined distributed data for alpha in alpha_result (partially done) Christian Urban <urbanc@in.tum.de> parents: 2890 diff changeset	138	alpha_cases : thm list,
116f9ba4f59f combined distributed data for alpha in alpha_result (partially done) Christian Urban <urbanc@in.tum.de> parents: 2890 diff changeset	139	alpha_raw_induct : thm}
116f9ba4f59f combined distributed data for alpha in alpha_result (partially done) Christian Urban <urbanc@in.tum.de> parents: 2890 diff changeset	140
2890 503630c553a8 added file Christian Urban <urbanc@in.tum.de> parents: diff changeset	141	end

author	Christian Urban <urbanc@in.tum.de>
	Thu, 07 Jul 2011 16:16:42 +0200
changeset 2957	01ff621599bc
parent 2927	116f9ba4f59f
child 2959	9bd97ed202f7
permissions	-rw-r--r--