1structure ASCIInumbersLib :> ASCIInumbersLib = 2struct 3 4open HolKernel Parse boolLib computeLib; 5open numposrepLib ASCIInumbersTheory 6 7structure Parse = struct 8 open Parse 9 val (Type, Term) = 10 parse_from_grammars ASCIInumbersTheory.ASCIInumbers_grammars 11end 12open Parse 13 14(* ------------------------------------------------------------------------- *) 15 16local 17 val thms = 18 [s2n_def, n2s_def, HEX_def, UNHEX_def, 19 num_from_bin_string_def, num_from_oct_string_def, 20 num_from_dec_string_def, num_from_hex_string_def, 21 num_to_bin_string_def, num_to_oct_string_def, 22 num_to_dec_string_def, num_to_hex_string_def, 23 fromBinString_def, fromDecString_def, fromHexString_def] 24in 25 fun add_ASCIInumbers_compset cmp = computeLib.add_thms thms cmp 26end 27 28val () = add_ASCIInumbers_compset computeLib.the_compset 29 30(* ------------------------------------------------------------------------- *) 31 32(* Testing... 33 34open ASCIInumbersLib 35 36val tst = Count.apply EVAL 37 38tst ``s2n 3 UNHEX "12110"``; 39tst ``n2s 3 HEX 21328``; 40tst ``num_from_bin_string "10111"``; 41tst ``num_from_oct_string "72140"``; 42tst ``num_from_dec_string "72149"``; 43tst ``num_from_hex_string "abaaf"``; 44tst ``num_to_bin_string 0b110111``; 45tst ``num_to_oct_string 123``; 46tst ``num_to_dec_string 23768``; 47tst ``num_to_hex_string 0xAAFF11``; 48 49*) 50 51end 52