20 | Bool bool -- "Boolean value" |
20 | Bool bool -- "Boolean value" |
21 | Intg int -- "integer value, name Intg instead of Int because |
21 | Intg int -- "integer value, name Intg instead of Int because |
22 of clash with HOL/Set.thy" |
22 of clash with HOL/Set.thy" |
23 | Addr loc -- "addresses, i.e. locations of objects " |
23 | Addr loc -- "addresses, i.e. locations of objects " |
24 |
24 |
25 consts |
25 primrec the_Bool :: "val => bool" where |
26 the_Bool :: "val => bool" |
|
27 the_Intg :: "val => int" |
|
28 the_Addr :: "val => loc" |
|
29 |
|
30 primrec |
|
31 "the_Bool (Bool b) = b" |
26 "the_Bool (Bool b) = b" |
32 |
27 |
33 primrec |
28 primrec the_Intg :: "val => int" where |
34 "the_Intg (Intg i) = i" |
29 "the_Intg (Intg i) = i" |
35 |
30 |
36 primrec |
31 primrec the_Addr :: "val => loc" where |
37 "the_Addr (Addr a) = a" |
32 "the_Addr (Addr a) = a" |
38 |
33 |
39 consts |
34 primrec defpval :: "prim_ty => val" -- "default value for primitive types" where |
40 defpval :: "prim_ty => val" -- "default value for primitive types" |
35 "defpval Void = Unit" |
41 default_val :: "ty => val" -- "default value for all types" |
36 | "defpval Boolean = Bool False" |
|
37 | "defpval Integer = Intg 0" |
42 |
38 |
43 primrec |
39 primrec default_val :: "ty => val" -- "default value for all types" where |
44 "defpval Void = Unit" |
|
45 "defpval Boolean = Bool False" |
|
46 "defpval Integer = Intg 0" |
|
47 |
|
48 primrec |
|
49 "default_val (PrimT pt) = defpval pt" |
40 "default_val (PrimT pt) = defpval pt" |
50 "default_val (RefT r ) = Null" |
41 | "default_val (RefT r ) = Null" |
51 |
42 |
52 end |
43 end |