9 theory Term = Main: |
9 theory Term = Main: |
10 |
10 |
11 typedecl cname (* class name *) |
11 typedecl cname (* class name *) |
12 typedecl vnam (* variable or field name *) |
12 typedecl vnam (* variable or field name *) |
13 typedecl mname (* method name *) |
13 typedecl mname (* method name *) |
14 types imname = "cname \<times> mname" |
|
15 |
14 |
16 datatype vname (* variable for special names *) |
15 datatype vname (* variable for special names *) |
17 = This (* This pointer *) |
16 = This (* This pointer *) |
18 | Param (* method parameter *) |
17 | Param (* method parameter *) |
19 | Res (* method result *) |
18 | Res (* method result *) |
24 | Comp stmt stmt ("_;; _" [91,90 ] 90) |
23 | Comp stmt stmt ("_;; _" [91,90 ] 90) |
25 | Cond expr stmt stmt ("If '(_') _ Else _" [99,91,91] 91) |
24 | Cond expr stmt stmt ("If '(_') _ Else _" [99,91,91] 91) |
26 | Loop vname stmt ("While '(_') _" [99,91 ] 91) |
25 | Loop vname stmt ("While '(_') _" [99,91 ] 91) |
27 | LAss vname expr ("_ :== _" [99, 95] 94) (* local ass. *) |
26 | LAss vname expr ("_ :== _" [99, 95] 94) (* local ass. *) |
28 | FAss expr vnam expr ("_.._:==_" [95,99,95] 94) (* field ass. *) |
27 | FAss expr vnam expr ("_.._:==_" [95,99,95] 94) (* field ass. *) |
29 | Meth cname mname (* virtual method *) |
28 | Meth "cname \<times> mname" (* virtual method *) |
30 | Impl imname (* method implementation *) |
29 | Impl "cname \<times> mname" (* method implementation *) |
31 and expr |
30 and expr |
32 = NewC cname ("new _" [ 99] 95) (* object creation *) |
31 = NewC cname ("new _" [ 99] 95) (* object creation *) |
33 | Cast cname expr (* type cast *) |
32 | Cast cname expr (* type cast *) |
34 | LAcc vname (* local access *) |
33 | LAcc vname (* local access *) |
35 | FAcc expr vnam ("_.._" [95,99] 95) (* field access *) |
34 | FAcc expr vnam ("_.._" [95,99] 95) (* field access *) |