tuned whitespace;
authorwenzelm
Sat, 17 Dec 2016 12:24:13 +0100
changeset 64577 0288a566c966
parent 64576 ce8802dc3145
child 64578 7b20f9f94f4e
tuned whitespace; tuned comments;
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 \<Rightarrow> yxml_of_term) option"}
   | mk_term_of ts =
-  let
-    val tuple = mk_tuples ts
-    val T = fastype_of tuple
-  in
-    @{term "Some :: (unit \<Rightarrow> yxml_of_term) \<Rightarrow> (unit \<Rightarrow> 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 \<Rightarrow> yxml_of_term) \<Rightarrow> (unit \<Rightarrow> 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
-