# HG changeset patch # User haftmann # Date 1254124052 -7200 # Node ID 866cebde3fcaf8ee5fe2f7ea8a48e721cd6142fa # Parent 9b014e62b716d22dccf80800473c0262f5b68575# Parent ad04cda866beabc79334c268386bc5bdca789e1b merged diff -r 9b014e62b716 -r 866cebde3fca src/HOL/Tools/Datatype/datatype.ML --- 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; diff -r 9b014e62b716 -r 866cebde3fca src/HOL/Tools/Datatype/datatype_aux.ML --- a/src/HOL/Tools/Datatype/datatype_aux.ML Sun Sep 27 22:25:13 2009 +0200 +++ b/src/HOL/Tools/Datatype/datatype_aux.ML Mon Sep 28 09:47:32 2009 +0200 @@ -191,18 +191,18 @@ alt_names : string list option, descr : descr, sorts : (string * sort) list, + inject : thm list, + distinct : simproc_dist, + inducts : thm list * thm, + exhaust : thm, + nchotomy : thm, rec_names : string list, rec_rewrites : thm list, case_name : string, case_rewrites : thm list, - inducts : thm list * thm, - exhaust : thm, - distinct : simproc_dist, - inject : thm list, - splits : thm * thm, - nchotomy : thm, case_cong : thm, - weak_case_cong : thm}; + weak_case_cong : thm, + splits : thm * thm}; fun mk_Free s T i = Free (s ^ (string_of_int i), T);