Changeset 2490 for src/joint


Ignore:
Timestamp:
Nov 25, 2012, 1:33:09 PM (7 years ago)
Author:
tranquil
Message:

switched back to Byte immediate (instead of beval ones)
propagated pending changes to all passes

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/Joint.ma

    r2462 r2490  
    1111   the ↓ edges are the only explicitly defined coercions). lin_params and
    1212   graph_params are simple wrappers of unserialized_params, and the coercions
    13    from them to params instantiate the missing bits with values for linarized
     13   from them to params instantate the missing bits with values for linarized
    1414   programs and graph programs respectively.
    1515
     
    3636inductive argument (T : Type[0]) : Type[0] ≝
    3737| Reg : T → argument T
    38 | Imm : beval → argument T.
     38| Imm : Byte → argument T.
    3939
    4040definition psd_argument ≝ argument register.
     
    4343coercion reg_to_psd_argument : ∀r : register.psd_argument ≝ psd_argument_from_reg
    4444  on _r : register to psd_argument.
    45 
     45(*
    4646definition psd_argument_from_beval : beval → psd_argument ≝ Imm register.
    4747coercion beval_to_psd_argument : ∀b : beval.psd_argument ≝ psd_argument_from_beval
    4848  on _b : beval to psd_argument.
    49 
    50 definition psd_argument_from_byte : Byte → psd_argument ≝ λb.Imm ? (BVByte b).
     49*)
     50definition psd_argument_from_byte : Byte → psd_argument ≝ Imm ?.
    5151coercion byte_to_psd_argument : ∀b : Byte.psd_argument ≝ psd_argument_from_byte
    5252  on _b : Byte to psd_argument.
     
    5757coercion reg_to_hdw_argument : ∀r : Register.hdw_argument ≝ hdw_argument_from_reg
    5858  on _r : Register to hdw_argument.
    59 
     59(*
    6060definition hdw_argument_from_beval : beval → hdw_argument ≝ Imm Register.
    6161coercion beval_to_hdw_argument : ∀b : beval.hdw_argument ≝ hdw_argument_from_beval
    6262  on _b : beval to hdw_argument.
    63 
    64 definition hdw_argument_from_byte : Byte → hdw_argument ≝ λb.Imm ? (BVByte b).
     63*)
     64definition hdw_argument_from_byte : Byte → hdw_argument ≝ Imm ?.
    6565coercion byte_to_hdw_argument : ∀b : Byte.psd_argument ≝ psd_argument_from_byte
    6666  on _b : Byte to hdw_argument.
     
    9696  | POP: acc_a_reg p → joint_seq p globals
    9797  | PUSH: acc_a_arg p → joint_seq p globals
    98   | ADDRESS: ∀i: ident. (member i (eq_identifier ?) globals) → dpl_reg p → dph_reg p → joint_seq p globals
     98  | ADDRESS: ∀i: ident. (member ? (eq_identifier ?) i globals) → dpl_reg p → dph_reg p → joint_seq p globals
    9999  | OPACCS: OpAccs → acc_a_reg p → acc_b_reg p → acc_a_arg p → acc_b_arg p → joint_seq p globals
    100100  | OP1: Op1 → acc_a_reg p → acc_a_reg p → joint_seq p globals
Note: See TracChangeset for help on using the changeset viewer.