1(*
2 * Copyright 2018, Data61
3 * Commonwealth Scientific and Industrial Research Organisation (CSIRO)
4 * ABN 41 687 119 230.
5 *
6 * This software may be distributed and modified according to the terms of
7 * the BSD 2-Clause license. Note that NO WARRANTY is provided.
8 * See "LICENSE_BSD2.txt" for details.
9 *
10 * @TAG(DATA61_BSD)
11 *)
12
13(* /*? macros.generated_file_notice() ?*/ *)
14
15open preamble basis /*- if me.type.control -*/ componentTheory /*- else -*/ connectorTheory /*- endif -*/
16
17val _ = new_theory "camkesEnd";
18
19val _ = translation_extends /*- if me.type.control -*/ "component" /*- else -*/ "connector" /*- endif -*/;
20
21val supervisor = process_topdecs `
22    fun camkes_entry u =
23        let
24            val dummy = Component.pre_init ();
25
26            val raw_result = Word8Array.array 1 (Word8.fromInt 0);
27            val dummy = #(pre_init_interface_sync) "" raw_result;
28            val result = Word8.toInt (Word8Array.sub raw_result 0) = 0;
29
30            val dummy = if result then (Component.post_init ()) else ();
31
32            val dummy = if result then (#(post_init_interface_sync) "" raw_result) else ();
33            val result = Word8.toInt (Word8Array.sub raw_result 0) = 0;
34
35            /*- if me.type.control -*/
36                val dummy = if result then (Component.run ()) else ();
37            /*- else -*/
38                val dummy = if result then (Connector.run ()) else ();
39            /*- endif -*/
40        in
41            ()
42        end
43`;
44
45val _ = append_prog supervisor;
46
47val _ = export_theory ();
48