source: src/LTL/LTL.ma @ 764

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

Lots more fixing to get both front and backends using same conventions and types.

File size: 921 bytes
Line 
1include "common/Graphs.ma".
2include "utilities/IdentifierTools.ma".
3include "LIN/LIN.ma".
4
5definition ltl_statement ≝ joint_statement ident.
6 
7definition ltl_statement_graph ≝ λglobals. graph (ltl_statement globals).
8 
9record ltl_internal_function (globals: list ident): Type[0] ≝
10{
11  ltl_if_luniverse: universe LabelTag;
12  ltl_if_runiverse: universe RegisterTag;
13  ltl_if_StackSize: nat;
14  ltl_if_Graph: ltl_statement_graph globals;
15  ltl_if_Entry: label;
16  ltl_if_Exit: label
17}.
18
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.
22 
23record ltl_program (globals: list (ident × nat)): Type[0] ≝
24{
25  ltl_pr_funcs: list (ident × (ltl_function_definition (map ? ? \fst globals)));
26  ltl_pr_main: option ident
27}.
Note: See TracBrowser for help on using the repository browser.