Changeset 1264


Ignore:
Timestamp:
Sep 23, 2011, 6:44:20 PM (8 years ago)
Author:
sacerdot
Message:

Almost ported to new Joint syntax.

Location:
src/LIN
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/LIN/LIN.ma

    r1250 r1264  
    2626     match l' with [ None ⇒ None … | Some l'' ⇒ if eq_identifier … l l'' then Some … x else None ?]) code).
    2727
     28definition lin_function ≝ λglobals. joint_function … (lin_params globals).
     29
    2830definition lin_program ≝ joint_program lin_params.
  • src/LIN/LINToASM.ma

    r1245 r1264  
    33include "utilities/IdentifierTools.ma".
    44include "LIN/LIN.ma".
    5  
     5
    66let rec association (i: ident) (l: list (ident × nat))
    77                    on l: member i (eq_identifier ?) (map ? ? (fst ? ?) l) → nat ≝
     
    2828definition statement_labels ≝
    2929  λg: list ident.
    30   λs: (option label) × (lin_statement g).
     30  λs: lin_statement g.
    3131  let 〈label, instr〉 ≝ s in
    3232  let generated ≝
     
    3939      ]
    4040    | joint_st_return ⇒ set_empty ?
    41     | joint_st_goto lbl ⇒ set_insert ? (word_of_identifier ? lbl) (set_empty ?)
    42     | joint_st_extension _ ⇒ set_empty ?
    43     ]
     41    | joint_st_goto lbl ⇒ set_insert ? (word_of_identifier ? lbl) (set_empty ?) ]
    4442  in
    4543  match label with
     
    5149  λglobals: list ident.
    5250  λlabels: BitVectorTrieSet ?.
    53   λstatement: (option label) × (lin_statement globals).
     51  λstatement: lin_statement globals.
    5452    set_union ? labels (statement_labels globals statement).
    5553
    56 (*
     54
    5755(* dpm: A = Identifier *)
    5856definition function_labels: ∀A. ∀globals. ∀f. BitVectorTrieSet ? ≝
    5957  λA: Type[0].
    6058  λglobals: list ident.
    61   λf: A × (lin_function_definition globals).
     59  λf: A × (lin_function globals).
    6260  let 〈ignore, fun_def〉 ≝ f in
    6361  match fun_def return λ_. BitVectorTrieSet ? with
    6462  [ Internal stmts ⇒
    65       foldl ? ? (function_labels_internal globals) (set_empty ?) stmts
     63      foldl ? ? (function_labels_internal globals) (set_empty ?) (pi1 … (joint_if_code ?? stmts))
    6664  | External _ ⇒ set_empty ?
    6765  ].
     
    7169  λglobals: list ident.
    7270  λlabels: BitVectorTrieSet ?.
    73   λfunct: A × (lin_function_definition globals).
     71  λfunct: A × (lin_function globals).
    7472    set_union ? labels (function_labels ? globals funct).
    75    
     73
     74(* CSC: here we are silently throwing away the region information *)
    7675definition program_labels ≝
    77   λprogram.
    78     foldl ? ? (program_labels_internal ? (map ? ? (fst ? ?) (lin_pr_vars program)))
    79               (set_empty ?) (lin_pr_funcs program).
    80 *)
     76 λprogram: lin_program.
     77    foldl … (program_labels_internal … (map … (λx. fst … (fst … x)) (prog_vars … program)))
     78              (set_empty …) (prog_funct … program).
     79
    8180definition data_of_int ≝ λbv. DATA bv.
    8281definition data16_of_int ≝ λbv. DATA16 (bitvector_of_nat 16 bv).
     
    8786  λglobals_old: list ident.
    8887  λprf: ∀i: ident. member i (eq_identifier ?) globals_old → member i (eq_identifier ?) (map ? ? (fst ? ?) globals).
    89   λstatement: lin_statement globals_old.
     88  λstatement: pre_lin_statement globals_old.
    9089  match statement with
    9190  [ joint_st_goto lbl ⇒ Jmp (word_of_identifier ? lbl)
    92   | joint_st_extension ext ⇒ ⊥
    9391  | joint_st_return ⇒ Instruction (RET ?)
    9492  | joint_st_sequential instr _ ⇒
    9593      match instr with
    96       [ joint_instr_comment comment ⇒ Comment comment
     94      [ joint_instr_extension ext ⇒ ⊥
     95      | joint_instr_comment comment ⇒ Comment comment
    9796      | joint_instr_cost_label lbl ⇒ Cost (Identifier_of_costlabel lbl)
    9897      | joint_instr_pop _ ⇒ Instruction (POP ? accumulator_address)
     
    105104        | DivuModu ⇒ Instruction (DIV ? ACC_A ACC_B)
    106105        ]
    107       | joint_instr_op1 op1 _
     106      | joint_instr_op1 op1 _ _
    108107        match op1 with
    109108        [ Cmpl ⇒ Instruction (CPL ? ACC_A)
    110109        | Inc ⇒ Instruction (INC ? ACC_A)
    111110        ]
    112       | joint_instr_op2 op2 _ reg ⇒
     111      | joint_instr_op2 op2 _ _ reg ⇒
    113112        match op2 with
    114113        [ Add ⇒
     
    252251  λglobals_old.
    253252  λprf.
    254   λstatement: (option label) × (lin_statement globals_old).
     253  λstatement: lin_statement globals_old.
    255254    〈\fst statement, translate_statements globals globals_old prf (\snd statement)〉.
    256255
     
    259258  λglobals_old: list ident.
    260259  λprf.
    261   λcode: list ((option label) × (lin_statement globals_old)).
     260  λcode: list (lin_statement globals_old).
    262261    map ? ? (build_translated_statement globals globals_old prf) code.
    263262   
     
    280279  λglobals_old.
    281280  λprf.
    282   λid_def.
     281  λid_def: ? × (fundef … (Σcode:list (lin_statement globals_old).?)).
    283282    let 〈id, def〉 ≝ id_def in
    284283    match def with
    285     [ lin_fu_internal code proof ⇒
    286       match translate_code globals globals_old prf code return λtranscode. well_formed_P ? ? transcode → list labelled_instruction with
     284    [ Internal code_proof ⇒
     285      match translate_code globals globals_old prf (pi1 ?? code_proof) return λtranscode. well_formed_P ? ? transcode → list labelled_instruction with
    287286      [ nil ⇒ λprf2. ⊥
    288287      | cons hd tl ⇒ λ_.
     
    294293            | None ⇒ 〈None ?, \snd r〉
    295294            ]) rest
    296       ] (translate_code_preserves_WellFormedP globals globals_old prf code proof)
    297     | _ ⇒ [ ]
     295      ] (translate_code_preserves_WellFormedP globals globals_old prf (pi1 ?? code_proof) (pi2 ?? code_proof))
     296    | External _ ⇒ [ ]
    298297    ].
    299     @ prf2
     298@prf2
    300299qed.
    301300   
     
    307306  λmain.
    308307  λfuncts.
    309   let preamble ≝
    310     match main with
    311     [ None ⇒ [ ]
    312     | Some main' ⇒ [ 〈None ?, Call main'〉 ; 〈Some ? exit_label, Jmp exit_label〉 ]
    313     ] in
    314       preamble @ (flatten ? (map ? ? (translate_fun_def globals globals_old prf) functs)).
    315 
    316 definition globals_addr_internal ≝
    317   λres_offset.
    318   λx_size: ident × nat.
     308  let preamble ≝ [ 〈None ?, Call main〉 ; 〈Some ? exit_label, Jmp exit_label〉 ] in
     309   preamble @ (flatten ? (map ? ? (translate_fun_def globals globals_old prf) functs)).
     310
     311(*CSC: region silently thrown away here *)
     312definition globals_addr ≝
     313 λl.
     314  let globals_addr_internal ≝
     315   λres_offset.
     316   λx_size: ident × region × nat.
    319317    let 〈res, offset〉 ≝ res_offset in
    320     let 〈x, size〉 ≝ x_size in
    321       〈〈x, offset〉 :: res, offset + size〉.
    322 
    323 definition globals_addr ≝
    324   λl.
     318    let 〈x, region, size〉 ≝ x_size in
     319      〈〈x, offset〉 :: res, offset + size〉
     320  in
    325321    \fst (foldl ? ? globals_addr_internal 〈[ ], 0〉 l).
    326322     
     
    329325
    330326(* dpm: fresh prefix stuff needs unifying with brian *)
    331 
    332 (*
    333 definition translate ≝
     327definition translate : lin_program → pseudo_assembly_program ≝
    334328  λp.
    335   let prog_lbls ≝ program_labels p in
    336   let exit_label ≝ fresh_prefix prog_lbls identifier_prefix in
    337   let global_addr ≝ globals_addr (LIN_Pr_vars p) in
    338     〈global_addr, translate_functs global_addr (map ? ? (fst ? ?) (LIN_Pr_vars p)) ? exit_label (LIN_Pr_main p) (LIN_Pr_funs p)〉.
    339 *)
     329  let prog_lbls ≝ program_labels … p in
     330  let exit_label ≝ ?(*fresh_prefix … prog_lbls identifier_prefix*) in
     331  let global_addr ≝ globals_addr (prog_vars … p) in
     332  let global_addr' ≝ map ?? (λx_off. let 〈x,off〉 ≝ x_off in 〈word_of_identifier ? x,off〉) global_addr in
     333    〈global_addr', translate_functs global_addr (prog_var_names … p) ? exit_label (word_of_identifier … (prog_main … p)) ?(*(prog_funct ?? p)*)〉.
     334[ generalize in match (prog_funct ?? p) #X whd in X:(?(??%)) whd in X:(?(??(?%)))
     335| #i normalize nodelta whd in match prog_var_names normalize nodelta elim (prog_vars … p)
     336  [ // | #hd #tl #H1 #H2 normalize in ⊢ (???(????%))   
Note: See TracChangeset for help on using the changeset viewer.