source: src/LTL/LTLToLIN.ma @ 1111

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

minor change: marked some possibly dodgy (and very complex) code
File size: 4.9 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
65(* XXX: look at this.  way too complicated to understand whether it is correct,
66   in my opinion.
67*)
68let rec visit
69  (globals: list ident) (g: ltl_statement_graph globals)
70  (required: BitVectorTrieSet 16) (visited: BitVectorTrieSet 16)
71  (generated: list (pre_lin_statement globals)) (l: label) (n: nat)
72    on n: BitVectorTrieSet 16 × (list (pre_lin_statement globals)) ≝
73  match n with
74  [ O ⇒ 〈required, generated〉
75  | S n' ⇒
76    let visited' ≝ mark l visited in
77    match fetch globals l g with
78    [ None ⇒ 〈required, generated〉 (* dpm: correct? *)
79    | Some statement ⇒
80      let translated_statement ≝ translate_statement globals statement in
81      let generated'' ≝ translated_statement :: generated in
82      match statement with
83      [ ltl_st_lift l ⇒
84        match l with
85        [ joint_st_sequential instr l2 ⇒
86          match instr with
87          [ joint_instr_cond_acc l1 ⇒
88              let required' ≝
89                if marked l2 visited' then
90                  require l2 required
91                else
92                  required in
93              let 〈required', generated''〉 ≝
94               foo l2 visited' required' globals generated'' g n' visit (*
95                if marked l2 visited' then
96                  〈required', (Joint_St_Goto ? globals l2) :: generated''〉
97                else
98                  visit globals g required' visited' generated'' l2 n'*) in
99              let required'' ≝ require l1 required' in
100                if ¬(marked l1 visited') then
101                  visit globals g required'' visited' generated'' l1 n'
102                else
103                  〈required', generated''〉
104          | _ ⇒
105            let required' ≝
106              if marked l2 visited' then
107                require l2 required
108              else
109                required in
110            if marked l2 visited' then
111              〈required', lin_st_goto globals l2 :: generated''〉
112            else
113              visit globals g required' visited' generated'' l2 n'
114          ]
115        | joint_st_return ⇒ 〈required, generated''〉 (* dpm: correct? *)
116      ]
117    | ltl_st_skip l ⇒
118       let required' ≝
119         if marked l visited' then
120           require l required
121         else
122           required
123       in
124         if marked l visited' then
125           〈required', lin_st_goto globals l :: generated''〉
126         else
127           visit globals g required' visited' generated'' l n'
128    ]
129  ]
130].
131
132(*
133definition translate_graph ≝
134  λglobals: list Identifier.
135  λg: LTLStatementGraph globals.
136  λentry: Identifier.
137    let visited ≝ set_empty ? in
138    let required ≝ set_insert ? entry (set_empty ?) in
139    let 〈required', translated〉 ≝ visit globals g required visited [ ] entry in
140    let reversed ≝ rev ? translated in
141      filter (λs: PreLINStatement globals. ?) reversed.
142*)
Note: See TracBrowser for help on using the repository browser.