1(*
2 * Copyright 2017, Data61, CSIRO
3 *
4 * This software may be distributed and modified according to the terms of
5 * the BSD 2-Clause license. Note that NO WARRANTY is provided.
6 * See "LICENSE_BSD2.txt" for details.
7 *
8 * @TAG(DATA61_BSD)
9 *)
10
11theory CLanguage
12imports "CProof"
13begin
14
15definition
16  creturn :: "((c_exntype \<Rightarrow> c_exntype) \<Rightarrow> ('c, 'd) state_scheme \<Rightarrow> ('c, 'd) state_scheme)
17      \<Rightarrow> (('a \<Rightarrow> 'a) \<Rightarrow> ('c, 'd) state_scheme \<Rightarrow> ('c, 'd) state_scheme)
18      \<Rightarrow> (('c, 'd) state_scheme \<Rightarrow> 'a) \<Rightarrow> (('c, 'd) state_scheme,'p,'f) com"
19where
20  "creturn rtu xfu v \<equiv> (Basic (\<lambda>s. xfu (\<lambda>_. v s) s);; (Basic (rtu (\<lambda>_. Return));; THROW))"
21
22definition
23  creturn_void :: "((c_exntype \<Rightarrow> c_exntype) \<Rightarrow> ('c, 'd) state_scheme
24      \<Rightarrow> ('c, 'd) state_scheme) \<Rightarrow> (('c, 'd) state_scheme,'p,'f) com"
25where
26  "creturn_void rtu \<equiv> (Basic (rtu (\<lambda>_. Return));; THROW)"
27
28definition
29  cbreak :: "((c_exntype \<Rightarrow> c_exntype) \<Rightarrow> ('c, 'd) state_scheme
30      \<Rightarrow> ('c, 'd) state_scheme) \<Rightarrow> (('c, 'd) state_scheme,'p,'f) com"
31where
32  "cbreak rtu \<equiv> (Basic (rtu (\<lambda>_. Break));; THROW)"
33
34definition
35  ccatchbrk :: "( ('c, 'd) state_scheme \<Rightarrow> c_exntype) \<Rightarrow> (('c, 'd) state_scheme,'p,'f) com"
36where
37  "ccatchbrk rt \<equiv> Cond {s. rt s = Break} SKIP THROW"
38
39definition
40  cchaos :: "('b \<Rightarrow> 'a \<Rightarrow> 'a) \<Rightarrow> ('a,'c,'d) com"
41where
42  "cchaos upd \<equiv> Spec { (s0,s) . \<exists>v. s = upd v s0 }"
43
44definition
45  "guarded_spec_body F R = Guard F (fst ` R) (Spec R)"
46
47end
48