diff options
Diffstat (limited to 'papers/cfrontend_new/macros.tex')
| -rw-r--r-- | papers/cfrontend_new/macros.tex | 146 |
1 files changed, 0 insertions, 146 deletions
diff --git a/papers/cfrontend_new/macros.tex b/papers/cfrontend_new/macros.tex deleted file mode 100644 index 26ff6cbf..00000000 --- a/papers/cfrontend_new/macros.tex +++ /dev/null @@ -1,146 +0,0 @@ - -%\newcommand{\xxx}[1]{{\color{BrickRed}{#1}}} -%\newcommand{\xxx}[1]{\marginpar{\footnotesize\color{red}{#1}}} -\newcommand{\xxx}{} -\newcommand{\comment}{} -\newcommand{\cminor}{Cminor} -\newcommand{\compcert}{CompCert} - -\newcommand{\defeq}{=_{\mathrm{def}}} -% Abbreviations - -% \newtheorem{thm}{Theorem}[section] -% \newtheorem{lemma}[thm]{Lemma} -% \newtheorem{corollary}[theorem]{Corollary} - -% \newtheorem{dfn}[theorem]{Definition} -% \newtheorem{definition}[theorem]{Definition} - -% Operators, relations, etc. - -\def\seq#1{#1^*} -\def\opt#1{#1^?} -\def\some#1{\lfloor #1 \rfloor} -\def\Clight{{Clight{}}} -\def\tr{{\it tr}} -\def\vg{{\it lv}} -\def\ls{\it ls} -\def\ofs{{\it ofs}} -\def\op{{\it op}} -\def\chunk{\kappa} %{\it chunk}} -\def\sig{{\sigma}} -\def\fn{{\it def{\char95}fn}} -\def\cfn{{\it fn}} -\def\prog{{\it prog}} -\def\evv{{\it ev}} -\def\ev{{\it e}} -\def\tr{{\it tr}} -\def\E0{{\it \emptyset_\tr}} -\def\fl{{\it fl}} -\def\cenv{\gamma} -\def\tcast#1#2{{\cal C}_{#1}^{#2}} -\def\tcasta{{\cal C}_1} -\def\tcastb{{\cal C}_2} -\def\tlval{{\cal L}} -\def\trval{{\cal R}} -\def\tstmt{{\cal S}} -\def\tfunction{{\cal F}} -\def\valinj#1{\stackrel{#1}{\approx}} -\def\meminj#1{\stackrel{#1}{\approx}} -\def\outinj#1#2{\stackrel{#1,#2}{\approx}} -\def\loc{{\it loc}} -\def\envmatch{{\it EnvMatch}} -\def\csmatch{{\it CallInv}} -\def\sp{{\it sp}} -\def\cs{{\it cs}} -\def\evallvalue{\stackrel{l}{\Rightarrow}} -\def\evalexpr{\Rightarrow} -\def\evalstmt{\Rightarrow} -\def\evalfunc{\stackrel{f}{\Rightarrow}} -\def\evalprog{\Rightarrow} -%\def\evalexpr2{\rightarrow} -%\def\evalstmt2{\rightarrow} -%\def\evalfunc2{\rightarrow} -%\def\evalprog2{\rightarrow} -\def\inj{\alpha} -\def\accessmode{{\cal A}} - -\newcommand{\sbcm}[1]{\textcolor{red}{\textit{#1}}} -\newcommand{\guardbox}{\raisebox{1pt}{\makebox[0pt][l]{\(\sqcap\)}}{\raisebox{-1pt}{\(\sqcup\)}}} -\newcommand{\danscarre}[2]{ \makebox[0pt][l]{\scriptsize \hspace{1pt}#1}{\guardbox{}^{#2}} } -\newcommand{\unannot}[2]{{\underline{#1}}^{#2}} -%\newcommand{\unannot}[2]{\mbox{\fbox{#1}\textsuperscript{#2}}} -%\newcommand{\unannot}[2]{\danscarre{#1}{#2}} - - -\newcommand{\tyface}[1]{\ensuremath{\mathsf{#1}}} - -\newcommand{\option}{\tyface{option}} -\newcommand{\val}{\tyface{val}} -\newcommand{\Vundef}{\tyface{Vundef}} -\newcommand{\Vint}{\tyface{Vint}} -\newcommand{\Vfloat}{\tyface{Vfloat}} -\newcommand{\Vptr}{\tyface{Vptr}} -\newcommand{\expr}{\tyface{expr}} -\newcommand{\env}{\tyface{env}} -\newcommand{\mem}{\tyface{mem}} -\newcommand{\exprlist}{\tyface{exprlist}} -\newcommand{\Some}{\tyface{Some}} -\newcommand{\None}{\tyface{None}} -\newcommand{\Eval}{\tyface{Eval}} -\newcommand{\Evar}{\tyface{Evar}} -\newcommand{\Eop}{\tyface{Eop}} -\newcommand{\Eload}{\tyface{Eload}} -\newcommand{\Econdition}{\tyface{Econdition}} -\newcommand{\Elet}{\tyface{Elet}} -\newcommand{\Eletvar}{\tyface{Eletvar}} -\newcommand{\Enil}{\tyface{Enil}} -\newcommand{\Econs}{\tyface{Econs}} -\newcommand{\Sassign}[2]{#1:=#2} -\newcommand{\Sstore}[3]{\tyface{[}#2\tyface{]}_{#1}\tyface{:=}#3} -\newcommand{\Scall}[4]{\tyface{call}\,#1\,#3\,#4} -\newcommand{\Sif}[3]{\tyface{if}\,#1\,\tyface{then}\,#2\,\tyface{else}\,#3} -\newcommand{\Sloop}[1]{\tyface{loop}\,#1} -\newcommand{\Sblock}[1]{\tyface{block}\,#1} -\newcommand{\Sexit}[1]{\tyface{exit}\,#1} -\newcommand{\Sreturn}[1]{\tyface{return}\,#1} -\newcommand{\Sseq}[2]{#1;#2} -\newcommand{\Sskip}{\tyface{skip}} - -\newcommand{\spt}{\ensuremath{\mathit{sp}}} -\newcommand{\stmt}{\tyface{stmt}} -\newcommand{\id}{\ensuremath{\mathit{id}}} -\newcommand{\out}{\ensuremath{\mathit{out}}} -\newcommand{\outcome}{\tyface{outcome}} -\newcommand{\outn}{\tyface{Out_{normal}}} -\newcommand{\oute}[1]{\tyface{Out_{exit}\,#1}} -\newcommand{\outr}[1]{\tyface{Out_{return}\,#1}} - -\newcommand{\updrho}[2]{\tyface{update_{rho}}(#1,#2)} -\newcommand{\updmem}[2]{\tyface{update_{mem}}(#1,#2)} -\newcommand{\updsp}[2]{\tyface{update_{sp}}(#1,#2)} -\newcommand{\updphi}[2]{\tyface{update_{phi}}(#1,#2)} -\newcommand{\strho}[1]{\tyface{get_{rho}}(#1)} -\newcommand{\stmem}[1]{\tyface{get_{mem}}(#1)} -\newcommand{\stsp}[1]{\tyface{get_{sp}}(#1)} - -%\newcommand{\evalexpr}[8]{#1;(#2;#3;#4;#5;#6) \vdash #7 \Downarrow #8} -%\newcommand{\evalexp}[3]{\fmap; #1 \vdash #2 \Downarrow #3} -\newcommand{\evaloperation}[5]{#1;#2 \vdash #3(#4) \Downarrow_\tyface{eval\_operation} #5} -\newcommand{\execstmts}[8]{#1;(#2;#3;#4) \Downarrow_#5 (#6;#7;#8)} -\newcommand{\execstmt}[4]{(#2,#1) \Downarrow_#3 #4} -\newcommand{\execstmtk}[5]{(#2,\Kseq{#1}{#3}) \Downarrow_{#4} #5} -\newcommand{\execpgm}[2]{\vdash #1 \Downarrow #2} - -\newcommand{\loadv}[4]{#1\vdash #2\stackrel{#3}{\mapsto}#4} -\newcommand{\storev}[5]{#5=#2[#3\stackrel{#1}{:=}#4]} -\newcommand{\agree}{\approx} -\newcommand{\safe}[1]{\tyface{safe}\,#1} -\newcommand{\cat}[2]{#1 \circ #2} - -\newcommand{\ceq}[3]{#2\stackrel{#1}{\mbox{\texttt{==}}}#3} -\newcommand{\ieq}[2]{\ceq{\mathrm{int}}{#1}{#2}} - -\newcommand{\nomem}[1]{\lfloor{#1}\rfloor} -\newcommand{\withmem}[2]{\lceil{#1}\rceil^{#2}} - |