slight clean ups
authorhaftmann
Wed Dec 21 15:18:17 2005 +0100 (2005-12-21)
changeset 184515ff0244e25e8
parent 18450 e57731ba01dd
child 18452 5ea633c9bc05
slight clean ups
src/HOL/List.thy
src/HOL/Tools/datatype_codegen.ML
src/HOL/Tools/datatype_package.ML
     1.1 --- a/src/HOL/List.thy	Wed Dec 21 13:25:20 2005 +0100
     1.2 +++ b/src/HOL/List.thy	Wed Dec 21 15:18:17 2005 +0100
     1.3 @@ -2692,4 +2692,6 @@
     1.4  
     1.5  setup list_codegen_setup
     1.6  
     1.7 +setup "[CodegenPackage.rename_inconsistent]"
     1.8 +
     1.9  end
     2.1 --- a/src/HOL/Tools/datatype_codegen.ML	Wed Dec 21 13:25:20 2005 +0100
     2.2 +++ b/src/HOL/Tools/datatype_codegen.ML	Wed Dec 21 15:18:17 2005 +0100
     2.3 @@ -7,10 +7,6 @@
     2.4  
     2.5  signature DATATYPE_CODEGEN =
     2.6  sig
     2.7 -  val is_datatype: theory -> string -> bool
     2.8 -  val get_datatype: theory -> string -> ((string * sort) list * string list) option
     2.9 -  val get_datacons: theory -> string * string -> typ list option
    2.10 -  val get_case_const_data: theory -> string -> (string * int) list option;
    2.11    val setup: (theory -> theory) list
    2.12  end;
    2.13  
    2.14 @@ -300,64 +296,20 @@
    2.15             end)
    2.16    | datatype_tycodegen _ _ _ _ _ _ _ = NONE;
    2.17  
    2.18 -fun is_datatype thy dtyco =
    2.19 -  Symtab.lookup (DatatypePackage.get_datatypes thy) dtyco
    2.20 -  |> is_some;
    2.21 -
    2.22 -fun get_datatype thy dtname =
    2.23 -  dtname
    2.24 -  |> Symtab.lookup (DatatypePackage.get_datatypes thy)
    2.25 -  |> Option.map (fn info => (#sorts info,
    2.26 -      (get_first (fn (_, (dtname', _, cs)) =>
    2.27 -        if dtname = dtname'
    2.28 -        then SOME (map fst cs)
    2.29 -        else NONE) (#descr info) |> the)));
    2.30 -  
    2.31 -fun get_datacons thy (c, dtname) =
    2.32 -  let
    2.33 -    val descr =
    2.34 -      dtname
    2.35 -      |> Symtab.lookup (DatatypePackage.get_datatypes thy)
    2.36 -      |> Option.map #descr
    2.37 -      |> these
    2.38 -    val one_descr =
    2.39 -      descr
    2.40 -      |> get_first (fn (_, (dtname', vs, cs)) =>
    2.41 -          if dtname = dtname'
    2.42 -          then SOME (vs, cs)
    2.43 -          else NONE);
    2.44 -  in
    2.45 -    if is_some one_descr
    2.46 -    then
    2.47 -      the one_descr
    2.48 -      |> (fn (vs, cs) =>
    2.49 -          c
    2.50 -          |> AList.lookup (op =) cs
    2.51 -          |> Option.map (map (DatatypeAux.typ_of_dtyp descr (map (rpair [])
    2.52 -               (map DatatypeAux.dest_DtTFree vs)))))
    2.53 -    else NONE
    2.54 -  end;
    2.55 -
    2.56 -fun get_case_const_data thy f =
    2.57 -  case Library.find_first (fn (_, {index, descr, case_name, ...}) =>
    2.58 -      case_name = f
    2.59 -    ) ((Symtab.dest o DatatypePackage.get_datatypes) thy)
    2.60 -   of NONE => NONE
    2.61 -    | SOME (_, {index, descr, ...}) =>
    2.62 -        (SOME o map (apsnd length) o #3 o the o AList.lookup (op =) descr) index;
    2.63 -
    2.64  
    2.65  val setup = [
    2.66    add_codegen "datatype" datatype_codegen,
    2.67    add_tycodegen "datatype" datatype_tycodegen,
    2.68    CodegenPackage.set_is_datatype
    2.69 -    is_datatype,
    2.70 -  CodegenPackage.add_defgen
    2.71 -    ("datatype", CodegenPackage.defgen_datatype get_datatype get_datacons),
    2.72 +    DatatypePackage.is_datatype,
    2.73 +  CodegenPackage.set_get_all_datatype_cons
    2.74 +    DatatypePackage.get_all_datatype_cons,
    2.75    CodegenPackage.add_defgen
    2.76 -    ("datacons", CodegenPackage.defgen_datacons get_datacons),
    2.77 +    ("datatype", CodegenPackage.defgen_datatype DatatypePackage.get_datatype DatatypePackage.get_datatype_cons),
    2.78 +  CodegenPackage.add_defgen
    2.79 +    ("datacons", CodegenPackage.defgen_datacons DatatypePackage.get_datatype_cons),
    2.80    CodegenPackage.add_appgen
    2.81 -    ("case", CodegenPackage.appgen_case get_case_const_data)
    2.82 +    ("case", CodegenPackage.appgen_case DatatypePackage.get_case_const_data)
    2.83  ];
    2.84  
    2.85  end;
     3.1 --- a/src/HOL/Tools/datatype_package.ML	Wed Dec 21 13:25:20 2005 +0100
     3.2 +++ b/src/HOL/Tools/datatype_package.ML	Wed Dec 21 15:18:17 2005 +0100
     3.3 @@ -66,6 +66,11 @@
     3.4    val print_datatypes : theory -> unit
     3.5    val datatype_info : theory -> string -> DatatypeAux.datatype_info option
     3.6    val datatype_info_err : theory -> string -> DatatypeAux.datatype_info
     3.7 +  val is_datatype : theory -> string -> bool
     3.8 +  val get_datatype : theory -> string -> ((string * sort) list * string list) option
     3.9 +  val get_datatype_cons : theory -> string * string -> typ list option
    3.10 +  val get_case_const_data : theory -> string -> (string * int) list option
    3.11 +  val get_all_datatype_cons : theory -> (string * string list) list
    3.12    val constrs_of : theory -> string -> term list option
    3.13    val case_const_of : theory -> string -> term option
    3.14    val weak_case_congs_of : theory -> thm list
    3.15 @@ -948,6 +953,61 @@
    3.16  val add_datatype = gen_add_datatype read_typ true;
    3.17  
    3.18  
    3.19 +(** queries **)
    3.20 +
    3.21 +fun is_datatype thy dtco =
    3.22 +  Symtab.lookup (get_datatypes thy) dtco
    3.23 +  |> is_some;
    3.24 +
    3.25 +fun get_datatype thy dtco =
    3.26 +  dtco
    3.27 +  |> Symtab.lookup (get_datatypes thy)
    3.28 +  |> Option.map (fn info => (#sorts info,
    3.29 +      (get_first (fn (_, (dtco', _, cs)) =>
    3.30 +        if dtco = dtco'
    3.31 +        then SOME (map fst cs)
    3.32 +        else NONE) (#descr info) |> the)));
    3.33 +  
    3.34 +fun get_datatype_cons thy (co, dtco) =
    3.35 +  let
    3.36 +    val descr =
    3.37 +      dtco
    3.38 +      |> Symtab.lookup (get_datatypes thy)
    3.39 +      |> Option.map #descr
    3.40 +      |> these
    3.41 +    val one_descr =
    3.42 +      descr
    3.43 +      |> get_first (fn (_, (dtco', vs, cs)) =>
    3.44 +          if dtco = dtco'
    3.45 +          then SOME (vs, cs)
    3.46 +          else NONE);
    3.47 +  in
    3.48 +    if is_some one_descr
    3.49 +    then
    3.50 +      the one_descr
    3.51 +      |> (fn (vs, cs) =>
    3.52 +          co
    3.53 +          |> AList.lookup (op =) cs
    3.54 +          |> Option.map (map (DatatypeAux.typ_of_dtyp descr (map (rpair [])
    3.55 +               (map DatatypeAux.dest_DtTFree vs)))))
    3.56 +    else NONE
    3.57 +  end;
    3.58 +
    3.59 +fun get_case_const_data thy c =
    3.60 +  case Library.find_first (fn (_, {index, descr, case_name, ...}) =>
    3.61 +      case_name = c
    3.62 +    ) ((Symtab.dest o get_datatypes) thy)
    3.63 +   of NONE => NONE
    3.64 +    | SOME (_, {index, descr, ...}) =>
    3.65 +        (SOME o map (apsnd length) o #3 o the o AList.lookup (op =) descr) index;
    3.66 +
    3.67 +fun get_all_datatype_cons thy =
    3.68 +  Symtab.fold (fn (dtco, _) => fold
    3.69 +    (fn co =>
    3.70 +      AList.default (op =) (co, []) #> AList.map_entry (op =) co (cons dtco))
    3.71 +    ((snd o the oo get_datatype) thy dtco)) (get_datatypes thy) [];
    3.72 +
    3.73 +
    3.74  (** package setup **)
    3.75  
    3.76  (* setup theory *)