Changeset 1268 for src/LIN


Ignore:
Timestamp:
Sep 26, 2011, 2:52:22 PM (8 years ago)
Author:
sacerdot
Message:

1) AST/Identifier.ma no longer used, utilities/IdentifierTools no longer used
2) LIN/LINToAsm porting completed but:

a) a small lemma need to be proved (easy, but boring because of foldl)
b) the code is BUGGED: labels coming from different universes

(for function names and for each function) are merged together.
However, they should be kept clearly separate. We will discuss how
to fix this issue at the next meeting in Paris.
Note: keeping 'em distinct from the very beginning also requires some
work, since some labels are entered directly by the user.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/LIN/LINToASM.ma

    r1264 r1268  
    11include "ASM/Util.ma".
    22include "utilities/BitVectorTrieSet.ma".
    3 include "utilities/IdentifierTools.ma".
    43include "LIN/LIN.ma".
    54
     
    9493      [ joint_instr_extension ext ⇒ ⊥
    9594      | joint_instr_comment comment ⇒ Comment comment
    96       | joint_instr_cost_label lbl ⇒ Cost (Identifier_of_costlabel lbl)
     95      | joint_instr_cost_label lbl ⇒ Cost (word_of_identifier ? lbl)
    9796      | joint_instr_pop _ ⇒ Instruction (POP ? accumulator_address)
    9897      | joint_instr_push _ ⇒ Instruction (PUSH ? accumulator_address)
     
    247246qed.
    248247
     248(*CSC: XXXXXXXXXXX looks bad: what invariant is needed here? *)
     249definition ident_of_label: label → ident ≝
     250 λl. an_identifier … (word_of_identifier … l).
     251
    249252definition build_translated_statement ≝
    250253  λglobals.
     
    252255  λprf.
    253256  λstatement: lin_statement globals_old.
    254     〈\fst statement, translate_statements globals globals_old prf (\snd statement)〉.
     257    〈option_map … ident_of_label (\fst statement), translate_statements globals globals_old prf (\snd statement)〉.
    255258
    256259definition translate_code ≝
     
    269272    //
    270273  | #G2 #G02 #IH (* CSC: understand here *)
    271     whd in ⊢ (% → %)
    272     normalize in ⊢ (% → %)
    273     //
    274   ]
     274    whd in ⊢ (% → %) whd in match build_translated_statement normalize nodelta
     275    cases (\fst G2) normalize // ]
    275276qed.
    276277
    277278definition translate_fun_def ≝
    278   λglobals.
     279  λglobals: list (ident × nat).
    279280  λglobals_old.
    280281  λprf.
    281   λid_def: ? × (fundef … (Σcode:list (lin_statement globals_old).?)).
     282  λid_def.
    282283    let 〈id, def〉 ≝ id_def in
    283284    match def with
    284     [ Internal code_proof ⇒
     285    [ Internal int ⇒
     286      let code_proof ≝ joint_if_code … (lin_params globals_old) int in
    285287      match translate_code globals globals_old prf (pi1 ?? code_proof) return λtranscode. well_formed_P ? ? transcode → list labelled_instruction with
    286288      [ nil ⇒ λprf2. ⊥
     
    307309  λfuncts.
    308310  let preamble ≝ [ 〈None ?, Call main〉 ; 〈Some ? exit_label, Jmp exit_label〉 ] in
    309    preamble @ (flatten ? (map ? ? (translate_fun_def globals globals_old prf) functs)).
     311   preamble @
     312    (flatten ? (map ? ? (translate_fun_def globals globals_old prf) functs)).
    310313
    311314(*CSC: region silently thrown away here *)
     
    320323  in
    321324    \fst (foldl ? ? globals_addr_internal 〈[ ], 0〉 l).
    322      
     325
    323326(* dpm: plays the role of the string "_exit" in the O'caml source *)
    324 axiom identifier_prefix: Identifier.
     327axiom identifier_prefix: Word.
     328(*CSC: XXXXXXX wrong anyway since labels from different functions can now
     329  clash with each other and with names of functions *)
     330axiom fresh_prefix: BitVectorTrieSet 16 → Word → Word.
    325331
    326332(* dpm: fresh prefix stuff needs unifying with brian *)
     
    328334  λp.
    329335  let prog_lbls ≝ program_labels … p in
    330   let exit_label ≝ ?(*fresh_prefix … prog_lbls identifier_prefix*) in
     336  let exit_label ≝ fresh_prefix prog_lbls identifier_prefix in
    331337  let global_addr ≝ globals_addr (prog_vars … p) in
    332338  let global_addr' ≝ map ?? (λx_off. let 〈x,off〉 ≝ x_off in 〈word_of_identifier ? x,off〉) global_addr in
    333     〈global_addr', translate_functs global_addr (prog_var_names … p) ? exit_label (word_of_identifier … (prog_main … p)) ?(*(prog_funct ?? p)*)〉.
    334 [ generalize in match (prog_funct ?? p) #X whd in X:(?(??%)) whd in X:(?(??(?%)))
    335 | #i normalize nodelta whd in match prog_var_names normalize nodelta elim (prog_vars … p)
    336   [ // | #hd #tl #H1 #H2 normalize in ⊢ (???(????%))   
     339    〈global_addr', translate_functs global_addr (prog_var_names … p) ? exit_label (word_of_identifier … (prog_main … p)) (prog_funct … p)〉.
     340 #i normalize nodelta -global_addr' global_addr exit_label prog_lbls;
     341 normalize in match prog_var_names normalize nodelta
     342 elim (prog_vars … p) //
     343 #hd #tl #IH whd in ⊢ (% → %)
     344 whd in match globals_addr normalize nodelta
     345 whd in match (foldl ???? (hd::tl)) normalize nodelta
     346 cases hd * #id #reg #size normalize nodelta
     347 cases daemon (*CSC: provable using a pair of lemmas over foldl *)
     348qed.
Note: See TracChangeset for help on using the changeset viewer.