1structure simpfrag :> simpfrag =
2struct
3
4open Abbrev
5
6type convdata = { name: string,
7                  key: (term list * term) option,
8                  trace: int,
9                  conv: (term list -> term -> thm) -> term list -> conv}
10
11type simpfrag = { convs: convdata list, rewrs: thm list}
12
13val empty_simpfrag = {convs = [], rewrs = []};
14
15fun add_rwts {convs, rewrs} newrwts = {convs = convs, rewrs = rewrs @ newrwts};
16
17fun add_convs cds {convs, rewrs} = {convs = convs@cds, rewrs = rewrs}
18
19val sconv_db = ref (Binarymap.mkDict String.compare : (string,thm -> convdata) Binarymap.dict)
20
21fun register_simpfrag_conv {name,code} =
22  sconv_db := Binarymap.insert(!sconv_db, name, code)
23
24fun lookup_simpfrag_conv k = Binarymap.peek(!sconv_db, k)
25
26val simpfrag_conv_tag = "ssfrag_CONV"
27
28end;
29