Project

General

Profile

Revision def3763d src/lib/EAFormula.ml

View differences:

src/lib/EAFormula.ml
78 78
  | ID f1 ->
79 79
      Buffer.add_string sb "0";
80 80
      prio 4 f1
81
  | MU (s, f1) ->
82
      Buffer.add_string sb "µ";
83
      Buffer.add_string sb s;
84
      Buffer.add_string sb ".";
85
      prio 4 f1
86
  | NU (s, f1) ->
87
      Buffer.add_string sb "ν";
88
      Buffer.add_string sb s;
89
      Buffer.add_string sb ".";
90
      prio 4 f1
81 91
  | E_AP s ->
82 92
      Buffer.add_string sb "E";
83 93
      Buffer.add_string sb "(";
......
196 206
  (*mapping from nominals to new syms*)
197 207
  let nomsub = ref StringMap.empty in
198 208

  
209
  print_endline (CoAlgFormula.exportFormula f);
210

  
199 211
  (*first rename nominals then change type to eaformula*)
200 212
  let form1help = rename f nomsub noms in
213
  print_string "form1help: ";
214
  print_endline (CoAlgFormula.exportFormula form1help);
215

  
201 216
  let form1 = coalgtoea form1help in
217
  print_string "form1: ";
218
  print_endline (exportFormula form1);
202 219

  
203 220
  (*first calculate flc (and in future the other stuff) then rename nominals then change type to eaformula*)
204 221
  (*TODO Wont work for this A in translation.. Fix it!*)
205 222
  let form2help = formula2 f noms nomTbl sorts in
223
  print_string "form2help: ";
224
  print_endline (CoAlgFormula.exportFormula form2help);
225

  
206 226
  let form22 = rename form2help nomsub noms in
227
  print_string "form22: ";
228
  print_endline (CoAlgFormula.exportFormula form22);
229

  
207 230
  let form2 = coalgtoea form22 in
208
  
231
  print_string "form2: ";
232
  print_endline (exportFormula form2);
233

  
209 234
  (*conjunction of all new nominalsymbols*)
210 235
  let form3 = if List.length !noms > 0 then formula3 !noms else TRUE in
236
  print_string "form3: ";
237
  print_endline (exportFormula form3);
211 238
  
212 239
  let formula = if List.length !noms > 0 then AND(AND(form1, form2), form3) else form1 in
213 240
 

Also available in: Unified diff