source: src/LIN/JointLTLLIN.ma @ 757

Last change on this file since 757 was 757, checked in by mulligan, 10 years ago

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

File size: 1.4 KB
RevLine 
[733]1include "ASM/String.ma".
2include "ASM/I8051.ma".
[757]3include "common/CostLabel.ma".
[733]4include "common/AST.ma".
[757]5include "common/Registers.ma".
[733]6
[757]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.
[733]24
[757]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 TracBrowser for help on using the repository browser.