2 * Copyright 2005-2010, Ecole des Mines de Nantes, University of Copenhagen
3 * Yoann Padioleau, Julia Lawall, Rene Rydhof Hansen, Henrik Stuart, Gilles Muller, Nicolas Palix
4 * This file is part of Coccinelle.
6 * Coccinelle is free software: you can redistribute it and/or modify
7 * it under the terms of the GNU General Public License as published by
8 * the Free Software Foundation, according to version 2 of the License.
10 * Coccinelle is distributed in the hope that it will be useful,
11 * but WITHOUT ANY WARRANTY; without even the implied warranty of
12 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
13 * GNU General Public License for more details.
15 * You should have received a copy of the GNU General Public License
16 * along with Coccinelle. If not, see <http://www.gnu.org/licenses/>.
18 * The authors reserve the right to distribute this or future versions of
19 * Coccinelle under other licenses.
24 * Copyright 2005-2010, Ecole des Mines de Nantes, University of Copenhagen
25 * Yoann Padioleau, Julia Lawall, Rene Rydhof Hansen, Henrik Stuart, Gilles Muller, Nicolas Palix
26 * This file is part of Coccinelle.
28 * Coccinelle is free software: you can redistribute it and/or modify
29 * it under the terms of the GNU General Public License as published by
30 * the Free Software Foundation, according to version 2 of the License.
32 * Coccinelle is distributed in the hope that it will be useful,
33 * but WITHOUT ANY WARRANTY; without even the implied warranty of
34 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
35 * GNU General Public License for more details.
37 * You should have received a copy of the GNU General Public License
38 * along with Coccinelle. If not, see <http://www.gnu.org/licenses/>.
40 * The authors reserve the right to distribute this or future versions of
41 * Coccinelle under other licenses.
45 module Ast
= Ast_cocci
46 module Past
= Ast_popl
48 (* --------------------------------------------------------------------- *)
50 let rec fvs_sequence = function
52 Common.union_set
(fvs_element elem
) (fvs_sequence seq
)
54 | Past.SExists
(var
,seq
) -> failwith
"not possible"
56 and fvs_element
= function
57 Past.Term
(term
) -> Ast.get_fvs term
58 | Past.Or
(seq1
,seq2
) ->
59 Common.union_set
(fvs_sequence seq1
) (fvs_sequence seq2
)
60 | Past.DInfo
(dots
,seq_bef
,seq_aft
) ->
64 Common.union_set
(fvs_element cur
) prev
)
65 (fvs_dots dots
) seq_bef
66 | Past.EExists
(var
,seq
) -> failwith
"not possible"
68 and fvs_dots
= function
70 | Past.Nest
(seq
) -> fvs_sequence seq
71 | Past.When
(dots
,seq
) -> Common.union_set
(fvs_dots dots
) (fvs_sequence seq
)
72 | Past.DExists
(var
,dots
) -> failwith
"not possible"
74 (* --------------------------------------------------------------------- *)
76 let rec quant_sequence bound
= function
78 let fe = fvs_element elem
in
79 let fs = fvs_sequence seq
in
80 let inter = Common.inter_set
fe fs in
81 let free = Common.minus_set
inter bound
in
82 let new_bound = free @ bound
in
83 List.fold_right
(function cur
-> function rest
-> Past.SExists
(cur
,rest
))
84 free (Past.Seq
(quant_element
new_bound elem
,
85 quant_sequence new_bound seq
))
86 | Past.Empty
-> Past.Empty
87 | Past.SExists
(var
,seq
) -> failwith
"not possible"
89 and quant_element bound
= function
90 Past.Term
(term
) as x
->
91 let free = Common.minus_set
(fvs_element x
) bound
in
92 List.fold_right
(function cur
-> function rest
-> Past.EExists
(cur
,rest
))
94 | Past.Or
(seq1
,seq2
) ->
95 Past.Or
(quant_sequence bound seq1
,quant_sequence bound seq2
)
96 | Past.DInfo
(dots
,seq_bef
,seq_aft
) ->
97 Past.DInfo
(quant_dots bound dots
,seq_bef
,
98 List.map
(quant_element bound
) seq_aft
)
99 | Past.EExists
(var
,seq
) -> failwith
"not possible"
101 and quant_dots bound
= function
102 Past.Dots
-> Past.Dots
103 | Past.Nest
(seq
) -> Past.Nest
(quant_sequence bound seq
)
104 | Past.When
(dots
,seq
) ->
105 let fd = fvs_dots dots
in
106 let fs = fvs_sequence seq
in
107 let inter = Common.inter_set
fd fs in
108 let free = Common.minus_set
inter bound
in
109 let new_bound = free @ bound
in
110 List.fold_right
(function cur
-> function rest
-> Past.DExists
(cur
,rest
))
111 free (Past.When
(quant_dots
new_bound dots
,
112 quant_sequence new_bound seq
))
113 | Past.DExists
(var
,dots
) -> failwith
"not possible"
115 (* --------------------------------------------------------------------- *)
117 let insert_quantifiers x
= quant_sequence [] x