1(* ========================================================================= *)
2(* A HOL INTERFACE TO THE METIS FIRST-ORDER PROVER.                          *)
3(* Created by Joe Hurd, October 2001                                         *)
4(* ========================================================================= *)
5
6signature metisTools =
7sig
8
9(* "Metis" trace levels:
10   0: No output
11   1: The equivalent of Meson dots
12   2: Timing information
13   3: More detailed prover information: slice by slice
14   4: Log of each step in proof translation
15   5: Log of each inference during proof search *)
16
17type 'a stream = 'a mlibStream.stream
18type limit     = mlibMeter.limit
19type term      = Term.term
20type thm       = Thm.thm
21type tactic    = Abbrev.tactic
22type Query     = folTools.Query
23type Result    = folTools.Result
24
25(* Parameters *)
26type Fparm      = folTools.parameters
27type Mparm      = mlibMetis.parameters
28type parameters = {interface : Fparm, solver : Mparm, limit : limit}
29
30val defaults         : parameters
31val update_interface : (Fparm -> Fparm) -> parameters -> parameters
32val update_solver    : (Mparm -> Mparm) -> parameters -> parameters
33val update_limit     : (limit -> limit) -> parameters -> parameters
34
35(* Prolog solver *)
36val PROLOG_SOLVE : thm list -> Query -> Result stream
37
38(* Metis solver *)
39val GEN_METIS_SOLVE : parameters -> thm list -> Query -> Result stream
40
41(* Tactic interface to the metis prover *)
42val GEN_METIS_TAC : parameters -> thm list -> tactic
43
44(* All the following use this limit *)
45val limit : limit ref
46
47(* Canned parameters for common situations *)
48val FO_METIS_TAC   : thm list -> tactic         (* First-order *)
49val FOT_METIS_TAC  : thm list -> tactic         (* + types *)
50val HO_METIS_TAC   : thm list -> tactic         (* Higher-order *)
51val HOT_METIS_TAC  : thm list -> tactic         (* + types *)
52val FULL_METIS_TAC : thm list -> tactic         (* + combinators & booleans *)
53
54(* Simple user interface to the metis prover *)
55val FO_METIS_PROVE   : thm list -> term -> thm  (* First-order *)
56val FOT_METIS_PROVE  : thm list -> term -> thm  (* + types *)
57val HO_METIS_PROVE   : thm list -> term -> thm  (* Higher-order *)
58val HOT_METIS_PROVE  : thm list -> term -> thm  (* + types *)
59val FULL_METIS_PROVE : thm list -> term -> thm  (* + combinators & booleans *)
60
61(* Uses heuristics to apply one of {FO|FOT}, {HO|HOT} or FULL. *)
62val METIS_TAC   : thm list -> tactic
63val METIS_PROVE : thm list -> term -> thm
64
65end
66