Last change
on this file since 1110 was
1110,
checked in by mulligan, 9 years ago

changes to get ltl to lin pass to work properly

File size:
1.1 KB

Line  

1  include "common/Graphs.ma". 

2  include "utilities/IdentifierTools.ma". 

3  include "LIN/LIN.ma". 

4  

5  inductive ltl_statement (globals: list ident): Type[0] ≝ 

6   ltl_st_lift: joint_statement label globals → ltl_statement globals 

7   ltl_st_skip: label → ltl_statement globals. 

8  

9  definition ltl_statement_graph ≝ λglobals. graph (ltl_statement globals). 

10  

11  record ltl_internal_function (globals: list ident): Type[0] ≝ 

12  { 

13  ltl_if_luniverse: universe LabelTag; 

14  ltl_if_runiverse: universe RegisterTag; 

15  ltl_if_stacksize: nat; 

16  ltl_if_graph: ltl_statement_graph globals; 

17  ltl_if_entry: Σl: label. lookup ? ? ltl_if_graph l ≠ None ?; 

18  ltl_if_exit: Σl: label. lookup ? ? ltl_if_graph l ≠ None ? 

19  }. 

20  

21  inductive ltl_function_definition (globals: list ident): Type[0] ≝ 

22   ltl_fu_internal_function: ltl_internal_function globals → ltl_function_definition globals 

23   ltl_fu_external_function: external_function → ltl_function_definition globals. 

24  

25  record ltl_program (globals: list (ident × nat)): Type[0] ≝ 

26  { 

27  ltl_pr_funcs: list (ident × (ltl_function_definition (map ? ? \fst globals))); 

28  ltl_pr_main: option ident 

29  }. 

Note: See
TracBrowser
for help on using the repository browser.