(*
 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
 *
 * SPDX-License-Identifier: BSD-2-Clause
 *)

open preamble basis fromSexpTheory astToSexprLib @PARSE_CML_LIB_TRANSLATION_THEORY@Theory;

val _ = new_theory "build";
val _ = translation_extends "@PARSE_CML_LIB_TRANSLATION_THEORY@";
val st = ml_translatorLib.get_ml_prog_state();
val maincall =
  ``Dlet unknown_loc (Pcon NONE []) (App Opapp [Var (Short "@PARSE_CML_LIB_CAKEML_ENTRY@"); Con NONE []])``;
val prog = ``SNOC ^maincall ^(get_prog st)``
           |> EVAL |> concl |> rhs;
val _ = astToSexprLib.write_ast_to_file "@SEXP_FILE@" prog;
val _ = export_theory ();