情報は力ではない

UE4 とか Blender とか。

Vim 8.0にした。

先々週9/12にVim 8がリリースされたので、だいぶ遅れたがVim 8をインストールした。 今回はソースコードビルドに挑戦してみたので、そのメモを書きます。 何気にソースコードビルドは初挑戦(お恥ずかしいことに今までVim 7.4.729を使っていた...)。

やり方

gitからVimソースコードを持ってきます。

git clone https://github.com/vim/vim.git

あとは、READMEに従ってビルドするだけです。 自分はOS XユーザなのでREADMEdir/README_mac.txtを見ながら実施。

make
sudo make install

これでvim/src以下にVimの実行ファイルが出来ます。 あとは、VimにPATHを通すだけです。 例えば、~Vimをcloneしたのであれば.bashrcとかに

export PATH=~/vim/src/:$PATH

とすれば良いかと思います。

感想

ソースコードからVimをビルドするのは簡単。 これでVim活が捗る(はず)。

TaPL 演習4.2.2

問題

arithの実装におけるeval関数の定義を、大ステップスタイルに変えよ。

答案

もう少しうまく書きたい。

let rec eval1' t = 
  try
    match t with
      TmIf(_, t1, t2, t3) -> (
        let t1' = eval1'(t1) in
        match t1' with
          TmTrue(_)  -> let v2 = eval1'(t2) in v2
        | TmFalse(_) -> let v3 = eval1'(t3) in v3
        | _ -> raise NoRuleApplies)
    | TmSucc(fi, t1) when isnumericval t1 ->
        TmSucc(fi, eval1'(t1))
    | TmPred(_, t1) -> (
        let t1' = eval1'(t1) in
        match t1' with
          TmZero(_) -> t1'
        | TmSucc(_, nv1) when isnumericval nv1 -> nv1
        | _ -> raise NoRuleApplies)
    | TmIsZero(_, t1) -> (
        let t1' = eval1'(t1) in
        match t1' with
          TmZero(_) -> TmTrue(dummyinfo)
        | TmSucc(_, nv1) when isnumericval nv1 -> TmFalse(dummyinfo)
        | _ -> raise NoRuleApplies)
    | _ -> raise NoRuleApplies
  with NoRuleApplies -> t

感想

軽く試した感じは、ちゃんと動いてる。ただ正確に動くかどうかはCoq等で証明すべきなんだろうな。 あとは関数名をeval'とかにすべきだったかも。

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されることがないようだ。

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