(* Author: Christian Urban

   data about nominal datatypes 

*)

signature NOMINAL_DT_DATA =

sig

  (* info of raw binding functions *)

  type bn_info = term * int * (int * term option) list list

  (* binding modes and binding clauses *)

  datatype bmode = Lst | Res | Set

  datatype bclause = BC of bmode * (term option * int) list * int list

  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

  datatype user_data = UserData of

    {dts      : Datatype.spec list,

     cn_names : string list,

     cn_tys   : (string * string) list,

     bn_funs  : (binding * typ * mixfix) list,

     bn_eqs   : (Attrib.binding * term) list,

     bclauses : bclause list list list}

  datatype raw_dt_info = RawDtInfo of

    {raw_dt_names         : string list,

     raw_dts              : Datatype.spec list,

     raw_tys              : typ list,

     raw_ty_args          : (string * sort) list,

     raw_cns_info         : cns_info list,

     raw_all_cns          : term list list,

     raw_inject_thms      : thm list,

     raw_distinct_thms    : thm list,

     raw_induct_thm       : thm,

     raw_induct_thms      : thm list,

     raw_exhaust_thms     : thm list,

     raw_size_trms        : term list,

     raw_size_thms        : thm list}

  datatype alpha_result = AlphaResult of

    {alpha_names      : string list,

     alpha_trms       : term list,

     alpha_tys        : typ list,

     alpha_bn_names   : string list,

     alpha_bn_trms    : term list,

     alpha_bn_tys     : typ list,

     alpha_intros     : thm list,

     alpha_cases      : thm list,

     alpha_raw_induct : thm}

end

structure Nominal_Dt_Data: NOMINAL_DT_DATA =

struct

(* term              - is constant of the bn-function 

   int               - is datatype number over which the bn-function is defined

   int * term option - is number of the corresponding argument with possibly

                       recursive call with bn-function term 

*)  

type bn_info = term * int * (int * term option) list list

datatype bmode = Lst | Res | Set

datatype bclause = BC of bmode * (term option * int) list * int list

(* 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

datatype user_data = UserData of

  {dts      : Datatype.spec list,

   cn_names : string list,

   cn_tys   : (string * string) list,

   bn_funs  : (binding * typ * mixfix) list,

   bn_eqs   : (Attrib.binding * term) list,

   bclauses : bclause list list list}

datatype raw_dt_info = RawDtInfo of

  {raw_dt_names         : string list,

   raw_dts              : Datatype.spec list,

   raw_tys              : typ list,

   raw_ty_args          : (string * sort) list,

   raw_cns_info         : cns_info list,

   raw_all_cns          : term list list,

   raw_inject_thms      : thm list,

   raw_distinct_thms    : thm list,

   raw_induct_thm       : thm,

   raw_induct_thms      : thm list,

   raw_exhaust_thms     : thm list,

   raw_size_trms        : term list,

   raw_size_thms        : thm list}

datatype alpha_result = AlphaResult of

  {alpha_names      : string list,

   alpha_trms       : term list,

   alpha_tys        : typ list,

   alpha_bn_names   : string list,

   alpha_bn_trms    : term list,

   alpha_bn_tys     : typ list,

   alpha_intros     : thm list,

   alpha_cases      : thm list,

   alpha_raw_induct : thm}

end