Changeset 1221


Ignore:
Timestamp:
Sep 16, 2011, 10:53:53 AM (8 years ago)
Author:
sacerdot
Message:

Cleanup.

Location:
src/ERTL
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTL.ma

    r1220 r1221  
    1 include "ASM/I8051.ma".
    21include "joint/Joint.ma".
    3 include "utilities/BitVectorTrieSet.ma".
    4 include "utilities/IdentifierTools.ma".
    52include "common/Graphs.ma".
    6 include "common/CostLabel.ma".
    7 include "common/Registers.ma".
    83
    94definition registers ≝ list register.
  • src/ERTL/semantics.ma

    r1163 r1221  
    4949axiom hwreg_store : Register → val → mRegisterMap → res mRegisterMap.
    5050
    51 definition genv ≝ λglobals. (genv_t Genv) (fundef (ertl_internal_function globals)).
     51definition genv ≝ λglobals. (genv_t Genv) (fundef (joint_internal_function globals … (ertl_sem_params_ globals))).
    5252
    5353(* CSC: frame reduced to this *)
     
    139139
    140140axiom fetch_statement: ∀globals: list ident. state → res (ertl_statement globals).
    141 axiom fetch_function: ∀globals: list ident. state → res (ertl_internal_function globals).
     141axiom fetch_function: ∀globals: list ident. state → res (joint_internal_function globals … (ertl_sem_params_ globals)).
    142142
    143143definition init_locals : list register → register_env val ≝
     
    191191  (* CSC: monadic notation missing here *)
    192192    bind ?? (fetch_function globals st) (λf.
    193     OK ? (ertl_if_stacksize globals f)).
     193    OK ? (joint_if_stacksize globals … f)).
    194194
    195195definition get_hwsp : state → res address ≝
Note: See TracChangeset for help on using the changeset viewer.