Changeset 437


Ignore:
Timestamp:
Dec 15, 2010, 11:35:37 PM (9 years ago)
Author:
sacerdot
Message:
  1. new function assembly_unlabelled_program
  2. the new function is now used in DoTest?.ma
Location:
Deliverables/D4.1
Files:
4 edited

Legend:

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

    r431 r437  
    431431nqed.
    432432
    433 ndefinition assembly0: assembly_program → Maybe (List Byte × (BitVectorTrie String sixteen)) ≝
     433ndefinition assembly: assembly_program → Maybe (List Byte × (BitVectorTrie String sixteen)) ≝
    434434  λp.
    435435    let 〈preamble, instr_list〉 ≝ p in
     
    518518nqed.
    519519
    520 ndefinition 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 …〉).
     520ndefinition assembly_unlabelled_program: List instruction → Maybe (List Byte × (BitVectorTrie String sixteen)) ≝
     521 λp.Just ? (〈fold_right ?? (λi,l. assembly1 i @ l) [ ] p, Stub …〉).
  • Deliverables/D4.1/Matita/DoTest.ma

    r431 r437  
    55ndefinition steps ≝ one_hundred_and_twenty_eight.
    66
    7 ndefinition testmem ≝ assembly 〈[ ], test〉.
     7ndefinition testmem ≝ assembly_unlabelled_program test.
    88ndefinition teststatus ≝
    99 match testmem with
  • Deliverables/D4.1/Matita/Test.ma

    r431 r437  
    11include "ASM.ma".
    22
    3 ndefinition 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 … )].
     3ndefinition 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 … ].
    150150 @.
    151151nqed.
  • Deliverables/D4.1/ToMatita.ml

    r430 r437  
    1010  let rec aux status pc =
    1111    let instr, pc', cost = ASMInterpret.fetch status.ASMInterpret.code_memory pc in
    12       print_string $ ("Instruction (" ^ pp_matita_instruction instr ^ ")");
     12      print_string $ pp_matita_instruction instr;
    1313      if int_of_vect pc' <= 200 then (* DPM: hardcoded on a case-by-case basis *)
    1414       begin
     
    1919    aux status status.ASMInterpret.pc
    2020in
    21  print_string "include \"ASM.ma\".\n\nndefinition test: List labelled_instruction ≝\n [";
     21 print_string "include \"ASM.ma\".\n\nndefinition test: List instruction ≝\n [";
    2222 mem_pretty_print status;
    2323 print_endline "].\n @.\nnqed."
Note: See TracChangeset for help on using the changeset viewer.