Ignore:
Timestamp:
Aug 30, 2011, 6:55:12 PM (9 years ago)
Author:
campbell
Message:

Merge trunk into branch.

Location:
Deliverables/D3.3/id-lookup-branch
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • Deliverables/D3.3/id-lookup-branch

  • Deliverables/D3.3/id-lookup-branch/LTL/LTLToLIN.ma

    r759 r1153  
    1212    [ joint_st_return ⇒ joint_st_return ? globals
    1313    | joint_st_sequential instr _ ⇒ joint_st_sequential ? globals instr it
    14     | joint_st_goto lbl ⇒ joint_st_goto ? globals lbl
     14    | joint_st_goto l ⇒ joint_st_goto ? globals l
    1515    ].
    1616   
    17 definition require: ident → BitVectorTrieSet 16 → BitVectorTrieSet 16 ≝
    18   λl: ident.
     17definition require: label → BitVectorTrieSet 16 → BitVectorTrieSet 16 ≝
     18  λl: label.
    1919  λg: BitVectorTrieSet 16.
    2020    set_insert ? (word_of_identifier ? l) g.
    2121   
    22 definition mark: ident → BitVectorTrieSet 16 → BitVectorTrieSet 16 ≝
    23   λl: ident.
     22definition mark: label → BitVectorTrieSet 16 → BitVectorTrieSet 16 ≝
     23  λl: label.
    2424  λg: BitVectorTrieSet 16.
    2525    set_insert ? (word_of_identifier ? l) g.
    2626   
    27 definition marked: ident → BitVectorTrieSet 16 → bool ≝
    28   λl: ident.
     27definition marked: label → BitVectorTrieSet 16 → bool ≝
     28  λl: label.
    2929  λg: BitVectorTrieSet 16.
    3030    set_member ? (word_of_identifier ? l) g.
     
    3434definition graph_lookup ≝
    3535  λglobals: list ident.
    36   λl: ident.
     36  λl: label.
    3737  λgr: ltl_statement_graph globals.
    3838    lookup LabelTag ? gr (an_identifier LabelTag (word_of_identifier ? l)).
    3939   
    40 definition fetch: ∀globals: list ident. ident → ltl_statement_graph globals → option (ltl_statement globals) ≝
     40definition fetch: ∀globals: list ident. label → ltl_statement_graph globals → option (ltl_statement globals) ≝
    4141  λglobals: list ident.
    42   λl: ident.
     42  λl: label.
    4343  λg: ltl_statement_graph globals.
    4444    graph_lookup globals l g.
     
    4747  λl2, visited, required, globals, generated, g, n.
    4848  λvisit:
    49   ∀globals: list Identifier.
    50   ∀g: LTLStatementGraph globals.
     49  ∀globals: list ident.
     50  ∀g: ltl_statement_graph globals.
    5151  ∀required: BitVectorTrieSet 16.
    5252  ∀visited: BitVectorTrieSet 16.
    53   ∀generated: list (PreLINStatement globals).
    54   ∀l: Identifier.
     53  ∀generated: list (pre_lin_statement globals).
     54  ∀l: label.
    5555  ∀n: nat.
    56     BitVectorTrieSet 16 × (list (PreLINStatement globals)).
     56    BitVectorTrieSet 16 × (list (pre_lin_statement globals)).
    5757  if marked l2 visited then
    58     〈require l2 required, (Joint_St_Goto ? globals l2) :: generated〉
     58    〈require l2 required, (joint_st_goto ? globals l2) :: generated〉
    5959  else
    6060   visit globals g required visited generated l2 n.
    6161
    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)) ≝
     62(* XXX: look at this.  way too complicated to understand whether it is correct,
     63   in my opinion.
     64*)
     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〉
     
    7681        match instr with
    7782        [ joint_instr_cond_acc l1 ⇒
     83              let required' ≝
     84                if marked l2 visited' then
     85                  require l2 required
     86                else
     87                  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          | _ ⇒
    78100            let required' ≝
    79101              if marked l2 visited' then
     
    81103              else
    82104                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' ≝
    96105            if marked l2 visited' then
    97               require l2 required
     106              〈required', joint_st_goto ? globals l2 :: generated''〉
    98107            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? *)
    116       ]
     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'
    117122    ]
    118   ].
     123  ]
     124].
    119125
    120126(*
Note: See TracChangeset for help on using the changeset viewer.