Changeset 1224 for src/common
- Timestamp:
- Sep 16, 2011, 6:39:05 PM (10 years ago)
- Location:
- src/common
- Files:
-
- 1 deleted
- 2 edited
Legend:
- Unmodified
- Added
- Removed
-
src/common/AST.ma
r1213 r1224 283 283 programs are common to all languages. *) 284 284 285 record program (F ,V: Type[0]) : Type[0] := {286 prog_ funct: list (ident × F);287 prog_ main: ident;288 prog_ vars: list (ident × region × V)285 record program (F: list ident → Type[0]) (V: Type[0]) : Type[0] := { 286 prog_vars: list (ident × region × V); 287 prog_funct: list (ident × (F (map … (λx. \fst (\fst x)) prog_vars))); 288 prog_main: ident 289 289 }. 290 290 291 291 292 definition prog_funct_names ≝ λF,V : Type[0]. λp: program F V.293 map ? ? (fst ident F) (prog_funct ??p).294 295 definition prog_var_names ≝ λF,V : Type[0]. λp: program F V.296 map ?? (λx: ident × region × V. (\fst (\fst x))) (prog_vars ??p).292 definition prog_funct_names ≝ λF,V. λp: program F V. 293 map … \fst (prog_funct … p). 294 295 definition prog_var_names ≝ λF,V. λp: program F V. 296 map … (λx. \fst (\fst x)) (prog_vars … p). 297 297 298 298 (* * * Generic transformations over programs *) … … 312 312 map ?? (λid_fn. 〈fst ?? id_fn, transf (snd ?? id_fn)〉) l. 313 313 314 definition transform_program : ∀A,B,V. (A → B) → program A V→ program B V ≝315 λA,B,V, transf,p.314 definition transform_program : ∀A,B,V. ∀p:program A V. (A (prog_var_names … p) → B (prog_var_names … p)) → program B V ≝ 315 λA,B,V,p,transf. 316 316 mk_program B V 317 (prog_vars A V p) 317 318 (transf_program ?? transf (prog_funct A V p)) 318 (prog_main A V p) 319 (prog_vars A V p). 319 (prog_main A V p). 320 320 (* 321 321 lemma transform_program_function: … … 346 346 list (A × B) → res (list (A × C)) ≝ 347 347 λA,B,C,f. mmap ?? (λab. let 〈a,b〉 ≝ ab in do c ← f b; OK ? 〈a,c〉). 348 349 lemma map_partial_preserves_first: 350 ∀A,B,C:Type[0]. ∀f: B → res C. ∀l: list (A × B). ∀l': list (A × C). 351 map_partial … f l = OK ? l' → 352 map … \fst l = map … \fst l'. 353 #A #B #C #f #l elim l 354 [ #l' #E normalize in E; destruct % 355 | * #a #b #tl #IH #l' normalize in ⊢ (??%? → ?) cases (f b) normalize in ⊢ (? → ??%? → ?) 356 [2: #err #E destruct 357 | #c change with (match map_partial … f tl with [ OK x ⇒ ? | Error y ⇒ ?] = ? → ?) 358 cases (map_partial … f tl) in IH ⊢ % 359 #x #IH normalize in ⊢ (??%? → ?) #ABS destruct 360 >(IH x) // ]] 361 qed. 362 348 363 (* 349 364 Fixpoint map_partial (l: list (A * B)) : res (list (A * C)) := … … 418 433 MSG "In function " :: CTX id :: MSG ": " :: nil. 419 434 *) 420 definition transform_partial_program : ∀A,B,V. (A → res B) → program A V → res (program B V) ≝ 421 λA,B,V,transf_partial,p. 422 do fl ← map_partial … (*prefix_funct_name*) transf_partial (prog_funct ?? p); 423 OK ? (mk_program … fl (prog_main ?? p) (prog_vars ?? p)). 435 definition transform_partial_program : ∀A,B,V. ∀p:program A V. (A (prog_var_names … p) → res (B (prog_var_names … p))) → res (program B V) ≝ 436 λA,B,V,p,transf_partial. 437 do fl ← map_partial … transf_partial (prog_funct … p); 438 OK (program B V) (mk_program … (prog_vars … p) fl (prog_main ?? p)). 439 424 440 (* 425 441 Lemma transform_partial_program_function: … … 464 480 MSG "In global variable " :: CTX (fst id_init) :: MSG ": " :: nil. 465 481 *) 466 definition transform_partial_program2 : ∀A,B,V,W. (A → res B) → (V → res W) → 467 program A V → res (program B W) ≝ 468 λA,B,V,W, transf_partial_function, transf_partial_variable, p. 469 do fl ← map_partial … (*prefix_funct_name*) transf_partial_function (prog_funct ?? p); 470 do vl ← map_partial … (*prefix_var_name*) transf_partial_variable (prog_vars ?? p); 471 OK ? (mk_program … fl (prog_main ?? p) vl). 482 483 (* CSC: ad hoc lemma, move away? *) 484 lemma map_fst: 485 ∀A,B,C,C':Type[0].∀l:list (A × B × C).∀l':list (A × B × C'). 486 map … \fst l = map … \fst l' → 487 map … (λx. \fst (\fst x)) l = map … (λx. \fst (\fst x)) l'. 488 #A #B #C #C' #l elim l 489 [ #l' elim l' // #he #tl #IH #ABS normalize in ABS; destruct 490 | #he1 #tl1 #IH #l' cases l' [ #ABS normalize in ABS; destruct ] 491 #he2 #tl2 #EQ whd in EQ:(??%%) ⊢ (??%%) >(IH tl2) destruct >e0 // 492 >e0 in e1 normalize #H @H ] 493 qed. 494 495 definition transform_partial_program2 : 496 ∀A,B,V,W. ∀p: program A V. 497 (A (prog_var_names … p) → res (B (prog_var_names ?? p))) 498 → (V → res W) → res (program B W) ≝ 499 λA,B,V,W,p, transf_partial_function, transf_partial_variable. 500 do fl ← map_partial … (*prefix_funct_name*) transf_partial_function (prog_funct ?? p); ?. 501 (*CSC: interactive mode because of dependent types *) 502 generalize in match (map_partial_preserves_first … transf_partial_variable (prog_vars … p)) 503 cases (map_partial … transf_partial_variable (prog_vars … p)) 504 [ #vl #EQ 505 @(OK (program B W) (mk_program … vl … (prog_main … p))) 506 <(map_fst … (EQ vl (refl …))) @fl 507 | #err #_ @(Error … err)] 508 qed. 509 472 510 (* 473 511 Lemma transform_partial_program2_function: -
src/common/Globalenvs.ma
r1139 r1224 52 52 of function descriptions. *) 53 53 54 globalenv: ∀F,V : Type[0]. (V → list init_data) → program F V → res (genv_t F);54 globalenv: ∀F,V. (V → list init_data) → ∀p:program F V. res (genv_t (F (prog_var_names … p))); 55 55 (* * Return the global environment for the given program. *) 56 56 57 init_mem: ∀F,V : Type[0]. (V → list init_data) → program F V → res mem;57 init_mem: ∀F,V. (V → list init_data) → program F V → res mem; 58 58 (* * Return the initial memory state for the given program. *) 59 59 … … 502 502 (OK ? init_env) vars. 503 503 504 definition globalenv_initmem : ∀F,V :Type[0]. (V → (list init_data)) → program F V → res (genv F× mem) ≝504 definition globalenv_initmem : ∀F,V. (V → (list init_data)) → ∀p:program F V. res (genv (F (prog_var_names … p)) × mem) ≝ 505 505 λF,V,init_info,p. 506 add_globals F Vinit_info506 add_globals … init_info 507 507 〈add_functs ? (empty …) (prog_funct F ? p), empty_mem〉 508 508 (prog_vars ?? p). 509 509 510 definition globalenv_ : ∀F,V :Type[0]. (V → list init_data) → program F V → res (genv F) ≝510 definition globalenv_ : ∀F,V. (V → list init_data) → ∀p:program F V. res (genv (F (prog_var_names … p))) ≝ 511 511 λF,V,i,p. 512 512 do 〈g,m〉 ← globalenv_initmem F V i p; 513 513 OK ? g. 514 definition init_mem_ : ∀F,V :Type[0]. (V → list init_data) → program F V → res (mem) ≝514 definition init_mem_ : ∀F,V. (V → list init_data) → program F V → res (mem) ≝ 515 515 λF,V,i,p. 516 516 do 〈g,m〉 ← globalenv_initmem F V i p;
Note: See TracChangeset
for help on using the changeset viewer.