1(* ========================================================================= *)
2(* A STORE FOR UNIT THEOREMS                                                 *)
3(* Copyright (c) 2001 Joe Hurd, distributed under the BSD License            *)
4(* ========================================================================= *)
5
6signature Units =
7sig
8
9(* ------------------------------------------------------------------------- *)
10(* A type of unit store.                                                     *)
11(* ------------------------------------------------------------------------- *)
12
13type unitThm = Literal.literal * Thm.thm
14
15type units
16
17(* ------------------------------------------------------------------------- *)
18(* Basic operations.                                                         *)
19(* ------------------------------------------------------------------------- *)
20
21val empty : units
22
23val size : units -> int
24
25val toString : units -> string
26
27val pp : units Print.pp
28
29(* ------------------------------------------------------------------------- *)
30(* Add units into the store.                                                 *)
31(* ------------------------------------------------------------------------- *)
32
33val add : units -> unitThm -> units
34
35val addList : units -> unitThm list -> units
36
37(* ------------------------------------------------------------------------- *)
38(* Matching.                                                                 *)
39(* ------------------------------------------------------------------------- *)
40
41val match : units -> Literal.literal -> (unitThm * Subst.subst) option
42
43(* ------------------------------------------------------------------------- *)
44(* Reducing by repeated matching and resolution.                             *)
45(* ------------------------------------------------------------------------- *)
46
47val reduce : units -> Rule.rule
48
49end
50