Changeset 722 for src/LTL


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

Committing changes from today. Several files do not typecheck.

Location:
src/LTL
Files:
3 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
  • src/LTL/LTLToLIN.ma

    r716 r722  
    22include "LIN/LIN.ma".
    33
    4 definition label_to_Identifier ≝
    5   λl: label.
    6   let n ≝ nat_of_pos l in
    7     bitvector_of_nat 8 n.
    8 
    9 definition translate_statement ≝
     4definition translate_statement: ∀globals. LTLStatement globals → LINStatement globals ≝
    105  λglobals: list Identifier.
    116  λs: LTLStatement globals.
    127    match s with
    13     [ LTL_St_Skip lbl ⇒ LIN_St_Goto globals (label_to_Identifier lbl)
    14     | LTL_St_Comment comment lbl ⇒ LIN_St_Comment globals comment
    15     | LTL_St_CostLabel cost lbl ⇒ LIN_St_CostLabel globals cost
    16     | LTL_St_Int register val lbl ⇒ LIN_St_Int globals register val
    17     | LTL_St_Pop lbl ⇒ LIN_St_Pop globals
    18     | LTL_St_Push lbl ⇒ LIN_St_Push globals
    19     | LTL_St_Address ident proof address lbl ⇒ LIN_St_Address globals ident proof
    20     | LTL_St_FromAcc register lbl ⇒ LIN_St_FromAcc globals register
    21     | LTL_St_ToAcc register lbl ⇒ LIN_St_ToAcc globals register
    22     | LTL_St_OpAccs opaccs lbl ⇒ LIN_St_OpAccs globals opaccs
    23     | LTL_St_Op1 op1 lbl ⇒ LIN_St_Op1 globals op1
    24     | LTL_St_Op2 op2 register lbl ⇒ LIN_St_Op2 globals op2 register
    25     | LTL_St_ClearCarry lbl ⇒ LIN_St_ClearCarry globals
    26     | LTL_St_Load lbl ⇒ LIN_St_Load globals
    27     | LTL_St_Store lbl ⇒ LIN_St_Store globals
    28     | LTL_St_CallId identifier lbl ⇒ LIN_St_CallId globals identifier
    29     | LTL_St_CondAcc tgt lbl ⇒ LIN_St_CondAcc globals (label_to_Identifier tgt)
    30     | LTL_St_Return ⇒ LIN_St_Return globals
     8    [ LIN_St_Return ⇒ LIN_St_Return ? globals
     9    | LIN_St_Sequential instr _ ⇒ LIN_St_Sequential ? globals instr it
    3110    ].
  • src/LTL/LTLToLINI.ma

    r716 r722  
     1include "common/Graphs.ma".
     2include "LTL/LTL.ma".
     3
     4definition fetch: ∀globals. LTLStatementGraph globals → label → option (LTLStatement globals) ≝
     5  λglobals: list Identifier.
     6  λgraph: LTLStatementGraph globals.
     7  λl: label.
     8    graph_lookup ? graph l.
     9   
     10definition generate: ∀globals. LTLStatement globals → list (LTLStatement globals) → list (LTLStatement globals) ≝
     11  λglobals.
     12  λstatement.
     13  λstatements.
     14    statement :: statements.
Note: See TracChangeset for help on using the changeset viewer.