Fonctions de sorties
A la suite d'une transformation d'une formule en son état final, ou durant la procédure de transformation, l'utilisateur peut, en utilisant les fonctions de sorties de notre programme, obtenir ses fonctions sur un support texte ou sur un support en langage TeX.
Voici les conventions d'écritures pour la sortie texte :
- Faux : Bot
- Vrai : Top
- Implication : =>
- Conjonction : &&
- Disjonction :
- Négation : !
- Possibilité : <>
- Necessité :
- Nabla : Nabla
- Littéraux : {a...z}
Pour une sortie LaTeX, nous avons utilisé les symboles correspondant aux codes TeX suivants :
- Tautologie : \top
- Faux : \bot
- Implication : \rightarrow
- Conjonction : \wedge
- Disjonction : \vee
- Négation : \neg
- Possibilité : \Diamond
- Nabla : \nabla
- Nécessité : \Box
- Littéraux : ${a...z}$
Nous précéderons notre programme de la commande :
open Types;;
Fonctions de sortie texte
val formule_to_convert : formule -> string
renvoie une chaîne de caractères comprenant la fonction retranscrite selon la convention d'écriture de texte.
Cette fonction est récursive.
val formule_to_file : formule -> out_channel -> unit
écrit la formule dans le fichier correspondant à la sortie out_channel.
Fonctions de sortie LaTeX
val formule_to_latex : formule -> string
renvoie une chaîne de caractères contenant la formule préparée pour un fichier LaTeX selon les conventions utilisées précédemment.
Cette fonction est récursive.
val formule_to_latexfile : formule -> out_channel -> unit
écrit la formule dans le fichier .tex correspondant à l'out_channel.
Pour laisser libre-choix à l'utilisateur de nommer son fichier de sortie, il devra, au préalable, affecter les off_channel pout et poutlatex aux fichiers qu'il souhaite.
Par exemple, pour un fichier de sortie "out.txt" et "test.tex" il devra définir :
let pout = open_out "out.txt" ;;
et
let poutlatex = open_out "test.tex" ;;
Fonctions développées :
formule_to_convert
let rec formule_to_convert formule = let rec write_nabla form = match form with [] -> " }"
|g::d ->formule_to_convert g^","^write_nabla d
in
match formule with VRAIf -> "Top"
|FAUXf -> "Bot"
|Impf(p,q) -> formule_to_convert p ^" => "^formule_to_convert q
|Conjf(p,q) ->"("^formule_to_convert p ^ " && "^ formule_to_convert q^" )"
|Disjf(g,d) -> "("^formule_to_convert g ^"||"^formule_to_convert d^" )"
|Negf(g) -> "!("^formule_to_convert g^" )"
|Nabf(g) -> "Nabla{ "^write_nabla g
|Possf(g) -> "<>( "^formule_to_convert g^" )"
|Necf(g) -> "[]( "^formule_to_convert g ^" )"
|Litf q-> q ;;formule_to_file
let formule_to_file formule pout= let buffer = formule_to_convert formule in match formule with a -> output_string pout buffer; close_out pout;;
formule_to_latex
let rec formule_to_latex formule = let rec write_nabla form = match form with [] -> " \\}
"
|g::d ->formule_to_latex g^","^write_nabla d
in
match formule with VRAIf -> "\\top"
|FAUXf -> "\\bot"
|Impf(p,q) -> "("^formule_to_latex p ^" \\rightarrow "^formule_to_latex q^")"
|Conjf(p,q) ->"("^formule_to_latex p ^ "\\wedge"^ formule_to_latex q^")"
|Disjf(g,d) -> "("^formule_to_latex g ^"\\vee"^formule_to_latex d^")"
|Negf(g) -> "\\neg("^formule_to_latex g^")"
|Nabf(g) -> "\\nabla\\{"^write_nabla g
|Possf(g) -> "\\Diamond("^formule_to_latex g^")"
|Necf(g) -> "\\Box("^formule_to_latex g^")"
|Litf q-> "$"^q^"$" ;;formule_to_latex
let formule_to_latexfile formule poutlatex= let intro = "\\documentclass{amsart}
\\begin{document}
\\begin{math}
"and fin = "\\end{math}
\\end{document}"
in
let buffer = formule_to_latex formule
in
match formule with a -> output_string poutlatex (intro^buffer^fin); close_out poutlatex;;Assignations facultatives :
En cas de fichier déjà existant, nous pourrons substituer
let pout = open_out "out.txt" ;;
par
let pout = open_out_gen [Open_creat; Open_append] [chmod] "out.txt";;
avec chmod = abc avec a,b et c correspondants respectivement aux entiers donnant droit à la lecture, l'écriture et l'exécution, similaire à la commande chmod sous Unix.
La fonction pour la sortie LaTeX ne peut malheureusement pas écrire à la suite d'un fichier, car, pour un document en TeX, il faut certaines conditions d'écriture pour que le fichier puisse se convertir en pdf. Ainsi, et par souci de temps, l'utilisateur devra prendre un fichier différent à chaque fois, ou écraser un ancien fichier.
Explication des fonctions :
formule_to_convert est une fonction récursive qui, pour une formule passée en paramètre, va faire un test sur la composition de son architecture, selon le typage utilisé pour son code. Ainsi, la fonction, pour chaque noeud, va rappeler la même formule au niveau du noeud inférieur, tout en concaténant le résultat du traitement du noeud en question. Elle poursuit jusqu'à la fin de l'arbre. La fonction renvoie alors une chaîne de caractères contenant l'intégralité de l'arbre parcouru.
La complexité de cette fonction est estimée à O(2n).
formule_to_file prend une formule et pout, un out_channel vers un fichier comme paramètre. De manière temporaire, cette fonction va créer un string buffer qui va être le résultat de la fonction formule_to_convert. Ensuite, la fonction utilise la fonction output_string buffer pout pour écrire dans le fichier la chaîne de caractères buffer. Enfin, elle ferme le descripteur pout pour que l'écriture s'effectue sans erreur.
La complexité de cette fonction est estimée à O(2n).
formule_to_latex est une fonction récursive qui, pour une formule passée en paramètre, va faire un test sur la composition de son architecture de manière analogue à formule_to_convert. La différence va s'effectuer sur les informations des chaînes de caractères concatenées. En sortie, nous aurons la chaîne de caractères retranscrivant la formule passée en paramètre, selon les conventions d'écriture vu plus haut.
La complexité de cette fonction est estimée à O(2n).
formule_to_latexfile va, de manière analogue à formule_to_file, prendre 2 paramètres. Elle va cependant définir au préalable deux variables temporaires intro et fin correspondant à du langage propre au langage Tex permettant un bon affichage et une bonne conversion pour une exportation pdf. De manière analogue, une fois l'écriture réalisée, la fonction ferme le descripteur associé.
La compléxité de cette fonction est estimée à O(2n).
Sortie correspondant
Pour un exemple :
let test = Disjf(Impf(Nabf[Litf "p";Litf "q";Conjf(Litf "p",Negf(Litf "q"))],VRAIf),Conjf(Necf(FAUXf),Impf(Possf(VRAIf),Possf(Necf(VRAIf)))));;
nous obtenons, pour une sortie texte :
(Nabla{ p,q,(p && !(q ) ), } => Top ||([]( Bot ) && <>( Top ) => <>( []( Top ) ) ) )et pour la sortie LaTeX :
\documentclass{amsart}
\begin{document}
\begin{math}
((\nabla\{$p$,$q$,($p$\wedge\neg($q$)), \}
\rightarrow \top)\vee(\Box(\bot)\wedge(\Diamond(\top) \rightarrow \Diamond(\Box(\top)))))\end{math}
\end{document}Ce qui correspond à une sortie pdf :
Améliorations possibles :
En vue des complexités des fonctions, nous pourrions se demander si une utilisation de fonctions tail-récursives pourrait réduire le coût de la procédure.
Le codage d'une formule est propice à l'utilisation de fonctions comme fold_left, qui sont tail-récursives.
Nous pouvons voir également quelques imperfections de la part des sortie, nous pourrions travailler sur un rendu plus propre, donc sans la virgule finale.
Nous pouvons également constater que la fonction d'écriture sur des fichiers ne prend que des formules de types formule, ainsi on pourrait créer les fonctions similaires pour les différents types de formules, à savoir formule_pos et formule_nab.