J-Bobを作ってみよう(7)

テストを移植しながら調べているとここが無限ループとは言わないまでも
やたらと時間がかかっていることを発見しました
なおインデントは自分で直しています（以下同文

>> (defs? (tdefs)
     '((defun double (x) (add x x))
       (defun len (xs) (if (atom xs) '0 (+ '1 (len (cdr xs)))))
       (dethm len>=0 (xs) (< '0 (+ (len xs) '1)))))

tdefsというのはこれ
J-Bobでは普通の意味での変数がないので、引数なしの関数として定義しています
preludeなどと同じ

(defun tdefs ()
  '((defun add (x y) (+ x y))
    (dethm eq (x) (equal (equal x x) 't))
    (defun li (x) (if (atom x) '() (cons (car x) (li (cdr x)))))
    (dethm xy (x y) (if (equal x 'a) (equal y '1) 't))))

引数が短ければすぐ帰ってきます

> (jeval '(def? (tdefs) '(defun double (x) (add x x))))
't

関数自体はそこまで繰り返しがあるようなものではありません

(defun defs? (known-defs defs)
  (if (atom defs)
    't
    (if (def? known-defs (car defs))
      (defs? (list-extend known-defs (car defs))
        (cdr defs))
      'nil)))

が、これをインタプリタが処理するところはというとうーん自分の脳が想像できる範囲を超えてる

ちょっとずつ引数を長くしていくとだんだん時間がかかるようになっていきます
もしかして普通に時間がかかってるだけなのかなあ

本に出てきたJ-Bob/*の例だと(prelude)を評価する時点で帰ってきません

これくらいにしてやると帰ってきます
最低限のしくみは一応動いてるみたい？

>> (J-Bob/step '()
  '(car (cons 'ham '(eggs)))
  '(((1) (cons 'ham '(eggs)))
    (() (car '(ham eggs)))))
'ham
>> (J-Bob/step
  '((dethm car/cons (x y) (equal (car (cons x y)) x)))
  '(car (cons 'ham '(eggs)))
  '((() (car/cons 'ham '(eggs)))))
'ham

でもこれだともう帰ってこない

>> (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))))))

どうするかなあ