Noq

노크

매우 중요합니다! 이 언어는 현재 진행 중인 작업입니다! 어떤 것도 예고 없이 언제든지 바뀔 수 있습니다! 이 언어를 사용하는 데 따른 위험은 귀하의 책임입니다!

콕이 아닙니다. Coq가 아닌 간단한 표현식 변환기입니다.

빠른 시작

$ cargo run ./examples/peano.noq 

주요 아이디어

주요 아이디어는 기호대수식의 변환규칙을 정의하고 이를 순차적으로 적용할 수 있다는 것이다.

표현

현재 표현식 구문은 대략 다음과 같이 정의할 수 있습니다.

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

규칙과 형태

언어의 두 가지 주요 엔터티는 규칙과 모양입니다. 규칙은 패턴(헤드)과 해당 대체(본문)를 정의합니다. 규칙 정의에는 다음 구문이 있습니다.

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

다음은 쌍의 요소를 바꾸는 규칙의 예입니다.

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

쉐이핑은 표현식에 규칙을 순차적으로 적용하여 이를 다른 표현식으로 변환하는 프로세스입니다. 쉐이핑에는 다음과 같은 구문이 있습니다.

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

예를 들어 위에 정의된 swap 규칙을 사용하여 표현식 swap(pair(f(a), g(b))) 구성하는 방법은 다음과 같습니다.

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

이 형태화의 결과는 pair(g(b), f(a)) 입니다.

익명 규칙

형성에 사용하기 위해 규칙을 정의할 필요는 없습니다.

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