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_element
= function
13 Past.Term
(term
) -> Ast.get_fvs term
14 | Past.Or
(seq1
,seq2
) ->
15 Common.union_set
(fvs_sequence seq1
) (fvs_sequence seq2
)
16 | Past.DInfo
(dots
,seq_bef
,seq_aft
) ->
20 Common.union_set
(fvs_element cur
) prev
)
21 (fvs_dots dots
) seq_bef
22 | Past.EExists
(var
,seq
) -> failwith
"not possible"
24 and fvs_dots
= function
26 | Past.Nest
(seq
) -> fvs_sequence seq
27 | Past.When
(dots
,seq
) -> Common.union_set
(fvs_dots dots
) (fvs_sequence seq
)
28 | Past.DExists
(var
,dots
) -> failwith
"not possible"
30 (* --------------------------------------------------------------------- *)
32 let rec quant_sequence bound
= function
34 let fe = fvs_element elem
in
35 let fs = fvs_sequence seq
in
36 let inter = Common.inter_set
fe fs in
37 let free = Common.minus_set
inter bound
in
38 let new_bound = free @ bound
in
39 List.fold_right
(function cur
-> function rest
-> Past.SExists
(cur
,rest
))
40 free (Past.Seq
(quant_element
new_bound elem
,
41 quant_sequence new_bound seq
))
42 | Past.Empty
-> Past.Empty
43 | Past.SExists
(var
,seq
) -> failwith
"not possible"
45 and quant_element bound
= function
46 Past.Term
(term
) as x
->
47 let free = Common.minus_set
(fvs_element x
) bound
in
48 List.fold_right
(function cur
-> function rest
-> Past.EExists
(cur
,rest
))
50 | Past.Or
(seq1
,seq2
) ->
51 Past.Or
(quant_sequence bound seq1
,quant_sequence bound seq2
)
52 | Past.DInfo
(dots
,seq_bef
,seq_aft
) ->
53 Past.DInfo
(quant_dots bound dots
,seq_bef
,
54 List.map
(quant_element bound
) seq_aft
)
55 | Past.EExists
(var
,seq
) -> failwith
"not possible"
57 and quant_dots bound
= function
58 Past.Dots
-> Past.Dots
59 | Past.Nest
(seq
) -> Past.Nest
(quant_sequence bound seq
)
60 | Past.When
(dots
,seq
) ->
61 let fd = fvs_dots dots
in
62 let fs = fvs_sequence seq
in
63 let inter = Common.inter_set
fd fs in
64 let free = Common.minus_set
inter bound
in
65 let new_bound = free @ bound
in
66 List.fold_right
(function cur
-> function rest
-> Past.DExists
(cur
,rest
))
67 free (Past.When
(quant_dots
new_bound dots
,
68 quant_sequence new_bound seq
))
69 | Past.DExists
(var
,dots
) -> failwith
"not possible"
71 (* --------------------------------------------------------------------- *)
73 let insert_quantifiers x
= quant_sequence [] x