Noq

Noq

EXTREMAMENTE IMPORTANTE! ESTA LÍNGUA É UM TRABALHO EM ANDAMENTO! TUDO PODE MUDAR A QUALQUER MOMENTO SEM AVISO PRÉVIO! USE ESTA LÍNGUA POR SUA CONTA E RISCO!

Não Coq. Transformador de expressão simples que NÃO é Coq.

Início rápido

$ cargo run ./examples/peano.noq 

Idéia principal

A ideia principal é ser capaz de definir regras de transformação de expressões algébricas simbólicas e aplicá-las sequencialmente.

Expressão

A sintaxe da expressão atual pode ser definida aproximadamente assim:

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

Regras e formas

As duas principais entidades da linguagem são Regras e Formas. Uma regra define o padrão (cabeça) e sua substituição correspondente (corpo). A definição da regra possui a seguinte sintaxe:

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

Aqui está um exemplo de regra que troca elementos de um par:

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

Shaping é um processo de aplicação sequencial de regras a uma expressão transformando-a em uma expressão diferente. A modelagem tem a seguinte sintaxe:

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

Por exemplo, aqui está como você molda a expressão swap(pair(f(a), g(b))) com a regra swap definida acima:

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

O resultado dessa modelagem é pair(g(b), f(a)) .

Regras anônimas

Você não precisa definir uma regra para usá-la na modelagem:

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