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