| (* |
| * 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 (); |
