Reasoned Schemer (100) わり算 続き2

(split n r l h)はnからrの長さ+1だけ取ってlとし残りをhとする
ただしlやhがちゃんとした数字になるようにする

n: (0 0 1 0 1 1)
r: (1 0 1)
↓
l: (0 0 1  )
h          (1 1)

これは、rがpビットの長さの数だとするとn = h*2^(p + 1) + lとなる関係に相当

    ((== '() n) (== '() h) (== '() l))

n=()ならh=()、l=()
っていう見方だけじゃないんだけどな
n=()、h=()、l=()なら成功、って読んだほうがいいのかな
ピンときづらい

    ((fresh (b n^)
       (== `(0 ,b . ,n^) n) (== '() r)
       (== `(,b . ,n^) h) (== '() l)))

r=()でnの最下位ビットが0ならばl=()でhは最下位ビットを取り払った数
^はhighのことっぽい

    ((fresh (n^)
       (== `(1 . ,n^) n) (== '() r)
       (== n^ h) (== '(1) l)))

r=()でnの最下位ビットが1ならばl=(1)でhは最下位ビットを取り払った数
上のゴールと合わせるとnが0でなくてrが()のときをカバーしている

    ((fresh (b n^ a r^)
       (== `(0 ,b . ,n^) n)
       (== `(,a . ,r^) r) (== '() l)
       (splito `(,b . ,n^) r^ '() h)))

nの最下位ビットが0でrの長さが1以上ならば
l=()としてnとrの最下位ビットを取り払って()とhに分け直し

    ((fresh (n^ a r^)
       (== `(1 . ,n^) n)
       (== `(,a . ,r^) r) (== '(1) l)
       (splito n^ r^ '() h)))

nの最下位ビットが1でrの長さが1以上ならば
l=(1)としてnとrの最下位ビットを取り払って()とhに分け直し

このふたつはlの上位ビットが0だったときの対応をやってるってことみたい
とりあえずlを()なり(1)なりにして試してみるけど
lの上位ビットに1が出てくると失敗するっていう寸法

n=(0 1 1) r=(1)とするとl=()で(splito (1 1) () () h)を評価する→失敗
n=(1 1 1) r=(1)とするとl=(1)で(splito (1 1) () () h)を評価する→失敗
n=(0 0 1) r=(1)とするとl=()で(splito (0 1) () () h)を評価する→h=(1)
n=(1 0 1) r=(1)とするとl=(1)で(splito (0 1) () () h)を評価する→h=(1)

たぶんそう

    ((fresh (b n^ a r^ l^)
       (== `(,b . ,n^) n)
       (== `(,a . ,r^) r)
       (== `(,b . ,l^) l)
       (poso l^)
       (splito n^ r^ l^ h)))))

nもrもlも長さが1以上ならば最下位ビットを取り払って分け直し
1周目よりはわかってる感じするぞ