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