author | wenzelm |
Fri, 12 Mar 2021 23:30:35 +0100 | |
changeset 73418 | 7d7d959547a1 |
child 73419 | 22f3f2117ed7 |
permissions | -rw-r--r-- |
73418
7d7d959547a1
support for SystemOnTPTP in Isabelle/ML and Isabelle/Scala (without perl);
wenzelm
parents:
diff
changeset
|
1 |
/* Title: HOL/Tools/ATP/system_on_tptp.scala |
7d7d959547a1
support for SystemOnTPTP in Isabelle/ML and Isabelle/Scala (without perl);
wenzelm
parents:
diff
changeset
|
2 |
Author: Makarius |
7d7d959547a1
support for SystemOnTPTP in Isabelle/ML and Isabelle/Scala (without perl);
wenzelm
parents:
diff
changeset
|
3 |
|
7d7d959547a1
support for SystemOnTPTP in Isabelle/ML and Isabelle/Scala (without perl);
wenzelm
parents:
diff
changeset
|
4 |
Support for remote ATPs via SystemOnTPTP. |
7d7d959547a1
support for SystemOnTPTP in Isabelle/ML and Isabelle/Scala (without perl);
wenzelm
parents:
diff
changeset
|
5 |
*/ |
7d7d959547a1
support for SystemOnTPTP in Isabelle/ML and Isabelle/Scala (without perl);
wenzelm
parents:
diff
changeset
|
6 |
|
7d7d959547a1
support for SystemOnTPTP in Isabelle/ML and Isabelle/Scala (without perl);
wenzelm
parents:
diff
changeset
|
7 |
package isabelle.atp |
7d7d959547a1
support for SystemOnTPTP in Isabelle/ML and Isabelle/Scala (without perl);
wenzelm
parents:
diff
changeset
|
8 |
|
7d7d959547a1
support for SystemOnTPTP in Isabelle/ML and Isabelle/Scala (without perl);
wenzelm
parents:
diff
changeset
|
9 |
import isabelle._ |
7d7d959547a1
support for SystemOnTPTP in Isabelle/ML and Isabelle/Scala (without perl);
wenzelm
parents:
diff
changeset
|
10 |
|
7d7d959547a1
support for SystemOnTPTP in Isabelle/ML and Isabelle/Scala (without perl);
wenzelm
parents:
diff
changeset
|
11 |
import java.net.URL |
7d7d959547a1
support for SystemOnTPTP in Isabelle/ML and Isabelle/Scala (without perl);
wenzelm
parents:
diff
changeset
|
12 |
|
7d7d959547a1
support for SystemOnTPTP in Isabelle/ML and Isabelle/Scala (without perl);
wenzelm
parents:
diff
changeset
|
13 |
|
7d7d959547a1
support for SystemOnTPTP in Isabelle/ML and Isabelle/Scala (without perl);
wenzelm
parents:
diff
changeset
|
14 |
object SystemOnTPTP |
7d7d959547a1
support for SystemOnTPTP in Isabelle/ML and Isabelle/Scala (without perl);
wenzelm
parents:
diff
changeset
|
15 |
{ |
7d7d959547a1
support for SystemOnTPTP in Isabelle/ML and Isabelle/Scala (without perl);
wenzelm
parents:
diff
changeset
|
16 |
def get_url(options: Options): URL = Url(options.string("SystemOnTPTP")) |
7d7d959547a1
support for SystemOnTPTP in Isabelle/ML and Isabelle/Scala (without perl);
wenzelm
parents:
diff
changeset
|
17 |
|
7d7d959547a1
support for SystemOnTPTP in Isabelle/ML and Isabelle/Scala (without perl);
wenzelm
parents:
diff
changeset
|
18 |
def proper_lines(text: String): List[String] = |
7d7d959547a1
support for SystemOnTPTP in Isabelle/ML and Isabelle/Scala (without perl);
wenzelm
parents:
diff
changeset
|
19 |
Library.trim_split_lines(text).filterNot(_.startsWith("%")) |
7d7d959547a1
support for SystemOnTPTP in Isabelle/ML and Isabelle/Scala (without perl);
wenzelm
parents:
diff
changeset
|
20 |
|
7d7d959547a1
support for SystemOnTPTP in Isabelle/ML and Isabelle/Scala (without perl);
wenzelm
parents:
diff
changeset
|
21 |
def list_systems(url: URL): List[String] = |
7d7d959547a1
support for SystemOnTPTP in Isabelle/ML and Isabelle/Scala (without perl);
wenzelm
parents:
diff
changeset
|
22 |
{ |
7d7d959547a1
support for SystemOnTPTP in Isabelle/ML and Isabelle/Scala (without perl);
wenzelm
parents:
diff
changeset
|
23 |
val result = |
7d7d959547a1
support for SystemOnTPTP in Isabelle/ML and Isabelle/Scala (without perl);
wenzelm
parents:
diff
changeset
|
24 |
HTTP.Client.post(url, user_agent = "Sledgehammer", parameters = |
7d7d959547a1
support for SystemOnTPTP in Isabelle/ML and Isabelle/Scala (without perl);
wenzelm
parents:
diff
changeset
|
25 |
List("NoHTML" -> 1, |
7d7d959547a1
support for SystemOnTPTP in Isabelle/ML and Isabelle/Scala (without perl);
wenzelm
parents:
diff
changeset
|
26 |
"QuietFlag" -> "-q0", |
7d7d959547a1
support for SystemOnTPTP in Isabelle/ML and Isabelle/Scala (without perl);
wenzelm
parents:
diff
changeset
|
27 |
"SubmitButton" -> "ListSystems", |
7d7d959547a1
support for SystemOnTPTP in Isabelle/ML and Isabelle/Scala (without perl);
wenzelm
parents:
diff
changeset
|
28 |
"ListStatus" -> "READY")) |
7d7d959547a1
support for SystemOnTPTP in Isabelle/ML and Isabelle/Scala (without perl);
wenzelm
parents:
diff
changeset
|
29 |
proper_lines(result.text) |
7d7d959547a1
support for SystemOnTPTP in Isabelle/ML and Isabelle/Scala (without perl);
wenzelm
parents:
diff
changeset
|
30 |
} |
7d7d959547a1
support for SystemOnTPTP in Isabelle/ML and Isabelle/Scala (without perl);
wenzelm
parents:
diff
changeset
|
31 |
|
7d7d959547a1
support for SystemOnTPTP in Isabelle/ML and Isabelle/Scala (without perl);
wenzelm
parents:
diff
changeset
|
32 |
object List_Systems extends Scala.Fun("SystemOnTPTP.list_systems") |
7d7d959547a1
support for SystemOnTPTP in Isabelle/ML and Isabelle/Scala (without perl);
wenzelm
parents:
diff
changeset
|
33 |
{ |
7d7d959547a1
support for SystemOnTPTP in Isabelle/ML and Isabelle/Scala (without perl);
wenzelm
parents:
diff
changeset
|
34 |
val here = Scala_Project.here |
7d7d959547a1
support for SystemOnTPTP in Isabelle/ML and Isabelle/Scala (without perl);
wenzelm
parents:
diff
changeset
|
35 |
def apply(url: String): String = cat_lines(list_systems(Url(url))) |
7d7d959547a1
support for SystemOnTPTP in Isabelle/ML and Isabelle/Scala (without perl);
wenzelm
parents:
diff
changeset
|
36 |
} |
7d7d959547a1
support for SystemOnTPTP in Isabelle/ML and Isabelle/Scala (without perl);
wenzelm
parents:
diff
changeset
|
37 |
} |