Changeset 759 for src/LTL


Ignore:
Timestamp:
Apr 18, 2011, 5:32:46 PM (9 years ago)
Author:
mulligan
Message:

More work on the RTL to ERTL pass.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/LTL/LTLToLIN.ma

    r757 r759  
    1818  λl: ident.
    1919  λg: BitVectorTrieSet 16.
    20     set_insert ? l g.
     20    set_insert ? (word_of_identifier ? l) g.
    2121   
    2222definition mark: ident → BitVectorTrieSet 16 → BitVectorTrieSet 16 ≝
    2323  λl: ident.
    2424  λg: BitVectorTrieSet 16.
    25     set_insert ? l g.
     25    set_insert ? (word_of_identifier ? l) g.
    2626   
    2727definition marked: ident → BitVectorTrieSet 16 → bool ≝
    2828  λl: ident.
    2929  λg: BitVectorTrieSet 16.
    30     set_member ? l g.
     30    set_member ? (word_of_identifier ? l) g.
     31   
     32(* alias id "lookupn" = "cic:/matita/cerco/common/Identifiers/lookup.def(3)". *)
    3133   
    3234definition graph_lookup ≝
    33   λglobals.
     35  λglobals: list ident.
     36  λl: ident.
     37  λgr: ltl_statement_graph globals.
     38    lookup LabelTag ? gr (an_identifier LabelTag (word_of_identifier ? l)).
     39   
     40definition fetch: ∀globals: list ident. ident → ltl_statement_graph globals → option (ltl_statement globals) ≝
     41  λglobals: list ident.
    3442  λl: ident.
    3543  λg: ltl_statement_graph globals.
    36     lookup LabelTag (LTLStatement globals) g (an_identifier LabelTag l).
    37    
    38 definition fetch: ∀globals: list Identifier. Identifier → LTLStatementGraph globals → option (LTLStatement globals) ≝
    39   λglobals: list Identifier.
    40   λl: Identifier.
    41   λg: LTLStatementGraph globals.
    4244    graph_lookup globals l g.
    4345
Note: See TracChangeset for help on using the changeset viewer.