hooks now take string list as arguments (mutual datatypes); some nice combinators in datatype_codegen
authorhaftmann
Fri Jul 21 14:47:22 2006 +0200 (2006-07-21)
changeset 201770af885e3dabf
parent 20176 36737fb58614
child 20178 e56fa3c8b1f1
hooks now take string list as arguments (mutual datatypes); some nice combinators in datatype_codegen
src/HOL/Tools/datatype_codegen.ML
src/HOL/Tools/datatype_hooks.ML
src/HOL/Tools/datatype_package.ML
     1.1 --- a/src/HOL/Tools/datatype_codegen.ML	Fri Jul 21 14:46:27 2006 +0200
     1.2 +++ b/src/HOL/Tools/datatype_codegen.ML	Fri Jul 21 14:47:22 2006 +0200
     1.3 @@ -11,9 +11,17 @@
     1.4      -> (((string * sort) list * (string * typ list) list) * tactic) option
     1.5    val get_all_datatype_cons: theory -> (string * string) list
     1.6    val dest_case_expr: theory -> term
     1.7 -    -> ((string * typ) list * ((term * typ) * (term * term) list)) option;
     1.8 +    -> ((string * typ) list * ((term * typ) * (term * term) list)) option
     1.9    val add_datatype_case_const: string -> theory -> theory
    1.10    val add_datatype_case_defs: string -> theory -> theory
    1.11 +  val datatypes_dependency: theory -> string list list
    1.12 +  val get_datatype_mut_specs: theory -> string list
    1.13 +    -> ((string * sort) list * (string * (string * typ list) list) list)
    1.14 +  val get_datatype_arities: theory -> string list -> sort
    1.15 +    -> (string * (((string * sort list) * sort)  * term list)) list option
    1.16 +  val datatype_prove_arities : tactic -> string list -> sort
    1.17 +    -> ((string * term list) list
    1.18 +    -> ((bstring * attribute list) * term) list) -> theory -> theory
    1.19    val setup: theory -> theory
    1.20  end;
    1.21  
    1.22 @@ -306,13 +314,88 @@
    1.23  
    1.24  (** code 2nd generation **)
    1.25  
    1.26 +fun datatypes_dependency thy =
    1.27 +  let
    1.28 +    val dtnames = DatatypePackage.get_datatypes thy;
    1.29 +    fun add_node (dtname, _) =
    1.30 +      let
    1.31 +        fun add_tycos (Type (tyco, tys)) = insert (op =) tyco #> fold add_tycos tys
    1.32 +          | add_tycos _ = I;
    1.33 +        val deps = (filter (Symtab.defined dtnames) o maps (fn ty =>
    1.34 +          add_tycos ty [])
    1.35 +            o maps snd o snd o the o DatatypePackage.get_datatype_spec thy) dtname
    1.36 +      in
    1.37 +        Graph.default_node (dtname, ())
    1.38 +        #> fold (fn dtname' =>
    1.39 +             Graph.default_node (dtname', ())
    1.40 +             #> Graph.add_edge (dtname', dtname)
    1.41 +           ) deps
    1.42 +      end
    1.43 +  in
    1.44 +    Graph.empty
    1.45 +    |> Symtab.fold add_node dtnames
    1.46 +    |> Graph.strong_conn
    1.47 +  end;
    1.48 +
    1.49 +fun get_datatype_mut_specs thy (tycos as tyco :: _) =
    1.50 +  let
    1.51 +    val tycos' = (map (#1 o snd) o #descr o DatatypePackage.the_datatype thy) tyco;
    1.52 +    val _ = if gen_subset (op =) (tycos, tycos') then () else
    1.53 +      error ("datatype constructors are not mutually recursive: " ^ (commas o map quote) tycos);
    1.54 +    val (vs::_, css) = split_list (map (the o DatatypePackage.get_datatype_spec thy) tycos);
    1.55 +  in (vs, tycos ~~ css) end;
    1.56 +
    1.57 +fun get_datatype_arities thy tycos sort =
    1.58 +  let
    1.59 +    val algebra = Sign.classes_of thy;
    1.60 +    val (vs_proto, css_proto) = get_datatype_mut_specs thy tycos;
    1.61 +    val vs = map (fn (v, vsort) => (v, Sorts.inter_sort algebra (vsort, sort))) vs_proto;
    1.62 +    fun inst_type tyco (c, tys) =
    1.63 +      let
    1.64 +        val tys' = (map o map_atyps)
    1.65 +          (fn TFree (v, _) => TFree (v, the (AList.lookup (op =) vs v))) tys
    1.66 +      in (c, tys') end;
    1.67 +    val css = map (fn (tyco, cs) => (tyco, (map (inst_type tyco) cs))) css_proto;
    1.68 +    fun mk_arity tyco =
    1.69 +      ((tyco, map snd vs), sort);
    1.70 +    fun typ_of_sort ty =
    1.71 +      let
    1.72 +        val arities = map (fn (tyco, _) => ((tyco, map snd vs), sort)) css;
    1.73 +      in ClassPackage.assume_arities_of_sort thy arities (ty, sort) end;
    1.74 +    fun mk_cons tyco (c, tys) =
    1.75 +      let
    1.76 +        val ts = Name.give_names Name.context "a" tys;
    1.77 +        val ty = tys ---> Type (tyco, map TFree vs);
    1.78 +      in list_comb (Const (c, ty), map Free ts) end;
    1.79 +  in if forall (fn (_, cs) => forall (fn (_, tys) => forall typ_of_sort tys) cs) css
    1.80 +    then SOME (
    1.81 +      map (fn (tyco, cs) => (tyco, (mk_arity tyco, map (mk_cons tyco) cs))) css
    1.82 +    ) else NONE
    1.83 +  end;
    1.84 +
    1.85 +fun datatype_prove_arities tac tycos sort f thy =
    1.86 +  case get_datatype_arities thy tycos sort
    1.87 +   of NONE => thy
    1.88 +    | SOME insts => let
    1.89 +        fun proven ((tyco, asorts), sort) =
    1.90 +          Sorts.of_sort (Sign.classes_of thy)
    1.91 +            (Type (tyco, map TFree (Name.give_names Name.context "'a" asorts)), sort);
    1.92 +        val (arities, css) = (split_list o map_filter
    1.93 +          (fn (tyco, (arity, cs)) => if proven arity
    1.94 +            then SOME (arity, (tyco, cs)) else NONE)) insts;
    1.95 +      in
    1.96 +        thy
    1.97 +        |> ClassPackage.prove_instance_arity tac
    1.98 +             arities ("", []) (f css)
    1.99 +      end;
   1.100 +
   1.101  fun dtyp_of_case_const thy c =
   1.102    get_first (fn (dtco, { case_name, ... }) => if case_name = c then SOME dtco else NONE)
   1.103      ((Symtab.dest o DatatypePackage.get_datatypes) thy);
   1.104  
   1.105  fun dest_case_app cs ts tys =
   1.106    let
   1.107 -    val abs = CodegenThingol.give_names [] (Library.drop (length ts, tys));
   1.108 +    val abs = Name.give_names Name.context "a" (Library.drop (length ts, tys));
   1.109      val (ts', t) = split_last (ts @ map Free abs);
   1.110      val (tys', sty) = split_last tys;
   1.111      fun freenames_of t = fold_aterms
   1.112 @@ -382,7 +465,7 @@
   1.113      get_datatype_spec_thms #>
   1.114    CodegenPackage.set_get_all_datatype_cons
   1.115      get_all_datatype_cons #>
   1.116 -  DatatypeHooks.add add_datatype_case_const #>
   1.117 -  DatatypeHooks.add add_datatype_case_defs
   1.118 +  DatatypeHooks.add (fold add_datatype_case_const) #>
   1.119 +  DatatypeHooks.add (fold add_datatype_case_defs)
   1.120  
   1.121  end;
     2.1 --- a/src/HOL/Tools/datatype_hooks.ML	Fri Jul 21 14:46:27 2006 +0200
     2.2 +++ b/src/HOL/Tools/datatype_hooks.ML	Fri Jul 21 14:47:22 2006 +0200
     2.3 @@ -7,7 +7,7 @@
     2.4  
     2.5  signature DATATYPE_HOOKS =
     2.6  sig
     2.7 -  type hook = string -> theory -> theory;
     2.8 +  type hook = string list -> theory -> theory;
     2.9    val add: hook -> theory -> theory;
    2.10    val invoke: hook;
    2.11    val setup: theory -> theory;
    2.12 @@ -19,7 +19,7 @@
    2.13  
    2.14  (* theory data *)
    2.15  
    2.16 -type hook = string -> theory -> theory;
    2.17 +type hook = string list -> theory -> theory;
    2.18  datatype T = T of (serial * hook) list;
    2.19  
    2.20  fun map_T f (T hooks) = T (f hooks);
    2.21 @@ -43,8 +43,8 @@
    2.22  fun add hook =
    2.23    DatatypeHooksData.map (map_T (cons (serial (), hook)));
    2.24  
    2.25 -fun invoke dtco thy =
    2.26 -  fold (fn (_, f) => f dtco) ((fn T hooks => hooks) (DatatypeHooksData.get thy)) thy;
    2.27 +fun invoke dtcos thy =
    2.28 +  fold (fn (_, f) => f dtcos) ((fn T hooks => hooks) (DatatypeHooksData.get thy)) thy;
    2.29  
    2.30  
    2.31  (* theory setup *)
     3.1 --- a/src/HOL/Tools/datatype_package.ML	Fri Jul 21 14:46:27 2006 +0200
     3.2 +++ b/src/HOL/Tools/datatype_package.ML	Fri Jul 21 14:47:22 2006 +0200
     3.3 @@ -723,7 +723,7 @@
     3.4        |> store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms)
     3.5        |> snd
     3.6        |> DatatypeRealizer.add_dt_realizers sorts (map snd dt_infos)
     3.7 -      |> fold (DatatypeHooks.invoke o fst) dt_infos;
     3.8 +      |> DatatypeHooks.invoke (map fst dt_infos);
     3.9    in
    3.10      ({distinct = distinct,
    3.11        inject = inject,
    3.12 @@ -783,7 +783,7 @@
    3.13        |> Theory.parent_path
    3.14        |> store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms) |> snd
    3.15        |> DatatypeRealizer.add_dt_realizers sorts (map snd dt_infos)
    3.16 -      |> fold (DatatypeHooks.invoke o fst) dt_infos;
    3.17 +      |> DatatypeHooks.invoke (map fst dt_infos);
    3.18    in
    3.19      ({distinct = distinct,
    3.20        inject = inject,
    3.21 @@ -893,7 +893,7 @@
    3.22        |> store_thmss "splits" new_type_names (map (fn (x, y) => [x, y]) split_thms)
    3.23        |> snd
    3.24        |> DatatypeRealizer.add_dt_realizers sorts (map snd dt_infos)
    3.25 -      |> fold (DatatypeHooks.invoke o fst) dt_infos;
    3.26 +      |> DatatypeHooks.invoke (map fst dt_infos);
    3.27    in
    3.28      ({distinct = distinct,
    3.29        inject = inject,