src/HOL/Bali/Value.thy
author wenzelm
Mon, 28 Jan 2002 18:51:48 +0100
changeset 12858 6214f03d6d27
parent 12857 a4386cc9b1c3
child 13688 a0b16d42d489
permissions -rw-r--r--
GPLed;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
12857
a4386cc9b1c3 tuned header;
wenzelm
parents: 12854
diff changeset
     1
(*  Title:      HOL/Bali/Value.thy
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     2
    ID:         $Id$
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     3
    Author:     David von Oheimb
12858
wenzelm
parents: 12857
diff changeset
     4
    License:    GPL (GNU GENERAL PUBLIC LICENSE)
12854
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     5
*)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     6
header {* Java values *}
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     7
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     8
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
     9
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    10
theory Value = Type:
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    11
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    12
typedecl loc            (* locations, i.e. abstract references on objects *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    13
arities	 loc :: "type"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    14
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    15
datatype val
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    16
	= Unit          (* dummy result value of void methods *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    17
	| Bool bool     (* Boolean value *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    18
	| Intg int      (* integer value *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    19
	| Null          (* null reference *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    20
	| Addr loc      (* addresses, i.e. locations of objects *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    21
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    22
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    23
translations "val" <= (type) "Term.val"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    24
             "loc" <= (type) "Term.loc"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    25
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    26
consts   the_Bool   :: "val \<Rightarrow> bool"  
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    27
primrec "the_Bool (Bool b) = b"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    28
consts   the_Intg   :: "val \<Rightarrow> int"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    29
primrec "the_Intg (Intg i) = i"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    30
consts   the_Addr   :: "val \<Rightarrow> loc"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    31
primrec "the_Addr (Addr a) = a"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    32
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    33
types	dyn_ty      = "loc \<Rightarrow> ty option"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    34
consts
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    35
  typeof        :: "dyn_ty \<Rightarrow> val \<Rightarrow> ty option"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    36
  defpval       :: "prim_ty \<Rightarrow> val"      (* default value for primitive types *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    37
  default_val   :: "     ty \<Rightarrow> val"      (* default value for all types *)
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    38
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    39
primrec "typeof dt  Unit    = Some (PrimT Void)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    40
	"typeof dt (Bool b) = Some (PrimT Boolean)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    41
	"typeof dt (Intg i) = Some (PrimT Integer)"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    42
	"typeof dt  Null    = Some NT"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    43
	"typeof dt (Addr a) = dt a"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    44
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    45
primrec	"defpval Void    = Unit"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    46
	"defpval Boolean = Bool False"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    47
	"defpval Integer = Intg 0"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    48
primrec	"default_val (PrimT pt) = defpval pt"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    49
	"default_val (RefT  r ) = Null"
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    50
00d4a435777f Isabelle/Bali sources;
schirmer
parents:
diff changeset
    51
end