File ‹ETTS_Active.ML›
signature ETTS_ACTIVE =
sig
val etts_indent : int Config.T
datatype etts_thm_type =
tts_lemma | tts_theorem | tts_corollary | tts_proposition
val theorem_string_of_term :
Proof.context ->
etts_thm_type ->
string ->
Token.src list ->
string ->
Token.src list ->
term ->
string
end;
structure ETTS_Active : ETTS_ACTIVE =
struct
val etts_indent = Attrib.setup_config_int \<^binding>‹tts_indent› (K 2)
fun etts_indent_val ctxt = Config.get ctxt etts_indent
fun mk_etts_indent ctxt n = replicate (n*(etts_indent_val ctxt)) " "
|> String.concat
datatype etts_thm_type =
tts_lemma | tts_theorem | tts_corollary | tts_proposition;
fun string_of_etts_thm_type tts_lemma = "tts_lemma"
| string_of_etts_thm_type tts_theorem = "tts_theorem"
| string_of_etts_thm_type tts_corollary = "tts_corollary"
| string_of_etts_thm_type tts_proposition = "tts_proposition";
fun print_term ctxt t = t
|> Print_Mode.setmp [] (Syntax.unparse_term ctxt #> Pretty.string_of)
|> Sledgehammer_Util.simplify_spaces
|> ATP_Util.maybe_quote ctxt;
fun mk_print_ctxt ctxt = fold
(fn opt => Config.put opt false)
[show_markup, Printer.show_type_emphasis, show_types, show_sorts, show_consts]
ctxt;
fun mk_assumptions ctxt assmcs =
let fun mk_eoln c = c ^ "\n"
in
case assmcs of
[] => ""
| assmcs =>
mk_etts_indent ctxt 1 ^
"assumes " ^
String.concatWith ((mk_etts_indent ctxt 2) ^ "and ") (map mk_eoln assmcs)
end;
fun mk_attr_string attrs =
if length attrs = 0
then ""
else
let
val attrsc = attrs
|> map (map Token.unparse)
|> map (String.concatWith " ")
|> String.concatWith ", "
in "[" ^ attrsc ^ "]" end
fun mk_is ctxt thm_in_str attrs_in =
mk_etts_indent ctxt 2 ^ "is " ^ thm_in_str ^ mk_attr_string attrs_in
fun mk_shows ctxt thm_in_str attrs_in conclcs = case conclcs of
[] => ""
| conclcs =>
mk_etts_indent ctxt 1 ^
"shows " ^
String.concatWith "\n" conclcs ^ "\n" ^
mk_is ctxt thm_in_str attrs_in;
fun mk_preamble etts_thm_type thm_out_str attrs_out =
(string_of_etts_thm_type etts_thm_type) ^ " " ^
thm_out_str ^
mk_attr_string attrs_out ^ ":\n"
fun theorem_string_of_term
ctxt etts_thm_type thm_out_str attrs_out thm_in_str attrs_in t =
let
val ctxt = mk_print_ctxt ctxt
val t = t
|> singleton (Syntax.uncheck_terms ctxt)
|> Sledgehammer_Isar_Annotate.annotate_types_in_term ctxt
val assmsc = t
|> Logic.strip_imp_prems
|> map (print_term ctxt)
|> mk_assumptions ctxt
val conclc = t
|> Logic.strip_imp_concl
|> Logic.dest_conjunctions
|> map (print_term ctxt)
|> mk_shows ctxt thm_in_str attrs_in
val preamblec = mk_preamble etts_thm_type thm_out_str attrs_out
val done = ".\n\n"
val thmc = String.concatWith "" [preamblec, assmsc, conclc, done]
in thmc end;
end;