情報は力ではない

VimとかC++とかCUDAとか。

vim-ocaml-stdlib-helpを作った。

最近、OCamlを勉強していて、VimOCamlを書いてます。その時に標準ライブラリの機能を調べたいなと思うのだけれど、いちいちブラウザで調べるのも面倒なのでVim pluginを作りました。

github.com

使い方は

:OCamlStdLibHelp {module-name}

という感じです。例えば

:OCamlStdLibHelp Array

とすれば

module Array: sig .. end
Array operations.
val length : 'a array -> int
Return the length (number of elements) of the given array.
val get : 'a array -> int -> 'a
Array.get a n returns the element number n of array a.
   The first element has number 0.
   The last element has number Array.length a - 1.
   You can also write a.(n) instead of Array.get a n.


   Raise Invalid_argument "index out of bounds"
   if n is outside the range 0 to (Array.length a - 1).
val set : 'a array -> int -> 'a -> unit
Array.set a n x modifies array a in place, replacing
   element number n with x.
   You can also write a.(n) <- x instead of Array.set a n x.


   Raise Invalid_argument "index out of bounds"
   if n is outside the range 0 to Array.length a - 1.

といった感じで出力されます。割と雑に作ってるので、まだ読みづらいです。

この標準ライブラリのドキュメントは The standard library から引っ張ってきています。

このサイトのHTMLは<p>タグが閉じられていないのでYQLを使ってタグが閉じられたHTMLを取得しています。

YQL - Yahoo Developer Network

あとはVital.Web.HTTPとVital.Web.XMLを用いてスクレイピングをしている感じです。

github.com

これらの方法はmattnさんのブログを見て作成をしました。

mattn.kaoriya.net

今後

まだ出力結果が見づらいので、そこを変更したい。また、コマンド実行時にVimをブロックしてしまうので非同期処理にしたいなと考えています。

TaPL 演習3.5.14

問題

定理3.5.4が算術演算の評価関係に関しても成り立つことを示せ。
すなわち、 t→t' かつ  t→t'' ならば  t'=t'' であることを示せ。

証明

 t→t' の導出に関する帰納法を使用し、  t→t' の導出で最後に使った規則に対する場合分けにより証明する。

 (i) E-SUCCの場合

 t succ  t_1 という形であり、またある  t_1' が存在して  t_1→t_1' である。
左側の最も外側に  succ を用いている規則はE-SUCCのみである。 よって、 t→t'' の導出で最後に使った規則もE-SUCCであり、ある  t_1'' が存在して t_1→t_1'' である。 帰納法の仮定より、 t_1' = t_1'' 。 したがって、 t' = succ  t_1' = succ  t_1'' = t''

 (ii) E-PREDZEROの場合

 t pred  t_1 という形であり、 t_1 = 0 である。 左側の最も外側に  pred を用いている規則はE-PREDZERO、E-PREDSUCCとE-PREDの3つであるので  t→t'' の導出の最後に使った規則はこのうちのいずれかである。  t→t'' の導出で最後に使った規則はE-PREDではない。 E-PREDであれば、ある  t_1'' が存在して  t_1→t_1'' となるが、0は値なので、評価されないからである。 E-PREDSUCCの場合、 t_1 = succ  nv_1となるが、 t_1 = 0 であるのでE-PREDSUCCでもない。 よって、 t→t'' の導出の最後に使った規則はE-PREDZEROであり、 t' = t'' となる。

 (iii) E-PREDSUCCの場合

 t pred  t_1 という形であり、 t_1 = succ  nvである。  (ii)と同様の推論により、 t→t'' の導出の最後に使った規則はE-PREDSUCCであることがわかる。 よって、 t' = t'' となる。

 (iv) E-PREDの場合

 t pred  t1という形であり、ある  t_1' が存在して  t_1→t_1' である。 (ii)と同様の推論により、 t→t'' の導出で最後に使った規則がE-PREDであることがわかる。 このとき、ある  t_1'' が存在して、 t_1→t_1'' である。 帰納法の仮定より、 t_1' = t_1''。 よって、 t' = pred  t_1' = pred  t_1'' = t''

 (v) E-ISZEROZEROの場合

 t iszero  t_1 という形をしており、 t_1 = 0である。 左側の最も外側に iszero を用いている規則はE-ISZEROZERO、E-ISZEROSUCC、E-ISZEROがあるが  succ  nv_1 と0は異なるので、 t→t'' の導出で最後に使った規則はE-ISZEROSUCCではない。 また、E-ISZEROでもない。なぜなら、E-ISZEROであれば、ある  t_1' が存在して t_1→t_1' となるが 0は値なので評価されないからである。 よって t→t'' の導出で最後に使った規則はE-ISZEROZEROであり、 t' = t''

 (vi) E-ISZEROSUCCの場合

 t iszero  t_1 という形をしており、 t_1 = succ  nv_1 である。  (v) と同様の推論で、 t→t'' の導出で最後に使った規則がE-ISZEROSUCCであることがわかる。 よって、 t' = t''

 (vii) E-ISZEROの場合

 t iszero  t_1という形をしており、ある t_1' が存在して  t_1→t_1' である。  (v) と同様の推論により、 t→t'' の導出で最後に使った規則がE-ISZEROであることがわかる。 このとき、ある  t_1'' が存在して、 t_1→t_1'' である。 帰納法の仮定より、 t_1' = t_1''。 よって、 t' = iszero  t_1' = iszero  t_1'' = t''

以上より、 t→t' かつ  t→t'' ならば  t' = t'' である。

所感

解答に書いている通り、tの構造に関する帰納法を用いたほうが簡潔だなぁ。

JavaScriptの論理演算子の評価値

最近、サイ本を読んでいます。 その中で少し驚いたものを一つ紹介したいと思います。

以下の論理演算子が何を返すかという話をします。

var o = { a: 0 };

var b1 = o && o.a;
var b2 = undefined && o;
var b3 = o || "";
var b4 = null || undefined

値の論理値への変換

JavaScriptの値は、すべて論理値に変換可能できます。 次の値は全てfalseに変換されます。

  • undefined
  • null
  • 0
  • -0
  • NaN
  • ""

上記以外の値は、すべてtrueに変換されるので、次の式はtrueに変換されることになります。

{ a: 0 }

&&演算子と||演算子

&&演算子は次のような処理を行う。 1. 左の被演算子が「falseに評価されるもの」であれば、それを返す。 2. 左の被演算子が「trueに評価されるもの」であれば、右の被演算子を返す。

||演算子は次のような処理を行う。 1. 左の被演算子が「trueに評価されるもの」であれば、それを返す。 2. 左の被演算子が「falseに評価されるもの」であれば、右の被演算子を返す。

ですので、この記事の冒頭で示した論理演算子の評価値は次のようになります。

var o = { a: 0 };
var b1 = o && o.a; // 0
var b2 = undefined && o; // undefined
var b3 = o || ""; // { a: 0 }
var b4 = undefined || null; // null

面白いと思うのは、trueやfalseを返すということではないということです。 これを用いると引数がnullやundefinedのときのデフォルト値を設定することができます。

function foo(x) {
  // xがfalseと評価されるものであれば、xは{a: 0}となる
  var x = x || { a: 0 };

  // ...
}

ただ、このxにtrueかfalseが入っているようにも見えるので、初心者はハマるかもなぁという感想です。

ほぼすべてサイ本の内容そのままという感じですが、自分でまとめると ちゃんとわかっているかの確認になってよいなという感じです。 今後もまたサイ本を読んで気になった箇所の記事を書きたいと思います。

www.amazon.co.jp

Vimの起動時間を計測する。

概要

Vimの起動時間を計測するには次のようにする。
{fname}にその結果が書き込まれる。

vim --startuptime {fname}

内容

Vimの起動時間を計測するには、--startuptimeオプションをつけてVimを起動する。このオプションには引数としてファイル名が必要。
helpによると、startuptime付きでVimコンパイルした時のみ有効だそうです。

例えば、次のように起動すると、hoge.txtに起動時の経過時間のメッセージが記述される。

vim --startuptime hoge.txt

hoge.txtの内容は次のような感じになってるはず。

times in msec
 clock   self+sourced   self:  sourced script
 clock   elapsed:              other lines

000.007  000.007: --- VIM STARTING ---
000.082  000.075: Allocated generic buffers
000.500  000.418: locale set
000.507  000.007: clipboard setup
000.517  000.010: window checked
002.179  001.662: inits 1
(略)
156.321  000.116: BufEnter autocommands
156.324  000.003: editing files in windows
156.892  000.568: VimEnter autocommands
156.899  000.007: before starting main loop
157.412  000.513: first screen update
157.414  000.002: --- VIM STARTED ---

左の列が起動開始からの時間(msec)で、次の列が、それぞれの処理にかかった時間(msec)になる。
これを使うことで、プラグインの読み込み時にかかる時間も確認することができる。

ヘルプ

:help --startuptime

Mockitoの@InjectMocksは何を見てInjectするのか

InjectMocks (Mockito 2.0.36-beta API)に書いてます。
思った挙動と異なっていたので、自分のためにメモ。

次のようなSampleクラスがあったとする。

public class Sample {
    private final Hoge hoge;
    private final Fuga fuga;

    private HogeHoge hogehoge;

    public Sample(Hoge hoge, Fuga fuga) {
        this.hoge = hoge;
        this.fuga = fuga;
    }

    public Hoge getHoge() {
        return hoge;
    }

    public Fuga getFuga() {
        return fuga;
    }

    public HogeHoge getHogeHoge() {
        return hogehoge;
    }
}

このクラスに対するテストを次のように書いて実行すると、コメントの部分でAssertionErrorになる。

public class SampleTest {
    @Mock
    Hoge hoge;

    @Mock
    Fuga fuga;

    @Mock
    HogeHoge hogehoge;

    @InjectMocks
    Sample sample;

    @Before
    public void setup() {
        MockitoAnnotations.initMocks(this);
    }

    @Test
    public void test() {
        assertEquals(hoge, sample.getHoge());
        assertEquals(fuga, sample.getFuga());
        assertEquals(hogehoge, sample.getHogeHoge());  // ここでAssertionError
    }
}

自分は最初、MockitoAnnotations.initMocks()を呼び出すことで@Mockを指定したすべてのクラスがSampleクラスにInjectされると思ってたが、違うようだった。
そこで、この記事の最初に掲載したドキュメントを読むとConstrucor injection, Setter injection, Field injectionのいずれか"のみ"でInjectされることがわかった。
Sampleクラスの場合、Constructor injectionが行われていて、HogeクラスとFugaクラスがInjectされる。Constructor Injectionが成功したので、HogeHogeクラスはInjectionされることがないようだ。

ちゃんとドキュメントは読むべきなのだなあと改めて思った出来事だった。

ハル研究所プログラミングコンテスト2015

一昨年のハル研プロコン2014に引き続き、去年もハル研プロコンに参加しました。
ハル研究所 プログラミングコンテスト2015 | TOP

今年の問題は宅配便でした。
問題の雰囲気は、車両配送問題(Vehicle Routing Problem, VRP)っぽい感じです。

開催されてからすぐに最適解らしいスコアが上位に現れ、そのスコアの人が上位に連なり、最終的には上位10人が同じスコアになり、1秒未満の戦いが上位で繰り広げられていました。
自分はそんな上には行けませんでした。うーん、悔しい。

自分は普段からコンテストに出ているような人ではないので、いろいろな解法を試してみようと思いながらちょくちょく回答を書いていました。

とかを実装してました。
動的計画法ではなぜかスコアが伸びなかったので(おそらく実装力のなさが原因)、最終的にはビームサーチに頼ってました。
評価関数どうするかがわからなくて結局スコア伸びなかったのですが。

今年度で学生が終わるのでハル研プロコンに出れるのが今回で最後。
今回のプロコンは最適解を出せて初めてスタートラインに立つようなものなので、最後のプロコンでスタートラインに立てなかったのは悔しさが残ります。
でもハル研プロコンに参加して、自分の雑魚さがよくわかったので良かったかなと思います。何より楽しかった。
ハル研プロコン実行委員会の皆さま、楽しいひと時をありがとうございました。


最終的な結果は1月29日に出るようです。

Material Design GuideのListsを読んだ。

そろそろMaterial Designについても知りたいなぁと思ってきたので、Material Designのサイトの気になるところから読んでいる。
今日はListsとLists: Controlを読んだ。
Lists - Components - Google design guidelines
Lists: Controls - Components - Google design guidelines
そこで初めて知ったり、覚えておこうと思ったものを少しメモしておく。
引用の英文を訳しているけど、雰囲気で訳しているので英文と日本語の文は同じ意味じゃないと思う。

リストの要素のテキストの行数が3行より多い場合はCardを使う

If more than three lines of text need to be shown in list tiles, use cards instead.

リストの要素の一番目立つコンテンツが画像ならグリッドリストを使う

If the primary distinguishing content consists of images, use a grid list.

リストの要素の中で最も目立つものは左に置き、最も目立つテキストは最初の行に書く

Bias the most distinguishing content in a tile towards the left of the tile. In tiles with mutli-line content, place the most distinguishing content in the first line.

とりあえず以上。
googleさんのドキュメント量はすごいなぁ。