1(*
2 * Copyright 2020, Data61, CSIRO (ABN 41 687 119 230)
3 *
4 * SPDX-License-Identifier: GPL-2.0-only
5 *)
6chapter \<open>\label{s:eventbase}Example -- Events\<close>
7(*<*)
8(* THIS FILE IS AUTOMATICALLY GENERATED. YOUR EDITS WILL BE OVERWRITTEN. *)
9theory GenEventBase
10imports "Types" "Abbreviations" "Connector"
11begin
12(*>*)
13
14text \<open>
15  This section provides an example following on from \autoref{h:procbase} that
16  gives an example of the corresponding definitions that are generated for a
17  system involving \camkes events. A system defined by the following
18  specification will be used throughout:
19
20  \camkeslisting{event.camkes}
21\<close>
22
23subsection \<open>\label{ssec:eventbase}Generated Base Theory\<close>
24
25subsubsection \<open>\label{sssec:eventbasetypes}Types\<close>
26text \<open>
27  The data types generated for a system involving events are similar to those
28  for a system involving procedures, however an additional instance is
29  derived for every
30  connection in the system that carries event messages.
31  This generated instance models the state of the event;
32  that is, whether it is pending or not.
33\<close>
34
35datatype channel
36  = simpleEvent1
37
38datatype inst
39  = sink
40  | source
41  | simpleEvent1\<^sub>e
42
43datatype Collector_channel
44  = Collector_ev
45
46datatype Emitter_channel
47  = Emitter_ev
48
49subsubsection \<open>\label{sssec:eventbaseprim}Interface Primitives\<close>
50text \<open>
51  For each component type with a @{term consumes} interface, two primitives are
52  generated for each interface. These correspond to the wait and poll functions
53  in generated glue code. As for procedures, @{term embed} functions must be
54  supplied by the user to save the result of the operation into the component's
55  local state.
56
57  Event callbacks are not currently represented. These can be represented by
58  hand in the intermediate user theory. We plan to extend the generator in
59  future to wrap this functionality in a primitive for the user.
60\<close>
61
62definition
63  Poll_Collector_ev :: "(Collector_channel \<Rightarrow> channel) \<Rightarrow>
64    ('cs local_state \<Rightarrow> bool \<Rightarrow> 'cs local_state) \<Rightarrow> (channel, 'cs) comp"
65where
66  "Poll_Collector_ev ch embed_data \<equiv> EventPoll (ch Collector_ev) embed_data"
67
68definition
69  Wait_Collector_ev :: "(Collector_channel \<Rightarrow> channel) \<Rightarrow>
70    ('cs local_state \<Rightarrow> bool \<Rightarrow> 'cs local_state) \<Rightarrow> (channel, 'cs) comp"
71where
72  "Wait_Collector_ev ch embed_data \<equiv> EventWait (ch Collector_ev) embed_data"
73
74text \<open>
75  For each component type with an @{term emits} interface, a single primitive is
76  generated to correpond to the emit function in the glue code. The emit
77  definition needs no embedding or projection functions because it is
78  state-independent.
79\<close>
80
81definition
82  Emit_Emitter_ev :: "(Emitter_channel \<Rightarrow> channel) \<Rightarrow> (channel, 'cs) comp"
83where
84  "Emit_Emitter_ev ch \<equiv> EventEmit (ch Emitter_ev)"
85
86subsubsection \<open>\label{sssec:eventbaseinst}Instantiations of Primitives\<close>
87text \<open>
88  As for procedure interfaces, the event primitives are specialised for each
89  interface in the system by partially applying them with a function mapping
90  the interface to the relevant -- in this case the only -- system connection.
91\<close>
92
93definition
94  Poll_sink_ev :: "('cs local_state \<Rightarrow> bool \<Rightarrow> 'cs local_state) \<Rightarrow>
95    (channel, 'cs) comp"
96where
97  "Poll_sink_ev \<equiv>
98    Poll_Collector_ev (\<lambda>c. case c of Collector_ev \<Rightarrow> simpleEvent1)"
99
100definition
101  Wait_sink_ev :: "('cs local_state \<Rightarrow> bool \<Rightarrow> 'cs local_state) \<Rightarrow>
102    (channel, 'cs) comp"
103where
104  "Wait_sink_ev \<equiv>
105    Wait_Collector_ev (\<lambda>c. case c of Collector_ev \<Rightarrow> simpleEvent1)"
106
107definition
108  Emit_source_ev :: "(channel, 'cs) comp"
109where
110  "Emit_source_ev \<equiv>
111    Emit_Emitter_ev (\<lambda>c. case c of Emitter_ev \<Rightarrow> simpleEvent1)"
112
113(*<*)
114end
115(*>*)
116