Ignore:
Timestamp:
Jan 20, 2011, 6:10:07 PM (9 years ago)
Author:
mulligan
Message:

Moved over to standard library.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D4.1/Matita/Test.ma

    r437 r465  
    11include "ASM.ma".
    22
    3 ndefinition test: List instruction ≝
     3ndefinition test: list instruction ≝
    44 [LJMP … (ADDR16 [[false;false;false;false;false;false;false;false;false;false;false;false;true;false;false;false]]);
    55  LCALL … (ADDR16 [[false;false;false;false;false;false;false;false;false;true;true;false;false;true;false;false]]);
    66  SJMP … (RELATIVE [[true;true;true;true;true;true;true;false]]);
    7   MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;false;false;false;false;false;false;true]]),(DATA [[false;false;false;false;false;true;true;true]])〉))));
     7  MOV … (inl … (inl … (inl … (inr … 〈(DIRECT [[true;false;false;false;false;false;false;true]]),(DATA [[false;false;false;false;false;true;true;true]])〉))));
    88  LCALL … (ADDR16 [[false;false;false;false;false;false;false;false;false;true;true;false;true;true;true;false]]);
    9   MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[true;false;false;false;false;false;true;false]])〉)))));
     9  MOV … (inl … (inl … (inl … (inl … (inl … 〈(ACC_A),(DIRECT [[true;false;false;false;false;false;true;false]])〉)))));
    1010  Jump … (JZ … (RELATIVE [[false;false;false;false;false;false;true;true]]));
    1111  LJMP … (ADDR16 [[false;false;false;false;false;false;false;false;false;false;false;false;false;false;true;true]]);
    12   MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[false;false;true]]),(DATA [[false;false;false;false;false;false;false;false]])〉)))));
    13   MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(REGISTER [[false;false;true]])〉)))));
    14   ORL … (Left … (Left … 〈(ACC_A),(DATA [[false;false;false;false;false;false;false;false]])〉));
     12  MOV … (inl … (inl … (inl … (inl … (inr … 〈(REGISTER [[false;false;true]]),(DATA [[false;false;false;false;false;false;false;false]])〉)))));
     13  MOV … (inl … (inl … (inl … (inl … (inl … 〈(ACC_A),(REGISTER [[false;false;true]])〉)))));
     14  ORL … (inl … (inl … 〈(ACC_A),(DATA [[false;false;false;false;false;false;false;false]])〉));
    1515  Jump … (JZ … (RELATIVE [[false;false;false;true;true;false;true;true]]));
    16   MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[false;true;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉)))));
    17   MOV … (Left … (Left … (Right … 〈(DPTR),(DATA16 [[false;false;false;false;false;false;false;false;false;true;true;true;false;false;true;false]])〉)));
    18   MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[false;false;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉)))));
    19   MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;false;true;false;false;false;false;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉))));
     16  MOV … (inl … (inl … (inl … (inl … (inr … 〈(REGISTER [[false;true;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉)))));
     17  MOV … (inl … (inl … (inr … 〈(DPTR),(DATA16 [[false;false;false;false;false;false;false;false;false;true;true;true;false;false;true;false]])〉)));
     18  MOV … (inl … (inl … (inl … (inl … (inr … 〈(REGISTER [[false;false;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉)))));
     19  MOV … (inl … (inl … (inl … (inr … 〈(DIRECT [[true;false;true;false;false;false;false;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉))));
    2020  CLR … (ACC_A);
    2121  MOVC … (ACC_A) (ACC_DPTR);
    22   MOVX … (Right … 〈(EXT_INDIRECT false),(ACC_A)〉);
     22  MOVX … (inr … 〈(EXT_INDIRECT false),(ACC_A)〉);
    2323  INC … (DPTR);
    2424  INC … (REGISTER [[false;false;false]]);
    25   Jump … (CJNE … (Right … 〈(REGISTER [[false;false;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉) (RELATIVE [[false;false;false;false;false;false;true;false]]));
     25  Jump … (CJNE … (inr … 〈(REGISTER [[false;false;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉) (RELATIVE [[false;false;false;false;false;false;true;false]]));
    2626  INC … (DIRECT [[true;false;true;false;false;false;false;false]]);
    2727  Jump … (DJNZ … (REGISTER [[false;false;true]]) (RELATIVE [[true;true;true;true;false;true;false;false]]));
    2828  Jump … (DJNZ … (REGISTER [[false;true;false]]) (RELATIVE [[true;true;true;true;false;false;true;false]]));
    29   MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;false;true;false;false;false;false;false]]),(DATA [[true;true;true;true;true;true;true;true]])〉))));
     29  MOV … (inl … (inl … (inl … (inr … 〈(DIRECT [[true;false;true;false;false;false;false;false]]),(DATA [[true;true;true;true;true;true;true;true]])〉))));
    3030  CLR … (ACC_A);
    31   MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[false;false;false]]),(DATA [[true;true;true;true;true;true;true;true]])〉)))));
    32   MOV … (Left … (Left … (Left … (Left … (Right … 〈(INDIRECT false),(ACC_A)〉)))));
     31  MOV … (inl … (inl … (inl … (inl … (inr … 〈(REGISTER [[false;false;false]]),(DATA [[true;true;true;true;true;true;true;true]])〉)))));
     32  MOV … (inl … (inl … (inl … (inl … (inr … 〈(INDIRECT false),(ACC_A)〉)))));
    3333  Jump … (DJNZ … (REGISTER [[false;false;false]]) (RELATIVE [[true;true;true;true;true;true;false;true]]));
    34   MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[false;false;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉)))));
    35   MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(REGISTER [[false;false;false]])〉)))));
    36   ORL … (Left … (Left … 〈(ACC_A),(DATA [[false;false;false;false;false;false;false;false]])〉));
     34  MOV … (inl … (inl … (inl … (inl … (inr … 〈(REGISTER [[false;false;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉)))));
     35  MOV … (inl … (inl … (inl … (inl … (inl … 〈(ACC_A),(REGISTER [[false;false;false]])〉)))));
     36  ORL … (inl … (inl … 〈(ACC_A),(DATA [[false;false;false;false;false;false;false;false]])〉));
    3737  Jump … (JZ … (RELATIVE [[false;false;false;false;true;false;true;false]]));
    38   MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[false;false;true]]),(DATA [[false;false;false;false;false;false;false;false]])〉)))));
    39   MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;false;true;false;false;false;false;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉))));
     38  MOV … (inl … (inl … (inl … (inl … (inr … 〈(REGISTER [[false;false;true]]),(DATA [[false;false;false;false;false;false;false;false]])〉)))));
     39  MOV … (inl … (inl … (inl … (inr … 〈(DIRECT [[true;false;true;false;false;false;false;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉))));
    4040  CLR … (ACC_A);
    41   MOVX … (Right … 〈(EXT_INDIRECT true),(ACC_A)〉);
     41  MOVX … (inr … 〈(EXT_INDIRECT true),(ACC_A)〉);
    4242  INC … (REGISTER [[false;false;true]]);
    4343  Jump … (DJNZ … (REGISTER [[false;false;false]]) (RELATIVE [[true;true;true;true;true;true;false;false]]));
    44   MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[false;false;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉)))));
    45   MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(REGISTER [[false;false;false]])〉)))));
    46   ORL … (Left … (Left … 〈(ACC_A),(DATA [[false;false;false;false;false;false;false;false]])〉));
     44  MOV … (inl … (inl … (inl … (inl … (inr … 〈(REGISTER [[false;false;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉)))));
     45  MOV … (inl … (inl … (inl … (inl … (inl … 〈(ACC_A),(REGISTER [[false;false;false]])〉)))));
     46  ORL … (inl … (inl … 〈(ACC_A),(DATA [[false;false;false;false;false;false;false;false]])〉));
    4747  Jump … (JZ … (RELATIVE [[false;false;false;false;true;true;false;false]]));
    48   MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[false;false;true]]),(DATA [[false;false;false;false;false;false;false;false]])〉)))));
    49   MOV … (Left … (Left … (Right … 〈(DPTR),(DATA16 [[false;false;false;false;false;false;false;false;false;false;false;false;false;false;false;false]])〉)));
     48  MOV … (inl … (inl … (inl … (inl … (inr … 〈(REGISTER [[false;false;true]]),(DATA [[false;false;false;false;false;false;false;false]])〉)))));
     49  MOV … (inl … (inl … (inr … 〈(DPTR),(DATA16 [[false;false;false;false;false;false;false;false;false;false;false;false;false;false;false;false]])〉)));
    5050  CLR … (ACC_A);
    51   MOVX … (Right … 〈(EXT_INDIRECT_DPTR),(ACC_A)〉);
     51  MOVX … (inr … 〈(EXT_INDIRECT_DPTR),(ACC_A)〉);
    5252  INC … (DPTR);
    5353  Jump … (DJNZ … (REGISTER [[false;false;false]]) (RELATIVE [[true;true;true;true;true;true;false;false]]));
    5454  Jump … (DJNZ … (REGISTER [[false;false;true]]) (RELATIVE [[true;true;true;true;true;false;true;false]]));
    5555  LJMP … (ADDR16 [[false;false;false;false;false;false;false;false;false;false;false;false;false;false;true;true]]);
    56   MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[false;false;false]]),(DATA [[false;false;false;false;false;true;false;true]])〉)))));
    57   MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;false;true;false;true]]),(DATA [[false;false;false;false;true;true;true;true]])〉))));
     56  MOV … (inl … (inl … (inl … (inl … (inr … 〈(REGISTER [[false;false;false]]),(DATA [[false;false;false;false;false;true;false;true]])〉)))));
     57  MOV … (inl … (inl … (inl … (inr … 〈(DIRECT [[false;false;false;false;false;true;false;true]]),(DATA [[false;false;false;false;true;true;true;true]])〉))));
    5858  XCHD … (ACC_A) (INDIRECT false);
    59   MOV … (Left … (Left … (Right … 〈(DPTR),(DATA16 [[false;false;false;false;false;false;false;false;false;false;false;false;false;false;false;false]])〉)));
     59  MOV … (inl … (inl … (inr … 〈(DPTR),(DATA16 [[false;false;false;false;false;false;false;false;false;false;false;false;false;false;false;false]])〉)));
    6060  RET … ;
    61   MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;false;false;false;false;false;true;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉))));
     61  MOV … (inl … (inl … (inl … (inr … 〈(DIRECT [[true;false;false;false;false;false;true;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉))));
    6262  RET … ;
    6363  NOP … ;
Note: See TracChangeset for help on using the changeset viewer.