Lambda-LaTeX/cc.sty at master · lambda-land/Lambda-LaTeX · GitHub

1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
%
% Choice calculus definitions.
%
\ProvidesPackage{cc}

\RequirePackage{lambda}
\RequirePackage{stmaryrd}

%
% choice calculus syntax
%

% keywords & formatting/indenting
\newcommand{\CCkeyw}[1]{\textbf{\textup{\textrm{#1}}}}
\newcommand{\LET}{\CCkeyw{share}}
\newcommand{\BE}{\OB{\shorteq}}
\newcommand{\DIM}{\CCkeyw{dim}}
\newcommand{\IN}{\CCkeyw{in}}

% structural nodes (tr=tree)
\newcommand{\subL}{\OB{\mathord\Yleft}}
\newcommand{\subR}{\OB{\mathord\Yright}}
\newcommand{\sub}[1]{\OB{\subL#1\subR}}
\newcommand{\tr}[2][a]{\OB{#1\sub{#2}}}
\newcommand{\trn}[2][a]{\OB{#1\sub{\vn{#2}}}}

% choices
\newcommand{\dimMeta}{D}
\newcommand{\chcL}{\OB{\langle}}
\newcommand{\chcR}{\OB{\rangle}}
\newcommand{\chc}[2][\dimMeta]{\OB{\mathit{#1}\chcL#2\chcR}}
\newcommand{\chcPP}[3][\dimMeta]{\chc[#1]{\prog{#2},\prog{#3}}}
\newcommand{\chcPPP}[4][\dimMeta]{\chc[#1]{\prog{#2},\prog{#3},\prog{#4}}}

% dimensions
\newcommand{\Dim}[2][\dimMeta]{\OB{\DIM\;\chc[#1]{#2}}}
\newcommand{\DimIn}[3][\dimMeta]{\OB{\Dim[#1]{#2}\;\IN\;#3}}
\newcommand{\FD}[1]{\OB{\mathit{FD}(#1)}}

% static sharing
\newcommand{\Let}[2]{\OB{\LET\;#1\BE\;#2}}
\newcommand{\LetIn}[3]{\OB{\Let{#1}{#2}\;\IN\;#3}}
\newcommand{\FV}[1]{\OB{\mathit{FV}(#1)}}
\newcommand{\BD}[1]{\OB{\mathit{BD}(#1)}}
\newcommand{\dimFree}[1]{\OB{\BD{#1}=\varnothing}}

% smart constructors
\newcommand{\Atags}{\OB{a_1,a_2}}
\newcommand{\Btags}{\OB{b_1,b_2}}
\newcommand{\Ctags}{\OB{c_1,c_2}}
\newcommand{\Dtags}{\OB{d_1,d_2}}
\newcommand{\dimA}[2][\Atags]{\DimIn[A]{#1}{#2}}
\newcommand{\dimB}[2][\Btags]{\DimIn[B]{#1}{#2}}
\newcommand{\dimC}[2][\Ctags]{\DimIn[C]{#1}{#2}}
\newcommand{\dimD}[2][\Dtags]{\DimIn[D]{#1}{#2}}
\newcommand{\chcA}[1]{\chc[A]{#1}}
\newcommand{\chcB}[1]{\chc[B]{#1}}
\newcommand{\chcC}[1]{\chc[C]{#1}}
\newcommand{\chcD}[1]{\chc[D]{#1}}
\newcommand{\dcA}[2][\Atags]{\dimA[#1]{\chcA{#2}}}
\newcommand{\dcB}[2][\Btags]{\dimB[#1]{\chcB{#2}}}
\newcommand{\dcC}[2][\Ctags]{\dimC[#1]{\chcC{#2}}}
\newcommand{\dcD}[2][\Dtags]{\dimD[#1]{\chcD{#2}}}


%
% choice calculus semantics
%

% tag selection
\newcommand{\selMeta}{\OB{\dimMeta.i}}
\newcommand{\tsel}[2][\selMeta]{\OB{\lfloor#2\rfloor_{#1}}}
\newcommand{\dec}[1]{\OB{[#1]}}

% computing variants
\newcommand{\variSym}{\OB{V}}
\newcommand{\vari}[1]{\OB{\variSym(#1)}}

% sharing expansion
\newcommand{\expSym}{\OB{\mu}}
\newcommand{\expEnv}{\OB{\rho}}
\newcommand{\expand}[2][\expEnv]{\expSym_{#1}(#2)}

% indicating plain expressions
\newcommand{\plain}[1]{\OB{\underline{#1}}}


%
% design theory
%

% inference rules
\newcommand{\rn}[1]{\TirName{#1}}

% equivalencies
\newcommand{\vequivSym}{\OB{\sim}}
\newcommand{\vequiv}[2]{\OB{#1\vequivSym#2}}
\newcommand{\equalt}[3][C]{\OB{#2\vequivSym_{#1}#3}}
\newcommand{\equtag}[3][C]{\OB{#2\vequivSym_{#1}#3}}
\newcommand{\nequivSym}{\OB{\not\sim}}
% \newcommand{\nequiv}[2]{\OB{#1\nequivSym#2}} conflicts with txfonts (mathptmx)
\newcommand{\nequalt}[3][C]{\OB{#2\nequivSym_{#1}#3}}
\newcommand{\nequtag}[3][C]{\OB{#2\nequivSym_{#1}#3}}

% transformations
\newcommand{\drop}[3][C]{\OB{{#2}_{#1}(#3)}}
\newcommand{\dropi}[4][C]{\OB{{#2}_{#1/#3}(#4)}}
\newcommand{\dropA}[3][C]{\dropi[#1]{\alpha}{#2}{#3}}
\newcommand{\dropT}[3][C]{\dropi[#1]{\tau}{#2}{#3}}
\newcommand{\dropC}[2][C]{\drop[#1]{\gamma}{#2}}
\newcommand{\dropD}[2][C]{\drop[#1]{\psi}{#2}}


%
% miscellaneous
%

% CPP annotations
\newcommand{\cpp}[1]{\prog{\##1}}
%\newcommand{\ifdef}{\cpp{ifdef}}

% CC Examples
\newcommand{\CCname}[1]{\textit{\textrm{#1}}}