src/HOL/Tools/datatype_realizer.ML
changeset 24699 c6674504103f
parent 23590 ad95084a5c63
child 24711 e8bba7723858
     1.1 --- a/src/HOL/Tools/datatype_realizer.ML	Tue Sep 25 10:27:43 2007 +0200
     1.2 +++ b/src/HOL/Tools/datatype_realizer.ML	Tue Sep 25 12:16:08 2007 +0200
     1.3 @@ -8,8 +8,8 @@
     1.4  
     1.5  signature DATATYPE_REALIZER =
     1.6  sig
     1.7 -  val add_dt_realizers: (string * sort) list ->
     1.8 -    DatatypeAux.datatype_info list -> theory -> theory
     1.9 +  val add_dt_realizers: string list -> theory -> theory
    1.10 +  val setup: theory -> theory
    1.11  end;
    1.12  
    1.13  structure DatatypeRealizer : DATATYPE_REALIZER =
    1.14 @@ -40,7 +40,7 @@
    1.15  
    1.16  fun mk_realizes T = Const ("realizes", T --> HOLogic.boolT --> HOLogic.boolT);
    1.17  
    1.18 -fun make_ind sorts ({descr, rec_names, rec_rewrites, induction, ...} : datatype_info) (is, thy) =
    1.19 +fun make_ind sorts ({descr, rec_names, rec_rewrites, induction, ...} : datatype_info) is thy =
    1.20    let
    1.21      val recTs = get_rec_types descr sorts;
    1.22      val pnames = if length descr = 1 then ["P"]
    1.23 @@ -160,7 +160,7 @@
    1.24    in Extraction.add_realizers_i [(ind_name, (vs, r', prf))] thy' end;
    1.25  
    1.26  
    1.27 -fun make_casedists sorts ({index, descr, case_name, case_rewrites, exhaustion, ...} : datatype_info, thy) =
    1.28 +fun make_casedists sorts ({index, descr, case_name, case_rewrites, exhaustion, ...} : datatype_info) thy =
    1.29    let
    1.30      val cert = cterm_of thy;
    1.31      val rT = TFree ("'P", HOLogic.typeS);
    1.32 @@ -216,11 +216,18 @@
    1.33       (exh_name, ([], Extraction.nullt, prf_of exhaustion))] thy'
    1.34    end;
    1.35  
    1.36 +fun add_dt_realizers names thy =
    1.37 +  if !proofs < 2 then thy
    1.38 +  else let
    1.39 +    val _ = message "Adding realizers for induction and case analysis ..."
    1.40 +    val infos = map (DatatypePackage.the_datatype thy) names;
    1.41 +    val info :: _ = infos;
    1.42 +  in
    1.43 +    thy
    1.44 +    |> fold_rev (make_ind (#sorts info) info) (subsets 0 (length (#descr info) - 1))
    1.45 +    |> fold_rev (make_casedists (#sorts info)) infos
    1.46 +  end;
    1.47  
    1.48 -fun add_dt_realizers sorts infos thy = if !proofs < 2 then thy else
    1.49 -  (message "Adding realizers for induction and case analysis ..."; thy
    1.50 -   |> curry (Library.foldr (make_ind sorts (hd infos)))
    1.51 -     (subsets 0 (length (#descr (hd infos)) - 1))
    1.52 -   |> curry (Library.foldr (make_casedists sorts)) infos);
    1.53 +val setup = DatatypePackage.add_interpretator add_dt_realizers;
    1.54  
    1.55  end;