popl09/insert_quantifiers.ml

   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_term = function
  13     Past.Atomic(term) -> Ast.get_fvs term
  14   | Past.IfThen(test,thn,(afvs,_,_,_)) ->
  15       Common.union_set afvs
  16         (Common.union_set (fvs_term test) (fvs_term thn))
  17   | Past.TExists(var,term) -> failwith "not possible"
  18
  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"
  25
  26 and fvs_dots = function
  27     Past.Dots -> []
  28   | Past.Nest(seq) -> fvs_sequence seq
  29   | Past.When(dots,seq) -> Common.union_set (fvs_dots dots) (fvs_sequence seq)
  30
  31 (* --------------------------------------------------------------------- *)
  32
  33 let inter_set l1 l2 = List.filter (function l1e -> List.mem l1e l2) l1
  34
  35 let minus_set l1 l2 = List.filter (function l1e -> not (List.mem l1e l2)) l1
  36
  37 let rec quant_sequence bound = function
  38     Past.Seq(elem,seq) ->
  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"
  49
  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))
  54         free x
  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,
  64                           aft))
  65   | Past.TExists(var,term) -> failwith "not possible"
  66
  67 and quant_element bound = function
  68     Past.Term(term,ba) ->
  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)
  72   | Past.DInfo(dots) ->
  73       Past.DInfo(quant_dots bound dots)
  74   | Past.EExists(var,seq) -> failwith "not possible"
  75
  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
  82
  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)
  88
  89 (* --------------------------------------------------------------------- *)
  90
  91 let insert_quantifiers x = quant_sequence [] x