J-Bobを作ってみよう(11) おしまい
まあ一度真正面からどう動いているのか見てやろうかと
ソースは組み込み関数を増やす前のものに戻しました
とりあえずこんな感じのベタなことをしてみました
これでも意外とつかめるかもしれないし
(define (jeval e)
(when debugging
(pretty-print e)
(read-line))
(cond
((string? e) e)
:
まずはお試し
>> (defun len (x) (if (atom x) '0 (+ '1 (len (cdr x)))))
'(defun len (x) (if (atom x) '0 (+ '1 (len (cdr x)))))
#<void>
>> (len '(a b c))
3
>> (debug 't)
#<void>
>> (len '(a b c))
'(len '(a b c))
'(if (atom '(a b c)) '0 (+ '1 (len (cdr '(a b c)))))
''(a b c)
'(+ '1 (len (cdr '(a b c))))
''1
'(len (cdr '(a b c)))
'(if (atom (cdr '(a b c))) '0 (+ '1 (len (cdr (cdr '(a b c))))))
'(atom (cdr '(a b c)))
'(cdr '(a b c))
''(a b c)
'(+ '1 (len (cdr (cdr '(a b c)))))
''1
'(len (cdr (cdr '(a b c))))
'(if (atom (cdr (cdr '(a b c)))) '0 (+ '1 (len (cdr (cdr (cdr '(a b c)))))))
'(atom (cdr (cdr '(a b c))))
'(cdr (cdr '(a b c)))
'(cdr '(a b c))
''(a b c)
'(+ '1 (len (cdr (cdr (cdr '(a b c))))))
''1
'(len (cdr (cdr (cdr '(a b c)))))
'(if (atom (cdr (cdr (cdr '(a b c)))))
'0
(+ '1 (len (cdr (cdr (cdr (cdr '(a b c))))))))
'(atom (cdr (cdr (cdr '(a b c)))))
'(cdr (cdr (cdr '(a b c))))
'(cdr (cdr '(a b c)))
'(cdr '(a b c))
''(a b c)
''0
3
こんな感じかな
て
ちょっと待て
そうなるのか?
ここ
'(len (cdr '(a b c)))
'(if (atom (cdr '(a b c))) '0 (+ '1 (len (cdr (cdr '(a b c))))))
まあ間違いじゃないんだけど
(cdr '(a b c))
を評価してからlen
を適用するんじゃないの?
誰がこんなこと書いてんの?(俺
・・・
そうか、japply
する前に引数を評価してないから
なまじちゃんと値を返すからよくない(お前がよくない
えーと、ということは
evlis
ってやつだ 思い出した
こう?
(define (evlis es)
(cond ((null? es) '())
(else (cons (jeval (car es)) (evlis (cdr es))))))
(define (jeval e)
:
(else (japply op (evlis (cdr e)))))))))
どれどれ
>> (len '(a b c))
'(len '(a b c))
''(a b c)
'(if (atom (a b c)) '0 (+ '1 (len (cdr (a b c)))))
'(atom (a b c))
'(a b c)
'b
car: contract violation
expected: pair?
given: 'b
あり?
・・・
'(atom (a b c))
ってのがおかしいな
'(a b c)
を評価して(a b c)
になったものをatom
に渡してるから
(a b c)
を関数適用だと思ってるのか
評価済みで値になっているものを区別しなきゃだめ?
jeval
したら常に値になってるはずだから区別する必要はないか
じゃあ・・・quote
つけるの?
(quote (a b c))
を評価してせっかく(a b c)
になったのに
またquote
をつけるのは釈然としないけど・・・
でも今の形で値を表現するならそれしかないのかな
こうですか?
(define (evlis es)
(cond ((null? es) '())
(else (cons (list 'quote (jeval (car es))) (evlis (cdr es))))))
もはやお祈りレベル
>> (len '(a b c))
'(len '(a b c))
''(a b c)
'(if (atom '(a b c)) '0 (+ '1 (len (cdr '(a b c)))))
'(atom '(a b c))
''(a b c)
'(+ '1 (len (cdr '(a b c))))
''1
'(len (cdr '(a b c)))
'(cdr '(a b c))
''(a b c)
'(if (atom '(b c)) '0 (+ '1 (len (cdr '(b c)))))
'(atom '(b c))
''(b c)
'(+ '1 (len (cdr '(b c))))
''1
'(len (cdr '(b c)))
'(cdr '(b c))
''(b c)
'(if (atom '(c)) '0 (+ '1 (len (cdr '(c)))))
'(atom '(c))
''(c)
'(+ '1 (len (cdr '(c))))
''1
'(len (cdr '(c)))
'(cdr '(c))
''(c)
'(if (atom '()) '0 (+ '1 (len (cdr '()))))
'(atom '())
''()
''0
3
OKらしい
>> (J-Bob/prove
'((dethm car/cons (x y) (equal (car (cons x y)) x))
(dethm equal-same (x) (equal (equal x x) 't))
(defun pair (x y) (cons x (cons y '())))
(defun first-of (x) (car x)))
'(((dethm first-of-pair (a b)
(equal (first-of (pair a b)) a))
nil
((1 1) (pair a b))
((1) (first-of (cons a (cons b '()))))
((1) (car/cons a (cons b '())))
(() (equal-same a)))))
't
一瞬じゃないですか
>> (show-profile)
'((tag? 272)
(untag 196)
(member? 185)
(elem1 151)
(defun? 91)
:
ええええそうでしょうとも
私が悪うございました
> (time (jload "LittleProver.jbb"))
chapter1.example1 ok
chapter1.example2 ok
:
:
dethm.align/align ok
dethm.align/align ok
cpu time: 1025497 real time: 1026689 gc time: 6980
全テスト通りました!
時間もそこそこで
何百倍かはかかってますけど
というわけでJ-Bobを作ろうシリーズおしまい!