Noq

Tidak

SANGAT PENTING! BAHASA INI ADALAH PEKERJAAN YANG DALAM PROGRES! APA SAJA DAPAT BERUBAH SETIAP SAAT TANPA PEMBERITAHUAN APAPUN! GUNAKAN BAHASA INI DENGAN RISIKO ANDA SENDIRI!

Bukan Coq. Transformator ekspresi sederhana yang BUKAN Coq.

Mulai Cepat

$ cargo run ./examples/peano.noq 

Ide Utama

Ide Utamanya adalah mampu mendefinisikan aturan transformasi ekspresi aljabar simbolik dan menerapkannya secara berurutan.

Ekspresi

Sintaks ekspresi saat ini dapat didefinisikan secara kasar seperti ini:

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

Aturan dan Bentuk

Dua entitas utama bahasa ini adalah Aturan dan Bentuk. Sebuah aturan mendefinisikan pola (kepala) dan substitusi yang sesuai (badan). Definisi aturan memiliki sintaks berikut:

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

Berikut adalah contoh aturan yang menukar elemen dari suatu pasangan:

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

Pembentukan adalah proses penerapan aturan secara berurutan pada suatu ekspresi yang mengubahnya menjadi ekspresi yang berbeda. Pembentukan memiliki sintaks berikut:

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

Misalnya, inilah cara Anda membentuk ekspresi swap(pair(f(a), g(b))) dengan aturan swap yang ditentukan di atas:

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

Hasil pembentukan ini adalah pair(g(b), f(a)) .

Aturan anonim

Anda tidak perlu menentukan aturan untuk menggunakannya dalam pembentukan:

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