--- a/src/HOL/Tools/Nitpick/kodkod.scala Tue Aug 18 18:23:17 2020 +0200
+++ b/src/HOL/Tools/Nitpick/kodkod.scala Wed Aug 19 13:29:53 2020 +0200
@@ -8,8 +8,10 @@
import isabelle._
+import java.util.concurrent.Executors
+
import org.antlr.runtime.{ANTLRInputStream, Lexer, RecognitionException}
-import de.tum.in.isabelle.Kodkodi.{KodkodiLexer, KodkodiParser}
+import de.tum.in.isabelle.Kodkodi.{Context, KodkodiLexer, KodkodiParser}
object Kodkod
@@ -19,17 +21,40 @@
prove: Boolean = false,
max_solutions: Int = Integer.MAX_VALUE,
cleanup_inst: Boolean = false,
- time_limit: Time = Time.zero,
max_threads: Int = 1): String =
{
- val in = Bytes(source).stream
- val stream = new ANTLRInputStream(in)
- val lexer = new KodkodiLexer(stream)
-
+ val context =
+ new Context {
+ private val out = new StringBuilder
+ private val err = new StringBuilder
+ def result: (String, String) = synchronized { (out.toString, err.toString) }
+ override def output(s: String): Unit = synchronized { out ++= s; out += '\n' }
+ override def error(s: String): Unit = synchronized { err ++= s; err += '\n' }
+ override def exit(rc: Int) { if (rc == 0) () else error("exit " + rc) }
+ }
+ val executor = Executors.newFixedThreadPool(max_threads)
+ val lexer = new KodkodiLexer(new ANTLRInputStream(Bytes(source).stream))
val parser =
- KodkodiParser.create(true, false, solve_all, prove, max_solutions,
- cleanup_inst, max_threads, lexer)
+ KodkodiParser.create(context, executor,
+ false, solve_all, prove, max_solutions, cleanup_inst, lexer)
- "FIXME"
+ val solution =
+ try { parser.problems() }
+ catch {
+ case exn: RecognitionException =>
+ parser.reportError(exn)
+ error("Parser error")
+ }
+ if (parser.getTokenStream.LA(1) != KodkodiParser.EOF) {
+ error("Trailing tokens")
+ }
+ if (lexer.getNumberOfSyntaxErrors > 0) error("Lexical error")
+ if (parser.getNumberOfSyntaxErrors > 0) error("Syntax error")
+
+ val (out, err) = context.result
+ Output.writeln(out)
+ Output.warning(err)
+
+ solution
}
}