 Timestamp:
 Sep 15, 2011, 6:05:31 PM (10 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ERTL/ERTL.ma
r1183 r1220 26 26 definition ertl_statement ≝ joint_statement ertl_params. 27 27 28 definition ertl_statement_graph ≝ λglobals. graph (ertl_statement globals). 28 definition ertl_sem_params_ : ∀globals. sem_params_ ertl_params globals ≝ 29 λglobals. 30 mk_sem_params_ ertl_params globals (graph (ertl_statement globals)) (lookup …). 29 31 30 record ertl_internal_function (globals: list ident): Type[0] ≝ 31 { 32 ertl_if_luniverse: universe LabelTag; 33 ertl_if_runiverse: universe RegisterTag; 34 ertl_if_params: nat; 35 ertl_if_locals: registers; 36 ertl_if_stacksize: nat; 37 ertl_if_graph: ertl_statement_graph globals; 38 ertl_if_entry: Σl: label. lookup ? ? ertl_if_graph l ≠ None ?; 39 ertl_if_exit: Σl: label. lookup ? ? ertl_if_graph l ≠ None ? 40 }. 41 42 definition set_luniverse ≝ 43 λglobals : list ident. 44 λint_fun : ertl_internal_function globals. 45 λluniverse: universe LabelTag. 46 let runiverse ≝ ertl_if_runiverse globals int_fun in 47 let params ≝ ertl_if_params globals int_fun in 48 let locals ≝ ertl_if_locals globals int_fun in 49 let stacksize ≝ ertl_if_stacksize globals int_fun in 50 let graph ≝ ertl_if_graph globals int_fun in 51 let entry ≝ ertl_if_entry globals int_fun in 52 let exit ≝ ertl_if_exit globals int_fun in 53 mk_ertl_internal_function globals 54 luniverse runiverse params locals 55 stacksize graph entry exit. 56 57 definition ertl_function ≝ λglobals. fundef (ertl_internal_function globals). 58 59 record ertl_program (globals: list ident): Type[0] ≝ 60 { 61 ertl_pr_vars: list (ident × nat); 62 ertl_pr_funcs: list (ident × (ertl_function globals)); 63 ertl_pr_main: option ident 64 }. 65 66 67 (* XXX: changed from O'Caml 68  ertl_st_addr_h: register → ident → label → ertl_statement 69  ertl_st_addr_l: register → ident → label → ertl_statement 32 (* 33 definition ertl_internal_function ≝ 34 λglobals. joint_internal_function globals … (ertl_sem_params_ globals). 70 35 *) 71 36 72 (* XXX: changed from O'Caml 73  ertl_st_opaccs_a: OpAccs → register → register → register → label → ertl_statement 74  ertl_st_opaccs_b: OpAccs → register → register → register → label → ertl_statement 75 *) 37 definition ertl_program ≝ λglobals. joint_program globals … (ertl_sem_params_ globals).
Note: See TracChangeset
for help on using the changeset viewer.