Changeset 1220


Ignore:
Timestamp:
Sep 15, 2011, 6:05:31 PM (8 years ago)
Author:
sacerdot
Message:

ERTL ported to the new joint syntax.

Location:
src
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTL.ma

    r1183 r1220  
    2626definition ertl_statement ≝ joint_statement ertl_params.
    2727
    28 definition ertl_statement_graph ≝ λglobals. graph (ertl_statement globals).
     28definition ertl_sem_params_ : ∀globals. sem_params_ ertl_params globals ≝
     29 λglobals.
     30  mk_sem_params_ ertl_params globals (graph (ertl_statement globals)) (lookup …).
    2931
    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(*
     33definition ertl_internal_function ≝
     34 λglobals. joint_internal_function globals … (ertl_sem_params_ globals).
    7035*)
    7136
    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 *)
     37definition ertl_program ≝ λglobals. joint_program globals … (ertl_sem_params_ globals).
  • src/joint/Joint.ma

    r1182 r1220  
    6363}.
    6464
     65definition set_luniverse ≝
     66  λglobals  : list ident.
     67  λpre.
     68  λp: sem_params_ pre globals.
     69  λint_fun  : joint_internal_function globals … p.
     70  λluniverse: universe LabelTag.
     71  let runiverse ≝ joint_if_runiverse … int_fun in
     72  let params    ≝ joint_if_params … int_fun in
     73  let locals    ≝ joint_if_locals … int_fun in
     74  let result    ≝ joint_if_result … int_fun in
     75  let stacksize ≝ joint_if_stacksize … int_fun in
     76  let graph     ≝ joint_if_graph … int_fun in
     77  let entry     ≝ joint_if_entry … int_fun in
     78  let exit      ≝ joint_if_exit … int_fun in
     79    mk_joint_internal_function globals ? p
     80      luniverse runiverse result params locals
     81      stacksize graph entry exit.
     82
    6583definition joint_function ≝ λglobals,pre,p. fundef (joint_internal_function globals pre p).
    6684
    67 record joint_program (globals: list ident) (pre) (p:sem_params_ pre globals) : Type[0] ≝
    68 {
    69   joint_pr_vars: list (ident × nat);
    70   joint_pr_functs: list (ident × (joint_function … p));
    71   joint_pr_main: option ident
    72 }.
     85definition joint_program :=
     86 λglobals:list ident.λpre.λp: sem_params_ pre globals.
     87  program (joint_function … p) nat.
    7388
    7489(****************************************************************************)
  • src/joint/semantics.ma

    r1217 r1220  
    307307  mk_execstep … (is_final globals p exit registersno) (m p) (eval_statement globals p).
    308308
    309 (* CSC: XXX the program type does not fit with the globalenv and init_mem *)
    310 axiom make_initial_state : ∀globals:list ident.∀sparams: sem_params2 globals. joint_program … (pre_sem_params … sparams) → res ((genv … (pre_sem_params … sparams)) × (state sparams)).(* ≝
    311 λp.
    312   do ge ← globalenv Genv ?? p;
    313   do m ← init_mem Genv ?? p;
    314   let main ≝ rtl_pr_main ?? p in
     309definition make_initial_state :
     310 ∀globals:list ident.∀sparams: sem_params2 globals. joint_program ?? (pre_sem_params ? sparams) →
     311   res ((genv ?? (pre_sem_params ? sparams)) × (state sparams)) ≝
     312λglobals,par,p.
     313  do ge ← globalenv Genv … (λx.[Init_space x]) p;
     314  do m ← init_mem Genv … (λx.[Init_space x]) p;
     315  let main ≝ prog_main … p in
    315316  do b ← opt_to_res ? [MSG MissingSymbol; CTX ? main] (find_symbol ? ? ge main);
    316317  do f ← opt_to_res ? [MSG BadFunction; CTX ? main] (find_funct_ptr ? ? ge b);
    317   OK ? 〈ge,Callstate f (nil ?) [ ] (nil ?) m〉.
     318  ?(*
     319  OK ? 〈ge,Callstate f (nil ?) [ ] (nil ?) m〉*).
     320(*
     321RTL:
     322 init_prog == init_mem
     323 init_sp: inizializzare lo stack pointer
     324 init_isp: inizializzare l'altro stack pointer
     325 init_renv: inizializzare i registri fisici
     326 init_main_call: chiamata di funzione
     327   --- init_fun_call: cambia fra ERTL e LTL
     328 change_carry: a 0
    318329*)
    319 
    320330definition joint_fullexec :
    321331 ∀globals:list ident. ∀sparams:sem_params2 globals. joint_program globals sparams (pre_sem_params … sparams) → fullexec io_out io_in ≝
Note: See TracChangeset for help on using the changeset viewer.