let replace_thingie s t =
  let dolT = Str.regexp "qqqqq" in
  Str.global_replace dolT t s

let instantiate_preds_for_format (f:Id.format_t) =
  replace_thingie
    ("pred cardGeq1(set S:qqqqq) = existpos x of qqqqq: x in S;\n" ^
     "pred cardGeq2(set S:qqqqq) = existpos x of qqqqq: existpos y of qqqqq: x in S & y in S & x != y;\n" ^
     "pred cardLeq1(set S:qqqqq) = allpos x, y of qqqqq: x in S & y in S => x=y;\n" ^
     "pred cardEq0(set S:qqqqq) = empty(S);\n" ^
     "pred cardEq1(set S:qqqqq) = cardGeq1(S) & cardLeq1(S);\n\n" ^
     "pred disjoint2(set S1:qqqqq, set S2:qqqqq) = empty(S1 inter S2);\n" ^
     "pred disjoint3(set S1:qqqqq, set S2:qqqqq, set S3:qqqqq) = \n" ^
     "     empty(S1 inter S2) &\n" ^
     "     empty(S1 inter S3) &\n" ^
     "     empty(S2 inter S3);\n" ^
     "pred disjoint4(set S1:qqqqq, set S2:qqqqq, set S3:qqqqq, set S4:qqqqq) =\n" ^
     "     disjoint3(S1, S2, S3) & \n" ^
     "     empty(S4 inter (S1 union S2 union S3));\n" ^
     "pred disjoint5(set S1:qqqqq, set S2:qqqqq, set S3:qqqqq, set S4:qqqqq, set S5:qqqqq) =\n" ^
     "     disjoint4(S1, S2, S3, S4) & \n" ^
     "     empty(S5 inter (S1 union S2 union S3 union S4)); \n\n")
    f

let collect_formats_from_impl (mi:string Iabsyn.impl_module) =
  List.map (fun x -> instantiate_preds_for_format x.Iabsyn.format_name) 
    mi.Iabsyn.formats 

let collect_formats_from_callees 
    ((ma : string Aabsyn.abst_body),
     (ms : Sabsyn.spec_module),
     (mi : string Iabsyn.impl_module)) : string =
  let visited = ref [] in
  let printed_formats = ref mi.Iabsyn.formats in
  let collect_callees (ms:Sabsyn.spec_module) =
    List.concat (List.map (fun x -> x.Sabsyn.calls) ms.Sabsyn.procs) in
  let rec cf (ms:Sabsyn.spec_module) = 
    String.concat "" (List.map (fun x0 -> 
      let x = Ast.fetch_spec x0 in
      String.concat "" 
        (List.map instantiate_preds_for_format x.Sabsyn.formats) ^
      if (not (List.mem x !visited)) then
        (visited := x :: !visited; cf x) else "") (collect_callees ms)) in
  cf ms

  (* Collect all formats that
     occur in the analysis of procedure p
     (formats in the implementation module mi for p,
     and formats in the specification modules
     called from p).

     Then, instantiate the definitions of standard
     predicates like cardEq and disjoint for these
     formats.
   *)

let write_preds (file : out_channel) 
    ((ma : string Aabsyn.abst_body),
     (ms : Sabsyn.spec_module),
     (mi : string Iabsyn.impl_module))
    (p : Sabsyn.proc_spec) : unit = 
  List.iter (output_string file) (collect_formats_from_impl mi);
  output_string file (collect_formats_from_callees (ma, ms, mi))