Changeset 1250 for src/joint


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
Location:
src/joint
Files:
2 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] ≝
  • src/joint/semantics.ma

    r1247 r1250  
    205205axiom FailedLoad : String.
    206206axiom BadFunction : String.
    207 
    208 (*CSC: move elsewhere, also in LIN.ma *)
    209 definition pi1: ∀A.∀P:A → Prop. (Σx:A. P x) → A ≝
    210  λA,P,c. match c with [ dp w _ ⇒ w ].
    211 coercion pi1: ∀A.∀P:A → Prop.∀p:(Σx:A. P x).A ≝ pi1 on _p:Σx:?.? to ?.
    212207
    213208definition eval_statement : ∀globals: list ident.∀p:sem_params2 globals. genv globals p → state p → IO io_out io_in (trace × (state p)) ≝
Note: See TracChangeset for help on using the changeset viewer.