Changeset 764 for src/common/AST.ma
 Timestamp:
 Apr 20, 2011, 5:38:58 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/common/AST.ma
r757 r764 184 184 definition prog_var_names ≝ λF,V: Type[0]. λp: program F V. 185 185 map ?? (λx: ident × (list init_data) × region × V. fst ?? (fst ?? (fst ?? x))) (prog_vars ?? p). 186 (* 187 (* * * Generic transformations over programs *)188 189 (* * We now define a general iterator over programs that applies a given186 187 (* * * Generic transformations over programs *) 188 189 (* * We now define a general iterator over programs that applies a given 190 190 code transformation function to all function descriptions and leaves 191 191 the other parts of the program unchanged. *) 192 192 (* 193 193 Section TRANSF_PROGRAM. 194 194 … … 231 231 Variable prefix_errmsg: A > errmsg. 232 232 Variable f: B > res C. 233 233 *) 234 definition map_partial : ∀A,B,C:Type[0]. (B → res C) → 235 list (A × B) → res (list (A × C)) ≝ 236 λA,B,C,f. mmap ?? (λab. let 〈a,b〉 ≝ ab in do c ← f b; OK ? 〈a,c〉). 237 (* 234 238 Fixpoint map_partial (l: list (A * B)) : res (list (A * C)) := 235 239 match l with … … 302 306 Definition prefix_funct_name (id: ident) : errmsg := 303 307 MSG "In function " :: CTX id :: MSG ": " :: nil. 304 305 Definition transform_partial_program (p: program A V) : res (program B V) := 306 do fl < map_partial prefix_funct_name transf_partial p.(prog_funct); 307 OK (mkprogram fl p.(prog_main) p.(prog_vars)). 308 308 *) 309 definition transform_partial_program : ∀A,B,V. (A → res B) → program A V → res (program B V) ≝ 310 λA,B,V,transf_partial,p. 311 do fl ← map_partial … (*prefix_funct_name*) transf_partial (prog_funct ?? p); 312 OK ? (mk_program … fl (prog_main ?? p) (prog_vars ?? p)). 313 (* 309 314 Lemma transform_partial_program_function: 310 315 forall p tp i tf, … … 347 352 Definition prefix_var_name (id_init: ident * list init_data) : errmsg := 348 353 MSG "In global variable " :: CTX (fst id_init) :: MSG ": " :: nil. 349 350 Definition transform_partial_program2 (p: program A V) : res (program B W) := 351 do fl < map_partial prefix_funct_name transf_partial_function p.(prog_funct); 352 do vl < map_partial prefix_var_name transf_partial_variable p.(prog_vars); 353 OK (mkprogram fl p.(prog_main) vl). 354 354 *) 355 definition transform_partial_program2 : ∀A,B,V,W. (A → res B) → (V → res W) → 356 program A V → res (program B W) ≝ 357 λA,B,V,W, transf_partial_function, transf_partial_variable, p. 358 do fl ← map_partial … (*prefix_funct_name*) transf_partial_function (prog_funct ?? p); 359 do vl ← map_partial … (*prefix_var_name*) transf_partial_variable (prog_vars ?? p); 360 OK ? (mk_program … fl (prog_main ?? p) vl). 361 (* 355 362 Lemma transform_partial_program2_function: 356 363 forall p tp i tf, … … 457 464  Internal: F → fundef F 458 465  External: external_function → fundef F. 459 (* 466 460 467 (* Implicit Arguments External [F]. *) 461 468 (* … … 471 478  External ef ⇒ External ? ef 472 479 ]. 473 *) 480 474 481 (* 475 482 End TRANSF_FUNDEF. … … 479 486 Variable A B: Type. 480 487 Variable transf_partial: A > res B. 481 482 Definition transf_partial_fundef (fd: fundef A): res (fundef B) := 488 *) 489 490 definition transf_partial_fundef : ∀A,B. (A → res B) → fundef A → res (fundef B) ≝ 491 λA,B,transf_partial,fd. 483 492 match fd with 484  Internal f => do f' < transf_partial f; OK (Internalf')485  External ef => OK (Externalef)486 end.487 493 [ Internal f ⇒ do f' ← transf_partial f; OK ? (Internal ? f') 494  External ef ⇒ OK ? (External ? ef) 495 ]. 496 (* 488 497 End TRANSF_PARTIAL_FUNDEF. 489 498 *)
Note: See TracChangeset
for help on using the changeset viewer.