Changeset 2103 for src/common
 Timestamp:
 Jun 21, 2012, 5:21:02 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/common/AST.ma
r1920 r2103 325 325 map ?? (λid_fn. 〈fst ?? id_fn, transf (snd ?? id_fn)〉) l. 326 326 327 definition transform_program : ∀A,B,V. ∀p:program A V. (A (prog_var_names … p) → B (prog_var_names … p)) → program B V ≝ 327 (* In principle we could allow the transformation to be specialised to a 328 particular set of variable names, but that makes it much harder to state 329 and prove properties. *) 330 331 definition transform_program : ∀A,B,V. ∀p:program A V. (∀varnames. A varnames → B varnames) → program B V ≝ 328 332 λA,B,V,p,transf. 329 333 mk_program B V 330 334 (prog_vars A V p) 331 (transf_program ?? transf(prog_funct A V p))335 (transf_program ?? (transf ?) (prog_funct A V p)) 332 336 (prog_main A V p). 333 337 (* … … 446 450 MSG "In function " :: CTX id :: MSG ": " :: nil. 447 451 *) 448 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) ≝452 definition transform_partial_program : ∀A,B,V. ∀p:program A V. (∀varnames. A varnames → res (B varnames)) → res (program B V) ≝ 449 453 λA,B,V,p,transf_partial. 450 do fl ← map_partial … transf_partial(prog_funct … p);454 do fl ← map_partial … (transf_partial ?) (prog_funct … p); 451 455 OK (program B V) (mk_program … (prog_vars … p) fl (prog_main ?? p)). 452 456 … … 508 512 definition transform_partial_program2 : 509 513 ∀A,B,V,W. ∀p: program A V. 510 ( A (prog_var_names … p) → res (B (prog_var_names ?? p)))514 (∀varnames. A varnames → res (B varnames)) 511 515 → (V → res W) → res (program B W) ≝ 512 516 λA,B,V,W,p, transf_partial_function, transf_partial_variable. 513 do fl ← map_partial … (*prefix_funct_name*) transf_partial_function(prog_funct ?? p); ?.517 do fl ← map_partial … (*prefix_funct_name*) (transf_partial_function ?) (prog_funct ?? p); ?. 514 518 (*CSC: interactive mode because of dependent types *) 515 519 generalize in match (map_partial_preserves_first … transf_partial_variable (prog_vars … p));
Note: See TracChangeset
for help on using the changeset viewer.