source: src/LTL/LTL.ma @ 1166

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

moved joint ltl lin files into their own directory. more changes to ltl and lin passes to help type checker in ertl pass

File size: 1.1 KB
Line 
1include "common/Graphs.ma".
2include "utilities/IdentifierTools.ma".
3include "LIN/JointLTLLIN.ma".
4
5inductive ltl_statement (globals: list ident): Type[0] ≝
6  ltl_st_lift_joint: joint_statement label Register Register Register Register Register registers_move globals → ltl_statement globals.
7 
8definition ltl_statement_graph ≝ λglobals. graph (ltl_statement globals).
9 
10record ltl_internal_function (globals: list ident): Type[0] ≝
11{
12  ltl_if_luniverse: universe LabelTag;
13  ltl_if_runiverse: universe RegisterTag;
14  ltl_if_stacksize: nat;
15  ltl_if_graph: ltl_statement_graph globals;
16  ltl_if_entry: Σl: label. lookup ? ? ltl_if_graph l ≠ None ?;
17  ltl_if_exit: Σl: label. lookup ? ? ltl_if_graph l ≠ None ?
18}.
19
20inductive ltl_function_definition (globals: list ident): Type[0] ≝
21  | ltl_fu_internal_function: ltl_internal_function globals → ltl_function_definition globals
22  | ltl_fu_external_function: external_function → ltl_function_definition globals.
23 
24record ltl_program (globals: list (ident × nat)): Type[0] ≝
25{
26  ltl_pr_funcs: list (ident × (ltl_function_definition (map ? ? \fst globals)));
27  ltl_pr_main: option ident
28}.
Note: See TracBrowser for help on using the repository browser.