1149 |
1149 |
1150 syntax "_Float" :: "float_const \<Rightarrow> 'a" ("_") |
1150 syntax "_Float" :: "float_const \<Rightarrow> 'a" ("_") |
1151 |
1151 |
1152 parse_translation {* |
1152 parse_translation {* |
1153 let |
1153 let |
1154 fun mk_number i = |
|
1155 let |
|
1156 fun mk 1 = Syntax.const @{const_syntax Num.One} |
|
1157 | mk i = |
|
1158 let |
|
1159 val (q, r) = Integer.div_mod i 2; |
|
1160 val bit = if r = 0 then @{const_syntax Num.Bit0} else @{const_syntax Num.Bit1}; |
|
1161 in Syntax.const bit $ (mk q) end; |
|
1162 in |
|
1163 if i = 0 then Syntax.const @{const_syntax Groups.zero} |
|
1164 else if i > 0 then Syntax.const @{const_syntax Num.numeral} $ mk i |
|
1165 else |
|
1166 Syntax.const @{const_syntax Groups.uminus} $ |
|
1167 (Syntax.const @{const_syntax Num.numeral} $ mk (~ i)) |
|
1168 end; |
|
1169 |
|
1170 fun mk_frac str = |
1154 fun mk_frac str = |
1171 let |
1155 let |
1172 val {mant = i, exp = n} = Lexicon.read_float str; |
1156 val {mant = i, exp = n} = Lexicon.read_float str; |
1173 val exp = Syntax.const @{const_syntax Power.power}; |
1157 val exp = Syntax.const @{const_syntax Power.power}; |
1174 val ten = mk_number 10; |
1158 val ten = Numeral.mk_number_syntax 10; |
1175 val exp10 = if n = 1 then ten else exp $ ten $ mk_number n; |
1159 val exp10 = if n = 1 then ten else exp $ ten $ Numeral.mk_number_syntax n;; |
1176 in Syntax.const @{const_syntax divide} $ mk_number i $ exp10 end; |
1160 in Syntax.const @{const_syntax divide} $ Numeral.mk_number_syntax i $ exp10 end; |
1177 |
1161 |
1178 fun float_tr [(c as Const (@{syntax_const "_constrain"}, _)) $ t $ u] = c $ float_tr [t] $ u |
1162 fun float_tr [(c as Const (@{syntax_const "_constrain"}, _)) $ t $ u] = c $ float_tr [t] $ u |
1179 | float_tr [t as Const (str, _)] = mk_frac str |
1163 | float_tr [t as Const (str, _)] = mk_frac str |
1180 | float_tr ts = raise TERM ("float_tr", ts); |
1164 | float_tr ts = raise TERM ("float_tr", ts); |
1181 in [(@{syntax_const "_Float"}, K float_tr)] end |
1165 in [(@{syntax_const "_Float"}, K float_tr)] end |