source: src/LTL/LTLToLIN.ma @ 715

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

Restored rev from Util as it appears that list reversal is not a part of the standard library, but a local modification.

File size: 742 bytes
Line 
1include "LTL/LTL.ma".
2include "LIN/LIN.ma".
3
4definition label_to_Identifier ≝
5  λl: label.
6  let n ≝ nat_of_pos l in
7    bitvector_of_nat 8 n.
8
9definition translate_statement ≝
10  λglobals: list Identifier.
11  λs: LTLStatement globals.
12    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
21    ].
Note: See TracBrowser for help on using the repository browser.