added DatatypeHooks
authorhaftmann
Tue May 09 10:09:37 2006 +0200 (2006-05-09)
changeset 19599a5c7eb37d14f
parent 19598 d68dd20af31f
child 19600 2d969d9a233b
added DatatypeHooks
src/HOL/Inductive.thy
src/HOL/Tools/datatype_codegen.ML
src/HOL/Tools/datatype_hooks.ML
src/HOL/Tools/datatype_package.ML
     1.1 --- a/src/HOL/Inductive.thy	Tue May 09 10:09:17 2006 +0200
     1.2 +++ b/src/HOL/Inductive.thy	Tue May 09 10:09:37 2006 +0200
     1.3 @@ -16,6 +16,7 @@
     1.4    ("Tools/datatype_rep_proofs.ML")
     1.5    ("Tools/datatype_abs_proofs.ML")
     1.6    ("Tools/datatype_realizer.ML")
     1.7 +  ("Tools/datatype_hooks.ML")
     1.8    ("Tools/datatype_package.ML")
     1.9    ("Tools/datatype_codegen.ML")
    1.10    ("Tools/recfun_codegen.ML")
    1.11 @@ -82,6 +83,10 @@
    1.12  use "Tools/datatype_rep_proofs.ML"
    1.13  use "Tools/datatype_abs_proofs.ML"
    1.14  use "Tools/datatype_realizer.ML"
    1.15 +
    1.16 +use "Tools/datatype_hooks.ML"
    1.17 +setup DatatypeHooks.setup
    1.18 +
    1.19  use "Tools/datatype_package.ML"
    1.20  setup DatatypePackage.setup
    1.21  
     2.1 --- a/src/HOL/Tools/datatype_codegen.ML	Tue May 09 10:09:17 2006 +0200
     2.2 +++ b/src/HOL/Tools/datatype_codegen.ML	Tue May 09 10:09:37 2006 +0200
     2.3 @@ -9,9 +9,7 @@
     2.4  sig
     2.5    val get_datatype_spec_thms: theory -> string
     2.6      -> (((string * sort) list * (string * typ list) list) * tactic) option
     2.7 -  val get_case_const_data: theory -> string -> (string * int) list option
     2.8    val get_all_datatype_cons: theory -> (string * string) list
     2.9 -  val get_datatype_case_consts: theory -> string list
    2.10    val setup: theory -> theory
    2.11  end;
    2.12  
    2.13 @@ -331,17 +329,13 @@
    2.14        ((snd o the oo DatatypePackage.get_datatype_spec) thy dtco))
    2.15          (DatatypePackage.get_datatypes thy) [];
    2.16  
    2.17 -fun get_case_const_data thy c =
    2.18 -  case find_first (fn (_, {index, descr, case_name, ...}) =>
    2.19 -      case_name = c
    2.20 -    ) ((Symtab.dest o DatatypePackage.get_datatypes) thy)
    2.21 -   of NONE => NONE
    2.22 -    | SOME (_, {index, descr, ...}) =>
    2.23 -        (SOME o map (apsnd length) o #3 o the o AList.lookup (op =) descr) index;
    2.24 -
    2.25 -fun get_datatype_case_consts thy =
    2.26 -  Symtab.fold (fn (_, {case_name, ...}) => cons case_name)
    2.27 -    (DatatypePackage.get_datatypes thy) [];
    2.28 +fun add_datatype_case_const dtco thy =
    2.29 +  let
    2.30 +    val {case_name, index, descr, ...} = DatatypePackage.the_datatype thy dtco
    2.31 +  in
    2.32 +    CodegenPackage.add_case_const case_name
    2.33 +      ((map (apsnd length) o #3 o the o AList.lookup (op =) descr) index) thy
    2.34 +  end;
    2.35  
    2.36  val setup = 
    2.37    add_codegen "datatype" datatype_codegen #>
    2.38 @@ -352,8 +346,6 @@
    2.39      DatatypePackage.get_datatype_spec #>
    2.40    CodegenPackage.set_get_all_datatype_cons
    2.41      get_all_datatype_cons #>
    2.42 -  CodegenPackage.ensure_datatype_case_consts
    2.43 -    get_datatype_case_consts
    2.44 -    get_case_const_data;
    2.45 +  DatatypeHooks.add add_datatype_case_const
    2.46  
    2.47  end;
     3.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     3.2 +++ b/src/HOL/Tools/datatype_hooks.ML	Tue May 09 10:09:37 2006 +0200
     3.3 @@ -0,0 +1,55 @@
     3.4 +(*  Title:      HOL/Tools/datatype_hooks.ML
     3.5 +    ID:         $Id$
     3.6 +    Author:     Florian Haftmann, TU Muenchen
     3.7 +
     3.8 +Hooks for datatype introduction.
     3.9 +*)
    3.10 +
    3.11 +signature DATATYPE_HOOKS =
    3.12 +sig
    3.13 +  type hook = string -> theory -> theory;
    3.14 +  val add: hook -> theory -> theory;
    3.15 +  val invoke: hook;
    3.16 +  val setup: theory -> theory;
    3.17 +end;
    3.18 +
    3.19 +structure DatatypeHooks : DATATYPE_HOOKS =
    3.20 +struct
    3.21 +
    3.22 +
    3.23 +(* theory data *)
    3.24 +
    3.25 +type hook = string -> theory -> theory;
    3.26 +datatype T = T of (serial * hook) list;
    3.27 +
    3.28 +fun map_T f (T hooks) = T (f hooks);
    3.29 +fun merge_T pp (T hooks1, T hooks2) =
    3.30 +  T (AList.merge (op =) (K true) (hooks1, hooks2));
    3.31 +
    3.32 +structure DatatypeHooksData = TheoryDataFun
    3.33 +(struct
    3.34 +  val name = "HOL/DatatypeHooks";
    3.35 +  type T = T;
    3.36 +  val empty = T [];
    3.37 +  val copy = I;
    3.38 +  val extend = I;
    3.39 +  val merge = merge_T;
    3.40 +  fun print _ _ = ();
    3.41 +end);
    3.42 +
    3.43 +
    3.44 +(* interface *)
    3.45 +
    3.46 +fun add hook =
    3.47 +  DatatypeHooksData.map (map_T (cons (serial (), hook)));
    3.48 +
    3.49 +fun invoke dtco thy =
    3.50 +  fold (fn (_, f) => f dtco) ((fn T hooks => hooks) (DatatypeHooksData.get thy)) thy;
    3.51 +
    3.52 +
    3.53 +(* theory setup *)
    3.54 +
    3.55 +val setup = DatatypeHooksData.init;
    3.56 +
    3.57 +end;
    3.58 +
     4.1 --- a/src/HOL/Tools/datatype_package.ML	Tue May 09 10:09:17 2006 +0200
     4.2 +++ b/src/HOL/Tools/datatype_package.ML	Tue May 09 10:09:37 2006 +0200
     4.3 @@ -139,14 +139,6 @@
     4.4          in SOME (map mk_co cos) end
     4.5      | NONE => NONE;
     4.6  
     4.7 -fun get_case_const_data thy c =
     4.8 -  case find_first (fn (_, {index, descr, case_name, ...}) =>
     4.9 -      case_name = c
    4.10 -    ) ((Symtab.dest o get_datatypes) thy)
    4.11 -   of NONE => NONE
    4.12 -    | SOME (_, {index, descr, ...}) =>
    4.13 -        (SOME o map (apsnd length) o #3 o the o AList.lookup (op =) descr) index;
    4.14 -
    4.15  fun find_tname var Bi =
    4.16    let val frees = map dest_Free (term_frees Bi)
    4.17        val params = rename_wrt_term Bi (Logic.strip_params Bi);
    4.18 @@ -717,9 +709,10 @@
    4.19        |> put_datatypes (fold Symtab.update dt_infos dt_info)
    4.20        |> add_cases_induct dt_infos induct
    4.21        |> Theory.parent_path
    4.22 -      |> store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms) |> snd
    4.23 +      |> store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms)
    4.24 +      |> snd
    4.25        |> DatatypeRealizer.add_dt_realizers sorts (map snd dt_infos)
    4.26 -      |> fold (CodegenPackage.add_case_const_i get_case_const_data) case_names';
    4.27 +      |> fold (DatatypeHooks.invoke o fst) dt_infos;
    4.28    in
    4.29      ({distinct = distinct,
    4.30        inject = inject,
    4.31 @@ -778,7 +771,7 @@
    4.32        |> Theory.parent_path
    4.33        |> store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms) |> snd
    4.34        |> DatatypeRealizer.add_dt_realizers sorts (map snd dt_infos)
    4.35 -      |> fold (CodegenPackage.add_case_const_i get_case_const_data) case_names;
    4.36 +      |> fold (DatatypeHooks.invoke o fst) dt_infos;
    4.37    in
    4.38      ({distinct = distinct,
    4.39        inject = inject,
    4.40 @@ -876,15 +869,18 @@
    4.41  
    4.42      val simps = List.concat (distinct @ inject @ case_thms) @ size_thms @ rec_thms;
    4.43  
    4.44 -    val thy11 = thy10 |>
    4.45 -      Theory.add_advanced_trfuns ([], [], make_case_tr' case_names descr, []) |>
    4.46 -      add_rules simps case_thms size_thms rec_thms inject distinct
    4.47 -        weak_case_congs (Simplifier.attrib (op addcongs)) |> 
    4.48 -      put_datatypes (fold Symtab.update dt_infos dt_info) |>
    4.49 -      add_cases_induct dt_infos induction' |>
    4.50 -      Theory.parent_path |>
    4.51 -      (snd o store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms)) |>
    4.52 -      DatatypeRealizer.add_dt_realizers sorts (map snd dt_infos);
    4.53 +    val thy11 =
    4.54 +      thy10
    4.55 +      |> Theory.add_advanced_trfuns ([], [], make_case_tr' case_names descr, [])
    4.56 +      |> add_rules simps case_thms size_thms rec_thms inject distinct
    4.57 +           weak_case_congs (Simplifier.attrib (op addcongs))
    4.58 +      |> put_datatypes (fold Symtab.update dt_infos dt_info)
    4.59 +      |> add_cases_induct dt_infos induction'
    4.60 +      |> Theory.parent_path
    4.61 +      |> store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms)
    4.62 +      |> snd
    4.63 +      |> DatatypeRealizer.add_dt_realizers sorts (map snd dt_infos)
    4.64 +      |> fold (DatatypeHooks.invoke o fst) dt_infos;
    4.65    in
    4.66      ({distinct = distinct,
    4.67        inject = inject,