30 val evaluate_in_smlnj: Proof.context -> (string * string) list * string -> Path.T -> string |
30 val evaluate_in_smlnj: Proof.context -> (string * string) list * string -> Path.T -> string |
31 val evaluate_in_ocaml: Proof.context -> (string * string) list * string -> Path.T -> string |
31 val evaluate_in_ocaml: Proof.context -> (string * string) list * string -> Path.T -> string |
32 val ghc_options: string Config.T |
32 val ghc_options: string Config.T |
33 val evaluate_in_ghc: Proof.context -> (string * string) list * string -> Path.T -> string |
33 val evaluate_in_ghc: Proof.context -> (string * string) list * string -> Path.T -> string |
34 val evaluate_in_scala: Proof.context -> (string * string) list * string -> Path.T -> string |
34 val evaluate_in_scala: Proof.context -> (string * string) list * string -> Path.T -> string |
|
35 val target_Scala: string |
|
36 val target_Haskell: string |
35 end |
37 end |
36 |
38 |
37 structure Code_Test: CODE_TEST = |
39 structure Code_Test: CODE_TEST = |
38 struct |
40 struct |
39 |
41 |
574 Outer_Syntax.command @{command_keyword test_code} |
576 Outer_Syntax.command @{command_keyword test_code} |
575 "compile test cases to target languages, execute them and report results" |
577 "compile test cases to target languages, execute them and report results" |
576 (Scan.repeat1 Parse.prop -- (@{keyword "in"} |-- Scan.repeat1 Parse.name) |
578 (Scan.repeat1 Parse.prop -- (@{keyword "in"} |-- Scan.repeat1 Parse.name) |
577 >> (fn (ts, targets) => Toplevel.keep (test_code_cmd ts targets o Toplevel.context_of))) |
579 >> (fn (ts, targets) => Toplevel.keep (test_code_cmd ts targets o Toplevel.context_of))) |
578 |
580 |
|
581 val target_Scala = "Scala_eval" |
|
582 val target_Haskell = "Haskell_eval" |
|
583 |
|
584 val _ = Theory.setup |
|
585 (Code_Target.add_derived_target (target_Scala, [(Code_Scala.target, I)]) |
|
586 #> Code_Target.add_derived_target (target_Haskell, [(Code_Haskell.target, I)])) |
|
587 |
579 val _ = |
588 val _ = |
580 Theory.setup (fold add_driver |
589 Theory.setup (fold add_driver |
581 [(polymlN, (evaluate_in_polyml, Code_ML.target_SML)), |
590 [(polymlN, (evaluate_in_polyml, Code_ML.target_SML)), |
582 (mltonN, (evaluate_in_mlton, Code_ML.target_SML)), |
591 (mltonN, (evaluate_in_mlton, Code_ML.target_SML)), |
583 (smlnjN, (evaluate_in_smlnj, Code_ML.target_SML)), |
592 (smlnjN, (evaluate_in_smlnj, Code_ML.target_SML)), |
584 (ocamlN, (evaluate_in_ocaml, Code_ML.target_OCaml)), |
593 (ocamlN, (evaluate_in_ocaml, Code_ML.target_OCaml)), |
585 (ghcN, (evaluate_in_ghc, Code_Haskell.target)), |
594 (ghcN, (evaluate_in_ghc, target_Haskell)), |
586 (scalaN, (evaluate_in_scala, Code_Scala.target))] |
595 (scalaN, (evaluate_in_scala, target_Scala))] |
587 #> fold (fn target => Value_Command.add_evaluator (target, eval_term target)) |
596 #> fold (fn target => Value_Command.add_evaluator (target, eval_term target)) |
588 [polymlN, mltonN, smlnjN, ocamlN, ghcN, scalaN]) |
597 [polymlN, mltonN, smlnjN, ocamlN, ghcN, scalaN]) |
589 |
598 |
590 end |
599 end |