source: src/LTL/LTLToLIN.ma @ 757

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

Lots more fixing to get both front and backends using same conventions and types.

File size: 4.5 KB
Line 
1include "LTL/LTL.ma".
2include "LIN/LIN.ma".
3include "utilities/BitVectorTrieSet.ma".
4include "common/Graphs.ma".
5
6axiom LTLTag: String.
7
8definition translate_statement: ∀globals. ltl_statement globals → pre_lin_statement globals ≝
9  λglobals: list ident.
10  λs: ltl_statement globals.
11    match s with
12    [ joint_st_return ⇒ joint_st_return ? globals
13    | joint_st_sequential instr _ ⇒ joint_st_sequential ? globals instr it
14    | joint_st_goto lbl ⇒ joint_st_goto ? globals lbl
15    ].
16   
17definition require: ident → BitVectorTrieSet 16 → BitVectorTrieSet 16 ≝
18  λl: ident.
19  λg: BitVectorTrieSet 16.
20    set_insert ? l g.
21   
22definition mark: ident → BitVectorTrieSet 16 → BitVectorTrieSet 16 ≝
23  λl: ident.
24  λg: BitVectorTrieSet 16.
25    set_insert ? l g.
26   
27definition marked: ident → BitVectorTrieSet 16 → bool ≝
28  λl: ident.
29  λg: BitVectorTrieSet 16.
30    set_member ? l g.
31   
32definition graph_lookup ≝
33  λglobals.
34  λl: ident.
35  λg: ltl_statement_graph globals.
36    lookup LabelTag (LTLStatement globals) g (an_identifier LabelTag l).
37   
38definition fetch: ∀globals: list Identifier. Identifier → LTLStatementGraph globals → option (LTLStatement globals) ≝
39  λglobals: list Identifier.
40  λl: Identifier.
41  λg: LTLStatementGraph globals.
42    graph_lookup globals l g.
43
44definition foo ≝
45  λl2, visited, required, globals, generated, g, n.
46  λvisit:
47  ∀globals: list Identifier.
48  ∀g: LTLStatementGraph globals.
49  ∀required: BitVectorTrieSet 16.
50  ∀visited: BitVectorTrieSet 16.
51  ∀generated: list (PreLINStatement globals).
52  ∀l: Identifier.
53  ∀n: nat.
54    BitVectorTrieSet 16 × (list (PreLINStatement globals)).
55  if marked l2 visited then
56    〈require l2 required, (Joint_St_Goto ? globals l2) :: generated〉
57  else
58   visit globals g required visited generated l2 n.
59
60let rec visit (globals: list ident) (g: ltl_statement_graph globals)
61              (required: BitVectorTrieSet 16) (visited: BitVectorTrieSet 16)
62              (generated: list (pre_lin_statement globals)) (l: ident) (n: nat) on n: BitVectorTrieSet 16 × (list (PreLINStatement globals)) ≝
63  match n with
64  [ O ⇒ 〈required, generated〉
65  | S n' ⇒
66    let visited' ≝ mark l visited in
67    match fetch globals l g with
68    [ None ⇒ 〈required, generated〉 (* dpm: correct? *)
69    | Some statement ⇒
70      let translated_statement ≝ translate_statement globals statement in
71      let generated'' ≝ translated_statement :: generated in
72      match statement with
73      [ joint_st_sequential instr l2 ⇒
74        match instr with
75        [ joint_instr_cond_acc l1 ⇒
76            let required' ≝
77              if marked l2 visited' then
78                require l2 required
79              else
80                required in
81            let 〈required', generated''〉 ≝
82             foo l2 visited' required' globals generated'' g n' visit (*
83              if marked l2 visited' then
84                〈required', (Joint_St_Goto ? globals l2) :: generated''〉
85              else
86                visit globals g required' visited' generated'' l2 n'*) in
87            let required'' ≝ require l1 required' in
88              if ¬(marked l1 visited') then
89                visit globals g required'' visited' generated'' l1 n'
90              else
91                〈required', generated''〉
92        | _ ⇒
93          let required' ≝
94            if marked l2 visited' then
95              require l2 required
96            else
97              required in
98          if marked l2 visited' then
99            〈required', Joint_St_Goto ? globals l2 :: generated''〉
100          else
101            visit globals g required' visited' generated'' l2 n'
102        ]
103      | joint_st_goto lbl ⇒
104        let required' ≝
105          if marked lbl visited' then
106            require lbl required
107          else
108            required in
109        if marked lbl visited' then
110          〈required', (Joint_St_Goto ? globals lbl) :: generated''〉
111        else
112          visit globals g required' visited' generated'' lbl n'
113      | joint_st_Return ⇒ 〈required, generated''〉 (* dpm: correct? *)
114      ]
115    ]
116  ].
117
118(*
119definition translate_graph ≝
120  λglobals: list Identifier.
121  λg: LTLStatementGraph globals.
122  λentry: Identifier.
123    let visited ≝ set_empty ? in
124    let required ≝ set_insert ? entry (set_empty ?) in
125    let 〈required', translated〉 ≝ visit globals g required visited [ ] entry in
126    let reversed ≝ rev ? translated in
127      filter (λs: PreLINStatement globals. ?) reversed.
128*)
Note: See TracBrowser for help on using the repository browser.