Changeset 1248


Ignore:
Timestamp:
Sep 22, 2011, 10:13:24 AM (8 years ago)
Author:
mulligan
Message:

deleted files that do not compile in utilities, changed ertl.ma to use new joint syntax

Location:
src
Files:
2 deleted
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTL.ma

    r1242 r1248  
    11include "joint/Joint.ma".
     2include alias "common/Graphs.ma".
    23
    34inductive move_registers: Type[0] ≝
     
    1011  | ertl_st_ext_frame_size: register → label → ertl_statement_extension.
    1112
    12 definition ertl_params: params
    13  mk_params
    14   (mk_params_ register register register register
     13definition ertl_params_: params_
     14 mk_params_
     15  (mk_params__ register register register register
    1516    (move_registers × move_registers) register
    1617      ertl_statement_extension unit (list register) nat) label.
    1718
    18 definition ertl_statement ≝ joint_statement ertl_params.
     19definition ertl_statement ≝ joint_statement ertl_params_.
    1920
    20 definition ertl_internal_function ≝ joint_internal_function ertl_params.
     21definition ertl_params: ∀globals. params globals ≝
     22  λglobals.
     23    mk_params globals ertl_params_ (graph (ertl_statement globals)) (lookup …).
     24
     25
     26definition ertl_internal_function ≝
     27  λglobals.
     28    joint_internal_function globals (ertl_params globals).
    2129
    2230definition ertl_program ≝ joint_program ertl_params.
Note: See TracChangeset for help on using the changeset viewer.