Changeset 1250 for src/joint/Joint.ma


Ignore:
Timestamp:
Sep 22, 2011, 12:02:35 PM (9 years ago)
Author:
sacerdot
Message:
  1. Sigma types projections moved to utilities/extralib.ma
  2. Extended statement turned into extended instructions, decreasing the amount of code in the translations
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/Joint.ma

    r1246 r1250  
    4141  | joint_instr_store: dpl_reg p → dph_reg p → acc_a_reg p → joint_instruction p globals
    4242  | joint_instr_call_id: ident → nat → joint_instruction p globals
    43   | joint_instr_cond: acc_a_reg p → label → joint_instruction p globals.
     43  | joint_instr_cond: acc_a_reg p → label → joint_instruction p globals
     44  | joint_instr_extension: extend_statements p → joint_instruction p globals.
    4445
    4546inductive joint_statement (p:params_) (globals: list ident): Type[0] ≝
    4647  | joint_st_sequential: joint_instruction p globals → succ p → joint_statement p globals
    4748  | joint_st_goto: label → joint_statement p globals
    48   | joint_st_return: joint_statement p globals
    49   | joint_st_extension: extend_statements p → joint_statement p globals.
     49  | joint_st_return: joint_statement p globals.
     50
    5051
    5152record params (globals: list ident): Type[1] ≝
Note: See TracChangeset for help on using the changeset viewer.