Projet à court terme

Système de modules

Pour avoir un système de module, il faut transformer la syntaxe du toplevel de PML en un ensemble de sucre syntaxique qui utilisent:

• Les records pour les champs calculer
• les existentiels pour les types/expressions abstraites.
• des redexs pour encoder des types ou expressions concrète.
• la dot notation qui permet d'accéder aux existentiels.
• des sous records pour les définitions mutuellement récursives de valeurs
• des tuples au niveau des expressions ou des paramètres en plus pour les types/expressions mutuellement récursive
• des let remontés devant le record pour des définitions privées.

auto_prove un peu plus stable.

Auto est complet au sens suivant: on doit pouvoir éliminer toutes les analyses de cas et tous les let de totalité d'un terme qui servent à établir une équation, si on configure auto avec des entiers assez grand (voir la doc que je mets à jour très vite).

cela commence à être stable et à marcher.

Il reste quelques choses importantes:

• tester un peu plus la complétude.

• générer le terme de preuve pour pouvoir revérifier la preuve sans auto et que la correction ne dépende pas de auto. On pourra aussi sauver ce terme pour ne pas refaire la preuve.

• éliminer les cases et les totalités initile du terme. Pour cela il faut que la piscine soit instrumenté pour que l'on sache quelles sont les hypothèses qui interviennent dans une contradiction.

• Cela donnera aussi les deux optimisations classique: évitement des autres cas dans un case (c'est à dire élimination d'une analyse de cas qui en fait ne sert pas) et apprentissage de clause, c'est à dire réutilisation d'un terme à un autre endroi.

Trop de preuves auto qui ne passent pas devraient passer. Le fait que l'on ait un retour vers le futur dans Timed a permis déjà des améliorations et un gain de performance. Il reste des bugs en particulier en présence de record.

return syntactic sugar

See example https://github.com/rlepigre/pml/blob/check_sub/tests/return.pml

Compilateur

Le langage étant petit, c'est facile si les variants et les labels de record sont codés par leur hash et si on ne cherche pas trop à optimiser les appels de fonctions.

Le mieux est alors de coder les appels de fonctions avec des tails call et un argument pour la pile, en utilisant l'une des calling convention de LLVM qui autorise les tails calls.

GC: Boehm ?

Types de base

Il faudraut avoir au moins

• entiers de gmp
• int32, int64, ...
• float32, float64
• tableau immutable
• caractère et chaîne

Problème: quels axiomes pour certains de ces types ? isomorphisme avec une définition en PML2 pure ?