source: src/LTL/LTLToLIN.ma @ 1224

Last change on this file since 1224 was 1224, checked in by sacerdot, 8 years ago

Type of programs in common/AST made more dependent.
In particular, the type of internal functions is now dependent on the
list of global variables. This is already used in the back-end to rule
out from the syntax programs that have free variables.

Note: only the test Clight/test/search.c.ma has been ported to the new type.
The porting requires two very minor changes.

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