src/HOL/Tools/numeral.ML
changeset 28663 bd8438543bf2
parent 28308 d4396a28fb29
child 28708 a1a436f09ec6
equal deleted inserted replaced
28662:64ab5bb68d4c 28663:bd8438543bf2
    57 
    57 
    58 local open Basic_Code_Thingol in
    58 local open Basic_Code_Thingol in
    59 
    59 
    60 fun add_code number_of negative unbounded target thy =
    60 fun add_code number_of negative unbounded target thy =
    61   let
    61   let
    62     val pls' = Code_Name.const thy @{const_name Int.Pls};
       
    63     val min' = Code_Name.const thy @{const_name Int.Min};
       
    64     val bit0' = Code_Name.const thy @{const_name Int.Bit0};
       
    65     val bit1' = Code_Name.const thy @{const_name Int.Bit1};
       
    66     val pr_numeral = (Code_Printer.literal_numeral o Code_Target.the_literals thy) target;
    62     val pr_numeral = (Code_Printer.literal_numeral o Code_Target.the_literals thy) target;
    67     fun dest_bit thm (IConst (c, _)) = if c = bit0' then 0
    63     fun dest_numeral naming thm =
    68           else if c = bit1' then 1
    64       let
    69           else Code_Printer.nerror thm "Illegal numeral expression: illegal bit"
    65         val SOME pls' = Code_Thingol.lookup_const naming @{const_name Int.Pls};
    70       | dest_bit thm _ = Code_Printer.nerror thm "Illegal numeral expression: illegal bit";
    66         val SOME min' = Code_Thingol.lookup_const naming @{const_name Int.Min};
    71     fun dest_numeral thm (IConst (c, _)) = if c = pls' then SOME 0
    67         val SOME bit0' = Code_Thingol.lookup_const naming @{const_name Int.Bit0};
    72           else if c = min' then
    68         val SOME bit1' = Code_Thingol.lookup_const naming @{const_name Int.Bit1};
    73             if negative then SOME ~1 else NONE
    69         fun dest_bit (IConst (c, _)) = if c = bit0' then 0
    74           else Code_Printer.nerror thm "Illegal numeral expression: illegal leading digit"
    70               else if c = bit1' then 1
    75       | dest_numeral thm (t1 `$ t2) =
    71               else Code_Printer.nerror thm "Illegal numeral expression: illegal bit"
    76           let val (n, b) = (dest_numeral thm t2, dest_bit thm t1)
    72           | dest_bit _ = Code_Printer.nerror thm "Illegal numeral expression: illegal bit";
    77           in case n of SOME n => SOME (2 * n + b) | NONE => NONE end
    73         fun dest_num (IConst (c, _)) = if c = pls' then SOME 0
    78       | dest_numeral thm _ = Code_Printer.nerror thm "Illegal numeral expression: illegal term";
    74               else if c = min' then
    79     fun pretty _ thm _ _ _ [(t, _)] =
    75                 if negative then SOME ~1 else NONE
    80       (Code_Printer.str o pr_numeral unbounded o the_default 0 o dest_numeral thm) t;
    76               else Code_Printer.nerror thm "Illegal numeral expression: illegal leading digit"
       
    77           | dest_num (t1 `$ t2) =
       
    78               let val (n, b) = (dest_num t2, dest_bit t1)
       
    79               in case n of SOME n => SOME (2 * n + b) | NONE => NONE end
       
    80           | dest_num _ = Code_Printer.nerror thm "Illegal numeral expression: illegal term";
       
    81       in dest_num end;
       
    82     fun pretty _ naming thm _ _ _ [(t, _)] =
       
    83       (Code_Printer.str o pr_numeral unbounded o the_default 0 o dest_numeral naming thm) t;
    81   in
    84   in
    82     thy
    85     thy
    83     |> Code_Target.add_syntax_const target number_of (SOME (1, pretty))
    86     |> Code_Target.add_syntax_const target number_of (SOME (1, pretty))
    84   end;
    87   end;
    85 
    88