Changeset 696 for src/LIN


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

Added missing I8051 file and completed most of LIN formalisation.

Location:
src/LIN
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/LIN/LIN.ma

    r688 r696  
    11include "arithmetics/nat.ma".
    2 include "cerco/String.ma".
     2include "ASM/String.ma".
    33
    4 include "cerco-intermediate-languages/ASM/I8051.ma".
    5 include "cerco-intermediate-languages/common/AST.ma".
    6 include "cerco-intermediate-languages/utilities/StringTools.ma".
     4include "ASM/I8051.ma".
     5include "common/AST.ma".
     6include "utilities/StringTools.ma".
    77
    8 alias id "ASMOp1" = "cic:/matita/cerco-intermediate-languages/ASM/I8051/Op1.ind(1,0,0)".
    9 alias id "ASMOp2" = "cic:/matita/cerco-intermediate-languages/ASM/I8051/Op2.ind(1,0,0)".
     8alias id "ASMOp1" = "cic:/matita/cerco/ASM/I8051/Op1.ind(1,0,0)".
     9alias id "ASMOp2" = "cic:/matita/cerco/ASM/I8051/Op2.ind(1,0,0)".
    1010
    1111let rec member (i: Identifier) (eq_i: Identifier → Identifier → bool)
  • 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.