1.1 --- a/src/HOL/Tools/Datatype/datatype.ML Tue Jun 23 15:32:34 2009 +0200
1.2 +++ b/src/HOL/Tools/Datatype/datatype.ML Tue Jun 23 16:27:12 2009 +0200
1.3 @@ -14,16 +14,16 @@
1.4 val rep_datatype : config -> (string list -> Proof.context -> Proof.context)
1.5 -> string list option -> term list -> theory -> Proof.state
1.6 val rep_datatype_cmd : string list option -> string list -> theory -> Proof.state
1.7 - val get_datatypes : theory -> info Symtab.table
1.8 - val get_datatype : theory -> string -> info option
1.9 - val the_datatype : theory -> string -> info
1.10 - val datatype_of_constr : theory -> string -> info option
1.11 - val datatype_of_case : theory -> string -> info option
1.12 - val the_datatype_spec : theory -> string -> (string * sort) list * (string * typ list) list
1.13 - val the_datatype_descr : theory -> string list
1.14 + val get_info : theory -> string -> info option
1.15 + val the_info : theory -> string -> info
1.16 + val the_descr : theory -> string list
1.17 -> descr * (string * sort) list * string list
1.18 * (string list * string list) * (typ list * typ list)
1.19 - val get_datatype_constrs : theory -> string -> (string * typ) list option
1.20 + val the_spec : theory -> string -> (string * sort) list * (string * typ list) list
1.21 + val get_constrs : theory -> string -> (string * typ) list option
1.22 + val get_all : theory -> info Symtab.table
1.23 + val info_of_constr : theory -> string -> info option
1.24 + val info_of_case : theory -> string -> info option
1.25 val interpretation : (config -> string list -> theory -> theory) -> theory -> theory
1.26 val distinct_simproc : simproc
1.27 val make_case : Proof.context -> bool -> string list -> term ->
1.28 @@ -61,7 +61,7 @@
1.29 cases = Symtab.merge (K true) (cases1, cases2)};
1.30 );
1.31
1.32 -val get_datatypes = #types o DatatypesData.get;
1.33 +val get_all = #types o DatatypesData.get;
1.34 val map_datatypes = DatatypesData.map;
1.35
1.36
1.37 @@ -77,23 +77,23 @@
1.38 (map (fn (_, info as {case_name, ...}) => (case_name, info)) dt_infos)
1.39 cases});
1.40
1.41 -val get_datatype = Symtab.lookup o get_datatypes;
1.42 +val get_info = Symtab.lookup o get_all;
1.43
1.44 -fun the_datatype thy name = (case get_datatype thy name of
1.45 +fun the_info thy name = (case get_info thy name of
1.46 SOME info => info
1.47 | NONE => error ("Unknown datatype " ^ quote name));
1.48
1.49 -val datatype_of_constr = Symtab.lookup o #constrs o DatatypesData.get;
1.50 -val datatype_of_case = Symtab.lookup o #cases o DatatypesData.get;
1.51 +val info_of_constr = Symtab.lookup o #constrs o DatatypesData.get;
1.52 +val info_of_case = Symtab.lookup o #cases o DatatypesData.get;
1.53
1.54 -fun get_datatype_descr thy dtco =
1.55 - get_datatype thy dtco
1.56 +fun get_info_descr thy dtco =
1.57 + get_info thy dtco
1.58 |> Option.map (fn info as { descr, index, ... } =>
1.59 (info, (((fn SOME (_, dtys, cos) => (dtys, cos)) o AList.lookup (op =) descr) index)));
1.60
1.61 -fun the_datatype_spec thy dtco =
1.62 +fun the_spec thy dtco =
1.63 let
1.64 - val info as { descr, index, sorts = raw_sorts, ... } = the_datatype thy dtco;
1.65 + val info as { descr, index, sorts = raw_sorts, ... } = the_info thy dtco;
1.66 val SOME (_, dtys, raw_cos) = AList.lookup (op =) descr index;
1.67 val sorts = map ((fn v => (v, (the o AList.lookup (op =) raw_sorts) v))
1.68 o DatatypeAux.dest_DtTFree) dtys;
1.69 @@ -101,9 +101,9 @@
1.70 (fn (co, tys) => (co, map (DatatypeAux.typ_of_dtyp descr sorts) tys)) raw_cos;
1.71 in (sorts, cos) end;
1.72
1.73 -fun the_datatype_descr thy (raw_tycos as raw_tyco :: _) =
1.74 +fun the_descr thy (raw_tycos as raw_tyco :: _) =
1.75 let
1.76 - val info = the_datatype thy raw_tyco;
1.77 + val info = the_info thy raw_tyco;
1.78 val descr = #descr info;
1.79
1.80 val SOME (_, dtys, raw_cos) = AList.lookup (op =) descr (#index info);
1.81 @@ -129,8 +129,8 @@
1.82
1.83 in (descr, vs, tycos, (names, auxnames), (Ts, Us)) end;
1.84
1.85 -fun get_datatype_constrs thy dtco =
1.86 - case try (the_datatype_spec thy) dtco
1.87 +fun get_constrs thy dtco =
1.88 + case try (the_spec thy) dtco
1.89 of SOME (sorts, cos) =>
1.90 let
1.91 fun subst (v, sort) = TVar ((v, 0), sort);
1.92 @@ -216,7 +216,7 @@
1.93
1.94 val distinctN = "constr_distinct";
1.95
1.96 -fun distinct_rule thy ss tname eq_t = case #distinct (the_datatype thy tname) of
1.97 +fun distinct_rule thy ss tname eq_t = case #distinct (the_info thy tname) of
1.98 FewConstrs thms => Goal.prove (Simplifier.the_context ss) [] [] eq_t (K
1.99 (EVERY [rtac eq_reflection 1, rtac iffI 1, rtac notE 1,
1.100 atac 2, resolve_tac thms 1, etac FalseE 1]))
1.101 @@ -240,7 +240,7 @@
1.102 (case (stripT (0, T1), stripT (0, T2)) of
1.103 ((i', Type (tname1, _)), (j', Type (tname2, _))) =>
1.104 if tname1 = tname2 andalso not (cname1 = cname2) andalso i = i' andalso j = j' then
1.105 - (case (get_datatype_descr thy) tname1 of
1.106 + (case (get_info_descr thy) tname1 of
1.107 SOME (_, (_, constrs)) => let val cnames = map fst constrs
1.108 in if cname1 mem cnames andalso cname2 mem cnames then
1.109 SOME (distinct_rule thy ss tname1
1.110 @@ -265,21 +265,21 @@
1.111 (**** translation rules for case ****)
1.112
1.113 fun make_case ctxt = DatatypeCase.make_case
1.114 - (datatype_of_constr (ProofContext.theory_of ctxt)) ctxt;
1.115 + (info_of_constr (ProofContext.theory_of ctxt)) ctxt;
1.116
1.117 fun strip_case ctxt = DatatypeCase.strip_case
1.118 - (datatype_of_case (ProofContext.theory_of ctxt));
1.119 + (info_of_case (ProofContext.theory_of ctxt));
1.120
1.121 fun add_case_tr' case_names thy =
1.122 Sign.add_advanced_trfuns ([], [],
1.123 map (fn case_name =>
1.124 let val case_name' = Sign.const_syntax_name thy case_name
1.125 - in (case_name', DatatypeCase.case_tr' datatype_of_case case_name')
1.126 + in (case_name', DatatypeCase.case_tr' info_of_case case_name')
1.127 end) case_names, []) thy;
1.128
1.129 val trfun_setup =
1.130 Sign.add_advanced_trfuns ([],
1.131 - [("_case_syntax", DatatypeCase.case_tr true datatype_of_constr)],
1.132 + [("_case_syntax", DatatypeCase.case_tr true info_of_constr)],
1.133 [], []);
1.134
1.135
1.136 @@ -395,7 +395,7 @@
1.137 | get_typ t = err t;
1.138 val dtnames = map get_typ (HOLogic.dest_conj (HOLogic.dest_Trueprop (Thm.concl_of induct')));
1.139
1.140 - val dt_info = get_datatypes thy;
1.141 + val dt_info = get_all thy;
1.142
1.143 val distinct = (map o maps) (fn thm => [thm, thm RS not_sym]) half_distinct;
1.144 val (case_names_induct, case_names_exhausts) =
1.145 @@ -466,7 +466,7 @@
1.146
1.147 val raw_cs = AList.group (op =) (map (type_of_constr o constr_of_term o prep_term thy) raw_ts);
1.148 val _ = case map_filter (fn (tyco, _) =>
1.149 - if Symtab.defined (get_datatypes thy) tyco then SOME tyco else NONE) raw_cs
1.150 + if Symtab.defined (get_all thy) tyco then SOME tyco else NONE) raw_cs
1.151 of [] => ()
1.152 | tycos => error ("Type(s) " ^ commas (map quote tycos)
1.153 ^ " already represented inductivly");
1.154 @@ -576,7 +576,7 @@
1.155 val (dts', constr_syntax, sorts', i) =
1.156 fold prep_dt_spec (dts ~~ new_type_names) ([], [], [], 0);
1.157 val sorts = sorts' @ (map (rpair (Sign.defaultS tmp_thy)) (tyvars \\ map fst sorts'));
1.158 - val dt_info = get_datatypes thy;
1.159 + val dt_info = get_all thy;
1.160 val (descr, _) = unfold_datatypes tmp_thy dts' sorts dt_info dts' i;
1.161 val _ = check_nonempty descr handle (exn as Datatype_Empty s) =>
1.162 if #strict config then error ("Nonemptiness check failed for datatype " ^ s)
1.163 @@ -648,7 +648,7 @@
1.164 (fn {source = src, context = ctxt, ...} => fn dtco =>
1.165 let
1.166 val thy = ProofContext.theory_of ctxt;
1.167 - val (vs, cos) = the_datatype_spec thy dtco;
1.168 + val (vs, cos) = the_spec thy dtco;
1.169 val ty = Type (dtco, map TFree vs);
1.170 fun pretty_typ_bracket (ty as Type (_, _ :: _)) =
1.171 Pretty.enclose "(" ")" [Syntax.pretty_typ ctxt ty]