Ignore:
Timestamp:
Jul 19, 2012, 2:42:02 PM (9 years ago)
Author:
tranquil
Message:
  • changed order of parameters of joint_internal_function and genv in semantics
  • in semantics, unified more_sem_unserialized_params and more_sem_genv_params
  • renamed all <language>_params to <LANGUAGE>
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTL_paolo.ma

    r2208 r2214  
     1
    12include "joint/Joint_paolo.ma".
    23include "RTL/RTL_paolo.ma".
     
    4849      (* localsT ≝ *) register).
    4950
    50 definition ertl_params ≝ mk_graph_params ertl_uns_params.
    51 definition ertl_program ≝ joint_program ertl_params.
     51definition ERTL ≝ mk_graph_params ertl_uns_params.
     52definition ertl_program ≝ joint_program ERTL.
    5253
    5354interpretation "move" 'mov r a = (MOVE ?? (mk_Prod move_dst move_src r a)).
     
    5657unification hint 0 ≔
    5758(*---------------*) ⊢
    58 pair_move ertl_params ≡ move_dst × move_src.
     59pair_move ERTL ≡ move_dst × move_src.
    5960unification hint 0 ≔
    6061(*---------------*) ⊢
    61 acc_a_reg ertl_params ≡ register.
     62acc_a_reg ERTL ≡ register.
    6263unification hint 0 ≔
    6364(*---------------*) ⊢
    64 acc_b_reg ertl_params ≡ register.
     65acc_b_reg ERTL ≡ register.
    6566unification hint 0 ≔
    6667(*---------------*) ⊢
    67 acc_a_arg ertl_params ≡ psd_argument.
     68acc_a_arg ERTL ≡ psd_argument.
    6869unification hint 0 ≔
    6970(*---------------*) ⊢
    70 acc_b_arg ertl_params ≡ psd_argument.
     71acc_b_arg ERTL ≡ psd_argument.
    7172unification hint 0 ≔
    7273(*---------------*) ⊢
    73 dpl_reg ertl_params ≡ register.
     74dpl_reg ERTL ≡ register.
    7475unification hint 0 ≔
    7576(*---------------*) ⊢
    76 dph_reg ertl_params ≡ register.
     77dph_reg ERTL ≡ register.
    7778unification hint 0 ≔
    7879(*---------------*) ⊢
    79 dpl_arg ertl_params ≡ psd_argument.
     80dpl_arg ERTL ≡ psd_argument.
    8081unification hint 0 ≔
    8182(*---------------*) ⊢
    82 dph_arg ertl_params ≡ psd_argument.
     83dph_arg ERTL ≡ psd_argument.
    8384unification hint 0 ≔
    8485(*---------------*) ⊢
    85 snd_arg ertl_params ≡ psd_argument.
     86snd_arg ERTL ≡ psd_argument.
    8687unification hint 0 ≔
    8788(*---------------*) ⊢
    88 call_args ertl_params ≡ ℕ.
     89call_args ERTL ≡ ℕ.
    8990unification hint 0 ≔
    9091(*---------------*) ⊢
    91 call_dest ertl_params ≡ unit.
     92call_dest ERTL ≡ unit.
    9293
    9394unification hint 0 ≔
    9495(*---------------*) ⊢
    95 ext_seq ertl_params ≡ ertl_seq.
     96ext_seq ERTL ≡ ertl_seq.
    9697unification hint 0 ≔
    9798(*---------------*) ⊢
    98 ext_call ertl_params ≡ void.
     99ext_call ERTL ≡ void.
    99100unification hint 0 ≔
    100101(*---------------*) ⊢
    101 ext_tailcall ertl_params ≡ void.
     102ext_tailcall ERTL ≡ void.
    102103
    103 coercion reg_to_ertl_snd_argument : ∀r : register.snd_arg ertl_params
     104coercion reg_to_ertl_snd_argument : ∀r : register.snd_arg ERTL
    104105  psd_argument_from_reg
    105   on _r : register to snd_arg ertl_params.
    106 coercion byte_to_ertl_snd_argument : ∀b : Byte.snd_arg ertl_params
     106  on _r : register to snd_arg ERTL.
     107coercion byte_to_ertl_snd_argument : ∀b : Byte.snd_arg ERTL
    107108  psd_argument_from_byte
    108   on _b : Byte to snd_arg ertl_params.
     109  on _b : Byte to snd_arg ERTL.
    109110 
    110 definition ertl_seq_joint ≝ extension_seq ertl_params.
    111 coercion ertl_seq_to_joint_seq : ∀globals.∀s : ertl_seq.joint_seq ertl_params globals ≝ ertl_seq_joint
    112   on _s : ertl_seq to joint_seq ertl_params.
    113 
     111definition ertl_seq_joint ≝ extension_seq ERTL.
     112coercion ertl_seq_to_joint_seq : ∀globals.∀s : ertl_seq.joint_seq ERTL globals ≝ ertl_seq_joint
     113  on _s : ertl_seq to joint_seq ERTL.
Note: See TracChangeset for help on using the changeset viewer.