Changeset 1171 for src/joint/Joint.ma


Ignore:
Timestamp:
Sep 2, 2011, 2:51:20 PM (8 years ago)
Author:
mulligan
Message:

changes made on claudio's request: changed order of nesting in the joint-ertl statements to make the semantics easier to write. big changes required...

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/Joint.ma

    r1169 r1171  
    3333  | joint_instr_cond: acc_a_reg p → label → joint_instruction p globals.
    3434
    35 inductive joint_statement (next: Type[0]) (p:params) (globals: list ident): Type[0] ≝
    36   | joint_st_sequential: joint_instruction p globals → next → joint_statement next p globals
    37   | joint_st_goto: label → joint_statement next p globals
    38   | joint_st_return: joint_statement next p globals.
     35inductive joint_statement (next: Type[0]) (extend: Type[0]) (p:params) (globals: list ident): Type[0] ≝
     36  | joint_st_sequential: joint_instruction p globals → next → joint_statement next extend p globals
     37  | joint_st_goto: label → joint_statement next extend p globals
     38  | joint_st_return: joint_statement next extend p globals
     39  | joint_st_extension: extend → joint_statement next extend p globals.
    3940
    4041(* Used in LTL and LIN *) 
Note: See TracChangeset for help on using the changeset viewer.