source: src/joint/Joint.ma @ 3145

Last change on this file since 3145 was 3145, checked in by tranquil, 7 years ago
  • removed sigma types from traces of intensional events
  • completed correctness.ma using axiom files, a single daemon remains
File size: 25.2 KB
Line 
1include "common/BackEndOps.ma".
2include "common/CostLabel.ma".
3include "common/Registers.ma".
4include "ASM/I8051.ma".
5include "common/Graphs.ma".
6include "utilities/lists.ma".
7include "common/LabelledObjects.ma".
8include "ASM/Util.ma".
9include "basics/lists/listb.ma".
10include "joint/String.ma".
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 instantate 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
28unserialized_params : things unrelated to being in graph or linear form
29stmt_params : adds successor type needed to define statements
30params : adds type of code and related properties *)
31
32(*
33inductive possible_flows : Type[0] ≝
34| Labels : list label → possible_flows
35| Call : possible_flows.
36*)
37
38inductive argument (T : Type[0]) : Type[0] ≝
39| Reg : T → argument T
40| Imm : Byte → argument T.
41
42definition psd_argument ≝ argument register.
43 
44definition psd_argument_from_reg : register → psd_argument ≝ Reg register.
45coercion reg_to_psd_argument : ∀r : register.psd_argument ≝ psd_argument_from_reg
46  on _r : register to psd_argument.
47(*
48definition psd_argument_from_beval : beval → psd_argument ≝ Imm register.
49coercion beval_to_psd_argument : ∀b : beval.psd_argument ≝ psd_argument_from_beval
50  on _b : beval to psd_argument.
51*)
52definition psd_argument_from_byte : Byte → psd_argument ≝ Imm ?.
53coercion byte_to_psd_argument : ∀b : Byte.psd_argument ≝ psd_argument_from_byte
54  on _b : Byte to psd_argument.
55
56definition hdw_argument ≝ argument Register.
57 
58definition hdw_argument_from_reg : Register → hdw_argument ≝ Reg Register.
59coercion reg_to_hdw_argument : ∀r : Register.hdw_argument ≝ hdw_argument_from_reg
60  on _r : Register to hdw_argument.
61(*
62definition hdw_argument_from_beval : beval → hdw_argument ≝ Imm Register.
63coercion beval_to_hdw_argument : ∀b : beval.hdw_argument ≝ hdw_argument_from_beval
64  on _b : beval to hdw_argument.
65*)
66definition hdw_argument_from_byte : Byte → hdw_argument ≝ Imm ?.
67coercion byte_to_hdw_argument : ∀b : Byte.psd_argument ≝ psd_argument_from_byte
68  on _b : Byte to hdw_argument.
69
70definition byte_of_nat : nat → Byte ≝ bitvector_of_nat 8.
71definition zero_byte : Byte ≝ bv_zero 8.
72
73record unserialized_params : Type[1] ≝
74 { acc_a_reg: Type[0] (* registers that will eventually need to be A *)
75 ; acc_b_reg: Type[0] (* registers that will eventually need to be B *)
76 ; acc_a_arg: Type[0] (* arguments that will eventually need to be A *)
77 ; acc_b_arg: Type[0] (* arguments that will eventually need to be B *)
78 ; dpl_reg: Type[0]   (* low address registers *)
79 ; dph_reg: Type[0]   (* high address registers *)
80 ; dpl_arg: Type[0]   (* low address registers *)
81 ; dph_arg: Type[0]   (* high address registers *)
82 ; snd_arg : Type[0]  (* second argument of binary op *)
83 ; pair_move: Type[0] (* argument of move instructions *)
84 ; call_args: Type[0] (* arguments of function calls *)
85 ; call_dest: Type[0] (* possible destination of function computation *)
86 (* other instructions not fitting in the general framework *)
87 ; ext_seq : Type[0]
88 ; ext_seq_labels : ext_seq → list label
89 ; has_tailcalls : bool
90 (* if needed: ; ext_fin_branch : Type[0] ; ext_fin_branch_labels : ext_fin_branch → list label *)
91 ; paramsT : Type[0]
92 }.
93 
94record get_pseudo_reg_functs (p : unserialized_params) : Type[0] ≝
95{ acc_a_regs : acc_a_reg p → list register
96; acc_b_regs : acc_b_reg p → list register
97; acc_a_args : acc_a_arg p → list register
98; acc_b_args : acc_b_arg p → list register
99; dpl_regs : dpl_reg p → list register
100; dph_regs : dph_reg p → list register
101; dpl_args : dpl_arg p → list register
102; dph_args : dph_arg p → list register
103; snd_args : snd_arg p → list register
104; pair_move_regs : pair_move p → list register
105; f_call_args : call_args p → list register
106; f_call_dest : call_dest p → list register
107; ext_seq_regs : ext_seq p → list register
108; params_regs : paramsT p → list register
109}.
110
111record uns_params : Type[1] ≝
112{ u_pars :> unserialized_params
113; functs : get_pseudo_reg_functs u_pars
114}.
115
116inductive joint_seq (p:unserialized_params) (globals: list ident): Type[0] ≝
117  | COMMENT: String → joint_seq p globals
118  | MOVE: pair_move p → joint_seq p globals
119  | POP: acc_a_reg p → joint_seq p globals
120  | PUSH: acc_a_arg p → joint_seq p globals
121  | ADDRESS: ∀i: ident. i ∈ globals → Word → dpl_reg p → dph_reg p → joint_seq p globals
122  | OPACCS: OpAccs → acc_a_reg p → acc_b_reg p → acc_a_arg p → acc_b_arg p → joint_seq p globals
123  | OP1: Op1 → acc_a_reg p → acc_a_reg p → joint_seq p globals
124  | OP2: Op2 → acc_a_reg p → acc_a_arg p → snd_arg p → joint_seq p globals
125  (* int done with generic move *)
126(*| INT: generic_reg p → Byte → joint_seq p globals *)
127  | CLEAR_CARRY: joint_seq p globals
128  | SET_CARRY: joint_seq p globals
129  | LOAD: acc_a_reg p → dpl_arg p → dph_arg p → joint_seq p globals
130  | STORE: dpl_arg p → dph_arg p → acc_a_arg p → joint_seq p globals
131  | extension_seq : ext_seq p → joint_seq p globals.
132 
133definition get_used_registers_from_seq : ∀p : unserialized_params.∀globals.
134get_pseudo_reg_functs p → joint_seq p globals → list register ≝
135λp,globals,functs,seq.
136match seq with
137[ COMMENT _ ⇒ [ ]
138| MOVE pm ⇒ pair_move_regs … functs pm
139| POP r ⇒ acc_a_regs … functs r
140| PUSH r ⇒ acc_a_args … functs r
141| ADDRESS _ _ _ r1 r2 ⇒ (dpl_regs … functs r1) @ (dph_regs … functs r2)
142| OPACCS o r1 r2 r3 r4 ⇒ (acc_a_regs … functs r1) @ (acc_b_regs … functs r2)
143       @ (acc_a_args … functs r3) @ (acc_b_args … functs r4)
144| OP1 o r1 r2 ⇒ (acc_a_regs … functs r1) @ (acc_a_regs … functs r2)
145| OP2 o r1 r2 r3 ⇒ (acc_a_regs … functs r1) @ (acc_a_args … functs r2) @
146         (snd_args … functs r3)
147| CLEAR_CARRY ⇒ [ ]
148| SET_CARRY ⇒ [ ]
149| LOAD r1 r2 r3 ⇒ (acc_a_regs … functs r1) @ (dpl_args … functs r2) @
150                  (dph_args … functs r3)
151| STORE r1 r2 r3 ⇒ (dpl_args … functs r1) @ (dph_args … functs r2) @
152                    (acc_a_args … functs r3)
153| extension_seq ext ⇒ ext_seq_regs … functs ext
154].
155
156definition NOOP ≝ λp,globals.COMMENT p globals EmptyString.
157
158notation "r ← a1 .op. a2" with precedence 60 for
159  @{'op2 $op $r $a1 $a2}.
160notation "r ← . op . a" with precedence 60 for
161  @{'op1 $op $r $a}.
162notation "r ← a" with precedence 60 for
163  @{'mov $r $a}. (* to be set in individual languages *)
164notation "❮r, s❯ ← a1 . op . a2" with precedence 55 for
165  @{'opaccs $op $r $s $a1 $a2}.
166
167interpretation "op2" 'op2 op r a1 a2 = (OP2 ? ? op r a1 a2).
168interpretation "op1" 'op1 op r a = (OP1 ? ? op r a).
169interpretation "opaccs" 'opaccs op r s a1 a2 = (OPACCS ? ? op r s a1 a2).
170
171coercion extension_seq_to_seq : ∀p,globals.∀s : ext_seq p.joint_seq p globals ≝
172  extension_seq on _s : ext_seq ? to joint_seq ??.
173
174(* inductive joint_branch (p : step_params) : Type[0] ≝
175  | COND: acc_a_reg p → label → joint_branch p
176  | extension_branch : ext_branch p → joint_branch p.*)
177
178(*coercion extension_to_branch : ∀p.∀s : ext_branch p.joint_branch p ≝
179  extension_branch on _s : ext_branch ? to joint_branch ?.*)
180
181inductive joint_step (p : unserialized_params) (globals : list ident) : Type[0] ≝
182  | COST_LABEL: costlabel → joint_step p globals
183  | CALL: (ident + (dpl_arg p × (dph_arg p))) → call_args p → call_dest p → joint_step p globals
184  | COND: acc_a_reg p → label → joint_step p globals
185  | step_seq : joint_seq p globals → joint_step p globals.
186 
187definition get_used_registers_from_step : ∀p : unserialized_params.∀globals.
188get_pseudo_reg_functs p → joint_step p globals → list register ≝
189λp,globals,functs,step.
190match step with
191[ COST_LABEL c ⇒ [ ]
192| CALL id args dest ⇒
193     let r_id ≝  match id with
194                   [ inl _ ⇒ [ ]
195                   | inr ptr ⇒ ((dpl_args … functs) (\fst ptr)) @
196                                                 ((dph_args … functs) (\snd ptr))
197                   ] in
198    r_id @ (f_call_args … functs args) @ (f_call_dest … functs dest)
199| COND r lbl ⇒  acc_a_regs … functs r
200| step_seq s ⇒ get_used_registers_from_seq … functs s
201].
202
203coercion seq_to_step : ∀p,globals.∀s : joint_seq p globals.joint_step p globals ≝
204  step_seq on _s : joint_seq ?? to joint_step ??.
205
206definition step_labels ≝
207  λp, globals.λs : joint_step p globals.
208  match s with
209  [ step_seq s ⇒
210    match s with
211    [ extension_seq ext ⇒ ext_seq_labels … ext
212    | _ ⇒ [ ]
213    ]
214  | COND _ l ⇒ [l]
215  | _ ⇒ [ ]
216  ].
217
218definition step_forall_labels : ∀p.∀globals.
219    (label → Prop) → joint_step p globals → Prop ≝
220λp,g,P,inst. All … P (step_labels … inst).
221
222record stmt_params : Type[1] ≝
223  { uns_pars :> uns_params
224  ; succ : Type[0]
225  ; succ_label : succ → option label
226  ; has_fcond : bool
227  }.
228
229inductive joint_fin_step (p: unserialized_params): Type[0] ≝
230  | GOTO: label → joint_fin_step p
231  | RETURN: joint_fin_step p
232  | TAILCALL :
233    has_tailcalls p → (ident + (dpl_arg p × (dph_arg p))) →
234    call_args p → joint_fin_step p.
235
236definition fin_step_labels ≝ λp.λs : joint_fin_step p.
237  match s with
238  [ GOTO l ⇒ [l]
239  | _ ⇒ [ ]
240  ].
241
242inductive joint_statement (p: stmt_params) (globals: list ident): Type[0] ≝
243  | sequential: joint_step p globals → succ p → joint_statement p globals
244  | final: joint_fin_step p → joint_statement p globals
245  | FCOND: has_fcond p → acc_a_reg p → label → label → joint_statement p globals.
246
247coercion fin_step_to_stmt : ∀p : stmt_params.∀globals.
248  ∀s : joint_fin_step p.joint_statement p globals ≝
249  final on _s : joint_fin_step ? to joint_statement ??.
250
251record params : Type[1] ≝
252 { stmt_pars :> stmt_params
253 ; codeT: list ident → Type[0]
254 ; code_point : Type[0]
255 ; stmt_at : ∀globals.codeT globals → code_point → option (joint_statement stmt_pars globals)
256 ; point_of_label : ∀globals.codeT globals → label → option code_point
257 ; point_of_succ : code_point → succ stmt_pars → code_point
258 }.
259
260definition code_has_point ≝
261  λp,globals,c,pt.match stmt_at p globals c pt with [Some _ ⇒ true | None ⇒ false].
262
263(* interpretation "code membership" 'mem p c = (code_has_point ?? c p). *)
264(*
265definition point_in_code ≝ λp,globals,code.Σpt.bool_to_Prop (code_has_point p globals code pt).
266unification 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)).
267
268definition stmt_at_safe ≝ λp,globals,code.λpt : point_in_code p globals code.
269  match pt with
270  [ mk_Sig pt' pt_prf ⇒
271    match stmt_at … code pt' return λx.stmt_at … code pt' = x → ? with
272    [ Some x ⇒ λ_.x
273    | None ⇒ λabs.⊥
274    ] (refl …)
275  ]. normalize in pt_prf;
276    >abs in pt_prf; // qed.
277*)
278
279definition forall_statements : ∀p : params.∀globals.pred_transformer (joint_statement p globals) (codeT p globals)  ≝
280  λp,globals,P,c. ∀pt,s.stmt_at ?? c pt = Some ? s → P s.
281
282definition forall_statements_i :
283  ∀p : params.∀globals.(code_point p → joint_statement p globals → Prop) →
284    codeT p globals → Prop  ≝
285  λp,globals,P,c. ∀pt,s.stmt_at ?? c pt = Some ? s → P pt s.
286
287lemma forall_statements_mp : ∀p,globals.modus_ponens ?? (forall_statements p globals).
288#p #globals #P #Q #H #y #G #pnt #s #EQ @H @(G … EQ) qed.
289
290lemma forall_statements_i_mp : ∀p,globals.∀P,Q.(∀pt,s.P pt s → Q pt s) →
291  ∀c.forall_statements_i p globals P c → forall_statements_i p globals Q c.
292#p #globals #P #Q #H #y #G #pnt #s #EQ @H @(G … EQ) qed.
293
294definition code_has_label ≝ λp,globals,c,l.
295  match point_of_label p globals c l with
296  [ Some pt ⇒ code_has_point … c pt
297  | None ⇒ false
298  ].
299
300definition stmt_explicit_labels :
301  ∀p,globals.
302  joint_statement p globals → list label ≝
303  λp,globals,stmt. match stmt with
304  [ sequential c _ ⇒ step_labels … c
305  | final c ⇒ fin_step_labels … c
306  | FCOND _ _ l1 l2 ⇒ [l1 ; l2]
307  ].
308
309definition stmt_implicit_label : ∀p,globals.joint_statement p globals →
310  option label ≝
311 λp,globals,s.match s with [ sequential _ s ⇒ succ_label … s | _ ⇒ None ?].
312 
313definition stmt_labels : ∀p : stmt_params.∀globals.
314    joint_statement p globals → list label ≝
315  λp,g,stmt.
316  (match stmt_implicit_label … stmt with
317     [ Some l ⇒ [l]
318     | None ⇒ [ ]
319     ]) @ stmt_explicit_labels … stmt.
320     
321definition stmt_registers : ∀p : stmt_params.∀globals.
322joint_statement p globals → list register ≝
323λp,globals,stmt.
324match stmt with
325[ sequential c _ ⇒ get_used_registers_from_step … (functs … p) c
326| final c ⇒
327   match c with [ TAILCALL _ _ r ⇒ f_call_args … (functs … p) r | _ ⇒ [ ] ]
328| FCOND _ r _ _ ⇒ acc_a_regs … (functs … p) r
329].
330
331definition stmt_forall_labels ≝
332  λp, globals.λ P : label → Prop.λs : joint_statement p globals.
333  All … P (stmt_labels … s).
334 
335
336lemma stmt_forall_labels_explicit : ∀p,globals,P.∀s : joint_statement p globals.
337  stmt_forall_labels … P s → All … P (stmt_explicit_labels … s).
338#p#globals#P #s
339whd in ⊢ (% → ?);
340whd in ⊢ (???% → ?);
341elim (stmt_implicit_label ???) [2: #next * #_] //
342qed.
343
344lemma stmt_forall_labels_implicit : ∀p,globals,P.∀s : joint_statement p globals.
345  stmt_forall_labels … P s →
346    opt_All … P (stmt_implicit_label … s).
347#p#globals#P#s
348whd in ⊢ (% → ?);
349whd in ⊢ (???% → ?);
350elim (stmt_implicit_label ???)
351[ //
352| #next * #Pnext #_ @Pnext
353]
354qed.
355
356definition code_forall_labels ≝
357  λp,globals,P,c.forall_statements p globals (stmt_forall_labels … P) c.
358
359lemma code_forall_labels_mp : ∀p,globals,P,Q.(∀l.P l → Q l) →
360  ∀c.code_forall_labels p globals P c → code_forall_labels … Q c ≝
361  λp,globals,P,Q,H.forall_statements_mp … (λs. All_mp … H ?).
362
363record lin_params : Type[1] ≝
364  { l_u_pars : uns_params  }.
365 
366lemma index_of_label_length : ∀tag,A,lbl,l.occurs_exactly_once ?? lbl l → lt (index_of_label tag A lbl l) (|l|).
367#tag #A #lbl #l elim l [*]
368** [2: #id] #a #tl #IH
369[ change with (if (eq_identifier ???) then ? else ?) in match (occurs_exactly_once ????);
370  change with (if (eq_identifier ???) then ? else ?) in match (index_of_label ????);
371  @eq_identifier_elim #Heq normalize nodelta
372  [ #_ normalize / by /]
373| whd in ⊢ (?%→?%?);
374]
375#H >(index_of_label_from_internal … H)
376@le_S_S @(IH H)
377qed.
378
379(* mv *)
380lemma nth_opt_hit_length : ∀A,l,n,x.nth_opt A n l = Some ? x → n < |l|.
381#A #l elim l normalize [ #n #x #ABS destruct(ABS)]
382#hd #tl #IH * [2:#n] #x normalize [#H @le_S_S @(IH … H)] /2 by /
383qed.
384
385lemma nth_opt_miss_length : ∀A,l,n.nth_opt A n l = None ? → n ≥ |l|.
386#A #l elim l [//] #hd #tl #IH * normalize [#ABS destruct(ABS)]
387#n' #H @le_S_S @(IH … H)
388qed.
389
390lemma nth_opt_safe : ∀A,l,n,prf.nth_opt A n l = Some ? (nth_safe A n l prf).
391#A #l elim l
392[ #n #ABS @⊥ /2 by absurd/
393| #hd #tl #IH * normalize //
394]
395qed.
396
397definition lin_params_to_params ≝
398  λlp : lin_params.
399     mk_params
400      (mk_stmt_params (l_u_pars lp) unit (λ_.None ?) true)
401    (* codeT ≝ *)(λglobals.list ((option label) × (joint_statement ? globals)))
402    (* code_point ≝ *)ℕ
403    (* stmt_at ≝ *)(λglobals,code,point.! ls ← nth_opt ? point code ; return \snd ls)
404    (* point_of_label ≝ *)(λglobals,c,lbl.
405      If occurs_exactly_once ?? lbl c then with prf do
406        return index_of_label ?? lbl c
407      else
408        None ?)
409    (* point_of_succ ≝ *)(λcurrent.λ_.S (current)).
410
411coercion lp_to_p : ∀lp : lin_params.params ≝ lin_params_to_params
412  on _lp : lin_params to params.
413 
414lemma lin_code_has_point : ∀lp : lin_params.∀globals.∀code:codeT lp globals.
415  ∀pt.code_has_point … code pt = leb (S pt) (|code|).
416#lp #globals #code elim code
417[ #pt %
418| #hd #tl #IH * [%]
419  #n @IH
420]qed.
421
422lemma lin_code_has_label : ∀lp : lin_params.∀globals.∀code:codeT lp globals.
423  ∀lbl.code_has_label … code lbl = occurs_exactly_once ?? lbl code.
424#lp #globals #code #lbl
425whd in match (code_has_label ????);
426whd in match (point_of_label ????);
427elim (true_or_false_Prop (occurs_exactly_once ?? lbl code))
428#Heq >Heq normalize nodelta
429[ >lin_code_has_point @(leb_elim (S ?)) [#_ |
430  #ABS elim(absurd ?? ABS) -ABS
431  @index_of_label_length assumption ]] %
432qed.
433
434record graph_params : Type[1] ≝
435  { g_u_pars : uns_params }.
436
437(* One common instantiation of params via Graphs of joint_statements
438   (all languages but LIN) *)
439definition graph_params_to_params ≝
440  λgp : graph_params.
441     mk_params
442      (mk_stmt_params (g_u_pars gp) label (Some ?) false)
443    (* codeT ≝ *)(λglobals.graph (joint_statement ? globals))
444    (* code_point ≝ *)label
445    (* stmt_at ≝ *)(λglobals,code.lookup LabelTag ? code)
446    (* point_of_label ≝ *)(λ_.λ_.λlbl.return lbl)
447    (* point_of_succ ≝ *)(λ_.λlbl.lbl).
448
449coercion gp_to_p : ∀gp:graph_params.params ≝ graph_params_to_params
450on _gp : graph_params to params.
451
452lemma graph_code_has_point : ∀gp : graph_params.∀globals.∀code:codeT gp globals.
453  ∀pt.code_has_point … code pt = (pt ∈ code). // qed.
454
455lemma graph_code_has_label : ∀gp : graph_params.∀globals.∀code:codeT gp globals.
456  ∀lbl.code_has_label … code lbl = (lbl ∈ code). // qed.
457
458definition stmt_forall_succ ≝ λp,globals.λP : succ p → Prop.
459  λs : joint_statement p globals.
460  match s with
461  [ sequential _ n ⇒ P n
462  | _ ⇒ True
463  ].
464
465definition statement_closed : ∀globals.∀p : params.
466  codeT p globals → code_point p → (joint_statement p globals) → Prop ≝
467λglobals,p,code,pt,s.
468  All ? (λl.bool_to_Prop (code_has_label ?? code l)) (stmt_explicit_labels … s) ∧
469  stmt_forall_succ … (λn.bool_to_Prop (code_has_point … code (point_of_succ ? pt n))) s.
470
471definition code_closed : ∀p : params.∀globals.
472  codeT p globals → Prop ≝ λp,globals,code.
473    forall_statements_i … (statement_closed … code) code.
474
475record joint_internal_function (p:params) (globals: list ident) : Type[0] ≝
476{ joint_if_luniverse: universe LabelTag;    (*CSC: used only for compilation*)
477  joint_if_runiverse: universe RegisterTag; (*CSC: used only for compilation*)
478  (* Paolo: if we want this machinery to work for RTLabs too, we will need the
479     following, right? *)
480(*  joint_if_sig: signature;  -- dropped in front end *)
481  joint_if_result   : call_dest p;
482  joint_if_params   : paramsT p;
483  joint_if_stacksize: nat;
484  joint_if_local_stacksize: nat; (* size of the stack devoted to "forced" stack positions
485    (that are already on stack in the front end) *)
486  joint_if_code     : codeT p globals ;
487  joint_if_entry : code_point p (* Paolo: condition entry ∈ code is ensured by good_if ;
488  joint_if_exit : Σpt.bool_to_Prop (code_has_point … joint_if_code pt) *)
489}.
490
491definition regs_in_universe : ∀p,globals.
492codeT p globals → universe RegisterTag → Prop ≝
493λp,globals,c,u.∀pt,stmt.stmt_at p globals c pt = return stmt →
494All ? (λreg.fresh_for_univ … reg u) (stmt_registers … stmt).
495
496definition code_in_universe : ∀p,globals.
497  codeT p globals → universe LabelTag → Prop ≝
498  λp,globals,c,u.∀l.code_has_label … c l → fresh_for_univ … l u.
499
500lemma memb_to_present : ∀tag,A.∀i : identifier tag.∀m.
501  i ∈ m → present tag A m i.
502#tag #A #i #m whd in ⊢ (?%→%); cases (lookup tag A m i)
503[ * | #x #_ % #ABS destruct ]
504qed.
505
506lemma present_to_memb : ∀tag,A.∀i : identifier tag.∀m.
507  present tag A m i → bool_to_Prop (i∈m).
508#tag #A #i #m whd in ⊢ (%→?%); cases (lookup tag A m i)
509[ * #ABS cases (ABS (refl …)) | #x #_ % ]
510qed.
511
512lemma graph_code_in_universe_if : ∀p : graph_params.∀globals.
513  ∀c : codeT p globals.∀u.fresh_map_for_univ … c u → code_in_universe … c u ≝
514λp,g,c,u,H,l,G.H ? (memb_to_present … G).
515
516lemma graph_code_in_universe_only_if : ∀p : graph_params.∀globals.
517  ∀c : codeT p globals.∀u.
518  code_in_universe … c u → fresh_map_for_univ … c u ≝
519λp,g,c,u,H,l,G.H ? (present_to_memb … G).
520
521include alias "basics/logic.ma".
522
523record good_if
524(p : params) (globals : list ident) (def : joint_internal_function p globals)
525: Prop ≝
526{ entry_unused :
527  let entry ≝ joint_if_entry … def in
528  let code ≝ joint_if_code … def in
529  forall_statements_i …
530    (λpt,stmt.stmt_forall_labels … (λlbl.point_of_label … code lbl ≠ Some ? entry) stmt ∧
531              stmt_forall_succ … (λnxt.point_of_succ … pt nxt ≠ entry) stmt) code
532; code_is_closed : code_closed … (joint_if_code … def)
533; code_is_in_universe :
534  code_in_universe … (joint_if_code … def) (joint_if_luniverse … def)
535; regs_are_in_univers :
536  regs_in_universe … (joint_if_code … def) (joint_if_runiverse … def)
537; entry_is_cost :
538  ∃nxt,c.
539  stmt_at p globals (joint_if_code … def) (joint_if_entry … def) =
540  Some ? (sequential p ? (COST_LABEL ?? c) nxt)
541}.
542 
543definition joint_closed_internal_function ≝
544  λp,globals.
545    Σdef : joint_internal_function p globals.good_if … def.
546
547unification hint 0 ≔ p,g ⊢
548  joint_closed_internal_function p g ≡
549  Sig (joint_internal_function p g) (λdef.good_if … def).
550
551definition set_joint_code ≝
552  λglobals: list ident.
553  λpars: params.
554  λint_fun: joint_internal_function pars globals.
555  λgraph: codeT pars globals.
556  λentry.
557  (*λexit.*)
558    mk_joint_internal_function pars globals
559      (joint_if_luniverse … int_fun) (joint_if_runiverse … int_fun) (joint_if_result … int_fun)
560      (joint_if_params … int_fun) (joint_if_stacksize … int_fun)
561       (joint_if_local_stacksize … int_fun)
562      graph entry (*exit*).
563
564definition set_luniverse ≝
565  λglobals,pars.
566  λp : joint_internal_function globals pars.
567  λluniverse: universe LabelTag.
568   mk_joint_internal_function globals pars
569    luniverse (joint_if_runiverse … p) (joint_if_result … p)
570    (joint_if_params … p) (joint_if_stacksize … p) (joint_if_local_stacksize … p)
571    (joint_if_code … p) (joint_if_entry … p) (*(joint_if_exit … p)*).
572
573definition set_runiverse ≝
574  λglobals,pars.
575  λp : joint_internal_function globals pars.
576  λruniverse: universe RegisterTag.
577   mk_joint_internal_function globals pars
578    (joint_if_luniverse … p) runiverse (joint_if_result … p)
579    (joint_if_params … p) (joint_if_stacksize … p) (joint_if_local_stacksize … p)
580    (joint_if_code … p) (joint_if_entry … p) (*(joint_if_exit … p)*).
581   
582(* Specialized for graph_params *)
583definition add_graph ≝
584  λg_pars : graph_params.λglobals.λl:label.λstmt.
585    λp:joint_internal_function g_pars globals.
586   let code ≝ add … (joint_if_code … p) l stmt in
587    mk_joint_internal_function …
588     (joint_if_luniverse … p) (joint_if_runiverse … p) (joint_if_result … p)
589     (joint_if_params … p) (joint_if_stacksize … p) (joint_if_local_stacksize … p)
590     code
591     (joint_if_entry … p)
592     (*(pi1 … (joint_if_exit … p))*).
593
594definition joint_function ≝ λp,functions,globals.
595  fundef (joint_closed_internal_function p (globals @ functions)).
596
597record joint_program (p : params) : Type[0] ≝
598{ jp_functions : list ident
599; joint_prog :> program (joint_function p jp_functions) (list init_data)
600; init_cost_label : costlabel
601(* here we can have global invariants (like injectivity of cost labels) *)
602; functions_ok : (prog_funct_names … joint_prog) = jp_functions
603}.
604
605definition prog_names ≝ λpars.λp : joint_program pars.
606  prog_var_names … p @ jp_functions … p.
607
608lemma transform_prog_funct_names : ∀A,B,V.∀p : program A V.
609∀trans: ∀vars.A vars → B vars.
610prog_funct_names … (transform_program A B V p trans) =
611prog_funct_names … p.
612#A #B #V * #vars #functs #main #trans elim functs //
613* #id #f #tl #IH whd in ⊢ (??%%); @eq_f @IH qed.
614
615definition transform_joint_program :
616 ∀src,dst : params.
617 (∀globals.joint_closed_internal_function src globals →
618  joint_closed_internal_function dst globals) →
619 joint_program src → joint_program dst ≝
620 λsrc,dst,trans,prog_in.
621 mk_joint_program dst
622  (jp_functions … prog_in)
623  (transform_program … prog_in (λvars.transf_fundef … (trans ?)))
624  (init_cost_label … prog_in)
625  ?.
626@hide_prf
627>transform_prog_funct_names @functions_ok qed.
628
629(* The cost model for stack consumption *)
630definition stack_cost_model ≝ list (ident × nat).
631
632(* move! *)
633let rec list_map_opt A B (f : A → option B) (l : list A) on l : list B ≝
634match l with
635[ nil ⇒ [ ]
636| cons hd tl ⇒
637  (match f hd with [ Some x ⇒ [ x ] | None ⇒ [ ]]) @ list_map_opt … f tl
638].
639
640definition stack_cost : ∀p:params. joint_program p → stack_cost_model ≝
641 λp,pr.
642  list_map_opt …
643    (λid_fun.match \snd id_fun with
644      [ Internal jif ⇒ Some ? 〈\fst id_fun, joint_if_stacksize ?? (pi1 … jif)〉
645      | _ ⇒ None ?
646      ]) (prog_funct ?? pr).
647
648definition stack_sizes : stack_cost_model → ident → option ℕ ≝
649λm,id.find …
650  (λpr.if eq_identifier … id (\fst pr) then Some ? (\snd pr) else None ?) m.
651
652include "common/Globalenvs.ma". (* for size_init_data_list, probably to be moved to AST.ma *)
653definition globals_stacksize : ∀p.joint_program p → nat ≝
654 λpars,p.
655 Σ_{entry ∈ prog_vars … p}(size_init_data_list … (\snd entry)).
656
Note: See TracBrowser for help on using the repository browser.