@@ -2,157 +2,188 @@
22%%
33%% A set of LaTeX macros and styling for working with Idris in LaTeX
44%%
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.
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.
918%%
1019%% ----------------------------------------------------------- [ Begin Package ]
1120\ProvidesPackage{idrislang}
1221
22+\RequirePackage{ifthen}
1323\RequirePackage{listings}
14−\RequirePackage{mathtools}
1524\RequirePackage{xspace}
25+%% ----------------------------------------------------------------- [ Options ]
26+\newboolean{literate}
27+\setboolean{literate}{false}
28+\newboolean{numbers}
29+\setboolean{numbers}{false}
30+
31+\DeclareOption{literate}{%
32+ \setboolean{literate}{true}
33+}
34+
35+\DeclareOption{numbers}{%
36+ \setboolean{numbers}{true}
37+}
38+
39+\ProcessOptions\relax
1640
41+%% ---------------------------------------------------------------- [ Commands ]
1742\newcommand{\Idris}{\textsc{Idris}\xspace}
43+\newcommand{\idris}{\textsc{Idris}\xspace}
1844
1945%% --------------------------------------------------- [ Define Idris Listings ]
2046\lstdefinelanguage{idris}{%
2147 sensitive,%
2248%% ----------------------------------------------------------- [ Default Style ]
23− % Default Style
24− basicstyle=\small\ttfamily,
49+ basicstyle=\ttfamily,
2550 flexiblecolumns=false,
26− basewidth={0.5em,0.45em},
2751 commentstyle=\footnotesize\sffamily,
2852%% ---------------------------------------------------------------- [ Keywords ]
29−%% From Idris Parser
53+%% From Idris Parser and idris-mode and vimscript
3054 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− },
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+},
3761%% ------------------------------------------------------- [ Prelude Functions ]
3862%% Generated using
3963%% find lib/ -name "*.idr" | xargs grep -e "^[a-zA-Z0-9]* :" | awk -F : '{printf $2", "}'
4064 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},
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+ },
108135%% ---------------------------------------------------------------- [ Comments ]
109136 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,
137+ morecomment=[n]{\{-}{-\}}
130138}[keywords,comments,strings]%
131139
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,
161+}
132162%% -------------------------------------------------- [ 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− }
163+
164+\lstdefinestyle{default}{%
165+ xleftmargin=\parindent,
166+ tabsize=2
167+}
168+\lstdefinestyle{numbers}{%
169+ xleftmargin=\parindent,
170+ tabsize=2,
171+ numbers=left,
172+ numbersep=10pt,
173+ numberstyle=\footnotesize\sffamily,
174+ frame=leftline
143175}
144176
145177%% ------------------------------------------------------ [ 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− }
178+%% Replicate the existence of literate haskell code environments,
179+%% option to make pretty with numbers.
180+\lstnewenvironment{code}[1][]
181+ {\ifthenelse{\boolean{literate}}{%
182+ \lstset{language=literateidris}}{%
183+ \lstset{language=idris}}
184+ \ifthenelse{\boolean{numbers}}{%
185+ \lstset{style=numbers, #1}}{%
186+ \lstset{style=default, #1}}
156187 }
157188 {}
158189\endinput