10 |
10 |
11 types val = nat (* for the meta theory, this may be anything, but with |
11 types val = nat (* for the meta theory, this may be anything, but with |
12 current Isabelle, types cannot be refined later *) |
12 current Isabelle, types cannot be refined later *) |
13 types glb |
13 types glb |
14 loc |
14 loc |
15 arities (*val,*)glb,loc :: term |
15 arities (*val,*)glb,loc :: type |
16 consts Arg, Res :: loc |
16 consts Arg, Res :: loc |
17 |
17 |
18 datatype vname = Glb glb | Loc loc |
18 datatype vname = Glb glb | Loc loc |
19 types globs = glb => val |
19 types globs = glb => val |
20 locals = loc => val |
20 locals = loc => val |
21 datatype state = st globs locals |
21 datatype state = st globs locals |
22 (* for the meta theory, the following would be sufficient: |
22 (* for the meta theory, the following would be sufficient: |
23 types state |
23 types state |
24 arities state::term |
24 arities state::type |
25 consts st:: [globs , locals] => state |
25 consts st:: [globs , locals] => state |
26 *) |
26 *) |
27 types aexp = state => val |
27 types aexp = state => val |
28 bexp = state => bool |
28 bexp = state => bool |
29 |
29 |
30 types pname |
30 types pname |
31 arities pname :: term |
31 arities pname :: type |
32 |
32 |
33 datatype com |
33 datatype com |
34 = SKIP |
34 = SKIP |
35 | Ass vname aexp ("_:==_" [65, 65 ] 60) |
35 | Ass vname aexp ("_:==_" [65, 65 ] 60) |
36 | Local loc aexp com ("LOCAL _:=_ IN _" [65, 0, 61] 60) |
36 | Local loc aexp com ("LOCAL _:=_ IN _" [65, 0, 61] 60) |