Acortado defs.tex y definida gramática bnf

1 files changed, 43 insertions, 161 deletions

diff --git a/defs.tex b/defs.tex
index 98e974f..b8b42df 100755
--- a/defs.tex
+++ b/defs.tex
@@ -1,67 +1,19 @@
 % Source: EasyCrypt manual (https://www.easycrypt.info)
 
 % !TeX root = easycrypt.tex
+
 %% Names
 % Tools
- \newcommand{\EasyCrypt}{\textsf{EasyCrypt}\xspace}
- \newcommand{\CertiCrypt}{\textsf{CertiCrypt}\xspace}
- \newcommand{\CertiPriv}{\textsf{CertiPriv}\xspace}
- \newcommand{\SsReflect}{\textsf{SsReflect}\xspace}
- \newcommand{\Coq}{\textsf{Coq}\xspace}
- \newcommand{\WhyThree}{\textsf{Why3}\xspace}
+\newcommand{\EasyCrypt}{\textsf{EasyCrypt}\xspace}
+\newcommand{\CertiCrypt}{\textsf{CertiCrypt}\xspace}
+\newcommand{\CertiPriv}{\textsf{CertiPriv}\xspace}
+\newcommand{\SsReflect}{\textsf{SsReflect}\xspace}
+\newcommand{\Coq}{\textsf{Coq}\xspace}
+\newcommand{\WhyThree}{\textsf{Why3}\xspace}
 
 % Languages and Logics
- \newcommand{\pWHILE}{\textsf{p}\textsc{While}\xspace}
- \newcommand{\pRHL}{\textsf{pRHL}\xspace}
-
-% Version numbers
- \newcommand{\ECversion}{0.$\beta$\xspace}
-
-%% Misc
-\newcommand{\DONE}{}% {{\color{red}DONE}}
-\newcommand{\Example}{\paragraph*{Example}}
-\newcommand{\Syntax}{\paragraph*{Syntax}}
-\newcommand{\Description}{\paragraph*{Description}}
-\setcounter{secnumdepth}{3}
-\renewcommand{\thesubsubsection}{\arabic{chapter}.\arabic{section}.\arabic{subsection}.\arabic{subsubsection}}
-\newbox\minicodebox
-\newenvironment{minicode}[1]{%
-\minipage[t]{#1\linewidth} %
-\centering %
-\verbatim %
-}{%
-\endverbatim %
-\endminipage% 
-}
-
-
-\newcounter{alarmcounter}
-\setcounter{alarmcounter}{1}
-\newcommand{\alarm}[1]
-            {\begingroup
-              \def\thefootnote{{\normalsize\color{red}(\arabic{footnote})}}
-              \footnote{\textsf{\textbf{{\color{red}\sc \bf ALARM:}
-                  #1}}}\endgroup}
-
-
-\newcommand{\infr}[2]{
-{\renewcommand{\arraystretch}{1.1}
-\begin{array}{c}
-{#1}\\
-\hline
-{#2}
-\end{array}}}
-
-%% Indexing
-\newcommand{\define}[2][]{\emph{#2}\index{easycrypt}{\ifx&#1&#2\else#1\fi}}
-
-%% Cross-referencing
-% \providecommand{\eqref}[1]{\textup{(\ref{#1})}}
-% \providecommand{\eqdef}{\raisebox{-.2ex}[.2ex]{$\stackrel{\textrm{\tiny def}}{~=~}$}}
-
-%% IDK
-\newcommand{\rname}[1]{[\textsc{#1}]}
-\newcommand{\result}{\mathsf{res}}
+\newcommand{\pWHILE}{\textsf{p}\textsc{While}\xspace}
+\newcommand{\pRHL}{\textsf{pRHL}\xspace}
 
 %% Security properties and schemes
 \newcommand{\INDCPA}{\textsf{IND-CPA}\xspace}
@@ -109,9 +61,7 @@
 \newcommand{\supp}{\mathsf{support}}
 \newcommand{\range}[2]{\mathsf{range}~{#1}~{#2}}
 
-%% Semantics 
-
-% \newcommand{\sem}[1]{\llbracket #1 \rrbracket}
+%% Semantics
 \newcommand{\subst}[2]{\left[{}^{#2}/{}_{#1}\right]}
 \newcommand{\fv}{\mathsf{fv}}
 \newcommand{\modifies}{\mathsf{mod}}
@@ -119,7 +69,7 @@
 \newcommand{\Env}{\mathcal{E}}
 
 %% Well-formed adversaries
-%% Program Judgements 
+%% Program Judgements
 \newcommand{\Hoare}[3]{\left[{#1}:{#2}\Longrightarrow{#3}\right]}
 \newcommand{\Equiv}[4]{\left[{#1}\sim{#2}:{#3}\Longrightarrow{#4}\right]}
 \newcommand{\bdHoareS}[5]{{\Hoare{#1}{#2}{#3}}\,{#4}\,{#5}}
@@ -127,41 +77,19 @@
 \newcommand{\HoareEq}[4]{\bdHoareS{#1}{#2}{#3}{=}{#4}}
 \newcommand{\HoareGe}[4]{\bdHoareS{#1}{#2}{#3}{\geq}{#4}}
 
-
-% \newcommand{\Equiv}[4]{\models {#1} \sim {#2} : {#3} \Longrightarrow {#4}}
-% \newcommand{\AEquiv}[6]{\models {#2} \sim_{#5,#6} {#3} : {#1} \Longrightarrow {#4}}
-% \newcommand{\JAEquiv}[6]{{#2} \sim_{#5,#6} {#3} : {#1} \Longrightarrow {#4}}
-% \newcommand{\EquivMem}[2]{\models {#1} \equiv {#2}}
-% \newcommand{\EqObs}[4]{\models {#1} \simeq^{#3}_{#4} {#2}}
-% \newcommand{\AEqObs}[5]{\models {#1} \simeq^{#3}_{{#4}} {#2} \preceq {#5}} 
-% \newcommand{\ACEqObs}[7]
-%         {\AEqObs{\left[ #1 \right]_{#6}}{\left[ #2 \right]_{#7}}{#3}{#4}{#5}}
-% \newcommand{\Triple}[3]{\sem{#2} {#3} \preceq {#1}}
-% \newcommand{\DTriple}[3]{\sem{#2} {#3} \succeq {#1}}
-% \newcommand{\dequiv}[3]{{#1} \simeq_{#3} {#2}}
-% \newcommand{\fequiv}[3]{{#1} =_{#3} {#2}}
-% \newcommand{\Pre}{\Psi}
-% \newcommand{\Post}{\Phi}
-% \newcommand{\Inv}{\Phi}
 \newcommand{\side}[1]{\langle #1 \rangle}
 \newcommand{\sidel}{\side{1}}
 \newcommand{\sider}{\side{2}}
-% \newcommand{\eqobsin}{\mathsf{eqobs\_in}}
-% \newcommand{\eqobsout}{\mathsf{eqobs\_out}}
 \newcommand{\pre}{\Psi}
 \newcommand{\post}{\Phi}
 \newcommand{\bound}{\delta}
 \newcommand{\ECinsupp}[2]{\mathec{Distr.in_supp}\,{#1}\,{#2}}
 \newcommand{\insupp}[2]{{#1}\in\mathec{supp}\,{#2}}
-%% Variables
 
-% \newcommand{\LH}{\gl{L}_H}
-% \newcommand{\LD}{\gl{L}_\Dec}
-% \newcommand{\cdef}{\gl{\gamma_\mathsf{def}}}
+%% Variables
 \newcommand{\var}[1]{\ensuremath{\mathit{#1}} \xspace}
 
 %% Constants and operators
-% TODO: Update!
 \newcommand{\true}{\mathsf{true}}
 \newcommand{\false}{\mathsf{false}}
 \newcommand{\nil}{\mathsf{nil}}
@@ -185,7 +113,6 @@
 \newcommand{\tbool}{\mathsf{bool}}
 
 %% Language
-% TODO: Update!
 \newcommand{\Skip}{\mathsf{skip}}
 \newcommand{\Seq}[2]{#1;\ #2}
 \newcommand{\Ass}[2]{#1 \leftarrow #2}
@@ -202,51 +129,20 @@
 \newcommand{\While}[2]{\mathsf{while}\ #1\ \mathsf{do}\ #2}
 \newcommand{\Call}[3]{#1 \leftarrow #2\mathsf{(}#3\mathsf{)}}
 \newcommand{\Return}{\mathsf{return}}
-% \newcommand{\Assert}[1]{\mathsf{assert}~#1}
-
-%% Tactics
-\newcommand{\tacname}{Error tacname}
-\newcommand{\vtacname}{Error tacname}
-\newcommand{\vararg}[1]{\ec{#1}}
-\newcommand{\cstarg}[1]{\ec{#1}}
-\newcommand{\typarg}[1]{\textit{#1}}
-\newcommand{\tacarg}[2]{(\vararg{#1}:\typarg{#2})}
-
-\newcommand{\addTacticIdx}[2]{\index{#1}{#2@\rawec{#2}}}
-
-\newcommand{\addTacticNoIdx}[2]{
-  \renewcommand{\tacname}{\rawec{#1}}
-  \renewcommand{\vtacname}{#1}
-  \subsubsection{#1}
-  \Syntax \ec{#1} #2
-  \Description}
-
-\newcommand{\addTacticPlain}[2]{
-  \renewcommand{\tacname}{\rawec{#1}}
-  \renewcommand{\vtacname}{#1}
-  \subsubsection{#1}
-  \Syntax {#2}
-  \Description}
-
-\newcommand{\addTactic}[3]{
-  \addTacticIdx{#1}{#2}
-  \addTacticNoIdx{#2}{#3}}
 
 %% Language definition
-\lstnewenvironment{easycrypt}[2][]%
-  {\lstset{language=easycrypt,caption={#2},#1}}%
-  {}
 
-\newcommand{\rawec}[2][basicstyle=\normalsize\sffamily,mathescape]{\lstinline[language=easycrypt,#1]{#2}}
-\newcommand{\mathec}[1]{\mbox{\rawec{#1}}}
-\newcommand{\ec}[2][basicstyle=\normalsize\sffamily]{\lstinline[language=easycrypt,style=easycrypt-pretty,#1]{#2}}
 
-\newcommand{\ecimport}[4][]{\lstinputlisting[language=easycrypt,linerange=#4,caption=#2,#1]{#3}}
+\newcounter{easycrypt}
+\lstnewenvironment{easycrypt}[2][]{
+  \renewcommand\lstlistingname{Listado de código}
+  \setcounter{lstlisting}{\value{easycrypt}}
+  \lstset{language=easycrypt,caption={#2},#1}
+}
+{\stepcounter{easycrypt}}
 
 \lstdefinelanguage{easycrypt}{
   style=easycrypt-default,
-%  procnamekeys={op,pred,fun},
-%  procnamestyle={\sffamily\itshape},
   keywordsprefix={'},
   morekeywords=[1]{unit,bool,int,real,bitstring,array,list,matrix,word},
   morekeywords=[2]{type,datatype,op,axiom,lemma,module,pred,const,declare},
@@ -259,7 +155,6 @@
                    progress,trivial},
   morekeywords=[8]{by,assumption,smt,reflexivity},
   morekeywords=[9]{first,last,do,try},
-%  moredirectives={prover,print}, % Incomplete
   morecomment=[n][\itshape]{(*}{*)},
   morecomment=[n][\bfseries]{(**}{*)}
 }
@@ -292,49 +187,36 @@
            {phin}{{$\!\phi_n$}}1
 }
 
-\lstdefinestyle{easycrypt-pretty}{
-    basicstyle=\small\sffamily,
-    literate={:=}{{$\mathrel{\gets}$}}1
-              {<=}{{$\mathrel{\leq}$}}1
-              {>=}{{$\mathrel{\geq}$}}1
-              {<>}{{$\mathrel{\neq}$}}1
-              {=\$}{{$\stackrel{\$}{\gets}$}}1
-              {forall}{{$\forall$}}1
-              {exists}{{$\exists$}}1
-              {->}{{$\rightarrow\;$}}1
-              {<-}{{$\leftarrow\;$}}1
-              {<->}{{$\leftrightarrow\;$}}1
-              {<=>}{{$\Leftrightarrow\;$}}1
-              {=>}{{$\Rightarrow\;$}}1
-              {==>}{{$\Rrightarrow\;$}}1
-              {\/\\}{{$\wedge$}}1
-              {\\\/}{{$\vee$}}1
-              {.\[}{{[}}1
-              {''ora}{{$\mathrel{||}$}}1 %needed for correct display in index
-              {'a}{{{\color{OliveGreen}$\alpha\,$}}}1
-              {'b}{{{\color{OliveGreen}$\beta\,$}}}1
-              {'c}{{{\color{OliveGreen}$\gamma\,$}}}1
-              {'t}{{{\color{OliveGreen}$\tau\,$}}}1
-              {'x}{{{\color{OliveGreen}$\chi\,$}}}1
-              {lambda}{{$\lambda\,$}}1
+\newcounter{bnf}
+\lstnewenvironment{bnf}[2][]{
+  \renewcommand\lstlistingname{Gramática}
+  \setcounter{lstlisting}{\value{bnf}}
+  \lstset{language=bnf,caption={#2},#1}
+}
+{\stepcounter{bnf}}
+
+\lstdefinestyle{bnf-style}{
+  frame=tb,
+  keywordstyle=[1]{\bfseries},
+  mathescape=true,
+  literate={<-}{{$ \leftarrow $}}1
+           % {<\$-}{{$\!\phi_1$}}1
+}
+
+\lstdefinelanguage{bnf}{
+  style=bnf-style,
+  morekeywords=[1]{while,do,if,then,else,skip}
 }
 
+\newcommand{\rawec}[2][basicstyle=\normalsize\sffamily,mathescape]{\lstinline
+[language=easycrypt,#1]{#2}}
+
 %% Typesetting
 \newcommand{\titledbox}[4]{{\color{#1}\fbox{\begin{minipage}{#2}{\textbf{#3:} \color{black}#4}\end{minipage}}}}
 \newcommand{\warningbox}[1]{\titledbox{red}{.9\textwidth}{Warning}{#1}}
 \newcommand{\futurebox}[1]{\titledbox{blue}{.9\textwidth}{Future}{#1}}
 
-
-
-\newcommand{\NotDocumented}{
-  \begin{center}{\color{blue}\fbox{\begin{minipage}{120pt}{\centering
-            \textbf{Not yet documented}}
-        \end{minipage}}}\end{center}}
-\newcommand{\NotImplemented}{
-  \begin{center}{\color{blue}\fbox{\begin{minipage}{120pt}{\centering
-            \textbf{Not yet implemented}}
-        \end{minipage}}}\end{center}}
-%%% Local Variables: 
+%%% Local Variables:
 %%% mode: latex
 %%% TeX-master: "memoria"
-%%% End: 
\ No newline at end of file
+%%% End:
\ No newline at end of file