--- a/src/HOL/Nominal/nominal_primrec.ML Fri Dec 02 13:38:24 2011 +0100
+++ b/src/HOL/Nominal/nominal_primrec.ML Fri Dec 02 13:51:36 2011 +0100
@@ -21,8 +21,6 @@
structure NominalPrimrec : NOMINAL_PRIMREC =
struct
-open Datatype_Aux;
-
exception RecError of string;
fun primrec_err s = error ("Nominal primrec definition error:\n" ^ s);
@@ -156,12 +154,12 @@
(fnames', fnss', (Const (@{const_name undefined}, dummyT))::fns))
| SOME (ls, cargs', rs, rhs, eq) =>
let
- val recs = filter (is_rec_type o snd) (cargs' ~~ cargs);
+ val recs = filter (Datatype_Aux.is_rec_type o snd) (cargs' ~~ cargs);
val rargs = map fst recs;
val subs = map (rpair dummyT o fst)
(rev (Term.rename_wrt_term rhs rargs));
val (rhs', (fnames'', fnss'')) = subst (map2 (fn (x, y) => fn z =>
- (Free x, (body_index y, Free z))) recs subs) rhs (fnames', fnss')
+ (Free x, (Datatype_Aux.body_index y, Free z))) recs subs) rhs (fnames', fnss')
handle RecError s => primrec_eq_err lthy s eq
in (fnames'', fnss'', fold_rev absfree (cargs' @ subs) rhs' :: fns)
end)
@@ -192,7 +190,7 @@
NONE =>
let
val dummy_fns = map (fn (_, cargs) => Const (@{const_name undefined},
- replicate (length cargs + length (filter is_rec_type cargs))
+ replicate (length cargs + length (filter Datatype_Aux.is_rec_type cargs))
dummyT ---> HOLogic.unitT)) constrs;
val _ = warning ("No function definition for datatype " ^ quote tname)
in
--- a/src/HOL/Tools/Function/size.ML Fri Dec 02 13:38:24 2011 +0100
+++ b/src/HOL/Tools/Function/size.ML Fri Dec 02 13:51:36 2011 +0100
@@ -13,8 +13,6 @@
structure Size: SIZE =
struct
-open Datatype_Aux;
-
structure SizeData = Theory_Data
(
type T = (string * thm list) Symtab.table;
@@ -56,16 +54,16 @@
val app = curry (list_comb o swap);
-fun prove_size_thms (info : info) new_type_names thy =
+fun prove_size_thms (info : Datatype.info) new_type_names thy =
let
val {descr, sorts, rec_names, rec_rewrites, induct, ...} = info;
val l = length new_type_names;
val descr' = List.take (descr, l);
val (rec_names1, rec_names2) = chop l rec_names;
- val recTs = get_rec_types descr sorts;
+ val recTs = Datatype_Aux.get_rec_types descr sorts;
val (recTs1, recTs2) = chop l recTs;
val (_, (_, paramdts, _)) :: _ = descr;
- val paramTs = map (typ_of_dtyp descr sorts) paramdts;
+ val paramTs = map (Datatype_Aux.typ_of_dtyp descr sorts) paramdts;
val ((param_size_fs, param_size_fTs), f_names) = paramTs |>
map (fn T as TFree (s, _) =>
let
@@ -96,10 +94,10 @@
(* instantiation for primrec combinator *)
fun size_of_constr b size_ofp ((_, cargs), (_, cargs')) =
let
- val Ts = map (typ_of_dtyp descr sorts) cargs;
- val k = length (filter is_rec_type cargs);
+ val Ts = map (Datatype_Aux.typ_of_dtyp descr sorts) cargs;
+ val k = length (filter Datatype_Aux.is_rec_type cargs);
val (ts, _, _) = fold_rev (fn ((dt, dt'), T) => fn (us, i, j) =>
- if is_rec_type dt then (Bound i :: us, i + 1, j + 1)
+ if Datatype_Aux.is_rec_type dt then (Bound i :: us, i + 1, j + 1)
else
(if b andalso is_poly thy dt' then
case size_of_type (K NONE) extra_size size_ofp T of
@@ -161,8 +159,8 @@
fun prove_unfolded_size_eqs size_ofp fs =
if null recTs2 then []
- else split_conj_thm (Skip_Proof.prove ctxt xs []
- (HOLogic.mk_Trueprop (mk_conj (replicate l HOLogic.true_const @
+ else Datatype_Aux.split_conj_thm (Skip_Proof.prove ctxt xs []
+ (HOLogic.mk_Trueprop (Datatype_Aux.mk_conj (replicate l HOLogic.true_const @
map (mk_unfolded_size_eq (AList.lookup op =
(new_type_names ~~ map (app fs) rec_combs1)) size_ofp fs)
(xs ~~ recTs2 ~~ rec_combs2))))
@@ -174,7 +172,7 @@
(* characteristic equations for size functions *)
fun gen_mk_size_eq p size_of size_ofp size_const T (cname, cargs) =
let
- val Ts = map (typ_of_dtyp descr sorts) cargs;
+ val Ts = map (Datatype_Aux.typ_of_dtyp descr sorts) cargs;
val tnames = Name.variant_list f_names (Datatype_Prop.make_tnames Ts);
val ts = map_filter (fn (sT as (s, T), dt) =>
Option.map (fn sz => sz $ Free sT)
@@ -202,7 +200,7 @@
(descr' ~~ size_fns ~~ recTs1);
val size_eqns = prove_size_eqs (is_poly thy') size_fns param_size simpset2 @
- prove_size_eqs is_rec_type overloaded_size_fns (K NONE) simpset3;
+ prove_size_eqs Datatype_Aux.is_rec_type overloaded_size_fns (K NONE) simpset3;
val ([size_thms], thy'') =
Global_Theory.add_thmss
@@ -222,7 +220,8 @@
val prefix =
Long_Name.map_base_name (K (space_implode "_" (map Long_Name.base_name new_type_names))) name;
val no_size = exists (fn (_, (_, _, constrs)) => exists (fn (_, cargs) => exists (fn dt =>
- is_rec_type dt andalso not (null (fst (strip_dtyp dt)))) cargs) constrs) descr
+ Datatype_Aux.is_rec_type dt andalso
+ not (null (fst (Datatype_Aux.strip_dtyp dt)))) cargs) constrs) descr
in
if no_size then thy
else
--- a/src/HOL/Tools/primrec.ML Fri Dec 02 13:38:24 2011 +0100
+++ b/src/HOL/Tools/primrec.ML Fri Dec 02 13:51:36 2011 +0100
@@ -24,8 +24,6 @@
structure Primrec : PRIMREC =
struct
-open Datatype_Aux;
-
exception PrimrecError of string * term option;
fun primrec_error msg = raise PrimrecError (msg, NONE);
@@ -147,12 +145,12 @@
(fnames', fnss', (Const (@{const_name undefined}, dummyT)) :: fns))
| SOME (ls, cargs', rs, rhs, eq) =>
let
- val recs = filter (is_rec_type o snd) (cargs' ~~ cargs);
+ val recs = filter (Datatype_Aux.is_rec_type o snd) (cargs' ~~ cargs);
val rargs = map fst recs;
val subs = map (rpair dummyT o fst)
(rev (Term.rename_wrt_term rhs rargs));
val (rhs', (fnames'', fnss'')) = subst (map2 (fn (x, y) => fn z =>
- (Free x, (body_index y, Free z))) recs subs) rhs (fnames', fnss')
+ (Free x, (Datatype_Aux.body_index y, Free z))) recs subs) rhs (fnames', fnss')
handle PrimrecError (s, NONE) => primrec_error_eqn s eq
in
(fnames'', fnss'', fold_rev absfree (cargs' @ subs @ ls @ rs) rhs' :: fns)
@@ -184,7 +182,7 @@
NONE =>
let
val dummy_fns = map (fn (_, cargs) => Const (@{const_name undefined},
- replicate (length cargs + length (filter is_rec_type cargs))
+ replicate (length cargs + length (filter Datatype_Aux.is_rec_type cargs))
dummyT ---> HOLogic.unitT)) constrs;
val _ = warning ("No function definition for datatype " ^ quote tname)
in
@@ -208,7 +206,7 @@
(* find datatypes which contain all datatypes in tnames' *)
-fun find_dts (dt_info : info Symtab.table) _ [] = []
+fun find_dts (dt_info : Datatype_Aux.info Symtab.table) _ [] = []
| find_dts dt_info tnames' (tname :: tnames) =
(case Symtab.lookup dt_info tname of
NONE => primrec_error (quote tname ^ " is not a datatype")