Introduced function DatatypeProp.make_primrec_Ts to avoid code duplication.
authorberghofe
Mon Jan 24 18:09:29 2005 +0100 (2005-01-24)
changeset 1545916dd63c78049
parent 15458 9c292e3e0ca1
child 15460 dd48bf51aff1
Introduced function DatatypeProp.make_primrec_Ts to avoid code duplication.
src/HOL/Tools/datatype_abs_proofs.ML
src/HOL/Tools/datatype_prop.ML
     1.1 --- a/src/HOL/Tools/datatype_abs_proofs.ML	Mon Jan 24 18:07:10 2005 +0100
     1.2 +++ b/src/HOL/Tools/datatype_abs_proofs.ML	Mon Jan 24 18:09:29 2005 +0100
     1.3 @@ -108,21 +108,7 @@
     1.4          (map ((curry (op ^) (big_rec_name' ^ "_")) o string_of_int)
     1.5            (1 upto (length descr'))));
     1.6  
     1.7 -    val rec_result_Ts = map TFree (variantlist (replicate (length descr') "'t", used) ~~
     1.8 -      replicate (length descr') HOLogic.typeS);
     1.9 -
    1.10 -    val reccomb_fn_Ts = flat (map (fn (i, (_, _, constrs)) =>
    1.11 -      map (fn (_, cargs) =>
    1.12 -        let
    1.13 -          val Ts = map (typ_of_dtyp descr' sorts) cargs;
    1.14 -          val recs = filter (is_rec_type o fst) (cargs ~~ Ts);
    1.15 -
    1.16 -          fun mk_argT (dt, T) =
    1.17 -            binder_types T ---> nth_elem (body_index dt, rec_result_Ts);
    1.18 -
    1.19 -          val argTs = Ts @ map mk_argT recs
    1.20 -        in argTs ---> nth_elem (i, rec_result_Ts)
    1.21 -        end) constrs) descr');
    1.22 +    val (rec_result_Ts, reccomb_fn_Ts) = DatatypeProp.make_primrec_Ts descr sorts used;
    1.23  
    1.24      val rec_set_Ts = map (fn (T1, T2) => reccomb_fn_Ts ---> HOLogic.mk_setT
    1.25        (HOLogic.mk_prodT (T1, T2))) (recTs ~~ rec_result_Ts);
     2.1 --- a/src/HOL/Tools/datatype_prop.ML	Mon Jan 24 18:07:10 2005 +0100
     2.2 +++ b/src/HOL/Tools/datatype_prop.ML	Mon Jan 24 18:09:29 2005 +0100
     2.3 @@ -13,6 +13,8 @@
     2.4    val make_injs : DatatypeAux.descr list -> (string * sort) list -> term list list
     2.5    val make_ind : DatatypeAux.descr list -> (string * sort) list -> term
     2.6    val make_casedists : DatatypeAux.descr list -> (string * sort) list -> term list
     2.7 +  val make_primrec_Ts : DatatypeAux.descr list -> (string * sort) list ->
     2.8 +    string list -> typ list * typ list
     2.9    val make_primrecs : string list -> DatatypeAux.descr list ->
    2.10      (string * sort) list -> theory -> term list
    2.11    val make_cases : string list -> DatatypeAux.descr list ->
    2.12 @@ -152,13 +154,9 @@
    2.13  
    2.14  (*************** characteristic equations for primrec combinator **************)
    2.15  
    2.16 -fun make_primrecs new_type_names descr sorts thy =
    2.17 +fun make_primrec_Ts descr sorts used =
    2.18    let
    2.19 -    val sign = Theory.sign_of thy;
    2.20 -
    2.21      val descr' = flat descr;
    2.22 -    val recTs = get_rec_types descr' sorts;
    2.23 -    val used = foldr add_typ_tfree_names (recTs, []);
    2.24  
    2.25      val rec_result_Ts = map TFree (variantlist (replicate (length descr') "'t", used) ~~
    2.26        replicate (length descr') HOLogic.typeS);
    2.27 @@ -176,6 +174,18 @@
    2.28          in argTs ---> nth_elem (i, rec_result_Ts)
    2.29          end) constrs) descr');
    2.30  
    2.31 +  in (rec_result_Ts, reccomb_fn_Ts) end;
    2.32 +
    2.33 +fun make_primrecs new_type_names descr sorts thy =
    2.34 +  let
    2.35 +    val sign = Theory.sign_of thy;
    2.36 +
    2.37 +    val descr' = flat descr;
    2.38 +    val recTs = get_rec_types descr' sorts;
    2.39 +    val used = foldr add_typ_tfree_names (recTs, []);
    2.40 +
    2.41 +    val (rec_result_Ts, reccomb_fn_Ts) = make_primrec_Ts descr sorts used;
    2.42 +
    2.43      val rec_fns = map (uncurry (mk_Free "f"))
    2.44        (reccomb_fn_Ts ~~ (1 upto (length reccomb_fn_Ts)));
    2.45