Ignore:
Timestamp:
Dec 15, 2010, 6:38:59 PM (9 years ago)
Author:
mulligan
Message:
  • README updated
  • Test and DoTest? fixed to work on assembly_program
  • assembly function for labelled programs avoided because of efficiency issues
File:
1 edited

Legend:

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

    r357 r431  
    11include "ASM.ma".
    22
    3 ndefinition test: List instruction ≝
    4  [LJMP … (ADDR16 [[false;false;false;false;false;false;false;false;false;false;false;false;true;false;false;false]]);
    5   LCALL … (ADDR16 [[false;false;false;false;false;false;false;false;false;true;true;false;false;true;false;false]]);
    6   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]])〉))));
    8   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]])〉)))));
    10   Jump … (JZ … (RELATIVE [[false;false;false;false;false;false;true;true]]));
    11   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]])〉));
    15   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]])〉))));
    20   CLR … (ACC_A);
    21   MOVC … (ACC_A) (ACC_DPTR);
    22   MOVX … (Right … 〈(EXT_INDIRECT false),(ACC_A)〉);
    23   INC … (DPTR);
    24   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]]));
    26   INC … (DIRECT [[true;false;true;false;false;false;false;false]]);
    27   Jump … (DJNZ … (REGISTER [[false;false;true]]) (RELATIVE [[true;true;true;true;false;true;false;false]]));
    28   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]])〉))));
    30   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)〉)))));
    33   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]])〉));
    37   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]])〉))));
    40   CLR … (ACC_A);
    41   MOVX … (Right … 〈(EXT_INDIRECT true),(ACC_A)〉);
    42   INC … (REGISTER [[false;false;true]]);
    43   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]])〉));
    47   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]])〉)));
    50   CLR … (ACC_A);
    51   MOVX … (Right … 〈(EXT_INDIRECT_DPTR),(ACC_A)〉);
    52   INC … (DPTR);
    53   Jump … (DJNZ … (REGISTER [[false;false;false]]) (RELATIVE [[true;true;true;true;true;true;false;false]]));
    54   Jump … (DJNZ … (REGISTER [[false;false;true]]) (RELATIVE [[true;true;true;true;true;false;true;false]]));
    55   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]])〉))));
    58   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]])〉)));
    60   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]])〉))));
    62   RET … ;
    63   NOP … ;
    64   NOP … ;
    65   NOP … ;
    66   NOP … ;
    67   NOP … ;
    68   NOP … ;
    69   NOP … ;
    70   NOP … ;
    71   NOP … ;
    72   NOP … ;
    73   NOP … ;
    74   NOP … ;
    75   NOP … ;
    76   NOP … ;
    77   NOP … ;
    78   NOP … ;
    79   NOP … ;
    80   NOP … ;
    81   NOP … ;
    82   NOP … ;
    83   NOP … ;
    84   NOP … ;
    85   NOP … ;
    86   NOP … ;
    87   NOP … ;
    88   NOP … ;
    89   NOP … ;
    90   NOP … ;
    91   NOP … ;
    92   NOP … ;
    93   NOP … ;
    94   NOP … ;
    95   NOP … ;
    96   NOP … ;
    97   NOP … ;
    98   NOP … ;
    99   NOP … ;
    100   NOP … ;
    101   NOP … ;
    102   NOP … ;
    103   NOP … ;
    104   NOP … ;
    105   NOP … ;
    106   NOP … ;
    107   NOP … ;
    108   NOP … ;
    109   NOP … ;
    110   NOP … ;
    111   NOP … ;
    112   NOP … ;
    113   NOP … ;
    114   NOP … ;
    115   NOP … ;
    116   NOP … ;
    117   NOP … ;
    118   NOP … ;
    119   NOP … ;
    120   NOP … ;
    121   NOP … ;
    122   NOP … ;
    123   NOP … ;
    124   NOP … ;
    125   NOP … ;
    126   NOP … ;
    127   NOP … ;
    128   NOP … ;
    129   NOP … ;
    130   NOP … ;
    131   NOP … ;
    132   NOP … ;
    133   NOP … ;
    134   NOP … ;
    135   NOP … ;
    136   NOP … ;
    137   NOP … ;
    138   NOP … ;
    139   NOP … ;
    140   NOP … ;
    141   NOP … ;
    142   NOP … ;
    143   NOP … ;
    144   NOP … ;
    145   NOP … ;
    146   NOP … ;
    147   NOP … ;
    148   NOP … ;
    149   NOP … ].
     3ndefinition test: List labelled_instruction ≝
     4 [Instruction (LJMP … (ADDR16 [[false;false;false;false;false;false;false;false;false;false;false;false;true;false;false;false]]));
     5  Instruction (LCALL … (ADDR16 [[false;false;false;false;false;false;false;false;false;true;true;false;false;true;false;false]]));
     6  Instruction (SJMP … (RELATIVE [[true;true;true;true;true;true;true;false]]));
     7  Instruction (MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;false;false;false;false;false;false;true]]),(DATA [[false;false;false;false;false;true;true;true]])〉)))));
     8  Instruction (LCALL … (ADDR16 [[false;false;false;false;false;false;false;false;false;true;true;false;true;true;true;false]]));
     9  Instruction (MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(DIRECT [[true;false;false;false;false;false;true;false]])〉))))));
     10  Instruction (Jump … (JZ … (RELATIVE [[false;false;false;false;false;false;true;true]])));
     11  Instruction (LJMP … (ADDR16 [[false;false;false;false;false;false;false;false;false;false;false;false;false;false;true;true]]));
     12  Instruction (MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[false;false;true]]),(DATA [[false;false;false;false;false;false;false;false]])〉))))));
     13  Instruction (MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(REGISTER [[false;false;true]])〉))))));
     14  Instruction (ORL … (Left … (Left … 〈(ACC_A),(DATA [[false;false;false;false;false;false;false;false]])〉)));
     15  Instruction (Jump … (JZ … (RELATIVE [[false;false;false;true;true;false;true;true]])));
     16  Instruction (MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[false;true;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉))))));
     17  Instruction (MOV … (Left … (Left … (Right … 〈(DPTR),(DATA16 [[false;false;false;false;false;false;false;false;false;true;true;true;false;false;true;false]])〉))));
     18  Instruction (MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[false;false;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉))))));
     19  Instruction (MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;false;true;false;false;false;false;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉)))));
     20  Instruction (CLR … (ACC_A));
     21  Instruction (MOVC … (ACC_A) (ACC_DPTR));
     22  Instruction (MOVX … (Right … 〈(EXT_INDIRECT false),(ACC_A)〉));
     23  Instruction (INC … (DPTR));
     24  Instruction (INC … (REGISTER [[false;false;false]]));
     25  Instruction (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]])));
     26  Instruction (INC … (DIRECT [[true;false;true;false;false;false;false;false]]));
     27  Instruction (Jump … (DJNZ … (REGISTER [[false;false;true]]) (RELATIVE [[true;true;true;true;false;true;false;false]])));
     28  Instruction (Jump … (DJNZ … (REGISTER [[false;true;false]]) (RELATIVE [[true;true;true;true;false;false;true;false]])));
     29  Instruction (MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;false;true;false;false;false;false;false]]),(DATA [[true;true;true;true;true;true;true;true]])〉)))));
     30  Instruction (CLR … (ACC_A));
     31  Instruction (MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[false;false;false]]),(DATA [[true;true;true;true;true;true;true;true]])〉))))));
     32  Instruction (MOV … (Left … (Left … (Left … (Left … (Right … 〈(INDIRECT false),(ACC_A)〉))))));
     33  Instruction (Jump … (DJNZ … (REGISTER [[false;false;false]]) (RELATIVE [[true;true;true;true;true;true;false;true]])));
     34  Instruction (MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[false;false;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉))))));
     35  Instruction (MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(REGISTER [[false;false;false]])〉))))));
     36  Instruction (ORL … (Left … (Left … 〈(ACC_A),(DATA [[false;false;false;false;false;false;false;false]])〉)));
     37  Instruction (Jump … (JZ … (RELATIVE [[false;false;false;false;true;false;true;false]])));
     38  Instruction (MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[false;false;true]]),(DATA [[false;false;false;false;false;false;false;false]])〉))))));
     39  Instruction (MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;false;true;false;false;false;false;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉)))));
     40  Instruction (CLR … (ACC_A));
     41  Instruction (MOVX … (Right … 〈(EXT_INDIRECT true),(ACC_A)〉));
     42  Instruction (INC … (REGISTER [[false;false;true]]));
     43  Instruction (Jump … (DJNZ … (REGISTER [[false;false;false]]) (RELATIVE [[true;true;true;true;true;true;false;false]])));
     44  Instruction (MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[false;false;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉))))));
     45  Instruction (MOV … (Left … (Left … (Left … (Left … (Left … 〈(ACC_A),(REGISTER [[false;false;false]])〉))))));
     46  Instruction (ORL … (Left … (Left … 〈(ACC_A),(DATA [[false;false;false;false;false;false;false;false]])〉)));
     47  Instruction (Jump … (JZ … (RELATIVE [[false;false;false;false;true;true;false;false]])));
     48  Instruction (MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[false;false;true]]),(DATA [[false;false;false;false;false;false;false;false]])〉))))));
     49  Instruction (MOV … (Left … (Left … (Right … 〈(DPTR),(DATA16 [[false;false;false;false;false;false;false;false;false;false;false;false;false;false;false;false]])〉))));
     50  Instruction (CLR … (ACC_A));
     51  Instruction (MOVX … (Right … 〈(EXT_INDIRECT_DPTR),(ACC_A)〉));
     52  Instruction (INC … (DPTR));
     53  Instruction (Jump … (DJNZ … (REGISTER [[false;false;false]]) (RELATIVE [[true;true;true;true;true;true;false;false]])));
     54  Instruction (Jump … (DJNZ … (REGISTER [[false;false;true]]) (RELATIVE [[true;true;true;true;true;false;true;false]])));
     55  Instruction (LJMP … (ADDR16 [[false;false;false;false;false;false;false;false;false;false;false;false;false;false;true;true]]));
     56  Instruction (MOV … (Left … (Left … (Left … (Left … (Right … 〈(REGISTER [[false;false;false]]),(DATA [[false;false;false;false;false;true;false;true]])〉))))));
     57  Instruction (MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[false;false;false;false;false;true;false;true]]),(DATA [[false;false;false;false;true;true;true;true]])〉)))));
     58  Instruction (XCHD … (ACC_A) (INDIRECT false));
     59  Instruction (MOV … (Left … (Left … (Right … 〈(DPTR),(DATA16 [[false;false;false;false;false;false;false;false;false;false;false;false;false;false;false;false]])〉))));
     60  Instruction (RET … );
     61  Instruction (MOV … (Left … (Left … (Left … (Right … 〈(DIRECT [[true;false;false;false;false;false;true;false]]),(DATA [[false;false;false;false;false;false;false;false]])〉)))));
     62  Instruction (RET … );
     63  Instruction (NOP … );
     64  Instruction (NOP … );
     65  Instruction (NOP … );
     66  Instruction (NOP … );
     67  Instruction (NOP … );
     68  Instruction (NOP … );
     69  Instruction (NOP … );
     70  Instruction (NOP … );
     71  Instruction (NOP … );
     72  Instruction (NOP … );
     73  Instruction (NOP … );
     74  Instruction (NOP … );
     75  Instruction (NOP … );
     76  Instruction (NOP … );
     77  Instruction (NOP … );
     78  Instruction (NOP … );
     79  Instruction (NOP … );
     80  Instruction (NOP … );
     81  Instruction (NOP … );
     82  Instruction (NOP … );
     83  Instruction (NOP … );
     84  Instruction (NOP … );
     85  Instruction (NOP … );
     86  Instruction (NOP … );
     87  Instruction (NOP … );
     88  Instruction (NOP … );
     89  Instruction (NOP … );
     90  Instruction (NOP … );
     91  Instruction (NOP … );
     92  Instruction (NOP … );
     93  Instruction (NOP … );
     94  Instruction (NOP … );
     95  Instruction (NOP … );
     96  Instruction (NOP … );
     97  Instruction (NOP … );
     98  Instruction (NOP … );
     99  Instruction (NOP … );
     100  Instruction (NOP … );
     101  Instruction (NOP … );
     102  Instruction (NOP … );
     103  Instruction (NOP … );
     104  Instruction (NOP … );
     105  Instruction (NOP … );
     106  Instruction (NOP … );
     107  Instruction (NOP … );
     108  Instruction (NOP … );
     109  Instruction (NOP … );
     110  Instruction (NOP … );
     111  Instruction (NOP … );
     112  Instruction (NOP … );
     113  Instruction (NOP … );
     114  Instruction (NOP … );
     115  Instruction (NOP … );
     116  Instruction (NOP … );
     117  Instruction (NOP … );
     118  Instruction (NOP … );
     119  Instruction (NOP … );
     120  Instruction (NOP … );
     121  Instruction (NOP … );
     122  Instruction (NOP … );
     123  Instruction (NOP … );
     124  Instruction (NOP … );
     125  Instruction (NOP … );
     126  Instruction (NOP … );
     127  Instruction (NOP … );
     128  Instruction (NOP … );
     129  Instruction (NOP … );
     130  Instruction (NOP … );
     131  Instruction (NOP … );
     132  Instruction (NOP … );
     133  Instruction (NOP … );
     134  Instruction (NOP … );
     135  Instruction (NOP … );
     136  Instruction (NOP … );
     137  Instruction (NOP … );
     138  Instruction (NOP … );
     139  Instruction (NOP … );
     140  Instruction (NOP … );
     141  Instruction (NOP … );
     142  Instruction (NOP … );
     143  Instruction (NOP … );
     144  Instruction (NOP … );
     145  Instruction (NOP … );
     146  Instruction (NOP … );
     147  Instruction (NOP … );
     148  Instruction (NOP … );
     149  Instruction (NOP … )].
    150150 @.
    151151nqed.
Note: See TracChangeset for help on using the changeset viewer.