Changeset 1224 for src/LTL


Ignore:
Timestamp:
Sep 16, 2011, 6:39:05 PM (8 years ago)
Author:
sacerdot
Message:

Type of programs in common/AST made more dependent.
In particular, the type of internal functions is now dependent on the
list of global variables. This is already used in the back-end to rule
out from the syntax programs that have free variables.

Note: only the test Clight/test/search.c.ma has been ported to the new type.
The porting requires two very minor changes.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/LTL/LTLToLIN.ma

    r1180 r1224  
    22include "LIN/LIN.ma".
    33include "utilities/BitVectorTrieSet.ma".
    4 include "common/Graphs.ma".
    54
    65axiom LTLTag: String.
     
    3130    set_member ? (word_of_identifier ? l) g.
    3231   
    33 (* alias id "lookupn" = "cic:/matita/cerco/common/Identifiers/lookup.def(3)". *)
    34    
    3532definition graph_lookup ≝
    3633  λglobals: list ident.
    3734  λl: label.
    38   λgr: ltl_statement_graph globals.
     35  λgr: graph (ltl_statement globals).
    3936    lookup LabelTag ? gr (an_identifier LabelTag (word_of_identifier ? l)).
    4037   
    41 definition fetch: ∀globals: list ident. label → ltl_statement_graph globals → option (ltl_statement globals) ≝
    42   λglobals: list ident.
    43   λl: label.
    44   λg: ltl_statement_graph globals.
    45     graph_lookup globals l g.
     38definition fetch: ∀globals: list ident. label → graph (ltl_statement globals) → option (ltl_statement globals) ≝
     39  λglobals,l,g.graph_lookup globals l g.
    4640
    4741definition foo ≝
     
    4943  λvisit:
    5044  ∀globals: list ident.
    51   ∀g: ltl_statement_graph globals.
     45  ∀g: graph (ltl_statement globals).
    5246  ∀required: BitVectorTrieSet 16.
    5347  ∀visited: BitVectorTrieSet 16.
     
    6559*)
    6660let rec visit
    67   (globals: list ident) (g: ltl_statement_graph globals)
     61  (globals: list ident) (g: graph (ltl_statement globals))
    6862  (required: BitVectorTrieSet 16) (visited: BitVectorTrieSet 16)
    6963  (generated: list (pre_lin_statement globals)) (l: label) (n: nat)
Note: See TracChangeset for help on using the changeset viewer.