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