Detalles

1 files changed, 36 insertions, 24 deletions

diff --git a/memoria.tex b/memoria.tex
index 91cb653..08cfc3d 100755
--- a/memoria.tex
+++ b/memoria.tex
@@ -392,8 +392,8 @@ aritmética entera, etc., y a menudo son capaces de resolver de forma automátic
 partes repetitivas y tediosas de las demostraciones, liberando de esa carga de
 trabajo al criptógrafo.
 
-\section{Motivación y objetivos}
-\label{sec:motiv-y-objet}
+\section{Objetivos}
+\label{sec:objetivos}
 
 Para este trabajo se ha decidido contribuir dentro de lo posible a mejorar el
 sistema EasyCrypt, desarrollado principalmente en el Instituto IMDEA Software en
@@ -448,7 +448,7 @@ distinta índole:
 La principal aportación de EasyCrypt con respecto a otros demostradores de
 teoremas como Coq\footnote{\url{http://coq.inria.fr/}} o
 Isabelle/HOL\footnote{\url{http://isabelle.in.tum.de/}} son todas las
-facilidades que proporciona para trabajar concretamente en el ámbito de la
+facilidades que proporciona para trabajar, concretamente, en el ámbito de la
 criptografía. Algunos ejemplos son el soporte a demostraciones basadas en
 secuencias de juegos, la riqueza de juicios (lógica de Hoare y variantes) o su
 exhaustiva biblioteca estándar, que define tipos de datos habituales (cadenas de
@@ -618,11 +618,11 @@ los más destacables son los dos siguientes:
   problema, si es que existe. Para contar con una única interfaz de
   programación ante la diversidad de resolvedores, EasyCrypt usa la plataforma
   \textbf{Why3}\footnote{\url{http://why3.lri.fr/}}.
-\item
-  \textbf{Menhir}\footnote{\url{http://gallium.inria.fr/~fpottier/menhir/}}.
+\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. Volveremos a esto una vez hayamos introducido las fases del análisis
-  del lenguaje a continuación.
+  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.
 \end{itemize}
 
 A fin de cuentas, EasyCrypt es un intérprete: lee un fichero fuente y realiza
@@ -646,14 +646,13 @@ identificador, comentario, inicio de bloque, etc. La salida de esta fase es una
 lista conteniendo todos los tokens que describen el programa original, formando
 una estructura de datos muy simple pero más sencilla de recorrer y manejar.
 
-\item \textbf{Análisis sintáctico}
-Durante esta fase se transforma la lista de tokens generada durante el análisis
-léxico en el denominado \textbf{árbol sintáctico abstracto}, una estructura de
-datos que contiene la estructura sintáctica del código fuente. Este analizador
-está especificado por la gramática formal del lenguaje (gramáticas libres de
-contexto, por lo general), cuyas reglas determinan el algoritmo a seguir durante
-la construcción del árbol sintáctico.
-L
+\item \textbf{Análisis sintáctico} Durante esta fase se transforma la lista de
+  tokens generada durante el análisis léxico en el denominado \textbf{árbol
+    sintáctico abstracto} (AST), una estructura de datos que contiene la
+  estructura sintáctica del código fuente. Este analizador está especificado por
+  la gramática formal del lenguaje (gramáticas libres de contexto, por lo
+  general), cuyas reglas determinan el algoritmo a seguir durante la
+  construcción del árbol sintáctico.  L
 \item \textbf{Análisis semántico/contextual}
 Durante esta fase se recorre el árbol sintáctico generado previamente y se anota
 con información de tipos, se construye la tabla de símbolos y se comprueba que
@@ -674,45 +673,58 @@ El siguiente diagrama resume el proceso de análisis del lenguaje de EasyCrypt:
 
 \tikzstyle{block} = [rectangle, draw, fill=blue!20,
     text width=5em, text centered, rounded corners, minimum height=4em]
-\tikzstyle{invisbl} = [
-    text width=5em, text centered, rounded corners, minimum height=4em]
+\tikzstyle{invisbl} = [text width=5em, text centered, minimum height=4em]
 \tikzstyle{line} = [draw, -latex']
-\tikzstyle{cloud} = [draw, ellipse,fill=green!20, node distance=3cm,
+\tikzstyle{cloud} = [draw, ellipse,fill=blue!10, node distance=3cm,
     minimum height=2em]
 
 \begin{center}
 \begin{tikzpicture}[node distance = 3cm, auto]
     % Nodes
-    \node [block] (lexer) {EcLexer};
+    \node [invisbl] (upper) {};
+    \node [block, below of=upper] (lexer) {EcLexer};
     \node [block, below of=lexer] (parser) {EcParser};
     \node [block, below of=parser] (typing) {EcTyping};
-    \node [invisbl, below of=typing] (resto) {...};
+    \node [invisbl, below of=typing] (lower) {...};
     \node [cloud, left of=lexer] (menhir1) {Menhir};
     \node [cloud, left of=parser] (menhir2) {Menhir};
     % Edges
     \path [line,dashed] (menhir1) -- (lexer);
     \path [line,dashed] (menhir2) -- (parser);
     \path [line]
-    (lexer) edge [] node {\textbf{Tokens} (en EcParser/EcLexer)} (parser)
-    (parser) edge [] node {\textbf{AST} (en EcParseTree)} (typing)
-    (typing) edge [] node {\textbf{AST tipado} (en EcFol)} (resto);
+    (upper) edge [] node {\textbf{Código fuente}} (lexer)
+    (lexer) edge [] node {\textbf{Tokens} (EcParser/EcLexer)} (parser)
+    (parser) edge [] node {\textbf{AST} (EcParseTree)} (typing)
+    (typing) edge [] node {\textbf{AST tipado} (EcFol)} (lower);
 \end{tikzpicture}
 \end{center}
 
 Para la implementación del coste es necesario modificar cada uno de los módulos
-involucrados en esta cadena. A continuación analizaremos cada una de las etapas
+involucrados en este proceso. A continuación analizaremos cada una de las etapas
 de la 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
+
 \section{Modificaciones al analizador sintáctico}
 \label{sec:modif-al-anal-sin}
 
+TODO: Más Menhir, modificaciones en EcParser y EcParseTree
+
 \section{Modificaciones al analizador semántico}
 \label{sec:modif-al-anal-sem}
 
+TODO: Modificaciones en EcTyping, EcFol, EcEnv, EcScope, EcTheory, EcPV,
+EcCommands... :)
+
+\section{Modificaciones al pretty-printer}
+\label{sec:modif-al-anal-sem}
+
+TODO: Modificaciones en EcPrinting
+
 \chapter{DESARROLLO: INTERFAZ WEB}
 
 \chapter{RESULTADOS Y CONCLUSIONES}