eval_cake_compile_x64Lib.sml

(*
  Functions for in-logic evaluation of the CakeML compiler for x64.
*)
structure eval_cake_compile_x64Lib =
struct

local

  open eval_cake_compileLib;

  val x64_arch_thms =
    { default_config_def  = x64_configTheory.x64_backend_config_def
    , default_config_simp = backend_x64_cvTheory.set_asm_conf_x64_backend_config
    , to_livesets_def     = backend_x64Theory.to_livesets_x64_def
    , compile_cake_def    = backend_x64Theory.compile_cake_x64_def
    , compile_cake_imp    = backend_x64Theory.compile_cake_x64_thm
    , cv_export_def       = backend_x64_cvTheory.cv_x64_export_def } : arch_thms;

in

  val eval_cake_compile_x64 = eval_cake_compile x64_arch_thms;
  val eval_cake_compile_x64_with_conf = eval_cake_compile_with_conf x64_arch_thms;
  val eval_cake_compile_x64_general = eval_cake_compile_general x64_arch_thms;

end

end