Simple expression transformer that is not Coq.

Tsoding

Last update: Jan 7, 2023

Related tags

Text processing Noq

Overview

Noq

Not Coq. Simple expression transformer that is not Coq.

Quick Start

$ 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:

<expression> ::= <symbol> | <functor> | <var>
<var> ::= [A-Z][a-zA-Z0-9]*
<symbol> ::= [a-z0-9][a-zA-Z0-9]*
<functor> ::= <expression> ( [<expression>],* )

Rules and Shapes

The two main entities of the languare are Rules and Shapes. A rule defines pattern (head) and it's corresponding substitution (body). The rule definition has the following syntax:

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

Here is an example of a rule that swaps elements of a pair:

rule 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:

shape <expression>
  ... sequence of rule applications ...
done

For example here is how you shape expression swap(pair(f(a), g(b))) with the swap rule defined above:

shape swap(pair(f(a), g(b)))
  apply all swap
done

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. You can directly describe it after the apply keyword:

shape swap(pair(f(a), g(b)))
  apply all rule swap(pair(A, B)) = pair(B, A)
done

Notice that we do not provide the rule name after the rule keyword.

Comments

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?

opened by semihartan 4

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

opened by mdrwsh 3

Added loading std from any location

Now you can set NOQ_STD_PATH env variable to a path to folder with standard library you wanna use. When loading path is prefixed with std/ it will be replaced with this variable(if it's not set, the standard loading would start).

opened by farkon00 0
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.

opened by ghaspias 3

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)

opened by wiebecommajonas 0

Owner

Tsoding

Recreational Programming

GitHub

Text Expression Runner – Readable and easy to use text expressions

ter - Text Expression Runner ter is a cli to run text expressions and perform basic text operations such as filtering, ignoring and replacing on the c

72 Jul 31, 2022

This tool is for those who often want to search for a string deeply into a directory in recursive mode, but not with the great tool: grep, ack, ripgrep .........一个工具最大的价值不是它有多少功能，而是它能够让你以多快的速度达成所愿......

SSS - so stupid search tool <阿Q的哥锐普> English Documentation install install from source code 1.install rust toolchain curl --proto '=https' --tlsv1.2 -