Ismaila FALL pushed to branch track-sexp-lexp at Stefan / Typer

Commits: 3c702b98 by “falismai@iro.umontreal.ca” at 2022-04-14T22:13:57+00:00 redac

- - - - -

6 changed files:

- + Rapport/template.tex - − redaction/Rapport Mémoire Typer.zip - src/debruijn.ml - src/debug.ml - src/lexp.ml - src/opslexp.ml

Changes:

===================================== Rapport/template.tex ===================================== @@ -0,0 +1,420 @@ +\documentclass[a4paper, 12pt]{report} +\usepackage[utf8]{inputenc} +\usepackage{microtype} +\usepackage{hyperref} +\hypersetup{ + colorlinks, + citecolor = black, + filecolor = black, + linkcolor = black, + urlcolor = black +} +\usepackage{glossaries} +\makeglossaries +\usepackage{enumitem} +\usepackage{rotating} +\usepackage[colorinlistoftodos]{todonotes} +\usepackage[most]{tcolorbox} +\usepackage{afterpage} +\usepackage{amsmath} +\usepackage{graphicx} +\usepackage{url} +\usepackage[Lenny]{fncychap} +\usepackage{ulem} +\usepackage{listings} +\usepackage{upquote} +\usepackage{pxfonts} +\usepackage{tcolorbox} +\usepackage{minted} + +\tcbuselibrary{skins} +\newtcblisting{cppcode}[1][]{ + listing engine = minted, + listing only, + minted language = cpp, + minted options = {linenos=true, numbersep=3mm, texcl=true, #1}, + left = 5mm, + enhanced, + overlay = { + \begin{tcbclipinterior}\fill[black!25] (frame.south west) + rectangle ([xshift=5mm]frame.north west); + \end{tcbclipinterior}} +} +\newcommand \FOO {$`#1`$} + + + + \renewcommand{\baselinestretch}{1.5} + \usepackage{mathptmx} + \usepackage{fancyhdr} + \pagestyle{fancy} + \fancyhf{} + \chead{} + \rfoot{\thepage} + \lfoot{\tiny{Amélioration des messages d'erreurs Typer par Algorithme Génétique \ Ismaïla Fall}} + \rhead{\fancyplain{}{\textit{\leftmark}}} + \usepackage{tabularx} + \usepackage{caption} + \usepackage[frenchb]{babel} + \usepackage{subcaption} +\addto{\captionsfrench}{ + \renewcommand{\mtctitle}{Sommaire} + \renewcommand{\tablename}{Tableau} + \renewcommand{\bibname}{Références} +} + + +\newcommand{\tabitem}{~~\llap{\textbullet}~~} + \usepackage{graphicx} + \usepackage{minitoc} + \usepackage{float} + \setcounter{secnumdepth}{3} + \setcounter{tocdepth}{2} + + + \title{Amélioration des messages d'erreurs Typer par Algorithme Génétique} +\author{Ismaïla FalIsmaïla Fal} +\date{} +\definecolor{myblue}{RGB}{51,51,153} +\newcommand\blankpage{% + \null + \thispagestyle{empty}% + \addtocounter{page}{-1}% + \newpage} + + +\newsavebox{\mybox} +\newlength{\mydepth} +\newlength{\myheight} + +\newenvironment{sidebar}% +{\begin{lrbox}{\mybox}\begin{minipage}{\textwidth}}% +{\end{minipage}\end{lrbox}% + \settodepth{\mydepth}{\usebox{\mybox}}% + \settoheight{\myheight}{\usebox{\mybox}}% + \addtolength{\myheight}{\mydepth}% + \noindent\makebox[0pt]{\hspace{-40pt}\rule[-\mydepth]{1pt}{\myheight}}% + \usebox{\mybox}} + + \newcommand{\HRule}{\rule{\linewidth}{0.4mm}} % Defines a new command for the horizontal lines, change thickness here + + +\begin{document} + +\begin{titlepage} + +\centering % Center everything on the page + +%---------------------------------------------------------------------------------------- +% HEADING SECTIONS +%---------------------------------------------------------------------------------------- + +%\textsc{\normalsize \textbf{Université de Montréal}}\[0.3cm] % Name of your university/college +%\includegraphics[scale=.1]{img/flag}\[0.15cm] +\text{\Large \text{Université de Montréal}}\[1.5cm] +%\includegraphics[scale=.2]{img/ucad}\[0.15cm] % Include a department/university logo - this will require the graphicx package +\text{\Large \text{Amélioration des messages d'erreurs Typer }}\ % Major heading such as course name +\text{\Large \text{par Algorithme Génétique}}\[1.5cm] % Major heading such as course name +\text{\normalsize \text{par}}\[0.5cm] +\text{\Large {\text {Ismaïla Fall}}}\[1cm] % Minor heading such as course title +\text{\small {\text {Département de mathématiques et de statistique }}}\ % Minor heading such as course title +\text{\small {\text {Faculté des arts et des sciences}}}\[2.5cm] % Minor heading such as course title + +\text{\small {\text {Mémoire présenté en vue de l’obtention du grade de }}}\ +\text{\small {\text {Maître ès sciences (M.Sc.)}}}\ +\text{\small {\text {en Discipline }}}\[2.5cm] + +\text{\today}\[2cm] + +\text{\small {\text {©Ismaila Fall, 2022}}} + +%---------------------------------------------------------------------------------------- +% DATE SECTION +%---------------------------------------------------------------------------------------- + +\end{titlepage} +\thispagestyle{empty} +\clearpage\null + +% Deuxieme page de garde + +\begin{titlepage} + +\centering % Center everything on the page + +%---------------------------------------------------------------------------------------- +% HEADING SECTIONS +%---------------------------------------------------------------------------------------- + +\text{\Large \text{Université de Montréal}}\ +\text{\small { \uline{Faculté des arts et des sciences}}}\[0.8cm] % Minor heading such as course title + +\text{\small {\text {Ce mémoire intitulé}}}\[0.8cm] % Minor heading such as course title + +\text{\Large \text{Amélioration des messages d'erreurs Typer }}\ % Major heading such as course name +\text{\Large \text{par Algorithme Génétique}}\[1.5cm] % Major heading such as course name + +\text{\normalsize \text{présenté par}}\[0.4cm] +\text{\Large {\text {Ismaïla Fall}}}\[1cm] % Minor heading such as course title + + \text{\small {\text {a été évalué par un jury composé des personnes suivantes :}}}\[1cm] % Minor heading such as course title + +\text{\small {\uline {Nom du président du jury}}}\ +\text{\small {\text {(président-rapporteur)}}}\ [1cm] + +\text{\small {\uline {Stefan Monnier}}}\ +\text{\small {\text {(directeur de recherche)}}}\ [1cm] + +\text{\small {\uline {Nom du membre de jury}}}\ +\text{\small {\text {(membre du jury)}}}\ [1cm] + +%---------------------------------------------------------------------------------------- +% HEADING SECTIONS +%---------------------------------------------------------------------------------------- + + +\end{titlepage} +\newpage + +\pagenumbering{roman} +\dominitoc +\chapter*{Dédicaces \markboth{Dédicaces}{}} +\markboth{DÉDICACES}{} + + +\chapter*{Remerciements \markboth{Remerciements}{}} +\markboth{REMERCIEMENTS}{} + + +\chapter*{Avant-propos \markboth{Avant-propos}{}} + + +\tableofcontents +\chapter*{Sigles et Abréviations \markboth{Sigles et Abréviations}{}} + +\listoffigures +\listoftables + +%---------------------------------------------------------------------------------------- +% Resume +%---------------------------------------------------------------------------------------- + +\chapter*{Résumé \markboth{Résumé}{}} +Le défi majeur des programmeurs (plus précisément des novices) sont les messages d'erreur du compilateur. Nous nous intéressons au problème d'affichage de bon message d'erreur de compilation. Dans certains langages comme Typer, la vérification du type des expressions est faite lors de la compilation; ce qui oblige le compilateur à déduire les types de certaines ou de toutes les expressions; mais aussi d'envisager la meilleure manière d'écrire le type (dans le langage source) dans un message d'erreur. Cependant l'interprétation du type des expressions faite par le compilateur est toujours diffèrent de ce que l'utilisateur aimerait voir en cas d'erreur de compilation. En effet, il n'existe pas d'algorithme déterministe permettant de trouver une représentation naturelle dans le code source correspondant à la représentation interne d'un type. D'où l'importance d'implémenter un système heuristique tel que les algorithmes génétiques où les réseaux de neurones qui nous donne cette information; permettant ainsi un meilleur affichage du texte des messages d'erreur. Donc, nous avons décidé de travailler sur l'amélioration des messages d'erreur du compilateur Typer, dans sa phase de traduction du langage (interprétation et représentation des différents expressions dans le langage source) en proposant une approche `algorithme génétique`.\ +\textbf{Mots Clés: Message d'erreur, Typer, Algorithme génétique, Compilateur} + + +%---------------------------------------------------------------------------------------- +% Abstract +%---------------------------------------------------------------------------------------- + +\chapter*{Abstract \markboth{Abstract}{}} +The major challenge for programmers (more precisely for novices) are compiler error messages. We are interested in the problem of displaying a good compiler error message. In some languages like Typer, the type checking of expressions is done at compile time; this forces the compiler to deduce the types of some or all expressions; but also to consider the best way to write the type (in the source language) in an error message. However, the compiler's interpretation of the type of expressions is always different from what the user would like to see in case of a compiler error. Indeed, there is no deterministic algorithm allowing to find a natural representation in the source code corresponding to the internal representation of a type. Hence the importance of implementing a heuristic system such as genetic algorithms or neural networks that gives us this information; thus allowing a better display of the text of error messages. So, we decided to work on the improvement of the error messages of the Typer compiler, in its language translation phase (interpretation and representation of the different expressions in the source language) by proposing a `genetic algorithm` approach.\ +\textbf{Keywords: Error message, Typer, Genetic algorithm, Compiler} + +%\chapter*{Introduction \markboth{Introduction}{}} \mtcaddchapter +\newpage +\null +\newpage +%\addcontentsline{toc}{chapter}{Introduction} + +%---------------------------------------------------------------------------------------- +% Chapitre 1 +%---------------------------------------------------------------------------------------- +\pagenumbering{arabic} +% CHAPITRE 1 +\chapter{Introduction Générale} +\textit{\textbf{Résumé:} \ +Dans ce chapitre, nous faisons une description de notre sujet en dégageant le contexte, la problématique ainsi que les objectifs que nous nous sommes fixes. Enfin, de bien mettre en avant le travail réalisé, nous présenterons les différents chapitres de ce mémoires. +} +\setcounter{minitocdepth}{2} +\minitoc +\newpage + +\section{Contexte} +Typer est un langage de programmation fortement typé qui appartient à la famille ML. La vérification de type statique faite lors de la compilation lui permet de fournir une sécurité de type au programmeur. Comme beaucoup de langage fonctionnelle, le système de type de Typer est inspiré en grand parti du système de type Hindley-Milner. \ +Le système de type Hindley-Milner combiné avec les macros expansions forment la partie élaboration (compilateur) de Typer. Cette combinaison de polymorphisme et d'interface de type permet de définir de nouveau type de donnée, augmentant ainsi la productivité des programmeurs mais aussi la fiabilité du système de type. Cependant elle n'est pas sans inconvénient, le signalement des messages d'erreur de type devient plus difficile. En effet, le compilateur n'indique pas précisément la source de l'erreur de type; mais aussi il arrive généralement que les types inférés ne correspondent pas aux types voulus. C'est dans cette optique qu'on nous a confié la tâche de proposer une solution algorithme génétique pour tenter d'amélioration les messages d'erreur du compilateur Typer. + + +\section{Problématique} +Implémenter à base par un langage similaire à Coq, Typer utilise un système de type dépendant, qu'il combine avec un système de macro puissant. Ce qui permet d'étendre le langage via la méta-programmation de manière transparente.\ +Cependant ce système de typage dépendant combiné avec la méta-programmation faite qu'on a un sérieux problème d'afficher de bon message d'erreur (généralement des erreurs de type). Mais d'autres problèmes supplémentaires viennent de certaines détails de Typer (tel que l'absence de mot réservés) qui implique que le type d'une valeur peut dépendre d'une autre valeur obtenue qu'au moment de la compilation. \ +Prenons par exemple la définition de type suivante: +\begin{cppcode} +type List (a : Type) + | nil + | cons (hd : a)(tl : List a); +\end{cppcode} + +Dans ce extrait, nous avons une fonction \FOO{List} qui prend en argument $`a`$ qui est un type et renvoie un nouveau type \FOO{List a}. Ce nouveau type est décrit comme étant formé soit de la constante $`nil`$ c'est-à-dire la liste vide; soit d'une valeur de la forme \mathit{`cons hd tl`} ou \mathit{`cons`} est un tag qui permet de reconnaître cette valeur, $`hd`$ est le premier élément de la liste et $`tl`$ est une référence qui pointe vers le reste de la liste.\ +Examinons la déclaration suivante: +\begin{cppcode} + x = cons 1 nil; +\end{cppcode} + +Nous avons dans $`x`$ une liste qui contient juste un entier (le chiffre 1). $`x`$ est de type \FOO{List Int}, qui est la représentation que le programmeur aimerait voir, dans Typer, mais au contraire il aura à la place un type qui représente plutôt à quelques choses comme ça : +\begin{cppcode} + typecons <qqch> (nil)(cons (hd : ##Int)(tl : List ##Int)) +\end{cppcode} + +Cette ligne incompréhensible pour le programmeur est le résultat de l'élaboration du code source, qui équivaut à \FOO{List Int} et donc ce sont deux représentations différentes du même type. Très souvent, ce résultat est diffèrent du code source. Au pire la bonne représentation qu'on aimerait utiliser (comme dans notre exemple \FOO{List Int}) n'est souvent présent nulle part dans le code source.\ +Dès lors, le problème qui se pose est comment transformer la forme incompréhensible en quelques choses comme \FOO{List Int}. + + +\section{Contributions} +Dans le but de proposer une solution au problème cité ci-dessus, notre contributions est de réaliser un système heuristique basé sur les algorithmes génétiques qui permettent au compilateur Typer de faire une meilleur représentation des messages d'erreur. Pour y arriver, nous nous sommes fixe des objectifs spécifiques, listés ci-dessous: +\begin{itemize} + \item[\Rightarrow] Apporter quelques modifications au compilateur en extrayant des informations utiles sur certaines parties. + + \item[\Rightarrow] Collecter et organiser quelques données qui nous permettrons d'entraîner et de tester notre système heuristique. + + \item[\Rightarrow] Implémenter un algorithme génétique pour mettre au compilateur Typer de générer de meilleur message d'erreur, compréhensible pour le programmeur. +\end{itemize} +\vspace{10pt} + + +\section{Plan} +Dans le but de bien mettre en avant le travail réalisé, nous structurons ce mémoire en quart (04) chapitres: +\begin{enumerate} + \item \textbf{État de l'art} : Il s'agit dans ce chapitre de faire une présentation des caractéristiques de notre projet. Dans un premier temps, nous faisons une synthèse des travaux étroitement liées à notre projet d'étude; ensuite, nous présenterons Typer plus précisément de son compilation. En troisième point, nous les systèmes heuristiques seront visités particulièrement les algorithmes génétiques. + + \item \textbf{Implémentions de la solution} : pour ce chapitre, il sera question d'exposer la stratégie de collection des données et la mise en oeuvre de la solution. + + \item \textbf{Évaluation du résultat } : ce chapitre permet de dévaluer l'aspect de notre travail. + + \item \textbf{Conclusion} : Finalement, ce chapitre permet d'exposer nos conclusions avant de finir par les limites et perspectives. \ \ +\end{enumerate} + +\textit{\textbf{Synthèse:} \ + Dans ce chapitre, nous avons décrit notre sujet de recherche en dégageant le contexte, la problématique et les objectifs. Nous y avons aussi profité pour présenter les différents chapitres qui composent notre mémoire. \ +Cependant, il a toujours été difficile de déduire la source d'un erreur à partir du message générer par le compilateur. Le prochaine chapitre fera donc l'objet d'une synthèse détail des études existant en rapport avec nos travaux; suivi de la présentation de Typer et des algorithmes génétiques. +} + + +%---------------------------------------------------------------------------------------- +% Chapitre 2 +%---------------------------------------------------------------------------------------- + +%CHAPITRE 2 +\chapter{ État de l'art } +\textit{\textbf{Résumé:} Ce chapitre consiste à mettre l'accent sur l'état de l'art des erreurs de compilations. Il s'agit de faire une synthèse de quelques travaux connexes qui essayent d'améliorer les messages d'erreur génère par le compilateur; de présenter ensuite le langage Typer ainsi que son compilateur et enfin nous finissons par parler des systèmes heuristiques particulièrement des algorithmes génétiques. +} +\setcounter{minitocdepth}{1} +\minitoc +\newpage + +\section{Travaux Connexes} +Un langage de programmation avec un système de type permet d'assurer le programmeur sur l'exactitude de son programme; elle permet au compilateur de rejeter les programmes non typé ou mal typés. Mais le problème de beaucoup de programmeur survient lorsque le compilateur rejette leur programme; en effet le processus de débogage est souvent fastidieux et inefficace. C'est dans cette optique que beaucoup de travaux ont vu le jour + + + +\section{Présentation de Typer} +\subsection{Structure de Typer} + +\subsection{Élaboration} +\subsubsection{Macro-expansions} +\subsubsection{Inférence de Type} + + + +\section{Les Algorithmes génétiques} +\subsection{les systèmes heuristiques} +\subsection{les algorithmes génétiques} + + +\textit{\textbf{Synthèse:} \ +conclusion +} + + +%---------------------------------------------------------------------------------------- +% Chapitre 3 +%---------------------------------------------------------------------------------------- + +%CHAPITRE 3 +%\chapter{ Aperçu de Typer } +%\textit{\textbf{Résumé:} } +%\setcounter{minitocdepth}{1} +%\minitoc + +%\section{Définitions des concepts du domaine} + +%\section{Fonctionnalités existantes} +%\subsection{Les modules existants} + +%\section{Architecture et Technologies utilisées} +%\subsection{Architecture technique} +%\subsection{Architecture applicative} + + + +%---------------------------------------------------------------------------------------- +% Chapitre 4 +%---------------------------------------------------------------------------------------- + +%CHAPITRE 4 +%\chapter{Les algorithmes génétiques} +%\textit{\textbf{Résumé:}} +%\setcounter{minitocdepth}{2} +%\minitoc +%\section{Les acteurs de l'application} +%\section{Présentation du domaine} + +%---------------------------------------------------------------------------------------- +% Chapitre 5 +%---------------------------------------------------------------------------------------- + +%CHAPITRE 5 +\chapter{Implémentions de la solution} +\textit{\textbf{Résumé : }} +\setcounter{minitocdepth}{1} +\minitoc +\newpage +\section{Solution technique} + +\section{Architecture de la plateforme} + + +%---------------------------------------------------------------------------------------- +% Chapitre 6 +%---------------------------------------------------------------------------------------- + + +%CHAPITRE 6 +\chapter{Évaluation du résultat} +\textit{\textbf{Résumé:} } +\minitoc +\newpage + + + +%---------------------------------------------------------------------------------------- +% Chapitre 7 +%---------------------------------------------------------------------------------------- + +%CHAPITRE 7 +\chapter{Conclusion et Perspectives} +\textit{\textbf{Résumé:} } +\minitoc +\newpage + +%\chapter*{Conclusion et Perspectives} \mtcaddchapter +%\markboth{Conclusion et Perspectives}{} +%\addcontentsline{toc}{ch1apter}{Conclusion et Perspectives} + +\bibliographystyle{plain} +\bibliography{biblio} + +\chapter*{Annexes} \mtcaddchapter +\addcontentsline{toc}{chapter}{Annexes} +\markboth{Annexes}{} +\newpage + + +\section*{Résumé \markboth{}{}} +\thispagestyle{empty} + + +\section*{Abstract \markboth{}{}} + +\end{document}

===================================== redaction/Rapport Mémoire Typer.zip deleted ===================================== Binary files "a/redaction/Rapport M\303\251moire Typer.zip" and /dev/null differ

===================================== src/debruijn.ml ===================================== @@ -368,17 +368,16 @@ let lctx_lookup (ctx : lexp_context) (v: vref): env_elem = else fun () -> summarize_lctx ctx dbi in fatal - ~loc ~print_action + ~loc:(sexp_location loc) ~print_action ({|DeBruijn index %d refers to wrong name. |} ^^ {|Expected: "%s" got "%s"|}) dbi ename name | _ -> () in - ret with | Not_found -> fatal - ~loc "DeBruijn index %d of `%s` out of bounds" dbi (maybename oename) + ~loc:(sexp_location loc) "DeBruijn index %d of `%s` out of bounds" dbi (maybename oename)

let lctx_lookup_type (ctx : lexp_context) (vref : vref) : lexp = let (_, i) = vref in

===================================== src/debug.ml ===================================== @@ -137,7 +137,7 @@ let debug_lexp_decls decls =

let str = match str with | scd :: tl - -> printf " FILE: %-25s : %s\n" loc.file scd; + -> printf " FILE: %-25s : %s\n" (Source.Location.to_string (sexp_location loc)) scd; tl | _ -> [] in

===================================== src/lexp.ml ===================================== @@ -540,7 +540,7 @@ let rec lexp_location e =

(********* Normalizing a term *********)

-let vdummy = (U.dummy_location, None) +let vdummy = (dummy_sinfo, None) let maybename n = match n with None -> "<anon>" | Some v -> v let sname (l, n) = (sexp_location l, maybename n)

===================================== src/opslexp.ml ===================================== @@ -230,7 +230,7 @@ let rec lexp_whnf_aux e (ctx : DB.lexp_context) : lexp = -> let subst = S.cons (get_refl e') (S.substitute e') in lexp_whnf_aux (push_susp default subst ) ctx | _ -> Log.log_error - ~section:"WHNF" ~loc:l + ~section:"WHNF" ~loc:(sexp_location l) {|Unhandled constructor "%s" in case expression|} name; mkCase (l, e, rt, branches, default) in (match lexp_lexp' e' with @@ -413,7 +413,7 @@ and conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = let ekind = get_type ctx etype in let elvl = match lexp'_whnf ekind ctx with | Sort (_, Stype l) -> l - | _ -> Log.log_fatal ~loc:(lexp_location ekind) + | _ -> Log.log_fatal ~loc:(sexp_location (lexp_location ekind)) "Target lexp's kind is not a sort"; in (* 1. Get the inductive for the field types *) let it, aargs = match lexp_lexp' etype with @@ -468,7 +468,7 @@ and conv_p' (ctx : DB.lexp_context) (vs : set_plexp) e1 e2 : bool = let subst = S.shift offset in let eaargs = List.map (fun (_, a) -> (P.Aerasable, a)) aargs in - let ctor = mkSusp (mkCall (mkCons (it, (DB.dloc, l1)) , + let ctor = mkSusp (mkCall (mkCons (it, (sexp_location (DB.dloc), l1)) , eaargs) ) subst in let hlxp = mkCall (ctor, args) in let nctx = ctx_extend_with_eq nctx subst hlxp in @@ -589,7 +589,7 @@ and check'' erased ctx e = if conv_p ctx t t' then () else log_tc_error - ~loc:(lexp_location e) + ~loc:(sexp_location (lexp_location e)) "Type mismatch for %s : %s != %s" (lexp_string e) (lexp_string t) (lexp_string t') in @@ -599,14 +599,14 @@ and check'' erased ctx e = | Sort _ -> () | _ -> let loc = lexp_location t in - log_tc_error ~loc "Not a proper type: %s" (lexp_string t)); + log_tc_error ~loc:(sexp_location loc) "Not a proper type: %s" (lexp_string t)); s in match lexp_lexp' e with | Imm (Float (_, _)) -> DB.type_float | Imm (Integer (_, _)) -> DB.type_int | Imm (String (_, _)) -> DB.type_string | Imm (Block (_, _) | Symbol _ | Node (_, _)) - -> (log_tc_error ~loc:(lexp_location e) "Unsupported immediate value!"; + -> (log_tc_error ~loc:(sexp_location (lexp_location e)) "Unsupported immediate value!"; DB.type_int ) | SortLevel SLz -> DB.type_level | SortLevel (SLsucc e) @@ -637,7 +637,7 @@ and check'' erased ctx e = | Var (((loc, name), idx) as v) -> if DB.set_mem idx erased then log_tc_error - ~loc + ~loc:(sexp_location loc) {|Var `%s` can't be used here, because it's erasable|} (maybename name) ; lookup_type ctx v @@ -670,13 +670,13 @@ and check'' erased ctx e = match sort_compose ctx nctx loc ak k1 k2 with | SortResult k -> k | SortInvalid - -> log_tc_error ~loc "Invalid arrow: inner TypelLevel argument"; + -> log_tc_error ~loc:(sexp_location loc) "Invalid arrow: inner TypelLevel argument"; mkSort (loc, StypeOmega) | SortK1NotType - -> log_tc_error ~loc:(lexp_location t1) "Not a proper type"; + -> log_tc_error ~loc:(sexp_location (lexp_location t1)) "Not a proper type"; mkSort (loc, StypeOmega) | SortK2NotType - -> log_tc_error ~loc:(lexp_location t2) "Not a proper type"; + -> log_tc_error ~loc:(sexp_location (lexp_location t2)) "Not a proper type"; mkSort (loc, StypeOmega) ) | Lambda (ak, ((l,_) as v), t, e) -> (let _k = check_type DB.set_empty ctx t in @@ -693,11 +693,11 @@ and check'' erased ctx e = match lexp'_whnf ft ctx with | Arrow (ak', _v, t1, _l, t2) -> if ak != ak' - then log_tc_error ~loc:(lexp_location arg) "arg kind mismatch"; + then log_tc_error ~loc:(sexp_location (lexp_location arg)) "arg kind mismatch"; assert_type ctx arg at t1; mkSusp t2 (S.substitute arg) | _ -> log_tc_error - ~loc:(lexp_location arg) + ~loc:(sexp_location (lexp_location arg)) "Calling a non functin (type = %s)!" (lexp_string ft); ft) ft args @@ -725,7 +725,7 @@ and check'' erased ctx e = (mkSusp level' (L.sunshift n) ) | _tt -> log_tc_error - ~loc:(lexp_location t) + ~loc:(sexp_location (lexp_location t)) ~print_action:(fun _ -> DB.print_lexp_ctx ictx; print_newline ()) "Field type %s is not a Type! (%s)" @@ -759,7 +759,7 @@ and check'' erased ctx e = let ekind = get_type ctx etype in let elvl = match lexp'_whnf ekind ctx with | Sort (_, Stype l) -> l - | _ -> Log.log_error ~loc:(lexp_location ekind) + | _ -> Log.log_error ~loc:(sexp_location (lexp_location ekind)) "Target lexp's kind is not a sort"; DB.level0 in let it, aargs = call_split etype in (match lexp'_whnf it ctx, aargs with @@ -772,7 +772,7 @@ and check'' erased ctx e = * returns a valid type. *) -> mksubst (S.cons aarg s) fargs aargs | _ - -> log_tc_error ~loc:l "Wrong arg number to inductive type!"; + -> log_tc_error ~loc:(sexp_location l) "Wrong arg number to inductive type!"; s in let s = mksubst S.identity fargs aargs in let ctx_extend_with_eq ctx subst hlxp nerased =

View it on GitLab: https://gitlab.com/monnier/typer/-/commit/3c702b98d43ea8e528c36a54884fc9aa1e...