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