Changeset 418


Ignore:
Timestamp:
Dec 14, 2010, 12:08:59 PM (9 years ago)
Author:
mulligan
Message:

Fixed type error in Mov instruction implementation.

File:
1 edited

Legend:

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

    r414 r418  
    421421      ].
    422422
     423ndefinition address_of: BitVectorTrie ? ? → String → addressing_mode ≝
     424    λmap.
     425    λstring.
     426      let address ≝ lookup … (bitvector_of_string … string) map (zero ?) in
     427      let address_bv ≝ nat_of_bitvector ? address in
     428        if less_than_b address_bv two_hundred_and_fifty_six then
     429          RELATIVE address
     430        else
     431          ?.
     432      nelim not_implemented.
     433nqed.
     434
    423435ndefinition assembly: assembly_program → Maybe (List Byte × (BitVectorTrie ? sixteen)) ≝
    424436  λp.
     
    484496                    let pc_offset ≝ lookup ? ? (bitvector_of_string ? trgt) datalabels (zero ?) in
    485497                    let address ≝ DATA16 pc_offset in
    486                       assembly1 (MOV ? (Right ? ?(Right ? ? (Right ? ? (Right ? ? (Right ? ? 〈DPTR, address〉))))))
    487                   | Instruction instr ⇒ ?
    488                   | Jmp jmp ⇒
     498                      assembly1 (MOV ? (? ? ? ? 〈DPTR, address〉))
     499                  | Instruction instr ⇒ assembly1 instr
     500                  | Jmp jmp ⇒ 
    489501                    let pc_offset ≝ lookup ? ? (bitvector_of_string ? jmp) labels (zero ?) in
    490502                    let address ≝ ADDR16 pc_offset in
    491503                      assembly1 (LJMP ? address)
    492                   | WithLabel jmp ⇒ ?
     504                  | WithLabel jmp ⇒ ? (*
     505                    assembly1 (Jump ? (assembly_jump ? ? jmp (address_of labels))) *)
    493506                  ]
    494507            ) instr_list
Note: See TracChangeset for help on using the changeset viewer.