proper context for resolve_tac, eresolve_tac, dresolve_tac, forward_tac etc.;
occasionally clarified use of context;
(* Title: HOL/Tools/Old_Datatype/old_datatype_data.ML
Author: Stefan Berghofer, TU Muenchen
Datatype package bookkeeping.
*)
signature OLD_DATATYPE_DATA =
sig
include OLD_DATATYPE_COMMON
val get_all : theory -> info Symtab.table
val get_info : theory -> string -> info option
val the_info : theory -> string -> info
val info_of_constr : theory -> string * typ -> info option
val info_of_constr_permissive : theory -> string * typ -> info option
val info_of_case : theory -> string -> info option
val register: (string * info) list -> theory -> theory
val the_spec : theory -> string -> (string * sort) list * (string * typ list) list
val the_descr : theory -> string list ->
descr * (string * sort) list * string list * string *
(string list * string list) * (typ list * typ list)
val all_distincts : theory -> typ list -> thm list list
val get_constrs : theory -> string -> (string * typ) list option
val mk_case_names_induct: descr -> attribute
val mk_case_names_exhausts: descr -> string list -> attribute list
val interpretation : (config -> string list -> theory -> theory) -> theory -> theory
val interpretation_data : config * string list -> theory -> theory
end;
structure Old_Datatype_Data: OLD_DATATYPE_DATA =
struct
(** theory data **)
(* data management *)
structure Data = Theory_Data
(
type T =
{types: Old_Datatype_Aux.info Symtab.table,
constrs: (string * Old_Datatype_Aux.info) list Symtab.table,
cases: Old_Datatype_Aux.info Symtab.table};
val empty =
{types = Symtab.empty, constrs = Symtab.empty, cases = Symtab.empty};
val extend = I;
fun merge
({types = types1, constrs = constrs1, cases = cases1},
{types = types2, constrs = constrs2, cases = cases2}) : T =
{types = Symtab.merge (K true) (types1, types2),
constrs = Symtab.join (K (AList.merge (op =) (K true))) (constrs1, constrs2),
cases = Symtab.merge (K true) (cases1, cases2)};
);
val get_all = #types o Data.get;
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 old-style datatype " ^ quote name));
fun info_of_constr thy (c, T) =
let
val tab = Symtab.lookup_list (#constrs (Data.get thy)) c;
in
(case body_type T of
Type (tyco, _) => AList.lookup (op =) tab tyco
| _ => NONE)
end;
fun info_of_constr_permissive thy (c, T) =
let
val tab = Symtab.lookup_list (#constrs (Data.get thy)) c;
val hint = (case body_type T of Type (tyco, _) => SOME tyco | _ => NONE);
val default = if null tab then NONE else SOME (snd (List.last tab));
(*conservative wrt. overloaded constructors*)
in
(case hint of
NONE => default
| SOME tyco =>
(case AList.lookup (op =) tab tyco of
NONE => default (*permissive*)
| SOME info => SOME info))
end;
val info_of_case = Symtab.lookup o #cases o Data.get;
fun ctrs_of_exhaust exhaust =
Logic.strip_imp_prems (prop_of exhaust) |>
map (head_of o snd o HOLogic.dest_eq o HOLogic.dest_Trueprop o the_single
o Logic.strip_assums_hyp);
fun case_of_case_rewrite case_rewrite =
head_of (fst (HOLogic.dest_eq (HOLogic.dest_Trueprop (prop_of case_rewrite))));
fun ctr_sugar_of_info ({exhaust, nchotomy, inject, distinct, case_rewrites, case_cong,
case_cong_weak, split, split_asm, ...} : Old_Datatype_Aux.info) =
let val ctrs as ctr1 :: _ = ctrs_of_exhaust exhaust in
{kind = Ctr_Sugar.Datatype,
T = body_type (fastype_of ctr1),
ctrs = ctrs,
casex = case_of_case_rewrite (hd case_rewrites),
discs = [],
selss = [],
exhaust = exhaust,
nchotomy = nchotomy,
injects = inject,
distincts = distinct,
case_thms = case_rewrites,
case_cong = case_cong,
case_cong_weak = case_cong_weak,
case_distribs = [],
split = split,
split_asm = split_asm,
disc_defs = [],
disc_thmss = [],
discIs = [],
disc_eq_cases = [],
sel_defs = [],
sel_thmss = [],
distinct_discsss = [],
exhaust_discs = [],
exhaust_sels = [],
collapses = [],
expands = [],
split_sels = [],
split_sel_asms = [],
case_eq_ifs = []}
end;
fun register dt_infos =
Data.map (fn {types, constrs, cases} =>
{types = types |> fold Symtab.update dt_infos,
constrs = constrs |> fold (fn (constr, dtname_info) =>
Symtab.map_default (constr, []) (cons dtname_info))
(maps (fn (dtname, info as {descr, index, ...}) =>
map (rpair (dtname, info) o fst) (#3 (the (AList.lookup op = descr index)))) dt_infos),
cases = cases |> fold Symtab.update
(map (fn (_, info as {case_name, ...}) => (case_name, info)) dt_infos)}) #>
fold (Ctr_Sugar.default_register_ctr_sugar_global (K true) o ctr_sugar_of_info o snd) dt_infos;
(* complex queries *)
fun the_spec thy dtco =
let
val {descr, index, ...} = the_info thy dtco;
val (_, dtys, raw_cos) = the (AList.lookup (op =) descr index);
val args = map Old_Datatype_Aux.dest_DtTFree dtys;
val cos = map (fn (co, tys) => (co, map (Old_Datatype_Aux.typ_of_dtyp descr) tys)) raw_cos;
in (args, cos) end;
fun the_descr thy (raw_tycos as raw_tyco :: _) =
let
val info = the_info thy raw_tyco;
val descr = #descr info;
val (_, dtys, _) = the (AList.lookup (op =) descr (#index info));
val vs = map Old_Datatype_Aux.dest_DtTFree dtys;
fun is_DtTFree (Old_Datatype_Aux.DtTFree _) = true
| is_DtTFree _ = false;
val k = find_index (fn (_, (_, dTs, _)) => not (forall is_DtTFree dTs)) descr;
val protoTs as (dataTs, _) =
chop k descr
|> (apply2 o map)
(fn (_, (tyco, dTs, _)) => (tyco, map (Old_Datatype_Aux.typ_of_dtyp descr) dTs));
val tycos = map fst dataTs;
val _ =
if eq_set (op =) (tycos, raw_tycos) then ()
else
error ("Type constructors " ^ commas_quote raw_tycos ^
" do not belong exhaustively to one mutually recursive old-style datatype");
val (Ts, Us) = apply2 (map Type) protoTs;
val names = map Long_Name.base_name tycos;
val (auxnames, _) =
Name.make_context names
|> fold_map (Name.variant o Old_Datatype_Aux.name_of_typ) Us;
val prefix = space_implode "_" names;
in (descr, vs, tycos, prefix, (names, auxnames), (Ts, Us)) end;
fun all_distincts thy Ts =
let
fun add_tycos (Type (tyco, Ts)) = insert (op =) tyco #> fold add_tycos Ts
| add_tycos _ = I;
val tycos = fold add_tycos Ts [];
in map_filter (Option.map #distinct o get_info thy) tycos end;
fun get_constrs thy dtco =
(case try (the_spec thy) dtco of
SOME (args, cos) =>
let
fun subst (v, sort) = TVar ((v, 0), sort);
fun subst_ty (TFree v) = subst v
| subst_ty ty = ty;
val dty = Type (dtco, map subst args);
fun mk_co (co, tys) = (co, map (Term.map_atyps subst_ty) tys ---> dty);
in SOME (map mk_co cos) end
| NONE => NONE);
(** various auxiliary **)
(* case names *)
local
fun dt_recs (Old_Datatype_Aux.DtTFree _) = []
| dt_recs (Old_Datatype_Aux.DtType (_, dts)) = maps dt_recs dts
| dt_recs (Old_Datatype_Aux.DtRec i) = [i];
fun dt_cases (descr: Old_Datatype_Aux.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 =
Old_Datatype_Prop.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 = Rule_Cases.case_names (induct_cases descr);
fun mk_case_names_exhausts descr new =
map (Rule_Cases.case_names o exhaust_cases descr o #1)
(filter (fn ((_, (name, _, _))) => member (op =) new name) descr);
end;
(** abstract theory extensions relative to a datatype characterisation **)
structure Old_Datatype_Plugin = Plugin(type T = Old_Datatype_Aux.config * string list);
val old_datatype_plugin = Plugin_Name.declare_setup @{binding old_datatype};
fun interpretation f =
Old_Datatype_Plugin.interpretation old_datatype_plugin
(fn (config, type_names as name :: _) =>
Local_Theory.background_theory (fn thy =>
thy
|> Sign.root_path
|> Sign.add_path (Long_Name.qualifier name)
|> f config type_names
|> Sign.restore_naming thy));
val interpretation_data = Named_Target.theory_map o Old_Datatype_Plugin.data_default;
open Old_Datatype_Aux;
end;