Changeset 316 for Deliverables/D4.1/Matita/ASM.ma

Timestamp:

Nov 26, 2010, 5:38:04 PM (10 years ago)

Author:

sacerdot

Message:

REGISTER now takes a BitVector? 3

File:

• Deliverables/D4.1/Matita/ASM.ma (modified) (2 diffs)

Deliverables/D4.1/Matita/ASM.ma

@@ -7 +7 @@
 | INDIRECT: Bit → addressing_mode
 | EXT_INDIRECT: Bit → addressing_mode
-| REGISTER: Bit → Bit → Bit → addressing_mode
+| REGISTER: BitVector (S (S (S Z))) → addressing_mode
 | ACC_A: addressing_mode
 | ACC_B: addressing_mode
@@ -51 +51 @@
    | indirect ⇒ match A with [ INDIRECT _ ⇒ true | _ ⇒ false ]
    | ext_indirect ⇒ match A with [ EXT_INDIRECT _ ⇒ true | _ ⇒ false ]
-   | register ⇒ match A with [ REGISTER _ _ _ ⇒ true | _ ⇒ false ]
+   | register ⇒ match A with [ REGISTER _ ⇒ true | _ ⇒ false ]
    | acc_a ⇒ match A with [ ACC_A ⇒ true | _ ⇒ false ]
    | acc_b ⇒ match A with [ ACC_B ⇒ true | _ ⇒ false ]