Last change
on this file since 856 was
757,
checked in by mulligan, 10 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.