File ‹CTR_TEST_PROCESS_CTR_RELATOR.ML›
signature CTR_TEST_PROCESS_CTR_RELATOR =
sig
type process_ctr_relator_in_type
val test_suite : Proof.context -> unit -> unit
end;
structure ctr_test_process_ctr_relator : CTR_TEST_PROCESS_CTR_RELATOR =
struct
open SpecCheck;
structure Prop = SpecCheck_Property;
structure Show = SpecCheck_Show;
fun mk_msg_ctr_relator msg = "ctr_relator: " ^ msg;
type process_ctr_relator_in_type = string * Proof.context;
fun show_ctr_relator_in (process_ctr_relator_in : process_ctr_relator_in_type) =
let
val (c, _) = process_ctr_relator_in
val name_c = "constant name: " ^ c
val ctxt_c = "lthy: unknown context"
val out_c = [name_c, ctxt_c] |> String.concatWith "\n"
in Pretty.str out_c end;
fun process_ctr_relator ((c, ctxt) : process_ctr_relator_in_type) =
CTR_Relators.process_ctr_relator c ctxt;
fun test_exc_template ctxt c err_msg_end_c test_name_c =
let
val args = (c, ctxt)
val err_msg = mk_msg_ctr_relator err_msg_end_c
val exn_prop = Prop.expect_failure (ERROR err_msg) process_ctr_relator
in
check_list_unit
show_ctr_relator_in
[args]
test_name_c
exn_prop
end;
fun test_exc_not_const ctxt _ = test_exc_template
ctxt "a + b" "the input must be a constant term" "not a constant";
fun test_exc_not_body_bool ctxt _ = test_exc_template
ctxt
"Cons"
"the body of the type of the input must be bool"
"not bool body";
fun test_exc_not_binders_2 ctxt _ = test_exc_template
ctxt
"Ex"
"the type of the input must have more than two binders"
"not two binders";
fun test_exc_not_binders_binrelT ctxt _ = test_exc_template
ctxt
"not_binders_binrelT"
(
"all of the binders associated with the type of the input" ^
"except the last two must be the binary relation types"
)
"not binary relation types";
fun test_exc_no_dup_binrelT ctxt _ = test_exc_template
ctxt
"no_dup_binrelT"
(
"the types of the binders of the binary relations associated " ^
"with the type of the input must have no duplicates"
)
"no duplicates in the binary relation types";
fun test_exc_not_binders_binrelT_ftv_stv ctxt _ = test_exc_template
ctxt
"not_binders_binrelT_ftv_stv"
(
"the types of the binders of the binary relation types associated " ^
"with the input type must be either free type variables or " ^
"schematic type variables"
)
"not binrel type ftv or stv";
fun test_exc_not_type_constructor_lhs ctxt _ = test_exc_template
ctxt
"not_type_constructor_lhs"
(
"the last two binders of the input type must be " ^
"the results of an application of a type constructor"
)
"not type constructor lhs";
fun test_exc_not_type_constructor_rhs ctxt _ = test_exc_template
ctxt
"not_type_constructor_rhs"
(
"the last two binders of the input type must be " ^
"the results of an application of a type constructor"
)
"not type constructor rhs";
fun test_exc_not_identical_type_constructors_lhs ctxt _ = test_exc_template
ctxt
"not_identical_type_constructors_lhs"
(
"the sequences of the input types to the type constructors that are " ^
"associated with the last two binders of the input type must be " ^
"identical to the sequences of the types formed by concatenating the " ^
"type variables associated with the left hand side and the right " ^
"hand side of the binary relation types, respectively"
)
"not identical type constructors lhs";
fun test_exc_not_identical_type_constructors_rhs ctxt _ = test_exc_template
ctxt
"not_identical_type_constructors_rhs"
(
"the sequences of the input types to the type constructors that are " ^
"associated with the last two binders of the input type must be " ^
"identical to the sequences of the types formed by concatenating the " ^
"type variables associated with the left hand side and the right " ^
"hand side of the binary relation types, respectively"
)
"not identical type constructors rhs";
fun test_suite ctxt s =
[
test_exc_not_const,
test_exc_not_body_bool,
test_exc_not_binders_2,
test_exc_not_binders_binrelT,
test_exc_no_dup_binrelT,
test_exc_not_binders_binrelT_ftv_stv,
test_exc_not_type_constructor_lhs,
test_exc_not_type_constructor_rhs,
test_exc_not_identical_type_constructors_lhs,
test_exc_not_identical_type_constructors_rhs
]
|> map (fn f => f ctxt s)
|> Lecker.test_group ctxt s;
end;