source: src/LTL/LTL.ma @ 722

Last change on this file since 722 was 722, checked in by mulligan, 9 years ago

Committing changes from today. Several files do not typecheck.

File size: 997 bytes
Line 
1include "common/Graphs.ma".
2include "common/AST.ma".
3
4include "utilities/IdentifierTools.ma".
5
6include "ASM/I8051.ma".
7include "ASM/String.ma".
8
9include "LIN/LIN.ma".
10
11definition LTLStatement ≝ JointStatement Identifier.
12 
13definition LTLStatementGraph ≝ λglobals. graph (LTLStatement globals).
14 
15record LTLInternalFunction (globals: list Identifier): Type[0] ≝
16{
17  LTL_IF_LUniverse: Universe;
18  LTL_IF_StackSize: nat;
19  LTL_IF_Graph: LTLStatementGraph globals;
20  LTL_IF_Entry: label;
21  LTL_IF_Exit: label
22}.
23
24inductive LTLFunctionDefinition (globals: list Identifier): Type[0] ≝
25  | LTL_Fu_InternalFunction: LTLInternalFunction globals → LTLFunctionDefinition globals
26  | LTL_Fu_ExternalFunction: ExternalFunction → LTLFunctionDefinition globals.
27 
28record LTLProgram (globals: list Identifier): Type[0] ≝
29{
30  LTL_Pr_Vars: list (Identifier × nat); (* 2nd component = size *)
31  LTL_Pr_Funs: list (Identifier × (LTLFunctionDefinition globals));
32  LTL_Pr_Main: option Identifier
33}.
Note: See TracBrowser for help on using the repository browser.