Changeset 3082


Ignore:
Timestamp:
Apr 4, 2013, 9:31:31 AM (4 years ago)
Author:
mckinna
Message:

Tidying up: the long comment about preamble/renamed_symbols in the defn of pseduo_assembly_program had become separated from the typedef.

Lots more opportunities, including an earlier abandoned attempt to use typedefs for code_memory and costlabel_map throughout the rest of ASM/*.

In future work, it might be interesting to examine the effects on the quality of extracted code.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/ASM.ma

    r3039 r3082  
    984984
    985985definition labelled_instruction ≝ labelled_obj ASMTag pseudo_instruction.
    986 (* The first associative list assigns symbol names to addresses in data memory.
    987    The second associative list assigns to Identifiers meant to be entry points
    988    of functions the name of the function (that lives in a different namespace) *)
    989986
    990987definition assembly_program ≝ list instruction.
     
    11431140definition code_size_opt : ∀code. option (code_size_p code) ≝
    11441141  λcode. nat_bound_opt MAX_CODE_SIZE (S (|code|)).
     1142
     1143(* The first associative list assigns symbol names to addresses in data memory.
     1144   The second associative list assigns to Identifiers meant to be entry points
     1145   of functions the name of the function (that lives in a different namespace) *)
    11451146
    11461147record pseudo_assembly_program : Type[0] ≝
Note: See TracChangeset for help on using the changeset viewer.