Changeset 2103 for src/common


Ignore:
Timestamp:
Jun 21, 2012, 5:21:02 PM (7 years ago)
Author:
campbell
Message:

Make transform_*program take a more general transformation to make
properties easier to state.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/AST.ma

    r1920 r2103  
    325325  map ?? (λid_fn. 〈fst ?? id_fn, transf (snd ?? id_fn)〉) l.
    326326
    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
     331definition transform_program : ∀A,B,V. ∀p:program A V. (∀varnames. A varnames → B varnames) → program B V ≝
    328332λA,B,V,p,transf.
    329333  mk_program B V
    330334    (prog_vars A V p)
    331     (transf_program ?? transf (prog_funct A V p))
     335    (transf_program ?? (transf ?) (prog_funct A V p))
    332336    (prog_main A V p).
    333337(*
     
    446450  MSG "In function " :: CTX id :: MSG ": " :: nil.
    447451*)
    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) ≝
     452definition transform_partial_program : ∀A,B,V. ∀p:program A V. (∀varnames. A varnames → res (B varnames)) →  res (program B V) ≝
    449453λ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);
    451455  OK (program B V) (mk_program … (prog_vars … p) fl (prog_main ?? p)).
    452456
     
    508512definition transform_partial_program2 :
    509513 ∀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))
    511515  →  (V → res W) → res (program B W) ≝
    512516λ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); ?.
    514518  (*CSC: interactive mode because of dependent types *)
    515519  generalize in match (map_partial_preserves_first … transf_partial_variable (prog_vars … p));
Note: See TracChangeset for help on using the changeset viewer.