1 files changed, 50 insertions, 4 deletions
diff --git a/memoria.tex b/memoria.tex
index e666b72..7b54c31 100755
--- a/memoria.tex
+++ b/memoria.tex
@@ -10,6 +10,14 @@
 
 \usepackage{tikz}
 
+\usepackage{float}
+\floatstyle{boxed}
+\newfloat{ocaml}{thp}{ext}
+
+\usepackage{alltt}
+\usepackage{color}
+\input{ocaml_colors}
+
 \usetikzlibrary{shapes,arrows}
 
 \input{defs}
@@ -627,9 +635,9 @@ los más destacables son los dos siguientes:
   \textbf{Why3}\footnote{\url{http://why3.lri.fr/}}.
 \item \textbf{Menhir}\footnote{\url{http://gallium.inria.fr/~fpottier/menhir/}}.
   Menhir es una biblioteca para generar analizadores léxicos y sintácticos en
-  OCaml. Se verá con mayor profundidad en la sección
-  \ref{sec:modif-al-anal-lex}, tras explicar las fases del análisis del
-  lenguaje.
+  OCaml. Se verá con mayor profundidad en las secciones
+  \ref{sec:modif-al-anal-lex} y \ref{sec:modif-al-anal-sin}, tras explicar las
+  fases del análisis del lenguaje.
 \end{itemize}
 
 A fin de cuentas, EasyCrypt es un intérprete: lee un fichero fuente y realiza
@@ -713,7 +721,45 @@ implementación tanto del operador especial de coste como del axioma de coste.
 \section{Modificaciones al analizador léxico}
 \label{sec:modif-al-anal-lex}
 
-TODO: Menhir, modificaciones en EcLexer
+EcLexer es el módulo que define el analizador léxico. Este módulo está contenido
+en el fichero <<ecLexer.mll>>, cuya extensión refleja el hecho de que no es un
+fichero OCaml válido, sino un fichero de definición de analizadores léxicos que
+deberá ser procesado por Menhir para generar el analizador real.
+
+La función principal de este módulo es asociar expresiones regulares con sus
+tokens correspondientes. Por ejemplo, la expresión regular \textbf{[0-9]*} emite
+el token UINT (Unsigned INTeger) parametrizado por el valor de la cadena
+coincidente convertida a número entero.
+
+La única modificación que debemos realizar a este módulo es el reconocimiento de
+nuestros dos nuevos tokens: \textbf{cost} y \textbf{caxiom}. Estos tokens son
+palabras reservadas: identificadores con significado especial dentro del
+lenguaje. En EcLexer, cuando se encuentra un identificador, se busca dentro de
+un \textbf{hash map} que relaciona palabras reservadas con sus respectivos
+tokens: en caso de existir la clave, se emite el token asociado; en caso
+contrario, se emite el token genérico IDENT. Por tanto, basta con añadir dos
+entradas a este hash map para que EcLexer emita los tokens COST y CAXIOM cuando
+encuentre los identificadores `cost` y `caxiom`, respectivamente:
+
+\begin{ocaml}
+\begin{alltt}
+
+\Clet{let} _keywords \Cnonalphakeyword{=} \Cnonalphakeyword{[}
+  \Cstring{"admit"} \Cnonalphakeyword{,} \Cconstructor{ADMIT}\Cnonalphakeyword{;}
+  \Cstring{"forall"}\Cnonalphakeyword{,} \Cconstructor{FORALL}\Cnonalphakeyword{;}
+  \Cstring{"exists"}\Cnonalphakeyword{,} \Cconstructor{EXIST}\Cnonalphakeyword{;}
+  \Cstring{"pragma"}\Cnonalphakeyword{,} \Cconstructor{PRAGMA}\Cnonalphakeyword{;}
+  \Ccomment{(* ... *)}
+
+  \Cstring{"cost"}  \Cnonalphakeyword{,} \Cconstructor{COST}\Cnonalphakeyword{;}
+  \Cstring{"caxiom"}\Cnonalphakeyword{,} \Cconstructor{CAXIOM}
+\Cnonalphakeyword{]}
+
+\Clet{let} keywords \Cnonalphakeyword{=} \Cconstructor{Hashtbl}\Cnonalphakeyword{.}create 100
+\Clet{let} \Cnonalphakeyword{_} \Cnonalphakeyword{=} \Cconstructor{List}\Cnonalphakeyword{.}iter
+    \Cnonalphakeyword{(}\Cfun{fun} \Cnonalphakeyword{(}x\Cnonalphakeyword{,} y\Cnonalphakeyword{)} \Cnonalphakeyword{->} \Cconstructor{Hashtbl}\Cnonalphakeyword{.}add keywords x y\Cnonalphakeyword{)} _keywords
+\end{alltt}
+\end{ocaml}
 
 \section{Modificaciones al analizador sintáctico}
 \label{sec:modif-al-anal-sin}