EXTREMELY IMPORTANT! THIS LANGUAGE IS A WORK IN PROGRESS! ANYTHING CAN CHANGE AT ANY MOMENT WITHOUT ANY NOTICE! USE THIS LANGUAGE AT YOUR OWN RISK!
Not Coq. Simple expression transformer that is NOT Coq.
$ cargo run ./examples/peano.noqThe Main Idea is being able to define transformation rules of symbolic algebraic expressions and sequentially applying them.
Current expression syntax can be defined roughly like this:
<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>),* `)`
The two main entities of the language are Rules and Shapes. A rule defines pattern (head) and it's corresponding substitution (body). The rule definition has the following syntax:
<name:symbol> :: <head:expression> = <body:expression>
Here is an example of a rule that swaps elements of a pair:
swap :: swap(pair(A, B)) = pair(B, A)
Shaping is a process of sequential applying of rules to an expression transforming it into a different expression. Shaping has the following syntax:
<expression> {
... sequence of rule applications ...
}
For example here is how you shape expression swap(pair(f(a), g(b))) with the swap rule defined above:
swap(pair(f(a), g(b))) {
swap | all
}
The result of this shaping is pair(g(b), f(a)).
You don't have to define a rule to use it in shaping:
swap(pair(f(a), g(b))) {
swap(pair(A, B)) = pair(B, A) | all
}