Changeset 2754 for src/ASM/Interpret2.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/Interpret2.ma

    r2516 r2754  
    3737(* Transition system on the object code *)
    3838
    39 (*CSC: move this definition elsewhere *)
    40 definition object_code: Type[0] ≝ list Byte × (BitVectorTrie costlabel 16).
    41 
    42 definition make_global: object_code → BitVectorTrie costlabel 16 ≝ \snd.
     39definition make_global: labelled_object_code → BitVectorTrie costlabel 16 ≝ \snd.
    4340
    4441definition execute_1_instruction:
     
    5552definition exec: trans_system io_out io_in ≝
    5653 mk_trans_system … is_final execute_1_instruction.
     54*)
     55
     56axiom exec: trans_system io_out io_in.
    5757
    5858definition ASM_fullexec: fullexec io_out io_in ≝
    59  mk_fullexec … exec make_global (λp.OK … (load (\fst p) (initialise_status … (Stub ??)))).
    60 *)
     59 mk_fullexec ??? exec make_global ?(*(λp.OK … (load (\fst p) (initialise_status … (Stub ??))))*).
     60
    6161axiom ASM_fullexec: fullexec io_out io_in.
Note: See TracChangeset for help on using the changeset viewer.