Changeset 1068 for src/RTL


Ignore:
Timestamp:
Jul 14, 2011, 2:27:41 PM (9 years ago)
Author:
mulligan
Message:

rtlabs translation complete subject to axioms

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/RTL/RTL.ma

    r1066 r1068  
    2626  | rtl_st_cond: register → label → label → rtl_statement
    2727  | rtl_st_set_carry: label → rtl_statement
    28   | rtl_st_return: registers → rtl_statement.
     28  | rtl_st_return: rtl_statement. (* XXX: change from o'caml *)
    2929 
    3030definition rtl_statement_graph ≝ graph rtl_statement.
     
    3434  rtl_if_luniverse: universe LabelTag;
    3535  rtl_if_runiverse: universe RegisterTag;
    36   rtl_if_sig: signature;
     36(*  rtl_if_sig: signature;  -- dropped in front end *)
    3737  rtl_if_result: registers;
    3838  rtl_if_params: registers;
     
    4444}.
    4545
    46 inductive rtl_function_definition: Type[0] ≝
    47   | rtl_f_internal: rtl_internal_function → rtl_function_definition
    48   | rtl_f_external: external_function → rtl_function_definition.
     46definition rtl_function_definition ≝ fundef rtl_internal_function.
    4947 
    5048record rtl_program: Type[0] ≝
Note: See TracChangeset for help on using the changeset viewer.