Changeset 431 for Deliverables


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
Location:
Deliverables/D4.1/Matita
Files:
5 edited

Legend:

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

    r425 r431  
    431431nqed.
    432432
    433 ndefinition assembly: assembly_program → Maybe (List Byte × (BitVectorTrie String sixteen)) ≝
     433ndefinition assembly0: assembly_program → Maybe (List Byte × (BitVectorTrie String sixteen)) ≝
    434434  λp.
    435435    let 〈preamble, instr_list〉 ≝ p in
     
    508508          ) in
    509509        Just (List ? × (BitVectorTrie ? ?)) 〈flat_list, costs〉.
    510   ##[##2,3,4,5,6: nnormalize; //;
     510  ##[##2,3,4,5,6: nnormalize; @;
    511511  ##| nwhd in ⊢ (? (? ? ? %));
    512512      ncases (less_than_b (nat_of_bitvector eight ?) two_hundred_and_fifty_six)
    513         [ nnormalize; //;
     513        [ nnormalize; @;
    514514      ##| nnormalize;
    515515          nelim not_implemented;
     
    518518nqed.
    519519
    520 (*
    521 ndefinition assembly: List instruction → List Byte ≝
    522  fold_right … (λi,l. assembly1 i @ l) [].
    523 *)
     520ndefinition assembly: assembly_program → Maybe (List Byte × (BitVectorTrie String sixteen)) ≝
     521 λp: assembly_program.
     522  Just ? (〈fold_right ?? (λi,l.
     523   match i with [ Instruction i ⇒ assembly1 i @ l | _ ⇒ l] ) [ ] (second ?? p), Stub …〉).
  • Deliverables/D4.1/Matita/DoTest.ma

    r403 r431  
    33include "Assembly.ma".
    44
    5 ndefinition testmem ≝ assembly test.
    6 ndefinition teststatus ≝ load testmem initialise_status.
    7 ndefinition testfinal ≝ execute four (*(four * two_hundred_and_fifty_six)*) teststatus.
     5ndefinition steps ≝ one_hundred_and_twenty_eight.
     6
     7ndefinition testmem ≝ assembly 〈[ ], test〉.
     8ndefinition teststatus ≝
     9 match testmem with
     10  [ Nothing ⇒ Nothing …
     11  | Just testmem ⇒ Just … (load (first … testmem) initialise_status)].
     12ndefinition testfinal ≝
     13 match teststatus with
     14  [ Nothing ⇒ Nothing …
     15  | Just teststatus ⇒ Just … (execute steps teststatus)].
    816
    917notation "'STATUS'" with precedence 90 for @{ 'status }.
     
    1624       first … (first … (fetch (code_memory s) (program_counter s))) :: execute_trace o (execute_1 s)
    1725    ].
     26
     27ndefinition testtrace ≝
     28 match teststatus with
     29  [ Nothing ⇒ Nothing …
     30  | Just teststatus ⇒ Just … (execute_trace steps teststatus)].
    1831
    1932interpretation "left" 'left x = (Left ?? x).
     
    129142interpretation "[[relative]]" 'hide = (VCons ?? relative (VEmpty ?)).
    130143
    131 nlemma xoo:
    132  execute_trace one_hundred_and_twenty_eight teststatus =
    133  execute_trace eight teststatus.
    134  nnormalize in ⊢ (??%?);
    135 (* nnormalize in ⊢ (???%);
     144nlemma do_test: testtrace = testtrace.
     145 nnormalize in ⊢ (??%?); (* STOP HERE TO SEE THE TRACE *)
     146 nnormalize;
    136147 @.
    137148nqed.
    138 
    139 nlemma xoo: program_counter testfinal = program_counter testfinal.
    140  nnormalize in ⊢ (??%?);
    141  nnormalize in ⊢ (???%);
    142  @.
    143 nqed.
    144 *)
  • Deliverables/D4.1/Matita/README

    r260 r431  
    1 To make this directory compile, replace the nlibrary directory of Matita with
    2 it.
     1To compile:
     2
     3 1) replace the nlibrary directory in the source code of Matita 0.5.9 with the
     4    current directory
     5 2) run
     6     matitadep.opt && matitac.opt
     7
     8
     9To run an Intel Hex file:
     10 1) use ToMatita.native to generate a Test.ma file from a Test.hex file
     11    (see the README in the O'Caml part of the deliverable)
     12 2) replace the Test.ma file in this directory with the generated one
     13 3) run matita.opt DoTest.ma to run the program. Stop execution at
     14    (* STOP HERE TO SEE THE TRACE *) to look at the instruction trace.
     15    You can change the number of steps in the trace by changing the "step"
     16    variable at the beginning of the file.
  • 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.
  • Deliverables/D4.1/Matita/depends

    r420 r431  
    99DoTest.ma Assembly.ma Interpret.ma Test.ma
    1010ASM.ma BitVector.ma Either.ma String.ma
    11 Map.ma Compare.ma Maybe.ma Universes.ma
    1211Fetch.ma ASM.ma Arithmetic.ma BitVectorTrie.ma
    1312Char.ma Universes.ma
Note: See TracChangeset for help on using the changeset viewer.