source: src/LTL/LTLToLIN.ma @ 1110

Last change on this file since 1110 was 1110, checked in by mulligan, 8 years ago

changes to get ltl to lin pass to work properly

File size: 4.8 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    [ ltl_st_lift l ⇒
13      match l with
14      [ joint_st_return ⇒ lin_st_lift globals (joint_st_return ? globals)
15      | joint_st_sequential instr _ ⇒ lin_st_lift globals (joint_st_sequential ? globals instr it)
16      ]
17    | ltl_st_skip l ⇒ lin_st_goto globals l
18    ].
19   
20definition require: label → BitVectorTrieSet 16 → BitVectorTrieSet 16 ≝
21  λl: label.
22  λg: BitVectorTrieSet 16.
23    set_insert ? (word_of_identifier ? l) g.
24   
25definition mark: label → BitVectorTrieSet 16 → BitVectorTrieSet 16 ≝
26  λl: label.
27  λg: BitVectorTrieSet 16.
28    set_insert ? (word_of_identifier ? l) g.
29   
30definition marked: label → BitVectorTrieSet 16 → bool ≝
31  λl: label.
32  λg: BitVectorTrieSet 16.
33    set_member ? (word_of_identifier ? l) g.
34   
35(* alias id "lookupn" = "cic:/matita/cerco/common/Identifiers/lookup.def(3)". *)
36   
37definition graph_lookup ≝
38  λglobals: list ident.
39  λl: label.
40  λgr: ltl_statement_graph globals.
41    lookup LabelTag ? gr (an_identifier LabelTag (word_of_identifier ? l)).
42   
43definition fetch: ∀globals: list ident. label → ltl_statement_graph globals → option (ltl_statement globals) ≝
44  λglobals: list ident.
45  λl: label.
46  λg: ltl_statement_graph globals.
47    graph_lookup globals l g.
48
49definition foo ≝
50  λl2, visited, required, globals, generated, g, n.
51  λvisit:
52  ∀globals: list ident.
53  ∀g: ltl_statement_graph globals.
54  ∀required: BitVectorTrieSet 16.
55  ∀visited: BitVectorTrieSet 16.
56  ∀generated: list (pre_lin_statement globals).
57  ∀l: label.
58  ∀n: nat.
59    BitVectorTrieSet 16 × (list (pre_lin_statement globals)).
60  if marked l2 visited then
61    〈require l2 required, (lin_st_goto globals l2) :: generated〉
62  else
63   visit globals g required visited generated l2 n.
64
65let rec visit
66  (globals: list ident) (g: ltl_statement_graph globals)
67  (required: BitVectorTrieSet 16) (visited: BitVectorTrieSet 16)
68  (generated: list (pre_lin_statement globals)) (l: label) (n: nat)
69    on n: BitVectorTrieSet 16 × (list (pre_lin_statement globals)) ≝
70  match n with
71  [ O ⇒ 〈required, generated〉
72  | S n' ⇒
73    let visited' ≝ mark l visited in
74    match fetch globals l g with
75    [ None ⇒ 〈required, generated〉 (* dpm: correct? *)
76    | Some statement ⇒
77      let translated_statement ≝ translate_statement globals statement in
78      let generated'' ≝ translated_statement :: generated in
79      match statement with
80      [ ltl_st_lift l ⇒
81        match l with
82        [ joint_st_sequential instr l2 ⇒
83          match instr with
84          [ joint_instr_cond_acc l1 ⇒
85              let required' ≝
86                if marked l2 visited' then
87                  require l2 required
88                else
89                  required in
90              let 〈required', generated''〉 ≝
91               foo l2 visited' required' globals generated'' g n' visit (*
92                if marked l2 visited' then
93                  〈required', (Joint_St_Goto ? globals l2) :: generated''〉
94                else
95                  visit globals g required' visited' generated'' l2 n'*) in
96              let required'' ≝ require l1 required' in
97                if ¬(marked l1 visited') then
98                  visit globals g required'' visited' generated'' l1 n'
99                else
100                  〈required', generated''〉
101          | _ ⇒
102            let required' ≝
103              if marked l2 visited' then
104                require l2 required
105              else
106                required in
107            if marked l2 visited' then
108              〈required', lin_st_goto globals l2 :: generated''〉
109            else
110              visit globals g required' visited' generated'' l2 n'
111          ]
112        | joint_st_return ⇒ 〈required, generated''〉 (* dpm: correct? *)
113      ]
114    | ltl_st_skip l ⇒
115       let required' ≝
116         if marked l visited' then
117           require l required
118         else
119           required
120       in
121         if marked l visited' then
122           〈required', lin_st_goto globals l :: generated''〉
123         else
124           visit globals g required' visited' generated'' l n'
125    ]
126  ]
127].
128
129(*
130definition translate_graph ≝
131  λglobals: list Identifier.
132  λg: LTLStatementGraph globals.
133  λentry: Identifier.
134    let visited ≝ set_empty ? in
135    let required ≝ set_insert ? entry (set_empty ?) in
136    let 〈required', translated〉 ≝ visit globals g required visited [ ] entry in
137    let reversed ≝ rev ? translated in
138      filter (λs: PreLINStatement globals. ?) reversed.
139*)
Note: See TracBrowser for help on using the repository browser.