(* Author: Christian Urban

   data about nominal datatypes 
*)

signature NOMINAL_DT_DATA =
sig
  type info =
   {inject : thm list,
    distinct : thm list,
    strong_inducts : thm list,
    strong_exhaust : thm list}

  val get_all_info: Proof.context -> (string * info) list
  val get_info: Proof.context -> string -> info option
  val the_info: Proof.context -> string -> info 
  val register_info: (string * info) -> Context.generic -> Context.generic
  val mk_infos: string list -> thm list -> thm list -> thm list -> thm list -> (string * info) list
end

structure Nominal_Dt_Data: NOMINAL_DT_DATA =
struct

(* information generated by nominal_datatype *)
type info =
   {inject : thm list,
    distinct : thm list,
    strong_inducts : thm list,
    strong_exhaust : thm list}

structure NominalData = Generic_Data
 (type T = info Symtab.table
  val empty = Symtab.empty
  val extend = I
  val merge = Symtab.merge (K true))

val get_all_info = Symtab.dest o NominalData.get o Context.Proof
val get_info = Symtab.lookup o NominalData.get o Context.Proof
val register_info = NominalData.map o Symtab.update

fun the_info thy name =
  (case get_info thy name of
    SOME info => info
  | NONE => error ("Unknown nominal datatype " ^ quote name))

fun mk_infos ty_names inject distinct strong_inducts strong_exhaust =
let
  fun aux ty_name =
    (ty_name, {inject = inject,
               distinct = distinct,
               strong_inducts = strong_inducts,
               strong_exhaust = strong_exhaust 
              })
in
  map aux ty_names
end


end