Changeset 1110 for src/LTL/LTLToLIN.ma


Ignore:
Timestamp:
Aug 24, 2011, 6:45:01 PM (8 years ago)
Author:
mulligan
Message:

changes to get ltl to lin pass to work properly

File:
1 edited

Legend:

Unmodified
Added
Removed

  • src/LTL/LTLToLIN.ma

    r759 r1110  
    1010  λs: ltl_statement globals.
    1111    match s with
    12     [ joint_st_return ⇒ joint_st_return ? globals
    13     | joint_st_sequential instr _ ⇒ joint_st_sequential ? globals instr it
    14     | joint_st_goto lbl ⇒ joint_st_goto ? globals lbl
     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
    1518    ].
    1619   
    17 definition require: ident → BitVectorTrieSet 16 → BitVectorTrieSet 16 ≝
    18   λl: ident.
     20definition require: label → BitVectorTrieSet 16 → BitVectorTrieSet 16 ≝
     21  λl: label.
    1922  λg: BitVectorTrieSet 16.
    2023    set_insert ? (word_of_identifier ? l) g.
    2124   
    22 definition mark: ident → BitVectorTrieSet 16 → BitVectorTrieSet 16 ≝
    23   λl: ident.
     25definition mark: label → BitVectorTrieSet 16 → BitVectorTrieSet 16 ≝
     26  λl: label.
    2427  λg: BitVectorTrieSet 16.
    2528    set_insert ? (word_of_identifier ? l) g.
    2629   
    27 definition marked: ident → BitVectorTrieSet 16 → bool ≝
    28   λl: ident.
     30definition marked: label → BitVectorTrieSet 16 → bool ≝
     31  λl: label.
    2932  λg: BitVectorTrieSet 16.
    3033    set_member ? (word_of_identifier ? l) g.
    … …  
    3437definition graph_lookup ≝
    3538  λglobals: list ident.
    36   λl: ident.
     39  λl: label.
    3740  λgr: ltl_statement_graph globals.
    3841    lookup LabelTag ? gr (an_identifier LabelTag (word_of_identifier ? l)).
    3942   
    40 definition fetch: ∀globals: list ident. ident → ltl_statement_graph globals → option (ltl_statement globals) ≝
     43definition fetch: ∀globals: list ident. label → ltl_statement_graph globals → option (ltl_statement globals) ≝
    4144  λglobals: list ident.
    42   λl: ident.
     45  λl: label.
    4346  λg: ltl_statement_graph globals.
    4447    graph_lookup globals l g.
    … …  
    4750  λl2, visited, required, globals, generated, g, n.
    4851  λvisit:
    49   ∀globals: list Identifier.
    50   ∀g: LTLStatementGraph globals.
     52  ∀globals: list ident.
     53  ∀g: ltl_statement_graph globals.
    5154  ∀required: BitVectorTrieSet 16.
    5255  ∀visited: BitVectorTrieSet 16.
    53   ∀generated: list (PreLINStatement globals).
    54   ∀l: Identifier.
     56  ∀generated: list (pre_lin_statement globals).
     57  ∀l: label.
    5558  ∀n: nat.
    56     BitVectorTrieSet 16 × (list (PreLINStatement globals)).
     59    BitVectorTrieSet 16 × (list (pre_lin_statement globals)).
    5760  if marked l2 visited then
    58     〈require l2 required, (Joint_St_Goto ? globals l2) :: generated〉
     61    〈require l2 required, (lin_st_goto globals l2) :: generated〉
    5962  else
    6063   visit globals g required visited generated l2 n.
    6164
    62 let rec visit (globals: list ident) (g: ltl_statement_graph globals)
    63               (required: BitVectorTrieSet 16) (visited: BitVectorTrieSet 16)
    64               (generated: list (pre_lin_statement globals)) (l: ident) (n: nat) on n: BitVectorTrieSet 16 × (list (PreLINStatement globals)) ≝
     65let rec visit
     66  (globals: list ident) (g: ltl_statement_graph globals)
     67  (required: BitVectorTrieSet 16) (visited: BitVectorTrieSet 16)
     68  (generated: list (pre_lin_statement globals)) (l: label) (n: nat)
     69    on n: BitVectorTrieSet 16 × (list (pre_lin_statement globals)) ≝
    6570  match n with
    6671  [ O ⇒ 〈required, generated〉
    … …  
    7378      let generated'' ≝ translated_statement :: generated in
    7479      match statement with
    75       [ joint_st_sequential instr l2 ⇒
    76         match instr with
    77         [ joint_instr_cond_acc l1 ⇒
     80      [ ltl_st_lift l ⇒
     81        match l with
     82        [ joint_st_sequential instr l2 ⇒
     83          match instr with
     84          [ joint_instr_cond_acc l1 ⇒
     85              let required' ≝
     86                if marked l2 visited' then
     87                  require l2 required
     88                else
     89                  required in
     90              let 〈required', generated''〉 ≝
     91               foo l2 visited' required' globals generated'' g n' visit (*
     92                if marked l2 visited' then
     93                  〈required', (Joint_St_Goto ? globals l2) :: generated''〉
     94                else
     95                  visit globals g required' visited' generated'' l2 n'*) in
     96              let required'' ≝ require l1 required' in
     97                if ¬(marked l1 visited') then
     98                  visit globals g required'' visited' generated'' l1 n'
     99                else
     100                  〈required', generated''〉
     101          | _ ⇒
    78102            let required' ≝
    79103              if marked l2 visited' then
    … …  
    81105              else
    82106                required in
    83             let 〈required', generated''〉 ≝
    84              foo l2 visited' required' globals generated'' g n' visit (*
    85               if marked l2 visited' then
    86                 〈required', (Joint_St_Goto ? globals l2) :: generated''〉
    87               else
    88                 visit globals g required' visited' generated'' l2 n'*) in
    89             let required'' ≝ require l1 required' in
    90               if ¬(marked l1 visited') then
    91                 visit globals g required'' visited' generated'' l1 n'
    92               else
    93                 〈required', generated''〉
    94         | _ ⇒
    95           let required' ≝
    96107            if marked l2 visited' then
    97               require l2 required
     108              〈required', lin_st_goto globals l2 :: generated''〉
    98109            else
    99               required in
    100           if marked l2 visited' then
    101             〈required', Joint_St_Goto ? globals l2 :: generated''〉
    102           else
    103             visit globals g required' visited' generated'' l2 n'
    104         ]
    105       | joint_st_goto lbl ⇒
    106         let required' ≝
    107           if marked lbl visited' then
    108             require lbl required
    109           else
    110             required in
    111         if marked lbl visited' then
    112           〈required', (Joint_St_Goto ? globals lbl) :: generated''〉
    113         else
    114           visit globals g required' visited' generated'' lbl n'
    115       | joint_st_Return ⇒ 〈required, generated''〉 (* dpm: correct? *)
     110              visit globals g required' visited' generated'' l2 n'
     111          ]
     112        | joint_st_return ⇒ 〈required, generated''〉 (* dpm: correct? *)
    116113      ]
     114    | ltl_st_skip l ⇒
     115       let required' ≝
     116         if marked l visited' then
     117           require l required
     118         else
     119           required
     120       in
     121         if marked l visited' then
     122           〈required', lin_st_goto globals l :: generated''〉
     123         else
     124           visit globals g required' visited' generated'' l n'
    117125    ]
    118   ].
     126  ]
     127].
    119128
    120129(*
Note: See TracChangeset for help on using the changeset viewer.