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>),* `)`

規則和形狀

語言的兩個主要實體是規則和形狀。規則定義模式（頭部）及其對應的替換（主體）。規則定義有以下語法：

 <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
}