Changeset 1282 for src/LTL


Ignore:
Timestamp:
Sep 28, 2011, 11:50:32 PM (8 years ago)
Author:
sacerdot
Message:

Cosmetic change: names of joint statements/instructions shortened and made
uppercase.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/LTL/LTLToLIN.ma

    r1250 r1282  
    88  λs: ltl_statement globals.
    99  match s with
    10   [ joint_st_return ⇒ joint_st_return ??
    11   | joint_st_sequential instr lbl ⇒ joint_st_sequential … instr it
    12   | joint_st_goto l ⇒ joint_st_goto lin_params_ globals l
     10  [ RETURN ⇒ RETURN ??
     11  | sequential instr lbl ⇒ sequential … instr it
     12  | GOTO l ⇒ GOTO lin_params_ globals l
    1313  ].
    1414
     
    2727  | S n' ⇒
    2828    if set_member … (word_of_identifier … l) visited then
    29      〈set_insert ? (word_of_identifier ? l) required, 〈None …, joint_st_goto … globals l〉 :: generated〉
     29     〈set_insert ? (word_of_identifier ? l) required, 〈None …, GOTO … globals l〉 :: generated〉
    3030    else
    3131     let visited' ≝ set_insert ? (word_of_identifier ? l) visited in
     
    3636       let generated' ≝ 〈Some … l, translated_statement〉 :: generated in
    3737       match statement with
    38        [ joint_st_sequential instr l2 ⇒
     38       [ sequential instr l2 ⇒
    3939         match instr with
    40          [ joint_instr_cond acc_a_reg l1 ⇒
     40         [ COND acc_a_reg l1 ⇒
    4141            let 〈required', generated''〉 ≝
    4242             visit globals g required visited' generated' l2 n' in
     
    4747               visit globals g required'' visited' generated'' l1 n'
    4848         | _ ⇒ visit globals g required visited' generated' l2 n']
    49      | joint_st_return ⇒ 〈required, generated'〉
    50      | joint_st_goto l2 ⇒ visit globals g required visited' generated' l2 n']]].
     49     | RETURN ⇒ 〈required, generated'〉
     50     | GOTO l2 ⇒ visit globals g required visited' generated' l2 n']]].
    5151[1,2: @daemon (*CSC: impossible cases, use more dependent types *) ]
    5252qed.
Note: See TracChangeset for help on using the changeset viewer.