53 end; |
53 end; |
54 |
54 |
55 |
55 |
56 (* code generator *) |
56 (* code generator *) |
57 |
57 |
58 fun add_code number_of negative unbounded target = |
58 local open Basic_Code_Thingol in |
59 Code_Target.add_literal_numeral target negative unbounded number_of |
59 |
60 @{const_name Int.Pls} @{const_name Int.Min} |
60 fun add_code number_of negative unbounded target thy = |
61 @{const_name Int.Bit0} @{const_name Int.Bit1}; |
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; |
|
67 fun dest_bit thm (IConst (c, _)) = if c = bit0' then 0 |
|
68 else if c = bit1' then 1 |
|
69 else Code_Printer.nerror thm "Illegal numeral expression: illegal bit" |
|
70 | dest_bit thm _ = Code_Printer.nerror thm "Illegal numeral expression: illegal bit"; |
|
71 fun dest_numeral thm (IConst (c, _)) = if c = pls' then SOME 0 |
|
72 else if c = min' then |
|
73 if negative then SOME ~1 else NONE |
|
74 else Code_Printer.nerror thm "Illegal numeral expression: illegal leading digit" |
|
75 | dest_numeral thm (t1 `$ t2) = |
|
76 let val (n, b) = (dest_numeral thm t2, dest_bit thm t1) |
|
77 in case n of SOME n => SOME (2 * n + b) | NONE => NONE end |
|
78 | dest_numeral thm _ = Code_Printer.nerror thm "Illegal numeral expression: illegal term"; |
|
79 fun pretty _ thm _ _ _ [(t, _)] = |
|
80 (Code_Printer.str o pr_numeral unbounded o the_default 0 o dest_numeral thm) t; |
|
81 in |
|
82 thy |
|
83 |> Code_Target.add_syntax_const target number_of (SOME (1, pretty)) |
|
84 end; |
|
85 |
|
86 end; (*local*) |
62 |
87 |
63 end; |
88 end; |