Changeset 425


Ignore:
Timestamp:
Dec 14, 2010, 4:55:01 PM (9 years ago)
Author:
mulligan
Message:

Removed Map.ma as no longer needed. Everything else seems to build apart from DoTest?.ma (are we including this in final distr?)

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

Legend:

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

    r421 r425  
    11include "ASM.ma".
    22include "BitVectorTrie.ma".
     3include "Arithmetic.ma".
     4include "Fetch.ma".
     5include "Status.ma".
    36
    47ndefinition assembly1 ≝
     
    400403             [ ([[false;true;true;false;false;false;true;true]]); b1; b2 ]
    401404          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]].
    402 
    403 include "Arithmetic.ma".
    404 include "Fetch.ma".
    405 include "Status.ma".
    406 
     405         
    407406ndefinition assembly_jump: (jump String) → (String → [[relative]]) → instruction ≝
    408407  λj: jump String.
     
    418417      | CJNE jmp jmp' ⇒ Jump ? (CJNE ? jmp (addr_of jmp'))
    419418      | DJNZ jmp jmp' ⇒ Jump ? (DJNZ ? jmp (addr_of jmp'))
    420       ]. (*
    421         match jmp return λx. bool_to_Prop (is_in … [[ register; direct ]] x) → ? with
    422           [ DIRECT d ⇒ λdptr: True. Jump ? (DJNZ ? jmp (addr_of jmp'))
    423           | REGISTER r ⇒ λregister:True. Jump ? (DJNZ ? jmp (addr_of jmp'))
    424           | _ ⇒ λother: False. ⊥
    425           ] (subaddressing_modein … jmp)
    426419      ].
    427   nassumption;
    428 nqed. *)
    429420
    430421ndefinition address_of: BitVectorTrie (BitVector eight) eight → String → addressing_mode ≝
Note: See TracChangeset for help on using the changeset viewer.