| changeset 45449 | cfe7f4a68e51 |
| parent 45362 | e08158671ef4 |
| child 45450 | eeba1eedf32d |
| 45448:08ad27488983 | 45449:cfe7f4a68e51 |
|---|---|
53 -> (Proof.context -> int * format * string) -> string * atp_config |
53 -> (Proof.context -> int * format * string) -> string * atp_config |
54 val add_atp : string * atp_config -> theory -> theory |
54 val add_atp : string * atp_config -> theory -> theory |
55 val get_atp : theory -> string -> atp_config |
55 val get_atp : theory -> string -> atp_config |
56 val supported_atps : theory -> string list |
56 val supported_atps : theory -> string list |
57 val is_atp_installed : theory -> string -> bool |
57 val is_atp_installed : theory -> string -> bool |
58 val is_ho_atp: string -> bool |
|
58 val refresh_systems_on_tptp : unit -> unit |
59 val refresh_systems_on_tptp : unit -> unit |
59 val setup : theory -> theory |
60 val setup : theory -> theory |
60 end; |
61 end; |
61 |
62 |
62 structure ATP_Systems : ATP_SYSTEMS = |
63 structure ATP_Systems : ATP_SYSTEMS = |
497 fun is_atp_installed thy name = |
498 fun is_atp_installed thy name = |
498 let val {exec, required_execs, ...} = get_atp thy name in |
499 let val {exec, required_execs, ...} = get_atp thy name in |
499 forall (curry (op <>) "" o getenv o fst) (exec :: required_execs) |
500 forall (curry (op <>) "" o getenv o fst) (exec :: required_execs) |
500 end |
501 end |
501 |
502 |
503 fun is_ho_atp name = |
|
504 let |
|
505 val local_ho_atps = [leo2N, satallaxN] |
|
506 val ho_atps = map (fn n => remote_prefix ^ n) local_ho_atps |
|
507 in List.filter (fn n => n = name) ho_atps |
|
508 |> List.null |
|
509 |> not |
|
510 end |
|
511 |
|
502 fun refresh_systems_on_tptp () = |
512 fun refresh_systems_on_tptp () = |
503 Synchronized.change systems (fn _ => get_systems ()) |
513 Synchronized.change systems (fn _ => get_systems ()) |
504 |
514 |
505 val atps = |
515 val atps = |
506 [e, leo2, satallax, spass, vampire, z3_tptp, remote_e, remote_leo2, |
516 [e, leo2, satallax, spass, vampire, z3_tptp, remote_e, remote_leo2, |