Changeset 757 for src/LTL/LTL.ma


Ignore:
Timestamp:
Apr 18, 2011, 12:30:53 PM (9 years ago)
Author:
mulligan
Message:

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

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/LTL/LTL.ma

    r753 r757  
    11include "common/Graphs.ma".
    22include "utilities/IdentifierTools.ma".
    3 
    43include "LIN/LIN.ma".
    54
    6 definition LTLStatement ≝ JointStatement Identifier.
     5definition ltl_statement ≝ joint_statement ident.
    76 
    8 definition LTLStatementGraph ≝ λglobals. graph (LTLStatement globals).
     7definition ltl_statement_graph ≝ λglobals. graph (ltl_statement globals).
    98 
    10 record LTLInternalFunction (globals: list Identifier): Type[0] ≝
     9record ltl_internal_function (globals: list ident): Type[0] ≝
    1110{
    12   LTL_IF_LUniverse: Universe;
    13   LTL_IF_StackSize: nat;
    14   LTL_IF_Graph: LTLStatementGraph globals;
    15   LTL_IF_Entry: label;
    16   LTL_IF_Exit: label
     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
    1717}.
    1818
    19 inductive LTLFunctionDefinition (globals: list Identifier): Type[0] ≝
    20   | LTL_Fu_InternalFunction: LTLInternalFunction globals → LTLFunctionDefinition globals
    21   | LTL_Fu_ExternalFunction: ExternalFunction → LTLFunctionDefinition globals.
     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.
    2222 
    23 record LTLProgram (globals: list (Identifier × nat)): Type[0] ≝
     23record ltl_program (globals: list (ident × nat)): Type[0] ≝
    2424{
    25   LTL_Pr_Funs: list (Identifier × (LTLFunctionDefinition (map ? ? \fst globals)));
    26   LTL_Pr_Main: option Identifier
     25  ltl_pr_funcs: list (ident × (ltl_function_definition (map ? ? \fst globals)));
     26  ltl_pr_main: option ident
    2727}.
Note: See TracChangeset for help on using the changeset viewer.