Last change
on this file since 1086 was
1082,
checked in by mulligan, 10 years ago

work from today on ertl > ltl pass

File size:
1007 bytes

Line  

1  include "common/Graphs.ma". 

2  include "utilities/IdentifierTools.ma". 

3  include "LIN/LIN.ma". 

4  

5  definition ltl_statement ≝ joint_statement ident. 

6  

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

8  

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

10  { 

11  ltl_if_luniverse: universe LabelTag; 

12  ltl_if_runiverse: universe RegisterTag; 

13  ltl_if_stacksize: nat; 

14  ltl_if_graph: ltl_statement_graph globals; 

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

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

17  }. 

18  

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

20   ltl_fu_internal_function: ltl_internal_function globals → ltl_function_definition globals 

21   ltl_fu_external_function: external_function → ltl_function_definition globals. 

22  

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

24  { 

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

26  ltl_pr_main: option ident 

27  }. 

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