(**************************************************************************)
(*       ___                                                              *)
(*      ||M||                                                             *)
(*      ||A||       A project by Andrea Asperti                           *)
(*      ||T||                                                             *)
(*      ||I||       Developers:                                           *)
(*      ||T||         The HELM team.                                      *)
(*      ||A||         http://helm.cs.unibo.it                             *)
(*      \   /                                                             *)
(*       \ /        This file is distributed under the terms of the       *)
(*        v         GNU General Public License Version 2                  *)
(*                                                                        *)
(**************************************************************************)

include "joint/joint_semantics.ma".
include "common/ExtraMonads.ma".

lemma fetch_function_no_minus_one :
  ∀F,V,i,p,bl.
  block_id (pi1 … bl) = -1 →
  fetch_function … (globalenv (λvars.fundef (F vars)) V i p)
    bl = Error … [MSG BadFunction].
 #F#V#i#p ** #r #id #EQ1 destruct
  whd in match fetch_function; normalize nodelta
  >globalenv_no_minus_one
  cases (symbol_for_block ???) normalize //
qed.

lemma fetch_function_no_zero :
 ∀F,V,i,p,bl.
  block_id (pi1 … bl) = 0 →
  fetch_function … (globalenv (λvars.fundef (F vars)) V i p)
    bl = Error … [MSG BadFunction].
 #F#V#i#p ** #r #id #EQ1 destruct
  whd in match fetch_function; normalize nodelta
  >globalenv_no_zero
  cases (symbol_for_block ???) normalize //
qed.

lemma fetch_function_transf :
 ∀A,B,V,init.∀prog_in : program A V.
 ∀trans : ∀vars.A vars → B vars.
 let prog_out ≝ transform_program … prog_in trans in
 ∀bl,i,f.
 fetch_function … (globalenv … init prog_in) bl = 
  return 〈i, f〉
→ fetch_function … (globalenv … init prog_out) bl =
  return 〈i, trans … f〉.
#A #B #V #init #prog_in #trans #bl #i #f
 whd in match fetch_function; normalize nodelta
 #H lapply (opt_eq_from_res ???? H) -H
 #H @('bind_inversion H) -H #id #eq_symbol_for_block
 #H @('bind_inversion H) -H #fd #eq_find_funct
 whd in ⊢ (??%?→?); #EQ destruct(EQ)
 >(symbol_for_block_transf … trans) >eq_symbol_for_block >m_return_bind
 >(find_funct_ptr_transf A B …  eq_find_funct) %
qed.


lemma fetch_internal_function_transf :
 ∀A,B.∀prog_in : program (λvars.fundef (A vars)) ℕ.
 ∀trans : ∀vars.A vars → B vars.
 let prog_out ≝ transform_program … prog_in (λvars.transf_fundef … (trans vars)) in
 ∀bl,i,f.
 fetch_internal_function … (globalenv_noinit … prog_in) bl = 
  return 〈i, f〉
→ fetch_internal_function … (globalenv_noinit … prog_out) bl =
  return 〈i, trans … f〉.
#A #B #prog #trans #bl #i #f
 whd in match fetch_internal_function; normalize nodelta
 #H @('bind_inversion H) * #id * #fd normalize nodelta #EQfetch
 whd in ⊢ (??%%→?); #EQ destruct(EQ)
 >(fetch_function_transf … EQfetch) %
qed.

lemma fetch_internal_function_no_zero :
∀F,V,i,p,bl.
  block_id (pi1 … bl) = 0 →
  fetch_internal_function ?
  (globalenv (λvars.fundef (F vars)) V i p) bl = 
  Error ? [MSG BadFunction].
#F #V #i #p #bl #EQbl whd in match fetch_internal_function; 
normalize nodelta >fetch_function_no_zero [2: assumption] %
qed.

lemma fetch_internal_function_no_minus_one :
∀F,V,i,p,bl.
  block_id (pi1 … bl) = -1 →
  fetch_internal_function ?
  (globalenv (λvars.fundef (F vars)) V i p) bl = 
  Error ? [MSG BadFunction].
#F #V #i #p #bl #EQbl whd in match fetch_internal_function; 
normalize nodelta >fetch_function_no_minus_one [2: assumption] %
qed.

include "joint/Traces.ma".

lemma fetch_statement_no_zero : 
∀pars,prog,stack_size,pc.
block_id(pi1 … (pc_block pc)) = 0 →
fetch_statement pars (prog_var_names … prog) 
(ev_genv (mk_prog_params pars prog stack_size)) pc = 
Error ? [MSG BadFunction].
#pars #vars #ge #pc #EQpc whd in match fetch_statement; normalize nodelta
>fetch_internal_function_no_zero [2: assumption] %
qed.

lemma fetch_statement_no_minus_one : 
∀pars,prog,stack_size,pc.
block_id(pi1 … (pc_block pc)) = -1 →
fetch_statement pars (prog_var_names … prog) 
(ev_genv (mk_prog_params pars prog stack_size)) pc = 
Error ? [MSG BadFunction].
#pars #vars #ge #pc #EQpc whd in match fetch_statement; normalize nodelta
>fetch_internal_function_no_minus_one [2: assumption] %
qed.

lemma fetch_function_transf_commute :
 ∀A,B,V,init.∀prog_in : program A V.
 ∀trans : ∀vars.A vars → B vars.
 let prog_out ≝ transform_program … prog_in trans in
 ∀bl.
 fetch_function … (globalenv … init prog_out) bl =
 ! 〈i,f〉 ← fetch_function … (globalenv … init prog_in) bl;
 return 〈i,trans … f〉.
#A #B #V #init #p #trans #bl whd in match fetch_function; normalize nodelta
>(symbol_for_block_transf … trans bl) cases(symbol_for_block ???) [%]
#i >m_return_bind >m_return_bind >(find_funct_ptr_transf_commute … trans bl)
cases(find_funct_ptr ???) [%] #f %
qed.

lemma fetch_internal_function_transf_commute :
  ∀A,B,init.∀prog_in : program (λvars.fundef (A vars)) ℕ.
 ∀trans : ∀vars.A vars → B vars.
 let prog_out ≝ transform_program … prog_in (λvars.transf_fundef … (trans vars)) in
 ∀bl.
 fetch_internal_function … (globalenv … init prog_out) bl =
 ! 〈i,f〉 ← fetch_internal_function … (globalenv … init prog_in) bl;
 return 〈i,trans … f〉.
#A #B #init #p #trans #bl whd in match fetch_internal_function; normalize nodelta
>(fetch_function_transf_commute … p … bl) cases(fetch_function ???) [2: #e %]
* #i * #f %
qed.