diff --git a/src/coalg/coalg.ml b/src/coalg/coalg.ml
index d0f2e010282ea3207324eac1bd422755d05a1477..b1795e25581870280f46dadbbe680aec2af2ce0f 100644
--- a/src/coalg/coalg.ml
+++ b/src/coalg/coalg.ml
@@ -12,25 +12,6 @@ module FE = FunctorParsing
open CoolUtils
-(* The type of formulae that are accepted. *)
-(*
-let sorts = Array.make 1 (CoAlgMisc.MultiModalK, [0])
-*)
-(*
-let sorts = Array.make 3 (CoAlgMisc.MultiModalK, [0])
-let _ = sorts.(0) <- (CoAlgMisc.Choice, [1; 2])
-*)
-(*
-let sorts = [| (CoAlgMisc.MultiModalKD, [0])
- (*; (CoAlgMisc.MultiModalKD, [1])
- ; (CoAlgMisc.Fusion, [1; 1]) *)
- |]
-let sorts = [| (CM.MultiModalK, [0])
- (*; (CoAlgMisc.MultiModalKD, [1])
- ; (CoAlgMisc.Fusion, [1; 1]) *)
- |]
-*)
-
(* A partial function mapping nominals to their sorts. *)
let nomTable name =
assert (CoAlgFormula.isNominal name);
@@ -39,11 +20,31 @@ let nomTable name =
let _ = Gc.set { (Gc.get()) with Gc.minor_heap_size = 4194304; major_heap_increment = 67108864; space_overhead = 120 }
-(*
-let _ =
- let str = "A . B C" in
- print_endline (FE.stringFromFunctorExp (FE.functorExpFromString str))
-*)
+type options =
+ { verbose : bool
+ }
+
+let defaultOpts = { verbose = false }
+
+let options =
+ [ { Args.long = "verbose"
+ ; Args.short = Some 'v'
+ ; Args.description = "print verbose output with statistics"
+ ; Args.argument = Args.No_arg (fun a -> { verbose = true })
+ }
+ ; { Args.long = "agents"
+ ; Args.short = None
+ ; Args.description = "expects the next argument AGLIST to be a list of integers\n"
+ ^ "which is treaten as the set of agents for CL formulas\n"
+ ^ "it defaults to 1,2,3,4,5,6,7,8,9,10"
+ ; Args.argument =
+ let parse_agents strAglist =
+ let aglist = List.map int_of_string (Str.split (Str.regexp ",") strAglist) in
+ CoolUtils.cl_set_agents (Array.of_list aglist)
+ in
+ Args.Required_arg ("AGLIST", fun s a -> parse_agents s; a)
+ }
+ ]
let printUsage name =
print_endline ("Usage: \"" ^ name ^ " <task> <functor> [<flags>]\" where");
@@ -61,12 +62,7 @@ let printUsage name =
print_endline " or <functor> . <functor> (binds strongest)";
print_endline " (so K+KD.CL*Id stand for (K + ((KD.CL) * Id)))";
print_endline " <flags> = a list of the following items";
- print_endline " --agents AGLIST";
- print_endline " expects the next argument AGLIST to be a list of integers";
- print_endline " which is treaten as the set of agents for CL formulas";
- print_endline " it defaults to 1,2,3,4,5,6,7,8,9,10";
- print_endline " --verbose";
- print_endline " print verbose output for sat task";
+ Args.help stdout 11 options;
print_endline "";
print_endline "Problems are read from standard input and have the form";
print_endline " [ ass_1; .. ; ass_n |- ] concept";
@@ -90,10 +86,9 @@ let printUsage name =
exit 1
let counter = ref 0
-let verbose = ref false
-let choiceSat () =
- let verb = !verbose in
+let choiceSat opts =
+ let verb = opts.verbose in
let sorts = (FE.sortTableFromString Sys.argv.(2)) in
(* test if GML or PML occurs in sort table *)
@@ -119,8 +114,8 @@ let choiceSat () =
done
with End_of_file -> ()
-let choiceProvable () =
- let verb = !verbose in
+let choiceProvable opts =
+ let verb = opts.verbose in
let sorted_not ((s,f):CF.sortedFormula) : CF.sortedFormula =
(s,CF.NOT f)
in
@@ -144,7 +139,7 @@ let choiceProvable () =
done
with End_of_file -> ()
-let choicePrint () =
+let choicePrint opts =
try
while true do
let input = read_line () in
@@ -158,7 +153,7 @@ let choicePrint () =
done
with End_of_file -> ()
-let choiceNom2fix () =
+let choiceNom2fix opts =
try
while true do
let input = read_line () in
@@ -173,7 +168,7 @@ let choiceNom2fix () =
done
with End_of_file -> ()
-let choiceNNF () =
+let choiceNNF opts =
try
while true do
let input = read_line () in
@@ -187,7 +182,7 @@ let choiceNNF () =
done
with End_of_file -> ()
-let choiceGraph () =
+let choiceGraph opts =
let sorts = (FE.sortTableFromString Sys.argv.(2)) in
let input = read_line () in
@@ -195,7 +190,7 @@ let choiceGraph () =
ignore(CoAlgReasoner.isSat sorts nomTable tbox f);
print_endline (CM.graphToDot ())
-let choiceVerify () =
+let choiceVerify opts =
try
while true do
print_string "> ";
@@ -212,40 +207,21 @@ let choiceVerify () =
done
with End_of_file -> ()
-let rec parseFlags arr offs : unit =
- let offs = ref (offs) in
- let getParam () =
- if ((!offs + 1) >= Array.length arr) then
- raise (CoAlgFormula.CoAlgException ("Parameter missing for flag »" ^ (arr.(!offs)) ^ "«"))
- else
- offs := !offs + 1;
- arr.(!offs)
- in
- if (!offs >= Array.length arr) then ()
- else (ignore (match arr.(!offs) with
- | "--verbose" -> verbose := true
- | "--agents" ->
- let strAglist = getParam () in
- let aglist = List.map int_of_string (Str.split (Str.regexp ",") strAglist) in
- CoolUtils.cl_set_agents (Array.of_list aglist)
- | _ ->
- raise (CoAlgFormula.CoAlgException ("Unknown flag »" ^ (arr.(!offs)) ^ "«"))
- ) ; parseFlags arr (!offs + 1)
- )
-
let _ =
if Array.length Sys.argv < 3 then printUsage (Sys.argv.(0))
else
let choice = Sys.argv.(1) in
- parseFlags Sys.argv 3;
- match choice with
- | "sat" -> choiceSat ()
- | "prov" -> choiceProvable ()
- | "print" -> choicePrint ()
- | "nnf" -> choiceNNF ()
- | "verify" -> choiceVerify ()
- | "graph" -> choiceGraph ()
- | "nom2fix" -> choiceNom2fix()
- | _ -> printUsage (Sys.argv.(0))
+ match Args.parse Sys.argv 3 options defaultOpts with
+ | Args.Error e -> Printf.printf "%s\n\n" e; printUsage (Sys.argv.(0))
+ | Args.Ok opts ->
+ match choice with
+ | "sat" -> choiceSat opts
+ | "prov" -> choiceProvable opts
+ | "print" -> choicePrint opts
+ | "nnf" -> choiceNNF opts
+ | "verify" -> choiceVerify opts
+ | "graph" -> choiceGraph opts
+ | "nom2fix" -> choiceNom2fix opts
+ | _ -> printUsage (Sys.argv.(0))
(* vim: set et sw=2 sts=2 ts=8 : *)
diff --git a/src/lib/CoolUtils.ml b/src/lib/CoolUtils.ml
index 92c6481c0cbe922c1e7beadaf616e59fa85c1cbc..ef61ee63a037780cd295ac16f678aa4d38b3f23c 100644
--- a/src/lib/CoolUtils.ml
+++ b/src/lib/CoolUtils.ml
@@ -43,6 +43,81 @@ module TList = struct
List.fold_left (fun acc x -> acc @ List.map (fun lst -> x::lst) tail) [] l
end
+module Args = struct
+ type 'a param_parser = 'a -> 'a
+ type 'a argument = Required_arg of string * (string -> 'a param_parser)
+ | No_arg of 'a param_parser
+
+ type 'a description =
+ { long : string
+ ; short : char option
+ ; description : string
+ ; argument : 'a argument
+ }
+
+ exception ParseError of string
+
+ let find str mapping =
+ try (List.find (fun arg -> arg.long = str) mapping)
+ with
+ Not_found -> raise (ParseError (Printf.sprintf "Unknown option %s" str))
+
+ let findShort char mapping =
+ try (List.find (fun arg -> arg.short = Some char) mapping)
+ with
+ Not_found -> raise (ParseError (Printf.sprintf "Unknown option %c" char))
+
+ type 'a result = Ok of 'a | Error of string
+
+ let parse ~argv ~offset ~options ~default =
+ let rec parseImpl offs args =
+ let offs = ref (offs) in
+ let getParam () =
+ if ((!offs + 1) >= Array.length argv) then
+ raise (ParseError (Printf.sprintf "Parameter missing for flag »%s«" argv.(!offs)))
+ else
+ offs := !offs + 1;
+ argv.(!offs)
+ in
+ if (!offs >= Array.length argv) then args
+ else
+ let arg = argv.(!offs) in
+ let arg_desc = if String.length arg > 2 && String.sub arg 0 2 = "--" then
+ find (String.sub arg 2 (String.length arg - 2)) options
+ else if String.length arg > 1 && String.get arg 0 = '-' then
+ findShort (String.get arg 1) options
+ else
+ raise (ParseError (Printf.sprintf "Unknown argument %s" arg))
+ in
+ let args = match arg_desc.argument with
+ | Required_arg (_,p) -> p (getParam ()) args
+ | No_arg p -> p args
+ in
+ parseImpl (!offs+1) args
+
+ in
+ try Ok (parseImpl offset default)
+ with ParseError e -> Error e
+
+ let help channel offset mapping =
+ let padding offset = String.make offset ' ' in
+ let help_option desc =
+ let long = "--" ^ desc.long in
+ let short = match desc.short with
+ | Some x -> ",-" ^ Char.escaped x
+ | None -> ""
+ in
+ let var = match desc.argument with
+ | No_arg _ -> ""
+ | Required_arg (a,_) -> " " ^ a
+ in
+ Printf.fprintf channel "%s%s%s%s\n" (padding offset) long short var;
+ (* TODO split_on_char is not available in ocaml < 4.04 *)
+ List.iter (Printf.fprintf channel "%s%s\n" (padding (offset+2))) (String.split_on_char '\n' desc.description)
+ in
+ List.iter help_option mapping
+end
+
let agents = ref ([|1;2;3;4;5|])
let cl_get_agents () = !agents
diff --git a/src/lib/CoolUtils.mli b/src/lib/CoolUtils.mli
index 191eed60dceed1f9e07d0b2529ebe7ec2caeca2b..f045e062ac79fdd744ac585052e1be642571a45f 100644
--- a/src/lib/CoolUtils.mli
+++ b/src/lib/CoolUtils.mli
@@ -25,6 +25,44 @@ module TList : sig
val combinations : 'a list list -> 'a list list
end
+(* TODO Document, test *)
+(** Command line argument parser *)
+module Args : sig
+ type 'a param_parser = 'a -> 'a
+
+ (** Specifies whether the option takes an addition paramter. *)
+ type 'a argument = Required_arg of string * (string -> 'a param_parser)
+ (** name of the argument and parser. *)
+ | No_arg of 'a param_parser
+
+ type 'a description =
+ { long : string
+ ; short : char option
+ ; description : string
+ ; argument : 'a argument
+ }
+
+ type 'a result = Ok of 'a | Error of string
+
+ (** parses command line options.
+
+ The user can choose the type 'a, provided they provide parsers and a
+ default value.
+
+ @param argv The Sys.argv array
+ @param offset The index in [argv] where option parsing should start
+ @param options Descriptions of all available options
+ @param default Default value for the option type
+ @return The option type or a parse error
+ *)
+ val parse : argv:string array -> offset:int -> options:'a description list
+ -> default:'a -> 'a result
+
+ (** [help out indent options] prints help for [options] to [out] indented
+ by [indent] characters *)
+ val help : out_channel -> int -> 'a description list -> unit
+end
+
val cl_get_agents : unit -> int array
val cl_set_agents : int array -> unit