Changeset 774 for src/RTLabs

Timestamp:

Apr 26, 2011, 4:51:44 PM (10 years ago)

Author:

campbell

Message:

Separate out the different forms of addition and subtraction in the frontend ops.

File:

• src/RTLabs/semantics.ma (modified) (2 diffs)

src/RTLabs/semantics.ma

@@ -74 +74 @@
 [ Aindexed i ⇒ λargs.
     do v ← reg_retrieve (locals f) ((args !!! 0) ?);
-    opt_to_res … (ev_add v (Vint i))
+    opt_to_res … (ev_addp v (Vint i))
 | Aindexed2 ⇒ λargs.
     do v1 ← reg_retrieve (locals f) ((args !!! 0) ?);
     do v2 ← reg_retrieve (locals f) ((args !!! 1) ?);
-    opt_to_res … (ev_add v1 v2)
+    opt_to_res … (ev_addp v1 v2)
 | Aglobal id off ⇒ λargs.
     do loc ← opt_to_res … (find_symbol ?? ge id);
@@ -85 +85 @@
     do loc ← opt_to_res … (find_symbol ?? ge id);
     do v ← reg_retrieve (locals f) ((args !!! 0) ?);
-    opt_to_res … (ev_add (Vptr Any loc ? zero_offset) v)
+    opt_to_res … (ev_addp (Vptr Any loc ? zero_offset) v)
 | Ainstack off ⇒ λargs.
     OK ? (Vptr Any (sp f) ? (shift_offset zero_offset off))