Changeset 2681 for src/RTL/RTL.ma


Ignore:
Timestamp:
Feb 19, 2013, 6:48:32 PM (7 years ago)
Author:
tranquil
Message:
  • improvements to the graph translation function
  • fixed passes up to LTL
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTL/RTL.ma

    r2640 r2681  
    44  | rtl_stack_address: register → register → rtl_seq.
    55 
    6 definition RTL_uns ≝ λhas_tailcalls.mk_unserialized_params
     6definition RTL_uns ≝ mk_unserialized_params
    77    (* acc_a_reg ≝ *) register
    88    (* acc_b_reg ≝ *) register
     
    1919    (* ext_seq ≝ *) rtl_seq
    2020    (* ext_seq_labels ≝ *) (λ_.[])
    21     (* has_tailcalls ≝ *) has_tailcalls
     21    (* has_tailcalls ≝ *) false
    2222    (* paramsT ≝ *) (list register).
    2323
    24 definition RTL ≝ mk_graph_params (RTL_uns true).
     24definition RTL ≝ mk_graph_params RTL_uns.
    2525definition rtl_program ≝ joint_program RTL.
    2626
     
    7474coercion byte_to_rtl_snd_argument : ∀b : Byte.snd_arg RTL ≝ psd_argument_from_byte
    7575  on _b : Byte to snd_arg RTL.
    76 
    77 
    78 (************ Same without tail calls ****************)
    79 
    80 definition RTL_ntc ≝ mk_graph_params (RTL_uns false).
    81 definition rtl_ntc_program ≝ joint_program RTL_ntc.
Note: See TracChangeset for help on using the changeset viewer.