From 4fd82fa112aefba40ab6eeed61b67810dc934ee1 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Thorsten=20Wi=C3=9Fmann?= <uni@thorsten-wissmann.de>
Date: Thu, 9 Jan 2014 13:04:44 +0100
Subject: [PATCH] Add parameter for functor
---
coalg.ml | 30 +++++++++++++++++++++++-------
1 file changed, 23 insertions(+), 7 deletions(-)
diff --git a/coalg.ml b/coalg.ml
index 5bad759..829cb8b 100644
--- a/coalg.ml
+++ b/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
--
GitLab