bulwahn@42801
|
1 |
(* Title: HOL/Tools/Quickcheck/narrowing_generators.ML
|
bulwahn@42776
|
2 |
Author: Lukas Bulwahn, TU Muenchen
|
bulwahn@42776
|
3 |
|
bulwahn@42801
|
4 |
Narrowing-based counterexample generation
|
bulwahn@42776
|
5 |
|
bulwahn@42776
|
6 |
*)
|
bulwahn@42776
|
7 |
|
bulwahn@42801
|
8 |
signature NARROWING_GENERATORS =
|
bulwahn@42776
|
9 |
sig
|
bulwahn@42776
|
10 |
val compile_generator_expr:
|
bulwahn@42776
|
11 |
Proof.context -> term -> int -> term list option * Quickcheck.report option
|
bulwahn@42776
|
12 |
val put_counterexample: (unit -> term list option) -> Proof.context -> Proof.context
|
bulwahn@42776
|
13 |
val setup: theory -> theory
|
bulwahn@42776
|
14 |
end;
|
bulwahn@42776
|
15 |
|
bulwahn@42801
|
16 |
structure Narrowing_Generators : NARROWING_GENERATORS =
|
bulwahn@42776
|
17 |
struct
|
bulwahn@42776
|
18 |
|
bulwahn@42801
|
19 |
val target = "Haskell"
|
bulwahn@42801
|
20 |
|
bulwahn@42776
|
21 |
(* invocation of Haskell interpreter *)
|
bulwahn@42776
|
22 |
|
bulwahn@42801
|
23 |
val narrowing_engine = File.read (Path.explode "~~/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs")
|
bulwahn@42776
|
24 |
|
bulwahn@42776
|
25 |
fun exec verbose code =
|
bulwahn@42776
|
26 |
ML_Context.exec (fn () => Secure.use_text ML_Env.local_context (0, "generated code") verbose code)
|
bulwahn@42776
|
27 |
|
bulwahn@42776
|
28 |
fun value ctxt (get, put, put_ml) (code, value) =
|
bulwahn@42776
|
29 |
let
|
bulwahn@42801
|
30 |
val tmp_prefix = "Quickcheck_Narrowing"
|
bulwahn@42776
|
31 |
fun run in_path =
|
bulwahn@42776
|
32 |
let
|
bulwahn@42776
|
33 |
val code_file = Path.append in_path (Path.basic "Code.hs")
|
bulwahn@42801
|
34 |
val narrowing_engine_file = Path.append in_path (Path.basic "Narrowing_Engine.hs")
|
bulwahn@42776
|
35 |
val main_file = Path.append in_path (Path.basic "Main.hs")
|
bulwahn@42776
|
36 |
val main = "module Main where {\n\n" ^
|
bulwahn@42804
|
37 |
"import Narrowing_Engine;\n" ^
|
bulwahn@42776
|
38 |
"import Code;\n\n" ^
|
bulwahn@42804
|
39 |
"main = Narrowing_Engine.smallCheck 7 (Code.value ())\n\n" ^
|
bulwahn@42776
|
40 |
"}\n"
|
bulwahn@42780
|
41 |
val code' = prefix "module Code where {\n\ndata Typerep = Typerep String [Typerep];\n"
|
bulwahn@42780
|
42 |
(unprefix "module Code where {" code)
|
bulwahn@42780
|
43 |
val _ = File.write code_file code'
|
bulwahn@42801
|
44 |
val _ = File.write narrowing_engine_file narrowing_engine
|
bulwahn@42776
|
45 |
val _ = File.write main_file main
|
bulwahn@42779
|
46 |
val executable = Path.implode (Path.append in_path (Path.basic "isa_lsc"))
|
bulwahn@42801
|
47 |
val cmd = getenv "EXEC_GHC" ^ " -fglasgow-exts " ^
|
bulwahn@42801
|
48 |
(space_implode " " (map Path.implode [code_file, narrowing_engine_file, main_file])) ^
|
bulwahn@42801
|
49 |
" -o " ^ executable ^ " && " ^ executable
|
bulwahn@42776
|
50 |
in
|
bulwahn@42776
|
51 |
bash_output cmd
|
bulwahn@42801
|
52 |
end
|
bulwahn@42780
|
53 |
val result = Isabelle_System.with_tmp_dir tmp_prefix run
|
bulwahn@42776
|
54 |
val output_value = the_default "NONE"
|
bulwahn@42776
|
55 |
(try (snd o split_last o filter_out (fn s => s = "") o split_lines o fst) result)
|
bulwahn@42776
|
56 |
val ml_code = "\nval _ = Context.set_thread_data (SOME (Context.map_proof (" ^ put_ml
|
bulwahn@42776
|
57 |
^ " (fn () => " ^ output_value ^ ")) (ML_Context.the_generic_context ())))";
|
bulwahn@42776
|
58 |
val ctxt' = ctxt
|
bulwahn@42776
|
59 |
|> put (fn () => error ("Bad evaluation for " ^ quote put_ml))
|
bulwahn@42776
|
60 |
|> Context.proof_map (exec false ml_code);
|
bulwahn@42776
|
61 |
in get ctxt' () end;
|
bulwahn@42776
|
62 |
|
bulwahn@42776
|
63 |
fun evaluation cookie thy evaluator vs_t args =
|
bulwahn@42776
|
64 |
let
|
bulwahn@42776
|
65 |
val ctxt = ProofContext.init_global thy;
|
bulwahn@42776
|
66 |
val (program_code, value_name) = evaluator vs_t;
|
bulwahn@42776
|
67 |
val value_code = space_implode " "
|
bulwahn@42776
|
68 |
(value_name :: "()" :: map (enclose "(" ")") args);
|
bulwahn@42776
|
69 |
in Exn.interruptible_capture (value ctxt cookie) (program_code, value_code) end;
|
bulwahn@42776
|
70 |
|
bulwahn@42776
|
71 |
fun dynamic_value_strict cookie thy postproc t args =
|
bulwahn@42776
|
72 |
let
|
bulwahn@42776
|
73 |
fun evaluator naming program ((_, vs_ty), t) deps =
|
bulwahn@42801
|
74 |
evaluation cookie thy (Code_Target.evaluator thy target naming program deps) (vs_ty, t) args;
|
bulwahn@42776
|
75 |
in Exn.release (Code_Thingol.dynamic_value thy (Exn.map_result o postproc) evaluator t) end;
|
bulwahn@42776
|
76 |
|
bulwahn@42776
|
77 |
(* counterexample generator *)
|
bulwahn@42776
|
78 |
|
bulwahn@42803
|
79 |
structure Counterexample = Proof_Data
|
bulwahn@42776
|
80 |
(
|
bulwahn@42776
|
81 |
type T = unit -> term list option
|
bulwahn@42807
|
82 |
fun init _ () = error "Counterexample"
|
bulwahn@42776
|
83 |
)
|
bulwahn@42776
|
84 |
|
bulwahn@42803
|
85 |
val put_counterexample = Counterexample.put
|
bulwahn@42776
|
86 |
|
bulwahn@42776
|
87 |
fun compile_generator_expr ctxt t size =
|
bulwahn@42776
|
88 |
let
|
bulwahn@42776
|
89 |
val thy = ProofContext.theory_of ctxt
|
bulwahn@42776
|
90 |
fun ensure_testable t =
|
bulwahn@42801
|
91 |
Const (@{const_name Quickcheck_Narrowing.ensure_testable}, fastype_of t --> fastype_of t) $ t
|
bulwahn@42776
|
92 |
val t = dynamic_value_strict
|
bulwahn@42803
|
93 |
(Counterexample.get, Counterexample.put, "Narrowing_Generators.put_counterexample")
|
bulwahn@42776
|
94 |
thy (Option.map o map) (ensure_testable t) []
|
bulwahn@42776
|
95 |
in
|
bulwahn@42776
|
96 |
(t, NONE)
|
bulwahn@42776
|
97 |
end;
|
bulwahn@42776
|
98 |
|
bulwahn@42776
|
99 |
|
bulwahn@42776
|
100 |
val setup =
|
bulwahn@42776
|
101 |
Context.theory_map
|
bulwahn@42807
|
102 |
(Quickcheck.add_generator ("narrowing", compile_generator_expr))
|
bulwahn@42776
|
103 |
|
bulwahn@42776
|
104 |
end; |