Changeset 757 for src/LTL/LTLToLIN.ma


Ignore:
Timestamp:
Apr 18, 2011, 12:30:53 PM (9 years ago)
Author:
mulligan
Message:

Lots more fixing to get both front and backends using same conventions and types.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/LTL/LTLToLIN.ma

    r753 r757  
    66axiom LTLTag: String.
    77
    8 definition translate_statement: ∀globals. LTLStatement globals → PreLINStatement globals ≝
    9   λglobals: list Identifier.
    10   λs: LTLStatement globals.
     8definition translate_statement: ∀globals. ltl_statement globals → pre_lin_statement globals ≝
     9  λglobals: list ident.
     10  λ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 lbl ⇒ Joint_St_Goto ? globals lbl
     12    [ joint_st_return ⇒ joint_st_return ? globals
     13    | joint_st_sequential instr _ ⇒ joint_st_sequential ? globals instr it
     14    | joint_st_goto lbl ⇒ joint_st_goto ? globals lbl
    1515    ].
    1616   
    17 definition require: Identifier → BitVectorTrieSet 16 → BitVectorTrieSet 16 ≝
    18   λl: Identifier.
     17definition require: ident → BitVectorTrieSet 16 → BitVectorTrieSet 16 ≝
     18  λl: ident.
    1919  λg: BitVectorTrieSet 16.
    2020    set_insert ? l g.
    2121   
    22 definition mark: Identifier → BitVectorTrieSet 16 → BitVectorTrieSet 16 ≝
    23   λl: Identifier.
     22definition mark: ident → BitVectorTrieSet 16 → BitVectorTrieSet 16 ≝
     23  λl: ident.
    2424  λg: BitVectorTrieSet 16.
    2525    set_insert ? l g.
    2626   
    27 definition marked: Identifier → BitVectorTrieSet 16 → bool ≝
    28   λl: Identifier.
     27definition marked: ident → BitVectorTrieSet 16 → bool ≝
     28  λl: ident.
    2929  λg: BitVectorTrieSet 16.
    3030    set_member ? l g.
     
    3232definition graph_lookup ≝
    3333  λglobals.
    34   λl: Identifier.
    35   λg: LTLStatementGraph globals.
     34  λl: ident.
     35  λg: ltl_statement_graph globals.
    3636    lookup LabelTag (LTLStatement globals) g (an_identifier LabelTag l).
    3737   
     
    5858   visit globals g required visited generated l2 n.
    5959
    60 let rec visit (globals: list Identifier) (g: LTLStatementGraph globals)
     60let rec visit (globals: list ident) (g: ltl_statement_graph globals)
    6161              (required: BitVectorTrieSet 16) (visited: BitVectorTrieSet 16)
    62               (generated: list (PreLINStatement globals)) (l: Identifier) (n: nat) on n: BitVectorTrieSet 16 × (list (PreLINStatement globals)) ≝
     62              (generated: list (pre_lin_statement globals)) (l: ident) (n: nat) on n: BitVectorTrieSet 16 × (list (PreLINStatement globals)) ≝
    6363  match n with
    6464  [ O ⇒ 〈required, generated〉
     
    7171      let generated'' ≝ translated_statement :: generated in
    7272      match statement with
    73       [ Joint_St_Sequential instr l2 ⇒
     73      [ joint_st_sequential instr l2 ⇒
    7474        match instr with
    75         [ Joint_Instr_CondAcc l1 ⇒
     75        [ joint_instr_cond_acc l1 ⇒
    7676            let required' ≝
    7777              if marked l2 visited' then
     
    101101            visit globals g required' visited' generated'' l2 n'
    102102        ]
    103       | Joint_St_Goto lbl ⇒
     103      | joint_st_goto lbl ⇒
    104104        let required' ≝
    105105          if marked lbl visited' then
     
    111111        else
    112112          visit globals g required' visited' generated'' lbl n'
    113       | Joint_St_Return ⇒ 〈required, generated''〉 (* dpm: correct? *)
     113      | joint_st_Return ⇒ 〈required, generated''〉 (* dpm: correct? *)
    114114      ]
    115115    ]
Note: See TracChangeset for help on using the changeset viewer.