Changeset 1245


Ignore:
Timestamp:
Sep 21, 2011, 10:22:13 PM (8 years ago)
Author:
sacerdot
Message:

RTLtoERTL and LINToASM: porting to new Joint data type in progress.
However, it seems better to go back to a Joint representation where
the "mapping" from label to internal functions is more concrete.
To be done.

Location:
src
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/LIN/LINToASM.ma

    r1179 r1245  
    2828definition statement_labels ≝
    2929  λg: list ident.
    30   λs: lin_statement g.
     30  λs: (option label) × (lin_statement g).
    3131  let 〈label, instr〉 ≝ s in
    3232  let generated ≝
     
    5151  λglobals: list ident.
    5252  λlabels: BitVectorTrieSet ?.
    53   λstatement: lin_statement globals.
     53  λstatement: (option label) × (lin_statement globals).
    5454    set_union ? labels (statement_labels globals statement).
    5555
     56(*
    5657(* dpm: A = Identifier *)
    5758definition function_labels: ∀A. ∀globals. ∀f. BitVectorTrieSet ? ≝
     
    6162  let 〈ignore, fun_def〉 ≝ f in
    6263  match fun_def return λ_. BitVectorTrieSet ? with
    63   [ lin_fu_internal stmts proof
     64  [ Internal stmts
    6465      foldl ? ? (function_labels_internal globals) (set_empty ?) stmts
    65   | lin_fu_external _ ⇒ set_empty ?
     66  | External _ ⇒ set_empty ?
    6667  ].
    6768 
     
    7778    foldl ? ? (program_labels_internal ? (map ? ? (fst ? ?) (lin_pr_vars program)))
    7879              (set_empty ?) (lin_pr_funcs program).
    79    
     80*) 
    8081definition data_of_int ≝ λbv. DATA bv.
    8182definition data16_of_int ≝ λbv. DATA16 (bitvector_of_nat 16 bv).
    8283definition accumulator_address ≝ DIRECT (bitvector_of_nat 8 224).
    83 
    84 axiom ImplementedInRuntime: False.
    8584
    8685definition translate_statements ≝
     
    8887  λglobals_old: list ident.
    8988  λprf: ∀i: ident. member i (eq_identifier ?) globals_old → member i (eq_identifier ?) (map ? ? (fst ? ?) globals).
    90   λstatement: pre_lin_statement globals_old.
     89  λstatement: lin_statement globals_old.
    9190  match statement with
    9291  [ joint_st_goto lbl ⇒ Jmp (word_of_identifier ? lbl)
    93   | joint_st_extension ext ⇒ Instruction (NOP ?) (* XXX: NOP or something else? *)
     92  | joint_st_extension ext ⇒
    9493  | joint_st_return ⇒ Instruction (RET ?)
    9594  | joint_st_sequential instr _ ⇒
     
    9796      [ joint_instr_comment comment ⇒ Comment comment
    9897      | joint_instr_cost_label lbl ⇒ Cost (Identifier_of_costlabel lbl)
    99       | joint_instr_pop ⇒ Instruction (POP ? accumulator_address)
    100       | joint_instr_push ⇒ Instruction (PUSH ? accumulator_address)
     98      | joint_instr_pop _ ⇒ Instruction (POP ? accumulator_address)
     99      | joint_instr_push _ ⇒ Instruction (PUSH ? accumulator_address)
    101100      | joint_instr_clear_carry ⇒ Instruction (CLR ? CARRY)
    102       | joint_instr_call_id f ⇒ Call (word_of_identifier ? f)
    103       | joint_instr_opaccs accs
     101      | joint_instr_call_id f _ ⇒ Call (word_of_identifier ? f)
     102      | joint_instr_opaccs accs _ _
    104103        match accs with
    105104        [ Mul ⇒ Instruction (MUL ? ACC_A ACC_B)
    106105        | DivuModu ⇒ Instruction (DIV ? ACC_A ACC_B)
    107106        ]
    108       | joint_instr_op1 op1
     107      | joint_instr_op1 op1 _
    109108        match op1 with
    110109        [ Cmpl ⇒ Instruction (CPL ? ACC_A)
    111110        | Inc ⇒ Instruction (INC ? ACC_A)
    112111        ]
    113       | joint_instr_op2 op2 reg ⇒
     112      | joint_instr_op2 op2 _ reg ⇒
    114113        match op2 with
    115114        [ Add ⇒
     
    205204          | _ ⇒ λother: False. ⊥
    206205          ] (subaddressing_modein … reg')
    207       | joint_instr_from_acc reg ⇒
    208         let reg' ≝ register_address reg in
    209           match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
    210                                                          direct;
    211                                                          registr ]] x) → ? with
    212           [ REGISTER r ⇒ λregister8: True.
    213             Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈REGISTER r, ACC_A〉))))))
    214           | ACC_A ⇒ λacc: True.
    215             Instruction (NOP ?)
    216           | DIRECT d ⇒ λdirect8: True.
    217             Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈DIRECT d, ACC_A〉)))))
    218           | _ ⇒ λother: False. ⊥
    219           ] (subaddressing_modein … reg')
    220       | joint_instr_to_acc reg ⇒
    221         let reg' ≝ register_address reg in
    222           match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
    223                                                          direct;
    224                                                          registr ]] x) → ? with
    225           [ REGISTER r ⇒ λregister9: True.
    226             Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉))))))
    227           | DIRECT d ⇒ λdirect9: True.
    228             Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉))))))
    229           | ACC_A ⇒ λacc_a: True.
    230             Instruction (NOP ?)
    231           | _ ⇒ λother: False. ⊥
    232           ] (subaddressing_modein … reg')
    233       | joint_instr_load ⇒ Instruction (MOVX ? (inl ? ? 〈ACC_A, EXT_INDIRECT_DPTR〉))
    234       | joint_instr_store ⇒ Instruction (MOVX ? (inr ? ? 〈EXT_INDIRECT_DPTR, ACC_A〉))
    235       | joint_instr_address addr proof ⇒
     206      | joint_instr_move regs ⇒
     207         match regs with
     208          [ from_acc reg ⇒
     209             let reg' ≝ register_address reg in
     210               match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
     211                                                              direct;
     212                                                              registr ]] x) → ? with
     213               [ REGISTER r ⇒ λregister8: True.
     214                 Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈REGISTER r, ACC_A〉))))))
     215               | ACC_A ⇒ λacc: True.
     216                 Instruction (NOP ?)
     217               | DIRECT d ⇒ λdirect8: True.
     218                 Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inr ? ? 〈DIRECT d, ACC_A〉)))))
     219               | _ ⇒ λother: False. ⊥
     220               ] (subaddressing_modein … reg')
     221          | to_acc reg ⇒
     222             let reg' ≝ register_address reg in
     223               match reg' return λx. bool_to_Prop (is_in … [[ acc_a;
     224                                                              direct;
     225                                                              registr ]] x) → ? with
     226               [ REGISTER r ⇒ λregister9: True.
     227                 Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, REGISTER r〉))))))
     228               | DIRECT d ⇒ λdirect9: True.
     229                 Instruction (MOV ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? (inl ? ? 〈ACC_A, DIRECT d〉))))))
     230               | ACC_A ⇒ λacc_a: True.
     231                 Instruction (NOP ?)
     232               | _ ⇒ λother: False. ⊥
     233               ] (subaddressing_modein … reg')]
     234      | joint_instr_load _ _ _ ⇒ Instruction (MOVX ? (inl ? ? 〈ACC_A, EXT_INDIRECT_DPTR〉))
     235      | joint_instr_store _ _ _ ⇒ Instruction (MOVX ? (inr ? ? 〈EXT_INDIRECT_DPTR, ACC_A〉))
     236      | joint_instr_address addr proof _ _ ⇒
    236237        let look ≝ association addr globals (prf ? proof) in
    237238          Instruction (MOV ? (inl ? ? (inl ? ? (inr ? ? (〈DPTR, (data16_of_int look)〉)))))
    238       | joint_instr_cond_acc lbl ⇒
     239      | joint_instr_cond _ lbl ⇒
    239240        (* dpm: this should be handled in translate_code! *)
    240241        Instruction (JNZ ? (word_of_identifier ? lbl))
     
    245246  try assumption
    246247  try @ I
    247   cases ImplementedInRuntime
    248248qed.
    249249
     
    252252  λglobals_old.
    253253  λprf.
    254   λstatement: lin_statement globals_old.
     254  λstatement: (option label) × (lin_statement globals_old).
    255255    〈\fst statement, translate_statements globals globals_old prf (\snd statement)〉.
    256256
     
    259259  λglobals_old: list ident.
    260260  λprf.
    261   λcode: list (lin_statement globals_old).
     261  λcode: list ((option label) × (lin_statement globals_old)).
    262262    map ? ? (build_translated_statement globals globals_old prf) code.
    263263   
  • src/RTL/RTLtoERTL.ma

    r1149 r1245  
    1 include "RTL/RTL.ma".
    21include "RTL/RTLTailcall.ma".
    32include "utilities/RegisterSet.ma".
    43include "common/Identifiers.ma".
    54include "ERTL/ERTL.ma".
    6 
    7 definition change_exit_label ≝
    8   λl: label.
    9   λp: ertl_internal_function.
    10   λprf: lookup ? ? (ertl_if_graph p) l ≠ None ?.
    11   let ertl_if_luniverse' ≝ ertl_if_luniverse p in
    12   let ertl_if_runiverse' ≝ ertl_if_runiverse p in
    13   let ertl_if_params' ≝ ertl_if_params p in
    14   let ertl_if_locals' ≝ ertl_if_locals p in
    15   let ertl_if_stacksize' ≝ ertl_if_stacksize p in
    16   let ertl_if_graph' ≝ ertl_if_graph p in
    17   let ertl_if_entry' ≝ ertl_if_entry p in
    18   let ertl_if_exit' ≝ l in
    19     mk_ertl_internal_function ertl_if_luniverse' ertl_if_runiverse'
    20                               ertl_if_params' ertl_if_locals' ertl_if_stacksize'
    21                               ertl_if_graph' ertl_if_entry' ertl_if_exit'.
    22   @prf
    23 qed.
    24 
    25 definition change_entry_label ≝
    26   λl: label.
    27   λp: ertl_internal_function.
    28   λprf: lookup ? ? (ertl_if_graph p) l ≠ None ?.
    29   let ertl_if_luniverse' ≝ ertl_if_luniverse p in
    30   let ertl_if_runiverse' ≝ ertl_if_runiverse p in
    31   let ertl_if_params' ≝ ertl_if_params p in
    32   let ertl_if_locals' ≝ ertl_if_locals p in
    33   let ertl_if_stacksize' ≝ ertl_if_stacksize p in
    34   let ertl_if_graph' ≝ ertl_if_graph p in
    35   let ertl_if_entry' ≝ l in
    36   let ertl_if_exit' ≝ ertl_if_exit p in
    37     mk_ertl_internal_function ertl_if_luniverse' ertl_if_runiverse'
    38                               ertl_if_params' ertl_if_locals' ertl_if_stacksize'
    39                               ertl_if_graph' ertl_if_entry' ertl_if_exit'.
    40   @prf
    41 qed.
    42                              
     5                     
    436definition add_graph ≝
    447  λl: label.
     
    7740  ]
    7841qed.
    79                             
     42                           
    8043definition fresh_label ≝
    8144  λdef.
     
    351314    in
    352315    let def ≝ add_graph tmp_lbl last_stmt def in
    353       change_exit_label tmp_lbl def ?
     316      set_joint_if_exit … tmp_lbl def ?
    354317  ] ?.
    355318  cases not_implemented (* dep types here, bug in matita too! *)
  • src/joint/Joint.ma

    r1236 r1245  
    6565}.
    6666
     67(* Currified form *)
     68definition set_joint_if_exit ≝
     69  λpars,globals.
     70  λexit: label.
     71  λp: joint_internal_function pars globals.
     72  λprf: joint_if_lookup … p exit ≠ None ?.
     73   mk_joint_internal_function pars globals
     74    (joint_if_luniverse … p) (joint_if_runiverse … p) (joint_if_result … p)
     75    (joint_if_params … p) (joint_if_locals … p) (joint_if_stacksize … p)
     76    (joint_if_lookup … p) (joint_if_entry … p) (dp … exit prf).
     77
     78
    6779definition set_luniverse ≝
    6880  λp:params.
Note: See TracChangeset for help on using the changeset viewer.