added nom2fix method

src/coalg/coalg.ml

@@ -46,7 +46,7 @@ let _ =
 
 let printUsage () =
   print_endline "Usage: \"alc <task> <functor> [<flags>]\" where";
-  print_endline "       <task> in { sat print verify nnf prov (is »not.(sat ¬f)«) }";
+  print_endline "       <task> in { sat print verify nnf prov (is »not.(sat ¬f)«) nom2fix }";
   print_endline "       <functor> in { MultiModalK (or equivalently K)";
   print_endline "                      MultiModalKD (or equivalently KD)";
   print_endline "                      Monotone";
@@ -154,6 +154,20 @@ let choicePrint () =
       done
     with End_of_file -> ()
 
+let choiceNom2fix () =
+	try
+		while true do
+			let input = read_line () in
+			if not (GenAndComp.isEmptyString input) then
+				let f = CoAlgFormula.importFormula input in
+				let str = CoAlgFormula.exportFormula f in
+				incr counter;
+				print_string("\nFormula " ^ (string_of_int !counter) ^ ": " ^ str ^ "\n");
+				flush stdout;
+			else ()
+		done
+	with End_of_file -> ()
+
 let choiceNNF () =
     try
       while true do
@@ -223,4 +237,5 @@ let _ =
     | "nnf" -> choiceNNF ()
     | "verify" -> choiceVerify ()
     | "graph" -> choiceGraph ()
+	| "nom2fix" -> choiceNom2fix()
     | _ -> printUsage ()