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

    r2753 r2754  
    4141          lin_to_asm p.
    4242
    43 (* JHM: object_code and program_size_ok defns added *)
    44 include "ASM/CodeMemory.ma".
    45 
    4643include "ASM/Policy.ma".
    4744(* Equivalent to the inclusion of ASM/Policy.ma, waiting for that slow
     
    5350   sigma_policy_specification 〈\fst program,\snd program〉 sigma policy). *)
    5451   
    55 definition assembler : pseudo_assembly_program → res (object_code × costlabel_map)
     52definition assembler : pseudo_assembly_program → res labelled_object_code
    5653λp.
    5754  let 〈preamble, list_instr〉 ≝ p in
    58   ! list_instr_ok ← opt_to_res ? (msg AssemblyTooLarge) (program_ok_opt ? list_instr);
     55  ! list_instr_ok ← opt_to_res ? (msg AssemblyTooLarge) ?(*(program_ok_opt ? list_instr)*);
    5956  let p' ≝ 〈preamble, list_instr〉 in
    6057  ! sigma_pol ← opt_to_res ? (msg Jump_expansion_failed) (jump_expansion' p');
     
    6259  let pol ≝ λppc. \snd sigma_pol ppc in
    6360  OK ? (assembly p sigma pol).
    64   % [1: @list_instr_ok | cases daemon]
     61  (* % [1: @list_instr_ok | cases daemon] *) cases daemon
    6562qed.
    6663
     
    103100
    104101definition compile : clight_program →
    105   res (object_code × costlabel_map × (𝚺labelled:clight_program. clight_cost_map labelled)) ≝
     102  res (labelled_object_code × (𝚺labelled:clight_program. clight_cost_map labelled)) ≝
    106103λp.
    107104  ! 〈init_cost,p',p〉 ← front_end p;
     
    112109    p'
    113110    (load_code_memory (\fst p))
    114     (\snd p)
     111    (\fst (\snd p))
    115112    k
    116113    in
Note: See TracChangeset for help on using the changeset viewer.