| 1 | include "ASM/I8051.ma". |
|---|
| 2 | include "utilities/BitVectorTrieSet.ma". |
|---|
| 3 | include "utilities/IdentifierTools.ma". |
|---|
| 4 | include "common/Graphs.ma". |
|---|
| 5 | include "common/CostLabel.ma". |
|---|
| 6 | include "common/Registers.ma". |
|---|
| 7 | |
|---|
| 8 | definition hardware_register ≝ Register. |
|---|
| 9 | definition registers ≝ list register. |
|---|
| 10 | |
|---|
| 11 | inductive ertl_statement: Type[0] ≝ |
|---|
| 12 | | ertl_st_skip: label → ertl_statement |
|---|
| 13 | | ertl_st_comment: String → label → ertl_statement |
|---|
| 14 | | ertl_st_cost: costlabel → label → ertl_statement |
|---|
| 15 | | ertl_st_get_hdw: register → hardware_register → label → ertl_statement |
|---|
| 16 | | ertl_st_set_hdw: hardware_register → register → label → ertl_statement |
|---|
| 17 | | ertl_st_hdw_to_hdw: hardware_register → hardware_register → label → ertl_statement |
|---|
| 18 | | ertl_st_new_frame: label → ertl_statement |
|---|
| 19 | | ertl_st_del_frame: label → ertl_statement |
|---|
| 20 | | ertl_st_frame_size: register → label → ertl_statement |
|---|
| 21 | | ertl_st_pop: register → label → ertl_statement |
|---|
| 22 | | ertl_st_push: register → label → ertl_statement |
|---|
| 23 | | ertl_st_addr_h: register → ident → label → ertl_statement |
|---|
| 24 | | ertl_st_addr_l: register → ident → label → ertl_statement |
|---|
| 25 | | ertl_st_int: register → Byte → label → ertl_statement |
|---|
| 26 | | ertl_st_move: register → register → label → ertl_statement |
|---|
| 27 | | ertl_st_opaccs: OpAccs → register → register → register → label → ertl_statement |
|---|
| 28 | | ertl_st_op1: Op1 → register → register → label → ertl_statement |
|---|
| 29 | | ertl_st_op2: Op2 → register → register → register → label → ertl_statement |
|---|
| 30 | | ertl_st_clear_carry: label → ertl_statement |
|---|
| 31 | | ertl_st_load: register → register → register → label → ertl_statement |
|---|
| 32 | | ertl_st_store: register → register → register → label → ertl_statement |
|---|
| 33 | | ertl_st_call_id: ident → Byte → label → ertl_statement |
|---|
| 34 | | ertl_st_cond_acc: register → label → label → ertl_statement |
|---|
| 35 | | ertl_st_return: registers → ertl_statement. |
|---|
| 36 | |
|---|
| 37 | definition ertl_statement_graph ≝ graph ertl_statement. |
|---|
| 38 | |
|---|
| 39 | record ertl_internal_function: Type[0] ≝ |
|---|
| 40 | { |
|---|
| 41 | ertl_if_luniverse: universe LabelTag; |
|---|
| 42 | ertl_if_runiverse: universe RegisterTag; |
|---|
| 43 | ertl_if_params: nat; |
|---|
| 44 | ertl_if_locals: registers; |
|---|
| 45 | ertl_if_stacksize: nat; |
|---|
| 46 | ertl_if_graph: ertl_statement_graph; |
|---|
| 47 | ertl_if_entry: label; |
|---|
| 48 | ertl_if_exit: label |
|---|
| 49 | }. |
|---|
| 50 | |
|---|
| 51 | inductive ertl_function: Type[0] ≝ |
|---|
| 52 | | ertl_f_internal: ertl_internal_function → ertl_function |
|---|
| 53 | | ertl_f_external: external_function → ertl_function. |
|---|
| 54 | |
|---|
| 55 | record ertl_program: Type[0] ≝ |
|---|
| 56 | { |
|---|
| 57 | ertl_pr_vars: list (ident × nat); |
|---|
| 58 | ertl_pr_funcs: list (ident × ertl_function); |
|---|
| 59 | ertl_pr_main: option ident |
|---|
| 60 | }. |
|---|
