1 | include "ASM/I8051.ma". |
---|
2 | include "common/CostLabel.ma". |
---|
3 | include "common/AST.ma". |
---|
4 | include "common/Registers.ma". |
---|
5 | include "utilities/sigma.ma". (* CSC: Only for Sigma type projections *) |
---|
6 | include "common/Graphs.ma". |
---|
7 | |
---|
8 | record params__: Type[1] ≝ |
---|
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 | ; call_args: Type[0] |
---|
16 | ; call_dest: Type[0] |
---|
17 | |
---|
18 | ; extend_statements: Type[0] |
---|
19 | }. |
---|
20 | |
---|
21 | record params_: Type[1] ≝ |
---|
22 | { pars__:> params__ |
---|
23 | ; succ: Type[0] |
---|
24 | }. |
---|
25 | |
---|
26 | (* One common instantiation of params via Graphs of joint_statements |
---|
27 | (all languages but LIN) *) |
---|
28 | definition graph_params_ : params__ → params_ ≝ |
---|
29 | λpars__. mk_params_ pars__ label. |
---|
30 | |
---|
31 | inductive joint_instruction (p:params__) (globals: list ident): Type[0] ≝ |
---|
32 | | COMMENT: String → joint_instruction p globals |
---|
33 | | COST_LABEL: costlabel → joint_instruction p globals |
---|
34 | | INT: generic_reg p → Byte → joint_instruction p globals |
---|
35 | | MOVE: pair_reg p → joint_instruction p globals |
---|
36 | | POP: acc_a_reg p → joint_instruction p globals |
---|
37 | | PUSH: acc_a_reg p → joint_instruction p globals |
---|
38 | | ADDRESS: ∀i: ident. (member i (eq_identifier ?) globals) → dpl_reg p → dph_reg p → joint_instruction p globals |
---|
39 | | OPACCS: OpAccs → acc_a_reg p → acc_b_reg p → acc_a_reg p → acc_b_reg p → joint_instruction p globals |
---|
40 | | OP1: Op1 → acc_a_reg p → acc_a_reg p → joint_instruction p globals |
---|
41 | | OP2: Op2 → acc_a_reg p → acc_a_reg p → generic_reg p → joint_instruction p globals |
---|
42 | | CLEAR_CARRY: joint_instruction p globals |
---|
43 | | SET_CARRY: joint_instruction p globals |
---|
44 | | LOAD: acc_a_reg p → dpl_reg p → dph_reg p → joint_instruction p globals |
---|
45 | | STORE: dpl_reg p → dph_reg p → acc_a_reg p → joint_instruction p globals |
---|
46 | | CALL_ID: ident → call_args p → call_dest p → joint_instruction p globals |
---|
47 | | COND: acc_a_reg p → label → joint_instruction p globals |
---|
48 | | extension: extend_statements p → joint_instruction p globals. |
---|
49 | |
---|
50 | inductive joint_statement (p:params_) (globals: list ident): Type[0] ≝ |
---|
51 | | sequential: joint_instruction p globals → succ p → joint_statement p globals |
---|
52 | | GOTO: label → joint_statement p globals |
---|
53 | | RETURN: joint_statement p globals. |
---|
54 | |
---|
55 | record params0: Type[1] ≝ |
---|
56 | { pars__' :> params__ |
---|
57 | ; resultT: Type[0] |
---|
58 | ; paramsT: Type[0] |
---|
59 | }. |
---|
60 | |
---|
61 | record params1 : Type[1] ≝ |
---|
62 | { pars0 :> params0 |
---|
63 | ; localsT: Type[0] |
---|
64 | }. |
---|
65 | |
---|
66 | record params (globals: list ident): Type[1] ≝ |
---|
67 | { succ_ : Type[0] |
---|
68 | ; pars1 :> params1 |
---|
69 | ; codeT: Type[0] |
---|
70 | ; lookup: codeT → label → option (joint_statement (mk_params_ pars1 succ_) globals) |
---|
71 | }. |
---|
72 | |
---|
73 | definition params__of_params: ∀globals. params globals → params_ ≝ |
---|
74 | λglobals,pars. mk_params_ pars (succ_ … pars). |
---|
75 | coercion params__of_params: ∀globals.∀p: params globals. params_ ≝ params__of_params |
---|
76 | on _p: params ? to params_. |
---|
77 | |
---|
78 | include alias "common/Graphs.ma". (* To pick the right lookup *) |
---|
79 | |
---|
80 | (* One common instantiation of params via Graphs of joint_statements |
---|
81 | (all languages but LIN) *) |
---|
82 | definition graph_params: params1 → ∀globals: list ident. params globals ≝ |
---|
83 | λpars1,globals. |
---|
84 | mk_params globals label pars1 |
---|
85 | (graph (joint_statement (graph_params_ pars1) globals)) (lookup …). |
---|
86 | |
---|
87 | |
---|
88 | (* CSC: special case where localsT is a list of register (RTL and ERTL) *) |
---|
89 | definition rtl_ertl_params1 ≝ λpars0. mk_params1 pars0 (list register). |
---|
90 | definition rtl_ertl_params ≝ λpars0. graph_params (rtl_ertl_params1 pars0). |
---|
91 | |
---|
92 | record joint_internal_function (globals: list ident) (p:params globals) : Type[0] ≝ |
---|
93 | { joint_if_luniverse: universe LabelTag; (*CSC: used only for compilation*) |
---|
94 | joint_if_runiverse: universe RegisterTag; (*CSC: used only for compilation*) |
---|
95 | (* joint_if_sig: signature; -- dropped in front end *) |
---|
96 | joint_if_result : resultT p; |
---|
97 | joint_if_params : paramsT p; |
---|
98 | joint_if_locals : localsT p; |
---|
99 | (*CSC: XXXXX stacksize unused for LTL-...*) |
---|
100 | joint_if_stacksize: nat; |
---|
101 | joint_if_code : codeT … p; |
---|
102 | (*CSC: XXXXX entry unused for LIN, but invariant in that case... *) |
---|
103 | joint_if_entry : Σl: label. lookup … joint_if_code l ≠ None ?; |
---|
104 | (*CSC: XXXXX exit only used up to RTL (and only for tailcall removal) *) |
---|
105 | joint_if_exit : Σl: label. lookup … joint_if_code l ≠ None ? |
---|
106 | }. |
---|
107 | |
---|
108 | (* Currified form *) |
---|
109 | definition set_joint_if_exit ≝ |
---|
110 | λglobals,pars. |
---|
111 | λexit: label. |
---|
112 | λp:joint_internal_function globals pars. |
---|
113 | λprf: lookup … (joint_if_code … p) exit ≠ None ?. |
---|
114 | mk_joint_internal_function globals pars |
---|
115 | (joint_if_luniverse … p) (joint_if_runiverse … p) (joint_if_result … p) |
---|
116 | (joint_if_params … p) (joint_if_locals … p) (joint_if_stacksize … p) |
---|
117 | (joint_if_code … p) (joint_if_entry … p) (dp … exit prf). |
---|
118 | |
---|
119 | definition set_joint_code ≝ |
---|
120 | λglobals: list ident. |
---|
121 | λpars: params globals. |
---|
122 | λint_fun: joint_internal_function globals pars. |
---|
123 | λgraph: codeT … pars. |
---|
124 | λentry. |
---|
125 | λexit. |
---|
126 | mk_joint_internal_function globals pars |
---|
127 | (joint_if_luniverse … int_fun) (joint_if_runiverse … int_fun) (joint_if_result … int_fun) |
---|
128 | (joint_if_params … int_fun) (joint_if_locals … int_fun) (joint_if_stacksize … int_fun) |
---|
129 | graph entry exit. |
---|
130 | |
---|
131 | definition set_joint_if_graph ≝ |
---|
132 | λglobals,pars. |
---|
133 | λgraph. |
---|
134 | λp:joint_internal_function globals pars. |
---|
135 | λentry_prf: lookup … graph (joint_if_entry … p) ≠ None ?. |
---|
136 | λexit_prf: lookup … graph (joint_if_exit … p) ≠ None ?. |
---|
137 | set_joint_code globals pars p graph |
---|
138 | (dp … (joint_if_entry … p) entry_prf) (dp … (joint_if_exit … p) exit_prf). |
---|
139 | |
---|
140 | definition set_luniverse ≝ |
---|
141 | λglobals,pars. |
---|
142 | λp : joint_internal_function globals pars. |
---|
143 | λluniverse: universe LabelTag. |
---|
144 | mk_joint_internal_function globals pars |
---|
145 | luniverse (joint_if_runiverse … p) (joint_if_result … p) |
---|
146 | (joint_if_params … p) (joint_if_locals … p) (joint_if_stacksize … p) |
---|
147 | (joint_if_code … p) (joint_if_entry … p) (joint_if_exit … p). |
---|
148 | |
---|
149 | definition set_runiverse ≝ |
---|
150 | λglobals,pars. |
---|
151 | λp : joint_internal_function globals pars. |
---|
152 | λruniverse: universe RegisterTag. |
---|
153 | mk_joint_internal_function globals pars |
---|
154 | (joint_if_luniverse … p) runiverse (joint_if_result … p) |
---|
155 | (joint_if_params … p) (joint_if_locals … p) (joint_if_stacksize … p) |
---|
156 | (joint_if_code … p) (joint_if_entry … p) (joint_if_exit … p). |
---|
157 | |
---|
158 | (* Specialized for graph_params *) |
---|
159 | definition add_graph ≝ |
---|
160 | λpars1,globals.λl:label.λstmt.λp:joint_internal_function globals (graph_params pars1 globals). |
---|
161 | let code ≝ add … (joint_if_code ?? p) l stmt in |
---|
162 | mk_joint_internal_function … (graph_params … globals) |
---|
163 | (joint_if_luniverse … p) (joint_if_runiverse … p) (joint_if_result … p) |
---|
164 | (joint_if_params … p) (joint_if_locals … p) (joint_if_stacksize … p) |
---|
165 | code (pi1 ?? (joint_if_entry … p)) (pi1 … (joint_if_exit … p)). |
---|
166 | normalize nodelta; |
---|
167 | [ cases (joint_if_entry … p) | cases (joint_if_exit … p)] |
---|
168 | #LBL #LBL_PRF @graph_add_lookup @LBL_PRF |
---|
169 | qed. |
---|
170 | |
---|
171 | definition set_locals ≝ |
---|
172 | λglobals,pars. |
---|
173 | λp : joint_internal_function globals pars. |
---|
174 | λlocals. |
---|
175 | mk_joint_internal_function globals pars |
---|
176 | (joint_if_luniverse … p) (joint_if_runiverse … p) (joint_if_result … p) |
---|
177 | (joint_if_params … p) locals (joint_if_stacksize … p) |
---|
178 | (joint_if_code … p) (joint_if_entry … p) (joint_if_exit … p). |
---|
179 | |
---|
180 | definition joint_function ≝ λp,globals. fundef (joint_internal_function p globals). |
---|
181 | |
---|
182 | definition joint_program ≝ |
---|
183 | λp:∀globals.params globals. program (λglobals. joint_function globals (p globals)) nat. |
---|