File ‹utils.ML›
fun repeat1_conv cv = cv then_conv Conv.repeat_conv cv
fun init [] = error "empty list"
| init [_] = []
| init (x :: xs) = x :: init xs
fun last [] = error "empty list"
| last [x] = x
| last (_ :: xs) = last xs
val unvarify_typ =
let
fun aux (TVar ((name, idx), sort)) = TFree (name ^ Value.print_int idx, sort)
| aux t = t
in map_atyps aux end
fun all_consts (Const (name, typ)) = [(name, typ)]
| all_consts (t $ u) = union (op =) (all_consts t) (all_consts u)
| all_consts (Abs (_, _, t)) = all_consts t
| all_consts _ = []
fun induct_of_bnf_const ctxt const =
let
open Dict_Construction_Util
val (name, _) = dest_Const const
fun cmp {T, ...} (Const (name', _)) = if name = name' then SOME T else NONE
| cmp _ _ = NONE
fun is_disc_or_sel (sugar as {discs, selss, ...}) =
maps (map (cmp sugar)) selss @ map (cmp sugar) discs
val Ts =
Ctr_Sugar.ctr_sugars_of ctxt
|> maps is_disc_or_sel
|> cat_options
in
case Ts of
(Type (typ_name, _) :: _) =>
BNF_FP_Def_Sugar.fp_sugar_of ctxt typ_name
|> Option.mapPartial #fp_co_induct_sugar
|> Option.map #co_inducts
| _ => NONE
end