HCoop / bpt / coccinelle.git / blame
| Commit | Line | Data |
|---|---|---|
| 951c7801 C |
1 | module Ast = Ast_cocci |
| 2 | module Past = Ast_popl | |
| 3 | ||
| 4 | (* --------------------------------------------------------------------- *) | |
| 5 | ||
| 6 | let rec fvs_sequence = function | |
| 7 | Past.Seq(elem,seq) -> | |
| 8 | Common.union_set (fvs_element elem) (fvs_sequence seq) | |
| 9 | | Past.Empty -> [] | |
| 10 | | Past.SExists(var,seq) -> failwith "not possible" | |
| 11 | ||
| 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) -> | |
| 17 | List.fold_left | |
| 18 | (function prev -> | |
| 19 | function cur -> | |
| 20 | Common.union_set (fvs_element cur) prev) | |
| 21 | (fvs_dots dots) seq_bef | |
| 22 | | Past.EExists(var,seq) -> failwith "not possible" | |
| 23 | ||
| 24 | and fvs_dots = function | |
| 25 | Past.Dots -> [] | |
| 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" | |
| 29 | ||
| 30 | (* --------------------------------------------------------------------- *) | |
| 31 | ||
| 32 | let rec quant_sequence bound = function | |
| 33 | Past.Seq(elem,seq) -> | |
| 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" | |
| 44 | ||
| 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)) | |
| 49 | free x | |
| 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" | |
| 56 | ||
| 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" | |
| 70 | ||
| 71 | (* --------------------------------------------------------------------- *) | |
| 72 | ||
| 73 | let insert_quantifiers x = quant_sequence [] x |