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