File ‹speccheck_dynamic.ML›
signature SPECCHECK_DYNAMIC =
sig
val check_dynamic : Proof.context -> string -> unit
end
structure SpecCheck_Dynamic : SPECCHECK_DYNAMIC =
struct
fun determine_type ctxt s =
let
val return = Unsynchronized.ref "return"
val context : ML_Compiler0.context =
{name_space = #name_space ML_Env.context,
print_depth = SOME 1000000,
here = #here ML_Env.context,
print = fn r => return := r,
error = #error ML_Env.context}
val _ =
Context.setmp_generic_context (SOME (Context.Proof ctxt))
(fn () =>
ML_Compiler0.ML context
{line = 0, file = "generated code", verbose = true, debug = false} s) ()
in SpecCheck_Dynamic_Construct.parse_pred (! return) end;
fun run_test ctxt s =
Context.setmp_generic_context (SOME (Context.Proof ctxt))
(fn () =>
ML_Compiler0.ML ML_Env.context
{line = 0, file = "generated code", verbose = false, debug = false} s) ();
fun input_split s =
let
fun dot c = c = #"."
fun space c = c = #" "
val (head, code) = Substring.splitl (not o dot) (Substring.full s)
in
(String.tokens space (Substring.string head),
Substring.string (Substring.dropl dot code))
end;
fun make_fun s =
let
val scan_param = Scan.one (fn s => s <> ";")
fun parameters s = Scan.repeat1 scan_param s
val p = $$ "ALL" |-- parameters
val (split, code) = input_split s
val stop = Scan.stopper (fn _ => ";") (fn s => s = ";");
val (params, _) = Scan.finite stop p split
in "fn (" ^ commas params ^ ") => " ^ code end;
fun gen_check_property check ctxt s =
let
val func = make_fun s
val (_, ty) = determine_type ctxt func
in run_test ctxt (check ctxt "Dynamic Test" (ty, func)) end;
val check_dynamic = gen_check_property SpecCheck_Dynamic_Construct.build_check
end;