-
Notifications
You must be signed in to change notification settings - Fork 24
/
README.md
73 lines (51 loc) · 1.88 KB
/
README.md
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
# Noq
**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](https://coq.inria.fr/). Simple expression transformer that is NOT Coq.
## Quick Start
```console
$ cargo run ./examples/add.noq
```
## Main Idea
The Main Idea is being able to define transformation rules of symbolic algebraic expressions and sequentially applying them.
## Expression
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>),* `)`
```
## Rules and Shapes
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))`.
### Anonymous rules
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
}
```