Changeset 1166


Ignore:
Timestamp:
Sep 2, 2011, 10:35:24 AM (10 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

Location:
src
Files:
1 added
4 edited
1 moved

Legend:

Unmodified
Added
Removed

  • src/ERTL/ERTLToLTL.ma

    r1165 r1166  
    6060    let off ≝ adjust_off globals int_fun off in
    6161    let luniv ≝ ertl_if_luniverse globals int_fun in
    62     let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential globals (joint_instr_move … globals (from_acc r)) l) in
     62    let 〈l, graph, luniv〉 ≝ generate globals luniv graph (joint_st_sequential ??????? globals (joint_instr_move … globals (from_acc r)) l) in
    6363    ?.
    6464   

  • src/LIN/LIN.ma

    r1164 r1166  
    11include "LIN/JointLTLLIN.ma".
    22 
    3 definition pre_lin_statement ≝
    4   joint_statement unit Register Register
    5                   Register Register Register
    6                   registers_move.
     3inductive pre_lin_statement (globals: list ident): Type[0] ≝
     4  | lin_st_lift_joint: joint_statement unit Register Register Register Register Register registers_move globals → pre_lin_statement globals.
    75
    86definition lin_statement ≝

  • src/LTL/LTL.ma

    r1164 r1166  
    33include "LIN/JointLTLLIN.ma".
    44
    5 definition ltl_statement ≝
    6     joint_statement label Register Register
    7                     Register Register Register
    8                     registers_move.
     5inductive ltl_statement (globals: list ident): Type[0] ≝
     6  ltl_st_lift_joint: joint_statement label Register Register Register Register Register registers_move globals → ltl_statement globals.
    97 
    108definition ltl_statement_graph ≝ λglobals. graph (ltl_statement globals).

  • 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.