source: src/joint/extra_joint_semantics.ma @ 2858

Last change on this file since 2858 was 2783, checked in by piccolo, 7 years ago

modified joint_closed_internal_function definition (added condition on pseudo-registers)
added new record for parameters
modified state definition with option for framesT

File size: 5.6 KB
Line 
1(**************************************************************************)
2(*       ___                                                              *)
3(*      ||M||                                                             *)
4(*      ||A||       A project by Andrea Asperti                           *)
5(*      ||T||                                                             *)
6(*      ||I||       Developers:                                           *)
7(*      ||T||         The HELM team.                                      *)
8(*      ||A||         http://helm.cs.unibo.it                             *)
9(*      \   /                                                             *)
10(*       \ /        This file is distributed under the terms of the       *)
11(*        v         GNU General Public License Version 2                  *)
12(*                                                                        *)
13(**************************************************************************)
14
15include "joint/joint_semantics.ma".
16include "common/ExtraMonads.ma".
17
18lemma fetch_function_no_minus_one :
19  ∀F,V,i,p,bl.
20  block_id (pi1 … bl) = -1 →
21  fetch_function … (globalenv (λvars.fundef (F vars)) V i p)
22    bl = Error … [MSG BadFunction].
23 #F#V#i#p ** #r #id #EQ1 destruct
24  whd in match fetch_function; normalize nodelta
25  >globalenv_no_minus_one
26  cases (symbol_for_block ???) normalize //
27qed.
28
29lemma fetch_function_no_zero :
30 ∀F,V,i,p,bl.
31  block_id (pi1 … bl) = 0 →
32  fetch_function … (globalenv (λvars.fundef (F vars)) V i p)
33    bl = Error … [MSG BadFunction].
34 #F#V#i#p ** #r #id #EQ1 destruct
35  whd in match fetch_function; normalize nodelta
36  >globalenv_no_zero
37  cases (symbol_for_block ???) normalize //
38qed.
39
40lemma fetch_function_transf :
41 ∀A,B,V,init.∀prog_in : program A V.
42 ∀trans : ∀vars.A vars → B vars.
43 let prog_out ≝ transform_program … prog_in trans in
44 ∀bl,i,f.
45 fetch_function … (globalenv … init prog_in) bl =
46  return 〈i, f〉
47→ fetch_function … (globalenv … init prog_out) bl =
48  return 〈i, trans … f〉.
49#A #B #V #init #prog_in #trans #bl #i #f
50 whd in match fetch_function; normalize nodelta
51 #H lapply (opt_eq_from_res ???? H) -H
52 #H @('bind_inversion H) -H #id #eq_symbol_for_block
53 #H @('bind_inversion H) -H #fd #eq_find_funct
54 whd in ⊢ (??%?→?); #EQ destruct(EQ)
55 >(symbol_for_block_transf … trans) >eq_symbol_for_block >m_return_bind
56 >(find_funct_ptr_transf A B …  eq_find_funct) %
57qed.
58
59
60lemma fetch_internal_function_transf :
61 ∀A,B.∀prog_in : program (λvars.fundef (A vars)) ℕ.
62 ∀trans : ∀vars.A vars → B vars.
63 let prog_out ≝ transform_program … prog_in (λvars.transf_fundef … (trans vars)) in
64 ∀bl,i,f.
65 fetch_internal_function … (globalenv_noinit … prog_in) bl =
66  return 〈i, f〉
67→ fetch_internal_function … (globalenv_noinit … prog_out) bl =
68  return 〈i, trans … f〉.
69#A #B #prog #trans #bl #i #f
70 whd in match fetch_internal_function; normalize nodelta
71 #H @('bind_inversion H) * #id * #fd normalize nodelta #EQfetch
72 whd in ⊢ (??%%→?); #EQ destruct(EQ)
73 >(fetch_function_transf … EQfetch) %
74qed.
75
76lemma fetch_internal_function_no_zero :
77∀F,V,i,p,bl.
78  block_id (pi1 … bl) = 0 →
79  fetch_internal_function ?
80  (globalenv (λvars.fundef (F vars)) V i p) bl =
81  Error ? [MSG BadFunction].
82#F #V #i #p #bl #EQbl whd in match fetch_internal_function;
83normalize nodelta >fetch_function_no_zero [2: assumption] %
84qed.
85
86lemma fetch_internal_function_no_minus_one :
87∀F,V,i,p,bl.
88  block_id (pi1 … bl) = -1 →
89  fetch_internal_function ?
90  (globalenv (λvars.fundef (F vars)) V i p) bl =
91  Error ? [MSG BadFunction].
92#F #V #i #p #bl #EQbl whd in match fetch_internal_function;
93normalize nodelta >fetch_function_no_minus_one [2: assumption] %
94qed.
95
96include "joint/Traces.ma".
97
98lemma fetch_statement_no_zero :
99∀pars,prog,stack_size,pc.
100block_id(pi1 … (pc_block pc)) = 0 →
101fetch_statement pars (prog_var_names … prog)
102(ev_genv (mk_prog_params pars prog stack_size)) pc =
103Error ? [MSG BadFunction].
104#pars #vars #ge #pc #EQpc whd in match fetch_statement; normalize nodelta
105>fetch_internal_function_no_zero [2: assumption] %
106qed.
107
108lemma fetch_statement_no_minus_one :
109∀pars,prog,stack_size,pc.
110block_id(pi1 … (pc_block pc)) = -1 →
111fetch_statement pars (prog_var_names … prog)
112(ev_genv (mk_prog_params pars prog stack_size)) pc =
113Error ? [MSG BadFunction].
114#pars #vars #ge #pc #EQpc whd in match fetch_statement; normalize nodelta
115>fetch_internal_function_no_minus_one [2: assumption] %
116qed.
117
118lemma fetch_function_transf_commute :
119 ∀A,B,V,init.∀prog_in : program A V.
120 ∀trans : ∀vars.A vars → B vars.
121 let prog_out ≝ transform_program … prog_in trans in
122 ∀bl.
123 fetch_function … (globalenv … init prog_out) bl =
124 ! 〈i,f〉 ← fetch_function … (globalenv … init prog_in) bl;
125 return 〈i,trans … f〉.
126#A #B #V #init #p #trans #bl whd in match fetch_function; normalize nodelta
127>(symbol_for_block_transf … trans bl) cases(symbol_for_block ???) [%]
128#i >m_return_bind >m_return_bind >(find_funct_ptr_transf_commute … trans bl)
129cases(find_funct_ptr ???) [%] #f %
130qed.
131
132lemma fetch_internal_function_transf_commute :
133  ∀A,B,init.∀prog_in : program (λvars.fundef (A vars)) ℕ.
134 ∀trans : ∀vars.A vars → B vars.
135 let prog_out ≝ transform_program … prog_in (λvars.transf_fundef … (trans vars)) in
136 ∀bl.
137 fetch_internal_function … (globalenv … init prog_out) bl =
138 ! 〈i,f〉 ← fetch_internal_function … (globalenv … init prog_in) bl;
139 return 〈i,trans … f〉.
140#A #B #init #p #trans #bl whd in match fetch_internal_function; normalize nodelta
141>(fetch_function_transf_commute … p … bl) cases(fetch_function ???) [2: #e %]
142* #i * #f %
143qed.
Note: See TracBrowser for help on using the repository browser.