Changeset 699 for src/LIN/LINToASM.ma


Ignore:
Timestamp:
Mar 18, 2011, 2:53:25 PM (9 years ago)
Author:
mulligan
Message:

More or less finished formalisation of LIN.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/LIN/LINToASM.ma

    r698 r699  
    11include "ASM/Util.ma".
    22include "utilities/BitVectorTrieSet.ma".
     3include "utilities/IdentifierTools.ma".
    34include "LIN/LIN.ma".
    45 
    56let rec association (i: Identifier) (l: list (Identifier × nat))
    6                     on l: member i (eq_bv ?) l → nat ≝
    7   match l return λl. member i (eq_bv ?) l → nat with
     7                    on l: member i (eq_bv ?) (map ? ? (fst ? ?) l) → nat ≝
     8  match l return λl. member i (eq_bv ?) (map ? ? (fst ? ?) l) → nat with
    89  [ nil ⇒ λabsd. ?
    910  | cons hd tl ⇒
    10     λprf: member i (eq_bv ?) (cons ? hd tl).
     11    λprf: member i (eq_bv ?) (map ? ? (fst ? ?) (cons ? hd tl)).
    1112      (match eq_bv ? (\fst hd) i return λb. eq_bv ? (\fst hd) i = b → nat with
    1213      [ true ⇒ λeq_prf. \snd hd
     
    2627
    2728definition statement_labels ≝
    28   λg: list (Identifier × nat).
     29  λg: list Identifier.
    2930  λs: LINStatement g.
    3031  match s with
     
    3738
    3839definition function_labels_internal ≝
    39   λglobals: list (Identifier × nat).
     40  λglobals: list Identifier.
    4041  λlabels: BitVectorTrieSet 8.
    4142  λstatement: LINStatement globals.
     
    4546definition function_labels: ∀A. ∀globals. ∀f. BitVectorTrieSet 8 ≝
    4647  λA: Type[0].
    47   λglobals: list (Identifier × nat).
     48  λglobals: list Identifier.
    4849  λf: A × (LINFunctionDefinition globals).
    4950  let 〈ignore, fun_def〉 ≝ f in
     
    5657definition program_labels_internal: ∀A. ∀globals. ∀labels. ∀funct. BitVectorTrieSet 8 ≝
    5758  λA: Type[0].
    58   λglobals: list (Identifier × nat).
     59  λglobals: list Identifier.
    5960  λlabels: BitVectorTrieSet 8.
    6061  λfunct: A × (LINFunctionDefinition globals).
     
    6263   
    6364definition program_labels ≝
    64   λglobals: list (Identifier × nat).
    6565  λprogram.
    66     foldl ? ? (program_labels_internal ? globals)
    67               (set_empty 8) (LIN_Pr_funs globals program).
     66    foldl ? ? (program_labels_internal ? (map ? ? (fst ? ?) (LIN_Pr_vars program)))
     67              (set_empty 8) (LIN_Pr_funs program).
    6868   
    6969definition data_of_int ≝ λbv. DATA bv.
     
    7575definition translate_statements ≝
    7676  λglobals: list (Identifier × nat).
    77   λlin_statement: LINStatement globals.
     77  λglobals_old: list Identifier.
     78  λprf: ∀i: Identifier. member i (eq_bv ?) globals_old → member i (eq_bv ?) (map ? ? (fst ? ?) globals).
     79  λlin_statement: LINStatement globals_old.
    7880  match lin_statement with
    7981  [ LIN_St_Goto lbl ⇒ [ Jmp lbl ]
     
    220222  | LIN_St_Store ⇒ [ Instruction (MOVX ? (inr ? ? 〈EXT_INDIRECT_DPTR, ACC_A〉)) ]
    221223  | LIN_St_Address addr proof ⇒
    222     let look ≝ association addr globals proof in
     224    let look ≝ association addr globals (prf ? proof) in
    223225      [ Instruction (MOV ? (inl ? ? (inl ? ? (inr ? ? (〈DPTR, (data16_of_int look)〉))))) ]
    224226  | LIN_St_CondAcc lbl ⇒
     
    233235definition translate_code ≝
    234236  λglobals: list (Identifier × nat).
    235   λcode: list (LINStatement globals).
    236     flatten ? (map ? ? (translate_statements globals) code).
     237  λglobals_old: list Identifier.
     238  λprf.
     239  λcode: list (LINStatement globals_old).
     240    flatten ? (map ? ? (translate_statements globals globals_old prf) code).
    237241   
    238242definition translate_fun_def ≝
    239   λglobals.
     243  λglobals.λglobals_old.λprf.
    240244  λid_def.
    241245    let 〈id, def〉 ≝ id_def in
    242246    match def with
    243     [ LIN_Fu_Internal code ⇒ (Label id) :: (translate_code globals code)
     247    [ LIN_Fu_Internal code ⇒ (Label id) :: (translate_code globals globals_old prf code)
    244248    | _ ⇒ [ ]
    245249    ].
     
    247251definition translate_functs ≝
    248252  λglobals.
     253  λglobals_old.
     254  λprf.
    249255  λexit_label.
    250256  λmain.
     
    255261    | Some main' ⇒ [ Call main' ; Label exit_label ; Jmp exit_label ]
    256262    ] in
    257       preamble @ (flatten ? (map ? ? (translate_fun_def globals) functs)).
     263      preamble @ (flatten ? (map ? ? (translate_fun_def globals globals_old prf) functs)).
    258264
    259265definition globals_addr_internal ≝
     
    266272definition globals_addr ≝
    267273  λl.
    268     foldl ? ? globals_addr_internal 〈[ ], 0〉 l.
     274    \fst (foldl ? ? globals_addr_internal 〈[ ], 0〉 l).
    269275     
    270 (*   
     276(* dpm: plays the role of the string "_exit" in the O'caml source *)
     277axiom identifier_prefix: Identifier.
     278
     279(*
    271280definition translate ≝
    272281  λp.
    273282  let prog_lbls ≝ program_labels p in
    274   let exit_label ≝
    275    
    276 let translate p =
    277   let prog_lbls = prog_labels p in
    278   let exit_label = Label.Gen.fresh_prefix prog_lbls "_exit" in
    279   let glbls_addr = globals_addr p.LIN.vars in
    280   let p =
    281     { ASM.ppreamble = p.LIN.vars ;
    282       ASM.pexit_label = exit_label ;
    283       ASM.pcode =
    284         translate_functs glbls_addr exit_label p.LIN.main p.LIN.functs ;
    285       ASM.phas_main = p.LIN.main <> None } in
    286   ASMInterpret.assembly p
    287   *)
     283  let exit_label ≝ fresh_prefix prog_lbls identifier_prefix in
     284  let global_addr ≝ globals_addr (LIN_Pr_vars p) in
     285    〈global_addr, translate_functs global_addr (map ? ? (fst ? ?) (LIN_Pr_vars p)) ? exit_label (LIN_Pr_main p) (LIN_Pr_funs p)〉.
     286    *)
Note: See TracChangeset for help on using the changeset viewer.