Changeset 2478 for src/common

Timestamp:

Nov 20, 2012, 2:28:06 PM (8 years ago)

Author:

tranquil

Message:

unified is_internal_function_of_program and is_internal_function

File:

• src/common/extraGlobalenvs.ma (modified) (6 diffs)

src/common/extraGlobalenvs.ma

@@ -2 +2 @@
 include "common/Globalenvs.ma".
 
-(* TODO: need this for global env *)
+(* 
 axiom find_funct_ptr_symbol_inversion:
     ∀F,V,init. ∀p: program F V.
@@ -21 +21 @@
     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.
@@ -30 +27 @@
     ! 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.
@@ -92 +98 @@
 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.
@@ -137 +138 @@
 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.
+∀A_in,A_out.
 ∀trans.
-∀prog_in : program (λvars.fundef (A_in vars)) B.
-let prog_out : program (λvars.fundef (A_out vars)) B ≝
+∀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 #B #trans #prog_in #ident
-* #ifn #H %{(trans … ifn)}
-@(Exists_map … H) * #id #fn #EQ destruct(EQ) % qed.
+#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.
@@ -218 +167 @@
 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≝ 
+  ∀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
-  ∀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) %
+  ∀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.