Noq

Noq

¡EXTREMADAMENTE IMPORTANTE! ¡ESTE IDIOMA ES UN TRABAJO EN PROGRESO! ¡CUALQUIER COSA PUEDE CAMBIAR EN CUALQUIER MOMENTO SIN NINGÚN AVISO! ¡UTILIZA ESTE IDIOMA BAJO TU PROPIO RIESGO!

No Coq. Transformador de expresión simple que NO es Coq.

Inicio rápido

$ cargo run ./examples/peano.noq 

Idea principal

La idea principal es poder definir reglas de transformación de expresiones algebraicas simbólicas y aplicarlas secuencialmente.

Expresión

La sintaxis de la expresión actual se puede definir más o menos así:

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

Reglas y formas

Las dos entidades principales del lenguaje son Reglas y Formas. Una regla define el patrón (cabeza) y su correspondiente sustitución (cuerpo). La definición de regla tiene la siguiente sintaxis:

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

A continuación se muestra un ejemplo de una regla que intercambia elementos de un par:

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

Dar forma es un proceso de aplicación secuencial de reglas a una expresión transformándola en una expresión diferente. Dar forma tiene la siguiente sintaxis:

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

Por ejemplo, así es como se le da forma a la expresión swap(pair(f(a), g(b))) con la regla swap definida anteriormente:

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

El resultado de esta configuración es pair(g(b), f(a)) .

Reglas anónimas

No es necesario definir una regla para usarlo al dar forma:

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