|
@@ -262,31 +262,90 @@ class ModelverseKernel(object):
|
|
|
#############################################
|
|
|
### Transformation rules for instructions ###
|
|
|
#############################################
|
|
|
- def break_init(self, user_root):
|
|
|
+ def continue_init(self, user_root):
|
|
|
user_frame, = yield [("RD", [user_root, "frame"])]
|
|
|
- phase_link, ip_link = \
|
|
|
- yield [("RDE", [user_frame, "phase"]),
|
|
|
- ("RDE", [user_frame, "IP"])
|
|
|
- ]
|
|
|
inst, = yield [("RD", [user_frame, "IP"])]
|
|
|
- while_inst, new_phase = \
|
|
|
- yield [("RD", [inst, "while"]),
|
|
|
+ while_inst, = yield [("RD", [inst, "while"])]
|
|
|
+ old_evalstack_link, old_phase_link, evalstack_roots = \
|
|
|
+ yield [("RDE", [user_frame, "evalstack"]),
|
|
|
+ ("RDE", [user_frame, "phase"]),
|
|
|
+ ("RRD", [while_inst, "inst"]),
|
|
|
+ ]
|
|
|
+
|
|
|
+ if len(evalstack_roots) == 1:
|
|
|
+ evalstack_root = evalstack_roots[0]
|
|
|
+ else:
|
|
|
+ raise Exception("Could not process continue statement!")
|
|
|
+
|
|
|
+ prev_evalstack_roots, old_evalstack_phase_link = \
|
|
|
+ yield [("RRD", [evalstack_root, "prev"]),
|
|
|
+ ("RDE", [evalstack_root, "phase"]),
|
|
|
+ ]
|
|
|
+
|
|
|
+ if len(prev_evalstack_roots) == 1:
|
|
|
+ prev_evalstack_root = prev_evalstack_roots[0]
|
|
|
+ else:
|
|
|
+ raise Exception("Could not process continue statement!")
|
|
|
+
|
|
|
+ new_evalstack_root, new_phase_while, new_phase_inst, prev_evalstack_root_link = \
|
|
|
+ yield [("CN", []),
|
|
|
+ ("CNV", ["init"]),
|
|
|
("CNV", ["finish"]),
|
|
|
+ ("RDE", [prev_evalstack_root, "prev"]),
|
|
|
]
|
|
|
- _, _, _, _ = yield [("CD", [user_frame, "phase", new_phase]),
|
|
|
- ("CD", [user_frame, "IP", while_inst]),
|
|
|
- ("DE", [phase_link]),
|
|
|
- ("DE", [ip_link]),
|
|
|
+
|
|
|
+ _, _, _, _, _, _, _, _ = \
|
|
|
+ yield [("CD", [user_frame, "evalstack", new_evalstack_root]),
|
|
|
+ ("CD", [new_evalstack_root, "prev", evalstack_root]),
|
|
|
+ ("CD", [user_frame, "phase", new_phase_inst]),
|
|
|
+ ("CD", [evalstack_root, "phase", new_phase_while]),
|
|
|
+ ("DE", [old_evalstack_link]),
|
|
|
+ ("DE", [prev_evalstack_root_link]),
|
|
|
+ ("DE", [old_phase_link]),
|
|
|
+ ("DE", [old_evalstack_phase_link]),
|
|
|
]
|
|
|
|
|
|
- def continue_init(self, user_root):
|
|
|
+ def break_init(self, user_root):
|
|
|
user_frame, = yield [("RD", [user_root, "frame"])]
|
|
|
- ip_link, inst = yield [("RDE", [user_frame, "IP"]),
|
|
|
- ("RD", [user_frame, "IP"]),
|
|
|
- ]
|
|
|
+ inst, = yield [("RD", [user_frame, "IP"])]
|
|
|
while_inst, = yield [("RD", [inst, "while"])]
|
|
|
- _, _ = yield [("CD", [user_frame, "IP", while_inst]),
|
|
|
- ("DE", [ip_link]),
|
|
|
+ old_evalstack_link, old_phase_link, evalstack_roots = \
|
|
|
+ yield [("RDE", [user_frame, "evalstack"]),
|
|
|
+ ("RDE", [user_frame, "phase"]),
|
|
|
+ ("RRD", [while_inst, "inst"]),
|
|
|
+ ]
|
|
|
+
|
|
|
+ if len(evalstack_roots) == 1:
|
|
|
+ evalstack_root = evalstack_roots[0]
|
|
|
+ else:
|
|
|
+ raise Exception("Could not process break statement!")
|
|
|
+
|
|
|
+ prev_evalstack_roots, old_evalstack_phase_link = \
|
|
|
+ yield [("RRD", [evalstack_root, "prev"]),
|
|
|
+ ("RDE", [evalstack_root, "phase"]),
|
|
|
+ ]
|
|
|
+
|
|
|
+ if len(prev_evalstack_roots) == 1:
|
|
|
+ prev_evalstack_root = prev_evalstack_roots[0]
|
|
|
+ else:
|
|
|
+ raise Exception("Could not process break statement!")
|
|
|
+
|
|
|
+ new_evalstack_root, new_phase_while, new_phase_inst, prev_evalstack_root_link = \
|
|
|
+ yield [("CN", []),
|
|
|
+ ("CNV", ["finish"]),
|
|
|
+ ("CNV", ["finish"]),
|
|
|
+ ("RDE", [prev_evalstack_root, "prev"]),
|
|
|
+ ]
|
|
|
+
|
|
|
+ _, _, _, _, _, _, _, _ = \
|
|
|
+ yield [("CD", [user_frame, "evalstack", new_evalstack_root]),
|
|
|
+ ("CD", [new_evalstack_root, "prev", evalstack_root]),
|
|
|
+ ("CD", [user_frame, "phase", new_phase_inst]),
|
|
|
+ ("CD", [evalstack_root, "phase", new_phase_while]),
|
|
|
+ ("DE", [old_evalstack_link]),
|
|
|
+ ("DE", [prev_evalstack_root_link]),
|
|
|
+ ("DE", [old_phase_link]),
|
|
|
+ ("DE", [old_evalstack_phase_link]),
|
|
|
]
|
|
|
|
|
|
def if_init(self, user_root):
|