git.iko.soy/Idris-dev
on d1663cc help sign in
Idris-dev/tutorial/idrislang.sty
188 lines 8.7 kB history raw
1%% --------------------------------------------------- [ Idris Styling Package ]
2%%
3%% A set of LaTeX macros and styling for working with Idris in LaTeX
4%%
5%% + Provides a listings bindings:
6%% + idris :: default ascii
7%% + literateidris :: convert ascii maths to math symbols.
8%% + Defines a `numbers' and `default' listings style.
9%% + Defines a `code' environment for typesetting idris.
10%% + \begin{code}[...] ... \end{code}
11%% + Defines commands typesetting the name Idris.
12%% + \Idris{}
13%% + \idris{}
14%%
15%% Options:
16%% - literate :: turn on literate idris for code environments.
17%% - numbers :: turn on numbers for code environments.
18%%
19%% ----------------------------------------------------------- [ Begin Package ]
20\ProvidesPackage{idrislang}
22\RequirePackage{ifthen}
23\RequirePackage{listings}
24\RequirePackage{xspace}
25%% ----------------------------------------------------------------- [ Options ]
26\newboolean{literate}
27\setboolean{literate}{false}
28\newboolean{numbers}
29\setboolean{numbers}{false}
31\DeclareOption{literate}{%
32 \setboolean{literate}{true}
35\DeclareOption{numbers}{%
36 \setboolean{numbers}{true}
39\ProcessOptions\relax
41%% ---------------------------------------------------------------- [ Commands ]
42\newcommand{\Idris}{\textsc{Idris}\xspace}
43\newcommand{\idris}{\textsc{Idris}\xspace}
45%% --------------------------------------------------- [ Define Idris Listings ]
46\lstdefinelanguage{idris}{%
47 sensitive,%
48%% ----------------------------------------------------------- [ Default Style ]
49 basicstyle=\ttfamily,
50 flexiblecolumns=false,
51 commentstyle=\footnotesize\sffamily,
52%% ---------------------------------------------------------------- [ Keywords ]
53%% From Idris Parser and idris-mode and vimscript
54 keywords={%
55 abstract, attack, case, compute, do, dsl, else, exact, focus, if,
56 import, in, infix, infixl, infixr, instance, intros, module,
57 mutual, namespace, of, let, parameters, partial, pattern, prefix,
58 private, public, refine, rewrite, solve, syntax, term, then,
59 total, trivial, try, using, where, with
60},
61%% ------------------------------------------------------- [ Prelude Functions ]
62%% Generated using
63%% find lib/ -name "*.idr" | xargs grep -e "^[a-zA-Z0-9]* :" | awk -F : '{printf $2", "}'
64 morekeywords={%
65 class, data, instance, record, dsl, postulate, default, assert_total,
66 lambda, variable, index_first, index_next
67 % trace, unsafePerformPrimIO, FInt, FChar, FByte, FShort, FLong,
68 % FBits8, FBits16, FBits32, FBits64, FBits8x16, FBits16x8,
69 % FBits32x4, FBits64x2, interpFTy, ForeignTy, mkForeignPrim,
70 % mkLazyForeignPrim, liftPrimIO, fork, unsafePerformIO, listens,
71 % censor, Writer, liftReaderT, asks, Reader, modify, gets, State,
72 % RWS, nGTSm, decideNatLTE, lte, vectInjective1, vectInjective2,
73 % run, myID, send, msgWaiting, recv, recvWithSender, create,
74 % sendToThread, checkMsgs, getMsg, viewB8x16, viewB16x8, viewB32x4,
75 % viewB64x2, pow, exp, log, pi, sin, cos, tan, asin, acos, atan,
76 % atan2, sinh, cosh, tanh, sqrt, floor, ceiling, count, countFrom,
77 % curry, uncurry, uniformB8x16, uniformB16x8, uniformB32x4,
78 % uniformB64x2, putStr, putStrLn, print, getLine, putChar, getChar,
79 % fopen, openFile, closeFile, fread, fwrite, feof, ferror, nullPtr,
80 % nullStr, validFile, while, readFile, userSuppliedName, seq, try,
81 % mkPair, getUName, unApply, mkApp, binderTy, divCeil, nextPow2,
82 % nextBytes, machineTy, bitsUsed, natToBits, getPad, pad8, pad16,
83 % pad32, pad64, shiftLeft, shiftRightLogical, shiftRightArithmetic,
84 % and, or, xor, plus, minus, times, sdiv, udiv, srem, urem, lt, lte,
85 % eq, gte, gt, complement, zeroExtend, intToBits, bitsToInt, bitAt,
86 % getBit, setBit, unsetBit, bitsToStr, findElem, replaceElem,
87 % replaceByElem, mapElem, anyNilAbsurd, anyElim, any, negAnyAll,
88 % notAllHere, notAllThere, all, length, index, weaken, take, toList,
89 % fromList, replicate, foldl, foldr, map, pad, zeroBoundIsEmpty,
90 % empty, insert, delete, contains, fromList, toList, applyKleisli,
91 % applyMor, applyEndo, absZ, negZ, negNat, minusNatZ, plusZ, subZ,
92 % multZ, fromInt, natPlusZPlus, natMultZMult, doubleNegElim,
93 % posInjective, negSInjective, posNotNeg, plusZeroLeftNeutralZ,
94 % plusZeroRightNeutralZ, plusCommutativeZ, modBin, modComp, div,
95 % rem, intToMod, modToStr, branch4, branch5, branch6, branch7,
96 % merge1, merge2, merge3, treeLookup, treeInsert, delType,
97 % treeDelete, treeToList, empty, lookup, insert, delete, fromList,
98 % toList, getWitness, getProof, FalseElim, replace, sym, trans,
99 % lazy, par, malloc, Not, id, the, const, fst, snd, flip, cong,
100 % boolElim, not, intToBool, boolOp, div, mod, strHead, strTail,
101 % strCons, strIndex, reverse, null, getArgs, getEnv, setEnv,
102 % unsetEnv, getEnvironment, exit, usleep, sequence, toHexDigit,
103 % b8ToString, b16ToString, b32ToString, b64ToString, tail, head,
104 % last, init, index, deleteAt, replaceAt, take, drop, fromList,
105 % replicate, zipWith, zip, unzip, concat, elemBy, elem, lookupBy,
106 % lookup, hasAnyBy, hasAny, find, findIndex, elemIndexBy, elemIndex,
107 % nubBy, nub, isPrefixOfBy, isPrefixOf, isSuffixOfBy, isSuffixOf,
108 % catMaybes, diag, range, isLeft, isRight, choose, either, lefts,
109 % rights, partitionEithers, fromEither, maybeToEither, strM, unpack,
110 % pack, span, break, split, ltrim, trim, words, lines, foldr1,
111 % unwords, length, realPart, imagPart, mkPolar, cis, magnitude,
112 % phase, conjugate, isNothing, isJust, maybe, fromMaybe, toMaybe,
113 % justInjective, lowerMaybe, raiseToMaybe, isNil, isCons, head,
114 % tail, last, init, take, drop, takeWhile, dropWhile, list, length,
115 % repeat, replicate, zipWith, zipWith3, zip, zip3, unzip, unzip3,
116 % mapMaybe, toList, reverse, intersperse, intercalate, elemBy, elem,
117 % lookupBy, lookup, hasAnyBy, hasAny, find, findIndex, findIndices,
118 % elemIndexBy, elemIndex, elemIndicesBy, elemIndices, filter, nubBy,
119 % nub, span, break, split, partition, isPrefixOfBy, isPrefixOf,
120 % isSuffixOfBy, isSuffixOf, sorted, mergeBy, merge, sort,
121 % maybeToList, listToMaybe, catMaybes, appendNilRightNeutral,
122 % appendAssociative, lengthAppend, mapPreservesLength,
123 % mapDistributesOverAppend, mapFusion, hasAnyByNilFalse,
124 % hasAnyNilFalse, fromIntegerNat, toIntegerNat, hyper, log2, gcd,
125 % liftA, liftA2, liftA3, guard, when, finToNat, finToInt, weaken,
126 % strengthen, last, natToFin, integerToFin, fromInteger, flatten,
127 % return, isUpper, isLower, isAlpha, isDigit, isAlphaNum, isSpace,
128 % isNL, toUpper, toLower, isHexDigit, isValidHeap, merge, insert,
129 % findMinimum, deleteMinimum, toList, fromList, sort, main, foldl,
130 % concat, concatMap, and, or, any, all, sum, product, Vars,
131 % getAction, setInfo, getInfo, lift, output, queryVars, postVars,
132 % cookieVars, queryVar, getOutput, getHeaders, flushHeaders, flush,
133 % getVars, getContent, getCgiEnv, runCGI, mult
134 },
135%% ---------------------------------------------------------------- [ Comments ]
136 morecomment=[l]--,%
137 morecomment=[n]{\{-}{-\}}
138}[keywords,comments,strings]%
140%% ---------------------------------------- [ Define Idris with Literate Stuff ]
141\lstdefinelanguage{literateidris}[]{idris}{
142 literate= {+}{{$+$}}1
143 {/}{{$/$}}1
144 {*}{{$*$}}1
145 {=}{{$=$}}1
146 {>}{{$>$}}1
147 {<}{{$<$}}1
148 {\\}{{$\lambda$}}1
149 {\\\\}{{\char`\\\char`\\}}1
150 {->}{{$\rightarrow$}}2
151 {>=}{{$\geq$}}2
152 {<-}{{$\leftarrow$}}2
153 {<=}{{$\leq$}}2
154 {=>}{{$\Rightarrow$}}2
155 {==}{{$\equiv$}}2
156 {\ .}{{$\circ$}}2
157 {\ .\ }{{$\circ$}}2
158 {>>}{{>>}}2
159 {>>=}{{>>=}}2
160 {|}{{$\mid$}}1,
162%% -------------------------------------------------- [ Default Listings Style ]
164\lstdefinestyle{default}{%
165 xleftmargin=\parindent,
166 tabsize=2
168\lstdefinestyle{numbers}{%
169 numbers=left,
170 numbersep=10pt,
171 numberstyle=\footnotesize\sffamily,
172 frame=leftline
175%% ------------------------------------------------------ [ A Code Environment ]
176%% Replicate the existence of literate haskell code environments,
177%% option to make pretty with numbers.
178\lstnewenvironment{code}[1][]
179 {\ifthenelse{\boolean{literate}}{%
180 \lstset{language=literateidris}}{%
181 \lstset{language=idris}}
182 \ifthenelse{\boolean{numbers}}{%
183 \lstset{style=numbers, #1}}{%
184 \lstset{style=default, #1}}
185 }
186 {}
187\endinput
188%% --------------------------------------------------------------------- [ EOF ]