Changeset 2319 for src/common/AST.ma


Ignore:
Timestamp:
Sep 3, 2012, 1:16:29 PM (8 years ago)
Author:
campbell
Message:

Generate per-program cost labels rather than per-function ones, and
produce an extra cost label for the global variable initialisation.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/common/AST.ma

    r2286 r2319  
    348348    (transf_program ?? (transf ?) (prog_funct A V p))
    349349    (prog_main A V p).
     350
     351(* Versions of the above that thread a fresh name generator through the
     352   transformation. *)
     353
     354definition transf_program_gen : ∀tag,A,B. universe tag →
     355  (universe tag → A → B × (universe tag)) →
     356  list (ident × A) →
     357  list (ident × B) × (universe tag) ≝
     358λtag,A,B,gen,transf,l.
     359  foldr ?? (λid_fn,bs_gen. let 〈fn',gen'〉 ≝ transf (\snd bs_gen) (\snd id_fn) in
     360                      〈〈\fst id_fn, fn'〉::(\fst bs_gen), gen'〉) 〈[ ], gen〉 l.
     361
     362lemma transf_program_gen_step : ∀tag,A,B,gen,transf,id,fn,tl.
     363  ∃gen'.
     364    \fst (transf_program_gen tag A B gen transf (〈id,fn〉::tl)) =
     365    〈id, \fst (transf gen' fn)〉::(\fst (transf_program_gen tag A B gen transf tl)).
     366#tag #A #B #gen #transf #id #fn #tl
     367whd in ⊢ (??(λ_.??(???%)?));
     368change with (transf_program_gen ??????) in match (foldr ?????);
     369cases (transf_program_gen ??????) #tl' #gen'
     370%{gen'} cases (transf gen' fn) //
     371qed.
     372
     373definition transform_program_gen : ∀tag,A,B,V. universe tag → ∀p:program A V.
     374  (∀varnames. universe tag → A varnames → B varnames × (universe tag)) →
     375  program B V × (universe tag) ≝
     376λtag,A,B,V,gen,p,trans.
     377  let fsg ≝ transf_program_gen tag ?? gen (trans ?) (prog_funct A V p) in
     378  〈mk_program B V
     379    (prog_vars A V p)
     380    (\fst fsg)
     381    (prog_main A V p), \snd fsg〉.
     382
     383
    350384(*
    351385lemma transform_program_function:
     
    748782] qed.
    749783
     784lemma transform_program_gen_match:
     785  ∀A,B,V,tag,gen.
     786    ∀trans_function: ∀vs. universe tag → A vs → B vs × (universe tag).
     787    ∀p: program A V.
     788  match_program (mk_matching A B V V
     789    (λvs,fd,tfd. ∃g,g'. trans_function vs g fd = 〈tfd,g'〉)
     790    (λv,w. v = w))
     791    p (\fst (transform_program_gen … gen p trans_function)).
     792#A #B #V #tag #gen #tf
     793* #vars #fns #main
     794%
     795[ normalize elim vars // * * #id #r #v #tl #H % /2/
     796| whd in match (prog_var_names ???);
     797  whd in match (prog_vars ???);
     798  whd in match (transform_program_gen ???????);
     799  generalize in match gen;
     800  elim fns
     801  [ //
     802  | * #id #f #tl #IH #g
     803    cases (transf_program_gen_step tag (A ?) (B ?) g (tf ?) id f tl)
     804    #g' #E >E % /4/
     805  ]
     806| //
     807] qed.
     808
    750809(* * * External functions *)
    751810
Note: See TracChangeset for help on using the changeset viewer.