4 (* --------------------------------------------------------------------- *)
6 let rec fvs_sequence = function
8 Common.union_set
(fvs_element elem
) (fvs_sequence seq
)
10 | Past.SExists
(var
,seq
) -> failwith
"not possible"
12 and fvs_term
= function
13 Past.Atomic
(term
) -> Ast.get_fvs term
14 | Past.IfThen
(test
,thn
,(afvs
,_
,_
,_
)) ->
16 (Common.union_set
(fvs_term test
) (fvs_term thn
))
17 | Past.TExists
(var
,term
) -> failwith
"not possible"
19 and fvs_element
= function
20 Past.Term
(term
,_
) -> fvs_term term
21 | Past.Or
(seq1
,seq2
) ->
22 Common.union_set
(fvs_sequence seq1
) (fvs_sequence seq2
)
23 | Past.DInfo
(dots
) -> fvs_dots dots
24 | Past.EExists
(var
,seq
) -> failwith
"not possible"
26 and fvs_dots
= function
28 | Past.Nest
(seq
) -> fvs_sequence seq
29 | Past.When
(dots
,seq
) -> Common.union_set
(fvs_dots dots
) (fvs_sequence seq
)
31 (* --------------------------------------------------------------------- *)
33 let inter_set l1 l2
= List.filter
(function l1e
-> List.mem l1e l2
) l1
35 let minus_set l1 l2
= List.filter
(function l1e
-> not
(List.mem l1e l2
)) l1
37 let rec quant_sequence bound
= function
39 let fe = fvs_element elem
in
40 let fs = fvs_sequence seq
in
41 let inter = inter_set fe fs in
42 let free = minus_set inter bound
in
43 let new_bound = free @ bound
in
44 List.fold_right
(function cur
-> function rest
-> Past.SExists
(cur
,rest
))
45 free (Past.Seq
(quant_element
new_bound elem
,
46 quant_sequence new_bound seq
))
47 | Past.Empty
-> Past.Empty
48 | Past.SExists
(var
,seq
) -> failwith
"not possible"
50 and quant_term bound
= function
51 (Past.Atomic
(term
)) as x
->
52 let free = minus_set (Ast.get_fvs term
) bound
in
53 List.fold_right
(function cur
-> function rest
-> Past.TExists
(cur
,rest
))
55 | Past.IfThen
(test
,thn
,((afvs
,_
,_
,_
) as aft
)) ->
56 let fts = fvs_term test
in
57 let fth = fvs_term thn
in
58 let inter = inter_set fts fth in
59 let free = minus_set inter bound
in
60 let new_bound = free @ bound
in
61 List.fold_right
(function cur
-> function rest
-> Past.TExists
(cur
,rest
))
62 free (Past.IfThen
(quant_term
new_bound test
,
63 quant_term
new_bound thn
,
65 | Past.TExists
(var
,term
) -> failwith
"not possible"
67 and quant_element bound
= function
69 Past.Term
(quant_term bound term
,dots_bef_aft bound ba
)
70 | Past.Or
(seq1
,seq2
) ->
71 Past.Or
(quant_sequence bound seq1
,quant_sequence bound seq2
)
73 Past.DInfo
(quant_dots bound dots
)
74 | Past.EExists
(var
,seq
) -> failwith
"not possible"
76 and dots_bef_aft bound
= function
77 Past.AddingBetweenDots
(brace_term
,n
) ->
78 Past.AddingBetweenDots
(quant_term bound brace_term
,n
)
79 | Past.DroppingBetweenDots
(brace_term
,n
) ->
80 Past.DroppingBetweenDots
(quant_term bound brace_term
,n
)
81 | Past.NoDots
-> Past.NoDots
83 and quant_dots bound
= function
84 Past.Dots
-> Past.Dots
85 | Past.Nest
(seq
) -> Past.Nest
(quant_sequence bound seq
)
86 | Past.When
(dots
,seq
) ->
87 Past.When
(quant_dots bound dots
, quant_sequence bound seq
)
89 (* --------------------------------------------------------------------- *)
91 let insert_quantifiers x
= quant_sequence [] x