Noq

Nr

EXTREM WICHTIG! DIESE SPRACHE IST IN ARBEIT! ALLES KANN SICH JEDERZEIT OHNE VORANKÜNDIGUNG ÄNDERN! BENUTZEN SIE DIESE SPRACHE AUF EIGENE GEFAHR!

Nicht Coq. Einfacher Ausdruckstransformator, der NICHT Coq ist.

Schnellstart

$ cargo run ./examples/peano.noq 

Hauptidee

Die Hauptidee besteht darin, Transformationsregeln symbolischer algebraischer Ausdrücke definieren und diese sequentiell anwenden zu können.

Ausdruck

Die aktuelle Ausdruckssyntax kann ungefähr so ​​definiert werden:

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

Regeln und Formen

Die beiden Haupteinheiten der Sprache sind Regeln und Formen. Eine Regel definiert das Muster (Kopf) und die entsprechende Ersetzung (Körper). Die Regeldefinition hat die folgende Syntax:

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

Hier ist ein Beispiel für eine Regel, die Elemente eines Paares vertauscht:

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

Beim Formen handelt es sich um einen Prozess der sequentiellen Anwendung von Regeln auf einen Ausdruck, der ihn in einen anderen Ausdruck umwandelt. Shaping hat die folgende Syntax:

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

So formen Sie beispielsweise den Ausdruck swap(pair(f(a), g(b))) mit der oben definierten swap Regel:

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

Das Ergebnis dieser Formung ist pair(g(b), f(a)) .

Anonyme Regeln

Sie müssen keine Regel definieren, um sie beim Formen zu verwenden:

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