Changeset 2976


Ignore:
Timestamp:
Mar 27, 2013, 4:09:20 PM (4 years ago)
Author:
tranquil
Message:
  • a dangling trivial proof obligation is now closed
File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/LIN/LINToASM.ma

    r2975 r2976  
    66
    77include "LIN/LIN.ma".
     8
     9
    810
    911(* utilities to provide Identifier's and addresses  *)
     
    1517; address_map : identifier_map SymbolTag Word
    1618; globals_are_in : ∀i : ident.i ∈ globals → i ∈ address_map
    17 ; fresh_cost_label: Pos
    1819}.
    19 
    20 definition 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〉.
    2920
    3021definition new_ASM_universe :
     
    4132  (an_identifier … one (* dummy *))
    4233  (empty_map …) (empty_map …)
    43   (\fst addresses) ? one.
     34  (\fst addresses) ?.
    4435@hide_prf
    4536normalize nodelta
     
    7566  ] in
    7667〈mk_ASM_universe … univ current (ident_map … u) (add … (label_map … u) current lmap)
    77   (address_map … u) (globals_are_in … u) (fresh_cost_label … u), id〉.
     68  (address_map … u) (globals_are_in … u), id〉.
    7869
    7970definition Identifier_of_ident :
     
    8980  ] in
    9081〈mk_ASM_universe … univ (current_funct … u) imap (label_map … u)
    91   (address_map … u) (globals_are_in … u) (fresh_cost_label … u), id〉.
     82  (address_map … u) (globals_are_in … u), id〉.
    9283
    9384definition start_funct_translation :
     
    9687  λg,id_f,u.
    9788    〈mk_ASM_universe … (id_univ … u) (\fst id_f) (ident_map … u) (label_map … u)
    98       (address_map … u) (globals_are_in … u) (fresh_cost_label … u), it〉.
     89      (address_map … u) (globals_are_in … u), it〉.
    9990
    10091definition address_of_ident :
     
    10798λg,u.let 〈id, univ〉 ≝ fresh … (id_univ … u) in
    10899〈mk_ASM_universe … univ (current_funct … u) (ident_map … u) (label_map … u)
    109   (address_map … u) (globals_are_in … u) (fresh_cost_label … u), id〉.
     100  (address_map … u) (globals_are_in … u), id〉.
    110101
    111102definition register_address: Register → [[ acc_a; direct; registr ]] ≝
     
    313304          return Instruction (JMP … INDIRECT_DPTR)
    314305        ]
    315       | COST_LABEL lbl ⇒
    316          !_ report_cost … lbl ;
    317          return Cost lbl
     306      | COST_LABEL lbl ⇒ return Cost lbl
    318307      | COND _ lbl ⇒
    319308        ! l ← Identifier_of_label … lbl;
     
    417406〈None ?, Instruction (MOV ? (inl ?? (inl ?? (inr ?? 〈DPTR, DATA16 (bitvector_of_Z … start_dptr)〉))))〉 ::
    418407\snd (foldr ?? f 〈start_dptr, [ ]〉 data).
     408@I qed.
    419409
    420410definition translate_initialization : ∀p : lin_program.
     
    467457     ! symboltable ← get_symboltable … ;
    468458     ! init ← translate_initialization p ;
    469      ! u ← state_get … ;
    470459     return
    471        (
    472         let code ≝
    473         init @
    474          〈None ?, Call main〉 ::
    475          〈Some ? exit_label, Cost (an_identifier … (fresh_cost_label … u))〉 ::
    476          〈None ?, Jmp exit_label〉 :: code in
     460       (let code ≝
     461        init @ 〈None ?, Call main〉 :: 〈Some ? exit_label, Jmp exit_label〉 :: code in
    477462        ! code_ok ← code_size_opt code ; 
    478463        (* atm no data identifier is used in the code, so preamble must be empty *)
Note: See TracChangeset for help on using the changeset viewer.