::Eldesh a b = LEFT a | RIGHT b

SML/NJ インタプリタの表示設定を変更する

SML

SML/NJのインタプリタは, 入力した式の評価結果をいい感じに表示してくれるので便利ですが,

複雑なデータは適当に省略されて表示されてしまいます.

たとえばこんな感じ.

- val xs = List.tabulate (15,fn x=>x);
val xs = [0,1,2,3,4,5,6,7,8,9,10,11,...] : int list

あと少しくらいがんばって欲しいワケですがバッサリ切られます

変更方法

この表示方法は,処理系専用に提供されているstructureから設定すれば変更することが出来ます.

- Control.Print.printLength := 15; (* 表示するリストの長さを伸長 *)
val it = () : unit
- val xs = List.tabulate (15,fn x=>x);
val xs = [0,1,2,3,4,5,6,7,8,9,10,11,12,13,14] : int list

おｋ

設定できる項目一覧

(* 表示は多少弄ってるが言いたいことは伝わる。多分。 *)
structure Control.Print :
  sig
	val printDepth : int ref  (* コンストラクタのネストをどこまで展開するか *)
	val printLength : int ref (* リストの長さ *)
	val stringDepth : int ref (* 文字列の長さ *)
	val intinfDepth : int ref (* LargeIntの表示桁数 *)
	val printLoop : bool ref  (* ループ検出を行うか *)
	val signatures : int ref  (* ネストしたシグネチャの展開段数 *)
	val printOpens : bool ref (* open したときシグネチャを表示するか *)
	val linewidth : int ref   (* 一行の長さ(これを超えると改行する) *)
	(* インタプリタの表示関数 *)
	val out : {flush:unit -> unit, say:string -> unit} ref
	val say : string -> unit
	val flush : unit -> unit
  end

大体名前から明らかですね. あんまり明らかじゃないモノを以下で解説します.

printLoop

	val printLoop : bool ref  (* ループ検出を行うか *)

これはデータ構造の循環構造を検出して, それと分かる表示をしてくれるオプションです.

datatype Loop = X | T of int * Loop ref
val xr = ref X;
val xs = T (1, xr);
xr := xs;
- xs; (* xs は [1..] のような遅延リストになる *)
val it = T (1,ref (T (1,%0)) as %0) : Loop
(* %0 は内部に自身への参照を持っていると分かる *)

これをオフにすると….

- Control.Print.printLoop := false;
- xs;
val it = T (1,ref (T (1,ref (T (1,ref (T (1,ref (T (1,ref #))))))))) : Loop
(* 深さ(or長さ)の制限まで展開し続けます *)

表示関数のフックと書き換え

	val out : {flush:unit -> unit, say:string -> unit} ref

インタプリタが表示に使う関数をこれで書き換えることが出来ます.

(* インタプリタの出力をログファイルに書き出す例 *)
let val f = TextIO.openIn "smlnj.log"
in Control.Print.out := {flush=fn()=>TextIO.flushOut f, say=fn s=> TextIO.output(f,s)}
end

.oO(ファイルを閉じてないけど。ま、いいか)

ref

マニュアル

intinfDepth の記載が無い件…

ツイートする

Permalink | コメント(0) | トラックバック(0) | 18:59

Coqチュートリアル#4(最終回) に参加しました

Coq, event

Coqチュートリアル#4最終回に行って来ました。4回とも参加できたので皆勤賞です！

講師の @tmiya_ さんと運営の @kenkoba さんお疲れ様でした。

参加者は入れ替わってたようですが、人数が変動してないのは特徴的でしたね。(もっと続けると続々と猛者が参戦した…のかも知れない)

まだ文法が身についてない感じがありますが、証明の手順や、Coqで出来そうなこととムリそうなことの雰囲気が掴めたかなーと思います。

もう少し習熟すれば普段書いてるコードも多少違ってくる予感はしますがどうなんでしょうね。

しかし実用への道のりは長そうです…。普段イカに何も考えずコード書いてるのかと。

あるいは現実は複雑なので空想世界で生きる術を模索するべきかもしれません…。

より詳しく知ろうとするなら、事あるごとに話題にのぼっていた名大の資料ですかね。おススメだそうです。＃なごやこわい

〆

ともかく、また知らない世界のことが多少なり覗けた良い経験になったと思います。

講師、運営、他の参加者の方々ありがとうございました。

ツイートする

Permalink | コメント(0) | トラックバック(0) | 15:28

純粋関数型言語のfoldlで副作用を起こす

Clean, C++

http://d.hatena.ne.jp/i_k_b/20120215/1329320486に触発されてCleanでも書いてみました。

module foldout
import StdEnv

// 出力する関数 (Fileは一意でなければならない)
// class (<<<) infixl a :: !*File !a -> *File

msg :== ["hello,", " uniqueness", " typing!", "\n"]

Start w # (cout, w) = stdio w
          cout = foldl (<<<) cout msg // side effect caused by foldl !
		/*
          cout = cout <<< "hello,"
          cout = cout <<< "uniqueness typing!"
         */
          (ok,w) = fclose cout w
        = w

実行結果

hello, uniqueness typing!

普通のfoldlに副作用を起こす関数(<<<)を渡せていますね。

解説

Cleanでは副作用を一意性型付け(uniqueness typing)によって扱います。

これをどのように表すかというと、型への 一意性を表す修飾(*) の有無で区別します。

この修飾はCleanコンパイラによって推論されるので、普通に副作用を含む式を書いていくとコンパイラが正しく修飾(と検査)を行ってくれます。

ところでこの修飾は式毎(= 使われる場所ごと)に行われるので、純粋なつもりで書いてある関数でも、途中で参照が共有されていなければ、安全に副作用を含む関数を渡すことが出来ます。

つまり副作用あり版と無し版をそれぞれ定義する必要がありません！スゴイね！

ツイートする

Permalink | コメント(0) | トラックバック(0) | 11:14

FreeBSDにredmineを入れる

FreeBSD, redmine

portsが壊れている(というかインストールできないようになってる)ので手動で入れた。

ここの通りにすればよい＞http://howtobsd.com/ 。

あらかじめrubyのバージョンが1.9になってる場合もどす必要がある。(see /usr/ports/UPDATING@20110823)

gemのバージョンも下げる必要がある。

$ gem update --system 1.6.2

で、リンク先の通りに作業するとセットアップ完了。

apache上でpassengerを使ってサブディレクトリ(/redmine)で公開するのに、以下のように設定した。

最後の抵抗(笑)としてpassengerはportsから入れた(www/rubygem-passenger)。

LoadModule passenger_module /usr/local/lib/ruby/gems/1.8/gems/passenger-3.0.11/ext/apache2/mod_passenger.so
PassengerRoot /usr/local/lib/ruby/gems/1.8/gems/passenger-3.0.11
PassengerRuby /usr/local/bin/ruby18
Alias /redmine "/usr/local/www/redmine-1.2/public"
<Directory "/usr/local/www/redmine-1.2/public">
        RailsEnv production
        RailsBaseURI /redmine
        Order deny,allow
        Allow from all
</Directory>

passengerはかなり柔軟に設定できる感じ＞

（ところで、ググって出てくる設定例はみんなVirtualHost使ってるんだけどナンデ？)

外部から見える場所にある場合は、[管理]>[設定]>[認証]>([認証が必要],[ユーザは自分で登録できる])をチェックしておくこと。

＃なんでこんなにバージョンセンシティブなの？しぬの？

ツイートする

Permalink | コメント(0) | トラックバック(0) | 11:53

Coqチュートリアル#1 行ってきた

Coq, event

気になっていたところに Formal Methods Forum主催Coqチュートリアル＃1があったので、どんなもんかと聞いてきました。

当日の資料もリンク先に挙がってますね。

受講者は8人くらい？来てました。

Formal Methods Forumの @tmiya_ さんが主に解説して @kencoba さんがフォローという形。

tutorial.vをCoqIDEで眺めながら、普通の言語と対応付くように文法を丁寧に解説してくれてるのを聞きつつ、

証明を記述する文法と流れが分かった…ような分からんような…？（え ド・モルガン則の証明をする演習までで第一回終了。

(隙を見てはvimでどうにかならないかググリつつやってましたけど、その場ではどうにもならず。どうにかしたい。)

二時間で且つ手取り足取りな感じなので、こんなモンでしょうか。

講師の@tmiya_さんがガリグ先生の資料推しだったのでチュートリアルと平行して読めればいいなーという感じ。

次回は2月のアタマにやるみたいです。

人数増やしていきたいらしいのでCoqが気になる人は行きましょう！

ツイートする

Permalink | コメント(0) | トラックバック(0) | 12:06