Ignore:
Timestamp:
Dec 2, 2010, 10:15:58 AM (9 years ago)
Author:
mulligan
Message:

Added \bot to all absd cases in execute_1 to get rid of as many open goals as possible. Moving to vectors instead of lists to get rid of rest.

File:
1 edited

Legend:

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

    r357 r358  
    112112                let s ≝ set_8051_sfr s SFR_DPL bl in
    113113                  set_8051_sfr s SFR_DPH bu
    114               | _ ⇒ λother: False. ?
     114              | _ ⇒ λother: False.
    115115              ] (subaddressing_modein … addr)
    116116       | DEC addr ⇒
     
    158158            | CARRY ⇒ λcarry: True. set_arg_1 s CARRY false
    159159            | BIT_ADDR b ⇒ λbit_addr: True. set_arg_1 s (BIT_ADDR b) false
    160             | _ ⇒ λother: False. ?
     160            | _ ⇒ λother: False.
    161161            ] (subaddressing_modein … addr)
    162162        | CPL addr ⇒
     
    210210                let s ≝ set_8051_sfr s SFR_SP new_sp in
    211211                  write_at_stack_pointer s d
    212               | _ ⇒ λother: False. ?
     212              | _ ⇒ λother: False.
    213213              ] (subaddressing_modein … addr)
    214214        | POP addr ⇒
     
    257257                  else
    258258                    s
    259                 | _ ⇒ λother: False. ?
     259                | _ ⇒ λother: False.
    260260                ] (subaddressing_modein … addr)
    261261            | JNC addr ⇒
     
    267267                  else
    268268                    s
    269                 | _ ⇒ λother: False. ?
     269                | _ ⇒ λother: False.
    270270                ] (subaddressing_modein … addr)
    271271            | JB addr1 addr2 ⇒
     
    277277                  else
    278278                    s
    279                 | _ ⇒ λother: False. ?
     279                | _ ⇒ λother: False.
    280280                ] (subaddressing_modein … addr2)
    281281            | JNB addr1 addr2 ⇒
     
    287287                  else
    288288                    s
    289                 | _ ⇒ λother: False. ?
     289                | _ ⇒ λother: False.
    290290                ] (subaddressing_modein … addr2)
    291291            | JBC addr1 addr2 ⇒
     
    298298                    else
    299299                      s
    300                 | _ ⇒ λother: False. ?
     300                | _ ⇒ λother: False.
    301301                ] (subaddressing_modein … addr2)
    302302            | JZ addr ⇒
     
    308308                    else
    309309                      s
    310                 | _ ⇒ λother: False. ?
     310                | _ ⇒ λother: False.
    311311                ] (subaddressing_modein … addr)
    312312            | JNZ addr ⇒
     
    318318                    else
    319319                      s
    320                 | _ ⇒ λother: False. ?
     320                | _ ⇒ λother: False.
    321321                ] (subaddressing_modein … addr)
    322322            | CJNE addr1 addr2 ⇒
     
    345345                            (set_flags s new_cy (Nothing ?) (get_ov_flag s))
    346346                    ]
    347                 | _ ⇒ λother: False. ?
     347                | _ ⇒ λother: False.
    348348                ] (subaddressing_modein … addr2)
    349349            | DJNZ addr1 addr2 ⇒
     
    357357                      else
    358358                        s
    359                 | _ ⇒ λother: False. ?
     359                | _ ⇒ λother: False.
    360360                ] (subaddressing_modein … addr2)
    361361            ]
     
    370370            [ ADDR16 a ⇒ λaddr16: True.
    371371                set_program_counter s a
    372             | _ ⇒ λother: False. ?
     372            | _ ⇒ λother: False.
    373373            ] (subaddressing_modein … addr)
    374374        | SJMP addr ⇒
     
    377377                let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) (sign_extension r) in
    378378                  set_program_counter s new_pc
    379             | _ ⇒ λother: False. ?
     379            | _ ⇒ λother: False.
    380380            ] (subaddressing_modein … addr)
    381381        | AJMP addr ⇒
     
    389389              let 〈carry, new_pc〉 ≝ half_add ? (program_counter s) new_addr in
    390390                set_program_counter s new_pc
    391             | _ ⇒ λother: False. ?
     391            | _ ⇒ λother: False.
    392392            ] (subaddressing_modein … addr)
    393393        | MOVC addr1 addr2 ⇒
     
    408408              let result ≝ lookup ? ? new_addr (code_memory s) (zero ?) in
    409409                set_8051_sfr s SFR_ACC_A result
    410             | _ ⇒ λother: False. ?
     410            | _ ⇒ λother: False.
    411411            ] (subaddressing_modein … addr2)
    412412        | MOVX addr ⇒
     
    464464              let s ≝ write_at_stack_pointer s pc_bu in
    465465                set_program_counter s a
    466             | _ ⇒ λother: False. ?
     466            | _ ⇒ λother: False.
    467467            ] (subaddressing_modein … addr)
    468468        | ACALL addr ⇒
     
    480480              let new_addr ≝ (fiv @@ thr) @@ pc_bl in
    481481                set_program_counter s new_addr
    482             | _ ⇒ λother: False. ?
     482            | _ ⇒ λother: False.
    483483            ] (subaddressing_modein … addr)
    484484        | NOP ⇒ s
Note: See TracChangeset for help on using the changeset viewer.