header {* \isaheader{Jinja Values} *}
theory Value imports TypeRel begin
type_synonym addr = nat
datatype val
= Unit -- "dummy result value of void expressions"
| Null -- "null reference"
| Bool bool -- "Boolean value"
| Intg int -- "integer value"
| Addr addr -- "addresses of objects in the heap"
primrec the_Intg :: "val => int" where
"the_Intg (Intg i) = i"
primrec the_Addr :: "val => addr" where
"the_Addr (Addr a) = a"
primrec default_val :: "ty => val" -- "default value for all types" where
"default_val Void = Unit"
| "default_val Boolean = Bool False"
| "default_val Integer = Intg 0"
| "default_val NT = Null"
| "default_val (Class C) = Null"
end