--- a/src/HOL/Tools/Datatype/datatype.ML Sun Sep 27 22:25:13 2009 +0200
+++ b/src/HOL/Tools/Datatype/datatype.ML Mon Sep 28 09:47:32 2009 +0200
@@ -39,8 +39,9 @@
open DatatypeAux;
+(** theory data **)
-(* theory data *)
+(* data management *)
structure DatatypesData = TheoryDataFun
(
@@ -62,13 +63,16 @@
);
val get_all = #types o DatatypesData.get;
-val map_datatypes = DatatypesData.map;
-
+val get_info = Symtab.lookup o get_all;
+fun the_info thy name = (case get_info thy name of
+ SOME info => info
+ | NONE => error ("Unknown datatype " ^ quote name));
-(** theory information about datatypes **)
+val info_of_constr = Symtab.lookup o #constrs o DatatypesData.get;
+val info_of_case = Symtab.lookup o #cases o DatatypesData.get;
-fun put_dt_infos (dt_infos : (string * info) list) =
- map_datatypes (fn {types, constrs, cases} =>
+fun register (dt_infos : (string * info) list) =
+ DatatypesData.map (fn {types, constrs, cases} =>
{types = fold Symtab.update dt_infos types,
constrs = fold Symtab.default (*conservative wrt. overloaded constructors*)
(maps (fn (_, info as {descr, index, ...}) => map (rpair info o fst)
@@ -77,19 +81,7 @@
(map (fn (_, info as {case_name, ...}) => (case_name, info)) dt_infos)
cases});
-val get_info = Symtab.lookup o get_all;
-
-fun the_info thy name = (case get_info thy name of
- SOME info => info
- | NONE => error ("Unknown datatype " ^ quote name));
-
-val info_of_constr = Symtab.lookup o #constrs o DatatypesData.get;
-val info_of_case = Symtab.lookup o #cases o DatatypesData.get;
-
-fun get_info_descr thy dtco =
- get_info thy dtco
- |> Option.map (fn info as { descr, index, ... } =>
- (info, (((fn SOME (_, dtys, cos) => (dtys, cos)) o AList.lookup (op =) descr) index)));
+(* complex queries *)
fun the_spec thy dtco =
let
@@ -143,69 +135,9 @@
| NONE => NONE;
-(** induct method setup **)
-
-(* case names *)
-
-local
-
-fun dt_recs (DtTFree _) = []
- | dt_recs (DtType (_, dts)) = maps dt_recs dts
- | dt_recs (DtRec i) = [i];
-
-fun dt_cases (descr: descr) (_, args, constrs) =
- let
- fun the_bname i = Long_Name.base_name (#1 (the (AList.lookup (op =) descr i)));
- val bnames = map the_bname (distinct (op =) (maps dt_recs args));
- in map (fn (c, _) => space_implode "_" (Long_Name.base_name c :: bnames)) constrs end;
-
-
-fun induct_cases descr =
- DatatypeProp.indexify_names (maps (dt_cases descr) (map #2 descr));
-
-fun exhaust_cases descr i = dt_cases descr (the (AList.lookup (op =) descr i));
-
-in
-
-fun mk_case_names_induct descr = RuleCases.case_names (induct_cases descr);
-
-fun mk_case_names_exhausts descr new =
- map (RuleCases.case_names o exhaust_cases descr o #1)
- (filter (fn ((_, (name, _, _))) => member (op =) new name) descr);
-
-end;
+(** various auxiliary **)
-fun add_rules simps case_thms rec_thms inject distinct
- weak_case_congs cong_att =
- PureThy.add_thmss [((Binding.name "simps", simps), []),
- ((Binding.empty, flat case_thms @
- flat distinct @ rec_thms), [Simplifier.simp_add]),
- ((Binding.empty, rec_thms), [Code.add_default_eqn_attribute]),
- ((Binding.empty, flat inject), [iff_add]),
- ((Binding.empty, map (fn th => th RS notE) (flat distinct)), [Classical.safe_elim NONE]),
- ((Binding.empty, weak_case_congs), [cong_att])]
- #> snd;
-
-
-(* add_cases_induct *)
-
-fun add_cases_induct infos inducts thy =
- let
- fun named_rules (name, {index, exhaust, ...}: info) =
- [((Binding.empty, nth inducts index), [Induct.induct_type name]),
- ((Binding.empty, exhaust), [Induct.cases_type name])];
- fun unnamed_rule i =
- ((Binding.empty, nth inducts i), [Thm.kind_internal, Induct.induct_type ""]);
- in
- thy |> PureThy.add_thms
- (maps named_rules infos @
- map unnamed_rule (length infos upto length inducts - 1)) |> snd
- |> PureThy.add_thmss [((Binding.name "inducts", inducts), [])] |> snd
- end;
-
-
-
-(**** simplification procedure for showing distinctness of constructors ****)
+(* simplification procedure for showing distinctness of constructors *)
fun stripT (i, Type ("fun", [_, T])) = stripT (i + 1, T)
| stripT p = p;
@@ -233,17 +165,21 @@
etac FalseE 1]))
end;
+fun get_constr thy dtco =
+ get_info thy dtco
+ |> Option.map (fn { descr, index, ... } => (#3 o the o AList.lookup (op =) descr) index);
+
fun distinct_proc thy ss (t as Const ("op =", _) $ t1 $ t2) =
(case (stripC (0, t1), stripC (0, t2)) of
((i, Const (cname1, T1)), (j, Const (cname2, T2))) =>
(case (stripT (0, T1), stripT (0, T2)) of
((i', Type (tname1, _)), (j', Type (tname2, _))) =>
if tname1 = tname2 andalso not (cname1 = cname2) andalso i = i' andalso j = j' then
- (case (get_info_descr thy) tname1 of
- SOME (_, (_, constrs)) => let val cnames = map fst constrs
+ (case get_constr thy tname1 of
+ SOME constrs => let val cnames = map fst constrs
in if cname1 mem cnames andalso cname2 mem cnames then
SOME (distinct_rule thy ss tname1
- (Logic.mk_equals (t, Const ("False", HOLogic.boolT))))
+ (Logic.mk_equals (t, HOLogic.false_const)))
else NONE
end
| NONE => NONE)
@@ -260,8 +196,79 @@
val simproc_setup =
Simplifier.map_simpset (fn ss => ss addsimprocs [distinct_simproc]);
+(* prepare datatype specifications *)
-(**** translation rules for case ****)
+fun read_typ thy ((Ts, sorts), str) =
+ let
+ val ctxt = ProofContext.init thy
+ |> fold (Variable.declare_typ o TFree) sorts;
+ val T = Syntax.read_typ ctxt str;
+ in (Ts @ [T], Term.add_tfreesT T sorts) end;
+
+fun cert_typ sign ((Ts, sorts), raw_T) =
+ let
+ val T = Type.no_tvars (Sign.certify_typ sign raw_T) handle
+ TYPE (msg, _, _) => error msg;
+ val sorts' = Term.add_tfreesT T sorts;
+ in (Ts @ [T],
+ case duplicates (op =) (map fst sorts') of
+ [] => sorts'
+ | dups => error ("Inconsistent sort constraints for " ^ commas dups))
+ end;
+
+(* arrange data entries *)
+
+fun make_dt_info alt_names descr sorts inducts reccomb_names rec_thms
+ ((((((((((i, (_, (tname, _, _))), case_name), case_thms),
+ exhaust_thm), distinct_thm), inject), splits), nchotomy), case_cong), weak_case_cong) =
+ (tname,
+ {index = i,
+ alt_names = alt_names,
+ descr = descr,
+ sorts = sorts,
+ inject = inject,
+ distinct = distinct_thm,
+ inducts = inducts,
+ exhaust = exhaust_thm,
+ nchotomy = nchotomy,
+ rec_names = reccomb_names,
+ rec_rewrites = rec_thms,
+ case_name = case_name,
+ case_rewrites = case_thms,
+ case_cong = case_cong,
+ weak_case_cong = weak_case_cong,
+ splits = splits});
+
+(* case names *)
+
+local
+
+fun dt_recs (DtTFree _) = []
+ | dt_recs (DtType (_, dts)) = maps dt_recs dts
+ | dt_recs (DtRec i) = [i];
+
+fun dt_cases (descr: descr) (_, args, constrs) =
+ let
+ fun the_bname i = Long_Name.base_name (#1 (the (AList.lookup (op =) descr i)));
+ val bnames = map the_bname (distinct (op =) (maps dt_recs args));
+ in map (fn (c, _) => space_implode "_" (Long_Name.base_name c :: bnames)) constrs end;
+
+fun induct_cases descr =
+ DatatypeProp.indexify_names (maps (dt_cases descr) (map #2 descr));
+
+fun exhaust_cases descr i = dt_cases descr (the (AList.lookup (op =) descr i));
+
+in
+
+fun mk_case_names_induct descr = RuleCases.case_names (induct_cases descr);
+
+fun mk_case_names_exhausts descr new =
+ map (RuleCases.case_names o exhaust_cases descr o #1)
+ (filter (fn ((_, (name, _, _))) => member (op =) new name) descr);
+
+end;
+
+(* translation rules for case *)
fun make_case ctxt = DatatypeCase.make_case
(info_of_constr (ProofContext.theory_of ctxt)) ctxt;
@@ -281,59 +288,199 @@
[("_case_syntax", DatatypeCase.case_tr true info_of_constr)],
[], []);
-
-(* prepare types *)
-
-fun read_typ thy ((Ts, sorts), str) =
- let
- val ctxt = ProofContext.init thy
- |> fold (Variable.declare_typ o TFree) sorts;
- val T = Syntax.read_typ ctxt str;
- in (Ts @ [T], Term.add_tfreesT T sorts) end;
+(* document antiquotation *)
-fun cert_typ sign ((Ts, sorts), raw_T) =
- let
- val T = Type.no_tvars (Sign.certify_typ sign raw_T) handle
- TYPE (msg, _, _) => error msg;
- val sorts' = Term.add_tfreesT T sorts;
- in (Ts @ [T],
- case duplicates (op =) (map fst sorts') of
- [] => sorts'
- | dups => error ("Inconsistent sort constraints for " ^ commas dups))
- end;
+val _ = ThyOutput.antiquotation "datatype" Args.tyname
+ (fn {source = src, context = ctxt, ...} => fn dtco =>
+ let
+ val thy = ProofContext.theory_of ctxt;
+ val (vs, cos) = the_spec thy dtco;
+ val ty = Type (dtco, map TFree vs);
+ fun pretty_typ_bracket (ty as Type (_, _ :: _)) =
+ Pretty.enclose "(" ")" [Syntax.pretty_typ ctxt ty]
+ | pretty_typ_bracket ty =
+ Syntax.pretty_typ ctxt ty;
+ fun pretty_constr (co, tys) =
+ (Pretty.block o Pretty.breaks)
+ (Syntax.pretty_term ctxt (Const (co, tys ---> ty)) ::
+ map pretty_typ_bracket tys);
+ val pretty_datatype =
+ Pretty.block
+ (Pretty.command "datatype" :: Pretty.brk 1 ::
+ Syntax.pretty_typ ctxt ty ::
+ Pretty.str " =" :: Pretty.brk 1 ::
+ flat (separate [Pretty.brk 1, Pretty.str "| "]
+ (map (single o pretty_constr) cos)));
+ in ThyOutput.output (ThyOutput.maybe_pretty_source (K pretty_datatype) src [()]) end);
-(**** make datatype info ****)
-
-fun make_dt_info alt_names descr sorts inducts reccomb_names rec_thms
- ((((((((((i, (_, (tname, _, _))), case_name), case_thms),
- exhaust_thm), distinct_thm), inject), splits), nchotomy), case_cong), weak_case_cong) =
- (tname,
- {index = i,
- alt_names = alt_names,
- descr = descr,
- sorts = sorts,
- rec_names = reccomb_names,
- rec_rewrites = rec_thms,
- case_name = case_name,
- case_rewrites = case_thms,
- inducts = inducts,
- exhaust = exhaust_thm,
- distinct = distinct_thm,
- inject = inject,
- splits = splits,
- nchotomy = nchotomy,
- case_cong = case_cong,
- weak_case_cong = weak_case_cong});
+(** abstract theory extensions relative to a datatype characterisation **)
structure DatatypeInterpretation = InterpretationFun
(type T = config * string list val eq: T * T -> bool = eq_snd op =);
fun interpretation f = DatatypeInterpretation.interpretation (uncurry f);
+fun add_rules simps case_thms rec_thms inject distinct
+ weak_case_congs cong_att =
+ PureThy.add_thmss [((Binding.name "simps", simps), []),
+ ((Binding.empty, flat case_thms @
+ flat distinct @ rec_thms), [Simplifier.simp_add]),
+ ((Binding.empty, rec_thms), [Code.add_default_eqn_attribute]),
+ ((Binding.empty, flat inject), [iff_add]),
+ ((Binding.empty, map (fn th => th RS notE) (flat distinct)), [Classical.safe_elim NONE]),
+ ((Binding.empty, weak_case_congs), [cong_att])]
+ #> snd;
-(******************* definitional introduction of datatypes *******************)
+fun add_cases_induct infos inducts thy =
+ let
+ fun named_rules (name, {index, exhaust, ...}: info) =
+ [((Binding.empty, nth inducts index), [Induct.induct_type name]),
+ ((Binding.empty, exhaust), [Induct.cases_type name])];
+ fun unnamed_rule i =
+ ((Binding.empty, nth inducts i), [Thm.kind_internal, Induct.induct_type ""]);
+ in
+ thy |> PureThy.add_thms
+ (maps named_rules infos @
+ map unnamed_rule (length infos upto length inducts - 1)) |> snd
+ |> PureThy.add_thmss [((Binding.name "inducts", inducts), [])] |> snd
+ end;
+
+fun derive_datatype_props config dt_names alt_names descr sorts induct inject distinct thy1 =
+ let
+ val thy2 = thy1 |> Theory.checkpoint
+ val new_type_names = map Long_Name.base_name (the_default dt_names alt_names);
+ val _ = message config ("Proofs for datatype(s) " ^ commas_quote new_type_names);
+ val (case_names_induct, case_names_exhausts) =
+ (mk_case_names_induct descr, mk_case_names_exhausts descr dt_names);
+ val inducts = Project_Rule.projections (ProofContext.init thy2) induct;
+
+ val (casedist_thms, thy3) = thy2 |>
+ DatatypeAbsProofs.prove_casedist_thms config new_type_names [descr] sorts induct
+ case_names_exhausts;
+ val ((reccomb_names, rec_thms), thy4) = DatatypeAbsProofs.prove_primrec_thms
+ config new_type_names [descr] sorts (get_all thy3) inject distinct
+ (Simplifier.theory_context thy3 dist_ss) induct thy3;
+ val ((case_thms, case_names), thy5) = DatatypeAbsProofs.prove_case_thms
+ config new_type_names [descr] sorts reccomb_names rec_thms thy4;
+ val (split_thms, thy6) = DatatypeAbsProofs.prove_split_thms
+ config new_type_names [descr] sorts inject distinct casedist_thms case_thms thy5;
+ val (nchotomys, thy7) = DatatypeAbsProofs.prove_nchotomys config new_type_names
+ [descr] sorts casedist_thms thy6;
+ val (case_congs, thy8) = DatatypeAbsProofs.prove_case_congs new_type_names
+ [descr] sorts nchotomys case_thms thy7;
+ val (weak_case_congs, thy9) = DatatypeAbsProofs.prove_weak_case_congs new_type_names
+ [descr] sorts thy8;
+
+ val simps = flat (distinct @ inject @ case_thms) @ rec_thms;
+ val dt_infos = map (make_dt_info alt_names descr sorts (inducts, induct) reccomb_names rec_thms)
+ ((0 upto length descr - 1) ~~ descr ~~ case_names ~~ case_thms ~~ casedist_thms ~~
+ map FewConstrs distinct ~~ inject ~~ split_thms ~~ nchotomys ~~ case_congs ~~ weak_case_congs);
+ val dt_names = map fst dt_infos;
+ in
+ thy9
+ |> add_case_tr' case_names
+ |> add_rules simps case_thms rec_thms inject distinct weak_case_congs (Simplifier.attrib (op addcongs))
+ |> register dt_infos
+ |> add_cases_induct dt_infos inducts
+ |> Sign.parent_path
+ |> store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms)
+ |> snd
+ |> DatatypeInterpretation.data (config, dt_names)
+ |> pair dt_names
+ end;
+
+
+(** declare existing type as datatype **)
-fun add_datatype_def (config : config) new_type_names descr sorts types_syntax constr_syntax dt_info
+fun prove_rep_datatype config dt_names alt_names descr sorts raw_induct raw_inject half_distinct thy1 =
+ let
+ val raw_distinct = (map o maps) (fn thm => [thm, thm RS not_sym]) half_distinct;
+ val new_type_names = map Long_Name.base_name (the_default dt_names alt_names);
+ val (case_names_induct, case_names_exhausts) =
+ (mk_case_names_induct descr, mk_case_names_exhausts descr dt_names);
+ val (((inject, distinct), [induct]), thy2) =
+ thy1
+ |> store_thmss "inject" new_type_names raw_inject
+ ||>> store_thmss "distinct" new_type_names raw_distinct
+ ||> Sign.add_path (space_implode "_" new_type_names)
+ ||>> PureThy.add_thms [((Binding.name "induct", raw_induct), [case_names_induct])];
+ in
+ thy2
+ |> derive_datatype_props config dt_names alt_names descr sorts induct inject distinct
+ end;
+
+fun gen_rep_datatype prep_term config after_qed alt_names raw_ts thy =
+ let
+ fun constr_of_term (Const (c, T)) = (c, T)
+ | constr_of_term t =
+ error ("Not a constant: " ^ Syntax.string_of_term_global thy t);
+ fun no_constr (c, T) = error ("Bad constructor: "
+ ^ Sign.extern_const thy c ^ "::"
+ ^ Syntax.string_of_typ_global thy T);
+ fun type_of_constr (cT as (_, T)) =
+ let
+ val frees = OldTerm.typ_tfrees T;
+ val (tyco, vs) = ((apsnd o map) (dest_TFree) o dest_Type o snd o strip_type) T
+ handle TYPE _ => no_constr cT
+ val _ = if has_duplicates (eq_fst (op =)) vs then no_constr cT else ();
+ val _ = if length frees <> length vs then no_constr cT else ();
+ in (tyco, (vs, cT)) end;
+
+ val raw_cs = AList.group (op =) (map (type_of_constr o constr_of_term o prep_term thy) raw_ts);
+ val _ = case map_filter (fn (tyco, _) =>
+ if Symtab.defined (get_all thy) tyco then SOME tyco else NONE) raw_cs
+ of [] => ()
+ | tycos => error ("Type(s) " ^ commas (map quote tycos)
+ ^ " already represented inductivly");
+ val raw_vss = maps (map (map snd o fst) o snd) raw_cs;
+ val ms = case distinct (op =) (map length raw_vss)
+ of [n] => 0 upto n - 1
+ | _ => error ("Different types in given constructors");
+ fun inter_sort m = map (fn xs => nth xs m) raw_vss
+ |> Library.foldr1 (Sorts.inter_sort (Sign.classes_of thy))
+ val sorts = map inter_sort ms;
+ val vs = Name.names Name.context Name.aT sorts;
+
+ fun norm_constr (raw_vs, (c, T)) = (c, map_atyps
+ (TFree o (the o AList.lookup (op =) (map fst raw_vs ~~ vs)) o fst o dest_TFree) T);
+
+ val cs = map (apsnd (map norm_constr)) raw_cs;
+ val dtyps_of_typ = map (dtyp_of_typ (map (rpair (map fst vs) o fst) cs))
+ o fst o strip_type;
+ val dt_names = map fst cs;
+
+ fun mk_spec (i, (tyco, constr)) = (i, (tyco,
+ map (DtTFree o fst) vs,
+ (map o apsnd) dtyps_of_typ constr))
+ val descr = map_index mk_spec cs;
+ val injs = DatatypeProp.make_injs [descr] vs;
+ val half_distincts = map snd (DatatypeProp.make_distincts [descr] vs);
+ val ind = DatatypeProp.make_ind [descr] vs;
+ val rules = (map o map o map) Logic.close_form [[[ind]], injs, half_distincts];
+
+ fun after_qed' raw_thms =
+ let
+ val [[[induct]], injs, half_distincts] =
+ unflat rules (map Drule.zero_var_indexes_list raw_thms);
+ (*FIXME somehow dubious*)
+ in
+ ProofContext.theory_result
+ (prove_rep_datatype config dt_names alt_names descr vs induct injs half_distincts)
+ #-> after_qed
+ end;
+ in
+ thy
+ |> ProofContext.init
+ |> Proof.theorem_i NONE after_qed' ((map o map) (rpair []) (flat rules))
+ end;
+
+val rep_datatype = gen_rep_datatype Sign.cert_term;
+val rep_datatype_cmd = gen_rep_datatype Syntax.read_term_global default_config (K I);
+
+
+(** definitional introduction of datatypes **)
+
+fun add_datatype_def config new_type_names descr sorts types_syntax constr_syntax dt_info
case_names_induct case_names_exhausts thy =
let
val _ = message config ("Proofs for datatype(s) " ^ commas_quote new_type_names);
@@ -373,155 +520,14 @@
|> Sign.add_path (space_implode "_" new_type_names)
|> add_rules simps case_thms rec_thms inject distinct
weak_case_congs (Simplifier.attrib (op addcongs))
- |> put_dt_infos dt_infos
+ |> register dt_infos
|> add_cases_induct dt_infos inducts
|> Sign.parent_path
|> store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms) |> snd
|> DatatypeInterpretation.data (config, map fst dt_infos);
in (dt_names, thy12) end;
-
-(*********************** declare existing type as datatype *********************)
-
-fun prove_rep_datatype (config : config) alt_names new_type_names descr sorts induct inject half_distinct thy =
- let
- val ((_, [induct']), _) =
- Variable.importT [induct] (Variable.thm_context induct);
-
- fun err t = error ("Ill-formed predicate in induction rule: " ^
- Syntax.string_of_term_global thy t);
-
- fun get_typ (t as _ $ Var (_, Type (tname, Ts))) =
- ((tname, map (fst o dest_TFree) Ts) handle TERM _ => err t)
- | get_typ t = err t;
- val dtnames = map get_typ (HOLogic.dest_conj (HOLogic.dest_Trueprop (Thm.concl_of induct')));
-
- val dt_info = get_all thy;
-
- val distinct = (map o maps) (fn thm => [thm, thm RS not_sym]) half_distinct;
- val (case_names_induct, case_names_exhausts) =
- (mk_case_names_induct descr, mk_case_names_exhausts descr (map #1 dtnames));
-
- val _ = message config ("Proofs for datatype(s) " ^ commas_quote new_type_names);
-
- val (casedist_thms, thy2) = thy |>
- DatatypeAbsProofs.prove_casedist_thms config new_type_names [descr] sorts induct
- case_names_exhausts;
- val ((reccomb_names, rec_thms), thy3) = DatatypeAbsProofs.prove_primrec_thms
- config new_type_names [descr] sorts dt_info inject distinct
- (Simplifier.theory_context thy2 dist_ss) induct thy2;
- val ((case_thms, case_names), thy4) = DatatypeAbsProofs.prove_case_thms
- config new_type_names [descr] sorts reccomb_names rec_thms thy3;
- val (split_thms, thy5) = DatatypeAbsProofs.prove_split_thms
- config new_type_names [descr] sorts inject distinct casedist_thms case_thms thy4;
- val (nchotomys, thy6) = DatatypeAbsProofs.prove_nchotomys config new_type_names
- [descr] sorts casedist_thms thy5;
- val (case_congs, thy7) = DatatypeAbsProofs.prove_case_congs new_type_names
- [descr] sorts nchotomys case_thms thy6;
- val (weak_case_congs, thy8) = DatatypeAbsProofs.prove_weak_case_congs new_type_names
- [descr] sorts thy7;
-
- val ((_, [induct']), thy10) =
- thy8
- |> store_thmss "inject" new_type_names inject
- ||>> store_thmss "distinct" new_type_names distinct
- ||> Sign.add_path (space_implode "_" new_type_names)
- ||>> PureThy.add_thms [((Binding.name "induct", induct), [case_names_induct])];
- val inducts = Project_Rule.projections (ProofContext.init thy10) induct';
-
- val dt_infos = map (make_dt_info alt_names descr sorts (inducts, induct') reccomb_names rec_thms)
- ((0 upto length descr - 1) ~~ descr ~~ case_names ~~ case_thms ~~ casedist_thms ~~
- map FewConstrs distinct ~~ inject ~~ split_thms ~~ nchotomys ~~ case_congs ~~ weak_case_congs);
-
- val simps = flat (distinct @ inject @ case_thms) @ rec_thms;
- val dt_names = map fst dt_infos;
-
- val thy11 =
- thy10
- |> add_case_tr' case_names
- |> add_rules simps case_thms rec_thms inject distinct
- weak_case_congs (Simplifier.attrib (op addcongs))
- |> put_dt_infos dt_infos
- |> add_cases_induct dt_infos inducts
- |> Sign.parent_path
- |> store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms)
- |> snd
- |> DatatypeInterpretation.data (config, dt_names);
- in (dt_names, thy11) end;
-
-fun gen_rep_datatype prep_term (config : config) after_qed alt_names raw_ts thy =
- let
- fun constr_of_term (Const (c, T)) = (c, T)
- | constr_of_term t =
- error ("Not a constant: " ^ Syntax.string_of_term_global thy t);
- fun no_constr (c, T) = error ("Bad constructor: "
- ^ Sign.extern_const thy c ^ "::"
- ^ Syntax.string_of_typ_global thy T);
- fun type_of_constr (cT as (_, T)) =
- let
- val frees = OldTerm.typ_tfrees T;
- val (tyco, vs) = ((apsnd o map) (dest_TFree) o dest_Type o snd o strip_type) T
- handle TYPE _ => no_constr cT
- val _ = if has_duplicates (eq_fst (op =)) vs then no_constr cT else ();
- val _ = if length frees <> length vs then no_constr cT else ();
- in (tyco, (vs, cT)) end;
-
- val raw_cs = AList.group (op =) (map (type_of_constr o constr_of_term o prep_term thy) raw_ts);
- val _ = case map_filter (fn (tyco, _) =>
- if Symtab.defined (get_all thy) tyco then SOME tyco else NONE) raw_cs
- of [] => ()
- | tycos => error ("Type(s) " ^ commas (map quote tycos)
- ^ " already represented inductivly");
- val raw_vss = maps (map (map snd o fst) o snd) raw_cs;
- val ms = case distinct (op =) (map length raw_vss)
- of [n] => 0 upto n - 1
- | _ => error ("Different types in given constructors");
- fun inter_sort m = map (fn xs => nth xs m) raw_vss
- |> Library.foldr1 (Sorts.inter_sort (Sign.classes_of thy))
- val sorts = map inter_sort ms;
- val vs = Name.names Name.context Name.aT sorts;
-
- fun norm_constr (raw_vs, (c, T)) = (c, map_atyps
- (TFree o (the o AList.lookup (op =) (map fst raw_vs ~~ vs)) o fst o dest_TFree) T);
-
- val cs = map (apsnd (map norm_constr)) raw_cs;
- val dtyps_of_typ = map (dtyp_of_typ (map (rpair (map fst vs) o fst) cs))
- o fst o strip_type;
- val new_type_names = map Long_Name.base_name (the_default (map fst cs) alt_names);
-
- fun mk_spec (i, (tyco, constr)) = (i, (tyco,
- map (DtTFree o fst) vs,
- (map o apsnd) dtyps_of_typ constr))
- val descr = map_index mk_spec cs;
- val injs = DatatypeProp.make_injs [descr] vs;
- val half_distincts = map snd (DatatypeProp.make_distincts [descr] vs);
- val ind = DatatypeProp.make_ind [descr] vs;
- val rules = (map o map o map) Logic.close_form [[[ind]], injs, half_distincts];
-
- fun after_qed' raw_thms =
- let
- val [[[induct]], injs, half_distincts] =
- unflat rules (map Drule.zero_var_indexes_list raw_thms);
- (*FIXME somehow dubious*)
- in
- ProofContext.theory_result
- (prove_rep_datatype config alt_names new_type_names descr vs induct injs half_distincts)
- #-> after_qed
- end;
- in
- thy
- |> ProofContext.init
- |> Proof.theorem_i NONE after_qed' ((map o map) (rpair []) (flat rules))
- end;
-
-val rep_datatype = gen_rep_datatype Sign.cert_term;
-val rep_datatype_cmd = gen_rep_datatype Syntax.read_term_global default_config (K I);
-
-
-
-(******************************** add datatype ********************************)
-
-fun gen_add_datatype prep_typ (config : config) new_type_names dts thy =
+fun gen_add_datatype prep_typ config new_type_names dts thy =
let
val _ = Theory.requires thy "Datatype" "datatype definitions";
@@ -588,7 +594,7 @@
val case_names_exhausts = mk_case_names_exhausts descr' (map #1 new_dts);
in
add_datatype_def
- (config : config) new_type_names descr sorts types_syntax constr_syntax dt_info
+ config new_type_names descr sorts types_syntax constr_syntax dt_info
case_names_induct case_names_exhausts thy
end;
@@ -596,7 +602,6 @@
val datatype_cmd = snd ooo gen_add_datatype read_typ default_config;
-
(** package setup **)
(* setup theory *)
@@ -607,7 +612,6 @@
trfun_setup #>
DatatypeInterpretation.init;
-
(* outer syntax *)
local
@@ -642,31 +646,5 @@
end;
-
-(* document antiquotation *)
-
-val _ = ThyOutput.antiquotation "datatype" Args.tyname
- (fn {source = src, context = ctxt, ...} => fn dtco =>
- let
- val thy = ProofContext.theory_of ctxt;
- val (vs, cos) = the_spec thy dtco;
- val ty = Type (dtco, map TFree vs);
- fun pretty_typ_bracket (ty as Type (_, _ :: _)) =
- Pretty.enclose "(" ")" [Syntax.pretty_typ ctxt ty]
- | pretty_typ_bracket ty =
- Syntax.pretty_typ ctxt ty;
- fun pretty_constr (co, tys) =
- (Pretty.block o Pretty.breaks)
- (Syntax.pretty_term ctxt (Const (co, tys ---> ty)) ::
- map pretty_typ_bracket tys);
- val pretty_datatype =
- Pretty.block
- (Pretty.command "datatype" :: Pretty.brk 1 ::
- Syntax.pretty_typ ctxt ty ::
- Pretty.str " =" :: Pretty.brk 1 ::
- flat (separate [Pretty.brk 1, Pretty.str "| "]
- (map (single o pretty_constr) cos)));
- in ThyOutput.output (ThyOutput.maybe_pretty_source (K pretty_datatype) src [()]) end);
-
end;