Changeset 1168 for src/ERTL/ERTL.ma


Ignore:
Timestamp:
Sep 2, 2011, 11:36:15 AM (9 years ago)
Author:
sacerdot
Message:

Joint statements parameterized over a record.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTL.ma

    r1165 r1168  
    11include "ASM/I8051.ma".
    2 include "LIN/JointLTLLIN.ma".
     2include "joint/Joint.ma".
    33include "utilities/BitVectorTrieSet.ma".
    44include "utilities/IdentifierTools.ma".
     
    1313  | hardware: Register → move_registers.
    1414
    15 definition pre_ertl_statement ≝
    16   joint_statement label register register register register
    17                   (move_registers × move_registers) register.
     15definition ertl_params: params ≝
     16 mk_params register register register register (move_registers × move_registers) register.
     17
     18definition pre_ertl_statement ≝ joint_statement label ertl_params.
    1819                 
    1920inductive ertl_statement (globals: list ident): Type[0] ≝
     
    2223  | ertl_st_del_frame: label → ertl_statement globals
    2324  | ertl_st_frame_size: register → label → ertl_statement globals.
    24 
    25 (*
    26 inductive ertl_statement: Type[0] ≝
    27   | ertl_st_skip: label → ertl_statement
    28   | ertl_st_comment: String → label → ertl_statement
    29   | ertl_st_cost: costlabel → label → ertl_statement
    30   | ertl_st_get_hdw: register → Register → label → ertl_statement
    31   | ertl_st_set_hdw: Register → register → label → ertl_statement
    32   | ertl_st_hdw_to_hdw: Register → Register → label → ertl_statement
    33   | ertl_st_new_frame: label → ertl_statement
    34   | ertl_st_del_frame: label → ertl_statement
    35   | ertl_st_frame_size: register → label → ertl_statement
    36   | ertl_st_pop: register → label → ertl_statement
    37   | ertl_st_push: register → label → ertl_statement
    38   | ertl_st_addr: register → register → ident → label → ertl_statement
    39   | ertl_st_int: register → Byte → label → ertl_statement
    40   | ertl_st_move: register → register → label → ertl_statement
    41   | ertl_st_opaccs: OpAccs → register → register → register → register → label → ertl_statement
    42   | ertl_st_op1: Op1 → register → register → label → ertl_statement
    43   | ertl_st_op2: Op2 → register → register → register → label → ertl_statement
    44   | ertl_st_clear_carry: label → ertl_statement
    45   | ertl_st_set_carry: label → ertl_statement
    46   | ertl_st_load: register → register → register → label → ertl_statement
    47   | ertl_st_store: register → register → register → label → ertl_statement
    48   | ertl_st_call_id: ident → nat → label → ertl_statement
    49   | ertl_st_cond: register → label → label → ertl_statement
    50   | ertl_st_return: ertl_statement.
    51 *)
    5225
    5326definition ertl_statement_graph ≝ λglobals. graph (ertl_statement globals).
Note: See TracChangeset for help on using the changeset viewer.