Changeset 2286 for src/ASM/I8051.ma


Ignore:
Timestamp:
Aug 2, 2012, 3:18:11 PM (8 years ago)
Author:
tranquil
Message:

Big update!

  • merge of all _paolo variants
  • reorganised some depends (in particular, Register and thus back-end laguages no longer have fake ASM dependency)
  • split I8051.ma spawning new BackEndOps?.ma

compiler.ma broken at the moment, but not by these changes as far as I can tell

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/I8051.ma

    r2275 r2286  
    33
    44include "ASM/String.ma".
    5 include "ASM/ASM.ma".
     5(*include "ASM/ASM.ma".*)
    66include "ASM/Arithmetic.ma". 
    77
     
    99definition ptr_size ≝ bitvector_of_nat 8 2.
    1010definition alignment ≝ None.
    11 
    12 (* dpm: Can these two inductive definitions be merged? In LIN, yes, but perhaps
    13         not further back in the translation chain.                            *)
    14 inductive OpAccs: Type[0] ≝
    15   Mul: OpAccs
    16 | DivuModu: OpAccs.
    17 
    18 inductive Op1: Type[0] ≝
    19   Cmpl: Op1
    20 | Inc: Op1
    21 | Rl: Op1. (* TODO: implement left rotation *)
    22 
    23 inductive Op2: Type[0] ≝
    24   Add: Op2
    25 | Addc: Op2
    26 | Sub: Op2
    27 | And: Op2
    28 | Or: Op2
    29 | Xor: Op2.
    3011
    3112(* dpm: maybe useless? *)
     
    170151   Register31; Register32; Register33; Register34; Register35;
    171152   Register36; Register37].
    172 
    173 definition register_address: Register → [[ acc_a; direct; registr ]] ≝
    174   λr: Register.
    175     match r with
    176     [ Register00 ⇒ REGISTER [[ false; false; false ]]
    177     | Register01 ⇒ REGISTER [[ false; false; true ]]
    178     | Register02 ⇒ REGISTER [[ false; true; false ]]
    179     | Register03 ⇒ REGISTER [[ false; true; true ]]
    180     | Register04 ⇒ REGISTER [[ true; false; false ]]
    181     | Register05 ⇒ REGISTER [[ true; false; true ]]
    182     | Register06 ⇒ REGISTER [[ true; true; false ]]
    183     | Register07 ⇒ REGISTER [[ true; true; true ]]
    184     | RegisterA ⇒ ACC_A
    185     | RegisterB ⇒ DIRECT (bitvector_of_nat 8 240)
    186     | RegisterDPL ⇒ DIRECT (bitvector_of_nat 8 82)
    187     | RegisterDPH ⇒ DIRECT (bitvector_of_nat 8 83)
    188     | _ ⇒ DIRECT (bitvector_of_nat 8 (nat_of_register r))
    189     ].
    190     [*: normalize
    191         @ I
    192     ]
    193 qed.
    194 
    195 record Eval: Type[0] ≝
    196 {
    197   opaccs: OpAccs → Byte → Byte → Byte × Byte;
    198   op1: Op1 → Byte → Byte;
    199   op2: Bit → Op2 → Byte → Byte → (Byte × Bit)
    200 }.
    201 
    202 axiom opaccs_implementation: OpAccs → Byte → Byte → Byte × Byte.
    203 axiom op1_implementation: Op1 → Byte → Byte.
    204 axiom op2_implementation: Bit → Op2 → Byte → Byte → (Byte × Bit).
    205 
    206 definition eval: Eval ≝
    207   mk_Eval opaccs_implementation
    208           op1_implementation
    209           op2_implementation.
Note: See TracChangeset for help on using the changeset viewer.