Changeset 757 for src/LIN/JointLTLLIN.ma


Ignore:
Timestamp:
Apr 18, 2011, 12:30:53 PM (9 years ago)
Author:
mulligan
Message:

Lots more fixing to get both front and backends using same conventions and types.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/LIN/JointLTLLIN.ma

    r733 r757  
    11include "ASM/String.ma".
    22include "ASM/I8051.ma".
     3include "common/CostLabel.ma".
    34include "common/AST.ma".
     5include "common/Registers.ma".
    46
    5 inductive JointInstruction (globals: list Identifier): Type[0] ≝
    6   | Joint_Instr_Comment: String → JointInstruction globals
    7   | Joint_Instr_CostLabel: Identifier → JointInstruction globals
    8   | Joint_Instr_Int: Register → Byte → JointInstruction globals
    9   | Joint_Instr_Pop: JointInstruction globals
    10   | Joint_Instr_Push: JointInstruction globals
    11   | Joint_Instr_Address: ∀i: Identifier. (member i (eq_bv ?) globals) → JointInstruction globals
    12   | Joint_Instr_FromAcc: Register → JointInstruction globals
    13   | Joint_Instr_ToAcc: Register → JointInstruction globals
    14   | Joint_Instr_OpAccs: OpAccs → JointInstruction globals
    15   | Joint_Instr_Op1: Op1 → JointInstruction globals
    16   | Joint_Instr_Op2: Op2 → Register → JointInstruction globals
    17   | Joint_Instr_ClearCarry: JointInstruction globals
    18   | Joint_Instr_Load: JointInstruction globals
    19   | Joint_Instr_Store: JointInstruction globals
    20   | Joint_Instr_CallId: Identifier → JointInstruction globals
    21   | Joint_Instr_CondAcc: Identifier → JointInstruction globals.
     7inductive joint_instruction (globals: list ident): Type[0] ≝
     8  | joint_instr_comment: String → joint_instruction globals
     9  | joint_instr_cost_label: costlabel → joint_instruction globals
     10  | joint_instr_int: register → Byte → joint_instruction globals
     11  | joint_instr_pop: joint_instruction globals
     12  | joint_instr_push: joint_instruction globals
     13  | joint_instr_address: ∀i: ident. (member i (eq_identifier ?) globals) → joint_instruction globals
     14  | joint_instr_from_acc: register → joint_instruction globals
     15  | joint_instr_to_acc: register → joint_instruction globals
     16  | joint_instr_opaccs: OpAccs → joint_instruction globals
     17  | joint_instr_op1: Op1 → joint_instruction globals
     18  | joint_instr_op2: Op2 → register → joint_instruction globals
     19  | joint_instr_clear_carry: joint_instruction globals
     20  | joint_instr_load: joint_instruction globals
     21  | joint_instr_store: joint_instruction globals
     22  | joint_instr_call_id: ident → joint_instruction globals
     23  | joint_instr_cond_acc: ident → joint_instruction globals.
    2224
    23 inductive JointStatement (A: Type[0]) (globals: list Identifier): Type[0] ≝
    24   | Joint_St_Sequential: JointInstruction globals → A → JointStatement A globals
    25   | Joint_St_Goto: Identifier → JointStatement A globals
    26   | Joint_St_Return: JointStatement A globals.
     25inductive joint_statement (A: Type[0]) (globals: list ident): Type[0] ≝
     26  | joint_st_sequential: joint_instruction globals → A → joint_statement A globals
     27  | joint_st_goto: ident → joint_statement A globals
     28  | joint_st_return: joint_statement A globals.
Note: See TracChangeset for help on using the changeset viewer.