diff --git a/.github/workflows/docs-ci-cd.yml b/.github/workflows/docs-ci-cd.yml index 7737e8836..7f47c7368 100644 --- a/.github/workflows/docs-ci-cd.yml +++ b/.github/workflows/docs-ci-cd.yml @@ -7,7 +7,7 @@ jobs: build-docs-job: runs-on: ubuntu-latest steps: - - uses: actions/checkout@v3 + - uses: actions/checkout@v6 - uses: cachix/install-nix-action@v22 with: nix_path: nixpkgs=channel:nixos-unstable @@ -21,7 +21,7 @@ jobs: nix-shell --pure --run "make NO_STACK=y html" nix-shell --pure --run "make NO_STACK=y pdf" cp dist/pbook.pdf _site/book.pdf - - uses: actions/upload-artifact@v3 + - uses: actions/upload-artifact@v4 with: name: generated-site path: _site @@ -34,7 +34,7 @@ jobs: if: success() && github.ref == 'refs/heads/main' steps: - uses: actions/checkout@v3 - - uses: actions/download-artifact@v3 + - uses: actions/download-artifact@v4 with: name: generated-site path: _site diff --git a/.github/workflows/whitespace.yml b/.github/workflows/whitespace.yml new file mode 100644 index 000000000..670b664d5 --- /dev/null +++ b/.github/workflows/whitespace.yml @@ -0,0 +1,12 @@ +name: Whitespace + +on: + pull_request: + push: + +jobs: + whitespace: + runs-on: ubuntu-latest + steps: + - uses: actions/checkout@v6 + - uses: andreasabel/fix-whitespace-action@v1 diff --git a/.gitignore b/.gitignore index d0126ee09..76a783175 100644 --- a/.gitignore +++ b/.gitignore @@ -4,4 +4,4 @@ .stack-work liquidhaskell-tutorial.cabal _site -dist \ No newline at end of file +dist diff --git a/Main.hs b/Main.hs index 8cc5655ca..42d4a52bb 100644 --- a/Main.hs +++ b/Main.hs @@ -1,6 +1,6 @@ -module Main where +module Main where -import qualified Data.List as L +import qualified Data.List as L import System.Directory (listDirectory) import System.FilePath (addExtension) import System.FilePath (()) @@ -21,7 +21,7 @@ hideIgnore file = do writeFile tmpFile str hide :: String -> String -hide str +hide str | L.isPrefixOf "{-@ ignore " str = "-- " ++ str | L.isPrefixOf "{-@ fail " str = "-- " ++ str - | otherwise = str \ No newline at end of file + | otherwise = str diff --git a/README.md b/README.md index ff9207014..7ca841996 100644 --- a/README.md +++ b/README.md @@ -10,7 +10,7 @@ the github repository and run locally for best results. LH is available as a GHC plugin from version 0.8.10. -Thus, **the best way** to do this tutorial is to +Thus, **the best way** to do this tutorial is to **Step 1** Clone this repository, @@ -24,13 +24,13 @@ $ git clone https://github.com/ucsd-progsys/liquidhaskell-tutorial.git $ cabal v2-build ``` -or +or ``` $ stack build --fast --file-watch ``` -The above workflow will let you use whatever Haskell tooling you use for your +The above workflow will let you use whatever Haskell tooling you use for your favorite editor, to automatically display LH errors as well. ## Contents diff --git a/build.sh b/build.sh index 3be7a3a24..1ed37a7f4 100755 --- a/build.sh +++ b/build.sh @@ -2,14 +2,14 @@ mkHTML() { srcFile=$1 - + echo "HTML for $srcFile" PANDOC_TARGET=src/$srcFile.html PANDOC_CODETEMPLATE=../liquid-client/templates/code.template stack exec -- pandoc --from=markdown+lhs+raw_html --to=html5 -s --mathjax --standalone --mathjax --toc --section-divs --filter filters/Codeblock.hs --filter filters/Figures.hs --filter filters/Html.hs --variable=notitle --highlight-style=tango --template=dist/page.template templates/preamble.lhs src/$srcFile.lhs templates/bib.lhs -o src/$srcFile.html } -mkLHS() { +mkLHS() { echo "Build single LHS file" cat src/Tutorial_01_Introduction.lhs src/Tutorial_02_Logic.lhs src/Tutorial_03_Basic.lhs src/Tutorial_04_Polymorphism.lhs src/Tutorial_05_Datatypes.lhs src/Tutorial_06_Measure_Bool.lhs src/Tutorial_07_Measure_Int.lhs src/Tutorial_08_Measure_Set.lhs src/Tutorial_09_Case_Study_Lazy_Queues.lhs src/Tutorial_10_Case_Study_Associative_Maps.lhs src/Tutorial_11_Case_Study_Pointers.lhs src/Tutorial_12_Case_Study_AVL.lhs > dist/pbook.lhs } diff --git a/filters/Figures.hs b/filters/Figures.hs index cb08d7222..ed0034fa2 100644 --- a/filters/Figures.hs +++ b/filters/Figures.hs @@ -104,7 +104,7 @@ isFigure s = s `elem` ["figure", "marginfigure"] makeFigure tgt prefix t r id cls kvs = RawBlock (Format tgtTxt) . pad prefix t id cls kvs <$> getCount r id - where tgtTxt = T.pack $ show tgt + where tgtTxt = T.pack $ show tgt -- pad :: Text -> _ -> _ -> _ -> [(Text, Text)] pad prefix tplt id cls kvs n @@ -139,7 +139,7 @@ emptyInfo getCount r id = do info <- readIORef r - let idS = T.unpack id + let idS = T.unpack id let m = label info let c = chapter info let i = count info diff --git a/filters/Latex.hs b/filters/Latex.hs index 7d1e201d0..4b4870b05 100644 --- a/filters/Latex.hs +++ b/filters/Latex.hs @@ -31,7 +31,7 @@ toLaTeX :: Text -> Text -> [Block] -> Text toLaTeX cls id = wrapLatex cls id . either errHandler (\x -> x) . runPure . writeLaTeX def . Pandoc mempty where errHandler = error $ unpack $ mconcat ["toLaTex: ", cls, " ", id] -wrapLatex :: Text -> Text -> Text -> Text +wrapLatex :: Text -> Text -> Text -> Text wrapLatex "footnotetext" _ str = T.pack $ printf "\\footnotetext{%s}" (T.unpack str) wrapLatex "hwex" name str = T.pack $ printf "\\begin{hwex}[%s]\n%s\n\\end{hwex}" (T.unpack name) (T.unpack str) wrapLatex cls name str = error $ printf "WrapLatex: %s %s" cls name @@ -76,7 +76,7 @@ txBlock _ b = [b] expandCodeBlock :: Block -> [Block] expandCodeBlock (CodeBlock a s) = CodeBlock a `fmap` tWords s - where + where tWords = fmap pack . words . unpack ------------------------------------------------------------------------------------- ------------------------------------------------------------------------------------- diff --git a/fix-whitespace.yaml b/fix-whitespace.yaml new file mode 100644 index 000000000..3f0d2d7b6 --- /dev/null +++ b/fix-whitespace.yaml @@ -0,0 +1,81 @@ +# This file contains the project-specific settings for `fix-whitespace` a tiny +# but useful tool to +# +# * Removes trailing whitespace. +# * Removes trailing lines containing nothing but whitespace. +# * Ensures that the file ends in a newline character. +# +# By default, fix-whitespace checks every directory under the current working +# directory but no files. This program should be placed under a text-based +# project. +# +# For directories, +# +# 1) excluded-dirs is a black-list of directories, +# 2) included-dirs is a white-list of excluded-dirs +# +# For files, +# +# 3) included-files is a white-list of files, +# 4) excluded-files is a black-list of included-files. +# +# The extended glob pattern can be used to specify file/direcotory names. +# For details, see http://hackage.haskell.org/package/filemanip-0.3.6.3/docs/System-FilePath-GlobPattern.html +# +included-dirs: + # Without this line the above path will be excluded. + +excluded-dirs: + - "**/dist*" # matches every dist* in any directory + - .git + - .stack-work + - .vscode + - js + - css + +# Every matched filename is included unless it is matched by excluded-files. +included-files: + - "*.ac" + - "*.bat" + - "*.c" + - "*.cabal" + - "*.cfg" + - "*.cmm" + - "*.conf" + - "*.config" + - "*.cpp" + - "*.css" + - "*.dhall" + - "*.h" + - "*.hs" + - "*.hs-boot" + - "*.hsc" + - "*.hsig" + - "*.html" + - "*.in" + - "*.inc" + - "*.js" + - "*.json" + - "*.lhs" + - "*.md" + - "*.project" + - "*.py" + - "*.rst" + - "*.sh" + - "*.sty" + - "*.tex" + - "*.toml" + - "*.txt" + - "*.yaml" + - "*.yml" + - "cabal.project.*" + - .gitattributes + - .gitignore + - AUTHORS + - LICENSE + +excluded-files: +# Exceptions + +# Files that use tabs + - Makefile diff --git a/src/Tutorial_01_Introduction.lhs b/src/Tutorial_01_Introduction.lhs index 121c55c6b..fb841bfd2 100644 --- a/src/Tutorial_01_Introduction.lhs +++ b/src/Tutorial_01_Introduction.lhs @@ -55,7 +55,7 @@ with modern languages like Go, Python, JavaScript and Lua; and of course, they're widely used in Haskell too. ~~~~~{.ghci} -ghci> :m +Data.Map +ghci> :m +Data.Map ghci> let m = fromList [ ("haskell", "lazy") , ("ocaml" , "eager")] @@ -177,9 +177,9 @@ Getting Started As of July 2020, LiquidHaskell, version 0.8.10 onwards, is available as a [GHC plugin](https://downloads.haskell.org/~ghc/8.10.1/docs/html/users_guide/extending_ghc.html). -This means, roughly, that you need simply +This means, roughly, that you need simply -1. Add LH to your project dependencies, after which +1. Add LH to your project dependencies, after which 2. GHC produces LH type errors whenever you compile the code, so that you can 3. View errors using your favorite editor's existing Haskell tooling. @@ -256,4 +256,3 @@ via pull-requests on github. \noindent Lets begin! - diff --git a/src/Tutorial_03_Basic.lhs b/src/Tutorial_03_Basic.lhs index e33369ca5..0c7e1535c 100644 --- a/src/Tutorial_03_Basic.lhs +++ b/src/Tutorial_03_Basic.lhs @@ -76,7 +76,7 @@ nonsense :: Int nonsense = one' where {-@ one' :: Zero @-} - one' = 1 + one' = 1 \end{code} \noindent diff --git a/src/Tutorial_04_Polymorphism.lhs b/src/Tutorial_04_Polymorphism.lhs index 68279200a..323e7511c 100644 --- a/src/Tutorial_04_Polymorphism.lhs +++ b/src/Tutorial_04_Polymorphism.lhs @@ -302,7 +302,7 @@ absoluteSum = undefined \newthought{Inference} LiquidHaskell verifies `vectorSum` -- or, to be precise, -the safety of the vector accesses `vec ! i`. +the safety of the vector accesses `vec ! i`. The verification works out because LiquidHaskell is able to *automatically infer* ^[In your editor, click on `go` to see the inferred type.] @@ -315,8 +315,8 @@ between `0` and the length of `vec` (inclusive). LiquidHaskell uses this and the test that `i < sz` to establish that `i` is between `0` and `(vlen vec)` to prove safety. -**Note** you need to run `liquid` with the option `--no-termination` -or make sure your source file has `{-@ LIQUID "--no-termination" @-}, +**Note** you need to run `liquid` with the option `--no-termination` +or make sure your source file has `{-@ LIQUID "--no-termination" @-}, otherwise the code for `go` fails the now default termination check. We will come back to this example later to see how to verify termination using metrics. diff --git a/src/Tutorial_06_Measure_Bool.lhs b/src/Tutorial_06_Measure_Bool.lhs index b58c758cf..f19588038 100644 --- a/src/Tutorial_06_Measure_Bool.lhs +++ b/src/Tutorial_06_Measure_Bool.lhs @@ -389,5 +389,3 @@ In this chapter we saw how LiquidHaskell lets you \noindent Of course, we can do a lot more with measures, so let's press on! - - diff --git a/src/Tutorial_07_Measure_Int.lhs b/src/Tutorial_07_Measure_Int.lhs index d36fd94cd..0be4fc4b0 100644 --- a/src/Tutorial_07_Measure_Int.lhs +++ b/src/Tutorial_07_Measure_Int.lhs @@ -460,7 +460,7 @@ We can use the dimension aware lists to create a safe vector API. \begin{code} {-@ data Vector a = V { vDim :: Nat - , vElts :: ListN a vDim } + , vElts :: ListN a vDim } @-} \end{code} diff --git a/src/Tutorial_09_Case_Study_Lazy_Queues.lhs b/src/Tutorial_09_Case_Study_Lazy_Queues.lhs index 9ba8bc405..92fb711f8 100644 --- a/src/Tutorial_09_Case_Study_Lazy_Queues.lhs +++ b/src/Tutorial_09_Case_Study_Lazy_Queues.lhs @@ -14,8 +14,8 @@ invariant with LiquidHaskell. {-@ LIQUID "--no-termination" @-} {-@ LIQUID "--maxparams=3" @-} -module Tutorial_09_Case_Study_Lazy_Queues - (Queue, insert, remove, emp, realSize) +module Tutorial_09_Case_Study_Lazy_Queues + (Queue, insert, remove, emp, realSize) where import Prelude hiding (replicate, take, length) diff --git a/src/Tutorial_12_Case_Study_AVL.lhs b/src/Tutorial_12_Case_Study_AVL.lhs index ec08ed84e..09c5d0505 100644 --- a/src/Tutorial_12_Case_Study_AVL.lhs +++ b/src/Tutorial_12_Case_Study_AVL.lhs @@ -23,7 +23,7 @@ module Tutorial_12_Case_Study_AVL , elems, hasElem, addElem, delElem ) where - + import qualified Data.Set as S import Prelude hiding (max) -- import Language.Haskell.Liquid.Prelude (liquidAssume) diff --git a/src/todo/case-study-kmeans.lhs b/src/todo/case-study-kmeans.lhs index 860b0d882..37880fdb6 100644 --- a/src/todo/case-study-kmeans.lhs +++ b/src/todo/case-study-kmeans.lhs @@ -433,4 +433,3 @@ implementation) to verify that KMeans indeed produces at most `k` clusters... [demo]: http://goto.ucsd.edu/~rjhala/liquid/haskell/demo/#?demo=KMeansHelper.hs [URL-kmeans]: http://hackage.haskell.org/package/kmeans - diff --git a/stack.yaml b/stack.yaml index c2912fe9e..d38bd47e0 100644 --- a/stack.yaml +++ b/stack.yaml @@ -17,4 +17,3 @@ extra-deps: - git: https://github.com/ucsd-progsys/liquid-fixpoint commit: 1aab5d84e3dd96f3052dd27b92316cbb5254def1 - diff --git a/templates/bib.lhs b/templates/bib.lhs index 2c21a7fea..250e730d0 100644 --- a/templates/bib.lhs +++ b/templates/bib.lhs @@ -4,13 +4,13 @@ [vecspec]: https://github.com/ucsd-progsys/liquidhaskell/blob/91e1074575ca102df810ea399c5a13063e8c8011/include/Data/Vector.spec [vec]: http://hackage.haskell.org/package/vector [agdavec]: http://code.haskell.org/Agda/examples/Vec.agda -[ref101]: /blog/2013/01/01/refinement-types-101.lhs/ -[ref102]: /blog/2013/01/27/refinements-101-reax.lhs/ +[ref101]: /blog/2013/01/01/refinement-types-101.lhs/ +[ref102]: /blog/2013/01/27/refinements-101-reax.lhs/ [data-list]: https://hackage.haskell.org/package/base-4.18.0.0/docs/Data-List.html [foldl]: https://hackage.haskell.org/package/base-4.18.0.0/docs/Data-List.html#v:foldl [listtail]: /blog/2013/01/31/safely-catching-a-list-by-its-tail.lhs/ [dmlarray]: https://www.cs.cmu.edu/~fp/papers/pldi98dml.pdf -[liquid-tutorial]: http://github.com/ucsd-progsys/liquidhaskell-tutorial.git +[liquid-tutorial]: http://github.com/ucsd-progsys/liquidhaskell-tutorial.git [liquid-emacs]: https://github.com/ucsd-progsys/liquid-types.el [liquid-vim]: https://github.com/ucsd-progsys/liquid-types.vim [liquid-spacemacs]: https://github.com/ucsd-progsys/liquid-types-spacemacs diff --git a/templates/book.tex b/templates/book.tex index 80c964a4b..514d426f3 100644 --- a/templates/book.tex +++ b/templates/book.tex @@ -6,7 +6,7 @@ \usepackage{amssymb,amsmath} \usepackage{ifxetex,ifluatex} -\usepackage{fixltx2e} +\usepackage{fixltx2e} \ifnum 0\ifxetex 1\fi\ifluatex 1\fi=0 % if pdftex \usepackage[T1]{fontenc} @@ -104,14 +104,14 @@ \VerbatimFootnotes % allows verbatim text in footnotes -\title{LiquidHaskell} +\title{LiquidHaskell} \author{Ranjit Jhala} \date{\today} \newcommand\cc[1]{\texttt{#1}} -\newcommand\myfootnote[1]{\footnotetext{#1}} +\newcommand\myfootnote[1]{\footnotetext{#1}} %% EXERCISE: HANDROLLED @@ -131,22 +131,22 @@ \usepackage{xcolor} -% spec +% spec \DefineVerbatimEnvironment% {spec}{Verbatim} {} -% error +% error \DefineVerbatimEnvironment% {liquiderror}{Verbatim} {} -% shell +% shell \DefineVerbatimEnvironment% {shell}{Verbatim} {} -% orig +% orig \DefineVerbatimEnvironment% {redverbatim}{Verbatim} {formatcom=\color{red}} diff --git a/templates/haskellListings.tex b/templates/haskellListings.tex index e00e8a7fc..c027697ac 100644 --- a/templates/haskellListings.tex +++ b/templates/haskellListings.tex @@ -4,103 +4,103 @@ \def\withcolor{} \ifdefined\withcolor - \definecolor{haskellblue}{rgb}{0.0, 0.0, 1.0} - \definecolor{haskellstr}{rgb}{0.2, 0.2, 0.6} - \definecolor{haskellred}{rgb}{1.0, 0.0, 0.0} - \definecolor{gray_ulisses}{gray}{0.55} - \definecolor{castanho_ulisses}{rgb}{0.71,0.33,0.14} - \definecolor{preto_ulisses}{rgb}{0.41,0.20,0.04} - \definecolor{green_ulisses}{rgb}{0.0,0.4,0.0} + \definecolor{haskellblue}{rgb}{0.0, 0.0, 1.0} + \definecolor{haskellstr}{rgb}{0.2, 0.2, 0.6} + \definecolor{haskellred}{rgb}{1.0, 0.0, 0.0} + \definecolor{gray_ulisses}{gray}{0.55} + \definecolor{castanho_ulisses}{rgb}{0.71,0.33,0.14} + \definecolor{preto_ulisses}{rgb}{0.41,0.20,0.04} + \definecolor{green_ulisses}{rgb}{0.0,0.4,0.0} \else - \definecolor{haskellblue}{gray}{0.1} - \definecolor{haskellstr}{gray}{0.1} - \definecolor{haskellred}{gray}{0.1} - \definecolor{gray_ulisses}{gray}{0.1} - \definecolor{castanho_ulisses}{gray}{0.1} - \definecolor{preto_ulisses}{gray}{0.1} - \definecolor{green_ulisses}{gray}{0.1} + \definecolor{haskellblue}{gray}{0.1} + \definecolor{haskellstr}{gray}{0.1} + \definecolor{haskellred}{gray}{0.1} + \definecolor{gray_ulisses}{gray}{0.1} + \definecolor{castanho_ulisses}{gray}{0.1} + \definecolor{preto_ulisses}{gray}{0.1} + \definecolor{green_ulisses}{gray}{0.1} \fi \def\codesize{\normalsize} \lstdefinelanguage{HaskellUlisses}{ - basicstyle=\codesize\ttfamily, - sensitive=true, - morecomment=[l][\color{gray_ulisses}\ttfamily\codesize]{--}, - morecomment=[s][\color{gray_ulisses}\ttfamily\codesize]{\{-}{-\}}, - morestring=[b]", - stringstyle=\color{haskellstr}, - showstringspaces=false, - numberstyle=\codesize, - numberblanklines=true, - showspaces=false, - breaklines=true, - showtabs=false, + basicstyle=\codesize\ttfamily, + sensitive=true, + morecomment=[l][\color{gray_ulisses}\ttfamily\codesize]{--}, + morecomment=[s][\color{gray_ulisses}\ttfamily\codesize]{\{-}{-\}}, + morestring=[b]", + stringstyle=\color{haskellstr}, + showstringspaces=false, + numberstyle=\codesize, + numberblanklines=true, + showspaces=false, + breaklines=true, + showtabs=false, % mathescape=true, - emph= - {[1] - FilePath,IOError,abs,acos,acosh,and,any,appendFile,approxRational,asTypeOf,asin, - asinh,atan,atan2,atanh,basicIORun,break,catch,ceiling,chr,compare,concat,concatMap, - const,cos,cosh,curry,cycle,decodeFloat,denominator,digitToInt,div,divMod,drop, - dropWhile,either,elem,encodeFloat,enumFrom,enumFromThen,enumFromThenTo,enumFromTo, - error,even,exp,exponent,fail,filter,flip,floatDigits,floatRadix,floatRange,floor, - fmap,foldl,foldl1,foldr,foldr1,fromDouble,fromEnum,fromInt,fromInteger, - fromRational,fst,gcd,getChar,getContents,getLine,head,id,inRange,index,init,intToDigit, - interact,ioError,isAlpha,isAlphaNum,isAscii,isControl,isDenormalized,isDigit,isHexDigit, - isIEEE,isInfinite,isLower,isNaN,isNegativeZero,isOctDigit,isPrint,isSpace,isUpper,iterate, - last,lcm,length,lex,lexDigits,lexLitChar,lines,log,logBase,lookup,map,mapM,mapM_,max, - maxBound,maximum,maybe,min,minBound,minimum,mod,negate,not,notElem,numerator,odd, - or,pi,primExitWith,print,product,properFraction,putChar,putStr,putStrLn,quot, - quotRem,range,rangeSize,read,readDec,readFile,readFloat,readHex,readIO,readInt,readList,readLitChar, - readLn,readOct,readParen,readSigned,reads,readsPrec,realToFrac,recip,rem,repeat,replicate, - reverse,round,scaleFloat,scanl,scanl1,scanr,scanr1,seq,sequence,sequence_,show,showChar,showInt, - showList,showLitChar,showParen,showSigned,showString,shows,showsPrec,significand,signum,sin, - sinh,snd,span,splitAt,sqrt,subtract,succ,sum,tail,take,takeWhile,tan,tanh,threadToIOResult,toEnum, - toInt,toInteger,toLower,toRational,toUpper,truncate,uncurry,undefined,unlines,until,unwords,unzip, - unzip3,userError,words,writeFile,zip,zip3,zipWith,zipWith3,listArray,doParse,for,initTo, + emph= + {[1] + FilePath,IOError,abs,acos,acosh,and,any,appendFile,approxRational,asTypeOf,asin, + asinh,atan,atan2,atanh,basicIORun,break,catch,ceiling,chr,compare,concat,concatMap, + const,cos,cosh,curry,cycle,decodeFloat,denominator,digitToInt,div,divMod,drop, + dropWhile,either,elem,encodeFloat,enumFrom,enumFromThen,enumFromThenTo,enumFromTo, + error,even,exp,exponent,fail,filter,flip,floatDigits,floatRadix,floatRange,floor, + fmap,foldl,foldl1,foldr,foldr1,fromDouble,fromEnum,fromInt,fromInteger, + fromRational,fst,gcd,getChar,getContents,getLine,head,id,inRange,index,init,intToDigit, + interact,ioError,isAlpha,isAlphaNum,isAscii,isControl,isDenormalized,isDigit,isHexDigit, + isIEEE,isInfinite,isLower,isNaN,isNegativeZero,isOctDigit,isPrint,isSpace,isUpper,iterate, + last,lcm,length,lex,lexDigits,lexLitChar,lines,log,logBase,lookup,map,mapM,mapM_,max, + maxBound,maximum,maybe,min,minBound,minimum,mod,negate,not,notElem,numerator,odd, + or,pi,primExitWith,print,product,properFraction,putChar,putStr,putStrLn,quot, + quotRem,range,rangeSize,read,readDec,readFile,readFloat,readHex,readIO,readInt,readList,readLitChar, + readLn,readOct,readParen,readSigned,reads,readsPrec,realToFrac,recip,rem,repeat,replicate, + reverse,round,scaleFloat,scanl,scanl1,scanr,scanr1,seq,sequence,sequence_,show,showChar,showInt, + showList,showLitChar,showParen,showSigned,showString,shows,showsPrec,significand,signum,sin, + sinh,snd,span,splitAt,sqrt,subtract,succ,sum,tail,take,takeWhile,tan,tanh,threadToIOResult,toEnum, + toInt,toInteger,toLower,toRational,toUpper,truncate,uncurry,undefined,unlines,until,unwords,unzip, + unzip3,userError,words,writeFile,zip,zip3,zipWith,zipWith3,listArray,doParse,for,initTo, create,get,set,div,rescale,add,delete,insert,prop_focus_left_master,average,best,insert,union,split,size,fromList,copy,group,good,bad,foo,explode,singleton,difference,fromJust,sort,unfold, target, query, decode, encode, check, refuteSMT, binder, - subst,unapply,apply,proxy,refinement,fresh,guard,constrain,oneOf, + subst,unapply,apply,proxy,refinement,fresh,guard,constrain,oneOf, queryList,queryCtor,queryField,ctors,decodeCtor,whichOf,ctorArity,eval, - mkCtor,gCtors,gEncode,gEncodeFields,gDecode,gDecodeFields,reproxyRep,empty,splitCtor,checkField,scanM, + mkCtor,gCtors,gEncode,gEncodeFields,gDecode,gDecodeFields,reproxyRep,empty,splitCtor,checkField,scanM, padAverage,focusUp,execute,checkSMT,inputTypes,outputType,toReft,app - %, inTypes, inputTypes, outputType, execute, smtFindModel, smtRefuteModel - }, - emphstyle={[1]\color{haskellblue}}, - emph= - {[2] - OkMap,OkRBT,OkStackSet,TTrue,Map,Bool,Char,Double,Either,Float,IO,Integer,Int,Maybe,Ordering,Rational,Ratio,ReadS,ShowS,String,Word8,Nat,Pos,Rng,Score, + %, inTypes, inputTypes, outputType, execute, smtFindModel, smtRefuteModel + }, + emphstyle={[1]\color{haskellblue}}, + emph= + {[2] + OkMap,OkRBT,OkStackSet,TTrue,Map,Bool,Char,Double,Either,Float,IO,Integer,Int,Maybe,Ordering,Rational,Ratio,ReadS,ShowS,String,Word8,Nat,Pos,Rng,Score, Ptr,ForeignPtr,CSize,InPacket,Tree,Prop,TreeEq,TreeLt,Vec, NullTerm,IncrList,DecrList,UniqList,BST,MinHeap,MaxHeap, PtrN,ByteStringN,ByteStringEq,VO,ByteStringsEq,ByteStringNE,OrdList,Var,RType,Constrain,Gen,Var,Proxy,SMT,Targetable,RefType,Refinement,Ctor,C1,Rep,Rec0,U1, GCtors,GDecode,GDecodeFields,GEncode,GEncodeFields,OrdMap,MinusKey, len,isBH,isBal,bh,isRB,keys,List,Sorted,RBT,Col,isBlack,OrdRBT,Set,sz, StackSet,NoDuplicates,Data,RBTree,XMonad,Generic,true - }, - emphstyle={[2]\color{castanho_ulisses}}, - emph= - {[3] - case,class,data,deriving,do,else,if,return,def,import,in,infixl,infixr,instance,let,tmapM,for2M,forM,zipWithM,otherwise, - module,measure,pred,predicate,of,primitive,then,type,where,lazy,throw,when - }, - emphstyle={[3]\color{preto_ulisses}\textbf}, - emph= - {[4] - quot,rem,div,mod,elem,notElem,seq - }, - emphstyle={[4]\color{castanho_ulisses}\textbf}, - emph= - {[5] - PS,Tip,Node,Black,Red,EQ,False,GT,Just,LT,Left,Nothing,Right,True,Show,Eq,Ord,Num,C,N,Leaf,Bin,CounterExample - }, - emphstyle={[5]\color{green_ulisses}}, - emph= - {[6] - patError, irrefutPatError, nonExhaustiveGuardsError, recSelError, errorOut, - noMethodBinding - }, - emphstyle={[6]\color{haskellred}} + }, + emphstyle={[2]\color{castanho_ulisses}}, + emph= + {[3] + case,class,data,deriving,do,else,if,return,def,import,in,infixl,infixr,instance,let,tmapM,for2M,forM,zipWithM,otherwise, + module,measure,pred,predicate,of,primitive,then,type,where,lazy,throw,when + }, + emphstyle={[3]\color{preto_ulisses}\textbf}, + emph= + {[4] + quot,rem,div,mod,elem,notElem,seq + }, + emphstyle={[4]\color{castanho_ulisses}\textbf}, + emph= + {[5] + PS,Tip,Node,Black,Red,EQ,False,GT,Just,LT,Left,Nothing,Right,True,Show,Eq,Ord,Num,C,N,Leaf,Bin,CounterExample + }, + emphstyle={[5]\color{green_ulisses}}, + emph= + {[6] + patError, irrefutPatError, nonExhaustiveGuardsError, recSelError, errorOut, + noMethodBinding + }, + emphstyle={[6]\color{haskellred}} } %%%ORIG