--- a/src/Tools/Code/code_haskell.ML Wed Jul 14 14:53:44 2010 +0200
+++ b/src/Tools/Code/code_haskell.ML Wed Jul 14 15:08:02 2010 +0200
@@ -7,7 +7,6 @@
signature CODE_HASKELL =
sig
val target: string
- val check: theory -> unit
val setup: theory -> theory
end;
@@ -464,14 +463,6 @@
else error "Only Haskell target allows for monad syntax" end;
-(** formal checking of compiled code **)
-
-fun check thy = Code_Target.external_check thy target
- "EXEC_GHC" I (fn ghc => fn p => fn module_name =>
- ghc ^ " -fglasgow-exts -odir build -hidir build -stubdir build -e \"\" " ^ module_name ^ ".hs");
-
-
-
(** Isar setup **)
fun isar_serializer module_name =
@@ -488,7 +479,10 @@
val setup =
Code_Target.add_target
- (target, { serializer = isar_serializer, literals = literals, check = () })
+ (target, { serializer = isar_serializer, literals = literals,
+ check = { env_var = "EXEC_GHC", make_destination = I,
+ make_command = fn ghc => fn p => fn module_name =>
+ ghc ^ " -fglasgow-exts -odir build -hidir build -stubdir build -e \"\" " ^ module_name ^ ".hs" } })
#> Code_Target.add_syntax_tyco target "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
brackify_infix (1, R) fxy (
print_typ (INFX (1, X)) ty1,
--- a/src/Tools/Code/code_ml.ML Wed Jul 14 14:53:44 2010 +0200
+++ b/src/Tools/Code/code_ml.ML Wed Jul 14 15:08:02 2010 +0200
@@ -12,8 +12,6 @@
-> Code_Thingol.naming -> Code_Thingol.program -> string list -> string * string option list
val print_tuple: (Code_Printer.fixity -> 'a -> Pretty.T)
-> Code_Printer.fixity -> 'a list -> Pretty.T option
- val check_SML: theory -> unit
- val check_OCaml: theory -> unit
val setup: theory -> theory
end;
@@ -952,17 +950,6 @@
serialize_ml target print_sml_module print_sml_stmt (SOME struct_name) true);
-(** formal checking of compiled code **)
-
-fun check_SML thy = Code_Target.external_check thy target_SML
- "ISABELLE_PROCESS" (fn p => Path.append p (Path.explode "ROOT.ML"))
- (fn isabelle => fn p => fn _ => isabelle ^ " -r -q -u Pure");
-
-fun check_OCaml thy = Code_Target.external_check thy target_OCaml
- "EXEC_OCAML" (fn p => Path.append p (Path.explode "ROOT.ocaml"))
- (fn ocaml => fn p => fn _ => ocaml ^ " -w pu nums.cma " ^ File.shell_path p);
-
-
(** Isar setup **)
fun isar_serializer_sml module_name =
@@ -977,9 +964,13 @@
val setup =
Code_Target.add_target
- (target_SML, { serializer = isar_serializer_sml, literals = literals_sml, check = () })
+ (target_SML, { serializer = isar_serializer_sml, literals = literals_sml,
+ check = { env_var = "ISABELLE_PROCESS", make_destination = fn p => Path.append p (Path.explode "ROOT.ML"),
+ make_command = fn isabelle => fn p => fn _ => isabelle ^ " -r -q -u Pure" } })
#> Code_Target.add_target
- (target_OCaml, { serializer = isar_serializer_ocaml, literals = literals_ocaml, check = () })
+ (target_OCaml, { serializer = isar_serializer_ocaml, literals = literals_ocaml,
+ check = { env_var = "EXEC_OCAML", make_destination = fn p => Path.append p (Path.explode "ROOT.ocaml"),
+ make_command = fn ocaml => fn p => fn _ => ocaml ^ " -w pu nums.cma " ^ File.shell_path p } })
#> Code_Target.add_syntax_tyco target_SML "fun" (SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
brackify_infix (1, R) fxy (
print_typ (INFX (1, X)) ty1,
--- a/src/Tools/Code/code_scala.ML Wed Jul 14 14:53:44 2010 +0200
+++ b/src/Tools/Code/code_scala.ML Wed Jul 14 15:08:02 2010 +0200
@@ -7,7 +7,6 @@
signature CODE_SCALA =
sig
val target: string
- val check: theory -> unit
val setup: theory -> theory
end;
@@ -414,14 +413,6 @@
} end;
-(** formal checking of compiled code **)
-
-fun check thy = Code_Target.external_check thy target
- "SCALA_HOME" I (fn scala_home => fn p => fn _ =>
- Path.implode (Path.append (Path.explode scala_home) (Path.explode "bin/scalac")) ^ " *.scala");
-
-
-
(** Isar setup **)
fun isar_serializer module_name =
@@ -430,7 +421,10 @@
val setup =
Code_Target.add_target
- (target, { serializer = isar_serializer, literals = literals, check = () })
+ (target, { serializer = isar_serializer, literals = literals,
+ check = { env_var = "SCALA_HOME", make_destination = I,
+ make_command = fn scala_home => fn p => fn _ =>
+ Path.implode (Path.append (Path.explode scala_home) (Path.explode "bin/scalac")) ^ " *.scala" } })
#> Code_Target.add_syntax_tyco target "fun"
(SOME (2, fn print_typ => fn fxy => fn [ty1, ty2] =>
brackify_infix (1, R) fxy (
--- a/src/Tools/Code/code_target.ML Wed Jul 14 14:53:44 2010 +0200
+++ b/src/Tools/Code/code_target.ML Wed Jul 14 15:08:02 2010 +0200
@@ -11,8 +11,9 @@
type serializer
type literals = Code_Printer.literals
- val add_target: string * { serializer: serializer, literals: literals, check: unit }
- -> theory -> theory
+ val add_target: string * { serializer: serializer, literals: literals,
+ check: { env_var: string, make_destination: Path.T -> Path.T,
+ make_command: string -> Path.T -> string -> string } } -> theory -> theory
val extend_target: string *
(string * (Code_Thingol.naming -> Code_Thingol.program -> Code_Thingol.program))
-> theory -> theory
@@ -35,8 +36,7 @@
val string: string list -> serialization -> string
val code_of: theory -> string -> int option -> string
-> string list -> (Code_Thingol.naming -> string list) -> string
- val external_check: theory -> string -> string
- -> (Path.T -> Path.T) -> (string -> Path.T -> string -> string) -> unit
+ val check: theory -> string -> unit
val set_default_code_width: int -> theory -> theory
val shell_command: string (*theory name*) -> string (*export_code expr*) -> unit
@@ -115,7 +115,9 @@
-> string list (*selected statements*)
-> serialization;
-datatype description = Fundamental of { serializer: serializer, literals: Code_Printer.literals, check: unit }
+datatype description = Fundamental of { serializer: serializer, literals: Code_Printer.literals,
+ check: { env_var: string, make_destination: Path.T -> Path.T,
+ make_command: string -> Path.T -> string -> string } }
| Extension of string * (Code_Thingol.naming -> Code_Thingol.program -> Code_Thingol.program);
datatype target = Target of {
@@ -221,15 +223,17 @@
(* montage *)
-fun the_literals thy =
+fun the_fundamental thy =
let
val ((targets, _), _) = Targets.get thy;
- fun literals target = case Symtab.lookup targets target
+ fun fundamental target = case Symtab.lookup targets target
of SOME data => (case the_description data
- of Fundamental { literals, ... } => literals
- | Extension (super, _) => literals super)
+ of Fundamental data => data
+ | Extension (super, _) => fundamental super)
| NONE => error ("Unknown code target language: " ^ quote target);
- in literals end;
+ in fundamental end;
+
+fun the_literals thy = #literals o the_fundamental thy;
local
@@ -353,8 +357,10 @@
if member (op =) names3 name then SOME c else NONE) (cs2 ~~ names2);
in union (op =) cs3 cs1 end;
-fun external_check thy target env_var make_destination make_command =
+fun check thy target =
let
+ val { env_var, make_destination, make_command } =
+ (#check o the_fundamental thy) target;
val env_param = getenv env_var;
fun ext_check env_param p =
let
@@ -374,6 +380,7 @@
else Cache_IO.with_tmp_dir "Code_Test" (ext_check env_param)
end;
+
fun export_code thy cs seris =
let
val (cs', (naming, program)) = Code_Thingol.consts_program thy false cs;