54 |
54 |
55 (* code generator *) |
55 (* code generator *) |
56 |
56 |
57 local open Basic_Code_Thingol in |
57 local open Basic_Code_Thingol in |
58 |
58 |
59 fun add_code number_of negative unbounded print target thy = |
59 fun add_code number_of negative print target thy = |
60 let |
60 let |
61 fun dest_numeral pls' min' bit0' bit1' thm = |
61 fun dest_numeral pls' min' bit0' bit1' thm = |
62 let |
62 let |
63 fun dest_bit (IConst (c, _)) = if c = bit0' then 0 |
63 fun dest_bit (IConst (c, _)) = if c = bit0' then 0 |
64 else if c = bit1' then 1 |
64 else if c = bit1' then 1 |
72 let val (n, b) = (dest_num t2, dest_bit t1) |
72 let val (n, b) = (dest_num t2, dest_bit t1) |
73 in case n of SOME n => SOME (2 * n + b) | NONE => NONE end |
73 in case n of SOME n => SOME (2 * n + b) | NONE => NONE end |
74 | dest_num _ = Code_Printer.eqn_error thm "Illegal numeral expression: illegal term"; |
74 | dest_num _ = Code_Printer.eqn_error thm "Illegal numeral expression: illegal term"; |
75 in dest_num end; |
75 in dest_num end; |
76 fun pretty literals [pls', min', bit0', bit1'] _ thm _ _ [(t, _)] = |
76 fun pretty literals [pls', min', bit0', bit1'] _ thm _ _ [(t, _)] = |
77 (print o Code_Printer.literal_numeral literals unbounded |
77 (Code_Printer.str o print literals o the_default 0 o dest_numeral pls' min' bit0' bit1' thm) t; |
78 o the_default 0 o dest_numeral pls' min' bit0' bit1' thm) t; |
|
79 in |
78 in |
80 thy |> Code_Target.add_syntax_const target number_of |
79 thy |> Code_Target.add_syntax_const target number_of |
81 (SOME (1, ([@{const_name Int.Pls}, @{const_name Int.Min}, |
80 (SOME (1, ([@{const_name Int.Pls}, @{const_name Int.Min}, |
82 @{const_name Int.Bit0}, @{const_name Int.Bit1}], pretty))) |
81 @{const_name Int.Bit0}, @{const_name Int.Bit1}], pretty))) |
83 end; |
82 end; |