source: src/ERTL/Liveness.ma @ 746

Last change on this file since 746 was 746, checked in by mulligan, 9 years ago

Changes to bitvectortrieset: equality on sets. Added new file for translation of variable set functor. other small changes.

File size: 1.5 KB
Line 
1include "ERTL/ERTL.ma".
2
3definition set_singleton ≝
4  λl: Identifier.
5    set_insert ? l (set_empty ?).
6
7definition statement_successors ≝
8  λstmt: ERTLStatement.
9  match stmt with
10  [ ERTL_St_Return _ ⇒ set_empty ?
11  | ERTL_St_Skip l ⇒ set_singleton l
12  | ERTL_St_Comment comment l ⇒ set_singleton l
13  | ERTL_St_Cost cost l ⇒ set_singleton l
14  | ERTL_St_Set_Hdw r1 r2 l ⇒ set_singleton l
15  | ERTL_St_Get_Hdw r1 r2 l ⇒ set_singleton l
16  | ERTL_St_Hdw_To_Hdw r1 r2 l ⇒ set_singleton l
17  | ERTL_St_NewFrame l ⇒ set_singleton l
18  | ERTL_St_DelFrame l ⇒ set_singleton l
19  | ERTL_St_FrameSize r l ⇒ set_singleton l
20  | ERTL_St_Push r l ⇒ set_singleton l
21  | ERTL_St_Pop r l ⇒ set_singleton l
22  | ERTL_St_AddrH r l1 l2 ⇒ set_singleton l2
23  | ERTL_St_AddrL r l1 l2 ⇒ set_singleton l2
24  | ERTL_St_Int r v l ⇒ set_singleton l
25  | ERTL_St_Move r1 r2 l ⇒ set_singleton l
26  | ERTL_St_Opaccs opaccs r1 r2 r3 l ⇒ set_singleton l
27  | ERTL_St_Op2 op2 r1 r2 r3 l ⇒ set_singleton l
28  | ERTL_St_Op1 op1 r1 r2 l ⇒ set_singleton l
29  | ERTL_St_ClearCarry l ⇒ set_singleton l
30  | ERTL_St_Load r1 r2 r3 l ⇒ set_singleton l
31  | ERTL_St_Store r1 r2 r3 l ⇒ set_singleton l
32  | ERTL_St_Call_Id id v l ⇒ set_singleton l
33  | ERTL_St_CondAcc _ l1 l2 ⇒ set_union ? (set_singleton l1) (set_singleton l2)
34  ].
35
36definition set_of_list ≝
37  λn: nat.
38  λl: list (BitVector n).
39    foldr ? ? (set_insert ?) (set_empty ?) l.
40   
41definition dptr ≝
42  set_insert ? (word_of_register RegisterDPL) (set_singleton ? (word_of_register RegisterDPH)).
Note: See TracBrowser for help on using the repository browser.