equal
deleted
inserted
replaced
92 vnam ("string") |
92 vnam ("string") |
93 mname ("string") |
93 mname ("string") |
94 loc_ ("int") |
94 loc_ ("int") |
95 |
95 |
96 consts_code |
96 consts_code |
97 "new_Addr" ("new'_addr {* %x. case x of None => True | Some y => False *}/ {* None *}/ {* Loc *}") |
97 "new_Addr" ("\<module>new'_addr {* %x. case x of None => True | Some y => False *}/ {* None *}/ {* Loc *}") |
|
98 attach {* |
|
99 fun new_addr p none loc hp = |
|
100 let fun nr i = if p (hp (loc i)) then (loc i, none) else nr (i+1); |
|
101 in nr 0 end; |
|
102 *} |
98 |
103 |
99 "arbitrary" ("(raise ERROR)") |
104 "arbitrary" ("(raise ERROR)") |
100 "arbitrary" :: "val" ("{* Unit *}") |
105 "arbitrary" :: "val" ("{* Unit *}") |
101 "arbitrary" :: "cname" ("{* Object *}") |
106 "arbitrary" :: "cname" ("{* Object *}") |
102 |
107 |
104 "test_nam" ("\"test\"") |
109 "test_nam" ("\"test\"") |
105 "append_name" ("\"append\"") |
110 "append_name" ("\"append\"") |
106 "makelist_name" ("\"makelist\"") |
111 "makelist_name" ("\"makelist\"") |
107 "val_nam" ("\"val\"") |
112 "val_nam" ("\"val\"") |
108 "next_nam" ("\"next\"") |
113 "next_nam" ("\"next\"") |
109 |
|
110 ML {* |
|
111 fun new_addr p none loc hp = |
|
112 let fun nr i = if p (hp (loc i)) then (loc i, none) else nr (i+1); |
|
113 in nr 0 end; |
|
114 *} |
|
115 |
114 |
116 subsection {* Single step execution *} |
115 subsection {* Single step execution *} |
117 |
116 |
118 generate_code |
117 generate_code |
119 test = "exec (E, start_state E test_name makelist_name)" |
118 test = "exec (E, start_state E test_name makelist_name)" |