Changeset 696 for src/LIN/LINToASM.ma


Ignore:
Timestamp:
Mar 18, 2011, 1:01:58 PM (10 years ago)
Author:
mulligan
Message:

Added missing I8051 file and completed most of LIN formalisation.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/LIN/LINToASM.ma

    r691 r696  
    235235  λcode: list (LINStatement globals).
    236236    flatten ? (map ? ? (translate_statements globals) code).
     237   
     238definition translate_fun_def ≝
     239  λglobals.
     240  λid_def.
     241    let 〈id, def〉 ≝ id_def in
     242    match def with
     243    [ LIN_Fu_Internal code ⇒ (Label id) :: (translate_code globals code)
     244    | _ ⇒ [ ]
     245    ].
     246   
     247definition translate_functs ≝
     248  λglobals.
     249  λexit_label.
     250  λmain.
     251  λfuncts.
     252  let preamble ≝
     253    match main with
     254    [ None ⇒ [ ]
     255    | Some main' ⇒ [ Call main' ; Label exit_label ; Jmp exit_label ]
     256    ] in
     257      preamble @ (flatten ? (map ? ? (translate_fun_def globals) functs)).
     258
     259definition globals_addr_internal ≝
     260  λres_offset.
     261  λx_size: Identifier × nat.
     262    let 〈res, offset〉 ≝ res_offset in
     263    let 〈x, size〉 ≝ x_size in
     264      〈〈x, offset〉 :: res, offset + size〉.
     265
     266definition globals_addr ≝
     267  λl.
     268    foldl ? ? globals_addr_internal 〈[ ], 0〉 l.
     269       
     270definition translate ≝
     271  λp.
     272  let prog_lbls ≝ program_labels p in
     273  let exit_label ≝
     274   
     275let translate p =
     276  let prog_lbls = prog_labels p in
     277  let exit_label = Label.Gen.fresh_prefix prog_lbls "_exit" in
     278  let glbls_addr = globals_addr p.LIN.vars in
     279  let p =
     280    { ASM.ppreamble = p.LIN.vars ;
     281      ASM.pexit_label = exit_label ;
     282      ASM.pcode =
     283        translate_functs glbls_addr exit_label p.LIN.main p.LIN.functs ;
     284      ASM.phas_main = p.LIN.main <> None } in
     285  ASMInterpret.assembly p
Note: See TracChangeset for help on using the changeset viewer.