equal
deleted
inserted
replaced
2 |
2 |
3 theory Procs imports BExp begin |
3 theory Procs imports BExp begin |
4 |
4 |
5 subsection "Procedures and Local Variables" |
5 subsection "Procedures and Local Variables" |
6 |
6 |
|
7 type_synonym pname = string |
|
8 |
7 datatype |
9 datatype |
8 com = SKIP |
10 com = SKIP |
9 | Assign name aexp ("_ ::= _" [1000, 61] 61) |
11 | Assign vname aexp ("_ ::= _" [1000, 61] 61) |
10 | Semi com com ("_;/ _" [60, 61] 60) |
12 | Semi com com ("_;/ _" [60, 61] 60) |
11 | If bexp com com ("(IF _/ THEN _/ ELSE _)" [0, 0, 61] 61) |
13 | If bexp com com ("(IF _/ THEN _/ ELSE _)" [0, 0, 61] 61) |
12 | While bexp com ("(WHILE _/ DO _)" [0, 61] 61) |
14 | While bexp com ("(WHILE _/ DO _)" [0, 61] 61) |
13 | Var name com ("(1{VAR _;;/ _})") |
15 | Var vname com ("(1{VAR _;;/ _})") |
14 | Proc name com com ("(1{PROC _ = _;;/ _})") |
16 | Proc pname com com ("(1{PROC _ = _;;/ _})") |
15 | CALL name |
17 | CALL pname |
16 |
18 |
17 definition "test_com = |
19 definition "test_com = |
18 {VAR ''x'';; |
20 {VAR ''x'';; |
19 ''x'' ::= N 0; |
21 ''x'' ::= N 0; |
20 {PROC ''p'' = ''x'' ::= Plus (V ''x'') (V ''x'');; |
22 {PROC ''p'' = ''x'' ::= Plus (V ''x'') (V ''x'');; |