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