Changeset 296


Ignore:
Timestamp:
Nov 25, 2010, 10:17:33 PM (9 years ago)
Author:
sacerdot
Message:

...

File:
1 edited

Legend:

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

    r293 r296  
    157157              [ DIRECT b1 ⇒ λ_.
    158158                 [ ([[true; false; true; true; false; true; false; true]]); b1; b3 ]
    159               [ DATA b1 ⇒ λ_.
     159              | DATA b1 ⇒ λ_.
    160160                 [ ([[true; false; true; true; false; true; false; false]]); b1; b3 ]
    161161              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
     
    165165               [ DATA b2 ⇒ λ_. b2
    166166               | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2) in
    167              match addr2 return λx. bool_to_Prop (is_in ? [[direct;data]] x) → ? with
    168               [ DIRECT b1 ⇒ λ_.
    169                  [ ([[true; false; true; true; false; true; false; true]]); b1; b3 ]
    170               [ DATA b1 ⇒ λ_.
    171                  [ ([[true; false; true; true; false; true; false; false]]); b1; b3 ]
    172               | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr2)
    173 
    174           ]
    175       | _ ⇒ [ ]
    176       ]
     167
     168[ ] (*
     169             match addr1 return λx. bool_to_Prop (is_in ? [[register;indirect]] x) → ? with
     170              [ REGISTER r1 r2 r3 ⇒ λ_. [](*
     171                 [ ([[true; false; true; true; true; r1; r2; r3]]); b2; b3 ]*)
     172              | INDIRECT i1 ⇒ λ_. [] (*
     173                 [ ([[true; false; true; true; false; true; true; i1]]); b2; b3 ] *)
     174              | _ ⇒ λK.match K in False with [ ] ] (subaddressing_modein … addr1)*) ]]
    177175  | _ ⇒ [ ]].
    178 
    179176(*
    180   | `CJNE (`U2 (`REG(r1,r2,r3), `DATA b1), `REL b2) ->
    181     [mk_byte_from_bits ((true,false,true,true),(true,r1,r2,r3)); b1; b2]
    182   | `CJNE (`U2 (`INDIRECT i1, `DATA b1), `REL b2) ->
    183     [mk_byte_from_bits ((true,false,true,true),(false,true,true,i1)); b1; b2]
    184 
    185 
    186177  | `INC `A ->
    187178    [mk_byte_from_bits ((false,false,false,false),(false,true,false,false))]
Note: See TracChangeset for help on using the changeset viewer.