項の構文解析

ソートと演算の宣言の組を指標 (signature) と呼ぶ。指標は well-formed な項の集合を定義する。例えば、次の 3つはモジュール NAT+ で宣言された指標において well-formed な項である:

• 0
• s(s(0))
• s(s(s(0))) + s(s(s(s(0))))

次の二つは well-formed な項ではない:

• s(s(0)) 0
• s(s(s(0))) * s(s(0))

well-formed な項は、解析木 (parse tree) を持つ。コマンド parse は項 <term> の構文を解析する:

parse <term> .

構文解析の例:

自然数の仕様で宣言したモジュール NAT+ を使って、項 s(s(0)) + s(s(s(0))) を構文解析する。

最初に、select コマンドを使って、モジュール NAT+ を選択する:

CafeOBJ> select NAT+
NAT+> 

parse コマンドを使って項 s(s(0)) + s(s(s(0))) を構文解析する:

The prompt has been changed into the current selected module. Parse s(s(0)) + s(s(s(0))) by using the parse command as follows:

NAT+> parse s(s(0)) + s(s(s(0))) .
(s(s(0)) + s(s(s(0)))) : Nat
NAT+> 

parse コマンドで解析した結果、s(s(0)) + s(s(s(0))) はソート Nat 上の項であることがわかる。

曖昧な項

ある項が複数の構文木を持つとき、その項は曖昧であると呼ぶ。例えば、項 s(0) + s(s(0)) + s(s(s(0))) は曖昧な項の例である。このような項を入力すると parse コマンドは警告を出す:

NAT+> parse s(0) + s(s(0)) + s(s(s(0))) .
[Warning]: Ambiguous term:
* Please select a term from the followings:
[1] _+_ : Nat Nat -> Nat ---------------------((s(0) + s(s(0))) + s(s(s(0))))
[2] _+_ : Nat Nat -> Nat ---------------------(s(0) + (s(s(0)) + s(s(s(0)))))
* Please input your choice (a number from 1 to 2, default is 1)? 1
Taking the first as correct.
((s(0) + s(s(0))) + s(s(s(0)))) : Nat
NAT+> 

この項は 2つの構文木 (1 + 2) + 3 と 1 + (2 + 3) を持つので、CafeOBJ 処理系はユーザにどちらの解釈を取るべきか尋ねてくる。ここでは前者の解釈を正しいとするために、1 を入力している。本来は、このような曖昧さが現れないよう、あらかじめ括弧を付けるなど、注意深く項を入力する必要がある。

構文解析木の表示

parse コマンドに構文解析木を表示させるには、verbose スイッチを on にする。

verbose スイッチを on にするには、set コマンドを用いる:

NAT+> set verbose on
NAT+>

verbose スイッチを on にすると、parse コマンドは解析木を表示する:

NAT+> parse (s(0) + s(s(0))) + s(s(s(0))) .
((s(0) + s(s(0))) + s(s(s(0)))) : Nat
       _+_:Nat
     /          \
  _+_:Nat     s:Nat
  /      \      |
s:Nat  s:Nat  s:Nat
  |      |      |
0:Nat  s:Nat  s:Nat
         |      |
       0:Nat  0:Nat

NAT+> 

補足

モジュールの選択を解除するには、次のようにタイプする:

NAT+> select .
CafeOBJ> 

[Next] 簡約

Original Copyright © Takahiro Seino, all rights reserved.