# HG changeset patch # User wenzelm # Date 1322830296 -3600 # Node ID 2888e076ac178cab9bbf5ad8cc21f7a8f6a49837 # Parent 7d7d7af647a9129ab7ec3deffd74748ad9998707 do not open ML structures; diff -r 7d7d7af647a9 -r 2888e076ac17 src/HOL/Nominal/nominal_primrec.ML --- 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 diff -r 7d7d7af647a9 -r 2888e076ac17 src/HOL/Tools/Function/size.ML --- 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 diff -r 7d7d7af647a9 -r 2888e076ac17 src/HOL/Tools/primrec.ML --- 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")