tsoding / noq Goto Github PK

Simple expression transformer that is not Coq.

License: MIT License

Rust 96.51% Emacs Lisp 3.49%

noq's Introduction

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. Simple expression transformer that is NOT Coq.

Quick Start

$ cargo run ./examples/peano.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
}

noq's People

Contributors

Stargazers

Watchers

noq's Issues

Boolean expression

would some kind of boolean expression be possible?

I tried it this way but no luck. Tbh i am not quite sure how the syntax works

true :: true = bool(0)
false :: false = bool(1)
not :: not(true) = false

bool_eq :: bool(A) == bool(B) = A == B

solve :: true == not(false) {
 true | all
 false | all
 bool_eq | all
}

No instruction for building

Hi,
For those who are not familiar with rust, can you provide instructions for compilation of Noq, especially under Windows?
I am getting an error when running cargo build:

note: LINK : fatal error LNK1181: cannot open input file 'advapi32.lib'

When running rustc main.rs, I get an error regarding termion:

error[E0433]: failed to resolve: maybe a missing crate termion?

Thanks.

Replacing name of a functor turns it into a symbol

noq> shape f(a, b, c)
shaping f(a, b, c)
> apply rule f = g
 => g
> done
noq>

I was playing with coq one day ... and stumbled on its tactics language. It was really hard to grasp and I was pleasantly surprised to hear the same from tsoding in one of his videos ... but he keeps saying that coq provides 'real proofs' and somehow noq proofs can't be considered 'real'. Can someone explain me what is the difference? What noq is missing for it proofs to be considered 'real'?
Any help is appreciated!

Cannot compile on windows

I've cloned the repo, but running 'cargo run' seems to be failing on my windows.

   Compiling termion v1.5.6
error[E0433]: failed to resolve: maybe a missing crate `sys`?
  --> C:\Users\user\.cargo\registry\src\github.com-1ecc6299db9ec823\termion-1.5.6\src\lib.rs:24:9
   |
24 | pub use sys::size::terminal_size;
   |         ^^^ maybe a missing crate `sys`?

error[E0433]: failed to resolve: maybe a missing crate `sys`?
  --> C:\Users\user\.cargo\registry\src\github.com-1ecc6299db9ec823\termion-1.5.6\src\lib.rs:27:9
   |
27 | pub use sys::tty::{is_tty, get_tty};
   |         ^^^ maybe a missing crate `sys`?

error[E0433]: failed to resolve: maybe a missing crate `sys`?
 --> C:\Users\user\.cargo\registry\src\github.com-1ecc6299db9ec823\termion-1.5.6\src\async.rs:5:5
  |
5 | use sys::tty::get_tty;
  |     ^^^ maybe a missing crate `sys`?

error[E0433]: failed to resolve: maybe a missing crate `sys`?
  --> C:\Users\user\.cargo\registry\src\github.com-1ecc6299db9ec823\termion-1.5.6\src\raw.rs:28:5
   |
28 | use sys::attr::{get_terminal_attr, raw_terminal_attr, set_terminal_attr};
   |     ^^^ maybe a missing crate `sys`?

error[E0432]: unresolved import `sys`
  --> C:\Users\user\.cargo\registry\src\github.com-1ecc6299db9ec823\termion-1.5.6\src\raw.rs:29:5
   |
29 | use sys::Termios;
   |     ^^^ maybe a missing crate `sys`?

error[E0425]: cannot find function `get_tty` in this scope
  --> C:\Users\user\.cargo\registry\src\github.com-1ecc6299db9ec823\termion-1.5.6\src\async.rs:14:36
   |
14 |     thread::spawn(move || for i in get_tty().unwrap().bytes() {
   |                                    ^^^^^^^ not found in this scope

error[E0425]: cannot find function `get_tty` in this scope
  --> C:\Users\user\.cargo\registry\src\github.com-1ecc6299db9ec823\termion-1.5.6\src\async.rs:43:36
   |
43 |     thread::spawn(move || for i in get_tty().unwrap().bytes() {
   |                                    ^^^^^^^ not found in this scope

error[E0425]: cannot find function `set_terminal_attr` in this scope
  --> C:\Users\user\.cargo\registry\src\github.com-1ecc6299db9ec823\termion-1.5.6\src\raw.rs:45:9
   |
45 |         set_terminal_attr(&self.prev_ios).unwrap();
   |         ^^^^^^^^^^^^^^^^^ not found in this scope

error[E0425]: cannot find function `get_terminal_attr` in this scope
   --> C:\Users\user\.cargo\registry\src\github.com-1ecc6299db9ec823\termion-1.5.6\src\raw.rs:102:23
    |
102 |         let mut ios = get_terminal_attr()?;
    |                       ^^^^^^^^^^^^^^^^^ not found in this scope

error[E0425]: cannot find function `raw_terminal_attr` in this scope
   --> C:\Users\user\.cargo\registry\src\github.com-1ecc6299db9ec823\termion-1.5.6\src\raw.rs:105:9
    |
105 |         raw_terminal_attr(&mut ios);
    |         ^^^^^^^^^^^^^^^^^ not found in this scope

error[E0425]: cannot find function `set_terminal_attr` in this scope
   --> C:\Users\user\.cargo\registry\src\github.com-1ecc6299db9ec823\termion-1.5.6\src\raw.rs:107:9
    |
107 |         set_terminal_attr(&ios)?;
    |         ^^^^^^^^^^^^^^^^^ not found in this scope

error[E0425]: cannot find function `set_terminal_attr` in this scope
   --> C:\Users\user\.cargo\registry\src\github.com-1ecc6299db9ec823\termion-1.5.6\src\raw.rs:119:9
    |
119 |         set_terminal_attr(&self.prev_ios)?;
    |         ^^^^^^^^^^^^^^^^^ not found in this scope

error[E0425]: cannot find function `get_terminal_attr` in this scope
   --> C:\Users\user\.cargo\registry\src\github.com-1ecc6299db9ec823\termion-1.5.6\src\raw.rs:125:23
    |
125 |         let mut ios = get_terminal_attr()?;
    |                       ^^^^^^^^^^^^^^^^^ not found in this scope

error[E0425]: cannot find function `raw_terminal_attr` in this scope
   --> C:\Users\user\.cargo\registry\src\github.com-1ecc6299db9ec823\termion-1.5.6\src\raw.rs:126:9
    |
126 |         raw_terminal_attr(&mut ios);
    |         ^^^^^^^^^^^^^^^^^ not found in this scope

error[E0425]: cannot find function `set_terminal_attr` in this scope
   --> C:\Users\user\.cargo\registry\src\github.com-1ecc6299db9ec823\termion-1.5.6\src\raw.rs:127:9
    |
127 |         set_terminal_attr(&ios)?;
    |         ^^^^^^^^^^^^^^^^^ not found in this scope

Some errors have detailed explanations: E0425, E0432, E0433.
For more information about an error, try `rustc --explain E0425`.
error: could not compile `termion` due to 15 previous errors

Cannot Compile On Windows

Hello,
I am a applied mathematician. I wanted to compile and give a try your interesting project but the compiling process fails on Windows due to Termion library. I am new to Rust and dont have any experience on it. Can somebody help me, please?

support for inequations and deductions

when we do basic algebra, we want to use rules of equivalence:

= in math;
if and only if in logic;
equivalence relation in abstract algebra.

and this is what we have in noq.

but sometimes we need thing that have some sort of order:

< in math;
imply in logic;
partial order in abstract algebra.

the killer application for this, is the ability to make logical deductions.

you can deduce Q from P and Q .
but you can not deduce P and Q from Q.

so we would have rules like:
A ^ B -> A
that allow us to replace the lhs by rhs. And also rules like:
A^B == B^A
that works both ways.

I suppose the way shaping would work in 2 possible ways:

manual mode where a shaping operation can be selected to be either equivalece of deductive (noob)
auto mode where shaping would be internally deductive, but if all steps are equivalence,
the result must be equal. (pro)

Changing termion for crossterm

As of 09/10/2023, Termion has no support for Windows.
As this looks like a project that shouldn't be attached to just Linux, I propose the use of Crossterm(Termion alternative) for the crossplatform.

By changing only changing that, the code would be accessible in any platform.

Referencing file `./examples/add.noq` that does not exist

Noq/README.md

Line 10 in f0bfa93

$ cargo run ./examples/add.noq

strategy for built-in rules

I suppose built-in rules should match with same semantic as user defined rules.
but there is no check for built-in corresponding to line 135.

built-in:

Noq/src/engine/rule.rs

Lines 155 to 157 in 716fae3

 if let Some(bindings) = Expr::replace_head().pattern_match(expr) { 

 *match_count += 1; 

 let meta_rule = Rule::User {

user:

Noq/src/engine/rule.rs

Lines 134 to 136 in 716fae3

 if let Some(bindings) = head.pattern_match(expr) { 

 let resolution = strategy.matched(*match_count); 

 *match_count += 1;

but I guess this feature is not released yet.

test case:

noq> test :: apply_rule(deep, b, c, apply_rule(deep, a, pair(b,b), a)) {

Request for procedures

Description

A shaping applies rules 'at compile time' whereas a procedure would apply the rules 'at runtime'.

Example

Disclaimer: This example assumes the usage of the 'all' strategy as described in #11, because I could not come up with a different example.

eq_f :: eq(bool(true), bool(false)) = bool(false)
eq_t :: eq(bool(A), bool(A)) = bool(true)

basic_comm :: B(X, Y) = B(Y, X)

# eq_resolve :: eq(bool(A), bool(B)) {
#     eq_t | all
#     eq_f | all
#     basic_comm | all
#     eq_f | all
# }
# 
# result: eq(bool(A), bool(B))

proc eq_resolve :: eq(bool(A), bool(B)) {
    eq_t | all
    eq_f | all
    basic_comm | all
    eq_f | all
}

eq(bool(false), bool(true)) {
    eq_resolve | all
}

# expected result: bool(false)

Semantics of `all` strategy

Description

The all strategy should really not throw an error when not match is found.

Reasoning

'All' matches are semantically just a list of matches. So if no match is found, 'all matches' is just an empty list. Applying every match in an empty list is thus properly defined and needs no different treatment.

This also allows 'conditional' (stretching the meaning of the word) application.

Example

and_f :: and(bool(false), bool(_)) = bool(false)
and_t :: and(bool(true), bool(true)) = bool(true)

basic_comm :: B(X, Y) = B(Y, X)

and(bool(true), bool(false)) {
    and_t | all
    and_f | all
    basic_comm | all
    and_f | all
}

Known issues

This could lead to issues where rule applications following an 'all' application expect the order of matches to be a specific way.

	if let Some(bindings) = Expr::replace_head().pattern_match(expr) {
	*match_count += 1;
	let meta_rule = Rule::User {

	if let Some(bindings) = head.pattern_match(expr) {
	let resolution = strategy.matched(*match_count);
	*match_count += 1;

tsoding / noq Goto Github PK

noq's Introduction

Noq

Quick Start

Main Idea

Expression

Rules and Shapes

Anonymous rules

noq's People

Contributors

Stargazers

Watchers

Forkers

noq's Issues

Description

Example

Description

Reasoning

Example

Known issues

Recommend Projects

Recommend Topics

Recommend Org