Changeset 2978


Ignore:
Timestamp:
Mar 27, 2013, 4:33:31 PM (4 years ago)
Author:
tranquil
Message:

merged accidentally backtracked changes

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/LIN/LINToASM.ma

    r2976 r2978  
    66
    77include "LIN/LIN.ma".
    8 
    9 
    108
    119(* utilities to provide Identifier's and addresses  *)
     
    1715; address_map : identifier_map SymbolTag Word
    1816; globals_are_in : ∀i : ident.i ∈ globals → i ∈ address_map
     17; fresh_cost_label: Pos
    1918}.
     19
     20definition report_cost:
     21 ∀globals. costlabel → state_monad (ASM_universe globals) unit ≝
     22 λglobals,cl,u.
     23  let clw ≝ word_of_identifier … cl in
     24  if leb (fresh_cost_label … u) clw then
     25   〈mk_ASM_universe … (id_univ … u) (current_funct … u) (ident_map … u)
     26    (label_map … u) (address_map … u) (globals_are_in … u) (succ clw), it〉 
     27  else
     28   〈u,it〉.
    2029
    2130definition new_ASM_universe :
     
    3241  (an_identifier … one (* dummy *))
    3342  (empty_map …) (empty_map …)
    34   (\fst addresses) ?.
     43  (\fst addresses) ? one.
    3544@hide_prf
    3645normalize nodelta
     
    6675  ] in
    6776〈mk_ASM_universe … univ current (ident_map … u) (add … (label_map … u) current lmap)
    68   (address_map … u) (globals_are_in … u), id〉.
     77  (address_map … u) (globals_are_in … u) (fresh_cost_label … u), id〉.
    6978
    7079definition Identifier_of_ident :
     
    8089  ] in
    8190〈mk_ASM_universe … univ (current_funct … u) imap (label_map … u)
    82   (address_map … u) (globals_are_in … u), id〉.
     91  (address_map … u) (globals_are_in … u) (fresh_cost_label … u), id〉.
    8392
    8493definition start_funct_translation :
     
    8796  λg,id_f,u.
    8897    〈mk_ASM_universe … (id_univ … u) (\fst id_f) (ident_map … u) (label_map … u)
    89       (address_map … u) (globals_are_in … u), it〉.
     98      (address_map … u) (globals_are_in … u) (fresh_cost_label … u), it〉.
    9099
    91100definition address_of_ident :
     
    98107λg,u.let 〈id, univ〉 ≝ fresh … (id_univ … u) in
    99108〈mk_ASM_universe … univ (current_funct … u) (ident_map … u) (label_map … u)
    100   (address_map … u) (globals_are_in … u), id〉.
     109  (address_map … u) (globals_are_in … u) (fresh_cost_label … u), id〉.
    101110
    102111definition register_address: Register → [[ acc_a; direct; registr ]] ≝
     
    304313          return Instruction (JMP … INDIRECT_DPTR)
    305314        ]
    306       | COST_LABEL lbl ⇒ return Cost lbl
     315      | COST_LABEL lbl ⇒
     316         !_ report_cost … lbl ;
     317         return Cost lbl
    307318      | COND _ lbl ⇒
    308319        ! l ← Identifier_of_label … lbl;
     
    457468     ! symboltable ← get_symboltable … ;
    458469     ! init ← translate_initialization p ;
     470     ! u ← state_get … ;
    459471     return
    460        (let code ≝
    461         init @ 〈None ?, Call main〉 :: 〈Some ? exit_label, Jmp exit_label〉 :: code in
     472       (
     473        let code ≝
     474        init @
     475         〈None ?, Call main〉 ::
     476         〈Some ? exit_label, Cost (an_identifier … (fresh_cost_label … u))〉 ::
     477         〈None ?, Jmp exit_label〉 :: code in
    462478        ! code_ok ← code_size_opt code ; 
    463479        (* atm no data identifier is used in the code, so preamble must be empty *)
Note: See TracChangeset for help on using the changeset viewer.