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