Changeset 1168 for src/LIN


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

Joint statements parameterized over a record.

Location:
src/LIN
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/LIN/LIN.ma

    r1167 r1168  
    1 include "Joint/JointLTLLIN.ma".
    2  
    3 inductive pre_lin_statement (globals: list ident): Type[0] ≝
    4   | lin_st_lift_joint: joint_statement unit Register Register Register Register Register registers_move globals → pre_lin_statement globals.
     1include "joint/Joint.ma".
     2
     3definition lin_params: params ≝
     4 mk_params unit unit unit unit registers_move Register.
     5
     6definition pre_lin_statement ≝
     7 λglobals: list ident. joint_statement unit lin_params globals.
    58
    69definition lin_statement ≝
  • src/LIN/LINToASM.ma

    r1149 r1168  
    3535      match instr' with
    3636      [ joint_instr_cost_label lbl ⇒ set_insert ? (word_of_identifier ? lbl) (set_empty ?)
    37       | joint_instr_cond_acc lbl ⇒ set_insert ? (word_of_identifier ? lbl) (set_empty ?)
     37      | joint_instr_cond lbl ⇒ set_insert ? (word_of_identifier ? lbl) (set_empty ?)
    3838      | _ ⇒ set_empty ?
    3939      ]
Note: See TracChangeset for help on using the changeset viewer.