src/HOL/Library/code_test.ML
changeset 64577 0288a566c966
parent 63806 c54a53ef1873
child 64578 7b20f9f94f4e
     1.1 --- a/src/HOL/Library/code_test.ML	Fri Dec 16 22:54:14 2016 +0100
     1.2 +++ b/src/HOL/Library/code_test.ML	Sat Dec 17 12:24:13 2016 +0100
     1.3 @@ -1,59 +1,66 @@
     1.4  (*  Title:      HOL/Library/code_test.ML
     1.5 -    Author:     Andreas Lochbihler, ETH Zurich
     1.6 +    Author:     Andreas Lochbihler, ETH Z├╝rich
     1.7  
     1.8 -Test infrastructure for the code generator
     1.9 +Test infrastructure for the code generator.
    1.10  *)
    1.11  
    1.12 -signature CODE_TEST = sig
    1.13 -  val add_driver : string * ((Proof.context -> (string * string) list * string -> Path.T -> string) * string) -> theory -> theory
    1.14 -  val get_driver : theory -> string -> ((Proof.context -> (string * string) list * string -> Path.T -> string) * string) option
    1.15 -  val overlord : bool Config.T
    1.16 -  val successN : string
    1.17 -  val failureN : string
    1.18 -  val start_markerN : string
    1.19 -  val end_markerN : string
    1.20 -  val test_terms : Proof.context -> term list -> string -> unit
    1.21 -  val test_targets : Proof.context -> term list -> string list -> unit list
    1.22 -  val test_code_cmd : string list -> string list -> Toplevel.state -> unit
    1.23 +signature CODE_TEST =
    1.24 +sig
    1.25 +  val add_driver:
    1.26 +    string * ((Proof.context -> (string * string) list * string -> Path.T -> string) * string) ->
    1.27 +    theory -> theory
    1.28 +  val get_driver: theory -> string ->
    1.29 +    ((Proof.context -> (string * string) list * string -> Path.T -> string) * string) option
    1.30 +  val overlord: bool Config.T
    1.31 +  val successN: string
    1.32 +  val failureN: string
    1.33 +  val start_markerN: string
    1.34 +  val end_markerN: string
    1.35 +  val test_terms: Proof.context -> term list -> string -> unit
    1.36 +  val test_targets: Proof.context -> term list -> string list -> unit list
    1.37 +  val test_code_cmd: string list -> string list -> Toplevel.state -> unit
    1.38  
    1.39 -  val eval_term : string -> Proof.context -> term -> term
    1.40 -
    1.41 -  val gen_driver :
    1.42 -   (theory -> Path.T -> string list -> string ->
    1.43 -    {files : (Path.T * string) list,
    1.44 -     compile_cmd : string option, run_cmd : string, mk_code_file : string -> Path.T})
    1.45 -   -> string -> string -> string
    1.46 -   -> theory -> (string * string) list * string -> Path.T -> string
    1.47 +  val eval_term: string -> Proof.context -> term -> term
    1.48  
    1.49 -  val ISABELLE_POLYML : string
    1.50 -  val polymlN : string
    1.51 -  val evaluate_in_polyml : Proof.context -> (string * string) list * string -> Path.T -> string
    1.52 +  val gen_driver:
    1.53 +   (theory -> Path.T -> string list -> string ->
    1.54 +    {files: (Path.T * string) list,
    1.55 +     compile_cmd: string option,
    1.56 +     run_cmd: string,
    1.57 +     mk_code_file: string -> Path.T}) ->
    1.58 +   string -> string -> string -> theory -> (string * string) list * string -> Path.T -> string
    1.59  
    1.60 -  val mltonN : string
    1.61 -  val ISABELLE_MLTON : string
    1.62 -  val evaluate_in_mlton : Proof.context -> (string * string) list * string -> Path.T -> string
    1.63 +  val ISABELLE_POLYML: string
    1.64 +  val polymlN: string
    1.65 +  val evaluate_in_polyml: Proof.context -> (string * string) list * string -> Path.T -> string
    1.66  
    1.67 -  val smlnjN : string
    1.68 -  val ISABELLE_SMLNJ : string
    1.69 -  val evaluate_in_smlnj : Proof.context -> (string * string) list * string -> Path.T -> string
    1.70 +  val mltonN: string
    1.71 +  val ISABELLE_MLTON: string
    1.72 +  val evaluate_in_mlton: Proof.context -> (string * string) list * string -> Path.T -> string
    1.73  
    1.74 -  val ocamlN : string
    1.75 -  val ISABELLE_OCAMLC : string
    1.76 -  val evaluate_in_ocaml : Proof.context -> (string * string) list * string -> Path.T -> string
    1.77 +  val smlnjN: string
    1.78 +  val ISABELLE_SMLNJ: string
    1.79 +  val evaluate_in_smlnj: Proof.context -> (string * string) list * string -> Path.T -> string
    1.80 +
    1.81 +  val ocamlN: string
    1.82 +  val ISABELLE_OCAMLC: string
    1.83 +  val evaluate_in_ocaml: Proof.context -> (string * string) list * string -> Path.T -> string
    1.84  
    1.85 -  val ghcN : string
    1.86 -  val ISABELLE_GHC : string
    1.87 -  val ghc_options : string Config.T
    1.88 -  val evaluate_in_ghc : Proof.context -> (string * string) list * string -> Path.T -> string
    1.89 +  val ghcN: string
    1.90 +  val ISABELLE_GHC: string
    1.91 +  val ghc_options: string Config.T
    1.92 +  val evaluate_in_ghc: Proof.context -> (string * string) list * string -> Path.T -> string
    1.93  
    1.94 -  val scalaN : string
    1.95 -  val ISABELLE_SCALA : string
    1.96 -  val evaluate_in_scala : Proof.context -> (string * string) list * string -> Path.T -> string
    1.97 +  val scalaN: string
    1.98 +  val ISABELLE_SCALA: string
    1.99 +  val evaluate_in_scala: Proof.context -> (string * string) list * string -> Path.T -> string
   1.100  end
   1.101  
   1.102 -structure Code_Test : CODE_TEST = struct
   1.103 +structure Code_Test: CODE_TEST =
   1.104 +struct
   1.105  
   1.106  (* convert a list of terms into nested tuples and back *)
   1.107 +
   1.108  fun mk_tuples [] = @{term "()"}
   1.109    | mk_tuples [t] = t
   1.110    | mk_tuples (t :: ts) = HOLogic.mk_prod (t, mk_tuples ts)
   1.111 @@ -67,42 +74,44 @@
   1.112  
   1.113  fun last_field sep str =
   1.114    let
   1.115 -    val n = size sep;
   1.116 -    val len = size str;
   1.117 +    val n = size sep
   1.118 +    val len = size str
   1.119      fun find i =
   1.120        if i < 0 then NONE
   1.121        else if String.substring (str, i, n) = sep then SOME i
   1.122 -      else find (i - 1);
   1.123 +      else find (i - 1)
   1.124    in
   1.125      (case find (len - n) of
   1.126        NONE => NONE
   1.127      | SOME i => SOME (String.substring (str, 0, i), String.extract (str, i + n, NONE)))
   1.128 -  end;
   1.129 +  end
   1.130  
   1.131  fun split_first_last start stop s =
   1.132 -  case first_field start s
   1.133 -   of NONE => NONE
   1.134 -    | SOME (initial, rest) =>
   1.135 -      case last_field stop rest
   1.136 -       of NONE => NONE
   1.137 -        | SOME (middle, tail) => SOME (initial, middle, tail);
   1.138 +  (case first_field start s of
   1.139 +    NONE => NONE
   1.140 +  | SOME (initial, rest) =>
   1.141 +      (case last_field stop rest of
   1.142 +        NONE => NONE
   1.143 +      | SOME (middle, tail) => SOME (initial, middle, tail)))
   1.144  
   1.145 -(* Data slot for drivers *)
   1.146 +
   1.147 +(* data slot for drivers *)
   1.148  
   1.149  structure Drivers = Theory_Data
   1.150  (
   1.151 -  type T = (string * ((Proof.context -> (string * string) list * string -> Path.T -> string) * string)) list;
   1.152 -  val empty = [];
   1.153 -  val extend = I;
   1.154 -  fun merge data : T = AList.merge (op =) (K true) data;
   1.155 +  type T =
   1.156 +    (string * ((Proof.context -> (string * string) list * string -> Path.T -> string) * string)) list
   1.157 +  val empty = []
   1.158 +  val extend = I
   1.159 +  fun merge data : T = AList.merge (op =) (K true) data
   1.160  )
   1.161  
   1.162 -val add_driver = Drivers.map o AList.update (op =);
   1.163 -val get_driver = AList.lookup (op =) o Drivers.get;
   1.164 +val add_driver = Drivers.map o AList.update (op =)
   1.165 +val get_driver = AList.lookup (op =) o Drivers.get
   1.166  
   1.167  (*
   1.168    Test drivers must produce output of the following format:
   1.169 -  
   1.170 +
   1.171    The start of the relevant data is marked with start_markerN,
   1.172    its end with end_markerN.
   1.173  
   1.174 @@ -112,7 +121,8 @@
   1.175    There must not be any additional whitespace in between.
   1.176  *)
   1.177  
   1.178 -(* Parsing of results *)
   1.179 +
   1.180 +(* parsing of results *)
   1.181  
   1.182  val successN = "True"
   1.183  val failureN = "False"
   1.184 @@ -121,7 +131,7 @@
   1.185  
   1.186  fun parse_line line =
   1.187    if String.isPrefix successN line then (true, NONE)
   1.188 -  else if String.isPrefix failureN line then (false, 
   1.189 +  else if String.isPrefix failureN line then (false,
   1.190      if size line > size failureN then
   1.191        String.extract (line, size failureN, NONE)
   1.192        |> YXML.parse_body
   1.193 @@ -132,20 +142,21 @@
   1.194    else raise Fail ("Cannot parse result of evaluation:\n" ^ line)
   1.195  
   1.196  fun parse_result target out =
   1.197 -  case split_first_last start_markerN end_markerN out
   1.198 -    of NONE => error ("Evaluation failed for " ^ target ^ "!\nBash output:\n" ^ out)
   1.199 -     | SOME (_, middle, _) => middle |> trim_line |> split_lines |> map parse_line
   1.200 +  (case split_first_last start_markerN end_markerN out of
   1.201 +    NONE => error ("Evaluation failed for " ^ target ^ "!\nBash output:\n" ^ out)
   1.202 +  | SOME (_, middle, _) => middle |> trim_line |> split_lines |> map parse_line)
   1.203  
   1.204 -(* Pretty printing of test results *)
   1.205 +
   1.206 +(* pretty printing of test results *)
   1.207  
   1.208  fun pretty_eval _ NONE _ = []
   1.209 -  | pretty_eval ctxt (SOME evals) ts = 
   1.210 -    [Pretty.fbrk,
   1.211 -     Pretty.big_list "Evaluated terms"
   1.212 -       (map (fn (t, eval) => Pretty.block 
   1.213 -         [Syntax.pretty_term ctxt t, Pretty.brk 1, Pretty.str "=", Pretty.brk 1,
   1.214 -          Syntax.pretty_term ctxt eval])
   1.215 -       (ts ~~ evals))]
   1.216 +  | pretty_eval ctxt (SOME evals) ts =
   1.217 +      [Pretty.fbrk,
   1.218 +       Pretty.big_list "Evaluated terms"
   1.219 +         (map (fn (t, eval) => Pretty.block
   1.220 +           [Syntax.pretty_term ctxt t, Pretty.brk 1, Pretty.str "=", Pretty.brk 1,
   1.221 +            Syntax.pretty_term ctxt eval])
   1.222 +         (ts ~~ evals))]
   1.223  
   1.224  fun pretty_failure ctxt target (((_, evals), query), eval_ts) =
   1.225    Pretty.block (Pretty.text ("Test in " ^ target ^ " failed for")
   1.226 @@ -155,60 +166,61 @@
   1.227  fun pretty_failures ctxt target failures =
   1.228    Pretty.blk (0, Pretty.fbreaks (map (pretty_failure ctxt target) failures))
   1.229  
   1.230 -(* Driver invocation *)
   1.231  
   1.232 -val overlord = Attrib.setup_config_bool @{binding "code_test_overlord"} (K false);
   1.233 +(* driver invocation *)
   1.234 +
   1.235 +val overlord = Attrib.setup_config_bool @{binding "code_test_overlord"} (K false)
   1.236  
   1.237  fun with_overlord_dir name f =
   1.238    let
   1.239 -    val path = Path.append (Path.explode "$ISABELLE_HOME_USER") (Path.basic (name ^ serial_string ()))
   1.240 -    val _ = Isabelle_System.mkdirs path;
   1.241 -  in
   1.242 -    Exn.release (Exn.capture f path)
   1.243 -  end;
   1.244 +    val path =
   1.245 +      Path.append (Path.explode "$ISABELLE_HOME_USER") (Path.basic (name ^ serial_string ()))
   1.246 +    val _ = Isabelle_System.mkdirs path
   1.247 +  in Exn.release (Exn.capture f path) end
   1.248  
   1.249  fun dynamic_value_strict ctxt t compiler =
   1.250    let
   1.251      val thy = Proof_Context.theory_of ctxt
   1.252 -    val (driver, target) = case get_driver thy compiler
   1.253 -     of NONE => error ("No driver for target " ^ compiler)
   1.254 -      | SOME f => f;
   1.255 +    val (driver, target) =
   1.256 +      (case get_driver thy compiler of
   1.257 +        NONE => error ("No driver for target " ^ compiler)
   1.258 +      | SOME f => f)
   1.259      val debug = Config.get (Proof_Context.init_global thy) overlord
   1.260      val with_dir = if debug then with_overlord_dir else Isabelle_System.with_tmp_dir
   1.261      fun evaluate f = with_dir "Code_Test" (driver ctxt f) |> parse_result compiler
   1.262      fun evaluator program _ vs_ty deps =
   1.263 -      Exn.interruptible_capture evaluate (Code_Target.computation_text ctxt target program deps true vs_ty);
   1.264 +      Exn.interruptible_capture evaluate
   1.265 +        (Code_Target.computation_text ctxt target program deps true vs_ty)
   1.266      fun postproc f = map (apsnd (map_option (map f)))
   1.267 -  in
   1.268 -    Exn.release (Code_Thingol.dynamic_value ctxt (Exn.map_res o postproc) evaluator t)
   1.269 -  end;
   1.270 +  in Exn.release (Code_Thingol.dynamic_value ctxt (Exn.map_res o postproc) evaluator t) end
   1.271  
   1.272 -(* Term preprocessing *)
   1.273 +
   1.274 +(* term preprocessing *)
   1.275  
   1.276  fun add_eval (Const (@{const_name Trueprop}, _) $ t) = add_eval t
   1.277    | add_eval (Const (@{const_name "HOL.eq"}, _) $ lhs $ rhs) = (fn acc =>
   1.278 -    acc
   1.279 -    |> add_eval rhs
   1.280 -    |> add_eval lhs
   1.281 -    |> cons rhs
   1.282 -    |> cons lhs)
   1.283 +      acc
   1.284 +      |> add_eval rhs
   1.285 +      |> add_eval lhs
   1.286 +      |> cons rhs
   1.287 +      |> cons lhs)
   1.288    | add_eval (Const (@{const_name "Not"}, _) $ t) = add_eval t
   1.289    | add_eval (Const (@{const_name "Orderings.ord_class.less_eq"}, _) $ lhs $ rhs) = (fn acc =>
   1.290 -    lhs :: rhs :: acc)
   1.291 +      lhs :: rhs :: acc)
   1.292    | add_eval (Const (@{const_name "Orderings.ord_class.less"}, _) $ lhs $ rhs) = (fn acc =>
   1.293 -    lhs :: rhs :: acc)
   1.294 +      lhs :: rhs :: acc)
   1.295    | add_eval _ = I
   1.296  
   1.297  fun mk_term_of [] = @{term "None :: (unit \<Rightarrow> yxml_of_term) option"}
   1.298    | mk_term_of ts =
   1.299 -  let
   1.300 -    val tuple = mk_tuples ts
   1.301 -    val T = fastype_of tuple
   1.302 -  in
   1.303 -    @{term "Some :: (unit \<Rightarrow> yxml_of_term) \<Rightarrow> (unit \<Rightarrow> yxml_of_term) option"} $
   1.304 -      (absdummy @{typ unit} (@{const yxml_string_of_term} $
   1.305 -        (Const (@{const_name Code_Evaluation.term_of}, T --> @{typ term}) $ tuple)))
   1.306 -  end
   1.307 +      let
   1.308 +        val tuple = mk_tuples ts
   1.309 +        val T = fastype_of tuple
   1.310 +      in
   1.311 +        @{term "Some :: (unit \<Rightarrow> yxml_of_term) \<Rightarrow> (unit \<Rightarrow> yxml_of_term) option"} $
   1.312 +          (absdummy @{typ unit} (@{const yxml_string_of_term} $
   1.313 +            (Const (@{const_name Code_Evaluation.term_of}, T --> @{typ term}) $ tuple)))
   1.314 +      end
   1.315  
   1.316  fun test_terms ctxt ts target =
   1.317    let
   1.318 @@ -216,24 +228,28 @@
   1.319  
   1.320      fun term_of t = Sign.of_sort thy (fastype_of t, @{sort term_of})
   1.321  
   1.322 -    fun ensure_bool t = case fastype_of t of @{typ bool} => ()
   1.323 -      | _ => error ("Test case not of type bool: " ^ Pretty.string_of (Syntax.pretty_term ctxt t))
   1.324 +    fun ensure_bool t =
   1.325 +      (case fastype_of t of
   1.326 +        @{typ bool} => ()
   1.327 +      | _ => error ("Test case not of type bool: " ^ Pretty.string_of (Syntax.pretty_term ctxt t)))
   1.328  
   1.329      val _ = map ensure_bool ts
   1.330  
   1.331      val evals = map (fn t => filter term_of (add_eval t [])) ts
   1.332      val eval = map mk_term_of evals
   1.333  
   1.334 -    val T = HOLogic.mk_prodT (@{typ bool}, Type (@{type_name option}, [@{typ unit} --> @{typ yxml_of_term}]))
   1.335 +    val T =
   1.336 +      HOLogic.mk_prodT (@{typ bool},
   1.337 +        Type (@{type_name option}, [@{typ unit} --> @{typ yxml_of_term}]))
   1.338      val t = HOLogic.mk_list T (map HOLogic.mk_prod (ts ~~ eval))
   1.339  
   1.340 -    val result = dynamic_value_strict ctxt t target;
   1.341 +    val result = dynamic_value_strict ctxt t target
   1.342  
   1.343      val failed =
   1.344        filter_out (fst o fst o fst) (result ~~ ts ~~ evals)
   1.345 -      handle ListPair.UnequalLengths => 
   1.346 +      handle ListPair.UnequalLengths =>
   1.347          error ("Evaluation failed!\nWrong number of test results: " ^ Int.toString (length result))
   1.348 -    val _ = case failed of [] => () 
   1.349 +    val _ = case failed of [] => ()
   1.350        | _ => error (Pretty.string_of (pretty_failures ctxt target failed))
   1.351    in
   1.352      ()
   1.353 @@ -243,8 +259,8 @@
   1.354  
   1.355  fun test_code_cmd raw_ts targets state =
   1.356    let
   1.357 -    val ctxt = Toplevel.context_of state;
   1.358 -    val ts = Syntax.read_terms ctxt raw_ts;
   1.359 +    val ctxt = Toplevel.context_of state
   1.360 +    val ts = Syntax.read_terms ctxt raw_ts
   1.361      val frees = fold Term.add_free_names ts []
   1.362      val _ = if frees = [] then () else
   1.363        error ("Terms contain free variables: " ^
   1.364 @@ -263,41 +279,41 @@
   1.365      val thy = Proof_Context.theory_of ctxt
   1.366  
   1.367      val T_t = fastype_of t
   1.368 -    val _ = if Sign.of_sort thy (T_t, @{sort term_of}) then () else error 
   1.369 -      ("Type " ^ Pretty.string_of (Syntax.pretty_typ ctxt T_t) ^ 
   1.370 +    val _ = if Sign.of_sort thy (T_t, @{sort term_of}) then () else error
   1.371 +      ("Type " ^ Pretty.string_of (Syntax.pretty_typ ctxt T_t) ^
   1.372         " of term not of sort " ^ Pretty.string_of (Syntax.pretty_sort ctxt @{sort term_of}))
   1.373  
   1.374      val T = HOLogic.mk_prodT (@{typ bool}, Type (@{type_name option}, [@{typ unit} --> @{typ yxml_of_term}]))
   1.375      val t' = HOLogic.mk_list T [HOLogic.mk_prod (@{term "False"}, mk_term_of [t])]
   1.376  
   1.377 -    val result = dynamic_value_strict ctxt t' target;
   1.378 -  in
   1.379 -    case result of [(_, SOME [t])] => t | _ => error "Evaluation failed"
   1.380 -  end
   1.381 +    val result = dynamic_value_strict ctxt t' target
   1.382 +  in (case result of [(_, SOME [t])] => t | _ => error "Evaluation failed") end
   1.383  
   1.384 -(* Generic driver *)
   1.385 +
   1.386 +(* generic driver *)
   1.387  
   1.388  fun gen_driver mk_driver env_var env_var_dest compilerN ctxt (code_files, value_name) =
   1.389    let
   1.390      val compiler = getenv env_var
   1.391 -    val _ = if compiler <> "" then () else error (Pretty.string_of (Pretty.para 
   1.392 +    val _ =
   1.393 +      if compiler <> "" then ()
   1.394 +      else error (Pretty.string_of (Pretty.para
   1.395           ("Environment variable " ^ env_var ^ " is not set. To test code generation with " ^
   1.396           compilerN ^ ", set this variable to your " ^ env_var_dest ^ " in the settings file.")))
   1.397  
   1.398      fun compile NONE = ()
   1.399        | compile (SOME cmd) =
   1.400 -        let
   1.401 -          val (out, ret) = Isabelle_System.bash_output cmd
   1.402 -        in
   1.403 -          if ret = 0 then () else error
   1.404 -            ("Compilation with " ^ compilerN ^ " failed:\n" ^ cmd ^ "\n" ^ out)
   1.405 -        end
   1.406 +          let
   1.407 +            val (out, ret) = Isabelle_System.bash_output cmd
   1.408 +          in
   1.409 +            if ret = 0 then () else error
   1.410 +              ("Compilation with " ^ compilerN ^ " failed:\n" ^ cmd ^ "\n" ^ out)
   1.411 +          end
   1.412  
   1.413 -    fun run (path : Path.T)= 
   1.414 +    fun run path =
   1.415        let
   1.416          val modules = map fst code_files
   1.417 -        val {files, compile_cmd, run_cmd, mk_code_file}
   1.418 -          =  mk_driver ctxt path modules value_name
   1.419 +        val {files, compile_cmd, run_cmd, mk_code_file} = mk_driver ctxt path modules value_name
   1.420  
   1.421          val _ = map (fn (name, code) => File.write (mk_code_file name) code) code_files
   1.422          val _ = map (fn (name, content) => File.write name content) files
   1.423 @@ -308,17 +324,14 @@
   1.424          val _ = if res = 0 then () else error
   1.425            ("Evaluation for " ^ compilerN ^ " terminated with error code " ^ Int.toString res ^
   1.426             "\nBash output:\n" ^ out)
   1.427 -      in
   1.428 -        out
   1.429 -      end
   1.430 -  in
   1.431 -    run
   1.432 -  end
   1.433 +      in out end
   1.434 +  in run end
   1.435  
   1.436 -(* Driver for PolyML *)
   1.437 +
   1.438 +(* driver for PolyML *)
   1.439  
   1.440  val ISABELLE_POLYML = "ISABELLE_POLYML"
   1.441 -val polymlN = "PolyML";
   1.442 +val polymlN = "PolyML"
   1.443  
   1.444  fun mk_driver_polyml _ path _ value_name =
   1.445    let
   1.446 @@ -327,10 +340,10 @@
   1.447  
   1.448      val code_path = Path.append path (Path.basic generatedN)
   1.449      val driver_path = Path.append path (Path.basic driverN)
   1.450 -    val driver = 
   1.451 +    val driver =
   1.452        "fun main prog_name = \n" ^
   1.453        "  let\n" ^
   1.454 -      "    fun format_term NONE = \"\"\n" ^ 
   1.455 +      "    fun format_term NONE = \"\"\n" ^
   1.456        "      | format_term (SOME t) = t ();\n" ^
   1.457        "    fun format (true, _) = \"" ^ successN ^ "\\n\"\n" ^
   1.458        "      | format (false, to) = \"" ^ failureN ^ "\" ^ format_term to ^ \"\\n\";\n" ^
   1.459 @@ -342,8 +355,8 @@
   1.460        "    ()\n" ^
   1.461        "  end;\n"
   1.462      val cmd =
   1.463 -      "echo \"use \\\"" ^ Path.implode code_path ^ "\\\"; use \\\"" ^ 
   1.464 -      Path.implode driver_path ^ "\\\"; main ();\" | " ^ 
   1.465 +      "echo \"use \\\"" ^ Path.implode code_path ^ "\\\"; use \\\"" ^
   1.466 +      Path.implode driver_path ^ "\\\"; main ();\" | " ^
   1.467        Path.implode (Path.variable ISABELLE_POLYML)
   1.468    in
   1.469      {files = [(driver_path, driver)], compile_cmd = NONE, run_cmd = cmd, mk_code_file = K code_path}
   1.470 @@ -352,7 +365,8 @@
   1.471  fun evaluate_in_polyml ctxt =
   1.472    gen_driver mk_driver_polyml ISABELLE_POLYML "PolyML executable" polymlN ctxt
   1.473  
   1.474 -(* Driver for mlton *)
   1.475 +
   1.476 +(* driver for mlton *)
   1.477  
   1.478  val mltonN = "MLton"
   1.479  val ISABELLE_MLTON = "ISABELLE_MLTON"
   1.480 @@ -367,8 +381,8 @@
   1.481      val code_path = Path.append path (Path.basic generatedN)
   1.482      val driver_path = Path.append path (Path.basic driverN)
   1.483      val ml_basis_path = Path.append path (Path.basic ml_basisN)
   1.484 -    val driver = 
   1.485 -      "fun format_term NONE = \"\"\n" ^ 
   1.486 +    val driver =
   1.487 +      "fun format_term NONE = \"\"\n" ^
   1.488        "  | format_term (SOME t) = t ();\n" ^
   1.489        "fun format (true, _) = \"" ^ successN ^ "\\n\"\n" ^
   1.490        "  | format (false, to) = \"" ^ failureN ^ "\" ^ format_term to ^ \"\\n\";\n" ^
   1.491 @@ -393,7 +407,8 @@
   1.492  fun evaluate_in_mlton ctxt =
   1.493    gen_driver mk_driver_mlton ISABELLE_MLTON "MLton executable" mltonN ctxt
   1.494  
   1.495 -(* Driver for SML/NJ *)
   1.496 +
   1.497 +(* driver for SML/NJ *)
   1.498  
   1.499  val smlnjN = "SMLNJ"
   1.500  val ISABELLE_SMLNJ = "ISABELLE_SMLNJ"
   1.501 @@ -405,11 +420,11 @@
   1.502  
   1.503      val code_path = Path.append path (Path.basic generatedN)
   1.504      val driver_path = Path.append path (Path.basic driverN)
   1.505 -    val driver = 
   1.506 +    val driver =
   1.507        "structure Test = struct\n" ^
   1.508        "fun main prog_name =\n" ^
   1.509        "  let\n" ^
   1.510 -      "    fun format_term NONE = \"\"\n" ^ 
   1.511 +      "    fun format_term NONE = \"\"\n" ^
   1.512        "      | format_term (SOME t) = t ();\n" ^
   1.513        "    fun format (true, _) = \"" ^ successN ^ "\\n\"\n" ^
   1.514        "      | format (false, to) = \"" ^ failureN ^ "\" ^ format_term to ^ \"\\n\";\n" ^
   1.515 @@ -432,7 +447,8 @@
   1.516  fun evaluate_in_smlnj ctxt =
   1.517    gen_driver mk_driver_smlnj ISABELLE_SMLNJ "SMLNJ executable" smlnjN ctxt
   1.518  
   1.519 -(* Driver for OCaml *)
   1.520 +
   1.521 +(* driver for OCaml *)
   1.522  
   1.523  val ocamlN = "OCaml"
   1.524  val ISABELLE_OCAMLC = "ISABELLE_OCAMLC"
   1.525 @@ -444,9 +460,9 @@
   1.526  
   1.527      val code_path = Path.append path (Path.basic generatedN)
   1.528      val driver_path = Path.append path (Path.basic driverN)
   1.529 -    val driver = 
   1.530 +    val driver =
   1.531        "let format_term = function\n" ^
   1.532 -      "  | None -> \"\"\n" ^ 
   1.533 +      "  | None -> \"\"\n" ^
   1.534        "  | Some t -> t ();;\n" ^
   1.535        "let format = function\n" ^
   1.536        "  | (true, _) -> \"" ^ successN ^ "\\n\"\n" ^
   1.537 @@ -473,7 +489,8 @@
   1.538  fun evaluate_in_ocaml ctxt =
   1.539    gen_driver mk_driver_ocaml ISABELLE_OCAMLC "ocamlc executable" ocamlN ctxt
   1.540  
   1.541 -(* Driver for GHC *)
   1.542 +
   1.543 +(* driver for GHC *)
   1.544  
   1.545  val ghcN = "GHC"
   1.546  val ISABELLE_GHC = "ISABELLE_GHC"
   1.547 @@ -486,12 +503,12 @@
   1.548  
   1.549      fun mk_code_file name = Path.append path (Path.basic (name ^ ".hs"))
   1.550      val driver_path = Path.append path (Path.basic driverN)
   1.551 -    val driver = 
   1.552 +    val driver =
   1.553        "module Main where {\n" ^
   1.554        String.concat (map (fn module => "import qualified " ^ module ^ ";\n") modules) ^
   1.555        "main = do {\n" ^
   1.556        "    let {\n" ^
   1.557 -      "      format_term Nothing = \"\";\n" ^ 
   1.558 +      "      format_term Nothing = \"\";\n" ^
   1.559        "      format_term (Just t) = t ();\n" ^
   1.560        "      format (True, _) = \"" ^ successN ^ "\\n\";\n" ^
   1.561        "      format (False, to) = \"" ^ failureN ^ "\" ++ format_term to ++ \"\\n\";\n" ^
   1.562 @@ -518,7 +535,8 @@
   1.563  fun evaluate_in_ghc ctxt =
   1.564    gen_driver mk_driver_ghc ISABELLE_GHC "GHC executable" ghcN ctxt
   1.565  
   1.566 -(* Driver for Scala *)
   1.567 +
   1.568 +(* driver for Scala *)
   1.569  
   1.570  val scalaN = "Scala"
   1.571  val ISABELLE_SCALA = "ISABELLE_SCALA"
   1.572 @@ -530,7 +548,7 @@
   1.573  
   1.574      val code_path = Path.append path (Path.basic (generatedN ^ ".scala"))
   1.575      val driver_path = Path.append path (Path.basic driverN)
   1.576 -    val driver = 
   1.577 +    val driver =
   1.578        "import " ^ generatedN ^ "._\n" ^
   1.579        "object Test {\n" ^
   1.580        "  def format_term(x : Option[Unit => String]) : String = x match {\n" ^
   1.581 @@ -567,7 +585,7 @@
   1.582  
   1.583  val test_codeP = Scan.repeat1 Parse.prop -- (@{keyword "in"} |-- Scan.repeat1 Parse.name)
   1.584  
   1.585 -val _ = 
   1.586 +val _ =
   1.587    Outer_Syntax.command @{command_keyword test_code}
   1.588      "compile test cases to target languages, execute them and report results"
   1.589        (test_codeP >> (fn (raw_ts, targets) => Toplevel.keep (test_code_cmd raw_ts targets)))
   1.590 @@ -580,7 +598,6 @@
   1.591     (ghcN, (evaluate_in_ghc, Code_Haskell.target)),
   1.592     (scalaN, (evaluate_in_scala, Code_Scala.target))]
   1.593    #> fold (fn target => Value_Command.add_evaluator (target, eval_term target))
   1.594 -    [polymlN, mltonN, smlnjN, ocamlN, ghcN, scalaN]);
   1.595 +    [polymlN, mltonN, smlnjN, ocamlN, ghcN, scalaN])
   1.596  
   1.597  end
   1.598 -