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