Changeset 2754 for src/LIN


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/LIN/LINToASM.ma

    r2708 r2754  
    352352    ].
    353353
     354definition get_symboltable :
     355  ∀globals.state_monad (ASM_universe globals) (list (Identifier × ident)) ≝
     356  λglobals,u.
     357  let imap ≝ ident_map … u in
     358  let f ≝ λiold,inew.cons ? 〈inew, iold〉 in
     359  〈u, foldi ??? f imap [ ]〉.
     360
    354361definition lin_to_asm : lin_program → pseudo_assembly_program ≝
    355362  λp.
     
    364371     ! main ← Identifier_of_ident … (prog_main … p) ;
    365372     let code ≝ 〈None ?, Call main〉 :: 〈Some ? exit_label, Jmp exit_label〉 :: code in
     373     ! symboltable ← get_symboltable … ;
    366374     (* atm no data identifier is used in the code, so preamble must be empty *)
    367      return 〈[ ], code〉).
     375     return 〈[ ], symboltable, code〉).
Note: See TracChangeset for help on using the changeset viewer.