Changeset 2561 for src/joint/Joint.ma


Ignore:
Timestamp:
Dec 18, 2012, 5:03:29 PM (8 years ago)
Author:
tranquil
Message:
  • moved CALL as different case than joint_seq: lots of broken code now
  • changed save_frame flag from bool to more descriprive variant type call_kind
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/Joint.ma

    r2547 r2561  
    107107  | LOAD: acc_a_reg p → dpl_arg p → dph_arg p → joint_seq p globals
    108108  | STORE: dpl_arg p → dph_arg p → acc_a_arg p → joint_seq p globals
    109   | CALL: (ident + (dpl_arg p × (dph_arg p))) → call_args p → call_dest p → joint_seq p globals
    110109  | extension_seq : ext_seq p → joint_seq p globals.
    111110
     
    138137inductive joint_step (p : unserialized_params) (globals : list ident) : Type[0] ≝
    139138  | step_seq : joint_seq p globals → joint_step p globals
     139  | CALL: (ident + (dpl_arg p × (dph_arg p))) → call_args p → call_dest p → joint_step p globals
    140140  | COND: acc_a_reg p → label → joint_step p globals.
    141141
     
    152152    ]
    153153  | COND _ l ⇒ [l]
     154  | CALL _ _ _ ⇒ [ ]
    154155  ].
    155156
Note: See TracChangeset for help on using the changeset viewer.