15 | Intg int --{* integer value *} |
15 | Intg int --{* integer value *} |
16 | Null --{* null reference *} |
16 | Null --{* null reference *} |
17 | Addr loc --{* addresses, i.e. locations of objects *} |
17 | Addr loc --{* addresses, i.e. locations of objects *} |
18 |
18 |
19 |
19 |
20 consts the_Bool :: "val \<Rightarrow> bool" |
20 primrec the_Bool :: "val \<Rightarrow> bool" |
21 primrec "the_Bool (Bool b) = b" |
21 where "the_Bool (Bool b) = b" |
22 consts the_Intg :: "val \<Rightarrow> int" |
22 |
23 primrec "the_Intg (Intg i) = i" |
23 primrec the_Intg :: "val \<Rightarrow> int" |
24 consts the_Addr :: "val \<Rightarrow> loc" |
24 where "the_Intg (Intg i) = i" |
25 primrec "the_Addr (Addr a) = a" |
25 |
|
26 primrec the_Addr :: "val \<Rightarrow> loc" |
|
27 where "the_Addr (Addr a) = a" |
26 |
28 |
27 types dyn_ty = "loc \<Rightarrow> ty option" |
29 types dyn_ty = "loc \<Rightarrow> ty option" |
28 consts |
|
29 typeof :: "dyn_ty \<Rightarrow> val \<Rightarrow> ty option" |
|
30 defpval :: "prim_ty \<Rightarrow> val" --{* default value for primitive types *} |
|
31 default_val :: " ty \<Rightarrow> val" --{* default value for all types *} |
|
32 |
30 |
33 primrec "typeof dt Unit = Some (PrimT Void)" |
31 primrec typeof :: "dyn_ty \<Rightarrow> val \<Rightarrow> ty option" |
34 "typeof dt (Bool b) = Some (PrimT Boolean)" |
32 where |
35 "typeof dt (Intg i) = Some (PrimT Integer)" |
33 "typeof dt Unit = Some (PrimT Void)" |
36 "typeof dt Null = Some NT" |
34 | "typeof dt (Bool b) = Some (PrimT Boolean)" |
37 "typeof dt (Addr a) = dt a" |
35 | "typeof dt (Intg i) = Some (PrimT Integer)" |
|
36 | "typeof dt Null = Some NT" |
|
37 | "typeof dt (Addr a) = dt a" |
38 |
38 |
39 primrec "defpval Void = Unit" |
39 primrec defpval :: "prim_ty \<Rightarrow> val" --{* default value for primitive types *} |
40 "defpval Boolean = Bool False" |
40 where |
41 "defpval Integer = Intg 0" |
41 "defpval Void = Unit" |
42 primrec "default_val (PrimT pt) = defpval pt" |
42 | "defpval Boolean = Bool False" |
43 "default_val (RefT r ) = Null" |
43 | "defpval Integer = Intg 0" |
|
44 |
|
45 primrec default_val :: "ty \<Rightarrow> val" --{* default value for all types *} |
|
46 where |
|
47 "default_val (PrimT pt) = defpval pt" |
|
48 | "default_val (RefT r ) = Null" |
44 |
49 |
45 end |
50 end |