--- a/src/HOL/Library/Efficient_Nat.thy Fri Jul 27 21:57:56 2012 +0200
+++ b/src/HOL/Library/Efficient_Nat.thy Fri Jul 27 22:26:38 2012 +0200
@@ -281,9 +281,10 @@
(SML "HOLogic.mk'_number/ HOLogic.natT")
text {*
- FIXME -- Evaluation with @{text "Quickcheck_Narrowing"} does not work, as
- @{text "code_module"} is very aggressive leading to bad Haskell code.
- Therefore, we simply deactivate the narrowing-based quickcheck from here on.
+ Evaluation with @{text "Quickcheck_Narrowing"} does not work yet,
+ since a couple of questions how to perform evaluations in Haskell are not that
+ clear yet. Therefore, we simply deactivate the narrowing-based quickcheck
+ from here on.
*}
declare [[quickcheck_narrowing_active = false]]
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Fri Jul 27 21:57:56 2012 +0200
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Fri Jul 27 22:26:38 2012 +0200
@@ -223,7 +223,7 @@
let val ({elapsed, ...}, result) = Timing.timing e ()
in (result, (description, Time.toMilliseconds elapsed)) end
-fun value (contains_existentials, ((genuine_only, (quiet, verbose)), size)) ctxt cookie (code, value_name) =
+fun value (contains_existentials, ((genuine_only, (quiet, verbose)), size)) ctxt cookie (code_modules, value_name) =
let
val ((is_genuine, counterexample_of), (get, put, put_ml)) = cookie
fun message s = if quiet then () else Output.urgent_message s
@@ -238,31 +238,34 @@
if Config.get ctxt overlord then with_overlord_dir else Isabelle_System.with_tmp_dir
fun run in_path =
let
- val code_file = Path.append in_path (Path.basic "Generated_Code.hs")
- val narrowing_engine_file = Path.append in_path (Path.basic "Narrowing_Engine.hs")
- val main_file = Path.append in_path (Path.basic "Main.hs")
+ fun mk_code_file name = Path.append in_path (Path.basic (name ^ ".hs"))
+ val generatedN = Code_Target.generatedN
+ val includes = AList.delete (op =) generatedN code_modules |> (map o apfst) mk_code_file;
+ val code = the (AList.lookup (op =) code_modules generatedN)
+ val code_file = mk_code_file generatedN
+ val narrowing_engine_file = mk_code_file "Narrowing_Engine"
+ val main_file = mk_code_file "Main"
val main = "module Main where {\n\n" ^
"import System.IO;\n" ^
"import System.Environment;\n" ^
"import Narrowing_Engine;\n" ^
- "import Generated_Code;\n\n" ^
+ "import " ^ generatedN ^ " ;\n\n" ^
"main = getArgs >>= \\[potential, size] -> " ^
- "Narrowing_Engine.depthCheck (read potential) (read size) (Generated_Code.value ())\n\n" ^
+ "Narrowing_Engine.depthCheck (read potential) (read size) (" ^ generatedN ^ ".value ())\n\n" ^
"}\n"
val code' = code
|> unsuffix "}\n"
|> suffix "data Typerep = Typerep String [Typerep];\n\n}\n" (* FIXME *)
- val _ = File.write code_file code'
- val _ = File.write narrowing_engine_file
- (if contains_existentials then pnf_narrowing_engine else narrowing_engine)
- val _ = File.write main_file main
+ val _ = map (uncurry File.write) (includes @
+ [(narrowing_engine_file, if contains_existentials then pnf_narrowing_engine else narrowing_engine),
+ (code_file, code'), (main_file, main)])
val executable = File.shell_path (Path.append in_path (Path.basic "isabelle_quickcheck_narrowing"))
val cmd = "exec \"$ISABELLE_GHC\" " ^ Code_Haskell.language_params ^ " " ^
ghc_options ^ " " ^
- (space_implode " " (map File.shell_path [code_file, narrowing_engine_file, main_file])) ^
+ (space_implode " " (map File.shell_path (map fst includes @ [code_file, narrowing_engine_file, main_file]))) ^
" -o " ^ executable ^ ";"
val (result, compilation_time) =
- elapsed_time "Haskell compilation" (fn () => Isabelle_System.bash cmd)
+ elapsed_time "Haskell compilation" (fn () => Isabelle_System.bash cmd)
val _ = Quickcheck.add_timing compilation_time current_result
fun haskell_string_of_bool v = if v then "True" else "False"
val _ = if Isabelle_System.bash cmd <> 0 then error "Compilation with GHC failed" else ()
@@ -314,7 +317,7 @@
val ctxt = Proof_Context.init_global thy
fun evaluator naming program ((_, vs_ty), t) deps =
Exn.interruptible_capture (value opts ctxt cookie)
- (Code_Target.evaluator thy target naming program deps (vs_ty, t));
+ (Code_Target.evaluator thy target naming program deps (vs_ty, t));
in Exn.release (Code_Thingol.dynamic_value thy (Exn.map_result o postproc) evaluator t) end;
(** counterexample generator **)
--- a/src/Tools/Code/code_haskell.ML Fri Jul 27 21:57:56 2012 +0200
+++ b/src/Tools/Code/code_haskell.ML Fri Jul 27 22:26:38 2012 +0200
@@ -395,7 +395,7 @@
Code_Target.serialization
(fn width => fn destination => K () o map (write_module width destination))
(fn present => fn width => rpair (try (deresolver ""))
- o format present width o Pretty.chunks o map snd)
+ o (map o apsnd) (format present width))
(map (uncurry print_module_frame o apsnd single) includes
@ map (fn module_name => print_module module_name (Graph.get_node haskell_program module_name))
((flat o rev o Graph.strong_conn) haskell_program))
--- a/src/Tools/Code/code_ml.ML Fri Jul 27 21:57:56 2012 +0200
+++ b/src/Tools/Code/code_ml.ML Fri Jul 27 22:26:38 2012 +0200
@@ -811,8 +811,9 @@
lift_markup = apsnd } ml_program));
fun write width NONE = writeln o format [] width
| write width (SOME p) = File.write p o format [] width;
+ fun prepare names width p = ([("", format names width p)], try (deresolver []));
in
- Code_Target.serialization write (rpair (try (deresolver [])) ooo format) p
+ Code_Target.serialization write prepare p
end;
val serializer_sml : Code_Target.serializer =
--- a/src/Tools/Code/code_runtime.ML Fri Jul 27 21:57:56 2012 +0200
+++ b/src/Tools/Code/code_runtime.ML Fri Jul 27 22:26:38 2012 +0200
@@ -87,7 +87,9 @@
val ctxt = Proof_Context.init_global thy;
in ((Sign.no_frees ctxt o Sign.no_vars ctxt o map_types (K dummyT)) t; t) end;
-fun obtain_evaluator thy some_target = Code_Target.evaluator thy (the_default target some_target);
+fun obtain_evaluator thy some_target naming program consts expr =
+ Code_Target.evaluator thy (the_default target some_target) naming program consts expr
+ |> apfst (fn ml_modules => space_implode "\n\n" (map snd ml_modules));
fun evaluation cookie thy evaluator vs_t args =
let
@@ -192,9 +194,10 @@
val ctxt = Proof_Context.init_global thy;
val (consts', (naming, program)) = Code_Thingol.consts_program thy false consts;
val tycos' = map (the o Code_Thingol.lookup_tyco naming) tycos;
- val (ml_code, target_names) =
+ val (ml_modules, target_names) =
Code_Target.produce_code_for thy
target NONE module_name [] naming program (consts' @ tycos');
+ val ml_code = space_implode "\n\n" (map snd ml_modules);
val (consts'', tycos'') = chop (length consts') target_names;
val consts_map = map2 (fn const =>
fn NONE =>
--- a/src/Tools/Code/code_scala.ML Fri Jul 27 21:57:56 2012 +0200
+++ b/src/Tools/Code/code_scala.ML Fri Jul 27 22:26:38 2012 +0200
@@ -385,8 +385,9 @@
lift_markup = I } scala_program);
fun write width NONE = writeln o format [] width
| write width (SOME p) = File.write p o format [] width;
+ fun prepare names width p = ([("", format names width p)], try (deresolver []));
in
- Code_Target.serialization write (rpair (try (deresolver [])) ooo format) p
+ Code_Target.serialization write prepare p
end;
val serializer : Code_Target.serializer =
--- a/src/Tools/Code/code_target.ML Fri Jul 27 21:57:56 2012 +0200
+++ b/src/Tools/Code/code_target.ML Fri Jul 27 22:26:38 2012 +0200
@@ -13,7 +13,7 @@
val export_code_for: theory -> Path.T option -> string -> int option -> string -> Token.T list
-> Code_Thingol.naming -> Code_Thingol.program -> string list -> unit
val produce_code_for: theory -> string -> int option -> string -> Token.T list
- -> Code_Thingol.naming -> Code_Thingol.program -> string list -> string * string option list
+ -> Code_Thingol.naming -> Code_Thingol.program -> string list -> (string * string) list * string option list
val present_code_for: theory -> string -> int option -> string -> Token.T list
-> Code_Thingol.naming -> Code_Thingol.program -> string list * string list -> string
val check_code_for: theory -> string -> bool -> Token.T list
@@ -22,15 +22,16 @@
val export_code: theory -> string list
-> (((string * string) * Path.T option) * Token.T list) list -> unit
val produce_code: theory -> string list
- -> string -> int option -> string -> Token.T list -> string * string option list
+ -> string -> int option -> string -> Token.T list -> (string * string) list * string option list
val present_code: theory -> string list -> (Code_Thingol.naming -> string list)
-> string -> int option -> string -> Token.T list -> string
val check_code: theory -> string list
-> ((string * bool) * Token.T list) list -> unit
+ val generatedN: string
val evaluator: theory -> string -> Code_Thingol.naming -> Code_Thingol.program
-> string list -> ((string * class list) list * Code_Thingol.itype) * Code_Thingol.iterm
- -> string * string
+ -> (string * string) list * string
type serializer
type literals = Code_Printer.literals
@@ -45,7 +46,7 @@
type serialization
val parse_args: 'a parser -> Token.T list -> 'a
val serialization: (int -> Path.T option -> 'a -> unit)
- -> (string list -> int -> 'a -> string * (string -> string option))
+ -> (string list -> int -> 'a -> (string * string) list * (string -> string option))
-> 'a -> serialization
val set_default_code_width: int -> theory -> theory
@@ -77,7 +78,7 @@
(** abstract nonsense **)
datatype destination = Export of Path.T option | Produce | Present of string list;
-type serialization = int -> destination -> (string * (string -> string option)) option;
+type serialization = int -> destination -> ((string * string) list * (string -> string option)) option;
fun serialization output _ content width (Export some_path) =
(output width some_path content; NONE)
@@ -85,12 +86,12 @@
string [] width content |> SOME
| serialization _ string content width (Present stmt_names) =
string stmt_names width content
- |> apfst (Pretty.output (SOME width) o Pretty.str)
+ |> (apfst o map o apsnd) (Pretty.output (SOME width) o Pretty.str)
|> SOME;
fun export some_path f = (f (Export some_path); ());
fun produce f = the (f Produce);
-fun present stmt_names f = fst (the (f (Present stmt_names)));
+fun present stmt_names f = space_implode "\n\n" (map snd (fst (the (f (Present stmt_names)))));
(** theory data **)
@@ -378,6 +379,8 @@
in
+val generatedN = "Generated_Code";
+
fun export_code_for thy some_path target some_width module_name args =
export (using_master_directory thy some_path)
ooo invoke_serializer thy target some_width module_name args;
@@ -398,15 +401,14 @@
fun check_code_for thy target strict args naming program names_cs =
let
- val module_name = "Generated_Code";
val { env_var, make_destination, make_command } =
(#check o the_fundamental thy) target;
fun ext_check p =
let
val destination = make_destination p;
val _ = export (SOME destination) (invoke_serializer thy target (SOME 80)
- module_name args naming program names_cs);
- val cmd = make_command module_name;
+ generatedN args naming program names_cs);
+ val cmd = make_command generatedN;
in
if Isabelle_System.bash ("cd " ^ File.shell_path p ^ " && " ^ cmd ^ " 2>&1") <> 0
then error ("Code check failed for " ^ target ^ ": " ^ cmd)
@@ -439,7 +441,7 @@
fun evaluator thy target naming program consts =
let
val (mounted_serializer, prepared_program) = mount_serializer thy
- target NONE "Generated_Code" [] naming program consts;
+ target NONE generatedN [] naming program consts;
in evaluation mounted_serializer prepared_program consts end;
end; (* local *)