source: src/LTL/LTL.ma @ 1179

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

changes to ertl, ltl and lin to use new notion of joint params. ertl to ltl pass in process of being changed

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