Changeset 722 for src/LTL/LTL.ma


Ignore:
Timestamp:
Mar 29, 2011, 6:32:47 PM (9 years ago)
Author:
mulligan
Message:

Committing changes from today. Several files do not typecheck.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/LTL/LTL.ma

    r716 r722  
    77include "ASM/String.ma".
    88
    9 inductive LTLStatement (globals: list Identifier): Type[0] ≝
    10   | LTL_St_Skip: label → LTLStatement globals
    11   | LTL_St_Comment: String → label → LTLStatement globals
    12   | LTL_St_CostLabel: Identifier → label → LTLStatement globals
    13   | LTL_St_Int: Register → Byte → label → LTLStatement globals
    14   | LTL_St_Pop: label → LTLStatement globals
    15   | LTL_St_Push: label → LTLStatement globals
    16   | LTL_St_Address: ∀i: Identifier. (member i (eq_bv ?) globals) → Identifier → label → LTLStatement globals
    17   | LTL_St_FromAcc: Register → label → LTLStatement globals
    18   | LTL_St_ToAcc: Register → label → LTLStatement globals
    19   | LTL_St_OpAccs: OpAccs → label → LTLStatement globals
    20   | LTL_St_Op1: Op1 → label → LTLStatement globals
    21   | LTL_St_Op2: Op2 → Register → label → LTLStatement globals
    22   | LTL_St_ClearCarry: label → LTLStatement globals
    23   | LTL_St_Load: label → LTLStatement globals
    24   | LTL_St_Store: label → LTLStatement globals
    25   | LTL_St_CallId: Identifier → label → LTLStatement globals
    26   | LTL_St_CondAcc: label → label → LTLStatement globals
    27   | LTL_St_Return: LTLStatement globals.
     9include "LIN/LIN.ma".
     10
     11definition LTLStatement ≝ JointStatement Identifier.
    2812 
    29 definition LTLFunctionGraph ≝ λglobals. graph (LTLStatement globals).
     13definition LTLStatementGraph ≝ λglobals. graph (LTLStatement globals).
    3014 
    3115record LTLInternalFunction (globals: list Identifier): Type[0] ≝
     
    3317  LTL_IF_LUniverse: Universe;
    3418  LTL_IF_StackSize: nat;
    35   LTL_IF_Graph: LTLFunctionGraph globals;
     19  LTL_IF_Graph: LTLStatementGraph globals;
    3620  LTL_IF_Entry: label;
    3721  LTL_IF_Exit: label
Note: See TracChangeset for help on using the changeset viewer.