本記事はLabBase テックカレンダー Advent Calendar 2024 19 日目です。
概要
Leanは関数型パラダイムを持ちなおかつ定理証明支援系で、強力なメタプログラミング機能をそなえたという変わった言語です。
本記事ではLeanを書いている最中にもシェルを叩けるように、Leanのメタプログラミング機能のElaborationをつかって、Leanのソースコード内で使える簡単なコマンドを自作します。
Elaborationとは
Leanは普通の関数型言語であり、なおかつ定理証明支援系でもある大変パワフルな言語です。
今回使用するElaborationという機能はLeanのパワフルさの源になっている機能で、要はコンパイラの機能をそのまま自由に使うことができます。（実はコンパイラが文法に意味を与えるプロセスはElaborationそのものです）
今回つかうコマンドのElaborationの他に、タクティク用、term用のElaborationがありますが、今回はコマンドのElaborationを使います。
"hello!"だけ出力するコマンド
前準備としてhelloだけ出力するコマンドを定義します。
import Lean
open Lean Elab
elab "#hello" : command => do
logInfo "hello!"
import、openはElaboration用の標準パッケージElabをインポートするコマンドです。新しくElaborationを定義するときは、これらのパッケージにあるelabコマンドを使って定義します。
"#hello"は今回つくるコマンドの名前で、ソースコードに書く実体はこれです。また今回はコマンドのElaborationなので: commandによってコマンドであることを示します。
logInfoはLeanを書いている最中にいつでも見れるInfo viewに、ログとして文字列を出力できる関数です。
このように定義したコマンド#helloは、定義した場所以降にそのまま書くことで使用できます。
（Leanでは、インタープリターのようなCLIの対話環境の代わりに、対話的に使える補助コマンドと、定義された変数や関数・ログなどの情報を表示するinfo view（および言語サーバー）によって開発できます。手軽さ的にはJupyter Notebookなどに近いです）
import Lean
open Lean Elab
elab "#hello" : command => do
logInfo "hello!"
#hello
-- info viewにログとして以下が表示される
hello!
ls -lの実行結果を出力するコマンド
次にls -lを実行するコマンドをつくっていきます。
import Lean
open Lean Elab
elab "#shell_ls" : command => do
let spawn_args: IO.Process.SpawnArgs := {cmd := "ls", args := #["-l"]}
let output <- IO.Process.output spawn_args
logInfo output.stdout
先程はlogInfo "hello!"だけだったelabの中身に、子プロセスの実行とその標準出力の表示が加わりました。
IO.Process.SpawnArgsは子プロセスとして実行したいシェルコマンドを表す構造体であり、フィールドにシェルコマンドを文字列として保持するcmdと、続く引数のargsを持ちます。
なので{cmd := "ls", args := #["-l"]}のように定義してspawn_argsに束縛します。
IO.Process.outputはIO.Process.SpawnArgsを子プロセスとして実際に実行する関数で、子プロセスの実行結果をoutputに束縛します。
あとはlogInfo output.stdoutで実行結果の標準出力をログに表示させれば、ls -lの実行結果を出力するコマンドの完成です。
#helloと同様、定義した場所以降に書くことで使用できます。
#shell_ls
-- info viewにログとして以下が表示される
Messages below (5)
43:0:
合計 28
drwxrwxr-x 2 denjiry denjiry 4096 9月 30 13:58 LightblueLean
-rw-rw-r-- 1 denjiry denjiry 161 12月 1 15:50 LightblueLean.lean
-rw-rw-r-- 1 denjiry denjiry 77 9月 30 03:46 Main.lean
-rw-rw-r-- 1 denjiry denjiry 16 9月 30 03:46 README.md
-rw-rw-r-- 1 denjiry denjiry 124 9月 30 13:54 lake-manifest.json
-rw-rw-r-- 1 denjiry denjiry 247 9月 30 03:46 lakefile.lean
-rw-rw-r-- 1 denjiry denjiry 24 9月 30 03:46 lean-toolchain
このように、ls -lを実行した結果を表示することができました。
任意のシェルのコマンドを実行するコマンド
最後に任意のシェルのコマンドを実行するコマンドを作ります。
#shell "wc" "README.md"
のような感じで、#shellコマンドのあとにシェルのコマンドを続けれるようにします。
import Lean
open Lean Elab
elab "#shell" s:str+ : command => do
let cmds := s.map TSyntax.getString
let (cmd, args) := (cmds[0]!, cmds[1:])
let cmd: IO.Process.SpawnArgs := {cmd, args}
let output <- IO.Process.output cmd
logInfo output.stdout
#shell_lsのコードに新たにs:str+が加わりました。
str+は正規表現で+が１個以上の繰り返しを表すのと似ていて、「１個以上の連続する文字列」という意味です。
すなわちs:str+は「１個以上の連続する文字列をsに束縛する」という意味になり、このコマンドを使用するときは#shellに続けて文字列を１個以上連続して続けるという形になります。
実際に#shellでwcをつかってREADME.mdの文字数をカウントしてみると次のようになります。
#shell "wc" "README.md"
-- info viewに以下が表示される
Messages below (5)
56:0:
0 2 16 README.md
またls -lなど、他のシェルコマンドも同様に動きます。
#shell "ls" "-l"
-- info viewに以下が表示される
Messages below (5)
43:0:
合計 28
drwxrwxr-x 2 denjiry denjiry 4096 9月 30 13:58 LightblueLean
-rw-rw-r-- 1 denjiry denjiry 161 12月 1 15:50 LightblueLean.lean
-rw-rw-r-- 1 denjiry denjiry 77 9月 30 03:46 Main.lean
-rw-rw-r-- 1 denjiry denjiry 16 9月 30 03:46 README.md
-rw-rw-r-- 1 denjiry denjiry 124 9月 30 13:54 lake-manifest.json
-rw-rw-r-- 1 denjiry denjiry 247 9月 30 03:46 lakefile.lean
-rw-rw-r-- 1 denjiry denjiry 24 9月 30 03:46 lean-toolchain
おわりに
本記事ではLeanの強力な機能であるElaborationを紹介し、子プロセスを実行するコマンドをどうやって定義するかについて、順を追って解説しました。
今回はIOの副作用が実行可能であることを利用して、子プロセスを実行するコマンドを定義しました。
しかしElaborationはユーザーが言語自体へ自由に介入することができる機能であり、今回は紹介できませんでしたが、IOの副作用以外にも、コンパイラが管理している様々な情報（定義されている変数や他のコマンドなど）の読み書きの副作用を扱うことができます。
したがって言語に関して想像できるようなことは、（気合があれば）なんでもできてしまう言語となっています。
最近は有志の方のおかげで日本語資料も読めるようになったので、興味のわいた方は新しいパラダイムのプログラミング言語としてLeanを勉強してみるのはいかがでしょうか
参考
Discussion