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 | include "utilities/lists.ma". |
---|
7 | include "common/LabelledObjects.ma". |
---|
8 | include "ASM/Util.ma". |
---|
9 | include "basics/deqsets.ma". |
---|
10 | include "basics/finset.ma". (* for DeqNat *) |
---|
11 | |
---|
12 | (* Here is the structure of parameter records (downward edges are coercions, |
---|
13 | the ↓ edges are the only explicitly defined coercions). lin_params and |
---|
14 | graph_params are simple wrappers of unserialized_params, and the coercions |
---|
15 | from them to params instantiate the missing bits with values for linarized |
---|
16 | programs and graph programs respectively. |
---|
17 | |
---|
18 | lin_params graph_params |
---|
19 | | \_____ /____ | |
---|
20 | | / \ | |
---|
21 | | / ↓ ↓ |
---|
22 | | | params |
---|
23 | | | | |
---|
24 | | | stmt_params |
---|
25 | | | / |
---|
26 | unserialized_params |
---|
27 | | \ |
---|
28 | | \ |
---|
29 | | local_params |
---|
30 | | | |
---|
31 | step_params funct_params |
---|
32 | |
---|
33 | step_params : types needed to define steps (stmts with a default fallthrough) |
---|
34 | stmt_params : adds successor type needed to define statements |
---|
35 | funct_params : types of result register and parameters of function |
---|
36 | local_params : adds types of local registers |
---|
37 | params : adds type of code and related properties *) |
---|
38 | |
---|
39 | record step_params : Type[1] ≝ |
---|
40 | { acc_a_reg: Type[0] (* registers that will eventually need to be A *) |
---|
41 | ; acc_b_reg: Type[0] (* registers that will eventually need to be B *) |
---|
42 | ; acc_a_arg: Type[0] (* arguments that will eventually need to be A *) |
---|
43 | ; acc_b_arg: Type[0] (* arguments that will eventually need to be B *) |
---|
44 | ; dpl_reg: Type[0] (* low address registers *) |
---|
45 | ; dph_reg: Type[0] (* high address registers *) |
---|
46 | ; dpl_arg: Type[0] (* low address registers *) |
---|
47 | ; dph_arg: Type[0] (* high address registers *) |
---|
48 | ; snd_arg : Type[0] (* second argument of binary op *) |
---|
49 | ; pair_move: Type[0] (* argument of move instructions *) |
---|
50 | ; call_args: Type[0] (* arguments of function calls *) |
---|
51 | ; call_dest: Type[0] (* possible destination of function computation *) |
---|
52 | ; ext_step: Type[0] (* other instructions not fitting in the general framework *) |
---|
53 | ; ext_step_labels : ext_step → list label |
---|
54 | ; ext_fin_stmt: Type[0] (* final instructions (e.g. tailcalls) not fitting in the general framework *) |
---|
55 | ; ext_fin_stmt_labels : ext_fin_stmt → list label |
---|
56 | }. |
---|
57 | |
---|
58 | inductive joint_step (p:step_params) (globals: list ident): Type[0] ≝ |
---|
59 | | COMMENT: String → joint_step p globals |
---|
60 | | COST_LABEL: costlabel → joint_step p globals |
---|
61 | | MOVE: pair_move p → joint_step p globals |
---|
62 | | POP: acc_a_reg p → joint_step p globals |
---|
63 | | PUSH: acc_a_arg p → joint_step p globals |
---|
64 | | ADDRESS: ∀i: ident. (member i (eq_identifier ?) globals) → dpl_reg p → dph_reg p → joint_step p globals |
---|
65 | | OPACCS: OpAccs → acc_a_reg p → acc_b_reg p → acc_a_arg p → acc_b_arg p → joint_step p globals |
---|
66 | | OP1: Op1 → acc_a_reg p → acc_a_reg p → joint_step p globals |
---|
67 | | OP2: Op2 → acc_a_reg p → acc_a_arg p → snd_arg p → joint_step p globals |
---|
68 | (* int done with generic move *) |
---|
69 | (*| INT: generic_reg p → Byte → joint_step p globals *) |
---|
70 | | CLEAR_CARRY: joint_step p globals |
---|
71 | | SET_CARRY: joint_step p globals |
---|
72 | | LOAD: acc_a_reg p → dpl_arg p → dph_arg p → joint_step p globals |
---|
73 | | STORE: dpl_arg p → dph_arg p → acc_a_arg p → joint_step p globals |
---|
74 | | CALL_ID: ident → call_args p → call_dest p → joint_step p globals |
---|
75 | | COND: acc_a_reg p → label → joint_step p globals |
---|
76 | | extension: ext_step p → joint_step p globals. |
---|
77 | |
---|
78 | axiom EmptyString : String. |
---|
79 | definition NOOP ≝ λp,globals.COMMENT p globals EmptyString. |
---|
80 | |
---|
81 | notation "r ← a1 .op. a2" with precedence 60 for |
---|
82 | @{'op2 $op $r $a1 $a2}. |
---|
83 | notation "r ← . op . a" with precedence 60 for |
---|
84 | @{'op1 $op $r $a}. |
---|
85 | notation "r ← a" with precedence 60 for |
---|
86 | @{'mov $r $a}. (* to be set in individual languages *) |
---|
87 | notation "❮r, s❯ ← a1 . op . a2" with precedence 55 for |
---|
88 | @{'opaccs $op $r $s $a1 $a2}. |
---|
89 | |
---|
90 | interpretation "op2" 'op2 op r a1 a2 = (OP2 ? ? op r a1 a2). |
---|
91 | interpretation "op1" 'op1 op r a = (OP1 ? ? op r a). |
---|
92 | interpretation "opaccs" 'opaccs op r s a1 a2 = (OPACCS ? ? op r s a1 a2). |
---|
93 | |
---|
94 | coercion extension_to_step : ∀p,globals.∀s : ext_step p.joint_step p globals ≝ |
---|
95 | extension on _s : ext_step ? to joint_step ??. |
---|
96 | |
---|
97 | definition step_labels ≝ |
---|
98 | λp, globals.λs : joint_step p globals. |
---|
99 | match s with |
---|
100 | [ COND _ l ⇒ [l] |
---|
101 | | extension ext_s ⇒ ext_step_labels ? ext_s |
---|
102 | | _ ⇒ [ ] |
---|
103 | ]. |
---|
104 | |
---|
105 | definition step_forall_labels : ∀p : step_params.∀globals. |
---|
106 | (label → Prop) → joint_step p globals → Prop ≝ |
---|
107 | λp,g,P,inst. All … P (step_labels … inst). |
---|
108 | |
---|
109 | record funct_params : Type[1] ≝ |
---|
110 | { resultT : Type[0] |
---|
111 | ; paramsT : Type[0] |
---|
112 | }. |
---|
113 | |
---|
114 | record local_params : Type[1] ≝ |
---|
115 | { funct_pars :> funct_params |
---|
116 | ; localsT: Type[0] |
---|
117 | }. |
---|
118 | |
---|
119 | |
---|
120 | record unserialized_params : Type[1] ≝ |
---|
121 | { u_inst_pars :> step_params |
---|
122 | ; u_local_pars :> local_params |
---|
123 | }. |
---|
124 | |
---|
125 | record stmt_params : Type[1] ≝ |
---|
126 | { uns_pars :> unserialized_params |
---|
127 | ; succ : Type[0] |
---|
128 | ; succ_label : succ → option label |
---|
129 | }. |
---|
130 | |
---|
131 | inductive joint_fin_step (p: stmt_params) (globals: list ident): Type[0] ≝ |
---|
132 | | GOTO: label → joint_fin_step p globals |
---|
133 | | RETURN: joint_fin_step p globals |
---|
134 | | extension_fin : ext_fin_stmt p → joint_fin_step p globals. |
---|
135 | |
---|
136 | inductive joint_statement (p: stmt_params) (globals: list ident): Type[0] ≝ |
---|
137 | | sequential: joint_step p globals → succ p → joint_statement p globals |
---|
138 | | final: joint_fin_step p globals → joint_statement p globals. |
---|
139 | |
---|
140 | coercion extension_fin_to_fin_step : ∀p : stmt_params.∀globals. |
---|
141 | ∀s : ext_fin_stmt p.joint_fin_step p globals ≝ |
---|
142 | extension_fin on _s : ext_fin_stmt ? to joint_fin_step ??. |
---|
143 | |
---|
144 | coercion fin_step_to_stmt : ∀p : stmt_params.∀globals. |
---|
145 | ∀s : joint_fin_step p globals.joint_statement p globals ≝ |
---|
146 | final on _s : joint_fin_step ?? to joint_statement ??. |
---|
147 | |
---|
148 | record params : Type[1] ≝ |
---|
149 | { stmt_pars :> stmt_params |
---|
150 | ; codeT: list ident → Type[0] |
---|
151 | ; code_point : DeqSet |
---|
152 | ; stmt_at : ∀globals.codeT globals → code_point → option (joint_statement stmt_pars globals) |
---|
153 | ; point_of_label : ∀globals.codeT globals → label → option code_point |
---|
154 | ; point_of_succ : code_point → succ stmt_pars → code_point |
---|
155 | }. |
---|
156 | |
---|
157 | definition code_has_point ≝ |
---|
158 | λp,globals,c,pt.match stmt_at p globals c pt with [Some _ ⇒ true | None ⇒ false]. |
---|
159 | |
---|
160 | interpretation "code membership" 'mem p c = (code_has_point ?? c p). |
---|
161 | |
---|
162 | definition point_in_code ≝ λp,globals,code.Σpt.bool_to_Prop (code_has_point p globals code pt). |
---|
163 | unification hint 0 ≔ p, globals, code ⊢ point_in_code p globals code ≡ Sig (code_point p) (λpt.bool_to_Prop (code_has_point p globals code pt)). |
---|
164 | |
---|
165 | definition stmt_at_safe ≝ λp,globals,code.λpt : point_in_code p globals code. |
---|
166 | match pt with |
---|
167 | [ mk_Sig pt' pt_prf ⇒ |
---|
168 | match stmt_at … code pt' return λx.stmt_at … code pt' = x → ? with |
---|
169 | [ Some x ⇒ λ_.x |
---|
170 | | None ⇒ λabs.⊥ |
---|
171 | ] (refl …) |
---|
172 | ]. normalize in pt_prf; |
---|
173 | >abs in pt_prf; // qed. |
---|
174 | |
---|
175 | definition forall_statements : ∀p : params.∀globals.pred_transformer (joint_statement p globals) (codeT p globals) ≝ |
---|
176 | λp,globals,P,c. ∀pt,s.stmt_at ?? c pt = Some ? s → P s. |
---|
177 | |
---|
178 | definition forall_statements_i : |
---|
179 | ∀p : params.∀globals.(code_point p → joint_statement p globals → Prop) → |
---|
180 | codeT p globals → Prop ≝ |
---|
181 | λp,globals,P,c. ∀pt,s.stmt_at ?? c pt = Some ? s → P pt s. |
---|
182 | |
---|
183 | lemma forall_statements_mp : ∀p,globals.modus_ponens ?? (forall_statements p globals). |
---|
184 | #p #globals #P #Q #H #y #G #pnt #s #EQ @H @(G … EQ) qed. |
---|
185 | |
---|
186 | lemma forall_statements_i_mp : ∀p,globals.∀P,Q.(∀pt,s.P pt s → Q pt s) → |
---|
187 | ∀c.forall_statements_i p globals P c → forall_statements_i p globals Q c. |
---|
188 | #p #globals #P #Q #H #y #G #pnt #s #EQ @H @(G … EQ) qed. |
---|
189 | |
---|
190 | definition code_has_label ≝ λp,globals,c,l. |
---|
191 | match point_of_label p globals c l with |
---|
192 | [ Some pt ⇒ code_has_point … c pt |
---|
193 | | None ⇒ false |
---|
194 | ]. |
---|
195 | |
---|
196 | definition fin_step_labels ≝ |
---|
197 | λp,globals.λs : joint_fin_step p globals. |
---|
198 | match s with |
---|
199 | [ GOTO l ⇒ [ l ] |
---|
200 | | RETURN ⇒ [ ] |
---|
201 | | extension_fin c ⇒ ext_fin_stmt_labels … c |
---|
202 | ]. |
---|
203 | |
---|
204 | definition stmt_explicit_labels : |
---|
205 | ∀p,globals. |
---|
206 | joint_statement p globals → list label ≝ |
---|
207 | λp,globals,stmt. match stmt with |
---|
208 | [ sequential c _ ⇒ step_labels … c |
---|
209 | | final c ⇒ fin_step_labels … c |
---|
210 | ]. |
---|
211 | |
---|
212 | definition stmt_implicit_label : ∀p,globals.joint_statement p globals → |
---|
213 | option label ≝ |
---|
214 | λp,globals,s.match s with [ sequential _ s ⇒ succ_label … s | _ ⇒ None ?]. |
---|
215 | |
---|
216 | definition stmt_labels : ∀p : stmt_params.∀globals. |
---|
217 | joint_statement p globals → list label ≝ |
---|
218 | λp,g,stmt. |
---|
219 | (match stmt_implicit_label … stmt with |
---|
220 | [ Some l ⇒ [l] |
---|
221 | | None ⇒ [ ] |
---|
222 | ]) @ stmt_explicit_labels … stmt. |
---|
223 | |
---|
224 | definition stmt_forall_labels ≝ |
---|
225 | λp, globals.λ P : label → Prop.λs : joint_statement p globals. |
---|
226 | All … P (stmt_labels … s). |
---|
227 | |
---|
228 | lemma stmt_forall_labels_explicit : ∀p,globals,P.∀s : joint_statement p globals. |
---|
229 | stmt_forall_labels … P s → All … P (stmt_explicit_labels … s). |
---|
230 | #p#globals#P #s |
---|
231 | whd in ⊢ (% → ?); |
---|
232 | whd in ⊢ (???% → ?); |
---|
233 | elim (stmt_implicit_label ???) [2: #next * #_] // |
---|
234 | qed. |
---|
235 | |
---|
236 | lemma stmt_forall_labels_implicit : ∀p,globals,P.∀s : joint_statement p globals. |
---|
237 | stmt_forall_labels … P s → |
---|
238 | opt_All … P (stmt_implicit_label … s). |
---|
239 | #p#globals#P#s |
---|
240 | whd in ⊢ (% → ?); |
---|
241 | whd in ⊢ (???% → ?); |
---|
242 | elim (stmt_implicit_label ???) |
---|
243 | [ // |
---|
244 | | #next * #Pnext #_ @Pnext |
---|
245 | ] |
---|
246 | qed. |
---|
247 | |
---|
248 | definition code_forall_labels ≝ |
---|
249 | λp,globals,P,c.forall_statements p globals (stmt_forall_labels … P) c. |
---|
250 | |
---|
251 | lemma code_forall_labels_mp : ∀p,globals,P,Q.(∀l.P l → Q l) → |
---|
252 | ∀c.code_forall_labels p globals P c → code_forall_labels … Q c ≝ |
---|
253 | λp,globals,P,Q,H.forall_statements_mp … (λs. All_mp … H ?). |
---|
254 | |
---|
255 | record lin_params : Type[1] ≝ |
---|
256 | { l_u_pars :> unserialized_params }. |
---|
257 | |
---|
258 | lemma index_of_label_length : ∀tag,A,lbl,l.occurs_exactly_once ?? lbl l → lt (index_of_label tag A lbl l) (|l|). |
---|
259 | #tag #A #lbl #l elim l [*] |
---|
260 | ** [2: #id] #a #tl #IH |
---|
261 | [ change with (if (eq_identifier ???) then ? else ?) in match (occurs_exactly_once ????); |
---|
262 | change with (if (eq_identifier ???) then ? else ?) in match (index_of_label ????); |
---|
263 | @eq_identifier_elim #Heq normalize nodelta |
---|
264 | [ #_ normalize / by /] |
---|
265 | | whd in ⊢ (?%→?%?); |
---|
266 | ] |
---|
267 | #H >(index_of_label_from_internal … H) |
---|
268 | @le_S_S @(IH H) |
---|
269 | qed. |
---|
270 | |
---|
271 | (* mv *) |
---|
272 | lemma nth_opt_hit_length : ∀A,l,n,x.nth_opt A n l = Some ? x → n < |l|. |
---|
273 | #A #l elim l normalize [ #n #x #ABS destruct(ABS)] |
---|
274 | #hd #tl #IH * [2:#n] #x normalize [#H @le_S_S @(IH … H)] /2 by / |
---|
275 | qed. |
---|
276 | |
---|
277 | lemma nth_opt_miss_length : ∀A,l,n.nth_opt A n l = None ? → n ≥ |l|. |
---|
278 | #A #l elim l [//] #hd #tl #IH * normalize [#ABS destruct(ABS)] |
---|
279 | #n' #H @le_S_S @(IH … H) |
---|
280 | qed. |
---|
281 | |
---|
282 | lemma nth_opt_safe : ∀A,l,n,prf.nth_opt A n l = Some ? (nth_safe A n l prf). |
---|
283 | #A #l elim l |
---|
284 | [ #n #ABS @⊥ /2 by absurd/ |
---|
285 | | #hd #tl #IH * normalize // |
---|
286 | ] |
---|
287 | qed. |
---|
288 | |
---|
289 | definition lin_params_to_params ≝ |
---|
290 | λlp : lin_params. |
---|
291 | mk_params |
---|
292 | (mk_stmt_params lp unit (λ_.None ?)) |
---|
293 | (* codeT ≝ *)(λglobals.list ((option label) × (joint_statement ? globals))) |
---|
294 | (* code_point ≝ *)DeqNat |
---|
295 | (* stmt_at ≝ *)(λglobals,code,point.! ls ← nth_opt ? point code ; return \snd ls) |
---|
296 | (* point_of_label ≝ *)(λglobals,c,lbl. |
---|
297 | If occurs_exactly_once ?? lbl c then with prf do |
---|
298 | return index_of_label ?? lbl c |
---|
299 | else |
---|
300 | None ?) |
---|
301 | (* point_of_succ ≝ *)(λcurrent.λ_.S (current)). |
---|
302 | |
---|
303 | coercion lp_to_p : ∀lp : lin_params.params ≝ lin_params_to_params |
---|
304 | on _lp : lin_params to params. |
---|
305 | |
---|
306 | lemma lin_code_has_point : ∀lp : lin_params.∀globals.∀code:codeT lp globals. |
---|
307 | ∀pt.pt ∈ code = leb (S pt) (|code|). |
---|
308 | #lp #globals #code elim code |
---|
309 | [ #pt % |
---|
310 | | #hd #tl #IH * [%] |
---|
311 | #n @IH |
---|
312 | ]qed. |
---|
313 | |
---|
314 | lemma lin_code_has_label : ∀lp : lin_params.∀globals.∀code:codeT lp globals. |
---|
315 | ∀lbl.code_has_label … code lbl = occurs_exactly_once ?? lbl code. |
---|
316 | #lp #globals #code #lbl |
---|
317 | whd in match (code_has_label ????); |
---|
318 | whd in match (point_of_label ????); |
---|
319 | elim (true_or_false_Prop (occurs_exactly_once ?? lbl code)) |
---|
320 | #Heq >Heq normalize nodelta |
---|
321 | [ >lin_code_has_point @(leb_elim (S ?)) [#_ | |
---|
322 | #ABS elim(absurd ?? ABS) -ABS |
---|
323 | @index_of_label_length assumption ]] % |
---|
324 | qed. |
---|
325 | |
---|
326 | record graph_params : Type[1] ≝ |
---|
327 | { g_u_pars :> unserialized_params }. |
---|
328 | |
---|
329 | (* One common instantiation of params via Graphs of joint_statements |
---|
330 | (all languages but LIN) *) |
---|
331 | definition graph_params_to_params ≝ |
---|
332 | λgp : graph_params. |
---|
333 | mk_params |
---|
334 | (mk_stmt_params gp label (Some ?)) |
---|
335 | (* codeT ≝ *)(λglobals.graph (joint_statement ? globals)) |
---|
336 | (* code_point ≝ *)(Deq_identifier LabelTag) |
---|
337 | (* stmt_at ≝ *)(λglobals,code.lookup LabelTag ? code) |
---|
338 | (* point_of_label ≝ *)(λ_.λ_.λlbl.return lbl) |
---|
339 | (* point_of_succ ≝ *)(λ_.λlbl.lbl). |
---|
340 | |
---|
341 | coercion gp_to_p : ∀gp:graph_params.params ≝ graph_params_to_params |
---|
342 | on _gp : graph_params to params. |
---|
343 | |
---|
344 | lemma graph_code_has_point : ∀gp : graph_params.∀globals.∀code:codeT gp globals. |
---|
345 | ∀pt.code_has_point … code pt = mem_set … code pt. |
---|
346 | #gp#globals*#m*#i % qed. |
---|
347 | |
---|
348 | lemma graph_code_has_label : ∀gp : graph_params.∀globals.∀code:codeT gp globals. |
---|
349 | ∀lbl.code_has_label … code lbl = mem_set … code lbl. |
---|
350 | #gp #globals * #m * #i % qed. |
---|
351 | |
---|
352 | definition stmt_forall_succ ≝ λp,globals.λP : succ p → Prop. |
---|
353 | λs : joint_statement p globals. |
---|
354 | match s with |
---|
355 | [ sequential _ n ⇒ P n |
---|
356 | | _ ⇒ True |
---|
357 | ]. |
---|
358 | |
---|
359 | definition statement_closed : ∀globals.∀p : params. |
---|
360 | codeT p globals → code_point p → (joint_statement p globals) → Prop ≝ |
---|
361 | λglobals,p,code,pt,s. |
---|
362 | All ? (λl.bool_to_Prop (code_has_label ?? code l)) (stmt_explicit_labels … s) ∧ |
---|
363 | stmt_forall_succ … (λn.bool_to_Prop (point_of_succ ? pt n ∈ code)) s. |
---|
364 | |
---|
365 | definition code_closed : ∀p : params.∀globals. |
---|
366 | codeT p globals → Prop ≝ λp,globals,code. |
---|
367 | forall_statements_i … (statement_closed … code) code. |
---|
368 | |
---|
369 | (* CSC: special case where localsT is a list of registers (RTL and ERTL) *) |
---|
370 | definition rtl_ertl_params : ?→?→params ≝ λinst_pars,funct_pars. |
---|
371 | (mk_graph_params (mk_unserialized_params inst_pars (mk_local_params funct_pars register))). |
---|
372 | |
---|
373 | record joint_internal_function (globals: list ident) (p:params) : Type[0] ≝ |
---|
374 | { joint_if_luniverse: universe LabelTag; (*CSC: used only for compilation*) |
---|
375 | joint_if_runiverse: universe RegisterTag; (*CSC: used only for compilation*) |
---|
376 | (* Paolo: if we want this machinery to work for RTLabs too, we will need the |
---|
377 | following, right? *) |
---|
378 | (* joint_if_sig: signature; -- dropped in front end *) |
---|
379 | joint_if_result : resultT p; |
---|
380 | joint_if_params : paramsT p; |
---|
381 | joint_if_locals : list (localsT p); (* use void where no locals are present *) |
---|
382 | (*CSC: XXXXX stacksize unused for LTL-...*) |
---|
383 | joint_if_stacksize: nat; |
---|
384 | joint_if_code : codeT p globals ; |
---|
385 | joint_if_entry : point_in_code … joint_if_code ; |
---|
386 | joint_if_exit : point_in_code … joint_if_code |
---|
387 | }. |
---|
388 | |
---|
389 | definition joint_closed_internal_function ≝ |
---|
390 | λglobals,p. |
---|
391 | Σdef : joint_internal_function globals p. code_closed … (joint_if_code … def). |
---|
392 | |
---|
393 | definition set_joint_code ≝ |
---|
394 | λglobals: list ident. |
---|
395 | λpars: params. |
---|
396 | λint_fun: joint_internal_function globals pars. |
---|
397 | λgraph: codeT pars globals. |
---|
398 | λentry. |
---|
399 | λexit. |
---|
400 | mk_joint_internal_function globals pars |
---|
401 | (joint_if_luniverse … int_fun) (joint_if_runiverse … int_fun) (joint_if_result … int_fun) |
---|
402 | (joint_if_params … int_fun) (joint_if_locals … int_fun) (joint_if_stacksize … int_fun) |
---|
403 | graph entry exit. |
---|
404 | |
---|
405 | definition set_joint_if_graph ≝ |
---|
406 | λglobals.λpars : graph_params. |
---|
407 | λgraph. |
---|
408 | λp:joint_internal_function globals pars. |
---|
409 | λentry_prf. |
---|
410 | λexit_prf. |
---|
411 | set_joint_code globals pars p |
---|
412 | graph |
---|
413 | (mk_Sig ?? (joint_if_entry ?? p) entry_prf) |
---|
414 | (mk_Sig … (joint_if_exit ?? p) exit_prf). |
---|
415 | |
---|
416 | definition set_luniverse ≝ |
---|
417 | λglobals,pars. |
---|
418 | λp : joint_internal_function globals pars. |
---|
419 | λluniverse: universe LabelTag. |
---|
420 | mk_joint_internal_function globals pars |
---|
421 | luniverse (joint_if_runiverse … p) (joint_if_result … p) |
---|
422 | (joint_if_params … p) (joint_if_locals … p) (joint_if_stacksize … p) |
---|
423 | (joint_if_code … p) (joint_if_entry … p) (joint_if_exit … p). |
---|
424 | |
---|
425 | definition set_runiverse ≝ |
---|
426 | λglobals,pars. |
---|
427 | λp : joint_internal_function globals pars. |
---|
428 | λruniverse: universe RegisterTag. |
---|
429 | mk_joint_internal_function globals pars |
---|
430 | (joint_if_luniverse … p) runiverse (joint_if_result … p) |
---|
431 | (joint_if_params … p) (joint_if_locals … p) (joint_if_stacksize … p) |
---|
432 | (joint_if_code … p) (joint_if_entry … p) (joint_if_exit … p). |
---|
433 | |
---|
434 | (* Specialized for graph_params *) |
---|
435 | definition add_graph ≝ |
---|
436 | λg_pars : graph_params.λglobals.λl:label.λstmt. |
---|
437 | λp:joint_internal_function globals g_pars. |
---|
438 | let code ≝ add … (joint_if_code … p) l stmt in |
---|
439 | mk_joint_internal_function ? g_pars |
---|
440 | (joint_if_luniverse … p) (joint_if_runiverse … p) (joint_if_result … p) |
---|
441 | (joint_if_params … p) (joint_if_locals … p) (joint_if_stacksize … p) |
---|
442 | code |
---|
443 | (pi1 … (joint_if_entry … p)) |
---|
444 | (pi1 … (joint_if_exit … p)). |
---|
445 | >graph_code_has_point whd in match code; >mem_set_add |
---|
446 | @orb_Prop_r [elim (joint_if_entry ???) | elim (joint_if_exit ???) ] |
---|
447 | #x #H <graph_code_has_point @H |
---|
448 | qed. |
---|
449 | |
---|
450 | definition set_locals ≝ |
---|
451 | λglobals,pars. |
---|
452 | λp : joint_internal_function globals pars. |
---|
453 | λlocals. |
---|
454 | mk_joint_internal_function globals pars |
---|
455 | (joint_if_luniverse … p) (joint_if_runiverse … p) (joint_if_result … p) |
---|
456 | (joint_if_params … p) locals (joint_if_stacksize … p) |
---|
457 | (joint_if_code … p) (joint_if_entry … p) (joint_if_exit … p). |
---|
458 | |
---|
459 | definition joint_function ≝ λp,globals. fundef (joint_internal_function p globals). |
---|
460 | |
---|
461 | definition joint_program ≝ |
---|
462 | λp:params. program (λglobals. joint_function globals p) nat. |
---|