source: src/LTL/LTL.ma @ 1132

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
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.