Sintáctico

1 files changed, 105 insertions, 21 deletions

diff --git a/memoria.tex b/memoria.tex
index ec9c4c2..1cfdf99 100755
--- a/memoria.tex
+++ b/memoria.tex
@@ -550,8 +550,6 @@ A lo largo de este capítulo se detallará el proceso que se ha seguido para
 implementar la funcionalidad que permita a la especificación del coste de
 algoritmos en EasyCrypt.
 
-TODO referencias a dónde se explica qué.
-
 \newpage
 \section{Motivación}
 \label{sec:motivacion}
@@ -720,14 +718,14 @@ de abstracción distintos. Conceptualmente, las fases de análisis son las
 siguientes:
 
 \begin{itemize}
-\item \textbf{Análisis léxico}
-Esta fase es la primera que se lleva a cabo y la que tiene un menor nivel de
-abstracción; su entrada es el propio fichero fuente. Durante el análisis léxico
-se transforma la secuencia de caracteres que forma el código fuente en unidades
-mínimas de información (\textbf{tokens}): número, cadena de caracteres,
-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 léxico} Esta fase es la primera que se lleva a cabo y la
+  que tiene un menor nivel de abstracción; su entrada es el propio fichero
+  fuente. Durante el análisis léxico se transforma la secuencia de caracteres
+  que forma el código fuente en unidades mínimas de información
+  (\textbf{tokens}): número, cadena de caracteres, 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
@@ -736,21 +734,21 @@ una estructura de datos muy simple pero más sencilla de recorrer y manejar.
   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.
-\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
-el programa, además de estar bien formado sintácticamente, tiene sentido
-semánticamente.
+
+\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 el programa, además de estar
+  bien formado sintácticamente, tiene sentido semánticamente.
 \end{itemize}
 
 EasyCrypt implementa cada una de estas etapas en tres módulos (EcLexer, EcParser
 y EcTyping) y define las estructuras de datos intermedias en otros dos
 (EcParseTree para el árbol sintáctico abstracto y EcFol para el árbol sintáctico
 anotado con información de tipos). Los módulos EcLexer y EcParser hacen uso de
-la biblioteca Menhir mencionada anteriormente para generar los
-analizadores. Estos módulos contienen las definiciones de tokens y las reglas de
-las gramáticas regular y libre de contexto usadas para indicar, respectivamente,
-el comportamiento de los analizadores léxico y sintáctico. Todo este proceso
+la biblioteca Menhir mencionada anteriormente para generar los analizadores.
+Estos módulos contienen las definiciones de tokens y las reglas de las
+gramáticas regular y libre de contexto usadas para indicar, respectivamente, el
+comportamiento de los analizadores léxico y sintáctico. Todo este proceso
 aparece ilustrado en la figura \ref{fig:ecparser}.
 
 \tikzstyle{line} = [draw]
@@ -853,6 +851,7 @@ Form>>. La sintaxis concreta que usa Menhir es la siguiente:
   | [<tokens o reglas>] { <valor_semántico> }
   | [<tokens o reglas>] { <valor_semántico> }
   | ...
+  ;
 \end{lstlisting}
 
 Cada regla define un símbolo no terminal ($<$nombre_regla$>$) que la identifica,
@@ -863,7 +862,90 @@ referencia a tokens o a otras reglas, y termina con una expresión entre llaves
 <<\{ , \}>> conteniendo las \textbf{acciones semánticas} de la regla (los
 efectos secundarios que se llevan a cabo durante su expansión).
 
-TODO: modificaciones en EcParser y EcParseTree
+Como el objetivo de esta fase es generar un árbol sintáctico abstracto, cada
+regla será la responsable de generar un nodo con su representación abstracto
+como acción semántica. Por eso, antes de escribir nuestras reglas modificaremos
+el fichero que define el árbol sintáctico.
+
+Para empezar, añadiremos un nodo que represente el operador especial de
+coste. De ahora en adelante lo llamaremos \textbf{expresión} de coste, ya que al
+fin y al cabo es una expresión (se evalúa a un número entero) y no provoca
+ambigüedad con el resto de operadores normales. La definición es la siguiente:
+
+\begin{code}
+  \begin{minted}{ocaml}
+type pcexpr = (pqsymbol * pexpr list) located
+  \end{minted}
+  \caption{Nodo: expresión de coste (ecParseTree.ml)}
+\end{code}
+
+Es decir, que ``pcexpr'' (<<parsed cost expression>>) es un tipo de datos cuyos
+valores son tuplas <<(símbolo, [expresiones])>> que almacenan respectivamente el
+operador cuyo coste se está evaluando y sus argumentos, y además contienen
+información de su ubicación en el código fuente: fila y columna
+(<<located>>).
+
+A continuación definiremos el nodo correspondiente al axioma de coste:
+
+\begin{code}
+  \begin{minted}{ocaml}
+type pcaxiom = {
+  pca_name  : psymbol;
+  pca_cargs : ptybindings option;
+  pca_spec  : pformula;
+}
+  \end{minted}
+  \caption{Nodo: axioma de coste (ecParseTree.ml)}
+\end{code}
+
+El axioma de coste es un ``record'' (estructura de datos con varios campos) que
+almacena su nombre, argumentos (opcionales) y especificación. La especificación
+es una fórmula: expresiones que pueden estar cuantificadas existencialmente o
+universalmente. Por tanto, también necesitaremos modificar el tipo de datos
+fórmula para que pueda contener expresiones de coste:
+
+\begin{code}
+  \begin{minted}{ocaml}
+type pformula  = pformula_r located
+
+and pformula_r =
+  | PFhole
+  | PFint    of int
+  | PFtuple  of pformula list
+
+  (* ... *)
+
+  | PFcost   of pcexpr
+  \end{minted}
+  \caption{Nodo: fórmulas (ecParseTree.ml)}
+\end{code}
+
+Una vez tenemos los nodos definidos, volvemos al analizador sintáctico para
+definir las reglas:
+
+\begin{lstlisting}[frame=lrtb]
+cexpr:
+  | COST '[' op=qident ']'
+      { (* ... *)
+        (op, []) }
+  | COST '[' op=qident ',' ps=plist0(expr, ',') ']'
+      { (* ... *)
+        (op, ps) }
+  ;
+
+caxiom:
+  | CAXIOM x=ident args=ptybindings? ':' spec=form
+      { { pca_name=x; pca_cargs=args; pca_spec=spec } }
+  ;
+\end{lstlisting}
+
+Se puede observar cómo cada regla, además de definir la sintaxis, crea su nodo
+correspondiente y lo devuelve como valor semántico. Esto es todo lo que
+necesitamos para que EasyCrypt reconozca sintácticamente las nuevas
+construcciones.
+
+A continuación pasaremos a la última etapa de la implementación del coste, y la
+más compleja: modificar el analizador semántico.
 
 \section{Modificaciones al analizador semántico}
 \label{sec:modif-al-anal-sem}
@@ -1268,7 +1350,7 @@ A continuación veremos los pasos que se han realizado para abordar la
 implementación del cliente, partiendo del diseño de la figura
 \ref{fig:prototype}.
 
-\subsection{Colocación de elementos}
+\subsection{Colocación de elementos} %TODO quitar (índice)
 \label{sec:coloc-de-elem}
 
 A la hora de distribuir los elementos de la página principal se ha usado una
@@ -1428,6 +1510,8 @@ A lo largo de este documento hemos abordado la mejora de dos aspectos
 relativamente independientes de EasyCrypt: una principalmente técnica (coste) y
 otra de usabilidad (interfaz web).
 
+% TODO qué he aprendido
+
 EasyCrypt es un marco orientado a un usuario muy concreto: profesionales de la
 criptografía. Si bien es cierto que en el propio Instituto IMDEA Software se usa
 y desarrolla activamente, el objetivo último sería crear comunidad. La