Changeset 699 for src/LIN


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

More or less finished formalisation of LIN.

Location:
src/LIN
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/LIN/LIN.ma

    r698 r699  
    44include "ASM/I8051.ma".
    55include "common/AST.ma".
    6 include "utilities/StringTools.ma".
    76
    87alias id "ASMOp1" = "cic:/matita/cerco/ASM/I8051/Op1.ind(1,0,0)".
    98alias id "ASMOp2" = "cic:/matita/cerco/ASM/I8051/Op2.ind(1,0,0)".
    109
     10(* dpm: should go to standard library *)
    1111let rec member (i: Identifier) (eq_i: Identifier → Identifier → bool)
    12                (g: list (Identifier × nat)) on g: Prop ≝
     12               (g: list Identifier) on g: Prop ≝
    1313  match g with
    1414  [ nil ⇒ False
    1515  | cons hd tl ⇒
    16       bool_to_Prop (eq_i (fst ? ? hd) i) ∨ member i eq_i tl
     16      bool_to_Prop (eq_i hd i) ∨ member i eq_i tl
    1717  ].
    1818
    19 inductive LINStatement (globals: list (Identifier × nat)): Type[0] ≝
     19inductive LINStatement (globals: list Identifier): Type[0] ≝
    2020  | LIN_St_Goto: Identifier → LINStatement globals
    2121  | LIN_St_Label: Identifier → LINStatement globals
    2222  | LIN_St_Comment: String → LINStatement globals
    23   | LIN_St_CostLabel: CostLabel → LINStatement globals
     23  | LIN_St_CostLabel: Identifier → LINStatement globals
    2424  | LIN_St_Int: Register → Byte → LINStatement globals
    2525  | LIN_St_Pop: LINStatement globals
     
    4040definition LINInternalFunction ≝ λglobals. list (LINStatement globals).
    4141
    42 inductive LINFunctionDefinition (globals: list (Identifier × nat)): Type[0] ≝
     42inductive LINFunctionDefinition (globals: list Identifier): Type[0] ≝
    4343  LIN_Fu_Internal: LINInternalFunction globals → LINFunctionDefinition globals
    4444| LIN_Fu_External: ExternalFunction → LINFunctionDefinition globals.
    4545
    46 record LINProgram (globals: list (Identifier × nat)): Type[0] ≝
     46record LINProgram: Type[0] ≝
    4747{
    4848  LIN_Pr_vars: list (Identifier × nat);
    49   LIN_Pr_funs: list (Identifier × (LINFunctionDefinition globals));
     49  LIN_Pr_funs: list (Identifier × (LINFunctionDefinition (map ? ? (fst ? ?) LIN_Pr_vars)));
    5050  LIN_Pr_main: option Identifier
    5151}.
     52
     53definition LIN_Pr_vars:
     54    LINProgram → list (Identifier × nat).
     55  # r
     56  cases r
     57  # H1 # H2 #H3
     58  @ H1
     59qed.
     60
     61definition LIN_Pr_funs:
     62  ∀p: LINProgram.
     63    list (Identifier × (LINFunctionDefinition (map ? ? (fst ? ?) (LIN_Pr_vars p)))).
     64  # r
     65  cases r
     66  # H1 # H2 #H3
     67  @ H2
     68qed.
  • 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.