Changeset 2767 for src/LIN/LINToASM.ma


Ignore:
Timestamp:
Mar 3, 2013, 2:03:58 PM (7 years ago)
Author:
mckinna
Message:

WARNING: BIG commit, which pushes code_size_opt check into LIN/LINToASM.ma
following CSC's comment on my previous partial commit
plus rolls all the miscellaneous code motion into the rest of the repo.

suggest REBUILD compiler.ma/correctness.ma from scratch.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/LIN/LINToASM.ma

    r2763 r2767  
     1include "utilities/BitVectorTrieSet.ma".
     2include "utilities/state.ma".
     3
    14include "ASM/Util.ma".
    2 include "utilities/BitVectorTrieSet.ma".
     5include "ASM/ASM.ma".
     6
    37include "LIN/LIN.ma".
    4 include "ASM/ASM.ma".
    5 include "utilities/state.ma".
    68
    79(* utilities to provide Identifier's and addresses  *)
     
    359361  〈u, foldi ??? f imap [ ]〉.
    360362
    361 definition lin_to_asm : lin_program → pseudo_assembly_program ≝
     363definition lin_to_asm : lin_program → option pseudo_assembly_program ≝
    362364  λp.
    363365  state_run ?? (new_ASM_universe p)
     
    370372     ! exit_label ← ASM_fresh … ;
    371373     ! main ← Identifier_of_ident … (prog_main … p) ;
    372      let code ≝ 〈None ?, Call main〉 :: 〈Some ? exit_label, Jmp exit_label〉 :: code in
    373374     ! symboltable ← get_symboltable … ;
    374      (* atm no data identifier is used in the code, so preamble must be empty *)
    375375     return
    376       (mk_pseudo_assembly_program [ ] code ? symboltable exit_label ? ?)).
     376      (let code ≝ 〈None ?, Call main〉 :: 〈Some ? exit_label, Jmp exit_label〉 :: code in
     377       ! code_ok ← code_size_opt code ; 
     378       (* atm no data identifier is used in the code, so preamble must be empty *)
     379       return
     380        (mk_pseudo_assembly_program [ ] code code_ok symboltable exit_label ? ?))).
    377381cases daemon
    378382qed.
Note: See TracChangeset for help on using the changeset viewer.