Changeset 2694


Ignore:
Timestamp:
Feb 22, 2013, 11:53:32 AM (6 years ago)
Author:
tranquil
Message:

completed ERTLptrToLTL

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTLptr/ERTLptrToLTL.ma

    r2693 r2694  
    295295     move ? false addr1 RegisterDPL @
    296296     move ? false addr2 RegisterDPH).
     297
     298definition translate_low_address :
     299  ∀globals.bool → decision → label →
     300  list (joint_seq LTL globals) ≝
     301  λglobals,carry_lives_after,dst,lbl.
     302  match dst return λ_.list (joint_seq LTL globals) with
     303  [ decision_colour r ⇒ [LOW_ADDRESS r lbl]
     304  | _ ⇒
     305    LOW_ADDRESS RegisterA lbl :: move ? carry_lives_after dst RegisterA
     306  ].
     307
     308definition translate_high_address :
     309  ∀globals.bool → decision → label →
     310  list (joint_seq LTL globals) ≝
     311  λglobals,carry_lives_after,dst,lbl.
     312  match dst return λ_.list (joint_seq LTL globals) with
     313  [ decision_colour r ⇒ [HIGH_ADDRESS r lbl]
     314  | _ ⇒
     315    HIGH_ADDRESS RegisterA lbl :: move ? carry_lives_after dst RegisterA
     316  ].
    297317
    298318definition translate_step:
     
    369389          ]
    370390        | LOW_ADDRESS r1 l ⇒
    371            translate_low_address ? carry_lives_after (lookup_arg r1) l
     391           translate_low_address ? carry_lives_after (lookup r1) l
    372392        | HIGH_ADDRESS r1 l ⇒
    373            translate_high_address ? carry_lives_after (lookup_arg r1) l       
     393           translate_high_address ? carry_lives_after (lookup r1) l       
    374394        ]
    375395    ]
     
    421441qed.
    422442
    423 definition ertl_to_ltl: ertl_program → ltl_program ≝
     443definition ertl_to_ltl: ertlptr_program → ltl_program ≝
    424444  b_graph_transform_program … translate_data.
Note: See TracChangeset for help on using the changeset viewer.