equal
deleted
inserted
replaced
20 | Addr loc (* addresses, i.e. locations of objects *) |
20 | Addr loc (* addresses, i.e. locations of objects *) |
21 types val = val_ |
21 types val = val_ |
22 translations "val" <= (type) "val_" |
22 translations "val" <= (type) "val_" |
23 |
23 |
24 consts |
24 consts |
25 the_Bool :: "val \\<Rightarrow> bool" |
25 the_Bool :: "val => bool" |
26 the_Intg :: "val \\<Rightarrow> int" |
26 the_Intg :: "val => int" |
27 the_Addr :: "val \\<Rightarrow> loc" |
27 the_Addr :: "val => loc" |
28 |
28 |
29 primrec |
29 primrec |
30 "the_Bool (Bool b) = b" |
30 "the_Bool (Bool b) = b" |
31 |
31 |
32 primrec |
32 primrec |
34 |
34 |
35 primrec |
35 primrec |
36 "the_Addr (Addr a) = a" |
36 "the_Addr (Addr a) = a" |
37 |
37 |
38 consts |
38 consts |
39 defpval :: "prim_ty \\<Rightarrow> val" (* default value for primitive types *) |
39 defpval :: "prim_ty => val" (* default value for primitive types *) |
40 default_val :: "ty \\<Rightarrow> val" (* default value for all types *) |
40 default_val :: "ty => val" (* default value for all types *) |
41 |
41 |
42 primrec |
42 primrec |
43 "defpval Void = Unit" |
43 "defpval Void = Unit" |
44 "defpval Boolean = Bool False" |
44 "defpval Boolean = Bool False" |
45 "defpval Integer = Intg (#0)" |
45 "defpval Integer = Intg (#0)" |