Changeset 2754 for src/ASM/Fetch.ma


Ignore:
Timestamp:
Mar 1, 2013, 10:26:31 AM (7 years ago)
Author:
sacerdot
Message:
  1. WARNING: I commented out one of James's function used in compiler.ma because it was undefined (partial commit). To be restored.
  2. The type of labelled_object_code programs now has a symbol table, used to generate the intensional events function call/return.
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ASM/Fetch.ma

    r2516 r2754  
    182182
    183183definition load_code_memory0:
    184  ∀program: list Byte. Σres: BitVectorTrie Byte 16.
     184 ∀program: object_code. Σres: BitVectorTrie Byte 16.
    185185  let program_size ≝ |program| in
    186186   program_size ≤ 2^16 →
     
    220220qed.
    221221
    222 definition load_code_memory: list Byte → BitVectorTrie Byte 16 ≝
     222definition load_code_memory: object_code → BitVectorTrie Byte 16 ≝
    223223 λprogram.load_code_memory0 program.
    224224
    225225lemma load_code_memory_ok:
    226  ∀program: list Byte.
     226 ∀program: object_code.
    227227  let program_size ≝ |program| in
    228228   program_size ≤ 2^16 →
Note: See TracChangeset for help on using the changeset viewer.