Changeset 1149


Ignore:
Timestamp:
Aug 30, 2011, 4:22:54 PM (8 years ago)
Author:
mulligan
Message:

changes to get everything type checking again after changing names of registers in i8051

Location:
src
Files:
4 edited

Legend:

Unmodified
Added
Removed
  • src/LIN/LINToASM.ma

    r1112 r1149  
    3232  let generated ≝
    3333    match instr with
    34     [ lin_st_lift l ⇒
    35       match l with
    36       [ joint_st_sequential instr' _ ⇒
    37         match instr' with
    38         [ joint_instr_cost_label lbl ⇒ set_insert ? (word_of_identifier ? lbl) (set_empty ?)
    39         | joint_instr_cond_acc lbl ⇒ set_insert ? (word_of_identifier ? lbl) (set_empty ?)
    40         | _ ⇒ set_empty ?
    41         ]
    42       | joint_st_return ⇒ set_empty ?
     34    [ joint_st_sequential instr' _ ⇒
     35      match instr' with
     36      [ joint_instr_cost_label lbl ⇒ set_insert ? (word_of_identifier ? lbl) (set_empty ?)
     37      | joint_instr_cond_acc lbl ⇒ set_insert ? (word_of_identifier ? lbl) (set_empty ?)
     38      | _ ⇒ set_empty ?
    4339      ]
    44     | lin_st_goto lbl ⇒ set_insert ? (word_of_identifier ? lbl) (set_empty ?)
     40    | joint_st_return ⇒ set_empty ?
     41    | joint_st_goto lbl ⇒ set_insert ? (word_of_identifier ? lbl) (set_empty ?)
    4542    ]
    4643  in
     
    9289  λstatement: pre_lin_statement globals_old.
    9390  match statement with
    94   [ lin_st_goto lbl ⇒ Jmp (word_of_identifier ? lbl)
    95   | lin_st_lift l ⇒
    96     match l with
    97     [ joint_st_return ⇒ Instruction (RET ?)
    98     | joint_st_sequential instr _ ⇒
     91  [ joint_st_goto lbl ⇒ Jmp (word_of_identifier ? lbl)
     92  | joint_st_return ⇒ Instruction (RET ?)
     93  | joint_st_sequential instr _ ⇒
    9994      match instr with
    10095      [ joint_instr_comment comment ⇒ Comment comment
     
    245240        Instruction (SETB ? CARRY)
    246241      ]
    247     ]
    248   ].
     242    ].
    249243  try assumption
    250244  try @ I
  • src/LTL/LTLToLIN.ma

    r1111 r1149  
    1010  λs: ltl_statement globals.
    1111    match s with
    12     [ ltl_st_lift l ⇒
    13       match l with
    14       [ joint_st_return ⇒ lin_st_lift globals (joint_st_return ? globals)
    15       | joint_st_sequential instr _ ⇒ lin_st_lift globals (joint_st_sequential ? globals instr it)
    16       ]
    17     | ltl_st_skip l ⇒ lin_st_goto globals l
     12    [ joint_st_return ⇒ joint_st_return ? globals
     13    | joint_st_sequential instr _ ⇒ joint_st_sequential ? globals instr it
     14    | joint_st_goto l ⇒ joint_st_goto ? globals l
    1815    ].
    1916   
     
    5956    BitVectorTrieSet 16 × (list (pre_lin_statement globals)).
    6057  if marked l2 visited then
    61     〈require l2 required, (lin_st_goto globals l2) :: generated〉
     58    〈require l2 required, (joint_st_goto ? globals l2) :: generated〉
    6259  else
    6360   visit globals g required visited generated l2 n.
     
    8178      let generated'' ≝ translated_statement :: generated in
    8279      match statement with
    83       [ ltl_st_lift l ⇒
    84         match l with
    85         [ joint_st_sequential instr l2 ⇒
    86           match instr with
    87           [ joint_instr_cond_acc l1 ⇒
     80      [ joint_st_sequential instr l2 ⇒
     81        match instr with
     82        [ joint_instr_cond_acc l1 ⇒
    8883              let required' ≝
    8984                if marked l2 visited' then
     
    109104                required in
    110105            if marked l2 visited' then
    111               〈required', lin_st_goto globals l2 :: generated''〉
     106              〈required', joint_st_goto ? globals l2 :: generated''〉
    112107            else
    113108              visit globals g required' visited' generated'' l2 n'
    114109          ]
    115110        | joint_st_return ⇒ 〈required, generated''〉 (* dpm: correct? *)
    116       ]
    117     | ltl_st_skip l ⇒
     111    | joint_st_goto l ⇒
    118112       let required' ≝
    119113         if marked l visited' then
     
    123117       in
    124118         if marked l visited' then
    125            〈required', lin_st_goto globals l :: generated''〉
     119           〈required', joint_st_goto ? globals l :: generated''〉
    126120         else
    127121           visit globals g required' visited' generated'' l n'
  • src/RTL/RTLtoERTL.ma

    r1138 r1149  
    222222  [ nil ⇒ [get_params_hdw_internal]
    223223  | _ ⇒
    224     let l ≝ zip_pottier ? ? params parameters in
     224    let l ≝ zip_pottier ? ? params RegisterParams in
    225225      save_hdws l
    226226  ].
     
    258258definition get_params ≝
    259259  λparams.
    260   let n ≝ min (length ? params) (length ? parameters) in
     260  let n ≝ min (length ? params) (length ? RegisterParams) in
    261261  let 〈hdw_params, stack_params〉 ≝ list_split ? n params in
    262262  let hdw_params ≝ get_params_hdw hdw_params in
     
    394394  [ nil ⇒ [ λstart_lbl. adds_graph [ertl_st_skip start_lbl] start_lbl]
    395395  | _ ⇒
    396     let l ≝ zip_pottier ? ? params parameters in
     396    let l ≝ zip_pottier ? ? params RegisterParams in
    397397      restore_hdws l
    398398  ].
     
    434434definition set_params ≝
    435435  λparams.
    436   let n ≝ min (|params|) (|parameters|) in
     436  let n ≝ min (|params|) (|RegisterParams|) in
    437437  let hdw_stack_params ≝ split ? params n ? in
    438438  let hdw_params ≝ \fst hdw_stack_params in
     
    530530  λdef.
    531531  let nb_params ≝ |rtl_if_params def| in
    532   let added_stacksize ≝ max 0 (nb_params - |parameters|) in
     532  let added_stacksize ≝ max 0 (nb_params - |RegisterParams|) in
    533533  let new_locals ≝ nub_by ? (eq_identifier ?) ((rtl_if_locals def) @ (rtl_if_params def)) in
    534534  let entry' ≝ rtl_if_entry def in
  • src/RTLabs/RTLAbstoRTL.ma

    r1138 r1149  
    12281228  let params ≝ map_list_local_env lenv (map ? ? \fst (f_params def)) in
    12291229  let locals ≝ map_list_local_env lenv (map ? ? \fst (f_locals def)) in
    1230   let result ≝f
     1230  let result ≝
    12311231    match (f_result def) with
    12321232    [ None ⇒ [ ]
Note: See TracChangeset for help on using the changeset viewer.