--- a/src/HOL/MicroJava/J/Term.thy Fri Jul 14 16:32:44 2000 +0200
+++ b/src/HOL/MicroJava/J/Term.thy Fri Jul 14 16:32:51 2000 +0200
@@ -6,33 +6,20 @@
Java expressions and statements
*)
-Term = Type +
-
-types loc (* locations, i.e. abstract references on objects *)
-arities loc :: term
-
-datatype val_ (* name non 'val' because of clash with ML token *)
- = Unit (* dummy result value of void methods *)
- | Null (* null reference *)
- | Bool bool (* Boolean value *)
- | Intg int (* integer value *) (* Name Intg instead of Int because
- of clash with HOL/Set.thy *)
- | Addr loc (* addresses, i.e. locations of objects *)
-types val = val_
-translations "val" <= (type) "val_"
+Term = Value +
datatype binop = Eq | Add (* function codes for binary operation *)
datatype expr
= NewC cname (* class instance creation *)
- | Cast ty expr (* type cast *)
+ | Cast ref_ty expr (* type cast *)
| Lit val (* literal value, also references *)
| BinOp binop expr expr (* binary operation *)
| LAcc vname (* local (incl. parameter) access *)
| LAss vname expr (* local assign *) ("_\\<Colon>=_" [ 90,90]90)
| FAcc cname expr vname (* field access *) ("{_}_.._"[10,90,99 ]90)
| FAss cname expr vname
- expr (* field ass. *)("{_}_.._\\<in>=_"[10,90,99,90]90)
+ expr (* field ass. *)("{_}_.._:=_"[10,90,99,90]90)
| Call expr mname (ty list) (expr list)(* method call*)
("_.._'({_}_')" [90,99,10,10] 90)
and stmt