Changeset 722 for src/LTL/LTLToLIN.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/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    ].
Note: See TracChangeset for help on using the changeset viewer.