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 = \<^master_dir> + \<^path>‹mlunta›

val library_path = mlunta_dir + \<^path>‹src/isalib/library.sml›
val basics_path = mlunta_dir + \<^path>‹src/isalib/basics.sml›

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

end