1(*
2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3 *
4 * SPDX-License-Identifier: BSD-2-Clause
5 *)
6
7open preamble basis fromSexpTheory astToSexprLib @PARSE_CML_LIB_TRANSLATION_THEORY@Theory;
8
9val _ = new_theory "build";
10val _ = translation_extends "@PARSE_CML_LIB_TRANSLATION_THEORY@";
11val st = ml_translatorLib.get_ml_prog_state();
12val maincall =
13  ``Dlet unknown_loc (Pcon NONE []) (App Opapp [Var (Short "@PARSE_CML_LIB_CAKEML_ENTRY@"); Con NONE []])``;
14val prog = ``SNOC ^maincall ^(get_prog st)``
15           |> EVAL |> concl |> rhs;
16val _ = astToSexprLib.write_ast_to_file "@SEXP_FILE@" prog;
17val _ = export_theory ();
18