Theory Compat
section ‹Tests for Compatibility with the Old Datatype Package›
theory Compat
imports Main
begin
subsection ‹Viewing and Registering New-Style Datatypes as Old-Style Ones›
ML ‹
fun check_len n xs label =
length xs = n orelse error ("Expected length " ^ string_of_int (length xs) ^ " for " ^ label);
fun check_lens (n1, n2, n3) (xs1, xs2, xs3) =
check_len n1 xs1 "old" andalso check_len n2 xs2 "unfold" andalso check_len n3 xs3 "keep";
fun get_descrs thy lens T_name =
(these (Option.map #descr (Old_Datatype_Data.get_info thy T_name)),
these (Option.map #descr (BNF_LFP_Compat.get_info thy [] T_name)),
these (Option.map #descr (BNF_LFP_Compat.get_info thy [BNF_LFP_Compat.Keep_Nesting] T_name)))
|> tap (check_lens lens);
›