Changeset 757 for src/ASM/Status.ma


Ignore:
Timestamp:
Apr 18, 2011, 12:30:53 PM (10 years ago)
Author:
mulligan
Message:

Lots more fixing to get both front and backends using same conventions and types.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Status.ma

    r705 r757  
    755755      ] (subaddressing_modein … a).
    756756     
    757 definition get_arg_8: Status → bool → [[ direct ; indirect ; register ;
     757definition get_arg_8: Status → bool → [[ direct ; indirect ; registr ;
    758758                                          acc_a ; acc_b ; data ; acc_dptr ;
    759759                                          acc_pc ; ext_indirect ;
    760760                                          ext_indirect_dptr ]] → Byte ≝
    761761  λs, l, a.
    762     match a return λx. bool_to_Prop (is_in ? [[ direct ; indirect ; register ;
     762    match a return λx. bool_to_Prop (is_in ? [[ direct ; indirect ; registr ;
    763763                                                acc_a ; acc_b ; data ; acc_dptr ;
    764764                                                acc_pc ; ext_indirect ;
     
    820820qed.
    821821
    822 definition set_arg_8: Status → [[ direct ; indirect ; register ;
     822definition set_arg_8: Status → [[ direct ; indirect ; registr ;
    823823                                   acc_a ; acc_b ; ext_indirect ;
    824824                                   ext_indirect_dptr ]] → Byte → Status ≝
    825825  λs, a, v.
    826     match a return λx. bool_to_Prop (is_in ? [[ direct ; indirect ; register ;
     826    match a return λx. bool_to_Prop (is_in ? [[ direct ; indirect ; registr ;
    827827                                                acc_a ; acc_b ; ext_indirect ;
    828828                                                ext_indirect_dptr ]] x) → ? with
Note: See TracChangeset for help on using the changeset viewer.