source: src/LTL/LTL.ma @ 1183

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

removed parameterised label types in the three lowest level languages

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