src/HOL/Library/code_test.ML
changeset 64582 3d20ded18f14
parent 64581 ee4b9cea7fb5
child 64901 18e6f83e4a09
     1.1 --- a/src/HOL/Library/code_test.ML	Sat Dec 17 14:13:15 2016 +0100
     1.2 +++ b/src/HOL/Library/code_test.ML	Sat Dec 17 14:47:41 2016 +0100
     1.3 @@ -20,11 +20,11 @@
     1.4    val eval_term: string -> Proof.context -> term -> term
     1.5    val evaluate:
     1.6     (theory -> Path.T -> string list -> string ->
     1.7 -    {files: (Path.T * string) list,
     1.8 -     compile_cmd: string option,
     1.9 -     run_cmd: string,
    1.10 -     mk_code_file: string -> Path.T}) ->
    1.11 -   string -> string -> string -> theory -> (string * string) list * string -> Path.T -> string
    1.12 +     {files: (Path.T * string) list,
    1.13 +       compile_cmd: string option,
    1.14 +       run_cmd: string,
    1.15 +       mk_code_file: string -> Path.T}) -> (string * string) option -> string -> theory ->
    1.16 +     (string * string) list * string -> Path.T -> string
    1.17    val evaluate_in_polyml: Proof.context -> (string * string) list * string -> Path.T -> string
    1.18    val evaluate_in_mlton: Proof.context -> (string * string) list * string -> Path.T -> string
    1.19    val evaluate_in_smlnj: Proof.context -> (string * string) list * string -> Path.T -> string
    1.20 @@ -273,15 +273,19 @@
    1.21  
    1.22  (* generic driver *)
    1.23  
    1.24 -fun evaluate mk_driver env_var env_var_dest compilerN ctxt (code_files, value_name) =
    1.25 +fun evaluate mk_driver opt_env_var compilerN ctxt (code_files, value_name) =
    1.26    let
    1.27 -    val compiler = getenv env_var
    1.28      val _ =
    1.29 -      if compiler <> "" then ()
    1.30 -      else error (Pretty.string_of (Pretty.para
    1.31 -        ("Environment variable " ^ env_var ^ " is not set. To test code generation with " ^
    1.32 -          compilerN ^ ", set this variable to your " ^ env_var_dest ^
    1.33 -          " in the $ISABELLE_HOME_USER/etc/settings file.")))
    1.34 +      (case opt_env_var of
    1.35 +        NONE => ()
    1.36 +      | SOME (env_var, env_var_dest) =>
    1.37 +          (case getenv env_var of
    1.38 +            "" =>
    1.39 +              error (Pretty.string_of (Pretty.para
    1.40 +                ("Environment variable " ^ env_var ^ " is not set. To test code generation with " ^
    1.41 +                  compilerN ^ ", set this variable to your " ^ env_var_dest ^
    1.42 +                  " in the $ISABELLE_HOME_USER/etc/settings file.")))
    1.43 +          | _ => ()))
    1.44  
    1.45      fun compile NONE = ()
    1.46        | compile (SOME cmd) =
    1.47 @@ -313,7 +317,6 @@
    1.48  
    1.49  (* driver for PolyML *)
    1.50  
    1.51 -val ISABELLE_POLYML = "ISABELLE_POLYML"
    1.52  val polymlN = "PolyML"
    1.53  
    1.54  fun mk_driver_polyml _ path _ value_name =
    1.55 @@ -339,14 +342,12 @@
    1.56        "  end;\n"
    1.57      val cmd =
    1.58        "echo \"use \\\"" ^ Path.implode code_path ^ "\\\"; use \\\"" ^
    1.59 -      Path.implode driver_path ^ "\\\"; main ();\" | " ^
    1.60 -      Path.implode (Path.variable ISABELLE_POLYML)
    1.61 +      Path.implode driver_path ^ "\\\"; main ();\" | \"$ML_HOME/poly\""
    1.62    in
    1.63      {files = [(driver_path, driver)], compile_cmd = NONE, run_cmd = cmd, mk_code_file = K code_path}
    1.64    end
    1.65  
    1.66 -fun evaluate_in_polyml ctxt =
    1.67 -  evaluate mk_driver_polyml ISABELLE_POLYML "PolyML executable" polymlN ctxt
    1.68 +fun evaluate_in_polyml ctxt = evaluate mk_driver_polyml NONE polymlN ctxt
    1.69  
    1.70  
    1.71  (* driver for mlton *)
    1.72 @@ -388,7 +389,7 @@
    1.73    end
    1.74  
    1.75  fun evaluate_in_mlton ctxt =
    1.76 -  evaluate mk_driver_mlton ISABELLE_MLTON "MLton executable" mltonN ctxt
    1.77 +  evaluate mk_driver_mlton (SOME (ISABELLE_MLTON, "MLton executable")) mltonN ctxt
    1.78  
    1.79  
    1.80  (* driver for SML/NJ *)
    1.81 @@ -428,7 +429,7 @@
    1.82    end
    1.83  
    1.84  fun evaluate_in_smlnj ctxt =
    1.85 -  evaluate mk_driver_smlnj ISABELLE_SMLNJ "SMLNJ executable" smlnjN ctxt
    1.86 +  evaluate mk_driver_smlnj (SOME (ISABELLE_SMLNJ, "SMLNJ executable")) smlnjN ctxt
    1.87  
    1.88  
    1.89  (* driver for OCaml *)
    1.90 @@ -470,7 +471,7 @@
    1.91    end
    1.92  
    1.93  fun evaluate_in_ocaml ctxt =
    1.94 -  evaluate mk_driver_ocaml ISABELLE_OCAMLC "ocamlc executable" ocamlN ctxt
    1.95 +  evaluate mk_driver_ocaml (SOME (ISABELLE_OCAMLC, "ocamlc executable")) ocamlN ctxt
    1.96  
    1.97  
    1.98  (* driver for GHC *)
    1.99 @@ -516,13 +517,12 @@
   1.100    end
   1.101  
   1.102  fun evaluate_in_ghc ctxt =
   1.103 -  evaluate mk_driver_ghc ISABELLE_GHC "GHC executable" ghcN ctxt
   1.104 +  evaluate mk_driver_ghc (SOME (ISABELLE_GHC, "GHC executable")) ghcN ctxt
   1.105  
   1.106  
   1.107  (* driver for Scala *)
   1.108  
   1.109  val scalaN = "Scala"
   1.110 -val ISABELLE_SCALA = "ISABELLE_SCALA"
   1.111  
   1.112  fun mk_driver_scala _ path _ value_name =
   1.113    let
   1.114 @@ -551,20 +551,17 @@
   1.115        "}\n"
   1.116  
   1.117      val compile_cmd =
   1.118 -      Path.implode (Path.append (Path.variable ISABELLE_SCALA) (Path.basic "scalac")) ^
   1.119 -      " -d " ^ File.bash_path path ^ " -classpath " ^ File.bash_path path ^ " " ^
   1.120 +      "\"$SCALA_HOME/bin/scalac\" -d " ^ File.bash_path path ^
   1.121 +      " -classpath " ^ File.bash_path path ^ " " ^
   1.122        File.bash_path code_path ^ " " ^ File.bash_path driver_path
   1.123  
   1.124 -    val run_cmd =
   1.125 -      Path.implode (Path.append (Path.variable ISABELLE_SCALA) (Path.basic "scala")) ^
   1.126 -      " -cp " ^ File.bash_path path ^ " Test"
   1.127 +    val run_cmd = "\"$SCALA_HOME/bin/scala\" -cp " ^ File.bash_path path ^ " Test"
   1.128    in
   1.129      {files = [(driver_path, driver)],
   1.130       compile_cmd = SOME compile_cmd, run_cmd = run_cmd, mk_code_file = K code_path}
   1.131    end
   1.132  
   1.133 -fun evaluate_in_scala ctxt =
   1.134 -  evaluate mk_driver_scala ISABELLE_SCALA "Scala directory" scalaN ctxt
   1.135 +fun evaluate_in_scala ctxt = evaluate mk_driver_scala NONE scalaN ctxt
   1.136  
   1.137  
   1.138  (* command setup *)