Changeset 284


Ignore:
Timestamp:
Nov 24, 2010, 11:15:13 PM (9 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

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

    r283 r284  
    5454          | N_BIT_ADDR b1 ⇒ λ_. [ ([[true;false;true;true;false;false;false;false]]) ; b1 ]
    5555          | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)]
    56  
    57   | _ ⇒ [ ([[false;false;false;false;false;false;false;false]]) ]].
    58 
    59 
     56  (*
    6057  | `CJNE (`U1 (`A, `DIRECT b1), `REL b2) ->
    6158    [mk_byte_from_bits ((true,false,true,true),(false,true,false,true)); b1; b2]
     
    6663  | `CJNE (`U2 (`INDIRECT i1, `DATA b1), `REL b2) ->
    6764    [mk_byte_from_bits ((true,false,true,true),(false,true,true,i1)); b1; b2]
    68   | `CLR `A ->
    69     [mk_byte_from_bits ((true,true,true,false),(false,true,false,false))]
    70   | `CLR `C ->
    71     [mk_byte_from_bits ((true,true,false,false),(false,false,true,true))]
    72   | `CLR (`BIT b1) ->
    73     [mk_byte_from_bits ((true,true,false,false),(false,false,true,false)); b1]
    74   | `CPL `A ->
    75     [mk_byte_from_bits ((true,true,true,true),(false,true,false,false))]
    76   | `CPL `C ->
    77     [mk_byte_from_bits ((true,false,true,true),(false,false,true,true))]
    78   | `CPL (`BIT b1) ->
    79     [mk_byte_from_bits ((true,false,true,true),(false,false,true,false)); b1]
    80   | `DA `A ->
    81     [mk_byte_from_bits ((true,true,false,true),(false,true,false,false))]
    82   | `DEC `A ->
    83     [mk_byte_from_bits ((false,false,false,true),(false,true,false,false))]
    84   | `DEC (`REG(r1,r2,r3)) ->
    85     [mk_byte_from_bits ((false,false,false,true),(true,r1,r2,r3))]
    86   | `DEC (`DIRECT b1) ->
    87     [mk_byte_from_bits ((false,false,false,true),(false,true,false,true)); b1]
    88   | `DEC (`INDIRECT i1) ->
    89     [mk_byte_from_bits ((false,false,false,true),(false,true,true,i1))]
    90   | `DIV (`A, `B) ->
    91     [mk_byte_from_bits ((true,false,false,false),(false,true,false,false))]
     65  *)
     66  | CLR addr ⇒
     67     match addr return λx. bool_to_Prop (is_in ? [[acc_a;carry;bit_addr]] x) → ? with
     68      [ ACC_A ⇒ λ_.
     69         [ ([[true; true; true; false; false; true; false; false]]) ]
     70      | CARRY ⇒ λ_.
     71         [ ([[true; true; false; false; false; false; true; true]]) ]
     72      | BIT_ADDR b1 ⇒ λ_.
     73         [ ([[true; true; false; false; false; false; true; false]]) ; b1 ]
     74      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
     75  | CPL addr ⇒
     76     match addr return λx. bool_to_Prop (is_in ? [[acc_a;carry;bit_addr]] x) → ? with
     77      [ ACC_A ⇒ λ_.
     78         [ ([[true; true; true; true; false; true; false; false]]) ]
     79      | CARRY ⇒ λ_.
     80         [ ([[true; false; true; true; false; false; true; true]]) ]
     81      | BIT_ADDR b1 ⇒ λ_.
     82         [ ([[true; false; true; true; false; false; true; false]]) ; b1 ]
     83      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
     84  | DA addr ⇒
     85     [ ([[true; true; false; true; false; true; false; false]]) ]
     86  | DEC addr ⇒
     87     match addr return λx. bool_to_Prop (is_in ? [[acc_a;register;direct;indirect]] x) → ? with
     88      [ ACC_A ⇒ λ_.
     89         [ ([[false; false; false; true; false; true; false; false]]) ]
     90      | REGISTER r1 r2 r3 ⇒ λ_.
     91         [ ([[false; false; false; true; true; r1; r2; r3]]) ]
     92      | DIRECT b1 ⇒ λ_.
     93         [ ([[false; false; false; true; false; true; false; true]]); b1 ]
     94      | INDIRECT i1 ⇒ λ_.
     95         [ ([[false; false; false; true; false; true; true; i1]]) ]
     96      | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr)
     97  | DIV addr1 addr2 ⇒
     98     [ ([[true;false;false;false;false;true;false;false]]) ]
     99
     100  | _ ⇒ [ ]].
     101
     102(*
    92103  | `DJNZ (`REG(r1,r2,r3), `REL b1) ->
    93104    [mk_byte_from_bits ((true,true,false,true),(true,r1,r2,r3)); b1]
     
    361372 
    362373 ].
    363 
     374*)
Note: See TracChangeset for help on using the changeset viewer.