Changeset 2319 for src/common


Ignore:
Timestamp:
Sep 3, 2012, 1:16:29 PM (7 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.

Location:
src/common
Files:
2 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
  • src/common/Globalenvs.ma

    r2226 r2319  
    770770//
    771771qed.
     772
     773lemma
     774  init_mem_transf_gen:
     775    ∀tag,A,B,V,iV,g. ∀transf: (∀vs. universe tag → A vs → B vs × (universe tag)). ∀p: program A V.
     776    init_mem … iV (\fst (transform_program_gen … g p transf)) = init_mem … iV p.
     777#tag #A #B #C #iV #g #transf #p
     778@(init_mem_match … (transform_program_gen_match … transf ?))
     779//
     780qed.
    772781   
    773782
     
    791800| @(find_funct_transf A B V iV tf p)
    792801| @(find_funct_ptr_transf A B V iV p tf)
     802] qed.
     803
     804record related_globals_gen (tag:String) (A,B:Type[0]) (t: universe tag → A → B × (universe tag)) (ge:genv_t A) (ge':genv_t B) : Prop ≝ {
     805  rgg_find_symbol: ∀s.
     806    find_symbol … ge s = find_symbol … ge' s;
     807  rgg_find_funct_ptr: ∀b,f.
     808    find_funct_ptr … ge b = Some ? f →
     809    ∃g. find_funct_ptr … ge' b = Some ? (\fst (t g f));
     810  rgg_find_funct: ∀v,f.
     811    find_funct … ge v = Some ? f →
     812    ∃g. find_funct … ge' v = Some ? (\fst (t g f))
     813}.
     814
     815include "utilities/bool.ma".
     816
     817theorem transform_program_gen_related : ∀tag,A,B,V,init,g,p. ∀tf:∀vs. universe tag → A vs → B vs × (universe tag).
     818  related_globals_gen tag (A ?) (B ?) (tf ?) (globalenv A V init p) (globalenv B V init (\fst (transform_program_gen tag A B V g p tf))).
     819#tag #A #B #V #iV #g #p #tf %
     820[ #s @sym_eq @(find_symbol_match … (transform_program_gen_match … tf p))
     821  #v #w * //
     822| #b #f #FFP
     823  cases (find_funct_ptr_match … (transform_program_gen_match … tf p) … FFP)
     824  [ 2: @iV
     825  | #fn' * #FFP'
     826    generalize in match (matching_vars ????);
     827    whd in match (prog_var_names ???); whd in match (prog_vars ???);
     828    #E >(K ?? E) * #g1 * #g2 whd in ⊢ (??%% → ?); #E' >FFP' %{g1} >E' %
     829  | skip
     830  ]
     831| * [5: #ptr #fn whd in match (find_funct ???);
     832     @if_elim #Eoff #FFP
     833     [ cases (find_funct_ptr_match … (transform_program_gen_match … tf p) … FFP)
     834       [ 2: @iV
     835       | #fn' * #FFP'
     836         generalize in match (matching_vars ????);
     837         whd in match (prog_var_names ???); whd in match (prog_vars ???);
     838         #E >(K ?? E) * #g1 * #g2 whd in ⊢ (??%% → ?); #E'
     839         %{g1} whd in ⊢ (??%?); >Eoff >FFP' >E' %
     840       ]
     841     | destruct
     842     ]
     843    | *: normalize #A #B try #C try #D destruct
     844    ]
    793845] qed.
    794846
Note: See TracChangeset for help on using the changeset viewer.