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