src/HOL/Bali/Value.thy
author haftmann
Mon Aug 14 13:46:06 2006 +0200 (2006-08-14)
changeset 20380 14f9f2a1caa6
parent 17160 fb65eda72fc7
child 32960 69916a850301
permissions -rw-r--r--
simplified code generator setup
wenzelm@12857
     1
(*  Title:      HOL/Bali/Value.thy
schirmer@12854
     2
    ID:         $Id$
schirmer@12854
     3
    Author:     David von Oheimb
schirmer@12854
     4
*)
schirmer@12854
     5
header {* Java values *}
schirmer@12854
     6
schirmer@12854
     7
schirmer@12854
     8
haftmann@16417
     9
theory Value imports Type begin
schirmer@12854
    10
schirmer@13688
    11
typedecl loc            --{* locations, i.e. abstract references on objects *}
schirmer@12854
    12
schirmer@12854
    13
datatype val
schirmer@13688
    14
	= Unit          --{* dummy result value of void methods *}
schirmer@13688
    15
	| Bool bool     --{* Boolean value *}
schirmer@13688
    16
	| Intg int      --{* integer value *}
schirmer@13688
    17
	| Null          --{* null reference *}
schirmer@13688
    18
	| Addr loc      --{* addresses, i.e. locations of objects *}
schirmer@12854
    19
schirmer@12854
    20
schirmer@12854
    21
translations "val" <= (type) "Term.val"
schirmer@12854
    22
             "loc" <= (type) "Term.loc"
schirmer@12854
    23
schirmer@12854
    24
consts   the_Bool   :: "val \<Rightarrow> bool"  
schirmer@12854
    25
primrec "the_Bool (Bool b) = b"
schirmer@12854
    26
consts   the_Intg   :: "val \<Rightarrow> int"
schirmer@12854
    27
primrec "the_Intg (Intg i) = i"
schirmer@12854
    28
consts   the_Addr   :: "val \<Rightarrow> loc"
schirmer@12854
    29
primrec "the_Addr (Addr a) = a"
schirmer@12854
    30
schirmer@12854
    31
types	dyn_ty      = "loc \<Rightarrow> ty option"
schirmer@12854
    32
consts
schirmer@12854
    33
  typeof        :: "dyn_ty \<Rightarrow> val \<Rightarrow> ty option"
schirmer@13688
    34
  defpval       :: "prim_ty \<Rightarrow> val"  --{* default value for primitive types *}
schirmer@13688
    35
  default_val   :: "     ty \<Rightarrow> val"  --{* default value for all types *}
schirmer@12854
    36
schirmer@12854
    37
primrec "typeof dt  Unit    = Some (PrimT Void)"
schirmer@12854
    38
	"typeof dt (Bool b) = Some (PrimT Boolean)"
schirmer@12854
    39
	"typeof dt (Intg i) = Some (PrimT Integer)"
schirmer@12854
    40
	"typeof dt  Null    = Some NT"
schirmer@12854
    41
	"typeof dt (Addr a) = dt a"
schirmer@12854
    42
schirmer@12854
    43
primrec	"defpval Void    = Unit"
schirmer@12854
    44
	"defpval Boolean = Bool False"
schirmer@12854
    45
	"defpval Integer = Intg 0"
schirmer@12854
    46
primrec	"default_val (PrimT pt) = defpval pt"
schirmer@12854
    47
	"default_val (RefT  r ) = Null"
schirmer@12854
    48
schirmer@12854
    49
end