Changeset 332


Ignore:
Timestamp:
Nov 29, 2010, 3:53:48 PM (9 years ago)
Author:
sacerdot
Message:

Code of fetch greatly simplified because of better behaviour of Matita.

Location:
Deliverables/D4.1/Matita
Files:
2 edited

Legend:

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

    r327 r332  
    55ndefinition next: BitVectorTrie Byte sixteen → Word → Word × Byte ≝
    66 λpmem,pc.
    7   let 〈x,res〉 ≝ half_add ? pc (bitvector_of_nat sixteen (S Z)) in
     7  let 〈x,res〉 ≝ half_add pc (bitvector_of_nat sixteen (S Z)) in
    88   〈res, lookup … pc pmem (zero eight)〉.
    99
     
    1818      let 〈b,v〉≝  head … v in if b then
    1919       let 〈b,v〉≝  head … v in if b then
    20         〈〈MOV … (Left ?? (Left ?? (Left ?? (Left ?? (Right ?? 〈(REGISTER v : [[?;?]]),(ACC_A : [[?;?;?]])〉))))), pc〉, one〉
    21        else
    22         let 〈b,v〉≝  head … v in if b then
    23          let 〈b,v〉≝  head … v in if b then
    24           〈〈MOV … (Left ?? (Left ?? (Left ?? (Left ?? (Right ?? 〈(INDIRECT (from_singl … v) : [[?;?]]),(ACC_A : [[?;?;?]])〉))))), pc〉, one〉
    25          else
    26           let 〈b,v〉≝  head … v in if b then
    27            let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … (Left ?? (Left ?? (Left ?? (Right ?? 〈(DIRECT b1:[[?]]),(ACC_A:[[?;?;?;?;?]])〉)))), pc〉, one〉
     20        〈〈MOV … (Left … (Left … (Left … (Left … (Right … 〈REGISTER v,ACC_A〉))))), pc〉, one〉
     21       else
     22        let 〈b,v〉≝  head … v in if b then
     23         let 〈b,v〉≝  head … v in if b then
     24          〈〈MOV … (Left … (Left … (Left … (Left … (Right … 〈INDIRECT (from_singl … v),ACC_A〉))))), pc〉, one〉
     25         else
     26          let 〈b,v〉≝  head … v in if b then
     27           let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … (Left … (Left … (Left … (Right … 〈DIRECT b1,ACC_A〉)))), pc〉, one〉
    2828          else
    2929           〈〈CPL … ACC_A, pc〉, one〉
    3030        else
    3131         let 〈b,v〉≝  head … v in if b then
    32           〈〈MOVX … (Right ?? 〈(EXT_INDIRECT (from_singl … v):[[?;?]]),(ACC_A:[[?]])〉), pc〉, two〉
     32          〈〈MOVX … (Right … 〈EXT_INDIRECT (from_singl … v),ACC_A〉), pc〉, two〉
    3333         else
    3434          let 〈b,v〉≝  head … v in if b then
    3535           let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[false;false;false]]) @@ b1)), pc〉, two〉
    3636          else
    37            〈〈MOVX … (Right ?? 〈(EXT_INDIRECT_DPTR:[[?;?]]),(ACC_A:[[?]])〉), pc〉, two〉
    38       else
    39        let 〈b,v〉≝  head … v in if b then
    40         〈〈MOV ? (Left ?? (Left ?? (Left ?? (Left ?? (Left ?? 〈(ACC_A:[[?]]),(REGISTER v : [[?;?;?;?]])〉))))), pc〉, one〉
    41        else
    42         let 〈b,v〉≝  head … v in if b then
    43          let 〈b,v〉≝  head … v in if b then
    44           〈〈MOV … (Left ?? (Left ?? (Left ?? (Left ?? (Left ?? 〈(ACC_A : [[?]]),(INDIRECT (from_singl … v):[[?;?;?;?]])〉))))), pc〉, one〉
    45          else
    46           let 〈b,v〉≝  head … v in if b then
    47            let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … (Left ?? (Left ?? (Left ?? (Left ?? (Left ?? 〈(ACC_A:[[?]]),(DIRECT b1:[[?;?;?;?]])〉))))), pc〉, one〉
     37           〈〈MOVX … (Right … 〈EXT_INDIRECT_DPTR,ACC_A〉), pc〉, two〉
     38      else
     39       let 〈b,v〉≝  head … v in if b then
     40        〈〈MOV … (Left … (Left … (Left … (Left … (Left … 〈ACC_A,REGISTER v〉))))), pc〉, one〉
     41       else
     42        let 〈b,v〉≝  head … v in if b then
     43         let 〈b,v〉≝  head … v in if b then
     44          〈〈MOV … (Left … (Left … (Left … (Left … (Left … 〈ACC_A,INDIRECT (from_singl … v)〉))))), pc〉, one〉
     45         else
     46          let 〈b,v〉≝  head … v in if b then
     47           let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … (Left … (Left … (Left … (Left … (Left … 〈ACC_A,DIRECT b1〉))))), pc〉, one〉
    4848          else
    4949           〈〈CLR … ACC_A, pc〉, one〉
    5050        else
    5151         let 〈b,v〉≝  head … v in if b then
    52           〈〈MOVX … (Left ?? 〈(ACC_A:[[?]]),(EXT_INDIRECT (from_singl … v):[[?;?]])〉), pc〉, two〉
     52          〈〈MOVX … (Left … 〈ACC_A,EXT_INDIRECT (from_singl … v)〉), pc〉, two〉
    5353         else
    5454          let 〈b,v〉≝  head … v in if b then
    5555           let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[false;false;false]]) @@ b1)), pc〉, two〉
    5656          else
    57            〈〈MOVX … (Left ?? 〈(ACC_A:[[?]]),(EXT_INDIRECT_DPTR:[[?;?]])〉), pc〉, two〉
     57           〈〈MOVX … (Left … 〈ACC_A,EXT_INDIRECT_DPTR〉), pc〉, two〉
    5858     else
    5959      let 〈b,v〉≝  head … v in if b then
    6060       let 〈b,v〉≝  head … v in if b then
    61         let 〈pc,b1〉≝ next pmem pc in 〈〈Jump … (DJNZ [[relative]] (REGISTER v) (RELATIVE b1)), pc〉, two〉
     61        let 〈pc,b1〉≝ next pmem pc in 〈〈Jump [[relative]] (DJNZ … (REGISTER v) (RELATIVE b1)), pc〉, two〉
    6262       else
    6363        let 〈b,v〉≝  head … v in if b then
     
    6666         else
    6767          let 〈b,v〉≝  head … v in if b then
    68            let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈Jump … (DJNZ [[relative]] (DIRECT b1) (RELATIVE b2)), pc〉, two〉
     68           let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈Jump [[relative]] (DJNZ … (DIRECT b1) (RELATIVE b2)), pc〉, two〉
    6969          else
    7070           〈〈DA … ACC_A, pc〉, one〉
     
    107107      let 〈b,v〉≝  head … v in if b then
    108108       let 〈b,v〉≝  head … v in if b then
    109         let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈Jump … (CJNE …  (Right ?? 〈(REGISTER v:[[?;?]]),(DATA b1:[[?]])〉) (RELATIVE b2:[[?]])), pc〉, two〉
    110        else
    111         let 〈b,v〉≝  head … v in if b then
    112          let 〈b,v〉≝  head … v in if b then
    113           let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈Jump … (CJNE … (Right ?? 〈(INDIRECT (from_singl … v):[[?;?]]),(DATA b1:[[?]])〉) (RELATIVE b2:[[?]])), pc〉, two〉
    114          else
    115           let 〈b,v〉≝  head … v in if b then
    116            let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈Jump … (CJNE …  (Left ?? 〈(ACC_A:[[?]]),(DIRECT b1:[[?;?]])〉) (RELATIVE b2:[[?]])), pc〉, two〉
    117           else
    118            let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈Jump … (CJNE … (Left ?? 〈(ACC_A:[[?]]),(DATA b1:[[?;?]])〉) (RELATIVE b2:[[?]])), pc〉, two〉
     109        let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈Jump [[relative]] (CJNE …  (Right … 〈REGISTER v,DATA b1〉) (RELATIVE b2)), pc〉, two〉
     110       else
     111        let 〈b,v〉≝  head … v in if b then
     112         let 〈b,v〉≝  head … v in if b then
     113          let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈Jump [[relative]] (CJNE … (Right … 〈INDIRECT (from_singl … v),DATA b1〉) (RELATIVE b2)), pc〉, two〉
     114         else
     115          let 〈b,v〉≝  head … v in if b then
     116           let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈Jump [[relative]] (CJNE …  (Left … 〈ACC_A,DIRECT b1〉) (RELATIVE b2)), pc〉, two〉
     117          else
     118           let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈Jump [[relative]] (CJNE … (Left … 〈ACC_A,DATA b1〉) (RELATIVE b2)), pc〉, two〉
    119119        else
    120120         let 〈b,v〉≝  head … v in if b then
     
    127127           let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[false;true;false]]) @@ b1)), pc〉, two〉
    128128          else
    129            let 〈pc,b1〉≝ next pmem pc in 〈〈ANL … (Right ?? 〈(CARRY:[[?]]),(N_BIT_ADDR b1:[[?;?]])〉), pc〉, two〉
    130       else
    131        let 〈b,v〉≝  head … v in if b then
    132         let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … (Left ?? (Left ?? (Left ?? (Left ?? (Right ?? 〈(REGISTER v:[[?;?]]),(DIRECT b1:[[?;?;?]])〉))))), pc〉, two〉
    133        else
    134         let 〈b,v〉≝  head … v in if b then
    135          let 〈b,v〉≝  head … v in if b then
    136           let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … (Left ?? (Left ?? (Left ?? (Left ?? (Right ?? 〈(INDIRECT (from_singl … v):[[?;?]]),(DIRECT b1:[[?;?;?]])〉))))), pc〉, two〉
     129           let 〈pc,b1〉≝ next pmem pc in 〈〈ANL … (Right … 〈CARRY,N_BIT_ADDR b1〉), pc〉, two〉
     130      else
     131       let 〈b,v〉≝  head … v in if b then
     132        let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … (Left … (Left … (Left … (Left … (Right … 〈REGISTER v,DIRECT b1〉))))), pc〉, two〉
     133       else
     134        let 〈b,v〉≝  head … v in if b then
     135         let 〈b,v〉≝  head … v in if b then
     136          let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … (Left … (Left … (Left … (Left … (Right … 〈INDIRECT (from_singl … v),DIRECT b1〉))))), pc〉, two〉
    137137         else
    138138          〈〈MUL … ACC_A ACC_B, pc〉, four〉
     
    142142           〈〈INC … DPTR, pc〉, two〉
    143143          else
    144            let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … (Left ?? (Right ?? 〈(CARRY:[[?]]),(BIT_ADDR b1:[[?]])〉)), pc〉, one〉
     144           let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … (Left … (Right … 〈CARRY,BIT_ADDR b1〉)), pc〉, one〉
    145145         else
    146146          let 〈b,v〉≝  head … v in if b then
    147147           let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[false;true;false]]) @@ b1)), pc〉, two〉
    148148          else
    149            let 〈pc,b1〉≝ next pmem pc in 〈〈ORL … (Right ?? 〈(CARRY:[[?]]),(N_BIT_ADDR b1:[[?;?]])〉), pc〉, two〉
     149           let 〈pc,b1〉≝ next pmem pc in 〈〈ORL … (Right … 〈CARRY,N_BIT_ADDR b1〉), pc〉, two〉
    150150     else
    151151      let 〈b,v〉≝  head … v in if b then
     
    166166           〈〈MOVC … ACC_A (ACC_DPTR), pc〉, two〉
    167167          else
    168            let 〈pc,b1〉≝ next pmem pc in 〈〈MOV ? (Right ?? 〈(BIT_ADDR b1:[[?]]),(CARRY:[[?]])〉), pc〉, two〉
     168           let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … (Right … 〈BIT_ADDR b1,CARRY〉), pc〉, two〉
    169169         else
    170170          let 〈b,v〉≝  head … v in if b then
    171171           let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[false;true;true]]) @@ b1)), pc〉, two〉
    172172          else
    173            let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈MOV … (Left ?? (Left ?? (Right ?? 〈(DPTR:[[?]]),(DATA16 (b1 @@ b2):[[?]])〉))), pc〉, two〉
    174       else
    175        let 〈b,v〉≝  head … v in if b then
    176         let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … (Left ?? (Left ?? (Left ?? (Right ?? 〈(DIRECT b1:[[?]]),(REGISTER v:[[?;?;?;?;?]])〉)))), pc〉, two〉
    177        else
    178         let 〈b,v〉≝  head … v in if b then
    179          let 〈b,v〉≝  head … v in if b then
    180           let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … (Left ?? (Left ?? (Left ?? (Right ?? 〈(DIRECT b1:[[?]]),(INDIRECT (from_singl … v):[[?;?;?;?;?]])〉)))), pc〉, two〉
    181          else
    182           let 〈b,v〉≝  head … v in if b then
    183            let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈MOV … (Left ?? (Left ?? (Left ?? (Right ?? 〈(DIRECT b1:[[?]]),(DIRECT b2:[[?;?;?;?;?]])〉)))), pc〉, two〉
     173           let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈MOV … (Left … (Left … (Right … 〈DPTR,DATA16 (b1 @@ b2)〉))), pc〉, two〉
     174      else
     175       let 〈b,v〉≝  head … v in if b then
     176        let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … (Left … (Left … (Left … (Right … 〈DIRECT b1,REGISTER v〉)))), pc〉, two〉
     177       else
     178        let 〈b,v〉≝  head … v in if b then
     179         let 〈b,v〉≝  head … v in if b then
     180          let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … (Left … (Left … (Left … (Right … 〈DIRECT b1,INDIRECT (from_singl … v)〉)))), pc〉, two〉
     181         else
     182          let 〈b,v〉≝  head … v in if b then
     183           let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈MOV … (Left … (Left … (Left … (Right … 〈DIRECT b1,DIRECT b2〉)))), pc〉, two〉
    184184          else
    185185           〈〈DIV … ACC_A ACC_B, pc〉, four〉
     
    189189           〈〈MOVC … ACC_A (ACC_PC), pc〉, two〉
    190190          else
    191            let 〈pc,b1〉≝ next pmem pc in 〈〈ANL … (Right ?? 〈(CARRY:[[?]]),(BIT_ADDR b1:[[?;?]])〉), pc〉, two〉
     191           let 〈pc,b1〉≝ next pmem pc in 〈〈ANL … (Right … 〈CARRY,BIT_ADDR b1〉), pc〉, two〉
    192192         else
    193193          let 〈b,v〉≝  head … v in if b then
     
    200200      let 〈b,v〉≝  head … v in if b then
    201201       let 〈b,v〉≝  head … v in if b then
    202         let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … (Left ?? (Left ?? (Left ?? (Left ?? (Right ?? 〈(REGISTER v:[[?;?]]),(DATA b1:[[?;?;?]])〉))))), pc〉, one〉
    203        else
    204         let 〈b,v〉≝  head … v in if b then
    205          let 〈b,v〉≝  head … v in if b then
    206           let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … (Left ?? (Left ?? (Left ?? (Left ?? (Right ?? 〈(INDIRECT (from_singl … v):[[?;?]]),(DATA b1:[[?;?;?]])〉))))), pc〉, one〉
    207          else
    208           let 〈b,v〉≝  head … v in if b then
    209            let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈MOV … (Left ?? (Left ?? (Left ?? (Right ?? 〈(DIRECT b1:[[?]]),(DATA b2:[[?;?;?;?;?]])〉)))), pc〉, three〉
    210           else
    211            let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … (Left ?? (Left ?? (Left ?? (Left ?? (Left ?? 〈(ACC_A:[[?]]),(DATA b1:[[?;?;?;?]])〉))))), pc〉, one〉
     202        let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … (Left … (Left … (Left … (Left … (Right … 〈REGISTER v,DATA b1〉))))), pc〉, one〉
     203       else
     204        let 〈b,v〉≝  head … v in if b then
     205         let 〈b,v〉≝  head … v in if b then
     206          let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … (Left … (Left … (Left … (Left … (Right … 〈INDIRECT (from_singl … v),DATA b1〉))))), pc〉, one〉
     207         else
     208          let 〈b,v〉≝  head … v in if b then
     209           let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈MOV … (Left … (Left … (Left … (Right … 〈DIRECT b1,DATA b2〉)))), pc〉, three〉
     210          else
     211           let 〈pc,b1〉≝ next pmem pc in 〈〈MOV … (Left … (Left … (Left … (Left … (Left … 〈ACC_A,DATA b1〉))))), pc〉, one〉
    212212        else
    213213         let 〈b,v〉≝  head … v in if b then
     
    215215           〈〈JMP … INDIRECT_DPTR, pc〉, two〉
    216216          else
    217            let 〈pc,b1〉≝ next pmem pc in 〈〈ORL … (Right ?? 〈(CARRY:[[?]]),(BIT_ADDR b1:[[?;?]])〉), pc〉, two〉
     217           let 〈pc,b1〉≝ next pmem pc in 〈〈ORL … (Right … 〈CARRY,BIT_ADDR b1〉), pc〉, two〉
    218218         else
    219219          let 〈b,v〉≝  head … v in if b then
    220220           let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[true;false;false]]) @@ b1)), pc〉, two〉
    221221          else
    222            let 〈pc,b1〉≝ next pmem pc in 〈〈Jump … (JNZ [[relative]] (RELATIVE b1)), pc〉, two〉
    223       else
    224        let 〈b,v〉≝  head … v in if b then
    225         〈〈XRL … (Left ?? 〈(ACC_A:[[?]]),(REGISTER v:[[?;?;?;?]])〉), pc〉, one〉
    226        else
    227         let 〈b,v〉≝  head … v in if b then
    228          let 〈b,v〉≝  head … v in if b then
    229           〈〈XRL … (Left ?? 〈(ACC_A:[[?]]),(INDIRECT (from_singl … v):[[?;?;?;?]])〉), pc〉, one〉
    230          else
    231           let 〈b,v〉≝  head … v in if b then
    232            let 〈pc,b1〉≝ next pmem pc in 〈〈XRL … (Left ?? 〈(ACC_A:[[?]]),(DIRECT b1:[[?;?;?;?]])〉), pc〉, one〉
    233           else
    234            let 〈pc,b1〉≝ next pmem pc in 〈〈XRL … (Left ?? 〈(ACC_A:[[?]]),(DATA b1:[[?;?;?;?]])〉), pc〉, one〉
    235         else
    236          let 〈b,v〉≝  head … v in if b then
    237           let 〈b,v〉≝  head … v in if b then
    238            let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈XRL … (Right ?? 〈(DIRECT b1:[[?]]),(DATA b2:[[?;?]])〉), pc〉, two〉
    239           else
    240            let 〈pc,b1〉≝ next pmem pc in 〈〈XRL … (Right ?? 〈(DIRECT b1:[[?]]),(ACC_A:[[?;?]])〉), pc〉, one〉
     222           let 〈pc,b1〉≝ next pmem pc in 〈〈Jump [[relative]] (JNZ … (RELATIVE b1)), pc〉, two〉
     223      else
     224       let 〈b,v〉≝  head … v in if b then
     225        〈〈XRL … (Left … 〈ACC_A,REGISTER v〉), pc〉, one〉
     226       else
     227        let 〈b,v〉≝  head … v in if b then
     228         let 〈b,v〉≝  head … v in if b then
     229          〈〈XRL … (Left … 〈ACC_A,INDIRECT (from_singl … v)〉), pc〉, one〉
     230         else
     231          let 〈b,v〉≝  head … v in if b then
     232           let 〈pc,b1〉≝ next pmem pc in 〈〈XRL … (Left … 〈ACC_A,DIRECT b1〉), pc〉, one〉
     233          else
     234           let 〈pc,b1〉≝ next pmem pc in 〈〈XRL … (Left … 〈ACC_A,DATA b1〉), pc〉, one〉
     235        else
     236         let 〈b,v〉≝  head … v in if b then
     237          let 〈b,v〉≝  head … v in if b then
     238           let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈XRL … (Right … 〈DIRECT b1,DATA b2〉), pc〉, two〉
     239          else
     240           let 〈pc,b1〉≝ next pmem pc in 〈〈XRL … (Right … 〈DIRECT b1,ACC_A〉), pc〉, one〉
    241241         else
    242242          let 〈b,v〉≝  head … v in if b then
    243243           let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[true;false;false]]) @@ b1)), pc〉, two〉
    244244          else
    245            let 〈pc,b1〉≝ next pmem pc in 〈〈Jump … (JZ [[relative]] (RELATIVE b1)), pc〉, two〉
     245           let 〈pc,b1〉≝ next pmem pc in 〈〈Jump [[relative]] (JZ … (RELATIVE b1)), pc〉, two〉
    246246     else
    247247      let 〈b,v〉≝  head … v in if b then
    248248       let 〈b,v〉≝  head … v in if b then
    249         〈〈ANL … (Left ?? (Left ?? 〈(ACC_A:[[?]]),(REGISTER v:[[?;?;?;?]])〉)), pc〉, one〉
    250        else
    251         let 〈b,v〉≝  head … v in if b then
    252          let 〈b,v〉≝  head … v in if b then
    253           〈〈ANL … (Left ?? (Left ?? 〈(ACC_A:[[?]]),(INDIRECT (from_singl … v):[[?;?;?;?]])〉)), pc〉, one〉
    254          else
    255           let 〈b,v〉≝  head … v in if b then
    256            let 〈pc,b1〉≝ next pmem pc in 〈〈ANL … (Left ?? (Left ?? 〈(ACC_A:[[?]]),(DIRECT b1:[[?;?;?;?]])〉)), pc〉, one〉
    257           else
    258            let 〈pc,b1〉≝ next pmem pc in 〈〈ANL … (Left ?? (Left ?? 〈(ACC_A:[[?]]),(DATA b1:[[?;?;?;?]])〉)), pc〉, one〉
    259         else
    260          let 〈b,v〉≝  head … v in if b then
    261           let 〈b,v〉≝  head … v in if b then
    262            let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈ANL … (Left ?? (Right ?? 〈(DIRECT b1:[[?]]),(DATA b2:[[?;?]])〉)), pc〉, two〉
    263           else
    264            let 〈pc,b1〉≝ next pmem pc in 〈〈ANL … (Left ?? (Right ?? 〈(DIRECT b1:[[?]]),(ACC_A:[[?;?]])〉)), pc〉, one〉
     249        〈〈ANL … (Left … (Left … 〈ACC_A,REGISTER v〉)), pc〉, one〉
     250       else
     251        let 〈b,v〉≝  head … v in if b then
     252         let 〈b,v〉≝  head … v in if b then
     253          〈〈ANL … (Left … (Left … 〈ACC_A,INDIRECT (from_singl … v)〉)), pc〉, one〉
     254         else
     255          let 〈b,v〉≝  head … v in if b then
     256           let 〈pc,b1〉≝ next pmem pc in 〈〈ANL … (Left … (Left … 〈ACC_A,DIRECT b1〉)), pc〉, one〉
     257          else
     258           let 〈pc,b1〉≝ next pmem pc in 〈〈ANL … (Left … (Left … 〈ACC_A,DATA b1〉)), pc〉, one〉
     259        else
     260         let 〈b,v〉≝  head … v in if b then
     261          let 〈b,v〉≝  head … v in if b then
     262           let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈ANL … (Left … (Right … 〈DIRECT b1,DATA b2〉)), pc〉, two〉
     263          else
     264           let 〈pc,b1〉≝ next pmem pc in 〈〈ANL … (Left … (Right … 〈DIRECT b1,ACC_A〉)), pc〉, one〉
    265265         else
    266266          let 〈b,v〉≝  head … v in if b then
    267267           let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[true;false;true]]) @@ b1)), pc〉, two〉
    268268          else
    269            let 〈pc,b1〉≝ next pmem pc in 〈〈Jump … (JNC [[relative]] (RELATIVE b1)), pc〉, two〉
    270       else
    271        let 〈b,v〉≝  head … v in if b then
    272         〈〈ORL … (Left ?? (Left ?? 〈(ACC_A:[[?]]),(REGISTER v:[[?;?;?;?]])〉)), pc〉, one〉
    273        else
    274         let 〈b,v〉≝  head … v in if b then
    275          let 〈b,v〉≝  head … v in if b then
    276           〈〈ORL … (Left ?? (Left ?? 〈(ACC_A:[[?]]),(INDIRECT (from_singl … v):[[?;?;?;?]])〉)), pc〉, one〉
    277          else
    278           let 〈b,v〉≝  head … v in if b then
    279            let 〈pc,b1〉≝ next pmem pc in 〈〈ORL … (Left ?? (Left ?? 〈(ACC_A:[[?]]),(DIRECT b1:[[?;?;?;?]])〉)), pc〉, one〉
    280           else
    281            let 〈pc,b1〉≝ next pmem pc in 〈〈ORL … (Left ?? (Left ?? 〈(ACC_A:[[?]]),(DATA b1:[[?;?;?;?]])〉)), pc〉, one〉
    282         else
    283          let 〈b,v〉≝  head … v in if b then
    284           let 〈b,v〉≝  head … v in if b then
    285            let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈ORL … (Left ?? (Right ?? 〈(DIRECT b1:[[?]]),(DATA b2:[[?;?]])〉)), pc〉, two〉
    286           else
    287            let 〈pc,b1〉≝ next pmem pc in 〈〈ORL … (Left ?? (Right ?? 〈(DIRECT b1:[[?]]),(ACC_A:[[?;?]])〉)), pc〉, one〉
     269           let 〈pc,b1〉≝ next pmem pc in 〈〈Jump [[relative]] (JNC … (RELATIVE b1)), pc〉, two〉
     270      else
     271       let 〈b,v〉≝  head … v in if b then
     272        〈〈ORL … (Left … (Left … 〈ACC_A,REGISTER v〉)), pc〉, one〉
     273       else
     274        let 〈b,v〉≝  head … v in if b then
     275         let 〈b,v〉≝  head … v in if b then
     276          〈〈ORL … (Left … (Left … 〈ACC_A,INDIRECT (from_singl … v)〉)), pc〉, one〉
     277         else
     278          let 〈b,v〉≝  head … v in if b then
     279           let 〈pc,b1〉≝ next pmem pc in 〈〈ORL … (Left … (Left … 〈ACC_A,DIRECT b1〉)), pc〉, one〉
     280          else
     281           let 〈pc,b1〉≝ next pmem pc in 〈〈ORL … (Left … (Left … 〈ACC_A,DATA b1〉)), pc〉, one〉
     282        else
     283         let 〈b,v〉≝  head … v in if b then
     284          let 〈b,v〉≝  head … v in if b then
     285           let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈ORL … (Left … (Right … 〈DIRECT b1,DATA b2〉)), pc〉, two〉
     286          else
     287           let 〈pc,b1〉≝ next pmem pc in 〈〈ORL … (Left … (Right … 〈DIRECT b1,ACC_A〉)), pc〉, one〉
    288288         else
    289289          let 〈b,v〉≝  head … v in if b then
    290290           let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[true;false;true]]) @@ b1)), pc〉, two〉
    291291          else
    292            let 〈pc,b1〉≝ next pmem pc in 〈〈Jump … (JC [[relative]] (RELATIVE b1)), pc〉, two〉
     292           let 〈pc,b1〉≝ next pmem pc in 〈〈Jump [[relative]] (JC … (RELATIVE b1)), pc〉, two〉
    293293    else
    294294     let 〈b,v〉≝  head … v in if b then
     
    315315           let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[true;true;false]]) @@ b1)), pc〉, two〉
    316316          else
    317            let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈Jump … (JNB [[relative]] (BIT_ADDR b1) (RELATIVE b2)), pc〉, two〉
     317           let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈Jump [[relative]] (JNB … (BIT_ADDR b1) (RELATIVE b2)), pc〉, two〉
    318318      else
    319319       let 〈b,v〉≝  head … v in if b then
     
    338338           let 〈pc,b1〉≝ next pmem pc in 〈〈ACALL … (ADDR11 (([[true;true;false]]) @@ b1)), pc〉, two〉
    339339          else
    340            let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈Jump … (JB [[relative]] (BIT_ADDR b1) (RELATIVE b2)), pc〉, two〉
     340           let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈Jump [[relative]] (JB … (BIT_ADDR b1) (RELATIVE b2)), pc〉, two〉
    341341     else
    342342      let 〈b,v〉≝  head … v in if b then
     
    362362           let 〈pc,b1〉≝ next pmem pc in 〈〈AJMP … (ADDR11 (([[true;true;true]]) @@ b1)), pc〉, two〉
    363363          else
    364            let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈Jump … (JBC [[relative]] (BIT_ADDR b1) (RELATIVE b2)), pc〉, two〉
     364           let 〈pc,b1〉≝ next pmem pc in let 〈pc,b2〉≝ next pmem pc in 〈〈Jump [[relative]] (JBC … (BIT_ADDR b1) (RELATIVE b2)), pc〉, two〉
    365365      else
    366366       let 〈b,v〉≝  head … v in if b then
  • Deliverables/D4.1/Matita/depends

    r329 r332  
     1Arithmetic.ma BitVector.ma Bool.ma Connectives.ma Exponential.ma List.ma Nat.ma Plogic/equality.ma Universes.ma
     2Status.ma ASM.ma Arithmetic.ma BitVectorTrie.ma
    13Exponential.ma Connectives.ma Nat.ma Plogic/equality.ma
    2 Status.ma ASM.ma Arithmetic.ma BitVectorTrie.ma
    3 Arithmetic.ma BitVector.ma Bool.ma Connectives.ma Exponential.ma List.ma Nat.ma Plogic/equality.ma Universes.ma
    44BitVectorTrie.ma BitVector.ma Bool.ma Maybe.ma
    55Cartesian.ma Universes.ma
    6 Universes.ma
    76Maybe.ma Bool.ma Plogic/equality.ma Universes.ma
    87Either.ma Bool.ma Maybe.ma Universes.ma
     8Universes.ma
    99ASM.ma BitVectorTrie.ma Either.ma String.ma
     10Vector.ma Cartesian.ma List.ma Maybe.ma Nat.ma Plogic/equality.ma Util.ma
    1011Fetch.ma ASM.ma Arithmetic.ma BitVectorTrie.ma
    1112Char.ma Universes.ma
    12 Vector.ma Cartesian.ma List.ma Maybe.ma Nat.ma Plogic/equality.ma Util.ma
    1313Connectives.ma Plogic/equality.ma
    1414Bool.ma Universes.ma
    1515Assembly.ma ASM.ma
    1616List.ma Bool.ma Maybe.ma Nat.ma Plogic/equality.ma Universes.ma Util.ma
     17Util.ma Nat.ma
    1718Interpret.ma Arithmetic.ma Cartesian.ma Fetch.ma List.ma Status.ma
    18 Util.ma Nat.ma
     19BitVector.ma Bool.ma List.ma Nat.ma Universes.ma Vector.ma
    1920Compare.ma Universes.ma
    20 BitVector.ma Bool.ma List.ma Nat.ma Universes.ma Vector.ma
    2121String.ma Char.ma List.ma
    2222Plogic/equality.ma Universes.ma
Note: See TracChangeset for help on using the changeset viewer.