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(pair(f(a), g(b))) с помощью правила swap определенного выше:

 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
}