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

(* 
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_function ≝ λF.λge : genv_t F.
  λi : ident.∃fd.
    ! bl ← find_symbol … ge i ;
    find_funct_ptr … ge bl = Some ? fd.

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).

definition is_internal_function_of_program :
  ∀A.program (λvars.fundef (A vars)) ℕ → ident → Prop ≝
  λA,prog,i.is_internal_function … (globalenv_noinit … prog) i.

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.

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 if_propagate :
∀A_in,A_out.
∀trans.
∀prog_in : program (λvars.fundef (A_in vars)) ℕ.
let prog_out : program (λvars.fundef (A_out vars)) ℕ ≝
  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 #trans #prog_in #ident
* #ifn
inversion (find_symbol ???) [ #_ #ABS whd in ABS : (??%%); destruct(ABS) ]
#bl #EQfind >m_return_bind #EQfunct_ptr
%{(trans … ifn)}
>find_symbol_transf >EQfind >m_return_bind
>(find_funct_ptr_transf … EQfunct_ptr) %
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 prog_if_of_function_transform :
  ∀A,B,trans.∀prog_in : program (λvars.fundef (A vars)) ℕ.
  let prog_out : program (λvars.fundef (B vars)) ℕ ≝ 
    transform_program … prog_in (λvars.transf_fundef … (trans vars)) in
  ∀i_out : Σi.is_internal_function_of_program … prog_out i.
  ∀i_in : Σi.is_internal_function_of_program … prog_in i.
  pi1 … i_out = pi1 … i_in →
  if_of_function … i_out = trans … (if_of_function … i_in).
#A #B #trans #prog * #i1 #i_prf1 * #i2 #i_prf2 #EQ destruct(EQ)
cut (∀A,B : Type[0].∀Q : option A → Prop.∀P : B → Prop.
  ∀m.∀prf : Q m.∀f1,f2.
  (∀x,prf.m = Some ? x → P (f1 x prf)) →
  (∀prf.m = None ? → P (f2 prf)) →
  P (match m return λx.Q x → ? with [ Some x ⇒ f1 x | None ⇒ f2 ] prf))
  [ #A #B #Q #P * /2 by / ] #aux
whd in ⊢ (??%?); @aux
[2: #prf #EQ generalize in match (? : False); * ]
#fd * #ifn #EQ1 #EQ destruct normalize nodelta
whd in ⊢ (???(??%)); @aux
[2: #prf #EQ generalize in match (? : False); * ]
#fd' * #ifn' #EQ1' #EQ' destruct normalize nodelta
inversion (find_symbol ???) in EQ'; [ #_ #ABS whd in ABS: (??%%); destruct ]
#bl #EQfind >m_return_bind #EQfunct
>find_symbol_transf in EQ; >EQfind >m_return_bind
>(find_funct_ptr_transf … EQfunct) #EQ'' destruct %
qed.
*)

include alias "common/PositiveMap.ma".

lemma add_functs_functions_miss : ∀F. ∀ge : genv_t F.∀ l.∀ id.
id < (nextfunction ? ge) → 
lookup_opt … id (functions ? ge) = None ? → 
lookup_opt … id (functions … (add_functs F ge l)) = None ?.
#F #ge #l #id whd in match add_functs; normalize nodelta
elim l -l [ #_ normalize //]
* #id1 #f1 #tl #IND #H #H1 whd in match (foldr ?????);
>lookup_opt_insert_miss [ inversion(lookup_opt ? ? ?) [ #_ %]
#f1 #H3 <(drop_fn_lfn … f1 H3) @(IND H H1)
| cut(nextfunction F ge ≤ nextfunction F (foldr … (add_funct F) ge tl))
[elim tl [normalize //]
#x #tl2 whd in match (foldr ?????) in ⊢ (? → %); #H %2{H} ]
#H2 lapply(transitive_le … H H2) @lt_to_not_eq
qed.

lemma add_globals_functions_miss : ∀F,V,init. ∀gem : genv_t F × mem.∀ id,l.
lookup_opt … id (functions ? (\fst gem)) = None ? → 
lookup_opt … id (functions … (\fst (add_globals F V init gem l))) = None ?. 
#F #V #init * #ge #m #id #l lapply ge -ge lapply m -m elim l [ #ge #m #H @H]
** #x1 #x2 #x3 #tl whd in match add_globals;
normalize nodelta #IND #m #ge #H whd in match (foldl ?????); normalize nodelta
cases(alloc m ? ? (*x2*)) #m1 #bl1 normalize nodelta @IND whd in match add_symbol;
normalize nodelta inversion(lookup_opt ? ? ?) [ #_ %]
#f1 #H3 <(drop_fn_lfn … f1 H3) assumption
qed.

  
lemma globalenv_no_minus_one :
 ∀F,V,i,p.
  find_funct_ptr … (globalenv F V i p) (mk_block (*Code*) (-1)) = None ?. 
#F #V #i #p
whd in match find_funct_ptr; normalize nodelta
whd in match globalenv; 
whd in match globalenv_allocmem; normalize nodelta
@add_globals_functions_miss @add_functs_functions_miss normalize //
qed.

lemma globalenv_no_zero :
 ∀F,V,i,p.
  find_funct_ptr … (globalenv F V i p) (mk_block (*Code*) OZ) = None ?. // 
qed.