--- a/src/HOL/Tools/Datatype/datatype_codegen.ML Mon Nov 30 11:42:48 2009 +0100
+++ b/src/HOL/Tools/Datatype/datatype_codegen.ML Mon Nov 30 11:42:49 2009 +0100
@@ -1,4 +1,4 @@
-(* Title: HOL/Tools/datatype_codegen.ML
+(* Title: HOL/Tools/Datatype/datatype_codegen.ML
Author: Stefan Berghofer and Florian Haftmann, TU Muenchen
Code generator facilities for inductive datatypes.
@@ -6,48 +6,23 @@
signature DATATYPE_CODEGEN =
sig
- include DATATYPE_COMMON
- val find_shortest_path: descr -> int -> (string * int) option
val setup: theory -> theory
end;
-structure DatatypeCodegen : DATATYPE_CODEGEN =
+structure Datatype_Codegen : DATATYPE_CODEGEN =
struct
-open DatatypeAux
-
-(** find shortest path to constructor with no recursive arguments **)
-
-fun find_nonempty (descr: descr) is i =
- let
- val (_, _, constrs) = the (AList.lookup (op =) descr i);
- fun arg_nonempty (_, DatatypeAux.DtRec i) = if member (op =) is i
- then NONE
- else Option.map (Integer.add 1 o snd) (find_nonempty descr (i::is) i)
- | arg_nonempty _ = SOME 0;
- fun max xs = Library.foldl
- (fn (NONE, _) => NONE
- | (SOME i, SOME j) => SOME (Int.max (i, j))
- | (_, NONE) => NONE) (SOME 0, xs);
- val xs = sort (int_ord o pairself snd)
- (map_filter (fn (s, dts) => Option.map (pair s)
- (max (map (arg_nonempty o DatatypeAux.strip_dtyp) dts))) constrs)
- in case xs of [] => NONE | x :: _ => SOME x end;
-
-fun find_shortest_path descr i = find_nonempty descr [i] i;
-
-
(** SML code generator **)
open Codegen;
(* datatype definition *)
-fun add_dt_defs thy defs dep module (descr: descr) sorts gr =
+fun add_dt_defs thy defs dep module descr sorts gr =
let
- val descr' = filter (can (map DatatypeAux.dest_DtTFree o #2 o snd)) descr;
+ val descr' = filter (can (map Datatype_Aux.dest_DtTFree o #2 o snd)) descr;
val rtnames = map (#1 o snd) (filter (fn (_, (_, _, cs)) =>
- exists (exists DatatypeAux.is_rec_type o snd) cs) descr');
+ exists (exists Datatype_Aux.is_rec_type o snd) cs) descr');
val (_, (tname, _, _)) :: _ = descr';
val node_id = tname ^ " (type)";
@@ -56,8 +31,8 @@
fun mk_dtdef prfx [] gr = ([], gr)
| mk_dtdef prfx ((_, (tname, dts, cs))::xs) gr =
let
- val tvs = map DatatypeAux.dest_DtTFree dts;
- val cs' = map (apsnd (map (DatatypeAux.typ_of_dtyp descr sorts))) cs;
+ val tvs = map Datatype_Aux.dest_DtTFree dts;
+ val cs' = map (apsnd (map (Datatype_Aux.typ_of_dtyp descr sorts))) cs;
val ((_, type_id), gr') = mk_type_id module' tname gr;
val (ps, gr'') = gr' |>
fold_map (fn (cname, cargs) =>
@@ -87,8 +62,8 @@
fun mk_term_of_def gr prfx [] = []
| mk_term_of_def gr prfx ((_, (tname, dts, cs)) :: xs) =
let
- val cs' = map (apsnd (map (DatatypeAux.typ_of_dtyp descr sorts))) cs;
- val dts' = map (DatatypeAux.typ_of_dtyp descr sorts) dts;
+ val cs' = map (apsnd (map (Datatype_Aux.typ_of_dtyp descr sorts))) cs;
+ val dts' = map (Datatype_Aux.typ_of_dtyp descr sorts) dts;
val T = Type (tname, dts');
val rest = mk_term_of_def gr "and " xs;
val (eqs, _) = fold_map (fn (cname, Ts) => fn prfx =>
@@ -110,12 +85,12 @@
fun mk_gen_of_def gr prfx [] = []
| mk_gen_of_def gr prfx ((i, (tname, dts, cs)) :: xs) =
let
- val tvs = map DatatypeAux.dest_DtTFree dts;
- val Us = map (DatatypeAux.typ_of_dtyp descr sorts) dts;
+ val tvs = map Datatype_Aux.dest_DtTFree dts;
+ val Us = map (Datatype_Aux.typ_of_dtyp descr sorts) dts;
val T = Type (tname, Us);
val (cs1, cs2) =
- List.partition (exists DatatypeAux.is_rec_type o snd) cs;
- val SOME (cname, _) = find_shortest_path descr i;
+ List.partition (exists Datatype_Aux.is_rec_type o snd) cs;
+ val SOME (cname, _) = Datatype_Aux.find_shortest_path descr i;
fun mk_delay p = Pretty.block
[str "fn () =>", Pretty.brk 1, p];
@@ -125,14 +100,14 @@
fun mk_constr s b (cname, dts) =
let
val gs = map (fn dt => mk_app false (mk_gen gr module' false rtnames s
- (DatatypeAux.typ_of_dtyp descr sorts dt))
- [str (if b andalso DatatypeAux.is_rec_type dt then "0"
+ (Datatype_Aux.typ_of_dtyp descr sorts dt))
+ [str (if b andalso Datatype_Aux.is_rec_type dt then "0"
else "j")]) dts;
- val Ts = map (DatatypeAux.typ_of_dtyp descr sorts) dts;
+ val Ts = map (Datatype_Aux.typ_of_dtyp descr sorts) dts;
val xs = map str
- (DatatypeProp.indexify_names (replicate (length dts) "x"));
+ (Datatype_Prop.indexify_names (replicate (length dts) "x"));
val ts = map str
- (DatatypeProp.indexify_names (replicate (length dts) "t"));
+ (Datatype_Prop.indexify_names (replicate (length dts) "t"));
val (_, id) = get_const_id gr cname
in
mk_let
@@ -378,10 +353,10 @@
| _ => NONE) cos;
fun prep_inject (trueprop $ (equiv $ (_ $ t1 $ t2) $ rhs)) =
trueprop $ (equiv $ mk_eq (t1, t2) $ rhs);
- val injects = map prep_inject (nth (DatatypeProp.make_injs [descr] vs) index);
+ val injects = map prep_inject (nth (Datatype_Prop.make_injs [descr] vs) index);
fun prep_distinct (trueprop $ (not $ (_ $ t1 $ t2))) =
[trueprop $ false_eq (t1, t2), trueprop $ false_eq (t2, t1)];
- val distincts = maps prep_distinct (snd (nth (DatatypeProp.make_distincts [descr] vs) index));
+ val distincts = maps prep_distinct (snd (nth (Datatype_Prop.make_distincts [descr] vs) index));
val refl = HOLogic.mk_Trueprop (true_eq (Free ("x", ty), Free ("x", ty)));
val simpset = Simplifier.context (ProofContext.init thy) (HOL_basic_ss addsimps
(map Simpdata.mk_eq (@{thm eq} :: @{thm eq_True} :: inject_thms @ distinct_thms)));
@@ -436,7 +411,7 @@
in
if null css then thy
else thy
- |> tap (fn _ => DatatypeAux.message config "Registering datatype for code generator ...")
+ |> tap (fn _ => Datatype_Aux.message config "Registering datatype for code generator ...")
|> fold Code.add_datatype css
|> fold_rev Code.add_default_eqn case_rewrites
|> fold Code.add_case certs