Testsuite.ml

module CM = CoAlgMisc
module PF = Printf

module CR = CoAlgReasoner

(* sort should be of the form:
    sorts = [| (parseFunctor Sys.argv.(2), [0]) |]
*)

type testResult = | Sat
                  | Unsat
                  | ParseError

                (* sat * functors * formula *)
type satCheck = testResult * (CoAlgMisc.sortTable) * string



let colored_string_of_testResult tr =
    match tr with
    | Sat -> ("1;33","sat")
    | Unsat -> ("1;34","unsat")
    | ParseError -> ("31","unparseable")

let colored_string col str =
    "\027["^col^"m"^str^"\027[0m"

let terminal_string_of_testResult tr =
    let (col,str) = colored_string_of_testResult tr in
    colored_string col str

let runSatCheck (_,logic,input) =
  try
      let nomTable name =
        assert (CoAlgFormula.isNominal name);
        Some 0
      in
      let (tbox, f) = CoAlgFormula.importQuery input in
      let res = CoAlgReasoner.isSat logic nomTable tbox f in
      if res then Sat else Unsat
  with | Stream.Error _ -> ParseError
       | CoAlgFormula.CoAlgException _ -> ParseError

let stringCrop width str =
    if (String.length str <= width) then str
    else ((Str.string_before str (width-1)) ^ "…")

let columnCreate width str =
    let shorten = (stringCrop width str) in
    let pad = String.make (max 0 (width - (String.length shorten))) ' ' in
    (shorten ^ pad)

let runSatCheckVerbose (sc:satCheck) =
    let cs = colored_string in
    let sotr = terminal_string_of_testResult in
    let (expectation,_,title) = sc in
    PF.printf "Is %s " (cs "1" (columnCreate 60 title));
    PF.printf "%s? → " (sotr expectation);
    flush stdout;
    let res = runSatCheck sc in
    (if (res = expectation)
    then PF.printf "%s\n" (cs "1;32" "Yes")
    else PF.printf "%s, cool claims it is %s\n"
                    (cs "1;31" "No")
                    (sotr res));
    flush stdout;
    res