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