# HG changeset patch # User wenzelm # Date 1481973853 -3600 # Node ID 0288a566c96659e9cffe65b40540661ec9fdc7fc # Parent ce8802dc31450a3781790cf33b14226d91b74a12 tuned whitespace; tuned comments; diff -r ce8802dc3145 -r 0288a566c966 src/HOL/Library/code_test.ML --- a/src/HOL/Library/code_test.ML Fri Dec 16 22:54:14 2016 +0100 +++ b/src/HOL/Library/code_test.ML Sat Dec 17 12:24:13 2016 +0100 @@ -1,59 +1,66 @@ (* Title: HOL/Library/code_test.ML - Author: Andreas Lochbihler, ETH Zurich + Author: Andreas Lochbihler, ETH Zürich -Test infrastructure for the code generator +Test infrastructure for the code generator. *) -signature CODE_TEST = sig - val add_driver : string * ((Proof.context -> (string * string) list * string -> Path.T -> string) * string) -> theory -> theory - val get_driver : theory -> string -> ((Proof.context -> (string * string) list * string -> Path.T -> string) * string) option - val overlord : bool Config.T - val successN : string - val failureN : string - val start_markerN : string - val end_markerN : string - val test_terms : Proof.context -> term list -> string -> unit - val test_targets : Proof.context -> term list -> string list -> unit list - val test_code_cmd : string list -> string list -> Toplevel.state -> unit +signature CODE_TEST = +sig + val add_driver: + string * ((Proof.context -> (string * string) list * string -> Path.T -> string) * string) -> + theory -> theory + val get_driver: theory -> string -> + ((Proof.context -> (string * string) list * string -> Path.T -> string) * string) option + val overlord: bool Config.T + val successN: string + val failureN: string + val start_markerN: string + val end_markerN: string + val test_terms: Proof.context -> term list -> string -> unit + val test_targets: Proof.context -> term list -> string list -> unit list + val test_code_cmd: string list -> string list -> Toplevel.state -> unit - val eval_term : string -> Proof.context -> term -> term - - val gen_driver : - (theory -> Path.T -> string list -> string -> - {files : (Path.T * string) list, - compile_cmd : string option, run_cmd : string, mk_code_file : string -> Path.T}) - -> string -> string -> string - -> theory -> (string * string) list * string -> Path.T -> string + val eval_term: string -> Proof.context -> term -> term - val ISABELLE_POLYML : string - val polymlN : string - val evaluate_in_polyml : Proof.context -> (string * string) list * string -> Path.T -> string + val gen_driver: + (theory -> Path.T -> string list -> string -> + {files: (Path.T * string) list, + compile_cmd: string option, + run_cmd: string, + mk_code_file: string -> Path.T}) -> + string -> string -> string -> theory -> (string * string) list * string -> Path.T -> string - val mltonN : string - val ISABELLE_MLTON : string - val evaluate_in_mlton : Proof.context -> (string * string) list * string -> Path.T -> string + val ISABELLE_POLYML: string + val polymlN: string + val evaluate_in_polyml: Proof.context -> (string * string) list * string -> Path.T -> string - val smlnjN : string - val ISABELLE_SMLNJ : string - val evaluate_in_smlnj : Proof.context -> (string * string) list * string -> Path.T -> string + val mltonN: string + val ISABELLE_MLTON: string + val evaluate_in_mlton: Proof.context -> (string * string) list * string -> Path.T -> string - val ocamlN : string - val ISABELLE_OCAMLC : string - val evaluate_in_ocaml : Proof.context -> (string * string) list * string -> Path.T -> string + val smlnjN: string + val ISABELLE_SMLNJ: string + val evaluate_in_smlnj: Proof.context -> (string * string) list * string -> Path.T -> string + + val ocamlN: string + val ISABELLE_OCAMLC: string + val evaluate_in_ocaml: Proof.context -> (string * string) list * string -> Path.T -> string - val ghcN : string - val ISABELLE_GHC : string - val ghc_options : string Config.T - val evaluate_in_ghc : Proof.context -> (string * string) list * string -> Path.T -> string + val ghcN: string + val ISABELLE_GHC: string + val ghc_options: string Config.T + val evaluate_in_ghc: Proof.context -> (string * string) list * string -> Path.T -> string - val scalaN : string - val ISABELLE_SCALA : string - val evaluate_in_scala : Proof.context -> (string * string) list * string -> Path.T -> string + val scalaN: string + val ISABELLE_SCALA: string + val evaluate_in_scala: Proof.context -> (string * string) list * string -> Path.T -> string end -structure Code_Test : CODE_TEST = struct +structure Code_Test: CODE_TEST = +struct (* convert a list of terms into nested tuples and back *) + fun mk_tuples [] = @{term "()"} | mk_tuples [t] = t | mk_tuples (t :: ts) = HOLogic.mk_prod (t, mk_tuples ts) @@ -67,42 +74,44 @@ fun last_field sep str = let - val n = size sep; - val len = size str; + val n = size sep + val len = size str fun find i = if i < 0 then NONE else if String.substring (str, i, n) = sep then SOME i - else find (i - 1); + else find (i - 1) in (case find (len - n) of NONE => NONE | SOME i => SOME (String.substring (str, 0, i), String.extract (str, i + n, NONE))) - end; + end fun split_first_last start stop s = - case first_field start s - of NONE => NONE - | SOME (initial, rest) => - case last_field stop rest - of NONE => NONE - | SOME (middle, tail) => SOME (initial, middle, tail); + (case first_field start s of + NONE => NONE + | SOME (initial, rest) => + (case last_field stop rest of + NONE => NONE + | SOME (middle, tail) => SOME (initial, middle, tail))) -(* Data slot for drivers *) + +(* data slot for drivers *) structure Drivers = Theory_Data ( - type T = (string * ((Proof.context -> (string * string) list * string -> Path.T -> string) * string)) list; - val empty = []; - val extend = I; - fun merge data : T = AList.merge (op =) (K true) data; + type T = + (string * ((Proof.context -> (string * string) list * string -> Path.T -> string) * string)) list + val empty = [] + val extend = I + fun merge data : T = AList.merge (op =) (K true) data ) -val add_driver = Drivers.map o AList.update (op =); -val get_driver = AList.lookup (op =) o Drivers.get; +val add_driver = Drivers.map o AList.update (op =) +val get_driver = AList.lookup (op =) o Drivers.get (* Test drivers must produce output of the following format: - + The start of the relevant data is marked with start_markerN, its end with end_markerN. @@ -112,7 +121,8 @@ There must not be any additional whitespace in between. *) -(* Parsing of results *) + +(* parsing of results *) val successN = "True" val failureN = "False" @@ -121,7 +131,7 @@ fun parse_line line = if String.isPrefix successN line then (true, NONE) - else if String.isPrefix failureN line then (false, + else if String.isPrefix failureN line then (false, if size line > size failureN then String.extract (line, size failureN, NONE) |> YXML.parse_body @@ -132,20 +142,21 @@ else raise Fail ("Cannot parse result of evaluation:\n" ^ line) fun parse_result target out = - case split_first_last start_markerN end_markerN out - of NONE => error ("Evaluation failed for " ^ target ^ "!\nBash output:\n" ^ out) - | SOME (_, middle, _) => middle |> trim_line |> split_lines |> map parse_line + (case split_first_last start_markerN end_markerN out of + NONE => error ("Evaluation failed for " ^ target ^ "!\nBash output:\n" ^ out) + | SOME (_, middle, _) => middle |> trim_line |> split_lines |> map parse_line) -(* Pretty printing of test results *) + +(* pretty printing of test results *) fun pretty_eval _ NONE _ = [] - | pretty_eval ctxt (SOME evals) ts = - [Pretty.fbrk, - Pretty.big_list "Evaluated terms" - (map (fn (t, eval) => Pretty.block - [Syntax.pretty_term ctxt t, Pretty.brk 1, Pretty.str "=", Pretty.brk 1, - Syntax.pretty_term ctxt eval]) - (ts ~~ evals))] + | pretty_eval ctxt (SOME evals) ts = + [Pretty.fbrk, + Pretty.big_list "Evaluated terms" + (map (fn (t, eval) => Pretty.block + [Syntax.pretty_term ctxt t, Pretty.brk 1, Pretty.str "=", Pretty.brk 1, + Syntax.pretty_term ctxt eval]) + (ts ~~ evals))] fun pretty_failure ctxt target (((_, evals), query), eval_ts) = Pretty.block (Pretty.text ("Test in " ^ target ^ " failed for") @@ -155,60 +166,61 @@ fun pretty_failures ctxt target failures = Pretty.blk (0, Pretty.fbreaks (map (pretty_failure ctxt target) failures)) -(* Driver invocation *) -val overlord = Attrib.setup_config_bool @{binding "code_test_overlord"} (K false); +(* driver invocation *) + +val overlord = Attrib.setup_config_bool @{binding "code_test_overlord"} (K false) fun with_overlord_dir name f = let - val path = Path.append (Path.explode "$ISABELLE_HOME_USER") (Path.basic (name ^ serial_string ())) - val _ = Isabelle_System.mkdirs path; - in - Exn.release (Exn.capture f path) - end; + val path = + Path.append (Path.explode "$ISABELLE_HOME_USER") (Path.basic (name ^ serial_string ())) + val _ = Isabelle_System.mkdirs path + in Exn.release (Exn.capture f path) end fun dynamic_value_strict ctxt t compiler = let val thy = Proof_Context.theory_of ctxt - val (driver, target) = case get_driver thy compiler - of NONE => error ("No driver for target " ^ compiler) - | SOME f => f; + val (driver, target) = + (case get_driver thy compiler of + NONE => error ("No driver for target " ^ compiler) + | SOME f => f) val debug = Config.get (Proof_Context.init_global thy) overlord val with_dir = if debug then with_overlord_dir else Isabelle_System.with_tmp_dir fun evaluate f = with_dir "Code_Test" (driver ctxt f) |> parse_result compiler fun evaluator program _ vs_ty deps = - Exn.interruptible_capture evaluate (Code_Target.computation_text ctxt target program deps true vs_ty); + Exn.interruptible_capture evaluate + (Code_Target.computation_text ctxt target program deps true vs_ty) fun postproc f = map (apsnd (map_option (map f))) - in - Exn.release (Code_Thingol.dynamic_value ctxt (Exn.map_res o postproc) evaluator t) - end; + in Exn.release (Code_Thingol.dynamic_value ctxt (Exn.map_res o postproc) evaluator t) end -(* Term preprocessing *) + +(* term preprocessing *) fun add_eval (Const (@{const_name Trueprop}, _) $ t) = add_eval t | add_eval (Const (@{const_name "HOL.eq"}, _) $ lhs $ rhs) = (fn acc => - acc - |> add_eval rhs - |> add_eval lhs - |> cons rhs - |> cons lhs) + acc + |> add_eval rhs + |> add_eval lhs + |> cons rhs + |> cons lhs) | add_eval (Const (@{const_name "Not"}, _) $ t) = add_eval t | add_eval (Const (@{const_name "Orderings.ord_class.less_eq"}, _) $ lhs $ rhs) = (fn acc => - lhs :: rhs :: acc) + lhs :: rhs :: acc) | add_eval (Const (@{const_name "Orderings.ord_class.less"}, _) $ lhs $ rhs) = (fn acc => - lhs :: rhs :: acc) + lhs :: rhs :: acc) | add_eval _ = I fun mk_term_of [] = @{term "None :: (unit \ yxml_of_term) option"} | mk_term_of ts = - let - val tuple = mk_tuples ts - val T = fastype_of tuple - in - @{term "Some :: (unit \ yxml_of_term) \ (unit \ yxml_of_term) option"} $ - (absdummy @{typ unit} (@{const yxml_string_of_term} $ - (Const (@{const_name Code_Evaluation.term_of}, T --> @{typ term}) $ tuple))) - end + let + val tuple = mk_tuples ts + val T = fastype_of tuple + in + @{term "Some :: (unit \ yxml_of_term) \ (unit \ yxml_of_term) option"} $ + (absdummy @{typ unit} (@{const yxml_string_of_term} $ + (Const (@{const_name Code_Evaluation.term_of}, T --> @{typ term}) $ tuple))) + end fun test_terms ctxt ts target = let @@ -216,24 +228,28 @@ fun term_of t = Sign.of_sort thy (fastype_of t, @{sort term_of}) - fun ensure_bool t = case fastype_of t of @{typ bool} => () - | _ => error ("Test case not of type bool: " ^ Pretty.string_of (Syntax.pretty_term ctxt t)) + fun ensure_bool t = + (case fastype_of t of + @{typ bool} => () + | _ => error ("Test case not of type bool: " ^ Pretty.string_of (Syntax.pretty_term ctxt t))) val _ = map ensure_bool ts val evals = map (fn t => filter term_of (add_eval t [])) ts val eval = map mk_term_of evals - val T = HOLogic.mk_prodT (@{typ bool}, Type (@{type_name option}, [@{typ unit} --> @{typ yxml_of_term}])) + val T = + HOLogic.mk_prodT (@{typ bool}, + Type (@{type_name option}, [@{typ unit} --> @{typ yxml_of_term}])) val t = HOLogic.mk_list T (map HOLogic.mk_prod (ts ~~ eval)) - val result = dynamic_value_strict ctxt t target; + val result = dynamic_value_strict ctxt t target val failed = filter_out (fst o fst o fst) (result ~~ ts ~~ evals) - handle ListPair.UnequalLengths => + handle ListPair.UnequalLengths => error ("Evaluation failed!\nWrong number of test results: " ^ Int.toString (length result)) - val _ = case failed of [] => () + val _ = case failed of [] => () | _ => error (Pretty.string_of (pretty_failures ctxt target failed)) in () @@ -243,8 +259,8 @@ fun test_code_cmd raw_ts targets state = let - val ctxt = Toplevel.context_of state; - val ts = Syntax.read_terms ctxt raw_ts; + val ctxt = Toplevel.context_of state + val ts = Syntax.read_terms ctxt raw_ts val frees = fold Term.add_free_names ts [] val _ = if frees = [] then () else error ("Terms contain free variables: " ^ @@ -263,41 +279,41 @@ val thy = Proof_Context.theory_of ctxt val T_t = fastype_of t - val _ = if Sign.of_sort thy (T_t, @{sort term_of}) then () else error - ("Type " ^ Pretty.string_of (Syntax.pretty_typ ctxt T_t) ^ + val _ = if Sign.of_sort thy (T_t, @{sort term_of}) then () else error + ("Type " ^ Pretty.string_of (Syntax.pretty_typ ctxt T_t) ^ " of term not of sort " ^ Pretty.string_of (Syntax.pretty_sort ctxt @{sort term_of})) val T = HOLogic.mk_prodT (@{typ bool}, Type (@{type_name option}, [@{typ unit} --> @{typ yxml_of_term}])) val t' = HOLogic.mk_list T [HOLogic.mk_prod (@{term "False"}, mk_term_of [t])] - val result = dynamic_value_strict ctxt t' target; - in - case result of [(_, SOME [t])] => t | _ => error "Evaluation failed" - end + val result = dynamic_value_strict ctxt t' target + in (case result of [(_, SOME [t])] => t | _ => error "Evaluation failed") end -(* Generic driver *) + +(* generic driver *) fun gen_driver mk_driver env_var env_var_dest compilerN ctxt (code_files, value_name) = let val compiler = getenv env_var - val _ = if compiler <> "" then () else error (Pretty.string_of (Pretty.para + val _ = + if compiler <> "" then () + else error (Pretty.string_of (Pretty.para ("Environment variable " ^ env_var ^ " is not set. To test code generation with " ^ compilerN ^ ", set this variable to your " ^ env_var_dest ^ " in the settings file."))) fun compile NONE = () | compile (SOME cmd) = - let - val (out, ret) = Isabelle_System.bash_output cmd - in - if ret = 0 then () else error - ("Compilation with " ^ compilerN ^ " failed:\n" ^ cmd ^ "\n" ^ out) - end + let + val (out, ret) = Isabelle_System.bash_output cmd + in + if ret = 0 then () else error + ("Compilation with " ^ compilerN ^ " failed:\n" ^ cmd ^ "\n" ^ out) + end - fun run (path : Path.T)= + fun run path = let val modules = map fst code_files - val {files, compile_cmd, run_cmd, mk_code_file} - = mk_driver ctxt path modules value_name + val {files, compile_cmd, run_cmd, mk_code_file} = mk_driver ctxt path modules value_name val _ = map (fn (name, code) => File.write (mk_code_file name) code) code_files val _ = map (fn (name, content) => File.write name content) files @@ -308,17 +324,14 @@ val _ = if res = 0 then () else error ("Evaluation for " ^ compilerN ^ " terminated with error code " ^ Int.toString res ^ "\nBash output:\n" ^ out) - in - out - end - in - run - end + in out end + in run end -(* Driver for PolyML *) + +(* driver for PolyML *) val ISABELLE_POLYML = "ISABELLE_POLYML" -val polymlN = "PolyML"; +val polymlN = "PolyML" fun mk_driver_polyml _ path _ value_name = let @@ -327,10 +340,10 @@ val code_path = Path.append path (Path.basic generatedN) val driver_path = Path.append path (Path.basic driverN) - val driver = + val driver = "fun main prog_name = \n" ^ " let\n" ^ - " fun format_term NONE = \"\"\n" ^ + " fun format_term NONE = \"\"\n" ^ " | format_term (SOME t) = t ();\n" ^ " fun format (true, _) = \"" ^ successN ^ "\\n\"\n" ^ " | format (false, to) = \"" ^ failureN ^ "\" ^ format_term to ^ \"\\n\";\n" ^ @@ -342,8 +355,8 @@ " ()\n" ^ " end;\n" val cmd = - "echo \"use \\\"" ^ Path.implode code_path ^ "\\\"; use \\\"" ^ - Path.implode driver_path ^ "\\\"; main ();\" | " ^ + "echo \"use \\\"" ^ Path.implode code_path ^ "\\\"; use \\\"" ^ + Path.implode driver_path ^ "\\\"; main ();\" | " ^ Path.implode (Path.variable ISABELLE_POLYML) in {files = [(driver_path, driver)], compile_cmd = NONE, run_cmd = cmd, mk_code_file = K code_path} @@ -352,7 +365,8 @@ fun evaluate_in_polyml ctxt = gen_driver mk_driver_polyml ISABELLE_POLYML "PolyML executable" polymlN ctxt -(* Driver for mlton *) + +(* driver for mlton *) val mltonN = "MLton" val ISABELLE_MLTON = "ISABELLE_MLTON" @@ -367,8 +381,8 @@ val code_path = Path.append path (Path.basic generatedN) val driver_path = Path.append path (Path.basic driverN) val ml_basis_path = Path.append path (Path.basic ml_basisN) - val driver = - "fun format_term NONE = \"\"\n" ^ + val driver = + "fun format_term NONE = \"\"\n" ^ " | format_term (SOME t) = t ();\n" ^ "fun format (true, _) = \"" ^ successN ^ "\\n\"\n" ^ " | format (false, to) = \"" ^ failureN ^ "\" ^ format_term to ^ \"\\n\";\n" ^ @@ -393,7 +407,8 @@ fun evaluate_in_mlton ctxt = gen_driver mk_driver_mlton ISABELLE_MLTON "MLton executable" mltonN ctxt -(* Driver for SML/NJ *) + +(* driver for SML/NJ *) val smlnjN = "SMLNJ" val ISABELLE_SMLNJ = "ISABELLE_SMLNJ" @@ -405,11 +420,11 @@ val code_path = Path.append path (Path.basic generatedN) val driver_path = Path.append path (Path.basic driverN) - val driver = + val driver = "structure Test = struct\n" ^ "fun main prog_name =\n" ^ " let\n" ^ - " fun format_term NONE = \"\"\n" ^ + " fun format_term NONE = \"\"\n" ^ " | format_term (SOME t) = t ();\n" ^ " fun format (true, _) = \"" ^ successN ^ "\\n\"\n" ^ " | format (false, to) = \"" ^ failureN ^ "\" ^ format_term to ^ \"\\n\";\n" ^ @@ -432,7 +447,8 @@ fun evaluate_in_smlnj ctxt = gen_driver mk_driver_smlnj ISABELLE_SMLNJ "SMLNJ executable" smlnjN ctxt -(* Driver for OCaml *) + +(* driver for OCaml *) val ocamlN = "OCaml" val ISABELLE_OCAMLC = "ISABELLE_OCAMLC" @@ -444,9 +460,9 @@ val code_path = Path.append path (Path.basic generatedN) val driver_path = Path.append path (Path.basic driverN) - val driver = + val driver = "let format_term = function\n" ^ - " | None -> \"\"\n" ^ + " | None -> \"\"\n" ^ " | Some t -> t ();;\n" ^ "let format = function\n" ^ " | (true, _) -> \"" ^ successN ^ "\\n\"\n" ^ @@ -473,7 +489,8 @@ fun evaluate_in_ocaml ctxt = gen_driver mk_driver_ocaml ISABELLE_OCAMLC "ocamlc executable" ocamlN ctxt -(* Driver for GHC *) + +(* driver for GHC *) val ghcN = "GHC" val ISABELLE_GHC = "ISABELLE_GHC" @@ -486,12 +503,12 @@ fun mk_code_file name = Path.append path (Path.basic (name ^ ".hs")) val driver_path = Path.append path (Path.basic driverN) - val driver = + val driver = "module Main where {\n" ^ String.concat (map (fn module => "import qualified " ^ module ^ ";\n") modules) ^ "main = do {\n" ^ " let {\n" ^ - " format_term Nothing = \"\";\n" ^ + " format_term Nothing = \"\";\n" ^ " format_term (Just t) = t ();\n" ^ " format (True, _) = \"" ^ successN ^ "\\n\";\n" ^ " format (False, to) = \"" ^ failureN ^ "\" ++ format_term to ++ \"\\n\";\n" ^ @@ -518,7 +535,8 @@ fun evaluate_in_ghc ctxt = gen_driver mk_driver_ghc ISABELLE_GHC "GHC executable" ghcN ctxt -(* Driver for Scala *) + +(* driver for Scala *) val scalaN = "Scala" val ISABELLE_SCALA = "ISABELLE_SCALA" @@ -530,7 +548,7 @@ val code_path = Path.append path (Path.basic (generatedN ^ ".scala")) val driver_path = Path.append path (Path.basic driverN) - val driver = + val driver = "import " ^ generatedN ^ "._\n" ^ "object Test {\n" ^ " def format_term(x : Option[Unit => String]) : String = x match {\n" ^ @@ -567,7 +585,7 @@ val test_codeP = Scan.repeat1 Parse.prop -- (@{keyword "in"} |-- Scan.repeat1 Parse.name) -val _ = +val _ = Outer_Syntax.command @{command_keyword test_code} "compile test cases to target languages, execute them and report results" (test_codeP >> (fn (raw_ts, targets) => Toplevel.keep (test_code_cmd raw_ts targets))) @@ -580,7 +598,6 @@ (ghcN, (evaluate_in_ghc, Code_Haskell.target)), (scalaN, (evaluate_in_scala, Code_Scala.target))] #> fold (fn target => Value_Command.add_evaluator (target, eval_term target)) - [polymlN, mltonN, smlnjN, ocamlN, ghcN, scalaN]); + [polymlN, mltonN, smlnjN, ocamlN, ghcN, scalaN]) end -