diff --git a/_oasis b/_oasis index 5a0e67fd0a8643da0c8f46b942e7001eceb5c4fb..370e66c45acf0ef98a157fa5da0ed41ff31d96ac 100644 --- a/_oasis +++ b/_oasis @@ -110,6 +110,17 @@ Executable coalgcompare if flag(static) CCLib: -static +Executable testsuite + CompiledObject: native + Path: src/testsuite/ + BuildTools: ocamlbuild + MainIs: cool-testsuite.ml + BuildDepends: libcool + NativeOpt: -cc g++ + ByteOpt: -cc g++ + CCOpt: -std=c++98 -x c++ + if flag(static) + CCLib: -static # some cabal similar syntax, so steal its syntax highlighting diff --git a/src/testsuite/Testsuite.ml b/src/testsuite/Testsuite.ml new file mode 100644 index 0000000000000000000000000000000000000000..22359e21668e0add4e22eaab24304db3df6656da --- /dev/null +++ b/src/testsuite/Testsuite.ml @@ -0,0 +1,16 @@ + + +module CM = CoAlgMisc + +module CR = CoAlgReasoner + +(* sort should be of the form: + sorts = [| (parseFunctor Sys.argv.(2), [0]) |] +*) + +type satCheck = bool * (CoAlgMisc.sortTable) * string (* sat * functors * formula *) + +type testResult = | Correct | WrongAnswer | ParseError + +let runSatCheck sc = + WrongAnswer diff --git a/src/testsuite/Testsuite.mli b/src/testsuite/Testsuite.mli new file mode 100644 index 0000000000000000000000000000000000000000..ae17962fa249b04e1a24ded16fcf777714bbc9c3 --- /dev/null +++ b/src/testsuite/Testsuite.mli @@ -0,0 +1,12 @@ + + +(* sort should be of the form: + sorts = [| (parseFunctor Sys.argv.(2), [0]) |] +*) + +type satCheck = bool * (CoAlgMisc.sortTable) * string (* sat * functors * formula *) + +type testResult = | Correct | WrongAnswer | ParseError + +val runSatCheck : satCheck -> testResult + diff --git a/src/testsuite/cool-testsuite.ml b/src/testsuite/cool-testsuite.ml new file mode 100644 index 0000000000000000000000000000000000000000..ab625be75d071a6a4e74f34183d3aeaed6460fd6 --- /dev/null +++ b/src/testsuite/cool-testsuite.ml @@ -0,0 +1,18 @@ +open CoolUtils +open Testsuite +module CF = CoAlgFormula +module CR = CoAlgReasoner +module CM = CoAlgMisc +module L = List + +let k = [| (CM.MultiModalK, [0]) |] +let kd = [| (CM.MultiModalKD, [0]) |] +let cl = [| (CM.CoalitionLogic, [0]) |] +let gml = [| (CM.GML, [0]) |] + +let main = + print_endline "todo" + + +let _ = main +