Ignore:
Timestamp:
Feb 19, 2013, 6:48:32 PM (7 years ago)
Author:
tranquil
Message:
  • improvements to the graph translation function
  • fixed passes up to LTL
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/joint/semanticsUtils.ma

    r2675 r2681  
    33include "utilities/hide.ma".
    44include "ASM/BitVectorTrie.ma".
     5include "joint/TranslateUtils.ma".
    56
    67record hw_register_env : Type[0] ≝
     
    162163whd in ⊢ (??%%→?); #EQ destruct(EQ) %{EQ1 EQ2}
    163164qed.
     165
     166axiom b_graph_transform_program_props :
     167 ∀src,dst:sem_graph_params.
     168 ∀data : ∀globals.joint_closed_internal_function src globals →
     169  bind_new register (b_graph_translate_data src dst globals).
     170 ∀prog_in : joint_program src.
     171 let prog_out ≝ b_graph_transform_program … data prog_in in
     172 let src_genv ≝ globalenv_noinit ? prog_in in
     173 let dst_genv ≝ globalenv_noinit ? prog_out in
     174 ∃init_regs : ident → list register.
     175 ∃f_lbls : ident → label → option (list label).
     176 ∃f_regs : ident → label → option (list register).
     177 ∀bl,id,def_in.
     178 fetch_internal_function ? src_genv bl = return 〈id, def_in〉 →
     179 ∃init_data,def_out.
     180 fetch_internal_function ? dst_genv bl = return 〈id, def_out〉 ∧
     181 bind_new_instantiates … init_data (data … def_in) (init_regs id) ∧
     182 b_graph_translate_props src dst ? init_data (init_regs id)
     183    def_in def_out (f_lbls id) (f_regs id).
Note: See TracChangeset for help on using the changeset viewer.