Changeset 1161 for src/LIN


Ignore:
Timestamp:
Aug 31, 2011, 6:24:03 PM (10 years ago)
Author:
mulligan
Message:

changes from today: merged ertl, ltl and lin into one datatype to simplify semantics

File:
1 edited

Legend:

Unmodified
Added
Removed

  • src/LIN/JointLTLLIN.ma

    r1132 r1161  
    66include "common/Registers.ma".
    77
    8 inductive joint_instruction (globals: list ident): Type[0] ≝
    9   | joint_instr_comment: String → joint_instruction globals
    10   | joint_instr_cost_label: costlabel → joint_instruction globals
    11   | joint_instr_int: Register → Byte → joint_instruction globals
    12   | joint_instr_pop: joint_instruction globals
    13   | joint_instr_push: joint_instruction globals
    14   | joint_instr_address: ∀i: ident. (member i (eq_identifier ?) globals) → joint_instruction globals
    15   | joint_instr_from_acc: Register → joint_instruction globals
    16   | joint_instr_to_acc: Register → joint_instruction globals
    17   | joint_instr_opaccs: OpAccs → joint_instruction globals
    18   | joint_instr_op1: Op1 → joint_instruction globals
    19   | joint_instr_op2: Op2 → Register → joint_instruction globals
    20   | joint_instr_clear_carry: joint_instruction globals
    21   | joint_instr_set_carry: joint_instruction globals
    22   | joint_instr_load: joint_instruction globals
    23   | joint_instr_store: joint_instruction globals
    24   | joint_instr_call_id: ident → joint_instruction globals
    25   | joint_instr_cond_acc: label → joint_instruction globals.
     8inductive joint_instruction
     9  (globals: list ident) (acc_a_reg: Type[0]) (acc_b_reg: Type[0])
     10  (dpl_reg: Type[0]) (dph_reg: Type[0]) (generic_reg: Type[0])
     11  (pair_reg: Type[0]): Type[0] ≝
     12  | joint_instr_comment: String → joint_instruction globals acc_a_reg acc_b_reg dpl_reg dph_reg generic_reg pair_reg
     13  | joint_instr_cost_label: costlabel → joint_instruction globals acc_a_reg acc_b_reg dpl_reg dph_reg generic_reg pair_reg
     14  | joint_instr_int: generic_reg → Byte → joint_instruction globals acc_a_reg acc_b_reg dpl_reg dph_reg generic_reg pair_reg
     15  | joint_instr_pop: acc_a_reg → joint_instruction globals acc_a_reg acc_b_reg dpl_reg dph_reg generic_reg pair_reg
     16  | joint_instr_push: acc_a_reg → joint_instruction globals acc_a_reg acc_b_reg dpl_reg dph_reg generic_reg pair_reg
     17  | joint_instr_address: ∀i: ident. (member i (eq_identifier ?) globals) → dpl_reg → dph_reg → joint_instruction globals acc_a_reg acc_b_reg dpl_reg dph_reg generic_reg pair_reg
     18  | joint_instr_hdw_to_hdw: pair_reg → joint_instruction globals acc_a_reg acc_b_reg dpl_reg dph_reg generic_reg pair_reg
     19  | joint_instr_opaccs: OpAccs → acc_a_reg → acc_b_reg → joint_instruction globals acc_a_reg acc_b_reg dpl_reg dph_reg generic_reg pair_reg
     20  | joint_instr_op1: Op1 → acc_a_reg → joint_instruction globals acc_a_reg acc_b_reg dpl_reg dph_reg generic_reg pair_reg
     21  | joint_instr_op2: Op2 → acc_a_reg → generic_reg → joint_instruction globals acc_a_reg acc_b_reg dpl_reg dph_reg generic_reg pair_reg
     22  | joint_instr_clear_carry: joint_instruction globals acc_a_reg acc_b_reg dpl_reg dph_reg generic_reg pair_reg
     23  | joint_instr_set_carry: joint_instruction globals acc_a_reg acc_b_reg dpl_reg dph_reg generic_reg pair_reg
     24  | joint_instr_load: acc_a_reg → dpl_reg → dph_reg → joint_instruction globals acc_a_reg acc_b_reg dpl_reg dph_reg generic_reg pair_reg
     25  | joint_instr_store: dpl_reg → dph_reg → acc_a_reg → joint_instruction globals acc_a_reg acc_b_reg dpl_reg dph_reg generic_reg pair_reg
     26  | joint_instr_call_id: ident → nat → joint_instruction globals acc_a_reg acc_b_reg dpl_reg dph_reg generic_reg pair_reg
     27  | joint_instr_cond: acc_a_reg → label → joint_instruction globals acc_a_reg acc_b_reg dpl_reg dph_reg generic_reg pair_reg.
    2628
    27 inductive joint_statement (A: Type[0]) (globals: list ident): Type[0] ≝
    28   | joint_st_sequential: joint_instruction globals → A → joint_statement A globals
    29   | joint_st_goto: label → joint_statement A globals
    30   | joint_st_return: joint_statement A globals.
     29inductive joint_statement
     30  (A: Type[0]) (globals: list ident) (acc_a_reg: Type[0]) (acc_b_reg: Type[0])
     31  (dpl_reg: Type[0]) (dph_reg: Type[0]) (generic_reg: Type[0]) (pair_reg: Type[0]): Type[0] ≝
     32  | joint_st_sequential: joint_instruction globals acc_a_reg acc_b_reg dpl_reg dph_reg generic_reg pair_reg → A → joint_statement A globals acc_a_reg acc_b_reg dpl_reg dph_reg generic_reg pair_reg
     33  | joint_st_goto: label → joint_statement A globals acc_a_reg acc_b_reg dpl_reg dph_reg generic_reg pair_reg
     34  | joint_st_return: joint_statement A globals acc_a_reg acc_b_reg dpl_reg dph_reg generic_reg pair_reg.
Note: See TracChangeset for help on using the changeset viewer.