File ‹old_show_generator.ML›
signature SHOW_GENERATOR =
sig
val mk_shows_idx : theory -> Old_Datatype_Aux.info -> (int -> term) * (term * int * int) list;
val mk_shows_list : typ -> term;
val derive : string -> string -> theory -> theory
end
structure Show_Generator : SHOW_GENERATOR =
struct
open Derive_Aux
val shows_ty = @{typ "shows"}
val string_ty = @{typ "string"}
val nat_ty = @{typ "nat"}
val sort = @{sort show}
val append = @{term "append :: string ⇒ shows"}
val default_prec = @{term "0 :: nat"}
fun mk_free_tysubst_i typ_subst x i ty = Free (x ^ string_of_int i, ty |> typ_subst)
fun mk_shows_idx thy info =
let
val typ_subst = typ_subst_for_sort thy info sort
val descr = #descr info
fun mk_shows s = append $ HOLogic.mk_string s
fun typ_of dty = Old_Datatype_Aux.typ_of_dtyp descr dty |> typ_subst
val rec_names = #rec_names info
val mk_free_i = mk_free_tysubst_i typ_subst
fun rec_idx i dtys = dt_number_recs (take i dtys) |> fst
fun mk_rhss (idx, (_, _, cons)) =
let
fun mk_rhs (_, (cname, dtysi)) =
let
val lvars = map_index (fn (i, dty) => mk_free_i "x_" i (typ_of dty)) dtysi
fun res_var (_, oc) = mk_free_i "res_" oc shows_ty;
val res_vars = dt_number_recs dtysi |> snd |> map res_var
val x = nth lvars
val show_cname = mk_shows (Long_Name.base_name cname)
fun combine_dts C e [] = C e
| combine_dts C e ((_, c) :: ics) =
combine_dts (fn e' => C (@{term "(+@+)"} $ e $ e')) c ics
fun parenthise t = @{term shows_sep_paren} $ t
fun shows_of_dty (i, Old_Datatype_Aux.DtRec j) =
res_var (j, rec_idx i dtysi) |> parenthise
| shows_of_dty (i, _) =
let
val xi = x i
val ty = Term.type_of xi
val shows = \<^Const>‹shows_prec ty for default_prec xi›
in shows |> parenthise end
val pre_rhs = map_index shows_of_dty dtysi
|> map_index I
|> combine_dts I show_cname
val rhs = fold lambda (rev (lvars @ res_vars)) pre_rhs
in rhs end
val rec_args = map_index (fn (i, c) => (mk_rhs (i, c), i, idx)) cons
in rec_args end
val nrec_args = flat (map mk_rhss descr)
val rec_args = map #1 nrec_args
fun mk_rec i =
let
val ty = typ_of (Old_Datatype_Aux.DtRec i)
val rec_ty = map type_of rec_args @ [ty] ---> shows_ty
val rec_name = nth rec_names i
val rhs = list_comb (Const (rec_name, rec_ty), rec_args)
in rhs end
in (mk_rec, nrec_args) end
fun mk_shows_list ty =
\<^Const>‹shows_list_aux ty for ‹Abs ("x", ty, \<^Const>‹shows_prec ty for default_prec ‹Bound 0››)››
fun mk_prop_trm thy info
(gen : (int -> term) -> (term -> term) -> term list * term list) =
let
fun main idx =
let
val xs = mk_xs thy info sort idx
val shows = fn a => fst (mk_shows_idx thy info) idx $ a
in gen xs shows end
in
#descr info
|> map (fst #> main)
end
val r_var = Free ("r", string_ty)
val s_var = Free ("s", string_ty)
fun mk_assoc_thm_trm thy info =
mk_prop_trm thy info (fn xs => fn show =>
let val x = xs 1
in
([HOLogic.mk_eq (append $ (show x $ r_var) $ s_var, show x $ (append $ r_var $ s_var))],
[x, r_var, s_var])
end)
fun simps_of_info (info : Old_Datatype_Aux.info) = #rec_rewrites info
fun mk_assoc_thm thy info =
let
val assoc_props = mk_assoc_thm_trm thy info
val ind_thm = #induct info
val simp_that = simps_of_info info
val assoc_thm_of_tac = inductive_thm thy assoc_props ind_thm sort
val nrec_args = mk_shows_idx thy info |> snd
val descr = #descr info
fun ind_tac ctxt i ihs _ _ _ =
let
val (_, j, idx) = nth nrec_args i
val c_info = nth descr idx |> snd |> (fn (_, _, info) => nth info j)
val pdtys = snd c_info
fun sub_case_tac [] [] = all_tac
| sub_case_tac (dty :: pdtys) ihs =
let
val (thm, ihs') = (case dty of Old_Datatype_Aux.DtRec _ => (hd ihs, tl ihs) | _ => (@{thm assoc(1)}, ihs))
in
resolve_tac ctxt
[case pdtys of [] => @{thm shows_sep_paren_final} | _ => @{thm shows_sep_paren}] 1
THEN resolve_tac ctxt [thm] 1
THEN sub_case_tac pdtys ihs'
end
| sub_case_tac _ _ = error "internal error in show_generator"
in
unfold_tac ctxt simp_that
THEN resolve_tac ctxt
[case pdtys of [] => @{thm append_assoc} | _ => @{thm append_assoc_trans}] 1
THEN sub_case_tac pdtys ihs
end
in assoc_thm_of_tac ind_tac end
fun derive dtyp_name _ thy =
let
val tyco = dtyp_name
val base_name = Long_Name.base_name tyco
val _ = writeln ("creating show-functions for data type " ^ base_name)
val info = BNF_LFP_Compat.the_info thy [] tyco
val vs =
let val i = BNF_LFP_Compat.the_spec thy tyco |> fst
in map (fn (n, _) => (n, sort)) i end
val shows_rhs = fst (mk_shows_idx thy info) 0
val shows_prec_rhs = lambda (Free ("p", nat_ty)) shows_rhs
val ty = Term.fastype_of shows_rhs |> Term.dest_Type |> snd |> hd
val shows_list_rhs = mk_shows_list ty
val shows_prec_def = mk_def (nat_ty --> ty --> shows_ty) @{const_name shows_prec} shows_prec_rhs
val shows_list_def = mk_def (\<^Type>‹list ty› --> shows_ty) @{const_name shows_list} shows_list_rhs
val ((shows_prec_thm, shows_list_thm), lthy) = Class.instantiation ([tyco], vs, sort) thy
|> define_overloaded ("shows_prec_" ^ base_name ^ "_def", shows_prec_def)
||>> define_overloaded ("shows_list_" ^ base_name ^ "_def", shows_list_def)
val assoc_thm = mk_assoc_thm thy info;
fun assoc_tac ctxt = unfold_tac ctxt [shows_prec_thm]
THEN resolve_tac ctxt [assoc_thm] 1;
val thy' = Class.prove_instantiation_exit (fn ctxt =>
Class.intro_classes_tac ctxt []
THEN assoc_tac ctxt
THEN unfold_tac ctxt [shows_list_thm]
THEN resolve_tac ctxt @{thms shows_list_aux_assoc} 1
THEN resolve_tac ctxt @{thms ballI} 1
THEN assoc_tac ctxt
) lthy;
val _ = writeln ("registered " ^ base_name ^ " in class show")
in thy' end
val _ =
Theory.setup
(Derive_Manager.register_derive "show" "derives a show function for a datatype" derive)
end