Changeset 326


Ignore:
Timestamp:
Nov 29, 2010, 1:08:14 AM (9 years ago)
Author:
sacerdot
Message:

Almost compiling.

File:
1 edited

Legend:

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

    r325 r326  
    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 (U2 (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 (U3 (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 (U2 (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 (U2 (EXT_IND_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 (U1 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 (U1 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 (U1 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 (U1 ACC_A EXT_IND_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
     
    7474           〈〈SETB … CARRY, pc〉, one〉
    7575          else
    76            let 〈pc,b1〉≝ next pmem pc in 〈〈SETB … (BIT_ADDR (from_singl … b1)), pc〉, one〉
     76           let 〈pc,b1〉≝ next pmem pc in 〈〈SETB … (BIT_ADDR b1), pc〉, one〉
    7777         else
    7878          let 〈b,v〉≝  head … v in if b then
     
    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 …  (U2 (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 … (U2 (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 …  (U1 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 … (U1 ACC_A (DATA b1)) (RELATIVE b2)), pc〉, two〉*)
     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〉
    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 (U3 C (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 (U2 (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 (U2 (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 (U5 C (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 (U3 C (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 (U6 (BIT_ADDR b1) C), 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 (U4 DPTR (DATA16 (mk_word 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 (U3 (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 (U3 (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 (U3 (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 (U3 C (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 (U2 (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 (U2 (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 (U3 (DIRECT b1) (DATA b2)), pc〉, three〉*)
    210           else
    211            let 〈pc,b1〉≝ next pmem pc in ?(*〈〈MOV (U1 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 (U3 C (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
     
    223223      else
    224224       let 〈b,v〉≝  head … v in if b then
    225         ?(*〈〈XRL(U1 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(U1 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(U1 ACC_A (DIRECT b1)), pc〉, one〉*)
    233           else
    234            let 〈pc,b1〉≝ next pmem pc in ?(*〈〈XRL(U1 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(U2 (DIRECT b1) (DATA b2)), pc〉, two〉*)
    239           else
    240            let 〈pc,b1〉≝ next pmem pc in ?(*〈〈XRL(U2 (DIRECT b1) ACC_A), pc〉, one〉*)
     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
     
    247247      let 〈b,v〉≝  head … v in if b then
    248248       let 〈b,v〉≝  head … v in if b then
    249         ?(*〈〈ANL (U1 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 (U1 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 (U1 ACC_A (DIRECT b1)), pc〉, one〉*)
    257           else
    258            let 〈pc,b1〉≝ next pmem pc in ?(*〈〈ANL (U1 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 (U2 (DIRECT b1) (DATA b2)), pc〉, two〉*)
    263           else
    264            let 〈pc,b1〉≝ next pmem pc in ?(*〈〈ANL (U2 (DIRECT b1) 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
     
    270270      else
    271271       let 〈b,v〉≝  head … v in if b then
    272         ?(*〈〈ORL (U1 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 (U1 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 (U1 ACC_A (DIRECT b1)), pc〉, one〉*)
    280           else
    281            let 〈pc,b1〉≝ next pmem pc in ?(*〈〈ORL (U1 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 (U2 (DIRECT b1) (DATA b2)), pc〉, two〉*)
    286           else
    287            let 〈pc,b1〉≝ next pmem pc in ?(*〈〈ORL (U2 (DIRECT b1) ACC_A), pc〉, one〉*)
     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
Note: See TracChangeset for help on using the changeset viewer.