Ignore:
Timestamp:
Jul 18, 2012, 1:26:43 PM (8 years ago)
Author:
tranquil
Message:
  • moving some code around
  • changed immediates to hold beval in general, not only bytes
  • fixed RTLabsToRTL after redefinitions in front end
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/Joint_paolo.ma

    r2186 r2208  
    3939| Labels : list label → possible_flows
    4040| Call : possible_flows.
     41
     42inductive argument (T : Type[0]) : Type[0] ≝
     43| Reg : T → argument T
     44| Imm : beval → argument T.
     45
     46definition psd_argument ≝ argument register.
     47 
     48definition psd_argument_from_reg : register → psd_argument ≝ Reg register.
     49coercion reg_to_psd_argument : ∀r : register.psd_argument ≝ psd_argument_from_reg
     50  on _r : register to psd_argument.
     51
     52definition psd_argument_from_beval : beval → psd_argument ≝ Imm register.
     53coercion beval_to_psd_argument : ∀b : beval.psd_argument ≝ psd_argument_from_beval
     54  on _b : beval to psd_argument.
     55
     56definition psd_argument_from_byte : Byte → psd_argument ≝ λb.Imm ? (BVByte b).
     57coercion byte_to_psd_argument : ∀b : Byte.psd_argument ≝ psd_argument_from_byte
     58  on _b : Byte to psd_argument.
     59
     60definition hdw_argument ≝ argument Register.
     61 
     62definition hdw_argument_from_reg : Register → hdw_argument ≝ Reg Register.
     63coercion reg_to_hdw_argument : ∀r : Register.hdw_argument ≝ hdw_argument_from_reg
     64  on _r : Register to hdw_argument.
     65
     66definition hdw_argument_from_beval : beval → hdw_argument ≝ Imm Register.
     67coercion beval_to_hdw_argument : ∀b : beval.hdw_argument ≝ hdw_argument_from_beval
     68  on _b : beval to hdw_argument.
     69
     70definition hdw_argument_from_byte : Byte → hdw_argument ≝ λb.Imm ? (BVByte b).
     71coercion byte_to_hdw_argument : ∀b : Byte.psd_argument ≝ psd_argument_from_byte
     72  on _b : Byte to hdw_argument.
     73
     74definition byte_of_nat : nat → Byte ≝ bitvector_of_nat 8.
     75definition zero_byte : Byte ≝ bv_zero 8.
    4176
    4277record step_params : Type[1] ≝
Note: See TracChangeset for help on using the changeset viewer.