BONNEVALLE Vincent pushed to branch unification at Stefan / Typer

Commits: 03807ed4 by n3f4s at 2016-10-05T11:42:24+02:00 add internship report tex file

- - - - - 9dab10b2 by n3f4s at 2016-10-05T11:42:24+02:00 add makefile for compiling report

- - - - - 6e100ad5 by n3f4s at 2016-10-05T11:42:24+02:00 update doc rule of main makefile for report

- - - - -

10 changed files:

- + Makefile - + doc/rapport/Makefile - + doc/rapport/cc.tex - + doc/rapport/gest-proj.tex - + doc/rapport/glossary.tex - + doc/rapport/infer.tex - + doc/rapport/main.tex - + doc/rapport/pres-univ.tex - + doc/rapport/remerciements.tex - + doc/rapport/typer.tex

Changes:

===================================== Makefile ===================================== --- /dev/null +++ b/Makefile @@ -0,0 +1,152 @@ + +# TODO : find a way to have debug only function + +# Name of the target binary program +TARGET := typer +CC := ocamlbuild +RM := rm -rf +MV := mv + +#COMPILE_MODE := native +COMPILE_MODE := byte + +BUILDDIR := _build +TESTDIR := tests +SRCDIR := src + +OBFLAGS := -I $(SRCDIR) -build-dir $(BUILDDIR) -pkg str +OBFLAGS_DEBUG := -tag debug -tag profile -tag "warn(+20)" +OBFLAGS_RELEASE := -tag unsafe -tag inline + +DEBUG ?= 1 +VERBOSE ?= 1 + +#--------------------------------------------------------------------------------- +#DO NOT EDIT BELOW THIS LINE +#--------------------------------------------------------------------------------- + +ifeq ($(DEBUG), 1) + OBFLAGS += $(OBFLAGS_DEBUG) +else + OBFLAGS += $(OBFLAGS_RELEASE) +endif + +BUILDTEST := $(BUILDDIR)/$(TESTDIR) +BUILDSRC := $(BUILDDIR)/$(SRCDIR) + + +SRC_FILES := $(wildcard $(SRCDIR)/*.ml) +CPL_FILES := $(patsubst $(SRCDIR)/%,$(BUILDSRC)/%,$(SRC_FILES:.ml=.cmo)) +TEST_FILES := $(wildcard ./$(TESTDIR)/*_test.ml) + + +TESTTARGETS := $(patsubst ./$(TESTDIR)/%,$(BUILDTEST)/%,$(TEST_FILES:.ml=.$(COMPILE_MODE))) + +all: $(TARGET) debug tests-build ## Build typer, debug-util and tests + +ifndef SYSTEMROOT +help: ## Prints help for targets with comments + @grep -E '^[a-zA-Z_-]+:.*?## .*$$' $(MAKEFILE_LIST) \ + | { echo -e 'typer: ## Build Typer'; sort; } \ + | awk 'BEGIN {FS = ":.*?## "}; {printf "\033[36m%-30s\033[0m %s\n", $$1, $$2}' +endif + +generate_debug_fun: +ifeq ($(DEBUG), 1) +ifeq ($(VERBOSE), 1) + @sed 's/__debug__/true/' src/debug_fun.ml.tpl > src/debug_fun.ml + @echo -e "Debug logging enabled" +else + @sed 's/__debug__/false/' src/debug_fun.ml.tpl > src/debug_fun.ml + @echo -e "Debug logging disabled" +endif +else + @sed 's/__debug__/false/' src/debug_fun.ml.tpl > src/debug_fun.ml + @echo -e "Debug logging disabled" +endif + + +# debug file eval +debug: generate_debug_fun $(SRCDIR)/debug_util.ml ## Build debug utils + # ============================ + # Build debug utils + # ============================ + @$(CC) src/debug_util.$(COMPILE_MODE) $(OBFLAGS) + @$(MV) _build/src/debug_util.$(COMPILE_MODE) _build/debug_util + +# interactive typer +$(TARGET): generate_debug_fun $(SRC_FILES) ## Build typer + # ============================ + # Build typer + # ============================ + @$(CC) src/REPL.$(COMPILE_MODE) $(OBFLAGS) + @$(MV) _build/src/REPL.$(COMPILE_MODE) _build/$(TARGET) + +tests-build: $(TESTTARGETS) + # ============================ + # Build tests + # ============================ + @$(CC) tests/utest_main.$(COMPILE_MODE) $(OBFLAGS) + @$(MV) _build/tests/utest_main.$(COMPILE_MODE) _build/tests/utests + +$(BUILDTEST)/%.$(COMPILE_MODE): $(TESTDIR)/%.ml + @$(CC) $(<:.ml=.$(COMPILE_MODE)) $(OBFLAGS) + +tests-run: + @./_build/tests/utests --verbose= 3 + +test-file: + @$(CC) src/test.$(COMPILE_MODE) $(OBFLAGS) + @$(MV) _build/src/test.$(COMPILE_MODE) _build/test + +# There is nothing here. I use this to test if opam integration works +install: tests + +tests: generate_debug_fun tests-build tests-run ## Build tests + +# Make language doc +doc-tex: ## Make language doc + @texi2pdf ./doc/manual.texi --pdf --build=clean + @make -C ./doc/rapport + +# Make implementation doc +doc-ocaml: ## Make implementation doc +ifndef SYSTEMROOT + @ls $(SRC_FILES)\ + | grep -v "src/unify.ml"\ + | grep -v "src/elaborate.ml"\ + | grep -v "ulexp.ml"\ + | grep -v "src/subst.ml"\ + | grep -v "javascript.ml"\ + | awk 'BEGIN { FS = "[/.]" }\ + { printf "%s/%s%s\n", $$1, substr($$2,1,1), substr($$2,2) }' > project.odocl + @$(CC) project.docdir/index.html $(OBFLAGS) # -docflag "-charset 'UTF8'" + @sed -i.bak 's/iso-8859-1/UTF-8/' _build/project.docdir/*.html +endif + +# everything is expected to be compiled in the "./_build/" folder +clean: ## Clean everything in BUILDDIR + @$(RM) $(BUILDDIR) + @$(RM) project.docdir + @$(RM) *.odocl + +.PHONY: typer debug tests + +run/typecheck: + @./_build/debug_util ./samples/test__.typer -typecheck + +run/debug_util: + @./_build/debug_util ./samples/test__.typer -fmt-type=on -fmt-index=off -fmt-pretty=on + +run/typer: + @./_build/typer + +run/tests: + @./_build/tests/utests --verbose= 1 + +run/typer-file: + @./_build/typer ./samples/test__.typer + +run/test-file: + @./_build/test +

===================================== doc/rapport/Makefile ===================================== --- /dev/null +++ b/doc/rapport/Makefile @@ -0,0 +1,46 @@ + +TARGET := report +DVI := pdflatex +BIB := biber +IDX := makeindex +PDF := ps2pdf +PS := dvips +GLOS := makeglossaries +OBJDIR := out + +LATEXFLAGS := -output-directory $(OBJDIR) -interaction=batchmode + +MAIN := main + +all: dvi copy + +dvi: + @mkdir -p $(OBJDIR) + @echo -e "First compilation" + @$(DVI) $(LATEXFLAGS) $(MAIN).tex + @echo -e "Generating index" + @$(IDX) $(MAIN).idx + @echo -e "Generating bibliography" + @$(BIB) --output-directory $(OBJDIR) $(MAIN) + @echo -e "Generating glossary" + @$(GLOS) -q -d $(OBJDIR) $(MAIN) + @echo -e "Second compilation" + @$(DVI) $(LATEXFLAGS) $(MAIN).tex + @$(DVI) $(LATEXFLAGS) $(MAIN).tex + +ps: dvi + @$(PS) $(MAIN).dvi + +pdf: ps + @$(PS) $(MAIN).ps + +copy: + @cp $(OBJDIR)/$(MAIN).pdf $(TARGET).pdf + +latexmk: + latexmk --output-directory=./$(OBJDIR) -pvc main.tex + cp main.pdf $(TARGET).pdf + +clean: + @echo -e "Cleaning" + @rm -f $(MAIN).{ps,pdf,log,aux,out,dvi,bbl,blg}

===================================== doc/rapport/cc.tex ===================================== --- /dev/null +++ b/doc/rapport/cc.tex @@ -0,0 +1,17 @@ +\chapter{Conclusion} + +Ce stage m'a permis de découvrir une partie de l'informatique que nous n'avons pas vu en cours: +les mécanismes d'inférence de type et l'interprétation de langage fonctionnel. +Il m'a permis de découvrir le $\lambda{}-calcul$, modèle de calcul utilisé pour l'implémentation des compilateurs +de langage fonctionnel. + +L'inférence de type d'un langage de programmation fonctionnel est fortement liée à la théorie du $\lambda{}-calcul$. +En effet, le type d'unification utilisé dans ces langages est un sous-ensemble d'un problème indécidable. +Par conséquent, lors de la création du langage, il faut faire attention à ne pas sortir de ce sous-ensemble. +De plus, la représentation interne utilisée par le compilateur influe beaucoup sur les algorithmes +utilisés par l'inférence de type. + +Le langage \typer{} et son compilateur étant en cours de développement, les +seul programmes écrit dans ce langage servent à tester le compilateur. +La création de programmes de moyenne ou grande taille permettra d'évaluer les avantages et les inconvénients de langages +sécurisé de la flexibilité pour cette sécurité.

===================================== doc/rapport/gest-proj.tex ===================================== --- /dev/null +++ b/doc/rapport/gest-proj.tex @@ -0,0 +1,66 @@ +\chapter{Gestion de Projet} + +\section{Planning} + +\structpar{planning} +Le stage a été découpé en quatre parties. + +\begin{figure}[!h] + \centering + \caption{Planning du stage} +\label{tab:plan} + \begin{tabular}{|l | l | l |} + \toprule + partie & durée & résumé \ + \midrule + première partie & une semaine & familiarisation avec le code et les outils utilisés\ + \midrule + deuxième partie & quatre semaines & Implémentation de l'unification de premier ordre\ + \midrule + troisième partie & trois semaines & Implémentation de l'inversion des substitutions d'index de \textit{de Bruijn}\ + \midrule + quatrième partie & quatre semaines & Intégration de l'unification dans l'inférence de type et résolution des bugs\ + \bottomrule + \end{tabular} +\end{figure} + +Les deux dernières semaines ont été laissées libres pour être utilisées pour résoudre les problèmes survenus lors de +l'implémentation des différentes parties ou au cas où une des parties du planning durerait plus longtemps que prévu. +\structpar{gantt} +\begin{figure}[!h] + \centering + \includegraphics[width=1\linewidth]{./plan-1.png} + \caption{Première partie du diagramme de Gantt} +\label{fig:gant1} +\end{figure} +\begin{figure}[!h] + \centering + \includegraphics[width=1\linewidth]{./plan-2.png} + \caption{Deuxième partie du diagramme de Gantt} +\label{fig:gant2} +\end{figure} +\structpar{rythmes des contacts} +Le rythme des contacts avec mon tuteur de stage était d'une fois par semaine. Ces contacts servaient à +faire un compte rendu de mon avancement durant cette semaine. +De plus, je pouvais contacter mon tuteur en cas de besoin, pour résoudre un problème théorique par exemple. + +\section{Cahier des charges} + +\structpar{cahier des charges} +Le but de ce stage était d'implémenter une première version d'inférence de type pour le compilateur +du langage \typer{}. + +\structpar{définition de l'inférence de type} +L'inférence de type est une technique permettant à un compilateur de déduire le type d'une expression. +L'inférence de type de \typer{} doit permettre au système de type de fournir un typage fort. + +L'inférence de type de \typer{} est proche de l'inférence de type de \textit{Hindley-Milner} et doit permettre +d'écrire du code sans aucune annotation de type. + +\structpar{contraintes techniques} +Le code du compilateur de \typer{} est hébergé sur un dépôt gitlab. +L'implémentation de l'inférence de type devait être codée dans le même langage que le compilateur: \texttt{ocaml}. +Les outils de compilation et débogage étaient ceux fournis avec le compilateur \texttt{ocaml}: \texttt{ocamlbuild} et \texttt{make} +pour la compilation et \texttt{ocamldebug} pour le débogage. + +Chaque partie du code devait être testée grâce à un framework de test créé pour le compilateur.

===================================== doc/rapport/glossary.tex ===================================== --- /dev/null +++ b/doc/rapport/glossary.tex @@ -0,0 +1,16 @@ + +\newglossaryentry{lexp}% +{% + name=\lexpgl,% + description={Lambda-Expression}% +} +\newglossaryentry{sexp}% +{% + name=\sexpgl,% + description={S-Expression}% +} +\newglossaryentry{pexp}% +{% + name=\pexpgl,% + description={Proto Lambda-Expression}% +}

===================================== doc/rapport/infer.tex ===================================== --- /dev/null +++ b/doc/rapport/infer.tex @@ -0,0 +1,129 @@ +\chapter{L'inférence de type} + \section{Parser} + + \structpar{Fonctionnement général du parser} + L'interprétation du code se fait de cette façon: + + \begin{center} + code typer $\xrightarrow[]{prelexer}$ code \say{prélexé} $\xrightarrow[]{lexer}$ \sexp{} $\xrightarrow[]{}$ \pexp{} $\xrightarrow[]{}$ \lexp.\ + \end{center} + + \structpar{Les \sexp{}} + Les \texttt{S-Expressions} (\textit{Symbolic expressions}) sont une structure de données en forme d'arbre. + Cette structure de données a été inventée et utilisée pour la première fois par le langage \textit{Lisp}. + Les \sexp{} permettent de représenter un arbre de syntaxe abstrait c'est pourquoi elles ont été utilisées + comme représentation interne du compilateur. + + \structpar{Les \pexp{}} + Les \texttt{Proto Lambda-Expression} sont une représentation à mi-chemin entre les \sexp{} et les \lexp{}. + Elles sont utilisées uniquement pour faciliter la transformation des \sexp{} en \lexp{}. + + \structpar{Les \lexp{}} + Les \lexp{}\ref{fig:ocmllxp} sont des expressions représentant les \textit{Lambda-Expressions} du $\lambda{}-calcul$. + Elles servent de représentation intermédiaire du code \typer{}. + Les différentes opérations, comme la vérification de type, se fait sur les \lexp{}. + + \structpar{Détails} + Lors de l'interprétation du code, il est tout d'abord \say{prélexé}. + Durant cette phase, les commentaires sont supprimés, les litéraux (nombres et chaines de caractères) + sont séparés du code et le code est séparé selon les parenthèses. + + Ensuite, le code \say{prélexé} passe par le lexer qui va transformer le code en \sexp{}. + Les \sexp{} sont ensuite transformées en \pexp{}. + Enfin, les \pexp{} sont transformés en \lexp{}. Durant cette phase, les informations de type vont être rajoutées aux \lexp{}. + + \structpar{L'inférence de type et l'unification} + L'inférence de type se fait sur les \lexp{}. En effet ce sont les seules expressions + à avoir une information sur leur type. + + \section{Unification} + L'unification est moyen permettant de déterminer si deux expressions sont équivalentes. + Dans le cas de l'inférence de type pour le compilateur \typer{}, + l'unification se fait sur les \lexp{}. + Deux \lexp{} sont unifiables si elles sont équivalentes. Si les expressions $S$ et $T$ + sont unifiables alors on peut écrire (en \typer{}) $S = T$. + + Dans le cas du compilateur \typer{}, l'unification permet de vérifier qu'il n'y a pas + d'erreur de typage. + + \subsection{Unification de premier ordre} + + \structpar{L'unification des \lexp} + L'unification de premier ordre permet de déterminer si deux \lexp{} sont équivalentes, dans les cas simples. + Cependant, toutes les informations nécessaires ne sont pas toujours disponibles lors de l'unification. + L'algorithme d'unification renvoie une liste de contraintes et une liste d'associations entre une méta-variable et une \lexp{} quelconque. + Le couple formé par ces deux listes est appelé le \textit{contexte d'unification}\ref{fig:ctxunif}. + + \structpar{Cas Évident} + Si deux \lexp{} sont équivalentes, elles sont unifiables. Par exemple, deux nombres égaux seront transformés en deux \lexp{} équivalentes. + Ces deux \lexp{} seront unifiables. + Dans ce cas, l'algorithme d'unification renvoie le même \textit{contexte d'unification} qui lui a été donné en paramètre. + + Respectivement, deux \lexp{} peuvent être facilement identifiées comme non unifiables. Par exemple, les \lexp{} générées par deux nombres différents + ne seront pas unifiables. + Dans ce cas, l'algorithme d'unification renvoie une erreur. En effet, l'unification de deux \lexp{} non unifiables correspond, + dans l'inférence de type, à une erreur de typage. + + \structpar{Cas qui renvoie une contrainte} + Certains cas ne permettent pas de donner une réponse sur le résultat de l'unification. En effet, les informations disponibles + ne sont pas suffisantes. C'est notamment le cas avec les variables et les fonctions. + Dans ce cas, l'algorithme d'unification renvoie une contrainte indiquant que les deux \lexp{} doivent être unifiables. + Plus tard dans l'exécution, cette contrainte sera validée, si le code est correct, ou invalidée, s'il y a une erreur de type. + La liste des contraintes du \textit{contexte d'unification} est représentée sous la forme d'une liste de couples. + Chaque couple représentant de \lexp{} qui doivent être unifiables pour que le typage soit correct. + L'algorithme d'unification renvoie, dans le cas où il doit générer une contrainte, le \textit{contexte d'unification} passé en paramètre + en rajoutant dans la liste des contraintes le couple formé par les deux \lexp{} passées en paramètre. + + \structpar{Méta-variables} + Lorsque l'algorithme d'unification rencontre une méta-variable, il l'associe à l'autre \lexp{} passée en paramètre. + Si la méta-variable est déjà associée à une \lexp{}, alors l'algorithme essaiera d'unifier la \lexp{} associée à la méta-variable + et la \lexp{} passée en paramètre. + Si la méta-variable n'est pas associée à une \lexp{}, l'algorithme renvoie le \textit{contexte d'unification} auquel est rajoutée une + association entre la \lexp{} et la méta-variable. Sinon, l'algorithme renvoie le résultat de l'unification de la \lexp{} passée en paramètre + avec la \lexp{} associée à la méta-variable. + + \structpar{Résultat de l'algorithme} + Le résultat de l'alogrithme permet donc de déterminer quel cas il à rencontré: + \begin{itemize} + \item Si la liste d'association est la même en entrée et en sortie alors les deux \lexp{} passées en paramètre sont unifiables. + \item Si l'unification ne renvoie rien les \lexp{} passée en paramètre ne sont pas unifiables. + \item Si la liste des contraintes renvoyé par l'unification contient une contrainte de plus alors l'unification ne possédait pas assez d'information pour renvoyer un resultat. + \item Si la liste d'association renvoyé par l'unification contient une association de plus alors une des deux \lexp{} passée en paramètre était une méta-variable. + \end{itemize} + + \structpar{Ce qu'il manque} + L'unification de premier ordre ne tient pas en compte des ajouts et suppressions de variables. C'est pourquoi cette forme d'unification ne suffit + pas pour l'inférence de type requise par \typer{}. + + \subsection{Unification des \hop{}} + \structpar{\hop{}} + L'unification de premier ordre ne suffit pas pour l'inférence de type requise par \typer{}. + En effet, l'unification de premier ordre ne tient pas compte des modifications des index de \textit{de Bruijn}. + L'unification de \typer{} utilise un sous-ensemble de l'unification des \hop{} + L'unification des \hop{} est un sous-ensemble décidable de l'unification d'ordre supérieur. + + \structpar{Les index de \textit{de Bruijn}} + Les index de \textit{de Bruijn} sont une notation inventée par Nicolaas Govert de Bruijn qui sert à représenter les + termes du $\lambda{}-calcul$. Cette notation utilise des index comme identificateur de variables (dans le code). L'index le plus grand + correspond à la première variable instanciée (et toujours définie). + + Les index de \textit{de Bruijn} facilitent la comparaison de variable par rapport à l'utilisation de nom de variable comme identifiant. + En effet, deux variables peuvent avoir le même nom de variable tout en étant différentes. Avec l'utilisation des index de \textit{de Bruijn}, + ces deux variables auront des index différents puisqu'elles sont différentes. + Cependant, le décalage des index lié à l'ajout et la suppression de variables peut causer des erreurs lors de la comparaison d'une même + variable dans des contextes différents. + + \structpar{La substitution des index de \textit{de Bruijn}} + Pour remédier au problème de l'ajout et de la suppression de variables avec les index de \textit{de Bruijn}, on associe au contexte des + variables une substitution. Cette substitution, une fois appliquée à un index, l'augmente ou le réduit. + Ceci permet de modifier les index en fonction du contexte et pouvoir comparer des variables dans différents contextes. + + \structpar{L'unification avec les index de \textit{de Bruijn}} + Pour prendre en compte les différences de contexte lors de l'unification, il faut intégrer + les substitutions d'index de \textit{de Bruijn} dans l'unification. + Pour cela, on associe à une meta-variable l'inverse de la substitution en cours. De cette + façon, les \texttt{Metavar} (représentation des méta-variables dans le compilateur) ne représentent plus + des méta-variables mais l'application d'une substitution à une méta-variable. + Cette modification permet de prendre en compte le contexte dans lequel la méta-variable a été créée + et ainsi de pouvoir appliquer les substitutions lors de l'unification de variables dans des contextes différents. +

===================================== doc/rapport/main.tex ===================================== --- /dev/null +++ b/doc/rapport/main.tex @@ -0,0 +1,173 @@ +\documentclass[a4paper, 15pt]{report} + +\usepackage[utf8]{inputenc} +\usepackage[T1]{fontenc} +\usepackage[pdftex]{graphicx} +\usepackage[backend=biber]{biblatex} +\usepackage[left=2cm,right=2cm,top=2.5cm,bottom=2cm]{geometry} +\usepackage{amssymb} +\usepackage{amsmath} +\usepackage{hyperref} +\usepackage{multirow} +\usepackage{booktabs} +\usepackage{makeidx} +\usepackage{filecontents} +\usepackage{listings} +\usepackage{color} +\usepackage{verbatim} +\usepackage[toc]{glossaries} +\usepackage{newunicodechar} % for \newunicodechar +\usepackage{title} +\usepackage{siunitx} +\usepackage[french]{babel} +\usepackage[left=\flqq, right=\frqq, leftsub=\flqq, rightsub=\frqq]{dirtytalk} + +\begin{filecontents*}{\jobname.bib} +@misc{ + udemnum, + title = { http://recteur.umontreal.ca/documents-institutionnels/faits-et-chiffres/%7D +} +@misc{ + wikinum, + title = { http://fin.umontreal.ca/direction-finances/etats-financiers/documents/ef%5C_... } +} +\end{filecontents*} + +\addto\captionsfrench{\renewcommand{\chaptername}{Partie}} + +\addbibresource{\jobname.bib} + +\lstset{language=caml, + basicstyle=\ttfamily, + keywordstyle=\color{blue}\ttfamily, + stringstyle=\color{red}\ttfamily, + commentstyle=\color{green}\ttfamily, + morecomment=[l][\color{magenta}]{#} +} + +\newcommand{\subsubsubsection}{\paragraph} +\renewcommand{\paragraph}{\subparagraph} +\setcounter{secnumdepth}{3} + +\newcommand{\udem}{Université de Montréal} +\newcommand{\typer}{\textit{Typer}} +\newcommand{\sexpgl}{\texttt{S-exp}} +\newcommand{\lexpgl}{\texttt{L-exp}} +\newcommand{\pexpgl}{\texttt{P-exp}} + +\newunicodechar{≡}{\ensuremath{\equiv}} +\newunicodechar{α}{\ensuremath{\alpha}} + +\title{Stage de quatrième année} +\subtitle{Développement d'inférence de type pour le langage Typer} +\author{BONNEVALLE Vincent} +\tuteurPoly{Guillaume Raschia} +\tuteurEntr{Stéfan Monnier} +\scolaryear{2015 -- 2016} +\thisyear{4} +\logo{% +\includegraphics[scale=0.5]{./img/udem.png}}{% +\includegraphics[scale=0.5]{./img/univ-nantes.png}}{% +\includegraphics[scale=0.5]{./img/polytech.png}% +} + +\makeindex +\makeglossaries +\input{./glossary.tex} + +\newcommand{\sexp}{\gls{sexp}\index{sexp@S-Expression}} +\newcommand{\lexp}{\gls{lexp}\index{lexp@Lambda-Expression}} +\newcommand{\pexp}{\gls{pexp}\index{pexp@P-Expression}} +\newcommand{\hop}{\textit{High Order Pattern}} + +\newboolean{release} +\newcommand{\release}[1]{\setboolean{release}{#1}} +\newcommand{\structpar}[1]{% + \ifthenelse{\boolean{release}}% + {\paragraph{}}% + {\paragraph{#1}}% +} + +\newboolean{outline} +\newcommand{\outline}[1]{\setboolean{outline}{#1}} + +\release{true} +\outline{false} +%% \par est équivalent à une ligne blanche + +\begin{document} + \maketitle + \tableofcontents + \clearpage + + \input{remerciements.tex} + \input{pres-univ.tex} + \input{gest-proj.tex} + \input{typer.tex} + \input{infer.tex} + \input{cc.tex} + \clearpage + + \appendix + \thispagestyle{empty} + \pagenumbering{roman} + + % TODO : remplir les parties dessous + % TODO : rajouter les citations ... + % \listoftables + \listoffigures + + \clearpage + \chapter*{Annexes} + \begin{figure}[h] + \centering + \verbatiminput{test2.typer} + \caption{Exemple de code typer} + \label{code:typer} + \end{figure} + \clearpage + \begin{figure}[h] + \centering + \begin{lstlisting}[language=caml] +type ltype = lexp + and lexp = + | Imm of sexp + | SortLevel of sort_level + | Sort of U.location * sort + | Builtin of vdef * ltype + | Var of vref + | Susp of lexp * subst + | Let of U.location * (vdef * lexp * ltype) list * lexp + | Arrow of arg_kind * vdef option * ltype * U.location * lexp + | Lambda of arg_kind * vdef * ltype * lexp + | Call of lexp * (arg_kind * lexp) lis + | Inductive of U.location * label + * ((arg_kind * vdef * ltype) list) + * ((arg_kind * vdef option * ltype) list) SMap.t + | Cons of vref * symbol + | Case of U.location * lexp + * ltype + * ltype + * (U.location * (arg_kind * vdef option) list * lexp) SMap.t + * lexp option + | Metavar of int * subst * vdef + \end{lstlisting} + \caption{Définition des \lexp{}} + \label{fig:ocmllxp} + \end{figure} + \begin{figure}[h] + \centering + \begin{lstlisting}[language=caml] +type substitution = lexp VMap.t (* VMap.t est une table associative *) +type constraints = (lexp * lexp) list +type unification_ctx = (substitution * constraints) + \end{lstlisting} + \caption{Contexte d'unification} + \label{fig:ctxunif} + \end{figure} + \clearpage + + \printindex + \printglossaries + \printbibliography +\end{document}

===================================== doc/rapport/pres-univ.tex ===================================== --- /dev/null +++ b/doc/rapport/pres-univ.tex @@ -0,0 +1,48 @@ +\chapter{Présentation de l'\udem{}} + + \section{L'université} + + \structpar{Chiffres} + L'\udem{} est une université située à Montréal au Canada. + Elle a été créée en 1878. + Tout les départements de l'\udem{} sont situés sur le même campus sur le Mont Royal. + + Elle est classée première université du Québec\cite{udemnum} et deuxième université du Canada\cite{udemnum}, que ce soit en nombre + d'étudiants ou pour la recherche. + + \structpar{Chiffres} + Cette université accueille près de \num{67 000} étudiants et \num{2 700} chercheurs dans 16 facultés et écoles\cite{udemnum}. + Elle dispose d'un budget de \num{1,05} milliard de dollards canadiens\cite{wikinum} (en 2014). + + L'\udem{} propose des programmes dans différents domaines d'études comme le droit, les sciences, la littérature \dots + \begin{figure}[!h] + \centering + \includegraphics[width=0.8\linewidth]{./img/DSCN0360.JPG} + \caption{\udem{}} +\label{fig:udem} + \end{figure} + \clearpage + + \section{Le département informatique} + + \structpar{Cursus possibles} + Le département informatique propose plusieurs cursus allant du développement web à la compilation. + + \structpar{LTP} + Le laboratoire dans lequel j'ai fait mon stage est le Laboratoire de Traitement Parallèle. + Il est composé de deux professeurs: Stefan Monnier et Marc Feeley. + + Initialement, ce laboratoire était dédié à des travaux sur le parallélisme. + Cependant, actuellement, le sujet de recherche des professeurs de ce laboratoire est la compilation. + \begin{figure}[!h] + \centering + \includegraphics[width=0.8\linewidth]{./img/DSCN0410.JPG} + \caption{Laboratoire de Traitement Parallèle} +\label{fig:ltp} + \end{figure} + + \structpar{Stefan Monnier} + Mon tuteur de stage était Stefan Monnier. Actuellement, ses sujets de recherche sont les langages de programmation fortement typés et les + langages sécurisés ainsi que les répercussions de ces langages sur les compilateurs, les \textit{runtimes system} et les systèmes d'exploitations. + Ces recherches l'ont amené à créer le langage \typer{} qui sert de preuve de concept pour un langage sécurisé et qui fournit des outils + pour la création de preuves de logiciels.

===================================== doc/rapport/remerciements.tex ===================================== --- /dev/null +++ b/doc/rapport/remerciements.tex @@ -0,0 +1,8 @@ +\chapter*{Remerciements} +Je tiens à remercier particulièrement mon tuteur monsieur Stefan Monnier de m'avoir accueilli dans son laboratoire +et de m'avoir permi de travailler sur un sujet que je n'aurai pas eu l'occasion d'étudier autrement. +Je le remercie aussi pour l'aide qu'il m'a apportée pendant ces treize semaines. + +Grâce à ce stage j'ai aussi eu la possibilité de découvrir Montréal. + +Je remercie aussi toutes les personnes que j'ai cotoyées dans ce laboratoire pour leur accueil chaleureux.

===================================== doc/rapport/typer.tex ===================================== --- /dev/null +++ b/doc/rapport/typer.tex @@ -0,0 +1,38 @@ +\chapter{Le langage \typer{}} + + \section{Présentation du langage} + \structpar{Description} + \typer{} est un langage de programmation fonctionnel pur. Il est total, typé statiquement et avec des types dépendants. + Les macros de \typer{} permettent de faire de la méta-programmation et d'étendre le langage + + Dans la suite du rapport, \say{\typer{}} fera référence au langage \typer{} et \say{le compilateur \typer{}} fera référence au compilateur + interprétant le langage \typer{} + + \structpar{Inspirations} + \typer{} est inspiré de \textit{Lisp}, \textit{Coq} et \textit{ML}. + Il est conceptuellement proche de \textit{Coq} (langage pur, total, typé statiquement et avec des types dépendants). Cependant, le but de \typer{} + est d'écrire des programmes et non des preuves. + Le système de macros de \typer{} est inspiré de \textit{Lisp}, il permet d'étendre facilement le langage + en manipulant le code comme des données. De plus, comme pour \textit{Lisp}, la syntaxe de \typer{} est stratifiée. + La syntaxe du code est proche de la syntaxe de \textit{ML}. L'inférence de type de \typer{} est un sur-ensemble de l'inférence de type + \textit{Hindley-Milner} + \structpar{Spécificités} + Les macros de \typer{} devraient, à terme, pouvoir être utilisées pour construire des preuves de programmes. % TODO : etoffer + + \section{Motivations} + \typer{} est un langage dont le but est de fournir des moyens d'écrire du code sûr. + En effet, les outils qu'il devrait fournir, à terme, facilitent l'écriture de code correct. + Par exemple, le compilateur de \typer{} peut vérifier qu'il n'y aura pas de récursion infinie. + De plus, les macros du langage devrait permettre, à terme, d'écrire des preuves de code. + + \section{État de l'implémentation} + \structpar{Avant} + Au début de mon stage, les bases du langage étaient implémentées: + la définition et l'appel de lambda, la création de type ainsi que la création de variables étaient supportées par le compilateur. + L'inférence de type n'étant pas implémentée, le compilateur requérait le typage explicite des variables et des paramètres de fonction. + Le compilateur fournissait peu de fonctions et opérations. + + \structpar{Après} + `A la fin du stage, une version basique de l'inférence de type était en cours d'intégration: il restait quelques bogues à résoudre avant que + cette version soit fonctionnelle. En effet, l'intégration de l'unification à système de typage a requis certaines modifications dans + ce système. Ces modifications ont entrainées des erreurs qui n'ont pas pu être résolues à temps.

View it on GitLab: https://gitlab.com/monnier/typer/compare/a84525ada25832cca6c86272fbddaeb6062...