Changeset 1220 for src/ERTL/ERTL.ma


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

ERTL ported to the new joint syntax.

File:
1 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).
Note: See TracChangeset for help on using the changeset viewer.