1/*#
2 *# Copyright 2017, 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
15/*? macros.check_isabelle_outfile(
16        '%s_Cimp_Base' % options.verification_base_name, outfile_name) ?*/
17
18theory "/*? options.verification_base_name ?*/_Cimp_Base" imports
19  "CamkesGlueSpec.Types"
20  "CamkesGlueSpec.Abbreviations"
21  "CamkesGlueSpec.Connector"
22begin
23
24/*- macro show_native_type(type) --*/
25    /*-- if type in ['int', 'int8_t', 'int16_t', 'int32_t', 'int64_t'] --*/
26        int
27    /*-- elif type in ['unsigned int', 'uint8_t', 'uint16_t', 'uint32_t', 'uint64_t', 'uintptr_t'] --*/
28        nat
29    /*-- elif type in ['char', 'character'] --*/
30        char
31    /*-- elif type == 'bool' --*/
32        bool
33    /*-- elif type == 'string' --*/
34        string
35    /*-- else --*/
36        /*? raise(TemplateError('unsupported native type: %s' % type)) ?*/
37    /*-- endif --*/
38/*-- endmacro -*/
39
40/*- macro show_wrapped_type(type) --*/
41    /*-- if type in ['int', 'int8_t', 'int16_t', 'int32_t', 'int64_t'] --*/
42        Integer
43    /*-- elif type in ['unsigned int', 'uint8_t', 'uint16_t', 'uint32_t', 'uint64_t', 'uintptr_t'] --*/
44        Number
45    /*-- elif type in ['char', 'character'] --*/
46        Char
47    /*-- elif type == 'bool' --*/
48        Boolean
49    /*-- elif type == 'string' --*/
50        String
51    /*-- else --*/
52        /*? raise(TemplateError('unsupported wrapped type: %s' % type)) ?*/
53    /*-- endif --*/
54/*-- endmacro -*/
55
56/*- set instances = composition.instances -*/
57/*- set connections = composition.connections -*/
58/*- set components = set(map(lambda('x: x.type'), instances)) -*/
59
60(** TPP: condense = True *)
61(* Connections *)
62datatype channel
63/*- for c in connections -*/
64  /*- if loop.first --*/
65    =
66  /*-- else --*/
67    |
68  /*-- endif -*/ /*? c.name ?*/
69/*- endfor -*/
70(** TPP: condense = False *)
71
72(** TPP: condense = True *)
73(* Component instances *)
74datatype inst
75/*- for i in instances -*/
76  /*- if loop.first --*/
77    =
78  /*-- else --*/
79    |
80  /*-- endif -*/ /*? i.name ?*/
81/*- endfor -*/
82/*- for c in connections -*/
83  /*- if c.type.from_type == 'Event' -*/
84  | /*? c.name ?*/\<^sub>e
85  /*- elif c.type.from_type == 'Dataport' -*/
86  | /*? c.name ?*/\<^sub>d
87  /*- endif -*/
88/*- endfor -*/
89(** TPP: condense = False *)
90
91/*- for c in components -*/
92
93(** TPP: condense = True *)
94(* /*? c.name ?*/'s interfaces *)
95datatype /*? c.name ?*/_channel
96/*- for i in c.uses + c.provides + c.emits + c.consumes + c.dataports -*/
97  /*- if loop.first --*/
98    =
99  /*-- else --*/
100    |
101  /*-- endif -*/ /*? c.name ?*/_/*? i.name ?*/
102/*- endfor -*/
103(** TPP: condense = False *)
104
105    /*# Glue code for each outgoing procedural interface. #*/
106    /*- for u in c.uses -*/
107        /*- for i, m in enumerate(u.type.methods) -*/
108(** TPP: condense = True *)
109definition
110  /*- set type_sig = ['(%s_channel \\<Rightarrow> channel) \\<Rightarrow>' % c.name] -*/
111  /*- for p in filter(lambda('x: x.direction in [\'in\', \'inout\']'), m.parameters) -*/
112    /*- do type_sig.append('(\'cs local_state \\<Rightarrow> %s) \\<Rightarrow>' % show_native_type(p.type)) -*/
113  /*- endfor -*/
114  /*- if m.return_type is not none or len(list(filter(lambda('x: x.direction in [\'out\', \'inout\']'), m.parameters))) > 0 -*/
115    /*- do type_sig.append('(\'cs local_state') -*/
116  /*- endif -*/
117  /*- if m.return_type is not none -*/
118    /*- do type_sig.append('\\<Rightarrow> %s' % show_native_type(m.return_type)) -*/
119  /*- endif -*/
120  /*- for p in filter(lambda('x: x.direction in [\'out\', \'inout\']'), m.parameters) -*/
121    /*- do type_sig.append('\\<Rightarrow> %s' % show_native_type(p.type)) -*/
122  /*- endfor -*/
123  /*- if m.return_type is not none or len(list(filter(lambda('x: x.direction in [\'out\', \'inout\']'), m.parameters))) > 0 -*/
124      /*# We had to unmarshal at least one parameter. #*/
125      /*- do type_sig.append('\\<Rightarrow> \'cs local_state) \\<Rightarrow>') -*/
126  /*- endif -*/
127  /*- do type_sig.append('(channel, \'cs) comp') -*/
128  Call_/*? c.name ?*/_/*? u.name ?*/_/*? m.name ?*/ :: "/*? ' '.join(type_sig) ?*/"
129where
130  /*- set ch = isabelle_symbol('ch') -*/
131  /*- set params = [ch] -*/
132  /*- for p in filter(lambda('x: x.direction in [\'in\', \'inout\']'), m.parameters) -*/
133    /*- do params.append('%s\\<^sub>P' % p.name) -*/
134  /*- endfor -*/
135  /*- if m.return_type is not none or len(list(filter(lambda('x: x.direction in [\'out\', \'inout\']'), m.parameters))) > 0 -*/
136    /*- do params.append('embed_ret') -*/
137  /*- endif -*/
138  "Call_/*? c.name ?*/_/*? u.name ?*/_/*? m.name ?*/ /*? ' '.join(params) ?*/
139  /*-- set s = isabelle_symbol('s') --*/
140  \<equiv> Request (\<lambda>/*? s ?*/. {\<lparr>q_channel = /*? ch ?*/ /*? c.name ?*/_/*? u.name ?*/, q_data = Call /*? i ?*/ (
141  /*- for p in filter(lambda('x: x.direction in [\'in\', \'inout\']'), m.parameters) -*/
142      /*? show_wrapped_type(p.type) ?*/ (/*? p.name ?*/\<^sub>P /*? s ?*/) #
143  /*- endfor -*/
144  [])\<rparr>}) discard ;;
145  /*- set q = isabelle_symbol() -*/
146  /*- set s = isabelle_symbol() -*/
147  /*- set xs = isabelle_symbol() -*/
148  Response (\<lambda>/*? q ?*/ /*? s ?*/. case q_data /*? q ?*/ of Return /*? xs ?*/ \<Rightarrow>
149  /*- if m.return_type is not none or len(list(filter(lambda('x: x.direction in [\'out\', \'inout\']'), m.parameters))) > 0 -*/
150      {(embed_ret /*? s ?*/
151      /*- if m.return_type is not none -*/
152          /*- set v = isabelle_symbol() -*/
153          (case hd /*? xs ?*/ of /*? show_wrapped_type(m.return_type) ?*/ /*? v ?*/ \<Rightarrow> /*? v ?*/)
154      /*- endif -*/
155      /*- for i, p in enumerate(filter(lambda('x: x.direction in [\'out\', \'inout\']'), m.parameters)) -*/
156          /*- set v = isabelle_symbol() -*/
157          (case /*? xs ?*/ ! /*? i + (1 if m.return_type is not none else 0) ?*/ of /*? show_wrapped_type(p.type) ?*/ /*? v ?*/ \<Rightarrow> /*? v ?*/)
158      /*- endfor -*/
159  /*- else -*/
160      {(/*? s ?*/
161  /*- endif -*/
162  , \<lparr>a_channel = /*? ch ?*/ /*? c.name ?*/_/*? u.name ?*/, a_data = Void\<rparr>)} | _ \<Rightarrow> {})"
163(** TPP: condense = False *)
164        /*- endfor -*/
165    /*- endfor -*/
166
167    /*# Glue code for each incoming procedural interface. #*/
168    /*- for u in c.provides -*/
169(** TPP: condense = True *)
170definition
171  /*- set type_sig = ['(%s_channel \\<Rightarrow> channel) \\<Rightarrow>' % c.name] -*/
172  /*- for m in u.type.methods -*/
173    /*- if len(list(filter(lambda('x: x.direction in [\'in\', \'inout\']'), m.parameters))) > 0 -*/
174      /*- do type_sig.append('(\'cs local_state \\<Rightarrow>') -*/
175      /*- for p in filter(lambda('x: x.direction in [\'in\', \'inout\']'), m.parameters) -*/
176        /*- do type_sig.append('%s \\<Rightarrow>' % show_native_type(p.type)) -*/
177      /*- endfor -*/
178      /*- do type_sig.append('\'cs local_state) \\<Rightarrow>') -*/
179    /*- endif -*/
180    /*- do type_sig.append('(channel, \'cs) comp \\<Rightarrow>') -*/
181    /*- if m.return_type is not none -*/
182      /*- do type_sig.append('(\'cs local_state \\<Rightarrow> %s) \\<Rightarrow>' % show_native_type(m.return_type)) -*/
183    /*- endif -*/
184    /*- for p in filter(lambda('x: x.direction in [\'out\', \'inout\']'), m.parameters) -*/
185      /*- do type_sig.append('(\'cs local_state \\<Rightarrow> %s) \\<Rightarrow>' % show_native_type(p.type)) -*/
186    /*- endfor -*/
187  /*- endfor -*/
188  /*- do type_sig.append('(channel, \'cs) comp') -*/
189  Recv_/*? c.name ?*/_/*? u.name ?*/ :: "/*? ' '.join(type_sig) ?*/"
190where
191  /*- set ch = isabelle_symbol('ch') -*/
192  /*- set params = [ch] -*/
193  /*- for m in u.type.methods -*/
194    /*- if len(list(filter(lambda('x: x.direction in [\'in\', \'inout\']'), m.parameters))) > 0 -*/
195      /*- do params.append('%s\\<^sub>E' % m.name) -*/
196    /*- endif -*/
197    /*- do params.append('%s_%s_%s' % (c.name, u.name, m.name)) -*/
198    /*- if m.return_type is not none -*/
199      /*- do params.append('%s_return\\<^sub>P' % m.name) -*/
200    /*- endif -*/
201    /*- for p in filter(lambda('x: x.direction in [\'out\', \'inout\']'), m.parameters) -*/
202      /*- do params.append('%s_%s\\<^sub>P' % (m.name, p.name)) -*/
203    /*- endfor -*/
204  /*- endfor -*/
205  "Recv_/*? c.name ?*/_/*? u.name ?*/ /*? ' '.join(params) ?*/
206  \<equiv>
207  /*- for i, m in enumerate(u.type.methods) -*/
208      /*- if not loop.first -*/
209          \<squnion>
210      /*- endif -*/
211      /*- set q = isabelle_symbol() -*/
212      /*- set s = isabelle_symbol() -*/
213      /*- set n = isabelle_symbol() -*/
214      /*- set xs = isabelle_symbol() -*/
215      (Response (\<lambda>/*? q ?*/ /*? s ?*/. case q_data /*? q ?*/ of Call /*? n ?*/ /*? xs ?*/ \<Rightarrow> (if /*? n ?*/ = /*? i ?*/ then {(
216      /*- if len(list(filter(lambda('x: x.direction in [\'in\', \'inout\']'), m.parameters))) > 0 -*/
217          /*? m.name ?*/\<^sub>E /*? s ?*/
218          /*- for k, p in enumerate(filter(lambda('x: x.direction in [\'in\', \'inout\']'), m.parameters)) -*/
219              /*- set v = isabelle_symbol() -*/
220              (case /*? xs ?*/ ! /*? k ?*/ of /*? show_wrapped_type(p.type) ?*/ /*? v ?*/ \<Rightarrow> /*? v ?*/)
221          /*- endfor -*/
222      /*- else -*/
223          /*? s ?*/
224      /*- endif -*/
225      , \<lparr>a_channel = /*? ch ?*/ /*? c.name ?*/_/*? u.name ?*/, a_data = Void\<rparr>)} else {}) | _ \<Rightarrow> {}) ;;
226      /*? c.name ?*/_/*? u.name ?*/_/*? m.name ?*/ ;;
227      /*- set s = isabelle_symbol() -*/
228      Request (\<lambda>/*? s ?*/. {\<lparr>q_channel = /*? ch ?*/ /*? c.name ?*/_/*? u.name ?*/, q_data = Return (
229      /*- if m.return_type is not none -*/
230          /*? show_wrapped_type(m.return_type) ?*/ (/*? m.name ?*/_return\<^sub>P /*? s ?*/) #
231      /*- endif -*/
232      /*- for p in filter(lambda('x: x.direction in [\'out\', \'inout\']'), m.parameters) -*/
233          /*? show_wrapped_type(p.type) ?*/ (/*? m.name ?*/_/*? p.name ?*/\<^sub>P /*? s ?*/) #
234      /*- endfor -*/
235      [])\<rparr>}) discard)
236  /*- endfor -*/
237  "
238(** TPP: condense = False *)
239    /*- endfor -*/
240
241    /*# Glue code for each outgoing event interface. #*/
242    /*- for u in c.emits -*/
243(** TPP: condense = True *)
244definition
245  Emit_/*? c.name ?*/_/*? u.name ?*/ :: "(/*? c.name ?*/_channel \<Rightarrow> channel) \<Rightarrow> (channel, 'cs) comp"
246where
247  /*- set ch = isabelle_symbol('ch') -*/
248  "Emit_/*? c.name ?*/_/*? u.name ?*/ /*? ch ?*/ \<equiv> EventEmit (/*? ch ?*/ /*? c.name ?*/_/*? u.name ?*/)"
249(** TPP: condense = False *)
250    /*- endfor -*/
251
252    /*# Glue code for each incoming event interface. #*/
253    /*- for u in c.consumes -*/
254(** TPP: condense = True *)
255definition
256  Poll_/*? c.name ?*/_/*? u.name ?*/ :: "(/*? c.name ?*/_channel \<Rightarrow> channel) \<Rightarrow> ('cs local_state \<Rightarrow> bool \<Rightarrow> 'cs local_state) \<Rightarrow> (channel, 'cs) comp"
257where
258  /*- set ch = isabelle_symbol('ch') -*/
259  /*- set embed = isabelle_symbol('embed') -*/
260  "Poll_/*? c.name ?*/_/*? u.name ?*/ /*? ch ?*/ /*? embed ?*/ \<equiv> EventPoll (/*? ch ?*/ /*? c.name ?*/_/*? u.name ?*/) /*? embed ?*/"
261(** TPP: condense = False *)
262
263(** TPP: condense = True *)
264definition
265  Wait_/*? c.name ?*/_/*? u.name ?*/ :: "(/*? c.name ?*/_channel \<Rightarrow> channel) \<Rightarrow> ('cs local_state \<Rightarrow> bool \<Rightarrow> 'cs local_state) \<Rightarrow> (channel, 'cs) comp"
266where
267  /*- set embed = isabelle_symbol('embed') -*/
268  "Wait_/*? c.name ?*/_/*? u.name ?*/ /*? ch ?*/ /*? embed ?*/ \<equiv> EventWait (/*? ch ?*/ /*? c.name ?*/_/*? u.name ?*/) /*? embed ?*/"
269(** TPP: condense = False *)
270    /*- endfor -*/
271
272    /*# Glue code for dataport interfaces. #*/
273    /*- for u in c.dataports -*/
274(** TPP: condense = True *)
275definition
276  Read_/*? c.name ?*/_/*? u.name ?*/ :: "(/*? c.name ?*/_channel \<Rightarrow> channel) \<Rightarrow> ('cs local_state \<Rightarrow> nat) \<Rightarrow> ('cs local_state \<Rightarrow> variable \<Rightarrow> 'cs local_state) \<Rightarrow> (channel, 'cs) comp"
277where
278  /*- set ch = isabelle_symbol('ch') -*/
279  /*- set addr = isabelle_symbol('addr') -*/
280  /*- set embed = isabelle_symbol('embed') -*/
281  "Read_/*? c.name ?*/_/*? u.name ?*/ /*? ch ?*/ /*? addr ?*/ /*? embed ?*/ \<equiv> MemoryRead (/*? ch ?*/ /*? c.name ?*/_/*? u.name ?*/) /*? addr ?*/ /*? embed ?*/"
282(** TPP: condense = False *)
283
284(** TPP: condense = True *)
285definition
286  Write_/*? c.name ?*/_/*? u.name ?*/ :: "(/*? c.name ?*/_channel \<Rightarrow> channel) \<Rightarrow> ('cs local_state \<Rightarrow> nat) \<Rightarrow> ('cs local_state \<Rightarrow> variable) \<Rightarrow> (channel, 'cs) comp"
287where
288  /*- set ch = isabelle_symbol('ch') -*/
289  /*- set addr = isabelle_symbol('addr') -*/
290  /*- set proj = isabelle_symbol('proj') -*/
291  "Write_/*? c.name ?*/_/*? u.name ?*/ /*? ch ?*/ /*? addr ?*/ /*? proj ?*/ \<equiv> MemoryWrite (/*? ch ?*/ /*? c.name ?*/_/*? u.name ?*/) /*? addr ?*/ /*? proj ?*/"
292(** TPP: condense = False *)
293    /*- endfor -*/
294
295/*- endfor -*/
296
297(* Component instantiations *)
298/*- for i in instances -*/
299    /*- set c = i.type -*/
300
301    /*- for u in c.uses -*/
302        /*- for m in u.type.methods -*/
303(** TPP: condense = True *)
304definition
305  /*- set type_sig = [] -*/
306  /*- for p in filter(lambda('x: x.direction in [\'in\', \'inout\']'), m.parameters) -*/
307    /*- do type_sig.append('(\'cs local_state \\<Rightarrow> %s) \\<Rightarrow>' % show_native_type(p.type)) -*/
308  /*- endfor -*/
309  /*- if m.return_type is not none or len(list(filter(lambda('x: x.direction in [\'out\', \'inout\']'), m.parameters))) > 0 -*/
310    /*- do type_sig.append('(\'cs local_state') -*/
311  /*- endif -*/
312  /*- if m.return_type is not none -*/
313    /*- do type_sig.append('\\<Rightarrow> %s' % show_native_type(m.return_type)) -*/
314  /*- endif -*/
315  /*- for p in filter(lambda('x: x.direction in [\'out\', \'inout\']'), m.parameters) -*/
316    /*- do type_sig.append('\\<Rightarrow> %s' % show_native_type(p.type)) -*/
317  /*- endfor -*/
318  /*- if m.return_type is not none or len(list(filter(lambda('x: x.direction in [\'out\', \'inout\']'), m.parameters))) > 0 -*/
319    /*# We had to unmarshal at least one parameter. #*/
320    /*- do type_sig.append('\\<Rightarrow> \'cs local_state) \\<Rightarrow>') -*/
321  /*- endif -*/
322  /*- do type_sig.append('(channel, \'cs) comp') -*/
323  Call_/*? i.name ?*/_/*? u.name ?*/_/*? m.name ?*/ :: "/*? ' '.join(type_sig) ?*/"
324where
325  "Call_/*? i.name ?*/_/*? u.name ?*/_/*? m.name ?*/ \<equiv>
326      /*- set l = isabelle_symbol() -*/
327      Call_/*? c.name ?*/_/*? u.name ?*/_/*? m.name ?*/ (\<lambda>/*? l ?*/. case /*? l ?*/ of
328      /*- set j = joiner('|') -*/
329      /*- for conn in connections -*/
330          /*- set idx = eval('[ idx for idx in range(len(conn.from_ends)) if i.name == conn.from_ends[idx].instance.name ]', {'i': i, 'conn': conn}) -*/
331          /*- if idx -*/
332              /*? j() ?*/ /*? c.name ?*/_/*? conn.from_ends[idx[0]].interface.name ?*/ \<Rightarrow> /*? conn.name ?*/
333          /*- endif -*/
334          /*- set idx = eval('[ idx for idx in range(len(conn.to_ends)) if i.name == conn.to_ends[idx].instance.name ]', {'i': i, 'conn': conn}) -*/
335          /*- if idx -*/
336              /*? j() ?*/ /*? c.name ?*/_/*? conn.to_ends[idx[0]].interface.name ?*/ \<Rightarrow> /*? conn.name ?*/
337          /*- endif -*/
338      /*- endfor -*/
339      )"
340(** TPP: condense = False *)
341        /*- endfor -*/
342    /*- endfor -*/
343
344    /*- for u in c.provides -*/
345(** TPP: condense = True *)
346definition
347  /*- set type_sig = [] -*/
348  /*- for m in u.type.methods -*/
349    /*- if len(list(filter(lambda('x: x.direction in [\'in\', \'inout\']'), m.parameters))) > 0 -*/
350      /*- do type_sig.append('(\'cs local_state \\<Rightarrow>') -*/
351      /*- for p in filter(lambda('x: x.direction in [\'in\', \'inout\']'), m.parameters) -*/
352        /*- do type_sig.append('%s \\<Rightarrow>' % show_native_type(p.type)) -*/
353      /*- endfor -*/
354      /*- do type_sig.append('\'cs local_state) \\<Rightarrow>') -*/
355    /*- endif -*/
356    /*- do type_sig.append('(channel, \'cs) comp \\<Rightarrow>') -*/
357    /*- if m.return_type -*/
358      /*- do type_sig.append('(\'cs local_state \\<Rightarrow> %s) \\<Rightarrow>' % show_native_type(m.return_type)) -*/
359    /*- endif -*/
360    /*- for p in filter(lambda('x: x.direction in [\'out\', \'inout\']'), m.parameters) -*/
361      /*- do type_sig.append('(\'cs local_state \\<Rightarrow> %s) \\<Rightarrow>' % show_native_type(p.type)) -*/
362    /*- endfor -*/
363  /*- endfor -*/
364  /*- do type_sig.append('(channel, \'cs) comp') -*/
365  Recv_/*? i.name ?*/_/*? u.name ?*/ :: "/*? ' '.join(type_sig) ?*/"
366where
367  "Recv_/*? i.name ?*/_/*? u.name ?*/ \<equiv>
368      /*- set l = isabelle_symbol() -*/
369      Recv_/*? c.name ?*/_/*? u.name ?*/ (\<lambda>/*? l ?*/. case /*? l ?*/ of
370      /*- set j = joiner('|') -*/
371      /*- for conn in connections -*/
372          /*- set idx = eval('[ idx for idx in range(len(conn.from_ends)) if i.name == conn.from_ends[idx].instance.name ]', {'i': i, 'conn': conn}) -*/
373          /*- if idx -*/
374              /*? j() ?*/ /*? c.name ?*/_/*? conn.from_ends[idx[0]].interface.name ?*/ \<Rightarrow> /*? conn.name ?*/
375          /*- endif -*/
376          /*- set idx = eval('[ idx for idx in range(len(conn.to_ends)) if i.name == conn.to_ends[idx].instance.name ]', {'i': i, 'conn': conn}) -*/
377          /*- if idx -*/
378              /*? j() ?*/ /*? c.name ?*/_/*? conn.to_ends[idx[0]].interface.name ?*/ \<Rightarrow> /*? conn.name ?*/
379          /*- endif -*/
380      /*- endfor -*/
381      )"
382(** TPP: condense = False *)
383    /*- endfor -*/
384
385    /*- for u in c.emits -*/
386(** TPP: condense = True *)
387definition
388  Emit_/*? i.name ?*/_/*? u.name ?*/ :: "(channel, 'cs) comp"
389where
390  /*- set l = isabelle_symbol() -*/
391  "Emit_/*? i.name ?*/_/*? u.name ?*/ \<equiv> Emit_/*? c.name ?*/_/*? u.name ?*/ (\<lambda>/*? l ?*/. case /*? l ?*/ of
392  /*- set j = joiner('|') -*/
393  /*- for conn in connections -*/
394      /*- set idx = eval('[ idx for idx in range(len(conn.from_ends)) if i.name == conn.from_ends[idx].instance.name ]', {'i': i, 'conn': conn}) -*/
395      /*- if idx -*/
396          /*? j() ?*/ /*? c.name ?*/_/*? conn.from_ends[idx[0]].interface.name ?*/ \<Rightarrow> /*? conn.name ?*/
397      /*- endif -*/
398      /*- set idx = eval('[ idx for idx in range(len(conn.to_ends)) if i.name == conn.to_ends[idx].instance.name ]', {'i': i, 'conn': conn}) -*/
399      /*- if idx -*/
400          /*? j() ?*/ /*? c.name ?*/_/*? conn.to_ends[idx[0]].interface.name ?*/ \<Rightarrow> /*? conn.name ?*/
401      /*- endif -*/
402  /*- endfor -*/
403  )"
404(** TPP: condense = False *)
405    /*- endfor -*/
406
407    /*- for u in c.consumes -*/
408(** TPP: condense = True *)
409definition
410  Poll_/*? i.name ?*/_/*? u.name ?*/ :: "('cs local_state \<Rightarrow> bool \<Rightarrow> 'cs local_state) \<Rightarrow> (channel, 'cs) comp"
411where
412  /*- set l = isabelle_symbol() -*/
413  "Poll_/*? i.name ?*/_/*? u.name ?*/ \<equiv> Poll_/*? c.name ?*/_/*? u.name ?*/ (\<lambda>/*? l ?*/. case /*? l ?*/ of
414  /*- set j = joiner('|') -*/
415  /*- for conn in connections -*/
416      /*- set idx = eval('[ idx for idx in range(len(conn.from_ends)) if i.name == conn.from_ends[idx].instance.name ]', {'i': i, 'conn': conn}) -*/
417      /*- if idx -*/
418          /*? j() ?*/ /*? c.name ?*/_/*? conn.from_ends[idx[0]].interface.name ?*/ \<Rightarrow> /*? conn.name ?*/
419      /*- endif -*/
420      /*- set idx = eval('[ idx for idx in range(len(conn.to_ends)) if i.name == conn.to_ends[idx].instance.name ]', {'i': i, 'conn': conn}) -*/
421      /*- if idx -*/
422          /*? j() ?*/ /*? c.name ?*/_/*? conn.to_ends[idx[0]].interface.name ?*/ \<Rightarrow> /*? conn.name ?*/
423      /*- endif -*/
424  /*- endfor -*/
425  )"
426(** TPP: condense = False *)
427
428(** TPP: condense = True *)
429definition
430  Wait_/*? i.name ?*/_/*? u.name ?*/ :: "('cs local_state \<Rightarrow> bool \<Rightarrow> 'cs local_state) \<Rightarrow> (channel, 'cs) comp"
431where
432  /*- set l = isabelle_symbol() -*/
433  "Wait_/*? i.name ?*/_/*? u.name ?*/ \<equiv> Wait_/*? c.name ?*/_/*? u.name ?*/ (\<lambda>/*? l ?*/. case /*? l ?*/ of
434  /*- set j = joiner('|') -*/
435  /*- for conn in connections -*/
436      /*- set idx = eval('[ idx for idx in range(len(conn.from_ends)) if i.name == conn.from_ends[idx].instance.name ]', {'i': i, 'conn': conn}) -*/
437      /*- if idx -*/
438          /*? j() ?*/ /*? c.name ?*/_/*? conn.from_ends[idx[0]].interface.name ?*/ \<Rightarrow> /*? conn.name ?*/
439      /*- endif -*/
440      /*- set idx = eval('[ idx for idx in range(len(conn.to_ends)) if i.name == conn.to_ends[idx].instance.name ]', {'i': i, 'conn': conn}) -*/
441      /*- if idx -*/
442          /*? j() ?*/ /*? c.name ?*/_/*? conn.to_ends[idx[0]].interface.name ?*/ \<Rightarrow> /*? conn.name ?*/
443      /*- endif -*/
444  /*- endfor -*/
445  )"
446(** TPP: condense = False *)
447    /*- endfor -*/
448
449    /*- for u in c.dataports -*/
450(** TPP: condense = True *)
451definition
452  Read_/*? i.name ?*/_/*? u.name ?*/ :: "('cs local_state \<Rightarrow> nat) \<Rightarrow> ('cs local_state \<Rightarrow> variable \<Rightarrow> 'cs local_state) \<Rightarrow> (channel, 'cs) comp"
453where
454  /*- set l = isabelle_symbol() -*/
455  "Read_/*? i.name ?*/_/*? u.name ?*/ \<equiv> Read_/*? c.name ?*/_/*? u.name ?*/ (\<lambda>/*? l ?*/. case /*? l ?*/ of
456  /*- set j = joiner('|') -*/
457  /*- for conn in connections -*/
458      /*- set idx = eval('[ idx for idx in range(len(conn.from_ends)) if i.name == conn.from_ends[idx].instance.name ]', {'i': i, 'conn': conn}) -*/
459      /*- if idx -*/
460          /*? j() ?*/ /*? c.name ?*/_/*? conn.from_ends[idx[0]].interface.name ?*/ \<Rightarrow> /*? conn.name ?*/
461      /*- endif -*/
462      /*- set idx = eval('[ idx for idx in range(len(conn.to_ends)) if i.name == conn.to_ends[idx].instance.name ]', {'i': i, 'conn': conn}) -*/
463      /*- if idx -*/
464          /*? j() ?*/ /*? c.name ?*/_/*? conn.to_ends[idx[0]].interface.name ?*/ \<Rightarrow> /*? conn.name ?*/
465      /*- endif -*/
466  /*- endfor -*/
467  )"
468(** TPP: condense = False *)
469
470(** TPP: condense = True *)
471definition
472  Write_/*? i.name ?*/_/*? u.name ?*/ :: "('cs local_state \<Rightarrow> nat) \<Rightarrow> ('cs local_state \<Rightarrow> variable) \<Rightarrow> (channel, 'cs) comp"
473where
474  /*- set l = isabelle_symbol() -*/
475  "Write_/*? i.name ?*/_/*? u.name ?*/ \<equiv> Write_/*? c.name ?*/_/*? u.name ?*/ (\<lambda>/*? l ?*/. case /*? l ?*/ of
476  /*- set j = joiner('|') -*/
477  /*- for conn in connections -*/
478      /*- set idx = eval('[ idx for idx in range(len(conn.from_ends)) if i.name == conn.from_ends[idx].instance.name ]', {'i': i, 'conn': conn}) -*/
479      /*- if idx -*/
480          /*? j() ?*/ /*? c.name ?*/_/*? conn.from_ends[idx[0]].interface.name ?*/ \<Rightarrow> /*? conn.name ?*/
481      /*- endif -*/
482      /*- set idx = eval('[ idx for idx in range(len(conn.to_ends)) if i.name == conn.to_ends[idx].instance.name ]', {'i': i, 'conn': conn}) -*/
483      /*- if idx -*/
484          /*? j() ?*/ /*? c.name ?*/_/*? conn.to_ends[idx[0]].interface.name ?*/ \<Rightarrow> /*? conn.name ?*/
485      /*- endif -*/
486  /*- endfor -*/
487  )"
488(** TPP: condense = False *)
489    /*- endfor -*/
490
491/*- endfor -*/
492
493locale system_state =
494  fixes init_component_state :: 'cs
495  fixes trusted :: "(inst, ((channel, 'cs) comp \<times> 'cs local_state)) map"
496begin
497
498/*- for c in components -*/
499    /*# Emit a broad definition for each component if the user does not want to instantiate it. #*/
500(** TPP: condense = True *)
501definition
502  /*? c.name ?*/_untrusted :: "(/*? c.name ?*/_channel \<Rightarrow> channel) \<Rightarrow> (channel, 'cs) comp"
503where
504  /*- set ch = isabelle_symbol('ch') -*/
505  "/*? c.name ?*/_untrusted /*? ch ?*/ \<equiv>
506      LOOP (
507          UserStep
508          /*- for i in c.uses + c.provides + c.emits + c.consumes + c.dataports -*/
509              \<squnion> ArbitraryRequest (/*? ch ?*/ /*? c.name ?*/_/*? i.name ?*/)
510              \<squnion> ArbitraryResponse (/*? ch ?*/ /*? c.name ?*/_/*? i.name ?*/)
511          /*- endfor -*/
512      )"
513(** TPP: condense = False *)
514/*- endfor -*/
515
516/*# Emit simulated components for each event. #*/
517/*- for e in reduce(lambda('xs, b: xs + ([b.type] if b.type not in xs else [])'), flatMap(lambda('x: x.emits + x.consumes'), components), []) -*/
518
519(* Simulated component for event /*? e ?*/. *)
520type_synonym /*? e ?*/_channel = unit
521
522(** TPP: condense = True *)
523definition
524  /*? e ?*/ :: "(/*? e ?*/_channel \<Rightarrow> channel) \<Rightarrow> (channel, 'cs) comp"
525where
526  /*- set ch = isabelle_symbol('ch') -*/
527  "/*? e ?*/ /*? ch ?*/ \<equiv> event (/*? ch ?*/ ())"
528(** TPP: condense = False *)
529/*- endfor -*/
530
531/*# Emit simulated components for each dataport. #*/
532/*- for d in reduce(lambda('xs, b: xs + ([b.type] if b.type not in xs else [])'), flatMap(lambda('x: x.dataports'), components), []) -*/
533    /*# The built-in type 'Buf' is defined in Connector.thy. #*/
534    /*- if d != 'Buf' -*/
535
536type_synonym /*? d ?*/\<^sub>d_channel = unit
537
538(** TPP: condense = True *)
539definition
540  /*? d ?*/\<^sub>d :: "(/*? d ?*/\<^sub>d_channel \<Rightarrow> channel) \<Rightarrow> (channel, 'cs) comp"
541where
542  /*- set ch = isabelle_symbol('ch') -*/
543  "/*? d ?*/\<^sub>d /*? ch ?*/ \<equiv> memory (/*? ch ?*/ ())"
544(** TPP: condense = False *)
545    /*- endif -*/
546/*- endfor -*/
547
548(* Component instantiations *)
549/*- for i in instances -*/
550    /*- set c = i.type -*/
551
552(** TPP: condense = True *)
553definition
554  /*? i.name ?*/_untrusted :: "(channel, 'cs) comp"
555where
556  /*- set l = isabelle_symbol() -*/
557  "/*? i.name ?*/_untrusted \<equiv> /*? c.name ?*/_untrusted (\<lambda>/*? l ?*/. case /*? l ?*/ of
558  /*- set j = joiner('|') -*/
559  /*- for conn in connections -*/
560      /*- set idx = eval('[ idx for idx in range(len(conn.from_ends)) if i.name == conn.from_ends[idx].instance.name ]', {'i': i, 'conn': conn}) -*/
561      /*- if idx -*/
562          /*? j() ?*/ /*? c.name ?*/_/*? conn.from_ends[idx[0]].interface.name ?*/ \<Rightarrow> /*? conn.name ?*/
563      /*- endif -*/
564      /*- set idx = eval('[ idx for idx in range(len(conn.to_ends)) if i.name == conn.to_ends[idx].instance.name ]', {'i': i, 'conn': conn}) -*/
565      /*- if idx -*/
566          /*? j() ?*/ /*? c.name ?*/_/*? conn.to_ends[idx[0]].interface.name ?*/ \<Rightarrow> /*? conn.name ?*/
567      /*- endif -*/
568  /*- endfor -*/
569  )"
570(** TPP: condense = False *)
571
572/*- endfor -*/
573
574/*# Simulated component instance for each event connection. #*/
575/*- for c in filter(lambda('x: x.type.from_type == \'Event\''), connections) -*/
576definition
577  /*? c.name ?*/\<^sub>e_instance :: "(channel, 'cs) comp"
578where
579  "/*? c.name ?*/\<^sub>e_instance \<equiv> /*? c.from_interface.type ?*/ (\<lambda>_. /*? c.name ?*/)"
580/*- endfor -*/
581
582/*# Simulated component instance for each dataport connection. #*/
583/*- for c in filter(lambda('x: x.type.from_type == \'Dataport\''), connections) -*/
584definition
585  /*? c.name ?*/\<^sub>d_instance :: "(channel, 'cs) comp"
586where
587  "/*? c.name ?*/\<^sub>d_instance \<equiv> /*? c.from_interface.type ?*/\<^sub>d (\<lambda>_. /*? c.name ?*/)"
588/*- endfor -*/
589
590(* Global initial state *)
591/*# Even though this is generated as a mapping to an option type it is actually
592 ** full.
593 #*/
594(** TPP: condense = True *)
595definition
596  gs\<^sub>0 :: "(inst, channel, 'cs) global_state"
597where
598  /*- set p = isabelle_symbol('p') -*/
599  /*- set s = isabelle_symbol() -*/
600  "gs\<^sub>0 /*? p ?*/ \<equiv> case trusted /*? p ?*/ of Some /*? s ?*/ \<Rightarrow> Some /*? s ?*/ | _ \<Rightarrow> (case /*? p ?*/ of
601  /*- set j = joiner('|') -*/
602  /*- for i in instances -*/
603      /*? j() ?*/ /*? i.name ?*/ \<Rightarrow> Some (/*? i.name ?*/_untrusted, Component init_component_state)
604  /*- endfor -*/
605  /*- for c in connections -*/
606      /*- if c.type.from_type == 'Event' -*/
607          /*? j() ?*/ /*? c.name ?*/\<^sub>e \<Rightarrow> Some (/*? c.name ?*/\<^sub>e_instance, init_event_state)
608      /*- elif c.type.from_type == 'Dataport' -*/
609          /*? j() ?*/ /*? c.name ?*/\<^sub>d \<Rightarrow> Some (/*? c.name ?*/\<^sub>d_instance, init_memory_state)
610      /*- endif -*/
611  /*- endfor -*/
612  )"
613(** TPP: condense = False *)
614
615end
616
617end
618