Changeset 1175 for src/ERTL/ERTL.ma


Ignore:
Timestamp:
Sep 2, 2011, 5:58:01 PM (9 years ago)
Author:
mulligan
Message:

changes to ertl pass

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTL.ma

    r1171 r1175  
    3737}.
    3838
     39definition set_luniverse ≝
     40  λglobals  : list ident.
     41  λint_fun  : ertl_internal_function globals.
     42  λluniverse: universe LabelTag.
     43  let runiverse ≝ ertl_if_runiverse globals int_fun in
     44  let params    ≝ ertl_if_params globals int_fun in
     45  let locals    ≝ ertl_if_locals globals int_fun in
     46  let stacksize ≝ ertl_if_stacksize globals int_fun in
     47  let graph     ≝ ertl_if_graph globals int_fun in
     48  let entry     ≝ ertl_if_entry globals int_fun in
     49  let exit      ≝ ertl_if_exit globals int_fun in
     50    mk_ertl_internal_function globals
     51      luniverse runiverse params locals
     52      stacksize graph entry exit.
     53
    3954definition ertl_function ≝ λglobals. fundef (ertl_internal_function globals).
    4055 
Note: See TracChangeset for help on using the changeset viewer.