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

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

File size:
921 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: label; 

16  ltl_if_Exit: label 

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.