Add parameter for functor

coalg.ml

@@ -4,6 +4,7 @@
     @author Florian Widmann
  *)
 
+module CM = CoAlgMisc
 
 (* The type of formulae that are accepted. *)
 (*
@@ -18,11 +19,11 @@ let sorts = [| (CoAlgMisc.MultiModalKD, [0])
             (*;  (CoAlgMisc.MultiModalKD, [1])
             ;  (CoAlgMisc.Fusion, [1; 1]) *)
             |]
-*)
-let sorts = [| (CoAlgMisc.MultiModalK, [0])
+let sorts = [| (CM.MultiModalK, [0])
             (*;  (CoAlgMisc.MultiModalKD, [1])
             ;  (CoAlgMisc.Fusion, [1; 1]) *)
             |]
+*)
 
 (* A partial function mapping nominals to their sorts. *)
 let nomTable name =
@@ -36,14 +37,30 @@ let _ = Gc.set { (Gc.get()) with Gc.minor_heap_size = 4194304; major_heap_increm
 let printUsage () =
   print_endline "Usage: \"alc <task> <functor> [<verbose>]\" where";
   print_endline "       <task> in { sat print }";
-  print_endline "       <functor> in { MultiModalK MultiModalKD CoalitionLogic }";
+  print_endline "       <functor> in { MultiModalK MultiModalKD CoalitionLogic";
+  print_endline "                      (or: K)     (or: KD)     (or: CL)       }";
   print_endline "       <verbose> = any (second) argument";
+  print_endline "";
+  print_endline "Examples:";
+  print_endline "  OCAMLRUNPARAM=b ./coalg sat K <<< '[R] False'";
+  print_endline "  OCAMLRUNPARAM=b ./coalg sat KD <<< '[R] False'";
+  print_endline "The OCAMLRUNPARAM=b is optional. It will show a backtrace in case of a crash";
   exit 1
 
 let counter = ref 0
 
+let parseFunctor str =
+    match str with
+    | "K" -> CM.MultiModalK
+    | "KD" -> CM.MultiModalKD
+    | "MultiModalK" -> CM.MultiModalK
+    | "MultiModalKD" -> CM.MultiModalKD
+    | "CoalitionLogic" -> CM.CoalitionLogic
+    | _ -> raise (CoAlgFormula.CoAlgException ("Unknown Functor name »" ^ str ^ "«"))
+
 let choiceSat () =
-    let verb = Array.length Sys.argv > 2 in
+    let verb = Array.length Sys.argv > 3 in
+    let sorts = [| (parseFunctor Sys.argv.(2), [0]) |] in
     let printRes sat =
       if not verb then
         print_endline (if sat then "satisfiable\n" else "unsatisfiable\n")
@@ -62,7 +79,6 @@ let choiceSat () =
       done
     with End_of_file -> ()
 
-
 let choicePrint () =
     try
       while true do
@@ -78,8 +94,8 @@ let choicePrint () =
     with End_of_file -> ()
 
 
-let _ = 
-  if Array.length Sys.argv < 2 then printUsage()
+let _ =
+  if Array.length Sys.argv < 3 then printUsage()
   else
     let choice = Sys.argv.(1) in
     match choice with