この記事はF# Advent Calendar 2020の 17 日目の記事です1。
# 概要
F*は、プログラム検証を目的とした関数型プログラミング言語です。 プログラム検証のために篩型などの機能を搭載しており、 バックエンドの SMT ソルバとしてZ3を使用するという特徴があります。
この記事ではF*処理系のコードを流用して
F*コードをパーズしてみます。ここではそれ以上踏み込みませんが、
このパーズ結果を利用してz3rlimitなどの F*のオプションを最適なものに変更するツールを
作成することができました。
# ビルド
F*の処理系は特殊な構成になっていて、内部のコードが OCaml と F#の双方で書かれています2。
いま必要なパーザのコードも、F#用の構文定義ファイル（parse.fsy）と
OCaml 用の構文定義ファイル（parse.mly）が併存しています。
今回はこの F#用のファイル群を使用します。
パーザのコードはsrc/parser以下に配置されています。
またこれらのコードはsrc/basicにも依存しています。
これらのファイル群をどのようにビルドすればよいかは、各々のディレクトリに含まれている
.fsprojファイルを読むとおおよそわかります。
ということで次のような.fsprojファイルを書きます。
なお、同じディレクトリにFStarという名前で F*の GitHub レポジトリがあるものとしています。
<Project Sdk="Microsoft.NET.Sdk">
<PropertyGroup>
<OutputType>Exe</OutputType>
<TargetFramework>net5.0</TargetFramework>
</PropertyGroup>
<ItemGroup>
<Compile Include="FStar/src/basic/basetypes-fake.fs" />
<Compile Include="FStar/src/basic/prims-fake.fs" />
<Compile Include="FStar/src/basic/st-fake.fs" />
<Compile Include="FStar/src/basic/exn-fake.fs" />
<Compile Include="FStar/src/basic/all-fake.fs" />
<Compile Include="FStar/src/basic/mul-fake.fs" />
<Compile Include="FStar/src/basic/fs/char.fsi" />
<Compile Include="FStar/src/basic/fs/char.fs" />
<Compile Include="FStar/src/basic/boot/FStar.BigInt.fsi" />
<Compile Include="FStar/src/basic/boot/NotFStar.BigInt.fs" />
<Compile Include="FStar/src/basic/boot/FStar.String.fsi" />
<Compile Include="FStar/src/basic/boot/FStar.String.fs" />
<Compile Include="FStar/src/basic/boot/FStar.List.fsi" />
<Compile Include="FStar/src/basic/boot/FStar.List.fs" />
<Compile Include="FStar/src/basic/boot/FStar.Util.fsi" />
<Compile Include="FStar/src/basic/boot/NotFStar.Util.fs" />
<Compile Include="FStar/src/basic/boot/FStar.Compiler.Bytes.fsi" />
<Compile Include="FStar/src/basic/boot/NotFStar.Compiler.Bytes.fs" />
<Compile Include="FStar/src/basic/boot/FStar.Dyn.fsi" />
<Compile Include="FStar/src/basic/boot/NotFStar.Dyn.fs" />
<Compile Include="FStar/src/basic/boot/FStar.StringBuffer.fsi" />
<Compile Include="FStar/src/basic/boot/FStar.StringBuffer.fs" />
<Compile Include="FStar/src/basic/FStar.Platform.fsi" />
<Compile Include="FStar/src/basic/NotFStar.Platform.fs" />
<Compile Include="FStar/src/basic/FStar.Thunk.fsi" />
<Compile Include="FStar/src/basic/FStar.Thunk.fs" />
<Compile Include="FStar/src/basic/FStar.Common.fs" />
<Compile Include="FStar/src/basic/FStar.Getopt.fsi" />
<Compile Include="FStar/src/basic/NotFStar.Getopt.fs" />
<Compile Include="FStar/src/basic/FStar.VConfig.fs" />
<Compile Include="FStar/src/basic/FStar.Options.fsi" />
<Compile Include="FStar/src/basic/FStar.Options.fs" />
<Compile Include="FStar/src/basic/FStar.Range.fsi" />
<Compile Include="FStar/src/basic/FStar.Range.fs" />
<Compile Include="FStar/src/basic/FStar.Ident.fsi" />
<Compile Include="FStar/src/basic/FStar.Ident.fs" />
<Compile Include="FStar/src/basic/FStar.Unionfind.fsi" />
<Compile Include="FStar/src/basic/NotFStar.Unionfind.fs" />
<Compile Include="FStar/src/basic/FStar.Const.fs" />
<Compile Include="FStar/src/basic/FStar.Order.fs" />
<Compile Include="FStar/src/basic/FStar.Errors.fs" />
<Compile Include="FStar/src/basic/FStar.Profiling.fsi" />
<Compile Include="FStar/src/basic/FStar.Profiling.fs" />
<Compile Include="FStar/src/basic/FStar.Version.fsi" />
<Compile Include="FStar/src/basic/FStar.Version.fs" />
<Content Include="FStar/src/basic/packages.config" />
<FsLex Include="FStar/src/parser/lex.fsl">
<OtherFlags>--unicode</OtherFlags>
</FsLex>
<Compile Include="FStar/src/parser/FStar.Parser.Const.fs" />
<Compile Include="FStar/src/parser/FStar.Parser.AST.fs" />
<Compile Include="FStar/src/parser/parseutil.fs" />
<FsYacc Include="FStar/src/parser/parse.fsy">
<OtherFlags>--module FStar.Parser.Parse --open FStar.Parser.AST</OtherFlags>
</FsYacc>
<Compile Include="parse.fs" />
<Compile Include="FStar/src/parser/FStar.Parser.Lexhelp.fs" />
<Compile Include="lex.fs" />
<Compile Include="FStar/src/parser/FStar.Parser.ParseIt.fsi" />
<Compile Include="FStar/src/parser/NotFStar.Parser.ParseIt.fs" />
<Compile Include="FStar/src/parser/FStar.Parser.Driver.fs" />
<Compile Include="Program.fs" />
</ItemGroup>
<ItemGroup>
<PackageReference Include="FSharp.Compatibility.OCaml" Version="0.1.14" />
<PackageReference Include="FsLexYacc" Version="10.2.0" />
</ItemGroup>
</Project>
src/parser/lex.fslとsrc/parser/parse.fsyがそれぞれ字句・構文の定義ファイルになっていて、
FsLexYacc でコンパイルしてから F#コンパイラに入力する必要があります。
これを行うために<FsLex>と<FsYacc>を使っています。
さて F*処理系は .NET Framework を想定しているため .NET Core ではビルドできません。
そこでこれを .NET Core に対応させる作業を行います。
その作業の内容はフォークした GitHub レポジトリにおきました。
ほとんどのコードは型情報を追加したり名前空間をいじったりすることで対応できますが、
json_of_stringとstring_of_jsonに関しては
.NET Framework にのみ存在する System.Web.Script.Serialization.JavaScriptSerializer を
使用しているため容易ではありません。これらの関数はパーザ内部では使われていないようなので、
とりあえずコメントアウトして対応しました。
# 実行
以上の編集で（大量の警告を吐きながらも）ビルドが通るようになりました。
適当な F*コード（Hello.fst）を用意して、次のように F*のパーザを F#から呼び出すと、
無事対応する AST が得られます。
[<EntryPoint>]
let main args =
let ast, _ =
FStar.Parser.Driver.parse_file "Hello.fst"
printfn "%A" ast
0
$ cat Hello.fst # このファイルはF* GitHub repoのexamples/helloより取得
(*
Copyright 2008-2018 Microsoft Research
Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at
http://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
*)
module Hello
open FStar.IO
let main = print_string "Hello F*!\n"
$ dotnet run
Module
({ ns = []
ident = { idText = "Hello"
idRange = { def_range = { file_name = "Hello.fst"
start_pos = { line = 16
col = 7 }
end_pos = { line = 16
col = 12 } }
use_range = { file_name = "Hello.fst"
start_pos = { line = 16
col = 7 }
end_pos = { line = 16
col = 12 } } } }
nsstr = ""
str = "Hello" },
[{ d =
TopLevelModule
{ ns = []
ident = { idText = "Hello"
idRange = { def_range = { file_name = "Hello.fst"
start_pos = { line = 16
col = 7 }
end_pos = { line = 16
col = 12 } }
use_range = { file_name = "Hello.fst"
start_pos = { line = 16
col = 7 }
end_pos = { line = 16
col = 12 } } } }
nsstr = ""
str = "Hello" }
drange =
{ def_range = { file_name = "Hello.fst"
start_pos = { line = 16
col = 0 }
end_pos = { line = 16
col = 12 } }
use_range = { file_name = "Hello.fst"
start_pos = { line = 16
col = 0 }
end_pos = { line = 16
col = 12 } } }
quals = []
attrs = [] };
{ d =
Open
{ ns = [{ idText = "FStar"
idRange = { def_range = { file_name = "Hello.fst"
start_pos = { line = 18
col = 5 }
end_pos = { line = 18
col = 10 } }
use_range = { file_name = "Hello.fst"
start_pos = { line = 18
col = 5 }
end_pos = { line = 18
col = 10 } } } }]
ident = { idText = "IO"
idRange = { def_range = { file_name = "Hello.fst"
start_pos = { line = 18
col = 11 }
end_pos = { line = 18
col = 13 } }
use_range = { file_name = "Hello.fst"
start_pos = { line = 18
col = 11 }
end_pos = { line = 18
col = 13 } } } }
nsstr = "FStar"
str = "FStar.IO" }
drange =
{ def_range = { file_name = "Hello.fst"
start_pos = { line = 18
col = 0 }
end_pos = { line = 18
col = 13 } }
use_range = { file_name = "Hello.fst"
start_pos = { line = 18
col = 0 }
end_pos = { line = 18
col = 13 } } }
quals = []
attrs = [] };
{ d =
TopLevelLet
(NoLetQualifier,
[({ pat =
PatVar
({ idText = "main"
idRange = { def_range = { file_name = "Hello.fst"
start_pos = { line = 20
col = 4 }
end_pos = { line = 20
col = 8 } }
use_range = { file_name = "Hello.fst"
start_pos = { line = 20
col = 4 }
end_pos = { line = 20
col = 8 } } } },
None)
prange =
{ def_range = { file_name = "Hello.fst"
start_pos = { line = 20
col = 4 }
end_pos = { line = 20
col = 8 } }
use_range = { file_name = "Hello.fst"
start_pos = { line = 20
col = 4 }
end_pos = { line = 20
col = 8 } } } },
{ tm =
App
({ tm =
Var
{ ns = []
ident = { idText = "print_string"
idRange = { def_range = { file_name = "Hello.fst"
start_pos = { line = 20
col = 11 }
end_pos = { line = 20
col = 23 } }
use_range = { file_name = "Hello.fst"
start_pos = { line = 20
col = 11 }
end_pos = { line = 20
col = 23 } } } }
nsstr = ""
str = "print_string" }
range =
{ def_range = { file_name = "Hello.fst"
start_pos = { line = 20
col = 11 }
end_pos = { line = 20
col = 23 } }
use_range = { file_name = "Hello.fst"
start_pos = { line = 20
col = 11 }
end_pos = { line = 20
col = 23 } } }
level = Un },
{ tm =
Const
(Const_string
("Hello F*!
",
{ def_range = { file_name = "Hello.fst"
start_pos = { line = 20
col = 24 }
end_pos = { line = 20
col = 37 } }
use_range = { file_name = "Hello.fst"
start_pos = { line = 20
col = 24 }
end_pos = { line = 20
col = 37 } } }))
range =
{ def_range = { file_name = "Hello.fst"
start_pos = { line = 20
col = 24 }
end_pos = { line = 20
col = 37 } }
use_range = { file_name = "Hello.fst"
start_pos = { line = 20
col = 24 }
end_pos = { line = 20
col = 37 } } }
level = Expr }, Nothing)
range =
{ def_range = { file_name = "Hello.fst"
start_pos = { line = 20
col = 11 }
end_pos = { line = 20
col = 37 } }
use_range = { file_name = "Hello.fst"
start_pos = { line = 20
col = 11 }
end_pos = { line = 20
col = 37 } } }
level = Un })])
drange =
{ def_range = { file_name = "Hello.fst"
start_pos = { line = 20
col = 0 }
end_pos = { line = 20
col = 37 } }
use_range = { file_name = "Hello.fst"
start_pos = { line = 20
col = 0 }
end_pos = { line = 20
col = 37 } } }
quals = []
attrs = [] }])
AST の各要素はFStar.Parser.ASTで定義されています。
基本的には根からパターンマッチと再帰をしつつたどっていくと、
必要な情報を得られます。詳細はリンク先のコードを参考にしてください。
-
12 月 18 日になってから書き始めたため、記事の日付とはずれています。 ↩︎
-
ただしビルドなどに使われているのは OCaml コードだけのようです。GitHub の Issue にもこの問題が取り上げられていますがいまのところ F#のサポートを落とすつもりは無いようです。 ↩︎
