# HG changeset patch # User haftmann # Date 1279112882 -7200 # Node ID cf35881776762b30d3f5bc5b4e754d6c8dad52c3 # Parent 3cbb22cec751f3e993ab904164409dbb4dcb74ee use generic description slot for formal code checking diff -r 3cbb22cec751 -r cf3588177676 src/Tools/Code/code_haskell.ML --- 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, diff -r 3cbb22cec751 -r cf3588177676 src/Tools/Code/code_ml.ML --- 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, diff -r 3cbb22cec751 -r cf3588177676 src/Tools/Code/code_scala.ML --- 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 ( diff -r 3cbb22cec751 -r cf3588177676 src/Tools/Code/code_target.ML --- 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;