Changeset 1149 for src/LTL


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

File:
1 edited

Legend:

Unmodified
Added
Removed
  • 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'
Note: See TracChangeset for help on using the changeset viewer.