1 | include "ASM/I8051.ma". |
---|
2 | include "common/CostLabel.ma". |
---|
3 | include "common/AST.ma". |
---|
4 | include "common/Registers.ma". |
---|
5 | include "common/Graphs.ma". |
---|
6 | |
---|
7 | record params: Type[1] ≝ |
---|
8 | { |
---|
9 | acc_a_reg: Type[0]; |
---|
10 | acc_b_reg: Type[0]; |
---|
11 | dpl_reg: Type[0]; |
---|
12 | dph_reg: Type[0]; |
---|
13 | pair_reg: Type[0]; |
---|
14 | generic_reg: Type[0]; |
---|
15 | |
---|
16 | extend_statements: Type[0]; |
---|
17 | |
---|
18 | resultT: Type[0]; |
---|
19 | localsT: Type[0]; |
---|
20 | paramsT: Type[0] |
---|
21 | }. |
---|
22 | |
---|
23 | inductive joint_instruction (p:params) (globals: list ident): Type[0] ≝ |
---|
24 | | joint_instr_comment: String → joint_instruction p globals |
---|
25 | | joint_instr_cost_label: costlabel → joint_instruction p globals |
---|
26 | | joint_instr_int: generic_reg p → Byte → joint_instruction p globals |
---|
27 | | joint_instr_move: pair_reg p → joint_instruction p globals |
---|
28 | | joint_instr_pop: acc_a_reg p → joint_instruction p globals |
---|
29 | | joint_instr_push: acc_a_reg p → joint_instruction p globals |
---|
30 | | joint_instr_address: ∀i: ident. (member i (eq_identifier ?) globals) → dpl_reg p → dph_reg p → joint_instruction p globals |
---|
31 | | joint_instr_opaccs: OpAccs → acc_a_reg p → acc_b_reg p → joint_instruction p globals |
---|
32 | | joint_instr_op1: Op1 → acc_a_reg p → joint_instruction p globals |
---|
33 | | joint_instr_op2: Op2 → acc_a_reg p → generic_reg p → joint_instruction p globals |
---|
34 | | joint_instr_clear_carry: joint_instruction p globals |
---|
35 | | joint_instr_set_carry: joint_instruction p globals |
---|
36 | | joint_instr_load: acc_a_reg p → dpl_reg p → dph_reg p → joint_instruction p globals |
---|
37 | | joint_instr_store: dpl_reg p → dph_reg p → acc_a_reg p → joint_instruction p globals |
---|
38 | | joint_instr_call_id: ident → nat → joint_instruction p globals |
---|
39 | | joint_instr_cond: acc_a_reg p → label → joint_instruction p globals. |
---|
40 | |
---|
41 | inductive joint_statement (p:params) (globals: list ident): Type[0] ≝ |
---|
42 | | joint_st_sequential: joint_instruction p globals → label → joint_statement p globals |
---|
43 | | joint_st_goto: label → joint_statement p globals |
---|
44 | | joint_st_return: joint_statement p globals |
---|
45 | | joint_st_extension: extend_statements p → joint_statement p globals. |
---|
46 | |
---|
47 | record sem_params_ (preparams: params) (globals: list ident): Type[1] ≝ |
---|
48 | { pmemoryT: Type[0] |
---|
49 | ; lookup: pmemoryT → label → option (joint_statement preparams globals) |
---|
50 | }. |
---|
51 | |
---|
52 | record joint_internal_function (globals: list ident) (pre) (p:sem_params_ pre globals): Type[0] ≝ |
---|
53 | { joint_if_luniverse: universe LabelTag; (*CSC: used only for compilation*) |
---|
54 | joint_if_runiverse: universe RegisterTag; (*CSC: used only for compilation*) |
---|
55 | (* joint_if_sig: signature; -- dropped in front end *) |
---|
56 | joint_if_result : resultT pre; |
---|
57 | joint_if_params : paramsT pre; |
---|
58 | joint_if_locals : localsT pre; |
---|
59 | joint_if_stacksize: nat; |
---|
60 | joint_if_graph : pmemoryT … p; |
---|
61 | joint_if_entry : Σl: label. lookup … p joint_if_graph l ≠ None ?; |
---|
62 | joint_if_exit : Σl: label. lookup … p joint_if_graph l ≠ None ? |
---|
63 | }. |
---|
64 | |
---|
65 | definition set_luniverse ≝ |
---|
66 | λglobals : list ident. |
---|
67 | λpre. |
---|
68 | λp: sem_params_ pre globals. |
---|
69 | λint_fun : joint_internal_function globals … p. |
---|
70 | λluniverse: universe LabelTag. |
---|
71 | let runiverse ≝ joint_if_runiverse … int_fun in |
---|
72 | let params ≝ joint_if_params … int_fun in |
---|
73 | let locals ≝ joint_if_locals … int_fun in |
---|
74 | let result ≝ joint_if_result … int_fun in |
---|
75 | let stacksize ≝ joint_if_stacksize … int_fun in |
---|
76 | let graph ≝ joint_if_graph … int_fun in |
---|
77 | let entry ≝ joint_if_entry … int_fun in |
---|
78 | let exit ≝ joint_if_exit … int_fun in |
---|
79 | mk_joint_internal_function globals ? p |
---|
80 | luniverse runiverse result params locals |
---|
81 | stacksize graph entry exit. |
---|
82 | |
---|
83 | definition joint_function ≝ λglobals,pre,p. fundef (joint_internal_function globals pre p). |
---|
84 | |
---|
85 | definition joint_program := |
---|
86 | λglobals:list ident.λpre.λp: sem_params_ pre globals. |
---|
87 | program (joint_function … p) nat. |
---|
88 | |
---|
89 | (****************************************************************************) |
---|
90 | |
---|
91 | (* Used in LTL and LIN *) |
---|
92 | inductive registers_move: Type[0] ≝ |
---|
93 | | from_acc: Register → registers_move |
---|
94 | | to_acc: Register → registers_move. |
---|