diff options
| -rwxr-xr-x | memoria.tex | 54 | ||||
| -rw-r--r-- | ocaml_colors.tex | 123 |
2 files changed, 173 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} diff --git a/ocaml_colors.tex b/ocaml_colors.tex new file mode 100644 index 0000000..0f9333c --- /dev/null +++ b/ocaml_colors.tex @@ -0,0 +1,123 @@ +\newcommand\Clinenum[1]{#1} +\definecolor{CconstructorColor}{rgb}{0.00,0.20,0.80} +\newcommand\Cconstructor[1]{\textcolor{CconstructorColor}{#1}} +\definecolor{CcommentColor}{rgb}{0.60,0.00,0.00} +\newcommand\Ccomment[1]{\textcolor{CcommentColor}{#1}} +\definecolor{CstringColor}{rgb}{0.67,0.27,0.27} +\newcommand\Cstring[1]{\textcolor{CstringColor}{#1}} +\newcommand\Cquotation[1]{#1} +\definecolor{CalphakeywordColor}{rgb}{0.50,0.50,0.50} +\newcommand\Calphakeyword[1]{\textcolor{CalphakeywordColor}{#1}} +\newcommand\Cnonalphakeyword[1]{#1} +\definecolor{CandColor}{rgb}{0.00,0.50,0.00} +\newcommand\Cand[1]{\textcolor{CandColor}{#1}} +\definecolor{CasColor}{rgb}{0.00,0.50,0.00} +\newcommand\Cas[1]{\textcolor{CasColor}{#1}} +\definecolor{CclassColor}{rgb}{0.00,0.50,0.00} +\newcommand\Cclass[1]{\textcolor{CclassColor}{#1}} +\definecolor{CconstraintColor}{rgb}{0.00,0.50,0.00} +\newcommand\Cconstraint[1]{\textcolor{CconstraintColor}{#1}} +\definecolor{CexceptionColor}{rgb}{0.00,0.50,0.00} +\newcommand\Cexception[1]{\textcolor{CexceptionColor}{#1}} +\definecolor{CexternalColor}{rgb}{0.00,0.50,0.00} +\newcommand\Cexternal[1]{\textcolor{CexternalColor}{#1}} +\definecolor{CfunColor}{rgb}{0.00,0.50,0.00} +\newcommand\Cfun[1]{\textcolor{CfunColor}{#1}} +\definecolor{CfunctionColor}{rgb}{0.00,0.50,0.00} +\newcommand\Cfunction[1]{\textcolor{CfunctionColor}{#1}} +\definecolor{CfunctorColor}{rgb}{0.00,0.50,0.00} +\newcommand\Cfunctor[1]{\textcolor{CfunctorColor}{#1}} +\definecolor{CinColor}{rgb}{0.00,0.50,0.00} +\newcommand\Cin[1]{\textcolor{CinColor}{#1}} +\definecolor{CinheritColor}{rgb}{0.00,0.50,0.00} +\newcommand\Cinherit[1]{\textcolor{CinheritColor}{#1}} +\definecolor{CinitializerColor}{rgb}{0.00,0.50,0.00} +\newcommand\Cinitializer[1]{\textcolor{CinitializerColor}{#1}} +\definecolor{CletColor}{rgb}{0.00,0.50,0.00} +\newcommand\Clet[1]{\textcolor{CletColor}{#1}} +\definecolor{CmethodColor}{rgb}{0.00,0.50,0.00} +\newcommand\Cmethod[1]{\textcolor{CmethodColor}{#1}} +\definecolor{CmoduleColor}{rgb}{0.00,0.50,0.00} +\newcommand\Cmodule[1]{\textcolor{CmoduleColor}{#1}} +\definecolor{CmutableColor}{rgb}{0.00,0.50,0.00} +\newcommand\Cmutable[1]{\textcolor{CmutableColor}{#1}} +\definecolor{CofColor}{rgb}{0.00,0.50,0.00} +\newcommand\Cof[1]{\textcolor{CofColor}{#1}} +\definecolor{CprivateColor}{rgb}{0.00,0.50,0.00} +\newcommand\Cprivate[1]{\textcolor{CprivateColor}{#1}} +\definecolor{CrecColor}{rgb}{0.00,0.50,0.00} +\newcommand\Crec[1]{\textcolor{CrecColor}{#1}} +\definecolor{CtypeColor}{rgb}{0.00,0.50,0.00} +\newcommand\Ctype[1]{\textcolor{CtypeColor}{#1}} +\definecolor{CvalColor}{rgb}{0.00,0.50,0.00} +\newcommand\Cval[1]{\textcolor{CvalColor}{#1}} +\definecolor{CvirtualColor}{rgb}{0.00,0.50,0.00} +\newcommand\Cvirtual[1]{\textcolor{CvirtualColor}{#1}} +\definecolor{CdoColor}{rgb}{0.47,0.67,0.67} +\newcommand\Cdo[1]{\textcolor{CdoColor}{#1}} +\definecolor{CdoneColor}{rgb}{0.47,0.67,0.67} +\newcommand\Cdone[1]{\textcolor{CdoneColor}{#1}} +\definecolor{CdowntoColor}{rgb}{0.47,0.67,0.67} +\newcommand\Cdownto[1]{\textcolor{CdowntoColor}{#1}} +\definecolor{CelseColor}{rgb}{0.47,0.67,0.67} +\newcommand\Celse[1]{\textcolor{CelseColor}{#1}} +\definecolor{CforColor}{rgb}{0.47,0.67,0.67} +\newcommand\Cfor[1]{\textcolor{CforColor}{#1}} +\definecolor{CifColor}{rgb}{0.47,0.67,0.67} +\newcommand\Cif[1]{\textcolor{CifColor}{#1}} +\definecolor{ClazyColor}{rgb}{0.47,0.67,0.67} +\newcommand\Clazy[1]{\textcolor{ClazyColor}{#1}} +\definecolor{CmatchColor}{rgb}{0.47,0.67,0.67} +\newcommand\Cmatch[1]{\textcolor{CmatchColor}{#1}} +\definecolor{CnewColor}{rgb}{0.47,0.67,0.67} +\newcommand\Cnew[1]{\textcolor{CnewColor}{#1}} +\definecolor{CorColor}{rgb}{0.47,0.67,0.67} +\newcommand\Cor[1]{\textcolor{CorColor}{#1}} +\definecolor{CthenColor}{rgb}{0.47,0.67,0.67} +\newcommand\Cthen[1]{\textcolor{CthenColor}{#1}} +\definecolor{CtoColor}{rgb}{0.47,0.67,0.67} +\newcommand\Cto[1]{\textcolor{CtoColor}{#1}} +\definecolor{CtryColor}{rgb}{0.47,0.67,0.67} +\newcommand\Ctry[1]{\textcolor{CtryColor}{#1}} +\definecolor{CwhenColor}{rgb}{0.47,0.67,0.67} +\newcommand\Cwhen[1]{\textcolor{CwhenColor}{#1}} +\definecolor{CwhileColor}{rgb}{0.47,0.67,0.67} +\newcommand\Cwhile[1]{\textcolor{CwhileColor}{#1}} +\definecolor{CwithColor}{rgb}{0.47,0.67,0.67} +\newcommand\Cwith[1]{\textcolor{CwithColor}{#1}} +\definecolor{CassertColor}{rgb}{0.80,0.60,0.00} +\newcommand\Cassert[1]{\textcolor{CassertColor}{#1}} +\definecolor{CincludeColor}{rgb}{0.80,0.60,0.00} +\newcommand\Cinclude[1]{\textcolor{CincludeColor}{#1}} +\definecolor{CopenColor}{rgb}{0.80,0.60,0.00} +\newcommand\Copen[1]{\textcolor{CopenColor}{#1}} +\definecolor{CbeginColor}{rgb}{0.60,0.00,0.60} +\newcommand\Cbegin[1]{\textcolor{CbeginColor}{#1}} +\definecolor{CendColor}{rgb}{0.60,0.00,0.60} +\newcommand\Cend[1]{\textcolor{CendColor}{#1}} +\definecolor{CobjectColor}{rgb}{0.60,0.00,0.60} +\newcommand\Cobject[1]{\textcolor{CobjectColor}{#1}} +\definecolor{CsigColor}{rgb}{0.60,0.00,0.60} +\newcommand\Csig[1]{\textcolor{CsigColor}{#1}} +\definecolor{CstructColor}{rgb}{0.60,0.00,0.60} +\newcommand\Cstruct[1]{\textcolor{CstructColor}{#1}} +\definecolor{CraiseColor}{rgb}{1.00,0.00,0.00} +\newcommand\Craise[1]{\textcolor{CraiseColor}{#1}} +\definecolor{CasrColor}{rgb}{0.50,0.50,0.50} +\newcommand\Casr[1]{\textcolor{CasrColor}{#1}} +\definecolor{ClandColor}{rgb}{0.50,0.50,0.50} +\newcommand\Cland[1]{\textcolor{ClandColor}{#1}} +\definecolor{ClorColor}{rgb}{0.50,0.50,0.50} +\newcommand\Clor[1]{\textcolor{ClorColor}{#1}} +\definecolor{ClslColor}{rgb}{0.50,0.50,0.50} +\newcommand\Clsl[1]{\textcolor{ClslColor}{#1}} +\definecolor{ClsrColor}{rgb}{0.50,0.50,0.50} +\newcommand\Clsr[1]{\textcolor{ClsrColor}{#1}} +\definecolor{ClxorColor}{rgb}{0.50,0.50,0.50} +\newcommand\Clxor[1]{\textcolor{ClxorColor}{#1}} +\definecolor{CmodColor}{rgb}{0.50,0.50,0.50} +\newcommand\Cmod[1]{\textcolor{CmodColor}{#1}} +\newcommand\Cfalse[1]{#1} +\newcommand\Ctrue[1]{#1} +\definecolor{CbarColor}{rgb}{0.47,0.67,0.67} +\newcommand\Cbar[1]{\textcolor{CbarColor}{#1}} |