(* Author: Christian Urban+
−
+
−
   data about nominal datatypes +
−
*)+
−
+
−
signature NOMINAL_DT_DATA =+
−
sig+
−
  (* info of raw datatypes *)+
−
  type dt_info = (string list * binding * mixfix * ((binding * typ list * mixfix) list)) list+
−
+
−
  (* 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      : dt_info,+
−
     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              : dt_info,+
−
     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+
−
+
−
(* string list      - type variables of a datatype+
−
   binding          - name of the datatype+
−
   mixfix           - its mixfix+
−
   (binding * typ list * mixfix) list  - datatype constructors of the type+
−
*)  +
−
type dt_info = (string list * binding * mixfix * ((binding * typ list * mixfix) list)) list+
−
+
−
+
−
(* 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      : dt_info,+
−
   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              : dt_info,+
−
   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+
−