1(*
2 * Copyright 2014, NICTA
3 *
4 * This software may be distributed and modified according to the terms of
5 * the GNU General Public License version 2. Note that NO WARRANTY is provided.
6 * See "LICENSE_GPLv2.txt" for details.
7 *
8 * @TAG(NICTA_GPL)
9 *)
10
11(* Some convenient definitions for accessing members inside types. *)
12
13(*<*)
14theory Helpers_CAMKES
15imports Types_CAMKES
16begin
17(*>*)
18
19(*<*)
20(* For finding a component or connection. *)
21definition
22  lookup :: "('a \<times> 'b) list \<Rightarrow> 'a \<Rightarrow> 'b"
23where (* Assumes the filter will return a unique element. *)
24  "lookup xs x = snd (hd (filter (\<lambda>y. (x = (fst y))) xs))"
25
26(* For accessing properties of a connection. *)
27abbreviation "from_components conn  \<equiv> map fst (conn_from conn)"
28abbreviation "from_interfaces conn  \<equiv> map snd (conn_from conn)"
29abbreviation "to_components conn    \<equiv> map fst (conn_to conn)"
30abbreviation "to_interfaces conn    \<equiv> map snd (conn_to conn)"
31
32(* For finding ''interfaces'' within a component. *)
33abbreviation "in_map conns xs \<equiv> (\<exists>s\<in>set conns. s \<in> (fst ` (set xs)))"
34
35abbreviation "does_provide c s \<equiv> (in_map s (provides c))"
36abbreviation "does_require c s \<equiv> (in_map s (requires c))"
37abbreviation "does_emit c s    \<equiv> (in_map s (emits c))"
38abbreviation "does_consume c s \<equiv> (in_map s (consumes c))"
39abbreviation "has_dataport c s \<equiv> (in_map s (dataports c))"
40(*>*)
41
42(*<*)end(*>*)
43