这是我认为如何完成的概述。
它开始于Num.thy parse_translation，ML 函数numeral_tr。
在该函数中，使用了Lexicon.read_xnum of lexicon.ML，它接受一个字符串参数。
我不知道细节，但字符串"15"是从类似的表达式中提取的
"15 = n@N|(num.Bit1 (num.Bit1 (num.Bit1 num.One)))",
并馈送到read_xnum，那里有这个等价物：
Lexicon.read_xnum "15" = {leading_zeros = 0, radix = 10, value = 15}
在read_xnum 中使用了函数Library.read_radix_int of library.ML，它接受一个整数基数和一个数字列表作为参数，如下等式所示：
Library.read_radix_int 10 ["1","5"] = (15, []);
接下来，从15 到(num.Bit1 (num.Bit1 (num.Bit1 num.One))) 的转换是IntInf.quotRem in the parse_translation 的结果。
这让我不再为isabelle.in.tum.de/repos 提供方便的 HTML 链接。
IntInf.quotRem 在 Isabelle2013-2\contrib\polyml-5.5.1-1\src\basis\IntInf.sml 中，定义为
val quotRem: int*int->int*int = RunCall.run_call2C2 POLY_SYS_quotrem,
这导致 Isabelle2013-2\contrib\polyml-5.5.1-1\src\basis\RuntimeCalls.ML 第 83 行：
val POLY_SYS_quotrem = 104 (* DCJM 05/03/10 *).
对于将我带到 Isabelle2013-2\contrib\polyml-5.5.1-1\src\libpolyml\x86asm.asm 第 1660 行的 Windows，虽然我可能会遗漏一些重要细节：
quotrem_really_long:
MOVL Reax,Redi
CALLMACRO CALL_IO POLY_SYS_quotrem
CALLMACRO RegMask quotrem,(M_Reax OR M_Redi OR M_Redx OR Mask_all).
我认为这足以回答我的问题。将字符串“15”转换为ML整数，然后使用一些汇编语言级别的商/余数除法将15转换为二进制Num.num。
我实际上只对read_radix_int 中的“15”如何转换为15 以及该函数的详细信息是否对我有帮助感兴趣。我将在下面详细解释该应用程序。
从这里开始，我为自己添加了更多的细节，以便将我收集的大部分信息以一种很好的形式呈现出来。
什么交易
我从一个二进制数作为bool list 开始，类似于[True, True, True, True] 表示二进制15，不过在这里，我在某些方面进行了简化。
然后将其转换为 [[True, False, True, False], [True, False, True]] 之类的东西，即十进制 15。
真正的问题是找到正确的搜索词组
搜索 "decimal to binary conversion" 之类的内容会返回指向许多基本数学算法的链接，这不是我想要的。
正常的编程转换也不是我需要的，这只是明确表明整数已经是二进制形式的基本事实：
最后，其他搜索让我找到了正确的词“基数”。此外，我还搜索了 C 中的事情是如何完成的，其中位移位是我想要联系的，尽管这些可能不是我需要的：
返回 Num.thy 的基数
“Radix”把我带回了 Num.thy，我认为这可能是行动的地方，但没有看到任何对我来说很明显的东西。
我包含一些来自 Num.thy、lexicon.ML 和 IntInf.sml 的源代码：
(* THE TWO MAIN EXTERNAL FUNCTIONS IN THE TRANSLATIONS: read_xnum, quotRem *)
ML{*
Lexicon.read_xnum; (* string ->
{leading_zeros: int, radix: int, value: int}.*)
Lexicon.read_xnum "15"; (* {leading_zeros = 0, radix = 10, value = 15}.*)
Lexicon.read_xnum "15" = {leading_zeros = 0, radix = 10, value = 15};
IntInf.quotRem; (* int * int -> int * int.*)
IntInf.quotRem (5,3); (* (1, 2) *)
*}
parse_translation {* (* Num.thy(293) *)
let
fun num_of_int n =
if n > 0 then
(case IntInf.quotRem (n, 2) of
(0, 1) => Syntax.const @{const_name One}
| (n, 0) => Syntax.const @{const_name Bit0} $ num_of_int n
| (n, 1) => Syntax.const @{const_name Bit1} $ num_of_int n)
else raise Match
val pos = Syntax.const @{const_name numeral}
val neg = Syntax.const @{const_name neg_numeral}
val one = Syntax.const @{const_name Groups.one}
val zero = Syntax.const @{const_name Groups.zero}
fun numeral_tr [(c as Const (@{syntax_const "_constrain"}, _)) $ t $ u] =
c $ numeral_tr [t] $ u
| numeral_tr [Const (num, _)] =
let
val {value, ...} = Lexicon.read_xnum num;
in
if value = 0 then zero else
if value > 0
then pos $ num_of_int value
else neg $ num_of_int (~value)
end
| numeral_tr ts = raise TERM ("numeral_tr", ts);
in [("_Numeral", K numeral_tr)] end
*}
ML{* (* lexicon.ML(367) *)
(* read_xnum: hex/bin/decimal *)
local
val ten = ord "0" + 10;
val a = ord "a";
val A = ord "A";
val _ = a > A orelse raise Fail "Bad ASCII";
fun remap_hex c =
let val x = ord c in
if x >= a then chr (x - a + ten)
else if x >= A then chr (x - A + ten)
else c
end;
fun leading_zeros ["0"] = 0
| leading_zeros ("0" :: cs) = 1 + leading_zeros cs
| leading_zeros _ = 0;
in
fun read_xnum str =
let
val (sign, radix, digs) =
(case Symbol.explode (perhaps (try (unprefix "#")) str) of
"0" :: "x" :: cs => (1, 16, map remap_hex cs)
| "0" :: "b" :: cs => (1, 2, cs)
| "-" :: cs => (~1, 10, cs)
| cs => (1, 10, cs));
in
{radix = radix,
leading_zeros = leading_zeros digs,
value = sign * #1 (Library.read_radix_int radix digs)}
end;
end;
*}
ML{* (* IntInf.sml(42) *)
val quotRem: int*int->int*int = RunCall.run_call2C2 POLY_SYS_quotrem
*}
我正在寻找的大部分内容；又是基数
(* THE FUNCTION WHICH TRANSLATES A LIST OF DIGITS/STRINGS TO A ML INTEGER *)
ML{*
Library.read_radix_int; (* int -> string list -> int * string list *)
Library.read_radix_int 10 ["1","5"]; (* (15, []): int * string list.*)
Library.read_radix_int 10 ["1","5"] = (15, []);
*}
ML{* (* library.ML(670) *)
fun read_radix_int radix cs =
let
val zero = ord "0";
val limit = zero + radix;
fun scan (num, []) = (num, [])
| scan (num, c :: cs) =
if zero <= ord c andalso ord c < limit then
scan (radix * num + (ord c - zero), cs)
else (num, c :: cs);
in scan (0, cs) end;
*}
低级划分动作
还有高层Integer.div_mod in integer.ML，上面的翻译没有用到：
fun div_mod x y = IntInf.divMod (x, y);
在 Isabelle2013-2\contrib\polyml-5.5.1-1\src\basis\IntInf.sml 中，可以将较高级别的divMod 与较低级别的quotRem 进行比较：
ML{* (* IntInf.sml(42) *)
val quotRem: int*int->int*int = RunCall.run_call2C2 POLY_SYS_quotrem
(* This should really be defined in terms of quotRem. *)
fun divMod(i, j) = (i div j, i mod j)
*}
quotRem 的低级操作显然是在汇编语言级别完成的：
ML{* (* RuntimeCalls.ML(83) *)
val POLY_SYS_quotrem = 104 (* DCJM 05/03/10 *)
*}
(* x86asm.asm(1660)
quotrem_really_long:
MOVL Reax,Redi
CALLMACRO CALL_IO POLY_SYS_quotrem
CALLMACRO RegMask quotrem,(M_Reax OR M_Redi OR M_Redx OR Mask_all)
*)
div 和 mod 的这些不同形式对我来说很重要。
我认为div 和mod 应尽可能避免，但我认为，如果分裂是不可避免的，则绑定quotRem 将是可行的方法。