# HG changeset patch # User haftmann # Date 1135174697 -3600 # Node ID 5ff0244e25e81f6caff4dca40b8ec4605b4ae769 # Parent e57731ba01dd75c6b246717da9b71fd334ce007d slight clean ups diff -r e57731ba01dd -r 5ff0244e25e8 src/HOL/List.thy --- a/src/HOL/List.thy Wed Dec 21 13:25:20 2005 +0100 +++ b/src/HOL/List.thy Wed Dec 21 15:18:17 2005 +0100 @@ -2692,4 +2692,6 @@ setup list_codegen_setup +setup "[CodegenPackage.rename_inconsistent]" + end diff -r e57731ba01dd -r 5ff0244e25e8 src/HOL/Tools/datatype_codegen.ML --- a/src/HOL/Tools/datatype_codegen.ML Wed Dec 21 13:25:20 2005 +0100 +++ b/src/HOL/Tools/datatype_codegen.ML Wed Dec 21 15:18:17 2005 +0100 @@ -7,10 +7,6 @@ signature DATATYPE_CODEGEN = sig - val is_datatype: theory -> string -> bool - val get_datatype: theory -> string -> ((string * sort) list * string list) option - val get_datacons: theory -> string * string -> typ list option - val get_case_const_data: theory -> string -> (string * int) list option; val setup: (theory -> theory) list end; @@ -300,64 +296,20 @@ end) | datatype_tycodegen _ _ _ _ _ _ _ = NONE; -fun is_datatype thy dtyco = - Symtab.lookup (DatatypePackage.get_datatypes thy) dtyco - |> is_some; - -fun get_datatype thy dtname = - dtname - |> Symtab.lookup (DatatypePackage.get_datatypes thy) - |> Option.map (fn info => (#sorts info, - (get_first (fn (_, (dtname', _, cs)) => - if dtname = dtname' - then SOME (map fst cs) - else NONE) (#descr info) |> the))); - -fun get_datacons thy (c, dtname) = - let - val descr = - dtname - |> Symtab.lookup (DatatypePackage.get_datatypes thy) - |> Option.map #descr - |> these - val one_descr = - descr - |> get_first (fn (_, (dtname', vs, cs)) => - if dtname = dtname' - then SOME (vs, cs) - else NONE); - in - if is_some one_descr - then - the one_descr - |> (fn (vs, cs) => - c - |> AList.lookup (op =) cs - |> Option.map (map (DatatypeAux.typ_of_dtyp descr (map (rpair []) - (map DatatypeAux.dest_DtTFree vs))))) - else NONE - end; - -fun get_case_const_data thy f = - case Library.find_first (fn (_, {index, descr, case_name, ...}) => - case_name = f - ) ((Symtab.dest o DatatypePackage.get_datatypes) thy) - of NONE => NONE - | SOME (_, {index, descr, ...}) => - (SOME o map (apsnd length) o #3 o the o AList.lookup (op =) descr) index; - val setup = [ add_codegen "datatype" datatype_codegen, add_tycodegen "datatype" datatype_tycodegen, CodegenPackage.set_is_datatype - is_datatype, - CodegenPackage.add_defgen - ("datatype", CodegenPackage.defgen_datatype get_datatype get_datacons), + DatatypePackage.is_datatype, + CodegenPackage.set_get_all_datatype_cons + DatatypePackage.get_all_datatype_cons, CodegenPackage.add_defgen - ("datacons", CodegenPackage.defgen_datacons get_datacons), + ("datatype", CodegenPackage.defgen_datatype DatatypePackage.get_datatype DatatypePackage.get_datatype_cons), + CodegenPackage.add_defgen + ("datacons", CodegenPackage.defgen_datacons DatatypePackage.get_datatype_cons), CodegenPackage.add_appgen - ("case", CodegenPackage.appgen_case get_case_const_data) + ("case", CodegenPackage.appgen_case DatatypePackage.get_case_const_data) ]; end; diff -r e57731ba01dd -r 5ff0244e25e8 src/HOL/Tools/datatype_package.ML --- a/src/HOL/Tools/datatype_package.ML Wed Dec 21 13:25:20 2005 +0100 +++ b/src/HOL/Tools/datatype_package.ML Wed Dec 21 15:18:17 2005 +0100 @@ -66,6 +66,11 @@ val print_datatypes : theory -> unit val datatype_info : theory -> string -> DatatypeAux.datatype_info option val datatype_info_err : theory -> string -> DatatypeAux.datatype_info + val is_datatype : theory -> string -> bool + val get_datatype : theory -> string -> ((string * sort) list * string list) option + val get_datatype_cons : theory -> string * string -> typ list option + val get_case_const_data : theory -> string -> (string * int) list option + val get_all_datatype_cons : theory -> (string * string list) list val constrs_of : theory -> string -> term list option val case_const_of : theory -> string -> term option val weak_case_congs_of : theory -> thm list @@ -948,6 +953,61 @@ val add_datatype = gen_add_datatype read_typ true; +(** queries **) + +fun is_datatype thy dtco = + Symtab.lookup (get_datatypes thy) dtco + |> is_some; + +fun get_datatype thy dtco = + dtco + |> Symtab.lookup (get_datatypes thy) + |> Option.map (fn info => (#sorts info, + (get_first (fn (_, (dtco', _, cs)) => + if dtco = dtco' + then SOME (map fst cs) + else NONE) (#descr info) |> the))); + +fun get_datatype_cons thy (co, dtco) = + let + val descr = + dtco + |> Symtab.lookup (get_datatypes thy) + |> Option.map #descr + |> these + val one_descr = + descr + |> get_first (fn (_, (dtco', vs, cs)) => + if dtco = dtco' + then SOME (vs, cs) + else NONE); + in + if is_some one_descr + then + the one_descr + |> (fn (vs, cs) => + co + |> AList.lookup (op =) cs + |> Option.map (map (DatatypeAux.typ_of_dtyp descr (map (rpair []) + (map DatatypeAux.dest_DtTFree vs))))) + else NONE + end; + +fun get_case_const_data thy c = + case Library.find_first (fn (_, {index, descr, case_name, ...}) => + case_name = c + ) ((Symtab.dest o get_datatypes) thy) + of NONE => NONE + | SOME (_, {index, descr, ...}) => + (SOME o map (apsnd length) o #3 o the o AList.lookup (op =) descr) index; + +fun get_all_datatype_cons thy = + Symtab.fold (fn (dtco, _) => fold + (fn co => + AList.default (op =) (co, []) #> AList.map_entry (op =) co (cons dtco)) + ((snd o the oo get_datatype) thy dtco)) (get_datatypes thy) []; + + (** package setup **) (* setup theory *)