source: src/joint/Joint.ma @ 2774

Last change on this file since 2774 was 2774, checked in by sacerdot, 7 years ago
  1. the compiler now outputs both the stack cost model and the max stack available
  2. hypothesis on initial status not failing removed from correctness.ma by using the low level definition
File size: 20.5 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
94inductive joint_seq (p:unserialized_params) (globals: list ident): Type[0] ≝
95  | COMMENT: String → joint_seq p globals
96  | MOVE: pair_move p → joint_seq p globals
97  | POP: acc_a_reg p → joint_seq p globals
98  | PUSH: acc_a_arg p → joint_seq p globals
99  | ADDRESS: ∀i: ident. i ∈ globals → dpl_reg p → dph_reg p → joint_seq p globals
100  | OPACCS: OpAccs → acc_a_reg p → acc_b_reg p → acc_a_arg p → acc_b_arg p → joint_seq p globals
101  | OP1: Op1 → acc_a_reg p → acc_a_reg p → joint_seq p globals
102  | OP2: Op2 → acc_a_reg p → acc_a_arg p → snd_arg p → joint_seq p globals
103  (* int done with generic move *)
104(*| INT: generic_reg p → Byte → joint_seq p globals *)
105  | CLEAR_CARRY: joint_seq p globals
106  | SET_CARRY: joint_seq p globals
107  | LOAD: acc_a_reg p → dpl_arg p → dph_arg p → joint_seq p globals
108  | STORE: dpl_arg p → dph_arg p → acc_a_arg p → joint_seq p globals
109  | extension_seq : ext_seq p → joint_seq p globals.
110
111definition NOOP ≝ λp,globals.COMMENT p globals EmptyString.
112
113notation "r ← a1 .op. a2" with precedence 60 for
114  @{'op2 $op $r $a1 $a2}.
115notation "r ← . op . a" with precedence 60 for
116  @{'op1 $op $r $a}.
117notation "r ← a" with precedence 60 for
118  @{'mov $r $a}. (* to be set in individual languages *)
119notation "❮r, s❯ ← a1 . op . a2" with precedence 55 for
120  @{'opaccs $op $r $s $a1 $a2}.
121
122interpretation "op2" 'op2 op r a1 a2 = (OP2 ? ? op r a1 a2).
123interpretation "op1" 'op1 op r a = (OP1 ? ? op r a).
124interpretation "opaccs" 'opaccs op r s a1 a2 = (OPACCS ? ? op r s a1 a2).
125
126coercion extension_seq_to_seq : ∀p,globals.∀s : ext_seq p.joint_seq p globals ≝
127  extension_seq on _s : ext_seq ? to joint_seq ??.
128
129(* inductive joint_branch (p : step_params) : Type[0] ≝
130  | COND: acc_a_reg p → label → joint_branch p
131  | extension_branch : ext_branch p → joint_branch p.*)
132
133(*coercion extension_to_branch : ∀p.∀s : ext_branch p.joint_branch p ≝
134  extension_branch on _s : ext_branch ? to joint_branch ?.*)
135
136inductive joint_step (p : unserialized_params) (globals : list ident) : Type[0] ≝
137  | COST_LABEL: costlabel → joint_step p globals
138  | CALL: (ident + (dpl_arg p × (dph_arg p))) → call_args p → call_dest p → joint_step p globals
139  | COND: acc_a_reg p → label → joint_step p globals
140  | step_seq : joint_seq p globals → joint_step p globals.
141
142coercion seq_to_step : ∀p,globals.∀s : joint_seq p globals.joint_step p globals ≝
143  step_seq on _s : joint_seq ?? to joint_step ??.
144
145definition step_labels ≝
146  λp, globals.λs : joint_step p globals.
147  match s with
148  [ step_seq s ⇒
149    match s with
150    [ extension_seq ext ⇒ ext_seq_labels … ext
151    | _ ⇒ [ ]
152    ]
153  | COND _ l ⇒ [l]
154  | _ ⇒ [ ]
155  ].
156
157definition step_forall_labels : ∀p.∀globals.
158    (label → Prop) → joint_step p globals → Prop ≝
159λp,g,P,inst. All … P (step_labels … inst).
160
161record stmt_params : Type[1] ≝
162  { uns_pars :> unserialized_params
163  ; succ : Type[0]
164  ; succ_label : succ → option label
165  ; has_fcond : bool
166  }.
167
168inductive joint_fin_step (p: unserialized_params): Type[0] ≝
169  | GOTO: label → joint_fin_step p
170  | RETURN: joint_fin_step p
171  | TAILCALL :
172    has_tailcalls p → (ident + (dpl_arg p × (dph_arg p))) →
173    call_args p → joint_fin_step p.
174
175definition fin_step_labels ≝ λp.λs : joint_fin_step p.
176  match s with
177  [ GOTO l ⇒ [l]
178  | _ ⇒ [ ]
179  ].
180
181inductive joint_statement (p: stmt_params) (globals: list ident): Type[0] ≝
182  | sequential: joint_step p globals → succ p → joint_statement p globals
183  | final: joint_fin_step p → joint_statement p globals
184  | FCOND: has_fcond p → acc_a_reg p → label → label → joint_statement p globals.
185
186coercion fin_step_to_stmt : ∀p : stmt_params.∀globals.
187  ∀s : joint_fin_step p.joint_statement p globals ≝
188  final on _s : joint_fin_step ? to joint_statement ??.
189
190record params : Type[1] ≝
191 { stmt_pars :> stmt_params
192 ; codeT: list ident → Type[0]
193 ; code_point : Type[0]
194 ; stmt_at : ∀globals.codeT globals → code_point → option (joint_statement stmt_pars globals)
195 ; point_of_label : ∀globals.codeT globals → label → option code_point
196 ; point_of_succ : code_point → succ stmt_pars → code_point
197 }.
198
199definition code_has_point ≝
200  λp,globals,c,pt.match stmt_at p globals c pt with [Some _ ⇒ true | None ⇒ false].
201
202(* interpretation "code membership" 'mem p c = (code_has_point ?? c p). *)
203(*
204definition point_in_code ≝ λp,globals,code.Σpt.bool_to_Prop (code_has_point p globals code pt).
205unification 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)).
206
207definition stmt_at_safe ≝ λp,globals,code.λpt : point_in_code p globals code.
208  match pt with
209  [ mk_Sig pt' pt_prf ⇒
210    match stmt_at … code pt' return λx.stmt_at … code pt' = x → ? with
211    [ Some x ⇒ λ_.x
212    | None ⇒ λabs.⊥
213    ] (refl …)
214  ]. normalize in pt_prf;
215    >abs in pt_prf; // qed.
216*)
217
218definition forall_statements : ∀p : params.∀globals.pred_transformer (joint_statement p globals) (codeT p globals)  ≝
219  λp,globals,P,c. ∀pt,s.stmt_at ?? c pt = Some ? s → P s.
220
221definition forall_statements_i :
222  ∀p : params.∀globals.(code_point p → joint_statement p globals → Prop) →
223    codeT p globals → Prop  ≝
224  λp,globals,P,c. ∀pt,s.stmt_at ?? c pt = Some ? s → P pt s.
225
226lemma forall_statements_mp : ∀p,globals.modus_ponens ?? (forall_statements p globals).
227#p #globals #P #Q #H #y #G #pnt #s #EQ @H @(G … EQ) qed.
228
229lemma forall_statements_i_mp : ∀p,globals.∀P,Q.(∀pt,s.P pt s → Q pt s) →
230  ∀c.forall_statements_i p globals P c → forall_statements_i p globals Q c.
231#p #globals #P #Q #H #y #G #pnt #s #EQ @H @(G … EQ) qed.
232
233definition code_has_label ≝ λp,globals,c,l.
234  match point_of_label p globals c l with
235  [ Some pt ⇒ code_has_point … c pt
236  | None ⇒ false
237  ].
238
239definition stmt_explicit_labels :
240  ∀p,globals.
241  joint_statement p globals → list label ≝
242  λp,globals,stmt. match stmt with
243  [ sequential c _ ⇒ step_labels … c
244  | final c ⇒ fin_step_labels … c
245  | FCOND _ _ l1 l2 ⇒ [l1 ; l2]
246  ].
247
248definition stmt_implicit_label : ∀p,globals.joint_statement p globals →
249  option label ≝
250 λp,globals,s.match s with [ sequential _ s ⇒ succ_label … s | _ ⇒ None ?].
251 
252definition stmt_labels : ∀p : stmt_params.∀globals.
253    joint_statement p globals → list label ≝
254  λp,g,stmt.
255  (match stmt_implicit_label … stmt with
256     [ Some l ⇒ [l]
257     | None ⇒ [ ]
258     ]) @ stmt_explicit_labels … stmt.
259
260definition stmt_forall_labels ≝
261  λp, globals.λ P : label → Prop.λs : joint_statement p globals.
262  All … P (stmt_labels … s).
263
264lemma stmt_forall_labels_explicit : ∀p,globals,P.∀s : joint_statement p globals.
265  stmt_forall_labels … P s → All … P (stmt_explicit_labels … s).
266#p#globals#P #s
267whd in ⊢ (% → ?);
268whd in ⊢ (???% → ?);
269elim (stmt_implicit_label ???) [2: #next * #_] //
270qed.
271
272lemma stmt_forall_labels_implicit : ∀p,globals,P.∀s : joint_statement p globals.
273  stmt_forall_labels … P s →
274    opt_All … P (stmt_implicit_label … s).
275#p#globals#P#s
276whd in ⊢ (% → ?);
277whd in ⊢ (???% → ?);
278elim (stmt_implicit_label ???)
279[ //
280| #next * #Pnext #_ @Pnext
281]
282qed.
283
284definition code_forall_labels ≝
285  λp,globals,P,c.forall_statements p globals (stmt_forall_labels … P) c.
286
287lemma code_forall_labels_mp : ∀p,globals,P,Q.(∀l.P l → Q l) →
288  ∀c.code_forall_labels p globals P c → code_forall_labels … Q c ≝
289  λp,globals,P,Q,H.forall_statements_mp … (λs. All_mp … H ?).
290
291record lin_params : Type[1] ≝
292  { l_u_pars : unserialized_params }.
293 
294lemma index_of_label_length : ∀tag,A,lbl,l.occurs_exactly_once ?? lbl l → lt (index_of_label tag A lbl l) (|l|).
295#tag #A #lbl #l elim l [*]
296** [2: #id] #a #tl #IH
297[ change with (if (eq_identifier ???) then ? else ?) in match (occurs_exactly_once ????);
298  change with (if (eq_identifier ???) then ? else ?) in match (index_of_label ????);
299  @eq_identifier_elim #Heq normalize nodelta
300  [ #_ normalize / by /]
301| whd in ⊢ (?%→?%?);
302]
303#H >(index_of_label_from_internal … H)
304@le_S_S @(IH H)
305qed.
306
307(* mv *)
308lemma nth_opt_hit_length : ∀A,l,n,x.nth_opt A n l = Some ? x → n < |l|.
309#A #l elim l normalize [ #n #x #ABS destruct(ABS)]
310#hd #tl #IH * [2:#n] #x normalize [#H @le_S_S @(IH … H)] /2 by /
311qed.
312
313lemma nth_opt_miss_length : ∀A,l,n.nth_opt A n l = None ? → n ≥ |l|.
314#A #l elim l [//] #hd #tl #IH * normalize [#ABS destruct(ABS)]
315#n' #H @le_S_S @(IH … H)
316qed.
317
318lemma nth_opt_safe : ∀A,l,n,prf.nth_opt A n l = Some ? (nth_safe A n l prf).
319#A #l elim l
320[ #n #ABS @⊥ /2 by absurd/
321| #hd #tl #IH * normalize //
322]
323qed.
324
325definition lin_params_to_params ≝
326  λlp : lin_params.
327     mk_params
328      (mk_stmt_params (l_u_pars lp) unit (λ_.None ?) true)
329    (* codeT ≝ *)(λglobals.list ((option label) × (joint_statement ? globals)))
330    (* code_point ≝ *)ℕ
331    (* stmt_at ≝ *)(λglobals,code,point.! ls ← nth_opt ? point code ; return \snd ls)
332    (* point_of_label ≝ *)(λglobals,c,lbl.
333      If occurs_exactly_once ?? lbl c then with prf do
334        return index_of_label ?? lbl c
335      else
336        None ?)
337    (* point_of_succ ≝ *)(λcurrent.λ_.S (current)).
338
339coercion lp_to_p : ∀lp : lin_params.params ≝ lin_params_to_params
340  on _lp : lin_params to params.
341 
342lemma lin_code_has_point : ∀lp : lin_params.∀globals.∀code:codeT lp globals.
343  ∀pt.code_has_point … code pt = leb (S pt) (|code|).
344#lp #globals #code elim code
345[ #pt %
346| #hd #tl #IH * [%]
347  #n @IH
348]qed.
349
350lemma lin_code_has_label : ∀lp : lin_params.∀globals.∀code:codeT lp globals.
351  ∀lbl.code_has_label … code lbl = occurs_exactly_once ?? lbl code.
352#lp #globals #code #lbl
353whd in match (code_has_label ????);
354whd in match (point_of_label ????);
355elim (true_or_false_Prop (occurs_exactly_once ?? lbl code))
356#Heq >Heq normalize nodelta
357[ >lin_code_has_point @(leb_elim (S ?)) [#_ |
358  #ABS elim(absurd ?? ABS) -ABS
359  @index_of_label_length assumption ]] %
360qed.
361
362record graph_params : Type[1] ≝
363  { g_u_pars : unserialized_params }.
364
365(* One common instantiation of params via Graphs of joint_statements
366   (all languages but LIN) *)
367definition graph_params_to_params ≝
368  λgp : graph_params.
369     mk_params
370      (mk_stmt_params (g_u_pars gp) label (Some ?) false)
371    (* codeT ≝ *)(λglobals.graph (joint_statement ? globals))
372    (* code_point ≝ *)label
373    (* stmt_at ≝ *)(λglobals,code.lookup LabelTag ? code)
374    (* point_of_label ≝ *)(λ_.λ_.λlbl.return lbl)
375    (* point_of_succ ≝ *)(λ_.λlbl.lbl).
376
377coercion gp_to_p : ∀gp:graph_params.params ≝ graph_params_to_params
378on _gp : graph_params to params.
379
380lemma graph_code_has_point : ∀gp : graph_params.∀globals.∀code:codeT gp globals.
381  ∀pt.code_has_point … code pt = (pt ∈ code). // qed.
382
383lemma graph_code_has_label : ∀gp : graph_params.∀globals.∀code:codeT gp globals.
384  ∀lbl.code_has_label … code lbl = (lbl ∈ code). // qed.
385
386definition stmt_forall_succ ≝ λp,globals.λP : succ p → Prop.
387  λs : joint_statement p globals.
388  match s with
389  [ sequential _ n ⇒ P n
390  | _ ⇒ True
391  ].
392
393definition statement_closed : ∀globals.∀p : params.
394  codeT p globals → code_point p → (joint_statement p globals) → Prop ≝
395λglobals,p,code,pt,s.
396  All ? (λl.bool_to_Prop (code_has_label ?? code l)) (stmt_explicit_labels … s) ∧
397  stmt_forall_succ … (λn.bool_to_Prop (code_has_point … code (point_of_succ ? pt n))) s.
398
399definition code_closed : ∀p : params.∀globals.
400  codeT p globals → Prop ≝ λp,globals,code.
401    forall_statements_i … (statement_closed … code) code.
402
403record joint_internal_function (p:params) (globals: list ident) : Type[0] ≝
404{ joint_if_luniverse: universe LabelTag;    (*CSC: used only for compilation*)
405  joint_if_runiverse: universe RegisterTag; (*CSC: used only for compilation*)
406  (* Paolo: if we want this machinery to work for RTLabs too, we will need the
407     following, right? *)
408(*  joint_if_sig: signature;  -- dropped in front end *)
409  joint_if_result   : call_dest p;
410  joint_if_params   : paramsT p;
411(*CSC: XXXXX stacksize unused for LTL-...*)
412  joint_if_stacksize: nat;
413  joint_if_code     : codeT p globals ;
414  joint_if_entry : Σpt.bool_to_Prop (code_has_point … joint_if_code pt) (*;
415  joint_if_exit : Σpt.bool_to_Prop (code_has_point … joint_if_code pt) *)
416}.
417
418definition code_in_universe : ∀p,globals.
419  codeT p globals → universe LabelTag → Prop ≝
420  λp,globals,c,u.∀l.code_has_label … c l → fresh_for_univ … l u.
421
422lemma memb_to_present : ∀tag,A.∀i : identifier tag.∀m.
423  i ∈ m → present tag A m i.
424#tag #A #i #m whd in ⊢ (?%→%); cases (lookup tag A m i)
425[ * | #x #_ % #ABS destruct ]
426qed.
427
428lemma present_to_memb : ∀tag,A.∀i : identifier tag.∀m.
429  present tag A m i → bool_to_Prop (i∈m).
430#tag #A #i #m whd in ⊢ (%→?%); cases (lookup tag A m i)
431[ * #ABS cases (ABS (refl …)) | #x #_ % ]
432qed.
433
434lemma graph_code_in_universe_if : ∀p : graph_params.∀globals.
435  ∀c : codeT p globals.∀u.fresh_map_for_univ … c u → code_in_universe … c u ≝
436λp,g,c,u,H,l,G.H ? (memb_to_present … G).
437
438lemma graph_code_in_universe_only_if : ∀p : graph_params.∀globals.
439  ∀c : codeT p globals.∀u.
440  code_in_universe … c u → fresh_map_for_univ … c u ≝
441λp,g,c,u,H,l,G.H ? (present_to_memb … G).
442
443include alias "basics/logic.ma".
444
445record good_if
446(p : params) (globals : list ident) (def : joint_internal_function p globals)
447: Prop ≝
448{ entry_costed :
449  ∃l,nxt.
450        stmt_at … (joint_if_code … def) (joint_if_entry … def) =
451          Some … (sequential … (COST_LABEL … l) nxt)
452; entry_unused :
453  let entry ≝ pi1 … (joint_if_entry … def) in
454  let code ≝ joint_if_code … def in
455  forall_statements_i …
456    (λpt,stmt.stmt_forall_labels … (λlbl.point_of_label … code lbl ≠ Some ? entry) stmt ∧
457              stmt_forall_succ … (λnxt.point_of_succ … pt nxt ≠ entry) stmt) code
458; code_is_closed : code_closed … (joint_if_code … def)
459; code_is_in_universe :
460  code_in_universe … (joint_if_code … def) (joint_if_luniverse … def)
461}.
462 
463definition joint_closed_internal_function ≝
464  λp,globals.
465    Σdef : joint_internal_function p globals.good_if … def.
466
467unification hint 0 ≔ p,g ⊢
468  joint_closed_internal_function p g ≡
469  Sig (joint_internal_function p g) (λdef.good_if … def).
470
471definition set_joint_code ≝
472  λglobals: list ident.
473  λpars: params.
474  λint_fun: joint_internal_function pars globals.
475  λgraph: codeT pars globals.
476  λentry.
477  (*λexit.*)
478    mk_joint_internal_function pars globals
479      (joint_if_luniverse … int_fun) (joint_if_runiverse … int_fun) (joint_if_result … int_fun)
480      (joint_if_params … int_fun) (joint_if_stacksize … int_fun)
481      graph entry (*exit*).
482
483definition set_joint_if_graph ≝
484  λglobals.λpars : graph_params.
485  λgraph.
486  λp:joint_internal_function pars globals.
487  λentry_prf.
488  (*λexit_prf.*)
489    set_joint_code globals pars p
490      graph
491      (mk_Sig ?? (joint_if_entry ?? p) entry_prf)
492      (*(mk_Sig … (joint_if_exit ?? p) exit_prf)*).
493
494definition set_luniverse ≝
495  λglobals,pars.
496  λp : joint_internal_function globals pars.
497  λluniverse: universe LabelTag.
498   mk_joint_internal_function globals pars
499    luniverse (joint_if_runiverse … p) (joint_if_result … p)
500    (joint_if_params … p) (joint_if_stacksize … p)
501    (joint_if_code … p) (joint_if_entry … p) (*(joint_if_exit … p)*).
502
503definition set_runiverse ≝
504  λglobals,pars.
505  λp : joint_internal_function globals pars.
506  λruniverse: universe RegisterTag.
507   mk_joint_internal_function globals pars
508    (joint_if_luniverse … p) runiverse (joint_if_result … p)
509    (joint_if_params … p) (joint_if_stacksize … p)
510    (joint_if_code … p) (joint_if_entry … p) (*(joint_if_exit … p)*).
511   
512(* Specialized for graph_params *)
513definition add_graph ≝
514  λg_pars : graph_params.λglobals.λl:label.λstmt.
515    λp:joint_internal_function g_pars globals.
516   let code ≝ add … (joint_if_code … p) l stmt in
517    mk_joint_internal_function …
518     (joint_if_luniverse … p) (joint_if_runiverse … p) (joint_if_result … p)
519     (joint_if_params … p) (joint_if_stacksize … p)
520     code
521     (pi1 … (joint_if_entry … p))
522     (*(pi1 … (joint_if_exit … p))*).
523>graph_code_has_point whd in match code; >mem_set_add
524@orb_Prop_r elim (joint_if_entry ???)
525#x #H <graph_code_has_point @H
526qed.
527
528definition joint_function ≝ λp,globals. fundef (joint_closed_internal_function p globals).
529
530definition joint_program ≝
531 λp:params. program (joint_function p) nat.
532
533(* The cost model for stack consumption *)
534definition stack_cost_model ≝ list (ident × nat).
535
536definition stack_cost : ∀p:params. joint_program p → stack_cost_model ≝
537 λp,pr.
538  foldr …
539   (λid_fun,acc. let 〈id,fun〉 ≝ id_fun in
540     match fun with
541     [ Internal jif ⇒ 〈id,joint_if_stacksize ?? (pi1 … jif)〉::acc
542     | External _ ⇒ acc ])
543   [ ] (prog_funct ?? pr).
544
Note: See TracBrowser for help on using the repository browser.