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