source: src/LTL/LTL.ma @ 1132

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

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

File size: 1007 bytes
RevLine 
[713]1include "common/Graphs.ma".
2include "utilities/IdentifierTools.ma".
[722]3include "LIN/LIN.ma".
4
[1132]5definition ltl_statement ≝ joint_statement label.
[713]6 
[757]7definition ltl_statement_graph ≝ λglobals. graph (ltl_statement globals).
[713]8 
[757]9record 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]19inductive 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]23record 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.