--- a/src/HOL/Tools/numeral.ML Wed Oct 22 14:15:44 2008 +0200
+++ b/src/HOL/Tools/numeral.ML Wed Oct 22 14:15:45 2008 +0200
@@ -59,25 +59,28 @@
fun add_code number_of negative unbounded target thy =
let
- val pls' = Code_Name.const thy @{const_name Int.Pls};
- val min' = Code_Name.const thy @{const_name Int.Min};
- val bit0' = Code_Name.const thy @{const_name Int.Bit0};
- val bit1' = Code_Name.const thy @{const_name Int.Bit1};
val pr_numeral = (Code_Printer.literal_numeral o Code_Target.the_literals thy) target;
- fun dest_bit thm (IConst (c, _)) = if c = bit0' then 0
- else if c = bit1' then 1
- else Code_Printer.nerror thm "Illegal numeral expression: illegal bit"
- | dest_bit thm _ = Code_Printer.nerror thm "Illegal numeral expression: illegal bit";
- fun dest_numeral thm (IConst (c, _)) = if c = pls' then SOME 0
- else if c = min' then
- if negative then SOME ~1 else NONE
- else Code_Printer.nerror thm "Illegal numeral expression: illegal leading digit"
- | dest_numeral thm (t1 `$ t2) =
- let val (n, b) = (dest_numeral thm t2, dest_bit thm t1)
- in case n of SOME n => SOME (2 * n + b) | NONE => NONE end
- | dest_numeral thm _ = Code_Printer.nerror thm "Illegal numeral expression: illegal term";
- fun pretty _ thm _ _ _ [(t, _)] =
- (Code_Printer.str o pr_numeral unbounded o the_default 0 o dest_numeral thm) t;
+ fun dest_numeral naming thm =
+ let
+ val SOME pls' = Code_Thingol.lookup_const naming @{const_name Int.Pls};
+ val SOME min' = Code_Thingol.lookup_const naming @{const_name Int.Min};
+ val SOME bit0' = Code_Thingol.lookup_const naming @{const_name Int.Bit0};
+ val SOME bit1' = Code_Thingol.lookup_const naming @{const_name Int.Bit1};
+ fun dest_bit (IConst (c, _)) = if c = bit0' then 0
+ else if c = bit1' then 1
+ else Code_Printer.nerror thm "Illegal numeral expression: illegal bit"
+ | dest_bit _ = Code_Printer.nerror thm "Illegal numeral expression: illegal bit";
+ fun dest_num (IConst (c, _)) = if c = pls' then SOME 0
+ else if c = min' then
+ if negative then SOME ~1 else NONE
+ else Code_Printer.nerror thm "Illegal numeral expression: illegal leading digit"
+ | dest_num (t1 `$ t2) =
+ let val (n, b) = (dest_num t2, dest_bit t1)
+ in case n of SOME n => SOME (2 * n + b) | NONE => NONE end
+ | dest_num _ = Code_Printer.nerror thm "Illegal numeral expression: illegal term";
+ in dest_num end;
+ fun pretty _ naming thm _ _ _ [(t, _)] =
+ (Code_Printer.str o pr_numeral unbounded o the_default 0 o dest_numeral naming thm) t;
in
thy
|> Code_Target.add_syntax_const target number_of (SOME (1, pretty))