[2783] | 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 | |
---|
| 15 | include "joint/joint_semantics.ma". |
---|
| 16 | include "common/ExtraMonads.ma". |
---|
| 17 | |
---|
| 18 | lemma 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 // |
---|
| 27 | qed. |
---|
| 28 | |
---|
| 29 | lemma 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 // |
---|
| 38 | qed. |
---|
| 39 | |
---|
| 40 | lemma 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) % |
---|
| 57 | qed. |
---|
| 58 | |
---|
| 59 | |
---|
| 60 | lemma 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) % |
---|
| 74 | qed. |
---|
| 75 | |
---|
| 76 | lemma 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; |
---|
| 83 | normalize nodelta >fetch_function_no_zero [2: assumption] % |
---|
| 84 | qed. |
---|
| 85 | |
---|
| 86 | lemma 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; |
---|
| 93 | normalize nodelta >fetch_function_no_minus_one [2: assumption] % |
---|
| 94 | qed. |
---|
| 95 | |
---|
| 96 | include "joint/Traces.ma". |
---|
| 97 | |
---|
| 98 | lemma fetch_statement_no_zero : |
---|
| 99 | ∀pars,prog,stack_size,pc. |
---|
| 100 | block_id(pi1 … (pc_block pc)) = 0 → |
---|
| 101 | fetch_statement pars (prog_var_names … prog) |
---|
| 102 | (ev_genv (mk_prog_params pars prog stack_size)) pc = |
---|
| 103 | Error ? [MSG BadFunction]. |
---|
| 104 | #pars #vars #ge #pc #EQpc whd in match fetch_statement; normalize nodelta |
---|
| 105 | >fetch_internal_function_no_zero [2: assumption] % |
---|
| 106 | qed. |
---|
| 107 | |
---|
| 108 | lemma fetch_statement_no_minus_one : |
---|
| 109 | ∀pars,prog,stack_size,pc. |
---|
| 110 | block_id(pi1 … (pc_block pc)) = -1 → |
---|
| 111 | fetch_statement pars (prog_var_names … prog) |
---|
| 112 | (ev_genv (mk_prog_params pars prog stack_size)) pc = |
---|
| 113 | Error ? [MSG BadFunction]. |
---|
| 114 | #pars #vars #ge #pc #EQpc whd in match fetch_statement; normalize nodelta |
---|
| 115 | >fetch_internal_function_no_minus_one [2: assumption] % |
---|
| 116 | qed. |
---|
| 117 | |
---|
| 118 | lemma 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) |
---|
| 129 | cases(find_funct_ptr ???) [%] #f % |
---|
| 130 | qed. |
---|
| 131 | |
---|
| 132 | lemma 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 % |
---|
| 143 | qed. |
---|