リリカル☆Lisp開発日記

久しぶりに新・ニコ動でLispを見てみたら、

数値比較したいです先生

というコメントがあったので、数値比較のための関数
=, <, >, <=, >=
を追加しました。

それから、階乗のプログラムを書く人が後を絶たないので、乗算も追加しました。
皆がどんなプログラムを試したかが残るというのはなかなか便利なものです。

comp.lang.lispのとある記事を見てて気づいたんですが、
(loop :until ... :do ...)
なんて書き方ができたんですね。
私は今まで
(loop :do ... :until)
のようなコードしか見たことがありませんでした。
当然、:untilだけでなく:whileでも同じようなことが出来るみたいです。

で、これらは同じ意味かと思ったら違うみたいです。

(loop :do (print 'oh!) :until t)
; OH!
; => NIL

(loop :until t :do (print 'oh!))
; => NIL

(macroexpand '(loop :do (print 'oh!) :until t))
; =>
; (MACROLET ((LOOP-FINISH NIL (SYSTEM::LOOP-FINISH-ERROR)))
;  (BLOCK NIL
;   (LET NIL
;    (MACROLET ((LOOP-FINISH NIL '(GO SYSTEM::END-LOOP)))
;     (TAGBODY SYSTEM::BEGIN-LOOP
;      (PROGN (PROGN (PRINT 'OH!)) (WHEN T (LOOP-FINISH)))
;      (GO SYSTEM::BEGIN-LOOP) SYSTEM::END-LOOP
;      (MACROLET
;       ((LOOP-FINISH NIL (SYSTEM::LOOP-FINISH-WARN)
;         '(GO SYSTEM::END-LOOP))))))))) ;
; T

(macroexpand '(loop :until t :do (print 'oh!)))
; =>
; (MACROLET ((LOOP-FINISH NIL (SYSTEM::LOOP-FINISH-ERROR)))
;  (BLOCK NIL
;   (LET NIL
;    (MACROLET ((LOOP-FINISH NIL '(GO SYSTEM::END-LOOP)))
;     (TAGBODY SYSTEM::BEGIN-LOOP
;      (PROGN (WHEN T (LOOP-FINISH)) (PROGN (PRINT 'OH!)))
;      (GO SYSTEM::BEGIN-LOOP) SYSTEM::END-LOOP
;      (MACROLET
;       ((LOOP-FINISH NIL (SYSTEM::LOOP-FINISH-WARN)
;         '(GO SYSTEM::END-LOOP))))))))) ;
; T

:doを先に書いた場合は、その内容が必ず1度は評価されるのに対し、
:whileや:untilを先に書いた場合はテストが先に行われるため、
:doの内容が評価されない場合もあるみたいです。

CLHSを眺めたところ、loopは基本的に書かれたとおりの順番に動くみたいです。
次のように気持ち悪いことも出来ます。

(loop :for i :from 0 :do (print i) :while (< i 3)  :collect i)
; 0
; 1
; 2
; 3
; => (0 1 2)

:whileを:collectより先に書いてあるので、リストに3は含まれません。
もちろん、:whileと:collectの順番を逆にすると、リストに3が含まれます。
loop恐るべし。

プログラミング Coqを参考に、CoqとCoqIDEを入れて試してみたが、
どうもCoqIDEの動きがおかしい。時々固まったり変な動作をする。
周りの人に相談したところ
「CoqIDEは使いものにならないからProof Generalを使え」
と言われたのでProof Generalとやらを入れてみた。
Emacs上で動く便利なものらしい。

以下はただのメモ書き。

* ダウンロード *
公式サイトからダウンロードする。
現時点のバージョンは4.0のようだ。

* インストール *
公式サイトの説明に従い、ファイルを展開して、
.emacsにload-fileを追加。

試しにEmacsで拡張子がvのファイルをひらいてみるが、
「Emacsのバージョンが23.1じゃないからダメ」
と怒られる。これまた公式サイトの説明に従いmake。

make clean
make compile EMACS=`which emacs`

しかし、make時にエラーが起こる。
「`font-lock-beginning-of-syntax-function’はobsoleteだから’syntax-begin-function’を使え」
と言ってるようなので、何も考えずにソースコード中の
font-lock-beginning-of-syntax-functionをsyntax-begin-functionに置換。
makeはこれで通った。

* 起動 *
Emacsで拡張子がvのファイルを開くと自動的にProof Generalが立ち上がる。
公式サイトのマニュアルを適当に眺めたところ、

• C-c C-nで証明をひとつ進める
• C-c C-uで証明をひとつ戻す

らしい。今の私の知識ではどうせこれしか使わない。後のものは後で覚えよう。

C-c C-RETでカーソルの位置まで証明を進めるみたいだが、
これをやろうとすると「C-c RET is undefined」と言われてしまう。
controlを押しながらreturnを押してるはずなんだけど、なんでだろう。
まあ、誰か詳しい人が解決法を教えてくれるだろう。

* 疑問点 *
CoqIDEでは「Eval simpl in xxx」みたいなものを、
専用の場所に書いていたけど、Proof Generalではどこに書けばいいんだろう。
ソース中に書いたら動いたけど、ソースとは分離したい。

前回に続いて、こんどはファイルのアップロード機能を付けました。

添付ファイルについて

セキュリティとか何も考えてないので結構怖いけど、
まあ、誰も使わないので今のところ大丈夫(?)でしょう。

前回とのdiffを貼っつけておきます。
(さらに…)