source: src/common/extraGlobalenvs.ma @ 2476

include "common/AST.ma".
include "common/Globalenvs.ma".

(* TODO: need this for global env *)
axiom find_funct_ptr_symbol_inversion:
    ∀F,V,init. ∀p: program F V.
    ∀id: ident. ∀b: block. ∀f: F ?.
    find_symbol ? (globalenv ?? init p) id = Some ? b →
    find_funct_ptr ? (globalenv ?? init p) b = Some ? f →
    In … (prog_funct ?? p) 〈id, f〉.

axiom find_funct_ptr_exists:
    ∀F,V,init. ∀p: program F V. ∀id: ident. ∀f: F ?.
    In … (prog_funct ?? p) 〈id, f〉 →
    ∃b. find_symbol ? (globalenv ?? init p) id = Some ? b
      ∧ find_funct_ptr ? (globalenv ?? init p) b = Some ? f.

axiom find_symbol_exists:
    ∀F,V,init. ∀p: program F V.
           ∀id: ident. ∀r,v.
    In ? (prog_vars ?? p) 〈〈id, r〉, v〉 →
    ∃b. find_symbol ? (globalenv ?? init p) id = Some ? b.

definition is_internal_function_of_program :
  ∀A,B.program (λvars.fundef (A vars)) B → ident → Prop ≝
  λA,B,prog,i.∃ifd.In … (prog_funct ?? prog) 〈i, Internal ? ifd〉.

definition is_function ≝ λF.λge : genv_t F.
  λi : ident.∃fd.
    ! bl ← find_symbol … ge i ;
    find_funct_ptr … ge bl = Some ? fd.

definition funct_of_ident : ∀F,ge.
  ident → option (Σi.is_function F ge i)
≝ λF,ge,i.
match ?
return λx.! bl ← find_symbol … ge i ;
    find_funct_ptr … ge bl = x → ?
with
[ Some fd ⇒ λprf.return «i, ex_intro ?? fd prf»
| None ⇒ λ_.None ?
] (refl …).

lemma symbol_of_function_block_ok :
  ∀F,ge,b,prf.symbol_for_block F ge b = Some ? (symbol_of_function_block F ge b prf).
#F #ge #b #FFP
cut (∀A,B : Type[0].∀P : B → Prop.∀x : option A.∀c1,c2.
  (∀v.∀prf : x = Some ? v.P (c1 v prf)) →
  (∀prf:x = None ?.P (c2 prf)) →
  P (match x return λy.x = y → ? with
     [ Some v ⇒ λprf.c1 v prf | None ⇒ λprf.c2 prf]
     (refl …))) [ #A #B #P * // ] #aux
whd in ⊢ (???(??%)); @aux [//] #H
generalize in match (? : False); *
qed.

definition funct_of_block : ∀F,ge.
  block → option  (Σi.is_function F ge i) ≝
λF,ge,bl.
   match find_funct_ptr … ge bl
   return λx.find_funct_ptr … ge bl = x → ? with
   [ Some fd ⇒ λprf.return mk_Sig
        ident (λi.is_function F ge i)
        (symbol_of_function_block … ge bl ?)
        (ex_intro … fd ?)
   | None ⇒ λ_.None ?
   ] (refl …).
[ >(symbol_of_block_rev … (symbol_of_function_block_ok ? ge bl ?)) @prf
| >prf % #ABS destruct(ABS)
]
qed.

definition block_of_funct ≝ λF,ge.
  λi : Σi.is_function F ge i.
  match find_symbol … ge i return λx.(∃fd.!bl ← x; ? = ?) → ? with
  [ Some bl ⇒ λ_.bl
  | None ⇒ λprf.⊥
  ] (pi2 … i).
cases prf #fd normalize #ABS destruct(ABS)
qed.

definition description_of_function : ∀F,ge.(Σi.is_function F ge i) → F ≝
λF,ge,i.
match ! bl ← find_symbol … ge i ;
        find_funct_ptr … ge bl
return λx.(∃fd.x = ?) → ?
with
[ Some fd ⇒ λ_.fd
| None ⇒ λprf.⊥
] (pi2 … i).
cases prf #fd #ABS destruct
qed.

definition is_internal_function ≝ λF.λge : genv_t (fundef F).
  λi : ident.∃fd.
    ! bl ← find_symbol … ge i ;
    find_funct_ptr … ge bl = Some ? (Internal ? fd).

lemma description_of_internal_function : ∀F,ge,i,fn.
  description_of_function ? ge i = Internal F fn → is_internal_function … ge i.
#F #ge * #i * #fd #EQ
#fn whd in ⊢ (??%?→?); >EQ normalize nodelta #EQ' >EQ' in EQ; #EQ
%{EQ}
qed.

definition int_funct_of_block : ∀F,ge.
  block → option (Σi.is_internal_function F ge i) ≝
  λF,ge,bl.
  ! f ← funct_of_block … ge bl ;
  match ?
  return λx.description_of_function … f = x → option (Σi.is_internal_function … ge i)
  with
  [ Internal fn ⇒ λprf.return «pi1 … f, ?»
  | External fn ⇒ λ_.None ?
  ] (refl …).
@(description_of_internal_function … prf)
qed.

lemma internal_function_is_function : ∀F,ge,i.
  is_internal_function F ge i → is_function … ge i.
#F #ge #i * #fn #prf %{prf} qed.

definition if_of_function : ∀F,ge.(Σi.is_internal_function F ge i) → F ≝
λF,ge,i.
match ! bl ← find_symbol … ge i ;
        find_funct_ptr … ge bl
return λx.(∃fn.x = ?) → ?
with
[ Some fd ⇒
  match fd return λx.(∃fn.Some ? x = ?) → ? with
  [ Internal fn ⇒ λ_.fn
  | External _ ⇒ λprf.⊥
  ]
| None ⇒ λprf.⊥
] (pi2 … i).
cases prf #fn #ABS destruct
qed.

lemma is_internal_function_of_program_ok :
  ∀A,B,init.∀prog:program (λvars.fundef (A vars)) B.∀i.
  is_internal_function … (globalenv ?? init prog) i →
  is_internal_function_of_program ?? prog i.
#A #B #init #prog #i whd in ⊢ (%→%); * #ifn
lapply (refl … (find_symbol … i))
[3: elim (find_symbol … i) in ⊢ (???%→%);
  [#_ #ABS normalize in ABS; destruct(ABS)]
|*:]
#bl #EQbl >m_return_bind #EQfind %{ifn}
@(find_funct_ptr_symbol_inversion … EQbl EQfind)
qed.

lemma ok_is_internal_function_of_program :
  ∀A,B,init.∀prog:program (λvars.fundef (A vars)) B.∀i.
  is_internal_function_of_program … prog i →
  is_internal_function ? (globalenv ?? init prog) i.
#A #B #init #prog #i whd in ⊢ (%→%); * #ifn #H
elim (find_funct_ptr_exists … init … H)
#bl * #EQ1 #EQ2 %{ifn} >EQ1 @EQ2 qed.

lemma Exists_find : ∀A,B,P,f,l.(∀x.P x → f x ≠ None ?) → Exists ? P l →
  find A B f l ≠ None ?.
#A #B #P #f #l #H elim l -l [ * ] normalize
#hd #tl #IH *
[ #Phd >(opt_to_opt_safe … (H … Phd)) normalize nodelta % #ABS destruct(ABS)
| #Ptl elim (f hd)
  [ @(IH Ptl)
  | #x % normalize #ABS destruct(ABS)
  ]
]
qed.

definition prog_if_of_function :
  ∀F,V,prog.
  (Σi.is_internal_function_of_program F V prog i) → F ? ≝
λF,V,prog,i.opt_safe ? (find ??
  (λpr.if eq_identifier ? (\fst pr) i then
    match \snd pr with
    [ Internal x ⇒ return x
    | External _ ⇒ None ?
    ]
  else None ?)
  (prog_funct … prog)) ?.
@hide_prf
cases i -i #i * #ifn #prf
@(Exists_find … prf)
* #i' #fn' #EQ destruct(EQ) >eq_identifier_refl normalize nodelta
% normalize in ⊢ (??%?→?); #ABS destruct(ABS)
qed.

definition if_in_global_env_to_if_in_prog :
  ∀A,B,init.∀prog:program (λvars.fundef (A vars)) B.
  (Σi.is_internal_function ? (globalenv ?? init prog) i) → 
  Σi.is_internal_function_of_program ?? prog i ≝
  λA,B,init,prog,f.«f, is_internal_function_of_program_ok … (pi2 … f)».

lemma if_propagate :
∀A_in,A_out,B.
∀trans.
∀prog_in : program (λvars.fundef (A_in vars)) B.
let prog_out : program (λvars.fundef (A_out vars)) B ≝
  transform_program … prog_in (λvars.transf_fundef … (trans vars)) in
∀i.is_internal_function_of_program … prog_in i →
is_internal_function_of_program … prog_out i.
#A_in #A_out #B #trans #prog_in #ident
* #ifn #H %{(trans … ifn)}
@(Exists_map … H) * #id #fn #EQ destruct(EQ) % qed.

lemma block_of_funct_ident_is_code : ∀F,ge,i.
  block_region (block_of_funct F ge i) = Code.
#F #ge * #i * #fd
whd in ⊢ (?→??(?%)?);
cases (find_symbol ???)
[ #ABS normalize in ABS; destruct(ABS) ]
#bl normalize nodelta >m_return_bind
whd in ⊢ (??%?→?); cases (block_region bl)
[ #ABS normalize in ABS; destruct(ABS) ]
#_ %
qed.


lemma find_map : ∀A,B,C,f,g,l.find B C f (map A B g l) = find A C (λx.f (g x)) l.
#A #B #C #f #g #l elim l -l [%] #hd #tl #IH normalize >IH % qed.

lemma find_bind : ∀A,B,C,f,g,l.
  find A C (λx.! y ← f x ; return g y) l = ! y ← find A B f l ; return g y.
#A #B #C #f #g #l elim l -l
[%]
#hd #tl #IH
whd in match (find ??? (hd::tl)) in ⊢ (??%%);
cases (f hd) [ @IH ] #x % qed.

lemma find_ext_eq : ∀A,B,f,g,l.(∀x.f x = g x) → find A B f l = find A B g l.
#A #B #f #g #l #H elim l -l [%] #hd #tl #IH normalize >H >IH % qed. 

lemma prog_if_of_function_transform :
  ∀A,B,V,trans.∀prog_in : program (λvars.fundef (A vars)) V.
  let prog_out : program (λvars.fundef (B vars)) V≝ 
    transform_program … prog_in (λvars.transf_fundef … (trans vars)) in
  ∀i1,i2.pi1 ?? i1 = pi1 ?? i2 →
  prog_if_of_function ?? prog_out i1 = trans … (prog_if_of_function ?? prog_in i2).
#A #B #V #trans #prog * #i1 #i_prf1 * #i #i_prf2 #EQ
change with (opt_safe ??? = ?)
@opt_safe_elim #ifn >find_map
cut (∀vars.∀x.
  if eq_identifier ? (\fst x) i1 then
    match transf_fundef … (trans vars) (\snd x) with
    [ Internal x ⇒ return x
    | _ ⇒ None ?
    ] else None ? =
  ! y ← if eq_identifier ? (\fst x) i1 then
        match \snd x with
        [ Internal x ⇒ return x
        | _ ⇒ None ?
        ] else None ? ;
  return trans vars y)
[ #vars * #id * #fn whd in match transf_fundef; normalize nodelta
  cases (eq_identifier ???) % ] #H
>(find_ext_eq … (H ?)) >find_bind
#EQfind
change with (? = trans ? (opt_safe ???))
@opt_safe_elim #ifn' #EQfind' destruct(EQ)
>EQfind' in EQfind; >m_return_bind whd in ⊢ (??%?→?); #EQ destruct(EQ) %
qed.