Ignore:
Timestamp:
Sep 7, 2011, 12:10:27 PM (9 years ago)
Author:
campbell
Message:

Merge trunk to 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

    r1153 r1197  
    99  λglobals: list ident.
    1010  λs: ltl_statement globals.
    11     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 l ⇒ joint_st_goto ? globals l
    15     ].
     11  match s with
     12  [ joint_st_return ⇒ joint_st_return lin_params globals
     13  | joint_st_sequential instr lbl ⇒ joint_st_sequential lin_params globals instr lbl
     14  | joint_st_goto l ⇒ joint_st_goto lin_params globals l
     15  | joint_st_extension ext ⇒ joint_st_extension lin_params globals ext
     16  ].
    1617   
    1718definition require: label → BitVectorTrieSet 16 → BitVectorTrieSet 16 ≝
     
    5657    BitVectorTrieSet 16 × (list (pre_lin_statement globals)).
    5758  if marked l2 visited then
    58     〈require l2 required, (joint_st_goto ? globals l2) :: generated〉
     59    〈require l2 required, (joint_st_goto globals l2) :: generated〉
    5960  else
    6061   visit globals g required visited generated l2 n.
     
    8081      [ joint_st_sequential instr l2 ⇒
    8182        match instr with
    82         [ joint_instr_cond_acc l1 ⇒
     83        [ joint_instr_cond acc_a_reg l1 ⇒
    8384              let required' ≝
    8485                if marked l2 visited' then
     
    104105                required in
    105106            if marked l2 visited' then
    106               〈required', joint_st_goto ? globals l2 :: generated''〉
     107              〈required', joint_st_goto globals l2 :: generated''〉
    107108            else
    108109              visit globals g required' visited' generated'' l2 n'
    109110          ]
    110         | joint_st_return ⇒ 〈required, generated''〉 (* dpm: correct? *)
     111    | joint_st_return ⇒ 〈required, generated''〉 (* dpm: correct? *)
    111112    | 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      let required' ≝
     114        if marked l visited' then
     115         require l required
     116        else
     117         required
     118      in
     119        if marked l visited' then
     120          〈required', joint_st_goto … globals l :: generated''〉
     121        else
     122          visit globals g required' visited' generated'' l n'
     123    | joint_st_extension ext ⇒ 〈required, generated〉
    122124    ]
    123125  ]
Note: See TracChangeset for help on using the changeset viewer.