source: src/LTL/LTLToLIN.ma @ 1171

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

changes made on claudio's request: changed order of nesting in the joint-ertl statements to make the semantics easier to write. big changes required...

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