Changeset 1163 for src/ERTL/ERTL.ma


Ignore:
Timestamp:
Sep 1, 2011, 4:23:42 PM (9 years ago)
Author:
mulligan
Message:

even more streamlining and fixes to get things type checking

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTL.ma

    r1161 r1163  
    99definition registers ≝ list register.
    1010
     11inductive move_registers: Type[0] ≝
     12  | pseudo: register → move_registers
     13  | hardware: Register → move_registers.
     14
    1115definition pre_ertl_statement ≝
    1216  λglobals: list ident.
    1317  joint_statement label globals register
    1418                  register register register
    15                   register (Register × Register).
     19                  (move_registers × move_registers) register.
    1620                 
    1721inductive ertl_statement (globals: list ident): Type[0] ≝
     
    1923  | ertl_st_new_frame: label → ertl_statement globals
    2024  | ertl_st_del_frame: label → ertl_statement globals
    21   | ertl_st_frame_size: register → label → ertl_statement globals
    22   | ertl_st_move: register → register → label → ertl_statement globals
    23   | ertl_st_get_hdw: register → Register → label → ertl_statement globals
    24   | ertl_st_set_hdw: Register → register → label → ertl_statement globals.
     25  | ertl_st_frame_size: register → label → ertl_statement globals.
    2526
    2627(*
Note: See TracChangeset for help on using the changeset viewer.