8 sig |
8 sig |
9 val compile_generator_expr: |
9 val compile_generator_expr: |
10 Proof.context -> (term * term list) list -> int list -> term list option * Quickcheck.report option |
10 Proof.context -> (term * term list) list -> int list -> term list option * Quickcheck.report option |
11 val put_counterexample: (unit -> term list option) -> Proof.context -> Proof.context |
11 val put_counterexample: (unit -> term list option) -> Proof.context -> Proof.context |
12 val finite_functions : bool Config.T |
12 val finite_functions : bool Config.T |
|
13 val overlord : bool Config.T |
13 val setup: theory -> theory |
14 val setup: theory -> theory |
14 end; |
15 end; |
15 |
16 |
16 structure Narrowing_Generators : NARROWING_GENERATORS = |
17 structure Narrowing_Generators : NARROWING_GENERATORS = |
17 struct |
18 struct |
61 |
62 |
62 fun mk_partial_term_of_eq thy ty (i, (c, (_, tys))) = |
63 fun mk_partial_term_of_eq thy ty (i, (c, (_, tys))) = |
63 let |
64 let |
64 val frees = map Free (Name.names Name.context "a" (map (K @{typ narrowing_term}) tys)) |
65 val frees = map Free (Name.names Name.context "a" (map (K @{typ narrowing_term}) tys)) |
65 val narrowing_term = @{term "Quickcheck_Narrowing.Ctr"} $ HOLogic.mk_number @{typ code_int} i |
66 val narrowing_term = @{term "Quickcheck_Narrowing.Ctr"} $ HOLogic.mk_number @{typ code_int} i |
66 $ (HOLogic.mk_list @{typ narrowing_term} frees) |
67 $ (HOLogic.mk_list @{typ narrowing_term} (rev frees)) |
67 val rhs = fold (fn u => fn t => @{term "Code_Evaluation.App"} $ t $ u) |
68 val rhs = fold (fn u => fn t => @{term "Code_Evaluation.App"} $ t $ u) |
68 (map mk_partial_term_of (frees ~~ tys)) |
69 (map mk_partial_term_of (frees ~~ tys)) |
69 (@{term "Code_Evaluation.Const"} $ HOLogic.mk_literal c $ HOLogic.mk_typerep (tys ---> ty)) |
70 (@{term "Code_Evaluation.Const"} $ HOLogic.mk_literal c $ HOLogic.mk_typerep (tys ---> ty)) |
70 val insts = |
71 val insts = |
71 map (SOME o Thm.cterm_of thy o map_types Logic.unvarifyT_global o Logic.varify_global) |
72 map (SOME o Thm.cterm_of thy o map_types Logic.unvarifyT_global o Logic.varify_global) |
84 (v, curry (Sorts.inter_sort algebra) @{sort typerep} sort)) raw_vs; |
85 (v, curry (Sorts.inter_sort algebra) @{sort typerep} sort)) raw_vs; |
85 val ty = Type (tyco, map TFree vs); |
86 val ty = Type (tyco, map TFree vs); |
86 val cs = (map o apsnd o apsnd o map o map_atyps) |
87 val cs = (map o apsnd o apsnd o map o map_atyps) |
87 (fn TFree (v, _) => TFree (v, (the o AList.lookup (op =) vs) v)) raw_cs; |
88 (fn TFree (v, _) => TFree (v, (the o AList.lookup (op =) vs) v)) raw_cs; |
88 val const = AxClass.param_of_inst thy (@{const_name partial_term_of}, tyco); |
89 val const = AxClass.param_of_inst thy (@{const_name partial_term_of}, tyco); |
89 val eqs = map_index (mk_partial_term_of_eq thy ty) cs; |
90 val var_insts = map (SOME o Thm.cterm_of thy o map_types Logic.unvarifyT_global o Logic.varify_global) |
|
91 [Free ("ty", Term.itselfT ty), @{term "Quickcheck_Narrowing.Var p tt"}, |
|
92 @{term "Code_Evaluation.Free (STR ''_'')"} $ HOLogic.mk_typerep ty] |
|
93 val var_eq = |
|
94 @{thm partial_term_of_anything} |
|
95 |> Drule.instantiate' [SOME (Thm.ctyp_of thy ty)] var_insts |
|
96 |> Thm.varifyT_global |
|
97 val eqs = var_eq :: map_index (mk_partial_term_of_eq thy ty) cs; |
90 in |
98 in |
91 thy |
99 thy |
92 |> Code.del_eqns const |
100 |> Code.del_eqns const |
93 |> fold Code.add_eqn eqs |
101 |> fold Code.add_eqn eqs |
94 end; |
102 end; |
181 val narrowing_engine = File.read (Path.explode "~~/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs") |
189 val narrowing_engine = File.read (Path.explode "~~/src/HOL/Tools/Quickcheck/Narrowing_Engine.hs") |
182 |
190 |
183 fun exec verbose code = |
191 fun exec verbose code = |
184 ML_Context.exec (fn () => Secure.use_text ML_Env.local_context (0, "generated code") verbose code) |
192 ML_Context.exec (fn () => Secure.use_text ML_Env.local_context (0, "generated code") verbose code) |
185 |
193 |
186 fun with_tmp_dir name f = |
194 fun with_overlord_dir name f = |
187 let |
195 let |
188 val path = Path.append (Path.explode "~/.isabelle") (Path.basic (name ^ serial_string ())) |
196 val path = Path.append (Path.explode "~/.isabelle") (Path.basic (name ^ serial_string ())) |
189 val _ = Isabelle_System.mkdirs path; |
197 val _ = Isabelle_System.mkdirs path; |
190 in Exn.release (Exn.capture f path) end; |
198 in Exn.release (Exn.capture f path) end; |
191 |
199 |
192 fun value ctxt (get, put, put_ml) (code, value) size = |
200 fun value ctxt (get, put, put_ml) (code, value) size = |
193 let |
201 let |
194 val tmp_prefix = "Quickcheck_Narrowing" |
202 val tmp_prefix = "Quickcheck_Narrowing" |
195 val with_tmp_dir = if Config.get ctxt overlord |
203 val with_tmp_dir = |
196 then Isabelle_System.with_tmp_dir else Quickcheck_Narrowing.with_tmp_dir |
204 if Config.get ctxt overlord then with_overlord_dir else Isabelle_System.with_tmp_dir |
197 fun run in_path = |
205 fun run in_path = |
198 let |
206 let |
199 val code_file = Path.append in_path (Path.basic "Code.hs") |
207 val code_file = Path.append in_path (Path.basic "Code.hs") |
200 val narrowing_engine_file = Path.append in_path (Path.basic "Narrowing_Engine.hs") |
208 val narrowing_engine_file = Path.append in_path (Path.basic "Narrowing_Engine.hs") |
201 val main_file = Path.append in_path (Path.basic "Main.hs") |
209 val main_file = Path.append in_path (Path.basic "Main.hs") |