Changeset 487 for Deliverables/D3.1/Csemantics/Globalenvs.ma
 Timestamp:
 Feb 9, 2011, 11:49:17 AM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

Deliverables/D3.1/Csemantics/Globalenvs.ma
r485 r487 40 40 41 41 (* FIXME: unimplemented stuff in AST.ma 42 naxiom transform_partial_program: ∀A,B,V:Type. (A → res B) → program A V → res (program B V).43 naxiom transform_partial_program2: ∀A,B,V,W:Type. (A → res B) → (V → res W) → program A V → res (program B W).44 naxiom match_program: ∀A,B,V,W:Type. program A V → program B W → Prop.42 axiom transform_partial_program: ∀A,B,V:Type[0]. (A → res B) → program A V → res (program B V). 43 axiom transform_partial_program2: ∀A,B,V,W:Type[0]. (A → res B) → (V → res W) → program A V → res (program B W). 44 axiom match_program: ∀A,B,V,W:Type[0]. program A V → program B W → Prop. 45 45 *) 46 46 47 nrecord GENV : Type[2] ≝ {47 record GENV : Type[2] ≝ { 48 48 (* * ** Types and operations *) 49 49 50 genv_t : Type → Type;50 genv_t : Type[0] → Type[0]; 51 51 (* * The type of global environments. The parameter [F] is the type 52 52 of function descriptions. *) 53 53 54 globalenv: ∀F,V: Type . program F V → res (genv_t F);54 globalenv: ∀F,V: Type[0]. program F V → res (genv_t F); 55 55 (* * Return the global environment for the given program. *) 56 56 57 init_mem: ∀F,V: Type . program F V → res mem;57 init_mem: ∀F,V: Type[0]. program F V → res mem; 58 58 (* * Return the initial memory state for the given program. *) 59 59 60 find_funct_ptr: ∀F: Type . genv_t F → block → option F;60 find_funct_ptr: ∀F: Type[0]. genv_t F → block → option F; 61 61 (* * Return the function description associated with the given address, 62 62 if any. *) 63 63 64 find_funct: ∀F: Type . genv_t F → val → option F;64 find_funct: ∀F: Type[0]. genv_t F → val → option F; 65 65 (* * Same as [find_funct_ptr] but the function address is given as 66 66 a value, which must be a pointer with offset 0. *) 67 67 68 find_symbol: ∀F: Type . genv_t F → ident → option (region × block)(*;68 find_symbol: ∀F: Type[0]. genv_t F → ident → option (region × block)(*; 69 69 (* * Return the address of the given global symbol, if any. *) 70 70 … … 72 72 73 73 find_funct_inv: 74 ∀F: Type . ∀ge: genv_t F. ∀v: val. ∀f: F.74 ∀F: Type[0]. ∀ge: genv_t F. ∀v: val. ∀f: F. 75 75 find_funct ? ge v = Some ? f → ∃b. v = Vptr Code b zero; 76 76 find_funct_find_funct_ptr: 77 ∀F: Type . ∀ge: genv_t F. ∀sp. ∀b: block.77 ∀F: Type[0]. ∀ge: genv_t F. ∀sp. ∀b: block. 78 78 find_funct ? ge (Vptr sp b zero) = find_funct_ptr ? ge b; 79 79 80 80 find_symbol_exists: 81 ∀F,V: Type . ∀p: program F V.81 ∀F,V: Type[0]. ∀p: program F V. 82 82 ∀id: ident. ∀sp. ∀init: list init_data. ∀v: V. 83 83 in_list ? 〈〈〈id, init〉,sp〉, v〉 (prog_vars ?? p) → 84 84 ∃b. find_symbol ? (globalenv ?? p) id = Some ? b; 85 85 find_funct_ptr_exists: 86 ∀F,V: Type . ∀p: program F V. ∀id: ident. ∀f: F.86 ∀F,V: Type[0]. ∀p: program F V. ∀id: ident. ∀f: F. 87 87 list_norepet ? (prog_funct_names ?? p) → 88 88 list_disjoint ? (prog_funct_names ?? p) (prog_var_names ?? p) → … … 92 92 93 93 find_funct_ptr_inversion: 94 ∀F,V: Type . ∀P: F → Prop. ∀p: program F V. ∀b: block. ∀f: F.94 ∀F,V: Type[0]. ∀P: F → Prop. ∀p: program F V. ∀b: block. ∀f: F. 95 95 find_funct_ptr ? (globalenv ?? p) b = Some ? f → 96 96 ∃id. in_list ? 〈id, f〉 (prog_funct ?? p); 97 97 find_funct_inversion: 98 ∀F,V: Type . ∀P: F → Prop. ∀p: program F V. ∀v: val. ∀f: F.98 ∀F,V: Type[0]. ∀P: F → Prop. ∀p: program F V. ∀v: val. ∀f: F. 99 99 find_funct ? (globalenv ?? p) v = Some ? f → 100 100 ∃id. in_list ? 〈id, f〉 (prog_funct ?? p); 101 101 find_funct_ptr_symbol_inversion: 102 ∀F,V: Type . ∀p: program F V. ∀id: ident. ∀sp. ∀b: block. ∀f: F.102 ∀F,V: Type[0]. ∀p: program F V. ∀id: ident. ∀sp. ∀b: block. ∀f: F. 103 103 find_symbol ? (globalenv ?? p) id = Some ? 〈sp,b〉 → 104 104 find_funct_ptr ? (globalenv ?? p) b = Some ? f → … … 106 106 107 107 find_funct_ptr_prop: 108 ∀F,V: Type . ∀P: F → Prop. ∀p: program F V. ∀b: block. ∀f: F.108 ∀F,V: Type[0]. ∀P: F → Prop. ∀p: program F V. ∀b: block. ∀f: F. 109 109 (∀id,f. in_list ? 〈id, f〉 (prog_funct ?? p) → P f) → 110 110 find_funct_ptr ? (globalenv ?? p) b = Some ? f → 111 111 P f; 112 112 find_funct_prop: 113 ∀F,V: Type . ∀P: F → Prop. ∀p: program F V. ∀v: val. ∀f: F.113 ∀F,V: Type[0]. ∀P: F → Prop. ∀p: program F V. ∀v: val. ∀f: F. 114 114 (∀id,f. in_list ? 〈id, f〉 (prog_funct ?? p) → P f) → 115 115 find_funct ? (globalenv ?? p) v = Some ? f → … … 117 117 118 118 initmem_nullptr: 119 ∀F,V: Type . ∀p: program F V.119 ∀F,V: Type[0]. ∀p: program F V. 120 120 let m ≝ init_mem ?? p in 121 121 valid_block m nullptr ∧ 122 122 (blocks m) nullptr = empty_block 0 0 Any; 123 123 (* initmem_inject_neutral: 124 ∀F,V: Type . ∀p: program F V.124 ∀F,V: Type[0]. ∀p: program F V. 125 125 mem_inject_neutral (init_mem ?? p);*) 126 126 find_funct_ptr_negative: 127 ∀F,V: Type . ∀p: program F V. ∀b: block. ∀f: F.127 ∀F,V: Type[0]. ∀p: program F V. ∀b: block. ∀f: F. 128 128 find_funct_ptr ? (globalenv ?? p) b = Some ? f → b < 0; 129 129 find_symbol_not_fresh: 130 ∀F,V: Type . ∀p: program F V. ∀id: ident. ∀sp. ∀b: block.130 ∀F,V: Type[0]. ∀p: program F V. ∀id: ident. ∀sp. ∀b: block. 131 131 find_symbol ? (globalenv ?? p) id = Some ? 〈sp,b〉 → b < nextblock (init_mem ?? p); 132 132 find_symbol_not_nullptr: 133 ∀F,V: Type . ∀p: program F V. ∀id: ident. ∀sp. ∀b: block.133 ∀F,V: Type[0]. ∀p: program F V. ∀id: ident. ∀sp. ∀b: block. 134 134 find_symbol ? (globalenv ?? p) id = Some ? 〈sp,b〉 → b ≠ nullptr; 135 135 global_addresses_distinct: 136 ∀F,V: Type . ∀p: program F V. ∀id1,id2,b1,b2.136 ∀F,V: Type[0]. ∀p: program F V. ∀id1,id2,b1,b2. 137 137 id1≠id2 → 138 138 find_symbol ? (globalenv ?? p) id1 = Some ? b1 → … … 144 144 145 145 find_funct_ptr_transf: 146 ∀A,B,V: Type . ∀transf: A → B. ∀p: program A V.146 ∀A,B,V: Type[0]. ∀transf: A → B. ∀p: program A V. 147 147 ∀b: block. ∀f: A. 148 148 find_funct_ptr ? (globalenv ?? p) b = Some ? f → 149 149 find_funct_ptr ? (globalenv ?? (transform_program … transf p)) b = Some ? (transf f); 150 150 find_funct_transf: 151 ∀A,B,V: Type . ∀transf: A → B. ∀p: program A V.151 ∀A,B,V: Type[0]. ∀transf: A → B. ∀p: program A V. 152 152 ∀v: val. ∀f: A. 153 153 find_funct ? (globalenv ?? p) v = Some ? f → 154 154 find_funct ? (globalenv ?? (transform_program … transf p)) v = Some ? (transf f); 155 155 find_symbol_transf: 156 ∀A,B,V: Type . ∀transf: A → B. ∀p: program A V.156 ∀A,B,V: Type[0]. ∀transf: A → B. ∀p: program A V. 157 157 ∀s: ident. 158 158 find_symbol ? (globalenv ?? (transform_program … transf p)) s = 159 159 find_symbol ? (globalenv ?? p) s; 160 160 init_mem_transf: 161 ∀A,B,V: Type . ∀transf: A → B. ∀p: program A V.161 ∀A,B,V: Type[0]. ∀transf: A → B. ∀p: program A V. 162 162 init_mem ?? (transform_program … transf p) = init_mem ?? p; 163 163 find_funct_ptr_rev_transf: 164 ∀A,B,V: Type . ∀transf: A → B. ∀p: program A V.164 ∀A,B,V: Type[0]. ∀transf: A → B. ∀p: program A V. 165 165 ∀b : block. ∀tf : B. 166 166 find_funct_ptr ? (globalenv ?? (transform_program … transf p)) b = Some ? tf → 167 167 ∃f : A. find_funct_ptr ? (globalenv ?? p) b = Some ? f ∧ transf f = tf; 168 168 find_funct_rev_transf: 169 ∀A,B,V: Type . ∀transf: A → B. ∀p: program A V.169 ∀A,B,V: Type[0]. ∀transf: A → B. ∀p: program A V. 170 170 ∀v : val. ∀tf : B. 171 171 find_funct ? (globalenv ?? (transform_program … transf p)) v = Some ? tf → … … 176 176 177 177 find_funct_ptr_transf_partial: 178 ∀A,B,V: Type . ∀transf: A → res B. ∀p: program A V. ∀p': program B V.178 ∀A,B,V: Type[0]. ∀transf: A → res B. ∀p: program A V. ∀p': program B V. 179 179 transform_partial_program … transf p = OK ? p' → 180 180 ∀b: block. ∀f: A. … … 183 183 find_funct_ptr ? (globalenv ?? p') b = Some ? f' ∧ transf f = OK ? f'; 184 184 find_funct_transf_partial: 185 ∀A,B,V: Type . ∀transf: A → res B. ∀p: program A V. ∀p': program B V.185 ∀A,B,V: Type[0]. ∀transf: A → res B. ∀p: program A V. ∀p': program B V. 186 186 transform_partial_program … transf p = OK ? p' → 187 187 ∀v: val. ∀f: A. … … 190 190 find_funct ? (globalenv ?? p') v = Some ? f' ∧ transf f = OK ? f'; 191 191 find_symbol_transf_partial: 192 ∀A,B,V: Type . ∀transf: A → res B. ∀p: program A V. ∀p': program B V.192 ∀A,B,V: Type[0]. ∀transf: A → res B. ∀p: program A V. ∀p': program B V. 193 193 transform_partial_program … transf p = OK ? p' → 194 194 ∀s: ident. 195 195 find_symbol ? (globalenv ?? p') s = find_symbol ? (globalenv ?? p) s; 196 196 init_mem_transf_partial: 197 ∀A,B,V: Type . ∀transf: A → res B. ∀p: program A V. ∀p': program B V.197 ∀A,B,V: Type[0]. ∀transf: A → res B. ∀p: program A V. ∀p': program B V. 198 198 transform_partial_program … transf p = OK ? p' → 199 199 init_mem ?? p' = init_mem ?? p; 200 200 find_funct_ptr_rev_transf_partial: 201 ∀A,B,V: Type . ∀transf: A → res B. ∀p: program A V. ∀p': program B V.201 ∀A,B,V: Type[0]. ∀transf: A → res B. ∀p: program A V. ∀p': program B V. 202 202 transform_partial_program … transf p = OK ? p' → 203 203 ∀b : block. ∀tf : B. … … 206 206 find_funct_ptr ? (globalenv ?? p) b = Some ? f ∧ transf f = OK ? tf; 207 207 find_funct_rev_transf_partial: 208 ∀A,B,V: Type . ∀transf: A → res B. ∀p: program A V. ∀p': program B V.208 ∀A,B,V: Type[0]. ∀transf: A → res B. ∀p: program A V. ∀p': program B V. 209 209 transform_partial_program … transf p = OK ? p' → 210 210 ∀v : val. ∀tf : B. … … 214 214 215 215 find_funct_ptr_transf_partial2: 216 ∀A,B,V,W: Type . ∀transf_fun: A → res B. ∀transf_var: V → res W.216 ∀A,B,V,W: Type[0]. ∀transf_fun: A → res B. ∀transf_var: V → res W. 217 217 ∀p: program A V. ∀p': program B W. 218 218 transform_partial_program2 … transf_fun transf_var p = OK ? p' → … … 222 222 find_funct_ptr ? (globalenv ?? p') b = Some ? f' ∧ transf_fun f = OK ? f'; 223 223 find_funct_transf_partial2: 224 ∀A,B,V,W: Type . ∀transf_fun: A → res B. ∀transf_var: V → res W.224 ∀A,B,V,W: Type[0]. ∀transf_fun: A → res B. ∀transf_var: V → res W. 225 225 ∀p: program A V. ∀p': program B W. 226 226 transform_partial_program2 … transf_fun transf_var p = OK ? p' → … … 230 230 find_funct ? (globalenv ?? p') v = Some ? f' ∧ transf_fun f = OK ? f'; 231 231 find_symbol_transf_partial2: 232 ∀A,B,V,W: Type . ∀transf_fun: A → res B. ∀transf_var: V → res W.232 ∀A,B,V,W: Type[0]. ∀transf_fun: A → res B. ∀transf_var: V → res W. 233 233 ∀p: program A V. ∀p': program B W. 234 234 transform_partial_program2 … transf_fun transf_var p = OK ? p' → … … 236 236 find_symbol ? (globalenv ?? p') s = find_symbol ? (globalenv ?? p) s; 237 237 init_mem_transf_partial2: 238 ∀A,B,V,W: Type . ∀transf_fun: A → res B. ∀transf_var: V → res W.238 ∀A,B,V,W: Type[0]. ∀transf_fun: A → res B. ∀transf_var: V → res W. 239 239 ∀p: program A V. ∀p': program B W. 240 240 transform_partial_program2 … transf_fun transf_var p = OK ? p' → 241 241 init_mem ?? p' = init_mem ?? p; 242 242 find_funct_ptr_rev_transf_partial2: 243 ∀A,B,V,W: Type . ∀transf_fun: A → res B. ∀transf_var: V → res W.243 ∀A,B,V,W: Type[0]. ∀transf_fun: A → res B. ∀transf_var: V → res W. 244 244 ∀p: program A V. ∀p': program B W. 245 245 transform_partial_program2 … transf_fun transf_var p = OK ? p' → … … 249 249 find_funct_ptr ? (globalenv ?? p) b = Some ? f ∧ transf_fun f = OK ? tf; 250 250 find_funct_rev_transf_partial2: 251 ∀A,B,V,W: Type . ∀transf_fun: A → res B. ∀transf_var: V → res W.251 ∀A,B,V,W: Type[0]. ∀transf_fun: A → res B. ∀transf_var: V → res W. 252 252 ∀p: program A V. ∀p': program B W. 253 253 transform_partial_program2 … transf_fun transf_var p = OK ? p' → … … 261 261 262 262 find_funct_ptr_match: 263 ∀A,B,V,W: Type . ∀match_fun: A → B → Prop.263 ∀A,B,V,W: Type[0]. ∀match_fun: A → B → Prop. 264 264 ∀match_var: V → W → Prop. ∀p: program A V. ∀p': program B W. 265 265 match_program … match_fun match_var p p' → … … 269 269 find_funct_ptr ? (globalenv ?? p') b = Some ? tf ∧ match_fun f tf; 270 270 find_funct_ptr_rev_match: 271 ∀A,B,V,W: Type . ∀match_fun: A → B → Prop.271 ∀A,B,V,W: Type[0]. ∀match_fun: A → B → Prop. 272 272 ∀match_var: V → W → Prop. ∀p: program A V. ∀p': program B W. 273 273 match_program … match_fun match_var p p' → … … 277 277 find_funct_ptr ? (globalenv ?? p) b = Some ? f ∧ match_fun f tf; 278 278 find_funct_match: 279 ∀A,B,V,W: Type . ∀match_fun: A → B → Prop.279 ∀A,B,V,W: Type[0]. ∀match_fun: A → B → Prop. 280 280 ∀match_var: V → W → Prop. ∀p: program A V. ∀p': program B W. 281 281 match_program … match_fun match_var p p' → … … 284 284 ∃tf : B. find_funct ? (globalenv ?? p') v = Some ? tf ∧ match_fun f tf; 285 285 find_funct_rev_match: 286 ∀A,B,V,W: Type . ∀match_fun: A → B → Prop.286 ∀A,B,V,W: Type[0]. ∀match_fun: A → B → Prop. 287 287 ∀match_var: V → W → Prop. ∀p: program A V. ∀p': program B W. 288 288 match_program … match_fun match_var p p' → … … 291 291 ∃f : A. find_funct ? (globalenv ?? p) v = Some ? f ∧ match_fun f tf; 292 292 find_symbol_match: 293 ∀A,B,V,W: Type . ∀match_fun: A → B → Prop.293 ∀A,B,V,W: Type[0]. ∀match_fun: A → B → Prop. 294 294 ∀match_var: V → W → Prop. ∀p: program A V. ∀p': program B W. 295 295 match_program … match_fun match_var p p' → … … 297 297 find_symbol ? (globalenv ?? p') s = find_symbol ? (globalenv ?? p) s; 298 298 init_mem_match: 299 ∀A,B,V,W: Type . ∀match_fun: A → B → Prop.299 ∀A,B,V,W: Type[0]. ∀match_fun: A → B → Prop. 300 300 ∀match_var: V → W → Prop. ∀p: program A V. ∀p': program B W. 301 301 match_program … match_fun match_var p p' → … … 304 304 305 305 306 nlet rec foldl (A,B:Type) (f:A → B → A) (a:A) (l:list B) on l : A ≝306 let rec foldl (A,B:Type[0]) (f:A → B → A) (a:A) (l:list B) on l : A ≝ 307 307 match l with 308 308 [ nil ⇒ a … … 314 314 (* XXX: temporary definition 315 315 NB: only global functions, no global variables *) 316 nrecord genv (F:Type) : Type≝ {316 record genv (F:Type[0]) : Type[0] ≝ { 317 317 functions: block → option F; 318 318 nextfunction: Z; … … 327 327 Section GENV. 328 328 329 Variable F: Type . (* The type of functions *)329 Variable F: Type[0]. (* The type of functions *) 330 330 Variable V: Type. (* The type of information over variables *) 331 331 … … 339 339 *) 340 340 341 ndefinition add_funct : ∀F:Type. (ident × F) → genv F → genv F ≝341 definition add_funct : ∀F:Type[0]. (ident × F) → genv F → genv F ≝ 342 342 λF,name_fun,g. 343 343 let b ≝ nextfunction ? g in … … 346 346 ((*PTree.set*) λi. match ident_eq (\fst name_fun) i with [ inl _ ⇒ Some ? 〈Code,b〉  inr _ ⇒ (symbols ? g i) ]). 347 347 348 ndefinition add_symbol : ∀F:Type. ident → region → block → genv F → genv F ≝348 definition add_symbol : ∀F:Type[0]. ident → region → block → genv F → genv F ≝ 349 349 λF,name,bsp,b,g. 350 350 mk_genv F (functions ? g) … … 387 387 *) 388 388 (* Construct environment and initial memory store *) 389 ndefinition empty_mem ≝ empty. (* XXX*)390 ndefinition empty : ∀F. genv F ≝389 definition empty_mem ≝ empty. (* XXX*) 390 definition empty : ∀F. genv F ≝ 391 391 λF. mk_genv F (λ_. None ?) (1) (λ_. None ?). 392 392 (* mkgenv (ZMap.init None) (1) (PTree.empty block).*) 393 393 394 ndefinition add_functs : ∀F:Type. genv F → list (ident × F) → genv F ≝394 definition add_functs : ∀F:Type[0]. genv F → list (ident × F) → genv F ≝ 395 395 λF,init,fns. 396 396 foldr ?? (add_funct F) init fns. … … 398 398 (* init *) 399 399 400 ndefinition store_init_data : ∀F.genv F → mem → region → block → Z → init_data → option mem ≝400 definition store_init_data : ∀F.genv F → mem → region → block → Z → init_data → option mem ≝ 401 401 λF,ge,m,r,b,p,id. 402 402 match id with … … 415 415 ]. 416 416 417 ndefinition size_init_data : init_data → Z ≝417 definition size_init_data : init_data → Z ≝ 418 418 λi_data.match i_data with 419 419 [ Init_int8 _ ⇒ 1 … … 426 426  Init_addrof r _ _ ⇒ size_pointer r]. 427 427 428 nlet rec store_init_data_list (F:Type) (ge:genv F)428 let rec store_init_data_list (F:Type[0]) (ge:genv F) 429 429 (m: mem) (r: region) (b: block) (p: Z) (idl: list init_data) 430 430 on idl : option mem ≝ … … 438 438 ]. 439 439 440 ndefinition size_init_data_list : list init_data → Z ≝440 definition size_init_data_list : list init_data → Z ≝ 441 441 λi_data.foldr ?? (λi_data,sz. size_init_data i_data + sz) OZ i_data. 442 442 … … 444 444 nremark size_init_data_list_pos: 445 445 ∀i_data. OZ ≤ size_init_data_list i_data. 446 #i_data; nelim i_data;//;447 #a;#tl; ncut (OZ ≤ size_init_data a)448 ##[ ncases a;nnormalize;//;449 #x; ncases x;nnormalize;//;446 #i_data;elim i_data;//; 447 #a;#tl;cut (OZ ≤ size_init_data a) 448 ##[cases a;normalize;//; 449 #x;cases x;normalize;//; 450 450 ###Hsize;#IH;nchange in ⊢ (??%) with (size_init_data a + (foldr ??? OZ tl)); 451 ncut (size_init_data a = OZ ∨ ∃m.size_init_data a = pos m)452 ##[ ncases (size_init_data a) in Hsize IH;451 cut (size_init_data a = OZ ∨ ∃m.size_init_data a = pos m) 452 ##[cases (size_init_data a) in Hsize IH; 453 453 ##[##1,2:/3/ 454 ##n normalize;#n;#Hfalse;nelim Hfalse]455 ###Hdisc; ncases Hdisc454 ##normalize;#n;#Hfalse;elim Hfalse] 455 ###Hdisc;cases Hdisc 456 456 ##[#Heq;nrewrite > Heq;//; 457 ###Heq; ncases Heq;#x;#Heq2;nrewrite > Heq2;457 ###Heq;cases Heq;#x;#Heq2;nrewrite > Heq2; 458 458 (* TODO: arithmetics *) napply daemon] 459 459 ##] 460 460 ##] 461 nqed.461 qed. 462 462 *) 463 463 464 ndefinition alloc_init_data : mem → list init_data → region → mem × block ≝464 definition alloc_init_data : mem → list init_data → region → mem × block ≝ 465 465 λm,i_data,bcl. 466 466 〈mk_mem (update ? (nextblock m) … … 473 473 (* init *) 474 474 475 ndefinition add_globals : ∀F,V:Type.475 definition add_globals : ∀F,V:Type[0]. 476 476 genv F × mem → list (ident × (list init_data) × region × V) → 477 477 res (genv F × mem) ≝ … … 479 479 foldl ?? 480 480 (λg_st: res (genv F × mem). λid_init: ident × (list init_data) × region × V. 481 match id_init with [ mk_pair id_init1 info ⇒482 match id_init1 with [ mk_pair id_init2 r ⇒483 match id_init2 with [ mk_pair id init ⇒481 match id_init with [ pair id_init1 info ⇒ 482 match id_init1 with [ pair id_init2 r ⇒ 483 match id_init2 with [ pair id init ⇒ 484 484 do 〈g,st〉 ← g_st; 485 match alloc_init_data st init r with [ mk_pair st' b ⇒485 match alloc_init_data st init r with [ pair st' b ⇒ 486 486 let g' ≝ add_symbol ? id r b g in 487 487 do st'' ← opt_to_res ? (store_init_data_list F g' st' r b OZ init); … … 490 490 (OK ? init_env) vars. 491 491 492 ndefinition globalenv_initmem : ∀F,V:Type. program F V → res (genv F × mem) ≝492 definition globalenv_initmem : ∀F,V:Type[0]. program F V → res (genv F × mem) ≝ 493 493 λF,V,p. 494 494 add_globals F V … … 496 496 (prog_vars ?? p). 497 497 498 ndefinition globalenv_ : ∀F,V:Type. program F V → res (genv F) ≝498 definition globalenv_ : ∀F,V:Type[0]. program F V → res (genv F) ≝ 499 499 λF,V,p. 500 500 do 〈g,m〉 ← globalenv_initmem F V p; 501 501 OK ? g. 502 ndefinition init_mem_ : ∀F,V:Type. program F V → res (mem) ≝502 definition init_mem_ : ∀F,V:Type[0]. program F V → res (mem) ≝ 503 503 λF,V,p. 504 504 do 〈g,m〉 ← globalenv_initmem F V p; … … 508 508 509 509 510 ndefinition Genv : GENV ≝ mk_GENV510 definition Genv : GENV ≝ mk_GENV 511 511 genv (* genv_t *) 512 512 globalenv_ … … 523 523 . 524 524 (* 525 ##[ #A B C transf p b f; nelim p; #fns main vars;526 nelim fns;527 ##[ nwhd in match globalenv_ in ⊢ %; nwhd in match globalenv_initmem in ⊢ %; nwhd in ⊢ (??%? → ??%?); normalize; #H; ndestruct;528 ## #h t; nelim h; #fid fd; #IH; nwhd in ⊢ (??(??%?)? → ??(??%?)?);525 ##[ #A B C transf p b f; elim p; #fns main vars; 526 elim fns; 527 ##[ whd in match globalenv_ in ⊢ %; whd in match globalenv_initmem in ⊢ %; whd in ⊢ (??%? → ??%?); normalize; #H; destruct; 528 ## #h t; elim h; #fid fd; #IH; whd in ⊢ (??(??%?)? → ??(??%?)?); 529 529 nrewrite > (?:nextfunction ?? = length ? t); 530 ##[ ##2: nelim t; ##[ //; ## #h t; nelim h; #h1 h2; nwhd in ⊢ (??%? → ??%?); #IH;531 nrewrite > IH; nwhd in ⊢ (??%(?%)); nrewrite > (Zsucc_pos …); //; ##]530 ##[ ##2: elim t; ##[ //; ## #h t; elim h; #h1 h2; whd in ⊢ (??%? → ??%?); #IH; 531 nrewrite > IH; whd in ⊢ (??%(?%)); nrewrite > (Zsucc_pos …); //; ##] 532 532 ## nrewrite > (?:nextfunction ?? = length ? t); 533 ##[ ##2: nelim t; ##[ //; ## #h t IH; nwhd in ⊢ (??%?); nrewrite > IH;534 nwhd in ⊢ (???(?%)); nrewrite > (Zsucc_pos …); //; ##]535 ## napply eqZb_elim; #eb; nwhd in ⊢ (??%? → ??%?);536 ##[ #H; ndestruct (H); //;533 ##[ ##2: elim t; ##[ //; ## #h t IH; whd in ⊢ (??%?); nrewrite > IH; 534 whd in ⊢ (???(?%)); nrewrite > (Zsucc_pos …); //; ##] 535 ## napply eqZb_elim; #eb; whd in ⊢ (??%? → ??%?); 536 ##[ #H; destruct (H); //; 537 537 ## #H; napply IH; napply H; 538 538 ##] … … 540 540 ##] 541 541 ##] 542 ## #A B C transf p v f; nelim v;543 ##[ nwhd in ⊢ (??%? → ??%?); #H; ndestruct;544 ## ##2,3: #x; nwhd in ⊢ (??%? → ??%?); #H; ndestruct;545 ## #pcl b off; nwhd in ⊢ (??%? → ??%?); nelim (eq off zero);546 nwhd in ⊢ (??%? → ??%?);547 ##[ nelim p; #fns main vars; nelim fns;548 ##[ nwhd in ⊢ (??%? → ??%?); #H; ndestruct;549 ## #h t; nelim h; #f fn IH;550 nwhd in ⊢ (??%? → ??%?);542 ## #A B C transf p v f; elim v; 543 ##[ whd in ⊢ (??%? → ??%?); #H; destruct; 544 ## ##2,3: #x; whd in ⊢ (??%? → ??%?); #H; destruct; 545 ## #pcl b off; whd in ⊢ (??%? → ??%?); elim (eq off zero); 546 whd in ⊢ (??%? → ??%?); 547 ##[ elim p; #fns main vars; elim fns; 548 ##[ whd in ⊢ (??%? → ??%?); #H; destruct; 549 ## #h t; elim h; #f fn IH; 550 whd in ⊢ (??%? → ??%?); 551 551 nrewrite > (?:nextfunction ?? = length ? t); 552 ##[ ##2: nelim t; ##[ //; ## #h t; nelim h; #h1 h2; nwhd in ⊢ (??%? → ??%?); #IH;553 nrewrite > IH; nwhd in ⊢ (??%(?%)); nrewrite > (Zsucc_pos …); //; ##]552 ##[ ##2: elim t; ##[ //; ## #h t; elim h; #h1 h2; whd in ⊢ (??%? → ??%?); #IH; 553 nrewrite > IH; whd in ⊢ (??%(?%)); nrewrite > (Zsucc_pos …); //; ##] 554 554 ## nrewrite > (?:nextfunction ?? = length ? t); 555 ##[ ##2: nelim t; ##[ //; ## #h t IH; nwhd in ⊢ (??%?); nrewrite > IH;556 nwhd in ⊢ (???(?%)); nrewrite > (Zsucc_pos …); //; ##]557 ## napply eqZb_elim; #e; nwhd in ⊢ (??%? → ??%?); #H;558 ##[ ndestruct (H); //;555 ##[ ##2: elim t; ##[ //; ## #h t IH; whd in ⊢ (??%?); nrewrite > IH; 556 whd in ⊢ (???(?%)); nrewrite > (Zsucc_pos …); //; ##] 557 ## napply eqZb_elim; #e; whd in ⊢ (??%? → ??%?); #H; 558 ##[ destruct (H); //; 559 559 ## napply IH; napply H; 560 560 ##] … … 562 562 ##] 563 563 ##] 564 ## #H; ndestruct;564 ## #H; destruct; 565 565 ##] 566 566 ##] 567 ## #A B C transf p id; nelim p; #fns main vars;568 nelim fns;569 ##[ n normalize; //570 ## #h t; nelim h; #fid fd; nwhd in ⊢ (??%% → ??%%); #IH;571 nelim (ident_eq fid id); #e;572 ##[ nwhd in ⊢ (??%%);567 ## #A B C transf p id; elim p; #fns main vars; 568 elim fns; 569 ##[ normalize; // 570 ## #h t; elim h; #fid fd; whd in ⊢ (??%% → ??%%); #IH; 571 elim (ident_eq fid id); #e; 572 ##[ whd in ⊢ (??%%); 573 573 nrewrite > (?:nextfunction ?? = length ? t); 574 ##[ ##2: nelim t; ##[ //; ## #h t; nelim h; #h1 h2; nwhd in ⊢ (??%? → ??%?); #IH;575 nrewrite > IH; nwhd in ⊢ (??%(?%)); nrewrite > (Zsucc_pos …); //; ##]574 ##[ ##2: elim t; ##[ //; ## #h t; elim h; #h1 h2; whd in ⊢ (??%? → ??%?); #IH; 575 nrewrite > IH; whd in ⊢ (??%(?%)); nrewrite > (Zsucc_pos …); //; ##] 576 576 ## nrewrite > (?:nextfunction ?? = length ? t); 577 ##[ ##2: nelim t; ##[ //; ## #h t; nelim h; #h1 h2; nwhd in ⊢ (??%? → ??%?); #IH; nrewrite > IH;578 nwhd in ⊢ (???(?%)); nrewrite > (Zsucc_pos …); //; ##]577 ##[ ##2: elim t; ##[ //; ## #h t; elim h; #h1 h2; whd in ⊢ (??%? → ??%?); #IH; nrewrite > IH; 578 whd in ⊢ (???(?%)); nrewrite > (Zsucc_pos …); //; ##] 579 579 ## // 580 580 ##] 581 581 ##] 582 ## nwhd in ⊢ (??%%); nrewrite > IH; napply refl;582 ## whd in ⊢ (??%%); nrewrite > IH; napply refl; 583 583 ##] 584 584 ##] 585 585 ## //; 586 ## #A B C transf p b tf; nelim p; #fns main vars;587 nelim fns;588 ##[ n normalize; #H; ndestruct;589 ## #h t; nelim h; #fid fd; #IH; nwhd in ⊢ (??%? → ??(λ_.?(??%?)?));586 ## #A B C transf p b tf; elim p; #fns main vars; 587 elim fns; 588 ##[ normalize; #H; destruct; 589 ## #h t; elim h; #fid fd; #IH; whd in ⊢ (??%? → ??(λ_.?(??%?)?)); 590 590 nrewrite > (?:nextfunction ?? = length ? t); 591 ##[ ##2: nelim t; ##[ //; ## #h t; nelim h; #h1 h2; nwhd in ⊢ (??%? → ??%?); #IH;592 nrewrite > IH; nwhd in ⊢ (??%(?%)); nrewrite > (Zsucc_pos …); //; ##]591 ##[ ##2: elim t; ##[ //; ## #h t; elim h; #h1 h2; whd in ⊢ (??%? → ??%?); #IH; 592 nrewrite > IH; whd in ⊢ (??%(?%)); nrewrite > (Zsucc_pos …); //; ##] 593 593 ## nrewrite > (?:nextfunction ?? = length ? t); 594 ##[ ##2: nelim t; ##[ //; ## #h t; nelim h; #h1 h2; nwhd in ⊢ (??%? → ??%?); #IH; nrewrite > IH;595 nwhd in ⊢ (???(?%)); nrewrite > (Zsucc_pos …); //; ##]596 ## napply eqZb_elim; #eb; nwhd in ⊢ (??%? → ??(λ_.?(??%?)?));597 ##[ #H; @fd; @; //; nelim (grumpydestruct1 ??? H); //;594 ##[ ##2: elim t; ##[ //; ## #h t; elim h; #h1 h2; whd in ⊢ (??%? → ??%?); #IH; nrewrite > IH; 595 whd in ⊢ (???(?%)); nrewrite > (Zsucc_pos …); //; ##] 596 ## napply eqZb_elim; #eb; whd in ⊢ (??%? → ??(λ_.?(??%?)?)); 597 ##[ #H; @fd; @; //; elim (grumpydestruct1 ??? H); //; 598 598 ## #H; napply IH; napply H; 599 599 ##] … … 601 601 ##] 602 602 ##] 603 ## #A B C transf p v tf; nelim p; #fns main vars; nelim v;604 ##[ n normalize; #H; ndestruct;605 ## ##2,3: #x; n normalize; #H; ndestruct;606 ## #pcl b off; nwhd in ⊢ (??%? → ??(λ_.?(??%?)?)); nelim (eq off zero);607 ##[ nwhd in ⊢ (??%? → ??(λ_.?(??%?)?));608 nelim fns;609 ##[ n normalize; #H; ndestruct;610 ## #h t; nelim h; #fid fd; #IH; nwhd in ⊢ (??%? → ??(λ_.?(??%?)?));603 ## #A B C transf p v tf; elim p; #fns main vars; elim v; 604 ##[ normalize; #H; destruct; 605 ## ##2,3: #x; normalize; #H; destruct; 606 ## #pcl b off; whd in ⊢ (??%? → ??(λ_.?(??%?)?)); elim (eq off zero); 607 ##[ whd in ⊢ (??%? → ??(λ_.?(??%?)?)); 608 elim fns; 609 ##[ normalize; #H; destruct; 610 ## #h t; elim h; #fid fd; #IH; whd in ⊢ (??%? → ??(λ_.?(??%?)?)); 611 611 nrewrite > (?:nextfunction ?? = length ? t); 612 ##[ ##2: nelim t; ##[ //; ## #h t; nelim h; #h1 h2; nwhd in ⊢ (??%? → ??%?); #IH;613 nrewrite > IH; nwhd in ⊢ (??%(?%)); nrewrite > (Zsucc_pos …); //; ##]612 ##[ ##2: elim t; ##[ //; ## #h t; elim h; #h1 h2; whd in ⊢ (??%? → ??%?); #IH; 613 nrewrite > IH; whd in ⊢ (??%(?%)); nrewrite > (Zsucc_pos …); //; ##] 614 614 ## nrewrite > (?:nextfunction ?? = length ? t); 615 ##[ ##2: nelim t; ##[ //; ## #h t; nelim h; #h1 h2; nwhd in ⊢ (??%? → ??%?); #IH; nrewrite > IH;616 nwhd in ⊢ (???(?%)); nrewrite > (Zsucc_pos …); //; ##]617 ## napply eqZb_elim; #eb; nwhd in ⊢ (??%? → ??(λ_.?(??%?)?));618 ##[ #H; @fd; @; //; nelim (grumpydestruct1 ??? H); //;615 ##[ ##2: elim t; ##[ //; ## #h t; elim h; #h1 h2; whd in ⊢ (??%? → ??%?); #IH; nrewrite > IH; 616 whd in ⊢ (???(?%)); nrewrite > (Zsucc_pos …); //; ##] 617 ## napply eqZb_elim; #eb; whd in ⊢ (??%? → ??(λ_.?(??%?)?)); 618 ##[ #H; @fd; @; //; elim (grumpydestruct1 ??? H); //; 619 619 ## #H; napply IH; napply H; 620 620 ##] … … 622 622 ##] 623 623 ##] 624 ## n normalize; #H; ndestruct;624 ## normalize; #H; destruct; 625 625 ##] 626 626 ##] 627 ##] nqed.627 ##] qed. 628 628 629 629 … … 1012 1012 Lemma add_functs_match: 1013 1013 forall (fns: list (ident * A)) (tfns: list (ident * B)), 1014 list_forall2 (match_funct_e ntry match_fun) fns tfns →1014 list_forall2 (match_funct_etry match_fun) fns tfns → 1015 1015 let r := add_functs (empty A) fns in 1016 1016 let tr := add_functs (empty B) tfns in … … 1041 1041 Lemma add_functs_rev_match: 1042 1042 forall (fns: list (ident * A)) (tfns: list (ident * B)), 1043 list_forall2 (match_funct_e ntry match_fun) fns tfns →1043 list_forall2 (match_funct_etry match_fun) fns tfns → 1044 1044 let r := add_functs (empty A) fns in 1045 1045 let tr := add_functs (empty B) tfns in … … 1072 1072 (vars: list (ident * list init_data * V)) 1073 1073 (tvars: list (ident * list init_data * W)), 1074 list_forall2 (match_var_e ntry match_var) vars tvars →1074 list_forall2 (match_var_etry match_var) vars tvars → 1075 1075 snd (add_globals (g1, m) vars) = snd (add_globals (g2, m) tvars). 1076 1076 Proof. … … 1091 1091 forall (vars: list (ident * list init_data * V)) 1092 1092 (tvars: list (ident * list init_data * W)), 1093 list_forall2 (match_var_e ntry match_var) vars tvars →1093 list_forall2 (match_var_etry match_var) vars tvars → 1094 1094 symbols (fst (add_globals (g1, m) vars)) = 1095 1095 symbols (fst (add_globals (g2, m) tvars)).
Note: See TracChangeset
for help on using the changeset viewer.