Changeset 1164 for src/LTL


Ignore:
Timestamp:
Sep 1, 2011, 4:53:01 PM (8 years ago)
Author:
mulligan
Message:

ltl to lin working again, more changes to joint syntax

Location:
src/LTL
Files:
2 edited

Legend:

Unmodified
Added
Removed
  • src/LTL/LTL.ma

    r1163 r1164  
    44
    55definition ltl_statement ≝
    6   λglobals.
    7     joint_statement label globals Register
     6    joint_statement label Register Register
    87                    Register Register Register
    9                     Register (Register × Register).
     8                    registers_move.
    109 
    1110definition ltl_statement_graph ≝ λglobals. graph (ltl_statement globals).
  • src/LTL/LTLToLIN.ma

    r1149 r1164  
    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 l ⇒ joint_st_goto ? globals l
     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
    1515    ].
    1616   
     
    5656    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.
     
    8080      [ joint_st_sequential instr l2 ⇒
    8181        match instr with
    82         [ joint_instr_cond_acc l1 ⇒
     82        [ joint_instr_cond acc_a_reg l1 ⇒
    8383              let required' ≝
    8484                if marked l2 visited' then
     
    104104                required in
    105105            if marked l2 visited' then
    106               〈required', joint_st_goto ? globals l2 :: generated''〉
     106              〈required', joint_st_goto globals l2 :: generated''〉
    107107            else
    108108              visit globals g required' visited' generated'' l2 n'
     
    117117       in
    118118         if marked l visited' then
    119            〈required', joint_st_goto ? globals l :: generated''〉
     119           〈required', joint_st_goto globals l :: generated''〉
    120120         else
    121121           visit globals g required' visited' generated'' l n'
Note: See TracChangeset for help on using the changeset viewer.