src/HOL/Library/code_test.ML
changeset 64580 43ad19fbe9dc
parent 64579 38a1d8b41189
child 64581 ee4b9cea7fb5
     1.1 --- a/src/HOL/Library/code_test.ML	Sat Dec 17 14:04:05 2016 +0100
     1.2 +++ b/src/HOL/Library/code_test.ML	Sat Dec 17 14:09:39 2016 +0100
     1.3 @@ -18,7 +18,7 @@
     1.4    val end_markerN: string
     1.5    val test_terms: Proof.context -> term list -> string -> unit
     1.6    val test_targets: Proof.context -> term list -> string list -> unit
     1.7 -  val test_code_cmd: string list -> string list -> Toplevel.state -> unit
     1.8 +  val test_code_cmd: string list -> string list -> Proof.context -> unit
     1.9  
    1.10    val eval_term: string -> Proof.context -> term -> term
    1.11  
    1.12 @@ -258,9 +258,8 @@
    1.13  
    1.14  fun pretty_free ctxt = Syntax.pretty_term ctxt o Free
    1.15  
    1.16 -fun test_code_cmd raw_ts targets state =
    1.17 +fun test_code_cmd raw_ts targets ctxt =
    1.18    let
    1.19 -    val ctxt = Toplevel.context_of state
    1.20      val ts = Syntax.read_terms ctxt raw_ts
    1.21      val frees = fold Term.add_frees ts []
    1.22      val _ =
    1.23 @@ -589,21 +588,24 @@
    1.24  fun evaluate_in_scala ctxt =
    1.25    gen_driver mk_driver_scala ISABELLE_SCALA "Scala directory" scalaN ctxt
    1.26  
    1.27 -val test_codeP = Scan.repeat1 Parse.prop -- (@{keyword "in"} |-- Scan.repeat1 Parse.name)
    1.28 +
    1.29 +(* command setup *)
    1.30  
    1.31  val _ =
    1.32    Outer_Syntax.command @{command_keyword test_code}
    1.33      "compile test cases to target languages, execute them and report results"
    1.34 -      (test_codeP >> (fn (raw_ts, targets) => Toplevel.keep (test_code_cmd raw_ts targets)))
    1.35 +      (Scan.repeat1 Parse.prop -- (@{keyword "in"} |-- Scan.repeat1 Parse.name)
    1.36 +        >> (fn (ts, targets) => Toplevel.keep (test_code_cmd ts targets o Toplevel.context_of)))
    1.37  
    1.38 -val _ = Theory.setup (fold add_driver
    1.39 -  [(polymlN, (evaluate_in_polyml, Code_ML.target_SML)),
    1.40 -   (mltonN, (evaluate_in_mlton, Code_ML.target_SML)),
    1.41 -   (smlnjN, (evaluate_in_smlnj, Code_ML.target_SML)),
    1.42 -   (ocamlN, (evaluate_in_ocaml, Code_ML.target_OCaml)),
    1.43 -   (ghcN, (evaluate_in_ghc, Code_Haskell.target)),
    1.44 -   (scalaN, (evaluate_in_scala, Code_Scala.target))]
    1.45 +val _ =
    1.46 +  Theory.setup (fold add_driver
    1.47 +    [(polymlN, (evaluate_in_polyml, Code_ML.target_SML)),
    1.48 +     (mltonN, (evaluate_in_mlton, Code_ML.target_SML)),
    1.49 +     (smlnjN, (evaluate_in_smlnj, Code_ML.target_SML)),
    1.50 +     (ocamlN, (evaluate_in_ocaml, Code_ML.target_OCaml)),
    1.51 +     (ghcN, (evaluate_in_ghc, Code_Haskell.target)),
    1.52 +     (scalaN, (evaluate_in_scala, Code_Scala.target))]
    1.53    #> fold (fn target => Value_Command.add_evaluator (target, eval_term target))
    1.54 -    [polymlN, mltonN, smlnjN, ocamlN, ghcN, scalaN])
    1.55 +      [polymlN, mltonN, smlnjN, ocamlN, ghcN, scalaN])
    1.56  
    1.57  end