src/HOL/Tools/datatype_codegen.ML
changeset 18451 5ff0244e25e8
parent 18386 e6240d62a7e6
child 18518 3b1dfa53e64f
     1.1 --- a/src/HOL/Tools/datatype_codegen.ML	Wed Dec 21 13:25:20 2005 +0100
     1.2 +++ b/src/HOL/Tools/datatype_codegen.ML	Wed Dec 21 15:18:17 2005 +0100
     1.3 @@ -7,10 +7,6 @@
     1.4  
     1.5  signature DATATYPE_CODEGEN =
     1.6  sig
     1.7 -  val is_datatype: theory -> string -> bool
     1.8 -  val get_datatype: theory -> string -> ((string * sort) list * string list) option
     1.9 -  val get_datacons: theory -> string * string -> typ list option
    1.10 -  val get_case_const_data: theory -> string -> (string * int) list option;
    1.11    val setup: (theory -> theory) list
    1.12  end;
    1.13  
    1.14 @@ -300,64 +296,20 @@
    1.15             end)
    1.16    | datatype_tycodegen _ _ _ _ _ _ _ = NONE;
    1.17  
    1.18 -fun is_datatype thy dtyco =
    1.19 -  Symtab.lookup (DatatypePackage.get_datatypes thy) dtyco
    1.20 -  |> is_some;
    1.21 -
    1.22 -fun get_datatype thy dtname =
    1.23 -  dtname
    1.24 -  |> Symtab.lookup (DatatypePackage.get_datatypes thy)
    1.25 -  |> Option.map (fn info => (#sorts info,
    1.26 -      (get_first (fn (_, (dtname', _, cs)) =>
    1.27 -        if dtname = dtname'
    1.28 -        then SOME (map fst cs)
    1.29 -        else NONE) (#descr info) |> the)));
    1.30 -  
    1.31 -fun get_datacons thy (c, dtname) =
    1.32 -  let
    1.33 -    val descr =
    1.34 -      dtname
    1.35 -      |> Symtab.lookup (DatatypePackage.get_datatypes thy)
    1.36 -      |> Option.map #descr
    1.37 -      |> these
    1.38 -    val one_descr =
    1.39 -      descr
    1.40 -      |> get_first (fn (_, (dtname', vs, cs)) =>
    1.41 -          if dtname = dtname'
    1.42 -          then SOME (vs, cs)
    1.43 -          else NONE);
    1.44 -  in
    1.45 -    if is_some one_descr
    1.46 -    then
    1.47 -      the one_descr
    1.48 -      |> (fn (vs, cs) =>
    1.49 -          c
    1.50 -          |> AList.lookup (op =) cs
    1.51 -          |> Option.map (map (DatatypeAux.typ_of_dtyp descr (map (rpair [])
    1.52 -               (map DatatypeAux.dest_DtTFree vs)))))
    1.53 -    else NONE
    1.54 -  end;
    1.55 -
    1.56 -fun get_case_const_data thy f =
    1.57 -  case Library.find_first (fn (_, {index, descr, case_name, ...}) =>
    1.58 -      case_name = f
    1.59 -    ) ((Symtab.dest o DatatypePackage.get_datatypes) thy)
    1.60 -   of NONE => NONE
    1.61 -    | SOME (_, {index, descr, ...}) =>
    1.62 -        (SOME o map (apsnd length) o #3 o the o AList.lookup (op =) descr) index;
    1.63 -
    1.64  
    1.65  val setup = [
    1.66    add_codegen "datatype" datatype_codegen,
    1.67    add_tycodegen "datatype" datatype_tycodegen,
    1.68    CodegenPackage.set_is_datatype
    1.69 -    is_datatype,
    1.70 -  CodegenPackage.add_defgen
    1.71 -    ("datatype", CodegenPackage.defgen_datatype get_datatype get_datacons),
    1.72 +    DatatypePackage.is_datatype,
    1.73 +  CodegenPackage.set_get_all_datatype_cons
    1.74 +    DatatypePackage.get_all_datatype_cons,
    1.75    CodegenPackage.add_defgen
    1.76 -    ("datacons", CodegenPackage.defgen_datacons get_datacons),
    1.77 +    ("datatype", CodegenPackage.defgen_datatype DatatypePackage.get_datatype DatatypePackage.get_datatype_cons),
    1.78 +  CodegenPackage.add_defgen
    1.79 +    ("datacons", CodegenPackage.defgen_datacons DatatypePackage.get_datatype_cons),
    1.80    CodegenPackage.add_appgen
    1.81 -    ("case", CodegenPackage.appgen_case get_case_const_data)
    1.82 +    ("case", CodegenPackage.appgen_case DatatypePackage.get_case_const_data)
    1.83  ];
    1.84  
    1.85  end;