Changeset 1166 for src/LTL/LTLToLIN.ma


Ignore:
Timestamp:
Sep 2, 2011, 10:35:24 AM (8 years ago)
Author:
mulligan
Message:

moved joint ltl lin files into their own directory. more changes to ltl and lin passes to help type checker in ertl pass

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/LTL/LTLToLIN.ma

    r1164 r1166  
    99  λglobals: list ident.
    1010  λs: ltl_statement globals.
    11     match s with
     11  match s with
     12  [ ltl_st_lift_joint joint ⇒
     13    match joint with
    1214    [ joint_st_return ⇒ joint_st_return … globals
    1315    | joint_st_sequential instr _ ⇒ joint_st_sequential … globals instr it
    1416    | joint_st_goto l ⇒ joint_st_goto … globals l
    15     ].
     17    ]
     18  ].
    1619   
    1720definition require: label → BitVectorTrieSet 16 → BitVectorTrieSet 16 ≝
     
    7881      let generated'' ≝ translated_statement :: generated in
    7982      match statement with
    80       [ joint_st_sequential instr l2 ⇒
    81         match instr with
    82         [ joint_instr_cond acc_a_reg l1 ⇒
     83      [ ltl_st_lift_joint joint ⇒
     84        match joint with
     85        [ joint_st_sequential instr l2 ⇒
     86          match instr with
     87          [ joint_instr_cond acc_a_reg l1 ⇒
     88                let required' ≝
     89                  if marked l2 visited' then
     90                    require l2 required
     91                  else
     92                    required in
     93                let 〈required', generated''〉 ≝
     94                 foo l2 visited' required' globals generated'' g n' visit (*
     95                  if marked l2 visited' then
     96                    〈required', (Joint_St_Goto ? globals l2) :: generated''〉
     97                  else
     98                    visit globals g required' visited' generated'' l2 n'*) in
     99                let required'' ≝ require l1 required' in
     100                  if ¬(marked l1 visited') then
     101                    visit globals g required'' visited' generated'' l1 n'
     102                  else
     103                    〈required', generated''〉
     104            | _ ⇒
    83105              let required' ≝
    84106                if marked l2 visited' then
     
    86108                else
    87109                  required in
    88               let 〈required', generated''〉 ≝
    89                foo l2 visited' required' globals generated'' g n' visit (*
    90                 if marked l2 visited' then
    91                   〈required', (Joint_St_Goto ? globals l2) :: generated''〉
    92                 else
    93                   visit globals g required' visited' generated'' l2 n'*) in
    94               let required'' ≝ require l1 required' in
    95                 if ¬(marked l1 visited') then
    96                   visit globals g required'' visited' generated'' l1 n'
    97                 else
    98                   〈required', generated''〉
    99           | _ ⇒
    100             let required' ≝
    101110              if marked l2 visited' then
    102                 require l2 required
     111                〈required', joint_st_goto … globals l2 :: generated''〉
    103112              else
    104                 required in
    105             if marked l2 visited' then
    106               〈required', joint_st_goto … globals l2 :: generated''〉
    107             else
    108               visit globals g required' visited' generated'' l2 n'
    109           ]
    110         | joint_st_return ⇒ 〈required, generated''〉 (* dpm: correct? *)
    111     | joint_st_goto l ⇒
    112        let required' ≝
    113          if marked l visited' then
    114            require l required
    115          else
    116            required
    117        in
    118          if marked l visited' then
    119            〈required', joint_st_goto … globals l :: generated''〉
    120          else
    121            visit globals g required' visited' generated'' l n'
     113                visit globals g required' visited' generated'' l2 n'
     114            ]
     115          | joint_st_return ⇒ 〈required, generated''〉 (* dpm: correct? *)
     116      | joint_st_goto l ⇒
     117        let required' ≝
     118           if marked l visited' then
     119             require l required
     120           else
     121             required
     122         in
     123           if marked l visited' then
     124             〈required', joint_st_goto … globals l :: generated''〉
     125           else
     126             visit globals g required' visited' generated'' l n'
     127      ]
    122128    ]
    123129  ]
Note: See TracChangeset for help on using the changeset viewer.