Theory EPAC_Checker_MLton

(*
  File:         PAC_Checker_MLton.thy
  Author:       Mathias Fleury, Daniela Kaufmann, JKU
  Maintainer:   Mathias Fleury, JKU
*)
theory EPAC_Checker_MLton
  imports EPAC_Checker_Synthesis
begin

export_code PAC_checker_l_impl PAC_update_impl PAC_empty_impl the_error is_cfailed is_cfound
  int_of_integer Del CL nat_of_integer String.implode remap_polys_l_impl
  fully_normalize_poly_impl union_vars_poly_impl empty_vars_impl
  full_checker_l_impl check_step_impl CSUCCESS
  Extension hashcode_literal' version
  in SML_imp module_name PAC_Checker
  file_prefix "checker"

text ‹Here is how to compile it:›
compile_generated_files _
  external_files
    ‹code/no_sharing/parser.sml›
    ‹code/no_sharing/pasteque.sml›
    ‹code/no_sharing/pasteque.mlb›
  where ‹fn dir =>
  let
    val exec = Generated_Files.execute (Path.append dir (Path.basic "code"));
     val _ = exec ‹Copy files›
      ("cp checker.ML " ^ ((File.bash_path \<^path>‹$ISAFOL›) ^ "/PAC_Checker2/code/no_sharing/checker.ML"));
     val _ = exec ‹Copy files›
      ("cp no_sharing/* .");
    val _ = exec ‹Copy files›
      ("ls .") |> @{print};
    val _ =
        exec ‹Compilation›
          (File.bash_path \<^path>‹$ISABELLE_MLTON› ^ " " ^
            "-const 'MLton.safe false' -verbose 1 -default-type int64 -output pasteque " ^
            "-codegen native -inline 700 -cc-opt -O3 pasteque.mlb"); 
    in () end›

end