Undecided

Agdaでかけ算の交換法則を Day2-answer.agda を参考に書きました。というかそのまんま。名前は Programming Language Foundations in Agda に合わせたつもりです。理解のためになるべくていねいに書こうと思ったんですが、 *-suc と *-comm をばらそうとするとエラーになってしまってめんどくさくなってしまいました。 *-suc は先にlemmaが必要なんだろうな。 *-comm は「あっているはずなのに」と思うんですが通らない。基本がわかってないんですよね。 refl はたんに計算するだけで、 rewrite は suc n を n にしたらいいのかと思うんですけど。まあ、いちおう C-c, C-l で通ります。 import Relation.Binary.PropositionalEquality as Eq open Eq using (_≡_; refl; cong; sym) open Eq.≡-Reasoning using (begin_; _≡⟨⟩_; step-≡; _∎) infixl 6 _+_ infixl 7 _*_ data ℕ : Set where zero : ℕ suc : ℕ → ℕ _+_ : ℕ → ℕ → ℕ zero + n = n (suc m) + n = suc (m + n) +-assoc : ∀ (m n p : ℕ) → (m + n) + p ≡ m + (n + p) +-assoc zero n p = begin (zero + n) + p ≡⟨⟩ n + p ≡⟨⟩ zero + (n + p) ∎ +-assoc (suc m) n p = begin (suc m + n) + p ≡⟨⟩ suc (m + n) + p ≡⟨⟩ suc ((m + n) + p) ≡⟨ cong suc (+-assoc m n p) ⟩ suc (m + (n + p)) ≡⟨⟩ suc m + (n + p) ∎ +-identityʳ : ∀ (m : ℕ) → m + zero ≡ m +-identity

おれおれマークダウンのスクリプトをスッキリさせたのだけど、元のマークダウンを埋め込む機能を入れたら、またごちゃごちゃになってしまいました。KISSの原則とか言うけど、このまま使い続けるかわからないコードまでは整理しないよね。自分しか使わないし。 ついでに変換のRubyコードもつっこんだ。大きくなりすぎるから悩んだけど、まあ大したことはないよね。ファイルを分割しないモチベーションが増えてしまった。 JavaScriptをひさびさにいじって楽しかった。昔には無かった便利機能がたくさんでかなり楽になっている。もうJavaScriptじゃないのか。 JavaScriptがからんでくるとアクセシビリティが気になってくるけど、まだそこまでいけてない。 そろそろ数学ネタもやらないとだな。まあ、思いついたところから。 自分の必要な機能をプログラミングするのは楽しいね。 ∨ Source markdown おれおれマークダウンに元のマークダウンと変換スクリプトの埋め込み機能の追加 おれおれマークダウンのスクリプトをスッキリさせたのだけど、元のマークダウンを埋め込む機能を入れたら、またごちゃごちゃになってしまいました。KISSの原則とか言うけど、このまま使い続けるかわからないコードまでは整理しないよね。自分しか使わないし。 ついでに変換のRubyコードもつっこんだ。大きくなりすぎるから悩んだけど、まあ大したことはないよね。ファイルを分割しないモチベーションが増えてしまった。 JavaScriptをひさびさにいじって楽しかった。昔には無かった便利機能がたくさんでかなり楽になっている。もうJavaScriptじゃないのか。 JavaScriptがからんでくるとアクセシビリティが気になってくるけど、まだそこまでいけてない。 そろそろ数学ネタもやらないとだな。まあ、思いついたところから。 自分の必要な機能をプログラミングするのは楽しいね。 ∨ Source code # coding: utf-8 require 'optparse' require 'open3' require 'strscan' $lib = "" class Context attr_reader :

今まではブロックの種類ごとにクラスを作っていたのですが、いちいち作るのもめんどうなので、全部まとめることにしました。最初はコードを表示していただけだったんですよね。 main.rb class Code < BlockState HEADER = '<pre style="overflow-x: scroll;padding: 1px 1px 1px 3px;border:1px solid black;margin-top: 0;"><code>' FOOTER = "</code></pre>" def start if !filename.nil? then printf "<div style=\"border: 1px solid black;padding-left: 3px;margin-bottom: 0;\">#{filename}</div>" end printf self.class::HEADER end attr_accessor :comp_lang, :filename def process(line) line.gsub!('&', "&amp;") line.gsub!('<', "&lt;") line.gsub!('>', "&gt;") puts line end end それを$LaTeX$、Ruby、PlantUMLのコードをソースと共に処理するようにしたら、ぐちゃぐちゃになってしまいました。 ```{math, echo=true, eval=true} e=mc^2 ``` Ruby ```{ruby, echo=true, eval=true} puts "test" puts "test" ``` ```{lib, include=fal

どう考えてもincludeは必要だろうと思ってはいたのですが、めんどくさくて後回しにしていました。でも、書いてみたらたったの3行！エラー処理とかすっ飛ばしていますが。 ``` end: ``` lang: filename: option: elsif md = line.match(/^! *include +(.*)/) then file = File.open(md[1]) puts file.read ``` end: ``` lang: filename: option: これで !include test.svg と書いて、 となります。 これでRを利用できるようになりました。 ``` end: ``` lang: filename: option: PlantUMLは Open3.popen3("java -jar /mnt/d/app/plantuml.jar -pipe -svg -charset UTF-8") do |i, o, e, w| とかやっているのですが、Rはいろいろ調べたけどパイプ経由では実行できないみたいなんですよね。Rubyから叩こうと思うと、いったんファイルに書き出して、それを実行して、できたファイルを読み込むしかなさそう。 ファイルが複数になると管理がめんどうなので、なるべく1つのファイルに押し込めたいんですけど。

Google日本語入力の変換キー設定を考えていたら頭がごちゃごちゃしてきたので整理しました。まず、設定で選べるのは 直接入力 入力文字なし 変換前入力中 変換中 サジェスト表示中 サジェスト選択中 の6種類です。設定がそうなっているからだろうけど、サジェストの無い変換前入力中は無い気がします。 最初は変換キーでサジェストのトップを選択にしていたのですが、入力中に英数とかなを切り替えられないと「Google日本語入力」のような単語を覚えさせられないのでリターンキーにしました。そのまま確定よりも頻度が高いので。そのため、これを書きながら誤変換の嵐です。助詞の「は」や「に」を入力してリターンキーを押してしまいます。慣れるしかないですね。 サジェストのトップを活用しようとすると、サジェストを選択してCtrl-Deleteでサジェストから削除が必要になりますね。asdfキーで即確定しないのはこれがあるからですかね？ だいたい整理はついたので、あとは慣れるだけです。 直接入力 かな入力文字なし 英数入力文字なし かな変換前入力中 英数変換前入力中 かな変換前入力中かつサジェスト表示中 英数変換前入力中かつサジェスト表示中 サジェスト選択中 変換中 確定 変換キー シフト＋変換キー シフト＋変換キー 変換キー 文字入力 文字入力 シフト＋変換キー 変換キー サジェスト表示 サジェスト表示 シフト＋変換キー 変換キー サジェスト選択↓or↵ サジェスト選択↓or↵ 変換space 変換space 確定shift+↵ 確定shift+↵

自分なりの新下駄配列が落ち着いてきました。いじったのなら、もう新下駄配列じゃないだろうというのは置いておきます。 最初は練られているデフォルトのまま使うのがいいだろうと思っていたのですが、ErgoDox EZでは使いづらくて、少しいじりました。そこからは、少しもたくさんも一緒だろうということで、いじりまくることになりました。 最初は 「して」「いて」が押しにくいので「て」と「ぶ」の入れ替え。 「げ」が打ちにくいので「ちぇ」と入れ替え。 だけのつもりでした。 次にGoogle日本語入力の「句読点変換」が使えないことに気がつきました。句読点変換だと行末以外なら、変換の結果が正しければリターンキー1つお得です。最初はあきらめたのですが、単打でなければ問題は出ないことに気がついたので、 「、」と「も」の入れ替え 「。」と「え」の入れ替え をしました。理由があって単打にしているものを動かしたら、もうなんでもありです。 次はそんなに頻度が高くないくせに単打を占有している「ぐ」と「ば」です。これは「て」と一緒に移動してきていた「わ」「せ」と交換しました。でも、小指下段のシフト面は押しにくかったので、さらに「ぐ」「ば」を「ぺ」「ぱ」と入れ替えました。 最後は覚えにくい頻度の低いものを整理しました。 右下に集まった「ぱ行」を「べ」も移動して並べる。 左下の「ざ行」をなんとなく「ざじづぜぞ」と覚えやすく並べる。「ず」じゃないんですけどね。 「しぇ」「じぇ」と「うぃ」「うぇ」「うぉ」を固める。 これで覚えやすくなりました。 あと気になっているのは、タイムアウト時間が50msだとシビアなのと、Google日本語入力の変換の際の運指ですかね。キーマップはこれで完成の予定。

Google日本語入力用の新下駄配列のローマ字テーブルをいじるのがつらいのでCSVから生成するプログラムをRubyで書きました。書き始めてしまえば早いんですよね。CSVは自分用なのでけっこういじってあります。デフォルトのものはありません。記号とかはほとんど使わないので省いてありますが、fとjに割り当てているやつは書けばいけるんじゃないかな？ ``` end: ``` lang: filename: option: キー,単打,k,l,i,o,s,d,f,j 1,1,ぁ,ゃ,ゅ,ょ,,,, 2,2,ぃ,みゃ,びゃ,ぴゃ,,,, 3,3,ぅ,みゅ,びゅ,ぴゅ,,,, 4,4,ぇ,みょ,びょ,ぴょ,,,, 5,5,ぉ,ゎ,゛,゜,,,, 6,6,,,,,・,…,, 7,7,,,,,,,, 8,8,,,,,,,, 9,9,,,,,,,, 0,0,,,,,,,, q,ー,ふぁ,ぢ,ひゅ,りゅ,,,, w,に,ご,め,しゅ,じゅ,,,, e,は,ふ,け,しょ,じょ,,,, r,も,ふぃ,てぃ,きゅ,ぎゅ,,,, t,ち,ふぇ,でぃ,ちゅ,にゅ,,,, y,わ,,,,,しぇ,じぇ,, u,せ,,,,,ぐ,ば,, i,こ,,,,,ど,よ,, o,が,,,,,や,み,, p,ひ,,,うぉ,ちぇ,うぃ,うぇ,, a,の,ほ,を,ひょ,りょ,,,, s,と,じ,さ,,,,,, d,か,れ,お,,,,,, f,ん,、,り,きょ,ぎょ,,,, g,っ,ゆ,ず,ちょ,にょ,,,, h,く,,,,,び,へ,, j,う,,,,,ら,あ,, k,い,,,,,,,, l,し,,,,,,,, ;,な,,,,,そ,。,, z,す,ぞ,ぜ,ひゃ,りゃ,,,, x,ま,づ,ざ,゙,゜,,,, c,き,ぼ,ぎ,しゃ,じゃ,,,, v,る,む,ろ,きゃ,ぎゃ,,,, b,つ,ふぉ,ぬ,ちゃ,にゃ,,,, n,ぶ,,,,,げ,ゔ,, m,た,,,,,だ,ね,, ",",で,,,,,べ,ぱ,, .,え,,,,,ぴ,ぷ,, /,て,,,,,ぺ,ぽ,, ``` end: ``` lang: filename: option: # coding: utf-8 require 'csv' def main filename = "romantable

ほとんど お気楽 Haskell プログラミング入門 の 電卓プログラムの作成 をRubyに直しただけのものです。括弧も単項演算子も使えませんが、それゆえにシンプルでわかりやすいと思います。字句解析して、構文木を作って、評価するだけです。これさえ理解してしまえば、あとは肉付けして機能を追加していくだけで自作言語のできあがりです。 ``` end: ``` lang: filename: option: require 'strscan' class Token attr_accessor :type attr_accessor :obj def initialize(type, obj) @type = type @obj = obj end end class Expr attr_accessor :type attr_accessor :expr1 attr_accessor :expr2 def initialize(type, expr1, expr2) @type = type @expr1 = expr1 @expr2 = expr2 end end def main if ARGV.size != 1 then puts "Usage: ruby lang.rb 'parse string'" end tokenArray = lexer(ARGV[0]) p tokenArray if tokenArray == "error" then puts "Error: lexer" return end expr = getParseTree(tokenArray) p expr if expr == "error" then puts "Error: getParseTree" return end ret = evalExpr(expr) p ret if expr == "error" then