File ‹ETTS_TEST_TTS_REGISTER_SBTS.ML›
signature ETTS_TEST_TTS_REGISTER_SBTS =
sig
type tts_register_sbts_in_type
val test_suite : Proof.context -> unit -> unit
end;
structure etts_test_tts_register_sbts : ETTS_TEST_TTS_REGISTER_SBTS =
struct
open SpecCheck;
structure Prop = SpecCheck_Property;
structure Show = SpecCheck_Show;
fun mk_msg_tts_register_sbts_error msg = "tts_register_sbts: " ^ msg
type tts_register_sbts_in_type =
(string * string list) * Proof.context
fun show_tts_register_sbts_in
(tts_register_sbts_in : tts_register_sbts_in_type) =
let
val ((sbt, risset), _) = tts_register_sbts_in
val ctxt_c = "ctxt: unknown context"
val sbt_c = "sbt: " ^ sbt
val risset_c = "risset: " ^ ML_Syntax.print_list I risset
val out_c = [ctxt_c, sbt_c, risset_c] |> String.concatWith "\n"
in Pretty.str out_c end;
fun tts_register_sbts ((args, ctxt) : tts_register_sbts_in_type) =
ETTS_Substitution.process_tts_register_sbts args ctxt;
fun test_exc_fvs ctxt _ =
let
val sbt = "g::'q"
val UA_c = "UA::'a set"
val UB_c = "UB::'b set"
val rissest = [UA_c, UB_c]
val tts_register_sbts_in : tts_register_sbts_in_type =
((sbt, rissest), ctxt)
val err_msg = mk_msg_tts_register_sbts_error
"all fixed variables that occur in the sbterm " ^
"must be fixed in the context"
val exn_prop = Prop.expect_failure (ERROR err_msg) tts_register_sbts
in
check_list_unit
(show_tts_register_sbts_in)
[tts_register_sbts_in]
"variables not fixed in the context"
exn_prop
end;
fun test_exc_repeated_risset ctxt _ =
let
val sbt = "f"
val UA_c = "UA::'a set"
val UB_c = "UA::'a set"
val rissest = [UA_c, UB_c]
val tts_register_sbts_in : tts_register_sbts_in_type =
((sbt, rissest), ctxt)
val err_msg = mk_msg_tts_register_sbts_error
"the type variables associated with the risset must be distinct"
val exn_prop = Prop.expect_failure (ERROR err_msg) tts_register_sbts
in
check_list_unit
show_tts_register_sbts_in
[tts_register_sbts_in]
"repeated risset"
exn_prop
end;
fun test_suite ctxt s = [test_exc_fvs ctxt s, test_exc_repeated_risset ctxt s]
|> Lecker.test_group ctxt s;
end;