Noq

ノーク

非常に重要です!この言語は進行中です!予告なしにいつでも変更される可能性があります。この言語はご自身の責任で使用してください。

コックではありません。 Coq ではない単純な式トランスフォーマー。

クイックスタート

$ cargo run ./examples/peano.noq 

本旨

主なアイデアは、シンボリック代数式の変換ルールを定義し、それらを順次適用できるようにすることです。

表現

現在の式の構文は大まかに次のように定義できます。

 <expression> ::= <operator-0>
<operator-0> ::= <operator-1> ((`+` | `-`) <operator-0>)*
<operator-1> ::= <operator-2> ((`*` | `/`) <operator-1>)*
<operator-2> ::= <primary> (`^` <operator-2>)*
<primary> ::= (`(` <expression> `)`) | <application-chain> | <symbol> | <variable>
<application-chain> ::= (<symbol> | <variable>) (<fun-args>)+
<symbol> ::= [a-z0-9][_a-zA-Z0-9]*
<variable> ::= [_A-Z][_a-zA-Z0-9]*
<fun-args> ::= `(` (<expression>),* `)`

ルールと形

言語の 2 つの主要なエンティティは、ルールとシェイプです。ルールはパターン (ヘッド) とそれに対応する置換 (ボディ) を定義します。ルール定義の構文は次のとおりです。

 <name:symbol> :: <head:expression> = <body:expression>

以下は、ペアの要素を交換するルールの例です。

 swap :: swap(pair(A, B)) = pair(B, A)

シェーピングは、式にルールを順次適用して、別の式に変換するプロセスです。シェーピングには次の構文があります。

 <expression> {
  ... sequence of rule applications ...
}

たとえば、上で定義したswapルールを使用して式swap(pair(f(a), g(b)))を整形する方法を次に示します。

 swap(pair(f(a), g(b))) {
  swap | all
}

この整形の結果はpair(g(b), f(a))です。

匿名ルール

整形に使用するルールを定義する必要はありません。

 swap(pair(f(a), g(b))) {
  swap(pair(A, B)) = pair(B, A) | all
}