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

reunified ltl and lin instruction type, removing lifting in ltl and lin and simplifying the ertl > ertl passes

File size:
1007 bytes

Rev  Line  

[713]  1  include "common/Graphs.ma". 

 2  include "utilities/IdentifierTools.ma". 

[722]  3  include "LIN/LIN.ma". 

 4  

[1132]  5  definition ltl_statement ≝ joint_statement label. 

[713]  6  

[757]  7  definition ltl_statement_graph ≝ λglobals. graph (ltl_statement globals). 

[713]  8  

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

[713]  10  { 

[757]  11  ltl_if_luniverse: universe LabelTag; 

 12  ltl_if_runiverse: universe RegisterTag; 

[1082]  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 ? 

[713]  17  }. 

 18  

[757]  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. 

[713]  22  

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

[713]  24  { 

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

 26  ltl_pr_main: option ident 

[713]  27  }. 

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