2 * Copyright 2005-2009, 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.
23 module Ast
= Ast_cocci
24 module Past
= Ast_popl
26 (* --------------------------------------------------------------------- *)
28 let rec fvs_sequence = function
30 Common.union_set
(fvs_element elem
) (fvs_sequence seq
)
32 | Past.SExists
(var
,seq
) -> failwith
"not possible"
34 and fvs_term
= function
35 Past.Atomic
(term
) -> Ast.get_fvs term
36 | Past.IfThen
(test
,thn
,(afvs
,_
,_
,_
)) ->
38 (Common.union_set
(fvs_term test
) (fvs_term thn
))
39 | Past.TExists
(var
,term
) -> failwith
"not possible"
41 and fvs_element
= function
42 Past.Term
(term
,_
) -> fvs_term term
43 | Past.Or
(seq1
,seq2
) ->
44 Common.union_set
(fvs_sequence seq1
) (fvs_sequence seq2
)
45 | Past.DInfo
(dots
) -> fvs_dots dots
46 | Past.EExists
(var
,seq
) -> failwith
"not possible"
48 and fvs_dots
= function
50 | Past.Nest
(seq
) -> fvs_sequence seq
51 | Past.When
(dots
,seq
) -> Common.union_set
(fvs_dots dots
) (fvs_sequence seq
)
53 (* --------------------------------------------------------------------- *)
55 let inter_set l1 l2
= List.filter
(function l1e
-> List.mem l1e l2
) l1
57 let minus_set l1 l2
= List.filter
(function l1e
-> not
(List.mem l1e l2
)) l1
59 let rec quant_sequence bound
= function
61 let fe = fvs_element elem
in
62 let fs = fvs_sequence seq
in
63 let inter = inter_set fe fs in
64 let free = minus_set inter bound
in
65 let new_bound = free @ bound
in
66 List.fold_right
(function cur
-> function rest
-> Past.SExists
(cur
,rest
))
67 free (Past.Seq
(quant_element
new_bound elem
,
68 quant_sequence new_bound seq
))
69 | Past.Empty
-> Past.Empty
70 | Past.SExists
(var
,seq
) -> failwith
"not possible"
72 and quant_term bound
= function
73 (Past.Atomic
(term
)) as x
->
74 let free = minus_set (Ast.get_fvs term
) bound
in
75 List.fold_right
(function cur
-> function rest
-> Past.TExists
(cur
,rest
))
77 | Past.IfThen
(test
,thn
,((afvs
,_
,_
,_
) as aft
)) ->
78 let fts = fvs_term test
in
79 let fth = fvs_term thn
in
80 let inter = inter_set fts fth in
81 let free = minus_set inter bound
in
82 let new_bound = free @ bound
in
83 List.fold_right
(function cur
-> function rest
-> Past.TExists
(cur
,rest
))
84 free (Past.IfThen
(quant_term
new_bound test
,
85 quant_term
new_bound thn
,
87 | Past.TExists
(var
,term
) -> failwith
"not possible"
89 and quant_element bound
= function
91 Past.Term
(quant_term bound term
,dots_bef_aft bound ba
)
92 | Past.Or
(seq1
,seq2
) ->
93 Past.Or
(quant_sequence bound seq1
,quant_sequence bound seq2
)
95 Past.DInfo
(quant_dots bound dots
)
96 | Past.EExists
(var
,seq
) -> failwith
"not possible"
98 and dots_bef_aft bound
= function
99 Past.AddingBetweenDots
(brace_term
,n
) ->
100 Past.AddingBetweenDots
(quant_term bound brace_term
,n
)
101 | Past.DroppingBetweenDots
(brace_term
,n
) ->
102 Past.DroppingBetweenDots
(quant_term bound brace_term
,n
)
103 | Past.NoDots
-> Past.NoDots
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 Past.When
(quant_dots bound dots
, quant_sequence bound seq
)
111 (* --------------------------------------------------------------------- *)
113 let insert_quantifiers x
= quant_sequence [] x