| author | wenzelm |
| Sun, 14 Mar 2021 13:21:59 +0100 | |
| changeset 73430 | c7f14309e291 |
| parent 73424 | 2b657a70116c |
| child 73431 | f27d7b12e8a4 |
| 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.ML |
|
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 |
signature SYSTEM_ON_TPTP = |
|
7d7d959547a1
support for SystemOnTPTP in Isabelle/ML and Isabelle/Scala (without perl);
wenzelm
parents:
diff
changeset
|
8 |
sig |
|
7d7d959547a1
support for SystemOnTPTP in Isabelle/ML and Isabelle/Scala (without perl);
wenzelm
parents:
diff
changeset
|
9 |
val get_url: unit -> string |
|
73424
2b657a70116c
clarified signature: url may change dynamically and is part of result;
wenzelm
parents:
73419
diff
changeset
|
10 |
val list_systems: unit -> {url: string, systems: string list}
|
|
73418
7d7d959547a1
support for SystemOnTPTP in Isabelle/ML and Isabelle/Scala (without perl);
wenzelm
parents:
diff
changeset
|
11 |
end |
|
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 |
structure SystemOnTPTP: SYSTEM_ON_TPTP = |
|
7d7d959547a1
support for SystemOnTPTP in Isabelle/ML and Isabelle/Scala (without perl);
wenzelm
parents:
diff
changeset
|
14 |
struct |
|
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 |
fun get_url () = Options.default_string \<^system_option>\<open>SystemOnTPTP\<close> |
|
7d7d959547a1
support for SystemOnTPTP in Isabelle/ML and Isabelle/Scala (without perl);
wenzelm
parents:
diff
changeset
|
17 |
|
|
73424
2b657a70116c
clarified signature: url may change dynamically and is part of result;
wenzelm
parents:
73419
diff
changeset
|
18 |
fun list_systems () = |
|
2b657a70116c
clarified signature: url may change dynamically and is part of result;
wenzelm
parents:
73419
diff
changeset
|
19 |
let |
|
2b657a70116c
clarified signature: url may change dynamically and is part of result;
wenzelm
parents:
73419
diff
changeset
|
20 |
val url = get_url () |
| 73430 | 21 |
val systems = trim_split_lines (\<^scala>\<open>SystemOnTPTP.list_systems\<close> url) |
|
73424
2b657a70116c
clarified signature: url may change dynamically and is part of result;
wenzelm
parents:
73419
diff
changeset
|
22 |
in {url = url, systems = systems} end
|
|
73418
7d7d959547a1
support for SystemOnTPTP in Isabelle/ML and Isabelle/Scala (without perl);
wenzelm
parents:
diff
changeset
|
23 |
|
|
7d7d959547a1
support for SystemOnTPTP in Isabelle/ML and Isabelle/Scala (without perl);
wenzelm
parents:
diff
changeset
|
24 |
end |