Theory Munta_Certificate_Testing

section ‹Testing Infrastructure›

theory Munta_Certificate_Testing
  imports Main
begin

― ‹Produces commands for generating a certificate for a single benchmark with \mlunta, e.g.
▩‹mluntac-poly -certificate PM_all_5.cert -renaming PM_all_5.renaming -model PM_all_5.muntax›
checking it with \munta, and checking the result:
▩‹./check_benchmark.sh
  muntac -certificate PM_all_5.cert -renaming PM_all_5.renaming -model PM_all_5.muntax›
›
ML ‹
fun mk_cert mlunta_path name =
  let
    val benchmark = name ^ ".muntax"
    val gen_certificate = implode_space [
      mlunta_path,
      "-certificate", name ^ ".cert",
      "-renaming", name ^ ".renaming",
      "-model", benchmark
    ]
  in
    gen_certificate
  end

val it1 = mk_cert "mluntac-poly" "PM_all_5"

fun check_cert muntac_path name =
  let
    val benchmark = name ^ ".muntax"
  in
    implode_space [
      "./check_benchmark.sh",
      muntac_path,
      "-certificate", name ^ ".cert",
      "-renaming", name ^ ".renaming",
      "-model", benchmark
    ]
  end

val it2 = check_cert "muntac" "PM_all_5"

val mlunta_dir_proper = Path.append (Path.current |> File.absolute_path) (Path.explode "mlunta")

val mlunta_dir = Path.explode "mlunta" |> File.absolute_path

val library_path =
  Path.append mlunta_dir (Path.explode "src/isalib/library.sml") |> Path.implode
val basics_path =
  Path.append mlunta_dir (Path.explode "src/isalib/basics.sml") |> Path.implode

val mlunta_certificate_path = "mlunta/src/serialization/mlunta_certificate"
›

end