feature: alethe parser #69
Conversation
| const aletheIdToNodeId = new Map<string, number>(); | ||
| const preProcNodes: PreProccessedNodeInterface[] = []; | ||
|
|
||
| const parsedProof = aletheProof.split('\n').reverse().filter(filterUndesiredLines); |
There was a problem hiding this comment.
aqui eu quebro a string por linha (\n), inverto o array resultante e filtro algumas linhas.
- Quebro a string por linha, pois iremos fazer o parse de linha a linha da demonstrações.
- Inverto o array, pois demonstrações no formato Alethe possuem em sua última linha, a conclusão da prova, ou seja, o nó Raiz do Grafo. Portanto, inicio o parse de trás para frente.
- As linhas filtradas são linhas vazias
''e linhas que possuam o identificadoranchor. O identificadoranchorexiste para indicar em qual passo da demonstração se iniciará a formação de um subgrafo. Não necessitamos saber disso, pois existe uma forma mais eficiente de se identificar um subgrafo na demonstração (linha 141)
| const conclusion = findEnclosedText(line, aletheId).slice(2).trim(); | ||
| const rule = parseRule(line); | ||
| const premises = findEnclosedText(line, ALETHE_IDENTIFIERS.premises); | ||
| const args = findEnclosedText(line, ALETHE_IDENTIFIERS.arguments); | ||
| const discharge = findEnclosedText(line, ALETHE_IDENTIFIERS.discharge); |
There was a problem hiding this comment.
aqui faço o parse dos identificadores alethe existentes em demonstrações. Utilizo uma função especial para fazer o parse da cláusula de rule, pois a estratégia aplicada para as demais cláusulas nem sempre funciona.
a função findEnclosedText retorna o texto entre parênteses que ocorre a partir de um identificador específico (segundo argumento da função).
já a função parseRule utiliza expressões regulares para fazer o parse das regras.
| const aletheId = parseAletheId(line); | ||
| aletheIdToNodeId.set(aletheId, index); |
There was a problem hiding this comment.
linhas em demonstrações Alethe também possuem identificadores. Eu poderia utilizá-los na prova, porém para manter o padrão da aplicação, utilizei um índice único gerado durante o parse para identificá-los.
Salvamos o aletheId em um Map, para que no futuro consigamos achar a referência desse identificador alethe com o identificador gerado que o representa na prova.
Isso é necessário para a parte de encontrarmos os nós de filho de cada nó parseado.
| const args = findEnclosedText(line, ALETHE_IDENTIFIERS.arguments); | ||
| const discharge = findEnclosedText(line, ALETHE_IDENTIFIERS.discharge); | ||
| // children must be resolved by the end of the loop, because by then we will have all the alethe nodes parsed and therefore the currting below will not return undefined | ||
| const children = premises ? premises.split(' ').map((premise) => () => aletheIdToNodeId.get(premise)) : []; |
There was a problem hiding this comment.
a cláusula :premises indica quais são os filhos diretos daquele nó. Equivale ao X -> Y em demonstrações .dot.
Dessa forma, checamos se existem filhos para o nó que está sendo parseado, e caso existam, executamos um split na string, para que tenhamos um array de strings em que cada elemento é uma child.
Após isso, executamos a high order function .map para cada elemento desse array, que acaba retornando um callback que retorna o elemento da estrutura de dadosMap. Utilizamos um callback nesse caso, pois, como a prova é lida de trás para frente, é possível que o nó criança que está sendo "procurado" ainda não foi inserido dentro do Map.
Portanto, apenas quando acabamos o parse da demonstração por completo, resolvemos os nós criança dela.
| if (rule === 'subproof') { | ||
| // if current node has rule of type subproof, then the next node is it's immediate child | ||
| children.push(() => index + 1); | ||
| } |
There was a problem hiding this comment.
se o nó atual tem a regra subproof, significa que a próxima linha imediata será seu filho.
| id: index, | ||
| conclusion: conclusion, | ||
| rule: rule, | ||
| args: joinStrings(args, discharge), |
There was a problem hiding this comment.
as cláusulas :args e :discharge representam os argumentos de um nó
| } else if (isAssumeLine(line)) { | ||
| const aletheId = line.match(/assume(.*?)\(/)?.[1].trim() || ''; | ||
| aletheIdToNodeId.set(aletheId, index); | ||
| const conclusion = line.slice(line.indexOf(aletheId) + aletheId.length + 1, -1).trim(); |
There was a problem hiding this comment.
para linhas com a cláusula assume, fazemos um parse diferente, pois elas representam nós folha, ou seja, que não tem filhos.
Dessa forma, eles indicam apenas a declaração de uma expressão.
| preProcNodes.forEach((node) => { | ||
| const children = node.children.map((child) => child()).filter(nonNullable); | ||
| nodes.push({ ...node, children }); | ||
| }); | ||
| // here, we resolved the parents. Now we can resolve the descendants. | ||
| nodes.forEach((node) => { | ||
| const parents = nodes.reduce<number[]>((acc, curr) => { | ||
| if (curr.children.includes(node.id)) acc.push(curr.id); | ||
| return acc; | ||
| }, []); | ||
| node.parents = parents; | ||
| }); | ||
| // resolved the descendants. | ||
| nodes.forEach((node) => { | ||
| const desc = findDescendants(nodes, node.id); | ||
| node.descendants = desc.length; | ||
| }); |
There was a problem hiding this comment.
nos 3 loops ocorrem processos interessantes:
- No primeiro, resolvemos os nós folha de cada nó, invocando o callback criado anteriormente para cada. Além disso, é necessário o
filter(nonNullable)por questão de segurança de tipos. O Typescript na versão do projeto, sempre que executamos umfilterem cima de um array que é do tipo(number | undefined)[], ele sempre retornará (number | undefined)[], mesmo que filtremos explicitamente elementos do tipoundefined. A funçãononNullableexecuta um filtro direto e também um type assertion em seu retorno, para que nosso array de children seja do tiponumber[]`. - No segundo laço, resolvemos os pais de cada nó do grafo. Isso é feito percorrendo toda a árvore e checando se o array de children de cada nó possui o nó específico que estamos procurando. Inclusive, é por isso, que só podemos resolver os pais depois de resolver os filhos.
- No terceiro laço, encontramos a quantidade de descendentes de um nó.Isso é feito através da função
findDescendants. AfindDescendantsé uma função recursiva, em que procuramos em todos os filhos de um nó a partir de um nó específico, ou seja, ao invocarmos essa função para cada nó da árvore, no fim, conseguiremos a quantidade de descendentes de todos.
1 participant
Esse Pull Request tem como principal finalidade adicionar um parser de demonstrações no formato Alethe à aplicação.
Além disso, também consertei todos os testes da aplicação e adicionei testes para p novo parser Alethe.
Escreverei mais explicações sobre o código nos comentários abaixo.