Yokohama.vim #8に行って来た。
Yokohama.vimに初参加して来ました。
@gu4さんによる挨拶
最初にYokohama.vimとVimの軌跡の比較をしていた。 スライドに記載していたはずのYokohama.vimの軌跡が残念ながら消えてたらしい :( Yokohama.vim #0は2010年から続いているみたい。 Yokohama.vim.osaka? #7には自分は大阪(Osaka.vim #6)から参加していたなぁとか思ってた。
そういえば10/29(土)にOsaka.vim #8があるそうです。関西の方は是非!
次にアイスブレイクとして、自己組織化ゲームをした。 指示役と移動役という役割を持った二人一組で行うゲーム。 指示役が「前」といえば、移動役が一歩前に歩くといった感じ。 複数のチームの中でどのチームが一番多く歩けるかというのがゲームに対するモチベーションだった。
今回はVimバージョンということで、指示役が行う指示はhjklだった。 自分の相手は@h0k0r0biさんで、指示役をやらせていただいた。 指示を出すとき、慣れるまでhが左でlが右ということがすっと出てこなかった。 Vim上でカーソルを移動する際におそらくhとかlとかを考えずに指が覚えているからだろうなぁと思った。 このゲームではhjkl以外のmapを使用可能だった。自分たちは特に使用しなかったけど ゲーム中に「gg」とか聞こえて来た気がする。
改めて@h0k0r0biさんありがとうございました。
@Watson_DNAさんの発表
TeXとVim scriptのクイックソートを比較していた。 TeXもVim scriptも遅いねという感じだった。
@Linda_ppさんの発表
すごいということしかわからなかったのだけれど、CコンパイラをVim scriptで作成したいという話だったと思う。すごい。
@thincaさんによるVim 8.0の機能の説明
:help version-8.0の内容を@thincaさんが解説するという急遽開催されたもの。 色々便利なものがあったけど、まだ自分は全然把握できていないので復習をする必要がありそう。
したこと
特に何もせずに話を聞いたり、少しもくもくしたり、TweetVimを始めたりしていた。
所感
Yokohama.vimは初参加だったけど、わいのわいのした感じで楽しかった。 ただ、vimrc読書会でお会いする方々に話しかけたい気もしたけど、人見知りなので話しかけれなかったのが残念だった(これは自分の問題だけれども)。 また参加する時にはお邪魔したいと思います。
Vim 8.0にした。
先々週9/12にVim 8がリリースされたので、だいぶ遅れたがVim 8をインストールした。 今回はソースコードビルドに挑戦してみたので、そのメモを書きます。 何気にソースコードビルドは初挑戦(お恥ずかしいことに今までVim 7.4.729を使っていた...)。
やり方
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
とすれば良いかと思います。
感想
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を勉強していて、VimでOCamlを書いてます。その時に標準ライブラリの機能を調べたいなと思うのだけれど、いちいちブラウザで調べるのも面倒なのでVim pluginを作りました。
使い方は
: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を取得しています。
あとはVital.Web.HTTPとVital.Web.XMLを用いてスクレイピングをしている感じです。
これらの方法はmattnさんのブログを見て作成をしました。
今後
まだ出力結果が見づらいので、そこを変更したい。また、コマンド実行時にVimをブロックしてしまうので非同期処理にしたいなと考えています。
TaPL 演習3.5.14
問題
定理3.5.4が算術演算の評価関係に関しても成り立つことを示せ。
すなわち、 かつ ならば であることを示せ。
証明
の導出に関する帰納法を使用し、 の導出で最後に使った規則に対する場合分けにより証明する。
E-SUCCの場合
は という形であり、またある が存在して である。
左側の最も外側に を用いている規則はE-SUCCのみである。
よって、 の導出で最後に使った規則もE-SUCCであり、ある が存在して である。
帰納法の仮定より、 。
したがって、
E-PREDZEROの場合
は という形であり、 である。 左側の最も外側に を用いている規則はE-PREDZERO、E-PREDSUCCとE-PREDの3つであるので の導出の最後に使った規則はこのうちのいずれかである。 の導出で最後に使った規則はE-PREDではない。 E-PREDであれば、ある が存在して となるが、0は値なので、評価されないからである。 E-PREDSUCCの場合、 となるが、 であるのでE-PREDSUCCでもない。 よって、 の導出の最後に使った規則はE-PREDZEROであり、 となる。
E-PREDSUCCの場合
は という形であり、 である。 と同様の推論により、 の導出の最後に使った規則はE-PREDSUCCであることがわかる。 よって、 となる。
E-PREDの場合
は という形であり、ある が存在して である。 (ii)と同様の推論により、 の導出で最後に使った規則がE-PREDであることがわかる。 このとき、ある が存在して、 である。 帰納法の仮定より、。 よって、
E-ISZEROZEROの場合
は という形をしており、である。 左側の最も外側に を用いている規則はE-ISZEROZERO、E-ISZEROSUCC、E-ISZEROがあるが と0は異なるので、 の導出で最後に使った規則はE-ISZEROSUCCではない。 また、E-ISZEROでもない。なぜなら、E-ISZEROであれば、ある が存在して となるが 0は値なので評価されないからである。 よって の導出で最後に使った規則はE-ISZEROZEROであり、
E-ISZEROSUCCの場合
は という形をしており、 である。 と同様の推論で、 の導出で最後に使った規則がE-ISZEROSUCCであることがわかる。 よって、
E-ISZEROの場合
は という形をしており、ある が存在して である。 と同様の推論により、 の導出で最後に使った規則がE-ISZEROであることがわかる。 このとき、ある が存在して、 である。 帰納法の仮定より、。 よって、
以上より、 かつ ならば である。
所感
解答に書いている通り、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が入っているようにも見えるので、初心者はハマるかもなぁという感想です。
ほぼすべてサイ本の内容そのままという感じですが、自分でまとめると ちゃんとわかっているかの確認になってよいなという感じです。 今後もまたサイ本を読んで気になった箇所の記事を書きたいと思います。