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を作ろうシリーズおしまい！