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