 Timestamp:
 Mar 18, 2011, 2:53:25 PM (9 years ago)
 Location:
 src/LIN
 Files:

 2 edited
Legend:
 Unmodified
 Added
 Removed

src/LIN/LIN.ma
r698 r699 4 4 include "ASM/I8051.ma". 5 5 include "common/AST.ma". 6 include "utilities/StringTools.ma".7 6 8 7 alias id "ASMOp1" = "cic:/matita/cerco/ASM/I8051/Op1.ind(1,0,0)". 9 8 alias id "ASMOp2" = "cic:/matita/cerco/ASM/I8051/Op2.ind(1,0,0)". 10 9 10 (* dpm: should go to standard library *) 11 11 let rec member (i: Identifier) (eq_i: Identifier → Identifier → bool) 12 (g: list (Identifier × nat)) on g: Prop ≝12 (g: list Identifier) on g: Prop ≝ 13 13 match g with 14 14 [ nil ⇒ False 15 15  cons hd tl ⇒ 16 bool_to_Prop (eq_i (fst ? ? hd)i) ∨ member i eq_i tl16 bool_to_Prop (eq_i hd i) ∨ member i eq_i tl 17 17 ]. 18 18 19 inductive LINStatement (globals: list (Identifier × nat)): Type[0] ≝19 inductive LINStatement (globals: list Identifier): Type[0] ≝ 20 20  LIN_St_Goto: Identifier → LINStatement globals 21 21  LIN_St_Label: Identifier → LINStatement globals 22 22  LIN_St_Comment: String → LINStatement globals 23  LIN_St_CostLabel: CostLabel→ LINStatement globals23  LIN_St_CostLabel: Identifier → LINStatement globals 24 24  LIN_St_Int: Register → Byte → LINStatement globals 25 25  LIN_St_Pop: LINStatement globals … … 40 40 definition LINInternalFunction ≝ λglobals. list (LINStatement globals). 41 41 42 inductive LINFunctionDefinition (globals: list (Identifier × nat)): Type[0] ≝42 inductive LINFunctionDefinition (globals: list Identifier): Type[0] ≝ 43 43 LIN_Fu_Internal: LINInternalFunction globals → LINFunctionDefinition globals 44 44  LIN_Fu_External: ExternalFunction → LINFunctionDefinition globals. 45 45 46 record LINProgram (globals: list (Identifier × nat)): Type[0] ≝46 record LINProgram: Type[0] ≝ 47 47 { 48 48 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))); 50 50 LIN_Pr_main: option Identifier 51 51 }. 52 53 definition LIN_Pr_vars: 54 LINProgram → list (Identifier × nat). 55 # r 56 cases r 57 # H1 # H2 #H3 58 @ H1 59 qed. 60 61 definition 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 68 qed. 
src/LIN/LINToASM.ma
r698 r699 1 1 include "ASM/Util.ma". 2 2 include "utilities/BitVectorTrieSet.ma". 3 include "utilities/IdentifierTools.ma". 3 4 include "LIN/LIN.ma". 4 5 5 6 let 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 with7 on l: member i (eq_bv ?) (map ? ? (fst ? ?) l) → nat ≝ 8 match l return λl. member i (eq_bv ?) (map ? ? (fst ? ?) l) → nat with 8 9 [ nil ⇒ λabsd. ? 9 10  cons hd tl ⇒ 10 λprf: member i (eq_bv ?) ( cons ? hd tl).11 λprf: member i (eq_bv ?) (map ? ? (fst ? ?) (cons ? hd tl)). 11 12 (match eq_bv ? (\fst hd) i return λb. eq_bv ? (\fst hd) i = b → nat with 12 13 [ true ⇒ λeq_prf. \snd hd … … 26 27 27 28 definition statement_labels ≝ 28 λg: list (Identifier × nat).29 λg: list Identifier. 29 30 λs: LINStatement g. 30 31 match s with … … 37 38 38 39 definition function_labels_internal ≝ 39 λglobals: list (Identifier × nat).40 λglobals: list Identifier. 40 41 λlabels: BitVectorTrieSet 8. 41 42 λstatement: LINStatement globals. … … 45 46 definition function_labels: ∀A. ∀globals. ∀f. BitVectorTrieSet 8 ≝ 46 47 λA: Type[0]. 47 λglobals: list (Identifier × nat).48 λglobals: list Identifier. 48 49 λf: A × (LINFunctionDefinition globals). 49 50 let 〈ignore, fun_def〉 ≝ f in … … 56 57 definition program_labels_internal: ∀A. ∀globals. ∀labels. ∀funct. BitVectorTrieSet 8 ≝ 57 58 λA: Type[0]. 58 λglobals: list (Identifier × nat).59 λglobals: list Identifier. 59 60 λlabels: BitVectorTrieSet 8. 60 61 λfunct: A × (LINFunctionDefinition globals). … … 62 63 63 64 definition program_labels ≝ 64 λglobals: list (Identifier × nat).65 65 λprogram. 66 foldl ? ? (program_labels_internal ? globals)67 (set_empty 8) (LIN_Pr_funs globalsprogram).66 foldl ? ? (program_labels_internal ? (map ? ? (fst ? ?) (LIN_Pr_vars program))) 67 (set_empty 8) (LIN_Pr_funs program). 68 68 69 69 definition data_of_int ≝ λbv. DATA bv. … … 75 75 definition translate_statements ≝ 76 76 λ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. 78 80 match lin_statement with 79 81 [ LIN_St_Goto lbl ⇒ [ Jmp lbl ] … … 220 222  LIN_St_Store ⇒ [ Instruction (MOVX ? (inr ? ? 〈EXT_INDIRECT_DPTR, ACC_A〉)) ] 221 223  LIN_St_Address addr proof ⇒ 222 let look ≝ association addr globals proofin224 let look ≝ association addr globals (prf ? proof) in 223 225 [ Instruction (MOV ? (inl ? ? (inl ? ? (inr ? ? (〈DPTR, (data16_of_int look)〉))))) ] 224 226  LIN_St_CondAcc lbl ⇒ … … 233 235 definition translate_code ≝ 234 236 λ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). 237 241 238 242 definition translate_fun_def ≝ 239 λglobals. 243 λglobals.λglobals_old.λprf. 240 244 λid_def. 241 245 let 〈id, def〉 ≝ id_def in 242 246 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) 244 248  _ ⇒ [ ] 245 249 ]. … … 247 251 definition translate_functs ≝ 248 252 λglobals. 253 λglobals_old. 254 λprf. 249 255 λexit_label. 250 256 λmain. … … 255 261  Some main' ⇒ [ Call main' ; Label exit_label ; Jmp exit_label ] 256 262 ] in 257 preamble @ (flatten ? (map ? ? (translate_fun_def globals ) functs)).263 preamble @ (flatten ? (map ? ? (translate_fun_def globals globals_old prf) functs)). 258 264 259 265 definition globals_addr_internal ≝ … … 266 272 definition globals_addr ≝ 267 273 λl. 268 foldl ? ? globals_addr_internal 〈[ ], 0〉 l.274 \fst (foldl ? ? globals_addr_internal 〈[ ], 0〉 l). 269 275 270 (* 276 (* dpm: plays the role of the string "_exit" in the O'caml source *) 277 axiom identifier_prefix: Identifier. 278 279 (* 271 280 definition translate ≝ 272 281 λp. 273 282 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.