diff options
Diffstat (limited to 'papers/cfrontend_new/macros.tex')
| -rw-r--r-- | papers/cfrontend_new/macros.tex | 146 |
1 files changed, 146 insertions, 0 deletions
diff --git a/papers/cfrontend_new/macros.tex b/papers/cfrontend_new/macros.tex new file mode 100644 index 0000000..26ff6cb --- /dev/null +++ b/papers/cfrontend_new/macros.tex @@ -0,0 +1,146 @@ + +%\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}} + |