camkes/templates/component.environment.end.cakeml

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

(* /*? macros.generated_file_notice() ?*/ *)

open preamble basis /*- if me.type.control -*/ componentTheory /*- else -*/ connectorTheory /*- endif -*/

val _ = new_theory "camkesEnd";

val _ = translation_extends /*- if me.type.control -*/ "component" /*- else -*/ "connector" /*- endif -*/;

val supervisor = process_topdecs `
    fun camkes_entry u =
        let
            val dummy = Component.pre_init ();

            val raw_result = Word8Array.array 1 (Word8.fromInt 0);
            val dummy = #(pre_init_interface_sync) "" raw_result;
            val result = Word8.toInt (Word8Array.sub raw_result 0) = 0;

            val dummy = if result then (Component.post_init ()) else ();

            val dummy = if result then (#(post_init_interface_sync) "" raw_result) else ();
            val result = Word8.toInt (Word8Array.sub raw_result 0) = 0;

            /*- if me.type.control -*/
                val dummy = if result then (Component.run ()) else ();
            /*- else -*/
                val dummy = if result then (Connector.run ()) else ();
            /*- endif -*/
        in
            ()
        end
`;

val _ = append_prog supervisor;

val _ = export_theory ();